v3.2.5: second <unsupported> site, AC#3 measured, and promote FEAT-074/075

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 `<unsupported>`."
+        - "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 `<unsupported>`. 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: <unsupported> — 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."

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 `<unsupported>` 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
+    /// `<unsupported>` 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("<unsupported>"),
+                "the taint fallback must name its operator: {:?}",
+                d.message
+            );
+        }
+    }
+
     fn analyze_default(src: &str) -> AnalysisResult {
         analyze(
             wat::parse_str(src).expect("assemble"),