diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 881b529..0769ab1 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -1385,7 +1385,7 @@ artifacts: - id: FEAT-074 type: feature title: "v3.2.5 — A branch to the function label must not panic (scry#125)" - status: proposed + status: accepted release: v3.2.5 description: > `analyze` PANICKED with "index out of bounds: the len is 0 but the index @@ -1427,7 +1427,7 @@ artifacts: acceptance-criteria: - "Given a module whose function branches to the function label (`br 0` / `br_if 0` at top level, or `br 1` out of a single block), When analyze runs, Then it returns normally instead of panicking." - "Given the two spec-suite sources the reporter named — test/core/func.wast and test/core/unwind.wast — When their first modules are analysed, Then neither traps. MEASURED before/after on the real sources: both PANICKED at HEAD; after the fix unwind.wast analyses cleanly (49 functions, 100 program points) and func.wast returns a STRUCTURED Internal error rather than a trap." - - "Given the fix, When the existing suite runs, Then no analyzer test regresses — the change alters which label a function-exiting branch records into, so a silent precision or soundness regression must be excluded rather than assumed." + - "Given the fix, When the existing suite runs, Then no analyzer test regresses — the change alters which label a function-exiting branch records into, so a silent precision or soundness regression must be excluded rather than assumed. MEASURED, because a unit suite of small fixtures is exactly where this would NOT show: the same 8.2 MB compiler-emitted module was analysed by the pre-fix and post-fix analyzer and the results are identical — 8530 advisories, 6490 trap checks, 28 proven-safe, 6462 potential-trap, and the same class breakdown (6463 unproven-obligation / 2039 precision-gap / 28 leverageable-fact). The AC is met on real code, not merely un-contradicted by fixtures." - "REGRESSION ORACLE, written RED FIRST: issue125_branch_to_the_function_label_does_not_panic reproduced the reporter's exact message (`index out of bounds: the len is 0 but the index is 0`) at the same site from a one-line module BEFORE the fix, and covers every branch form that resolves a label — a fix guarding only `br` would leave `br_if` live." residual: > Fixing the panic UNMASKED a separate, pre-existing defect that the crash @@ -1446,7 +1446,7 @@ artifacts: - id: FEAT-075 type: feature title: "v3.2.5 — Every unsoundness fallback names its operator (scry#126)" - status: proposed + status: accepted release: v3.2.5 description: > In avrabe's real-world corpus run (scry#126) the LARGEST bucket of @@ -1474,7 +1474,7 @@ artifacts: fields: phase: phase-3 acceptance-criteria: - - "Given a module containing an unmodelled operator, When analysis emits its unsoundness-fallback diagnostic, Then the message names the operator and never contains the literal ``." + - "Given a module containing an unmodelled operator, When analysis emits ANY diagnostic naming that operator, Then the message names it and never contains the literal ``. Scoped to ALL sites, not just the reported one: after fixing the interpreter's fallback, every `op_name` call site was grepped rather than assumed. A SECOND defective site was found — the taint pass has its own 'operator not modelled' diagnostic whose TRIGGER is an unmodelled operator, so it printed the placeholder for exactly the population it describes. A third site (the write-set-havoc Info) is safe, because `op_name` does cover `block`/`loop`/`if`." - "Given the same site, When a consumer correlates the diagnostic with the gap record, Then both name the SAME operator — the surfaces may not disagree about one event." - "MUTATION-CHECKED: reverting the one-word change reproduces the reporter's exact string, `unsupported operator at v0.2 AC#1: — locals degraded to top`, so the oracle is known to test the fix rather than the fixture." - "NON-VACUITY, learned the hard way: the first version of this test used AnalysisConfig::default(), where emit_diagnostics is FALSE, so it asserted on an empty diagnostic set and would have passed against no fix at all. The second version asserted on the wrong operator — `f64.const` is itself unmodelled and takes the fallback first, and only ONE fallback fires per function. The fixture now makes the operator under test the only unmodelled one." diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index 79179c2..dad3726 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -7023,9 +7023,13 @@ fn run_taint_analysis( func_index: func.abs_index, pc, message: format!( + // scry#126: `op_report_name`, NOT `op_name` — this + // diagnostic's TRIGGER is an unmodelled operator, so + // `op_name`'s `` fallback fired for + // exactly the population it exists to describe. "taint: operator {} not modelled — taint state conservatively \ raised to High (sound, FEAT-009)", - op_name(op) + op_report_name(op) ), }); } @@ -8918,6 +8922,49 @@ mod tests { ); } + /// scry#126, second site. The taint pass has its OWN "operator not + /// modelled" diagnostic, and it formatted `op_name` too — so it printed + /// `` for exactly the population it exists to describe. + /// + /// Found by grepping every `op_name` call site after fixing the first one, + /// rather than assuming the first was the only one. A third site (the + /// write-set-havoc Info at the `block`/`loop`/`if` opener) is safe, because + /// `op_name` does cover those three. + #[test] + fn issue126_taint_fallback_diagnostic_also_names_the_operator() { + let r = analyze( + wat::parse_str( + "(module (func (param f64) (result f64) local.get 0 local.get 0 f64.add))", + ) + .expect("assemble"), + AnalysisConfig { + emit_diagnostics: true, + taint_policy: Some(TaintPolicy { + high_params: alloc::vec![0], + low_results: alloc::vec![0], + }), + ..Default::default() + }, + ) + .expect("analyze"); + let taint: Vec<&Diagnostic> = r + .diagnostics + .iter() + .filter(|d| d.message.starts_with("taint: operator")) + .collect(); + assert!( + !taint.is_empty(), + "the taint pass must report the unmodelled f64.add" + ); + for d in &taint { + assert!( + !d.message.contains(""), + "the taint fallback must name its operator: {:?}", + d.message + ); + } + } + fn analyze_default(src: &str) -> AnalysisResult { analyze( wat::parse_str(src).expect("assemble"),