Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data ProofResult a b c
- type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)
- type EquivalenceResult = ProofResult ([VM], [VM]) VM ()
- isQed :: ProofResult a b c -> Bool
- containsA :: Eq a => Eq b => Eq c => ProofResult a b c -> [(d, e, ProofResult a b c)] -> Bool
- data VeriOpts = VeriOpts {}
- 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
- data CalldataFragment
- symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])
- cdLen :: [CalldataFragment] -> Expr EWord
- writeSelector :: Expr Buf -> Text -> Expr Buf
- combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop])
- abstractVM :: Maybe (Text, [AbiType]) -> [String] -> 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)
- maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
- type Precondition = VM -> Prop
- type Postcondition = VM -> Expr End -> Prop
- checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])
- checkAssertions :: [Word256] -> Postcondition
- defaultPanicCodes :: [Word256]
- allPanicCodes :: [Word256]
- panicMsg :: Word256 -> ByteString
- verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
- pruneDeadPaths :: [VM] -> [VM]
- runExpr :: Stepper (Expr End)
- flattenExpr :: Expr End -> [([Prop], Expr End)]
- reachable :: SolverGroup -> Expr End -> IO ([SMT2], Expr End)
- evalProp :: Prop -> Prop
- extractProps :: Expr End -> [Prop]
- verify :: SolverGroup -> VeriOpts -> VM -> Maybe Postcondition -> IO (Expr End, [VerifyResult])
- equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [(Maybe SMTCex, Prop, ProofResult () () ())]
- 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
Documentation
data ProofResult a b c Source #
Instances
(Show a, Show b, Show c) => Show (ProofResult a b c) Source # | |
Defined in EVM.SymExec 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) Source # | |
Defined in EVM.SymExec (==) :: 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) Source #
type EquivalenceResult = ProofResult ([VM], [VM]) VM () Source #
isQed :: ProofResult a b c -> Bool Source #
containsA :: Eq a => Eq b => Eq c => ProofResult a b c -> [(d, e, ProofResult a b c)] -> Bool Source #
rpcVeriOpts :: (BlockNumber, Text) -> VeriOpts Source #
extractCex :: VerifyResult -> Maybe (Expr End, SMTCex) Source #
data CalldataFragment Source #
Instances
Show CalldataFragment Source # | |
Defined in EVM.SymExec showsPrec :: Int -> CalldataFragment -> ShowS # show :: CalldataFragment -> String # showList :: [CalldataFragment] -> ShowS # | |
Eq CalldataFragment Source # | |
Defined in EVM.SymExec (==) :: CalldataFragment -> CalldataFragment -> Bool # (/=) :: CalldataFragment -> CalldataFragment -> Bool # |
symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop]) Source #
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.
combineFragments :: [CalldataFragment] -> Expr Buf -> (Expr Buf, [Prop]) Source #
abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> Maybe Precondition -> StorageModel -> VM Source #
loadSymVM :: ContractCode -> Expr Storage -> Expr EWord -> Expr EWord -> Expr Buf -> [Prop] -> VM Source #
interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper (Expr End) -> StateT VM IO (Expr End) Source #
Interpreter which explores all paths at branching points. returns an Expr representing the possible executions
type Precondition = VM -> Prop Source #
checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult]) Source #
checkAssertions :: [Word256] -> Postcondition Source #
Checks if an assertion violation has been encountered
hevm recognises the following as an assertion violation:
- the invalid opcode (0xfe) (solc < 0.8)
- 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.
defaultPanicCodes :: [Word256] Source #
By default hevm checks for all assertions except those which result from arithmetic overflow
allPanicCodes :: [Word256] Source #
panicMsg :: Word256 -> ByteString Source #
Produces the revert message for solc >=0.8 assertion violations
verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult]) Source #
pruneDeadPaths :: [VM] -> [VM] Source #
runExpr :: Stepper (Expr End) Source #
Stepper that parses the result of Stepper.runFully into an Expr End
flattenExpr :: Expr End -> [([Prop], Expr End)] Source #
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) Source #
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
verify :: SolverGroup -> VeriOpts -> VM -> Maybe Postcondition -> IO (Expr End, [VerifyResult]) Source #
Symbolically execute the VM and check all endstates against the postcondition, if available.
equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [(Maybe SMTCex, Prop, ProofResult () () ())] Source #
Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.
produceModels :: SolverGroup -> Expr End -> IO [(Expr End, CheckSatResult)] Source #