hevm 0.41.0 → 0.42.0

raw patch · 21 files changed

+1307/−840 lines, 21 filesdep −cborgdep ~QuickCheckdep ~brickdep ~cryptonitePVP ok

version bump matches the API change (PVP)

Dependencies removed: cborg

Dependency ranges changed: QuickCheck, brick, cryptonite, lens, lens-aeson, megaparsec, memory, optparse-generic, regex-tdfa, sbv, time, vty

API changes (from Hackage documentation)

Files

• CHANGELOG.md +21/−4
• hevm-cli/hevm-cli.hs +123/−61
• hevm.cabal +13/−14
• src/EVM.hs +96/−82
• src/EVM/ABI.hs +4/−2
• src/EVM/Concrete.hs +2/−1
• src/EVM/Dev.hs +10/−3
• src/EVM/Emacs.hs +1/−1
• src/EVM/Facts.hs +28/−2
• src/EVM/Fetch.hs +142/−94
• src/EVM/Flatten.hs +251/−48
• src/EVM/Format.hs +46/−12
• src/EVM/Solidity.hs +19/−14
• src/EVM/Stepper.hs +1/−1
• src/EVM/SymExec.hs +41/−20
• src/EVM/Symbolic.hs +18/−32
• src/EVM/TTY.hs +92/−16
• src/EVM/Types.hs +28/−0
• src/EVM/UnitTest.hs +137/−87
• src/EVM/VMTest.hs +144/−295
• test/test.hs +90/−51

@@ -1,12 +1,29 @@ # hevm changelog +## 0.42.0 - 2020-10-31++### Changed++- z3 updated to 4.8.8+- optimize SMT queries+- More useful trace output for unknown calls+- Default to on chain values for `coinbase`, `timestamp`, `difficulty`, `blocknumber` when rpc is provided+- Perform tx initialization (gas payment, value transfer) in `hevm exec`, `hevm symbolic` and `hevm dapp-test`.++### Added++- TTY commands `P` and `c-p` for taking larger steps backwards in the debuger.+- `--cache` flag for `dapp-test`, `exec`, `symbolic`, `interactive`,+  enabling caching of contracts received by rpc.+- `load(address,bytes32)` cheat code allowing storage reads from arbitrary contracts.+ ## 0.41.0 - 2020-08-19  ### Changed  - 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, +- Generate more interesting values in property based testing,  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@@ -34,9 +51,9 @@   - 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`.-  +   - contract.storage: `Map Word Word` -> `Storage`, defined as: ```hs data Storage@@ -53,7 +70,7 @@ See the README for details on usage.  The new module `EVM.SymExec` exposes several library functions dealing with symbolic execution.-In particular, +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. 

