Symex: fork isolation, concrete-detection hardening, bulk-memory hook surface, explore_next

[pgoodman]

Summary

• Fork isolation — _fork_child was not propagating three per-path fields (findings, _region_at_suspension, _lazy_regions_used) to child paths; sibling paths shared the parent's mutable state. Fixed by propagating all three fields on fork, matching what Path.clone() already did. Also fixed _init_seeded_path for the same fields.

• Per-path CoW for concrete writes — _make_default_mem_write previously wrote concrete values only to shared ConcreteMemory, so any fork that wrote through the default handler would have its write visible to sibling paths. Concrete writes now also place per-byte BitVecVal entries in the per-path shadow, giving copy-on-write isolation. Shadow reads use a new _shadow_range_is_concrete helper to distinguish fully-concrete shadow ranges (unwrap to int) from symbolic ones (return z3 expression), preserving analyst-visible symbolic shape.

• Concrete-detection hardening — narrow isinstance(v, int) checks at terminal-use sites (address coercion, branch resolution, is_true) replaced with _concrete_int / _concrete_bool helpers that call z3.simplify so a structurally non-trivial but provably-constant z3 expression (e.g. Concat(BVV, BVV) + 0 from a multi-byte shadow load) does not force a spurious MemAddrSuspension or branch fork.

• Endian enum — all "little" / "big" string literals and str(self._engine.endian) cargo-cult wrappers replaced with Endian.LITTLE / Endian.BIG from _types.py.

• _memop_name helper — bulk-op name derivation now drives off mx.ir.MemOp(int(op)).name so the name list stays in sync with the C++ enum automatically instead of a hand-maintained dict.

• Bulk-memory hook surface — new intercept.bulk_memory(op="memcpy") (and other op names) hook axis. The C++ substrate calls mem_bulk_op; Python dispatches to any registered analyst handlers and then to a per-op default decomposer that re-fires the existing memory_read / memory_write hooks per byte. Supported ops: memcpy, memmove, memset, bzero, memcmp, memchr, strlen, strnlen, strcmp, strncmp, strchr, strrchr, strcpy, stpcpy, strncpy, stpncpy, strcat, strncat.

• explore_next / from_path= — engine.explore(..., from_path=P) clones the prior path's per-path state into a fresh initial path for the new target function. path.explore_next(target) is the sugar.

• Phase 15 test correction — a C switch with no default: label still has an implicit default IR edge (three successors total); the test assertion for that case was wrong. Corrected to expect three completed paths with return values {10, 20, 0}.

🤖 Generated with Claude Code