hevm-0.50.1: Ethereum virtual machine evaluator
Safe HaskellSafe-Inferred
LanguageGHC2021

EVM

Synopsis

Data types

data VMResult Source #

The possible result states of a VM

Constructors

VMFailure Error

An operation failed

VMSuccess (Expr Buf)

Reached STOP, RETURN, or end-of-code

Instances

Instances details
Show VMResult Source # 
Instance details

Defined in EVM

data VM Source #

The state of a stepwise EVM execution

Instances

Instances details
Show VM Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> VM -> ShowS #

show :: VM -> String #

showList :: [VM] -> ShowS #

data Trace Source #

Instances

Instances details
Show Trace Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Trace -> ShowS #

show :: Trace -> String #

showList :: [Trace] -> ShowS #

data Query where Source #

Queries halt execution until resolved through RPC calls or SMT queries

Constructors

PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query 
PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM ()) -> Query 
PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query 
PleaseDoFFI :: [String] -> (ByteString -> EVM ()) -> Query 

Instances

Instances details
Show Query Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Query -> ShowS #

show :: Query -> String #

showList :: [Query] -> ShowS #

data Choose where Source #

Constructors

PleaseChoosePath :: Expr EWord -> (Bool -> EVM ()) -> Choose 

Instances

Instances details
Show Choose Source # 
Instance details

Defined in EVM

type EVM a = State VM a Source #

Alias for the type of e.g. exec1.

data BranchCondition Source #

The possible return values of a SMT query

Constructors

Case Bool 
Unknown 
Inconsistent 

Instances

Instances details
Show BranchCondition Source # 
Instance details

Defined in EVM

data IsUnique a Source #

The possible return values of a `is unique` SMT query

Instances

Instances details
Show a => Show (IsUnique a) Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> IsUnique a -> ShowS #

show :: IsUnique a -> String #

showList :: [IsUnique a] -> ShowS #

data Cache Source #

The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.

Instances

Instances details
Monoid Cache Source # 
Instance details

Defined in EVM

Methods

mempty :: Cache #

mappend :: Cache -> Cache -> Cache #

mconcat :: [Cache] -> Cache #

Semigroup Cache Source # 
Instance details

Defined in EVM

Methods

(<>) :: Cache -> Cache -> Cache #

sconcat :: NonEmpty Cache -> Cache #

stimes :: Integral b => b -> Cache -> Cache #

Show Cache Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Cache -> ShowS #

show :: Cache -> String #

showList :: [Cache] -> ShowS #

data StorageBase Source #

Constructors

Concrete 
Symbolic 

Instances

Instances details
Show StorageBase Source # 
Instance details

Defined in EVM

Eq StorageBase Source # 
Instance details

Defined in EVM

data Frame Source #

An entry in the VM's "call/create stack"

Instances

Instances details
Show Frame Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Frame -> ShowS #

show :: Frame -> String #

showList :: [Frame] -> ShowS #

data FrameState Source #

The "registers" of the VM along with memory and data stack

Instances

Instances details
Show FrameState Source # 
Instance details

Defined in EVM

data TxState Source #

The state that spans a whole transaction

Instances

Instances details
Show TxState Source # 
Instance details

Defined in EVM

data SubState Source #

The "accrued substate" across a transaction

Instances

Instances details
Show SubState Source # 
Instance details

Defined in EVM

data ContractCode Source #

A contract is either in creation (running its "constructor") or post-creation, and code in these two modes is treated differently by instructions like EXTCODEHASH, so we distinguish these two code types.

The definition follows the structure of code output by solc. We need to use some heuristics here to deal with symbolic data regions that may be present in the bytecode since the fully abstract case is impractical:

  • initcode has concrete code, followed by an abstract data "section"
  • runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)

hopefully we do not have to deal with dynamic immutable before we get a real data section...

Constructors

InitCode ByteString (Expr Buf)

Constructor code, during contract creation

RuntimeCode RuntimeCode

Instance code, after contract creation

data RuntimeCode Source #

We have two variants here to optimize the fully concrete case. ConcreteRuntimeCode just wraps a ByteString SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).

Instances

Instances details
Show RuntimeCode Source # 
Instance details

Defined in EVM

Eq RuntimeCode Source # 
Instance details

Defined in EVM

Ord RuntimeCode Source # 
Instance details

Defined in EVM

data Contract Source #

A contract can either have concrete or symbolic storage depending on what type of execution we are doing data Storage = Concrete (Map Word Expr EWord) | Symbolic [(Expr EWord, Expr EWord)] (SArray (WordN 256) (WordN 256)) deriving (Show)

The state of a contract

