EVM.SymExec

Documentation

data Sig

A method name, and the (ordered) types of it's arguments

Constructors

Sig Text [AbiType]

data ProofResult a b c

Constructors

Qed a

Cex b

Timeout c

Instances

(Show a, Show b, Show c) => Show (ProofResult a b c)

Defined in EVM.SymExec

Methods

showsPrec :: Int -> ProofResult a b c -> ShowS

show :: ProofResult a b c -> String

showList :: [ProofResult a b c] -> ShowS

(Eq a, Eq b, Eq c) => Eq (ProofResult a b c)

Defined in EVM.SymExec

Methods

(==) :: ProofResult a b c -> ProofResult a b c -> Bool

(/=) :: ProofResult a b c -> ProofResult a b c -> Bool

type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)

type EquivResult = ProofResult () SMTCex ()

isTimeout :: ProofResult a b c -> Bool

isCex :: ProofResult a b c -> Bool

isQed :: ProofResult a b c -> Bool

data VeriOpts

Constructors

VeriOpts

Fields

• simp :: Bool
• debug :: Bool
• maxIter :: Maybe Integer
• askSmtIters :: Maybe Integer
• rpcInfo :: RpcInfo

Instances

Show VeriOpts

Defined in EVM.SymExec

Methods

showsPrec :: Int -> VeriOpts -> ShowS

show :: VeriOpts -> String

showList :: [VeriOpts] -> ShowS

Eq VeriOpts

Defined in EVM.SymExec

Methods

(==) :: VeriOpts -> VeriOpts -> Bool

(/=) :: VeriOpts -> VeriOpts -> Bool

defaultVeriOpts :: VeriOpts

rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts

debugVeriOpts :: VeriOpts

extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)

inRange :: Int -> Expr EWord -> Prop

bool :: Expr EWord -> Prop

symAbiArg :: Text -> AbiType -> CalldataFragment

Abstract calldata argument generation

data CalldataFragment

Constructors

St [Prop] (Expr EWord)

Dy [Prop] (Expr EWord) (Expr Buf)

Comp [CalldataFragment]

Instances

Show CalldataFragment

Defined in EVM.SymExec

Methods

showsPrec :: Int -> CalldataFragment -> ShowS

show :: CalldataFragment -> String

showList :: [CalldataFragment] -> ShowS

Eq CalldataFragment

Defined in EVM.SymExec

Methods

(==) :: CalldataFragment -> CalldataFragment -> Bool

(/=) :: CalldataFragment -> CalldataFragment -> Bool

symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])

Generates calldata matching given type signature, optionally specialized with concrete arguments. Any argument given as "symbolic" or omitted at the tail of the list are kept symbolic.

cdLen :: [CalldataFragment] -> Expr EWord

writeSelector :: Expr Buf -> Text -> Expr Buf

combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])

abstractVM :: (Expr Buf, [Prop]) -> ByteString -> Maybe Precondition -> StorageModel -> VM

loadSymVM :: ContractCode -> Expr Storage -> Expr EWord -> Expr EWord -> Expr Buf -> [Prop] -> VM

interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper (Expr End) -> StateT VM IO (Expr End)

Interpreter which explores all paths at branching points. returns an Expr representing the possible executions

maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool

type Precondition = VM -> Prop

type Postcondition = VM -> Expr End -> Prop

checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])

checkAssertions :: [Word256] -> Postcondition

Checks if an assertion violation has been encountered

hevm recognises the following as an assertion violation:

1. the invalid opcode (0xfe) (solc < 0.8)
2. a revert with a reason of the form `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of the following (solc >= 0.8): - 0x00: Used for generic compiler inserted panics. - 0x01: If you call assert with an argument that evaluates to false. - 0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block. - 0x12; If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0). - 0x21: If you convert a value that is too big or negative into an enum type. - 0x22: If you access a storage byte array that is incorrectly encoded. - 0x31: If you call .pop() on an empty array. - 0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0). - 0x41: If you allocate too much memory or create an array that is too large. - 0x51: If you call a zero-initialized variable of internal function type.

see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require

defaultPanicCodes :: [Word256]

By default hevm checks for all assertions except those which result from arithmetic overflow

allPanicCodes :: [Word256]

panicMsg :: Word256 -> ByteString

Produces the revert message for solc >=0.8 assertion violations

mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])

Builds a buffer representing calldata from the provided method description and concrete arguments

verifyContract :: SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])

pruneDeadPaths :: [VM] -> [VM]

runExpr :: Stepper (Expr End)

Stepper that parses the result of Stepper.runFully into an Expr End

flattenExpr :: Expr End -> [([Prop], Expr End)]

Converts a given top level expr into a list of final states and the associated path conditions for each state

reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)

Strips unreachable branches from a given expr Returns a list of executed SMT queries alongside the reduced expression for debugging purposes Note that the reduced expression loses information relative to the original one if jump conditions are removed. This restriction can be removed once Expr supports attaching knowledge to AST nodes. Although this algorithm currently parallelizes nicely, it does not exploit the incremental nature of the task at hand. Introducing support for incremental queries might let us go even faster here. TODO: handle errors properly

evalProp :: Prop -> Prop

Evaluate the provided proposition down to its most concrete result

extractProps :: Expr End -> [Prop]

Extract contraints stored in Expr End nodes

verify :: SolverGroup -> VeriOpts -> VM -> Maybe Postcondition -> IO (Expr End, [VerifyResult])

Symbolically execute the VM and check all endstates against the postcondition, if available.

type UnsatCache = TVar [Set Prop]

equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) -> IO [EquivResult]

Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.

We do this by asking the solver to find a common input for each pair of endstates that satisfies the path conditions for both sides and produces a differing output. If we can find such an input, then we have a clear equivalence break, and since we run this check for every pair of end states, the check is exhaustive.

both' :: (a -> b) -> (a, a) -> (b, b)

produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)]

showModel :: Expr Buf -> (Expr End, CheckSatResult) -> IO ()

formatCex :: Expr Buf -> SMTCex -> Text

subModel :: SMTCex -> Expr a -> Expr a

Takes a buffer and a Cex and replaces all abstract values in the buf with concrete ones from the Cex