@@ -9,19 +9,21 @@ {-# Language NumDecimals #-} {-# Language OverloadedStrings #-} {-# Language TypeOperators #-}+{-# Language RecordWildCards #-}  module Main where  import EVM (StorageModel(..)) import qualified EVM-import EVM.Concrete (createAddress, w256)-import EVM.Symbolic (forceLitBytes, litBytes, litAddr, w256lit, sw256, SymWord(..), Buffer(..), len)+import EVM.Concrete (createAddress, w256, wordValue)+import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len, forceLit, litWord) import qualified EVM.FeeSchedule as FeeSchedule import qualified EVM.Fetch import qualified EVM.Flatten import qualified EVM.Stepper import qualified EVM.TTY import qualified EVM.Emacs+import EVM.Dev (concatMapM)  #if MIN_VERSION_aeson(1, 0, 0) import qualified EVM.VMTest as VMTest@@ -105,8 +107,10 @@       , difficulty    :: w ::: Maybe W256       <?> "Block: difficulty"       , chainid       :: w ::: Maybe W256       <?> "Env: chainId"   -- remote state opts-      , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"-      , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"+      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"+      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"+      , state         :: w ::: Maybe String     <?> "Path to state repository"+      , cache         :: w ::: Maybe String     <?> "Path to rpc cache repository"    -- symbolic execution opts       , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"@@ -127,6 +131,7 @@       , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 20000)"       , 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"       }   | Exec -- Execute a given program with specified env & calldata       { code        :: w ::: Maybe ByteString <?> "Program bytecode"@@ -149,6 +154,7 @@       , debug       :: w ::: Bool             <?> "Run interactively"       , trace       :: w ::: Bool             <?> "Dump trace"       , state       :: w ::: Maybe String     <?> "Path to state repository"+      , cache       :: w ::: Maybe String     <?> "Path to rpc cache repository"       , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"       , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"       , jsonFile    :: w ::: Maybe String     <?> "Filename or path to dapp build output (default: out/*.solc.json)"@@ -164,6 +170,7 @@       , verbose     :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"       , coverage    :: w ::: Bool                     <?> "Coverage analysis"       , 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"       }   | Interactive -- Browse & run unit tests interactively@@ -171,6 +178,7 @@       , dappRoot :: w ::: Maybe String <?> "Path to dapp project root directory (default: . )"       , rpc      :: w ::: Maybe URL    <?> "Fetch state from a remote node"       , state    :: w ::: Maybe String <?> "Path to state repository"+      , cache    :: w ::: Maybe String <?> "Path to rpc cache repository"       , replay   :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"       }   | BcTest -- Run an Ethereum Blockhain/GeneralState test@@ -225,6 +233,24 @@ optsMode :: Command Options.Unwrapped -> Mode optsMode x = if debug x then Debug else Run +applyCache :: (Maybe String, Maybe String) -> IO (EVM.VM -> EVM.VM)+applyCache (state, cache) =+  let applyState = flip Facts.apply+      applyCache = flip Facts.applyCache+  in case (state, cache) of+    (Nothing, Nothing) -> do+      pure id+    (Nothing, Just cachePath) -> do+      facts <- Git.loadFacts (Git.RepoAt cachePath)+      pure $ applyCache facts+    (Just statePath, Nothing) -> do+      facts <- Git.loadFacts (Git.RepoAt statePath)+      pure $ applyState facts+    (Just statePath, Just cachePath) -> do+      cacheFacts <- Git.loadFacts (Git.RepoAt cachePath)+      stateFacts <- Git.loadFacts (Git.RepoAt statePath)+      pure $ (applyState stateFacts) . (applyCache cacheFacts)+ unitTestOptions :: Command Options.Unwrapped -> String -> IO UnitTestOptions unitTestOptions cmd testFile = do   let root = fromMaybe "." (dappRoot cmd)@@ -233,15 +259,9 @@     Just (contractMap, sourceCache) ->       pure $ dappInfo root contractMap sourceCache -  vmModifier <--    case state cmd of-      Nothing ->-        pure id-      Just repoPath -> do-        facts <- Git.loadFacts (Git.RepoAt repoPath)-        pure (flip Facts.apply facts)+  vmModifier <- applyCache (state cmd, cache cmd) -  params <- getParametersFromEnvironmentVariables+  params <- getParametersFromEnvironmentVariables (rpc cmd)    let     testn = testNumber params@@ -286,7 +306,7 @@         testOpts <- unitTestOptions cmd testFile         case (coverage cmd, optsMode cmd) of           (False, Run) ->-            dappTest testOpts (optsMode cmd) testFile+            dappTest testOpts (optsMode cmd) testFile (cache cmd)           (False, Debug) ->             EVM.TTY.main testOpts root testFile           (True, _) ->@@ -354,15 +374,28 @@         , intercalate ", " xs         ] -dappTest :: UnitTestOptions -> Mode -> String -> IO ()-dappTest opts _ solcFile =+dappTest :: UnitTestOptions -> Mode -> String -> Maybe String -> IO ()+dappTest opts _ solcFile cache =   readSolc solcFile >>=     \case-      Just (contractMap, cache) -> do+      Just (contractMap, sourceCache) -> do         let matcher = regexMatches (EVM.UnitTest.match opts)             unitTests = (findUnitTests matcher) (Map.elems contractMap)-        results <- mapM (runUnitTestContract opts contractMap cache) unitTests-        when (any (== False) results) exitFailure++        results <- concatMapM (runUnitTestContract opts contractMap sourceCache) unitTests+        let (passing, vms) = unzip results++        case cache of+          Nothing ->+            pure ()+          Just path ->+            -- merge all of the post-vm caches and save into the state+            let+              cache' = mconcat [view EVM.cache vm | vm <- vms]+            in+              Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts cache')++        unless (all id passing) exitFailure       Nothing ->         error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'") @@ -468,7 +501,7 @@       io $ void $ EVM.TTY.runFromVM         (maxIterations cmd)         srcInfo-        (EVM.Fetch.oracle smtState rpcinfo model)+        (EVM.Fetch.oracle (Just smtState) rpcinfo model True)         preState    else@@ -527,13 +560,13 @@ dappCoverage opts _ solcFile =   readSolc solcFile >>=     \case-      Just (contractMap, cache) -> do+      Just (contractMap, sourceCache) -> do         let matcher = regexMatches (EVM.UnitTest.match opts)         let unitTests = (findUnitTests matcher) (Map.elems contractMap)-        covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap cache) unitTests+        covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap sourceCache) unitTests          let-          dapp = dappInfo "." contractMap cache+          dapp = dappInfo "." contractMap sourceCache           f (k, vs) = do             putStr "***** hevm coverage for "             putStrLn (unpack k)@@ -556,19 +589,10 @@ launchExec :: Command Options.Unwrapped -> IO () launchExec cmd = do   dapp <- getSrcInfo cmd-   vm <- vmFromCommand cmd-  vm1 <- case state cmd of-    Nothing -> pure vm-    Just path ->-      -- Note: this will load the code, so if you've specified a state-      -- repository, then you effectively can't change `--code' after-      -- the first run.-      Facts.apply vm <$> Git.loadFacts (Git.RepoAt path)-   case optsMode cmd of     Run -> do-      vm' <- execStateT (interpret fetcher Nothing . void $ EVM.Stepper.execFully) vm1+      vm' <- execStateT (EVM.Stepper.interpret fetcher . void $ EVM.Stepper.execFully) vm       when (trace cmd) $ hPutStr stderr (showTraceTree dapp vm')       case view EVM.result vm' of         Nothing ->@@ -588,7 +612,12 @@             Nothing -> pure ()             Just path ->               Git.saveFacts (Git.RepoAt path) (Facts.vmFacts vm')-    Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm1+          case cache cmd of+            Nothing -> pure ()+            Just path ->+              Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts (view EVM.cache vm'))++    Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm    where fetcher = maybe EVM.Fetch.zero (EVM.Fetch.http block') (rpc cmd)          block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd) @@ -654,25 +683,48 @@ -- | Creates a (concrete) VM from command line options vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM vmFromCommand cmd = do-  vm <- case (rpc cmd, address cmd) of-    (Just url, Just addr') -> do+  withCache <- applyCache (state cmd, cache cmd)++  (miner,ts,blockNum,diff) <- case rpc cmd of+    Nothing -> return (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 _number+                                   , wordValue _difficulty+                                   )++  contract <- case (rpc cmd, address cmd, code cmd) of+    (Just url, Just addr', Just c) -> do       EVM.Fetch.fetchContractFrom block' url addr' >>= \case-        Nothing -> error $ "contract not found: " <> show address'-        Just contract' -> case code cmd of-          Nothing -> return (vm1 contract')+        Nothing ->+          error $ "contract not found: " <> show address'+        Just contract' ->           -- if both code and url is given,           -- fetch the contract and overwrite the code-          Just c -> return . vm1 $+          return $             EVM.initialContract  (codeType $ hexByteString "--code" $ strip0x c)               & set EVM.storage  (view EVM.storage  contract')               & set EVM.balance  (view EVM.balance  contract')               & set EVM.nonce    (view EVM.nonce    contract')               & set EVM.external (view EVM.external contract') -    _ -> return . vm1 . EVM.initialContract . codeType $ bytes code ""+    (Just url, Just addr', Nothing) ->+      EVM.Fetch.fetchContractFrom block' url addr' >>= \case+        Nothing ->+          error $ "contract not found: " <> show address'+        Just contract' -> return contract' -  return $ vm & EVM.env . EVM.contracts . ix address' . EVM.balance +~ (w256 value')-      where+    (_, _, Just c)  ->+      return $+        EVM.initialContract (codeType $ hexByteString "--code" $ strip0x c)++    (_, _, Nothing) ->+      error $ "must provide at least (rpc + address) or code"++  return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract)+    where         decipher = hexByteString "bytes" . strip0x         block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)         value'   = word value 0@@ -684,7 +736,7 @@               then createAddress origin' (word nonce 0)               else addr address 0xacab -        vm1 c = EVM.makeVm $ EVM.VMOpts+        vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts           { EVM.vmoptContract      = c           , EVM.vmoptCalldata      = (calldata', literal . num $ len calldata')           , EVM.vmoptValue         = w256lit value'@@ -693,13 +745,13 @@           , EVM.vmoptOrigin        = origin'           , EVM.vmoptGas           = word gas 0           , EVM.vmoptGaslimit      = word gas 0-          , EVM.vmoptCoinbase      = addr coinbase 0-          , EVM.vmoptNumber        = word number 0-          , EVM.vmoptTimestamp     = word timestamp 0+          , EVM.vmoptCoinbase      = addr coinbase miner+          , EVM.vmoptNumber        = word number blockNum+          , EVM.vmoptTimestamp     = w256lit $ word timestamp ts           , EVM.vmoptBlockGaslimit = word gaslimit 0           , EVM.vmoptGasprice      = word gasprice 0           , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff-          , EVM.vmoptDifficulty    = word difficulty 0+          , EVM.vmoptDifficulty    = word difficulty diff           , EVM.vmoptSchedule      = FeeSchedule.istanbul           , EVM.vmoptChainId       = word chainid 1           , EVM.vmoptCreate        = create cmd@@ -711,7 +763,18 @@  symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM symvmFromCommand cmd = do++  (miner,blockNum,diff) <- case rpc cmd of+    Nothing -> return (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 _difficulty+                                   )+   caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)+  ts <- maybe (sw256 <$> freshVar_) (return . w256lit) (timestamp cmd)   callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)   (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of     -- fully abstract calldata (up to 1024 bytes)@@ -742,34 +805,33 @@     Just SymbolicS -> EVM.Symbolic <$> freshArray_ Nothing     Nothing -> EVM.Symbolic <$> freshArray_ (if create cmd then (Just 0) else Nothing) -  vm <- case (rpc cmd, address cmd, code cmd) of+  withCache <- io $ applyCache (state cmd, cache cmd)++  contract' <- case (rpc cmd, address cmd, code cmd) of     (Just url, Just addr', _) ->       io (EVM.Fetch.fetchContractFrom block' url addr') >>= \case         Nothing ->           error $ "contract not found."-        Just contract' ->-          return $-            vm1 cdlen calldata' callvalue' caller' (contract'' & set EVM.storage store)+        Just contract' -> return contract''           where             contract'' = case code cmd of               Nothing -> contract'               -- if both code and url is given,               -- fetch the contract and overwrite the code               Just c -> EVM.initialContract (codeType $ decipher c)-                        & set EVM.storage     (view EVM.storage contract')                         & set EVM.origStorage (view EVM.origStorage contract')                         & set EVM.balance     (view EVM.balance contract')                         & set EVM.nonce       (view EVM.nonce contract')                         & set EVM.external    (view EVM.external contract')      (_, _, Just c)  ->-      return $-        vm1 cdlen calldata' callvalue' caller' $-          (EVM.initialContract . codeType $ decipher c) & set EVM.storage store+      return $ (EVM.initialContract . codeType $ decipher c)     (_, _, Nothing) ->       error $ "must provide at least (rpc + address) or code" -  return $ vm & over EVM.pathConditions (<> [pathCond])+  return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract')+    & over EVM.pathConditions (<> [pathCond])+    & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store    where     decipher = hexByteString "bytes" . strip0x@@ -779,7 +841,7 @@     address' = if create cmd           then createAddress origin' (word nonce 0)           else addr address 0xacab-    vm1 cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts+    vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts       { EVM.vmoptContract      = c       , EVM.vmoptCalldata      = (calldata', cdlen)       , EVM.vmoptValue         = callvalue'@@ -788,13 +850,13 @@       , EVM.vmoptOrigin        = origin'       , EVM.vmoptGas           = word gas 0xffffffffffffffff       , EVM.vmoptGaslimit      = word gas 0xffffffffffffffff-      , EVM.vmoptCoinbase      = addr coinbase 0-      , EVM.vmoptNumber        = word number 0-      , EVM.vmoptTimestamp     = word timestamp 0+      , EVM.vmoptCoinbase      = addr coinbase miner+      , EVM.vmoptNumber        = word number blockNum+      , EVM.vmoptTimestamp     = ts       , EVM.vmoptBlockGaslimit = word gaslimit 0       , EVM.vmoptGasprice      = word gasprice 0       , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff-      , EVM.vmoptDifficulty    = word difficulty 0+      , EVM.vmoptDifficulty    = word difficulty diff       , EVM.vmoptSchedule      = FeeSchedule.istanbul       , EVM.vmoptChainId       = word chainid 1       , EVM.vmoptCreate        = create cmd

@@ -2,7 +2,7 @@ name:   hevm version:-  0.41.0+  0.42.0 synopsis:   Ethereum virtual machine evaluator description:@@ -81,10 +81,10 @@   install-includes:     ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h   build-depends:-    QuickCheck                        >= 2.13.2 && < 2.14,+    QuickCheck                        >= 2.13.2 && < 2.15,     containers                        >= 0.6.0 && < 0.7,     deepseq                           >= 1.4.4 && < 1.5,-    time                              >= 1.8.0 && < 1.9,+    time                              >= 1.8.0 && < 1.11,     transformers                      >= 0.5.6 && < 0.6,     tree-view                         == 0.5,     abstract-par                      >= 0.3.3 && < 0.4,@@ -97,38 +97,37 @@     vector                            >= 0.12.1 && < 0.13,     ansi-wl-pprint                    >= 0.6.9 && < 0.7,     base16-bytestring                 >= 0.1.1 && < 0.2,-    brick                             >= 0.47.1 && < 0.48,-    megaparsec                        >= 7.0.5 && < 7.1,+    brick                             >= 0.47.1 && < 0.56,+    megaparsec                        >= 7.0.5 && < 8.1,     mtl                               >= 2.2.2 && < 2.3,     directory                         >= 1.3.3 && < 1.4,     filepath                          >= 1.4.2 && < 1.5,-    vty                               >= 5.25.1 && < 5.26,-    cborg                             >= 0.2.2 && < 0.3,+    vty                               >= 5.25.1 && < 5.31,     cereal                            >= 0.5.8 && < 0.6,-    cryptonite                        >= 0.25 && < 0.26,-    memory                            >= 0.14.18 && < 0.15,+    cryptonite                        >= 0.25 && < 0.28,+    memory                            >= 0.14.18 && < 0.16,     data-dword                        >= 0.3.1 && < 0.4,     fgl                               >= 5.7.0 && < 5.8,     free                              >= 5.1.3 && < 5.2,     haskeline                         >= 0.7.4 && < 0.8,     process                           >= 1.6.5 && < 1.7,-    lens                              >= 4.17.1 && < 4.18,-    lens-aeson                        >= 1.0.2 && < 1.1,+    lens                              >= 4.17.1 && < 4.20,+    lens-aeson                        >= 1.0.2 && < 1.2,     monad-par                         >= 0.3.5 && < 0.4,     multiset                          >= 0.3.4 && < 0.4,     operational                       >= 0.2.3 && < 0.3,-    optparse-generic                  >= 1.3.1 && < 1.4,+    optparse-generic                  >= 1.3.1 && < 1.5,     quickcheck-text                   >= 0.1.2 && < 0.2,     restless-git                      >= 0.7 && < 0.8,     rosezipper                        >= 0.2 && < 0.3,     s-cargot                          >= 0.1.4 && < 0.2,-    sbv                               >= 8.7.5 && < 8.8,+    sbv                               >= 8.7.5 && < 8.9,     semver-range                      >= 0.2.7 && < 0.3,     temporary                         >= 1.3 && < 1.4,     text-format                       >= 0.3.2 && < 0.4,     witherable                        >= 0.3.5 && < 0.4,     wreq                              >= 0.5.3 && < 0.6,-    regex-tdfa                        >= 1.2.3 && < 1.3,+    regex-tdfa                        >= 1.2.3 && < 1.4,     base                              >= 4.9 && < 5   hs-source-dirs:     src

@@ -128,7 +128,7 @@ data Query where   PleaseFetchContract :: Addr         -> (Contract   -> EVM ()) -> Query   PleaseFetchSlot     :: Addr -> Word -> (Word       -> EVM ()) -> Query-  PleaseAskSMT        :: SymWord -> [SBool] -> (JumpCondition -> EVM ()) -> Query+  PleaseAskSMT        :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query  data Choose where   PleaseChoosePath    :: (Bool -> EVM ()) -> Choose@@ -156,9 +156,9 @@  type CodeLocation = (Addr, Int) --- | The possible return values of a SMT query regarding JUMPI-data JumpCondition = Iszero Bool | Unknown | Inconsistent-  deriving (Show)+-- | The possible return values of a SMT query+data BranchCondition = Case Bool | Unknown | Inconsistent+  deriving Show  -- | The cache is data that can be persisted for efficiency: -- any expensive query that is constant at least within a block.@@ -178,7 +178,7 @@   , vmoptGas :: W256   , vmoptGaslimit :: W256   , vmoptNumber :: W256-  , vmoptTimestamp :: W256+  , vmoptTimestamp :: SymWord   , vmoptCoinbase :: Addr   , vmoptDifficulty :: W256   , vmoptMaxCodeSize :: W256@@ -207,7 +207,9 @@     , creationContextSubstate  :: SubState     }   | CallContext-    { callContextOffset    :: Word+    { callContextTarget    :: Addr+    , callContextContext   :: Addr+    , callContextOffset    :: Word     , callContextSize      :: Word     , callContextCodehash  :: W256     , callContextAbi       :: Maybe Word@@ -325,13 +327,13 @@ -- | Data about the block data Block = Block   { _coinbase    :: Addr-  , _timestamp   :: Word+  , _timestamp   :: SymWord   , _number      :: Word   , _difficulty  :: Word   , _gaslimit    :: Word   , _maxCodeSize :: Word   , _schedule    :: FeeSchedule Word-  }+  } deriving Show  blankState :: FrameState blankState = FrameState@@ -370,10 +372,20 @@  instance Semigroup Cache where   a <> b = Cache-    { _fetched = mappend (view fetched a) (view fetched b),-      _path = mappend (view path a) (view path b)+    { _fetched = Map.unionWith unifyCachedContract (view fetched a) (view fetched b)+    , _path = mappend (view path a) (view path b)     } +-- only intended for use in Cache merges, where we expect+-- everything to be Concrete+unifyCachedContract :: Contract -> Contract -> Contract+unifyCachedContract a b = a & set storage merged+  where merged = case (view storage a, view storage b) of+                   (Concrete sa, Concrete sb) ->+                     Concrete (mappend sa sb)+                   _ ->+                     view storage a+ instance Monoid Cache where   mempty = Cache { _fetched = mempty,                    _path = mempty@@ -406,7 +418,7 @@   , _traces = Zipper.fromForest []   , _block = Block     { _coinbase = vmoptCoinbase o-    , _timestamp = w256 $ vmoptTimestamp o+    , _timestamp = vmoptTimestamp o     , _number = w256 $ vmoptNumber o     , _difficulty = w256 $ vmoptDifficulty o     , _maxCodeSize = w256 $ vmoptMaxCodeSize o@@ -436,9 +448,7 @@     , _keccakUsed = mempty     , _storageModel = vmoptStorageModel o     }-  , _cache = Cache (Map.fromList-    [(vmoptAddress o, vmoptContract o)])-    mempty+  , _cache = Cache mempty mempty   , _burned = 0   , _pathConditions = []   , _iterations = mempty@@ -455,14 +465,15 @@       keccak (stripBytecodeMetadata theCode)   , _storage  = Concrete mempty   , _balance  = 0-  , _nonce    = 0+  , _nonce    = if creation then 1 else 0   , _opIxMap  = mkOpIxMap theCode   , _codeOps  = mkCodeOps theCode   , _external = False   , _origStorage = mempty-  } where theCode = case theContractCode of-            InitCode b    -> b-            RuntimeCode b -> b+  } where+      (creation, theCode) = case theContractCode of+            InitCode b    -> (True, b)+            RuntimeCode b -> (False, b)  contractWithStore :: ContractCode -> Storage -> Contract contractWithStore theContractCode store =@@ -643,7 +654,7 @@         -- op: SHL         0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n         -- op: SHR-        0x1c -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftRight x n+        0x1c -> stackOp2 (const g_verylow) $ uncurry shiftRight'         -- op: SAR         0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n @@ -850,7 +861,7 @@         -- op: TIMESTAMP         0x42 ->           limitStack 1 . burn g_base $-            next >> push (the block timestamp)+            next >> pushSym (the block timestamp)          -- op: NUMBER         0x43 ->@@ -996,7 +1007,7 @@                   in case maybeLitWord y of                       Just y' -> jump (0 == y')                       -- if the jump condition is symbolic, an smt query has to be made.-                      Nothing -> askSMT (self, the state pc) y jump+                      Nothing -> askSMT (self, the state pc) (0 .== y) jump             _ -> underrun          -- op: PC@@ -1075,9 +1086,7 @@                               assign callvalue (litWord xValue)                               assign caller (litAddr self)                               assign contract xTo-                            zoom (env . contracts) $ do-                              ix self . balance -= xValue-                              ix xTo  . balance += xValue+                            transfer self xTo xValue                             touchAccount self                             touchAccount xTo             _ ->@@ -1246,6 +1255,12 @@         xxx ->           vmError (UnrecognizedOpcode xxx) +transfer :: Addr -> Addr -> Word -> EVM ()+transfer xFrom xTo xValue =+  zoom (env . contracts) $ do+    ix xFrom . balance -= xValue+    ix xTo  . balance += xValue+ -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc. callChecks   :: (?op :: Word8)@@ -1299,9 +1314,7 @@         Just 1 ->           fetchAccount recipient $ \_ -> do -          zoom (env . contracts) $ do-            ix self . balance -= xValue-            ix recipient  . balance += xValue+          transfer self recipient xValue           touchAccount self           touchAccount recipient           touchAccount precompileAddr@@ -1509,8 +1522,8 @@ getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm)  -- | Construct SMT Query and halt execution until resolved-askSMT :: CodeLocation -> SymWord -> (Bool -> EVM ()) -> EVM ()-askSMT codeloc jumpcondition continue = do+askSMT :: CodeLocation -> SBool -> (Bool -> EVM ()) -> EVM ()+askSMT codeloc condition continue = do   -- We keep track of how many times we have come across this particular   -- (contract, pc) combination in the `iteration` mapping.   iteration <- use (iterations . at codeloc . non 0)@@ -1519,23 +1532,23 @@   -- already. So we first check the cache to see if the result is known   use (cache . path . at (codeloc, iteration)) >>= \case      -- If the query has been done already, select path or select the only available-     Just w -> choosePath (Iszero w)+     Just w -> choosePath (Case w)      -- If this is a new query, run the query, cache the result      -- increment the iterations and select appropriate path      Nothing -> do pathconds <- use pathConditions                    assign result . Just . VMFailure . Query $ PleaseAskSMT-                     jumpcondition pathconds choosePath+                     condition pathconds choosePath     where -- Only one path is possible-         choosePath :: JumpCondition -> EVM ()-         choosePath (Iszero v) = do assign result Nothing-                                    pathConditions <>= if v then [litWord 0 .== jumpcondition] else [litWord 0 ./= jumpcondition]-                                    iteration <- use (iterations . at codeloc . non 0)-                                    assign (cache . path . at (codeloc, iteration)) (Just v)-                                    assign (iterations . at codeloc) (Just (iteration + 1))-                                    continue v+         choosePath :: BranchCondition -> EVM ()+         choosePath (Case v) = do assign result Nothing+                                  pushTo pathConditions (if v then condition else sNot condition)+                                  iteration <- use (iterations . at codeloc . non 0)+                                  assign (cache . path . at (codeloc, iteration)) (Just v)+                                  assign (iterations . at codeloc) (Just (iteration + 1))+                                  continue v          -- Both paths are possible; we ask for more input-         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Iszero+         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Case          -- None of the paths are possible; fail this branch          choosePath Inconsistent = vmError DeadPath @@ -1814,46 +1827,47 @@     input = readMemory (inOffset + 4) (inSize - 4) vm   case fromSized <$> unliteral abi of     Nothing -> vmError UnexpectedSymbolicArg-    Just abi ->-              case Map.lookup abi cheatActions of-                Nothing ->-                  vmError (BadCheatCode (Just abi))-                Just (argTypes, action) ->-                  case input of-                    SymbolicBuffer _ -> vmError UnexpectedSymbolicArg-                    ConcreteBuffer input' ->-                      case runGetOrFail-                             (getAbiSeq (length argTypes) argTypes)-                             (LS.fromStrict input') of-                        Right ("", _, args) ->-                          action (toList args) >>= \case-                            Nothing -> do-                              next-                              push 1-                            Just (encodeAbiValue -> bs) -> do-                              next-                              modifying (state . memory)-                                (writeMemory (ConcreteBuffer bs) outSize 0 outOffset)-                              push 1-                        _ ->-                          vmError (BadCheatCode (Just abi))+    Just abi' ->+      case Map.lookup abi' cheatActions of+        Nothing ->+          vmError (BadCheatCode (Just abi'))+        Just (argTypes, action) ->+          case input of+            SymbolicBuffer _ -> vmError UnexpectedSymbolicArg+            ConcreteBuffer input' ->+              case runGetOrFail+                     (getAbiSeq (length argTypes) argTypes)+                     (LS.fromStrict input') of+                Right ("", _, args) -> do+                  action outOffset outSize (toList args)+                  next+                  push 1+                _ ->+                  vmError (BadCheatCode (Just abi')) -type CheatAction = ([AbiType], [AbiValue] -> EVM (Maybe AbiValue))+type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ())  cheatActions :: Map Word32 CheatAction cheatActions =   Map.fromList     [ action "warp(uint256)" [AbiUIntType 256] $-        \[AbiUInt 256 x] -> do-          assign (block . timestamp) (w256 (W256 x))-          return Nothing,+        \_ _ [AbiUInt 256 x] ->+          assign (block . timestamp) (sw256 $ num x),+      action "roll(uint256)" [AbiUIntType 256] $+        \_ _ [AbiUInt 256 x] ->+          assign (block . number) (w256 (W256 x)),       action "store(address,bytes32,bytes32)" [AbiAddressType, AbiBytesType 32, AbiBytesType 32] $-        \[AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do+        \_ _ [AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do           let slot = w256lit $ word x               new  = w256lit $ word y           fetchAccount a $ \_ -> do-            modifying (env . contracts . ix a . storage) (writeStorage slot new)-          return Nothing+            modifying (env . contracts . ix a . storage) (writeStorage slot new),+      action "load(address,bytes32)" [AbiAddressType, AbiBytesType 32] $+        \outOffset _ [AbiAddress a, AbiBytes 32 x] -> do+          let slot = w256lit $ word x+          accessStorage a slot $ \res -> do+            assign (state . returndata . word256At 0) res+            assign (state . memory . word256At outOffset) res     ]   where     action s ts f = (abiKeccak s, (ts, f))@@ -1875,11 +1889,13 @@         Just target ->           burn xGas $ do             let newContext = CallContext-                  { callContextOffset = xOutOffset-                  , callContextSize = xOutSize-                  , callContextCodehash = view codehash target+                  { callContextTarget    = xTo+                  , callContextContext   = xContext+                  , callContextOffset    = xOutOffset+                  , callContextSize      = xOutSize+                  , callContextCodehash  = view codehash target                   , callContextReversion = view (env . contracts) vm0-                  , callContextSubState = view (tx . substate) vm0+                  , callContextSubState  = view (tx . substate) vm0                   , callContextAbi =                       if xInSize >= 4                       then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)@@ -1959,15 +1975,13 @@          zoom (env . contracts) $ do           oldAcc <- use (at newAddr)-          let oldBal = case oldAcc of-                Nothing -> 0-                Just c  -> view balance c-          assign (at newAddr) (Just newContract)-          assign (ix newAddr . balance) (oldBal + xValue)-          assign (ix newAddr . nonce) 1-          modifying (ix self . balance) (flip (-) xValue)+          let oldBal = maybe 0 (view balance) oldAcc++          assign (at newAddr) (Just (newContract & balance .~ oldBal))           modifying (ix self . nonce) succ +        transfer self newAddr xValue+         pushTrace (FrameTrace newContext)         next         vm1 <- get@@ -1999,7 +2013,7 @@           & set balance (view balance now)           & set nonce   (view nonce now)         RuntimeCode _ ->-          error "internal error: can't replace code of deployed contract"+          error ("internal error: can't replace code of deployed contract " <> show target)       Nothing ->         error "internal error: can't replace code of nonexistent contract" @@ -2084,7 +2098,7 @@       case view frameContext nextFrame of          -- Were we calling?-        CallContext (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do+        CallContext _ _ (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do            let             revertContracts = assign (env . contracts) reversion

@@ -30,6 +30,8 @@ module EVM.ABI   ( AbiValue (..)   , AbiType (..)+  , AbiKind (..)+  , abiKind   , Event (..)   , Anonymity (..)   , Indexed (..)@@ -437,7 +439,7 @@    AbiTupleType ts ->      AbiTuple <$> mapM genAbiValue ts   where-    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax n+    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax (2^n-1)  instance Arbitrary AbiType where   arbitrary = sized $ \n -> oneof $ -- prevent empty tuples@@ -533,7 +535,7 @@ -- Essentially a mix between three types of generators: -- one that strongly prefers values close to 0, one that prefers values close to max -- and one that chooses uniformly.-arbitraryIntegralWithMax :: (Integral a) => Int -> Gen a+arbitraryIntegralWithMax :: (Integral a) => Integer -> Gen a arbitraryIntegralWithMax maxbound =   sized $ \s ->     do let mn = 0 :: Int

@@ -7,7 +7,7 @@  import EVM.Keccak (keccak) import EVM.RLP-import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes)+import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes, Buffer)  import Control.Lens    ((^?), ix) import Data.Bits       (Bits (..), FiniteBits (..), shiftL, shiftR)@@ -40,6 +40,7 @@ data Whiff = Dull            | FromKeccak ByteString            | Var String+           | FromBytes Buffer            | InfixBinOp String Whiff Whiff            | BinOp String Whiff Whiff            | UnOp String Whiff

@@ -20,6 +20,10 @@ import qualified Data.Map as Map import qualified Data.ByteString.Lazy   as LazyByteString +concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]+concatMapM op = foldr f (pure [])+    where f x xs = do x <- op x; if null x then xs else do xs <- xs; pure $ x++xs+ loadDappInfo :: String -> String -> IO DappInfo loadDappInfo path file =   withCurrentDirectory path $@@ -40,7 +44,7 @@         Just repoPath -> do           facts <- Git.loadFacts (Git.RepoAt repoPath)           pure (flip Facts.apply facts)-    params <- getParametersFromEnvironmentVariables+    params <- getParametersFromEnvironmentVariables Nothing     let       opts = UnitTestOptions         { oracle = EVM.Fetch.zero@@ -56,7 +60,10 @@       \case         Just (contractMap, cache) -> do           let unitTests = findUnitTests ("test" `isPrefixOf`) (Map.elems contractMap)-          mapM (runUnitTestContract opts contractMap cache) unitTests+          results <- concatMapM (runUnitTestContract opts contractMap cache) unitTests+          let (passing, _) = unzip results+          pure passing+         Nothing ->           error ("Failed to read Solidity JSON for `" ++ path ++ "'") @@ -90,7 +97,7 @@         Just repoPath -> do           facts <- Git.loadFacts (Git.RepoAt repoPath)           pure (flip Facts.apply facts)-    params <- getParametersFromEnvironmentVariables+    params <- getParametersFromEnvironmentVariables Nothing     let       testOpts = UnitTestOptions         { oracle = EVM.Fetch.zero

@@ -516,7 +516,7 @@  defaultUnitTestOptions :: MonadIO m => m UnitTestOptions defaultUnitTestOptions = do-  params <- liftIO getParametersFromEnvironmentVariables+  params <- liftIO $ getParametersFromEnvironmentVariables Nothing   pure UnitTestOptions     { oracle            = Fetch.zero     , verbose           = Nothing

@@ -27,16 +27,18 @@   , Data (..)   , Path (..)   , apply+  , applyCache+  , cacheFacts   , contractFacts   , vmFacts   , factToFile   , fileToFact   ) where -import EVM          (VM, Contract)+import EVM          (VM, Contract, Cache) import EVM.Concrete (Word) import EVM.Symbolic (litWord, SymWord, forceLit)-import EVM          (balance, nonce, storage, bytecode, env, contracts, contract, state)+import EVM          (balance, nonce, storage, bytecode, env, contracts, contract, state, cache, fetched) import EVM.Types    (Addr)  import qualified EVM@@ -129,6 +131,11 @@       , which = fromIntegral k       } +cacheFacts :: Cache -> Set Fact+cacheFacts c = Set.fromList $ do+  (k, v) <- Map.toList (view EVM.fetched c)+  contractFacts k v+ vmFacts :: VM -> Set Fact vmFacts vm = Set.fromList $ do   (k, v) <- Map.toList (view (env . contracts) vm)@@ -154,6 +161,19 @@     NonceFact   {..} ->       vm & set (env . contracts . ix addr . nonce) what +apply2 :: VM -> Fact -> VM+apply2 vm fact =+  case fact of+    CodeFact    {..} -> flip execState vm $ do+      assign (cache . fetched . at addr) (Just (EVM.initialContract (EVM.RuntimeCode blob)))+      when (view (state . contract) vm == addr) $ EVM.loadContract addr+    StorageFact {..} ->+      vm & over (cache . fetched . ix addr . storage) (EVM.writeStorage (litWord which) (litWord what))+    BalanceFact {..} ->+      vm & set (cache . fetched . ix addr . balance) what+    NonceFact   {..} ->+      vm & set (cache . fetched . ix addr . nonce) what+ -- Sort facts in the right order for `apply1` to work. instance Ord Fact where   compare = comparing f@@ -169,6 +189,12 @@ apply =   -- The set's ordering is relevant; see `apply1`.   foldl apply1+--+-- Applies a set of facts to a VM.+applyCache :: VM -> Set Fact -> VM+applyCache =+  -- The set's ordering is relevant; see `apply1`.+  foldl apply2  factToFile :: Fact -> File factToFile fact = case fact of

@@ -1,5 +1,6 @@ {-# Language GADTs #-} {-# Language StandaloneDeriving #-}+{-# Language LambdaCase #-}  module EVM.Fetch where @@ -7,7 +8,9 @@  import EVM.Types    (Addr, W256, hexText) import EVM.Concrete (Word, w256)-import EVM          (EVM, Contract, StorageModel, initialContract, nonce, balance, external)+import EVM.Symbolic (litWord)+import EVM          (EVM, Contract, Block, StorageModel, initialContract, nonce, balance, external)+import qualified EVM.FeeSchedule as FeeSchedule  import qualified EVM @@ -20,7 +23,7 @@ import Data.Aeson import Data.Aeson.Lens import Data.ByteString (ByteString)-import Data.Text (Text, unpack)+import Data.Text (Text, unpack, pack) import Network.Wreq import Network.Wreq.Session (Session) @@ -29,6 +32,7 @@ -- | Abstract representation of an RPC fetch request data RpcQuery a where   QueryCode    :: Addr         -> RpcQuery ByteString+  QueryBlock   ::                 RpcQuery Block   QueryBalance :: Addr         -> RpcQuery W256   QueryNonce   :: Addr         -> RpcQuery W256   QuerySlot    :: Addr -> W256 -> RpcQuery W256@@ -38,7 +42,7 @@  deriving instance Show (RpcQuery a) -rpc :: String -> [String] -> Value+rpc :: String -> [Value] -> Value rpc method args = object   [ "jsonrpc" .= ("2.0" :: String)   , "id"      .= Number 1@@ -47,17 +51,20 @@   ]  class ToRPC a where-  toRPC :: a -> String+  toRPC :: a -> Value  instance ToRPC Addr where-  toRPC = show+  toRPC = String . pack . show  instance ToRPC W256 where-  toRPC = show+  toRPC = String . pack . show +instance ToRPC Bool where+  toRPC = Bool+ instance ToRPC BlockNumber where-  toRPC Latest          = "latest"-  toRPC (BlockNumber n) = show n+  toRPC Latest          = String "latest"+  toRPC (BlockNumber n) = String . pack $ show n  readText :: Read a => Text -> a readText = read . unpack@@ -65,32 +72,45 @@ fetchQuery   :: Show a   => BlockNumber-  -> (Value -> IO (Maybe Text))+  -> (Value -> IO (Maybe Value))   -> RpcQuery a   -> IO (Maybe a) fetchQuery n f q = do   x <- case q of-    QueryCode addr ->-      fmap hexText  <$>-        f (rpc "eth_getCode" [toRPC addr, toRPC n])-    QueryNonce addr ->-      fmap readText <$>-        f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])-    QueryBalance addr ->-      fmap readText <$>-        f (rpc "eth_getBalance" [toRPC addr, toRPC n])-    QuerySlot addr slot ->-      fmap readText <$>-        f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])-    QueryChainId ->-      fmap readText <$>-        f (rpc "eth_chainId" [toRPC n])+    QueryCode addr -> do+        m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])+        return $ hexText <$> view _String <$> m+    QueryNonce addr -> do+        m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])+        return $ readText <$> view _String <$> m+    QueryBlock -> do+      m <- f (rpc "eth_getBlockByNumber" [toRPC n, toRPC False])+      return $ m >>= parseBlock+    QueryBalance addr -> do+        m <- f (rpc "eth_getBalance" [toRPC addr, toRPC n])+        return $ readText <$> view _String <$> m+    QuerySlot addr slot -> do+        m <- f (rpc "eth_getStorageAt" [toRPC addr, toRPC slot, toRPC n])+        return $ readText <$> view _String <$> m+    QueryChainId -> do+        m <- f (rpc "eth_chainId" [toRPC n])+        return $ readText <$> view _String <$> m   return x -fetchWithSession :: Text -> Session -> Value -> IO (Maybe Text)++parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block+parseBlock json = do+  coinbase   <- readText <$> json ^? key "miner" . _String+  timestamp  <- litWord <$> readText <$> json ^? key "timestamp" . _String+  number     <- readText <$> json ^? key "number" . _String+  difficulty <- readText <$> json ^? key "difficulty" . _String+  -- default codesize, default gas limit, default feescedule+  return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.istanbul++fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value) fetchWithSession url sess x = do   r <- asValue =<< Session.post sess (unpack url) x-  return (r ^? responseBody . key "result" . _String)+  return (r ^? responseBody . key "result")  fetchContractWithSession   :: BlockNumber -> Text -> Addr -> Session -> IO (Maybe Contract)@@ -115,6 +135,16 @@   fmap w256 <$>     fetchQuery n (fetchWithSession url sess) (QuerySlot addr slot) +fetchBlockWithSession+  :: BlockNumber -> Text -> Session -> IO (Maybe Block)+fetchBlockWithSession n url sess =+  fetchQuery n (fetchWithSession url sess) QueryBlock++fetchBlockFrom :: BlockNumber -> Text -> IO (Maybe Block)+fetchBlockFrom n url =+  Session.withAPISession+    (fetchBlockWithSession n url)+ fetchContractFrom :: BlockNumber -> Text -> Addr -> IO (Maybe Contract) fetchContractFrom n url addr =   Session.withAPISession@@ -126,91 +156,109 @@     (\s -> fetchSlotWithSession n url s addr slot)  http :: BlockNumber -> Text -> Fetcher-http n url q =-  case q of-    EVM.PleaseFetchContract addr continue ->-      fetchContractFrom n url addr >>= \case-        Just x  ->-          return (continue x)-        Nothing -> error ("oracle error: " ++ show q)-    EVM.PleaseFetchSlot addr slot continue ->-      fetchSlotFrom n url addr (fromIntegral slot) >>= \case-        Just x  -> return (continue x)-        Nothing -> error ("oracle error: " ++ show q)-    EVM.PleaseAskSMT _ _ _ -> error "smt calls not available for this oracle"--zero :: Fetcher-zero q =-  case q of-    EVM.PleaseFetchContract _ continue ->-      return (continue (initialContract (EVM.RuntimeCode mempty)))-    EVM.PleaseFetchSlot _ _ continue ->-      return (continue 0)-    EVM.PleaseAskSMT _ _ continue ->-      return $ continue EVM.Unknown----type Fetcher = EVM.Query -> IO (EVM ())+http n url = oracle Nothing (Just (n, url)) EVM.ConcreteS True  -- smtsolving + (http or zero)-oracle :: SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Fetcher-oracle state info model q = do+oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Bool -> Fetcher+oracle smtstate info model ensureConsistency q = do   case q of-    EVM.PleaseAskSMT jumpcondition pathconditions continue ->-      flip runReaderT state $ SBV.runQueryT $ do+    EVM.PleaseAskSMT branchcondition pathconditions continue ->+      case smtstate of+        Nothing -> return $ continue EVM.Unknown+        Just state -> flip runReaderT state $ SBV.runQueryT $ do          let pathconds = sAnd pathconditions-         noJump <- checksat $ pathconds .&& jumpcondition ./= 0-         case noJump of-            -- Unsat means condition-            -- cannot be nonzero-            Unsat -> do jump <- checksat $ pathconds .&& jumpcondition .== 0-                        -- can it be zero?-                        case jump of-                          -- No. We are on an inconsistent path.-                          Unsat -> return $ continue EVM.Inconsistent-                          -- Yes. It must be 0.-                          Sat -> return $ continue (EVM.Iszero True)-                          -- Assume 0 is still possible.-                          Unk -> return $ continue (EVM.Iszero True)-            -- Sat means its possible for condition-            -- to be nonzero.-            Sat -> do jump <- checksat $ pathconds .&& jumpcondition .== 0-                      -- can it also be zero?-                      case jump of-                        -- No. It must be nonzero-                        Unsat -> return $ continue (EVM.Iszero False)-                        -- Yes. Both branches possible-                        Sat -> return $ continue EVM.Unknown-                        -- Explore both branches in case of timeout-                        Unk -> return $ continue EVM.Unknown+         -- Is is possible to satisfy the condition?+         continue <$> checkBranch pathconds branchcondition ensureConsistency -            -- If the query times out, we simply explore both paths-            Unk -> return $ continue EVM.Unknown     -- if we are using a symbolic storage model,     -- we generate a new array to the fetched contract here     EVM.PleaseFetchContract addr continue -> do       contract <- case info of-                    Nothing -> return $ Just (initialContract (EVM.RuntimeCode mempty))+                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode mempty)                     Just (n, url) -> fetchContractFrom n url addr       case contract of-        Just x  -> case model of+        Just x -> case model of           EVM.ConcreteS -> return $ continue x-          EVM.InitialS  -> return $ continue $ x & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])-          EVM.SymbolicS -> -            flip runReaderT state $ SBV.runQueryT $ do-              store <- freshArray_ Nothing-              return $ continue $ x & set EVM.storage (EVM.Symbolic store)+          EVM.InitialS  -> return $ continue $ x+             & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])+          EVM.SymbolicS -> case smtstate of+            Nothing -> return (continue $ x+                               & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 []))++            Just state ->+              flip runReaderT state $ SBV.runQueryT $ do+                store <- freshArray_ Nothing+                return $ continue $ x+                  & set EVM.storage (EVM.Symbolic store)         Nothing -> error ("oracle error: " ++ show q)      --- for other queries (there's only slot left right now) we default to zero or http-    _ -> case info of-      Nothing -> zero q-      Just (n, url) -> http n url q+    EVM.PleaseFetchSlot addr slot continue ->+      case info of+        Nothing -> return (continue 0)+        Just (n, url) ->+         fetchSlotFrom n url addr (fromIntegral slot) >>= \case+           Just x  -> return (continue x)+           Nothing ->+             error ("oracle error: " ++ show q) +zero :: Fetcher+zero = oracle Nothing Nothing EVM.ConcreteS True++type Fetcher = EVM.Query -> IO (EVM ())+ checksat :: SBool -> Query CheckSatResult-checksat b = do resetAssertions+checksat b = do push 1                 constrain b                 m <- checkSat-                resetAssertions+                pop 1                 return m++-- | Checks which branches are satisfiable, checking the pathconditions for consistency+-- if the third argument is true.+-- When in debug mode, we do not want to be able to navigate to dead paths,+-- but for normal execution paths with inconsistent pathconditions+-- will be pruned anyway.+checkBranch :: SBool -> SBool -> Bool -> Query EVM.BranchCondition+checkBranch pathconds branchcondition False = do+  constrain pathconds+  checksat branchcondition >>= \case+     -- the condition is unsatisfiable+     Unsat -> -- if pathconditions are consistent then the condition must be false+            return $ EVM.Case False+     -- Sat means its possible for condition to hold+     Sat -> -- is its negation also possible?+            checksat (sNot branchcondition) >>= \case+               -- No. The condition must hold+               Unsat -> return $ EVM.Case True+               -- Yes. Both branches possible+               Sat -> return EVM.Unknown+               -- Explore both branches in case of timeout+               Unk -> return EVM.Unknown+     -- If the query times out, we simply explore both paths+     Unk -> return EVM.Unknown++checkBranch pathconds branchcondition True = do+  constrain pathconds+  checksat branchcondition >>= \case+     -- the condition is unsatisfiable+     Unsat -> -- are the pathconditions even consistent?+              checksat (sNot branchcondition) >>= \case+                -- No. We are on an inconsistent path.+                Unsat -> return EVM.Inconsistent+                -- Yes. The condition must be false.+                Sat -> return $ EVM.Case False+                -- Assume the negated condition is still possible.+                Unk -> return $ EVM.Case False+     -- Sat means its possible for condition to hold+     Sat -> -- is its negation also possible?+            checksat (sNot branchcondition) >>= \case+               -- No. The condition must hold+               Unsat -> return $ EVM.Case True+               -- Yes. Both branches possible+               Sat -> return EVM.Unknown+               -- Explore both branches in case of timeout+               Unk -> return EVM.Unknown++     -- If the query times out, we simply explore both paths+     Unk -> return EVM.Unknown

@@ -18,7 +18,7 @@ -- The AST is a deep JSON structure, so we use Aeson and Lens. import Control.Lens (preview, view, universe) import Data.Aeson (Value (String))-import Data.Aeson.Lens (key, _String, _Array)+import Data.Aeson.Lens (key, _String, _Array, _Integer)  -- We use the FGL graph library for the topological sort. -- (We use four FGL functions and they're all in different modules!)@@ -36,10 +36,10 @@ import Data.ByteString (ByteString) import Data.Foldable (foldl', toList) import Data.List (sort, nub)-import Data.Map (Map, (!))-import Data.Maybe (mapMaybe, isJust)+import Data.Map (Map, (!), (!?))+import Data.Maybe (mapMaybe, isJust, catMaybes, fromMaybe) import Data.Monoid ((<>))-import Data.Text (Text, unpack, pack)+import Data.Text (Text, unpack, pack, intercalate) import Data.Text.Encoding (encodeUtf8) import Text.Read (readMaybe) @@ -97,6 +97,57 @@     asts :: Map Text Value     asts = view (dappSources . sourceAsts) dapp +    topScopeIds :: [Integer]+    topScopeIds = mconcat $ fmap f $ Map.elems asts+      where+        id' = preview (key "id" . _Integer)+        f ast =+          [ fromJust' "no id for SourceUnit" $ id' node+          | node <- universe ast+          , nodeIs "SourceUnit" node+          ]++    contractsAndStructsToRename :: Map Integer Text+    contractsAndStructsToRename =+      Map.fromList+        $ indexed [ x | x <- xs, (snd x) `elem` xs' ]+      where+        xs = mconcat $ fmap f $ Map.elems asts+        xs' = repeated $ fmap snd xs+        scope = preview (key "attributes" . key "scope" . _Integer)+        name = preview (key "attributes" . key "name" . _String)+        id' = preview (key "id" . _Integer)+        p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)+          && (fromJust' "no contract/struct scope" $ scope x) `elem` topScopeIds+        f ast =+          [ ( fromJust' "no id for top scoped contract or struct" $ id' node+            , fromJust' "no id for top scoped contract or struct" $ name node+            )+          | node <- universe ast+          , p node+          ]++    contractStructs :: [(Integer, (Integer, Text))]+    contractStructs = mconcat $ fmap f $ Map.elems asts+      where+        scope = preview (key "attributes" . key "scope" . _Integer)+        cname = preview (key "attributes" . key "canonicalName" . _String)+        id' = preview (key "id" . _Integer)+        p x = (nodeIs "StructDefinition" x)+          && (fromJust' "line:137 nested struct" $ scope x) `Map.member` contractsAndStructsToRename+        f ast =+          [ let+              id'' = fromJust' "no id for nested struct" $ id' node+              cname' = fromJust'+                ("no canonical name of nested struct with id:" ++ show id'') $ cname node+              ref = fromJust'+                ("no scope of nested struct with id:" ++ show id'') $ scope node+            in+              (id'', (ref, cname'))+          | node <- universe ast+          , p node+          ]+   -- We use the target source file to make a relevant subgraph   -- with only files transitively depended on from the target.   case Map.lookup target indices of@@ -116,7 +167,7 @@          -- Take the highest Solidity version from all pragmas.         pragma :: Text-        pragma = maximalPragma (Map.elems asts)+        pragma = maximalPragma (Map.elems (Map.filterWithKey (\k _ -> k `elem` ordered) asts))        -- Read the source files in order and strip unwanted directives.       -- Also add an informative comment with the original source file path.@@ -125,7 +176,13 @@           src <- BS.readFile (unpack path)           pure $ mconcat             [ "////// ", encodeUtf8 path, "\n"-            , stripImportsAndPragmas src (asts ! path), "\n"+            -- Fold over a list of source transforms+            , fst+                (prefixContractAst+                  contractsAndStructsToRename+                  contractStructs+                  (stripImportsAndPragmas (src, 0) (asts ! path))+                  (asts ! path)), "\n"             ]        -- Force all evaluation before any printing happens, to avoid@@ -140,15 +197,43 @@ -- Construct a new Solidity version pragma for the highest mentioned version -- given a list of source file ASTs. maximalPragma :: [Value] -> Text-maximalPragma asts =-  case mapMaybe versions asts of-    [] -> error "no Solidity version pragmas in any source files"-    xs ->-      "pragma solidity "-        <> pack (show (rangeIntersection xs))-        <> ";\n"+maximalPragma asts = (+    case mapMaybe versions asts of+      [] -> error "no Solidity version pragmas in any source files"+      xs ->+        "pragma solidity "+          <> pack (show (rangeIntersection xs))+          <> ";\n"+  )+  <> (+    mconcat . nub . sort . fmap (\ast ->+      mconcat $ fmap+        (\xs -> "pragma "+          <> intercalate " " [x | String x <- xs]+          <> ";\n")+        (otherPragmas ast)+    )+  ) asts +   where+    isVersionPragma :: [Value] -> Bool+    isVersionPragma =+      \case+        String "solidity" : _ -> True+        _ -> False++    pragmaComponents :: Value -> [[Value]]+    pragmaComponents ast = components+      where+        ps :: [Value]+        ps = filter (nodeIs "PragmaDirective") (universe ast)++        components :: [[Value]]+        components = catMaybes $ fmap+          ((fmap toList) . preview (key "attributes" . key "literals" . _Array))+          ps+     -- Simple way to combine many SemVer ranges.  We don't actually     -- optimize these boolean expressions, so the resulting pragma     -- might be redundant, like ">=0.4.23 >=0.5.0 <0.6.0".@@ -160,30 +245,26 @@     versions :: Value -> Maybe SemVerRange     versions ast = fmap grok components       where-        pragma :: Maybe Value-        pragma =-          case filter (nodeIs "PragmaDirective") (universe ast) of-            [x] -> Just x-            []  -> Nothing-            _   -> error "multiple version pragmas"-         components :: Maybe [Value]-        components = fmap toList-          (pragma >>= preview (key "attributes" . key "literals" . _Array))+        components =+          case filter isVersionPragma (pragmaComponents ast) of+            [_:xs] -> Just xs+            []  -> Nothing+            x   -> error $ "multiple version pragmas" ++ show x          grok :: [Value] -> SemVerRange-        grok = \case-          String "solidity" : xs ->-            let-              rangeText = mconcat [x | String x <- xs]-            in-              case parseSemVerRange rangeText of-                Right r -> r-                Left _ ->-                  error ("failed to parse SemVer range " ++ show rangeText)-          x ->-            error ("unrecognized pragma: " ++ show x)+        grok xs =+          let+            rangeText = mconcat [x | String x <- xs]+          in+            case parseSemVerRange rangeText of+              Right r -> r+              Left _ ->+                error ("failed to parse SemVer range " ++ show rangeText) +    otherPragmas :: Value -> [[Value]]+    otherPragmas = (filter (not . isVersionPragma)) . pragmaComponents+ nodeIs :: Text -> Value -> Bool nodeIs t x = isSourceNode && hasRightName   where@@ -192,29 +273,20 @@     hasRightName =       Just t == preview (key "name" . _String) x -stripImportsAndPragmas :: ByteString -> Value -> ByteString-stripImportsAndPragmas bs ast = stripAstNodes bs ast p+stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int)+stripImportsAndPragmas bso ast = stripAstNodes bso ast p   where     p x = nodeIs "ImportDirective" x || nodeIs "PragmaDirective" x -stripAstNodes :: ByteString -> Value -> (Value -> Bool) -> ByteString-stripAstNodes bs ast p =+stripAstNodes :: (ByteString, Int)-> Value -> (Value -> Bool) -> (ByteString, Int)+stripAstNodes bso ast p =   cutRanges [sourceRange node | node <- universe ast, p node]    where-    -- Parses the `src` field of an AST node into a pair of byte indices.-    sourceRange :: Value -> (Int, Int)-    sourceRange v =-      case preview (key "src" . _String) v of-        Just (Text.splitOn ":" -> [readAs -> Just i, readAs -> Just n, _]) ->-          (i, i + n)-        _ ->-          error "internal error: no source position for AST node"-     -- Removes a set of non-overlapping ranges from a bytestring     -- by commenting them out.-    cutRanges :: [(Int, Int)] -> ByteString-    cutRanges (sort -> rs) = fst (foldl' f (bs, 0) rs)+    cutRanges :: [(Int, Int)] -> (ByteString, Int)+    cutRanges (sort -> rs) = foldl' f bso rs       where         f (bs', n) (i, j) =           ( cut bs' (i + n) (j + n)@@ -228,3 +300,134 @@  readAs :: Read a => Text -> Maybe a readAs = readMaybe . Text.unpack++prefixContractAst :: Map Integer Text -> [(Integer, (Integer, Text))] -> (ByteString, Int) -> Value -> (ByteString, Int)+prefixContractAst castr cs bso ast = prefixAstNodes+  where+    bs = fst bso+    refDec = preview (key "attributes" . key "referencedDeclaration" . _Integer)+    name = preview (key "attributes" . key "name" . _String)+    id' = preview (key "id" . _Integer)++    -- Is node top level defined type (contract/interface/struct)+    p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)+      && (fromJust' "id of any" $ id' x) `Map.member` castr++    -- Is node identifier that is referencing top level defined type+    p' x =+      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)+        && (fromJust' "refDec of ident/userdef" $ refDec x) `Map.member` castr++    -- Is node identifier that is referencing a struct nested in a top level+    -- defined contract/interface+    p'' x =+      (nodeIs "Identifier" x || nodeIs "UserDefinedTypeName" x)+      && (isJust $ name x)+      && (+        let+          refs = fmap fst cs+          i = fromJust' "no id for ident/userdef" $ id' x+          ref = fromJust' ("no refDec for ident/userdef: " ++ show i) $ refDec x+          n = fromJust' ("no name for ident/userdef: " ++ show i) $ name x+          cn = fromJust'+            ("no match for lookup in nested structs: "+              ++ show i+              ++ " -> "+              ++ show ref+            ) $ lookup ref cs+        in+          -- XXX: comparing canonical name with name of nested structs+          -- might not be super great+          ref `elem` refs && n == snd cn+      )++    p''' x = p x || p' x || p'' x++    prefixAstNodes :: (ByteString, Int)+    prefixAstNodes  =+      cutRanges [sourceId node | node <- universe ast, p''' node]++    -- Parses the `id` and `attributes.referencedDeclaration` field of an AST node+    -- into a pair of byte indices.+    sourceId :: Value -> (Int, Integer)+    sourceId v =+      if (not $ p v || p' v) &&  p'' v then (+        let+          ref = fromJust' "refDec of nested struct ref" $ refDec v+          cn = fromJust' "no match for lookup in nested structs" $ lookup ref cs+        in+          (end, fst cn)+      ) else+        fromJust' "internal error: no id found for contract reference" x++      where+        (start, end) = sourceRange v+        x :: Maybe (Int, Integer)+        x = case preview (key "name" . _String) v of+          Just t+            | t `elem` ["ContractDefinition", "StructDefinition"] ->+              let+                name' = encodeUtf8 $ fromJust' "no name for contract/struct" $ name v+                bs' = snd $ BS.splitAt (start + snd bso) bs+                pos = start+                  + (BS.length $ fst $ BS.breakSubstring name' bs')+                  + (BS.length name')+              in+                fmap ((,) pos) $ id' v+            | t `elem` ["UserDefinedTypeName", "Identifier"] ->+              fmap ((,) end) $ refDec v+            | otherwise ->+              error "internal error: not a contract reference"+          Nothing ->+            error "internal error: not a contract reference"++    -- Prefix a set of non-overlapping ranges from a bytestring+    -- by commenting them out.+    cutRanges :: [(Int, Integer)] -> (ByteString, Int)+    cutRanges (sort -> rs) = foldl' f bso rs+      where+        f (bs', n) (i, t) =+          let+            t' = "_" <> (castr ! t)+          in+            ( prefix t' bs' (i + n)+            , n + Text.length t' )++    -- Comments out the bytes between two indices from a bytestring.+    prefix :: Text -> ByteString -> Int -> ByteString+    prefix t x i =+      let (a, b) = BS.splitAt i x+      in a <> encodeUtf8 t <> b++-- Parses the `src` field of an AST node into a pair of byte indices.+sourceRange :: Value -> (Int, Int)+sourceRange v =+  case preview (key "src" . _String) v of+    Just (Text.splitOn ":" -> [readAs -> Just i, readAs -> Just n, _]) ->+      (i, i + n)+    _ ->+      error "internal error: no source position for AST node"++fromJust' :: String -> Maybe a -> a+fromJust' msg = \case+  Just x -> x+  Nothing -> error msg++repeated :: Eq a => [a] -> [a]+repeated = fmap fst $ foldl' f ([], [])+  where+    f (acc, seen) x =+      ( if (x `elem` seen) && (not $ x `elem` acc)+        then x : acc+        else acc+      , x : seen+      )++indexed :: [(Integer, Text)] -> [(Integer, Text)]+indexed = fst . foldl' f ([], Map.empty) -- (zip (fmap snd xs) $ replicate (length xs) 0) xs+  where+    f (acc, seen) (id', n) =+      let+        count = (fromMaybe 0 $ seen !? n) + 1+      in+        ((id', pack $ show count) : acc, Map.insert n count seen)

@@ -6,15 +6,15 @@  import EVM (VM, cheatCode, traceForest, traceData, Error (..)) import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..))-import EVM.Dapp (DappInfo, dappSolcByHash, showTraceLocation, dappEventMap)+import EVM.Dapp (DappInfo, dappSolcByHash, dappSolcByName, showTraceLocation, dappEventMap) import EVM.Concrete (Word (..), wordValue)-import EVM.Symbolic (maybeLitWord, Buffer(..), len)-import EVM.Types (W256 (..), num)+import EVM.Symbolic (maybeLitWord, len)+import EVM.Types (W256 (..), num, Buffer(..)) import EVM.ABI (AbiValue (..), Event (..), AbiType (..)) import EVM.ABI (Indexed (NotIndexed), getAbiSeq, getAbi) import EVM.ABI (parseTypeName) import EVM.Solidity (SolcContract, contractName, abiMap)-import EVM.Solidity (methodOutput, methodSignature)+import EVM.Solidity (methodOutput, methodSignature, methodName)  import Control.Arrow ((>>>)) import Control.Lens (view, preview, ix, _2, to, _Just)@@ -58,6 +58,17 @@ showWordExact :: Word -> Text showWordExact (C _ (W256 w)) = humanizeInteger w +showWordExplanation :: W256 -> DappInfo -> Text+showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w+showWordExplanation w dapp =+  let+    fullAbiMap =+      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))+  in+    case Map.lookup (fromIntegral w) fullAbiMap of+      Nothing -> showDec Unsigned w+      Just x  -> "keccak(\"" <> view methodSignature x <> "\")"+ humanizeInteger :: (Num a, Integral a, Show a) => a -> Text humanizeInteger =   Text.intercalate ","@@ -149,6 +160,8 @@       case showTraceLocation dapp trace of         Left x -> " \x1b[90m" <> x <> "\x1b[0m"         Right x -> " \x1b[90m(" <> x <> ")\x1b[0m"+    fullAbiMap =+      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))   in case view traceData trace of     EventTrace (Log _ bytes topics) ->       case topics of@@ -198,10 +211,19 @@         _ ->           "\x1b[91merror\x1b[0m " <> pack (show e) <> pos -    ReturnTrace out (CallContext _ _ hash (Just abi) _ _ _) ->+    ReturnTrace out (CallContext _ _ _ _ hash (Just abi) _ _ _) ->       case getAbiMethodOutput dapp hash abi of         Nothing ->-          "← " <> formatSBinary out+          "← " <>+            case Map.lookup (fromIntegral abi) fullAbiMap of+              Just m  ->+                case (view methodOutput m) of+                  Just (_, t) ->+                    pack (show t) <> " " <> showValue t out+                  Nothing ->+                    formatSBinary out+              Nothing ->+                formatSBinary out         Just (_, t) ->           "← " <> pack (show t) <> " " <> showValue t out     ReturnTrace out (CallContext {}) ->@@ -213,12 +235,25 @@       t     FrameTrace (CreationContext hash _ _ ) ->       "create " <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp) <> pos-    FrameTrace (CallContext _ _ hash abi calldata _ _) ->-      case preview (dappSolcByHash . ix hash . _2) dapp of+    FrameTrace (CallContext target context _ _ hash abi calldata _ _) ->+      let calltype = if target == context+                     then "call "+                     else "delegatecall "+      in case preview (dappSolcByHash . ix hash . _2) dapp of         Nothing ->-          "call [unknown]" <> pos+          calltype+            <> pack (show target)+            <> pack "::"+            <> case Map.lookup (fromIntegral (fromMaybe 0x00 abi)) fullAbiMap of+                 Just m  ->+                   view methodName m+                   <> showCall (catMaybes (getAbiTypes (view methodSignature m))) calldata+                 Nothing ->+                   formatSBinary calldata+            <> pos+         Just solc ->-          "call "+          calltype             <> "\x1b[1m"             <> view (contractName . to contractNamePart) solc             <> "::"@@ -226,7 +261,6 @@                  (fromMaybe "[unknown method]" . maybeAbiName solc)                  abi             <> maybe ("(" <> formatSBinary calldata <> ")")-                 -- todo: if unknown method, then just show raw calldata                  (\x -> showCall (catMaybes x) calldata)                  (abi >>= fmap getAbiTypes . maybeAbiName solc)             <> "\x1b[0m"@@ -260,7 +294,7 @@   _             -> formatBinary bs  showValues :: [AbiType] -> Buffer -> Text-showValues ts (SymbolicBuffer sbs) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts))+showValues ts (SymbolicBuffer  _) = "symbolic: " <> (pack . show $ AbiTupleType (fromList ts)) showValues ts (ConcreteBuffer bs) =   case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of     Right (_, _, xs) -> showAbiValues xs