Instances

Instances details
Show Contract Source # 
Instance details

Defined in EVM

data StorageModel Source #

When doing symbolic execution, we have three different ways to model the storage of contracts. This determines not only the initial contract storage model but also how RPC or state fetched contracts will be modeled.

Constructors

ConcreteS

Uses Concrete Storage. Reading / Writing from abstract locations causes a runtime failure. Can be nicely combined with RPC.

SymbolicS

Uses Symbolic Storage. Reading / Writing never reaches RPC, but always done using an SMT array with no default value.

InitialS

Uses Symbolic Storage. Reading / Writing never reaches RPC, but always done using an SMT array with 0 as the default value.

data Env Source #

Various environmental data

Instances

Instances details
Show Env Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Env -> ShowS #

show :: Env -> String #

showList :: [Env] -> ShowS #

data Block Source #

Data about the block

Instances

Instances details
Show Block Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Block -> ShowS #

show :: Block -> String #

showList :: [Block] -> ShowS #

bytecode :: Getter Contract (Expr Buf) Source #

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

Data accessors

Data constructors

initialContract :: ContractCode -> Contract Source #

Initialize empty contract with given code

Opcode dispatch (exec1)

next :: (?op :: Word8) => EVM () Source #

Update program counter

exec1 :: EVM () Source #

Executes the EVM one step

transfer :: Addr -> Addr -> W256 -> EVM () Source #

callChecks :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Word64 -> EVM ()) -> EVM () Source #

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

precompiledContract :: (?op :: Word8) => Contract -> Word64 -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM () Source #

executePrecompile :: (?op :: Word8) => Addr -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> EVM () Source #

Opcode helper actions

noop :: Monad m => m () Source #

pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m () Source #

pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m () Source #

branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM () Source #

fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM () Source #

Construct RPC Query and halt execution until resolved

accessStorage Source #

Arguments

:: Addr

Contract address

-> Expr EWord

Storage slot key

-> (Expr EWord -> EVM ())

Continuation

-> EVM () 

How to finalize a transaction

loadContract :: Addr -> EVM () Source #

Loads the selected contract as the current contract to execute

limitStack :: Int -> EVM () -> EVM () Source #

notStatic :: EVM () -> EVM () Source #

burn :: Word64 -> EVM () -> EVM () Source #

Burn gas, failing if insufficient gas is available

forceConcrete :: Expr EWord -> String -> (W256 -> EVM ()) -> EVM () Source #

forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM () Source #

Substate manipulation

accessAndBurn :: Addr -> EVM () -> EVM () Source #

accessAccountForGas :: Addr -> EVM Bool Source #

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 :: Addr -> Expr EWord -> EVM Bool Source #

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

cheat :: (?op :: Word8) => (W256, W256) -> (W256, W256) -> EVM () Source #

ethsign :: PrivateKey -> Digest Keccak_256 -> Signature Source #

We don't wanna introduce the machinery needed to sign with a random nonce, so we just use the same nonce every time (420). This is obviusly very insecure, but fine for testing purposes.

General call implementation ("delegateCall")

delegateCall :: (?op :: Word8) => Contract -> Word64 -> Expr EWord -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord] -> (Addr -> EVM ()) -> EVM () Source #

create :: (?op :: Word8) => Addr -> Contract -> Word64 -> W256 -> [Expr EWord] -> Addr -> Expr Buf -> EVM () Source #

replaceCode :: Addr -> ContractCode -> EVM () Source #

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

VM error implementation

data FrameResult Source #

A stack frame can be popped in three ways.

Constructors

FrameReturned (Expr Buf)

STOP, RETURN, or no more code

FrameReverted (Expr Buf)

REVERT

FrameErrored Error

Any other error

Instances

Instances details
Show FrameResult Source # 
Instance details

Defined in EVM

finishFrame :: FrameResult -> EVM () Source #

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

Tracing

Stack manipulation

push :: W256 -> EVM () Source #

stackOp1 :: (?op :: Word8) => (Expr EWord -> Word64) -> (Expr EWord -> Expr EWord) -> EVM () Source #

stackOp2 :: (?op :: Word8) => ((Expr EWord, Expr EWord) -> Word64) -> ((Expr EWord, Expr EWord) -> Expr EWord) -> EVM () Source #

Bytecode data functions

readOp :: Word8 -> [Expr Byte] -> Op Source #

Reads

Gas cost calculation helpers

Arithmetic

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

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

log2 :: FiniteBits b => b -> Int Source #

opslen :: ContractCode -> Int Source #

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

codelen :: ContractCode -> Expr EWord Source #

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

Emacs setup