ADR structure-dominator-tree gets "the noreturn guard": the invariant (the arm
that ends in a call to a callee declared never to return cannot complete, so the
other arm's statements run on the same paths in the same order), the owner
(`structure/guard.rs`, last in `render::structured`, certificate-gated), the
evidence (`Evidence::never_returns`, the declaration and never a name), the
complexity (O(statements), each visited once), the other arm over a marked negated
atom, the exactly-one-arm rule, and the measurements below. ROADMAP D75 records
what landed, what was measured and what was found.
Mined set (1,595 scored, DecBench's GED), base a0d9e34a to 23728d11: perfect 261 to
268 (7 newly, 0 lost), mean 43.99 to 43.91, total 70,163 to 70,040, 45 functions
better and 13 worse (the source's spelling read; `test_flush` is one edge moved), gotos and refused unchanged, 108
of 1,639 pairs change. Corpus (bash, ls-toybox, pigz, 0pack, pumasim, 26,935
functions): 1,136 change (828 braces and indentation only, 308 an else arm swapped,
0 other), none newly refused, gotos 27,108 and residual sites 157,006 unchanged.
Census 442 + 24 unmoved; certification 50 rendered, 30 refused, 0 panicked, 0
crashed, 0 invented, 0 dropped; workspace suite 3,027 passed, 0 failed; release
`pdd` on Apple M5, 0pack 0x62ecf0 +0.11% instructions retired, pumasim 0x23fdf0
byte-identical and -0.03%.
Held-out set, report only (bash, diffutils, findutils, gzip, libexpat at both levels, 5,150 functions): 203 change
(131 braces and indentation only, 72 an else arm swapped, 0 other), none newly refused, gotos 13,098 and residual sites
33,918 unchanged; GED over the 4,759 scored: perfect 1,350 to 1,357 (7 newly, 0 lost), total 117,742 to 117,595.
Hand reads (command `r2s -q -c 'aa; pdd @ ADDR' BINARY`, base and head): 0pack
0x491dee, `if (r == 0) { return x; } else { __throw_system_error(e); }` is
`if (r != 0) { __throw_system_error(e); } return x;`; 0pack 0x47ca92, the string
constructor's null check is `if (p == 0) { __cxa_throw(...); }` with the writes
after it; pumasim 0x27dec0, `if (a <= 0 || b >= c) {} else { fwrite(...); exit(1); }`
is `if (a > 0 && b < c) { fwrite(...); exit(1); }`; 0pack 0x6e3990 keeps
`goto L8` after the guard; bash 0x435f0 turns empty then arms into guards.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`x = c ? a : b;` and the `if` that assigns it are the same C when both arms are
side-effect free and their operands are values, and AGENTS rule 8 forbids control
the machine did not have. The ADR separates the three owners of a `?:` in a
rendering (an r2il Select, the renderer's own overshift guard in `terms.rs::shift`,
and a branch-born selection `shape::select` writes from a diamond), states what
the machine had for each, and measures the counterfactual on the mined set.
Mined set, 1,595 scored, build 23728d11: 2,708 `x = c ? a : b;` statements in 555
of 1,639 functions, 50 of them branch-born (2 functions), 1,755 overshift guards
by the shape of their condition, 903 data selects. Respelling every `?:` as an
`if` (the counterfactual script's transform): perfect 268 to 282, total GED 70,040
to 67,122, 369 better and 22 worse. Respelling only the 50 branch-born ones (a
build with `shape::select` not run): perfect 268 to 268, total GED +59, 11 better
and 27 worse. So the lever sits in selects the machine has no branch for and in
guards that are not selects at all. Folding the 150 overshift guards whose count is
a literal (`(uint32_t)8U >= (uint32_t)32U ? 0 : x << 8`, 40 functions) is a text
counterfactual of 70,040 to 68,852, 40 better and 0 worse, and spells no control:
recorded in ROADMAP D75 as found, not built.
Recommendation: keep `?:` (A); the one subset a CFG fact licenses is worth nothing
on the score; reading the source's shape from DWARF line tables (C) is the only
sound route to the rest and does nothing for the stripped DecBench binaries.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
A chain written on the arm that falls to the exit is the guard's test as it
stands (`a_conjunction_whose_arm_exits_is_a_guard_with_the_rest_after_it` through
the engine: `if (a != 0 && b != 0) { exit(1); } return 0;`, the chain stage having
chosen the exit's side already), and a chain whose exit is on the else arm is
negated by swapping its connective with its tests, which the unit test
`a_chain_on_the_swapped_arm_is_negated_by_swapping_its_connective` states on the
tree. Tests only; the measured build is unchanged.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The guard needs a continuation: one arm ends in the call and the other carries
on. Where both end in such a call nothing runs past either, and spelling one as
the guard writes the other arm's statements as if the function went on after it.
Both arms are now rewritten first and the guard applies when exactly one ends in
the call, which also drops the second visit of the statements a swap frees (each
statement is visited once, in both directions).
Measured on the mined set (bzip2, zlib, grep at O2 and O2-noinline, 1,595 scored,
DecBench's GED): bzip2 `mySIGSEGVorSIGBUScatcher` at O2-noinline was GED-perfect
and lost it (0 to 6) when `if (c == 1) { cleanUpAndFail(3); } else { showFileNames();
cleanUpAndFail(2); }` was written `if (c == 1) { cleanUpAndFail(3); } showFileNames();
cleanUpAndFail(2);`, the one perfect row the unrefined guard lost.
Failing first: with `(true, _)` for the then-arm case the engine test
`two_arms_that_both_end_in_a_call_that_never_returns_keep_their_else` fails
(crates/r2engine/tests/engine/structure.rs:923, the rendering has no `else`); the unit
test `two_arms_that_never_return_leave_neither_as_the_guard` states it on the tree.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`if (c) { rest } else { f(); }` with `f` declared never to return is spelled
`if (!c) { f(); } rest`. A test the lowering wrote carries no marker and the
certificate reads a negation only over a marked atom, so the guard writes the
test as one atom carrying copies of the `if`'s markers, as loop rotation does,
and `respell_negations` writes the opposite comparison after the final
certificate. An `if` nothing observed keeps its else (no markers to copy), and
where both arms end in such a call the then arm is the guard and the polarity
stays. The statements the swap frees are already visited, so each statement is
still visited once.
`condition::as_atoms` and `condition::negated` are what `rotate` had privately;
they move to the owner of marked tests and rotation uses them. The marker
fixture of rotation's tests moves to `structure/support.rs` for the guard's.
Failing first: with the swap disabled the engine test
`an_else_arm_that_never_returns_is_a_guard_on_the_opposite_test` fails
(crates/r2engine/tests/engine/structure.rs:898, the rendering keeps `} else {`).
`test edi, edi; je rest; mov edi, 1; call exit; rest: mov eax, 7; ret` rendered
`if (arg0 == 0) { return 7; } else { exit(1); }` and renders
`if (arg0 != 0) { exit(1); } return 7;`. The unit tests: the swap certifies, and
the same arms under the unnegated test are an `EdgeMismatch` at the test's block.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`if (c) { f(); } else { rest }` with `f` declared never to return is spelled
`if (c) { f(); } rest`. The then arm cannot complete, so `rest` runs on exactly
the paths the else arm took, in the same order. The stage is `structure/guard.rs`,
last in `render::structured`, one `Evidence::never_returns` in (the predicate the
tails and the certificate already read: the callee's declaration, never a name),
kept only while the control certificate holds and reverted whole otherwise.
O(statements): each statement is visited once, a guard's else statements join the
sequence they sit in. Only the then arm is a guard: `if (c == 0) return 7; else
exit(1);` needs the test negated, which the certificate reads from a marked atom
and a lowered test has none, so it keeps its else.
Failing first: with the stage not run, the three engine tests that state the
guard fail on crates/r2engine/tests/engine/structure.rs (lines 824, 842 and 862:
an arm that ends in exit, two guards with a store between them, the statements of
the arm the guard frees); the three negatives (puts, `call rax`, a never-returning
else arm) pass both ways, as they should. `test edi, edi; jne cold; mov eax, 7;
ret; cold: mov edi, 1; call exit` rendered `if (arg0 != 0) { exit(1); } else {
return 7; }` and renders `if (arg0 != 0) { exit(1); } return 7;`.
Unit tests beside the rule: the then arm frees the else and certifies; the leaves
run in the else's order through two nested guards; evidence that does not declare
the call leaves the tree equal; an else arm that never returns is not a guard; a
guard on evidence the machine does not have fails the certificate (so the stage
is reverted). The `exit` fixtures of the tails tests move to `structure/support.rs`.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
Three read-only designs and a judge (library prototypes into values, widths from reads, a proven
return or void) gave measured expectations well under the DecBench class ceilings: about +27 to +32
net union rows together against the 270 rows between r2s and kuna. D70 repairs the soundness gate
first (it splits function pointer parameters on every comma and accepts r2s's own `arg0` as a source
name), D71 and D72 are the two items to build, D73 waits for a measurement, D74 holds the real
findings (a dereferenced parameter declared integer, a silently wrong void, stack arguments past six
never recovered), and D75 names the structurer respellings as the larger measured lever.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The source body and the source graph each took the first preprocessed unit, in discovery
order, whose text or CFGs held the function's name, so a static function defined in
several units showed another unit's body and graph. The unit is now the owner the binary's
DWARF gives the address (binfmt.source_function_owners, with the run's abstract-origin
policy), as ged_causes and counterfactual_ged already take it; a function with no owner
prints "no DWARF owner" and no source. The DWARF variables came from a loop that accepted
any address whose only function carried the name; they are now what the type metric's own
_ground_truth_for_function joins for the address, so the display shows what was scored.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
pick_source fell back to the first translation unit, in sorted order, that defined a
same-named function when the binary's stem named no unit, so a binary with static
functions of one name in several units could be scored against another function's graph
and the mined and held-out gates would approve or reject a structurer change on the wrong
GED. The driver, ged_causes and counterfactual_ged all ask the compiled binary's DWARF
for the owner of each address (binfmt.source_function_owners, with the run's abstract-origin
policy); score does now too, and the source CFGs are cached by unit and name instead of by
name alone (a new cache file name, so a stale cache is never read as the new shape).
A function with no owner is scored "no_owner" and one whose owner yields no CFG
"no_source_cfg", as the driver abstains. score prints both counts per binary and pair
prints them per run. The compiled binary is found through the stripped copy, which keeps
its file name: a stem map over compiled/ would meet <stem>.i and <stem>.c.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The stripped file was looked up as stripped/<toml stem>, so libz.so.1.2.13 (stem
libz.so.1.2) never existed and the loop skipped it with a bare continue: its time and
peak RSS were missing from the totals without a word. The directory is now read into a
{stem: file} map by run_gate.binaries_by_stem, which mined_set.dump uses too. A toml with
no stripped file prints a NO-STRIPPED-BINARY row, and the run ends with a stderr line
that counts timed, unresolved and failed binaries.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The project was loaded only under `if not a.no_source`, and the graph block read it
whenever --graphs was given. It is now loaded when either the source or the graphs are
asked for, and not for the rendering alone. main takes argv so the test can drive it
over stand-ins for DecBench and a dict for the checkpoint.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The equivalence ratchet's 828 records come from eight small C files, so none of the real-binary
functions D58, D59 or D65 move (55, 12 and 215) is covered by it. The skeptics' hand-run differential
execution and their uninitialized-read sweep found what the goldens, the suite, the census and the
equivalence run missed, and live in scratch. D67 also records that r2s's mean GED is unexplained.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The 2026-10-17 record scored no bash row for r2s, kuna or ghidra, so its "r2s 4th of 4"
compared 692 angr-only rows as misses for the other three. On all 6,978 rows r2s is third
on union-perfect (28.0%), first on byte_match and third on GED and type_match. D51 and the
measurement ADR carry the corrected figures, the old record says it is superseded, and D52's
type_match target moves to kuna's 539 (8.5%) on the corrected population. The chains and
tails cut gotos 36% for +6 union rows, so D67 orders the next work by ceiling: library
prototypes into values, a proven return, widths from reads, one object per web.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
Two structuring items graded their changes with scratch scripts: dump every
function of bzip2, zlib and grep at O2 and O2-noinline with each build, score
with DecBench's GED, pair the two runs. mined_set.py is that, in three steps
(dump, score, pair), with the pinned lists that split mining (bzip2, zlib, grep)
from held-out (the other five projects, nightly and at an item's exit).
pair reports the perfect count (newly, lost), mean and total GED, gotos, functions
with a goto, functions whose text changed and newly refused ones, and refuses to
pair a mining run with a held-out run. On the scratch scores of the s3 step it
prints the numbers the scratch pairing script did (perfect 60 -> 55, mean GED
49.11 -> 48.33, total 21509 -> 21170, gotos 4143 -> 4080). dump finds the stripped
binary by the driver's stem (libz.so.1.2.13 is libz.so.1.2); the scratch
measure.py looked for a file named by the stem and would have skipped it.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
report_decbench.py now prints, for the decompilers the results name (or --compare),
the rows every one of them scored, how many rows that left out, how many rows each
has no score for, and per project and decompiler scored over rows, then perfect
count and mean over the common rows. It exits 73, before it compares or accepts a
baseline, when a compared decompiler scored nothing in a project, or fewer than
--min-scored-fraction of the rows. A decompiler is owed only the cells it ran in
when the results are a merge of shards.
On the 2026-10-17 results it stops at 'kuna scored 0 of 4144 rows of bash'; on the
2026-10-23 results it passes. run_decbench.sh forwards --compare.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The 2026-10-17 run lost every bash evaluation to the OOM killer, evaluate_project
returned {} and the scoreboard dropped the rows without a word. run_gate.py
checks, after the driver, that each binary a decompiler rendered in this run has
a score key of that decompiler in evaluated/<binary>.toml; the 16-byte
'binary = "bash"' file, a missing file and a file that scores only other
decompilers exit 71. On the 2026-10-17 tree it reports 55 of 192 cells, all bash.
More than one worker is refused (exit 72) for a binary whose decompiled C is over
8 MB: before the run for C already in the tree, by evaluate_checkpointed.py, and
inside the driver before evaluate_project, as SystemExit because the driver
catches Exception there and goes on with {}. run_decbench.sh also expands its
empty arrays in a way bash 3.2 accepts.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The backend pickled the whole partial result after every function: 2.5 MB each
on bzip2 and 18 MB on bash, quadratic in the function count, which is why the
bash backend took 1,253 s and 1,723 s against about 140 s for r2s alone. It
now writes a checkpoint when R2SLEIGH_CHECKPOINT_SECONDS (default 30) have
passed since the last one, and once more when the run ends or fails, so a kill
loses one interval of answers at most.
A checkpoint carries the r2s build, the binary's sha256 and the targets with
their names. A re-run that finds one for the same task asks r2s only for the
addresses it has no answer for; one for another task is not read.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
run_batch called on_answer for a process's answers only after that process had
ended, so a consumer that checkpointed from it kept nothing of a run killed
mid-process, and a failing consumer could not stop r2s. The answer now goes to
on_answer the moment it is final, in request order, and a callback that raises
kills the r2s process it was reading.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The 2026-10-17 run scored no bash row for any decompiler except 692 angr rows: the host's OOM killer took the
evaluation worker (5.2 GB for r2s's bash) and evaluate_project returned {} for every bash binary. On the 2,736 rows
all four have, r2s moved union 689 to 695, GED perfect 589 to 594, type_match 90 to 91; functions with a goto fell
1,054 to 732. With bash scored for all four, r2s is third on union (28.0%).
tests/decbench: compare_runs.py (tables, deltas, paired counts), type_causes.py (one verdict per DWARF variable from
DecBench's own matcher, asserted equal to the stored value), ged_causes.py and counterfactual_ged.py (block-graph
deltas and respelling re-scores), evaluate_checkpointed.py (the driver's functions on stored decompilations),
r2s_timing.py, show_function.py, a test for their pure parts, and a README section on memory and coverage.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`import_stub` took the import's name from discovery (`import_at(entry)`) and
its signature from the callee the body transfers to, and checked only that the
callee's class was an import. A container-stated stub whose bytes jump through
another import's slot (a patched Mach-O `__stubs` entry) passed: `free`
rendered as `extern void* free(uint64_t)`, `malloc`'s types under `free`'s
name.
The address the transfer reaches must now be bound, by `import_at`, to the
same import the entry is stated as. Both sides are the container's statement
(the stub table, the loader's write into the slot), not the callee identity's
spelling. Otherwise the function is no stub: it renders as a body, and
`R2DEC_TRACE_REFUSAL` prints the stated import, the address reached and what
is bound there. `import_stub` now asks `Program` itself, so `stub_of` takes
the program; the body proof is split out as `lone_transfer` to stay under the
function-length ratchet.
Test `a_stub_whose_jump_goes_to_another_import_is_a_body_not_the_stated_stub`
fails at 298ae95b with
`/* r2sleigh: import stub at 0x1010; this symbol is the import `free` ... */
extern void* free(uint64_t);` and now renders the function with its
`UnresolvedIndirectBranch` gap. `a_stub_the_container_states_is_its_import_s_declaration_where_its_jump_agrees`
pins the container-stated stub whose jump agrees.
Measured, release, base 298ae95b against this tree: pdd of every function of
bash and pumasim (16,866) is byte-identical, 0 changed (pumasim's 522 import
stubs unchanged); pdd of all 6,878 `sym.imp.*` functions of the 781 small
radare2 test ELF, Mach-O and PE binaries (2,222 ELF and 2,814 Mach-O stub
renderings) identical, afl identical. cargo test -p r2engine --all-targets
628 passed; golden 442 and stable_temporaries 24 unmoved;
structure-report.sh exit 0, counts unmoved; fmt, clippy --tests -D warnings
and comment_runs --base clean.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
r2engine's stub route asked the body alone: one tail transfer to a
callee r2types resolves as an import, no effect beside it. A function in
`.text` that ends in a jump to an import's stub passed, whatever came
before: a test, a return on another path, arithmetic on the argument.
`afl` listed none of them as an import, and `pdd` declared them away as
the import itself. Two owners decided one fact and disagreed.
Discovery owns it. `program::naming::imports` reads the stubs the
container states and decodes the linkage sections, and
`Program::import_at(entry)` answers it in O(log stubs).
`native::sealed` now asks it, and `SealedFunctionAnalysis::stub_of` runs
`stub::import_stub` only for a stated import, which then proves the body
is only the transfer and names the stub as discovery does. The two entry
points that have no program, `seal_function_from_input` and
`decompile_function_from_input`, no longer take the route.
Hand-read, release build, DecBench's stripped bzip2 O2:
r2s -q -c 's 0x5b00; pdd' bzip2
before: /* r2sleigh: import stub at 0x5b00; this symbol is the import
`free` and has no body of its own. */
after: void fcn_5b00(void) { void free(void*); ...
if ((uint8_t)((uint64_t)r2sleigh_residual_u64(1) == 0U)) { return; }
else { free((void*)r2sleigh_residual_u64(2)); return; } }
r2s -q -c 's 0x5b20; pdd' bzip2
before: import stub at 0x5b20; this symbol is the import `malloc`
after: uint64_t fcn_5b20(void) { ... return malloc(product of two
residual reads); }
`test rsi, rsi; je; mov rdi, rsi; jmp free` and `imul esi, edx; movsxd
rdi, esi; jmp malloc` keep their test and their product. The parameters
come out as residuals with the proof line saying so ("1 argument slot
read with no parameter"): the unread `opaque` makes the arity floor a
P7 matter, not this one's.
The 63 DecBench rows r2s declined this way (2026-10-23, refusals of the
48 binaries on contabo): 52 write an argument register before the jump,
2 test first, 9 are a bare `jmp` to the stub. All 63 render now: 22
without a residual, 24 with a parameter the body reads and nothing
declares (P7), 16 with an int result whose upper half is a residual
(W47), 1 with both. 380 declined rows becomes about 317 if nothing else
moves; the run is the main session's.
Over bash, ls-toybox, pigz, 0pack and pumasim (26,935 functions, base
and this build in one session each): 1,415 rendered as an import stub at
the base. 1,200 are `afl`'s `sym.imp.*` and stay stubs. 215 are
functions with a name or a body of their own (0pack 100, pumasim 90,
bash 13, ls-toybox 12) and render now: none newly refused, no goto
added, +86 residual sites, instructions retired and peak RSS flat (290 s
and 575 MB both). The base was wrong on them: pumasim's
`QLayoutItem::~QLayoutItem()` deleting destructor (`0x295d10`) printed
as `extern void _ZdlPvm(void*, uint64_t)` with its constant size
dropped, and a static initialiser's `__cxa_atexit(f, p, d)` as the
import itself. Where the import has no declaration the function is now
a visible `TailTransferNotRendered` gap (ls-toybox `0x34ac0`,
`getxattr`) rather than a silent "prototype nothing states".
Tests: `a_guarded_wrapper_of_a_stub_is_a_body_not_the_stub`,
`a_wrapper_that_computes_the_stub_s_argument_is_a_body_not_the_stub` and
`a_function_that_only_jumps_to_a_stub_is_a_body_not_the_stub` fail with
the base route (checked); `an_import_stub_is_its_import_s_declaration`
and `an_effect_before_the_jump_keeps_a_stub_a_body` still hold.
Gates: fmt; clippy --workspace --all-features --tests -D warnings;
cargo test --workspace --all-features --no-fail-fast: 3001 passed, 0
failed, 8 ignored; golden 442 and stable_temporaries 24 unmoved;
structure-report.sh exit 0 with no count moved; Dylint 12 (baseline 12);
comment_runs --base, check_shards; certify_render --limit 24
--functions 8 identical to the base (50 rendered, 30 refused, 0
invented); `afl` identical to the base over 40 radare2 test binaries and
all 333 `sym.imp.*` functions render as before. diff_r2.py refuses this
checkout's radare2 6.2.5 (its judgments are against 6.2.4), so it was
not run.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
doc/adr-decompiler-rewrite.md gains "A name is read where its definition has run (D68)": the
defect (D58's reverse postorder is not dominance; r2ssa's lane pick was the wrong fact), the owner
(r2ssa: defined_before, narrowed_argument, validate_boundary_values), the guard in r2dec and why it
is a hard rule and not a debug_assert, the siblings of the pick, the measurements and the
mutation table. ROADMAP gains the D68 row; D58's row says bash 0x26760 has 221 residual sites and
1,026 residual obligations (it said 227 and 1,106; the binaries and the base print 221 and 1,026),
and that pumasim's "2 fewer" are 0x279d80 and 0x27b040 reading a lane their block does not dominate
(it said a definition the old write order read before spelling it).
Measured at the code tip against 15486ea7 (pddj of every function, same method):
functions changed 2 of 25,735 (pumasim 0x279d80, 0x27b040); 0 of 14,034 in ten more
newly refused 0 of 25,735, 0 of 14,034, 0 of 1,920 generated float functions
names read out of scope 4 in 2 functions at the tip, 0 now over bash, ls-toybox, pigz, 0pack
and pumasim, and 0 under O1, O2 and O3 on all five
clang -Wuninitialized pumasim 13 to 11 functions, others equal; 56 of 1,920 generated
float functions to 0, under all four write orders
residual sites / gotos 135,070 / 27,108 equal; generated 63,560 to 63,531, one function +1 goto
census.py orders (2,508) 0, 0, 0 differ under O1, O2, O3; 0pack 0x476982 9 sites in all four
release pdd, instructions 0pack 0x62ecf0 71.79G to 71.88G, pumasim 0x23fdf0 84.99G to 85.10G
(mean of two runs, +0.1%), renderings md5-identical, peak 251-261 MB
gates fmt, clippy (--workspace --all-features --tests -D warnings): exit 0;
tests 3,008 passed, 0 failed, 8 ignored (2,998 before); golden 442
and stable_temporaries 24 unchanged, nothing blessed; structure
report exit 0; Dylint 12 (baseline 12); comment runs and shards
clean; certification 50 rendered, 30 refused, 0 invented, dropped,
panicked or undefined; scripts/test_*.py ok
mutation 25 mutants, 22 killed, 3 alive with reasons
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
scripts/mutants_d68.py applies each mutant, runs the tests that should kill it, restores the file,
and exits 1 where a mutant lives that should die or dies that should live. 22 die: the lane pick
unfiltered (with the check of the facts, and with it skipped), the check unwired, the guard unwired,
never told its block, letting a name through or naming the wrong cause, each of the validator's
eight fact families dropped, defined_before off by one, with its phi case or its entry case wrong or
always true, and the production write order changed three ways. Three live, each with its reason:
the guard with r2ssa's pick and check both gone (by design, the guard holds alone), strictly_dominates
for dominates in defined_before (equivalent: the same block returns above), and the block-end read
placed at the block's start in the validator (no fact the fixtures hold reads a value its own block
defines). 25 edits apply once each (--check).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
spelled.rs and the ADR said each edge is spelled before the operand its block branches on "so a
copy is set before the test reads". It is not pinned and holds for no input: a block's test reads
no merge its own forward edges pay, since a merge the test reads dominates the block and so enters
it only by a back edge, which pays nothing (the skeptic's mutant that spells the test first moves
no function of bash, ls-toybox and pigz and fails no test). The order stays as the one the Writer
used; no verdict depends on it.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
fact_mutants (a cargo feature, off by default, enabled only by r2engine's dev-dependency) adds
with_facts(Facts, body), a thread-local: UnsoundLanes makes narrowed_argument take the first lane of
the class without asking whether its definition has run, as before D68, with validate_boundary_values
kept; UnsoundLanesUnchecked also skips it. Engine tests over lane_nondom9, lane_nondom7 and
lane_nondom8 under the four write orders:
- UnsoundLanes: the function is refused ("SSA integrity: a boundary fact names a value its
definition does not dominate") and no call is written;
- UnsoundLanesUnchecked: the call's argument is r2sleigh_residual_u32, never tmp_lane_..., and the
proof line names "assigned on only some paths to its read" where the lane's write is spelled first.
The second is the test that a violating input becomes a residual and not wrong C; without the knob
nothing violates. r2ssa has the matching unit test (sealing with an unsound pick is refused; the
same pick unchecked states the lane of the other arm).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
The order a build without placement_mutants writes in (exits inlined, no list permuted) was a
second implementation no test compiled, since the tests run with --all-features: the mutants
inline_exits false, exits reversed and merges reversed on it died only to 3, 9 and 20 goldens of the
release run. The module is now compiled under test beside the feature's, and one unit test pins
all three, so each mutant of it dies to production_writes_in_the_facts_own_order.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
fingerprint() returned None for a refused record, so a function refused the same way under two
orders was equal whatever its ledger or refusal reason did. It now carries the refusal (kind and
reason, which counts the obligations and names the first unaccounted one) and the ledger, and
verdict_moves compares them; a function refused on one side only is a move in either direction
(only "refused only under the mutant" counted before). Guards to tip moved 7 refused functions
toward residual (ls-toybox 0x5323c rendered 807 to 806, residual 214 to 216; libc-2.31 0xcd010,
0xcd190, 0xcd320; libc-2.32 0xcd540, 0xcd6c0, 0xcd850), which the gate could not see.
Tests: scripts/test_census.py (17 tests).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
D68. D58 reads a bound name as a variable when every write to it is spelled (`owed` is 0), and spells
blocks in reverse postorder, which is not dominance: a name defined on the other arm of a branch was
read as assigned. read_name now also asks r2ssa (SsaArtifact::value_defined_before, the rule
validate_boundary_values checks facts by) whether the definition has run in the block being spelled
(Values::enter, called once per block by Spelling::block); if not it is a residual read with
refusal evidence (read-not-dominated) and a proof-line cause of its own (assigned on only some
paths to its read), never C that reads an unassigned variable.
The guard stays a hard rule and not a debug_assert: it is the one check on the text itself (the
validator checks facts at their reads, this checks every read the text makes, including the terms
the arena expands), it is O(1) per read, and a debug_assert would abort in the build whose test
shows a violating read becoming a residual. It decides nothing r2ssa owns: the rule is r2ssa's, the
policy (a residual, named in the proof line) is the renderer's.
Test: variable_or_residual's table (an unspelled write is Unassigned and asks no scope; a violating
read is NotDominated). Values cannot be built without a sealed artifact, so the wiring is covered by
the engine tests under the fact_mutants knob of the commit that adds it, and by the mutants table in
the ADR (guard-unwired and block-never-entered die).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
D68. narrowed_argument took ValueViews::low_lane_value (the first value of the lane's class in
definition order) with no dominance test, so a SUBPIECE read on the other arm of a branch became the
call's argument. pumasim 0x279d80: carrier XMM1_6 in 0x279e1c, lane in 0x279e4c, call in 0x279ec8,
and 0x279e3e branches to either; 0x27b040 the same (4 reads). The lane is now kept only where
integrity::defined_before holds at the call (an entry value, a phi or an earlier operation of the
block, or a strictly dominating block's; O(1) from the dominator tree's intervals), else the carrier
the walk reached is the argument, which renders as (uint32_t)xmm1_6.
validate_boundary_values, called in Sealed::into_artifact, checks every value a sealed fact reads
against the place it reads it: call arguments and their carriers, call targets, return values,
return address, exit stack pointer, branch conditions, switch selectors; O(facts); a violation
refuses the function (IntegrityRule::BoundaryValueNotDominated). It is beside validate_ssa_function
and not in it: that runs on the SSAFunction before the seal, and these facts exist only after the
seal has dropped the operations it reads. Call results are definitions the call makes, and a
comparison's operands are class_value names no renderer reads; checking them refused 44 of bash's
1,568 functions, so they are not checked.
Read by hand (r2s -q -c 'aa; s 0x279d80; pdd' pumasim, tip against now): the two atan2f arguments
(lines 301 and 323) read tmp_lane_279e4c_0_0_1 and now (uint32_t)xmm1_6, which is assigned at lines
261 and 266, both arms of an if, before them; the lane is assigned at 350, after. 0x27b040 the same
with xmm1_6 and tmp_lane_27b110_0_0_1. Ledger unchanged (rendered 352 and 327, residual 39 and 30).
Of 1,920 generated float functions 90 change, none is newly refused: 47 differ in one call argument
line (lane to carrier, e.g. s106_O1 0x8000690 hypotf's first argument to (uint32_t)xmm0_12); 8 also
lose the lane's now dead statement, sites equal (s109_O1 0x8000320); 35 change residual sites, 34 to
fewer (a residual argument becomes the carrier, s113_O1 0x8000670 fmodf and atan2f, 78 sites to 76)
and s106_O1 0x8000540 from 19 to 25 with one goto more, since the carrier's chain it now renders
reads a register held from entry.
Tests: function::tests::lanes (a lane on the other arm is not the argument, with the old pick it is;
a lane read above the branch still is; every fact family refuses a forged value; defined_before's
order within a block; an unsound pick is refused).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
pumasim 0x279d80 and 0x27b040 read tmp_lane_..., assigned on the arm that does not hold the
call, since D58 reads a bound name in reverse postorder. Three programs (the skeptic's
lane_nondom9, lane_nondom7 and lane_nondom8, bytes from literals, atan2f imported) under the four
write orders, checked by a definite-assignment pass over the rendered C: it fails at 15486ea7 on
lane_nondom9 and lane_nondom7 (tmp_lane_1023_0_0_1 unassigned on the path to the call).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
doc/adr-structure-dominator-tree.md gains "the guards and the spelling order, stacked": where D59 and D60
meet D58 (an edge's copy is spelled as EdgeText::Copies and marked as a statement of the block it leaves,
the latch hoist's reads are counted once and its copy test asks Placed::edge_copy, a chain member is a
test whose text is nothing else), what the effects add and the table of the mined set. Over 25,735
functions of bash, ls-toybox, pigz, 0pack and pumasim 17 change under the guards alone and 55 under the
spelling order alone, none under both, none newly refused. Residual sites: 0pack 47,850 to 47,898,
pumasim 67,628 to 67,644, the guards add none. Mined set: 206 perfect, 43.795 mean GED and 57,153 total
GED at the base, with the guards and with the tip (eight zlib `inflateCopy` renderings renumber a local,
no graph moves); held out gotos 2,100, 2,098, 2,098 with the same 338 refused. Write orders O1, O2, O3
differ 0, 0, 0 at the tip against 0, 120, 187 on the base with the knobs alone. Release pdd instructions
retired -0.02% to +0.10% on six large functions, renderings byte-identical. The equivalence gate holds
all 828 baseline records on x86-64 (744 equal) and AArch64 (750 equal), none differing.
ROADMAP: the SD row records the stack's numbers. D61 (3) gains the one function the stack makes gain a
goto: bash 0x48140, 1 to 2, because D58's rule reads its tail's r13_4 as a residual and a tail that holds
one is not copied.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
doc/adr-decompiler-rewrite.md gets "D2's spelling order" (one pass in reverse postorder, why a pass and
not a prediction, forward edges, the late edge promise, the gate and its measured table) and the
forward-edge rule in "Merges"; doc/adr-structure-dominator-tree.md no longer ledgers D58. ROADMAP D58
is done with the measured numbers (the order sweep 0, 0, 0 against 0, 120, 187 with the knobs alone;
13 of 2,508 functions move in the natural order, +9 sites; 0pack +48 and pumasim +16 residual sites
over 23,213 functions, none rendered to refused; instructions retired within -0.12% to +0.13%);
the old row moves verbatim to doc/roadmap-history.md. New rows, numbered after the guards' D61: D62
(a callee's result presence, r2ssa states, r2types joins, r2dec reads; the exact repro bash 0x61520 and
the negative test for pumasim png_free), D63 (any rendered forward copy, conditional on the certificate
agreeing a gap traps) and D64 (Values immutable once spelled).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
A forward edge can retreat in reverse postorder when the region is irreducible: its copy is spelled
after the first reads of the merge it enters. Owing that copy at those reads made them residual
whatever the copy would be. The merge now owes only the forward edges spelled before it, the late
edge is verified instead: the first attempt reads the merge as a variable, `Values::broken` names
each merge whose late copy gapped, and `render` spells the function again with those merges owing
one more than any edge pays (`spell_function`; each attempt adds a merge to `forced`, so there are
at most as many attempts as merges). The rule is still "every forward edge renders its copy",
checked by the attempt that stands.
Measured over bash, ls-toybox and pigz (2,508 functions), natural order against the base: the
conservative rule of the previous commits moved 51 functions (+437 residual sites), 36 of them
(+424 sites, 174 names) only because a late edge paid after the first reads (pigz `0x4118e0`
`rax_8`, bash `0x46500` 31 late edges, +34 sites); now 13 move (+9 sites). Of the 13, seven bash
functions only renumber the locals of their block-transfer loops (`reached_5`, `to_5`: lazily
declared names are numbered in reverse postorder instead of write order), bash `0x8ee40` lists its
`_next` temporaries in another order, and five hold a gapped forward copy: bash `0x2dd90` (`rbx_2`),
`0x48140` (`r13_4`, which also stops a return tail from being copied over a residual), `0x85d70`
(`rsp_8` read twice, the entry copy at `0x85de0` is a gap), ls-toybox `0x392dc` and `0x501c8` (a
256-bit merge, which has no residual, so its read becomes a gap). The order sweep still gives 0
differing under O1, O2 and O3.
Tests, from byte literals under the four write orders: an irreducible cycle whose closing edge
renders its copy reads without a residual (22 bytes; fails at the previous commit on the plain read
turned residual), and one whose closing edge carries a frame address reads the merge as a residual
after the second attempt (36 bytes; with the retry removed it fails).
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`census.py orders` runs `pddj` over every function of the given binaries with the natural order and
the three `placement_mutants` orders (`R2SLEIGH_WRITE_ORDER` = o1, o2, o3) and compares per
function: the ledger's columns, the names read as never assigned (from the proof line), the residual
sites by instruction address, cause, gap kind, callee and reason, the declared variables and links,
and the set of statement lines apart from control (labels, jumps, braces) and site numbers. It
fails when a verdict differs from natural's, or when an order changes the text of fewer functions
than `--min-live` (a knob that moves nothing proves nothing), and reports a function refused on one
side only. A difference that only the selection pass explains (`if (c) x = a; else x = b;` against
`x = c ? a : b;`, a structure stage that reads the layout) is counted apart, not as a move.
Measured over bash, ls-toybox and pigz (2,508 functions) with the mutant build of each commit of the
branch: the mutants alone (base behaviour) 0 differ under O1, 120 under O2 and 187 under O3 (the
skeptic's 119 and 183 by ledger alone); the spelling pass 0, 0, 0; the forward-edge rule 0, 0, 0. Text
changes in 64 functions under O1 (an exit is inlined only in a loop that has one), 338 under O2 and
722 under O3. Python tests for the fingerprint, the selection rule and the refusal parity.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
A merge stays owed when a forward edge into it renders no copy (`gapped-forward-copy`), and an edge
that is forward by dominance can still retreat in reverse postorder, which only an irreducible region
does (`late-forward-edge`: its copy is spelled after the first reads of the merge it enters). Both
print under `R2DEC_TRACE_REFUSAL` with the edge, so a residual read of a merge can be traced to the
edge that keeps it owed and the corpus counted by edge. At this commit a late edge's copy is owed at
those reads: 36 of 2,508 functions (bash, ls-toybox, pigz) read 424 more sites as residuals only for
that (pigz 0x4118e0: 1 late edge; bash 0x46500: 31), which the commit after the census command
removes.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`Values::assigned` (a bool set by any copy or write spelled so far) is `owed`, a count by value
index. A parameter owes 0, an operation's output 1, and a merge one per distinct placed forward
edge in (`forward_in`, from the CFG's predecessors and `DomTree::is_back_edge`, O(preds) once per
block that holds a named merge). A write sets it to 0 (`defines`); a copy on a forward edge pays
one (`account_copy`); a copy on a back edge, a self copy and a gap (`unrendered_copy`) pay none. A
read of a name still owed is the NeverAssigned residual, as before. So a latch copy, which is
spelled after every header-side read in the same order the facts give, can never justify one, and
one gapped forward copy keeps the merge residual: a gap traps where it stands, but the certificate
(`GapKind::ValuesNotRendered.ends_control()` is false) lets control go on past it, and a verdict
must not lean on what the certificate denies (`a_gap_is_written_as_the_residual_call_whose_helper_traps`
pins the premise). A read turns to a residual where only a back edge or a gapped copy justified it, and to a
variable where the old write order read a name before its forward copy was spelled.
Tests, through the real pipeline from byte literals, each under the four write orders with a fresh
program per order (`crates/r2engine/tests/engine/structure.rs`): a loop-carried merge whose entry
copy is a frame-address gap (43 and 48 bytes) has the same verdicts under every order and every read
of it is `r2sleigh_residual_u64(`; a merge with one gapped and one rendered forward copy reads
residual (24 bytes, which pins ALL against ANY); a merge whose copies all render reads as a variable
in every order (16 bytes). Fail first: at the mutants-only head the first fails on O1 against
natural (`return rax_2;` after the loop against `return r2sleigh_residual_u64(2);`, ledger 22
rendered and 6 residual against 20 and 8); at the spelling-seam head the verdicts agree under every
order and both residual tests still fail on the plain read the latch copy justified; all three pass
here.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
`render::spelled::spell` walks the placed blocks in the CFG's reverse postorder (`function.block_addrs()`,
r2ssa's block order, asserted equal to `cfg.reverse_postorder()`) and fills a typed table: each
block's statements, the copies or tail text on every edge it leaves by, and how it ends (a test, a
selector, a return, a never-returning call, or a trap). `control::Writer` composes that table and
loses `&Values` and every `values::` call: it decides layout (regions, loops, labels, switch case
grouping) and nothing about a value. Within a block the order is the one `arms` always used (each
edge, so a copy is set before the test reads it, then the operand); a switch spells its selector, its
default edge, then the other targets in reverse postorder.
Why: whether a statement renders, a name is a variable or a residual, an extern is declared and a local
is numbered used to depend on which block `Writer` happened to reach first, so a verdict could
change with the write order. After this commit every `Values` entry point is called from one loop
over a fixed order, and `crates/r2dec/tests/architecture.rs` keeps it so (control.rs names no
`Values`; spelled.rs reads no placement). Gap `origin` strings stay `render::control`, which names the
D1 stage rather than a file, so no golden moves for that.
This commit moves the order only; the rule that decides whether a merge reads as a variable is the
next commit's.
Co-Authored-By: Claude Sonnet 5.5 <[email protected]>
Claude-Session: https://claude.ai/code/session_01456qmqCGpCWJkrg6JUZNNM