@@ -6,6 +6,7 @@ module EVM.Solidity   ( solidity   , solcRuntime+  , solidity'   , JumpType (..)   , SolcContract (..)   , StorageItem (..)@@ -49,18 +50,13 @@ import EVM.Keccak import EVM.Types -import Codec.CBOR.Term      (decodeTerm)-import Codec.CBOR.Read      (deserialiseFromBytes) import Control.Applicative import Control.Lens         hiding (Indexed) import Data.Aeson           (Value (..)) import Data.Aeson.Lens import Data.Scientific-import Data.Binary.Get      (runGet, getWord16be) import Data.ByteString      (ByteString)-import Data.ByteString.Lazy (fromStrict) import Data.Char            (isDigit)-import Data.Either          (isRight) import Data.Foldable import Data.Map.Strict      (Map) import Data.Maybe@@ -88,7 +84,7 @@ import qualified Data.Vector            as Vector  data StorageItem = StorageItem {-  _type  :: SlotType,+  _type   :: SlotType,   _offset :: Int,   _slot   :: Int   } deriving (Show, Eq)@@ -440,14 +436,23 @@ -- as the codehash matches otherwise, we don't care if there is some -- difference there. stripBytecodeMetadata :: ByteString -> ByteString-stripBytecodeMetadata bc | BS.length cl /= 2 = bc-                         | BS.length h >= cl' && (isRight . deserialiseFromBytes decodeTerm $ fromStrict cbor) = bc'-                         | otherwise = bc-  where-      l = BS.length bc-      (h, cl) = BS.splitAt (l - 2) bc-      cl' = fromIntegral . runGet getWord16be $ fromStrict cl-      (bc', cbor) = BS.splitAt (BS.length h - cl') h+stripBytecodeMetadata bs =+  let stripCandidates = flip BS.breakSubstring bs <$> knownBzzrPrefixes in+    case find ((/= mempty) . snd) stripCandidates of+      Nothing -> bs+      Just (b, _) -> b++knownBzzrPrefixes :: [ByteString]+knownBzzrPrefixes = [+  -- a1 65 "bzzr0" 0x58 0x20 (solc <= 0.5.8)+  BS.pack [0xa1, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20],+  -- a2 65 "bzzr0" 0x58 0x20 (solc >= 0.5.9)+  BS.pack [0xa2, 0x65, 98, 122, 122, 114, 48, 0x58, 0x20],+  -- a2 65 "bzzr1" 0x58 0x20 (solc >= 0.5.11)+  BS.pack [0xa2, 0x65, 98, 122, 122, 114, 49, 0x58, 0x20],+  -- a2 64 "ipfs" 0x58 0x22 (solc >= 0.6.0)+  BS.pack [0xa2, 0x64, 0x69, 0x70, 0x66, 0x73, 0x58, 0x22]+  ]  -- | Every node in the AST has an ID, and other nodes reference those -- IDs.  This function recurses through the tree looking for objects

@@ -33,7 +33,7 @@ import Control.Lens (use) import Data.Binary.Get (runGetOrFail) import Data.Text (Text)-import EVM.Symbolic (Buffer)+import EVM.Types (Buffer)  import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose) import qualified EVM

