analyzeGadgetEffect symbolically executes one gadget's raw P-Code (reusing the
pcode_encoder register-machine modeling) and reports a context-free transfer
function: each changed register's final source (stack-slot@offset / const /
register / sp-relative), the sp delta, memory writes, and the terminator. Z3 is
used only inside the executor to fold/identify sources — GadgetEffect holds no
z3::expr, so it crosses the fold_core/fold_ghidra boundary cleanly and the
analyzer is unit-testable on synthetic P-Code.
Inputs are seeded as recognizable Z3 consts (in_<off> registers, stk_<k> stack
slots loaded relative to the initial SP); classification simplifies each final
value and matches it back. Register offsets come from a GadgetRegModel resolved
by name at lift time (no hardcoded offsets in the analyzer).
This is the foundation for the Z3 chain planner (3b); not yet wired into chains,
so no finding behavior changes. Design references (not deps): Triton's
per-instruction symbolic state, angrop/ropper gadget controllability.
Unit: test_gadget_semantics — pop rdi;ret → rdi=stack[0], sp_delta 16; mov
rax,0x3b;syscall → rax=const, Syscall; pop rsi/pop rdx → stack[0]/stack[8],
sp_delta 24; mov [rdi],rsi → write-what-where reg→reg; bare ret → sp_delta 8
(22 assertions). meson test 78/78.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
