| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
EVM.SymExec
Synopsis
- data ProofResult a b c
- type VerifyResult = ProofResult (Tree BranchInfo) (Tree BranchInfo) (Tree BranchInfo)
- type EquivalenceResult = ProofResult ([VM], [VM]) VM ()
- sbytes32 :: Query [SWord 8]
- sbytes128 :: Query [SWord 8]
- sbytes256 :: Query [SWord 8]
- sbytes512 :: Query [SWord 8]
- sbytes1024 :: Query [SWord 8]
- mkByte :: Query [SWord 8]
- symAbiArg :: AbiType -> Query ([SWord 8], W256)
- symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256)
- abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM
- loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM
- data BranchInfo = BranchInfo {
- _vm :: VM
- _branchCondition :: Maybe Whiff
- doInterpret :: Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (Tree BranchInfo)
- interpret' :: Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])
- interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper a -> StateT VM Query [a]
- maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
- type Precondition = VM -> SBool
- type Postcondition = (VM, VM) -> SBool
- checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (VerifyResult, VM)
- checkAssertions :: [Word256] -> Postcondition
- defaultPanicCodes :: [Word256]
- allPanicCodes :: [Word256]
- panicMsg :: Word256 -> ByteString
- verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (VerifyResult, VM)
- pruneDeadPaths :: [VM] -> [VM]
- consistentPath :: VM -> Query (Maybe VM)
- consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))
- leaves :: Tree BranchInfo -> [VM]
- verify :: VM -> Maybe Integer -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query VerifyResult
- equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query EquivalenceResult
- both' :: (a -> b) -> (a, a) -> (b, b)
- showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query ()
Documentation
type VerifyResult = ProofResult (Tree BranchInfo) (Tree BranchInfo) (Tree BranchInfo) Source #
type EquivalenceResult = ProofResult ([VM], [VM]) VM () Source #
sbytes32 :: Query [SWord 8] Source #
Convenience functions for generating large symbolic byte strings
sbytes128 :: Query [SWord 8] Source #
Convenience functions for generating large symbolic byte strings
sbytes256 :: Query [SWord 8] Source #
Convenience functions for generating large symbolic byte strings
sbytes512 :: Query [SWord 8] Source #
Convenience functions for generating large symbolic byte strings
sbytes1024 :: Query [SWord 8] Source #
Convenience functions for generating large symbolic byte strings
symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256) 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.
abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM Source #
loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM Source #
data BranchInfo Source #
Constructors
| BranchInfo | |
Fields
| |
interpret' :: Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo]) Source #
interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper a -> StateT VM Query [a] Source #
Interpreter which explores all paths at | branching points. | returns a list of possible final evm states
type Precondition = VM -> SBool Source #
checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (VerifyResult, VM) 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 :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (VerifyResult, VM) Source #
pruneDeadPaths :: [VM] -> [VM] Source #
consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo)) Source #
verify :: VM -> Maybe Integer -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query VerifyResult Source #
Symbolically execute the VM and check all endstates against the postcondition, if available.
equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query EquivalenceResult Source #
Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.