@@ -16,7 +16,7 @@ import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational import EVM.Types hiding (Word)-import EVM.Symbolic (litBytes, SymWord(..), sw256, Buffer(..))+import EVM.Symbolic (SymWord(..), sw256) import EVM.Concrete (createAddress, Word) import qualified EVM.FeeSchedule as FeeSchedule import Data.SBV.Trans.Control@@ -133,6 +133,7 @@     }) & set (env . contracts . at (createAddress ethrunAddress 1))              (Just (contractWithStore x initStore)) + -- | Interpreter which explores all paths at -- | branching points. -- | returns a list of possible final evm states@@ -140,14 +141,14 @@   :: Fetch.Fetcher   -> Maybe Integer --max iterations   -> Stepper a-  -> StateT VM IO [a]+  -> StateT VM Query [a] interpret fetcher maxIter =   eval . Operational.view    where     eval       :: Operational.ProgramView Stepper.Action a-      -> StateT VM IO [a]+      -> StateT VM Query [a]      eval (Operational.Return x) =       pure [x]@@ -161,14 +162,33 @@         Stepper.Ask (EVM.PleaseChoosePath continue) -> do           vm <- get           case maxIterationsReached vm maxIter of-            Nothing -> do a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)+            Nothing -> do push 1+                          a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)                           put vm+                          pop 1+                          push 1                           b <- interpret fetcher maxIter (Stepper.evm (continue False) >>= k)+                          pop 1                           return $ a <> b             Just n -> interpret fetcher maxIter (Stepper.evm (continue (not n)) >>= k)-        Stepper.Wait q ->-          do m <- liftIO (fetcher q)-             interpret fetcher maxIter (Stepper.evm m >>= k)+        Stepper.Wait q -> do+          let performQuery =+                do m <- liftIO (fetcher q)+                   interpret fetcher maxIter (Stepper.evm m >>= k)++          case q of+            PleaseAskSMT _ _ continue -> do+              codelocation <- getCodeLocation <$> get+              iters <- use (iterations . at codelocation)+              case iters of+                -- 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.+                Nothing -> interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k)+                _ -> performQuery+            _ -> performQuery+         Stepper.EVM m ->           State.state (runState m) >>= interpret fetcher maxIter . k @@ -184,23 +204,20 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: ContractCode -> Maybe Integer -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)-checkAssert c maxIter signature' concreteArgs = verifyContract c maxIter signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)+checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)+checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)  checkAssertions :: Postcondition checkAssertions (_, out) = case view result out of   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse   _ -> sTrue -verifyContract :: ContractCode -> Maybe Integer -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)-verifyContract code' maxIter signature' concreteArgs storagemodel pre maybepost = do+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) 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 pathConditions ((++) [pre preStateRaw]) preStateRaw-    verify preState maxIter Nothing maybepost-  where theCode = case code' of-          InitCode b    -> b-          RuntimeCode b -> b+    verify preState Nothing Nothing maybepost  pruneDeadPaths :: [VM] -> [VM] pruneDeadPaths =@@ -215,10 +232,11 @@ verify preState maxIter rpcinfo maybepost = do   let model = view (env . storageModel) preState   smtState <- queryState-  results <- io $ fst <$> runStateT (interpret (Fetch.oracle smtState rpcinfo model) maxIter Stepper.runFully) preState+  results <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) rpcinfo model False) maxIter Stepper.runFully) preState   case maybepost of     (Just post) -> do       let livePaths = pruneDeadPaths results+      -- can also do these queries individually (even concurrently!). Could save time and report multiple violations           postC = sOr $ fmap (\postState -> (sAnd (view pathConditions postState)) .&& sNot (post (preState, postState))) livePaths       -- is there any path which can possibly violate       -- the postcondition?@@ -232,7 +250,7 @@                     return $ Left (preState, livePaths)         Sat -> return $ Right preState -    Nothing -> do io $ putStrLn "Q.E.D."+    Nothing -> do io $ putStrLn "Nothing to check"                   return $ Left (preState, pruneDeadPaths results)  -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states.@@ -249,8 +267,12 @@       preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set pathConditions pathconds    smtState <- queryState-  (aVMs, bVMs) <- both (\x -> io $ fst <$> runStateT (interpret (Fetch.oracle smtState Nothing SymbolicS) maxiter Stepper.runFully) x)-    (preStateA, preStateB)+  push 1+  aVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateA+  pop 1+  push 1+  bVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateB+  pop 1   -- Check each pair of endstates for equality:   let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths aVMs, b <- pruneDeadPaths bVMs]       distinct a b =@@ -279,7 +301,6 @@         in sAnd aPath .&& sAnd bPath .&& differingResults   -- If there exists a pair of endstates where this is not the case,   -- the following constraint is satisfiable-  resetAssertions   constrain $ sOr differingEndStates    checkSat >>= \case

