Skip to content

feat(vm): build contextual stack SSA - #751

Open
Jon-Becker wants to merge 1 commit into
feat/canonical-instruction-effectsfrom
feat/contextual-stack-ssa
Open

feat(vm): build contextual stack SSA#751
Jon-Becker wants to merge 1 commit into
feat/canonical-instruction-effectsfrom
feat/contextual-stack-ssa

Conversation

@Jon-Becker

Copy link
Copy Markdown
Owner

What changed? Why?

Adds deterministic context-sensitive stack SSA over canonical CFG states and lowers the explicit effects from #750 onto stable SSA operands.

The new core::ssa module provides:

  • a stable SSA value arena for concrete, symbolic, mixed, and unknown abstract values;
  • contextual blocks keyed by the full shrinking continuation context;
  • predecessor-qualified phi nodes for joined entry-stack slots;
  • explicit entry seeds so loop headers do not lose their initial definitions;
  • SSA operands and outputs for canonical instruction effects; and
  • retained before/after memory, storage, and transient-storage roots.

This is an analysis artifact only. Production Solidity/Yul generation remains on the legacy backend until graph structuring and typed lowering are validated.

This PR is stacked on #750.

Notes to reviewers

  • Phi construction uses contextual predecessors, not flattened canonical block IDs.
  • Equal abstract atoms are interned globally; actual predecessor disagreement creates a block-local phi result.
  • Multiple edge labels from the same contextual predecessor are deduplicated because they provide the same post-terminator stack definition.
  • ContextualCfg::initial_states retains pre-fixpoint root seeds separately from joined entry states.
  • Incoming edges are indexed once. This reduced Seaport SSA construction from an initial O(points × edges) 4.76s implementation to 103ms.
  • This is stack/effect SSA groundwork, not yet complete memory SSA source lowering or structured control-flow recovery.

How has it been tested?

  • cargo test -p heimdall-vm --lib — 204 passed
  • cargo test -p heimdall-vm --features smt --lib — 210 passed
  • cargo check --workspace --all-targets — passed
  • cargo +nightly fmt --all -- --check — passed
  • git diff --check — passed
  • Added diamond-CFG regression coverage proving predecessor-qualified phi creation and effect-lowering coverage proving SSA operands preserve state-version transitions.
  • Production SSA measurements:
    • USDT: 399 contextual blocks, 56 phis, 292 effects, 1ms
    • Uniswap V2: 466 blocks, 194 phis, 413 effects, 1ms
    • Uniswap V3 SwapRouter: 1,080 blocks, 166 phis, 788 effects, 8ms
    • Seaport: 9,707 blocks, 2,468 phis, 7,349 effects, 103ms

@github-actions

github-actions Bot commented Sep 6, 2026

Copy link
Copy Markdown
Contributor

❌ AI Evaluation Suite for 88ce5ea

Completed heimdall-eval. View workflow run.

Test Case CFG Decompilation
NestedLoop 100 20
SimpleStorage 100 95
NestedMappings 100 45
SimpleLoop 100 25
WhileLoop 100 25
NestedMapping 100 8
Mapping 100 95
TransientStorage 100 15
WETH9 100 95
Events 100 63
Average 100 48
⚠️ 7 eval(s) scoring <70%

NestedLoop (CFG: 100, Decompilation: 20)

Decompilation

{
  "score": 20,
  "summary": "The public getter for the storage variable is correctly recovered, but the contract's only real logic — the nested loop that repeatedly increments storage slot 0 — is entirely lost. loop(uint256) is decompiled as an unconditional revert(), so neither the loop control flow, the arithmetic, nor the state write is represented. The function is also marked view despite mutating state.",
  "differences": [
    "loop(uint256) body is replaced with an unconditional revert(); the original executes and returns normally for any input (including loops == 0)",
    "Both the outer and inner for-loops (i < loops, j < loops) and their counter increments are completely absent — no loop control flow was recovered",
    "The state mutation `number += 1` (SSTORE to slot 0, executed loops*loops times) is missing; the decompiled contract never writes storage",
    "loop(uint256) is annotated as `public view` though the original is state-mutating, so mutability behavior is misrepresented",
    "The storage variable is typed as bytes32 in the loop-related logic path; irrelevant to the getter but the increment arithmetic on it is entirely gone"
  ]
}

NestedMappings (CFG: 100, Decompilation: 45)

Decompilation

{
  "score": 45,
  "summary": "The state-mutating function (approve) is decompiled correctly, including the two-level nested mapping write at slot 0 keyed by msg.sender and the spender argument. However, both read paths (the explicit allowance(address,address) getter at 0xdd62ed3e and the auto-generated public mapping getter allowances(address,address) at 0x55b6ed5c) are emitted as empty bodies: they show only calldata-length checks, perform no nested mapping storage read, take only one of the two address arguments, and declare no return value. Two of the three externally reachable functions therefore lose their entire logic, so the decompilation captures the write side of the contract but not the read side.",
  "differences": [
    "Unresolved_dd62ed3e (allowance) does not read storage and returns nothing; the original returns allowances[owner][spender], so the nested keccak slot computation and SLOAD are entirely missing",
    "Unresolved_55b6ed5c (public allowances getter) likewise has an empty body with no storage read and no return value",
    "Both getters are decompiled with a single address parameter instead of two, dropping the second mapping key from the signature",
    "Both getters are marked 'pure' although they read contract storage (original is 'view')",
    "approve is marked 'payable' whereas the original is non-payable and the bytecode contains a callvalue check (the check is reduced to 'require(true)')"
  ]
}

