Modules
Structs
Identifies a sequential block of instructions within the original
bytecode sequence. That is, a sequence does not contain a jump
destination (other than at the very start), and ends either with a
terminating instruction (e.g.
RETURN
, REVERT
, etc) or an
unconditional branch (to another block).A concrete stack implementation backed by a
Vec
.Identifies all contiguous code blocks within the bytecode program.
Here, a block is a sequence of bytecodes terminated by either
STOP
, REVERT
, RETURN
or JUMP
. Observe that a JUMPDEST
can only appear as the first instruction of a block. In fact,
every reachable block (except the root block) begins with a
JUMPDEST
.Represents an EVM of some form. This could be a concrete EVM (i.e. useful for actually
executing bytecodes), or an abstract EVM (i.e. useful for some kind of dataflow analysis).
Enums
Traits
Represents an EVM stack of some form. This could a concrete
stack (i.e. useful for execution) or an abstract stack
(i.e. useful for analysis).
A stepper is a trait for describing a single execution step of the
EVM. This is subtle because it can be abstract or concrete.
Represents the fundamental unit of computation within the EVM,
namely a word. This is intentially left abstract, so that it
could be reused across both concrete and abstract semantics.