diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 59ea6bcb..575dc440 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3566,3 +3566,116 @@ 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 + # 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 + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-mcdc-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-mcdc- + - 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 + # 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" bash 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..767bcb2c --- /dev/null +++ b/crates/synth-mcdc-harness/src/lib.rs @@ -0,0 +1,640 @@ +//! 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 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 +/// 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..e1d48ee0 --- /dev/null +++ b/scripts/mcdc_gate.py @@ -0,0 +1,268 @@ +#!/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. +# +# 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. +# +# 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 = 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. +CEILING_DEAD = 50 + + +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 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: + 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..1ba03ef7 --- /dev/null +++ b/scripts/repro/mcdc_912_gate.md @@ -0,0 +1,293 @@ +# RQ-57-MCDC (#912) — MC/DC structural coverage: surface, measurement, potency + +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`. + +## 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 — 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 +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 +``` + +**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 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 +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 **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 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 — 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. + +**(a) Delete a condition** — remove the #871 fix `|| rs2 == Reg::RA` from the +RV32 allocation validator's save-set predicate: + +``` +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 +FAIL: dead conditions 52 > ceiling 50 +``` + +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): + +``` +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 — 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 + +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).