Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 35 additions & 21 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -862,31 +862,45 @@ jobs:
# ONLY (no unicorn/wasmtime).
- name: Run VCR-DEC-001 graph-alloc spike differential (#242, thumb2)
run: python scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth
# VCR-DEC-001 increment 2 (#242): EXECUTION-gate the DIVERGENT bytes the
# join-aware colouring now produces. This is NOT redundant with the byte
# differential above: increment 1's correctness followed transitively from
# byte identity, and increment 2 broke that. `validate_cfg_rewrite` — the
# pass's own CFG-lifted trace-equality oracle — SHARES the CFG shape with
# the pass it validates, and #872 is the standing lesson that a validator
# can share its pass's blind spot, so the new bytes get EXECUTED: unicorn
# runs the flag-ON image and compares return value + linear-memory window
# against wasmtime, over every join shape the allocator reaches (real
# if/else, if-without-else, desugared block+br_if, early return, counted
# and data-dependent loops, two-level br_if). PROVEN non-vacuous by
# MUTATION: emptying `cfg_exit_observable` (the exit contract the pass and
# its validator SHARE) while removing the churn bias that masks it emits
# code leaving the return value in the wrong register — validate_cfg_rewrite
# AND VCR-RA-003 both ACCEPT it and only this gate catches it (16 wrong
# results). The grep asserts the NON-ZERO check count AND a non-zero
# engaged-function count from the machine-readable summary: exit 0 alone is
# not trusted, and a run where the allocator stopped changing bytes would
# pass every comparison while gating nothing.
- name: Run VCR-DEC-001 join-allocator execution differential (#242, thumb2)
# VCR-DEC-001 increments 2+3 (#242): EXECUTION-gate the DIVERGENT bytes the
# join- and call-aware colouring now produces. This is NOT redundant with
# the byte differential above: increment 1's correctness followed
# transitively from byte identity, and increment 2 broke that.
# `validate_cfg_rewrite` — the pass's own CFG-lifted trace-equality oracle
# — SHARES the CFG shape with the pass it validates, and #872 is the
# standing lesson that a validator can share its pass's blind spot, so the
# new bytes get EXECUTED: unicorn runs the flag-ON image and compares
# return value + linear-memory window against wasmtime, over every join
# shape the allocator reaches (real if/else, if-without-else, desugared
# block+br_if, early return, counted and data-dependent loops, two-level
# br_if). PROVEN non-vacuous by MUTATION: emptying `cfg_exit_observable`
# (the exit contract the pass and its validator SHARE) while removing the
# churn bias that masks it emits code leaving the return value in the wrong
# register — validate_cfg_rewrite AND VCR-RA-003 both ACCEPT it and only
# this gate catches it (16 wrong results).
#
# Increment 3 (v0.54) adds the CALL shapes and the same argument applies
# with MORE force: the AAPCS contract (`liveness::call_effect`) is SHARED
# by the pass and the validator on purpose (two hand-maintained copies
# would be the VCR-ORACLE mirror-pinning failure mode), so neither can
# catch an error IN the contract. Both halves are executed — the CLOBBER
# half (a value live across a `bl`, incl. self-recursion) and the ARGUMENT
# half (5/6/7-argument callees that pack each argument into its own nibble,
# register AND stack). Likewise proven non-vacuous by MUTATION: emptying
# `call_effect`'s clobber set makes the colourer home a cross-call value in
# R0-R3; `validate_cfg_rewrite` accepts it and only this gate fails it.
#
# The grep asserts the NON-ZERO check count, a non-zero engaged-function
# count AND the ≥4 engaged CALL-shape floor from the machine-readable
# summary: exit 0 alone is not trusted, and a run where the allocator
# stopped reaching call-containing functions would pass every comparison
# while leaving the whole increment-3 class ungated.
- name: Run VCR-DEC-001 join+call allocator execution differential (#242, thumb2)
run: |
set -o pipefail
SYNTH=./target/debug/synth python scripts/repro/vcr_dec_001_join_alloc_execution_differential.py | tee ga_join.out
grep -q "^VCR-DEC-001-JOIN CHECKS=" ga_join.out
awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0) ok = 1 } END { exit ok ? 0 : 1 }' ga_join.out
awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0 && $8+0 >= 4) ok = 1 } END { exit ok ? 0 : 1 }' ga_join.out
# #798/#879: the RV32 active-data-segment FULL-BOOT oracle — found
# un-wired in the same #879 audit as the gpio gate. clang+lld build a
# bare-metal riscv32 firmware from synth's object + generated startup/
Expand Down
78 changes: 78 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,84 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## [Unreleased]

### Added

