hevm 0.47.0 → 0.48.0
raw patch · 19 files changed
+736/−503 lines, 19 filesdep ~asyncdep ~cryptonitePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: async, cryptonite
API changes (from Hackage documentation)
- EVM: NoSuchContract :: Addr -> Error
- EVM.UnitTest: [allowFFI] :: UnitTestOptions -> Bool
- EVM.UnitTest: [testBalanceCall] :: TestVMParams -> W256
- EVM.UnitTest: defaultBalanceForCreated :: W256
- EVM.UnitTest: defaultBalanceForCreator :: W256
+ EVM: InvalidFormat :: Error
+ EVM: [_baseFee] :: Block -> Word
+ EVM: [_txPriorityFee] :: TxState -> Word
+ EVM: [vmoptBaseFee] :: VMOpts -> W256
+ EVM: [vmoptPriorityFee] :: VMOpts -> W256
+ EVM: baseFee :: Lens' Block Word
+ EVM: txPriorityFee :: Lens' TxState Word
+ EVM.Fetch: [QueryAccount] :: Addr -> RpcQuery (ByteString, W256, W256)
+ EVM.Solidity: yul :: Text -> Text -> IO (Maybe ByteString)
+ EVM.Solidity: yul' :: Text -> IO (Text, Text)
+ EVM.Solidity: yulRuntime :: Text -> Text -> IO (Maybe ByteString)
+ EVM.SymExec: Cex :: b -> ProofResult a b c
+ EVM.SymExec: Qed :: a -> ProofResult a b c
+ EVM.SymExec: Timeout :: c -> ProofResult a b c
+ EVM.SymExec: data ProofResult a b c
+ EVM.SymExec: type EquivalenceResult = ProofResult ([VM], [VM]) VM ()
+ EVM.SymExec: type VerifyResult = ProofResult (Tree BranchInfo) (Tree BranchInfo) (Tree BranchInfo)
+ EVM.Transaction: EIP1559Transaction :: TxType
+ EVM.Transaction: [txMaxFeePerGas] :: Transaction -> Maybe W256
+ EVM.Transaction: [txMaxPriorityFeeGas] :: Transaction -> Maybe W256
+ EVM.UnitTest: [askSmtIters] :: UnitTestOptions -> Maybe Integer
+ EVM.UnitTest: [ffiAllowed] :: UnitTestOptions -> Bool
+ EVM.UnitTest: [testBaseFee] :: TestVMParams -> W256
+ EVM.UnitTest: [testPriorityFee] :: TestVMParams -> W256
+ EVM.UnitTest: defaultBalanceForTestContract :: W256
- EVM: Block :: Addr -> SymWord -> Word -> Word -> Word -> Word -> FeeSchedule Integer -> Block
+ EVM: Block :: Addr -> SymWord -> Word -> Word -> Word -> Word -> Word -> FeeSchedule Integer -> Block
- EVM: TxState :: Word -> Word -> Addr -> Addr -> SymWord -> SubState -> Bool -> Map Addr Contract -> TxState
+ EVM: TxState :: Word -> Word -> Word -> Addr -> Addr -> SymWord -> SubState -> Bool -> Map Addr Contract -> TxState
- EVM: VMOpts :: Contract -> (Buffer, SymWord) -> SymWord -> Addr -> SAddr -> Addr -> W256 -> W256 -> W256 -> SymWord -> Addr -> W256 -> W256 -> W256 -> W256 -> FeeSchedule Integer -> W256 -> Bool -> StorageModel -> Map Addr [W256] -> Bool -> VMOpts
+ EVM: VMOpts :: Contract -> (Buffer, SymWord) -> SymWord -> W256 -> Addr -> SAddr -> Addr -> W256 -> W256 -> W256 -> SymWord -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> FeeSchedule Integer -> W256 -> Bool -> StorageModel -> Map Addr [W256] -> Bool -> VMOpts
- EVM.Fetch: rpc :: String -> [Value] -> Value
+ EVM.Fetch: rpc :: String -> [Value] -> Scientific -> Value
- EVM.SymExec: checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
+ EVM.SymExec: checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (VerifyResult, VM)
- EVM.SymExec: doInterpret :: Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)
+ EVM.SymExec: doInterpret :: Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (Tree BranchInfo)
- EVM.SymExec: equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)
+ EVM.SymExec: equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query EquivalenceResult
- EVM.SymExec: interpret :: Fetcher -> Maybe Integer -> Stepper a -> StateT VM Query [a]
+ EVM.SymExec: interpret :: Fetcher -> Maybe Integer -> Maybe Integer -> Stepper a -> StateT VM Query [a]
- EVM.SymExec: interpret' :: Fetcher -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])
+ EVM.SymExec: interpret' :: Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])
- EVM.SymExec: verify :: VM -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo))
+ EVM.SymExec: verify :: VM -> Maybe Integer -> Maybe Integer -> Maybe (BlockNumber, Text) -> Maybe Postcondition -> Query VerifyResult
- EVM.SymExec: verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)
+ EVM.SymExec: verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (VerifyResult, VM)
- EVM.Transaction: Transaction :: ByteString -> W256 -> W256 -> W256 -> W256 -> W256 -> Maybe Addr -> W256 -> W256 -> TxType -> [AccessListEntry] -> Transaction
+ EVM.Transaction: Transaction :: ByteString -> W256 -> Maybe W256 -> W256 -> W256 -> W256 -> Maybe Addr -> W256 -> W256 -> TxType -> [AccessListEntry] -> Maybe W256 -> Maybe W256 -> Transaction
- EVM.Transaction: [txGasPrice] :: Transaction -> W256
+ EVM.Transaction: [txGasPrice] :: Transaction -> Maybe W256
- EVM.UnitTest: TestVMParams :: Addr -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> W256 -> W256 -> TestVMParams
+ EVM.UnitTest: TestVMParams :: Addr -> Addr -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> Addr -> W256 -> W256 -> W256 -> W256 -> W256 -> W256 -> W256 -> TestVMParams
- EVM.UnitTest: UnitTestOptions :: (Query -> IO (EVM ())) -> Maybe Int -> Maybe Integer -> Maybe Int -> Maybe Integer -> Maybe State -> Maybe Text -> Text -> Int -> Maybe (Text, ByteString) -> (VM -> VM) -> DappInfo -> TestVMParams -> Bool -> UnitTestOptions
+ EVM.UnitTest: UnitTestOptions :: (Query -> IO (EVM ())) -> Maybe Int -> Maybe Integer -> Maybe Integer -> Maybe Int -> Maybe Integer -> Maybe State -> Maybe Text -> Text -> Int -> Maybe (Text, ByteString) -> (VM -> VM) -> DappInfo -> TestVMParams -> Bool -> UnitTestOptions
Files
- CHANGELOG.md +254/−177
- hevm-cli/hevm-cli.hs +51/−32
- hevm.cabal +3/−2
- src/EVM.hs +39/−44
- src/EVM/Dev.hs +4/−2
- src/EVM/Emacs.hs +15/−14
- src/EVM/Exec.hs +2/−0
- src/EVM/Facts.hs +1/−2
- src/EVM/Fetch.hs +31/−25
- src/EVM/Solidity.hs +44/−5
- src/EVM/StorageLayout.hs +2/−2
- src/EVM/SymExec.hs +58/−46
- src/EVM/Symbolic.hs +2/−2
- src/EVM/TTY.hs +18/−15
- src/EVM/Transaction.hs +40/−21
- src/EVM/Types.hs +2/−2
- src/EVM/UnitTest.hs +31/−29
- src/EVM/VMTest.hs +42/−12
- test/test.hs +97/−71
CHANGELOG.md view
@@ -1,10 +1,26 @@ # hevm changelog +## Unreleased++## 0.48.0 - 2021-08-03++### Changed++- Updated to London hard fork!+- The configuration variable `DAPP_TEST_BALANCE_CREATE` has been renamed to `DAPP_TEST_BALANCE`+- Default `smttimeout` has been increased to 1 minute.+- A new flag has been added to hevm (`--ask-smt-iterations`) that controls the number of iterations+ at which the symbolic execution engine will stop eager evaluation and begin to query the smt+ solver whether a given branch is reachable or not.+- Contract fetching now happens asynchronously.+- Fixed no contract definition crashes+- Removed NoSuchContract failures+ ## 0.47.0 - 2021-07-01 - A new test runner for checking invariants against random reachable contract states. - `hevm symbolic` can search for solc 0.8 style assertion violations, and a new `--assertions` flag- has been added allowing users to customize which assertions should be reported+ has been added allowing users to customize which assertions should be reported - A new cheatcode `ffi(string[])` that executes an arbitrary command in the system shell ### Changed@@ -67,7 +83,7 @@ ### Fixed - Symbolic execution now generates calldata arguments restricted to the proper ranges,-following the semantics of fuzzing.+ following the semantics of fuzzing. - If the `--address` flag is present in `hevm exec` or `hevm symbolic`, it overrides the contract address at which a contract will be created. - Address pretty printing@@ -138,11 +154,11 @@ - Switched to [PVP](https://github.com/haskell/pvp/blob/master/pvp-faq.md) for version control, starting now at `0.41.0` (MAJOR.MAJOR.MINOR). - z3 updated to 4.8.7 - Generate more interesting values in property based testing,- and implement proper shrinking for all abi values.+ and implement proper shrinking for all abi values. - Fixed soundness bug when using KECCAK or SHA256 opcode/precompile - Fixed an issue in debug mode where backstepping could cause path information to be forgotten - Ensure that pathconditions are consistent when branching, and end the execution with VMFailure: DeadPath if this is not the case-- Fixed a soundness bug where nonzero jumpconditions were assumed to equal one.+- Fixed a soundness bug where nonzero jumpconditions were assumed to equal one. - default `--smttimeout` changed from unlimited to 20 seconds - `hevm symbolic --debug` now respects `--max-iterations` @@ -157,18 +173,20 @@ - hevm is now capable of symbolic execution! ### Changed+ As a result, the types of several registers of the EVM have changed to admit symbolic values as well as concrete ones. - - state.stack: `Word` -> `SymWord`.- - state.memory: `ByteString` -> `[SWord 8]`.- - state.callvalue: `W256` -> `SymWord`.- - state.caller: `Addr` -> `SAddr`.- - state.returndata: `ByteString` -> `[SWord 8]`.- - state.calldata: `ByteString` -> `([SWord 8], (SWord 32))`. The first element is a list of symbolic bytes, the second is the length of calldata. We have `fst calldata !! i .== 0` for all `snd calldata < i`.+- state.stack: `Word` -> `SymWord`.+- state.memory: `ByteString` -> `[SWord 8]`.+- state.callvalue: `W256` -> `SymWord`.+- state.caller: `Addr` -> `SAddr`.+- state.returndata: `ByteString` -> `[SWord 8]`.+- state.calldata: `ByteString` -> `([SWord 8], (SWord 32))`. The first element is a list of symbolic bytes, the second is the length of calldata. We have `fst calldata !! i .== 0` for all `snd calldata < i`. - - tx.value: `W256` -> `SymWord`.+- tx.value: `W256` -> `SymWord`. - - contract.storage: `Map Word Word` -> `Storage`, defined as:+- contract.storage: `Map Word Word` -> `Storage`, defined as:+ ```hs data Storage = Concrete (Map Word SymWord)@@ -177,305 +195,364 @@ ``` ### Added+ New cli commands:- - `hevm symbolic`: search for assertion violations, or step through a symbolic execution in debug mode.- - `hevm equivalence`: compare two programs for equivalence. +- `hevm symbolic`: search for assertion violations, or step through a symbolic execution in debug mode.+- `hevm equivalence`: compare two programs for equivalence.+ See the README for details on usage. The new module `EVM.SymExec` exposes several library functions dealing with symbolic execution. In particular,- - `SymExec.interpret`: implements an operational monad script similar to `TTY.interpret` and `Stepper.interpret`, but returns a list of final VM states rather than a single VM.- - `SymExec.verify`: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition. +- `SymExec.interpret`: implements an operational monad script similar to `TTY.interpret` and `Stepper.interpret`, but returns a list of final VM states rather than a single VM.+- `SymExec.verify`: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition.+ ### Removed The concrete versions of a lot of arithmetic operations, replaced with their more general symbolic counterpart. - ## 0.39 - 2020-07-13- - Exposes abi encoding to cli- - Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`- - Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.- - `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`. +- Exposes abi encoding to cli+- Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`+- Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.+- `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`.+ ## 0.38 - 2020-04-23- - Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).- - Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).- - Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358). +- Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).+- Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).+- Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358).+ ## 0.37 - 2020-03-24- - Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files. +- Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files.+ ## 0.36 - 2020-01-07- - Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)- - Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).- - Make InvalidTx a fatal error for vm tests and ci.- - Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.- - Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.- - Correct gas readouts for unit tests- - Prevent crash when trying to jump to next source code point if source code is missing +- Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)+- Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).+- Make InvalidTx a fatal error for vm tests and ci.+- Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.+- Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.+- Correct gas readouts for unit tests+- Prevent crash when trying to jump to next source code point if source code is missing+ ## 0.35 - 2019-11-02- - Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)- - RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)- - Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)- - Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f) +- Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)+- RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)+- Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)+- Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f)+ ## 0.34 - 2019-08-28- - handle new solc bzzr metadata in codehash for source map- - show VM hex outputs as hexadecimal- - rpc defaults to latest block- - `hevm interactive`:- - fix rpc fetch- - scrollable memory pane- - Fix regression in VMTest compliance.- - `hevm exec` ergonomics:- - Allow code/calldata prefixed with 0x- - create transactions with specific caller nonce- - interactive help pane- - memory pane scrolling +- handle new solc bzzr metadata in codehash for source map+- show VM hex outputs as hexadecimal+- rpc defaults to latest block+- `hevm interactive`:+- fix rpc fetch+- scrollable memory pane+- Fix regression in VMTest compliance.+- `hevm exec` ergonomics:+- Allow code/calldata prefixed with 0x+- create transactions with specific caller nonce+- interactive help pane+- memory pane scrolling+ ## 0.33 - 2019-08-06- - Full compliance with the [General State Tests][245] (with the- BlockchainTest format), using the Yellow and Jello papers as- reference, for Constantinople Fix (aka Petersburg). Including:- - full precompile support- - correct substate accounting, including touched accounts,- selfdestructs and refunds- - memory read/write semantics- - many gas cost corrections- - Show more information for non solc bytecode in interactive view- (trace and storage)- - Help text for all cli options- - Enable `--debug` flag in `hevm dapp-test` +- Full compliance with the [General State Tests][245] (with the+ BlockchainTest format), using the Yellow and Jello papers as+ reference, for Constantinople Fix (aka Petersburg). Including:+- full precompile support+- correct substate accounting, including touched accounts,+ selfdestructs and refunds+- memory read/write semantics+- many gas cost corrections+- Show more information for non solc bytecode in interactive view+ (trace and storage)+- Help text for all cli options+- Enable `--debug` flag in `hevm dapp-test`+ [245]: https://github.com/dapphub/dapptools/pull/245 ## 0.32 - 2019-06-14- - Fix dapp-test [nonce initialisation bug][224] +- Fix dapp-test [nonce initialisation bug][224]+ [224]: https://github.com/dapphub/dapptools/pull/224 ## 0.31 - 2019-05-29- - Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,- ECPAIRING, MODEXP- - Show the hevm version with `hevm version`- - Interactive mode:- - no longer exits on reaching halt- - new shortcuts: 'a' / 'e' for start / end- - allow returning to test picker screen- - Exact integer formatting in dapp-test and tty +- Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,+ ECPAIRING, MODEXP+- Show the hevm version with `hevm version`+- Interactive mode:+- no longer exits on reaching halt+- new shortcuts: 'a' / 'e' for start / end+- allow returning to test picker screen+- Exact integer formatting in dapp-test and tty+ ## 0.30 - 2019-05-09- - Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`- - Working stack build +- Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`+- Working stack build+ ## 0.29 - 2019-04-03- - Significant jump in compliance with client tests- - Add support for running GeneralStateTests +- Significant jump in compliance with client tests+- Add support for running GeneralStateTests+ ## 0.28 - 2019-03-22- - Fix delegatecall gas metering, as reported in- https://github.com/dapphub/dapptools/issues/34 +- Fix delegatecall gas metering, as reported in+ https://github.com/dapphub/dapptools/issues/34+ ## 0.27 - 2019-02-06- - Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)- related to SemVer ranges in Solidity version pragmas +- Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)+ related to SemVer ranges in Solidity version pragmas+ ## 0.26 - 2019-02-05- - Format Solidity Error(string) messages in trace +- Format Solidity Error(string) messages in trace+ ## 0.25 - 2019-02-04- - Add SHL, SHR and SAR opcodes +- Add SHL, SHR and SAR opcodes+ ## 0.24 - 2019-01-23- - Fix STATICCALL for precompiled contracts- - Assume Solidity 0.5.2 in tests +- Fix STATICCALL for precompiled contracts+- Assume Solidity 0.5.2 in tests+ ## 0.23 - 2018-12-12- - Show passing test traces with --verbose flag +- Show passing test traces with --verbose flag+ ## 0.22 - 2018-11-13- - Simple memory view in TTY +- Simple memory view in TTY+ ## 0.21 - 2018-10-29- - Fix Hackage package by including C header files for ethjet +- Fix Hackage package by including C header files for ethjet+ ## 0.20 - 2018-10-27- - Parse constructor inputs from Solidity AST +- Parse constructor inputs from Solidity AST+ ## 0.19 - 2018-10-09- - Enable experimental 'cheat' address, allowing for modification of the- EVM environment from within the tests. Currently just the block- timestamp can be adjusted. +- Enable experimental 'cheat' address, allowing for modification of the+ EVM environment from within the tests. Currently just the block+ timestamp can be adjusted.+ ## 0.18 - 2018-10-09- - Fix [duplicate address bug](https://github.com/dapphub/dapptools/issues/70) +- Fix [duplicate address bug](https://github.com/dapphub/dapptools/issues/70)+ ## 0.17 - 2018-10-05- - Semigroup/Monoid fix +- Semigroup/Monoid fix+ ## 0.16 - 2018-09-19- - Move ethjet into hevm +- Move ethjet into hevm+ ## [0.15] - 2018-05-09- - Fix SDIV/SMOD definitions for extreme case +- Fix SDIV/SMOD definitions for extreme case+ ## [0.14.1] - 2018-04-17- - Improve PC display in TTY +- Improve PC display in TTY+ ## [0.14] - 2018-03-08- - Implement STATICCALL +- Implement STATICCALL+ ## [0.13] - 2018-02-28- - Require specific block number for RPC debugging- - Implement RETURNDATACOPY and RETURNDATASIZE- - Fix bug where created contracts didn't get their balance +- Require specific block number for RPC debugging+- Implement RETURNDATACOPY and RETURNDATASIZE+- Fix bug where created contracts didn't get their balance+ ## [0.12.3] - 2017-12-19- - More useful RPC debugging because we strip the entire BZZR metadata +- More useful RPC debugging because we strip the entire BZZR metadata+ ## [0.12.2] - 2017-12-17- - Experimental new ecrecover implementation via libethjet- - Correct error checking for setUp() invocations +- Experimental new ecrecover implementation via libethjet+- Correct error checking for setUp() invocations+ ## [0.12.1] - 2017-11-28- - Test name regex matching via --match- - Fixed source map parsing bug when used with solc --optimize- - TTY: fix a padding-related display glitch +- Test name regex matching via --match+- Fixed source map parsing bug when used with solc --optimize+- TTY: fix a padding-related display glitch+ ## [0.12] - 2017-11-14- - Use 13 different environment variables to control block parameters- for unit testing, e.g. block number, timestamp, initial balance, etc. - Full list:+- Use 13 different environment variables to control block parameters+ for unit testing, e.g. block number, timestamp, initial balance, etc. - - `DAPP_TEST_ADDRESS`- - `DAPP_TEST_CALLER`- - `DAPP_TEST_ORIGIN`- - `DAPP_TEST_GAS_CREATE`- - `DAPP_TEST_GAS_CALL`- - `DAPP_TEST_BALANCE_CREATE`- - `DAPP_TEST_BALANCE_CALL`- - `DAPP_TEST_COINBASE`- - `DAPP_TEST_NUMBER`- - `DAPP_TEST_TIMESTAMP`- - `DAPP_TEST_GAS_LIMIT`- - `DAPP_TEST_GAS_PRICE`- - `DAPP_TEST_DIFFICULTY`+ Full list: + - `DAPP_TEST_ADDRESS`+ - `DAPP_TEST_CALLER`+ - `DAPP_TEST_ORIGIN`+ - `DAPP_TEST_GAS_CREATE`+ - `DAPP_TEST_GAS_CALL`+ - `DAPP_TEST_BALANCE_CREATE`+ - `DAPP_TEST_BALANCE_CALL`+ - `DAPP_TEST_COINBASE`+ - `DAPP_TEST_NUMBER`+ - `DAPP_TEST_TIMESTAMP`+ - `DAPP_TEST_GAS_LIMIT`+ - `DAPP_TEST_GAS_PRICE`+ - `DAPP_TEST_DIFFICULTY`+ ## [0.11.5] - 2017-11-14- - Use --state with --exec --debug +- Use --state with --exec --debug+ ## [0.11.4] - 2017-11-12- - Fix bug when unit test contract has creations in constructor +- Fix bug when unit test contract has creations in constructor+ ## [0.11.3] - 2017-11-08- - Fix array support in ABI module +- Fix array support in ABI module+ ## [0.11.2] - 2017-11-04- - TTY: show a help bar with key bindings at the bottom +- TTY: show a help bar with key bindings at the bottom+ ## [0.11.1] - 2017-11-02- - TTY: fix a display glitch- - TTY: improve display of ABI hashes on the stack +- TTY: fix a display glitch+- TTY: improve display of ABI hashes on the stack+ ## [0.11] - 2017-10-31- - Add "hevm flatten" for Etherscan-ish source code concatenation- - Simplify code by removing concrete/symbolic machine abstraction +- Add "hevm flatten" for Etherscan-ish source code concatenation+- Simplify code by removing concrete/symbolic machine abstraction+ ## [0.10.9] - 2017-10-23- - Fix bugs in ABI formatting +- Fix bugs in ABI formatting+ ## [0.10.7] - 2017-10-19- - Fix library linking bug- - Fix gas consumption of DELEGATECALL- - Better error tracing- - Experimental "contract browser" (stupid list of addresses) +- Fix library linking bug+- Fix gas consumption of DELEGATECALL+- Better error tracing+- Experimental "contract browser" (stupid list of addresses)+ ## [0.10.6] - 2017-10-19- - Enable library linking for unit tests and debugger- - Use the same default gas/balance values as `ethrun` +- Enable library linking for unit tests and debugger+- Use the same default gas/balance values as `ethrun`+ ## [0.10.5] - 2017-10-17- - Better trace output including arguments and return values- - Proof of concept coverage analysis via `dapp-test --coverage` +- Better trace output including arguments and return values+- Proof of concept coverage analysis via `dapp-test --coverage`+ ## [0.10] - 2017-10-10- - Enable new trace output by default for failing tests- - Exit with failure code from test runner when tests fail- - More fixes to improve Ethereum test suite compliance +- Enable new trace output by default for failing tests+- Exit with failure code from test runner when tests fail+- More fixes to improve Ethereum test suite compliance+ ## [0.9.5] - 2017-10-06- - Prototype of new trace output with `hevm dapp-test --verbose`- - Nicer trace tree in the TTY debugger- - Many fixes to improve Ethereum test suite compliance +- Prototype of new trace output with `hevm dapp-test --verbose`+- Nicer trace tree in the TTY debugger+- Many fixes to improve Ethereum test suite compliance+ ## [0.9] - 2017-09-29- - Integrates with live chains via RPC (read-only)- - Exposes a special contract address with test-related functionality (time warp) +- Integrates with live chains via RPC (read-only)+- Exposes a special contract address with test-related functionality (time warp)+ ## [0.8.5] - 2017-09-22- - Renames `hevm` from its maiden name `hsevm` :sparkles: +- Renames `hevm` from its maiden name `hsevm` :sparkles:+ ## [0.8] - 2017-09-21- - Implements gas metering (Metropolis rules by default)- - Shows gas counter in the terminal interface- - Enables debugger for consensus test executions- - Consensus test runner script with HTML reporting- - Passes 564 of the `VMTests`; fails 115 (see [0.8 test report])- - Command line options for specifying initial gas amounts and balances- - Improved TTY UI layout +- Implements gas metering (Metropolis rules by default)+- Shows gas counter in the terminal interface+- Enables debugger for consensus test executions+- Consensus test runner script with HTML reporting+- Passes 564 of the `VMTests`; fails 115 (see [0.8 test report])+- Command line options for specifying initial gas amounts and balances+- Improved TTY UI layout+ ## [0.7] - 2017-09-07- - Can save and load contract states to disk using a Git-backed store (only `--exec`)- - Can debug raw EVM bytecode using `exec --debug`- - Fixes `exec --value`- - Has smarter defaults for command line when running tests or debugging- - Fixes bug with `MSIZE` in `CALL` context +- Can save and load contract states to disk using a Git-backed store (only `--exec`)+- Can debug raw EVM bytecode using `exec --debug`+- Fixes `exec --value`+- Has smarter defaults for command line when running tests or debugging+- Fixes bug with `MSIZE` in `CALL` context+ ## [0.6.5] - 2017-09-01- - Fixes `exec` with regards to exit codes and error messages +- Fixes `exec` with regards to exit codes and error messages+ ## [0.6.1] - 2017-08-03- - TTY: Adds command `C-n` in TTY for "stepping over" +- TTY: Adds command `C-n` in TTY for "stepping over"+ ## [0.6] - 2017-08-03- - TTY: Adds second line to stack entries with humanized formatting- - TTY: Gets rid of the separate log pane in favor of a unified trace pane +- TTY: Adds second line to stack entries with humanized formatting+- TTY: Gets rid of the separate log pane in favor of a unified trace pane+ ## [0.5] - 2017-08-02- - TTY: Adds `p` command for stepping backwards- - Adds ability to track origins of stack and heap words- - Tracks Keccak preimage for words that come from the `SHA3` instruction +- TTY: Adds `p` command for stepping backwards+- Adds ability to track origins of stack and heap words+- Tracks Keccak preimage for words that come from the `SHA3` instruction+ ## [0.4] - 2017-07-31- - Parallelizes unit test runner- - Improves speed by changing representation of memory- - Internal refactoring for future support of symbolic execution- - Adds logs to the trace pane +- Parallelizes unit test runner+- Improves speed by changing representation of memory+- Internal refactoring for future support of symbolic execution+- Adds logs to the trace pane+ ## [0.3.2] - 2017-06-17- - Adds `REVERT` opcode- - Sets `TIMESTAMP` value to `1` in unit tests +- Adds `REVERT` opcode+- Sets `TIMESTAMP` value to `1` in unit tests+ ## [0.3.0] - 2017-06-14- - Reverts contract state after `CALL` fails- - Improves test runner console output +- Reverts contract state after `CALL` fails+- Improves test runner console output+ ## [0.2.0] - 2017-06-13- - Fixes bug in `CALL` +- Fixes bug in `CALL`+ ## [0.1.0.1] - 2017-03-31- - Highlights Solidity exactly on character level- - Adds `N` command for stepping by Solidity source position instead of by opcode +- Highlights Solidity exactly on character level+- Adds `N` command for stepping by Solidity source position instead of by opcode+ ## 0.1.0.0 - 2017-03-29- - First release -[0.8 test report]: https://hydra.dapp.tools/build/135/download/1/index.html+- First release +[0.8 test report]: https://hydra.dapp.tools/build/135/download/1/index.html [0.12]: https://github.com/dapphub/hevm/compare/0.11.5...0.12 [0.11.5]: https://github.com/dapphub/hevm/compare/0.11.4...0.11.5 [0.11.4]: https://github.com/dapphub/hevm/compare/0.11.3...0.11.4
hevm-cli/hevm-cli.hs view
@@ -104,6 +104,8 @@ , gas :: w ::: Maybe W256 <?> "Tx: gas amount" , number :: w ::: Maybe W256 <?> "Block: number" , timestamp :: w ::: Maybe W256 <?> "Block: timestamp"+ , basefee :: w ::: Maybe W256 <?> "Block: base fee"+ , priorityFee :: w ::: Maybe W256 <?> "Tx: priority fee" , gaslimit :: w ::: Maybe W256 <?> "Tx: gas limit" , gasprice :: w ::: Maybe W256 <?> "Tx: gas price" , create :: w ::: Bool <?> "Tx: creation"@@ -125,21 +127,23 @@ , debug :: w ::: Bool <?> "Run interactively" , getModels :: w ::: Bool <?> "Print example testcase for each execution path" , showTree :: w ::: Bool <?> "Print branches explored in tree view"- , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 30000)"+ , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 60000)" , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point" , solver :: w ::: Maybe Text <?> "Used SMT solver: z3 (default) or cvc4" , smtdebug :: w ::: Bool <?> "Print smt queries sent to the solver" , assertions :: w ::: Maybe [Word256] <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"+ , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)" } | Equivalence -- prove equivalence between two programs- { codeA :: w ::: ByteString <?> "Bytecode of the first program"- , codeB :: w ::: ByteString <?> "Bytecode of the second program"- , sig :: w ::: Maybe Text <?> "Signature of types to decode / encode"- , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 30000)"- , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"- , solver :: w ::: Maybe Text <?> "Used SMT solver: z3 (default) or cvc4"- , smtoutput :: w ::: Bool <?> "Print verbose smt output"- , smtdebug :: w ::: Bool <?> "Print smt queries sent to the solver"+ { codeA :: w ::: ByteString <?> "Bytecode of the first program"+ , codeB :: w ::: ByteString <?> "Bytecode of the second program"+ , sig :: w ::: Maybe Text <?> "Signature of types to decode / encode"+ , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 60000)"+ , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"+ , solver :: w ::: Maybe Text <?> "Used SMT solver: z3 (default) or cvc4"+ , smtoutput :: w ::: Bool <?> "Print verbose smt output"+ , smtdebug :: w ::: Bool <?> "Print smt queries sent to the solver"+ , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)" } | Exec -- Execute a given program with specified env & calldata { code :: w ::: Maybe ByteString <?> "Program bytecode"@@ -153,6 +157,8 @@ , gas :: w ::: Maybe W256 <?> "Tx: gas amount" , number :: w ::: Maybe W256 <?> "Block: number" , timestamp :: w ::: Maybe W256 <?> "Block: timestamp"+ , basefee :: w ::: Maybe W256 <?> "Block: base fee"+ , priorityFee :: w ::: Maybe W256 <?> "Tx: priority fee" , gaslimit :: w ::: Maybe W256 <?> "Tx: gas limit" , gasprice :: w ::: Maybe W256 <?> "Tx: gas price" , create :: w ::: Bool <?> "Tx: creation"@@ -183,11 +189,12 @@ , state :: w ::: Maybe String <?> "Path to state repository" , cache :: w ::: Maybe String <?> "Path to rpc cache repository" , match :: w ::: Maybe String <?> "Test case filter - only run methods matching regex"- , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 30000)"- , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point" , solver :: w ::: Maybe Text <?> "Used SMT solver: z3 (default) or cvc4" , smtdebug :: w ::: Bool <?> "Print smt queries sent to the solver" , ffi :: w ::: Bool <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"+ , smttimeout :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 60000)"+ , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"+ , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)" } | BcTest -- Run an Ethereum Blockhain/GeneralState test { file :: w ::: String <?> "Path to .json test file"@@ -288,6 +295,7 @@ Just url -> EVM.Fetch.oracle (Just state) (Just (block', url)) True Nothing -> EVM.Fetch.oracle (Just state) Nothing True , EVM.UnitTest.maxIter = maxIterations cmd+ , EVM.UnitTest.askSmtIters = askSmtIterations cmd , EVM.UnitTest.smtTimeout = smttimeout cmd , EVM.UnitTest.solver = solver cmd , EVM.UnitTest.smtState = Just state@@ -301,7 +309,7 @@ , EVM.UnitTest.vmModifier = vmModifier , EVM.UnitTest.testParams = params , EVM.UnitTest.dapp = srcInfo- , EVM.UnitTest.allowFFI = ffi cmd+ , EVM.UnitTest.ffiAllowed = ffi cmd } main :: IO ()@@ -311,7 +319,7 @@ root = fromMaybe "." (dappRoot cmd) case cmd of Version {} -> putStrLn (showVersion Paths.version)- Symbolic {} -> assert cmd+ Symbolic {} -> withCurrentDirectory root $ assert cmd Equivalence {} -> equivalence cmd Exec {} -> launchExec cmd@@ -419,17 +427,20 @@ return $ Just (view methodSignature method', snd <$> view methodInputs method') void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) . query $- equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case- Right vm -> do io $ putStrLn "Not equal!"- io $ putStrLn "Counterexample:"- showCounterexample vm maybeSignature- io exitFailure- Left (postAs, postBs) -> io $ do+ equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) (askSmtIterations cmd) maybeSignature >>= \case+ Cex vm -> do+ io $ putStrLn "Not equal!"+ io $ putStrLn "Counterexample:"+ showCounterexample vm maybeSignature+ io exitFailure+ Qed (postAs, postBs) -> io $ do putStrLn $ "Explored: " <> show (length postAs) <> " execution paths of A and: " <> show (length postBs) <> " paths of B." putStrLn "No discrepancies found."-+ Timeout () -> io $ do+ hPutStr stderr "Solver timeout!"+ exitFailure -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)` runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a@@ -438,7 +449,7 @@ | solver == Just "z3" = runwithz3 | solver == Nothing = runwithz3 | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"- where timeout = fromMaybe 30000 maybeTimeout+ where timeout = fromMaybe 60000 maybeTimeout runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb runwithcvc4 = do setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)@@ -515,13 +526,15 @@ runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do preState <- symvmFromCommand cmd let errCodes = fromMaybe defaultPanicCodes (assertions cmd)- verify preState (maxIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case- Right tree -> do+ verify preState (maxIterations cmd) (askSmtIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case+ Cex tree -> do io $ putStrLn "Assertion violation found." showCounterexample preState maybesig treeShowing tree io $ exitWith (ExitFailure 1)- Left tree -> do+ Timeout _ -> do+ io $ exitWith (ExitFailure 1)+ Qed tree -> do io $ putStrLn $ "Explored: " <> show (length tree) <> " branches without assertion violations" treeShowing tree@@ -698,12 +711,13 @@ vmFromCommand cmd = do withCache <- applyCache (state cmd, cache cmd) - (miner,ts,blockNum,diff) <- case rpc cmd of- Nothing -> return (0,0,0,0)+ (miner,ts,baseFee,blockNum,diff) <- case rpc cmd of+ Nothing -> return (0,0,0,0,0) Just url -> EVM.Fetch.fetchBlockFrom block' url >>= \case Nothing -> error "Could not fetch block" Just EVM.Block{..} -> return (_coinbase , wordValue $ forceLit _timestamp+ , wordValue _baseFee , wordValue _number , wordValue _difficulty )@@ -736,7 +750,7 @@ (_, _, Nothing) -> error "must provide at least (rpc + address) or code" - return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract)+ return $ VMTest.initTx $ withCache (vm0 baseFee miner ts blockNum diff contract) where decipher = hexByteString "bytes" . strip0x block' = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)@@ -749,7 +763,7 @@ then addr address (createAddress origin' (word nonce 0)) else addr address 0xacab - vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts+ vm0 baseFee miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts { EVM.vmoptContract = c , EVM.vmoptCalldata = (calldata', litWord (num $ len calldata')) , EVM.vmoptValue = w256lit value'@@ -757,6 +771,8 @@ , EVM.vmoptCaller = litAddr caller' , EVM.vmoptOrigin = origin' , EVM.vmoptGas = word gas 0+ , EVM.vmoptBaseFee = baseFee+ , EVM.vmoptPriorityFee = word priorityFee 0 , EVM.vmoptGaslimit = word gas 0 , EVM.vmoptCoinbase = addr coinbase miner , EVM.vmoptNumber = word number blockNum@@ -779,12 +795,13 @@ symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM symvmFromCommand cmd = do - (miner,blockNum,diff) <- case rpc cmd of- Nothing -> return (0,0,0)+ (miner,blockNum,baseFee,diff) <- case rpc cmd of+ Nothing -> return (0,0,0,0) Just url -> io $ EVM.Fetch.fetchBlockFrom block' url >>= \case Nothing -> error "Could not fetch block" Just EVM.Block{..} -> return (_coinbase , wordValue _number+ , wordValue _baseFee , wordValue _difficulty ) @@ -844,7 +861,7 @@ (_, _, Nothing) -> error "must provide at least (rpc + address) or code" - return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract')+ return $ (VMTest.initTx $ withCache $ vm0 baseFee miner ts blockNum diff cdlen calldata' callvalue' caller' contract') & over EVM.constraints (<> [pathCond]) & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store @@ -856,7 +873,7 @@ address' = if create cmd then addr address (createAddress origin' (word nonce 0)) else addr address 0xacab- vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts+ vm0 baseFee miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts { EVM.vmoptContract = c , EVM.vmoptCalldata = (calldata', cdlen) , EVM.vmoptValue = callvalue'@@ -865,6 +882,8 @@ , EVM.vmoptOrigin = origin' , EVM.vmoptGas = word gas 0xffffffffffffffff , EVM.vmoptGaslimit = word gas 0xffffffffffffffff+ , EVM.vmoptBaseFee = baseFee+ , EVM.vmoptPriorityFee = word priorityFee 0 , EVM.vmoptCoinbase = addr coinbase miner , EVM.vmoptNumber = word number blockNum , EVM.vmoptTimestamp = ts
hevm.cabal view
@@ -2,7 +2,7 @@ name: hevm version:- 0.47.0+ 0.48.0 synopsis: Ethereum virtual machine evaluator description:@@ -81,6 +81,7 @@ ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h build-depends: QuickCheck >= 2.13.2 && < 2.15,+ async == 2.2.3, Decimal >= 0.5.1 && < 0.6, containers >= 0.6.0 && < 0.7, deepseq >= 1.4.4 && < 1.5,@@ -104,7 +105,7 @@ filepath >= 1.4.2 && < 1.5, vty >= 5.25.1 && < 5.34, cereal >= 0.5.8 && < 0.6,- cryptonite >= 0.27 && < 0.29,+ cryptonite >= 0.27 && <= 0.29, memory >= 0.14.18 && < 0.16, data-dword >= 0.3.1 && < 0.4, fgl >= 5.7.0 && < 5.8,
src/EVM.hs view
@@ -75,7 +75,6 @@ | StackUnderrun | BadJumpDestination | Revert ByteString- | NoSuchContract Addr | OutOfGas Word Word | BadCheatCode (Maybe Word32) | StackLimitExceeded@@ -86,6 +85,7 @@ | InvalidMemoryAccess | CallDepthLimitReached | MaxCodeSizeExceeded Word Word+ | InvalidFormat | PrecompileFailure | UnexpectedSymbolicArg | DeadPath@@ -195,6 +195,7 @@ { vmoptContract :: Contract , vmoptCalldata :: (Buffer, SymWord) , vmoptValue :: SymWord+ , vmoptPriorityFee :: W256 , vmoptAddress :: Addr , vmoptCaller :: SAddr , vmoptOrigin :: Addr@@ -207,6 +208,7 @@ , vmoptMaxCodeSize :: W256 , vmoptBlockGaslimit :: W256 , vmoptGasprice :: W256+ , vmoptBaseFee :: W256 , vmoptSchedule :: FeeSchedule Integer , vmoptChainId :: W256 , vmoptCreate :: Bool@@ -269,6 +271,7 @@ data TxState = TxState { _gasprice :: Word , _txgaslimit :: Word+ , _txPriorityFee :: Word , _origin :: Addr , _toAddr :: Addr , _value :: SymWord@@ -377,6 +380,7 @@ , _number :: Word , _difficulty :: Word , _gaslimit :: Word+ , _baseFee :: Word , _maxCodeSize :: Word , _schedule :: FeeSchedule Integer } deriving Show@@ -460,6 +464,7 @@ , _tx = TxState { _gasprice = w256 $ vmoptGasprice o , _txgaslimit = w256 $ vmoptGaslimit o+ , _txPriorityFee = w256 $ vmoptPriorityFee o , _origin = txorigin , _toAddr = txtoAddr , _value = vmoptValue o@@ -478,6 +483,7 @@ , _difficulty = w256 $ vmoptDifficulty o , _maxCodeSize = w256 $ vmoptMaxCodeSize o , _gaslimit = w256 $ vmoptBlockGaslimit o+ , _baseFee = w256 $ vmoptBaseFee o , _schedule = vmoptSchedule o } , _state = FrameState@@ -963,6 +969,11 @@ limitStack 1 . burn g_low $ next >> push (view balance this) + -- op: BASEFEE+ 0x48 ->+ limitStack 1 . burn g_base $+ next >> push (the block baseFee)+ -- op: POP 0x50 -> case stk of@@ -1052,12 +1063,12 @@ unless (current' == new') $ if current' == original then when (original /= 0 && new' == 0) $- refund r_sclear+ refund (g_sreset + g_access_list_storage_key) else do when (original /= 0) $ if new' == 0- then refund r_sclear- else unRefund r_sclear+ then refund (g_sreset + g_access_list_storage_key)+ else unRefund (g_sreset + g_access_list_storage_key) when (original == new') $ if original == 0 then refund (g_sset - g_sload)@@ -1198,31 +1209,24 @@ output = readMemory xOffset xSize vm codesize = num (len output) maxsize = the block maxCodeSize- case view frames vm of- [] ->- case (the tx isCreate) of- True ->- if codesize > maxsize- then- finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))- else- burn (g_codedeposit * num codesize) $- finishFrame (FrameReturned output)- False ->+ creation = case view frames vm of+ [] -> the tx isCreate+ frame:_ -> case view frameContext frame of+ CreationContext {} -> True+ CallContext {} -> False+ if creation+ then+ if codesize > maxsize+ then+ finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))+ else+ if isConcretely (readByteOrZero 0 output) ((==) 0xef)+ then finishFrame $ FrameErrored InvalidFormat+ else do+ burn (g_codedeposit * num codesize) $ finishFrame (FrameReturned output)- (frame: _) -> do- let- context = view frameContext frame- case context of- CreationContext {} ->- if codesize > maxsize- then- finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))- else- burn (g_codedeposit * num codesize) $- finishFrame (FrameReturned output)- CallContext {} ->- finishFrame (FrameReturned output)+ else+ finishFrame (FrameReturned output) _ -> underrun -- op: DELEGATECALL@@ -1299,8 +1303,6 @@ then num g_selfdestruct_newaccount else 0 burn (g_selfdestruct + c_new + cost) $ do- destructs <- use (tx . substate . selfdestructs)- unless (elem self destructs) $ refund r_selfdestruct selfdestruct self touchAccount xTo @@ -1621,9 +1623,9 @@ condition' (fst <$> pathconds) choosePath where condition' = simplifyCondition condition whiff- -- Only one path is possible choosePath :: BranchCondition -> EVM ()+ -- Only one path is possible choosePath (Case v) = do assign result Nothing pushTo constraints $ if v then (condition', whiff) else (sNot condition', IsZero whiff) iteration <- use (iterations . at codeloc . non 0)@@ -1652,12 +1654,7 @@ (\c -> do assign (cache . fetched . at addr) (Just c) assign (env . contracts . at addr) (Just c) assign result Nothing- tryContinue c)- where- tryContinue c =- if (view external c) && (accountEmpty c)- then vmError . NoSuchContract $ addr- else continue c+ continue c) readStorage :: Storage -> SymWord -> Maybe (SymWord) readStorage (Symbolic _ s) (S w loc) = Just $ S (FromStorage w s) $ readArray s loc@@ -1750,15 +1747,17 @@ miner <- use (block . coinbase) blockReward <- num . r_block <$> (use (block . schedule)) gasPrice <- use (tx . gasprice)+ priorityFee <- use (tx . txPriorityFee) gasLimit <- use (tx . txgaslimit) gasRemaining <- use (state . gas) let gasUsed = gasLimit - gasRemaining- cappedRefund = min (quot gasUsed 2) (num sumRefunds)+ cappedRefund = min (quot gasUsed 5) (num sumRefunds) originPay = (gasRemaining + cappedRefund) * gasPrice- minerPay = gasPrice * (gasUsed - cappedRefund) + minerPay = priorityFee * gasUsed+ modifying (env . contracts) (Map.adjust (over balance (+ originPay)) txOrigin) modifying (env . contracts)@@ -2086,11 +2085,7 @@ callChecks this gasGiven xContext' xTo' xValue xInOffset xInSize xOutOffset xOutSize xs $ \xGas -> do vm0 <- get- fetchAccount xTo' . const $- preuse (env . contracts . ix xTo') >>= \case- Nothing ->- vmError (NoSuchContract xTo')- Just target -> do+ fetchAccount xTo' $ \target -> burn xGas $ do let newContext = CallContext { callContextTarget = xTo'
src/EVM/Dev.hs view
@@ -63,6 +63,7 @@ { oracle = EVM.Fetch.zero , verbose = Nothing , maxIter = Nothing+ , askSmtIters = Nothing , smtTimeout = Nothing , smtState = Nothing , solver = Nothing@@ -73,7 +74,7 @@ , dapp = emptyDapp , testParams = params , maxDepth = Nothing- , allowFFI = False+ , ffiAllowed = False } readSolc path >>= \case@@ -122,6 +123,7 @@ { oracle = EVM.Fetch.zero , verbose = Nothing , maxIter = Nothing+ , askSmtIters = Nothing , smtTimeout = Nothing , smtState = Nothing , solver = Nothing@@ -132,7 +134,7 @@ , dapp = emptyDapp , testParams = params , maxDepth = Nothing- , allowFFI = False+ , ffiAllowed = False } EVM.TTY.main testOpts root path
src/EVM/Emacs.hs view
@@ -505,20 +505,21 @@ defaultUnitTestOptions = do params <- liftIO $ getParametersFromEnvironmentVariables Nothing pure UnitTestOptions- { oracle = Fetch.zero- , verbose = Nothing- , maxIter = Nothing- , smtTimeout = Nothing- , smtState = Nothing- , solver = Nothing- , match = ""- , fuzzRuns = 100- , replay = Nothing- , vmModifier = id- , dapp = emptyDapp- , testParams = params- , maxDepth = Nothing- , allowFFI = False+ { oracle = Fetch.zero+ , verbose = Nothing+ , maxIter = Nothing+ , askSmtIters = Nothing+ , smtTimeout = Nothing+ , smtState = Nothing+ , solver = Nothing+ , match = ""+ , fuzzRuns = 100+ , replay = Nothing+ , vmModifier = id+ , dapp = emptyDapp+ , testParams = params+ , maxDepth = Nothing+ , ffiAllowed = False } initialStateForTest
src/EVM/Exec.hs view
@@ -35,6 +35,8 @@ , vmoptDifficulty = 0 , vmoptGas = 0xffffffffffffffff , vmoptGaslimit = 0xffffffffffffffff+ , vmoptBaseFee = 0+ , vmoptPriorityFee = 0 , vmoptMaxCodeSize = 0xffffffff , vmoptSchedule = FeeSchedule.berlin , vmoptChainId = 1
src/EVM/Facts.hs view
@@ -47,7 +47,6 @@ import Control.Lens (view, set, at, ix, (&), over, assign) import Control.Monad.State.Strict (execState, when) import Data.ByteString (ByteString)-import Data.Monoid ((<>)) import Data.Ord (comparing) import Data.Set (Set) import Text.Read (readMaybe)@@ -119,7 +118,7 @@ , NonceFact a (view nonce x) , CodeFact a b ]- SymbolicBuffer b ->+ SymbolicBuffer _ -> -- here simply ignore storing the bytecode storageFacts a x ++ [ BalanceFact a (view balance x)
src/EVM/Fetch.hs view
@@ -5,6 +5,7 @@ module EVM.Fetch where import Prelude hiding (Word)+import Data.Scientific import EVM.ABI import EVM.Types (Addr, w256, W256, hexText, Word, Buffer(..))@@ -16,12 +17,12 @@ import Control.Lens hiding ((.=)) import Control.Monad.Reader-import Control.Monad.Trans.Maybe import Data.SBV.Trans.Control import qualified Data.SBV.Internals as SBV import Data.SBV.Trans hiding (Word) import Data.Aeson import Data.Aeson.Lens+import Control.Concurrent.Async import qualified Data.ByteString as BS import Data.Text (Text, unpack, pack) @@ -34,6 +35,7 @@ -- | Abstract representation of an RPC fetch request data RpcQuery a where+ QueryAccount :: Addr -> RpcQuery (BS.ByteString, W256, W256) QueryCode :: Addr -> RpcQuery BS.ByteString QueryBlock :: RpcQuery Block QueryBalance :: Addr -> RpcQuery W256@@ -45,10 +47,10 @@ deriving instance Show (RpcQuery a) -rpc :: String -> [Value] -> Value-rpc method args = object+rpc :: String -> [Value] -> Scientific -> Value+rpc method args i = object [ "jsonrpc" .= ("2.0" :: String)- , "id" .= Number 1+ , "id" .= Number i , "method" .= method , "params" .= args ]@@ -79,36 +81,41 @@ -> RpcQuery a -> IO (Maybe a) fetchQuery n f q = do- x <- case q of+ case q of+ QueryAccount addr -> do+ [m, m', m''] <- mapConcurrently (\(x, i) -> f (rpc x [toRPC addr, toRPC n] i)) [("eth_getCode", 1), ("eth_getBalance", 2), ("eth_getTransactionCount", 3)]+ return $ liftM3 (\a b c ->+ (hexText . view _String $ a,+ readText . view _String $ b,+ readText . view _String $ c)) m m' m'' QueryCode addr -> do- m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])+ m <- f (rpc "eth_getCode" [toRPC addr, toRPC n] 1) return $ hexText . view _String <$> m QueryNonce addr -> do- m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])+ m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n] 1) return $ readText . view _String <$> m QueryBlock -> do- m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])+ m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False] 1) return $ m >>= parseBlock QueryBalance addr -> do- m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])+ m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n] 1) return $ readText . view _String <$> m QuerySlot addr slot -> do- m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])+ m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n] 1) return $ readText . view _String <$> m QueryChainId -> do- m <- f (rpc "eth_chainId" [toRPC n])+ m <- f (rpc "eth_chainId" [toRPC n] 1) return $ readText . view _String <$> m- return x - parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block parseBlock j = do coinbase <- readText <$> j ^? key "miner" . _String timestamp <- litWord . readText <$> j ^? key "timestamp" . _String number <- readText <$> j ^? key "number" . _String difficulty <- readText <$> j ^? key "difficulty" . _String+ baseFee <- readText <$> j ^? key "baseFeePerGas" . _String -- default codesize, default gas limit, default feescedule- return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.berlin+ return $ EVM.Block coinbase timestamp number difficulty 0xffffffff baseFee 0xffffffff FeeSchedule.berlin fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value) fetchWithSession url sess x = do@@ -117,20 +124,19 @@ fetchContractWithSession :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)-fetchContractWithSession n url addr sess = runMaybeT $ do+fetchContractWithSession n url addr sess = let fetch :: Show a => RpcQuery a -> IO (Maybe a) fetch = fetchQuery n (fetchWithSession url sess)-- theCode <- MaybeT $ fetch (QueryCode addr)- theNonce <- MaybeT $ fetch (QueryNonce addr)- theBalance <- MaybeT $ fetch (QueryBalance addr)-- return $- initialContract (EVM.RuntimeCode (ConcreteBuffer theCode))- & set nonce (w256 theNonce)- & set balance (w256 theBalance)- & set external True+ in+ fetch (QueryAccount addr) >>= \case+ Nothing -> return Nothing+ Just (theCode, theBalance, theNonce) ->+ return $ Just $ + initialContract (EVM.RuntimeCode (ConcreteBuffer theCode))+ & set nonce (w256 theNonce)+ & set balance (w256 theBalance)+ & set external True fetchSlotWithSession :: BlockNumber -> Text -> Session -> Addr -> W256 -> IO (Maybe Word)
src/EVM/Solidity.hs view
@@ -9,6 +9,9 @@ ( solidity , solcRuntime , solidity'+ , yul'+ , yul+ , yulRuntime , JumpType (..) , SolcContract (..) , StorageItem (..)@@ -293,6 +296,22 @@ sourceCache <- makeSourceCache sources asts return $! Just (contracts, sourceCache) +yul :: Text -> Text -> IO (Maybe ByteString)+yul contract src = do+ (json, path) <- yul' src+ let (Just f) = json ^?! key "contracts" ^? key path+ (Just c) = f ^? key (if Text.null contract then "object" else contract)+ bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" . _String+ pure $ toCode <$> (Just bytecode)++yulRuntime :: Text -> Text -> IO (Maybe ByteString)+yulRuntime contract src = do+ (json, path) <- yul' src+ let (Just f) = json ^?! key "contracts" ^? key path+ (Just c) = f ^? key (if Text.null contract then "object" else contract)+ bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" . _String+ pure $ toCode <$> (Just bytecode)+ solidity :: Text -> Text -> IO (Maybe ByteString) solidity contract src = do (json, path) <- solidity' src@@ -334,8 +353,9 @@ let theRuntimeCode = toCode (x ^?! key "bin-runtime" . _String) theCreationCode = toCode (x ^?! key "bin" . _String)- abis =- toList ((x ^?! key "abi" . _String) ^?! _Array)+ abis = toList $ case (x ^?! key "abi") ^? _Array of+ Just v -> v -- solc >= 0.8+ Nothing -> (x ^?! key "abi" . _String) ^?! _Array -- solc < 0.8 in SolcContract { _runtimeCode = theRuntimeCode, _creationCode = theCreationCode,@@ -347,7 +367,7 @@ _constructorInputs = mkConstructor abis, _abiMap = mkAbiMap abis, _eventMap = mkEventMap abis,- _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String,+ _storageLayout = mkStorageLayout $ x ^? key "storage-layout", _immutableReferences = mempty -- TODO: deprecate combined-json } @@ -389,7 +409,7 @@ _constructorInputs = mkConstructor abis, _abiMap = mkAbiMap abis, _eventMap = mkEventMap abis,- _storageLayout = mkStorageLayout $ x ^? key "storageLayout" . _String,+ _storageLayout = mkStorageLayout $ x ^? key "storageLayout", _immutableReferences = fromMaybe mempty $ do x' <- runtime ^? key "immutableReferences" case fromJSON x' of@@ -444,7 +464,7 @@ [] -> [] -- default constructor has zero inputs _ -> error "strange: contract has multiple constructors" -mkStorageLayout :: Maybe Text -> Maybe (Map Text StorageItem)+mkStorageLayout :: Maybe Value -> Maybe (Map Text StorageItem) mkStorageLayout Nothing = Nothing mkStorageLayout (Just json) = do items <- json ^? key "storage" . _Array@@ -534,6 +554,25 @@ } } }+ }+ |]+ x <- pack <$>+ readProcess+ "solc"+ ["--allow-paths", path, "--standard-json", (path <> ".json")]+ ""+ return (x, pack path)++yul' :: Text -> IO (Text, Text)+yul' src = withSystemTempFile "hevm.yul" $ \path handle -> do+ hClose handle+ writeFile path src+ writeFile (path <> ".json")+ [Here.i|+ {+ "language": "Yul",+ "sources": { ${path}: { "urls": [ ${path} ] } },+ "settings": { "outputSelection": { "*": { "*": ["*"], "": [ "*" ] } } } } |] x <- pack <$>
src/EVM/StorageLayout.hs view
@@ -6,7 +6,7 @@ import EVM.Solidity (SolcContract, creationSrcmap, SlotType(..)) import EVM.ABI (AbiType (..), parseTypeName) -import Data.Aeson (Value (Number))+import Data.Aeson (Value (..)) import Data.Aeson.Lens import Control.Lens@@ -43,7 +43,7 @@ let root :: Value root =- fromMaybe (error "no contract definition AST")+ fromMaybe Null (findContractDefinition dapp solc) in case preview ( key "attributes"
src/EVM/SymExec.hs view
@@ -34,6 +34,10 @@ import qualified Control.Monad.State.Class as State import Control.Applicative +data ProofResult a b c = Qed a | Cex b | Timeout c+type VerifyResult = ProofResult (Tree BranchInfo) (Tree BranchInfo) (Tree BranchInfo)+type EquivalenceResult = ProofResult ([VM], [VM]) VM ()+ -- | Convenience functions for generating large symbolic byte strings sbytes32, sbytes128, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8]) sbytes32 = toBytes <$> freshVar_ @ (WordN 256)@@ -134,6 +138,8 @@ , vmoptDifficulty = 0 , vmoptGas = 0xffffffffffffffff , vmoptGaslimit = 0xffffffffffffffff+ , vmoptBaseFee = 0+ , vmoptPriorityFee = 0 , vmoptMaxCodeSize = 0xffffffff , vmoptSchedule = FeeSchedule.berlin , vmoptChainId = 1@@ -149,14 +155,14 @@ _branchCondition :: Maybe Whiff } -doInterpret :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)-doInterpret fetcher maxIter vm = let- f (vm', cs) = Node (BranchInfo (if length cs == 0 then vm' else vm) Nothing) cs- in f <$> interpret' fetcher maxIter vm+doInterpret :: Fetch.Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (Tree BranchInfo)+doInterpret fetcher maxIter askSmtIters vm = let+ f (vm', cs) = Node (BranchInfo (if null cs then vm' else vm) Nothing) cs+ in f <$> interpret' fetcher maxIter askSmtIters vm -interpret' :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (VM, [(Tree BranchInfo)])-interpret' fetcher maxIter vm = let- cont s = interpret' fetcher maxIter $ execState s vm+interpret' :: Fetch.Fetcher -> Maybe Integer -> Maybe Integer -> VM -> Query (VM, [Tree BranchInfo])+interpret' fetcher maxIter askSmtIters vm = let+ cont s = interpret' fetcher maxIter askSmtIters $ execState s vm in case view EVM.result vm of Nothing -> cont exec1@@ -166,7 +172,7 @@ iteration = num $ fromMaybe 0 $ view (iterations . at codelocation) vm -- as an optimization, we skip consulting smt -- if we've been at the location less than 5 times- in if iteration < (max (fromMaybe 0 maxIter) 5)+ in if iteration < (fromMaybe 5 askSmtIters) then cont $ continue EVM.Unknown else io (fetcher q) >>= cont @@ -179,10 +185,10 @@ rvm = execState (continue False) vm in do push 1- (leftvm, left) <- interpret' fetcher maxIter lvm+ (leftvm, left) <- interpret' fetcher maxIter askSmtIters lvm pop 1 push 1- (rightvm, right) <- interpret' fetcher maxIter rvm+ (rightvm, right) <- interpret' fetcher maxIter askSmtIters rvm pop 1 return (vm, [Node (BranchInfo leftvm (Just whiff)) left, Node (BranchInfo rightvm (Just whiff)) right]) Just n -> cont $ continue (not n)@@ -195,10 +201,11 @@ -- | returns a list of possible final evm states interpret :: Fetch.Fetcher- -> Maybe Integer --max iterations+ -> Maybe Integer -- max iterations+ -> Maybe Integer -- ask smt iterations -> Stepper a -> StateT VM Query [a]-interpret fetcher maxIter =+interpret fetcher maxIter askSmtIters = eval . Operational.view where@@ -212,47 +219,47 @@ eval (action Operational.:>>= k) = case action of Stepper.Exec ->- exec >>= interpret fetcher maxIter . k+ exec >>= interpret fetcher maxIter askSmtIters . k Stepper.Run ->- run >>= interpret fetcher maxIter . k+ run >>= interpret fetcher maxIter askSmtIters . k Stepper.IOAct q ->- mapStateT io q >>= interpret fetcher maxIter . k+ mapStateT io q >>= interpret fetcher maxIter askSmtIters . k Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do vm <- get case maxIterationsReached vm maxIter of Nothing -> do push 1- a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)+ a <- interpret fetcher maxIter askSmtIters (Stepper.evm (continue True) >>= k) put vm pop 1 push 1- b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k)+ b <- interpret fetcher maxIter askSmtIters (Stepper.evm (continue False) >>= k) pop 1 return $ a <> b Just n ->- interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k)+ interpret fetcher maxIter askSmtIters (Stepper.evm (continue (not n)) >>= k) Stepper.Wait q -> do let performQuery = do m <- liftIO (fetcher q)- interpret fetcher maxIter (Stepper.evm m >>= k)+ interpret fetcher maxIter askSmtIters (Stepper.evm m >>= k) case q of PleaseAskSMT _ _ continue -> do codelocation <- getCodeLocation <$> get- iteration <- num <$> fromMaybe 0 <$> use (iterations . at codelocation)+ iteration <- num . fromMaybe 0 <$> use (iterations . at codelocation) -- if this is the first time we are branching at this point, -- explore both branches without consulting SMT. -- Exploring too many branches is a lot cheaper than -- consulting our SMT solver.- if iteration < (max (fromMaybe 0 maxIter) 5)- then interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k)+ if iteration < (fromMaybe 5 askSmtIters)+ then interpret fetcher maxIter askSmtIters (Stepper.evm (continue EVM.Unknown) >>= k) else performQuery _ -> performQuery Stepper.EVM m ->- State.state (runState m) >>= interpret fetcher maxIter . k+ State.state (runState m) >>= interpret fetcher maxIter askSmtIters . k maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool maxIterationsReached _ Nothing = Nothing@@ -266,7 +273,7 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)+checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (VerifyResult, VM) checkAssert errs c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just $ checkAssertions errs) {- |Checks if an assertion violation has been encountered@@ -305,12 +312,12 @@ panicMsg :: Word256 -> ByteString panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err) -verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (VerifyResult, VM) verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do preStateRaw <- abstractVM signature' concreteArgs theCode storagemodel -- add the pre condition to the pathconditions to ensure that we are only exploring valid paths let preState = over constraints ((++) [(pre preStateRaw, Todo "assumptions" [])]) preStateRaw- v <- verify preState Nothing Nothing maybepost+ v <- verify preState Nothing Nothing Nothing maybepost return (v, preState) pruneDeadPaths :: [VM] -> [VM]@@ -347,36 +354,41 @@ leaves (Node _ xs) = concatMap leaves xs -- | 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.-verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo))-verify preState maxIter rpcinfo maybepost = do+verify :: VM -> Maybe Integer -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query VerifyResult+verify preState maxIter askSmtIters rpcinfo maybepost = do smtState <- queryState- tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter preState+ tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter askSmtIters preState case maybepost of (Just post) -> do let livePaths = pruneDeadPaths $ leaves tree- -- can also do these queries individually (even concurrently!). Could save time and report multiple violations+ -- have we hit max iterations at any point in a given path+ maxReached :: VM -> Bool+ maxReached p = case maxIter of+ Just maxI -> any (>= (fromInteger maxI)) (view iterations p)+ Nothing -> False+ -- is there any path which can possibly violate the postcondition?+ -- can also do these queries individually (even concurrently!). Could save time and report multiple violations postC = sOr $ fmap (\postState -> (sAnd (fst <$> view constraints postState)) .&& sNot (post (preState, postState))) livePaths- -- is there any path which can possibly violate- -- the postcondition? resetAssertions constrain postC io $ putStrLn "checking postcondition..." checkSat >>= \case Unk -> do io $ putStrLn "postcondition query timed out"- return $ Left tree- Unsat -> do io $ putStrLn "Q.E.D."- return $ Left tree- Sat -> return $ Right tree+ return $ Timeout tree+ Unsat -> do+ if any maxReached livePaths+ then io $ putStrLn "WARNING: max iterations reached, execution halted prematurely"+ else io $ putStrLn "Q.E.D."+ return $ Qed tree+ Sat -> return $ Cex tree DSat _ -> error "unexpected DSAT" Nothing -> do io $ putStrLn "Nothing to check"- return $ Left tree+ return $ Qed tree -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.-equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)-equivalenceCheck bytecodeA bytecodeB maxiter signature' = do+equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query EquivalenceResult+equivalenceCheck bytecodeA bytecodeB maxiter askSmtIters signature' = do let bytecodeA' = if BS.null bytecodeA then BS.pack [0] else bytecodeA bytecodeB' = if BS.null bytecodeB then BS.pack [0] else bytecodeB@@ -392,10 +404,10 @@ smtState <- queryState push 1- aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateA+ aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter askSmtIters preStateA pop 1 push 1- bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateB+ bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter askSmtIters preStateB pop 1 -- Check each pair of endstates for equality: let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths (leaves aVMs), b <- pruneDeadPaths (leaves bVMs)]@@ -428,9 +440,9 @@ constrain $ sOr differingEndStates checkSat >>= \case- Unk -> error "solver said unknown!"- Sat -> return $ Right preStateA- Unsat -> return $ Left (leaves aVMs, leaves bVMs)+ Unk -> return $ Timeout ()+ Sat -> return $ Cex preStateA+ Unsat -> return $ Qed (leaves aVMs, leaves bVMs) DSat _ -> error "unexpected DSAT" both' :: (a -> b) -> (a, a) -> (b, b)
src/EVM/Symbolic.hs view
@@ -259,13 +259,13 @@ Div x y -> whiffValue x `sDiv` whiffValue y Mod x y -> whiffValue x `sMod` whiffValue y Exp x y -> whiffValue x .^ whiffValue y- Neg x -> negate $ whiffValue x+ Neg x -> complement $ whiffValue x Var _ v -> v FromKeccak (ConcreteBuffer bstr) -> literal $ num $ keccak bstr FromKeccak (SymbolicBuffer buf) -> symkeccak' buf Literal x -> literal $ num $ x FromBytes buf -> rawVal $ readMemoryWord 0 buf- FromStorage ind arr -> readArray arr (whiffValue ind) + FromStorage ind arr -> readArray arr (whiffValue ind) -- | Special cases that have proven useful in practice simplifyCondition :: SBool -> Whiff -> SBool
src/EVM/TTY.hs view
@@ -234,20 +234,21 @@ let opts = UnitTestOptions- { oracle = oracle'- , verbose = Nothing- , maxIter = maxIter'- , smtTimeout = Nothing- , smtState = Nothing- , solver = Nothing- , maxDepth = Nothing- , match = ""- , fuzzRuns = 1- , replay = error "irrelevant"- , vmModifier = id- , testParams = error "irrelevant"- , dapp = dappinfo- , allowFFI = False+ { oracle = oracle'+ , verbose = Nothing+ , maxIter = maxIter'+ , askSmtIters = Nothing+ , smtTimeout = Nothing+ , smtState = Nothing+ , solver = Nothing+ , maxDepth = Nothing+ , match = ""+ , fuzzRuns = 1+ , replay = error "irrelevant"+ , vmModifier = id+ , testParams = error "irrelevant"+ , dapp = dappinfo+ , ffiAllowed = False } ui0 = initUiVmState vm opts (void Stepper.execFully) @@ -623,7 +624,9 @@ -> IO UiVmState initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) = do let state' = fromMaybe (error "Internal Error: missing smtState") smtState- (buf, len) <- flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types []+ (buf, len) <- case test of+ SymbolicTest _ -> flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types []+ _ -> return (error "unreachable", error "unreachable") let script = do Stepper.evm . pushTrace . EntryTrace $ "test " <> theTestName <> " (" <> theContractName <> ")"
src/EVM/Transaction.hs view
@@ -29,12 +29,13 @@ data TxType = LegacyTransaction | AccessListTransaction+ | EIP1559Transaction deriving (Show, Eq) data Transaction = Transaction { txData :: ByteString, txGasLimit :: W256,- txGasPrice :: W256,+ txGasPrice :: Maybe W256, txNonce :: W256, txR :: W256, txS :: W256,@@ -42,12 +43,13 @@ txV :: W256, txValue :: W256, txType :: TxType,- txAccessList :: [AccessListEntry]+ txAccessList :: [AccessListEntry],+ txMaxPriorityFeeGas :: Maybe W256,+ txMaxFeePerGas :: Maybe W256 } deriving Show --- utility function for getting a more useful representation of accesslistentries+-- | utility function for getting a more useful representation of accesslistentries -- duplicates only matter for gas computation--- ugly! could use a review.... txAccessMap :: Transaction -> Map Addr [W256] txAccessMap tx = ((Map.fromListWith (++)) . makeTups) $ txAccessList tx where makeTups = map (\ale -> (accessAddress ale, accessStorageKeys ale))@@ -70,23 +72,27 @@ then eip155Data else normalData AccessListTransaction -> eip2930Data+ EIP1559Transaction -> eip1559Data where v = fromIntegral (txV tx) to' = case txToAddr tx of Just a -> BS $ word160Bytes a Nothing -> BS mempty+ Just maxFee = txMaxFeePerGas tx+ Just maxPrio = txMaxPriorityFeeGas tx+ Just gasPrice = txGasPrice tx accessList = txAccessList tx rlpAccessList = EVM.RLP.List $ map (\accessEntry ->- EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry), + EVM.RLP.List [BS $ word160Bytes (accessAddress accessEntry), EVM.RLP.List $ map rlpWordFull $ accessStorageKeys accessEntry] ) accessList normalData = rlpList [rlpWord256 (txNonce tx),- rlpWord256 (txGasPrice tx),+ rlpWord256 gasPrice, rlpWord256 (txGasLimit tx), to', rlpWord256 (txValue tx), BS (txData tx)] eip155Data = rlpList [rlpWord256 (txNonce tx),- rlpWord256 (txGasPrice tx),+ rlpWord256 gasPrice, rlpWord256 (txGasLimit tx), to', rlpWord256 (txValue tx),@@ -94,22 +100,33 @@ rlpWord256 (fromIntegral chainId), rlpWord256 0x0, rlpWord256 0x0]+ eip1559Data = cons 0x02 $ rlpList [+ rlpWord256 (fromIntegral chainId),+ rlpWord256 (txNonce tx),+ rlpWord256 maxPrio,+ rlpWord256 maxFee,+ rlpWord256 (txGasLimit tx),+ to',+ rlpWord256 (txValue tx),+ BS (txData tx),+ rlpAccessList]+ eip2930Data = cons 0x01 $ rlpList [ rlpWord256 (fromIntegral chainId), rlpWord256 (txNonce tx),- rlpWord256 (txGasPrice tx),+ rlpWord256 gasPrice, rlpWord256 (txGasLimit tx),- to', + to', rlpWord256 (txValue tx), BS (txData tx), rlpAccessList] accessListPrice :: FeeSchedule Integer -> [AccessListEntry] -> Integer accessListPrice fs al =- sum (map - (\ale -> - g_access_list_address fs + - (g_access_list_storage_key fs * (toInteger . length) (accessStorageKeys ale))) + sum (map+ (\ale ->+ g_access_list_address fs ++ (g_access_list_storage_key fs * (toInteger . length) (accessStorageKeys ale))) al) txGasCost :: FeeSchedule Integer -> Transaction -> Integer@@ -118,7 +135,7 @@ zeroBytes = BS.count 0 calldata nonZeroBytes = BS.length calldata - zeroBytes baseCost = g_transaction fs- + if isNothing (txToAddr tx) then g_txcreate fs else 0+ + (if isNothing (txToAddr tx) then g_txcreate fs else 0) + (accessListPrice fs $ txAccessList tx) zeroCost = g_txdatazero fs nonZeroCost = g_txdatanonzero fs@@ -127,8 +144,6 @@ instance FromJSON AccessListEntry where parseJSON (JSON.Object val) = do accessAddress_ <- addrField val "address"- --storageKeys <- (val JSON..: "storageKeys")- --accessStorageKeys_ <- JSON.listParser (JSON.withText "W256" (return . readNull 0 . Text.unpack)) storageKeys accessStorageKeys_ <- (val JSON..: "storageKeys") >>= parseJSONList return $ AccessListEntry accessAddress_ accessStorageKeys_ parseJSON invalid =@@ -138,7 +153,9 @@ parseJSON (JSON.Object val) = do tdata <- dataField val "data" gasLimit <- wordField val "gasLimit"- gasPrice <- wordField val "gasPrice"+ gasPrice <- fmap read <$> val JSON..:? "gasPrice"+ maxPrio <- fmap read <$> val JSON..:? "maxPriorityFeePerGas"+ maxFee <- fmap read <$> val JSON..:? "maxFeePerGas" nonce <- wordField val "nonce" r <- wordField val "r" s <- wordField val "s"@@ -146,14 +163,16 @@ v <- wordField val "v" value <- wordField val "value" txType <- fmap read <$> (val JSON..:? "type")- --let legacyTxn = Transaction tdata gasLimit gasPrice nonce r s toAddr v value case txType of- Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction []+ Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing Just 0x01 -> do accessListEntries <- (val JSON..: "accessList") >>= parseJSONList- return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries+ return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing+ Just 0x02 -> do+ accessListEntries <- (val JSON..: "accessList") >>= parseJSONList+ return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee Just _ -> fail "unrecognized custom transaction type"- Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction []+ Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing parseJSON invalid = JSON.typeMismatch "Transaction" invalid
src/EVM/Types.hs view
@@ -245,8 +245,8 @@ SGT x y -> infix' " s> " x y IsZero x -> "IsZero(" ++ show x ++ ")" SHL x y -> infix' " << " x y- SHR x y -> infix' " << " x y- SAR x y -> infix' " a<< " x y+ SHR x y -> infix' " >> " x y+ SAR x y -> infix' " a>> " x y Add x y -> infix' " + " x y Sub x y -> infix' " - " x y Mul x y -> infix' " * " x y
src/EVM/UnitTest.hs view
@@ -70,20 +70,21 @@ import Test.QuickCheck hiding (verbose) data UnitTestOptions = UnitTestOptions- { oracle :: EVM.Query -> IO (EVM ())- , verbose :: Maybe Int- , maxIter :: Maybe Integer- , maxDepth :: Maybe Int- , smtTimeout :: Maybe Integer- , smtState :: Maybe SBV.State- , solver :: Maybe Text- , match :: Text- , fuzzRuns :: Int- , replay :: Maybe (Text, BSLazy.ByteString)- , vmModifier :: VM -> VM- , dapp :: DappInfo- , testParams :: TestVMParams- , allowFFI :: Bool+ { oracle :: EVM.Query -> IO (EVM ())+ , verbose :: Maybe Int+ , maxIter :: Maybe Integer+ , askSmtIters :: Maybe Integer+ , maxDepth :: Maybe Int+ , smtTimeout :: Maybe Integer+ , smtState :: Maybe SBV.State+ , solver :: Maybe Text+ , match :: Text+ , fuzzRuns :: Int+ , replay :: Maybe (Text, BSLazy.ByteString)+ , vmModifier :: VM -> VM+ , dapp :: DappInfo+ , testParams :: TestVMParams+ , ffiAllowed :: Bool } data TestVMParams = TestVMParams@@ -92,8 +93,9 @@ , testOrigin :: Addr , testGasCreate :: W256 , testGasCall :: W256+ , testBaseFee :: W256+ , testPriorityFee :: W256 , testBalanceCreate :: W256- , testBalanceCall :: W256 , testCoinbase :: Addr , testNumber :: W256 , testTimestamp :: W256@@ -110,11 +112,8 @@ defaultGasForInvoking :: W256 defaultGasForInvoking = 0xffffffffffff -defaultBalanceForCreator :: W256-defaultBalanceForCreator = 0xffffffffffffffffffffffff--defaultBalanceForCreated :: W256-defaultBalanceForCreated = 0xffffffffffffffffffffffff+defaultBalanceForTestContract :: W256+defaultBalanceForTestContract = 0xffffffffffffffffffffffff defaultMaxCodeSize :: W256 defaultMaxCodeSize = 0xffffffff@@ -441,7 +440,7 @@ runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> SBV.Query (Text, Either Text Text, VM)-runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi+runTest opts@UnitTestOptions{} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, types) = liftIO $ case replay of Nothing -> fuzzRun opts vm testName types@@ -539,9 +538,9 @@ getTargetContracts :: UnitTestOptions -> Stepper [Addr] getTargetContracts UnitTestOptions{..} = do- vm <- Stepper.evm $ get- let Just contract = currentContract vm- theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract) dapp+ vm <- Stepper.evm get+ let Just contract' = currentContract vm+ theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract') dapp setUp = abiKeccak (encodeUtf8 "targetContracts()") case Map.lookup setUp theAbi of Nothing -> return []@@ -668,7 +667,7 @@ -- get all posible postVMs for the test method allPaths <- fst <$> runStateT- (EVM.SymExec.interpret oracle maxIter (execSymTest opts testName cd')) vm+ (EVM.SymExec.interpret oracle maxIter askSmtIters (execSymTest opts testName cd')) vm let consistentPaths = flip filter allPaths $ \(_, vm') -> case view result vm' of Just (VMFailure DeadPath) -> False@@ -704,7 +703,7 @@ then Right () else Left (vm', prettyCd) Unsat -> return $ Right ()- Unk -> return $ Left (vm', "unknown; query timeout")+ Unk -> return $ Left (vm', "SMT Query Timeout! Try setting a higher timeout with the --smttimeout flag or the DAPP_TEST_SMTTIMEOUT environment variable.") DSat _ -> error "Unexpected DSat" if null $ lefts results@@ -920,6 +919,8 @@ , vmoptTimestamp = litWord $ w256 testTimestamp , vmoptBlockGaslimit = testGaslimit , vmoptGasprice = testGasprice+ , vmoptBaseFee = testBaseFee+ , vmoptPriorityFee = testPriorityFee , vmoptMaxCodeSize = testMaxCodeSize , vmoptDifficulty = testDifficulty , vmoptSchedule = FeeSchedule.berlin@@ -927,7 +928,7 @@ , vmoptCreate = True , vmoptStorageModel = ConcreteS -- TODO: support RPC , vmoptTxAccessList = mempty -- TODO: support unit test access lists???- , vmoptAllowFFI = allowFFI+ , vmoptAllowFFI = ffiAllowed } creator = initialContract (RuntimeCode mempty)@@ -975,8 +976,9 @@ <*> getAddr "DAPP_TEST_ORIGIN" ethrunAddress <*> getWord "DAPP_TEST_GAS_CREATE" defaultGasForCreating <*> getWord "DAPP_TEST_GAS_CALL" defaultGasForInvoking- <*> getWord "DAPP_TEST_BALANCE_CREATE" defaultBalanceForCreator- <*> getWord "DAPP_TEST_BALANCE_CALL" defaultBalanceForCreated+ <*> getWord "DAPP_TEST_BASEFEE" 0+ <*> getWord "DAPP_TEST_PRIORITYFEE" 0+ <*> getWord "DAPP_TEST_BALANCE" defaultBalanceForTestContract <*> getAddr "DAPP_TEST_COINBASE" miner <*> getWord "DAPP_TEST_NUMBER" blockNum <*> getWord "DAPP_TEST_TIMESTAMP" ts
src/EVM/VMTest.hs view
@@ -30,7 +30,7 @@ import GHC.Stack -import Data.Aeson ((.:), FromJSON (..))+import Data.Aeson ((.:), (.:?), FromJSON (..)) import Data.Foldable (fold) import Data.Map (Map) import Data.Maybe (fromMaybe, isNothing)@@ -48,6 +48,7 @@ { blockCoinbase :: Addr , blockDifficulty :: W256 , blockGasLimit :: W256+ , blockBaseFee :: W256 , blockNumber :: W256 , blockTimestamp :: W256 , blockTxs :: [Transaction]@@ -199,8 +200,9 @@ difficulty <- wordField v' "difficulty" gasLimit <- wordField v' "gasLimit" number <- wordField v' "number"+ baseFee <- fmap read <$> v' .:? "baseFeePerGas" timestamp <- wordField v' "timestamp"- return $ Block coinbase difficulty gasLimit number timestamp txs+ return $ Block coinbase difficulty gasLimit (fromMaybe 0 baseFee) number timestamp txs parseJSON invalid = JSON.typeMismatch "Block" invalid @@ -248,7 +250,7 @@ fromBlockchainCase :: BlockchainCase -> Either BlockchainError Case fromBlockchainCase (BlockchainCase blocks preState postState network) = case (blocks, network) of- ([block], "Berlin") -> case blockTxs block of+ ([block], "London") -> case blockTxs block of [tx] -> fromBlockchainCase' block tx preState postState [] -> Left NoTxs _ -> Left TooManyTxs@@ -260,7 +262,7 @@ -> Either BlockchainError Case fromBlockchainCase' block tx preState postState = let isCreate = isNothing (txToAddr tx) in- case (sender 1 tx, checkTx tx preState) of+ case (sender 1 tx, checkTx tx block preState) of (Nothing, _) -> Left SignatureUnverified (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx) (Just origin, Just checkState) -> Right $ Case@@ -272,6 +274,8 @@ , vmoptCaller = litAddr origin , vmoptOrigin = origin , vmoptGas = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)+ , vmoptBaseFee = blockBaseFee block+ , vmoptPriorityFee = priorityFee tx (blockBaseFee block) , vmoptGaslimit = txGasLimit tx , vmoptNumber = blockNumber block , vmoptTimestamp = litWord $ w256 $ blockTimestamp block@@ -279,7 +283,7 @@ , vmoptDifficulty = blockDifficulty block , vmoptMaxCodeSize = 24576 , vmoptBlockGaslimit = blockGasLimit block- , vmoptGasprice = txGasPrice tx+ , vmoptGasprice = effectiveGasPrice , vmoptSchedule = feeSchedule , vmoptChainId = 1 , vmoptCreate = isCreate@@ -297,27 +301,53 @@ theCode = if isCreate then EVM.InitCode (ConcreteBuffer (txData tx)) else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode+ effectiveGasPrice = effectiveprice tx (blockBaseFee block) cd = if isCreate then (mempty, 0) else let l = num . BS.length $ txData tx in (ConcreteBuffer $ txData tx, litWord l) +effectiveprice :: Transaction -> W256 -> W256+effectiveprice tx baseFee = priorityFee tx baseFee + baseFee -validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe ()-validateTx tx cs = do+priorityFee :: Transaction -> W256 -> W256+priorityFee tx baseFee = let+ (txPrioMax, txMaxFee) = case txType tx of+ EIP1559Transaction ->+ let Just maxPrio = txMaxPriorityFeeGas tx+ Just maxFee = txMaxFeePerGas tx+ in (maxPrio, maxFee)+ _ ->+ let Just gasPrice = txGasPrice tx+ in (gasPrice, gasPrice)+ in min txPrioMax (txMaxFee - baseFee)++maxBaseFee :: Transaction -> W256+maxBaseFee tx =+ case txType tx of+ EIP1559Transaction ->+ let Just maxFee = txMaxFeePerGas tx+ in maxFee+ _ ->+ let Just gasPrice = txGasPrice tx+ in gasPrice+++validateTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe ()+validateTx tx block cs = do origin <- sender 1 tx originBalance <- (view balance) <$> view (at origin) cs originNonce <- (view nonce) <$> view (at origin) cs- let gasDeposit = w256 $ (txGasPrice tx) * (txGasLimit tx)+ let gasDeposit = w256 $ (effectiveprice tx (blockBaseFee block)) * (txGasLimit tx) if gasDeposit + (w256 $ txValue tx) <= originBalance- && (w256 $ txNonce tx) == originNonce+ && (w256 $ txNonce tx) == originNonce && blockBaseFee block <= maxBaseFee tx then Just () else Nothing -checkTx :: Transaction -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)-checkTx tx prestate = do+checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)+checkTx tx block prestate = do origin <- sender 1 tx- validateTx tx prestate+ validateTx tx block prestate let isCreate = isNothing (txToAddr tx) senderNonce = EVM.wordValue $ view (accountAt origin . nonce) prestate toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)
test/test.hs view
@@ -22,6 +22,7 @@ import Test.Tasty import Test.Tasty.QuickCheck import Test.Tasty.HUnit+import Test.Tasty.Runners import Control.Monad.State.Strict (execState, runState) import Control.Lens hiding (List, pre, (.>))@@ -51,7 +52,15 @@ fail = io . fail main :: IO ()-main = defaultMain $ testGroup "hevm"+main = defaultMain tests++-- | run a subset of tests in the repl. p is a tasty pattern:+-- https://github.com/UnkindPartition/tasty/tree/ee6fe7136fbcc6312da51d7f1b396e1a2d16b98a#patterns+runSubSet :: String -> IO ()+runSubSet p = defaultMain . applyPattern p $ tests++tests :: TestTree+tests = testGroup "hevm" [ testGroup "ABI" [ testProperty "Put/get inverse" $ \x -> case runGetOrFail (getAbi (abiValueType x)) (runPut (putAbi x)) of@@ -145,8 +154,8 @@ , testGroup "metadata stripper" [ testCase "it strips the metadata for solc => 0.6" $ do- let code = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"- stripped = stripBytecodeMetadata code+ let code' = hexText "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fea265627a7a723158205d775f914dcb471365a430b5f5b2cfe819e615cbbb5b2f1ccc7da1fd802e43c364736f6c634300050b0032"+ stripped = stripBytecodeMetadata code' assertEqual "failed to strip metadata" (show (ByteStringS stripped)) "0x608060405234801561001057600080fd5b50600436106100365760003560e01c806317bf8bac1461003b578063acffee6b1461005d575b600080fd5b610043610067565b604051808215151515815260200191505060405180910390f35b610065610073565b005b60008060015414905090565b6000809054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f8a8fd6d6040518163ffffffff1660e01b815260040160206040518083038186803b1580156100da57600080fd5b505afa1580156100ee573d6000803e3d6000fd5b505050506040513d602081101561010457600080fd5b810190808051906020019092919050505060018190555056fe" , testCase "it strips the metadata and constructor args" $ do@@ -160,10 +169,10 @@ } |] - (json, path) <- solidity' srccode- let Just (solc, _, _) = readJSON json+ (json, path') <- solidity' srccode+ let Just (solc', _, _) = readJSON json initCode :: ByteString- Just initCode = solc ^? ix (path <> ":A") . creationCode+ Just initCode = solc' ^? ix (path' <> ":A") . creationCode -- add constructor arguments assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode) ]@@ -214,7 +223,7 @@ in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y _ -> sFalse- (Left res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post+ (Qed res, _) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -236,31 +245,11 @@ in case view result poststate of Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y _ -> sFalse- (Left res, _) <- runSMTWith z3 $ query $+ (Qed res, _) <- runSMTWith z3 $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) putStrLn $ "successfully explored: " <> show (length res) <> " paths" ,- testCase "factorize 973013" $ do- Just factor <- solcRuntime "PrimalityCheck"- [i|- contract PrimalityCheck {- function factor(uint x, uint y) public pure {- require(1 < x && x < 973013 && 1 < y && y < 973013);- assert(x*y != 973013);- }- }- |]- bs <- runSMTWith cvc4 $ query $ do- (Right _, vm) <- checkAssert defaultPanicCodes factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []- case view (state . calldata . _1) vm of- SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs- ConcreteBuffer _ -> error "unexpected"-- let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs- assertEqual "" True (x == 953 && y == 1021 || x == 1021 && y == 953)- ,-- testCase "summary storage writes" $ do+ testCase "summary storage writes" $ do Just c <- solcRuntime "A" [i| contract A {@@ -286,9 +275,35 @@ in case view result poststate of Just (VMSuccess _) -> prex + 2 * y .== postx _ -> sFalse- (Left res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post+ (Qed res, _) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post putStrLn $ "successfully explored: " <> show (length res) <> " paths" ,+ -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule+ -- regression test for: https://github.com/dapphub/dapptools/pull/698+ testCase "Neg" $ do+ let src =+ [i|+ object "Neg" {+ code {+ // Deploy the contract+ datacopy(0, dataoffset("runtime"), datasize("runtime"))+ return(0, datasize("runtime"))+ }+ object "runtime" {+ code {+ let v := calldataload(4)+ if iszero(iszero(and(v, not(0xffffffffffffffffffffffffffffffffffffffff)))) {+ invalid()+ }+ }+ }+ }+ |]+ Just c <- yulRuntime "Neg" src+ (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("hello(address)", [AbiAddressType])) []+ putStrLn $ "successfully explored: " <> show (length res) <> " paths"+ ,+ -- Inspired by these `msg.sender == to` token bugs -- which break linearity of totalSupply. testCase "catch storage collisions" $ do@@ -318,7 +333,7 @@ Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256) _ -> sFalse bs <- runSMT $ query $ do- (Right _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)+ (Cex _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post) case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected"@@ -345,7 +360,7 @@ } } |]- (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []+ (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (cvc4)" $ do@@ -367,7 +382,7 @@ } } |]- (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []+ (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "Deposit contract loop (error version)" $ do@@ -390,7 +405,7 @@ } |] bs <- runSMT $ query $ do- (Right _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) []+ (Cex _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected"@@ -407,7 +422,7 @@ } } |]- (Left res, _) <- runSMTWith z3 $ do+ (Qed res, _) <- runSMTWith z3 $ do setTimeOut 5000 query $ checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths"@@ -422,7 +437,7 @@ } } |]- (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+ (Qed res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , testCase "injectivity of keccak (32 bytes)" $ do@@ -434,7 +449,7 @@ } } |]- (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+ (Qed res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn $ "successfully explored: " <> show (length res) <> " paths" , @@ -448,7 +463,7 @@ } |] bs <- runSMTWith z3 $ query $ do- (Right _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []+ (Cex _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] case view (state . calldata . _1) vm of SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs ConcreteBuffer _ -> error "unexpected"@@ -478,7 +493,7 @@ } } |]- Left res <- runSMTWith z3 $ do+ Qed res <- runSMTWith z3 $ do setTimeOut 5000 query $ fst <$> checkAssert defaultPanicCodes c Nothing [] putStrLn $ "successfully explored: " <> show (length res) <> " paths"@@ -497,13 +512,13 @@ } |] -- should find a counterexample- Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+ Cex _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] putStrLn "found counterexample:" , testCase "multiple contracts" $ do- let code =+ let code' = [i| contract C { uint x;@@ -519,9 +534,9 @@ } |] aAddr = Addr 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B- Just c <- solcRuntime "C" code- Just a <- solcRuntime "A" code- Right _ <- runSMT $ query $ do+ Just c <- solcRuntime "C" code'+ Just a <- solcRuntime "A" code'+ Cex _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS store <- freshArray (show aAddr) Nothing let vm = vm0@@ -529,11 +544,11 @@ & over (env . contracts) (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) & set EVM.storage (EVM.Symbolic [] store)))- verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+ verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "calling unique contracts (read from storage)" $ do- let code =+ let code' = [i| contract C { uint x;@@ -549,16 +564,16 @@ uint public x; } |]- Just c <- solcRuntime "C" code- Right _ <- runSMT $ query $ do+ Just c <- solcRuntime "C" code'+ Cex _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0- verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+ verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "keccak concrete and sym agree" $ do- let code =+ let code' = [i| contract C { function kecc(uint x) public pure {@@ -568,22 +583,22 @@ } } |]- Just c <- solcRuntime "C" code- Left _ <- runSMT $ query $ do+ Just c <- solcRuntime "C" code'+ Qed _ <- runSMT $ query $ do vm0 <- abstractVM (Just ("kecc(uint256)", [AbiUIntType 256])) [] c SymbolicS let vm = vm0 & set (state . callvalue) 0- verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+ verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "found counterexample:" , testCase "safemath distributivity (yul)" $ do- Left _ <- runSMTWith cvc4 $ query $ do+ Qed _ <- runSMTWith cvc4 $ query $ do let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b" vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity SymbolicS- verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+ verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "Proven" , testCase "safemath distributivity (sol)" $ do- let code =+ let code' = [i| contract C { function distributivity(uint x, uint y, uint z) public {@@ -602,11 +617,11 @@ } } |]- Just c <- solcRuntime "C" code+ Just c <- solcRuntime "C" code' - Left _ <- runSMTWith z3 $ query $ do+ Qed _ <- runSMTWith cvc4 $ query $ do vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] c SymbolicS- verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+ verify vm Nothing Nothing Nothing (Just $ checkAssertions defaultPanicCodes) putStrLn "Proven" ]@@ -614,20 +629,29 @@ [ testCase "yul optimized" $ do -- These yul programs are not equivalent: (try --calldata $(seth --to-uint256 2) for example)- -- A: B:- -- { {- -- calldatacopy(0, 0, 32) calldatacopy(0, 0, 32)- -- switch mload(0) switch mload(0)- -- case 0 { } case 0 { }- -- case 1 { } case 2 { }- -- default { invalid() } default { invalid() }- -- } }- let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250"- bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152"+ Just aPrgm <- yul ""+ [i|+ {+ calldatacopy(0, 0, 32)+ switch mload(0)+ case 0 { }+ case 1 { }+ default { invalid() }+ }+ |]+ Just bPrgm <- yul ""+ [i|+ {+ calldatacopy(0, 0, 32)+ switch mload(0)+ case 0 { }+ case 2 { }+ default { invalid() }+ }+ |] runSMTWith z3 $ query $ do- Right _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing+ Cex _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing Nothing return ()- ] ] where@@ -759,3 +783,5 @@ b' <- f a' return (b, b') +applyPattern :: String -> TestTree -> TestTree+applyPattern p = localOption (TestPattern (parseExpr p))