Relax CEI analysis to prevent false positive warnings#29576
Conversation
This change rewrites the ordering part of the CEI analysis to focus specifically on storage access instead of broad categories of operations. We reframe Read and Write to mean specifically "touches mutable persistent state another program's finalize could observe or modify," and drop strictly ordering based lints. Cross-layer taint is unchanged.
f82850d to
81d6f66
Compare
4b0944a to
d442799
Compare
| } | ||
| let variant = func.function.variant; | ||
| let block = func.function.block.clone(); | ||
| let s = if block.statements.is_empty() { |
There was a problem hiding this comment.
The empty-body check also matches a user-written final fn helper() {}. Is this a problem?
|
|
||
| // FP4: suppress per-statement warnings inside a body that has | ||
| // already fired the loop-level warning. | ||
| let new_suppress = mixed || self.suppress; |
There was a problem hiding this comment.
Once a loop is flagged mixed, this suppresses all the specific warnings inside it. I would think this is unwanted.
| let ast = std::mem::take(&mut state.ast); | ||
| let mut scanner = Scanner::new(state); | ||
| match &ast { | ||
| Ast::Program(p) => scanner.visit_program(p), |
There was a problem hiding this comment.
This scans library ASTs, but the deleted finalize visitor and the sibling cross_layer_taint phase both skip them. Intended, or should libraries be skipped here too?
| let body_summary = { | ||
| let mut s = Summary::default(); | ||
| let prog = self.program; | ||
| let stmts = it.block.statements.clone(); |
There was a problem hiding this comment.
Is this clone necessary? Can we just change iterate in place in the loop below?
| return Summary::default(); | ||
| } | ||
| let variant = func.function.variant; | ||
| let block = func.function.block.clone(); |
There was a problem hiding this comment.
Can we explore other possibilities to avoid this deep clone?
| if let Some(intr) = Intrinsic::from_symbol(i.name, &i.type_parameters) | ||
| && let Some(op) = classify_intrinsic(&intr) | ||
| { | ||
| let desc = format!("a call to `{}`", i.name); |
There was a problem hiding this comment.
Do we really need to format! here? Seems a bit wasteful.
| // each as a fresh finalize context. Non-async code in the transition | ||
| // body is proof-context and outside CEI's remit. | ||
|
|
||
| fn scan_entrypoint(&mut self, b: &Block) { |
There was a problem hiding this comment.
This whole feels like it would be done with a Visitor but I could be wrong.
| } | ||
|
|
||
| // CEI warning codes (must match `errors/cei_analyzer.rs`). | ||
| const CODE_CHECK: i32 = 13000; |
There was a problem hiding this comment.
Do these really need to be exactly the same error code? Could these 4 not be merged into an enum? They seem to be only used for deduplication
2 participants
This change rewrites the ordering part of the CEI analysis to focus specifically on storage access instead of broad categories of operations.
We reframe Read and Write to mean specifically "touches mutable persistent state another program's finalize could observe or modify," and drop strictly ordering based lints.
Cross-layer taint is unchanged.