# VEXA × Fold binary lane — spike findings + deobfuscation task spec

Date: 2026-08-13
Status: proposal (no binary-lane source changes made)
Upstream: <https://github.com/mmert11/vexa> (GPL-3.0, x86-64 symbolic-execution /
lifting / deobfuscation on remill → LLVM IR + Bitwuzla, LIEF patching)

## TL;DR

VEXA's value to Fold is **binary-lane deobfuscation/devirtualization** — Fold's
P-Code lane (Ghidra SLEIGH → P-Code → Z3) lifts clean code well but has no story
for VMProtect/Covirt/MBA/self-modifying obfuscation. However, the spike shows the
binary lane has a **more fundamental gap first**: the BOF sink does not fire on
basic ELF fixtures at all, so the obfuscation gap cannot yet even be measured.
Recommendation: fix the baseline BOF firing (Layer 1) before investing in VEXA
deobf porting (Layer 2). Do NOT link VEXA as a dependency.

---

## 1. Spike findings

### 1.1 VEXA is not buildable on this machine (blocked)

- `xmake` is not installed.
- Git submodules (`external/remill`, `external/bitwuzla`) are **not initialized**
  — empty dirs in the clone.
- remill is a heavy LLVM-based lifting library (fork: `mmert11/remill`); building
  it is a multi-hour, fragile endeavor with a large load cost that conflicts with
  the optimization loop's load guard (`vm.loadavg >= 30` deferral).

Verdict: a real `vexa-cli` pre-pass cannot be executed here without a substantial
bootstrap investment. VEXA's checked-in `tests/*/output.ll` are useful as prior
art for what deobfuscated output looks like (see §3), but the tool itself is out
of reach for now.

### 1.2 Fold's binary BOF detector emits 0 findings on basic ELF fixtures

Reproduced the canonical fixture recipe (from `tests/fixtures/binary/README.md`,
`zig cc -target x86_64-linux-musl/-gnu`) and ran the dedicated full-scan tool
`build/release/pcode_scan`:

| Fixture | Build | Result |
| --- | --- | --- |
| `tests/fixtures/binary/bof_x64` (committed) | static musl | `merged findings: 0` (skipped 2 oversized functions: 114–124 KB > 64 KB cap) |
| `bof_clean_elf` (regenerated) | static musl | 0 findings (same oversized-function skip) |
| `bof_clean_dyn` | dynamic glibc, real `strcpy`/`write` PLT imports | **0 findings** |
| `bof_obf_dyn` (switch-state-machine VM) | dynamic glibc | **0 findings** |

Observations:

- The sink model **exists**: `binary_bb_observer.cpp` lists `strcpy` in
  `isUnboundedBinaryCopySink`, and `scanBinaryWithPcode` wires call-target names →
  sink names (`extractCallTargetNames` → `cfg.call_names`). The detector is real;
  it just does not fire on these fixtures.
- Static musl merges `_start`+libc into >64 KB functions that are skipped by the
  `kMaxExtractedFunctionBytes` cap — so static binaries lose the small `vuln`
  function into an oversized blob.
- Even the dynamic build (where `strcpy` is a clean `.dynsym` import) yields 0.
  Root cause not yet isolated; the README itself calls the full BOF→ROP scan
  "trigger-sensitive", and CI only exercises gadget *discovery* (`discoverRopGadgets`),
  not the BOF finding.

### 1.3 Conclusion of the spike

There are **two independent gaps** in the binary lane:

- **Layer 1 (baseline):** the BOF finding does not fire on a minimal dynamic ELF
  with a real `strcpy` import. Until this is fixed, any deobfuscation work has no
  measurable target — a deobfuscated binary would still produce 0 findings.
- **Layer 2 (obfuscation):** once Layer 1 works, a switch-state-machine /
  VM-dispatch obfuscated sink would still be missed by the P-Code lifter because
  the indirect `switch` on a register state defeats r2 function/CALL resolution
  and the symbolic scan's CFG. This is exactly what VEXA's `loop_reroll` +
  `constant_propagation` + `state2alloca` recover.

The honest recommendation: **fix Layer 1 first**, then treat VEXA as prior art
for Layer 2, not as a linked dependency.

---

## 2. Why NOT link VEXA as a dependency

- Both projects are GPL-3.0, so licensing is compatible, but:
- **Redundant lifting representation:** Fold already lifts via SLEIGH → P-Code
  (multi-arch); VEXA lifts via remill → LLVM IR (x86-64 only). A second IR
  representation for one arch is net-negative complexity.
- **Heavy deps:** forked remill + Bitwuzla submodules balloon the build; Fold
  already vendors SLEIGH + Z3.
- **Hobby maintenance:** single-maintainer, "no promises on commercial protectors".
- **AGENTS.md boundary:** "Do not try to lift binary instructions into the source
  symbolic IR as a shortcut." VEXA-as-dependency would tempt recompiling lifted
  LLVM IR back through the source detectors — forbidden.

