Safe Haskell	None
Language	Haskell2010

EVM

Contents

Data types
Data accessors
Data constructors
Opcode dispatch (exec1)
Opcode helper actions
How to finalize a transaction
Substate manipulation
Cheat codes
General call implementation ("delegateCall")
VM error implementation
Memory helpers
Tracing
Stack manipulation
Bytecode data functions
Gas cost calculation helpers
Uninterpreted functions
Arithmetic
Emacs setup

Synopsis

data Error
- = BalanceTooLow Word Word
- | UnrecognizedOpcode Word8
- | SelfDestruction
- | StackUnderrun
- | BadJumpDestination
- | Revert ByteString
- | NoSuchContract Addr
- | OutOfGas Word Word
- | BadCheatCode (Maybe Word32)
- | StackLimitExceeded
- | IllegalOverflow
- | Query Query
- | Choose Choose
- | StateChangeWhileStatic
- | InvalidMemoryAccess
- | CallDepthLimitReached
- | MaxCodeSizeExceeded Word Word
- | PrecompileFailure
- | UnexpectedSymbolicArg
- | DeadPath
data VMResult
- = VMFailure Error
- | VMSuccess Buffer
data VM = VM {
- _result :: Maybe VMResult
- _state :: FrameState
- _frames :: [Frame]
- _env :: Env
- _block :: Block
- _tx :: TxState
- _logs :: Seq Log
- _traces :: TreePos Empty Trace
- _cache :: Cache
- _burned :: Word
- _pathConditions :: [SBool]
- _iterations :: Map CodeLocation Int
}
data Trace = Trace {
- _traceCodehash :: W256
- _traceOpIx :: Int
- _traceData :: TraceData
}
data TraceData
- = EventTrace Log
- | FrameTrace FrameContext
- | QueryTrace Query
- | ErrorTrace Error
- | EntryTrace Text
- | ReturnTrace Buffer FrameContext
data Query where
- PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query
- PleaseFetchSlot :: Addr -> Word -> (Word -> EVM ()) -> Query
- PleaseAskSMT :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query
data Choose where
- PleaseChoosePath :: (Bool -> EVM ()) -> Choose
type EVM a = State VM a
type CodeLocation = (Addr, Int)
data BranchCondition
- = Case Bool
- | Unknown
- | Inconsistent
data Cache = Cache {
- _fetched :: Map Addr Contract
- _path :: Map (CodeLocation, Int) Bool
}
data VMOpts = VMOpts {
- vmoptContract :: Contract
- vmoptCalldata :: (Buffer, SWord 32)
- vmoptValue :: SymWord
- vmoptAddress :: Addr
- vmoptCaller :: SAddr
- vmoptOrigin :: Addr
- vmoptGas :: W256
- vmoptGaslimit :: W256
- vmoptNumber :: W256
- vmoptTimestamp :: SymWord
- vmoptCoinbase :: Addr
- vmoptDifficulty :: W256
- vmoptMaxCodeSize :: W256
- vmoptBlockGaslimit :: W256
- vmoptGasprice :: W256
- vmoptSchedule :: FeeSchedule Word
- vmoptChainId :: W256
- vmoptCreate :: Bool
- vmoptStorageModel :: StorageModel
}
data Log = Log Addr Buffer [SymWord]
data Frame = Frame {
- _frameContext :: FrameContext
- _frameState :: FrameState
}
data FrameContext
- = CreationContext {
  }
- | CallContext {
  - callContextTarget :: Addr
  - callContextContext :: Addr
  - callContextOffset :: Word
  - callContextSize :: Word
  - callContextCodehash :: W256
  - callContextAbi :: Maybe Word
  - callContextData :: Buffer
  - callContextReversion :: Map Addr Contract
  - callContextSubState :: SubState
  }
