Safe Haskell | None |
---|---|
Language | Haskell2010 |
- 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
- 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
- | NotUnique Whiff
- | SMTTimeout
- data VMResult
- data VM = VM {}
- data Trace = Trace {}
- data TraceData
- data Query where
- 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
- data Choose where
- PleaseChoosePath :: Whiff -> (Bool -> EVM ()) -> Choose
- type EVM a = State VM a
- type CodeLocation = (Addr, Int)
- data BranchCondition
- = Case Bool
- | Unknown
- | Inconsistent
- data IsUnique a
- = Unique a
- | Multiple
- | InconsistentU
- | TimeoutU
- data Cache = Cache {}
- data VMOpts = VMOpts {
- vmoptContract :: Contract
- vmoptCalldata :: (Buffer, SymWord)
- 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 Integer
- vmoptChainId :: W256
- vmoptCreate :: Bool
- vmoptStorageModel :: StorageModel
- vmoptTxAccessList :: Map Addr [W256]
- data Log = Log Addr Buffer [SymWord]
- data Frame = Frame {}
- data FrameContext
- = CreationContext { }
- | CallContext { }
- data FrameState = FrameState {}
- data TxState = TxState {}
- data SubState = SubState {
- _selfdestructs :: [Addr]
- _touchedAccounts :: [Addr]
- _accessedAddresses :: Set Addr
- _accessedStorageKeys :: Set (Addr, W256)
- _refunds :: [(Addr, Integer)]
- data ContractCode
- data Storage
- data Contract = Contract {}
- data StorageModel
- 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 Integer
- 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 Buffer
- callvalue :: Lens' FrameState SymWord
- caller :: Lens' FrameState SAddr
- calldata :: Lens' FrameState (Buffer, SymWord)
- frameState :: Lens' Frame FrameState
- frameContext :: Lens' Frame FrameContext
- timestamp :: Lens' Block SymWord
- schedule :: Lens' Block (FeeSchedule Integer)
- 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, Integer)]
- accessedStorageKeys :: Lens' SubState (Set (Addr, W256))
- accessedAddresses :: Lens' SubState (Set Addr)
- 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 (Maybe 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)
- logs :: Lens' VM (Seq Log)
- iterations :: Lens' VM (Map CodeLocation Int)
- frames :: Lens' VM [Frame]
- env :: Lens' VM Env
- constraints :: Lens' VM [(SBool, Whiff)]
- cache :: Lens' VM Cache
- burned :: Lens' VM Word
- block :: Lens' VM Block
- bytecode :: Getter Contract Buffer
- 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 -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Integer -> EVM ()) -> EVM ()
- precompiledContract :: (?op :: Word8) => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> EVM ()
- executePrecompile :: (?op :: Word8) => Addr -> Integer -> 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
- makeUnique :: SymWord -> (Word -> EVM ()) -> EVM ()
- askSMT :: CodeLocation -> (SBool, Whiff) -> (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 :: Integer -> 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 :: Integer -> EVM ()
- unRefund :: Integer -> EVM ()
- touchAccount :: Addr -> EVM ()
- selfdestruct :: Addr -> EVM ()
- accessAndBurn :: Addr -> EVM () -> EVM ()
- accessAccountForGas :: Addr -> EVM Bool
- accessStorageForGas :: Addr -> SymWord -> EVM Bool
- cheatCode :: Addr
- cheat :: (?op :: Word8) => (Word, Word) -> (Word, Word) -> EVM ()
- type CheatAction = Word -> Word -> Buffer -> EVM ()
- cheatActions :: Map Word32 CheatAction
- ethsign :: PrivateKey -> Digest Keccak_256 -> Signature
- delegateCall :: (?op :: Word8) => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord] -> (Addr -> EVM ()) -> EVM ()
- collision :: Maybe Contract -> Bool
- create :: (?op :: Word8) => Addr -> Contract -> Word -> Word -> [SymWord] -> Addr -> Buffer -> EVM ()
- replaceCode :: Addr -> ContractCode -> EVM ()
- replaceCodeOfSelf :: ContractCode -> EVM ()
- resetState :: EVM ()
- vmError :: Error -> EVM ()
- underrun :: EVM ()
- data FrameResult
- finishFrame :: FrameResult -> EVM ()
- accessUnboundedMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM ()
- accessMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM ()
- accessMemoryWord :: FeeSchedule Integer -> 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 -> Integer) -> (SymWord -> SymWord) -> EVM ()
- stackOp2 :: (?op :: Word8) => ((SymWord, SymWord) -> Integer) -> ((SymWord, SymWord) -> SymWord) -> EVM ()
- stackOp3 :: (?op :: Word8) => ((SymWord, SymWord, SymWord) -> Integer) -> ((SymWord, SymWord, SymWord) -> SymWord) -> EVM ()
- checkJump :: Integral n => n -> [SymWord] -> EVM ()
- opSize :: Word8 -> Int
- mkOpIxMap :: Buffer -> Vector Int
- vmOp :: VM -> Maybe Op
- vmOpIx :: VM -> Maybe Int
- opParams :: VM -> Map String SymWord
- readOp :: Word8 -> Buffer -> Op
- mkCodeOps :: Buffer -> Vector (Int, Op)
- costOfCall :: FeeSchedule Integer -> Bool -> Word -> Word -> Word -> Addr -> EVM (Integer, Integer)
- costOfCreate :: FeeSchedule Integer -> Word -> Word -> (Integer, Integer)
- concreteModexpGasFee :: ByteString -> Integer
- costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer
- memoryCost :: FeeSchedule Integer -> Integer -> Integer
- ceilDiv :: (Num a, Integral a) => a -> a -> a
- allButOne64th :: (Num a, Integral a) => a -> a
- log2 :: FiniteBits b => b -> Int
Data types
EVM failure modes
The possible result states of a VM
The state of a stepwise EVM execution
Trace | |
|
Queries halt execution until resolved through RPC calls or SMT queries
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 |
PleaseChoosePath :: Whiff -> (Bool -> EVM ()) -> Choose |
type CodeLocation = (Addr, Int) Source #
data BranchCondition Source #
The possible return values of a SMT query
Instances
Show BranchCondition Source # | |
Defined in EVM showsPrec :: Int -> BranchCondition -> ShowS # show :: BranchCondition -> String # showList :: [BranchCondition] -> ShowS # |
The possible return values of a `is unique` SMT query
The cache is data that can be persisted for efficiency: any expensive query that is constant at least within a block.
A way to specify an initial VM state
VMOpts | |
|
A log entry
An entry in the VM's "call/create stack"
data FrameContext Source #
Call/create info
Instances
Show FrameContext Source # | |
Defined in EVM showsPrec :: Int -> FrameContext -> ShowS # show :: FrameContext -> String # showList :: [FrameContext] -> ShowS # | |
SDisplay FrameContext Source # | |
data FrameState Source #
The "registers" of the VM along with memory and data stack
Instances
Show FrameState Source # | |
Defined in EVM showsPrec :: Int -> FrameState -> ShowS # show :: FrameState -> String # showList :: [FrameState] -> ShowS # | |
SDisplay FrameState Source # | |
The state that spans a whole transaction
The "accrued substate" across a transaction
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.
InitCode Buffer | Constructor code, during contract creation |
RuntimeCode Buffer | Instance code, after contract creation |
Instances
Show ContractCode Source # | |
Defined in EVM showsPrec :: Int -> ContractCode -> ShowS # show :: ContractCode -> String # showList :: [ContractCode] -> ShowS # |
A contract can either have concrete or symbolic storage depending on what type of execution we are doing
The state of a contract
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.
ConcreteS | Uses |
SymbolicS | Uses |
InitialS | Uses |
Instances
Read StorageModel Source # | |
Defined in EVM readsPrec :: Int -> ReadS StorageModel # readList :: ReadS [StorageModel] # | |
Show StorageModel Source # | |
Defined in EVM showsPrec :: Int -> StorageModel -> ShowS # show :: StorageModel -> String # showList :: [StorageModel] -> ShowS # | |
ParseField StorageModel Source # | |
Defined in EVM 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 # |
Various environmental data
Env | |
|
Data about the block
Block | |
|
iterations :: Lens' VM (Map CodeLocation Int) Source #
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
contractWithStore :: ContractCode -> Storage -> Contract Source #
Opcode dispatch (exec1)
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 #
truncpadlit :: Int -> ByteString -> ByteString Source #
lazySlice :: Word -> Word -> ByteString -> ByteString Source #
parseModexpLength :: ByteString -> (Word, Word, Word) Source #
asInteger :: ByteString -> Integer Source #
Opcode helper actions
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 #
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
accountEmpty :: Contract -> Bool Source #
How to finalize a transaction
loadContract :: Addr -> EVM () Source #
Loads the selected contract as the current contract to execute
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
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
touchAccount :: Addr -> EVM () Source #
selfdestruct :: Addr -> 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
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.
replaceCodeOfSelf :: ContractCode -> EVM () Source #
resetState :: EVM () Source #
VM error implementation
data FrameResult Source #
A stack frame can be popped in three ways.
FrameReturned Buffer | STOP, RETURN, or no more code |
FrameReverted Buffer | REVERT |
FrameErrored Error | Any other error |
Instances
Show FrameResult Source # | |
Defined in EVM 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 Integer -> Word -> Word -> EVM () -> EVM () Source #
accessMemoryRange :: FeeSchedule Integer -> Word -> Word -> EVM () -> EVM () Source #
accessMemoryWord :: FeeSchedule Integer -> Word -> EVM () -> EVM () Source #
Tracing
withTraceLocation :: MonadState VM m => TraceData -> m Trace Source #
insertTrace :: TraceData -> EVM () Source #
Stack manipulation
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
Gas cost calculation helpers
costOfCall :: FeeSchedule Integer -> Bool -> Word -> Word -> Word -> Addr -> EVM (Integer, Integer) Source #
costOfCreate :: FeeSchedule Integer -> Word -> Word -> (Integer, Integer) Source #
costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer Source #
memoryCost :: FeeSchedule Integer -> Integer -> Integer Source #
Arithmetic
allButOne64th :: (Num a, Integral a) => a -> a Source #
log2 :: FiniteBits b => b -> Int Source #