- **VCR-DEC-001 increment 3 (#242): the graph-colouring allocator colours ACROSS
CALLS.** Increment 2's second-largest decline bucket was `call` /
`call-indirect` — 68 of the measured corpus — because a `bl` had no modeled
effect and the join CFG builder refused the whole function. The AAPCS call
boundary is now modeled: `liveness::call_effect` states the contract ONCE
(`defs = {R0,R1,R2,R3,R12,LR}`, `uses = {R0..R3}` plus a `blx`'s target,
conservatively all four argument registers since the callee's signature is not
visible), and BOTH the pass (`graph_alloc::joins` — liveness, interference,
identity pins) and its acceptance oracle (`validate_cfg_rewrite`'s backward
transfer) consume that one definition. Modeling it in the pass alone would
have been the #872 defect verbatim: a validator that treats `bl` as
effect-free accepts a non-identity equation across it, i.e. it certifies its
own pass's *"live value parked in call-clobbered scratch"* miscompile — and
that is exactly what `validate_cfg_rewrite` did before this change. Calls are
emitted verbatim with both rename maps re-checked as the identity;
single-block functions containing a call are now taken too (increment 1
structurally cannot, since a call is not `is_straight_line`). `reg_effect` is
deliberately NOT widened — its `None`-on-call is load-bearing for the shipping
pipeline (fail-safe prologue, `shrink_callee_saved_saves`' decline, VCR-RA-003
invariant 1), so widening it would move shipped bytes.

**Measured** (`scripts/repro/vcr_dec_001_join_alloc_measure.py`, ARM repro
corpus, ELF-symtab bytes + `--emit-wcet` sound bounds):

| path | increment 2 | increment 3 |
|---|---|---|
| relocatable | −46 B (−0.11 %) / −25 cyc, 275 applied, 8 shrank / 1 grew | **−100 B (−0.24 %) / −33 cyc, 307 applied, 24 shrank / 5 grew** |
| self-contained | −70 B (−0.14 %) / −9 cyc, 81 applied, 10 shrank / 1 grew | **−120 B (−0.24 %) / −17 cyc, 108 applied, 27 shrank / 3 grew** |

Zero WCET-bound regressions on either path (12 functions' bounds shrank, 0
grew). Decline histogram: `call` 57 → **0** (taken); `call-indirect` 11 → 11
(renamed `call-indirect-pseudo` — the high-level `Call`/`CallIndirect`
pseudo-ops are expanded downstream into a bounds guard + table load + result
move, so the register footprint here is not the one that ships, and they stay
declined by name). The residual buckets are `unmodeled-op` 174, `single-block`
73, `identity-colouring` 31, `unreachable-block` 11, `call-indirect-pseudo` 11,
`numeric-branch` 10.

Still **flag-off by default** (`SYNTH_GRAPH_ALLOC`): this is a measurement
spike, not a behaviour change. Frozen anchors byte-identical, 10/10.

**Mutation evidence.** The AAPCS contract is shared by the pass and the
validator on purpose (two hand-maintained copies would be the VCR-ORACLE
mirror-pinning failure mode), so neither can catch an error *in* the contract —
only execution can. Emptying the ARGUMENT half (with the churn bias replaced by
a churn-maximising one, which otherwise masks it) makes the colourer re-home
argument staging and yields **5 wrong results** in
`vcr_dec_001_join_alloc_execution_differential.py` — `call6(1,2,3,4,5,6)`
returns `0x00651321` instead of `0x00654321` — while `validate_cfg_rewrite`
AND VCR-RA-003 both accept it; the churn-maximising bias *alone*, with the
contract intact, produces **0 wrong results**, so the failure is attributable
to the contract and nothing else. Emptying BOTH halves — the pre-increment-3
effect-free `bl`, the briefed hazard — is killed by three unit tests. Emptying
the CLOBBER half alone is NOT caught, and that is documented on `call_effect`
rather than papered over: with the conservative `uses` intact the two halves
overlap for the R0-R8 pool, so `defs`' independent duties today are the
non-pool `{R12, LR}` and keeping the pass from proposing colourings the oracle
would reject. A future increment that makes the argument set arity-precise
makes `defs` the sole soundness guard for R0-R3 — narrow one and widen the
tests for the other in the same change.

### Changed

- `vcr_dec_001_join_alloc_execution_differential.py` gains an increment-3 CALL
population covering both halves of the contract: the CLOBBER half
(`local_promote_cross_call::cross_call`, `intra_module_callee_saved::a` — both
written so a caller-saved home is observably wrong — and the self-recursive
`stack_canary_687::recurse`) and the ARGUMENT half (`call_5args::caller`,
`call_6_7args::call6`/`call7`, whose callees pack each argument into its own
nibble). The harness now passes arguments per AAPCS (0-3 in R0-R3, 4+ on an
8-byte-aligned stack), verifies each declared call shape really CONTAINS a
`bl`/`blx` in its emitted bytes, and enforces its own non-vacuity floor (≥4
divergent call-containing functions) which the CI wiring re-asserts from the
`CALLSHAPES=` summary field (#890). 56/56 checks, 19 engaged functions of which
6 are call shapes.

## [0.53.0] - 2026-07-30

**"The last mile" — seven lanes.** falcon's VFP wall comes down, RISC-V compiles
Expand Down
Loading
Loading