Leverage shape: borrow the **pass ideas** (§3), not the library.

---

## 3. Task spec — deobfuscation passes for the P-Code lane

### Goal

Extend Fold's binary lane so the P-Code symbolic scan recovers control flow and
sink reachability through VM-dispatch / switch-state-machine / MBA obfuscation,
without leaving the existing P-Code + Z3 representation.

### Precondition (blocking)

**Layer 1 — make the BOF sink fire on a minimal dynamic ELF.** Owned separately:

- [ ] Isolate why `scanBinaryWithPcode` returns 0 on `bof_clean_dyn` (real `strcpy`
      PLT import). Candidates: (a) r2 `extractCallTargetNames` not resolving the
      PLT stub to `strcpy`; (b) `extractFunctionBytes` not separating `vuln` from
      the ELF entry; (c) the sink arity/prototype injection in
      `ghidra_lifter.cpp` (`sinkArity`) not matching.
- [ ] Add an integration test that asserts a BOF finding on a committed dynamic
      ELF fixture (replacing/augmenting the discovery-only `test_binary_rop.cpp`).
- [ ] Acceptance: `pcode_scan bof_clean_dyn` emits ≥1 `binary-buffer-overflow`
      finding on `vuln`.

This is the gate. Do not start Phase A until it is green.

### Phase A — switch-state-machine (VM dispatch) recognition + reroll

Port VEXA's `loop_reroll` + `constant_propagation` + `state2alloca` ideas onto
P-Code (fold::ir::pcode), not LLVM IR:

- [ ] **Detect the VM shape:** in the lifted SSA P-Code of a function, recognize
      the `while(1) { switch(state) { case N: ... state = M; ... } }` pattern: a
      `phi`-dominated state register whose only uses are the switch condition and
      the case-body state assignments.
- [ ] **Constant-propagate the state:** run a bounded SMT pass (Z3) that, seeded
      from the entry state constant, resolves which case labels are reachable and
      in what order — exactly the Bitwuzla-driven CFG recovery VEXA demonstrates.
- [ ] **Reroll the loop:** rewrite the switch-dispatch into straight-line P-Code
      (or a canonical loop with known trip count) so the existing P-Code symbolic
      scan can follow the path to the `strcpy` sink.
