| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
EVM.SymExec
Synopsis
- sbytes32 :: Query [SWord 8]
- sbytes256 :: Query [SWord 8]
- sbytes512 :: Query [SWord 8]
- sbytes1024 :: Query [SWord 8]
- sbytes128 :: QueryT IO [SWord 8]
- symAbiArg :: AbiType -> Query ([SWord 8], SWord 32)
- symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], SWord 32)
- abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM
- loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SWord 32) -> VM
- interpret :: Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
- maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool
- type Precondition = VM -> SBool
- type Postcondition = (VM, VM) -> SBool
- checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)
- checkAssertions :: Postcondition
- verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
- pruneDeadPaths :: [VM] -> [VM]
- verify :: VM -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)
- equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
- both' :: (a -> b) -> (a, a) -> (b, b)
- showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query ()
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.
abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> StorageModel -> Query VM Source #
loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SWord 32) -> VM Source #
interpret :: Fetcher -> 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 :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM) Source #
verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM) Source #
pruneDeadPaths :: [VM] -> [VM] Source #
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.