hevm-0.41.0: Ethereum virtual machine evaluator

Safe HaskellNone
LanguageHaskell2010

EVM.SymExec

Synopsis

Documentation

sbytes32 :: 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], SWord 32) Source #

Abstract calldata argument generation We don't assume input types are restricted to their proper range here; such assumptions should instead be given as preconditions. This could catch some interesting calldata mismanagement errors.

symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], SWord 32) 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.

interpret :: Fetcher -> Maybe Integer -> Stepper a -> StateT VM IO [a] Source #

Interpreter which explores all paths at | branching points. | returns a list of possible final evm states

verify :: VM -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) Source #

Symbolically execute the VM and check all endstates against the postcondition, if available. Returns `Right VM` if the postcondition can be violated, where VM is a prestate counterexample, or `Left (VM, [VM])`, a pair of prestate and post vm states.

equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM) 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 #