Module block_analysis 

Abstract stack interpretation for resolving dynamic jump targets and constant propagation.

This pass builds a basic-block CFG and runs worklist-based abstract interpretation to a fixpoint, propagating abstract stack states across blocks. It resolves jump targets that the block-local pass block_analysis_local (which interprets each block independently) cannot handle — including internal function return patterns where multiple callers push different return addresses.

After the fixpoint converges, the known-constant operands at each instruction are persisted as OperandSnapshots so that later passes (e.g. code generation) can query the known-constant value of stack operands.

Abstract domain

Per-value lattice (ascending order):

• Const(U256Imm) — a single known constant.
• ConstSet(ConstSetIdx) — multiple known constants (interned, sorted, deduplicated).
• Top — reachable but unknown.

Per-block lattice:

• Bottom — block not yet reached.
• Known(Vec<AbsValue>) — reached with a known stack state (top-aligned; when predecessors have different stack heights, the shorter stack is bottom-padded with Top).

Soundness

When the fixpoint does not converge (iteration cap reached) or unresolved Top jumps remain, a transitive predecessor analysis invalidates suspect resolutions that may be based on incomplete information, ensuring that only sound jump targets are reported as resolved.

Structs

Block 🔒

A block index in the CFG.

BlockData 🔒

A basic block in the CFG.

Cfg 🔒

CFG for abstract interpretation.

ConstSetIdx 🔒

Index into the interned constant-set pool.

ConstSetInterner 🔒

Constant-set interner used by the abstract interpreter.

Snapshots 🔒

Bundles input and output snapshots for recording during abstract interpretation.

Worklist 🔒

FIFO worklist with deduplication.

Enums

AbsValue 🔒

Abstract value on the stack.

BlockState 🔒

Abstract state at the entry of a block.

JumpTarget 🔒

Resolved jump target after fixpoint.

Constants

MAX_ABS_STACK_DEPTH 🔒

Maximum abstract stack depth tracked by the analysis. Top-aligned joins across paths with differing stack heights pad the shorter stack with Top at the bottom; on CFG cycles this padding can grow without bound. Clamping discards only those bottom Top entries, so no precision is lost.

Type Aliases

OperandSnapshot 🔒

Per-instruction snapshot of abstract operand values.