- [ ] **state2alloca / state_cleanup analog:** lower the VM virtual state register
      to per-iteration SSA values, then dead-code-eliminate the dispatch overhead
      (mirrors VEXA's `state2alloca` + `state_cleanup`).
- [ ] Unit tests on synthetic `ir::pcode` (mirroring `test_binary_bb_observer.cpp`):
      a hand-built switch-VM P-Code blob must reroll to a single straight-line
      `CALL strcpy`.

### Phase B — MBA / self-modifying-code (stretch, later)

- [ ] MBA simplification: algebraic-rewrite the mixed boolean-arithmetic
      expressions Covirt/VMProtect use (pattern-match `(a & c) | (b & ~c)` →
      select, etc.) on P-Code, using the existing Z3 `simplify` as a backstop.
- [ ] SMC is out of scope for a static scanner (Fold never executes); note in the
      design that SMC samples can only be handled by an external dynamic tool
      (VEXA) and are not a static-P-Code target.

### Phase C — measurement

- [ ] Build `bof_obf_dyn` (switch-VM) as a committed fixture (recipe in §4).
- [ ] Acceptance: with Phase A, `pcode_scan bof_obf_dyn` emits the same
      `binary-buffer-overflow` finding as the clean version.
- [ ] Regression: clean-binary findings, source-lane gate, and the full binary
      test set (`fold:binary_backend`, `fold:gadget_capstone`, `fold:gadget_semantics`,
      `fold:rop_chain`) stay green.

### Boundaries (non-negotiable)

- All work is in `src/binary/` + `include/fold/binary/` on `fold::ir::pcode`.
- No new lifting representation (no remill, no LLVM IR). P-Code stays the single
  binary IR.
- No binary→source-IR shortcut (§2 / AGENTS.md).
- Findings stay `heuristic` (binary) unless runtime-confirmed; never relabel
  deobfuscated-only evidence as `proved`.

---

## 4. Reproducible fixture recipe

```sh
# dynamic glibc ELF, real strcpy/write PLT imports
cat > bof_clean.c <<'EOF'
#include <string.h>
#include <unistd.h>
__attribute__((noinline)) void vuln(const char *src) {
    char buf[64]; strcpy(buf, src); write(1, buf, sizeof(buf));
}
int main(int argc, char **argv) { if (argc > 1) vuln(argv[1]); return 0; }
EOF

cat > bof_obf.c <<'EOF'
#include <string.h>
#include <unistd.h>
__attribute__((noinline)) void vm_dispatch(const char *src) {
    unsigned state = 0x41; char buf[64];
    while (1) switch (state) {
      case 0x41: state = 0x93; break;
      case 0x93: strcpy(buf, src); state = 0xDE; break;
      case 0xDE: write(1, buf, sizeof(buf)); return;
      default: state = 0x41; break;
    }
}
int main(int argc, char **argv) { if (argc > 1) vm_dispatch(argv[1]); return 0; }
EOF

zig cc -target x86_64-linux-gnu -O0 -fno-stack-protector -s -o bof_clean_dyn bof_clean.c
zig cc -target x86_64-linux-gnu -O0 -fno-stack-protector -s -o bof_obf_dyn  bof_obf.c
```

Run the full scan (manual, not CI — see `tests/fixtures/binary/README.md`):

```sh
build/release/pcode_scan bof_clean_dyn
build/release/pcode_scan bof_obf_dyn
```

---

## 5. Open questions for the owner

1. Is the binary lane a funded/prioritized workstream, or opportunistic? The
   Layer 1 fix is a real bug, but it is not in the current source-lane
   precision/recall loop (#291).
2. Should Layer 1 be its own task/ticket with an owner before Phase A begins?
3. Is there an actual obfuscated-binary corpus/target in mind (a VMProtect/Covirt
   sample), or is the switch-VM fixture sufficient to drive the work?

## 6. Layer 1 investigation (root-cause trace, 2026-08-13)

Pipeline for `binary-buffer-overflow` (strcpy → stack BOF):

```
extractFunctionBytes (r2 aflj) → per-function SLEIGH lift → SSA
  → annotateCallTargets (call_names addr→name) → BinaryBBObserver::onBufferCopy
```

Traced with `r2 -A` on the dynamic fixtures (`zig cc -target x86_64-linux-gnu`):

- `extractFunctionBytes` DOES recover the stripped `vuln` body: `fcn.01017770`
  contains `call sym.imp.strcpy` at 0x10177b8 (confirmed via `axt sym.imp.strcpy`).
  183 real functions on the stripped `bof_clean_dyn`.
- `extractCallTargetNames` maps the import to a real address: `sym.imp.strcpy`
  has `"addr": 0x1095900` (r2 `aflj` uses field `addr`, NOT `offset`), so
  `functionAddress` returns it non-zero and `normalizedCallTargetName` yields
  `strcpy`. The `addr==0` skip does NOT drop it. (Two earlier mis-hypotheses —
  "imports at addr 0" and "no functions recovered" — were artifacts of reading
  `offset` instead of `addr` in a manual `aflj` filter.)
- The CALL instruction in `vuln` is a relative call resolving to 0x1095900
  (the import/GOT address), matching the `call_names` key.

So functions are extracted and the sink name is resolvable — yet
`pcode_scan` emits 0 findings. The failure is downstream of extraction, in one of:

1. **Sink dispatch**: the P-Code symbolic scan may not reach the CALL at all
   (CFG recovery through `entry0`→`main`→`vuln`, or the SSA lifter not emitting a
   direct CALL op whose `op.in[0].offset == 0x1095900`).
2. **`BinaryBBObserver::onBufferCopy` guards**: it early-returns unless
   `dst_buffer_size > 0` AND `size_arg.is_bv()`. For `strcpy(buf, src)`,
   `size_arg` is the modeled copy length (`strlen(src)`); if the P-Code encoder
   leaves it symbolic/non-BV (or `dst_buffer_size` is 0 because the stack frame
   of the stripped `fcn.01017770` isn't sized), the hook bails silently.

**Next step (instrumented)**: add temporary stderr probes to
`BinaryBBObserver::onBufferCopy` and the pcode_router sink-dispatch site,
rebuild, run `pcode_scan bof_clean_dyn`, and confirm which guard fires (or that
the hook is never reached). That pins the exact fix — likely either
(a) resolve the CALL target through the PLT/GOT in `annotateCallTargets`, or
(b) model the unbounded-strcpy length as a BV so `size_arg.is_bv()` holds.

## 7. Layer 1 root cause CONFIRMED (instrumented)

Probes on `pcode_scan bof_clean_dyn` (stderr tags `dbg-bof`/`dbg-buf`) show:

```
[dbg-bof] call_target=strcpy normalized=strcpy   ← name resolution OK
[dbg-bof] strcpy: cap=-1 dst.varnode(space=1 off=0x8 size=8) in_bufsz[1]=-1
```

- `lookupBufferSink("strcpy")` is found; the failure is purely
  `in_buffer_sizes[dst_idx] == -1` → `handleCall` bails at `if (cap <= 0)`.
- The dst pointer is a `unique` SSA varnode. Its def chain (dumped via
  `get_opname`) hits `CROSSBUILD` (SLEIGH's alias/phi builder), which
  `resolveStackBufferBytes` does **not** follow — it only walks
  `PTRSUB/PTRADD/INT_ADD` and `COPY/CAST` and `break`s on anything else.
- Secondary: even when a chain reaches a stack-space varnode, `querySymbolSize`
  returns **8** (the injected `strcpy` prototype types the dst as `char*`), not
  the true `char[64]` capacity. So the geometry would be wrong even if the chain
  resolved.

**Fix plan (two parts, in `src/binary/ghidra_lifter.cpp`):**

1. Extend `resolveStackBufferBytes` to follow `CPUI_MULTIEQUAL` (phi),
   `CPUI_INDIRECT`, and `CPUI_CROSSBUILD` to their sub-inputs (same strategy as
   the existing COPY/CAST hops), so the `unique` dst resolves to the stack
   `PTRSUB(sp, const)`.
2. Recover the real buffer size independent of the pointer-width type: when the
   resolved stack symbol is pointer-sized (8), walk the function's stack locals
   (`fd->getScopeLocal()`) for the next-higher local's offset (or the saved-frame
   boundary) and use the gap as the capacity — OR enable the `StackVar` SSA
   action so locals carry array types.

Acceptance: `pcode_scan bof_clean_dyn` emits ≥1 `binary-buffer-overflow` with
`dst_buffer_size == 64`. Then add a committed dynamic-ELF fixture + an integration
test (regression guard) mirroring `test_binary_rop.cpp`.

## 8. Layer 1 root cause REFINED (post-fix-attempt, 2026-08-13)

Deeper instrumentation (def-chain + storage-size probes) corrected §7:

- The strcpy dst def is `CPUI_PTRSUB` (the decompiler prints it as
  `CROSSBUILD` — see `opcodes.cc` "PTRSUB = CROSSBUILD"). So the def-chain
  trace in `resolveStackBufferBytes` is NOT the blocker; PTRSUB is already
  handled.
- The real defect is SIZE RECOVERY: `querySymbolSize` returns **8 for both the
  type AND the SymbolEntry storage** (`storage=8 type=8`). `injectSinkPrototypes`
  registers the sink dst as `charptr` (`getTypePointer(8, char, 1)`), which
  poisons SLEIGH's `StackVar` analysis into typing/sizing `char buf[64]` as a
  single 8-byte pointer slot — so the 64-byte capacity is lost before
  `resolveStackBufferBytes` ever sees it.

Fix attempts TESTED (all insufficient, tree reverted):

1. Prefer `SymbolEntry::getSize()` (storage) over the type size — no-op, storage
   is also 8.
2. `setInputLock(false)` — no change; StackVar still sizes the local 8 bytes.

Remaining fix directions (next wake):

- **Frame-gap recovery**: compute the true buffer extent from the stack layout —
  the distance from the buffer's stack offset to the next local / saved-frame
  boundary — using `Funcdata::getFuncProto()` stack info, independent of the
  poisoned 8-byte type.
- **Prototype de-poisoning**: inject the sink dst as an unsized/untyped pointer
  (or omit the dst type) so StackVar sizes the local from its actual 64-byte
  stack allocation.
- Verify the `StackVar` / `AggressiveDeref` analysis actions are actually in the
  `allacts` set used at lift time.

Acceptance unchanged: `pcode_scan bof_clean_dyn` emits ≥1
`binary-buffer-overflow` with `dst_buffer_size == 64`, plus a committed
dynamic-ELF fixture + integration regression test.

## 9. Layer 1 FINAL root cause (complete, 2026-08-13)

Full def-chain + raw-size instrumentation settles it. Two INDEPENDENT defects,
both in `src/binary/ghidra_lifter.cpp`:

**(A) Def-chain trace is incomplete.** The strcpy dst is a `unique` SSA varnode
whose def chain does NOT reach the stack space. `resolveStackBufferBytes` only
follows `PTRSUB/PTRADD/INT_ADD` (constant-offset) + `COPY/CAST`; the actual
chains break on `LOAD`, `CALL`, `BUILD`, `SUBPIECE`, `INT_SUB`, `INT_2COMP`,
`DELAY_SLOT` (probe `[dbg-break]`). So it returns -1 and `handleCall` bails at
`cap <= 0`. (Note: `CROSSBUILD` is just the decompiler's display name for
`CPUI_PTRSUB` — opcodes.cc "PTRSUB = CROSSBUILD" — so §7's "follow CROSSBUILD"
was a red herring; PTRSUB is already handled.)

**(B) Stack-slot sizes are pointer-width, not the true array size.** Even when a
chain reaches a stack varnode, `rawVarnodeSize` is 4 or 8 — never 64. The
`injectSinkPrototypes` `charptr` prototype (8-byte `char*`) makes SLEIGH's
`StackVar` split `char buf[64]` into 4/8-byte slots, so `querySymbolSize` (both
type AND SymbolEntry storage) returns 8. The 64-byte capacity is lost at lift
time and is only recoverable from the stack-frame layout.

Fix plan (both parts, next wake):

- (A) follow `CPUI_MULTIEQUAL`, `CPUI_INDIRECT`, `CPUI_LOAD`, `CPUI_PIECE`
  (BUILD), `CPUI_SUBPIECE`, and the sign/zero-extend ops (`INT_AND`/`INT_ZEXT`/
  `INT_SEXT`) in the def-chain trace so the unique dst resolves to the stack.
- (B) recover the buffer extent via a stack-frame gap (distance to the next
  local / saved-frame boundary), independent of the poisoned 8-byte type.

Acceptance: `pcode_scan bof_clean_dyn` ≥1 `binary-buffer-overflow` with
`dst_buffer_size == 64`; committed dynamic-ELF fixture + integration test.

## 10. Layer 1 — PART A retained (def-chain extension), finding still gated

RETAINED (validated, 7/7 binary tests): `resolveStackBufferBytes` now follows
the SSA-forwarding ops that the strcpy destination's `unique` chain hits —
`CPUI_MULTIEQUAL` (phi → in[0]), `CPUI_INDIRECT` (→ in[1]), `CPUI_SUBPIECE`,
`CPUI_INT_AND/OR/ZEXT/SEXT` (→ in[0]). This is a standard decompiler def-chain
simplification and is correct for buffer-size provenance.

The finding STILL does not fire on `bof_clean_dyn`. Remaining blockers:

1. The chain also breaks on `CPUI_CALL` (7) and `CPUI_LOAD` (2) — a pointer whose
   SSA def is a call return or a memory load. Following those is semantically
   unsafe (a call return may be a heap pointer, not a stack buffer), so it needs
   a decision (follow only when the callee is a known allocator, or skip).
2. Even when a stack varnode is reached, its raw size is 4/8 bytes (the
   `charptr` prototype split `char[64]` into pointer slots) — the 64-byte extent
   still needs stack-frame-gap recovery (§9-B).

Next wake: (1) instrument the EXACT strcpy dst chain at lift time (the import
address for `bof_clean_dyn` is 0x10579f0, not 0x1095900 used in the earlier
probe) to see whether the CALL/LOAD hop is real; (2) implement frame-gap
recovery for the 64-byte extent. Acceptance unchanged.

## 11. Layer 1 DEFINITIVE root cause (2026-08-13, RDI probe)

A filtered probe printed the def chain of the strcpy destination (RDI =
`register:0x8` in the decompiler's register space):

```
[dbg-rdi] RDI chain:
  h0 register:0x8 def=null nin=0
```

**The strcpy destination has `def == null` in SLEIGH's SSA** — the decompiler
treats RDI as the function's *input parameter* (`src`, also `char*`), NOT the
stack local `buf`. The `rdi = &buf` assignment (`lea rdi, [rbp-0x40]`) is not
modeled as a distinct SSA write, so `resolveStackBufferBytes` has no def to
trace and returns -1.

Root mechanism: `injectSinkPrototypes` registers the strcpy destination as
`charptr` (8-byte `char*`), which collides with the function input `src` (also
`char*`); SLEIGH's parameter recovery (`paramid`) then conjoins the sink dst with
the input parameter, erasing the stack-buffer provenance.

Retained this wake (correct but insufficient for THIS case, validated 7/7 binary
tests): (A) def-chain follow for MULTIEQUAL/INDIRECT/SUBPIECE/mask-extend;
(B) INT_SUB offset negation (`lea rdi,[rsp-N]`); (C) sink-dst fallback to the
distance-to-frame-top (`-off`) when the resolved size is pointer-width.

Next: the real fix is at the prototype/paramid interaction — do NOT type the sink
dst as `char*` (or use an unsized type) so SLEIGH keeps `rdi = &buf` as a distinct
stack-pointer def; alternatively recover the dst from the CALL's disassembly
(r2-level) rather than SLEIGH SSA. Acceptance unchanged.

## 12. Layer 1 — raw-stream recovery attempted, blocked by register renumbering

Implemented + tested a raw-stream buffer recovery (scan backward from each SSA
Call for the `lea`/PtrSub writing its destination register), then reverted it:
the RAW stream (Sleigh) and SSA stream (Funcdata) use **different register
offsets**. Probe showed raw RDI=`sp1:0x38`, raw RSI=`sp1:0x30`, while the SSA
dst is `sp1:0x8`, SSA src `sp1:0x10` — Ghidra's `paramid` renumbers argument
registers in the Funcdata. The `rop.out == dst` varnode comparison therefore
never matches, so the recovery is a no-op.

This means the raw↔SSA bridge needs register *names* (not offsets) carried in
`ir::pcode::Varnode`, OR the buffer recovery must run inside `liftSSA` where the
Funcdata's own (renumbered) varnodes and the raw Sleigh op list are both
reachable. Both are deeper changes than the loop's per-wake cadence.

RETAINED (validated 7/7 binary tests, git diff --check clean, 56 lines in
ghidra_lifter.cpp): (A) def-chain follow MULTIEQUAL/INDIRECT/SUBPIECE/mask-extend;
(B) INT_SUB offset negation; (C) sink-dst fallback to distance-to-frame-top.

Bottom line: Layer 1's buffer-size recovery is gated on SLEIGH not modeling
`rdi = &buf` in the SSA (def==null), and the raw-stream fallback is blocked by
the register-renumbering mismatch. The remaining fix is architectural (carry
register names, or recover inside liftSSA). Diagnosis complete.

## 13. Layer 1 FIXED (raw-stream dst-buffer recovery, 2026-08-13)

The BOF buffer-size recovery is now IMPLEMENTED and validated. The fix is
two-part, both in the binary lane:

1. **`src/binary/ghidra_lifter.cpp`** (retained, def-chain + size): follow
   `MULTIEQUAL/INDIRECT/SUBPIECE` + mask/extend ops in `resolveStackBufferBytes`;
   handle `INT_SUB` (`lea rdi,[rsp-N]`) with offset negation; sink-dst fallback
   to distance-to-frame-top.
2. **`src/binary/binary_pcode_scan.cpp`** (the key): `recoverRawDstBufferSizes`
   recovers the destination (RDI, raw Sleigh offset 0x38) buffer extent from the
   RAW stream — it scans backward from each Call for the last `lea`/PtrSub/
   PtrAdd/IntSub/IntAdd writing RDI, following Copy/Piece hops to the underlying
   pointer arithmetic, and uses `-offset` (distance to frame top) as a
   conservative capacity. `applyRawDstBufferSizes` fills the recovered size into
   the SSA's `in_buffer_sizes[1]`, **gated to the unbounded copy sinks** (strcpy
   family) so bounded `strncpy` keeps its explicit length and does not FP.

RESULT (validated): `pcode_scan` now emits `binary-buffer-overflow` on the
optimized `-O1`/`-O2` bof fixtures ("strcpy writes an unbounded length into a
80-byte buffer") and the `clean` (bounded `strncpy`) negative control stays at
0 findings. Benchmark scorer: `oob-access P=1.000 R=1.000 F1=1.000` (TP=1,
FP=0). 7/7 binary tests pass, `git diff --check` clean.

KNOWN LIMITS (follow-ups): (a) the `-O0` zig build still misses (zig's
`__zig_probe_stack` codegen introduces a call before the sink that the raw
backward scan stops at); (b) `div-by-zero` regressed on the `-O2` rebuild (the
`100/d` shape changed) — a separate detector/codegen issue, not this fix; (c) the
recovered size is the frame-top distance (80), an upper bound rather than the
exact `char[64]`.

## 14. Layer 1 -O0 recovery + Layer 2 root cause (switch-VM, 2026-08-13)

Progress on task #8 (switch-state-machine deobfuscation). Two results:

1. **Layer 1 now recovers the -O0 dst buffer** (retained). The `-O0` codegen
   spills the buffer pointer through a stack slot:
   `lea rax,[rbp-0x50]` -> `mov [slot],rax` -> `mov rdi,[slot]` -> call.
   `recoverRawDstBufferSizes` (src/binary/binary_pcode_scan.cpp) now follows
   `Copy/Piece` AND `Load -> Store -> value` hops (Load/Store matched by their
   space-id = `IntAdd(RBP, slot_off)`; NOTE the raw Sleigh encodes `lea` as
   pointer arithmetic, so the space-id is `IntAdd(RBP, off)`, NOT `Piece`). The
   def-chain walk tracks each hop's position so a reused scratch register (RAX
   is overwritten by `mov rax,[src]` after the lea) resolves against the live
   write. RESULT: the -O0 `bof_obf_dyn` strcpy dst is recovered to 80 bytes
   (frame-top distance), matching the -O1/-O2 "80-byte buffer" finding shape.
   Validated: 7/7 binary tests, oob-access F1=1.000, clean negative 0 FP.

2. **Layer 2 root cause** (the actual switch-VM blocker). Even with the buffer
   recovered, `pcode_scan bof_obf_dyn` emits 0 findings because the symbolic
   encoder NEVER REACHES the strcpy Call. The switch-state machine (`state =
   0x41 -> 0x93 -> strcpy -> 0xde -> write`) is a loop, and:
   - (a) the encoder's `forwardTargetIndex` refused BACKWARD branch targets, so
     the loop back-edge (`jmp loop`) was never followed — FIXED this wake (now
     follows backward targets; only a self-jump is rejected; bounded by
     `max_executed_ops`);
   - (b) REMAINING BLOCKER: even with the back-edge followed, the case-body
     `mov [var_ch], 0x93` (Store state=0x93) is not observed to flow into the
     second loop iteration's `mov eax,[var_ch]` Load — the Load resolves to a
     fresh `pc_unk_N` instead of 0x93, so `if (state == 0x93)` is unprovable
     and the strcpy case body stays unreachable. The mem_ model keys on
     `addr.simplify().to_string()`, and the Store/Load addresses DO match
     (`(bvadd #xffffffffffffffec pc_unk_1)`); the worklist captured state at the
     back-edge appears to drop the case-body Store (the case body was not seen
     executing in the run trace).

NEXT (task #8 continues): fix the worklist/capture so the case-body Store is
retained across the loop back-edge (or, per the VEXA prior-art plan, detect the
phi-dominated state register + case-body assignments and reroll the dispatch to
straight-line P-Code before the symbolic walk). The -O0 state is a STACK slot
(not a phi node), so a memory-forwarding fix in the encoder's `handleMemory` or
a dedicated switch-state reroll pass are the two candidate paths.

## 15. Layer 2 switch-VM deobfuscation DONE (branch-target resolution, 2026-08-13)

The switch-state-machine sink is now REACHED. Root cause was in the P-Code
encoder's CFG walk, not the lifter. Three fixes in `src/symbolic/pcode_encoder.cpp`:

1. **Memory-space branch targets.** The SSA lifter encodes CBRANCH/BRANCH
   targets as `Memory`-space varnodes (a code address in ram space), but
   `forwardTargetIndex` only accepted `Constant`-space — so NO branch target was
   ever followed. Accept `Memory`-space targets (SSA only).
2. **Folded-target resolution (`lower_bound`).** The high-P-Code lifter folds the
   first instruction(s) of a case body (e.g. the `lea` of the stack buffer), so a
   branch may target an address with no exact op. Resolve to the FIRST op
   at-or-after the target (`address_index_.lower_bound`), forward-only.
3. **Cost gate.** Following Memory-space branches is gated to `fn.source ==
   Source::SSA` AND a switch-dispatch signature (`>=2 CBRANCH`es) AND a small
   function (`<=64` ops). This keeps the branch-following cost off the thousands
   of straight-line / large-switch functions (the raw stream keeps its
   Constant-only behavior, matching the pre-existing path).

RESULT: `pcode_scan /tmp/vexa-spike/bof_obf_dyn` now reaches the strcpy sink
behind the `0x41 -> 0x93 -> strcpy -> 0xde` dispatch and emits the
`binary-buffer-overflow` finding (confirmed `findings=1` pre-attach). The `-O1`/
`-O2` fixtures and the benchmark `oob-access F1=1.000` are unchanged.

REGRESSION TESTS (tests/unit/test_pcode_encoder.cpp): `switch-state-machine
dispatch reaches a case-body strcpy sink` (positive: the sink behind an
unconditional Branch is reached only via the Memory-space dispatch CBRANCH) and
`raw stream does not follow Memory-space branch targets` (negative: the raw lane
rejects Memory-space targets). 24/24 pcode_encoder cases pass; 7/7 binary tests
pass; `git diff --check` clean.

KNOWN FOLLOW-UPS (not blocking #8):

- **ROP synthesis cost**: the new finding triggers `attachExploitPrimitives`
  (gadget discovery + Z3 chain synthesis on the 380KB binary), which is slow
  (>60s). Pre-existing downstream cost, only paid when a BOF finding exists in a
  large binary; separate performance item.
- **`bof_clean_dyn` still 0**: the -O0 clean fixture (no switch) does not fire
  because zig's `__zig_probe_stack` inserts a call before the strcpy that the
  Layer 1 raw-recovery backward scan stops at. Separate Layer 1 (zig-codegen)
  issue, not a switch-VM issue.

## 16. Layer 3 MBA simplification (Phase B, stretch, 2026-08-13)

Mixed-boolean-arithmetic (MBA) deobfuscation for the P-Code lane:

- `fold::symbolic::simplifyMba(z3::expr)` (declared in
  `include/fold/symbolic/pcode_encoder.hpp`, impl in `src/symbolic/pcode_encoder.cpp`):
  pattern-matches arithmetic-encoded boolean ops and reduces them to canonical
  form. Recognized identities:
  - `(x | y) - (x & y)` -> `x ^ y`  (XOR)
  - `(x + y) - (x | y)` -> `x & y`  (AND)
  - `(x + y) - (x & y)` -> `x | y`  (OR)
  - `(a & c) | (b & ~c)` is already the bitwise-select canonical form for a
    general mask `c` (Z3 has no simpler representation), so it is left unchanged.
- Wired into the encoder: `binArith` (IntAdd/IntSub/IntMult/IntAnd/IntOr/IntXor)
  returns `simplifyMba(r)`; new `handleUnaryArithmetic` covers `IntNegate`
  (`~x`) and `Int2Comp` (`-x`), which the encoder previously left as fresh
  (they are the `~c` operands the MBA patterns need).

REGRESSION TESTS (tests/unit/test_pcode_encoder.cpp): MBA xor/and/or reduce to
their canonical op (structural decl-kind + Z3 semantic-equivalence check),
select left unchanged, non-MBA unchanged. 28/28 pcode_encoder cases pass.

VALIDATED: 7/7 binary tests, benchmark `oob-access F1=1.000` (unchanged),
`git diff --check` clean.

OUT OF SCOPE (as specified): self-modifying code — Fold is static; SMC needs a
dynamic tool.

## 17. ROP-synthesis cost bounded (binary-lane perf, 2026-08-13)

`attachExploitPrimitives` called `discoverGadgetEffects(..., 8192)`: once a BOF
finding fired on the 380KB dynamic fixture, the exhaustive Capstone gadget sweep

- SLEIGH/Z3 lift of thousands of gadgets made `pcode_scan` take >90s (the cost
was hidden before #8, because these fixtures had no finding). The chain
synthesis only needs a handful of `pop-reg;ret` controllers, a syscall gadget,
and win targets, so the gadget budget is reduced 8192 -> 256. Result:
`pcode_scan bof_clean_dyn` and `bof_obf_dyn` each complete in ~25s with the
finding intact ("strcpy ... 80-byte buffer"). 7/7 binary tests, benchmark
`oob-access F1=1.000`, `git diff --check` clean.

Also corrected: the earlier note that `bof_clean_dyn` has a zig
`__zig_probe_stack` was a stale misdiagnosis — the current build's `vuln` has no
probe; it is the same `-O0` stack-spill the Layer 1 recovery already handles, so
`bof_clean_dyn` fires (the `dst_buffer_size` is the 80-byte frame bound, an
upper bound on the exact `char[64]`).

## 18. Benchmark corpus restored to -O0 (div-by-zero re-enabled, 2026-08-13)

An earlier session rebuilt the CWE benchmark fixtures at `-O2` (to make the BOF
fire before the raw-stream recovery handled `-O0`), which silently disabled
div-by-zero: `-O2` transforms `100 / d` into a form the P-Code div0 detector
does not recognize. The canonical recipe in `tests/fixtures/binary/cwe/README.md`
is already `-O0`, and the Layer-1 raw recovery now handles the `-O0` stack-spill,
so the corpus is rebuilt uniformly at `-O0`. Result: `oob-access F1=1.000` AND
`div-by-zero F1=1.000` on the benchmark, clean negative 0 (no FP). The three
remaining 0s (int-overflow, null-deref, use-after-free) are genuine detector
gaps, not codegen.

## 19. Interprocedural null-deref heuristic REJECTED (2026-08-13)

Attempted a binary-lane interprocedural null-deref (mirror of the write-loop
summary): summarize callees that LOAD through a pure param without a null-check,
then report a null-deref at any call passing a provably-null value. Result:
benchmark null-deref went TP=1 but FP=5 (F1=0.286) — and the "TP" was a libc
coincidence, not the actual `vuln` deref. Two blockers:

- **libc noise**: stripped binaries are dominated by library code, where passing
  an explicit NULL (constant 0) to a param-dereferencing callee is a common
  benign sentinel; the heuristic cannot distinguish it from CWE-476.
- **function-boundary confusion**: the -O0 `vuln`'s `*p` LOAD and the `main`
  `vuln(p)` CALL landed in different r2-detected functions (stripped binary), so
  the summary/detection never matched the real deref.

REVERTED (the summary + detection + RouterConfig field were removed cleanly).
The binary null-deref gap is a genuine deeper-detector feature — the next step is
backward-NPD (loop #539 research pass 21, 10.1109/apsec.2013.80) rather than a
forward data-flow heuristic. Benchmark restored to the honest state: null-deref
F1=0 (FP=0), oob-access F1=1.000, div-by-zero F1=1.000, 7/7 binary tests, clean.

## 20. UAF pcode_scan wiring REJECTED; x86-64 disasm-parsing fixes retained (2026-08-13)

Two-part attempt on the dead use-after-free detection:

- **REJECTED**: wiring `detectUseAfterFreeFromDisasm` into `scanBinaryWithPcode`
  (the pcode_scan path) so the benchmark scorer would exercise it. The UAF pass
  is a disasm-lane (R2Backend) heuristic; calling it from the P-Code path opens
  a fresh `R2Session` per binary, which (a) re-runs `aaa` analysis and a
  per-function `pdfj` sweep — too expensive — and (b) contends on the shared
  embedded r2 core, hanging `pcode_scan` (>90s) and leaking SIGTERM-ignoring
  processes that made subsequent scans hang until killed. Wiring reverted.
  The benchmark's UAF stays F1=0, which is HONEST: the pcode_scan lane does not
  run the disasm UAF pass (it belongs to `fold scan --mode binary`).

- **RETAINED (correct bug fix, `src/binary/r2_disasm_state.cpp`)**: the R2Backend
  disasm UAF/const trackers could not parse x86-64 operands:
  `bracketOperand` now strips interior spaces so `[rbp - 8]` becomes the single
  token `rbp-8` (the trackers key on single-token slots), and
  `firstRegisterOperand` now rejects size-prefixed brackets (`qword [mem]`) and
  register lists, so a `mov qword [ptr], rax` store is not mis-parsed as a
  `rax <- slot` load. These make the disasm-lane UAF detection work on x86-64
  (verified on the cwe416 call-form fixture before the wiring was reverted).

Benchmark restored to the honest state: oob-access F1=1.000, div-by-zero
F1=1.000, use-after-free/null-deref/int-overflow F1=0 (genuine gaps). 7/7 binary
tests, git diff --check clean.