Add symbolic execution engine (Phases 0-14) with IR binding fixes#585
Merged
Add symbolic execution engine (Phases 0-14) with IR binding fixes#585
Conversation
…uite Implements PythonPolicy for symbolic execution via Python-subclassable policy objects, unified init_state/step API dispatching on argument type, PythonScheduler with fork/continuation support, and a 260-function test suite (177/230 passing). Includes generated IR instruction bindings, COW call stack, and concrete fallback for all value operations. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Factor mem_bulk_op (~480 lines) and memory helpers out of PythonPolicy into shared free functions in ConcreteOps, eliminating verbatim duplication between ConcretePolicy and SymbolicInterpreter. Both policies now delegate to concrete_mem_bulk_op. Add AtomicExpr handling in IRGen — Clang represents __atomic_fetch_* builtins as AtomicExpr AST nodes (not CallExpr), so they were falling through to UNKNOWN. Now emits proper READ_MODIFY_WRITE instructions for fetch-op, op-fetch, and exchange; MEMORY loads/stores for atomic load/store. Fixes 28 atomic test failures (205/230 passing). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
These 16-bit count-leading/trailing-zeros builtins were missing from the IRGen builtin table, causing them to fall through to UNKNOWN. 206/230 tests now pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
CALL instructions now print as `CALL @function_name [args...]` for direct calls and `CALL @<indirect> [args...]` for indirect calls. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add is_float flag to ScalarValue so float values are distinguishable from integers at the value level. This fixes three related issues: 1. value_to_python now returns Python floats (not raw bit integers) for float ScalarValues, so Python policies can operate on float values naturally in their own domain. 2. concrete_write_to_mem narrows f64→f32 when writing a double value to a 4-byte float slot (previously wrote low 4 bytes of the f64 bit pattern, producing 0.0 for any value). 3. init_state detects float parameters via BuiltinType::is_floating_point and passes is_float=true in the MemAccessHint. 223/230 tests passing (was 206). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Remove is_float parameter from concrete_write_to_mem — narrowing now uses the value's own is_float tag instead of an external hint. Simplify concrete_read_from_mem to return raw bits with float tag rather than interpreting through float/double types. Fix as_float32() to narrow f64 values through double→float instead of reading wrong low-32 bits. Use direct IEEE 754 division/fmod in concrete_binary_op. Fix f32 test oracles to compute at f32 precision and handle fptrunc overflow. All 230 symbolic executor tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Ship two interlocking refactors that landed on this branch as the substrate for the symbolic-execution work to come: Continuation refactor. A `Continuation<ValueT>` now represents every suspension point — branches, calls, global resolution, memory address concretization — under one polymorphic shape. `with_address` emits a `MemAddrContinuation` that the driver resolves by picking concrete addresses; `resume_addr` specializes a suspended state and continues stepping. New headers: Continuation.h, Sharable.h, SharablePy.h. Sharable interpreter state. `Sharable<T, Policy>` picks the ref-count system per (class, instantiation) at compile time — `StdShared` for the CLI, `PyObjectRC` for the Python bindings — so class code stays policy-agnostic. The Python arm lives in SharablePy.h to keep the plain Sharable header Python-free. Policy<> drops its scheduler template parameter; ConcretePolicy is Sched-agnostic; the no-op scheduler is inlined into the loop. The interpreter library now owns the step loop end-to-end and bin/ InterpretIR is a thin CLI on top. Python bindings expose resume_addr, the sharable state, and a Python-policy subclass surface. memory_view.py adds typed views over ConcreteMemory using the multiplier type system. New test fixtures exercise atomics, unions, and symbolic-address forking. All 235 interpreter tests pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 0 of the symbolic-execution vision (docs/symex-vision.md). Adds the two interpreter primitives the analyst-facing layer needs to stand up under-constrained execution that begins partway through a function with named globals at chosen addresses. Mid-block entry. Split `enter_block` into `clear + push_block_work_items` so the cache-clearing path is separable from the work-pushing path. The new `interp_init_state_at` template seeds `frame.values` with caller-supplied live-ins and pushes a chosen block's work items directly, bypassing the work-stack ENTER_BLOCK handler that would otherwise wipe the seed. Layout primitive. `ConcreteMemory::place_at(addr, size, align)` pre-allocates a region at a chosen virtual address with overlap detection against live regions and bumps `next_alloc_` past placed regions so subsequent bump-allocations don't collide. Python: `init_state_at(state, memory, py_policy, func, block, param_addrs, return_addr, value_seed[, …])` and `place_at` on the `ConcreteMemory` wrapper. Tests: `tests/symex/test_phase0.py` covers P0.1–P0.4 (entry-block equivalence, non-entry start, place_at success / overlap / alignment / post-place allocation) — 8/8 green. The 235-test InterpretIR gate still passes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lands the analyst-facing skeleton on top of the existing C++ symbolic
substrate. Pure Python except for a small tweak to InterpreterState's
steps/empty/depth getters so they read the symbolic state too.
The package (bindings/Python/symex) ships:
- Layout: name -> address book backed by ConcreteMemory.place_at,
with place_global / place_function / __getitem__ / function_at /
address_range.
- SymExEngine: explore(start_func, args, policy, until, ...) drives
init_state + step until terminal or until-predicate. Forks come
in two flavors -- BranchContinuation enumerates both edges,
MemAddrContinuation is concretized via a strategy callable
(default ConcretizeFinite([0])).
- Path: wraps an InterpreterState, carries .id, .events, .tags,
.solver, .clone(), and stub .snapshot()/.restore() pending Phase 3.
- Ctx, MemView, ArgsView: lens/locator shapes for the Phase 2 hook
layer. Phase 1 doesn't dispatch hooks, but the data classes are
stable so hook bodies built on them won't churn later.
- ExploreUntil: composable .path_count(N) / .steps(N) / .time(s)
predicates wired through __or__/__and__.
Tests in tests/symex/test_phase1.py cover P1.1-P1.7 from the vision
plan; P1.5 (z3 named-global readback) is skipped pending the Phase 4
solver integration. The 235-test InterpretIR regression gate stays
green.
Driving forks needs a policy that propagates symbolic-ness through
memory and answers is_true/resolve_branch with None for non-concrete
values. tests/symex/conftest.py ships ForkOnSymbolicBranchPolicy as
the test harness for that until Phase 2 makes it ergonomic.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two-namespace hook layer for the analyst-facing symex API:
* `engine.intercept.<event>` — agentic. Each handler takes
`next_hook` as its last positional argument; forward by calling
it, short-circuit by returning a value without calling it.
* `engine.observe.<event>` — listen-only fan-out, auto-recorded
onto `path.events`. Defaults to the `after` phase; `before` is
available via `engine.observe.before.<event>`.
Composition shape (no `PASS / SKIP / STOP` sentinels): handlers
chain right-to-left at dispatch time so the first-registered runs
outermost. Each `next_hook` is a closure bound to "everything after
me", so the pattern scales to N>2 without changes to the
dispatcher. The chain bottom is a per-event default function that
mirrors the substrate's natural behavior (concrete read for
`memory_read`, concrete write for `memory_write`, defer-to-inline
for `call` / `indirect_call`). `ctx.default()` returns the
substrate's default for the current event; `ctx.stop_path()` marks
the path as stopped without short-circuiting the in-flight chain.
Substrate change in `InterpreterLoop.h::exec_call`: always invoke
`policy.resolve_call` (was: skipped when `target_decl` resolved to
IR). The skip prevented `intercept.call(name=…)` from firing on
direct calls. Concrete policies fall through to `func_resolver_`,
so inlining is preserved.
Lens additions in `lens.py`:
* `MemView.read_struct` / `write_struct` over `(name, offset,
size, signed)` tuples.
* `ArgsView.as_string` / `as_pointer_to`, plus a `_PointerLens`
helper so analysts can read/write through pointer-shaped args.
Reference libc model pack at `bindings/Python/symex/models/libc.py`
covering `strlen`, `memcpy`, `memset`, `read`, `malloc`, `free`.
`engine.use(models.libc)` installs the lot. Each handler doubles as
a composition reference: those that can short-circuit do, those
that can't (e.g., when a pointer arg is symbolic) forward via
`next_hook(ctx)`.
Tests: `tests/symex/test_phase2.py` — 14 P2.x cases covering
addr-range gating, symbolic propagation through `compare`,
write-drop semantics, call/indirect_call interception, the
"forward through next_hook" chain pattern, pre-write-then-forward,
observer auto-recording, observer/intercept coexistence,
exception isolation in observers, and libc-pack registration.
Gates: `pytest tests/symex` 30 passed / 1 skipped;
`tests/InterpretIR` 235 passed.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- Backedge analysis (`cfg.py`): iterative DFS classifies CFG edges as tree / forward / back / cross, names headers and latches, and precomputes which outgoing edge of a loop-guard cond_branch re-enters the loop versus exits it. Cached per function on the engine. - `intercept.branch` chain dispatch + `intercept.loop` sugar with the composition shape — no `CONTINUE / STOP / SKIP_BODY / REPLAY` verbs. Branch handlers compose `(ctx, condition, next_hook)`; loop handlers wrap that with `(ctx, next_hook)` plus a per-firing `LoopContext` carrying iteration / header_block / latch_block / would_exit. `_default_branch` returns `_FORK` for symbolic conditions and `condition != 0` for concrete ones, so a forwarding handler keeps the natural decision. - Per-path back-edge counter `Path._loop_iters[(latch, header)]` bumped by the loop wrapper; survives fork / suspension cloning. - `Path.snapshot()` / `restore()` / `replay(modify=…)` round-trip full path state — interpreter state, events, tags, terminal, return_value, loop counter — through `_Snapshot` and re-clone on restore so snapshots stay reusable. `replay` drives `engine.resume_from` which clones the snapshot's state onto a fresh `Path`, applies `modify(path)`, and runs the engine driver. - `engine.explore(strategy="bfs"|"dfs")` + `ExploreUntil.max_paths(N)` / `max_depth(D)`. DFS commits to a path before opening siblings; BFS expands breadth-first. The engine now pins its layout on first `explore` so subsequent calls (and replay) share an address space. - 6 P3.x tests plus 2 ExploreUntil tests in `tests/symex/test_phase3.py`; phase 0/1/2 (30+1) and InterpretIR (235) gates remain green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
EventLog and PathSet wrappers (list subclasses sharing a
_FilterableList base) add Django-ORM-style predicate queries:
where/first/count over events.kind, addr, step, name, etc., and
over path-level filters terminal, return_value, tags__contains,
events__contains_kind, events__contains_addr.
Path.summary() and path.dot_cfg() render human-readable views over
the recorded event stream. The substrate doesn't yet emit per-block
enter events to Python, so dot_cfg renders branch-transition graphs.
z3 wiring lands across dispatch, path, and engine:
- ctx.solver.fresh_int(name, *, size, lo=None, hi=None) mints a
cached BitVec and adds the optional bounds to path_condition.
- compare / binary_op / unary_op produce derived z3 exprs when an
operand is a z3 expression; opcode dispatch is table-driven and
anchored to mx.ir.OpCode so the ranges track the C++ enum.
- is_true / resolve_branch return None on z3 conditions so the
substrate forks; _handle_branch_forks accumulates the branch
condition (cond on true child, Not(cond) on false child) onto
each child's path_condition.
- path.assert_(cond) adds a constraint and marks the path
terminal=Terminal.INFEASIBLE when the resulting set is unsat.
- path.solver.model() returns {name: int} on sat, None on unsat.
- The z3 module reference is cached at module load so the
per-IR-op _is_z3 check costs one dict lookup, not a try/import.
Stringly-typed code is gathered into StrEnums (EventKind, Phase,
BranchDirection, Terminal, StepResultKind, Strategy, CallAction,
EdgeKind) so equality with the existing string literals still works
but call sites reference the typed members.
6 P4.x tests in tests/symex/test_phase4.py exercise the new
surfaces; tests/symex/test_phase1.py::test_p1_5_z3_named_global
is un-skipped and now solves.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Symbolic-address suspensions previously consumed a single `concretize=lambda fork: [k]` callable. Phase 5 makes this typed, named, selector-routed, and sound under the path's z3 condition. Adds: - `AddressStrategy` ABC + `Decision` / `ConcretizeTo` types in `bindings/Python/symex/concretize.py`. `Decision` is the seam Phase 6 widens with `SplitByRegion` and `ConstrainTo`. - Four built-ins: `ConcretizeFinite`, `ConcretizePointerSet` (with `.functions(layout)` / `.globals(layout)` classmethods), `ConcretizeByRegion`, `ConcretizeViaSolver`. - `engine.address_strategy` (default), and selector-based `engine.concretize_at(strategy, **selector_kwargs)` reusing the intercept dispatch's `_Selector` (`addr_range=`, `name=`, `eid=`). - `ConcretizeViaSolver` attaches `addr_var == k` as `extra_constraint` so the child path's solver agrees with the executed address. - Feasibility pre-check on every concrete candidate; emits `concretization_infeasible` for rejects. - New `EventKind.CONCRETIZATION_TRUNCATED` / `CONCRETIZATION_INFEASIBLE`; new `Terminal.CONCRETIZATION_REFUSED` (distinct from STUCK_SUSPENSION). - Legacy callable shape (`concretize=lambda fork: [...]`) still works through `_CallableStrategy`. Tests: 10 new P5.x tests in `tests/symex/test_phase5.py`. Two are strategy unit tests (P5.2 ViaSolver + P5.3 PointerSet + P5.4 ByRegion + P5.8 feasibility) since the substrate's `ptr_add` collapses z3 indices to concrete during pointer arithmetic, so an organic explore never produces a suspension whose `address_expr` is a live z3 expression. The remaining tests are end-to-end through `symbolic_test_ptr_add`. Gates: 56/56 tests/symex green (46 prior + 10 P5); 235/235 tests/InterpretIR green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Multiplier's Python bindings already return the most-derived type, so `mx.ast.FunctionDecl.FROM(decl)` and similar `.FROM` casts are unnecessary in Python — they're a C++-flavored code smell. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 6 widens the Phase 5 Decision seam so the engine can fork on region-shaped suspensions, materialize lazy backing storage for unbacked symbolic pointers, and surface concrete-mode bug findings through a sink registry. - Region, LazyRegion, RegionTable (sorted-by-base interval index) in bindings/Python/symex/region.py. Layout upgraded to back globals with Region objects plus regions(), region_containing(addr), regions_overlapping(lo, hi); legacy globals()/functions()/ address_range()/[name] API preserved. - New Decision variants: ConstrainTo(z3_predicate) and SplitByRegion(regions=(...)). ConcretizeByRegion widened to return a single SplitByRegion so the in-region offset stays symbolic when the substrate carries it (Phase 7 dependency, see below). ConcretizeByRegion(..., lazy_default=True) materializes a fresh LazyRegion via Layout.declare_lazy when the layout has no regions. - Engine wiring: _handle_suspension dispatches the three Decision variants through dedicated helpers; SplitByRegion + ConstrainTo each have a symbolic-addr path (resume_addr_symbolic, assert in-region predicate) and a concrete-addr fallback (degrade to resume_addr at the region base / chosen address). lazy_region_budget caps LazyRegion materializations per path; over-quota emits lazy_budget_exhausted and refuses. - Per-region z3 Array overlay (BitVec(64) -> BitVec(8)) with per-byte store/select primitives. Overlay backing array is K(0) so unwritten bytes read as zero. Concrete writes mirror byte-by-byte into existing overlays so symbolic-offset reads see the prior concrete bytes; cost is paid only after first symbolic touch. - Required substrate hook: interp_resume_addr_symbolic(state, eid, py_value) writes a Python value (typically a z3 expression) into the suspended op's address slot. Sibling get_value_at(state, eid) for testing the round-trip. - Sink framework: Sink ABC, Finding dataclass (kind, addr_eid, step, witness, region, mode), SinkRegistry. Three built-ins: OOBSink, NullDerefSink (memory_read/memory_write); DivByZeroSink (binary_op). Each has a concrete-addr mode (containment / numeric check, no solver) and a symbolic-addr mode (path_condition ∧ bad-predicate). OOBSink's concrete-addr mode discriminates substrate-internal accesses from real OOB by requiring a MEMADDR_CONCRETIZE event for the access's address. Sinks fire after the policy event; fatal=True terminates with Terminal.SINK_HIT. - path.findings (FilterableList) and path.regions_touched() aggregating per-region read/write counts from auto-recorded memory events. Memory events now record unconditionally so sinks and queries work without an explicit observer. - New event kinds: region_materialized, lazy_budget_exhausted, constrain_to_concrete_addr, split_by_region, sink_fired, binary_op. New terminal: SINK_HIT. - 16 P6.x tests (8 [U] strategy/overlay, 8 [E2E] end-to-end, including a CWE-787-style worked example through symbolic_test_ptr_add over an 8-byte g_buf with ConcretizeFinite enumeration). 72 total in tests/symex; 235 in tests/InterpretIR unchanged. Deferred to Phase 7: Python dispatch for PythonPolicy::ptr_add / ptr_diff / ptr_offset (SymbolicInterpreter.cpp:442/449/456). Until that lands, organic explores never produce a suspension whose address_expr is a live z3 expression, and Phase 6's symbolic-addr modes only fire on synthesized fixtures (or on DivByZeroSink where binary_op is already Python-dispatched and routes a symbolic divisor through). Phase 6 was structured so the seam, region table, overlay, and sink registry are all correct under both modes — Phase 7 flips one switch. The CWE-787 store-side variant in tests/symex/c/cwe787_oob_write.c is also Phase 7 material: adding a new C file requires rebuilding the InterpretIR test database. Phase 6's exemplar test produces the same shape (oob_read concrete-mode Findings) through the existing corpus. docs/symex-vision.md updated: Phase 6 section replaces the old "polishing & docs" stub with regions+sinks; Phase 7 section calls out ptr_add dispatch as the gating item alongside the worked notebook polish. docs/symex-phase6-plan.md deleted. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
PythonPolicy::{ptr_add, ptr_diff, ptr_offset} now dispatch through
Python first, mirroring the binary_op / cast shape; new cache fields
cached_ptr_*_. The concrete fallback runs only when the policy returns
NotImplemented, so callers without ptr_* methods see no behavior change.
InterceptorPolicy.{ptr_add, ptr_diff, ptr_offset} lower symbolic
operands to z3 BitVec(64) — base zero-extended, index sign-extended,
element-size scaled in z3; ptr_diff's element-size division uses UDiv.
A small _addr_as_z3 helper normalizes ints / ("ptr", N) / z3.
Adds tests/symex/c/cwe787_oob_write.c (copy_into / store_at /
store_at_u64) as the corpus for the worked example. The InterpretIR
compile_commands.json (untracked, user-local) carries the new
entry; the test DB is regenerated by the user out of band.
tests/symex/test_phase7.py (7 tests, P7.1–P7.7):
- P7.1 proves ptr_add now dispatches through Python via the
presence of a MEMADDR_CONCRETIZE event.
- P7.2 proves _addr_feasible filters unreachable decisions
against the live path condition (vacuous pre-Phase 7).
- P7.3 verifies ConstrainTo on a synthesized symbolic addr_expr
lands the constraint without firing the concrete-fallback
regression-guard event.
- P7.4 drives _dispatch_split_by_region over a region whose size
is not a multiple of the access size; OOBSink fires symbolic
mode at the partial-overflow upper boundary.
- P7.5 is the CWE-787 worked example: store_at over dst[16] with
ConcretizeFinite enumerating in/OOB addresses; OOB children
produce reproducible oob_write Findings whose witness is the
resolved address.
- P7.6 walks copy_into end to end, verifying both branches of
the bounds check (8 src reads + 8 dst writes on the safe path,
0 dst writes on the early-return path).
- P7.7 sweeps the symex package with doctest.testmod.
P6.9 / P6.12 had idx ranges that were vacuously satisfiable only
under the substrate's pre-Phase 7 collapse-to-concrete behavior;
widened the bounds so ConcretizeFinite's decisions remain feasible
under the new symbolic addr_expr.
Substrate gap (deferred, documented in symex-vision.md):
with_address_impl re-suspends on every symbolic-addr LOAD, so
end-to-end exploration through SplitByRegion / ConstrainTo (which
resume via resume_addr_symbolic) needs a future symbolic_load /
symbolic_store policy hook. P7.3 / P7.4 cover the wiring up to that
seam synthetically; P7.5's witness flow goes through ConcretizeFinite
+ resume_addr (concrete) and is unaffected.
79 symex tests + 235 InterpretIR tests green.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes the substrate gap Phase 7 documented but couldn't fix without scope creep: with `SplitByRegion`, the resumed path used to re-suspend on every LOAD because `with_address_impl` saw a non-extractable z3 address. End-to-end exploration through `SplitByRegion`, `ConstrainTo`, and `LazyRegion` now runs organically through `engine.explore`. `exec_load` / `exec_store` consult `policy.exec_symbolic_load` / `exec_symbolic_store` before falling through to `with_address`'s suspension path. The CRTP base in `Policy.h` provides a no-op default; `PythonPolicy` overrides via cached `cached_symbolic_load_` / `cached_symbolic_store_` method handles that mirror the `mem_read` / `mem_write` shape exactly. Other `with_address` callsites (indirect-call resolution, init-time memcpy, etc.) are unchanged. `InterceptorPolicy.symbolic_load` / `symbolic_store` consult `path._region_at_suspension` to read/write through the region overlay (`region.select_byte` / `store_byte`) little-endian. Returning `NotImplemented` when no region context is available keeps the existing suspension semantics for non-region-tagged paths — no silent default-0 collapse. Tests: 7 P8a cases in `tests/symex/test_phase8a.py` upgrade Phase 7's hybrid P7.3 / P7.4 to true E2E for the SplitByRegion / ConstrainTo paths and exercise the LazyRegion + concrete-write- mirror seams. `tests/symex` total: 86 (was 79); `tests/InterpretIR` still 235. `docs/symex-vision.md` Phase 7 future-work block converted to delivered, with explicit non-goals retained for the still-deferred phases (typed pointer values, cross-path merging, auto-derived layouts, float-typed overlay slots, custom symbolic memory models). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two surgical correctness fixes that close honesty gaps Phase 8a left visible: 1. `read_return_value` no longer collapses symbolic returns to 0. The substrate used to overwrite the live `ret_from_inst` with a slot read of `frame.return_ptr`; for symbolic returns the slot was never written (the default `mem_write` chain drops z3 values), so `path.return_value` came back silently as `0`. A new `bool has_ret_value` thread through `exec_ret` short-circuits to `ret_from_inst` whenever the RET carried an operand. Aggregate- style returns (RET without operand, function memcpy'd into the slot) are unaffected — `has_ret_value=false` still flows through the existing slot-read code. 2. `engine.observe.global_read` / `global_write` actually fire. The events were declared, exported, and selector-matched but no dispatch path ever called `_fire_observers(GLOBAL_READ, …)`. `InterceptorPolicy` now fans `mem_read`, `mem_write`, and the Phase 8a `symbolic_load` / `symbolic_store` accesses out to the global-event registry whenever the access lands in a `kind == "global"` region. Lazy and function-placement regions are filtered out — they aren't analyst-named globals. Goal #9 ("per-path trace of which globals were accessed and when") is now real. 10 new tests in `tests/symex/test_phase8b.py` (P8b.1–P8b.10; P8b.4 skipped — corpus has no function exposing a no-operand RET). `tests/symex` total: 96. The 235-test InterpretIR harness still passes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 8b shipped a workaround for symbolic primitive returns: a
has_ret_value short-circuit in read_return_value that bypassed the
slot read whenever RET carried an SSA operand. The underlying gap
remained — the dispatcher's default mem_write silently dropped z3
values, so any symbolic write to a substrate-allocated address
(return slot, ALLOCA/ARG, ALLOCA/LOCAL, VLA storage) vanished. The
workaround also cemented a confusing dual-source-of-truth in the IR
(RET carries the value AND the preceding store puts it in the slot).
Phase 8c does it the right way:
- Path now carries a per-path _symbolic_shadow: dict[(addr, size)
-> z3 expr] whose reference is shared with the InterceptorPolicy
constructed for that path. The dispatcher's default mem_read /
mem_write consult the shadow for z3 values written to concrete
substrate-allocated addresses, so writes survive across steps
(policy is fresh per step; path is durable). Concrete writes
evict the shadow entry at the same key. snapshot/restore round-
trip the shadow in place so any policy still holding the
reference sees the post-restore state.
- IRGen no longer sets inst.operand_indices on RET; the value flows
exclusively through RETURN_PTR + MEMORY/STORE into the slot.
RetInst::return_value() is removed (header, impl, generated
Python binding, type stub). RET is a pure terminator.
- read_return_value is restored to its pre-Phase-8b shape (no
has_ret_value parameter, no SSA-operand short-circuit). The slot
read is the universal mechanism. P8b.1's symbolic-return
invariant still holds — now via the shadow-backed slot read.
Phase 8b's global-event fan-out (_fire_global_event_if_applicable
and the four call sites in mem_read / mem_write / symbolic_load /
symbolic_store) is orthogonal and unchanged.
One new test in tests/symex/test_phase8c.py (P8c.1) drives a z3
mem_write and a same-(addr, size) mem_read through two distinct
InterceptorPolicy instances sharing the same Path, exercising the
cross-step flow that the return slot, ALLOCA/ARG, and ALLOCA/LOCAL
all rely on.
Gates after re-indexing /tmp/tests.db against the new schema:
- tests/symex: 96 passed, 1 skipped (95 baseline + P8c.1; P8b.4
aggregate-return placeholder remains skipped).
- tests/InterpretIR: 235 passed.
docs/symex-vision.md gains a Phase 8c subsection and an updated
Definition of done entry.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Four loose ends from Phase 8c, none requiring architectural rework: 1. `engine.intercept.symbolic_load` / `symbolic_store` are reachable. Adds SYMBOLIC_LOAD / SYMBOLIC_STORE to EventKind, exposes them through InterceptDispatcher, and refactors the existing region- overlay logic into a chain bottom that analyst handlers compose over via `next_hook`. New `region=` selector matches against `path._region_at_suspension`. 2. Init-time z3 args persist. `engine._init_path` migrates the init-policy's symbolic shadow to the path's durable shadow after `init_state` runs, so `engine.explore(name, args=[z3_var])` works end-to-end through ALLOCA/ARG (P8d.3). 3. P8b.4 un-skipped. Drives `make_large` from `tests/InterpretIR/test_byvalue.c` to exercise the substrate's `read_return_value` sz>8 branch. (Field-value verification is gated on a separate substrate quirk with LOCAL_VALUE allocas through InterceptorPolicy; documented inline.) 4. Per-block-enter event. New `on_enter_block(state, block)` policy callback fires at the top of every `enter_block` in InterpreterLoop.h. ConcretePolicy keeps a no-op default; PythonPolicy fans out to `engine.observe.block_enter` and appends BLOCK_ENTER events to `path.events`. `path.dot_cfg` widens to walk both BRANCH and BLOCK_ENTER events, so branchless functions render real graphs instead of the empty placeholder. Tests: tests/symex/test_phase8d.py (P8d.1, P8d.2, P8d.2b, P8d.3, P8d.4) — 5 added; P8b.4 un-skipped; tests/symex/test_phase4.py P4.6 updated for the new dot_cfg behavior. Final counts: 103 symex passed (was 96+1 skipped), 235 InterpretIR passed. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Phase 8d's tightened P8b.4 surfaced that engine.explore("make_large",
args=[7]) silently returned a return slot full of zeros — every field
store landed at address 0 instead of the local's slot. Three substrate
seams were complicit:
- value_to_python lowers a Value to a bare PyLong, dropping the
("ptr", N) tag carried by make_literal_ptr.
- The ptr_add / ptr_offset C++ fallbacks ran results through that
lowering, producing plain ints from pointer arithmetic.
- PythonPolicy::extract_address only accepted tuple-tagged pointers,
so any plain-int address triggered the symbolic-suspension path,
which the default address strategy collapsed to 0.
The fix wraps the ptr_add / ptr_offset fallbacks in make_literal_ptr
and teaches extract_address to also accept bare PyLongs (a plain int
IS a concrete address). After the fix, engine.explore is correctness-
equivalent to ConcretePolicy on every function in the corpus that
exercises LOCAL_VALUE allocas through GEP_FIELD.
P8b.4's "substrate quirk" caveat is removed — the tightened test now
asserts [7, 8, 9, 10, 11] field values directly. Three pre-existing
tests in tests/InterpretIR/test_symbolic_addresses.py that relied on
plain-int suspension were reworked to use an opaque-sentinel policy
so they still drive the suspension/resumption loop without exploiting
the old bug.
Phase 8e Item 2 (float-typed overlay slots): _coerce_store_value now
packs Python floats via _struct.pack("<f"|"<d", val) and lifts the
IEEE byte pattern into a z3.BitVecVal. A symbolic-overlay float store
+ load round-trips through the bit pattern.
tests/symex: 103 → 109 (+P8e.1, P8e.2[*4], P8e.3); InterpretIR: 235.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two probe-time fixes for BuildCommandAction. GetCompilerInfo no longer re-adds `-o /dev/null` after stripping the original output flag. Some Apple clang flag combinations error with "cannot specify -o when generating multiple output files" when the redirect is present, and Subprocess::Execute already discards the probe's stdout, so the explicit redirect is redundant. Run() now skips translation units whose command line is preprocess- only (`-E`, `--preprocess`, `-Eonly`). PASTA strips `-E` to force AST construction, which makes such commands fail later with confusing diagnostics about missing types — e.g. APR's `export_vars.c` is fed through `clang -E | sed` to generate an exports list, not as a real TU. Skipping up front avoids the noise. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Multiplier's Python bindings already return the most-derived type; .FROM(...) downcasts are a C++-style smell. Replace them with isinstance(...) checks, factoring an _as(ty, cls) helper in memory_view.py where the pattern repeats and a pair of _func_decl_for / _var_decl_for unwrappers across the InterpretIR test helpers. Cross-entity converters (FunctionDecl -> IRFunction) keep using .FROM since they cross hierarchies rather than downcast within one. Also collapses nested Fragment.IN -> Decl.IN -> FunctionDecl.FROM loops into a direct FunctionDecl.IN(index), and replaces Entity.FROM(idx, eid) with idx.entity(eid). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`engine.explore_many(start_funcs)` accepts a list of names or IRFunctions (mixed allowed), a compiled regex pattern, or a name predicate, and drives one combined exploration over every matched entry under a shared Layout and a shared `until` predicate. Each Path carries an `entry_func` attribute (the IRFunction the path started in), propagated through forks. `PathSet.by_entry()` groups the result by entry in resolution order so analysts can answer "which entries hit the OOB sink?" in one pass. Entries drive sequentially. The user's `until` sees the cumulative state across entries; a cross-entry guard re-checks before initializing each next entry, so a triggered predicate cleanly skips remaining entries (they leave no zero-step paths behind). Empty resolution raises ValueError to catch typo'd regexes before they vanish into a silent no-op exploration. Sub-block resume granularity, path serialization, and per-entry args mapping remain deferred per the vision doc. tests/symex: 109 -> 116 (P8f.1-P8f.7); InterpretIR: 235. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Forward — intercept.address_for(kind=, name=, eid=) fires when the engine needs an address for a function, global, or thread-local entity. Pre-placement in Layout wins over the hook chain wins over the substrate auto-allocator. Memoized per canonical_eid so repeat references reuse the assigned address. observe.address_resolved provides telemetry with source and handler fields. Reverse — intercept.indirect_call now accepts target_kind="symbolic" and fires on symbolic call targets via a new "call-addr" suspension sub_kind. Returning a list of addresses forks one child per candidate, each with target_expr == candidate_addr asserted. Terminal.UNRESOLVED_CALL terminates paths whose handler returns None. Substrate: AddressKind enum + GlobalInfo.address_hint; function_addresses per-state cache; compute_func_ptr honors FunctionAddressResolver hint; exec_call marks call-target suspensions via mark_next_suspension_as_call_target; MemAddrContinuation.is_call_target flag; all Symbolic* entry points thread func_addr_resolver_obj; _make_global_resolver_with_hints returns 5-tuples; PythonPolicy.address_for_function_impl + mark_next_suspension. Layout gains place_functions, place_globals, next_function_address (0x4000_0000_0000_0000 cursor), tls_offset + tls_base (0x6000 range). Path gains tls_base and _tls_shadow; _fork_child propagates both. Per-path TLS isolation is implemented at the Python level via _tls_shadow (same shape as _symbolic_shadow), verified by P9.7b/c. engine.value_origins side-table ships for Phase 10 lineage walks. _current_path set around each step call so address_for hooks receive a path-aware ctx. tests/symex: 116 -> 131 (P9.1-P9.13 with P9.7b/c); InterpretIR: 235. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Instruments solver.fresh_int to record mint-site metadata into
path._origin_by_name (kind, name, size, path_id, step). Adds
Path.origin(expr) which DFS-walks a z3 AST to collect origin records
for all leaf BitVec variables, deduplicating repeated leaves. Adds
Path.origin_tree(expr) for a recursive {"kind":"leaf"/"op"} view.
Both propagate through clone() and _fork_child so forked paths retain
the full provenance of symbolic inputs minted before the fork.
Tests P10.1–P10.10 cover: origin recording, idempotency, single-var and
compound-expr aggregation, concrete exprs, unknown variables, tree shape,
op nodes, clone propagation with independence, and deduplication.
symex 131 → 141 (P10.1–P10.10); InterpretIR 235.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
PathSet gains six new analysis methods:
- all_terminal() — True when every path has a non-None terminal
- terminals() — {terminal: PathSet} partition
- findings() — aggregated FindingsList across all paths, each finding
annotated with path_id
- summary_table() — human-readable counts per terminal + finding total
- counter_example(pred) — first (path, SMT-model) where pred holds and
path is SAT; None when nothing matches
Path gains two thin taint helpers built on origin():
- taint_sources(expr) → frozenset of fresh_int variable names that
flow into expr, excluding unknown/external variables
- is_tainted(expr) → bool shorthand
Tests P11.1–P11.14 cover: taint_sources basic/exclude-unknown,
is_tainted T/F, all_terminal T/F, terminals grouping, findings
aggregation/empty, summary_table content + findings line,
counter_example found/none/unsat-skipped.
symex 141 → 155 (P11.1–P11.14); InterpretIR 235.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Adds four analyst-facing query methods to Path, all side-effect-free (each builds a fresh z3.Solver or z3.Optimize from path_condition): - can_be(expr, value) → bool: SAT check with expr == value added - must_be(expr, value) → bool: UNSAT check with expr != value added - possible_values(expr, *, limit=10) → sorted list[int]: enumerates distinct satisfying values by blocking each found assignment - value_range(expr) → (lo, hi) or None: tight unsigned bounds via z3.Optimize minimize/maximize; None on UNSAT Tests P12.1–P12.14 cover: unconstrained/constrained can_be, must_be T/F/partial, possible_values multiple/constrained/UNSAT/sorted, value_range bounded/unconstrained/UNSAT, compound expressions, and non-destructive invariant for can_be. symex 155 → 169 (P12.1–P12.14); InterpretIR 235. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
… 6-10 _Snapshot was missing seven fields introduced after its initial design: findings, region_at_suspension, lazy_regions_used (Phase 6), entry_func (Phase 8f), tls_base, tls_shadow (Phase 9), origin_by_name (Phase 10). snapshot() silently dropped these fields; restore() left them at stale values; resume_from() only had a getattr guard for tls_base. After a snapshot/restore or replay cycle, findings, per-path TLS values, and symbolic-value provenance were all wrong. Changes: - _Snapshot.__slots__ and __init__ extended with all 7 fields - Path.snapshot() populates them (defensive copies for dicts/lists) - Path.restore() restores them; mutable dicts use clear()+update() in-place to preserve any external references - engine.resume_from() restores findings/region_at_suspension/ lazy_regions_used/entry_func/tls_shadow/origin_by_name via getattr so pre-Phase-13 pickled snapshots still work - FindingsList imported at module scope in engine.py (was inline-only) Tests P13.1–P13.9 verify round-trip for each field + snapshot independence + __slots__ completeness check. symex 169 → 179 (P13.1–P13.9 + P13.1b); InterpretIR 235. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…th.condition_str
_FilterableList (base for EventLog, PathSet, FindingsList) gains:
- last(**filters) — last matching item, complement of first()
- groupby(field) — {field_value: same-subclass} partition, preserves order
- unique(field) — set of distinct values for a field across all items
- _get_field(item, key) hook: dict.get for dict-like items, getattr for objects
Layout gains:
- name_for(addr) → str | None — reverse lookup wrapping region_containing()
Path gains:
- condition_str(*, sep="\nAND ") → str — human-readable path condition;
returns "True" for an unconstrained path
Tests P14.1–P14.18 cover: last with/without filter, no-match/empty,
groupby kind/order/missing-field, unique basic/empty/None, PathSet.groupby
via base class, name_for global/unmapped/function, condition_str
empty/single/multi/custom-sep.
symex 179 → 197 (P14.1–P14.18); InterpretIR 235.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Tests: 18 new end-to-end integration tests (IT.1-IT.18) against real indexed IR in tests/symex/c/ (mx-index.db built with --fork_mode). Coverage: address_for/address_resolved hooks (P9), origin/taint_sources on real IR arithmetic (P10), multi-path PathSet analysis (P11), can_be/must_be/value_range on real path conditions (P12), snapshot round-trips (P13), groupby/unique/last on real event logs (P14). Fixes: _init_path now registers externally-supplied z3 BitVec args in path._origin_by_name so origin() / taint_sources() can trace provenance through them. Previously only args minted via solver.fresh_int() were recorded; args passed directly to explore() were silently unknown. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Module.cpp: inject __path__ = [<site-packages>/multiplier/] at the end of PyInit_multiplier via a small PyRun_String snippet, making multiplier act as a package so `import multiplier.symex` works without renaming the .so. - CMakeLists.txt: install symex/ as multiplier/symex/ in both the build-tree copy and the install target. - lens.py: add LocalsView — debugger-style lens over a function's ALLOCAs (discover, seed concrete/symbolic values, seed_dict for engine.explore(), read/write/dump on live paths). - __init__.py: export LocalsView from the top-level symex package. - All symex tests updated: from symex.X → from multiplier.symex.X. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Layout() now takes an optional ConcreteMemory as its first argument.
When omitted the existing default ConcreteMemory() is used unchanged;
when supplied the caller's memory becomes the backing address space.
This lets the analyst control address width and the allocator cursor:
mem = mx.ir.interpret.ConcreteMemory(4) # 32-bit
layout = Layout(mem)
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
layout.place_string(name, value, *, addr=None, encoding="utf-8",
null_terminate=True) -> int
Places a string literal (str or bytes) in the layout's backing memory
and returns the pointer address. Null-termination is on by default.
When addr is omitted, auto-allocation first checks whether the exact
byte sequence already appears as a tail of any existing string region
(suffix sharing — same deduplication strategy linkers use for string
tables). "world\0" placed after "hello world\0" aliases into it at
the appropriate offset without new allocation. Explicit addr= bypasses
the check and uses place_at as usual.
Suffix-shared names are registered in _by_name but not added to
_regions, since their bytes are owned by the enclosing region.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Removes the suffix-finding scan entirely. Auto-allocated strings use the memory bump allocator; explicit addr= writes directly without collision checks (the user is responsible for the address). String regions are not added to the RegionTable (the sorted interval tree used by OOB sinks and region_containing), so overlapping strings placed at explicit addresses don't raise. layout["name"] still returns the pointer via _by_name. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ThreadLocal::GetOrInit used a raw pointer (tInstance) for the fast-path
cache, which produced a false hit when a new ThreadLocalBase was allocated
at the same address as a previously destroyed one. The result was
returning stale thread-local data from a different Index, causing a
null-pointer deref inside SQLiteEntityProvider::DeclsFor.
Fix: assign each ThreadLocalBase a monotone uint64_t id_ on construction
and store tInstanceId alongside tInstance in the fast path; both must
match before returning the cached pointer. Also switch the slow-path
map lookup from operator[] (which silently inserts a nullptr entry under
a shared_lock — a data race) to find().
Other changes in this commit:
- symex/events.py: add INSTRUCTION EventKind for the on_instruction hook
- symex/layout.py: add bind_string_literal + entity= arg to place_string
for the resolve_string_ptr hook
- unsupported_args.cfg: extend skip list with -ffixed-r{8,9}/-mno-abicalls
- test_phase7.py: test_p7_5/p7_6 use symex_index not index (store_at and
copy_into live in the symex C corpus, not the InterpretIR database)
215 symex + 235 InterpretIR tests green.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- Policy.h: add on_instruction() / on_instruction_impl() (no-op default) and abort_requested() / abort_requested_impl() (returns false) CRTP hooks - InterpreterLoop.h: dispatch() calls policy.on_instruction(state, sched, inst) before the switch for every non-trivial work item (not ENTER_BLOCK/ANALYZE); clears work_stack and returns if abort_requested() - SymbolicInterpreter.h/cpp: PythonPolicy::on_instruction_impl_inner() looks up and calls the Python policy's on_instruction method; cached_on_instruction_ field added; destructor Py_XDECREF'd - dispatch.py: InterceptorPolicy.on_instruction() dispatches to engine.observe.instruction observers; INSTRUCTION imported from events Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
compute_global_ptr ran info.initializer unconditionally, so a C global's IR initializer would overwrite memory the analyst had already seeded via engine.layout.place_global(..., init=...). Guard with !placed_via_hint: when the address hint was honoured (either place_at succeeded or the region was already live), the analyst's init data is authoritative and the IR initializer must not run. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Python hook exceptions raised inside intercept.call (and other policy callbacks) were silently swallowed: resolve_call caught them in a try/except, recorded INTERCEPT_ERROR, and returned _DEFER, while C++ called PyErr_Clear() on any remaining indicator. Fix: - Remove try/except from Python resolve_call so the exception propagates into C++ as a set PyErr indicator. - Add capture_exception() / has_pending_exception() / abort_requested_impl() / raise_pending_exception() to PythonPolicy so the indicator is captured rather than cleared. - interp_step checks abort_requested() after each dispatch() call and breaks the loop immediately when set. - SymbolicStep re-raises the captured exception before returning to Python so the caller sees the original traceback. - MemView.write_bytes now raises a descriptive TypeError instead of passing a z3 expression to bytes(), which produces a confusing error. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
resolve_call and resolve_branch both have (or have access to) the
triggering IRInstruction on the C++ side but were not passing it to
Python, leaving Python handlers with less context than the C++ interface
provides.
- Policy::resolve_branch gains `const IRInstruction &branch_inst` as its
second parameter (after sched, before condition). ConcretePolicy and
InterpreterLoop updated accordingly.
- PythonPolicy::resolve_call names the previously-anonymous `call_inst`
parameter and converts it via to_python<IRInstruction>.
- PythonPolicy::resolve_branch converts `branch_inst` the same way.
- Both C++ methods prepend the instruction object as the first positional
arg to their Python calls ("N..." format steals the new reference).
- InterceptorPolicy.resolve_call and resolve_branch each receive the
instruction as their first positional parameter and assign it to
ctx.inst, making it available to every intercept.call / intercept.branch
handler via ctx.inst.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
… branch/call handlers IRInstruction.to_python previously always allocated the base IRInstruction wrapper regardless of opcode, so isinstance(inst, mx.ir.EnterScopeInst) always failed. Added an opcode-based dispatch that mirrors the from() methods in InstructionKinds.cpp: single opcodes map directly to their subtype wrapper; ALLOCA dispatches by alloca_kind; MEMORY dispatches by ConsumeVAParamInst::from(). ctx.inst is now set in intercept.call and intercept.branch handlers (the instruction object is the call site or conditional branch that triggered the event). This required: - ForkOnSymbolicBranchPolicy.resolve_branch receives branch_inst as first arg - InterceptorPolicy.resolve_call has call_inst=None default so test code that calls it directly without a live instruction still works - test_p9_8 passes call_inst=None explicitly Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The generated to_python always allocated gType (IRStructure base), breaking isinstance checks for IRIfStructure, IRForStructure, etc. Switch on StructureKind to select the right gTypes[] slot. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
kumarak
approved these changes
Apr 29, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
bindings/Python/symex/— mid-block entry, layout/memory model, intercept/observe hook chains, path snapshots, DFS/BFS exploration, z3 SMT integration, region-aware OOB detection, symbolic load/store, provenance walk, taint tracking, PathSet analysis, and address-space mediationIRInstruction.to_pythonandIRStructure.to_pythonnow dispatch to most-derived Python subtypes (opcode/StructureKind switch), soisinstance(inst, mx.ir.EnterScopeInst)works correctlycall_instandbranch_instthreaded from C++ substrate throughPythonPolicyinto Python hook context (ctx.inst); exception propagation from hooks back through the interpreter loopTest plan
python -m pytest tests/symex/ -q— 215 passedpython -m pytest tests/InterpretIR/ -q— 235 passed (no regressions)🤖 Generated with Claude Code