hevm-0.46.0: Ethereum virtual machine evaluator
Safe HaskellNone
LanguageHaskell2010

EVM

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

Instances details
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

Instances details
Show VM Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> VM -> ShowS #

show :: VM -> String #

showList :: [VM] -> ShowS #

SDisplay VM Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: VM -> SExpr Text Source #

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 -> StorageModel -> (Contract -> EVM ()) -> Query 
PleaseMakeUnique :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query 
PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query 
PleaseAskSMT :: SBool -> [SBool] -> (BranchCondition -> 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 :: Whiff -> (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.

Constructors

Cache 

Instances

Instances details
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] 

Instances

Instances details
Show Log Source # 
Instance details

Defined in EVM

Methods

showsPrec :: Int -> Log -> ShowS #

show :: Log -> String #

showList :: [Log] -> ShowS #

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 #

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

Instances details
Show FrameState Source # 
Instance details

Defined in EVM

SDisplay FrameState Source # 
Instance details

Defined in EVM.Emacs

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.

Constructors

InitCode Buffer

Constructor code, during contract creation

RuntimeCode Buffer

Instance code, after contract creation

Instances

Instances details
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 [(SymWord, SymWord)] (SArray (WordN 256) (WordN 256)) 

Instances

Instances details
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

Instances details
Show Contract Source # 
Instance details

Defined in EVM

FromJSON Contract Source # 
Instance details

Defined in EVM.VMTest

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

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

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

Ask the SMT solver to provide a concrete model for val iff a unique model exists

askSMT :: CodeLocation -> (SBool, Whiff) -> (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 :: Integer -> EVM () -> EVM () Source #

Burn gas, failing if insufficient gas is available We use the Integer type to avoid overflows in intermediate calculations and throw if the value won't fit into a uint64

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

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

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

type CheatAction = Word -> Word -> Buffer -> EVM () Source #

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

Hack deterministic signing, totally insecure...

General call implementation ("delegateCall")

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

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

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

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

Stack manipulation

push :: Word -> EVM () Source #

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

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

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

Bytecode data functions

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

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 #

Emacs setup