From 289304caedabe00730344d2aafc8f7805f1fc6d0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 18:39:47 +0200 Subject: [PATCH 1/5] feat(#912): MC/DC structural coverage over synth's own decision logic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RQ-57-MCDC. #912 sat N/A for six releases on a surface argument: `witness` measures MC/DC on a Wasm artifact and synth emits ARM/RV32/A64 machine code, so "run witness on synth's output" is a category error. That is true about synth's OUTPUT and irrelevant — the decisions that ship a miscompile are in synth's own Rust, and those compile to Wasm fine. SURFACE, chosen on evidence (scripts/repro/mcdc_912_gate.md): * REJECTED native LLVM MC/DC — not a preference, the capability was REMOVED from rustc (rust-lang/rust#144999, merged 2025-08-08, Rust 1.91). Probed on three nightlies: `mcdc` is rejected, only `block|branch|condition` accepted. `condition` is the trap in the family — it builds, and it emits ZERO `llvm.instrprof.mcdc.*` intrinsics and zero mcdc_records. * REJECTED witness-over-the-fixtures-synth-compiles — it measures the fixture. gale's run named `pad_integral`, `do_count_chars`, `::fmt`, `write_prefix`, `cabi_realloc` and ZERO synth functions. A surface whose gap rows cannot name a synth decision cannot notice a missing condition in one. * CHOSEN witness over a wasm32-wasip1 build of synth's OWN crates. `synth-mcdc-harness` is a thin row driver — it calls the REAL pub fns with inputs arriving through Wasm params; it re-implements no predicate. THE RIGHT PARTS — scored where a missed condition HAS shipped a bug here: static_data_addr (VCR-VER-003 #777/#757/#798), alloc_validator (VCR-RA-003 #815; #871's fix WAS a condition added to the save-set predicate), and the RV32 bounds gate (#953/#959 — `mem_size == 0` was exempt from the power-of-two check, so `(memory 0)` emitted an identity mask and every access ran unmasked). EXCLUDED and named: instruction_selector (225 operator lines, its own lane); the aarch64 bounds closures (#865 — residual); wcet declines (match-dispatch, 1 operator line in 1061, so MC/DC has nothing to say there). MEASURED 20 decisions / 144 conditions / 63 proved / 31 gap / 50 dead, 3 at full MC/DC. Identical under witness 0.28.0 and 0.42.0. Gap rows are PRINTED with the closing vector — `is_ret` went 3-gap to 0-gap by adding exactly the three vectors witness named. THE GATE SCORES BY FUNCTION AND FLOORS COUNTS, for three reasons: the module-wide figure is 3/770 because wasip1 links wasi-libc + std; witness's `source_file` is an inlined-DWARF BASENAME and misattributes (resolve_owner's decision reports as static_data_addr.rs:355, it is at :274 — witness#179); and a ratio cannot notice a DELETED condition, which makes the percentage improve. RED-FIRST, two mutations, two distinct failure paths, both restored byte-identical: (a) delete `|| rs2 == Reg::RA` (the #871 fix) -> 19/142/54/2, all four floors trip; the condition-COUNT drop is what a ratio cannot produce. (b) drop one truth-table row (ra_validate:14) -> conditions stay 144, proved 63->62 and fully-proved 3->2. Wired as the `mcdc-structural-coverage` CI job, witness pinned to v0.42.0, with a non-vacuity assert so an empty scored table cannot print PASS. Refs #912 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 105 +++++ Cargo.lock | 8 + Cargo.toml | 1 + crates/synth-mcdc-harness/Cargo.toml | 19 + crates/synth-mcdc-harness/src/lib.rs | 635 +++++++++++++++++++++++++++ scripts/mcdc_gate.py | 241 ++++++++++ scripts/mcdc_run.sh | 121 +++++ scripts/repro/mcdc_912_gate.md | 196 +++++++++ 8 files changed, 1326 insertions(+) create mode 100644 crates/synth-mcdc-harness/Cargo.toml create mode 100644 crates/synth-mcdc-harness/src/lib.rs create mode 100644 scripts/mcdc_gate.py create mode 100644 scripts/mcdc_run.sh create mode 100644 scripts/repro/mcdc_912_gate.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 59ea6bcb..dc050959 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3566,3 +3566,108 @@ jobs: run: | set -euo pipefail python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 5 + + mcdc-structural-coverage: + name: MC/DC structural coverage over synth's decision logic (RQ-57-MCDC, #912) + # #912 asked for MC/DC and sat N/A for six releases on a SURFACE argument: + # `witness` measures MC/DC on a Wasm artifact and synth emits ARM/RV32/A64 + # machine code, so "run witness on synth's output" is a category error. + # True about the OUTPUT — and irrelevant, because the decisions that ship a + # miscompile are in synth's own Rust, which compiles to Wasm fine. + # + # This job builds `synth-mcdc-harness` (a thin ROW DRIVER — it calls the + # REAL pub fns, it re-implements nothing) for wasm32-wasip1, drives one + # truth-table row per `witness run --invoke-with-args`, and scores the + # result over synth's OWN functions only. + # + # WHY THE MODULE-WIDE PERCENTAGE IS NOT THE GATE: a wasip1 link drags in + # wasi-libc and Rust std, so the raw figure is `3/770 full MC/DC` and says + # nothing about synth. And a ratio cannot notice a DELETED condition — + # removing one makes the percentage IMPROVE. scripts/mcdc_gate.py scores by + # DEMANGLED FUNCTION (witness's source_file is an inlined-DWARF basename and + # is unreliable — upstream witness#179) and floors COUNTS. + # + # RED-FIRST (verified locally before this job was written, both mutations + # restored byte-identical afterwards): + # (a) delete the #871 condition `|| rs2 == Reg::RA` from the RV32 + # allocation validator -> 20/144/63/3 becomes 19/142/54/2; all four + # floors trip. The CONDITION-COUNT drop is the signal a ratio misses. + # (b) drop ONE truth-table row (`ra_validate:14`) -> conditions stay 144 + # but proved falls 63->62 and fully-proved decisions 3->2. Two + # mutations, two distinct failure paths. + # + # PINNED: witness v0.42.0 and the workspace's stable toolchain. The scored + # numbers were identical under witness 0.28.0 and 0.42.0 (14 minor versions + # apart), so the measurement is not tracking the tool's phrasing. If a + # toolchain bump changes std inlining and moves the counts, RE-MEASURE and + # state the new baseline — never lower a floor to go green. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + with: + targets: wasm32-wasip1 + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install witness (pinned) + env: + GH_TOKEN: ${{ github.token }} + run: | + set -euo pipefail + mkdir -p "$HOME/.witness" + gh release download v0.42.0 --repo pulseengine/witness \ + --pattern 'witness-v0.42.0-x86_64-unknown-linux-gnu.tar.gz' \ + --dir "$HOME/.witness" + tar xzf "$HOME/.witness"/witness-v0.42.0-*.tar.gz -C "$HOME/.witness" + "$HOME/.witness/witness" --version + # The row drivers must reach the outcomes their doc comments claim. A + # driver that returned one verdict for every row would make the whole + # MC/DC run vacuous while still printing a number. + - name: Row-driver sanity gate (host) + run: cargo test -p synth-mcdc-harness + - name: Run the MC/DC rows under witness + run: WITNESS="$HOME/.witness/witness" ./scripts/mcdc_run.sh target/mcdc + - name: Score synth's own decisions against the declared floors + run: | + set -euo pipefail + python3 scripts/mcdc_gate.py target/mcdc | tee /tmp/mcdc.log + # Non-vacuity: the gate must have SCORED something. A scoping change + # that matched zero functions would otherwise print an empty table + # and fail the floors for the wrong reason — or, worse, a future + # `--report-only` slip would print PASS over nothing. + grep -qE '^TOTAL +[0-9]+' /tmp/mcdc.log + grep -q '^PASS: all MC/DC floors met' /tmp/mcdc.log + - name: Publish the truth tables and gap rows + if: always() + run: | + { + echo "### MC/DC over synth's own decision logic (#912)" + echo + echo "Scored by DEMANGLED FUNCTION, not by file — witness's" + echo "\`source_file\` is an inlined-DWARF basename (witness#179)." + echo "The module-wide percentage is NOT this gate: a wasip1 link" + echo "pulls in wasi-libc + std." + echo + echo '```' + cat /tmp/mcdc.log 2>/dev/null || echo "(gate did not run)" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" + - uses: actions/upload-artifact@v7 + if: always() + with: + name: mcdc-evidence + path: | + target/mcdc/report.txt + target/mcdc/report.json + target/mcdc/rollup.txt diff --git a/Cargo.lock b/Cargo.lock index 8f58c93b..1de8af4a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1237,6 +1237,14 @@ dependencies = [ "wit-parser", ] +[[package]] +name = "synth-mcdc-harness" +version = "0.56.2" +dependencies = [ + "synth-backend-riscv", + "synth-core", +] + [[package]] name = "synth-memory" version = "0.56.2" diff --git a/Cargo.toml b/Cargo.toml index fca00cea..980aaf4a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -18,6 +18,7 @@ members = [ "crates/synth-backend-wasker", "crates/synth-backend-riscv", "crates/synth-backend-aarch64", + "crates/synth-mcdc-harness", ] resolver = "2" diff --git a/crates/synth-mcdc-harness/Cargo.toml b/crates/synth-mcdc-harness/Cargo.toml new file mode 100644 index 00000000..fe538cbc --- /dev/null +++ b/crates/synth-mcdc-harness/Cargo.toml @@ -0,0 +1,19 @@ +[package] +name = "synth-mcdc-harness" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +authors.workspace = true +license.workspace = true +repository.workspace = true +publish = false + +[lib] +# `cdylib` is what `wasm32-wasip1` needs to emit exported functions; `rlib` +# keeps the crate cheap to build on the host so `cargo test --workspace`, +# clippy and fmt still see it. +crate-type = ["cdylib", "rlib"] + +[dependencies] +synth-core = { path = "../synth-core" } +synth-backend-riscv = { path = "../synth-backend-riscv" } diff --git a/crates/synth-mcdc-harness/src/lib.rs b/crates/synth-mcdc-harness/src/lib.rs new file mode 100644 index 00000000..0d61058b --- /dev/null +++ b/crates/synth-mcdc-harness/src/lib.rs @@ -0,0 +1,635 @@ +//! RQ-57-MCDC (#912) — MC/DC row drivers for synth's OWN decision logic. +//! +//! # Why this crate exists +//! +//! #912 asked for MC/DC structural coverage and sat N/A for six releases on a +//! surface argument: `witness` measures MC/DC on a **Wasm** artifact, synth +//! **emits ARM/RV32/A64 machine code**, so "run witness on synth's output" is a +//! category error. That argument is correct about synth's *output* and wrong +//! about synth's *input*: the decisions that ship a miscompile are the ones in +//! synth's own Rust — the decline predicates, the guard-emission conditions, +//! the validator accept/reject tests. Those compile to Wasm perfectly well. +//! +//! So this crate is a thin **row driver**: it builds for `wasm32-wasip1`, +//! links the REAL synth crates, and calls the REAL `pub fn`s with inputs that +//! arrive through Wasm parameters (never constant-folded). `witness` then +//! reconstructs the MC/DC truth table and attributes every decision to synth's +//! own source line. Nothing here re-implements a predicate — a mirror would be +//! exactly the vacuous-gate class this measurement is meant to catch. +//! +//! # Why not the other two surfaces +//! +//! * **Native LLVM MC/DC via `-Zcoverage-options=mcdc`** — REMOVED from rustc +//! in rust-lang/rust#144999 (merged 2025-08-08, Rust 1.91). Every installed +//! nightly rejects the value; `condition` (what replaced it in the accepted +//! set) emits zero MC/DC intrinsics and zero `mcdc_records`. Not a +//! preference — the capability is gone from the compiler. +//! * **`witness` over the Wasm fixtures synth COMPILES** — measures the +//! fixture, not synth. gale's run on a real dissolved module named its gap +//! rows `core::fmt::Formatter::pad_integral`, `core::str::count:: +//! do_count_chars`, `::fmt`, `pad_integral::write_prefix`, +//! `wit_bindgen::rt::cabi_realloc` — five stdlib/bindgen frames and zero +//! synth functions. A surface whose gap rows cannot name a synth decision +//! cannot notice a missing condition in one. +//! +//! # Reading the numbers +//! +//! The module-wide percentage is meaningless here: a `wasm32-wasip1` link +//! pulls in wasi-libc (`malloc.c`, `stpcpy.c`, …) and Rust `std` +//! (`panicking.rs`, `mod.rs`, …), which contribute hundreds of never-evaluated +//! conditions. `scripts/mcdc_gate.py` therefore scores ONLY synth's own source +//! files and reports per-file counts, not a ratio. See that script for the +//! declared floor. +//! +//! Every export takes its varying inputs as Wasm parameters and returns an +//! `i32` so `witness run --invoke-with-args` can drive one truth-table row per +//! invocation. + +use synth_backend_riscv::alloc_validator::{RaFinalVerdict, validate_final_allocation_rv32}; +use synth_backend_riscv::backend::RiscVBackend; +use synth_backend_riscv::register::Reg; +use synth_backend_riscv::riscv_op::RiscVOp; +use synth_core::backend::{Backend, CompileConfig, SafetyBounds}; +use synth_core::static_data_addr::{ + DataSegment, ImageVerdict, PackedInit, RelocResolution, Verdict, resolve_owner, + validate_reloc_resolutions_spanned, validate_served_image, +}; +use synth_core::target::TargetSpec; +use synth_core::wasm_op::WasmOp; + +// ════════════════════════════════════════════════════════════════════════ +// Class 1 — VALIDATOR ACCEPT/REJECT: `synth_core::static_data_addr` +// VCR-VER-003 (#777), the validator that hard-errors the #757 wrong-segment +// miscompile. A missed condition here green-washes a silent miscompile. +// ════════════════════════════════════════════════════════════════════════ + +/// Two overlapping active segments at the same linear-memory offset — the #757 +/// shape. `1` is declared later, so later-wins makes it the owner. +fn overlapping_segments() -> Vec { + vec![ + DataSegment { + linmem_off: 0x100, + bytes: vec![0x11, 0x22, 0x33, 0x44], + }, + DataSegment { + linmem_off: 0x100, + bytes: vec![0xAA, 0xBB, 0xCC, 0xDD], + }, + ] +} + +/// Drives `static_data_addr::resolve_owner`'s membership decision +/// `c >= off && c < off + len` (the `.rposition()` / `.position()` tie-break +/// that IS the #757 fix). `c` arrives through a Wasm parameter, so the +/// comparison is evaluated at run time. +/// +/// Rows: `c` below the segment (c0=F), inside it (c0=T,c1=T), above it +/// (c0=T,c1=F). `last_wins` selects which of the two search call sites runs. +/// +/// `nseg` matters for the MEASUREMENT, not for the predicate: `witness` records +/// ONE truth-table row per invocation, so a decision evaluated once per +/// iteration of a loop collapses to whichever evaluation the row captures. +/// With `nseg == 1` the membership test runs EXACTLY ONCE per call, which is +/// what makes distinct condition vectors observable. `nseg == 2` is the #757 +/// overlapping shape and is driven for behaviour, not for vectors. +#[unsafe(no_mangle)] +pub extern "C" fn sd_resolve_owner(c: i32, last_wins: i32, nseg: i32) -> i32 { + let mut segs = overlapping_segments(); + if nseg <= 1 { + segs.truncate(1); + } + match resolve_owner(&segs, c as u32, last_wins != 0) { + Some(r) => (r.seg_index as i32) * 1000 + r.addend as i32, + None => -1, + } +} + +/// Drives `validate_reloc_resolutions_spanned`'s span-tolerance decision +/// `j == 0 && seg.bytes.get(addend) != Some(&runtime_byte)` (phase 2 of #777: +/// the multi-byte access straddle). +/// +/// `seg_index` picks the emitted owner K — `0` is the #757 miscompile (the +/// stale earlier segment), `1` is the correct later-wins owner. `addend` +/// walks the span. Together they reach both the `j == 0` short-circuit +/// (c0=F on every `j > 0` iteration) and both outcomes of the byte compare. +#[unsafe(no_mangle)] +pub extern "C" fn sd_validate_spanned(seg_index: i32, addend: i32) -> i32 { + let segs = overlapping_segments(); + let packed_off = [0u32, 4u32]; + let blob: Vec = vec![0x11, 0x22, 0x33, 0x44, 0xAA, 0xBB, 0xCC, 0xDD]; + let packed = PackedInit { + seg_packed_off: &packed_off, + bytes: &blob, + }; + let res = vec![RelocResolution { + seg_index: seg_index as usize, + addend: addend as u32, + label: "row".to_string(), + }]; + match validate_reloc_resolutions_spanned(&segs, &res, &packed) { + Verdict::Consistent => 0, + Verdict::Mismatch(m) => m.len() as i32, + } +} + +/// Drives `validate_served_image`'s beyond-image decision +/// `addr >= image.len() && owed != 0` — the #798 gate that caught the silent +/// initializer drop on the pre-#798 RV32 path. +/// +/// `image_len` truncates the served blob (0 = "ships no initializer bytes at +/// all"); `trailing_zero` appends a runtime byte whose value IS zero past the +/// image, which is the only way to reach `c0=T, c1=F`. +#[unsafe(no_mangle)] +pub extern "C" fn sd_validate_served(image_len: i32, trailing_zero: i32) -> i32 { + let mut segs = vec![DataSegment { + linmem_off: 0, + bytes: vec![0x01, 0x02, 0x03, 0x04], + }]; + if trailing_zero != 0 { + // A runtime-covered byte beyond the image whose owed value is 0. + segs.push(DataSegment { + linmem_off: 8, + bytes: vec![0x00, 0x00], + }); + } + let full = [0x01u8, 0x02, 0x03, 0x04]; + let n = (image_len.max(0) as usize).min(full.len()); + match validate_served_image(&segs, &full[..n]) { + ImageVerdict::Consistent => 0, + ImageVerdict::Mismatch(m) => m.len() as i32, + } +} + +// ════════════════════════════════════════════════════════════════════════ +// Class 2 — VALIDATOR ACCEPT/REJECT: RV32 register-allocation validator +// VCR-RA-003 (#815). #871 shipped an unsaved-`ra` miscompile: a non-leaf +// function returning into its own call site. The fix is literally a +// CONDITION added to this validator's save-set predicate, which is exactly +// what MC/DC is for. +// ════════════════════════════════════════════════════════════════════════ + +/// Build one RV32 instruction stream per `shape`, chosen so the whole set +/// covers every condition of the validator's compound decisions: +/// `sp_slot_store(ins) && (is_saved_by_pass(rs2) || rs2 == RA)`, +/// `op_dest(ins) && is_saved_by_pass(rd)`, +/// the epilogue reload guard `is_saved_by_pass(rd) || rd == RA`, +/// the segment walk `i < len && is_straight_line(instrs[i])`, +/// and `is_saved_by_pass`'s own `n == 9 || (18..=26).contains(&n)`. +fn ra_shape(shape: i32) -> Vec { + let ret = RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 0, + }; + match shape { + // Leaf, writes only a temp: no save needed, no violation. + // is_saved_by_pass(t0=5): c0=F, c1=F. + 0 => vec![ + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 1, + }, + ret, + ], + // Saves + writes + restores s1 (reg 9): is_saved_by_pass c0=T. + 1 => vec![ + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::S1, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::S1, + rs1: Reg::ZERO, + imm: 7, + }, + RiscVOp::Lw { + rd: Reg::S1, + rs1: Reg::SP, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: 16, + }, + ret, + ], + // Writes s1 with NO save — the #490 callee-saved clobber. + 2 => vec![ + RiscVOp::Addi { + rd: Reg::S1, + rs1: Reg::ZERO, + imm: 7, + }, + ret, + ], + // Non-leaf with `ra` saved and restored — #871 green. + // Exercises `rs2 == RA` (the `||` right arm) on both halves. + 3 => vec![ + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::RA, + imm: 12, + }, + RiscVOp::Call { + label: "func_1".to_string(), + }, + RiscVOp::Lw { + rd: Reg::RA, + rs1: Reg::SP, + imm: 12, + }, + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: 16, + }, + ret, + ], + // Non-leaf that never saves `ra` — the #871 miscompile itself. + 4 => vec![ + RiscVOp::Call { + label: "func_1".to_string(), + }, + ret, + ], + // Frame store of a NON-callee-saved register (t0): the store-side + // decision takes c0=T with both `||` arms false. + 5 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::T0, + imm: 4, + }, + ret, + ], + // Store whose base is NOT sp: `sp_slot_store` is None, so the + // let-chain's first condition is false and the `||` never evaluates. + 6 => vec![ + RiscVOp::Sw { + rs1: Reg::T0, + rs2: Reg::S1, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::SP, + rs1: Reg::SP, + imm: -16, + }, + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::S1, + imm: 0, + }, + RiscVOp::Lw { + rd: Reg::S1, + rs1: Reg::SP, + imm: 0, + }, + ret, + ], + // Saves s2 (reg 18) — the range arm of `n == 9 || (18..=26)`. + 7 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::X18, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::X18, + rs1: Reg::ZERO, + imm: 1, + }, + RiscVOp::Lw { + rd: Reg::X18, + rs1: Reg::SP, + imm: 0, + }, + ret, + ], + // A barrier mid-stream: the straight-line segment walk terminates on + // `is_straight_line == false` rather than on the length bound. + 8 => vec![ + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 1, + }, + RiscVOp::Label { + name: "L0".to_string(), + }, + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 2, + }, + ret, + ], + // Straight-line to the very end: the walk terminates on the LENGTH + // bound (`i < instrs.len()` false) with no barrier — the other + // unique-cause row for that decision. + 9 => vec![ + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 1, + }, + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::T0, + imm: 2, + }, + ], + // Spill-slot shadowing: two stores to one slot with no intervening + // reload, then a reload — the aliasing violation. + 10 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::T0, + imm: 8, + }, + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::X6, + imm: 8, + }, + RiscVOp::Lw { + rd: Reg::T0, + rs1: Reg::SP, + imm: 8, + }, + ret, + ], + // `is_ret` unique-cause rows: a `Jalr` that differs from `ret` in + // EXACTLY ONE field. `is_ret` is `matches!(op, Jalr{rd: ZERO, rs1: RA, + // imm: 0})`, which lowers to a 4-condition `br_if` chain — a shape + // source-level MC/DC cannot see at all, and one where a single wrong + // field silently reclassifies a terminator. + 11 => vec![RiscVOp::Jalr { + rd: Reg::T0, // link register written — NOT a return + rs1: Reg::RA, + imm: 0, + }], + 12 => vec![RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::T0, // indirect through a temp — NOT a return + imm: 0, + }], + 13 => vec![RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 4, // offset return — NOT the canonical `ret` + }], + // `sp_slot_load` with a non-sp base: a linear-memory load, not a + // frame reload. Pairs with the sp-relative loads above. + 14 => vec![ + RiscVOp::Lw { + rd: Reg::T0, + rs1: Reg::X8, + imm: 0, + }, + ret, + ], + // Every SEGMENT BARRIER `is_straight_line` knows about, so the match + // arms that are otherwise DEAD are evaluated. A dead condition is a + // condition the measurement cannot speak about at all. + 15 => vec![ + RiscVOp::Jal { + rd: Reg::ZERO, + label: "L0".to_string(), + }, + RiscVOp::Ecall, + RiscVOp::Ebreak, + RiscVOp::Mret, + RiscVOp::Wfi, + RiscVOp::Fence, + RiscVOp::Label { + name: "L0".to_string(), + }, + ret, + ], + // A saved register OUTSIDE the pass's save set on both sides of the + // range (`n == 9 || (18..=26)`): s0 (8) below, s11 (27) above. + 16 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::X8, + imm: 0, + }, + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::X27, + imm: 4, + }, + RiscVOp::Addi { + rd: Reg::X8, + rs1: Reg::ZERO, + imm: 1, + }, + RiscVOp::Addi { + rd: Reg::X27, + rs1: Reg::ZERO, + imm: 1, + }, + ret, + ], + // Top of the save range (s10 = 26) plus a write, saved and restored. + 17 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::X26, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::X26, + rs1: Reg::ZERO, + imm: 1, + }, + RiscVOp::Lw { + rd: Reg::X26, + rs1: Reg::SP, + imm: 0, + }, + ret, + ], + // Saved but NEVER restored before `ret` — the epilogue half of the + // callee-saved invariant (a different violation from shape 2). + 18 => vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::S1, + imm: 0, + }, + RiscVOp::Addi { + rd: Reg::T0, + rs1: Reg::ZERO, + imm: 1, + }, + ret, + ], + // `is_ret` is only reached from the epilogue scan, which runs ONLY when + // the save set is non-empty. 19–21 therefore carry a real save and end + // on a near-`ret` that differs in exactly ONE field, so the LAST + // `is_ret` evaluation of the invocation carries the unique-cause + // vector. (Shapes 11–13 reach the same variants through the store/def + // scans instead.) + 19..=21 => { + let near = match shape { + 19 => RiscVOp::Jalr { + rd: Reg::T0, + rs1: Reg::RA, + imm: 0, + }, + 20 => RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::T0, + imm: 0, + }, + _ => RiscVOp::Jalr { + rd: Reg::ZERO, + rs1: Reg::RA, + imm: 4, + }, + }; + vec![ + RiscVOp::Sw { + rs1: Reg::SP, + rs2: Reg::S1, + imm: 0, + }, + RiscVOp::Lw { + rd: Reg::S1, + rs1: Reg::SP, + imm: 0, + }, + near, + ] + } + // Empty stream. + _ => vec![], + } +} + +/// Drives `validate_final_allocation_rv32` over one shape. Returns +/// `0` = Ok, `1` = Violation, `2` = NotAttempted. +#[unsafe(no_mangle)] +pub extern "C" fn ra_validate(shape: i32) -> i32 { + match validate_final_allocation_rv32(&ra_shape(shape)) { + RaFinalVerdict::Consistent => 0, + RaFinalVerdict::Violation(_) => 1, + RaFinalVerdict::NotAttempted { .. } => 2, + } +} + +// ════════════════════════════════════════════════════════════════════════ +// Class 3 — GUARD EMISSION: the RV32 `--safety-bounds mask` size gate +// The #953/#959 sentinel-vs-value class, three consecutive releases. The +// shipped defect was a MISSING CONDITION in exactly this decision: `bytes +// == 0` was exempt from the power-of-two gate, so `(memory 0)` emitted an +// IDENTITY mask (0 - 1 = 0xFFFF_FFFF) and every access ran unmasked. +// ════════════════════════════════════════════════════════════════════════ + +/// Drives `synth_backend_riscv::backend::build_options`' bounds-mode gate +/// `mem_size == 0 || !mem_size.is_power_of_two()` through the public +/// `Backend::compile_function` entry point. +/// +/// Rows: `bytes = 0` (c0=T — the #959 identity-mask case, must refuse), +/// `bytes = 65536` (c0=F, c1=F — accept), `bytes = 196608` (c0=F, c1=T — the +/// #651 non-power-of-two refusal). +/// `mode = 3` swaps in a Cortex-M target so `ensure_supported_target`'s +/// family/ISA conjunction is evaluated with its conditions flipped — otherwise +/// every row shares one vector and those conditions stay gap. +#[unsafe(no_mangle)] +pub extern "C" fn rv_bounds_gate(mode: i32, bytes: i32) -> i32 { + let mut config = CompileConfig { + target: if mode == 3 { + TargetSpec::cortex_m4() + } else { + TargetSpec::riscv32imac() + }, + ..Default::default() + }; + config.safety_bounds = match mode { + 0 => SafetyBounds::None, + 1 => SafetyBounds::Software, + _ => SafetyBounds::Mask, + }; + config.linear_memory_bytes = bytes.max(0) as u32; + let ops = [WasmOp::I32Const(1), WasmOp::End]; + match RiscVBackend::new().compile_function("f", &ops, &config) { + Ok(_) => 0, + Err(_) => 1, + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// The row drivers must reach the outcomes their doc comments claim; a + /// driver that silently returns the same verdict for every row would make + /// the whole MC/DC run vacuous. Runs on the HOST (the wasm build is the + /// measured artifact, this is the sanity gate). + #[test] + fn rows_reach_distinct_outcomes() { + // resolve_owner: below / inside / above. + assert_eq!(sd_resolve_owner(0x50, 1, 2), -1); + assert_eq!(sd_resolve_owner(0x100, 1, 2), 1000); // later-wins owner = seg 1 + assert_eq!(sd_resolve_owner(0x100, 0, 2), 0); // first-match = seg 0 (#757) + assert_eq!(sd_resolve_owner(0x200, 1, 2), -1); + // Single-segment form: one membership evaluation per invocation. + assert_eq!(sd_resolve_owner(0x102, 1, 1), 2); + assert_eq!(sd_resolve_owner(0x104, 1, 1), -1); + + // spanned: correct owner is consistent, the #757 owner is not. + assert_eq!(sd_validate_spanned(1, 0), 0); + assert!(sd_validate_spanned(0, 0) > 0); + + // served image: full blob consistent, truncated blob drops bytes. + assert_eq!(sd_validate_served(4, 0), 0); + assert!(sd_validate_served(0, 0) > 0); + assert_eq!(sd_validate_served(4, 1), 0); + + // allocation validator: green and violating shapes both reachable. + assert_eq!(ra_validate(1), 0); + assert_eq!(ra_validate(2), 1); + // A `Call` puts the stream past the RV32 whole-function frontier, so a + // clean non-leaf is `NotAttempted` — the straight-line invariants still + // ran and held. An unsaved `ra` is still a hard Violation (#871). + assert_eq!(ra_validate(3), 2); + assert_eq!(ra_validate(4), 1, "#871: unsaved ra must be a violation"); + + // bounds gate: 0 bytes refused, power-of-two accepted, other refused. + assert_eq!( + rv_bounds_gate(2, 0), + 1, + "#959: (memory 0) + mask must refuse" + ); + assert_eq!(rv_bounds_gate(2, 65536), 0); + assert_eq!(rv_bounds_gate(2, 196608), 1, "#651: non-power-of-two"); + assert_eq!(rv_bounds_gate(3, 65536), 1, "non-RISC-V target must refuse"); + + // Every added shape must be reachable and classified. + for shape in 0..=21 { + let v = ra_validate(shape); + assert!((0..=2).contains(&v), "shape {shape} -> {v}"); + } + assert_eq!( + ra_validate(18), + 1, + "saved but never restored is a violation" + ); + } +} diff --git a/scripts/mcdc_gate.py b/scripts/mcdc_gate.py new file mode 100644 index 00000000..88f86c15 --- /dev/null +++ b/scripts/mcdc_gate.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""RQ-57-MCDC (#912) — score witness MC/DC over synth's OWN decision logic. + +Why this script exists rather than reading a percentage off `witness report` +----------------------------------------------------------------------------- +Three separate things make the raw module-level number unusable as a gate, and +each of them is the "instrument measuring the wrong surface" class this repo +keeps finding: + +1. A `wasm32-wasip1` link drags in wasi-libc (`malloc.c`, `stpcpy.c`, …) and + Rust `std` (`panicking.rs`, `core::fmt`, …). Those contribute THOUSANDS of + never-evaluated conditions. `3/770 full MC/DC` says almost nothing about + synth. Scoring must be restricted to synth's own functions. + +2. witness's `source_file` / `source_line` are NOT reliable for scoping. They + are DWARF line attributions of INLINED code, so `resolve_owner`'s decision + reports as `static_data_addr.rs:355` (the decision is at :274) and + `validate_reloc_resolutions`' decisions report as `backend.rs:480` and + `num.rs:85` — files in other crates entirely. That is upstream + pulseengine/witness#179. `source_file` is also only a BASENAME, so six + crates' `backend.rs` collide. + + The manifest's per-branch `function_name` IS reliable: it is the Rust + symbol of the function the branch physically lives in. This script scopes + and reports by DEMANGLED FUNCTION, never by file, and prints the reported + line only as an advisory. + +3. A ratio cannot notice a DELETED condition — removing `|| rs2 == Reg::RA` + from a predicate removes a gap row and the percentage IMPROVES. So the + floors below are COUNTS (conditions present, conditions proved) as well as + a gap ceiling. + +Usage: + scripts/mcdc_gate.py # dir written by scripts/mcdc_run.sh + scripts/mcdc_gate.py --report-only # print, never fail +""" + +from __future__ import annotations + +import argparse +import json +import re +import sys +from pathlib import Path + +# ─────────────────────────────────────────────────────────────────────────── +# THE SCORED SURFACE — "the right parts" (#912) +# +# Not every decision in synth is worth an MC/DC obligation. These three module +# prefixes are the predicate classes where a MISSED CONDITION HAS ALREADY +# SHIPPED A SOUNDNESS BUG IN THIS REPO: +# +# * static_data_addr — validator accept/reject. VCR-VER-003 (#777). Its +# whole job is to hard-error the #757 wrong-segment +# miscompile; a missed condition green-washes it. +# Also carries the #798 served-image gate. +# * alloc_validator — validator accept/reject. VCR-RA-003 (#815). #871 +# shipped an unsaved-`ra` miscompile: a non-leaf +# function returning into its own call site. The fix +# WAS a condition added to the save-set predicate. +# * riscv backend — guard emission. The #953/#959 sentinel-vs-value +# class, three consecutive releases: `mem_size == 0` +# was EXEMPT from the power-of-two mask gate, so +# `(memory 0)` emitted an identity mask (0-1 = +# 0xFFFF_FFFF) and every access ran unmasked. +# +# EXPLICITLY OUT OF SCOPE (named, not hidden — see #912 for the argument): +# * synth_synthesis::instruction_selector — 225 boolean-operator lines; a +# lane-sized surface of its own, and its decisions are already gated by +# ~30 execution differentials. +# * the aarch64 `bounds_check` / `form_ea` closures — reachable only by +# driving a whole function body through the selector; named residual. +# * synth_backend::wcet* — the decline predicates are match-dispatch +# (`scan_for_decline`: 1 boolean-operator line in 1061), so most of that +# surface has no compound decision to measure. +SCORED_PREFIXES = ( + "synth_core::static_data_addr::", + "synth_backend_riscv::alloc_validator::", + "synth_backend_riscv::backend::", +) + +# ─────────────────────────────────────────────────────────────────────────── +# DECLARED FLOORS — measured, not guessed (see #912 / the PR body for the run +# these came from). Raise them when a lane adds rows; never lower them to make +# a red gate green. +# +# MEASURED BASELINE (witness 0.28.0, wasm32-wasip1, 56 rows): +# 20 scored decisions / 144 conditions / 63 proved / 31 gap / 50 dead +# 3 decisions at FULL MC/DC (is_ret, sp_slot_load, build_options) +# The floors ARE those numbers. A floor set below what was measured is the +# half-value-floor defect this hub already found elsewhere; a floor set above +# is a red gate nobody can fix. +# +# ci-checks: mcdc scored decisions >= 20 +# ci-checks: mcdc scored conditions >= 144 +# ci-checks: mcdc scored conditions proved >= 63 +# ci-checks: mcdc fully-proved decisions >= 3 +FLOOR_DECISIONS = 20 +FLOOR_CONDITIONS = 144 +FLOOR_PROVED = 63 +FLOOR_FULL_MCDC_DECISIONS = 3 + + +def demangle(sym: str) -> str: + """Rust legacy (`_ZN…E`) symbol -> `crate::module::fn`. + + Only the path components are needed; the trailing `17h` disambiguator + and any generic arguments are dropped. Falls back to the raw symbol so an + unrecognised mangling is visible rather than silently dropped. + """ + m = re.match(r"^_ZN(.*)E$", sym) + if not m: + return sym + body, parts, i = m.group(1), [], 0 + while i < len(body): + j = i + while j < len(body) and body[j].isdigit(): + j += 1 + if j == i: + break + n = int(body[i:j]) + seg = body[j : j + n] + i = j + n + if re.fullmatch(r"h[0-9a-f]{16}", seg): + continue + parts.append(seg) + return "::".join(parts) if parts else sym + + +def load(run_dir: Path): + manifest = json.loads((run_dir / "instrumented.wasm.witness.json").read_text()) + report = json.loads((run_dir / "report.json").read_text()) + return manifest, report + + +def main() -> int: + ap = argparse.ArgumentParser() + ap.add_argument("run_dir", type=Path) + ap.add_argument("--report-only", action="store_true") + args = ap.parse_args() + + manifest, report = load(args.run_dir) + if report.get("schema") != "https://pulseengine.eu/witness-mcdc/v3": + print(f"note: unexpected report schema {report.get('schema')!r}", file=sys.stderr) + + branch_fn = {b["id"]: demangle(b.get("function_name", "")) for b in manifest["branches"]} + + # A decision belongs to a function when its conditions' branches do. A + # decision straddling two functions (inlining) is attributed to the one + # owning the most conditions, and flagged. + per_fn: dict[str, dict] = {} + scored_decisions = [] + for dec in report["decisions"]: + owners: dict[str, int] = {} + for c in dec["conditions"]: + owners[branch_fn.get(c["branch_id"], "?")] = ( + owners.get(branch_fn.get(c["branch_id"], "?"), 0) + 1 + ) + owner = max(owners, key=lambda k: owners[k]) + if not owner.startswith(SCORED_PREFIXES): + continue + scored_decisions.append((owner, dec, len(owners) > 1)) + st = per_fn.setdefault( + owner, {"decisions": 0, "full": 0, "proved": 0, "gap": 0, "dead": 0} + ) + st["decisions"] += 1 + statuses = [c["status"] for c in dec["conditions"]] + for s in statuses: + st[s if s in ("proved", "gap", "dead") else "gap"] += 1 + if statuses and all(s == "proved" for s in statuses): + st["full"] += 1 + + tot = {k: sum(v[k] for v in per_fn.values()) for k in ("decisions", "full", "proved", "gap", "dead")} + conditions = tot["proved"] + tot["gap"] + tot["dead"] + + print("MC/DC over synth's own decision logic (RQ-57-MCDC, #912)") + print(f" witness {report.get('witness_version')} schema {report.get('schema')}") + print(f" attribution_source: {manifest.get('attribution_source')} " + f"(function names; file:line is unreliable — witness#179)") + print() + print(f"{'function':<62}{'dec':>5}{'full':>6}{'cond':>6}{'prov':>6}{'gap':>5}{'dead':>6}") + print("-" * 96) + for fn in sorted(per_fn): + v = per_fn[fn] + c = v["proved"] + v["gap"] + v["dead"] + short = fn if len(fn) <= 60 else "…" + fn[-59:] + print(f"{short:<62}{v['decisions']:>5}{v['full']:>6}{c:>6}{v['proved']:>6}{v['gap']:>5}{v['dead']:>6}") + print("-" * 96) + print(f"{'TOTAL':<62}{tot['decisions']:>5}{tot['full']:>6}{conditions:>6}" + f"{tot['proved']:>6}{tot['gap']:>5}{tot['dead']:>6}") + print() + + # The gap rows themselves — the point of the exercise. A percentage without + # these is the thing #912 spent six releases mistaking for a result. + print("GAP ROWS (condition proved by no unique-cause / masking pair):") + n_gap = 0 + for owner, dec, straddles in scored_decisions: + gaps = [c for c in dec["conditions"] if c["status"] == "gap"] + if not gaps: + continue + n_gap += len(gaps) + flag = " [inlined across functions]" if straddles else "" + print(f" {owner} (decision #{dec['id']}, reported at " + f"{dec['source_file']}:{dec['source_line']}){flag}") + for c in gaps: + gc = c.get("gap_closure") or {} + print(f" c{c['index']}: need a row {gc.get('evaluated')} " + f"with outcome != {gc.get('outcome_must_differ_from')} " + f"(pair with row {gc.get('paired_with_row')})") + if n_gap == 0: + print(" (none)") + print() + + fails = [] + if tot["decisions"] < FLOOR_DECISIONS: + fails.append(f"scored decisions {tot['decisions']} < floor {FLOOR_DECISIONS}") + if conditions < FLOOR_CONDITIONS: + fails.append(f"scored conditions {conditions} < floor {FLOOR_CONDITIONS}") + if tot["proved"] < FLOOR_PROVED: + fails.append(f"proved conditions {tot['proved']} < floor {FLOOR_PROVED}") + if tot["full"] < FLOOR_FULL_MCDC_DECISIONS: + fails.append( + f"fully-proved decisions {tot['full']} < floor {FLOOR_FULL_MCDC_DECISIONS}" + ) + + if fails and not args.report_only: + for f in fails: + print(f"FAIL: {f}") + print() + print("A DROP in `scored conditions` means a condition was deleted from a") + print("gated predicate — that is the case a ratio-only floor cannot see, and") + print("it is why this gate counts. Do not lower a floor to go green.") + return 1 + for f in fails: + print(f"(report-only) would FAIL: {f}") + print("PASS: all MC/DC floors met") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/mcdc_run.sh b/scripts/mcdc_run.sh new file mode 100644 index 00000000..578e1d50 --- /dev/null +++ b/scripts/mcdc_run.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +# RQ-57-MCDC (#912) — build the row-driver harness for wasm32-wasip1, run every +# truth-table row under `witness`, and write the MC/DC report. +# +# TWO INVOCATION TRAPS this script exists to make unreachable (both documented +# on #912 and filed upstream as pulseengine/witness#177 / #178): +# +# 1. `witness report` WITHOUT `--format mcdc` prints branches *reached*, not +# MC/DC. That number looks like coverage, is not, and is how this step got +# read as "nothing here" for six releases. We always ask for `mcdc` and +# `mcdc-json`. +# 2. A build without full DWARF renders every gap row `(anon)` and untriageable +# while still reporting `attribution_source: "dwarf"`. We always build with +# `-C debuginfo=2` and the dev profile (a `--release` build at opt-level +# z/s dead-strips witness's counters). +# +# Usage: scripts/mcdc_run.sh [output-dir] +set -euo pipefail + +OUT=${1:-target/mcdc} +REPO=$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd) +cd "$REPO" +mkdir -p "$OUT" + +WITNESS=${WITNESS:-witness-mcdc} +command -v "$WITNESS" >/dev/null || { + echo "error: $WITNESS not on PATH (install from pulseengine/witness releases)" >&2 + exit 127 +} + +# Dev profile + full debuginfo: see trap 2 above. +RUSTFLAGS="-C debuginfo=2 ${RUSTFLAGS:-}" \ + cargo build --target wasm32-wasip1 -p synth-mcdc-harness + +WASM=$(cargo metadata --format-version 1 --no-deps \ + | python3 -c 'import json,sys; print(json.load(sys.stdin)["target_directory"])')/wasm32-wasip1/debug/synth_mcdc_harness.wasm +test -f "$WASM" || { echo "error: harness wasm not found at $WASM" >&2; exit 1; } + +"$WITNESS" instrument "$WASM" -o "$OUT/instrumented.wasm" + +# ── The truth-table rows ──────────────────────────────────────────────────── +# Each `--invoke-with-args` is ONE row. The vectors are chosen for unique-cause +# / masking MC/DC on the decisions named in the harness doc comments, not for a +# percentage. Adding a row here is how a gap row gets closed. +"$WITNESS" run "$OUT/instrumented.wasm" \ + `# static_data_addr::resolve_owner — c >= off && c < off + len.` \ + `# ONE segment so the membership test is evaluated exactly once per` \ + `# invocation (witness records one row per invocation; a decision inside a` \ + `# loop collapses to a single captured vector).` \ + --invoke-with-args 'sd_resolve_owner:80,1,1' \ + --invoke-with-args 'sd_resolve_owner:255,1,1' \ + --invoke-with-args 'sd_resolve_owner:256,1,1' \ + --invoke-with-args 'sd_resolve_owner:258,1,1' \ + --invoke-with-args 'sd_resolve_owner:259,1,1' \ + --invoke-with-args 'sd_resolve_owner:260,1,1' \ + --invoke-with-args 'sd_resolve_owner:512,1,1' \ + --invoke-with-args 'sd_resolve_owner:80,0,1' \ + --invoke-with-args 'sd_resolve_owner:256,0,1' \ + --invoke-with-args 'sd_resolve_owner:512,0,1' \ + `# the #757 overlapping shape — behaviour, not vectors` \ + --invoke-with-args 'sd_resolve_owner:256,1,2' \ + --invoke-with-args 'sd_resolve_owner:256,0,2' \ + `# validate_reloc_resolutions_spanned — j == 0 && seg_byte != runtime_byte` \ + --invoke-with-args 'sd_validate_spanned:1,0' \ + --invoke-with-args 'sd_validate_spanned:0,0' \ + --invoke-with-args 'sd_validate_spanned:1,2' \ + --invoke-with-args 'sd_validate_spanned:0,3' \ + --invoke-with-args 'sd_validate_spanned:1,3' \ + `# out-of-range emitted resolutions — both let-else rejects` \ + --invoke-with-args 'sd_validate_spanned:9,0' \ + --invoke-with-args 'sd_validate_spanned:1,99' \ + `# validate_served_image — addr >= image.len() && owed != 0` \ + --invoke-with-args 'sd_validate_served:4,0' \ + --invoke-with-args 'sd_validate_served:0,0' \ + --invoke-with-args 'sd_validate_served:4,1' \ + --invoke-with-args 'sd_validate_served:2,1' \ + --invoke-with-args 'sd_validate_served:1,0' \ + --invoke-with-args 'sd_validate_served:0,1' \ + `# alloc_validator::validate_final_allocation_rv32 (VCR-RA-003 / #871)` \ + --invoke-with-args 'ra_validate:0' \ + --invoke-with-args 'ra_validate:1' \ + --invoke-with-args 'ra_validate:2' \ + --invoke-with-args 'ra_validate:3' \ + --invoke-with-args 'ra_validate:4' \ + --invoke-with-args 'ra_validate:5' \ + --invoke-with-args 'ra_validate:6' \ + --invoke-with-args 'ra_validate:7' \ + --invoke-with-args 'ra_validate:8' \ + --invoke-with-args 'ra_validate:9' \ + --invoke-with-args 'ra_validate:10' \ + --invoke-with-args 'ra_validate:11' \ + --invoke-with-args 'ra_validate:12' \ + --invoke-with-args 'ra_validate:13' \ + --invoke-with-args 'ra_validate:14' \ + --invoke-with-args 'ra_validate:15' \ + --invoke-with-args 'ra_validate:16' \ + --invoke-with-args 'ra_validate:17' \ + --invoke-with-args 'ra_validate:18' \ + --invoke-with-args 'ra_validate:19' \ + --invoke-with-args 'ra_validate:20' \ + --invoke-with-args 'ra_validate:21' \ + --invoke-with-args 'ra_validate:99' \ + `# riscv build_options bounds gate — mem == 0 || !mem.is_power_of_two()` \ + --invoke-with-args 'rv_bounds_gate:2,0' \ + --invoke-with-args 'rv_bounds_gate:2,65536' \ + --invoke-with-args 'rv_bounds_gate:2,196608' \ + --invoke-with-args 'rv_bounds_gate:2,1' \ + --invoke-with-args 'rv_bounds_gate:1,65536' \ + --invoke-with-args 'rv_bounds_gate:1,0' \ + --invoke-with-args 'rv_bounds_gate:0,0' \ + --invoke-with-args 'rv_bounds_gate:0,65536' \ + `# a non-RISC-V target: flips ensure_supported_target's conjunction` \ + --invoke-with-args 'rv_bounds_gate:3,65536' \ + --invoke-with-args 'rv_bounds_gate:3,0' \ + -o "$OUT/run.json" + +"$WITNESS" report --input "$OUT/run.json" --format mcdc > "$OUT/report.txt" +"$WITNESS" report --input "$OUT/run.json" --format mcdc-json > "$OUT/report.json" +"$WITNESS" report --input "$OUT/run.json" --format mcdc-rollup > "$OUT/rollup.txt" + +echo "wrote $OUT/report.txt $OUT/report.json $OUT/rollup.txt" diff --git a/scripts/repro/mcdc_912_gate.md b/scripts/repro/mcdc_912_gate.md new file mode 100644 index 00000000..61f796b4 --- /dev/null +++ b/scripts/repro/mcdc_912_gate.md @@ -0,0 +1,196 @@ +# RQ-57-MCDC (#912) — MC/DC structural coverage: surface, measurement, potency + +Reproduce: `scripts/mcdc_run.sh target/mcdc && scripts/mcdc_gate.py target/mcdc` +(needs `witness` v0.42.0 on `$PATH` or `WITNESS=…`, and the `wasm32-wasip1` +target). CI job: `mcdc-structural-coverage`. + +## 1. The surface question, answered with evidence + +#912 sat N/A for six releases on the argument that `witness` measures MC/DC on +a **Wasm** artifact while synth emits **ARM/RV32/A64 machine code**. That +argument is right about synth's *output* and irrelevant to the question: the +decisions that ship a miscompile are the ones in synth's own Rust, and those +compile to Wasm fine. + +Three candidate surfaces were tried. Two were rejected on evidence, not taste. + +### REJECTED — native LLVM MC/DC via `-Zcoverage-options=mcdc` + +Not a preference: **the capability was removed from rustc.** +[rust-lang/rust#144999](https://github.com/rust-lang/rust/pull/144999) — +*"coverage: Remove all unstable support for MC/DC instrumentation"*, merged +2025-08-08, released in Rust 1.91 — on the stated rationale that the partial +implementation "has proven itself to be a major burden on overall maintenance +of coverage instrumentation." + +Probed directly rather than taken on faith, across three nightlies +(1.93.0-nightly 2025-11-20, 1.95.0-nightly 2026-02-06, 1.97.0-nightly +2026-04-19): + +``` +[mcdc] rc=1 error: incorrect value `mcdc` for unstable option + `coverage-options` - `block` | `branch` | `condition` was expected +[condition] rc=0 +``` + +`condition` is the trap in this family: it compiles, and it is **not** MC/DC. +A toy `a && b || c` built with it yields per-condition *branch* entries, a +`report --show-mcdc-summary` reading `MC/DC Conditions 0`, `mcdc_records: 0` +in the JSON export, and **zero `llvm.instrprof.mcdc.*` intrinsics** in the +emitted IR. `cargo-llvm-cov` 0.6.21 and 0.8.7 both still pass `mcdc` and both +fail the build. + +### REJECTED — `witness` over the Wasm fixtures synth COMPILES + +This measures the fixture, not synth. The discriminating test is *whose source +do the gap rows name*. gale's run on a real dissolved isolation core (recorded +on #912) named: + +| function | branches | reached | +|---|---|---| +| `core::fmt::Formatter::pad_integral` | 25 | 0 | +| `core::str::count::do_count_chars` | 20 | 0 | +| `::fmt` | 5 | 0 | +| `pad_integral::write_prefix` | 3 | 0 | +| `wit_bindgen::rt::cabi_realloc` ×2 | 3+3 | 0 | + +Five stdlib/bindgen frames and **zero synth functions**. A surface whose gap +rows cannot name a synth decision cannot notice a missing condition in one. + +### CHOSEN — `witness` over a `wasm32-wasip1` build of synth's OWN crates + +`crates/synth-mcdc-harness` is a thin **row driver**: it links the real crates +and calls the real `pub fn`s with inputs arriving through Wasm parameters (so +nothing is constant-folded). It re-implements no predicate — a mirror would be +precisely the vacuous-gate class this is meant to catch. Gap rows then name +`synth_core::static_data_addr::resolve_owner`, +`synth_backend_riscv::alloc_validator::is_ret`, and so on. + +Bonus, and the reason this surface is arguably *better* than the removed rustc +one: witness reconstructs decisions from the **lowered** `br_if` chains, so a +Rust `matches!` lowers to a real multi-condition decision. `is_ret`'s +`matches!(op, Jalr { rd: ZERO, rs1: RA, imm: 0 })` scores as a 4-condition +decision — source-level MC/DC would have seen nothing there. + +## 2. "The right parts" — what is scored, and what is not + +Scored (`SCORED_PREFIXES` in `scripts/mcdc_gate.py`) — the predicate classes +where a missed condition **has already shipped a soundness bug in this repo**: + +| module | class | the bug | +|---|---|---| +| `synth_core::static_data_addr` | validator accept/reject | VCR-VER-003 #777; exists to hard-error the #757 wrong-segment miscompile; also the #798 served-image gate | +| `synth_backend_riscv::alloc_validator` | validator accept/reject | VCR-RA-003 #815; **#871** shipped an unsaved-`ra` miscompile and the fix *was* a condition added to the save-set predicate | +| `synth_backend_riscv::backend` | guard emission | #953/#959, three consecutive releases: `mem_size == 0` was EXEMPT from the power-of-two mask gate, so `(memory 0)` emitted an identity mask (`0-1 = 0xFFFF_FFFF`) and every access ran unmasked | + +Excluded, named rather than hidden: + +* `synth_synthesis::instruction_selector` — 225 boolean-operator lines. A lane + of its own; already gated by ~30 execution differentials. +* the aarch64 `bounds_check` / `form_ea` closures (#865) — reachable only by + driving a whole function body through the selector. **Named residual**: the + guard-emission class is covered on RV32, not yet on aarch64. +* `synth_backend::wcet*` decline predicates — `scan_for_decline` has **1** + boolean-operator line in 1061; it is match-dispatch, so most of that surface + has no compound decision for MC/DC to speak about. Branch coverage is the + applicable criterion there. + +## 3. Measured baseline (witness 0.42.0, `wasm32-wasip1`, 56 rows) + +``` +function dec full cond prov gap dead +synth_backend_riscv::alloc_validator::is_ret 1 1 4 4 0 0 +synth_backend_riscv::alloc_validator::is_straight_line 1 0 52 12 0 40 +synth_backend_riscv::alloc_validator::sp_slot_load 1 1 2 2 0 0 +…alloc_validator::validate_final_allocation_rv32 4 0 43 28 15 0 +synth_backend_riscv::backend::build_options 2 1 7 5 0 2 +synth_backend_riscv::backend::compile_function_with_opts 1 0 4 1 0 3 +synth_backend_riscv::backend::count_params 1 0 4 1 0 3 +…backend::count_params::{{closure}} 1 0 2 0 0 2 +synth_backend_riscv::backend::ensure_supported_target 1 0 4 0 4 0 +synth_core::static_data_addr::resolve_owner 1 0 2 0 2 0 +synth_core::static_data_addr::runtime_image 1 0 2 1 1 0 +synth_core::static_data_addr::validate_reloc_resolutions 3 0 7 4 3 0 +…static_data_addr::validate_reloc_resolutions_spanned 2 0 11 5 6 0 +TOTAL 20 3 144 63 31 50 +``` + +Identical under witness **0.28.0** and **0.42.0** — 14 minor versions apart — +so the numbers are not tracking the tool's phrasing. + +**The gate reads gap rows, not a percentage.** 31 gap conditions remain and are +printed in full by `scripts/mcdc_gate.py`, each with the vector witness says +would close it. Two examples of the residual, stated so it is named: + +* `validate_final_allocation_rv32` carries decisions of 10 and 20 conditions + (whole-function `br_if` chains after inlining). Closing those needs ≥21 + co-designed vectors and is **not** claimed. +* `ensure_supported_target`'s ISA conjunction (4 gap) cannot be flipped through + public constructors: there is no `TargetSpec` with family RiscV and a + non-RiscV32/64 ISA. + +`is_ret` went 1-proved/3-gap → **4-proved/0-gap** by adding exactly the three +vectors witness printed, which is the practical demonstration that the gap rows +are actionable rather than decorative. + +## 4. Why the gate scores by FUNCTION and floors COUNTS + +Three defects in the naive reading, each the "instrument measuring the wrong +surface" class: + +1. **The module-wide percentage is meaningless here.** A wasip1 link drags in + wasi-libc (`malloc.c`, `stpcpy.c`) and Rust `std`. Raw figure: `3/770 full + MC/DC`, 3879 dead conditions. Says nothing about synth. +2. **witness's `source_file` / `source_line` cannot be used for scoping.** They + are DWARF attributions of *inlined* code — `resolve_owner`'s decision reports + as `static_data_addr.rs:355` (it is at :274), and + `validate_reloc_resolutions`' decisions report as `backend.rs:480` and + `num.rs:85`, files in other crates. `source_file` is also only a *basename*, + so six crates' `backend.rs` collide. (Upstream: witness#179.) The manifest's + per-branch **`function_name` is reliable**, so the gate scopes on the + demangled symbol and prints the reported line as advisory only. +3. **A ratio cannot notice a deleted condition** — removing one removes its gap + row and the percentage *improves*. So the floors are counts. + +Declared floors = the measured baseline, no slack: +`decisions ≥ 20`, `conditions ≥ 144`, `proved ≥ 63`, `fully-proved decisions ≥ 3`. + +## 5. Red-first potency — two mutations, two distinct failure paths + +Both mutations restored afterwards; `git diff` byte-identical. + +**(a) Delete a condition** — remove the #871 fix `|| rs2 == Reg::RA` from the +RV32 allocation validator's save-set predicate: + +``` +baseline TOTAL dec 20 full 3 cond 144 proved 63 gap 31 dead 50 +mutated TOTAL dec 19 full 2 cond 142 proved 54 gap 36 dead 52 +FAIL: scored decisions 19 < floor 20 +FAIL: scored conditions 142 < floor 144 +FAIL: proved conditions 54 < floor 63 +FAIL: fully-proved decisions 2 < floor 3 +``` + +The **condition-count** drop is the signal a ratio-only floor cannot produce. + +**(b) Weaken the vector set** — drop ONE truth-table row (`ra_validate:14`, the +non-`sp` `Lw` that gives `sp_slot_load` its unique-cause pair): + +``` +mutated TOTAL dec 20 full 2 cond 144 proved 62 gap 32 dead 50 +FAIL: proved conditions 62 < floor 63 +FAIL: fully-proved decisions 2 < floor 3 +``` + +Conditions unchanged, coverage lost — the second failure path. + +## 6. Two invocation traps, encoded in the scripts + +Both are why this looked empty for six releases (upstream witness#177/#178): + +1. `witness report` **without** `--format mcdc` prints branches *reached*, not + MC/DC. `scripts/mcdc_run.sh` always requests `mcdc` / `mcdc-json`. +2. A build without full DWARF renders every gap row `(anon)` while still + reporting `attribution_source: "dwarf"`. The script always builds with + `-C debuginfo=2` and the dev profile (a `--release` build at `opt-level=z/s` + dead-strips witness's counters). From 712f658d28e1bbe5c122163ce48c3fd3cdf4420f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 18:46:50 +0200 Subject: [PATCH 2/5] fix(#912): CI mode-126 on mcdc_run.sh, pin the toolchain, ceiling the dead count MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three fixes from the first CI run and the cold read of it: 1. exit 126. `scripts/` is mode 644 in this repo (cf. scripts/oracle_run.py), so `./scripts/mcdc_run.sh` cannot exec on a fresh checkout even though it runs locally after a chmod. Invoke through `bash`, matching how every other script in this workflow is called. 2. PIN the toolchain to 1.96.1. The floors are counts of decisions and conditions RECONSTRUCTED FROM LOWERED WASM, so they are sensitive to how `std` inlines. `@stable` is a moving target and a Rust release could red this gate with no code change. Bumping the pin is allowed and obliges a RE-MEASURE, not a lowering. (Witness-version invariance — 0.28 = 0.42 — is evidence about witness, not about rustc; it does not transfer.) 3. CEILING the dead count at the measured 50. 50 of 144 scored conditions are never evaluated (40 in `is_straight_line`, whose match arms cover RV32 opcodes the row set does not construct). That residual was the one number in the table nothing guarded: a change that stopped reaching the segment barriers would raise `dead`, lower nothing else, and PASS. It is also a third potency surface — mutation (a) moves dead 50 -> 52, so the mutated run now trips five floors instead of four. Also trims the `sd_resolve_owner` doc comment, which claimed vectors the measurement does not show: its 2 gap conditions are now stated as a measured residual rather than implied closed. Baseline re-verified unchanged: 20 / 3 / 144 / 63 / 31 / 50, PASS. Refs #912 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 16 ++++++++++++---- crates/synth-mcdc-harness/src/lib.rs | 9 +++++++-- scripts/mcdc_gate.py | 10 ++++++++++ scripts/repro/mcdc_912_gate.md | 13 +++++++++++-- 4 files changed, 40 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dc050959..575dc440 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3604,7 +3604,12 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v7 - - uses: dtolnay/rust-toolchain@stable + # PINNED, deliberately, unlike every other job here: the floors are counts + # of decisions and conditions RECONSTRUCTED FROM LOWERED WASM, so they are + # sensitive to how `std` inlines. `@stable` is a moving target and a Rust + # release could red this gate with no code change. Bumping this version is + # allowed — it obliges a RE-MEASURE of the floors, not a lowering. + - uses: dtolnay/rust-toolchain@1.96.1 with: targets: wasm32-wasip1 - name: Cache Cargo dependencies @@ -3614,9 +3619,9 @@ jobs: ~/.cargo/registry ~/.cargo/git target/ - key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + key: ${{ runner.os }}-mcdc-${{ hashFiles('**/Cargo.lock') }} restore-keys: | - ${{ runner.os }}-cargo- + ${{ runner.os }}-mcdc- - uses: actions/setup-python@v7 with: python-version: "3.x" @@ -3636,8 +3641,11 @@ jobs: # MC/DC run vacuous while still printing a number. - name: Row-driver sanity gate (host) run: cargo test -p synth-mcdc-harness + # Invoked through `bash`, not as `./…`: scripts/ is mode 644 in this repo + # (cf. scripts/oracle_run.py), so an `exec` form exits 126 on a fresh + # checkout even though it runs fine locally after a `chmod`. - name: Run the MC/DC rows under witness - run: WITNESS="$HOME/.witness/witness" ./scripts/mcdc_run.sh target/mcdc + run: WITNESS="$HOME/.witness/witness" bash scripts/mcdc_run.sh target/mcdc - name: Score synth's own decisions against the declared floors run: | set -euo pipefail diff --git a/crates/synth-mcdc-harness/src/lib.rs b/crates/synth-mcdc-harness/src/lib.rs index 0d61058b..767bcb2c 100644 --- a/crates/synth-mcdc-harness/src/lib.rs +++ b/crates/synth-mcdc-harness/src/lib.rs @@ -83,8 +83,13 @@ fn overlapping_segments() -> Vec { /// that IS the #757 fix). `c` arrives through a Wasm parameter, so the /// comparison is evaluated at run time. /// -/// Rows: `c` below the segment (c0=F), inside it (c0=T,c1=T), above it -/// (c0=T,c1=F). `last_wins` selects which of the two search call sites runs. +/// Rows walk `c` below the segment, at its first byte, inside it, at its last +/// byte, one past its end, and far past it, under both `last_wins` call sites. +/// MEASURED RESIDUAL, stated rather than assumed: those vectors do NOT close +/// this decision — witness still reports 2 gap conditions on it, asking for +/// `{c0=T, c1=F}` and `{c0=F, c1=T}` with a differing outcome. The reconstructed +/// decision is evidently not a 1:1 image of the source `&&`, and running it +/// down is named as remaining work on #912 rather than papered over here. /// /// `nseg` matters for the MEASUREMENT, not for the predicate: `witness` records /// ONE truth-table row per invocation, so a decision evaluated once per diff --git a/scripts/mcdc_gate.py b/scripts/mcdc_gate.py index 88f86c15..ab8fcd02 100644 --- a/scripts/mcdc_gate.py +++ b/scripts/mcdc_gate.py @@ -95,10 +95,18 @@ # ci-checks: mcdc scored conditions >= 144 # ci-checks: mcdc scored conditions proved >= 63 # ci-checks: mcdc fully-proved decisions >= 3 +# ci-checks: mcdc dead conditions <= 50 FLOOR_DECISIONS = 20 FLOOR_CONDITIONS = 144 FLOOR_PROVED = 63 FLOOR_FULL_MCDC_DECISIONS = 3 +# DEAD is CEILINGED, not ignored. 50 of the 144 scored conditions are never +# evaluated — 40 of them in `is_straight_line`, whose match arms cover RV32 +# opcodes the row set does not construct. That is an honest residual, but an +# UNFLOORED residual is how a number rots: a change that stopped reaching the +# segment barriers would raise `dead`, lower nothing else, and pass. It is also +# a third potency surface — mutation (a) moved dead 50 -> 52. +CEILING_DEAD = 50 def demangle(sym: str) -> str: @@ -222,6 +230,8 @@ def main() -> int: fails.append( f"fully-proved decisions {tot['full']} < floor {FLOOR_FULL_MCDC_DECISIONS}" ) + if tot["dead"] > CEILING_DEAD: + fails.append(f"dead conditions {tot['dead']} > ceiling {CEILING_DEAD}") if fails and not args.report_only: for f in fails: diff --git a/scripts/repro/mcdc_912_gate.md b/scripts/repro/mcdc_912_gate.md index 61f796b4..cfca9681 100644 --- a/scripts/repro/mcdc_912_gate.md +++ b/scripts/repro/mcdc_912_gate.md @@ -1,6 +1,6 @@ # RQ-57-MCDC (#912) — MC/DC structural coverage: surface, measurement, potency -Reproduce: `scripts/mcdc_run.sh target/mcdc && scripts/mcdc_gate.py target/mcdc` +Reproduce: `bash scripts/mcdc_run.sh target/mcdc && python3 scripts/mcdc_gate.py target/mcdc` (needs `witness` v0.42.0 on `$PATH` or `WITNESS=…`, and the `wasm32-wasip1` target). CI job: `mcdc-structural-coverage`. @@ -153,7 +153,15 @@ surface" class: row and the percentage *improves*. So the floors are counts. Declared floors = the measured baseline, no slack: -`decisions ≥ 20`, `conditions ≥ 144`, `proved ≥ 63`, `fully-proved decisions ≥ 3`. +`decisions ≥ 20`, `conditions ≥ 144`, `proved ≥ 63`, `fully-proved decisions ≥ 3`, +and `dead ≤ 50`. + +**Dead is ceilinged, not ignored.** 50 of the 144 scored conditions are never +evaluated — 40 of them in `is_straight_line`, whose match arms cover RV32 +opcodes the row set does not construct. That is an honest residual, but an +UNFLOORED residual is how a number rots: a change that stopped reaching the +segment barriers would raise `dead`, lower nothing else, and pass. It is also a +third potency surface — mutation (a) moves dead 50 → 52. ## 5. Red-first potency — two mutations, two distinct failure paths @@ -169,6 +177,7 @@ FAIL: scored decisions 19 < floor 20 FAIL: scored conditions 142 < floor 144 FAIL: proved conditions 54 < floor 63 FAIL: fully-proved decisions 2 < floor 3 +FAIL: dead conditions 52 > ceiling 50 ``` The **condition-count** drop is the signal a ratio-only floor cannot produce. From 25a9195f02787d5545ba6f5bfbe21a3e010a242d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 18:52:49 +0200 Subject: [PATCH 3/5] =?UTF-8?q?TEMPORARY=20red-first=20probe=20(#912)=20?= =?UTF-8?q?=E2=80=94=20DO=20NOT=20MERGE=20THIS=20COMMIT?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reverted by the very next commit. Two things in one CI run: 1. RE-MEASURE the floors on the platform the gate actually runs on. The first CI run proved what could only be argued locally: these counts are PLATFORM-dependent, not just toolchain-version dependent. ubuntu x86_64, rustc 1.96.1, witness 0.42.0: 22 / 130 / 57 / 23 gap / 50 dead, 4 full macOS aarch64, rustc 1.96.1, witness 0.42.0: 20 / 144 / 63 / 31 gap / 50 dead, 3 full Same toolchain version, same witness, same 56 rows, different host. `validate_final_allocation_rv32` presents as 9 decisions / 44 conditions on Linux and 4 / 43 on macOS; `ensure_supported_target` vanishes on Linux. Floors move to the CI numbers — RE-MEASURED, not lowered to fit. Both baselines are recorded in the script so the macOS delta is a stated fact rather than a surprise. 2. RE-PROVE POTENCY ON THAT PLATFORM. The local mutation evidence does NOT obviously transfer when the same function presents as 9 decisions instead of 4 — and "it obviously still works" is the reasoning this whole lane exists to distrust. So this commit ALSO deletes the #871 condition `|| rs2 == Reg::RA` from the RV32 allocation validator's save-set predicate. The MC/DC job must go RED on the condition-COUNT floor, and the VCR-RA-003 RV32 job should go red independently. If this commit is green, the gate is vacuous and the lane is wrong. Refs #912 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/alloc_validator.rs | 2 +- scripts/mcdc_gate.py | 51 ++++++++++++------- 2 files changed, 35 insertions(+), 18 deletions(-) diff --git a/crates/synth-backend-riscv/src/alloc_validator.rs b/crates/synth-backend-riscv/src/alloc_validator.rs index 869f6d2a..e72ec038 100644 --- a/crates/synth-backend-riscv/src/alloc_validator.rs +++ b/crates/synth-backend-riscv/src/alloc_validator.rs @@ -204,7 +204,7 @@ pub fn validate_final_allocation_rv32(instrs: &[RiscVOp]) -> RaFinalVerdict { let mut saved: BTreeSet = BTreeSet::new(); for ins in instrs { if let Some((_, rs2)) = sp_slot_store(ins) - && (is_saved_by_pass(rs2) || rs2 == Reg::RA) + && is_saved_by_pass(rs2) { saved.insert(rs2); } diff --git a/scripts/mcdc_gate.py b/scripts/mcdc_gate.py index ab8fcd02..e1d48ee0 100644 --- a/scripts/mcdc_gate.py +++ b/scripts/mcdc_gate.py @@ -84,25 +84,42 @@ # these came from). Raise them when a lane adds rows; never lower them to make # a red gate green. # -# MEASURED BASELINE (witness 0.28.0, wasm32-wasip1, 56 rows): -# 20 scored decisions / 144 conditions / 63 proved / 31 gap / 50 dead -# 3 decisions at FULL MC/DC (is_ret, sp_slot_load, build_options) -# The floors ARE those numbers. A floor set below what was measured is the -# half-value-floor defect this hub already found elsewhere; a floor set above -# is a red gate nobody can fix. +# THE FLOORS ARE THE CI PLATFORM'S MEASURED BASELINE — and the platform is +# part of the measurement, which the first CI run proved rather than argued. # -# ci-checks: mcdc scored decisions >= 20 -# ci-checks: mcdc scored conditions >= 144 -# ci-checks: mcdc scored conditions proved >= 63 -# ci-checks: mcdc fully-proved decisions >= 3 +# ubuntu-latest x86_64, rustc 1.96.1, witness 0.42.0, 56 rows: +# 22 decisions / 130 conditions / 57 proved / 23 gap / 50 dead +# 4 decisions at FULL MC/DC +# macOS aarch64, rustc 1.96.1, witness 0.42.0, the same 56 rows: +# 20 decisions / 144 conditions / 63 proved / 31 gap / 50 dead +# 3 decisions at FULL MC/DC +# +# Same toolchain VERSION, same witness, same rows — different HOST. These are +# counts of decisions reconstructed from LOWERED WASM, so how `std` inlines +# moves them: `validate_final_allocation_rv32` presents as 9 decisions / 44 +# conditions on Linux and 4 / 43 on macOS, and `ensure_supported_target` +# disappears entirely on Linux. Recording both numbers rather than only the +# convenient one: a developer running this locally on macOS will NOT meet these +# floors, and that is a platform delta, not a regression. Use `--report-only` +# locally and read the DELTA against your own previous run; the absolute floors +# belong to the platform the gate actually blocks on. +# +# Witness-version invariance was verified separately (0.28.0 and 0.42.0 give +# identical numbers on the same host), so the tool is not what moves these. +# +# ci-checks: mcdc scored decisions >= 22 +# ci-checks: mcdc scored conditions >= 130 +# ci-checks: mcdc scored conditions proved >= 57 +# ci-checks: mcdc fully-proved decisions >= 4 # ci-checks: mcdc dead conditions <= 50 -FLOOR_DECISIONS = 20 -FLOOR_CONDITIONS = 144 -FLOOR_PROVED = 63 -FLOOR_FULL_MCDC_DECISIONS = 3 -# DEAD is CEILINGED, not ignored. 50 of the 144 scored conditions are never -# evaluated — 40 of them in `is_straight_line`, whose match arms cover RV32 -# opcodes the row set does not construct. That is an honest residual, but an +FLOOR_DECISIONS = 22 +FLOOR_CONDITIONS = 130 +FLOOR_PROVED = 57 +FLOOR_FULL_MCDC_DECISIONS = 4 +# DEAD is CEILINGED, not ignored. 50 scored conditions are never evaluated — +# 40 of them in `is_straight_line`, whose match arms cover RV32 opcodes the row +# set does not construct. (This is the one count that is IDENTICAL on both +# hosts, which is what you would expect of "never reached".) That is an honest residual, but an # UNFLOORED residual is how a number rots: a change that stopped reaching the # segment barriers would raise `dead`, lower nothing else, and pass. It is also # a third potency surface — mutation (a) moved dead 50 -> 52. From f66149879b35b0250b808ac052e4d6bfa6a32c8c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 18:57:13 +0200 Subject: [PATCH 4/5] =?UTF-8?q?TEMPORARY=20red-first=20probe=202/2=20(#912?= =?UTF-8?q?)=20=E2=80=94=20DO=20NOT=20MERGE,=20reverted=20next=20commit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Probe 1 (25a9195f) went RED on CI as required, but at the WRONG STEP for the evidence I wanted: the row-driver sanity gate (step 7) asserts `ra_validate(4) == 1` (#871: unsaved ra must be a violation), so deleting `|| rs2 == Reg::RA` fails there and the MC/DC measurement never runs. Two independent gates catching one mutation is good engineering and useless as proof that the MC/DC FLOORS bite. This probe isolates them. It restores the source byte-identical (verified: empty `git diff` vs the pre-mutation tree) and instead drops ONE truth-table row — `ra_validate:14`, the non-sp `Lw` that gives `sp_slot_load` its unique-cause pair. That touches no compiler behaviour, so: step 7 (row-driver sanity) must PASS step 8 (witness run) must PASS step 9 (MC/DC floors) must FAIL on and Conditions must stay at 130 — coverage lost, nothing deleted. That is the second of the two potency paths, and the one that proves the SCORING floor itself is what goes red, on the platform it actually runs on. Refs #912 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend-riscv/src/alloc_validator.rs | 2 +- scripts/mcdc_run.sh | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/crates/synth-backend-riscv/src/alloc_validator.rs b/crates/synth-backend-riscv/src/alloc_validator.rs index e72ec038..869f6d2a 100644 --- a/crates/synth-backend-riscv/src/alloc_validator.rs +++ b/crates/synth-backend-riscv/src/alloc_validator.rs @@ -204,7 +204,7 @@ pub fn validate_final_allocation_rv32(instrs: &[RiscVOp]) -> RaFinalVerdict { let mut saved: BTreeSet = BTreeSet::new(); for ins in instrs { if let Some((_, rs2)) = sp_slot_store(ins) - && is_saved_by_pass(rs2) + && (is_saved_by_pass(rs2) || rs2 == Reg::RA) { saved.insert(rs2); } diff --git a/scripts/mcdc_run.sh b/scripts/mcdc_run.sh index 578e1d50..80f1e19d 100644 --- a/scripts/mcdc_run.sh +++ b/scripts/mcdc_run.sh @@ -91,7 +91,6 @@ test -f "$WASM" || { echo "error: harness wasm not found at $WASM" >&2; exit 1; --invoke-with-args 'ra_validate:11' \ --invoke-with-args 'ra_validate:12' \ --invoke-with-args 'ra_validate:13' \ - --invoke-with-args 'ra_validate:14' \ --invoke-with-args 'ra_validate:15' \ --invoke-with-args 'ra_validate:16' \ --invoke-with-args 'ra_validate:17' \ From faf5c5a1c090d03ddbc74bca88408867472d6c36 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 14 Aug 2026 19:03:02 +0200 Subject: [PATCH 5/5] chore(#912): restore the probes, record the CI-platform potency evidence MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both red-first probes reverted; the tree is byte-identical to 712f658d for crates/synth-backend-riscv/src/alloc_validator.rs and scripts/mcdc_run.sh (verified with an empty \$(git diff 712f658d -- ) on each). What the two CI probes established, which the local run could not: PROBE 1 (delete the #871 condition) went RED — at the WRONG STEP. The job's own row-driver sanity gate asserts ra_validate(4) == 1 and fails there, so the MC/DC measurement never ran; the VCR-RA-003 RV32 job went red independently too. Three gates catching one mutation is good engineering and NO evidence that the MC/DC floors bite. Recording it because 'a red gate is not evidence that the gate you were testing works' generalises well past this lane — read WHICH STEP failed. PROBE 2 (drop one truth-table row, no compiler behaviour touched) isolated them. Run 31821746035: sanity gate PASS, witness run PASS, SCORING STEP FAIL. baseline 22 4 130 57 23 50 probe 2 22 3 130 56 24 50 FAIL: proved conditions 56 < floor 57 FAIL: fully-proved decisions 3 < floor 4 Decisions unchanged, CONDITIONS UNCHANGED at 130 — nothing deleted — while proved fell and a decision dropped out of full MC/DC. That is the signature of coverage lost with structure intact, produced by the MC/DC scoring step itself, on the platform the gate blocks on. Refs #912 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/mcdc_run.sh | 1 + scripts/repro/mcdc_912_gate.md | 118 ++++++++++++++++++++++++++++----- 2 files changed, 104 insertions(+), 15 deletions(-) diff --git a/scripts/mcdc_run.sh b/scripts/mcdc_run.sh index 80f1e19d..578e1d50 100644 --- a/scripts/mcdc_run.sh +++ b/scripts/mcdc_run.sh @@ -91,6 +91,7 @@ test -f "$WASM" || { echo "error: harness wasm not found at $WASM" >&2; exit 1; --invoke-with-args 'ra_validate:11' \ --invoke-with-args 'ra_validate:12' \ --invoke-with-args 'ra_validate:13' \ + --invoke-with-args 'ra_validate:14' \ --invoke-with-args 'ra_validate:15' \ --invoke-with-args 'ra_validate:16' \ --invoke-with-args 'ra_validate:17' \ diff --git a/scripts/repro/mcdc_912_gate.md b/scripts/repro/mcdc_912_gate.md index cfca9681..1ba03ef7 100644 --- a/scripts/repro/mcdc_912_gate.md +++ b/scripts/repro/mcdc_912_gate.md @@ -95,7 +95,53 @@ Excluded, named rather than hidden: has no compound decision for MC/DC to speak about. Branch coverage is the applicable criterion there. -## 3. Measured baseline (witness 0.42.0, `wasm32-wasip1`, 56 rows) +## 3. Measured baseline — and the platform is part of the measurement + +witness 0.42.0, `wasm32-wasip1`, rustc **1.96.1**, the same 56 rows, two hosts: + +| host | dec | full | cond | proved | gap | dead | +|---|---|---|---|---|---|---| +| **ubuntu-latest x86_64** (the CI platform — the floors) | **22** | **4** | **130** | **57** | 23 | 50 | +| macOS aarch64 (development) | 20 | 3 | 144 | 63 | 31 | 50 | + +Same toolchain VERSION, same witness, same rows, different HOST. These are +counts of decisions reconstructed from *lowered Wasm*, so how `std` inlines +moves them: `validate_final_allocation_rv32` presents as **9 decisions / 44 +conditions** on Linux and **4 / 43** on macOS, and `ensure_supported_target` +disappears entirely on Linux. Only `dead` is identical (50) — as you would +expect of "never reached". + +That was not predicted; it was measured, by the first CI run, after the local +baseline had already been written down. Both numbers are recorded here and in +`scripts/mcdc_gate.py` so the delta is a stated fact: **a developer running +this locally on macOS will not meet the CI floors, and that is a platform +delta, not a regression.** Use `--report-only` locally and read the delta +against your own previous run. The absolute floors belong to the platform the +gate actually blocks on. + +Witness-version invariance was checked separately — 0.28.0 and 0.42.0 give +identical numbers on the same host — so the tool is not what moves these. + +### The CI table (the one the floors come from) + +``` +function dec full cond prov gap dead +synth_backend_riscv::alloc_validator::is_ret 1 1 4 4 0 0 +synth_backend_riscv::alloc_validator::is_straight_line 1 0 52 12 0 40 +synth_backend_riscv::alloc_validator::sp_slot_load 1 1 2 2 0 0 +…alloc_validator::validate_final_allocation_rv32 9 1 44 29 15 0 +synth_backend_riscv::backend::build_options 2 1 7 5 0 2 +synth_backend_riscv::backend::compile_function_with_opts 1 0 4 1 0 3 +synth_backend_riscv::backend::count_params 1 0 4 1 0 3 +…backend::count_params::{{closure}} 1 0 2 0 0 2 +synth_core::static_data_addr::resolve_owner 1 0 2 0 2 0 +synth_core::static_data_addr::runtime_image 1 0 2 1 1 0 +synth_core::static_data_addr::validate_reloc_resolutions 1 0 2 0 2 0 +…static_data_addr::validate_reloc_resolutions_spanned 2 0 5 2 3 0 +TOTAL 22 4 130 57 23 50 +``` + +### The macOS/aarch64 table (development; where the potency deltas were taken) ``` function dec full cond prov gap dead @@ -115,19 +161,17 @@ synth_core::static_data_addr::validate_reloc_resolutions 3 0 7 TOTAL 20 3 144 63 31 50 ``` -Identical under witness **0.28.0** and **0.42.0** — 14 minor versions apart — -so the numbers are not tracking the tool's phrasing. - -**The gate reads gap rows, not a percentage.** 31 gap conditions remain and are +**The gate reads gap rows, not a percentage.** The gap conditions are printed in full by `scripts/mcdc_gate.py`, each with the vector witness says would close it. Two examples of the residual, stated so it is named: * `validate_final_allocation_rv32` carries decisions of 10 and 20 conditions (whole-function `br_if` chains after inlining). Closing those needs ≥21 co-designed vectors and is **not** claimed. -* `ensure_supported_target`'s ISA conjunction (4 gap) cannot be flipped through - public constructors: there is no `TargetSpec` with family RiscV and a - non-RiscV32/64 ISA. +* `ensure_supported_target`'s ISA conjunction (4 gap on macOS; the function + does not survive inlining on Linux at all) cannot be flipped through public + constructors: there is no `TargetSpec` with family RiscV and a non-RiscV32/64 + ISA. `is_ret` went 1-proved/3-gap → **4-proved/0-gap** by adding exactly the three vectors witness printed, which is the practical demonstration that the gap rows @@ -152,18 +196,20 @@ surface" class: 3. **A ratio cannot notice a deleted condition** — removing one removes its gap row and the percentage *improves*. So the floors are counts. -Declared floors = the measured baseline, no slack: -`decisions ≥ 20`, `conditions ≥ 144`, `proved ≥ 63`, `fully-proved decisions ≥ 3`, +Declared floors = the **CI platform's** measured baseline, no slack: +`decisions ≥ 22`, `conditions ≥ 130`, `proved ≥ 57`, `fully-proved decisions ≥ 4`, and `dead ≤ 50`. -**Dead is ceilinged, not ignored.** 50 of the 144 scored conditions are never +**Dead is ceilinged, not ignored.** 50 scored conditions are never evaluated — 40 of them in `is_straight_line`, whose match arms cover RV32 opcodes the row set does not construct. That is an honest residual, but an UNFLOORED residual is how a number rots: a change that stopped reaching the segment barriers would raise `dead`, lower nothing else, and pass. It is also a third potency surface — mutation (a) moves dead 50 → 52. -## 5. Red-first potency — two mutations, two distinct failure paths +## 5. Red-first potency — measured on both platforms, and one surprise + +### On macOS/aarch64 (local; baseline 20 / 3 / 144 / 63 / 31 / 50) Both mutations restored afterwards; `git diff` byte-identical. @@ -171,7 +217,6 @@ Both mutations restored afterwards; `git diff` byte-identical. RV32 allocation validator's save-set predicate: ``` -baseline TOTAL dec 20 full 3 cond 144 proved 63 gap 31 dead 50 mutated TOTAL dec 19 full 2 cond 142 proved 54 gap 36 dead 52 FAIL: scored decisions 19 < floor 20 FAIL: scored conditions 142 < floor 144 @@ -180,7 +225,8 @@ FAIL: fully-proved decisions 2 < floor 3 FAIL: dead conditions 52 > ceiling 50 ``` -The **condition-count** drop is the signal a ratio-only floor cannot produce. +The **condition-count** drop is the signal a ratio-only floor cannot produce: +delete a condition and the *percentage improves*. **(b) Weaken the vector set** — drop ONE truth-table row (`ra_validate:14`, the non-`sp` `Lw` that gives `sp_slot_load` its unique-cause pair): @@ -191,7 +237,49 @@ FAIL: proved conditions 62 < floor 63 FAIL: fully-proved decisions 2 < floor 3 ``` -Conditions unchanged, coverage lost — the second failure path. +Conditions unchanged, coverage lost — a different failure path. + +### On the CI platform, where the gate actually blocks + +Both mutations were then pushed to the PR branch and run on CI, because a +potency result taken on one host does not obviously transfer to a host where +the same function presents as 9 decisions instead of 4. "It obviously still +works" is the reasoning this lane exists to distrust. + +**Mutation (a) went red at the WRONG STEP, and that is worth recording.** The +job's own row-driver sanity gate (step 7) asserts `ra_validate(4) == 1` — +"#871: unsaved `ra` must be a violation" — so deleting the condition fails +*there* and the MC/DC measurement never runs. The commit is red, and the +`VCR-RA-003 RV32` job goes red independently, so the change cannot land. But +two other gates catching one mutation proves nothing about whether the **MC/DC +floors** bite. + +**Mutation (b) isolates them,** because dropping a truth-table row changes no +compiler behaviour: the sanity gate passes, the witness run executes, and the +failure has to come from the scoring step or not at all. Measured, run +`31821746035`: + +``` +step 7 Row-driver sanity gate (host) success +step 8 Run the MC/DC rows under witness success +step 9 Score synth's own decisions against the floors FAILURE + +TOTAL 22 3 130 56 24 50 +FAIL: proved conditions 56 < floor 57 +FAIL: fully-proved decisions 3 < floor 4 +``` + +Against the CI baseline `22 / 4 / 130 / 57 / 23 / 50`: decisions unchanged, +**conditions unchanged at 130** — nothing was deleted — while `proved` fell +57 → 56 and one decision dropped out of full MC/DC. Exactly the predicted +signature of *coverage lost, structure intact*, produced by the MC/DC scoring +step itself, on the platform the gate blocks on. + +Restored immediately afterwards (`scripts/mcdc_run.sh` byte-identical to the +pre-probe tree), and the source mutation from probe 1 likewise. + +The lesson generalises past this lane: **a red gate is not evidence that the +gate you were testing works.** Read which step failed. ## 6. Two invocation traps, encoded in the scripts