EVM.SymExec

Documentation

data Sig

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

Constructors

Sig Text [AbiType]

data LoopHeuristic

Constructors

Naive

StackBased

Instances

Generic LoopHeuristic

Defined in EVM.SymExec

Associated Types

type Rep LoopHeuristic :: Type -> Type

Methods

from :: LoopHeuristic -> Rep LoopHeuristic x

to :: Rep LoopHeuristic x -> LoopHeuristic

Read LoopHeuristic

Defined in EVM.SymExec

Methods

readsPrec :: Int -> ReadS LoopHeuristic

readList :: ReadS [LoopHeuristic]

readPrec :: ReadPrec LoopHeuristic

readListPrec :: ReadPrec [LoopHeuristic]

Show LoopHeuristic

Defined in EVM.SymExec

Methods

showsPrec :: Int -> LoopHeuristic -> ShowS

show :: LoopHeuristic -> String

showList :: [LoopHeuristic] -> ShowS

Eq LoopHeuristic

Defined in EVM.SymExec

Methods

(==) :: LoopHeuristic -> LoopHeuristic -> Bool

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

ParseField LoopHeuristic

Defined in EVM.SymExec

Methods

parseField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic

parseListOfField :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser [LoopHeuristic]

readField :: ReadM LoopHeuristic

metavar :: proxy LoopHeuristic -> String

ParseFields LoopHeuristic

Defined in EVM.SymExec

Methods

parseFields :: Maybe Text -> Maybe Text -> Maybe Char -> Maybe String -> Parser LoopHeuristic

ParseRecord LoopHeuristic

Defined in EVM.SymExec

Methods

parseRecord :: Parser LoopHeuristic

type Rep LoopHeuristic

Defined in EVM.SymExec

type Rep LoopHeuristic = D1 ('MetaData "LoopHeuristic" "EVM.SymExec" "hevm-0.51.0-inplace" 'False) (C1 ('MetaCons "Naive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StackBased" 'PrefixI 'False) (U1 :: Type -> Type))

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 :: Integer
• loopHeuristic :: LoopHeuristic
• 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 -> Expr Storage -> VM

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

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

Interpreter which explores all paths at branching points. Returns an 'Expr End' representing the possible executions.

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

askSmtItersReached :: VM -> Integer -> Bool

isLoopHead :: LoopHeuristic -> VM -> Maybe Bool

Loop head detection heuristic

The main thing we wish to differentiate between, are actual loop heads, and branch points inside of internal functions that are called multiple times.

One way to do this is to observe that for internal functions, the compiler must always store a stack item representing the location that it must jump back to. If we compare the stack at the time of the previous visit, and the time of the current visit, and notice that this location has changed, then we can guess that the location is a jump point within an internal function instead of a loop (where such locations should be constant between iterations).

This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.

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 only checks for user-defined assertions

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 -> Expr Storage -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])

runExpr :: Stepper (Expr End)

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

flattenExpr :: Expr End -> [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

isPartial :: Expr a -> Bool

getPartials :: [Expr End] -> [PartialExec]

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.