EVM.SymExec

Documentation

sbytes32 :: Query [SWord 8]

Convenience functions for generating large symbolic byte strings

sbytes128 :: Query [SWord 8]

Convenience functions for generating large symbolic byte strings

sbytes256 :: Query [SWord 8]

Convenience functions for generating large symbolic byte strings

sbytes512 :: Query [SWord 8]

Convenience functions for generating large symbolic byte strings

sbytes1024 :: Query [SWord 8]

Convenience functions for generating large symbolic byte strings

mkByte :: Query [SWord 8]

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

Abstract calldata argument generation

symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256)

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

loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM

data BranchInfo

Constructors

BranchInfo

Fields

• _vm :: VM
• _branchCondition :: Maybe Whiff

doInterpret :: Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)

interpret' :: Fetcher -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])

interpret :: Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]

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

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

type Precondition = VM -> SBool

type Postcondition = (VM, VM) -> SBool

checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)

checkAssertions :: Postcondition

verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), 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 (BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo))

Symbolically execute the VM and check all endstates against the postcondition, if available. Returns `Right (Tree BranchInfo)` if the postcondition can be violated, or or `Left (Tree BranchInfo)`, if the postcondition holds for all endstates.

equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)

Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.

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

showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query ()