EVM

Documentation

blankState :: VMOps t => ST s (FrameState t s)

bytecode :: Getter Contract (Maybe (Expr Buf))

An "external" view of a contract's bytecode, appropriate for e.g. EXTCODEHASH.

Data accessors

currentContract :: VM t s -> Maybe Contract

Data constructors

makeVm :: VMOps t => VMOpts t -> ST s (VM t s)

unknownContract :: Expr EAddr -> Contract

Initialize an abstract contract with unknown code

abstractContract :: ContractCode -> Expr EAddr -> Contract

Initialize an abstract contract with known code

emptyContract :: Contract

Initialize an empty contract without code

initialContract :: ContractCode -> Contract

Initialize empty contract with given code

isCreation :: ContractCode -> Bool

Opcode dispatch (exec1)

next :: (?op :: Word8) => EVM t s ()

Update program counter

exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()

Executes the EVM one step

transfer :: VMOps t => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()

callChecks :: forall (t :: VMType) s. (?op :: Word8, VMOps t) => Contract -> Gas t -> Expr EAddr -> Expr EAddr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> (Gas t -> EVM t s ()) -> EVM t s ()

Checks a *CALL for failure; OOG, too many callframes, memory access etc.

precompiledContract :: (?op :: Word8, VMOps t) => Contract -> Gas t -> Addr -> Addr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> EVM t s ()

executePrecompile :: (?op :: Word8, VMOps t) => Addr -> Gas t -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> EVM t s ()

truncpadlit :: Int -> ByteString -> ByteString

lazySlice :: W256 -> W256 -> ByteString -> ByteString

parseModexpLength :: ByteString -> (W256, W256, W256)

isZero :: W256 -> W256 -> ByteString -> Bool

asInteger :: ByteString -> Integer

Opcode helper actions

noop :: Monad m => m ()

pushTo :: MonadState s m => Lens s s [a] [a] -> a -> m ()

pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()

getCodeLocation :: VM t s -> CodeLocation

query :: Query t s -> EVM t s ()

choose :: Choose s -> EVM Symbolic s ()

fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()

Construct RPC Query and halt execution until resolved

accessStorage :: VMOps t => Expr EAddr -> Expr EWord -> (Expr EWord -> EVM t s ()) -> EVM t s ()

accountExists :: Expr EAddr -> VM t s -> Bool

accountEmpty :: Contract -> Bool

How to finalize a transaction

finalize :: VMOps t => EVM t s ()

loadContract :: Expr EAddr -> State (VM t s) ()

Loads the selected contract as the current contract to execute

limitStack :: VMOps t => Int -> EVM (t :: VMType) s () -> EVM t s ()

notStatic :: VMOps t => EVM t s () -> EVM t s ()

forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()

forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()

forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()

forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()

forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()

forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()

Substate manipulation

refund :: Word64 -> EVM t s ()

unRefund :: Word64 -> EVM t s ()

touchAccount :: Expr EAddr -> EVM t s ()

selfdestruct :: Expr EAddr -> EVM t s ()

accessAndBurn :: VMOps t => Expr EAddr -> EVM t s () -> EVM t s ()

accessAccountForGas :: Expr EAddr -> EVM t s Bool

returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold

accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool

returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929) otherwise cold

Cheat codes

cheatCode :: Expr EAddr

cheat :: (?op :: Word8, VMOps t) => (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> EVM t s ()

type CheatAction t s = Expr EWord -> Expr EWord -> Expr Buf -> EVM t s ()

cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)

General call implementation ("delegateCall")

delegateCall :: (VMOps t, ?op :: Word8) => Contract -> Gas t -> Expr EAddr -> Expr EAddr -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord] -> (Expr EAddr -> EVM t s ()) -> EVM t s ()

collision :: Maybe Contract -> Bool

create :: forall t s. (?op :: Word8, VMOps t) => Expr EAddr -> Contract -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s ()

parseInitCode :: Expr Buf -> Maybe ContractCode

Parses a raw Buf into an InitCode

solidity implements constructor args by appending them to the end of the initcode. we support this internally by treating initCode as a concrete region (initCode) followed by a potentially symbolic region (arguments).

