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

bindings/Python/SymbolicInterpreter.cpp

@@ -239,6 +239,7 @@ PythonPolicy::~PythonPolicy() {
   Py_XDECREF(cached_on_enter_block_);
   Py_XDECREF(cached_on_global_initialized_);
   Py_XDECREF(cached_on_instruction_);
+  Py_XDECREF(cached_mem_bulk_op_);
   Py_XDECREF(pending_exc_type_);
   Py_XDECREF(pending_exc_value_);
   Py_XDECREF(pending_exc_tb_);
@@ -699,6 +700,37 @@ bool PythonPolicy::exec_symbolic_store_impl(PythonScheduler &,
 bool PythonPolicy::mem_bulk_op(PythonScheduler &, MemOp sub,
                                 const std::vector<SharedPyPtr> &ops,
                                 const MemoryInst &mi, SharedPyPtr &result) {
+  // Try the Python policy first so analysts can intercept whole bulk
+  // ops (and so the per-byte default decomposition fires `mem_read` /
+  // `mem_write` hooks). NotImplemented = "fall through to concrete";
+  // any other return is the IR result of the bulk op.
+  if (PyObject *method = lookup_method(cached_mem_bulk_op_, "mem_bulk_op")) {
+    PyObject *ops_list = PyList_New(static_cast<Py_ssize_t>(ops.size()));
+    if (!ops_list) {
+      capture_exception();
+      result = make_default();
+      return true;
+    }
+    for (size_t i = 0; i < ops.size(); ++i) {
+      PyObject *o = or_none(ops[i].Get());
+      Py_INCREF(o);
+      PyList_SET_ITEM(ops_list, static_cast<Py_ssize_t>(i), o);
+    }
+    PyObject *py_result = PyObject_CallFunction(
+        method, "iN", static_cast<int>(sub), ops_list);
+    if (!py_result) {
+      capture_exception();
+      result = make_default();
+      return true;
+    }
+    if (py_result != Py_NotImplemented) {
+      result = SharedPyPtr(py_result);
+      Py_DECREF(py_result);
+      return true;
+    }
+    Py_DECREF(py_result);  // NotImplemented — fall through to concrete.
+  }
+
   std::vector<Value> concrete_ops;
   concrete_ops.reserve(ops.size());
   for (auto &op : ops) concrete_ops.push_back(python_to_value(op.Get()));
@@ -845,11 +877,13 @@ bool PythonPolicy::resolve_call(PythonScheduler &,
       capture_exception();
       return false;
     }
-    if (result != Py_NotImplemented && result != Py_None) {
-      // Any non-None / non-NotImplemented return is a skip with that
-      // value as the call's result. A `Skip(value)` instance is the
-      // disambiguator for "skip even though the value is None"; we
-      // unwrap it here. Anything else is taken as the value itself.
+    if (result != Py_NotImplemented) {
+      // Any non-NotImplemented return is a skip with that value as the
+      // call's result — `None` stubs the call to return `None`, an int
+      // / SymExpr / z3 expr is the replacement value, and `Skip(value)`
+      // is the typed marker analysts can still use (we unwrap it here).
+      // Only `NotImplemented` falls through to inlining, matching the
+      // convention used by `mem_read` / `mem_write` and the pure ops.
       static PyObject *cls_Skip = nullptr;
       if (!cls_Skip) {
         PyObject *mod = PyImport_ImportModule("multiplier.symex.events");

bindings/Python/SymbolicInterpreter.h

@@ -366,6 +366,7 @@ class PythonPolicy
   PyObject *cached_on_enter_block_{nullptr};
   PyObject *cached_on_instruction_{nullptr};
   PyObject *cached_on_global_initialized_{nullptr};
+  PyObject *cached_mem_bulk_op_{nullptr};
 
   // Pending exception state. Captured when a Python hook raises so the
   // interpreter loop can exit cleanly and SymbolicStep can re-raise it.

bindings/Python/symex/ctx.py

@@ -11,10 +11,12 @@
 lens, args lens (for call events), layout, and solver.
 
 Hooks compose by calling `next_hook(...)` to forward to the rest of
-the chain. To short-circuit with the substrate's natural default
-(e.g., "let the call return None / 0 instead of inlining"), use
-`ctx.default()`. To stop the entire path cleanly, call
-`ctx.stop_path()` and then return `ctx.default()` (or any value).
+the chain. To short-circuit a call hook with `None` as the return
+value (the common "stub this function" case), just `return None`.
+`ctx.default()` is the typed equivalent. To fall through to the
+substrate's own resolver (e.g., let an IR function inline), return
+`NotImplemented`. To stop the entire path cleanly, call
+`ctx.stop_path()` and then return any value.
 """
 
 from .events import Terminal, StopNow
@@ -37,13 +39,12 @@ def __init__(self, *, path, mem, args=None, layout=None, solver=None):
         self.solver = solver
 
     def default(self):
-        """The substrate's "natural default" for the current event,
-        wrapped in `Skip` so the substrate treats it as an explicit
-        skip-with-this-value rather than a fall-through.
+        """The substrate's "natural default" for the current event.
 
-        Phase 2 uses `None` as the default value for every event;
-        per-event typed defaults (e.g., width-correct zero for
-        memory reads) can land later if a use-case demands it.
+        Equivalent to `return None` from a call handler — the call is
+        skipped with `None` as the return value. Returns `Skip()` (a
+        typed marker the substrate unwraps) so this is also safe in
+        any future hook surface that might re-disambiguate `None`.
         """
         from .events import Skip
         return Skip()