SimpleLoop (CFG: 100, Decompilation: 25)

Decompilation

{
  "score": 25,
  "summary": "The public getter for the storage variable is correctly recovered, but the contract's only real logic — the counting loop in loop(uint256) — is entirely lost and replaced with an unconditional revert(). No loop, no comparison against the argument, and no storage increment appear anywhere in the output, so the decompilation fails to capture the contract's primary behavior.",
  "differences": [
    "loop(uint256) is decompiled as an unconditional revert(); the original executes a bounded for-loop and returns normally.",
    "The loop control flow (i = 0; i < loops; i++) is missing — no comparison against arg0, no induction variable, no back-edge/branch structure.",
    "The state change 'number++' (SLOAD/ADD/SSTORE on slot 0) is missing; loop() is marked 'view' and performs no storage write, whereas the original is state-mutating.",
    "Mutability is misreported: loop(uint256) is non-payable and modifies state in the original, but is annotated 'view' with no side effects in the decompiled output."
  ]
}

WhileLoop (CFG: 100, Decompilation: 25)

Decompilation

{
  "score": 25,
  "summary": "The public getter for the storage variable is correctly recovered, but the contract's only real logic — the while loop that increments the stored counter `loops` times — is entirely absent. `loop(uint256)` is rendered as an unconditional `revert()`, so no loop, no comparison, no storage read/modify/write is preserved. Roughly half the ABI surface is right, but the functional core of the contract is lost.",
  "differences": [
    "loop(uint256) is decompiled as an unconditional revert(); the original never reverts for any input (it simply does nothing when loops == 0).",
    "The while (i < loops) loop and its induction variable / bound comparison are completely missing from the output.",
    "The storage write `number = number + 1` (SLOAD, ADD, SSTORE on slot 0x00) inside the loop body is not represented at all.",
    "loop(uint256) is annotated `view`, but the original mutates state (non-payable, state-changing); the recovered mutability is wrong.",
    "The dependency of the number of state increments on the argument arg0 is lost, so the post-call value of `number` is not reproducible from the decompiled code."
  ]
}

NestedMapping (CFG: 100, Decompilation: 8)

Decompilation

{
  "score": 8,
  "summary": "The decompilation recovers the correct number of external entry points (7 selectors, matching the 3 setters, 1 getter, and 3 public mapping getters), but essentially none of the functional behavior. Every recovered function body is either a bare revert() or a calldata-length check followed by require(true). No keccak256 nested-mapping slot derivation, no SSTORE for any of the three setters, no SLOAD/return for any getter, and no return data at all. All functions are marked `pure`, contradicting the storage-mutating and storage-reading nature of the originals.",
  "differences": [
    "setAllowance: the SSTORE to allowances[owner][spender] and the two-level keccak256 slot computation are entirely absent; the corresponding function body is empty (require(true)) or reverts.",
    "setGrid: the SSTORE to grid[x][y] (including the bool packing/masking) is missing; body reverts.",
    "setDeepNested: the three-level keccak256 slot derivation and SSTORE to deepNested[a][b][c] are missing; body is empty.",
    "getAllowance: no SLOAD and no return value; the function returns nothing instead of the stored uint256.",
    "The three auto-generated public mapping getters (allowances, grid, deepNested) are reduced to reverts or no-ops, losing their storage reads and returns.",
    "All arguments are truncated: functions taking 3-4 parameters are shown with only 1-2, so parameter usage in slot computation is lost.",
    "Mutability is wrong: storage-writing functions are annotated `pure`, and view getters are annotated `pure` with no state access.",
    "Several functions are represented as unconditional revert(), which would make the contract non-functional if this were the actual behavior."
  ]
}

TransientStorage (CFG: 100, Decompilation: 15)

Decompilation