when constructing a contract that has symbolic constructor args, we need to apply some heuristics to convert the (unstructured) initcode in memory into this structured representation. The (unsound, bad, hacky) way that we do this, is by: looking for the first potentially symbolic byte in the input buffer and then splitting it there into code / data.

replaceCode :: Expr EAddr -> ContractCode -> EVM t s ()

Replace a contract's code, like when CREATE returns from the constructor code.

replaceCodeOfSelf :: ContractCode -> EVM t s ()

resetState :: VMOps t => EVM t s ()

VM error implementation

vmError :: VMOps t => EvmError -> EVM t s ()

wrap :: Typeable a => [Expr a] -> [SomeExpr]

underrun :: VMOps t => EVM t s ()

data FrameResult

A stack frame can be popped in three ways.

Constructors

FrameReturned (Expr Buf)

STOP, RETURN, or no more code

FrameReverted (Expr Buf)

REVERT

FrameErrored EvmError

Any other error

Instances

Show FrameResult

Defined in EVM

Methods

showsPrec :: Int -> FrameResult -> ShowS

show :: FrameResult -> String

showList :: [FrameResult] -> ShowS

finishFrame :: VMOps t => FrameResult -> EVM t s ()

This function defines how to pop the current stack frame in either of the ways specified by FrameResult.

It also handles the case when the current stack frame is the only one; in this case, we set the final _result of the VM execution.

Memory helpers

accessUnboundedMemoryRange :: VMOps t => Word64 -> Word64 -> EVM t s () -> EVM t s ()

accessMemoryRange :: VMOps t => Expr EWord -> Expr EWord -> EVM t s () -> EVM t s ()

accessMemoryWord :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()

copyBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM t s ()

copyCallBytesToMemory :: Expr Buf -> Expr EWord -> Expr EWord -> EVM t s ()

readMemory :: Expr EWord -> Expr EWord -> EVM t s (Expr Buf)

Tracing

withTraceLocation :: TraceData -> EVM t s Trace

pushTrace :: TraceData -> EVM t s ()

insertTrace :: TraceData -> EVM t s ()

popTrace :: EVM t s ()

zipperRootForest :: TreePos Empty a -> Forest a

traceForest :: VM t s -> Forest Trace

traceForest' :: Expr End -> Forest Trace

traceContext :: Expr End -> Map (Expr EAddr) Contract

traceTopLog :: [Expr Log] -> EVM t s ()

Stack manipulation

push :: W256 -> EVM t s ()

pushSym :: Expr EWord -> EVM t s ()

pushAddr :: Expr EAddr -> EVM t s ()

stackOp1 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord) -> EVM t s ()

stackOp2 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord -> Expr EWord) -> EVM t s ()

stackOp3 :: (?op :: Word8, VMOps t) => Word64 -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> EVM t s ()

Bytecode data functions

checkJump :: VMOps t => Int -> [Expr EWord] -> EVM t s ()

noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t s ()

isValidJumpDest :: VM t s -> Int -> Bool

opSize :: Word8 -> Int

mkOpIxMap :: ContractCode -> Vector Int

vmOp :: VM t s -> Maybe Op

vmOpIx :: VM t s -> Maybe Int

mkCodeOps :: ContractCode -> Vector (Int, Op)

Gas cost calculation helpers

concreteModexpGasFee :: ByteString -> Word64

costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64

memoryCost :: FeeSchedule Word64 -> Word64 -> Word64

hashcode :: ContractCode -> Expr EWord

opslen :: ContractCode -> Int

The length of the code ignoring any constructor args. This represents the region that can contain executable opcodes

codelen :: ContractCode -> Expr EWord

The length of the code including any constructor args. This can return an abstract value

toBuf :: ContractCode -> Maybe (Expr Buf)

codeloc :: EVM t s CodeLocation

createAddress :: Expr EAddr -> Maybe W64 -> EVM t s (Expr EAddr)

create2Address :: Expr EAddr -> W256 -> ByteString -> EVM t s (Expr EAddr)

freshSymAddr :: EVM t s (Expr EAddr)

isPrecompileAddr :: Expr EAddr -> Bool

Arithmetic

ceilDiv :: (Num a, Integral a) => a -> a -> a

