hevm-0.48.0: Ethereum virtual machine evaluator
Safe HaskellNone
LanguageHaskell2010

EVM.SymExec

Synopsis

Documentation

data ProofResult a b c Source #

Constructors

Qed a 
Cex b 
Timeout c 

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

symAbiArg :: AbiType -> Query ([SWord 8], W256) Source #

Abstract calldata argument generation

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.

data BranchInfo Source #

Constructors

BranchInfo 

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

checkAssertions :: [Word256] -> Postcondition Source #

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] Source #

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

panicMsg :: Word256 -> ByteString Source #

Produces the revert message for solc >=0.8 assertion violations

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.

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