data FrameState = FrameState {
- _contract :: Addr
- _codeContract :: Addr
- _code :: ByteString
- _pc :: Int
- _stack :: [SymWord]
- _memory :: Buffer
- _memorySize :: Int
- _calldata :: (Buffer, SWord 32)
- _callvalue :: SymWord
- _caller :: SAddr
- _gas :: Word
- _returndata :: Buffer
- _static :: Bool
}
data TxState = TxState {
- _gasprice :: Word
- _txgaslimit :: Word
- _origin :: Addr
- _toAddr :: Addr
- _value :: SymWord
- _substate :: SubState
- _isCreate :: Bool
- _txReversion :: Map Addr Contract
}
data SubState = SubState {
- _selfdestructs :: [Addr]
- _touchedAccounts :: [Addr]
- _refunds :: [(Addr, Word)]
}
data ContractCode
- = InitCode ByteString
- | RuntimeCode ByteString
data Storage
- = Concrete (Map Word SymWord)
- | Symbolic (SArray (WordN 256) (WordN 256))
data Contract = Contract {
- _contractcode :: ContractCode
- _storage :: Storage
- _balance :: Word
- _nonce :: Word
- _codehash :: W256
- _opIxMap :: Vector Int
- _codeOps :: Vector (Int, Op)
- _external :: Bool
- _origStorage :: Map Word Word
}
data StorageModel
- = ConcreteS
- | SymbolicS
- | InitialS
data Env = Env {
- _contracts :: Map Addr Contract
- _chainId :: Word
- _storageModel :: StorageModel
- _sha3Crack :: Map Word ByteString
- _keccakUsed :: [([SWord 8], SWord 256)]
}
data Block = Block {
- _coinbase :: Addr
- _timestamp :: SymWord
- _number :: Word
- _difficulty :: Word
- _gaslimit :: Word
- _maxCodeSize :: Word
- _schedule :: FeeSchedule Word
}
blankState :: FrameState
static :: Lens' FrameState Bool
stack :: Lens' FrameState [SymWord]
returndata :: Lens' FrameState Buffer
pc :: Lens' FrameState Int
memorySize :: Lens' FrameState Int
memory :: Lens' FrameState Buffer
gas :: Lens' FrameState Word
contract :: Lens' FrameState Addr
codeContract :: Lens' FrameState Addr
code :: Lens' FrameState ByteString
callvalue :: Lens' FrameState SymWord
caller :: Lens' FrameState SAddr
calldata :: Lens' FrameState (Buffer, SWord 32)
frameState :: Lens' Frame FrameState
frameContext :: Lens' Frame FrameContext
timestamp :: Lens' Block SymWord
schedule :: Lens' Block (FeeSchedule Word)
number :: Lens' Block Word
maxCodeSize :: Lens' Block Word
gaslimit :: Lens' Block Word
difficulty :: Lens' Block Word
coinbase :: Lens' Block Addr
value :: Lens' TxState SymWord
txgaslimit :: Lens' TxState Word
txReversion :: Lens' TxState (Map Addr Contract)
toAddr :: Lens' TxState Addr
substate :: Lens' TxState SubState
origin :: Lens' TxState Addr
isCreate :: Lens' TxState Bool
gasprice :: Lens' TxState Word
touchedAccounts :: Lens' SubState [Addr]
selfdestructs :: Lens' SubState [Addr]
refunds :: Lens' SubState [(Addr, Word)]
storage :: Lens' Contract Storage
origStorage :: Lens' Contract (Map Word Word)
opIxMap :: Lens' Contract (Vector Int)
nonce :: Lens' Contract Word
external :: Lens' Contract Bool
contractcode :: Lens' Contract ContractCode
codehash :: Lens' Contract W256
codeOps :: Lens' Contract (Vector (Int, Op))
balance :: Lens' Contract Word
storageModel :: Lens' Env StorageModel
sha3Crack :: Lens' Env (Map Word ByteString)
keccakUsed :: Lens' Env [([SWord 8], SWord 256)]
contracts :: Lens' Env (Map Addr Contract)
chainId :: Lens' Env Word
path :: Lens' Cache (Map (CodeLocation, Int) Bool)
fetched :: Lens' Cache (Map Addr Contract)
traceOpIx :: Lens' Trace Int
traceData :: Lens' Trace TraceData
traceCodehash :: Lens' Trace W256
tx :: Lens' VM TxState
traces :: Lens' VM (TreePos Empty Trace)
state :: Lens' VM FrameState
result :: Lens' VM (Maybe VMResult)
pathConditions :: Lens' VM [SBool]
logs :: Lens' VM (Seq Log)
iterations :: Lens' VM (Map CodeLocation Int)
frames :: Lens' VM [Frame]
env :: Lens' VM Env
cache :: Lens' VM Cache
burned :: Lens' VM Word
block :: Lens' VM Block
bytecode :: Getter Contract ByteString
unifyCachedContract :: Contract -> Contract -> Contract
currentContract :: VM -> Maybe Contract
makeVm :: VMOpts -> VM
initialContract :: ContractCode -> Contract
contractWithStore :: ContractCode -> Storage -> Contract
next :: (?op :: Word8) => EVM ()
exec1 :: EVM ()
transfer :: Addr -> Addr -> Word -> EVM ()
callChecks :: (?op :: Word8) => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Word -> EVM ()) -> EVM ()
precompiledContract :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM ()
executePrecompile :: (?op :: Word8) => Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM ()
truncpadlit :: Int -> ByteString -> ByteString
lazySlice :: Word -> Word -> ByteString -> ByteString
parseModexpLength :: ByteString -> (Word, Word, Word)
isZero :: Word -> Word -> ByteString -> Bool
asInteger :: ByteString -> Integer
noop :: Monad m => m ()
pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()
pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()
getCodeLocation :: VM -> CodeLocation
askSMT :: CodeLocation -> SBool -> (Bool -> EVM ()) -> EVM ()
fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()
readStorage :: Storage -> SymWord -> Maybe SymWord
writeStorage :: SymWord -> SymWord -> Storage -> Storage
accessStorage :: Addr -> SymWord -> (SymWord -> EVM ()) -> EVM ()
accountExists :: Addr -> VM -> Bool
accountEmpty :: Contract -> Bool
finalize :: EVM ()
loadContract :: Addr -> EVM ()
limitStack :: Int -> EVM () -> EVM ()
notStatic :: EVM () -> EVM ()
burn :: Word -> EVM () -> EVM ()
forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM ()
forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM ()
forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM ()
forceConcrete3 :: (SymWord, SymWord, SymWord) -> ((Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete4 :: (SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete5 :: (SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcrete6 :: (SymWord, SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()
forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM ()
refund :: Word -> EVM ()
unRefund :: Word -> EVM ()
touchAccount :: Addr -> EVM ()
selfdestruct :: Addr -> EVM ()
cheatCode :: Addr
cheat :: (?op :: Word8) => (Word, Word) -> (Word, Word) -> EVM ()
type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ())
cheatActions :: Map Word32 CheatAction
delegateCall :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM () -> EVM ()
collision :: Maybe Contract -> Bool
create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> ByteString -> EVM ()
replaceCode :: Addr -> ContractCode -> EVM ()
replaceCodeOfSelf :: ContractCode -> EVM ()
resetState :: EVM ()
vmError :: Error -> EVM ()
underrun :: EVM ()
data FrameResult
- = FrameReturned Buffer
- | FrameReverted Buffer
- | FrameErrored Error
finishFrame :: FrameResult -> EVM ()
accessUnboundedMemoryRange :: FeeSchedule Word -> Word -> Word -> EVM () -> EVM ()
accessMemoryRange :: FeeSchedule Word -> Word -> Word -> EVM () -> EVM ()
accessMemoryWord :: FeeSchedule Word -> Word -> EVM () -> EVM ()
copyBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM ()
copyCallBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM ()
readMemory :: Word -> Word -> VM -> Buffer
word256At :: Functor f => Word -> (SymWord -> f SymWord) -> Buffer -> f Buffer
withTraceLocation :: MonadState VM m => TraceData -> m Trace
pushTrace :: TraceData -> EVM ()
insertTrace :: TraceData -> EVM ()
popTrace :: EVM ()
zipperRootForest :: TreePos Empty a -> Forest a
traceForest :: VM -> Forest Trace
traceLog :: MonadState VM m => Log -> m ()
push :: Word -> EVM ()
pushSym :: SymWord -> EVM ()
stackOp1 :: (?op :: Word8) => (SymWord -> Word) -> (SymWord -> SymWord) -> EVM ()
stackOp2 :: (?op :: Word8) => ((SymWord, SymWord) -> Word) -> ((SymWord, SymWord) -> SymWord) -> EVM ()
stackOp3 :: (?op :: Word8) => ((SymWord, SymWord, SymWord) -> Word) -> ((SymWord, SymWord, SymWord) -> SymWord) -> EVM ()
checkJump :: Integral n => n -> [SymWord] -> EVM ()
opSize :: Word8 -> Int
mkOpIxMap :: ByteString -> Vector Int
vmOp :: VM -> Maybe Op
vmOpIx :: VM -> Maybe Int
opParams :: VM -> Map String SymWord
readOp :: Word8 -> ByteString -> Op
mkCodeOps :: ByteString -> Vector (Int, Op)
costOfCall :: FeeSchedule Word -> Bool -> Word -> Word -> Word -> (Word, Word)
costOfCreate :: FeeSchedule Word -> Word -> Word -> (Word, Word)
costOfPrecompile :: FeeSchedule Word -> Addr -> Buffer -> Word
memoryCost :: FeeSchedule Word -> Word -> Word
symSHA256N :: SInteger -> SInteger -> SWord 256
symkeccakN :: SInteger -> SInteger -> SWord 256
toSInt :: [SWord 8] -> SInteger
symkeccak' :: [SWord 8] -> SWord 256
symSHA256 :: [SWord 8] -> [SWord 8]
ceilDiv :: (Num a, Integral a) => a -> a -> a
allButOne64th :: (Num a, Integral a) => a -> a
log2 :: FiniteBits b => b -> Int

Data types

data Error Source #

EVM failure modes

Instances

Show Error Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Error -> ShowS # show :: Error -> String # showList :: [Error] -> ShowS #

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 Methods showsPrec :: Int -> VMResult -> ShowS # show :: VMResult -> String # showList :: [VMResult] -> ShowS #
SDisplay VMResult Source #
Instance details Defined in EVM.Emacs Methods sexp :: VMResult -> SExpr Text Source #

data VM Source #

The state of a stepwise EVM execution

Constructors

VM
Fields _result :: Maybe VMResult _state :: FrameState _frames :: [Frame] _env :: Env _block :: Block _tx :: TxState _logs :: Seq Log _traces :: TreePos Empty Trace _cache :: Cache _burned :: Word _pathConditions :: [SBool] _iterations :: Map CodeLocation Int

Instances

SDisplay VM Source #
Instance details Defined in EVM.Emacs Methods sexp :: VM -> SExpr Text Source #

data Trace Source #

Constructors

Trace
Fields _traceCodehash :: W256 _traceOpIx :: Int _traceData :: TraceData

data TraceData Source #

Constructors

EventTrace Log
FrameTrace FrameContext
QueryTrace Query
ErrorTrace Error
EntryTrace Text
ReturnTrace Buffer FrameContext

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 :: SBool -> [SBool] -> (BranchCondition -> 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 Methods showsPrec :: Int -> Choose -> ShowS # show :: Choose -> String # showList :: [Choose] -> ShowS #

type EVM a = State VM a Source #

Alias for the type of e.g. exec1.

type CodeLocation = (Addr, Int) Source #

data BranchCondition Source #

The possible return values of a SMT query

Constructors

Case Bool
Unknown
Inconsistent

Instances

Show BranchCondition Source #
Instance details Defined in EVM Methods showsPrec :: Int -> BranchCondition -> ShowS # show :: BranchCondition -> String # showList :: [BranchCondition] -> 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
Fields _fetched :: Map Addr Contract _path :: Map (CodeLocation, Int) Bool

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 VMOpts Source #

A way to specify an initial VM state

Constructors

VMOpts

Fields

vmoptContract :: Contract
vmoptCalldata :: (Buffer, SWord 32)
vmoptValue :: SymWord
vmoptAddress :: Addr
vmoptCaller :: SAddr
vmoptOrigin :: Addr
vmoptGas :: W256
vmoptGaslimit :: W256
vmoptNumber :: W256
vmoptTimestamp :: SymWord
vmoptCoinbase :: Addr
vmoptDifficulty :: W256
vmoptMaxCodeSize :: W256
vmoptBlockGaslimit :: W256
vmoptGasprice :: W256
vmoptSchedule :: FeeSchedule Word
vmoptChainId :: W256
vmoptCreate :: Bool
vmoptStorageModel :: StorageModel

Instances

Show VMOpts Source #
Instance details Defined in EVM Methods showsPrec :: Int -> VMOpts -> ShowS # show :: VMOpts -> String # showList :: [VMOpts] -> ShowS #

data Log Source #

A log entry

Constructors

Log Addr Buffer [SymWord]

data Frame Source #

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

Constructors

Frame
Fields _frameContext :: FrameContext _frameState :: FrameState

Instances

SDisplay Frame Source #
Instance details Defined in EVM.Emacs Methods sexp :: Frame -> SExpr Text Source #

data FrameContext Source #

Call/create info

Constructors

CreationContext
Fields creationContextCodehash :: W256 creationContextReversion :: Map Addr Contract creationContextSubstate :: SubState
CallContext
Fields callContextTarget :: Addr callContextContext :: Addr callContextOffset :: Word callContextSize :: Word callContextCodehash :: W256 callContextAbi :: Maybe Word callContextData :: Buffer callContextReversion :: Map Addr Contract callContextSubState :: SubState

Instances

SDisplay FrameContext Source #
Instance details Defined in EVM.Emacs Methods sexp :: FrameContext -> SExpr Text Source #

data FrameState Source #

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

Constructors

FrameState
Fields _contract :: Addr _codeContract :: Addr _code :: ByteString _pc :: Int _stack :: [SymWord] _memory :: Buffer _memorySize :: Int _calldata :: (Buffer, SWord 32) _callvalue :: SymWord _caller :: SAddr _gas :: Word _returndata :: Buffer _static :: Bool

Instances

SDisplay FrameState Source #
Instance details Defined in EVM.Emacs Methods sexp :: FrameState -> SExpr Text Source #

data TxState Source #

The state that spans a whole transaction

Constructors

TxState
Fields _gasprice :: Word _txgaslimit :: Word _origin :: Addr _toAddr :: Addr _value :: SymWord _substate :: SubState _isCreate :: Bool _txReversion :: Map Addr Contract

data SubState Source #

The "accrued substate" across a transaction

Constructors

SubState
Fields _selfdestructs :: [Addr] _touchedAccounts :: [Addr] _refunds :: [(Addr, Word)]

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 Methods (==) :: ContractCode -> ContractCode -> Bool # (/=) :: ContractCode -> ContractCode -> Bool #
Show ContractCode Source #
Instance details Defined in EVM Methods showsPrec :: Int -> ContractCode -> ShowS # show :: ContractCode -> String # showList :: [ContractCode] -> ShowS #

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 Methods showsPrec :: Int -> Storage -> ShowS # show :: Storage -> String # showList :: [Storage] -> ShowS #
SDisplay Storage Source #
Instance details Defined in EVM.Emacs Methods sexp :: Storage -> SExpr Text Source #

data Contract Source #

The state of a contract

Constructors

Contract
Fields _contractcode :: ContractCode _storage :: Storage _balance :: Word _nonce :: Word _codehash :: W256 _opIxMap :: Vector Int _codeOps :: Vector (Int, Op) _external :: Bool _origStorage :: Map Word Word

Instances

Eq Contract Source #
Instance details Defined in EVM Methods (==) :: Contract -> Contract -> Bool # (/=) :: Contract -> Contract -> Bool #
Show Contract Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Contract -> ShowS # show :: Contract -> String # showList :: [Contract] -> ShowS #
FromJSON Contract Source #
Instance details Defined in EVM.VMTest Methods parseJSON :: Value -> Parser Contract # parseJSONList :: Value -> Parser [Contract] #
SDisplay Contract Source #
Instance details Defined in EVM.Emacs Methods sexp :: Contract -> SExpr Text Source #

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.

Instances

Read StorageModel Source #
Instance details Defined in EVM Methods readsPrec :: Int -> ReadS StorageModel # readList :: ReadS [StorageModel] # readPrec :: ReadPrec StorageModel # readListPrec :: ReadPrec [StorageModel] #
Show StorageModel Source #
Instance details Defined in EVM Methods showsPrec :: Int -> StorageModel -> ShowS # show :: StorageModel -> String # showList :: [StorageModel] -> ShowS #
ParseField StorageModel Source #
Instance details Defined in EVM Methods parseField :: Maybe Text -> Maybe Text -> Maybe Char -> Parser StorageModel # parseListOfField :: Maybe Text -> Maybe Text -> Maybe Char -> Parser [StorageModel] # readField :: ReadM StorageModel # metavar :: proxy StorageModel -> String #

data Env Source #

Various environmental data

Constructors

Env
Fields _contracts :: Map Addr Contract _chainId :: Word _storageModel :: StorageModel _sha3Crack :: Map Word ByteString _keccakUsed :: [([SWord 8], SWord 256)]

data Block Source #

Data about the block

Constructors

Block
Fields _coinbase :: Addr _timestamp :: SymWord _number :: Word _difficulty :: Word _gaslimit :: Word _maxCodeSize :: Word _schedule :: FeeSchedule Word

Instances

Show Block Source #
Instance details Defined in EVM Methods showsPrec :: Int -> Block -> ShowS # show :: Block -> String # showList :: [Block] -> ShowS #

blankState :: FrameState Source #

static :: Lens' FrameState Bool Source #

stack :: Lens' FrameState [SymWord] Source #

returndata :: Lens' FrameState Buffer Source #

pc :: Lens' FrameState Int Source #

memorySize :: Lens' FrameState Int Source #

memory :: Lens' FrameState Buffer Source #

gas :: Lens' FrameState Word Source #

contract :: Lens' FrameState Addr Source #

codeContract :: Lens' FrameState Addr Source #

code :: Lens' FrameState ByteString Source #

callvalue :: Lens' FrameState SymWord Source #

caller :: Lens' FrameState SAddr Source #

calldata :: Lens' FrameState (Buffer, SWord 32) Source #

frameState :: Lens' Frame FrameState Source #

frameContext :: Lens' Frame FrameContext Source #

timestamp :: Lens' Block SymWord Source #

schedule :: Lens' Block (FeeSchedule Word) Source #

number :: Lens' Block Word Source #

maxCodeSize :: Lens' Block Word Source #

gaslimit :: Lens' Block Word Source #

difficulty :: Lens' Block Word Source #

coinbase :: Lens' Block Addr Source #

value :: Lens' TxState SymWord Source #

txgaslimit :: Lens' TxState Word Source #

txReversion :: Lens' TxState (Map Addr Contract) Source #

toAddr :: Lens' TxState Addr Source #

substate :: Lens' TxState SubState Source #

origin :: Lens' TxState Addr Source #

isCreate :: Lens' TxState Bool Source #

gasprice :: Lens' TxState Word Source #

touchedAccounts :: Lens' SubState [Addr] Source #

selfdestructs :: Lens' SubState [Addr] Source #

refunds :: Lens' SubState [(Addr, Word)] Source #

storage :: Lens' Contract Storage Source #

origStorage :: Lens' Contract (Map Word Word) Source #

opIxMap :: Lens' Contract (Vector Int) Source #

nonce :: Lens' Contract Word Source #

external :: Lens' Contract Bool Source #

contractcode :: Lens' Contract ContractCode Source #

codehash :: Lens' Contract W256 Source #

codeOps :: Lens' Contract (Vector (Int, Op)) Source #

balance :: Lens' Contract Word Source #

storageModel :: Lens' Env StorageModel Source #

sha3Crack :: Lens' Env (Map Word ByteString) Source #

keccakUsed :: Lens' Env [([SWord 8], SWord 256)] Source #

contracts :: Lens' Env (Map Addr Contract) Source #

chainId :: Lens' Env Word Source #

path :: Lens' Cache (Map (CodeLocation, Int) Bool) Source #

fetched :: Lens' Cache (Map Addr Contract) Source #

traceOpIx :: Lens' Trace Int Source #

traceData :: Lens' Trace TraceData Source #

traceCodehash :: Lens' Trace W256 Source #

tx :: Lens' VM TxState Source #

traces :: Lens' VM (TreePos Empty Trace) Source #

state :: Lens' VM FrameState Source #

result :: Lens' VM (Maybe VMResult) Source #

pathConditions :: Lens' VM [SBool] Source #

logs :: Lens' VM (Seq Log) Source #

iterations :: Lens' VM (Map CodeLocation Int) Source #

frames :: Lens' VM [Frame] Source #

env :: Lens' VM Env Source #

cache :: Lens' VM Cache Source #

burned :: Lens' VM Word Source #

block :: Lens' VM Block Source #

bytecode :: Getter Contract ByteString Source #

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

unifyCachedContract :: Contract -> Contract -> Contract Source #

Data accessors

currentContract :: VM -> Maybe Contract Source #

Data constructors

makeVm :: VMOpts -> VM Source #

initialContract :: ContractCode -> Contract Source #

Initialize empty contract with given code

contractWithStore :: ContractCode -> Storage -> Contract Source #

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 -> 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 #

truncpadlit :: Int -> ByteString -> ByteString Source #

lazySlice :: Word -> Word -> ByteString -> ByteString Source #

parseModexpLength :: ByteString -> (Word, Word, Word) Source #

isZero :: Word -> Word -> ByteString -> Bool Source #

asInteger :: ByteString -> Integer 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 #

getCodeLocation :: VM -> CodeLocation Source #

askSMT :: CodeLocation -> SBool -> (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

readStorage :: Storage -> SymWord -> Maybe SymWord Source #

writeStorage :: SymWord -> SymWord -> Storage -> Storage Source #

accessStorage Source #

Arguments

:: Addr	Contract address
-> SymWord	Storage slot key
-> (SymWord -> EVM ())	Continuation
-> EVM ()

accountExists :: Addr -> VM -> Bool Source #

accountEmpty :: Contract -> Bool Source #

How to finalize a transaction

finalize :: EVM () Source #

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 #

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

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

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

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

forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM () Source #

Substate manipulation

refund :: Word -> EVM () Source #

unRefund :: Word -> EVM () Source #

touchAccount :: Addr -> EVM () Source #

selfdestruct :: Addr -> EVM () Source #

Cheat codes

cheatCode :: Addr Source #

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

type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ()) Source #

cheatActions :: Map Word32 CheatAction Source #

General call implementation ("delegateCall")

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

collision :: Maybe Contract -> Bool 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.

replaceCodeOfSelf :: ContractCode -> EVM () Source #

resetState :: EVM () Source #

VM error implementation

vmError :: Error -> EVM () Source #

underrun :: EVM () Source #

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 Methods showsPrec :: Int -> FrameResult -> ShowS # show :: FrameResult -> String # showList :: [FrameResult] -> ShowS #

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

accessUnboundedMemoryRange :: FeeSchedule Word -> Word -> Word -> EVM () -> EVM () Source #

accessMemoryRange :: FeeSchedule Word -> Word -> Word -> EVM () -> EVM () Source #

accessMemoryWord :: FeeSchedule Word -> Word -> EVM () -> EVM () Source #

copyBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM () Source #

copyCallBytesToMemory :: Buffer -> Word -> Word -> Word -> EVM () Source #

readMemory :: Word -> Word -> VM -> Buffer Source #

word256At :: Functor f => Word -> (SymWord -> f SymWord) -> Buffer -> f Buffer Source #

Tracing

withTraceLocation :: MonadState VM m => TraceData -> m Trace Source #

pushTrace :: TraceData -> EVM () Source #

insertTrace :: TraceData -> EVM () Source #

popTrace :: EVM () Source #

zipperRootForest :: TreePos Empty a -> Forest a Source #

traceForest :: VM -> Forest Trace Source #

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

Stack manipulation

push :: Word -> EVM () Source #

pushSym :: SymWord -> 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 #

opSize :: Word8 -> Int Source #

mkOpIxMap :: ByteString -> Vector Int Source #

vmOp :: VM -> Maybe Op Source #

vmOpIx :: VM -> Maybe Int Source #

opParams :: VM -> Map String SymWord Source #

readOp :: Word8 -> ByteString -> Op Source #

mkCodeOps :: ByteString -> Vector (Int, Op) Source #

Gas cost calculation helpers

costOfCall :: FeeSchedule Word -> Bool -> Word -> Word -> Word -> (Word, Word) Source #

costOfCreate :: FeeSchedule Word -> Word -> Word -> (Word, Word) Source #

costOfPrecompile :: FeeSchedule Word -> Addr -> Buffer -> Word Source #

memoryCost :: FeeSchedule Word -> Word -> Word Source #

Uninterpreted functions

symSHA256N :: SInteger -> SInteger -> SWord 256 Source #

symkeccakN :: SInteger -> SInteger -> SWord 256 Source #

toSInt :: [SWord 8] -> SInteger Source #

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 #

BalanceTooLow Word Word
UnrecognizedOpcode Word8
SelfDestruction
StackUnderrun
BadJumpDestination
Revert ByteString
NoSuchContract Addr
OutOfGas Word Word
BadCheatCode (Maybe Word32)
StackLimitExceeded
IllegalOverflow
Query Query
Choose Choose
StateChangeWhileStatic
InvalidMemoryAccess
CallDepthLimitReached
MaxCodeSizeExceeded Word Word
PrecompileFailure
UnexpectedSymbolicArg
DeadPath

Data types

Data accessors

Data constructors

Opcode dispatch (exec1)

Opcode helper actions

How to finalize a transaction

Substate manipulation

Cheat codes

General call implementation ("delegateCall")

VM error implementation

Memory helpers

Tracing

Stack manipulation

Bytecode data functions

Gas cost calculation helpers

Uninterpreted functions

Arithmetic

Emacs setup