@@ -34,9 +34,6 @@ litAddr :: Addr -> SAddr litAddr = SAddr . literal . toSizzle -litBytes :: ByteString -> [SWord 8]-litBytes bs = fmap (toSized . literal) (BS.unpack bs)- maybeLitWord :: SymWord -> Maybe Word maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a) @@ -59,6 +56,9 @@ forceLitBytes :: [SWord 8] -> ByteString forceLitBytes = BS.pack . fmap (fromSized . fromJust . unliteral) +forceBuffer :: Buffer -> ByteString+forceBuffer (ConcreteBuffer b) = b+forceBuffer (SymbolicBuffer b) = forceLitBytes b  -- | Arithmetic operations on SymWord @@ -92,6 +92,13 @@ sgt (S _ x) (S _ y) =   sw256 $ ite (sFromIntegral x .> (sFromIntegral y :: (SInt 256))) 1 0 +shiftRight' :: SymWord -> SymWord -> SymWord+shiftRight' (S _ a') b@(S _ b') = case (num <$> unliteral a', b) of+  (Just n, (S (FromBytes (SymbolicBuffer a)) _)) | n `mod` 8 == 0 && n <= 256 ->+    let bs = replicate (n `div` 8) 0 <> (take ((256 - n) `div` 8) a)+    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)+  _ -> sw256 $ sShiftRight b' a'+ -- | Operations over symbolic memory (list of symbolic bytes) swordAt :: Int -> [SWord 8] -> SymWord swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs@@ -144,9 +151,14 @@ -- the index is symbolic, but it still seems (kind of) manageable -- for the solvers. readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord-readSWordWithBound ind (SymbolicBuffer xs) bound =-  let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]-  in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]+readSWordWithBound ind (SymbolicBuffer xs) bound = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of+  (Just i, Just b) ->+    let bs = truncpad 32 $ drop i (take b xs)+    in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)+  _ -> +    let boundedList = [ite (i .<= bound) x 0 | (x, i) <- zip xs [1..]]+    in sw256 . fromBytes $ [select' boundedList 0 (ind + j) | j <- [0..31]]+ readSWordWithBound ind (ConcreteBuffer xs) bound =   case fromSized <$> unliteral ind of     Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound@@ -154,32 +166,6 @@        -- INVARIANT: bound should always be length xs for concrete bytes        -- so we should be able to safely ignore it here          litWord $ Concrete.readMemoryWord (num x') xs----- | Operations over buffers (concrete or symbolic)---- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`.--- In symbolic settings, it is a list of symbolic bitvectors of size 8.-data Buffer-  = ConcreteBuffer ByteString-  | SymbolicBuffer [SWord 8]-  deriving (Show)--instance Semigroup Buffer where-  ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)-  ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)-  SymbolicBuffer a <> ConcreteBuffer b = SymbolicBuffer (a <> litBytes b)-  SymbolicBuffer a <> SymbolicBuffer b = SymbolicBuffer (a <> b)--instance Monoid Buffer where-  mempty = ConcreteBuffer mempty--instance EqSymbolic Buffer where-  ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)-  ConcreteBuffer a .== SymbolicBuffer b = litBytes a .== b-  SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b-  SymbolicBuffer a .== SymbolicBuffer b = a .== b-  -- a whole foldable instance seems overkill, but length is always good to have! len :: Buffer -> Int

@@ -12,13 +12,13 @@  import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)-import EVM.Symbolic (SymWord(..), Buffer(..))+import EVM.Symbolic (SymWord(..)) import EVM.SymExec (maxIterationsReached) import EVM.Dapp (DappInfo, dappInfo) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) import EVM.Dapp (dappAstSrcMap) import EVM.Debug-import EVM.Format (Signedness (..), showDec, showWordExact)+import EVM.Format (showWordExact, showWordExplanation) import EVM.Format (contractNamePart, contractPathPart, showTraceTree) import EVM.Hexdump (prettyHex) import EVM.Op@@ -40,9 +40,9 @@ import Data.Aeson.Lens import Data.ByteString (ByteString) import Data.Maybe (isJust, fromJust, fromMaybe)-import Data.Map (Map, insert, lookupLT, singleton)+import Data.Map (Map, insert, lookupLT, singleton, filter) import Data.Monoid ((<>))-import Data.Text (Text, unpack, pack)+import Data.Text (Text, pack) import Data.Text.Encoding (decodeUtf8) import Data.List (sort, lookup) import Data.Version (showVersion)@@ -309,6 +309,27 @@     m = interpret mode (view uiStepper ui)     nxt = runStateT (m <* modify renderVm) ui +backstep+  :: (?fetcher :: Fetcher+     ,?maxIter :: Maybe Integer)+  => UiVmState -> EventM n UiVmState+backstep s = case view uiStep s of+  0 -> return s+  n ->+    let+      (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)+      s1 = s+        & set uiVm vm+        & set (uiVm . cache) (view (uiVm . cache) s)+        & set uiStep step+        & set uiStepper stepper+      stepsToTake = n - step - 1++    in+      liftIO $ runStateT (interpret (Step stepsToTake) stepper) s1 >>= \case+        (Continue steps, ui') -> return $ ui' & set uiStepper steps+        _ -> error "unexpected end"+ appEvent   :: (?fetcher::Fetcher, ?maxIter :: Maybe Integer) =>   UiState ->@@ -422,7 +443,7 @@        in takeStep s' (Step 0) --- Vm Overview: p - step+-- Vm Overview: p - backstep appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [])) =   case view uiStep s of     0 ->@@ -445,6 +466,70 @@        takeStep s1 (Step stepsToTake) +-- Vm Overview: P - backstep+appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) =+  case view uiStep s of+    0 ->+      -- We're already at the first step; ignore command.+      continue st+    n -> do+      s1 <- backstep s+      let+        -- find a vm with a different source location than s1+        snapshots' = Data.Map.filter (isNextSourcePosition s1 . fst) (view uiSnapshots s1)+      case lookupLT n snapshots' of+          -- s2 source position is the first one. Go to the beginning.+          Nothing ->+            let+              (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (Step 0)+          -- step until we reach the source location of s1+          Just (step', (vm', stepper')) ->+            let+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (StepUntil (not . isNextSourcePosition s1))++-- Vm Overview: c-p - backstep+appEvent st@(ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =+  case view uiStep s of+    0 ->+      -- We're already at the first step; ignore command.+      continue st+    n -> do+      s1 <- backstep s+      let+        -- find a vm with a different source location than s1+        snapshots' = Data.Map.filter (isNextSourcePositionWithoutEntering s1 . fst) (view uiSnapshots s1)+      case lookupLT n snapshots' of+          -- s2 source position is the first one. Go to the beginning.+          Nothing ->+            let+              (step', (vm', stepper')) = fromJust $ lookupLT (n - 1) (view uiSnapshots s)+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (Step 0)+          -- step until we reach the source location of s1+          Just (step', (vm', stepper')) ->+            let+              s2 = s1+                & set uiVm vm'+                & set (uiVm . cache) (view (uiVm . cache) s1)+                & set uiStep step'+                & set uiStepper stepper'+            in takeStep s2 (StepUntil (not . isNextSourcePosition s1))+ -- Vm Overview: 0 - choose no jump appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) =   case view (uiVm . result) s of@@ -571,6 +656,8 @@         "N      Step fwds to the next source position\n" <>         "C-n    Step fwds to the next source position skipping CALL & CREATE\n" <>         "p      Step back by one instruction\n\n" <>+        "P      Step back to the previous source position\n\n" <>+        "C-p    Step back to the previous source position skipping CALL & CREATE\n\n" <>         "m      Toggle memory pane\n" <>         "0      Choose the branch which does not jump \n" <>         "1      Choose the branch which does jump \n" <>@@ -834,17 +921,6 @@            ])       False       (view uiStackList ui)--showWordExplanation :: W256 -> DappInfo -> Text-showWordExplanation w _ | w > 0xffffffff = showDec Unsigned w-showWordExplanation w dapp =-  let-    fullAbiMap =-      mconcat (map (view abiMap) (Map.elems (view dappSolcByName dapp)))-  in-    case Map.lookup (fromIntegral w) fullAbiMap of-      Nothing -> showDec Unsigned w-      Just x  -> "keccak(\"" <> view methodSignature x <> "\")"  drawBytecodePane :: UiVmState -> UiWidget drawBytecodePane ui =

@@ -84,6 +84,34 @@ instance (ToSizzleBV Addr) instance (FromSizzleBV (WordN 160)) ++litBytes :: ByteString -> [SWord 8]+litBytes bs = fmap (toSized . literal) (BS.unpack bs)++-- | Operations over buffers (concrete or symbolic)++-- | A buffer is a list of bytes. For concrete execution, this is simply `ByteString`.+-- In symbolic settings, it is a list of symbolic bitvectors of size 8.+data Buffer+  = ConcreteBuffer ByteString+  | SymbolicBuffer [SWord 8]+  deriving (Show)++instance Semigroup Buffer where+  ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)+  ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)+  SymbolicBuffer a <> ConcreteBuffer b = SymbolicBuffer (a <> litBytes b)+  SymbolicBuffer a <> SymbolicBuffer b = SymbolicBuffer (a <> b)++instance Monoid Buffer where+  mempty = ConcreteBuffer mempty++instance EqSymbolic Buffer where+  ConcreteBuffer a .== ConcreteBuffer b = literal (a == b)+  ConcreteBuffer a .== SymbolicBuffer b = litBytes a .== b+  SymbolicBuffer a .== ConcreteBuffer b = a .== litBytes b+  SymbolicBuffer a .== SymbolicBuffer b = a .== b+ newtype Addr = Addr { addressWord160 :: Word160 }   deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic) 

