hevm-0.41.0: Ethereum virtual machine evaluator

Safe HaskellNone
LanguageHaskell2010

EVM

Contents

Synopsis

Data types

data VMResult Source #

The possible result states of a VM

Constructors

VMFailure Error

An operation failed

VMSuccess Buffer

Reached STOP, RETURN, or end-of-code

Instances
Show VMResult Source # 
Instance details

Defined in EVM

SDisplay VMResult Source # 
Instance details

Defined in EVM.Emacs

data VM Source #

The state of a stepwise EVM execution

Instances
SDisplay VM Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: VM -> SExpr Text Source #

data Trace Source #

Constructors

Trace 

data Query where Source #

Queries halt execution until resolved through RPC calls or SMT queries

Constructors

PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query 
PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query 
PleaseAskSMT :: SymWord -> [SBool] -> (JumpCondition -> EVM ()) -> Query 
Instances
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 :: (Bool -> EVM ()) -> Choose 
Instances
Show Choose Source # 
Instance details

Defined in EVM

type EVM a = State VM a Source #

Alias for the type of e.g. exec1.

data JumpCondition Source #

The possible return values of a SMT query regarding JUMPI

Instances
Show JumpCondition Source # 
Instance details

Defined in EVM

data Cache Source #

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

Constructors

Cache 
Instances
Show Cache Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Cache -> ShowS #

show :: Cache -> String #

showList :: [Cache] -> ShowS #

Semigroup Cache Source # 
Instance details

Defined in EVM

Methods

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

sconcat :: NonEmpty Cache -> Cache #

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

Monoid Cache Source # 
Instance details

Defined in EVM

Methods

mempty :: Cache #

mappend :: Cache -> Cache -> Cache #

mconcat :: [Cache] -> Cache #

data Log Source #

A log entry

Constructors

Log Addr Buffer [SymWord] 

data Frame Source #

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

Instances
SDisplay Frame Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Frame -> SExpr Text Source #

data FrameState Source #

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

Instances
SDisplay FrameState Source # 
Instance details

Defined in EVM.Emacs

data TxState Source #

The state that spans a whole transaction

data SubState Source #

The "accrued substate" across a transaction

Constructors

SubState 

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.

Constructors

InitCode ByteString

Constructor code, during contract creation

RuntimeCode ByteString

Instance code, after contract creation

Instances
Eq ContractCode Source # 
Instance details

Defined in EVM

Show ContractCode Source # 
Instance details

Defined in EVM

data Storage Source #

A contract can either have concrete or symbolic storage depending on what type of execution we are doing

Constructors

Concrete (Map Word SymWord) 
Symbolic (SArray (WordN 256) (WordN 256)) 
Instances
Eq Storage Source # 
Instance details

Defined in EVM

Methods

(==) :: Storage -> Storage -> Bool #

(/=) :: Storage -> Storage -> Bool #

Show Storage Source # 
Instance details

Defined in EVM

SDisplay Storage Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Storage -> SExpr Text Source #

data Contract Source #

The state of a contract

Instances
Eq Contract Source # 
Instance details

Defined in EVM

Show Contract Source # 
Instance details

Defined in EVM

SDisplay Contract Source # 
Instance details

Defined in EVM.Emacs

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 Storage Storage. Reading / Writing never reaches RPC, but always done using an SMT array with no default value.

InitialS

Uses Storage 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

data Block Source #

Data about the block

bytecode :: Getter Contract ByteString 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

callChecks :: (?op :: Word8) => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Word -> EVM ()) -> EVM () Source #

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

precompiledContract :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () Source #

executePrecompile :: (?op :: Word8) => Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> 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 #

askSMT :: CodeLocation -> SymWord -> (Bool -> EVM ()) -> EVM () Source #

Construct SMT Query and halt execution until resolved

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

Construct RPC Query and halt execution until resolved

accessStorage Source #

Arguments

:: Addr

Contract address

-> SymWord

Storage slot key

-> (SymWord -> 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 :: Word -> EVM () -> EVM () Source #

Burn gas, failing if insufficient gas is available

forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM () Source #

forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM () Source #

forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM () Source #

Substate manipulation

Cheat codes

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

General call implementation ("delegateCall")

delegateCall :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () -> EVM () Source #

create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> ByteString -> 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 Buffer

STOP, RETURN, or no more code

FrameReverted Buffer

REVERT

FrameErrored Error

Any other error

Instances
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

traceLog :: MonadState VM m => Log -> m () Source #

Stack manipulation

push :: Word -> EVM () Source #

stackOp1 :: (?op :: Word8) => (SymWord -> Word) -> (SymWord -> SymWord) -> EVM () Source #

stackOp2 :: (?op :: Word8) => ((SymWord, SymWord) -> Word) -> ((SymWord, SymWord) -> SymWord) -> EVM () Source #

stackOp3 :: (?op :: Word8) => ((SymWord, SymWord, SymWord) -> Word) -> ((SymWord, SymWord, SymWord) -> SymWord) -> EVM () Source #

Bytecode data functions

checkJump :: Integral n => n -> [SymWord] -> EVM () Source #

Gas cost calculation helpers

Uninterpreted functions

symkeccak' :: [SWord 8] -> SWord 256 Source #

Although we'd like to define this directly as an uninterpreted function, we cannot because [a] is not a symbolic type. We must convert the list into a suitable symbolic type first. The only important property of this conversion is that it is injective. We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.

symSHA256 :: [SWord 8] -> [SWord 8] Source #

Arithmetic

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

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

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

Emacs setup