Drives the dual-stream router over a real binary end-to-end.
- r2_backend: detectBinaryArch() (iIj) + extractFunctionBytes() (aflj + p8,
skipping import thunks) — r2 supplies arch + per-function bytes; the Ghidra
lifter consumes them.
- binary_pcode_scan.cpp (fold-ghidra lib): scanBinaryWithPcode() maps the
r2 arch to a vendored SLEIGH spec (arm64-LE -> AARCH64:LE:64:v8A today;
unknown arch -> {} so the caller falls back to the r2-disasm passes),
enumerates functions, routes each through both lift streams, and merges +
dedups across functions. max_functions caps the sweep (robustness).
- meson: -DFOLD_GHIDRA_SPECS_DIR baked to the vendored specs path so the lifter
locates .ldefs/.sla at runtime; binary_pcode_scan added to fold-ghidra; the
pcode_scan driver gains a whole-binary `pcode_scan <binary>` mode.
Validated on the CTF corpus: libdiv_by_zero.dylib -> exactly 2 div-by-zero
(div_by_zero_direct + mod_by_zero, correctly attributed; div_by_zero_variable
abstains pending path-forking), and 0 on the other 9 dylibs. This reaches
parity with the shipped slice-4 div-by-zero TPs through the proper Z3/P-Code
pipeline. Next (Phase 4 part 2): wire into scan_runner additively (dedup the
div-by-zero overlap with the structural passes), then the encoder increments
(path-forking, null-deref, overflow) for the remaining corpus gains.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Wires the whole pipeline together: binary bytes -> raw+SSA lift -> P-Code
encoder -> Z3 -> BinaryBBObserver -> merged finding.
- include/fold/binary/pcode_router.{hpp} + src/binary/pcode_router.cpp:
routeFunctionToFindings() lifts a function both ways (liftRaw + liftSSA),
encodes each into a fresh Z3 context/observer, tags findings with the lift
level (evidence.backend = binary-pcode-raw|ssa), and merges + dedups by
(kind, line, detector) — raw wins on collision (more direct hazard evidence).
- meson: gated `fold-ghidra` static lib (ghidra_lifter + pcode_router) linking
fold_core_dep + ghidra_decompiler_dep (first fold_core <-> Ghidra link), and
the `pcode_scan` smoke driver. Defined after fold_core so both deps are in
scope; built only when -Dghidra=enabled.
- pcode_encoder fix: value map now keys on (space, offset) without size and
coerces on read, so a sub-register divisor read (w9, size 4) sees the
full-register zero write (x9, size 8) the lifter emits for `mov w9,#0`
(ARM64 zero-extend). New unit test locks this aliasing.
Validated end-to-end: pcode_scan on arm64 sym._div_by_zero_direct emits exactly
one finding — `[binary-pcode-raw] division by zero proven by Z3` — with the SSA
stream correctly contributing nothing (it folds x/0 -> 0) and the router
merging. Full suite 71 Ok / 0 Fail / 1 pre-existing binary_backend timeout.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