@@ -1,3 +1,5 @@+{-# Language LambdaCase #-}+ module EVM.UnitTest where  import Prelude hiding (Word)@@ -12,6 +14,8 @@ import EVM.Format import EVM.Solidity import EVM.Types+import EVM.VMTest+import qualified EVM.Fetch  import qualified EVM.FeeSchedule as FeeSchedule @@ -20,7 +24,6 @@ import qualified Control.Monad.Operational as Operational  import Control.Lens hiding (Indexed)-import Control.Monad ((>=>)) import Control.Monad.State.Strict hiding (state) import qualified Control.Monad.State.Strict as State @@ -29,7 +32,8 @@  import qualified Data.ByteString.Lazy as BSLazy import Data.ByteString    (ByteString)-import Data.SBV+import Data.SBV    hiding (verbose)+import Data.Either        (isRight) import Data.Foldable      (toList) import Data.Map           (Map) import Data.Maybe         (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe)@@ -352,7 +356,7 @@   -> Map Text SolcContract   -> SourceCache   -> (Text, [(Text, [AbiType])])-  -> IO Bool+  -> IO [(Bool, VM)] runUnitTestContract   opts@(UnitTestOptions {..}) contractMap sources (name, testSigs) = do @@ -381,90 +385,114 @@           Text.putStrLn "\x1b[31m[FAIL]\x1b[0m setUp()"           tick "\n"           tick $ failOutput vm1 opts "setUp()"-          pure False+          pure [(False, vm1)]         Just (VMSuccess _) -> do--          -- Define the thread spawner for normal test cases           let-            runOne testName args = do-              let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args)-              (bailed, vm2) <--                runStateT-                  (interpret oracle (execTest opts testName args))-                  vm1-              (success, vm) <- runStateT (interpret oracle (checkFailures opts testName args bailed)) vm2-              if success-              then-                 let gasSpent = num (testGasCall testParams) - view (state . gas) vm2-                     gasText = pack . show $ (fromIntegral gasSpent :: Integer)-                 in-                    pure-                      ("\x1b[32m[PASS]\x1b[0m "-                       <> testName <> argInfo <> " (gas: " <> gasText <> ")"-                       , Right (passOutput vm opts testName)-                      )-              else-                    pure-                      ("\x1b[31m[FAIL]\x1b[0m "-                       <> testName <> argInfo-                       , Left (failOutput vm opts testName)-                      )--          -- Define the thread spawner for property based tests-          let fuzzRun (testName, types) = do-                let args = Args{ replay          = Nothing-                               , maxSuccess      = fuzzRuns-                               , maxDiscardRatio = 10-                               , maxSize         = 100-                               , chatty          = isJust verbose-                               , maxShrinks      = maxBound-                               }-                res <- quickCheckWithResult args (fuzzTest opts testName types vm1)-                case res of-                  Success numTests _ _ _ _ _ ->-                    pure ("\x1b[32m[PASS]\x1b[0m "-                           <> testName <> " (runs: " <> (pack $ show numTests) <> ")",-                           -- vm1 isn't quite the post vm we want...-                           -- but the vm we want is not accessible here anyway...-                           Right (passOutput vm1 opts testName))-                  Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->-                    let abiValue = decodeAbiValue (AbiTupleType (Vector.fromList types)) $ BSLazy.fromStrict $ hexText (pack $ concat failCase)-                        ppOutput = pack $ show abiValue-                    in do-                    -- Run the failing test again to get a proper trace-                    vm2 <- execStateT (interpret oracle (runUnitTest opts testName abiValue)) vm1-                    pure ("\x1b[31m[FAIL]\x1b[0m "-                             <> testName <> ". Counterexample: " <> ppOutput-                             <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\""-                             <> (pack (concat failCase)) <> "\")'\nto test this case again, or \n dapp debug --replay '(\""-                             <> testName <> "\",\"" <> (pack (concat failCase)) <> "\")'\nto debug it.",-                             Left (failOutput vm2 opts testName))-                  _ -> pure ("\x1b[31m[OOPS]\x1b[0m "-                              <> testName, Left (failOutput vm1 opts testName))--          let runTest (testName, []) = runOne testName emptyAbi-              runTest (testName, types) = case replay of-                Nothing -> fuzzRun (testName, types)-                Just (sig, callData) -> if sig == testName-                                         then runOne testName $-                                              decodeAbiValue (AbiTupleType (Vector.fromList types)) callData-                                         else fuzzRun (testName, types)--          let inform (x, y) = Text.putStrLn x >> pure y+            runCache :: ([(Either Text Text, VM)], VM) -> (Text, [AbiType])+                        -> IO ([(Either Text Text, VM)], VM)+            runCache (results, vm) (testName, types) = do+              (t, r, vm') <- runTest opts vm (testName, types)+              Text.putStrLn t+              let vmCached = vm & set (cache . fetched) (view (cache . fetched) vm')+              pure (((r, vm'): results), vmCached) -          -- Run all the test cases and print their status updates-          details <--            mapM (runTest >=> inform) testSigs+          -- Run all the test cases and print their status updates,+          -- accumulating the vm cache throughout+          (details, _) <- foldM runCache ([], vm1) testSigs -          let running = [x | Right x <- details]-          let bailing = [x | Left x <- details]+          let running = [x | (Right x, _) <- details]+          let bailing = [x | (Left  x, _) <- details]            tick "\n"           tick (Text.unlines (filter (not . Text.null) running))           tick (Text.unlines (filter (not . Text.null) bailing)) -          pure (null bailing)+          pure [(isRight r, vm) | (r, vm) <- details] +++runTest :: UnitTestOptions -> VM -> (Text, [AbiType]) -> IO (Text, Either Text Text, VM)+runTest opts@UnitTestOptions{..} vm (testName, []) = runOne opts vm testName emptyAbi+runTest opts@UnitTestOptions{..} vm (testName, types) = case replay of+  Nothing ->+    fuzzRun opts vm testName types+  Just (sig, callData) ->+    if sig == testName+    then runOne opts vm testName $+      decodeAbiValue (AbiTupleType (Vector.fromList types)) callData+    else fuzzRun opts vm testName types++-- | Define the thread spawner for normal test cases +runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM)+runOne opts@UnitTestOptions{..} vm testName args = do+  let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args)+  (bailed, vm') <-+    runStateT+      (interpret oracle (execTest opts testName args))+      vm+  (success, vm'') <-+    runStateT+      (interpret oracle (checkFailures opts testName args bailed)) vm'+  if success+  then+     let gasSpent = num (testGasCall testParams) - view (state . gas) vm'+         gasText = pack $ show (fromIntegral gasSpent :: Integer)+     in+        pure+          ("\x1b[32m[PASS]\x1b[0m "+           <> testName <> argInfo <> " (gas: " <> gasText <> ")"+          , Right (passOutput vm'' opts testName)+          , vm''+          )+  else+        pure+          ("\x1b[31m[FAIL]\x1b[0m "+           <> testName <> argInfo+          , Left (failOutput vm'' opts testName)+          , vm''+          )++-- | Define the thread spawner for property based tests+fuzzRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> IO (Text, Either Text Text, VM)+fuzzRun opts@UnitTestOptions{..} vm testName types = do+  let args = Args{ replay          = Nothing+                 , maxSuccess      = fuzzRuns+                 , maxDiscardRatio = 10+                 , maxSize         = 100+                 , chatty          = isJust verbose+                 , maxShrinks      = maxBound+                 }+  quickCheckWithResult args (fuzzTest opts testName types vm) >>= \case+    Success numTests _ _ _ _ _ ->+      pure ("\x1b[32m[PASS]\x1b[0m "+             <> testName <> " (runs: " <> (pack $ show numTests) <> ")"+             -- this isn't the post vm we actually want, as we+             -- can't retrieve the correct vm from quickcheck+           , Right (passOutput vm opts testName)+           , vm+           )+    Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->+      let abiValue = decodeAbiValue (AbiTupleType (Vector.fromList types)) $ BSLazy.fromStrict $ hexText (pack $ concat failCase)+          ppOutput = pack $ show abiValue+      in do+        -- Run the failing test again to get a proper trace+        vm' <- execStateT (interpret oracle (runUnitTest opts testName abiValue)) vm+        pure ("\x1b[31m[FAIL]\x1b[0m "+               <> testName <> ". Counterexample: " <> ppOutput+               <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\""+               <> (pack (concat failCase)) <> "\")'\nto test this case again, or \n dapp debug --replay '(\""+               <> testName <> "\",\"" <> (pack (concat failCase)) <> "\")'\nto debug it."+             , Left (failOutput vm' opts testName)+             , vm'+             )+    _ -> pure ("\x1b[31m[OOPS]\x1b[0m "+               <> testName+              , Left (failOutput vm opts testName)+              , vm+              )+++ indentLines :: Int -> Text -> Text indentLines n s =   let p = Text.replicate n " "@@ -548,14 +576,18 @@ word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]]  setupCall :: TestVMParams -> Text -> AbiValue -> EVM ()-setupCall TestVMParams{..} sig args  = do+setupCall TestVMParams{..} sig args = do   resetState-  use (env . contracts) >>= assign (tx . txReversion)   assign (tx . isCreate) False   loadContract testAddress-  assign (state . calldata) $ (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)+  assign (state . calldata) (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)   assign (state . caller) (litAddr testCaller)   assign (state . gas) (w256 testGasCall)+  origin' <- fromMaybe (initialContract (RuntimeCode mempty)) <$> use (env . contracts . at testOrigin)+  let originBal = view balance origin'+  when (originBal <= (w256 testGasprice) * (w256 testGasCall)) $ error "insufficient balance for gas cost"+  vm <- get+  put $ initTx vm  initialUnitTestVm :: UnitTestOptions -> SolcContract -> VM initialUnitTestVm (UnitTestOptions {..}) theContract =@@ -572,7 +604,7 @@            , vmoptGaslimit = testGasCreate            , vmoptCoinbase = testCoinbase            , vmoptNumber = testNumber-           , vmoptTimestamp = testTimestamp+           , vmoptTimestamp = litWord $ w256 $ testTimestamp            , vmoptBlockGaslimit = testGaslimit            , vmoptGasprice = testGasprice            , vmoptMaxCodeSize = testMaxCodeSize@@ -589,8 +621,26 @@   in vm     & set (env . contracts . at ethrunAddress) (Just creator) -getParametersFromEnvironmentVariables :: IO TestVMParams-getParametersFromEnvironmentVariables = do++maybeM :: (Monad m) => b -> (a -> b) -> m (Maybe a) -> m b+maybeM def f mayb = do+  may <- mayb+  return $ maybe def f may++getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams+getParametersFromEnvironmentVariables rpc = do+  block' <- maybeM EVM.Fetch.Latest (EVM.Fetch.BlockNumber . read) (lookupEnv "DAPP_TEST_NUMBER")++  (miner,ts,blockNum,diff) <-+    case rpc of+      Nothing  -> return (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 _number+                                      , wordValue _difficulty+                                      )   let     getWord s def = maybe def read <$> lookupEnv s     getAddr s def = maybe def read <$> lookupEnv s@@ -603,11 +653,11 @@     <*> getWord "DAPP_TEST_GAS_CALL" defaultGasForInvoking     <*> getWord "DAPP_TEST_BALANCE_CREATE" defaultBalanceForCreator     <*> getWord "DAPP_TEST_BALANCE_CALL" defaultBalanceForCreated-    <*> getAddr "DAPP_TEST_COINBASE" 0-    <*> getWord "DAPP_TEST_NUMBER" 0-    <*> getWord "DAPP_TEST_TIMESTAMP" 1+    <*> getAddr "DAPP_TEST_COINBASE" miner+    <*> getWord "DAPP_TEST_NUMBER" blockNum+    <*> getWord "DAPP_TEST_TIMESTAMP" ts     <*> getWord "DAPP_TEST_GAS_LIMIT" 0     <*> getWord "DAPP_TEST_GAS_PRICE" 0     <*> getWord "DAPP_TEST_MAXCODESIZE" defaultMaxCodeSize-    <*> getWord "DAPP_TEST_DIFFICULTY" 1+    <*> getWord "DAPP_TEST_DIFFICULTY" diff     <*> getWord "DAPP_TEST_CHAINID" 99

@@ -4,14 +4,16 @@ module EVM.VMTest   ( Case #if MIN_VERSION_aeson(1, 0, 0)-  , parseSuite   , parseBCSuite #endif+  , initTx+  , setupTx   , vmForCase   , checkExpectation   ) where  import qualified EVM+import EVM (contractcode, storage, origStorage, balance, nonce, Storage(..), initialContract) import qualified EVM.Concrete as EVM import qualified EVM.FeeSchedule @@ -25,12 +27,10 @@ import Control.Lens import Control.Monad -import Data.ByteString (ByteString)-import Data.Aeson ((.:), (.:?), FromJSON (..))-import Data.Bifunctor (bimap)+import Data.Aeson ((.:), FromJSON (..)) import Data.Foldable (fold) import Data.Map (Map)-import Data.Maybe (fromMaybe)+import Data.Maybe (fromMaybe, isNothing, isJust) import Data.Witherable (Filterable, catMaybes)  import qualified Data.Map          as Map@@ -52,47 +52,25 @@  data Case = Case   { testVmOpts      :: EVM.VMOpts-  , checkContracts  :: Map Addr Contract-  , testExpectation :: Maybe Expectation+  , checkContracts  :: Map Addr EVM.Contract+  , testExpectation :: Map Addr EVM.Contract   } deriving Show  data BlockchainCase = BlockchainCase   { blockchainBlocks  :: [Block]-  , blockchainPre     :: Map Addr Contract-  , blockchainPost    :: Map Addr Contract+  , blockchainPre     :: Map Addr EVM.Contract+  , blockchainPost    :: Map Addr EVM.Contract   , blockchainNetwork :: String   } deriving Show -data Contract = Contract-  { _balance :: W256-  , _code    :: EVM.ContractCode-  , _nonce   :: W256-  , _storage :: Map W256 W256-  , _create  :: Bool-  } deriving Show--data Expectation = Expectation-  { expectedOut       :: Maybe ByteString-  , expectedContracts :: Map Addr Contract-  , expectedGas       :: Maybe W256-  } deriving Show--makeLenses ''Contract--accountAt :: Addr -> Getter (Map Addr Contract) Contract+accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract accountAt a = (at a) . (to $ fromMaybe newAccount) -touchAccount :: Addr -> Map Addr Contract -> Map Addr Contract+touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract touchAccount a = Map.insertWith (flip const) a newAccount -newAccount :: Contract-newAccount = Contract-  { _balance = 0-  , _code    = EVM.RuntimeCode mempty-  , _nonce   = 0-  , _storage = mempty-  , _create  = False-  }+newAccount :: EVM.Contract+newAccount = initialContract $ EVM.RuntimeCode mempty  splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b) splitEithers =@@ -100,12 +78,16 @@   . (fmap fst &&& fmap snd)   . (fmap (preview _Left &&& preview _Right)) -checkStateFail :: Bool -> Case -> Expectation -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool-checkStateFail diff x expectation vm (okState, okMoney, okNonce, okData, okCode) = do+checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool, Bool) -> IO Bool+checkStateFail diff x vm (okState, okMoney, okNonce, okData, okCode) = do   let-    printField :: (v -> String) -> Map Addr v -> IO ()-    printField f d = putStrLn $ Map.foldrWithKey (\k v acc ->-      acc ++ show k ++ " : " ++ f v ++ "\n") "" d+    printContracts :: Map Addr EVM.Contract -> IO ()+    printContracts cs = putStrLn $ Map.foldrWithKey (\k v acc ->+      acc ++ show k ++ " : "+                   ++ (show . toInteger  $ (view nonce v)) ++ " "+                   ++ (show . toInteger  $ (view balance v)) ++ " "+                   ++ (printStorage $ (view storage v))+        ++ "\n") "" cs      reason = map fst (filter (not . snd)         [ ("bad-state",       okMoney || okNonce || okData  || okCode || okState)@@ -115,54 +97,28 @@         , ("bad-code",    not okCode  || okMoney || okNonce || okData || okState)         ])     check = checkContracts x-    initial = initTx x-    expected = expectedContracts expectation+    expected = testExpectation x     actual = view (EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))) vm     printStorage (EVM.Symbolic c) = show c     printStorage (EVM.Concrete c) = show $ Map.toList c    putStr (unwords reason)   when (diff && (not okState)) $ do-    putStrLn "\nCheck balance/state: "-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "-                   ++ (show . toInteger  $ _balance v) ++ " "-                   ++ (show . Map.toList $ _storage v)) check-    putStrLn "\nInitial balance/state: "-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "-                   ++ (show . toInteger  $ _balance v) ++ " "-                   ++ (show . Map.toList $ _storage v)) initial+    putStrLn "\nPre balance/state: "+    printContracts check     putStrLn "\nExpected balance/state: "-    printField (\v -> (show . toInteger  $ _nonce v) ++ " "-                   ++ (show . toInteger  $ _balance v) ++ " "-                   ++ (show . Map.toList $ _storage v)) expected+    printContracts expected     putStrLn "\nActual balance/state: "-    printField (\v -> (show . toInteger  $ EVM._nonce v) ++ " "-                   ++ (show . toInteger  $ EVM._balance v) ++ " "-                   ++ (printStorage      $ EVM._storage v)) actual+    printContracts actual   return okState  checkExpectation :: Bool -> Case -> EVM.VM -> IO Bool-checkExpectation diff x vm =-  case (testExpectation x, view EVM.result vm) of-    (Just expectation, _) -> do-      let (okState, b2, b3, b4, b5) =-            checkExpectedContracts vm (expectedContracts expectation)-      _ <- if not okState then-               checkStateFail-                 diff x expectation vm (okState, b2, b3, b4, b5)-           else return True-      return okState--    (Nothing, Just (EVM.VMSuccess _)) -> do-      putStr "unexpected-success"-      return False--    (Nothing, Just (EVM.VMFailure _)) ->-      return True--    (_, Nothing) -> do-      print (view EVM.result vm)-      error "internal error"+checkExpectation diff x vm = do+  let expectation = testExpectation x+  let (okState, b2, b3, b4, b5) = checkExpectedContracts vm $ expectation+  unless okState $ void $ checkStateFail+    diff x vm (okState, b2, b3, b4, b5)+  return okState  -- quotient account state by nullness (~=) :: Map Addr EVM.Contract -> Map Addr EVM.Contract -> Bool@@ -173,10 +129,10 @@         padded_cs  = padNewAccounts cs  (Map.keys cs')     in padded_cs == padded_cs' -checkExpectedContracts :: EVM.VM -> Map Addr Contract -> (Bool, Bool, Bool, Bool, Bool)+checkExpectedContracts :: EVM.VM -> Map Addr EVM.Contract -> (Bool, Bool, Bool, Bool, Bool) checkExpectedContracts vm expected =   let cs = vm ^. EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))-      expectedCs = clearOrigStorage <$> realizeContracts expected+      expectedCs = clearOrigStorage <$> expected   in ( (expectedCs ~= cs)      , (clearBalance <$> expectedCs) ~= (clearBalance <$> cs)      , (clearNonce   <$> expectedCs) ~= (clearNonce   <$> cs)@@ -185,45 +141,44 @@      )  clearOrigStorage :: EVM.Contract -> EVM.Contract-clearOrigStorage = set EVM.origStorage mempty+clearOrigStorage = set origStorage mempty  clearZeroStorage :: EVM.Contract -> EVM.Contract-clearZeroStorage c = case EVM._storage c of+clearZeroStorage c = case view storage c of   EVM.Symbolic _ -> c   EVM.Concrete m -> let store = Map.filter (\x -> forceLit x /= 0) m                     in set EVM.storage (EVM.Concrete store) c  clearStorage :: EVM.Contract -> EVM.Contract-clearStorage = set EVM.storage (EVM.Concrete mempty)+clearStorage = set storage (EVM.Concrete mempty)  clearBalance :: EVM.Contract -> EVM.Contract-clearBalance = set EVM.balance 0+clearBalance = set balance 0  clearNonce :: EVM.Contract -> EVM.Contract-clearNonce = set EVM.nonce 0+clearNonce = set nonce 0  clearCode :: EVM.Contract -> EVM.Contract-clearCode = set EVM.contractcode (EVM.RuntimeCode mempty)+clearCode = set contractcode (EVM.RuntimeCode mempty)  #if MIN_VERSION_aeson(1, 0, 0) -instance FromJSON Contract where-  parseJSON (JSON.Object v) = Contract-    <$> v .: "balance"-    <*> (EVM.RuntimeCode <$> (hexText <$> v .: "code"))-    <*> v .: "nonce"-    <*> v .: "storage"-    <*> pure False-  parseJSON invalid =-    JSON.typeMismatch "VM test case contract" invalid+instance FromJSON EVM.Contract where+  parseJSON (JSON.Object v) = do+    code <- (EVM.RuntimeCode <$> (hexText <$> v .: "code"))+    storage' <- Map.mapKeys EVM.w256 <$> v .: "storage"+    balance' <- v .: "balance"+    nonce'   <- v .: "nonce"+    return+      $+      EVM.initialContract code+       & balance .~ EVM.w256 balance'+       & nonce   .~ EVM.w256 nonce'+       & storage .~ EVM.Concrete (fmap (litWord . EVM.w256) storage')+       & origStorage .~ fmap EVM.w256 storage' -instance FromJSON Case where-  parseJSON (JSON.Object v) = Case-    <$> parseVmOpts v-    <*> parseContracts Pre v-    <*> parseExpectation v   parseJSON invalid =-    JSON.typeMismatch "VM test case" invalid+    JSON.typeMismatch "Contract" invalid  instance FromJSON BlockchainCase where   parseJSON (JSON.Object v) = BlockchainCase@@ -247,63 +202,19 @@   parseJSON invalid =     JSON.typeMismatch "Block" invalid -parseVmOpts :: JSON.Object -> JSON.Parser EVM.VMOpts-parseVmOpts v =-  do envV  <- v .: "env"-     execV <- v .: "exec"-     case (envV, execV) of-       (JSON.Object env, JSON.Object exec) ->-         EVM.VMOpts-           <$> (dataField exec "code" >>= pure . EVM.initialContract . EVM.RuntimeCode)-           <*> (dataField exec "data" >>= \a -> pure ( (ConcreteBuffer a), literal . num $ BS.length a))-           <*> (w256lit <$> wordField exec "value")-           <*> addrField exec "address"-           <*> (litAddr <$> addrField exec "caller")-           <*> addrField exec "origin"-           <*> wordField exec "gas" -- XXX: correct?-           <*> wordField exec "gas" -- XXX: correct?-           <*> wordField env  "currentNumber"-           <*> wordField env  "currentTimestamp"-           <*> addrField env  "currentCoinbase"-           <*> wordField env  "currentDifficulty"-           <*> pure 0xffffffff-           <*> wordField env  "currentGasLimit"-           <*> wordField exec "gasPrice"-           <*> pure (EVM.FeeSchedule.istanbul)-           <*> pure 1-           <*> pure False-           <*> pure EVM.ConcreteS-       _ ->-         JSON.typeMismatch "VM test case" (JSON.Object v)- parseContracts ::-  Which -> JSON.Object -> JSON.Parser (Map Addr Contract)+  Which -> JSON.Object -> JSON.Parser (Map Addr EVM.Contract) parseContracts w v =   v .: which >>= parseJSON   where which = case w of           Pre  -> "pre"           Post -> "postState" -parseExpectation :: JSON.Object -> JSON.Parser (Maybe Expectation)-parseExpectation v =-  do out       <- fmap hexText <$> v .:? "out"-     contracts <- v .:? "post"-     gas       <- v .:? "gas"-     case (out, contracts, gas) of-       (Just x, Just y, Just z) ->-         return (Just (Expectation (Just x) y (Just z)))-       _ ->-         return Nothing--parseSuite ::-  Lazy.ByteString -> Either String (Map String Case)-parseSuite = JSON.eitherDecode'- parseBCSuite ::   Lazy.ByteString -> Either String (Map String Case) parseBCSuite x = case (JSON.eitherDecode' x) :: Either String (Map String BlockchainCase) of   Left e        -> Left e-  Right bcCases -> let allCases = (fromBlockchainCase <$> bcCases)+  Right bcCases -> let allCases = fromBlockchainCase <$> bcCases                        keepError (Left e) = errorFatal e                        keepError _        = True                        filteredCases = Map.filter keepError allCases@@ -315,32 +226,10 @@     else Right parsedCases #endif -realizeContracts :: Map Addr Contract -> Map Addr EVM.Contract-realizeContracts = Map.fromList . map f . Map.toList-  where-    f (a, x) = (a, realizeContract x)--realizeContract :: Contract -> EVM.Contract-realizeContract x =-  EVM.initialContract (x ^. code)-    & EVM.balance .~ EVM.w256 (x ^. balance)-    & EVM.nonce   .~ EVM.w256 (x ^. nonce)-    & EVM.storage .~ EVM.Concrete (-        Map.fromList .-        map (bimap EVM.w256 (litWord . EVM.w256)) .-        Map.toList $ x ^. storage-        )-    & EVM.origStorage .~ (-        Map.fromList .-        map (bimap EVM.w256 EVM.w256) .-        Map.toList $ x ^. storage-        )- data BlockchainError   = TooManyBlocks   | TooManyTxs   | NoTxs-  | TargetMissing   | SignatureUnverified   | InvalidTx   | OldNetwork@@ -350,7 +239,6 @@ errorFatal :: BlockchainError -> Bool errorFatal TooManyBlocks = True errorFatal TooManyTxs = True-errorFatal TargetMissing = True errorFatal SignatureUnverified = True errorFatal InvalidTx = True errorFatal _ = False@@ -359,75 +247,32 @@ fromBlockchainCase (BlockchainCase blocks preState postState network) =   case (blocks, network) of     ([block], "Istanbul") -> case blockTxs block of-      [tx] -> case txToAddr tx of-        Nothing -> fromCreateBlockchainCase block tx preState postState-        Just _  -> fromNormalBlockchainCase block tx preState postState+      [tx] -> fromBlockchainCase' block tx preState postState       []        -> Left NoTxs       _         -> Left TooManyTxs     ([_], _) -> Left OldNetwork     (_, _)        -> Left TooManyBlocks -fromCreateBlockchainCase :: Block -> Transaction-                         -> Map Addr Contract -> Map Addr Contract-                         -> Either BlockchainError Case-fromCreateBlockchainCase block tx preState postState =-  case (sender 1 tx,-        checkCreateTx tx block preState) of-    (Nothing, _) -> Left SignatureUnverified-    (_, Nothing) -> Left FailedCreate-    (Just origin, Just (checkState, createdAddr)) -> let-      feeSchedule = EVM.FeeSchedule.istanbul-      in Right $ Case-         (EVM.VMOpts-          { vmoptContract      = EVM.initialContract (EVM.InitCode (txData tx))-          , vmoptCalldata      = (mempty, 0)-          , vmoptValue         = w256lit $ txValue tx-          , vmoptAddress       = createdAddr-          , vmoptCaller        = (litAddr origin)-          , vmoptOrigin        = origin-          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)-          , vmoptGaslimit      = txGasLimit tx-          , vmoptNumber        = blockNumber block-          , vmoptTimestamp     = blockTimestamp block-          , vmoptCoinbase      = blockCoinbase block-          , vmoptDifficulty    = blockDifficulty block-          , vmoptMaxCodeSize   = 24576-          , vmoptBlockGaslimit = blockGasLimit block-          , vmoptGasprice      = txGasPrice tx-          , vmoptSchedule      = feeSchedule-          , vmoptChainId       = 1-          , vmoptCreate        = True-          , vmoptStorageModel  = EVM.ConcreteS-          })-        checkState-        (Just $ Expectation Nothing postState Nothing)---fromNormalBlockchainCase :: Block -> Transaction-                       -> Map Addr Contract -> Map Addr Contract+fromBlockchainCase' :: Block -> Transaction+                       -> Map Addr EVM.Contract -> Map Addr EVM.Contract                        -> Either BlockchainError Case-fromNormalBlockchainCase block tx preState postState =-  let Just toAddr = txToAddr tx-      feeSchedule = EVM.FeeSchedule.istanbul-      toCode = Map.lookup toAddr preState-      theCode = case toCode of-          Nothing -> EVM.RuntimeCode mempty-          Just c -> view code c-  in case (toAddr , toCode , sender 1 tx , checkNormalTx tx block preState) of-      (_, _, Nothing, _) -> Left SignatureUnverified-      (_, _, _, Nothing) -> Left InvalidTx-      (_, _, Just origin, Just checkState) -> Right $ Case+fromBlockchainCase' block tx preState postState =+  let isCreate = isNothing (txToAddr tx)+  in 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         (EVM.VMOpts          { vmoptContract      = EVM.initialContract theCode-         , vmoptCalldata      = (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)+         , vmoptCalldata      = cd          , vmoptValue         = litWord (EVM.w256 $ txValue tx)          , vmoptAddress       = toAddr-         , vmoptCaller        = (litAddr origin)+         , vmoptCaller        = litAddr origin          , vmoptOrigin        = origin          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)          , vmoptGaslimit      = txGasLimit tx          , vmoptNumber        = blockNumber block-         , vmoptTimestamp     = blockTimestamp block+         , vmoptTimestamp     = litWord $ EVM.w256 $ blockTimestamp block          , vmoptCoinbase      = blockCoinbase block          , vmoptDifficulty    = blockDifficulty block          , vmoptMaxCodeSize   = 24576@@ -435,92 +280,96 @@          , vmoptGasprice      = txGasPrice tx          , vmoptSchedule      = feeSchedule          , vmoptChainId       = 1-         , vmoptCreate        = False+         , vmoptCreate        = isCreate          , vmoptStorageModel  = EVM.ConcreteS          })         checkState-        (Just $ Expectation Nothing postState Nothing)+        postState+          where+            toAddr = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)+            senderNonce = EVM.wordValue $ view (accountAt origin . nonce) preState+            feeSchedule = EVM.FeeSchedule.istanbul+            toCode = Map.lookup toAddr preState+            theCode = if isCreate+                      then EVM.InitCode (txData tx)+                      else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode+            cd = if isCreate+                 then (mempty, 0)+                 else (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)  -validateTx :: Transaction -> Map Addr Contract -> Maybe Bool+validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe () validateTx tx cs = do   origin        <- sender 1 tx   originBalance <- (view balance) <$> view (at origin) cs   originNonce   <- (view nonce)   <$> view (at origin) cs-  let gasDeposit = fromIntegral (txGasPrice tx) * (txGasLimit tx)-  return $ gasDeposit + (txValue tx) <= originBalance-    && (txNonce tx) == originNonce--checkNormalTx :: Transaction -> Block -> Map Addr Contract -> Maybe (Map Addr Contract)-checkNormalTx tx block prestate = do-  toAddr <- txToAddr tx-  origin <- sender 1 tx-  valid  <- validateTx tx prestate-  let gasDeposit = fromIntegral (txGasPrice tx) * (txGasLimit tx)-      coinbase   = blockCoinbase block-  if not valid then mzero else-    return $-    (Map.adjust ((over nonce   (+ 1))-               . (over balance (subtract gasDeposit))) origin)-    . touchAccount origin-    . touchAccount toAddr-    . touchAccount coinbase $ prestate+  let gasDeposit = EVM.w256 $ (txGasPrice tx) * (txGasLimit tx)+  if gasDeposit + (EVM.w256 $ txValue tx) <= originBalance+    && (EVM.w256 $ txNonce tx) == originNonce+  then Just ()+  else Nothing -checkCreateTx :: Transaction -> Block -> Map Addr Contract -> Maybe ((Map Addr Contract), Addr)-checkCreateTx tx block prestate = do+checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)+checkTx tx block prestate = do   origin <- sender 1 tx-  valid  <- validateTx tx prestate-  let gasDeposit  = fromIntegral (txGasPrice tx) * (txGasLimit tx)-      coinbase    = blockCoinbase block-      senderNonce = view (accountAt origin . nonce) prestate-      createdAddr = EVM.createAddress origin senderNonce-      prevCode    = view (accountAt createdAddr .  code) prestate-      prevNonce   = view (accountAt createdAddr . nonce) prestate-  if (prevCode /= EVM.RuntimeCode mempty) || (prevNonce /= 0) || (not valid)+  validateTx tx prestate+  let isCreate   = isNothing (txToAddr tx)+      senderNonce = EVM.wordValue $ view (accountAt origin . nonce) prestate+      toAddr      = fromMaybe (EVM.createAddress origin senderNonce) (txToAddr tx)+      prevCode    = view (accountAt toAddr . contractcode) prestate+      prevNonce   = view (accountAt toAddr . nonce) prestate+  if isCreate && ((prevCode /= EVM.RuntimeCode mempty) || (prevNonce /= 0))   then mzero   else-    return-    ((Map.adjust ((over nonce   (+ 1))-                 . (over balance (subtract gasDeposit))) origin)-    . touchAccount origin-    . touchAccount createdAddr-    . touchAccount coinbase $ prestate, createdAddr)--initTx :: Case -> Map Addr Contract-initTx x =-  let-    checkState = checkContracts x-    opts     = testVmOpts x-    toAddr   = EVM.vmoptAddress  opts-    origin   = EVM.vmoptOrigin   opts-    value    = EVM.vmoptValue    opts-    initcode = EVM._contractcode (EVM.vmoptContract opts)-    creation = EVM.vmoptCreate   opts-  in-    (Map.adjust (over balance (subtract (EVM.wordValue $ forceLit value))) origin)-    . (Map.adjust (over balance (+ (EVM.wordValue $ forceLit value))) toAddr)-    . (if creation-       then (Map.adjust (set code initcode) toAddr)-          . (Map.adjust (set nonce 1) toAddr)-          . (Map.adjust (set storage mempty) toAddr)-          . (Map.adjust (set create True) toAddr)-       else id)-    $ checkState+    return $ prestate  vmForCase :: Case -> EVM.VM vmForCase x =   let-    checkState = checkContracts x-    initState = initTx x-    opts = testVmOpts x-    creation = EVM.vmoptCreate opts-    touchedAccounts =-      if creation then-        [EVM.vmoptOrigin opts]-      else-        [EVM.vmoptOrigin opts, EVM.vmoptAddress opts]+    vm = EVM.makeVm (testVmOpts x)+      & set (EVM.env . EVM.contracts) (checkContracts x)   in-    EVM.makeVm (testVmOpts x)-    & EVM.env . EVM.contracts .~ realizeContracts initState-    & EVM.tx . EVM.txReversion .~ realizeContracts checkState-    & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touchedAccounts+    initTx vm++-- | Increments origin nonce and pays gas deposit+setupTx :: Addr -> Addr -> EVM.Word -> EVM.Word -> Map Addr EVM.Contract -> Map Addr EVM.Contract+setupTx origin coinbase gasPrice gasLimit prestate =+  let gasCost = gasPrice * gasLimit+  in (Map.adjust ((over nonce   (+ 1))+               . (over balance (subtract gasCost))) origin)+    . touchAccount origin+    . touchAccount coinbase $ prestate++-- | Given a valid tx loaded into the vm state,+-- subtract gas payment from the origin, increment the nonce+-- and pay receiving address+initTx :: EVM.VM -> EVM.VM+initTx vm = let+    toAddr   = view (EVM.state . EVM.contract) vm+    origin   = view (EVM.tx . EVM.origin) vm+    gasPrice = view (EVM.tx . EVM.gasprice) vm+    gasLimit = view (EVM.tx . EVM.txgaslimit) vm+    coinbase = view (EVM.block . EVM.coinbase) vm+    value    = view (EVM.state . EVM.callvalue) vm+    toContract = initialContract (EVM.InitCode (view (EVM.state . EVM.code) vm))+    preState = setupTx origin coinbase gasPrice gasLimit $ view (EVM.env . EVM.contracts) vm+    oldBalance = view (accountAt toAddr . balance) preState+    creation = view (EVM.tx . EVM.isCreate) vm+    initState =+      (if isJust (maybeLitWord value)+       then (Map.adjust (over balance (subtract (forceLit value))) origin)+        . (Map.adjust (over balance (+ (forceLit value))) toAddr)+       else id)+      . (if creation+         then Map.insert toAddr (toContract & balance .~ oldBalance)+         else touchAccount toAddr)+      $ preState++    touched = if creation+              then [origin]+              else [origin, toAddr]++    in+      vm & EVM.env . EVM.contracts .~ initState+         & EVM.tx . EVM.txReversion .~ preState+         & EVM.tx . EVM.substate . EVM.touchedAccounts .~ touched

@@ -1,4 +1,5 @@ {-# Language OverloadedStrings #-}+{-# Language LambdaCase #-} {-# Language QuasiQuotes #-} {-# Language TypeSynonymInstances #-} {-# Language FlexibleInstances #-}@@ -18,23 +19,28 @@ import Test.Tasty.QuickCheck-- hiding (forAll) import Test.Tasty.HUnit -import Control.Monad.State.Strict (execState, runState)+import Control.Monad.State.Strict (execState, runState, when) import Control.Lens hiding (List, pre)  import qualified Data.Vector as Vector import Data.String.Here  import Control.Monad.Fail+import Debug.Trace  import Data.Binary.Put (runPut)-import Data.SBV hiding ((===), forAll)+import Data.SBV hiding ((===), forAll, sList) import Data.SBV.Control+import Data.SBV.Trans (sList)+import Data.SBV.List (implode)+import qualified Data.SBV.List as SL import qualified Data.Map as Map import Data.Binary.Get (runGetOrFail)  import EVM hiding (Query) import EVM.SymExec import EVM.Symbolic+import EVM.Concrete (w256) import EVM.ABI import EVM.Exec import EVM.Patricia as Patricia@@ -117,6 +123,31 @@         in x == y     ] +  , testGroup "metadata stripper"+    [ testCase "it strips the metadata for solc => 0.6" $ do+        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+        let srccode =+              [i|+                contract A {+                  uint y;+                  constructor(uint x) public {+                    y = x;+                  }+                }+                |]++        (json, path) <- solidity' srccode+        let Just (solc, _, _) = readJSON json+            initCode :: ByteString+            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)+    ]+   , testGroup "RLP encodings"     [ testProperty "rlp decode is a retraction (bytes)" $ \(Bytes bs) -> --      withMaxSuccess 100000 $@@ -155,19 +186,15 @@             }           }           |]-        let asWord :: [SWord 8] -> SWord 256-            asWord = fromBytes-            pre preVM = let SymbolicBuffer bs = ditch 4 (fst $ view (state . calldata) preVM)-                            (x, y) = splitAt 32 bs-                        in asWord x .<= asWord x + asWord y+        let pre preVM = let [x, y] = getStaticAbiArgs preVM+                        in x .<= x + y                            .&& view (state . callvalue) preVM .== 0             post = Just $ \(prestate, poststate) ->-              let SymbolicBuffer input = fst $ view (state.calldata) prestate-                  (x, y) = splitAt 32 (drop 4 input)+              let [x, y] = getStaticAbiArgs prestate               in case view result poststate of-                Just (VMSuccess (SymbolicBuffer out)) -> (asWord out) .== (asWord x) + (asWord y)+                Just (VMSuccess (SymbolicBuffer out)) -> (fromBytes out) .== x + y                 _ -> sFalse-        Left (_, res) <- runSMT $ query $ verifyContract (RuntimeCode safeAdd) Nothing (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post+        Left (_, res) <- runSMT $ query $ verifyContract safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post         putStrLn $ "successfully explored: " <> show (length res) <> " paths"      , @@ -180,21 +207,17 @@             }           }           |]-        let asWord :: [SWord 8] -> SWord 256-            asWord = fromBytes-            pre preVM = let SymbolicBuffer bs = ditch 4 (fst $ view (state . calldata) preVM)-                            (x, y) = splitAt 32 bs-                           in (asWord x .<= asWord x + asWord y)-                              .&& (x .== y)-                              .&& view (state . callvalue) preVM .== 0-            post = Just $ \(prestate, poststate)-              -> let SymbolicBuffer input = fst $ view (state.calldata) prestate-                     (_, y) = splitAt 32 (drop 4 input)-                 in case view result poststate of-                      Just (VMSuccess (SymbolicBuffer out)) -> asWord out .== 2 * asWord y+        let pre preVM = let [x, y] = getStaticAbiArgs preVM+                        in (x .<= x + y)+                           .&& (x .== y)+                           .&& view (state . callvalue) preVM .== 0+            post (prestate, poststate) =+              let [_, y] = getStaticAbiArgs prestate+              in case view result poststate of+                      Just (VMSuccess (SymbolicBuffer out)) -> fromBytes out .== 2 * y                       _ -> sFalse         Left (_, res) <- runSMTWith z3 $ query $-          verifyContract (RuntimeCode safeAdd) Nothing (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post+          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@@ -208,15 +231,15 @@           }           |]         bs <- runSMTWith cvc4 $ query $ do-          Right vm <- checkAssert (RuntimeCode factor) Nothing (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+          Right vm <- checkAssert 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 AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))-            [AbiUInt 256 x, AbiUInt 256 y] = Vector.toList xy+        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         Just c <- solcRuntime "A"           [i|@@ -230,7 +253,7 @@           |]         let pre vm = 0 .== view (state . callvalue) vm             post = Just $ \(prestate, poststate) ->-              let SymbolicBuffer y = ditch 4 $ fst (view (state.calldata) prestate)+              let [y] = getStaticAbiArgs prestate                   this = view (state . codeContract) prestate                   Just preC = view (env.contracts . at this) prestate                   Just postC = view (env.contracts . at this) poststate@@ -239,9 +262,9 @@                   prex = readArray prestore 0                   postx = readArray poststore 0               in case view result poststate of-                Just (VMSuccess _) -> prex + 2 * (fromBytes y) .== postx+                Just (VMSuccess _) -> prex + 2 * y .== postx                 _ -> sFalse-        Left (_, res) <- runSMT $ query $ verifyContract (RuntimeCode c) Nothing (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post+        Left (_, res) <- runSMT $ query $ verifyContract c (Just ("f(uint256)", [AbiUIntType 256])) [] SymbolicS pre post         putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,         -- Inspired by these `msg.sender == to` token bugs@@ -261,9 +284,8 @@           }           |]         let pre vm = 0 .== view (state . callvalue) vm-            post = Just $ \(prestate, poststate) ->-              let SymbolicBuffer bs = fst (view (state.calldata) prestate)-                  (x,y) = over both (fromBytes) (splitAt 32 $ drop 4 bs)+            post (prestate, poststate) =+              let [x,y] = getStaticAbiArgs prestate                   this = view (state . codeContract) prestate                   (Just preC, Just postC) = both' (view (env.contracts . at this)) (prestate, poststate)                   --Just postC = view (env.contracts . at this) poststate@@ -274,13 +296,12 @@                 Just (VMSuccess _) -> prex + prey .== postx + (posty :: SWord 256)                 _ -> sFalse         bs <- runSMT $ query $ do-          Right vm <- verifyContract (RuntimeCode c) Nothing (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre post+          Right 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 bs -> error "unexpected" -        let AbiTuple xyz = decodeAbiValue (AbiTupleType $ Vector.fromList [AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))-            [AbiUInt 256 x, AbiUInt 256 y] = Vector.toList xyz+        let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs         assertEqual "Catch storage collisions" x y         ,         testCase "Deposit contract loop (z3)" $ do@@ -302,7 +323,7 @@               }              }             |]-          Left (_, res) <- runSMTWith z3 $ query $ checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint256)", [AbiUIntType 256])) []+          Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,                 testCase "Deposit contract loop (cvc4)" $ do@@ -324,7 +345,7 @@               }              }             |]-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint256)", [AbiUIntType 256])) []+          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,         testCase "Deposit contract loop (error version)" $ do@@ -347,15 +368,14 @@              }             |]           bs <- runSMT $ query $ do-            Right vm <- checkAssert (RuntimeCode c) Nothing (Just ("deposit(uint8)", [AbiUIntType 8])) []+            Right vm <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) []             case view (state . calldata . _1) vm of               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs               ConcreteBuffer _ -> error "unexpected" -          let deposit = decodeAbiValue (AbiUIntType 8) (BS.fromStrict (BS.drop 4 bs))+          let [deposit] = decodeAbiValues [AbiUIntType 8] bs           assertEqual "overflowing uint8" deposit (AbiUInt 8 255)      ,-        -- This test uses cvc4 instead of z3         testCase "explore function dispatch" $ do         Just c <- solcRuntime "A"           [i|@@ -365,7 +385,9 @@             }           }           |]-        Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []+        Left (_, res) <- runSMTWith z3 $ do+          setTimeOut 5000+          query $ checkAssert c Nothing []         putStrLn $ "successfully explored: " <> show (length res) <> " paths"         , @@ -378,7 +400,7 @@               }             }             |]-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []+          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,         testCase "injectivity of keccak (32 bytes)" $ do@@ -390,7 +412,7 @@               }             }             |]-          Left (_, res) <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []+          Left (_, res) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"        , @@ -404,15 +426,18 @@             }             |]           bs <- runSMTWith z3 $ query $ do-            Right vm <- checkAssert (RuntimeCode c) Nothing (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []+            Right vm <- checkAssert 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"               -          let AbiTuple xywz = decodeAbiValue (AbiTupleType $ Vector.fromList-                                              [AbiUIntType 256, AbiUIntType 256,-                                               AbiUIntType 256, AbiUIntType 256]) (BS.fromStrict (BS.drop 4 bs))-              [AbiUInt 256 x, AbiUInt 256 y, AbiUInt 256 w, AbiUInt 256 z] = Vector.toList xywz+          let [AbiUInt 256 x,+               AbiUInt 256 y,+               AbiUInt 256 w,+               AbiUInt 256 z] = decodeAbiValues [AbiUIntType 256,+                                                 AbiUIntType 256,+                                                 AbiUIntType 256,+                                                 AbiUIntType 256] bs           assertEqual "x == w" x w           assertEqual "y == z" y z        ,@@ -431,7 +456,9 @@               }             }             |]-          Left (_, res) <- runSMTWith z3 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []+          Left (_, res) <- runSMTWith z3 $ do+            setTimeOut 5000+            query $ checkAssert c Nothing []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,@@ -448,7 +475,7 @@               }             |]           -- should find a counterexample-          Right counterexample <- runSMTWith cvc4 $ query $ checkAssert (RuntimeCode c) Nothing Nothing []+          Right counterexample <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           putStrLn $ "found counterexample:"  @@ -507,6 +534,7 @@   where     (===>) = assertSolidityComputation + runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of                       Nothing -> Nothing@@ -574,6 +602,17 @@       ${stmts}     }   |] (abiCalldata s (Vector.fromList args))++getStaticAbiArgs :: VM -> [SWord 256]+getStaticAbiArgs vm =+  let SymbolicBuffer bs = ditch 4 $ view (state . calldata . _1) vm+  in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)]++-- includes shaving off 4 byte function sig+decodeAbiValues :: [AbiType] -> ByteString -> [AbiValue]+decodeAbiValues types bs =+  let AbiTuple xy = decodeAbiValue (AbiTupleType $ Vector.fromList types) (BS.fromStrict (BS.drop 4 bs))+  in Vector.toList xy  newtype Bytes = Bytes ByteString   deriving Eq