allButOne64th :: (Num a, Integral a) => a -> a

log2 :: FiniteBits b => b -> Int

writeMemory :: MutableMemory s -> Int -> ByteString -> EVM t s ()

freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)

symbolify :: VM Concrete s -> VM Symbolic s

symbolifyFrameState :: FrameState Concrete s -> FrameState Symbolic s

symbolifyFrame :: Frame Concrete s -> Frame Symbolic s

symbolifyResult :: VMResult Concrete s -> VMResult Symbolic s

forceLit :: Expr EWord -> W256

burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()

Orphan instances

VMOps 'Concrete

Methods

burn' :: Gas 'Concrete -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnExp :: Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnSha3 :: Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnCalldatacopy :: Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnCodecopy :: Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnExtcodecopy :: Expr 'EAddr -> Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnReturndatacopy :: Expr 'EWord -> EVM 'Concrete s () -> EVM 'Concrete s ()

burnLog :: Expr 'EWord -> Word8 -> EVM 'Concrete s () -> EVM 'Concrete s ()

initialGas :: Gas 'Concrete

ensureGas :: Word64 -> EVM 'Concrete s () -> EVM 'Concrete s ()

gasTryFrom :: Expr 'EWord -> Either () (Gas 'Concrete)

costOfCreate :: FeeSchedule Word64 -> Gas 'Concrete -> Expr 'EWord -> Bool -> (Gas 'Concrete, Gas 'Concrete)

costOfCall :: FeeSchedule Word64 -> Bool -> Expr 'EWord -> Gas 'Concrete -> Gas 'Concrete -> Expr 'EAddr -> (Word64 -> Word64 -> EVM 'Concrete s ()) -> EVM 'Concrete s ()

reclaimRemainingGasAllowance :: VM 'Concrete s -> EVM 'Concrete s ()

payRefunds :: EVM 'Concrete s ()

pushGas :: EVM 'Concrete s ()

enoughGas :: Word64 -> Gas 'Concrete -> Bool

subGas :: Gas 'Concrete -> Word64 -> Gas 'Concrete

toGas :: Word64 -> Gas 'Concrete

whenSymbolicElse :: EVM 'Concrete s a -> EVM 'Concrete s a -> EVM 'Concrete s a

partial :: PartialExec -> EVM 'Concrete s ()

branch :: Expr 'EWord -> (Bool -> EVM 'Concrete s ()) -> EVM 'Concrete s ()

VMOps 'Symbolic

Methods

burn' :: Gas 'Symbolic -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnExp :: Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnSha3 :: Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnCalldatacopy :: Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnCodecopy :: Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnExtcodecopy :: Expr 'EAddr -> Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnReturndatacopy :: Expr 'EWord -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

burnLog :: Expr 'EWord -> Word8 -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

initialGas :: Gas 'Symbolic

ensureGas :: Word64 -> EVM 'Symbolic s () -> EVM 'Symbolic s ()

gasTryFrom :: Expr 'EWord -> Either () (Gas 'Symbolic)

costOfCreate :: FeeSchedule Word64 -> Gas 'Symbolic -> Expr 'EWord -> Bool -> (Gas 'Symbolic, Gas 'Symbolic)

costOfCall :: FeeSchedule Word64 -> Bool -> Expr 'EWord -> Gas 'Symbolic -> Gas 'Symbolic -> Expr 'EAddr -> (Word64 -> Word64 -> EVM 'Symbolic s ()) -> EVM 'Symbolic s ()

reclaimRemainingGasAllowance :: VM 'Symbolic s -> EVM 'Symbolic s ()

payRefunds :: EVM 'Symbolic s ()

pushGas :: EVM 'Symbolic s ()

enoughGas :: Word64 -> Gas 'Symbolic -> Bool

subGas :: Gas 'Symbolic -> Word64 -> Gas 'Symbolic

toGas :: Word64 -> Gas 'Symbolic

whenSymbolicElse :: EVM 'Symbolic s a -> EVM 'Symbolic s a -> EVM 'Symbolic s a

partial :: PartialExec -> EVM 'Symbolic s ()

branch :: Expr 'EWord -> (Bool -> EVM 'Symbolic s ()) -> EVM 'Symbolic s ()