{
  "score": 15,
  "summary": "Only one of six functions (setTempOwner) retains any recognizable logic, and even that is rendered as a masked read-modify-write with an inverted mask. The remaining five functions (incrementCounter, lock, unlock, getCounter, isLocked) are collapsed into meaningless constant declarations with no transient load/store operations, no increment arithmetic, and no return of actual state. The decompilation fails to capture transient storage (TLOAD/TSTORE) semantics almost entirely.",
  "differences": [
    "incrementCounter is emitted as an empty 'bytes public constant' with no body: the counter read, +1 arithmetic, and store back are all missing",
    "lock() is emitted as an empty constant; the write of true to the locked flag is missing",
    "unlock() is emitted as an empty constant; the write of false to the locked flag is missing",
    "getCounter is represented as 'uint256 public constant getCounter = 1' instead of loading and returning the counter value; it returns a hardcoded 1 rather than state",
    "isLocked is represented as a constant 'true' instead of loading and returning the locked flag; it never reads state and cannot return false",
    "setTempOwner is marked 'pure' despite performing a state (transient) write",
    "In setTempOwner the mask is applied incorrectly: 'arg0 | 0xffff...ff000...0 & tstore_a' preserves the high 96 bits of the prior slot value and does not mask arg0 to 160 bits, whereas the source assigns the address outright",
    "setTempOwner includes a spurious calldata-length guard ('require(... >= 0x20)') and a 'require(true)' that do not correspond to any source-level condition",
    "The distinction between transient storage and persistent storage is not consistently modeled; declared members (tstore_a, tstore_b) have 'unknown' slots and tstore_b is never used, while the counter and locked variables have no storage representation at all"
  ]
}

Events (CFG: 100, Decompilation: 63)

Decompilation

{
  "score": 63,
  "summary": "Five of the seven functions are recovered faithfully: emitDeposit, emitWithdrawal, emitLog, emitLogBytes and emitMultiple all show the correct event emissions, including the multi-emit sequence with Transfer(address(0), account, amount) and the inline string literal \"Multiple events emitted\", plus the correct calldata bounds checks for the dynamic string/bytes arguments. However, the two three-parameter functions (emitTransfer and emitApproval) are decompiled as bodies containing only calldata-length checks with no LOG instruction at all, so the sole behavior of those functions is lost, and the Approval event is absent from the reconstructed event list. Argument recovery for those two functions is also truncated to a single address parameter despite the 0x60 calldata-size check.",
  "differences": [
    "Function 0x5687f2b8 (a 3-argument function corresponding to emitTransfer/emitApproval) emits no event; its entire body is reduced to require checks, losing the LOG3 emission that is the function's only purpose.",
    "Function 0x23de6651 (the other 3-argument function corresponding to emitApproval/emitTransfer) likewise emits no event, losing the indexed-topic emission entirely.",
    "The Approval event is missing from the decompiled event declarations, consistent with the dropped emission.",
    "The two 3-argument functions are given only one recovered parameter (address arg0) instead of three, so the indexed address and the uint256 value arguments are not represented even though the 0x60 minimum-calldata check implies them.",
    "Indexed vs. non-indexed topic structure is not represented anywhere: emitted events show flat parameter lists, so which arguments become topics vs. data is not recoverable from the output.",
    "All functions are annotated `pure` despite emitting logs (state-mutability classification is wrong for every function that contains a LOG)."
  ]
}
  • Run AI Evaluation Suite

@github-actions

github-actions Bot commented Sep 6, 2026

Copy link
Copy Markdown
Contributor

✅ Coverage Report for adf706c

Metric Value
Base branch 70.99%
PR branch 75.20%
Diff +4.21%

@Jon-Becker
Jon-Becker force-pushed the feat/contextual-stack-ssa branch from 88ce5ea to 3dcfb2f Compare September 6, 2026 21:41
@Jon-Becker
Jon-Becker force-pushed the feat/contextual-stack-ssa branch from 3dcfb2f to e7a3103 Compare September 6, 2026 23:40
@github-actions

github-actions Bot commented Sep 7, 2026

Copy link
Copy Markdown
Contributor

Benchmark for adf706c

Click to view benchmark
Test Base PR %
heimdall_cfg/complex 14.7±0.64ms 229.6±13.27ms +1461.90%
heimdall_cfg/simple 1402.7±64.80µs 635.5±16.94µs -54.69%
heimdall_decoder/seaport 56.8±2.65µs 56.2±2.14µs -1.06%
heimdall_decoder/transfer 4.4±0.33µs 4.2±0.30µs -4.55%
heimdall_decoder/uniswap 16.2±0.73µs 15.7±0.58µs -3.09%
heimdall_decompiler/abi_complex 59.4±0.95ms 289.1±14.74ms +386.70%
heimdall_decompiler/abi_simple 1509.1±47.65µs 2.1±0.01ms +39.16%
heimdall_decompiler/sol_complex 76.3±1.59ms 320.9±13.64ms +320.58%
heimdall_decompiler/sol_simple 1952.8±19.31µs 2.6±0.02ms +33.14%
heimdall_decompiler/yul_complex 65.8±1.94ms 296.9±9.83ms +351.22%
heimdall_decompiler/yul_simple 1702.3±15.66µs 2.3±0.14ms +35.11%
heimdall_disassembler/complex 1247.5±49.98µs 1612.7±85.85µs +29.27%
heimdall_disassembler/simple 62.2±7.36µs 74.9±4.49µs +20.42%
heimdall_vm/erc20_transfer 264.5±11.45µs 266.7±9.41µs +0.83%
heimdall_vm/fib 853.3±34.79µs 844.7±16.67µs -1.01%
heimdall_vm/ten_thousand_hashes 715.4±17.67ms 713.6±16.84ms -0.25%

📊 View the full Criterion report

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant