hevm 0.42.0 → 0.44.1

raw patch · 26 files changed

+2802/−1754 lines, 26 filesdep +Decimaldep ~sbvPVP ok

version bump matches the API change (PVP)

Dependencies added: Decimal

Dependency ranges changed: sbv

API changes (from Hackage documentation)

Files

• CHANGELOG.md +66/−0
• hevm-cli/hevm-cli.hs +154/−152
• hevm.cabal +3/−3
• src/EVM.hs +372/−343
• src/EVM/ABI.hs +34/−17
• src/EVM/Concrete.hs +6/−92
• src/EVM/Dapp.hs +87/−28
• src/EVM/Debug.hs +1/−29
• src/EVM/Dev.hs +145/−17
• src/EVM/Emacs.hs +7/−5
• src/EVM/Facts.hs +3/−4
• src/EVM/Fetch.hs +44/−24
• src/EVM/Flatten.hs +43/−29
• src/EVM/Format.hs +281/−151
• src/EVM/Keccak.hs +0/−38
• src/EVM/Patricia.hs +1/−2
• src/EVM/Solidity.hs +198/−116
• src/EVM/Stepper.hs +2/−7
• src/EVM/SymExec.hs +165/−77
• src/EVM/Symbolic.hs +148/−117
• src/EVM/TTY.hs +250/−239
• src/EVM/Transaction.hs +62/−4
• src/EVM/Types.hs +312/−46
• src/EVM/UnitTest.hs +292/−114
• src/EVM/VMTest.hs +21/−72
• test/test.hs +105/−28

@@ -1,5 +1,71 @@ # hevm changelog +## 0.44.1 - 2020-02-02++### Changed++- hevm cheatcodes now accept symbolic arguments, allowing e.g. symbolic jumps in time in unit tests++## 0.44.0 - 2020-01-26++### Added++- `hevm` now accepts solidity json output built via `--standard-json` as+  well as `--combined-json`.+- addresses in the trace output are prefixed with `ContractName@0x...`+  if there is a corresponding contract and `@0x...` otherwise.+- More efficient arithmetic overflow checks by translating queries to a more [intelligent form](www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf).++### Fixed++- Symbolic execution now generates calldata arguments restricted to the proper ranges,+following the semantics of fuzzing.+- If the `--address` flag is present in `hevm exec` or `hevm symbolic`,+  it overrides the contract address at which a contract will be created.+- Address pretty printing+- Updated sbv to `8.9.5` to fix "non-const in array declaration" cvc4 issue with ds-test.++### Changed++- Use cvc4 as default smt solver++## 0.43.2 - 2020-12-10++### Changed++- The default smttimeout has been increased from 20s to 30s++## 0.43.1 - 2020-12-10++### Changed++- Counterexamples from symbolic tests now show clearer failure reasons++### Fixed++- Symbolic tests now work with RPC+- Branch selection is working again in the interactive debugger++## 0.43.0 - 2020-11-29++### Added++- A `--show-tree` option to `hevm symbolic` which prints the execution tree explored.+- Some symbolic terms are displayed with richer semantic information, instead of the black box `<symbolic>`.+- `hevm dapp-test` now supports symbolic execution of test methods that are prefixed with `prove` or `proveFail`+- The `hevm interactive` alias has been removed, as it is equivalent to `hevm dapp-test --debug`+- `hevm dapp-test --match` now matches on contract name and file path, as well as test name+- Step through the callstack in debug mode using the arrow keys++### Changed++- `dapp-test` trace output now detects ds-note events and shows `LogNote`+- create addresses are shown with `@<address>` in the trace+- `DSTest.setUp()` is only run if it exists, rather than failing+- support new ds-test `log_named_x(string, x)` (previously bytes32 keys)+- return arguments are fully displayed in the trace (previously only a single word)+- return/revert trace will now show the correct source position+ ## 0.42.0 - 2020-10-31  ### Changed

@@ -6,7 +6,6 @@ {-# Language DeriveGeneric #-} {-# Language GADTs #-} {-# Language LambdaCase #-}-{-# Language NumDecimals #-} {-# Language OverloadedStrings #-} {-# Language TypeOperators #-} {-# Language RecordWildCards #-}@@ -15,15 +14,15 @@  import EVM (StorageModel(..)) import qualified EVM-import EVM.Concrete (createAddress, w256, wordValue)-import EVM.Symbolic (forceLitBytes, litAddr, w256lit, sw256, SymWord(..), len, forceLit, litWord)+import EVM.Concrete (createAddress,  wordValue)+import EVM.Symbolic (litWord, forceLitBytes, litAddr, len, forceLit) 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)+import EVM.Dev (interpretWithTrace)  #if MIN_VERSION_aeson(1, 0, 0) import qualified EVM.VMTest as VMTest@@ -37,8 +36,8 @@ import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract) import EVM.UnitTest (runUnitTestContract) import EVM.UnitTest (getParametersFromEnvironmentVariables, testNumber)-import EVM.Dapp (findUnitTests, dappInfo, DappInfo)-import EVM.Format (showTraceTree)+import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp)+import EVM.Format (showTraceTree, showTree', renderTree, showBranchInfoWithAbi, showLeafInfo) import EVM.RLP (rlpdecode) import qualified EVM.Patricia as Patricia import Data.Map (Map)@@ -47,12 +46,14 @@ import qualified EVM.Facts.Git as Git import qualified EVM.UnitTest +import GHC.IO.Encoding import Control.Concurrent.Async   (async, waitCatch)-import Control.Lens hiding (pre)+import Control.Lens hiding (pre, passing) import Control.Monad              (void, when, forM_, unless)-import Control.Monad.State.Strict (execStateT)+import Control.Monad.State.Strict (execStateT, liftIO) import Data.ByteString            (ByteString) import Data.List                  (intercalate, isSuffixOf)+import Data.Tree import Data.Text                  (Text, unpack, pack) import Data.Text.Encoding         (encodeUtf8) import Data.Text.IO               (hPutStr)@@ -60,9 +61,9 @@ import Data.Version               (showVersion) import Data.SBV hiding (Word, solver, verbose, name) import Data.SBV.Control hiding (Version, timeout, create)-import System.IO                  (hFlush, hPrint, stdout, stderr)+import System.IO                  (hFlush, stdout, stderr, utf8) import System.Directory           (withCurrentDirectory, listDirectory)-import System.Exit                (die, exitFailure, exitWith, ExitCode(..))+import System.Exit                (exitFailure, exitWith, ExitCode(..)) import System.Environment         (setEnv) import System.Process             (callProcess) import qualified Data.Aeson        as JSON@@ -72,15 +73,14 @@ import qualified Data.Vector as V import qualified Data.ByteString.Lazy  as Lazy +import qualified Data.SBV               as SBV import qualified Data.ByteString        as ByteString import qualified Data.ByteString.Char8  as Char8 import qualified Data.ByteString.Lazy   as LazyByteString import qualified Data.Map               as Map-import qualified Data.Sequence          as Seq import qualified System.Timeout         as Timeout  import qualified Paths_hevm      as Paths-import qualified Text.Regex.TDFA as Regex  import Options.Generic as Options @@ -120,18 +120,21 @@       , arg           :: w ::: [String]           <?> "Values to encode"       , debug         :: w ::: Bool               <?> "Run interactively"       , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"-      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 20000)"+      , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"+      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 30000)"       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"+      , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"       }   | Equivalence -- prove equivalence between two programs       { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"       , codeB         :: w ::: ByteString    <?> "Bytecode of the second program"       , sig           :: w ::: Maybe Text    <?> "Signature of types to decode / encode"-      , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 20000)"+      , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 30000)"       , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text    <?> "Used SMT solver: z3 (default) or cvc4"       , smtoutput     :: w ::: Bool          <?> "Print verbose smt output"+      , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"       }   | Exec -- Execute a given program with specified env & calldata       { code        :: w ::: Maybe ByteString <?> "Program bytecode"@@ -152,6 +155,7 @@       , difficulty  :: w ::: Maybe W256       <?> "Block: difficulty"       , chainid     :: w ::: Maybe W256       <?> "Env: chainId"       , debug       :: w ::: Bool             <?> "Run interactively"+      , jsontrace   :: w ::: Bool             <?> "Print json trace output at every step"       , trace       :: w ::: Bool             <?> "Dump trace"       , state       :: w ::: Maybe String     <?> "Path to state repository"       , cache       :: w ::: Maybe String     <?> "Path to rpc cache repository"@@ -161,32 +165,30 @@       , dappRoot    :: w ::: Maybe String     <?> "Path to dapp project root directory (default: . )"       }   | DappTest -- Run DSTest unit tests-      { jsonFile    :: w ::: Maybe String             <?> "Filename or path to dapp build output (default: out/*.solc.json)"-      , dappRoot    :: w ::: Maybe String             <?> "Path to dapp project root directory (default: . )"-      , debug       :: w ::: Bool                     <?> "Run interactively"-      , fuzzRuns    :: w ::: Maybe Int                <?> "Number of times to run fuzz tests"-      , replay      :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"-      , rpc         :: w ::: Maybe URL                <?> "Fetch state from a remote node"-      , 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-      { jsonFile :: w ::: Maybe String <?> "Filename or path to dapp build output (default: out/*.solc.json)"-      , 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"+      { jsonFile      :: w ::: Maybe String             <?> "Filename or path to dapp build output (default: out/*.solc.json)"+      , dappRoot      :: w ::: Maybe String             <?> "Path to dapp project root directory (default: . )"+      , debug         :: w ::: Bool                     <?> "Run interactively"+      , jsontrace     :: w ::: Bool                     <?> "Print json trace output at every step"+      , fuzzRuns      :: w ::: Maybe Int                <?> "Number of times to run fuzz tests"+      , replay        :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"+      , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"+      , 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"+      , smttimeout    :: w ::: Maybe Integer            <?> "Timeout given to SMT solver in milliseconds (default: 30000)"+      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"+      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc4"+      , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"       }   | BcTest -- Run an Ethereum Blockhain/GeneralState test-      { file    :: w ::: String    <?> "Path to .json test file"-      , test    :: w ::: [String]  <?> "Test case filter - only run specified test method(s)"-      , debug   :: w ::: Bool      <?> "Run interactively"-      , diff    :: w ::: Bool      <?> "Print expected vs. actual state on failure"-      , timeout :: w ::: Maybe Int <?> "Execution timeout (default: 10 sec.)"+      { file      :: w ::: String    <?> "Path to .json test file"+      , test      :: w ::: [String]  <?> "Test case filter - only run specified test method(s)"+      , debug     :: w ::: Bool      <?> "Run interactively"+      , jsontrace :: w ::: Bool      <?> "Print json trace output at every step"+      , diff      :: w ::: Bool      <?> "Print expected vs. actual state on failure"+      , timeout   :: w ::: Maybe Int <?> "Execution timeout (default: 10 sec.)"       }   | Compliance -- Run Ethereum Blockhain compliance report       { tests   :: w ::: String       <?> "Path to Ethereum Tests directory"@@ -231,37 +233,38 @@     Options.parseRecordWithModifiers Options.lispCaseModifiers  optsMode :: Command Options.Unwrapped -> Mode-optsMode x = if debug x then Debug else Run+optsMode x = if debug x then Debug else if jsontrace x then JsonTrace else Run  applyCache :: (Maybe String, Maybe String) -> IO (EVM.VM -> EVM.VM) applyCache (state, cache) =   let applyState = flip Facts.apply-      applyCache = flip Facts.applyCache+      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+      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)+      pure $ (applyState stateFacts) . (applyCache' cacheFacts) -unitTestOptions :: Command Options.Unwrapped -> String -> IO UnitTestOptions+unitTestOptions :: Command Options.Unwrapped -> String -> Query UnitTestOptions unitTestOptions cmd testFile = do   let root = fromMaybe "." (dappRoot cmd)-  srcInfo <- readSolc testFile >>= \case+  srcInfo <- liftIO $ readSolc testFile >>= \case     Nothing -> error "Could not read .sol.json file"     Just (contractMap, sourceCache) ->       pure $ dappInfo root contractMap sourceCache -  vmModifier <- applyCache (state cmd, cache cmd)+  vmModifier <- liftIO $ applyCache (state cmd, cache cmd) -  params <- getParametersFromEnvironmentVariables (rpc cmd)+  params <- liftIO $ getParametersFromEnvironmentVariables (rpc cmd)+  state <- queryState    let     testn = testNumber params@@ -272,12 +275,16 @@   pure EVM.UnitTest.UnitTestOptions     { EVM.UnitTest.oracle =         case rpc cmd of-         Just url -> EVM.Fetch.http block' url-         Nothing  -> EVM.Fetch.zero+         Just url -> EVM.Fetch.oracle (Just state) (Just (block', url)) True+         Nothing  -> EVM.Fetch.oracle (Just state) Nothing True+    , EVM.UnitTest.maxIter = maxIterations cmd+    , EVM.UnitTest.smtTimeout = smttimeout cmd+    , EVM.UnitTest.solver = solver cmd+    , EVM.UnitTest.smtState = Just state     , EVM.UnitTest.verbose = verbose cmd-    , EVM.UnitTest.match   = pack $ fromMaybe "^test" (match cmd)+    , EVM.UnitTest.match = pack $ fromMaybe ".*" (match cmd)     , EVM.UnitTest.fuzzRuns = fromMaybe 100 (fuzzRuns cmd)-    , EVM.UnitTest.replay   = do+    , EVM.UnitTest.replay = do         arg' <- replay cmd         return (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg'))     , EVM.UnitTest.vmModifier = vmModifier@@ -303,19 +310,13 @@     DappTest {} ->       withCurrentDirectory root $ do         testFile <- findJsonFile (jsonFile cmd)-        testOpts <- unitTestOptions cmd testFile-        case (coverage cmd, optsMode cmd) of-          (False, Run) ->-            dappTest testOpts (optsMode cmd) testFile (cache cmd)-          (False, Debug) ->-            EVM.TTY.main testOpts root testFile-          (True, _) ->-            dappCoverage testOpts (optsMode cmd) testFile-    Interactive {} ->-      withCurrentDirectory root $ do-        testFile <- findJsonFile (jsonFile cmd)-        testOpts <- unitTestOptions cmd testFile-        EVM.TTY.main testOpts root testFile+        runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do+          testOpts <- unitTestOptions cmd testFile+          case (coverage cmd, optsMode cmd) of+            (False, Run) -> dappTest testOpts testFile (cache cmd)+            (False, Debug) -> liftIO $ EVM.TTY.main testOpts root testFile+            (False, JsonTrace) -> error "json traces not implemented for dappTest"+            (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) testFile     Compliance {} ->       case (group cmd) of         Just "Blockchain" -> launchScript "/run-blockchain-tests" cmd@@ -374,41 +375,27 @@         , intercalate ", " xs         ] -dappTest :: UnitTestOptions -> Mode -> String -> Maybe String -> IO ()-dappTest opts _ solcFile cache =-  readSolc solcFile >>=-    \case-      Just (contractMap, sourceCache) -> do-        let matcher = regexMatches (EVM.UnitTest.match opts)-            unitTests = (findUnitTests matcher) (Map.elems contractMap)--        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 ++ "'")+dappTest :: UnitTestOptions -> String -> Maybe String -> Query ()+dappTest opts solcFile cache = do+  out <- liftIO $ readSolc solcFile+  case out of+    Just (contractMap, _) -> do+      let unitTests = findUnitTests (EVM.UnitTest.match opts) $ Map.elems contractMap+      results <- concatMapM (runUnitTestContract opts contractMap) 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+            liftIO $ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts cache') -regexMatches :: Text -> Text -> Bool-regexMatches regexSource =-  let-    compOpts =-      Regex.defaultCompOpt { Regex.lastStarGreedy = True }-    execOpts =-      Regex.defaultExecOpt { Regex.captureGroups = False }-    regex = Regex.makeRegexOpts compOpts execOpts (unpack regexSource)-  in-    Regex.matchTest regex . Seq.fromList . unpack+      liftIO $ unless (and passing) exitFailure+    Nothing ->+      error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'")  equivalence :: Command Options.Unwrapped -> IO () equivalence cmd =@@ -419,34 +406,36 @@        Just sig' -> do method' <- functionAbi sig'                        return $ Just (view methodSignature method', snd <$> view methodInputs method') -     void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) . query $+     void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) . query $        equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case          Right vm -> do io $ putStrLn "Not equal!"                         io $ putStrLn "Counterexample:"                         showCounterexample vm maybeSignature-                        io $ exitFailure+                        io exitFailure          Left (postAs, postBs) -> io $ do            putStrLn $ "Explored: " <> show (length postAs)                        <> " execution paths of A and: "                        <> show (length postBs) <> " paths of B."-           putStrLn $ "No discrepancies found."+           putStrLn "No discrepancies found."   -- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`-runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Symbolic a -> IO a-runSMTWithTimeOut solver maybeTimeout sym-  | solver == Just "cvc4" = do-      setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)-      a <- runSMTWith cvc4 sym-      setEnv "SBV_CVC4_OPTIONS" ""-      return a+runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Bool -> Symbolic a -> IO a+runSMTWithTimeOut solver maybeTimeout smtdebug symb+  | solver == Just "cvc4" = runwithcvc4   | solver == Just "z3" = runwithz3-  | solver == Nothing = runwithz3+  | solver == Nothing = runwithcvc4   | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"- where timeout = fromMaybe 20000 maybeTimeout-       runwithz3 = runSMTWith z3 $ (setTimeOut timeout) >> sym+ where timeout = fromMaybe 30000 maybeTimeout+       runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb+       runwithcvc4 = do+         setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)+         a <- runSMTWith cvc4{SBV.verbose=smtdebug} symb+         setEnv "SBV_CVC4_OPTIONS" ""+         return a  + checkForVMErrors :: [EVM.VM] -> [String] checkForVMErrors [] = [] checkForVMErrors (vm:vms) =@@ -459,18 +448,15 @@     _ ->       checkForVMErrors vms -emptyDapp :: DappInfo-emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty mempty)- getSrcInfo :: Command Options.Unwrapped -> IO DappInfo getSrcInfo cmd =   let root = fromMaybe "." (dappRoot cmd)   in case (jsonFile cmd) of     Nothing ->-      pure $ emptyDapp+      pure emptyDapp     Just json -> readSolc json >>= \case       Nothing ->-        pure $ emptyDapp+        pure emptyDapp       Just (contractMap, sourceCache) ->         pure $ dappInfo root contractMap sourceCache @@ -482,10 +468,19 @@ -- If function signatures are known, they should always be given for best results. assert :: Command Options.Unwrapped -> IO () assert cmd = do+  srcInfo <- getSrcInfo cmd   let block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)       rpcinfo = (,) block' <$> rpc cmd-      model = fromMaybe (if create cmd then InitialS else SymbolicS) (storageModel cmd)-  srcInfo <- getSrcInfo cmd+      treeShowing :: Tree BranchInfo -> Query ()+      treeShowing tree =+        when (showTree cmd) $ do+          consistentTree tree >>= \case+            Nothing -> io $ putStrLn "No consistent paths" -- unlikely+            Just tree' -> let+              showBranch = showBranchInfoWithAbi srcInfo+              renderTree' = renderTree showBranch (showLeafInfo srcInfo)+              in io $ setLocaleEncoding utf8 >> putStrLn (showTree' (renderTree' tree'))+   maybesig <- case sig cmd of     Nothing ->       return Nothing@@ -495,27 +490,29 @@           name = view methodSignature method'       return $ Just (name,typ)   if debug cmd then-    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do       preState <- symvmFromCommand cmd       smtState <- queryState       io $ void $ EVM.TTY.runFromVM         (maxIterations cmd)         srcInfo-        (EVM.Fetch.oracle (Just smtState) rpcinfo model True)+        (EVM.Fetch.oracle (Just smtState) rpcinfo True)         preState    else-    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do       preState <- symvmFromCommand cmd       verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case-        Right _ -> do+        Right tree -> do           io $ putStrLn "Assertion violation found."           showCounterexample preState maybesig+          treeShowing tree           io $ exitWith (ExitFailure 1)-        Left (pre, posts) -> do-          io $ putStrLn $ "Explored: " <> show (length posts)+        Left tree -> do+          io $ putStrLn $ "Explored: " <> show (length tree)                        <> " branches without assertion violations"-          let vmErrs = checkForVMErrors posts+          treeShowing tree+          let vmErrs = checkForVMErrors $ leaves tree           unless (null vmErrs) $ io $ do             putStrLn $               "However, "@@ -524,18 +521,21 @@             print vmErrs           -- When `--get-models` is passed, we print example vm info for each path           when (getModels cmd) $-            forM_ (zip [1..] posts) $ \(i, postVM) -> do+            forM_ (zip [(1:: Integer)..] (leaves tree)) $ \(i, postVM) -> do               resetAssertions-              constrain (sAnd (view EVM.pathConditions postVM))+              constrain (sAnd (fst <$> view EVM.constraints postVM))               io $ putStrLn $-                "-- Branch (" <> show i <> "/" <> show (length posts) <> ") --"+                "-- Branch (" <> show i <> "/" <> show (length tree) <> ") --"               checkSat >>= \case+                DSat _ -> error "assert: unexpected SMT result"                 Unk -> io $ do putStrLn "Timed out"                                print $ view EVM.result postVM                 Unsat -> io $ do putStrLn "Inconsistent path conditions: dead path"                                  print $ view EVM.result postVM                 Sat -> do-                  showCounterexample pre maybesig+                  showCounterexample preState maybesig+                  io $ putStrLn "-- Pathconditions --"+                  io $ print $ snd <$> view EVM.constraints postVM                   case view EVM.result postVM of                     Nothing ->                       error "internal error; no EVM result"@@ -561,10 +561,9 @@   readSolc solcFile >>=     \case       Just (contractMap, sourceCache) -> do-        let matcher = regexMatches (EVM.UnitTest.match opts)-        let unitTests = (findUnitTests matcher) (Map.elems contractMap)-        covs <- mconcat <$> mapM (coverageForUnitTestContract opts contractMap sourceCache) unitTests-+        let unitTests = findUnitTests (EVM.UnitTest.match opts) $ Map.elems contractMap+        covs <- mconcat <$> mapM+          (coverageForUnitTestContract opts contractMap sourceCache) unitTests         let           dapp = dappInfo "." contractMap sourceCache           f (k, vs) = do@@ -618,6 +617,7 @@               Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts (view EVM.cache vm'))      Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm+    JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm    where fetcher = maybe EVM.Fetch.zero (EVM.Fetch.http block') (rpc cmd)          block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd) @@ -688,9 +688,9 @@   (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"+      Nothing -> error "Could not fetch block"       Just EVM.Block{..} -> return (_coinbase-                                   , wordValue $ forceLit $ _timestamp+                                   , wordValue $ forceLit _timestamp                                    , wordValue _number                                    , wordValue _difficulty                                    )@@ -721,7 +721,7 @@         EVM.initialContract (codeType $ hexByteString "--code" $ strip0x c)      (_, _, Nothing) ->-      error $ "must provide at least (rpc + address) or code"+      error "must provide at least (rpc + address) or code"    return $ VMTest.initTx $ withCache (vm0 miner ts blockNum diff contract)     where@@ -733,12 +733,12 @@         calldata' = ConcreteBuffer $ bytes calldata ""         codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode         address' = if create cmd-              then createAddress origin' (word nonce 0)+              then addr address (createAddress origin' (word nonce 0))               else addr address 0xacab          vm0 miner ts blockNum diff c = EVM.makeVm $ EVM.VMOpts           { EVM.vmoptContract      = c-          , EVM.vmoptCalldata      = (calldata', literal . num $ len calldata')+          , EVM.vmoptCalldata      = (calldata', litWord (num $ len calldata'))           , EVM.vmoptValue         = w256lit value'           , EVM.vmoptAddress       = address'           , EVM.vmoptCaller        = litAddr caller'@@ -774,24 +774,24 @@                                    )    caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)-  ts <- maybe (sw256 <$> freshVar_) (return . w256lit) (timestamp cmd)-  callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)+  ts <- maybe (var "Timestamp" <$> freshVar_) (return . w256lit) (timestamp cmd)+  callvalue' <- maybe (var "CallValue" <$> freshVar_) (return . w256lit) (value cmd)   (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of-    -- fully abstract calldata (up to 1024 bytes)+    -- fully abstract calldata (up to 256 bytes)     (Nothing, Nothing) -> do       cd <- sbytes256-      len <- freshVar_-      return (SymbolicBuffer cd, len, len .<= 256)+      len' <- freshVar_+      return (SymbolicBuffer cd, var "CALLDATALENGTH" len', (len' .<= 256, Todo "len < 256" []))     -- fully concrete calldata     (Just c, Nothing) ->       let cd = ConcreteBuffer $ decipher c-      in return (cd, num (len cd), sTrue)+      in return (cd, litWord (num $ len cd), (sTrue, Todo "" []))     -- calldata according to given abi with possible specializations from the `arg` list     (Nothing, Just sig') -> do       method' <- io $ functionAbi sig'       let typs = snd <$> view methodInputs method'       (cd, cdlen) <- symCalldata (view methodSignature method') typs (arg cmd)-      return (SymbolicBuffer cd, cdlen, sTrue)+      return (SymbolicBuffer cd, litWord (num cdlen), (sTrue, Todo "" []))      _ -> error "incompatible options: calldata and abi" @@ -800,10 +800,10 @@     -- ConcreteS cannot (instead values can be fetched from rpc!)     -- Initial defaults to 0 for uninitialized storage slots,     -- whereas the values of SymbolicS are unconstrained.-    Just InitialS  -> EVM.Symbolic <$> freshArray_ (Just 0)+    Just InitialS  -> EVM.Symbolic [] <$> freshArray_ (Just 0)     Just ConcreteS -> return (EVM.Concrete mempty)-    Just SymbolicS -> EVM.Symbolic <$> freshArray_ Nothing-    Nothing -> EVM.Symbolic <$> freshArray_ (if create cmd then (Just 0) else Nothing)+    Just SymbolicS -> EVM.Symbolic [] <$> freshArray_ Nothing+    Nothing -> EVM.Symbolic [] <$> freshArray_ (if create cmd then (Just 0) else Nothing)    withCache <- io $ applyCache (state cmd, cache cmd) @@ -811,7 +811,7 @@     (Just url, Just addr', _) ->       io (EVM.Fetch.fetchContractFrom block' url addr') >>= \case         Nothing ->-          error $ "contract not found."+          error "contract not found."         Just contract' -> return contract''           where             contract'' = case code cmd of@@ -827,10 +827,10 @@     (_, _, Just c)  ->       return $ (EVM.initialContract . codeType $ decipher c)     (_, _, Nothing) ->-      error $ "must provide at least (rpc + address) or code"+      error "must provide at least (rpc + address) or code"    return $ (VMTest.initTx $ withCache $ vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' contract')-    & over EVM.pathConditions (<> [pathCond])+    & over EVM.constraints (<> [pathCond])     & set (EVM.env . EVM.contracts . (ix address') . EVM.storage) store    where@@ -839,7 +839,7 @@     origin'  = addr origin 0     codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode     address' = if create cmd-          then createAddress origin' (word nonce 0)+          then addr address (createAddress origin' (word nonce 0))           else addr address 0xacab     vm0 miner ts blockNum diff cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts       { EVM.vmoptContract      = c@@ -895,10 +895,12 @@     action <- async $       case mode of         Run ->-          Timeout.timeout (1e6 * (fromMaybe 10 timelimit)) $+          Timeout.timeout (1000000 * (fromMaybe 10 timelimit)) $             execStateT (EVM.Stepper.interpret EVM.Fetch.zero . void $ EVM.Stepper.execFully) vm0         Debug ->           Just <$> EVM.TTY.runFromVM Nothing emptyDapp EVM.Fetch.zero vm0+        JsonTrace ->+          Just <$> execStateT (interpretWithTrace EVM.Fetch.zero EVM.Stepper.runFully) vm0     waitCatch action   case result of     Right (Just vm1) -> do

@@ -2,7 +2,7 @@ name:   hevm version:-  0.42.0+  0.44.1 synopsis:   Ethereum virtual machine evaluator description:@@ -48,7 +48,6 @@     EVM.Fetch,     EVM.FeeSchedule,     EVM.Hexdump,-    EVM.Keccak,     EVM.Op,     EVM.Patricia,     EVM.Precompiled,@@ -82,6 +81,7 @@     ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h   build-depends:     QuickCheck                        >= 2.13.2 && < 2.15,+    Decimal                           == 0.5.1,     containers                        >= 0.6.0 && < 0.7,     deepseq                           >= 1.4.4 && < 1.5,     time                              >= 1.8.0 && < 1.11,@@ -121,7 +121,7 @@     restless-git                      >= 0.7 && < 0.8,     rosezipper                        >= 0.2 && < 0.3,     s-cargot                          >= 0.1.4 && < 0.2,-    sbv                               >= 8.7.5 && < 8.9,+    sbv                               >= 8.7.5,     semver-range                      >= 0.2.7 && < 0.3,     temporary                         >= 1.3 && < 1.4,     text-format                       >= 0.3.2 && < 0.4,

@@ -13,22 +13,20 @@  module EVM where -import Prelude hiding (log, Word, exponent)+import Prelude hiding (log, Word, exponent, GT, LT)  import Data.SBV hiding (Word, output, Unknown) import Data.Proxy (Proxy(..)) import EVM.ABI import EVM.Types import EVM.Solidity-import EVM.Keccak-import EVM.Concrete (Word(..), w256, createAddress, wordValue, keccakBlob, create2Address)+import EVM.Concrete (createAddress, wordValue, keccakBlob, create2Address) import EVM.Symbolic import EVM.Op import EVM.FeeSchedule (FeeSchedule (..)) import Options.Generic as Options import qualified EVM.Precompiled -import Data.Binary.Get (runGetOrFail) import Data.Text (Text) import Data.Word (Word8, Word32) import Control.Lens hiding (op, (:<), (|>), (.>))@@ -58,8 +56,8 @@ import qualified Data.Vector as RegularVector  import Crypto.Number.ModArithmetic (expFast)-import Crypto.Hash (Digest, SHA256, RIPEMD160) import qualified Crypto.Hash as Crypto+import Crypto.Hash (Digest, SHA256, RIPEMD160)  -- * Data types @@ -85,6 +83,8 @@   | PrecompileFailure   | UnexpectedSymbolicArg   | DeadPath+  | NotUnique Whiff+  | SMTTimeout deriving instance Show Error  -- | The possible result states of a VM@@ -106,15 +106,17 @@   , _traces         :: Zipper.TreePos Zipper.Empty Trace   , _cache          :: Cache   , _burned         :: Word-  , _pathConditions :: [SBool]+  , _constraints    :: [(SBool, Whiff)]   , _iterations     :: Map CodeLocation Int   }+  deriving (Show)  data Trace = Trace   { _traceCodehash :: W256-  , _traceOpIx     :: Int+  , _traceOpIx     :: Maybe Int   , _traceData     :: TraceData   }+  deriving (Show)  data TraceData   = EventTrace Log@@ -123,32 +125,38 @@   | ErrorTrace Error   | EntryTrace Text   | ReturnTrace Buffer FrameContext+  deriving (Show)  -- | Queries halt execution until resolved through RPC calls or SMT queries data Query where-  PleaseFetchContract :: Addr         -> (Contract   -> EVM ()) -> Query-  PleaseFetchSlot     :: Addr -> Word -> (Word       -> EVM ()) -> Query+  PleaseFetchContract :: Addr -> StorageModel -> (Contract -> EVM ()) -> Query+  PleaseMakeUnique    :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query+  PleaseFetchSlot     :: Addr -> Word -> (Word -> EVM ()) -> Query   PleaseAskSMT        :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query  data Choose where-  PleaseChoosePath    :: (Bool -> EVM ()) -> Choose+  PleaseChoosePath    :: Whiff -> (Bool -> EVM ()) -> Choose  instance Show Query where   showsPrec _ = \case-    PleaseFetchContract addr _ ->+    PleaseFetchContract addr _ _ ->       (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)     PleaseFetchSlot addr slot _ ->       (("<EVM.Query: fetch slot "         ++ show slot ++ " for "         ++ show addr ++ ">") ++)-    PleaseAskSMT condition pathConditions _ ->+    PleaseAskSMT condition constraints _ ->       (("<EVM.Query: ask SMT about "         ++ show condition ++ " in context "-        ++ show pathConditions ++ ">") ++)+        ++ show constraints ++ ">") ++)+    PleaseMakeUnique val constraints _ ->+      (("<EVM.Query: make value "+        ++ show val ++ " unique in context "+        ++ show constraints ++ ">") ++)  instance Show Choose where   showsPrec _ = \case-    PleaseChoosePath _ ->+    PleaseChoosePath _ _ ->       (("<EVM.Choice: waiting for user to select path (0,1)") ++)  -- | Alias for the type of e.g. @exec1@.@@ -160,6 +168,10 @@ data BranchCondition = Case Bool | Unknown | Inconsistent   deriving Show +-- | The possible return values of a `is unique` SMT query+data IsUnique a = Unique a | Multiple | InconsistentU | TimeoutU+  deriving Show+ -- | The cache is data that can be persisted for efficiency: -- any expensive query that is constant at least within a block. data Cache = Cache@@ -170,7 +182,7 @@ -- | A way to specify an initial VM state data VMOpts = VMOpts   { vmoptContract :: Contract-  , vmoptCalldata :: (Buffer, (SWord 32)) -- maximum size of uint32 as per eip 1985+  , vmoptCalldata :: (Buffer, SymWord)   , vmoptValue :: SymWord   , vmoptAddress :: Addr   , vmoptCaller :: SAddr@@ -184,7 +196,7 @@   , vmoptMaxCodeSize :: W256   , vmoptBlockGaslimit :: W256   , vmoptGasprice :: W256-  , vmoptSchedule :: FeeSchedule Word+  , vmoptSchedule :: FeeSchedule Integer   , vmoptChainId :: W256   , vmoptCreate :: Bool   , vmoptStorageModel :: StorageModel@@ -192,17 +204,20 @@  -- | A log entry data Log = Log Addr Buffer [SymWord]+  deriving (Show)  -- | An entry in the VM's "call/create stack" data Frame = Frame   { _frameContext   :: FrameContext   , _frameState     :: FrameState   }+  deriving (Show)  -- | Call/create info data FrameContext   = CreationContext-    { creationContextCodehash  :: W256+    { creationContextAddress   :: Addr+    , creationContextCodehash  :: W256     , creationContextReversion :: Map Addr Contract     , creationContextSubstate  :: SubState     }@@ -217,6 +232,7 @@     , callContextReversion :: Map Addr Contract     , callContextSubState  :: SubState     }+  deriving (Show)  -- | The "registers" of the VM along with memory and data stack data FrameState = FrameState@@ -227,13 +243,14 @@   , _stack        :: [SymWord]   , _memory       :: Buffer   , _memorySize   :: Int-  , _calldata     :: (Buffer, (SWord 32))+  , _calldata     :: (Buffer, SymWord)   , _callvalue    :: SymWord   , _caller       :: SAddr   , _gas          :: Word   , _returndata   :: Buffer   , _static       :: Bool   }+  deriving (Show)  -- | The state that spans a whole transaction data TxState = TxState@@ -246,14 +263,16 @@   , _isCreate        :: Bool   , _txReversion     :: Map Addr Contract   }+  deriving (Show)  -- | The "accrued substate" across a transaction data SubState = SubState   { _selfdestructs   :: [Addr]   , _touchedAccounts :: [Addr]-  , _refunds         :: [(Addr, Word)]+  , _refunds         :: [(Addr, Integer)]   -- in principle we should include logs here, but do not for now   }+  deriving (Show)  -- | A contract is either in creation (running its "constructor") or -- post-creation, and code in these two modes is treated differently@@ -268,7 +287,7 @@ -- depending on what type of execution we are doing data Storage   = Concrete (Map Word SymWord)-  | Symbolic (SArray (WordN 256) (WordN 256))+  | Symbolic [(SymWord, SymWord)] (SArray (WordN 256) (WordN 256))   deriving (Show)  -- to allow for Eq Contract (which useful for debugging vmtests)@@ -276,8 +295,8 @@ -- It should not (cannot) be used though. instance Eq Storage where   (==) (Concrete a) (Concrete b) = fmap forceLit a == fmap forceLit b-  (==) (Symbolic _) (Concrete _) = False-  (==) (Concrete _) (Symbolic _) = False+  (==) (Symbolic _ _) (Concrete _) = False+  (==) (Concrete _) (Symbolic _ _) = False   (==) _ _ = error "do not compare two symbolic arrays like this!"  -- | The state of a contract@@ -322,6 +341,7 @@   , _sha3Crack    :: Map Word ByteString   , _keccakUsed   :: [([SWord 8], SWord 256)]   }+  deriving (Show)   -- | Data about the block@@ -332,7 +352,7 @@   , _difficulty  :: Word   , _gaslimit    :: Word   , _maxCodeSize :: Word-  , _schedule    :: FeeSchedule Word+  , _schedule    :: FeeSchedule Integer   } deriving Show  blankState :: FrameState@@ -450,7 +470,7 @@     }   , _cache = Cache mempty mempty   , _burned = 0-  , _pathConditions = []+  , _constraints = []   , _iterations = mempty   } where theCode = case _contractcode (vmoptContract o) of             InitCode b    -> b@@ -511,11 +531,11 @@     let ?op = 0x00 -- dummy value     let       calldatasize = snd (the state calldata)-    case unliteral calldatasize of+    case maybeLitWord calldatasize of         Nothing -> vmError UnexpectedSymbolicArg         Just calldatasize' -> do           copyBytesToMemory (fst $ the state calldata) (num calldatasize') 0 0-          executePrecompile self (the state gas) 0 (num calldatasize') 0 0 []+          executePrecompile self (num $ the state gas) 0 (num calldatasize') 0 0 []           vmx <- get           case view (state.stack) vmx of             (x:_) -> case maybeLitWord x of@@ -543,8 +563,8 @@         -- op: PUSH         x | x >= 0x60 && x <= 0x7f -> do           let !n = num x - 0x60 + 1-              !xs = BS.take n (BS.drop (1 + the state pc)-                                       (the state code))+              !xs = padRight n $ BS.take n (BS.drop (1 + the state pc)+                                        (the state code))           limitStack 1 $             burn g_verylow $ do               next@@ -587,7 +607,7 @@                         bytes         = readMemory (num xOffset) (num xSize) vm                         log           = Log self bytes topics -                    burn (g_log + g_logdata * xSize + num n * g_logtopic) $+                    burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $                       accessMemoryRange fees xOffset xSize $ do                         traceLog log                         next@@ -614,7 +634,7 @@           stackOp2 (const g_low) (uncurry sdiv)          -- op: MOD-        0x06 -> stackOp2 (const g_low) $ \(x, y) -> ite (y .== 0) 0 (x `sMod` y)+        0x06 -> stackOp2 (const g_low) $ \(S a x, S b y) -> S (ITE (IsZero b) (Literal 0) (Mod a b)) (ite (y .== 0) 0 (x `sMod` y))          -- op: SMOD         0x07 -> stackOp2 (const g_low) $ uncurry smod@@ -624,18 +644,18 @@         0x09 -> stackOp3 (const g_mid) (\(x, y, z) -> mulmod x y z)          -- op: LT-        0x10 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .< y) 1 0+        0x10 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (LT a b) (x .< y) 1 0         -- op: GT-        0x11 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .> y) 1 0+        0x11 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (GT a b) (x .> y) 1 0         -- op: SLT         0x12 -> stackOp2 (const g_verylow) $ uncurry slt         -- op: SGT         0x13 -> stackOp2 (const g_verylow) $ uncurry sgt          -- op: EQ-        0x14 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .== y) 1 0+        0x14 -> stackOp2 (const g_verylow) $ \(S a x, S b y) -> iteWhiff (Eq a b) (x .== y) 1 0         -- op: ISZERO-        0x15 -> stackOp1 (const g_verylow) $ \x -> ite (x .== 0) 1 0+        0x15 -> stackOp1 (const g_verylow) $ \(S a x) -> iteWhiff (IsZero a) (x .== 0) 1 0          -- op: AND         0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.)@@ -652,11 +672,11 @@           (n, x) | otherwise          -> 0xff .&. shiftR x (8 * (31 - num (forceLit n)))          -- op: SHL-        0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n+        0x1b -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHL b a) $ sShiftLeft x n         -- op: SHR-        0x1c -> stackOp2 (const g_verylow) $ uncurry shiftRight'+        0x1c -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SHR b a) $ sShiftRight x n         -- op: SAR-        0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n+        0x1d -> stackOp2 (const g_verylow) $ \((S a n), (S b x)) -> S (SAR b a) $ sSignedShiftArithRight x n          -- op: SHA3         -- more accurately refered to as KECCAK@@ -664,29 +684,38 @@           case stk of             (xOffset' : xSize' : xs) ->               forceConcrete xOffset' $-                \xOffset -> forceConcrete xSize' $ \xSize -> do-                  (hash, invMap) <- case readMemory xOffset xSize vm of-                                     ConcreteBuffer bs -> pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs)+                \xOffset -> forceConcrete xSize' $ \xSize ->+                  burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $+                    accessMemoryRange fees xOffset xSize $ do+                      (hash@(S _ hash'), invMap, bytes) <- case readMemory xOffset xSize vm of+                                         ConcreteBuffer bs -> do+                                           pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs, litBytes bs)+                                         SymbolicBuffer bs -> do+                                           let hash' = symkeccak' bs+                                           return (S (FromKeccak $ SymbolicBuffer bs) hash', mempty, bs) -                                     -- Although we would like to simply assert that the uninterpreted function symkeccak'-                                     -- is injective, this proves to cause a lot of concern for our smt solvers, probably-                                     -- due to the introduction of universal quantifiers into the queries.+                      -- Although we would like to simply assert that the uninterpreted function symkeccak'+                      -- is injective, this proves to cause a lot of concern for our smt solvers, probably+                      -- due to the introduction of universal quantifiers into the queries. -                                     -- Instead, we keep track of all of the particular invocations of symkeccak' we see-                                     -- (similarly to sha3Crack), and simply assert that injectivity holds for these-                                     -- particular invocations.+                      -- Instead, we keep track of all of the particular invocations of symkeccak' we see+                      -- (similarly to sha3Crack), and simply assert that injectivity holds for these+                      -- particular invocations.+                      --+                      -- We additionally make the probabalisitc assumption that the output of symkeccak'+                      -- is greater than 100. This lets us avoid having to reason about storage collisions+                      -- between mappings and "normal" slots -                                     SymbolicBuffer bs -> do-                                                   let hash' = symkeccak' bs-                                                       previousUsed = view (env . keccakUsed) vm-                                                   env . keccakUsed <>= [(bs, hash')]-                                                   pathConditions <>= fmap (\(preimage, image) ->-                                                                               image .== hash' .=> preimage .== bs)-                                                                           previousUsed-                                                   return (sw256 hash', mempty)+                      let previousUsed = view (env . keccakUsed) vm+                      env . keccakUsed <>= [(bytes, hash')]+                      constraints <>= (hash' .> 100, Todo "probabilistic keccak assumption" []):+                        (fmap (\(preimage, image) ->+                          -- keccak is a function+                          ((preimage .== bytes .=> image .== hash') .&&+                          -- which is injective+                          (image .== hash' .=> preimage .== bytes), Todo "injective keccak assumption" []))+                         previousUsed) -                  burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $-                    accessMemoryRange fees xOffset xSize $ do                       next                       assign (state . stack) (hash : xs)                       (env . sha3Crack) <>= invMap@@ -717,7 +746,10 @@         -- op: CALLER         0x33 ->           limitStack 1 . burn g_base $-            let toSymWord = sw256 . sFromIntegral . saddressWord160+            let toSymWord :: SAddr -> SymWord+                toSymWord (SAddr x) = case unliteral x of+                  Just s -> litWord $ num s+                  Nothing -> var "CALLER" $ sFromIntegral x             in next >> pushSym (toSymWord (the state caller))          -- op: CALLVALUE@@ -727,23 +759,23 @@          -- op: CALLDATALOAD         0x35 -> stackOp1 (const g_verylow) $-          \(S _ x) -> uncurry (readSWordWithBound (sFromIntegral x)) (the state calldata)+          \ind -> uncurry (readSWordWithBound ind) (the state calldata)          -- op: CALLDATASIZE         0x36 ->           limitStack 1 . burn g_base $-            next >> pushSym (sw256 . zeroExtend . snd $ (the state calldata))+            next >> pushSym (snd (the state calldata))          -- op: CALLDATACOPY         0x37 ->           case stk of             (xTo' : xFrom' : xSize' : xs) -> forceConcrete3 (xTo',xFrom',xSize') $ \(xTo,xFrom,xSize) ->-              burn (g_verylow + g_copy * ceilDiv xSize 32) $+              burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $                 accessUnboundedMemoryRange fees xTo xSize $ do                   next                   assign (state . stack) xs                   case the state calldata of-                    (SymbolicBuffer cd, cdlen) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo+                    (SymbolicBuffer cd, (S _ cdlen)) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo                     -- when calldata is concrete,                     -- the bound should always be equal to the bytestring length                     (cd, _) -> copyBytesToMemory cd xSize xFrom xTo@@ -774,7 +806,7 @@         -- op: EXTCODESIZE         0x3b ->           case stk of-            (x':xs) -> forceConcrete x' $ \x ->+            (x':xs) -> makeUnique x' $ \x ->               if x == num cheatCode                 then do                   next@@ -818,7 +850,7 @@           case stk of             (xTo' : xFrom' : xSize' :xs) -> forceConcrete3 (xTo', xFrom', xSize') $               \(xTo, xFrom, xSize) ->-                burn (g_verylow + g_copy * ceilDiv xSize 32) $+                burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $                   accessUnboundedMemoryRange fees xTo xSize $ do                     next                     assign (state . stack) xs@@ -945,12 +977,12 @@               accessStorage self x $ \current -> do                 availableGas <- use (state . gas) -                if availableGas <= g_callstipend-                  then finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))+                if num availableGas <= g_callstipend+                  then finishFrame (FrameErrored (OutOfGas availableGas (num g_callstipend)))                   else do                     let original = case view storage this of                                   Concrete _ -> fromMaybe 0 (Map.lookup (forceLit x) (view origStorage this))-                                  Symbolic _ -> 0 -- we don't use this value anywhere anyway+                                  Symbolic _ _ -> 0 -- we don't use this value anywhere anyway                         cost = case (maybeLitWord current, maybeLitWord new) of                                  (Just current', Just new') ->                                     if (current' == new') then g_sload@@ -999,7 +1031,7 @@         -- op: JUMPI         0x57 -> do           case stk of-            (x:y:xs) -> forceConcrete x $ \x' ->+            (x:y@(S w _):xs) -> forceConcrete x $ \x' ->                 burn g_high $                   let jump :: Bool -> EVM ()                       jump True = assign (state . stack) xs >> next@@ -1007,7 +1039,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) (0 .== y) jump+                      Nothing -> askSMT (self, the state pc) (0 .== y, IsZero w) jump             _ -> underrun          -- op: PC@@ -1023,7 +1055,7 @@         -- op: GAS         0x5a ->           limitStack 1 . burn g_base $-            next >> push (the state gas - g_base)+            next >> push (the state gas - num g_base)          -- op: JUMPDEST         0x5b -> burn g_jumpdest next@@ -1034,16 +1066,16 @@                 if exponent == 0                 then g_exp                 else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)-          in stackOp2 cost $ \((S _ x),(S _ y)) -> sw256 $ x .^ y+          in stackOp2 cost $ \((S a x),(S b y)) -> S (Exp a b) (x .^ y)          -- op: SIGNEXTEND         0x0b ->-          stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S _ x)) ->+          stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S a x)) ->             if bytes >= 32 then w             else let n = num bytes * 8 + 7 in-              sw256 $ ite (sTestBit x n)-                      (x .|. complement (bit n - 1))-                      (x .&. (bit n - 1))+              S (Todo "signextend" [a]) $ ite (sTestBit x n)+                                          (x .|. complement (bit n - 1))+                                          (x .&. (bit n - 1))          -- op: CREATE         0xf0 ->@@ -1057,38 +1089,32 @@                     newAddr = createAddress self (wordValue (view nonce this))                     (cost, gas') = costOfCreate fees availableGas 0                   burn (cost - gas') $ forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode ->-                    create self this gas' xValue xs newAddr initCode+                    create self this (num gas') xValue xs newAddr initCode             _ -> underrun          -- op: CALL         0xf1 ->           case stk of             ( xGas'-              : xTo'+              : S _ xTo               : (forceLit -> xValue)               : xInOffset'               : xInSize'               : xOutOffset'               : xOutSize'               : xs-             ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->-              (if xValue > 0 then notStatic else id) $-                case xTo of-                  n | n > 0 && n <= 9 ->-                    precompiledContract this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs-                  n | num n == cheatCode ->-                    do-                      assign (state . stack) xs-                      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-                  _ -> delegateCall this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ do-                            zoom state $ do-                              assign callvalue (litWord xValue)-                              assign caller (litAddr self)-                              assign contract xTo-                            transfer self xTo xValue-                            touchAccount self-                            touchAccount xTo+             ) -> forceConcrete5 (xGas',xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->+                (if xValue > 0 then notStatic else id) $+                  let target = SAddr $ sFromIntegral xTo in+                  delegateCall this xGas target target xValue xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do+                    zoom state $ do+                      assign callvalue (litWord xValue)+                      assign caller (litAddr self)+                      assign contract callee+                    transfer self callee xValue+                    touchAccount self+                    touchAccount callee             _ ->               underrun @@ -1096,23 +1122,21 @@         0xf2 ->           case stk of             ( xGas'-              : xTo'+              : S _ xTo'               : (forceLit -> xValue)               : xInOffset'               : xInSize'               : xOutOffset'               : xOutSize'               : xs-              ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->-                case xTo of-                  n | n > 0 && n <= 9 ->-                    precompiledContract this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs-                  _ -> delegateCall this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ do-                         zoom state $ do-                           assign callvalue (litWord xValue)-                           assign caller (litAddr self)-                         touchAccount self+              ) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $+                \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->+                  let target = SAddr $ sFromIntegral xTo' in+                  delegateCall this xGas target (litAddr self) xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                    zoom state $ do+                      assign callvalue (litWord xValue)+                      assign caller (litAddr self)+                    touchAccount self             _ ->               underrun @@ -1133,7 +1157,7 @@                         then                           finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))                         else-                          burn (g_codedeposit * codesize) $+                          burn (g_codedeposit * num codesize) $                             finishFrame (FrameReturned output)                       False ->                         finishFrame (FrameReturned output)@@ -1146,7 +1170,7 @@                         then                           finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))                         else-                          burn (g_codedeposit * codesize) $+                          burn (g_codedeposit * num codesize) $                             finishFrame (FrameReturned output)                       CallContext {} ->                           finishFrame (FrameReturned output)@@ -1156,22 +1180,16 @@         0xf4 ->           case stk of             (xGas'-             :xTo'+             :S _ xTo              :xInOffset'              :xInSize'              :xOutOffset'              :xOutSize'-             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->-                case xTo of-                  n | n > 0 && n <= 9 ->-                    precompiledContract this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs-                  n | num n == cheatCode -> do-                        assign (state . stack) xs-                        cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-                  _ -> do-                        delegateCall this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs $ do-                          touchAccount self+             :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->+                let target = SAddr $ sFromIntegral xTo in+                delegateCall this xGas target (litAddr self) 0 xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                  touchAccount self             _ -> underrun          -- op: CREATE2@@ -1190,31 +1208,29 @@                     newAddr  = create2Address self (num xSalt) initCode                     (cost, gas') = costOfCreate fees availableGas xSize                    in burn (cost - gas') $-                    create self this gas' xValue xs newAddr initCode+                    create self this (num gas') xValue xs newAddr initCode             _ -> underrun          -- op: STATICCALL         0xfa ->           case stk of             (xGas'-             :xTo'+             :S _ xTo              :xInOffset'              :xInSize'              :xOutOffset'              :xOutSize'-             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $-              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->-                case xTo of-                  n | n > 0 && n <= 9 ->-                    precompiledContract this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs-                  _ -> delegateCall this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ do-                            zoom state $ do-                              assign callvalue 0-                              assign caller (litAddr self)-                              assign contract xTo-                              assign static True-                            touchAccount self-                            touchAccount xTo+             :xs) -> forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do+                let target = SAddr $ sFromIntegral xTo+                delegateCall this xGas target target 0 xInOffset xInSize xOutOffset xOutSize xs $ \callee -> do+                  zoom state $ do+                    assign callvalue 0+                    assign caller (litAddr self)+                    assign contract callee+                    assign static True+                  touchAccount self+                  touchAccount callee             _ ->               underrun @@ -1265,8 +1281,8 @@ callChecks   :: (?op :: Word8)   => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]-   -- continuation with gas avail for call-  -> (Word -> EVM ())+   -- continuation with gas available for call+  -> (Integer -> EVM ())   -> EVM () callChecks this xGas xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue = do   vm <- get@@ -1287,7 +1303,7 @@              then do                assign (state . stack) (0 : xs)                assign (state . returndata) mempty-               pushTrace $ ErrorTrace $ CallDepthLimitReached+               pushTrace $ ErrorTrace CallDepthLimitReached                next              else continue gas' @@ -1324,7 +1340,7 @@ executePrecompile   :: (?op :: Word8)   => Addr-  -> Word -> Word -> Word -> Word -> Word -> [SymWord]+  -> Integer -> Word -> Word -> Word -> Word -> [SymWord]   -> EVM () executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do   vm <- get@@ -1332,12 +1348,12 @@       fees = view (block . schedule) vm       cost = costOfPrecompile fees preCompileAddr input       notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented"-      precompileFail = burn (gasCap - cost) $ do+      precompileFail = burn (num gasCap - cost) $ do                          assign (state . stack) (0 : xs)-                         pushTrace $ ErrorTrace $ PrecompileFailure+                         pushTrace $ ErrorTrace PrecompileFailure                          next-  if cost > gasCap then-    burn gasCap $ do+  if cost > num gasCap then+    burn (num gasCap) $ do       assign (state . stack) (0 : xs)       next   else@@ -1363,7 +1379,7 @@         0x2 ->           let             hash = case input of-                     ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack $ (Crypto.hash input' :: Digest SHA256)+                     ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack (Crypto.hash input' :: Digest SHA256)                      SymbolicBuffer input' -> SymbolicBuffer $ symSHA256 input'           in do             assign (state . stack) (1 : xs)@@ -1407,9 +1423,9 @@                    truncpadlit (num lenm) (asBE (0 :: Int))                  False ->                    let-                     b = asInteger $ lazySlice 96 lenb $ input'-                     e = asInteger $ lazySlice (96 + lenb) lene $ input'-                     m = asInteger $ lazySlice (96 + lenb + lene) lenm $ input'+                     b = asInteger $ lazySlice 96 lenb input'+                     e = asInteger $ lazySlice (96 + lenb) lene input'+                     m = asInteger $ lazySlice (96 + lenb + lene) lenm input'                    in                      padLeft (num lenm) (asBE (expFast b e m))           in do@@ -1521,9 +1537,23 @@ getCodeLocation :: VM -> CodeLocation getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm) +-- | Ask the SMT solver to provide a concrete model for val iff a unique model exists+makeUnique :: SymWord -> (Word -> EVM ()) -> EVM ()+makeUnique sw@(S w val) cont = case maybeLitWord sw of+  Nothing -> do+    conditions <- use constraints+    assign result . Just . VMFailure . Query $ PleaseMakeUnique val (fst <$> conditions) $ \case+      Unique a -> do+        assign result Nothing+        cont (C w $ fromSizzle a)+      InconsistentU -> vmError $ DeadPath+      TimeoutU -> vmError $ SMTTimeout+      Multiple -> vmError $ NotUnique w+  Just a -> cont a+ -- | Construct SMT Query and halt execution until resolved-askSMT :: CodeLocation -> SBool -> (Bool -> EVM ()) -> EVM ()-askSMT codeloc condition continue = do+askSMT :: CodeLocation -> (SBool, Whiff) -> (Bool -> EVM ()) -> EVM ()+askSMT codeloc (condition, whiff) 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)@@ -1535,20 +1565,22 @@      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+     Nothing -> do pathconds <- use constraints                    assign result . Just . VMFailure . Query $ PleaseAskSMT-                     condition pathconds choosePath+                     condition' (fst <$> pathconds) choosePath -   where -- Only one path is possible+   where condition' = simplifyCondition condition whiff+     -- Only one path is possible+          choosePath :: BranchCondition -> EVM ()          choosePath (Case v) = do assign result Nothing-                                  pushTo pathConditions (if v then condition else sNot condition)+                                  pushTo constraints $ if v then (condition', whiff) else (sNot condition', IsZero whiff)                                   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 . Case+         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath whiff $ choosePath . Case          -- None of the paths are possible; fail this branch          choosePath Inconsistent = vmError DeadPath @@ -1562,9 +1594,10 @@         Just c -> do           assign (env . contracts . at addr) (Just c)           continue c-        Nothing ->-          assign result . Just . VMFailure . Query $-            PleaseFetchContract addr+        Nothing -> do+          model <- use (env . storageModel)+          assign result . Just . VMFailure $ Query $+            PleaseFetchContract addr model               (\c -> do assign (cache . fetched . at addr) (Just c)                         assign (env . contracts . at addr) (Just c)                         assign result Nothing@@ -1576,11 +1609,11 @@         else continue c  readStorage :: Storage -> SymWord -> Maybe (SymWord)-readStorage (Symbolic s) (S _ loc) = Just . sw256 $ readArray s loc+readStorage (Symbolic _ s) (S w loc) = Just $ S (FromStorage w s) $ readArray s loc readStorage (Concrete s) loc = Map.lookup (forceLit loc) s  writeStorage :: SymWord -> SymWord -> Storage -> Storage-writeStorage (S _ loc) (S _ val) (Symbolic s) = Symbolic (writeArray s loc val)+writeStorage k@(S _ loc) v@(S _ val) (Symbolic xs s) = Symbolic ((k,v):xs) (writeArray s loc val) writeStorage loc val (Concrete s) = Concrete (Map.insert (forceLit loc) val s)  accessStorage@@ -1635,7 +1668,6 @@ finalize :: EVM () finalize = do   let-    burnRemainingGas = use (state . gas) >>= flip burn noop     revertContracts  = use (tx . txReversion) >>= assign (env . contracts)     revertSubstate   = assign (tx . substate) (SubState mempty mempty mempty) @@ -1646,7 +1678,8 @@       revertContracts       revertSubstate     Just (VMFailure _) -> do-      burnRemainingGas+      -- burn remaining gas+      assign (state . gas) 0       revertContracts       revertSubstate     Just (VMSuccess output) -> do@@ -1662,14 +1695,14 @@   txOrigin     <- use (tx . origin)   sumRefunds   <- (sum . (snd <$>)) <$> (use (tx . substate . refunds))   miner        <- use (block . coinbase)-  blockReward  <- r_block <$> (use (block . schedule))+  blockReward  <- num . r_block <$> (use (block . schedule))   gasPrice     <- use (tx . gasprice)   gasLimit     <- use (tx . txgaslimit)   gasRemaining <- use (state . gas)    let     gasUsed      = gasLimit - gasRemaining-    cappedRefund = min (quot gasUsed 2) sumRefunds+    cappedRefund = min (quot gasUsed 2) (num sumRefunds)     originPay    = (gasRemaining + cappedRefund) * gasPrice     minerPay     = gasPrice * (gasUsed - cappedRefund) @@ -1735,16 +1768,22 @@     else continue  -- | Burn gas, failing if insufficient gas is available-burn :: Word -> EVM () -> EVM ()-burn n continue = do-  available <- use (state . gas)-  if n <= available-    then do-      state . gas -= n-      burned += n-      continue-    else-      vmError (OutOfGas available n)+-- We use the `Integer` type to avoid overflows in intermediate+-- calculations and throw if the value won't fit into a uint64+burn :: Integer -> EVM () -> EVM ()+burn n' continue =+  if n' > (2 :: Integer) ^ (64 :: Integer) - 1+  then vmError IllegalOverflow+  else do+    let n = num n'+    available <- use (state . gas)+    if n <= available+      then do+        state . gas -= n+        burned += n+        continue+      else+        vmError (OutOfGas available n)  forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM () forceConcreteAddr n continue = case maybeLitAddr n of@@ -1788,12 +1827,12 @@ forceConcreteBuffer (ConcreteBuffer b) continue = continue b  -- * Substate manipulation-refund :: Word -> EVM ()+refund :: Integer -> EVM () refund n = do   self <- use (state . contract)   pushTo (tx . substate . refunds) (self, n) -unRefund :: Word -> EVM ()+unRefund :: Integer -> EVM () unRefund n = do   self <- use (state . contract)   refs <- use (tx . substate . refunds)@@ -1831,101 +1870,110 @@       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'))+        Just action -> do+            action outOffset outSize input+            next+            push 1 -type CheatAction = ([AbiType], Word -> Word -> [AbiValue] -> EVM ())+type CheatAction = Word -> Word -> Buffer -> EVM ()  cheatActions :: Map Word32 CheatAction cheatActions =   Map.fromList-    [ action "warp(uint256)" [AbiUIntType 256] $-        \_ _ [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-          let slot = w256lit $ word x-              new  = w256lit $ word y-          fetchAccount a $ \_ -> do-            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+    [ action "warp(uint256)" $+        \sig _ _ input -> case decodeStaticArgs input of+          [x]  -> assign (block . timestamp) (mksym x)+          _ -> vmError (BadCheatCode sig),++      action "roll(uint256)" $+        \sig _ _ input -> case decodeStaticArgs input of+          [x] -> forceConcrete (mksym x) (assign (block . number))+          _ -> vmError (BadCheatCode sig),++      action "store(address,bytes32,bytes32)" $+        \sig _ _ input -> case decodeStaticArgs input of+          [a, slot, new] ->+            makeUnique (mksym $ sFromIntegral a) $ \(C _ (num -> a')) ->+              fetchAccount a' $ \_ -> do+                modifying (env . contracts . ix a' . storage) (writeStorage (mksym slot) (mksym new))+          _ -> vmError (BadCheatCode sig),++      action "load(address,bytes32)" $+        \sig outOffset _ input -> case decodeStaticArgs input of+          [a, slot] ->+            makeUnique (mksym $ sFromIntegral a) $ \(C _ (num -> a'))->+              accessStorage a' (mksym slot) $ \res -> do+                assign (state . returndata . word256At 0) res+                assign (state . memory . word256At outOffset) res+          _ -> vmError (BadCheatCode sig)     ]   where-    action s ts f = (abiKeccak s, (ts, f))+    action s f = (abiKeccak s, f (Just $ abiKeccak s))+    mksym x = S (Todo "abidecode" []) x  -- * General call implementation ("delegateCall") delegateCall   :: (?op :: Word8)-  => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]-  -> EVM ()+  => Contract -> Word -> SAddr -> SAddr -> Word -> Word -> Word -> Word -> Word -> [SymWord]+  -> (Addr -> EVM ())   -> EVM ()-delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue =-  callChecks this gasGiven xContext xValue xInOffset xInSize xOutOffset xOutSize xs $-  \xGas -> do-    vm0 <- get-    fetchAccount xTo . const $-      preuse (env . contracts . ix xTo) >>= \case-        Nothing ->-          vmError (NoSuchContract xTo)-        Just target ->-          burn xGas $ do-            let newContext = CallContext-                  { callContextTarget    = xTo-                  , callContextContext   = xContext-                  , callContextOffset    = xOutOffset-                  , callContextSize      = xOutSize-                  , callContextCodehash  = view codehash target-                  , callContextReversion = view (env . contracts) vm0-                  , callContextSubState  = view (tx . substate) vm0-                  , callContextAbi =-                      if xInSize >= 4-                      then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)-                           of Nothing -> Nothing-                              Just abi -> Just . w256 $ num abi-                      else Nothing-                  , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)-                  }+delegateCall this gasGiven (SAddr xTo) (SAddr xContext) xValue xInOffset xInSize xOutOffset xOutSize xs continue =+  makeUnique (S (Todo "xTo" []) $ sFromIntegral xTo) $ \(C _ (num -> xTo')) ->+    makeUnique (S (Todo "xcontext" []) $ sFromIntegral xContext) $ \(C _ (num -> xContext')) ->+      if xTo' > 0 && xTo' <= 9+      then precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs+      else if num xTo' == cheatCode then+        do+          assign (state . stack) xs+          cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+      else+        callChecks this gasGiven xContext' xValue xInOffset xInSize xOutOffset xOutSize xs $+        \xGas -> do+          vm0 <- get+          fetchAccount xTo' . const $+            preuse (env . contracts . ix xTo') >>= \case+              Nothing ->+                vmError (NoSuchContract xTo')+              Just target -> do+                burn xGas $ do+                  let newContext = CallContext+                                    { callContextTarget    = xTo'+                                    , callContextContext   = xContext'+                                    , callContextOffset    = xOutOffset+                                    , callContextSize      = xOutSize+                                    , callContextCodehash  = view codehash target+                                    , callContextReversion = view (env . contracts) vm0+                                    , callContextSubState  = view (tx . substate) vm0+                                    , callContextAbi =+                                        if xInSize >= 4+                                        then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)+                                             of Nothing -> Nothing+                                                Just abi -> Just . w256 $ num abi+                                        else Nothing+                                    , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)+                                    } -            pushTrace (FrameTrace newContext)-            next-            vm1 <- get+                  pushTrace (FrameTrace newContext)+                  next+                  vm1 <- get -            pushTo frames $ Frame-              { _frameState = (set stack xs) (view state vm1)-              , _frameContext = newContext-              }+                  pushTo frames $ Frame+                    { _frameState = (set stack xs) (view state vm1)+                    , _frameContext = newContext+                    } -            zoom state $ do-              assign gas xGas-              assign pc 0-              assign code (view bytecode target)-              assign codeContract xTo-              assign stack mempty-              assign memory mempty-              assign memorySize 0-              assign returndata mempty-              assign calldata (readMemory (num xInOffset) (num xInSize) vm0, literal (num xInSize))+                  zoom state $ do+                    assign gas (num xGas)+                    assign pc 0+                    assign code (view bytecode target)+                    assign codeContract xTo'+                    assign stack mempty+                    assign memory mempty+                    assign memorySize 0+                    assign returndata mempty+                    assign calldata (readMemory (num xInOffset) (num xInSize) vm0, w256lit (num xInSize)) -            continue+                  continue xTo'  -- -- * Contract creation @@ -1938,8 +1986,9 @@ create :: (?op :: Word8)   => Addr -> Contract   -> Word -> Word -> [SymWord] -> Addr -> ByteString -> EVM ()-create self this xGas xValue xs newAddr initCode = do+create self this xGas' xValue xs newAddr initCode = do   vm0 <- get+  let xGas = num xGas'   if xValue > view balance this   then do     assign (state . stack) (0 : xs)@@ -1958,46 +2007,47 @@     modifying (env . contracts . ix self . nonce) succ     next   else burn xGas $ do-        touchAccount self-        touchAccount newAddr-        let-          store = case view (env . storageModel) vm0 of-            ConcreteS -> Concrete mempty-            SymbolicS -> Symbolic $ sListArray 0 []-            InitialS -> Symbolic $ sListArray 0 []-          newContract =-            initialContract (InitCode initCode) & set storage store-          newContext  =-            CreationContext { creationContextCodehash  = view codehash newContract-                            , creationContextReversion = view (env . contracts) vm0-                            , creationContextSubstate = view (tx . substate) vm0-                            }+    touchAccount self+    touchAccount newAddr+    let+      store = case view (env . storageModel) vm0 of+        ConcreteS -> Concrete mempty+        SymbolicS -> Symbolic [] $ sListArray 0 []+        InitialS  -> Symbolic [] $ sListArray 0 []+      newContract =+        initialContract (InitCode initCode) & set storage store+      newContext  =+        CreationContext { creationContextAddress   = newAddr+                        , creationContextCodehash  = view codehash newContract+                        , creationContextReversion = view (env . contracts) vm0+                        , creationContextSubstate  = view (tx . substate) vm0+                        } -        zoom (env . contracts) $ do-          oldAcc <- use (at newAddr)-          let oldBal = maybe 0 (view balance) oldAcc+    zoom (env . contracts) $ do+      oldAcc <- use (at newAddr)+      let oldBal = maybe 0 (view balance) oldAcc -          assign (at newAddr) (Just (newContract & balance .~ oldBal))-          modifying (ix self . nonce) succ+      assign (at newAddr) (Just (newContract & balance .~ oldBal))+      modifying (ix self . nonce) succ -        transfer self newAddr xValue+    transfer self newAddr xValue -        pushTrace (FrameTrace newContext)-        next-        vm1 <- get-        pushTo frames $ Frame-          { _frameContext = newContext-          , _frameState   = (set stack xs) (view state vm1)-          }+    pushTrace (FrameTrace newContext)+    next+    vm1 <- get+    pushTo frames $ Frame+      { _frameContext = newContext+      , _frameState   = (set stack xs) (view state vm1)+      } -        assign state $-          blankState-            & set contract   newAddr-            & set codeContract newAddr-            & set code       initCode-            & set callvalue  (litWord xValue)-            & set caller     (litAddr self)-            & set gas        xGas+    assign state $+      blankState+        & set contract   newAddr+        & set codeContract newAddr+        & set code       initCode+        & set callvalue  (litWord xValue)+        & set caller     (litAddr self)+        & set gas        xGas'  -- | Replace a contract's code, like when CREATE returns -- from the constructor code.@@ -2065,10 +2115,6 @@     -- Are there some remaining frames?     nextFrame : remainingFrames -> do -      -- Pop the top frame.-      assign frames remainingFrames-      -- Install the state of the frame to which we shall return.-      assign state (view frameState nextFrame)       -- Insert a debug trace.       insertTrace $         case how of@@ -2083,6 +2129,11 @@       -- Pop to the previous level of the debug trace stack.       popTrace +      -- Pop the top frame.+      assign frames remainingFrames+      -- Install the state of the frame to which we shall return.+      assign state (view frameState nextFrame)+       -- When entering a call, the gas allowance is counted as burned       -- in advance; this unburns the remainder and adds it to the       -- parent frame.@@ -2127,9 +2178,8 @@               revertSubstate               assign (state . returndata) mempty               push 0-         -- Or were we creating?-        CreationContext _ reversion substate' -> do+        CreationContext _ _ reversion substate' -> do           creator <- use (state . contract)           let             createe = view (state . contract) oldVm@@ -2167,7 +2217,7 @@ -- * Memory helpers  accessUnboundedMemoryRange-  :: FeeSchedule Word+  :: FeeSchedule Integer   -> Word   -> Word   -> EVM ()@@ -2182,7 +2232,7 @@       continue  accessMemoryRange-  :: FeeSchedule Word+  :: FeeSchedule Integer   -> Word   -> Word   -> EVM ()@@ -2194,7 +2244,7 @@     else accessUnboundedMemoryRange fees f l continue  accessMemoryWord-  :: FeeSchedule Word -> Word -> EVM () -> EVM ()+  :: FeeSchedule Integer -> Word -> EVM () -> EVM () accessMemoryWord fees x = accessMemoryRange fees x 32  copyBytesToMemory@@ -2234,11 +2284,11 @@   vm <- get   let     Just this =-      preview (env . contracts . ix (view (state . codeContract) vm)) vm+      currentContract vm   pure Trace     { _traceData = x     , _traceCodehash = view codehash this-    , _traceOpIx = (view opIxMap this) Vector.! (view (state . pc) vm)+    , _traceOpIx = (view opIxMap this) Vector.!? (view (state . pc) vm)     }  pushTrace :: TraceData -> EVM ()@@ -2286,7 +2336,7 @@  stackOp1   :: (?op :: Word8)-  => ((SymWord) -> Word)+  => ((SymWord) -> Integer)   -> ((SymWord) -> (SymWord))   -> EVM () stackOp1 cost f =@@ -2301,7 +2351,7 @@  stackOp2   :: (?op :: Word8)-  => (((SymWord), (SymWord)) -> Word)+  => (((SymWord), (SymWord)) -> Integer)   -> (((SymWord), (SymWord)) -> (SymWord))   -> EVM () stackOp2 cost f =@@ -2315,7 +2365,7 @@  stackOp3   :: (?op :: Word8)-  => (((SymWord), (SymWord), (SymWord)) -> Word)+  => (((SymWord), (SymWord), (SymWord)) -> Integer)   -> (((SymWord), (SymWord), (SymWord)) -> (SymWord))   -> EVM () stackOp3 cost f =@@ -2334,13 +2384,15 @@   theCode <- use (state . code)   self <- use (state . codeContract)   theCodeOps <- use (env . contracts . ix self . codeOps)+  theOpIxMap <- use (env . contracts . ix self . opIxMap)   if x < num (BS.length theCode) && BS.index theCode (num x) == 0x5b     then-      case RegularVector.find (\(i, op) -> i == num x && op == OpJumpdest) theCodeOps of-        Nothing ->  vmError BadJumpDestination-        _ -> do-             state . stack .= xs-             state . pc .= num x+      if OpJumpdest == snd (theCodeOps RegularVector.! (theOpIxMap Vector.! num x))+      then do+        state . stack .= xs+        state . pc .= num x+      else+        vmError BadJumpDestination     else vmError BadJumpDestination  opSize :: Word8 -> Int@@ -2507,12 +2559,14 @@  -- Gas cost function for CALL, transliterated from the Yellow Paper. costOfCall-  :: FeeSchedule Word+  :: FeeSchedule Integer   -> Bool -> Word -> Word -> Word-  -> (Word, Word)-costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas =+  -> (Integer, Integer)+costOfCall (FeeSchedule {..}) recipientExists xValue availableGas' xGas' =   (c_gascap + c_extra, c_callgas)   where+    availableGas = num availableGas'+    xGas = num xGas'     c_extra =       num g_call + c_xfer + c_new     c_xfer =@@ -2530,17 +2584,18 @@  -- Gas cost of create, including hash cost if needed costOfCreate-  :: FeeSchedule Word-  -> Word -> Word -> (Word, Word)-costOfCreate (FeeSchedule {..}) availableGas hashSize =+  :: FeeSchedule Integer+  -> Word -> Word -> (Integer, Integer)+costOfCreate (FeeSchedule {..}) availableGas' hashSize =   (createCost + initGas, initGas)   where+    availableGas = num availableGas'     createCost = g_create + hashCost-    hashCost   = g_sha3word * ceilDiv (hashSize) 32+    hashCost   = g_sha3word * ceilDiv (num hashSize) 32     initGas    = allButOne64th (availableGas - createCost)  -- Gas cost of precompiles-costOfPrecompile :: FeeSchedule Word -> Addr -> Buffer -> Word+costOfPrecompile :: FeeSchedule Integer -> Addr -> Buffer -> Integer costOfPrecompile (FeeSchedule {..}) precompileAddr input =   case precompileAddr of     -- ECRECOVER@@ -2584,7 +2639,7 @@     _ -> error ("unimplemented precompiled contract " ++ show precompileAddr)  -- Gas cost of memory expansion-memoryCost :: FeeSchedule Word -> Word -> Word+memoryCost :: FeeSchedule Integer -> Integer -> Integer memoryCost FeeSchedule{..} byteCount =   let     wordCount = ceilDiv byteCount 32@@ -2592,32 +2647,6 @@     quadraticCost = div (wordCount * wordCount) 512   in     linearCost + quadraticCost---- * Uninterpreted functions--symSHA256N :: SInteger -> SInteger -> SWord 256-symSHA256N = uninterpret "sha256"--symkeccakN :: SInteger -> SInteger -> SWord 256-symkeccakN = uninterpret "keccak"--toSInt :: [SWord 8] -> SInteger-toSInt bs = sum $ zipWith (\a i -> sFromIntegral a * 256 ^ i) bs [0..]---- | Although we'd like to define this directly as an uninterpreted function,--- we cannot because [a] is not a symbolic type. We must convert the list into a suitable--- symbolic type first. The only important property of this conversion is that it is injective.--- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.-symkeccak' :: [SWord 8] -> SWord 256-symkeccak' bytes = case length bytes of-  0 -> literal $ toSizzle $ keccak ""-  n -> symkeccakN (num n) (toSInt bytes)--symSHA256 :: [SWord 8] -> [SWord 8]-symSHA256 bytes = case length bytes of-  0 -> litBytes $ BS.pack $ BA.unpack $ (Crypto.hash BS.empty :: Digest SHA256)-  n -> toBytes $ symSHA256N (num n) (toSInt bytes)-  -- * Arithmetic 

@@ -26,6 +26,7 @@ -}  {-# Language StrictData #-}+{-# Language DataKinds #-}  module EVM.ABI   ( AbiValue (..)@@ -46,28 +47,31 @@   , emptyAbi   , encodeAbiValue   , decodeAbiValue+  , decodeStaticArgs+  , formatString   , parseTypeName   , makeAbiValue   , parseAbiValue   , selector   ) where -import EVM.Keccak (abiKeccak) import EVM.Types  import Control.Monad      (replicateM, replicateM_, forM_, void)-import Data.Binary.Get    (Get, runGet, label, getWord8, getWord32be, skip)+import Data.Binary.Get    (Get, runGet, runGetOrFail, label, getWord8, getWord32be, skip) import Data.Binary.Put    (Put, runPut, putWord8, putWord32be) import Data.Bits          (shiftL, shiftR, (.&.)) import Data.ByteString    (ByteString) import Data.DoubleWord    (Word256, Int256, signedWord) import Data.Functor       (($>)) import Data.Monoid        ((<>))-import Data.Text          (Text, pack)-import Data.Text.Encoding (encodeUtf8)-import Data.Vector        (Vector)+import Data.Text          (Text, pack, unpack)+import Data.Text.Encoding (encodeUtf8, decodeUtf8')+import Data.Vector        (Vector, toList) import Data.Word          (Word32) import Data.List          (intercalate)+import Data.SBV           (SWord, fromBytes, sFromIntegral, literal)+import Data.Maybe import GHC.Generics  import Test.QuickCheck hiding ((.&.), label)@@ -104,7 +108,7 @@   show (AbiBool b)           = if b then "true" else "false"   show (AbiBytes      _ b)   = show (ByteStringS b)   show (AbiBytesDynamic b)   = show (ByteStringS b)-  show (AbiString       s)   = show s+  show (AbiString       s)   = formatString s   show (AbiArrayDynamic _ v) =     "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]"   show (AbiArray      _ _ v) =@@ -112,6 +116,12 @@   show (AbiTuple v) =     "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")" +formatString :: ByteString -> String+formatString bs =+  case decodeUtf8' (fst (BS.spanEnd (== 0) bs)) of+    Right s -> "\"" <> unpack s <> "\""+    Left _ -> "❮utf8 decode failed❯: " <> (show $ ByteStringS bs)+ data AbiType   = AbiUIntType         Int   | AbiIntType          Int@@ -183,7 +193,7 @@      AbiIntType n   -> asUInt n (AbiInt n)     AbiAddressType -> asUInt 256 AbiAddress-    AbiBoolType    -> asUInt 256 (AbiBool . (== (1 :: Int)))+    AbiBoolType    -> asUInt 256 (AbiBool . (> (0 :: Integer)))      AbiBytesType n ->       AbiBytes n <$> getBytesWith256BitPadding n@@ -194,8 +204,9 @@           >>= label "bytes data" . getBytesWith256BitPadding)      AbiStringType -> do-      AbiBytesDynamic x <- getAbi AbiBytesDynamicType-      pure (AbiString x)+      AbiString <$>+        (label "string length prefix" getWord256+          >>= label "string data" . getBytesWith256BitPadding)      AbiArrayType n t' ->       AbiArray n t' <$> getAbiSeq n (repeat t')@@ -497,17 +508,17 @@  makeAbiValue :: AbiType -> String -> AbiValue makeAbiValue typ str = case readP_to_S (parseAbiValue typ) str of-  [] -> error "could not parse abi arguments"-  ((val,_):_) -> val+  [(val,"")] -> val+  _ -> error $  "could not parse abi argument: " ++ str ++ " : " ++ show typ  parseAbiValue :: AbiType -> ReadP AbiValue-parseAbiValue (AbiUIntType n) = do W256 w256 <- readS_to_P reads-                                   return $ AbiUInt n w256-parseAbiValue (AbiIntType n) = do W256 w256 <- readS_to_P reads-                                  return $ AbiInt n (num w256)+parseAbiValue (AbiUIntType n) = do W256 w <- readS_to_P reads+                                   return $ AbiUInt n w+parseAbiValue (AbiIntType n) = do W256 w <- readS_to_P reads+                                  return $ AbiInt n (num w) parseAbiValue AbiAddressType = AbiAddress <$> readS_to_P reads-parseAbiValue AbiBoolType = (do W256 w256 <- readS_to_P reads-                                return $ AbiBool (w256 /= 0))+parseAbiValue AbiBoolType = (do W256 w <- readS_to_P reads+                                return $ AbiBool (w /= 0))                             <|> (do Boolz b <- readS_to_P reads                                     return $ AbiBool b) parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- readS_to_P reads@@ -529,6 +540,12 @@                                                   skipSpaces                                                   return a) `sepBy` (char ',')) +decodeStaticArgs :: Buffer -> [SWord 256]+decodeStaticArgs buffer = let+    bs = case buffer of+      ConcreteBuffer b -> litBytes b+      SymbolicBuffer b -> b+  in fmap (\i -> fromBytes $ take 32 (drop (i*32) bs)) [0..((length bs) `div` 32 - 1)]  -- A modification of 'arbitrarySizedBoundedIntegral' quickcheck library -- which takes the maxbound explicitly rather than relying on a Bounded instance.

@@ -5,12 +5,11 @@  import Prelude hiding (Word) -import EVM.Keccak (keccak) import EVM.RLP-import EVM.Types (Addr, W256 (..), num, word, padRight, word160Bytes, word256Bytes, Buffer)+import EVM.Types  import Control.Lens    ((^?), ix)-import Data.Bits       (Bits (..), FiniteBits (..), shiftL, shiftR)+import Data.Bits       (Bits (..), shiftL, shiftR) import Data.ByteString (ByteString) import Data.Maybe      (fromMaybe) import Data.Semigroup  ((<>))@@ -36,21 +35,7 @@     let bs' = BS.take size (BS.drop offset bs)     in bs' <> BS.replicate (size - BS.length bs') 0 --- | This type can give insight into the provenance of a term-data Whiff = Dull-           | FromKeccak ByteString-           | Var String-           | FromBytes Buffer-           | InfixBinOp String Whiff Whiff-           | BinOp String Whiff Whiff-           | UnOp String Whiff-  deriving Show -w256 :: W256 -> Word-w256 = C Dull--data Word = C Whiff W256 --maybe to remove completely in the future- wordValue :: Word -> W256 wordValue (C _ x) = x @@ -76,12 +61,14 @@  readMemoryWord :: Word -> ByteString -> Word readMemoryWord (C _ i) m =+  if i > (num $ BS.length m) then 0 else   let     go !a (-1) = a     go !a !n = go (a + shiftL (num $ readByteOrZero (num i + n) m)                               (8 * (31 - n))) (n - 1)+    w = go (0 :: W256) (31 :: Int)   in {-# SCC "readMemoryWord" #-}-    w256 $ go (0 :: W256) (31 :: Int)+    C (Literal w) w  readMemoryWord32 :: Word -> ByteString -> Word readMemoryWord32 (C _ i) m =@@ -100,81 +87,8 @@ setMemoryByte (C _ i) x =   writeMemory (BS.singleton x) 1 0 (num i) -readBlobWord :: Word -> ByteString -> Word-readBlobWord (C _ i) x =-  if i > num (BS.length x)-  then 0-  else w256 (wordAt (num i) x)--blobSize :: ByteString -> Word-blobSize x = w256 (num (BS.length x))- keccakBlob :: ByteString -> Word-keccakBlob x = C (FromKeccak x) (keccak x)--instance Show Word where-  show (C Dull x) = show x-  show (C (Var var) x) = var ++ ": " ++ show x-  show (C (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z-  show (C (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z-  show (C (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z-  show (C whiff x) = show whiff ++ ": " ++ show x--instance Read Word where-  readsPrec n s =-    case readsPrec n s of-      [(x, r)] -> [(C Dull x, r)]-      _ -> []--instance Bits Word where-  (C _ x) .&. (C _ y) = w256 (x .&. y)-  (C _ x) .|. (C _ y) = w256 (x .|. y)-  (C _ x) `xor` (C _ y) = w256 (x `xor` y)-  complement (C _ x) = w256 (complement x)-  shift (C _ x) i = w256 (shift x i)-  rotate (C _ x) i = w256 (rotate x i)-  bitSize (C _ x) = bitSize x-  bitSizeMaybe (C _ x) = bitSizeMaybe x-  isSigned (C _ x) = isSigned x-  testBit (C _ x) = testBit x-  bit i = w256 (bit i)-  popCount (C _ x) = popCount x--instance FiniteBits Word where-  finiteBitSize (C _ x) = finiteBitSize x-  countLeadingZeros (C _ x) = countLeadingZeros x-  countTrailingZeros (C _ x) = countTrailingZeros x--instance Bounded Word where-  minBound = w256 minBound-  maxBound = w256 maxBound--instance Eq Word where-  (C _ x) == (C _ y) = x == y--instance Enum Word where-  toEnum i = w256 (toEnum i)-  fromEnum (C _ x) = fromEnum x--instance Integral Word where-  quotRem (C _ x) (C _ y) =-    let (a, b) = quotRem x y-    in (w256 a, w256 b)-  toInteger (C _ x) = toInteger x--instance Num Word where-  (C _ x) + (C _ y) = w256 (x + y)-  (C _ x) * (C _ y) = w256 (x * y)-  abs (C _ x) = w256 (abs x)-  signum (C _ x) = w256 (signum x)-  fromInteger x = w256 (fromInteger x)-  negate (C _ x) = w256 (negate x)--instance Real Word where-  toRational (C _ x) = toRational x--instance Ord Word where-  compare (C _ x) (C _ y) = compare x y+keccakBlob x = C (FromKeccak (ConcreteBuffer x)) (keccak x)  -- Copied from the standard library just to get specialization. -- We also use bit operations instead of modulo and multiply.

@@ -1,54 +1,70 @@ {-# Language TemplateHaskell #-}+{-# Language OverloadedStrings #-}  module EVM.Dapp where -import EVM (Trace, traceCodehash, traceOpIx)+import EVM (Trace, traceCodehash, traceOpIx, Env) import EVM.ABI (Event, AbiType) import EVM.Debug (srcMapCodePos)-import EVM.Keccak (abiKeccak)-import EVM.Solidity (SolcContract, CodeType (..), SourceCache, SrcMap)+import EVM.Solidity (SolcContract, CodeType (..), SourceCache (..), SrcMap, Method) import EVM.Solidity (contractName, methodInputs) import EVM.Solidity (runtimeCodehash, creationCodehash, abiMap)-import EVM.Solidity (runtimeSrcmap, creationSrcmap, eventMap)-import EVM.Solidity (methodSignature, contractAst, astIdMap, astSrcMap)-import EVM.Types (W256)+import EVM.Solidity (runtimeSrcmap, sourceAsts, creationSrcmap, eventMap)+import EVM.Solidity (methodSignature, astIdMap, astSrcMap)+import EVM.Types (W256, abiKeccak)  import Data.Aeson (Value)-import Data.Text (Text, isPrefixOf, pack)+import Data.Bifunctor (first)+import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8)-import Data.Map (Map)+import Data.Map (Map, toList) import Data.Monoid ((<>))+import Data.Maybe (isJust, fromJust) import Data.Word (Word32)  import Control.Applicative ((<$>)) import Control.Arrow ((>>>)) import Control.Lens -import qualified Data.Map as Map+import qualified Data.Map        as Map+import qualified Data.Sequence   as Seq+import qualified Text.Regex.TDFA as Regex  data DappInfo = DappInfo   { _dappRoot       :: FilePath   , _dappSolcByName :: Map Text SolcContract   , _dappSolcByHash :: Map W256 (CodeType, SolcContract)   , _dappSources    :: SourceCache-  , _dappUnitTests  :: [(Text, [(Text, [AbiType])])]+  , _dappUnitTests  :: [(Text, [(Test, [AbiType])])]+  , _dappAbiMap     :: Map Word32 Method   , _dappEventMap   :: Map W256 Event   , _dappAstIdMap   :: Map Int Value   , _dappAstSrcMap  :: SrcMap -> Maybe Value   } +data DappContext = DappContext+  { _contextInfo :: DappInfo+  , _contextEnv  :: Env+  }++data Test = ConcreteTest Text | SymbolicTest Text+ makeLenses ''DappInfo+makeLenses ''DappContext +instance Show Test where+  show t = unpack $ extractSig t+ dappInfo   :: FilePath -> Map Text SolcContract -> SourceCache -> DappInfo dappInfo root solcByName sources =   let     solcs = Map.elems solcByName-    astIds = astIdMap (map (view contractAst) solcs)+    astIds = astIdMap $ snd <$> toList (view sourceAsts sources)    in DappInfo     { _dappRoot = root-    , _dappUnitTests = findUnitTests ("test" `isPrefixOf`) solcs+    , _dappUnitTests = findAllUnitTests solcs     , _dappSources = sources     , _dappSolcByName = solcByName     , _dappSolcByHash =@@ -59,35 +75,78 @@            (f runtimeCodehash  Runtime)            (f creationCodehash Creation) -    , _dappEventMap =-        -- Sum up the event ABI maps from all the contracts.-        mconcat (map (view eventMap) solcs)+      -- Sum up the ABI maps from all the contracts.+    , _dappAbiMap   = mconcat (map (view abiMap) solcs)+    , _dappEventMap = mconcat (map (view eventMap) solcs)      , _dappAstIdMap  = astIds     , _dappAstSrcMap = astSrcMap astIds     } +emptyDapp :: DappInfo+emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty)++-- Dapp unit tests are detected by searching within abi methods+-- that begin with "test" or "prove", that are in a contract with+-- the "IS_TEST()" abi marker, for a given regular expression.+--+-- The regex is matched on the full test method name, including path+-- and contract, i.e. "path/to/file.sol:TestContract.test_name()".+--+-- Tests beginning with "test" are interpreted as concrete tests, whereas+-- tests beginning with "prove" are interpreted as symbolic tests.+ unitTestMarkerAbi :: Word32 unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()") -findUnitTests :: (Text -> Bool) -> ([SolcContract] -> [(Text, [(Text, [AbiType])])])-findUnitTests matcher =+findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])]+findAllUnitTests = findUnitTests ".*:.*\\.(test|prove).*"++mkTest :: Text -> Maybe Test+mkTest sig+  | "test" `isPrefixOf` sig = Just (ConcreteTest sig)+  | "prove" `isPrefixOf` sig = Just (SymbolicTest sig)+  | otherwise = Nothing++regexMatches :: Text -> Text -> Bool+regexMatches regexSource =+  let+    compOpts =+      Regex.defaultCompOpt { Regex.lastStarGreedy = True }+    execOpts =+      Regex.defaultExecOpt { Regex.captureGroups = False }+    regex = Regex.makeRegexOpts compOpts execOpts (unpack regexSource)+  in+    Regex.matchTest regex . Seq.fromList . unpack++findUnitTests :: Text -> ([SolcContract] -> [(Text, [(Test, [AbiType])])])+findUnitTests match =   concatMap $ \c ->     case preview (abiMap . ix unitTestMarkerAbi) c of       Nothing -> []       Just _  ->-        let testNames = unitTestMethodsFiltered matcher c-        in ([(view contractName c, testNames) | not (null testNames)])+        let testNames = unitTestMethodsFiltered (regexMatches match) c+        in [(view contractName c, testNames) | not (null testNames)] -unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [(Text, [AbiType])])-unitTestMethodsFiltered matcher c = filter (matcher . fst) $ unitTestMethods c+unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [(Test, [AbiType])])+unitTestMethodsFiltered matcher c =+  let+    testName method = (view contractName c) <> "." <> (extractSig (fst method))+  in+    filter (matcher . testName) (unitTestMethods c) -unitTestMethods :: SolcContract -> [(Text, [AbiType])]-unitTestMethods = view abiMap-                  >>> Map.elems-                  >>> map (\f -> (view methodSignature f,-                                  snd <$> view methodInputs f))+unitTestMethods :: SolcContract -> [(Test, [AbiType])]+unitTestMethods =+  view abiMap+  >>> Map.elems+  >>> map (\f -> (mkTest $ view methodSignature f, snd <$> view methodInputs f))+  >>> filter (isJust . fst)+  >>> fmap (first fromJust) +extractSig :: Test -> Text+extractSig (ConcreteTest sig) = sig+extractSig (SymbolicTest sig) = sig+ traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap traceSrcMap dapp trace =   let@@ -97,9 +156,9 @@     Nothing ->       Nothing     Just (Creation, solc) ->-      preview (creationSrcmap . ix i) solc+      i >>= \i' -> preview (creationSrcmap . ix i') solc     Just (Runtime, solc) ->-      preview (runtimeSrcmap . ix i) solc+      i >>= \i' -> preview (runtimeSrcmap . ix i') solc  showTraceLocation :: DappInfo -> Trace -> Either Text Text showTraceLocation dapp trace =

@@ -15,7 +15,7 @@  import Text.PrettyPrint.ANSI.Leijen -data Mode = Debug | Run deriving (Eq, Show)+data Mode = Debug | Run | JsonTrace deriving (Eq, Show)  object :: [(Doc, Doc)] -> Doc object xs =@@ -101,34 +101,6 @@ --     Just x -> Just x --     Nothing -> --       vm ^? env . solcByCreationHash . ix hash---- currentSolc :: VM -> Maybe SolcContract--- currentSolc vm =---   let---     c = vm ^?! env . contracts . ix (vm ^. state . contract)---     theCodehash = view codehash c---   in---     case vm ^? env . solcByRuntimeHash . ix theCodehash of---         Just x ->---           Just x---         Nothing ->---           vm ^? env . solcByCreationHash . ix theCodehash---- currentSrcMap :: VM -> Maybe SrcMap--- currentSrcMap vm =---   let---     c = vm ^?! env . contracts . ix (vm ^. state . contract)---     theOpIx = (c ^. opIxMap) Vector.! (vm ^. state . pc)---     theCodehash = view codehash c---     (isRuntime, solc) =---       case vm ^? env . solcByRuntimeHash . ix theCodehash of---         Just x ->---           (True, Just x)---         Nothing ->---           (False, vm ^? env . solcByCreationHash . ix theCodehash)---     srcmapLens = if isRuntime then runtimeSrcmap else creationSrcmap---   in---     join (fmap (preview (srcmapLens . ix theOpIx)) solc)  srcMapCodePos :: SourceCache -> SrcMap -> Maybe (Text, Int) srcMapCodePos cache sm =

@@ -1,11 +1,17 @@+{-# LANGUAGE DeriveAnyClass #-} module EVM.Dev where  import System.Directory +import Prelude hiding (Word)++import EVM.Types import EVM.Dapp import EVM.Solidity import EVM.UnitTest+import EVM.Symbolic +import EVM hiding (path) import qualified EVM.Fetch import qualified EVM.TTY import qualified EVM.Emacs@@ -14,31 +20,37 @@ import qualified EVM.Stepper import qualified EVM.VMTest    as VMTest +import Data.SBV hiding (Word)+import qualified Data.Aeson           as JSON+import Options.Generic+import Data.SBV.Trans.Control import Control.Monad.State.Strict (execStateT)-import Data.Text (isPrefixOf)  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+import qualified Data.ByteString      as BS+import qualified Data.ByteString.Lazy.Char8 as B+import qualified Control.Monad.State.Class as State+import Control.Monad.State.Strict (runState, liftIO, StateT, get)+import Control.Lens hiding (op, passing)+import Control.Monad.Operational (ProgramViewT(..), ProgramView)+import qualified Control.Monad.Operational as Operational  loadDappInfo :: String -> String -> IO DappInfo loadDappInfo path file =   withCurrentDirectory path $     readSolc file >>=       \case-        Just (contractMap, cache) ->-          pure (dappInfo "." contractMap cache)+        Just (contractMap, sourcecache) ->+          pure (dappInfo "." contractMap sourcecache)         _ ->           error "nope, sorry"  ghciTest :: String -> String -> Maybe String -> IO [Bool]-ghciTest root path state =+ghciTest root path statePath =   withCurrentDirectory root $ do     loadFacts <--      case state of+      case statePath of         Nothing ->           pure id         Just repoPath -> do@@ -50,17 +62,21 @@         { oracle = EVM.Fetch.zero         , verbose = Nothing         , maxIter = Nothing+        , smtTimeout = Nothing+        , smtState = Nothing+        , solver = Nothing         , match = ""         , fuzzRuns = 100         , replay = Nothing         , vmModifier = loadFacts+        , dapp = emptyDapp         , testParams = params         }     readSolc path >>=       \case-        Just (contractMap, cache) -> do-          let unitTests = findUnitTests ("test" `isPrefixOf`) (Map.elems contractMap)-          results <- concatMapM (runUnitTestContract opts contractMap cache) unitTests+        Just (contractMap, _) -> do+          let unitTests = findAllUnitTests (Map.elems contractMap)+          results <- runSMT $ query $ concatMapM (runUnitTestContract opts contractMap) unitTests           let (passing, _) = unzip results           pure passing @@ -71,9 +87,9 @@ runBCTest (name, x) = do   let vm0 = VMTest.vmForCase x   putStr (name ++ " ")-  result <--      execStateT (EVM.Stepper.interpret EVM.Fetch.zero EVM.Stepper.execFully) vm0-  ok <- VMTest.checkExpectation False x result+  out <-+    execStateT (EVM.Stepper.interpret EVM.Fetch.zero EVM.Stepper.execFully) vm0+  ok <- VMTest.checkExpectation False x out   putStrLn (if ok then "ok" else "")   return ok @@ -88,10 +104,10 @@         mapM_ runBCTest (Map.toList allTests)  ghciTty :: String -> String -> Maybe String -> IO ()-ghciTty root path state =+ghciTty root path statePath =   withCurrentDirectory root $ do     loadFacts <--      case state of+      case statePath of         Nothing ->           pure id         Just repoPath -> do@@ -102,10 +118,15 @@       testOpts = UnitTestOptions         { oracle = EVM.Fetch.zero         , verbose = Nothing+        , maxIter = Nothing+        , smtTimeout = Nothing+        , smtState = Nothing+        , solver = Nothing         , match = ""         , fuzzRuns = 100         , replay = Nothing         , vmModifier = loadFacts+        , dapp = emptyDapp         , testParams = params         }     EVM.TTY.main testOpts root path@@ -116,3 +137,110 @@  foo :: IO () foo = ghciEmacs++data VMTrace =+  VMTrace+  { pc      :: Int+  , op      :: Int+  , stack   :: [Word]+  , memSize :: Int+  , depth   :: Int+  , gas     :: Word+  } deriving (Generic, JSON.ToJSON)++data VMTraceResult =+  VMTraceResult+  { output  :: String+  , gasUsed :: Word+  } deriving (Generic, JSON.ToJSON)++getOp :: VM -> Word8+getOp vm =+  if BS.length (view (state . code) vm) <= view (state . EVM.pc) vm+  then 0+  else fromIntegral $ BS.index (view (state . code) vm) (view (state . EVM.pc) vm)+++vmtrace :: VM -> VMTrace+vmtrace vm =+  let+    -- Convenience function to access parts of the current VM state.+    -- Arcane type signature needed to avoid monomorphism restriction.+    the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a+    the f g = view (f . g) vm+    memsize = the state memorySize+  in VMTrace { pc = the state EVM.pc+             , op = num $ getOp vm+             , gas = the state EVM.gas+             , memSize = memsize+             -- increment to match geth format+             , depth = 1 + length (view frames vm)+             -- reverse to match geth format+             , stack = reverse $ forceLit <$> the state EVM.stack+             }++vmres :: VM -> VMTraceResult+vmres vm =+  let+    gasUsed' = view (tx . txgaslimit) vm - view (state . EVM.gas) vm+    res = case view result vm of+      Just (VMSuccess out) -> forceBuffer out+      Just (VMFailure (Revert out)) -> out+      _ -> mempty+  in VMTraceResult+     -- more oddities to comply with geth+     { output = drop 2 $ show $ ByteStringS res+     , gasUsed = gasUsed'+     }++interpretWithTrace :: EVM.Fetch.Fetcher -> EVM.Stepper.Stepper a -> StateT VM IO a+interpretWithTrace fetcher =+  eval . Operational.view++  where+    eval+      :: ProgramView EVM.Stepper.Action a+      -> StateT VM IO a++    eval (Return x) = do+      vm <- get+      liftIO $ B.putStrLn $ JSON.encode $ vmres vm+      pure x++    eval (action :>>= k) = do+      vm <- get+      case action of+        EVM.Stepper.Run -> do+          -- Have we reached the final result of this action?+          use result >>= \case+            Just _ -> do+              -- Yes, proceed with the next action.+              interpretWithTrace fetcher (k vm)+            Nothing -> do+              liftIO $ B.putStrLn $ JSON.encode $ vmtrace vm++              -- No, keep performing the current action+              State.state (runState exec1)+              interpretWithTrace fetcher (EVM.Stepper.run >>= k)++        -- Stepper wants to keep executing?+        EVM.Stepper.Exec -> do+          -- Have we reached the final result of this action?+          use result >>= \case+            Just r -> do+              -- Yes, proceed with the next action.+              interpretWithTrace fetcher (k r)+            Nothing -> do+              liftIO $ B.putStrLn $ JSON.encode $ vmtrace vm++              -- No, keep performing the current action+              State.state (runState exec1)+              interpretWithTrace fetcher (EVM.Stepper.exec >>= k)+        EVM.Stepper.Wait q ->+          do m <- liftIO (fetcher q)+             State.state (runState m) >> interpretWithTrace fetcher (k ())+        EVM.Stepper.Ask _ ->+          error "cannot make choices with this interpretWithTraceer"+        EVM.Stepper.EVM m -> do+          r <- State.state (runState m)+          interpretWithTrace fetcher (k r)

@@ -21,7 +21,6 @@ import Data.SBV hiding (Word, output) import EVM import EVM.ABI-import EVM.Concrete import EVM.Symbolic import EVM.Dapp import EVM.Debug (srcMapCodePos)@@ -86,10 +85,8 @@      eval (action Operational.:>>= k) =       case action of-         -- Stepper wants to keep executing?         Stepper.Exec -> do-           let             -- When pausing during exec, we should later restart             -- the exec with the same continuation.@@ -420,7 +417,7 @@   sexp = id  instance SDisplay Storage where-  sexp (Symbolic _) = error "idk"+  sexp (Symbolic _ _) = error "idk"   sexp (Concrete d) = sexp d  instance SDisplay VM where@@ -521,10 +518,14 @@     { oracle            = Fetch.zero     , verbose           = Nothing     , maxIter           = Nothing+    , smtTimeout        = Nothing+    , smtState          = Nothing+    , solver            = Nothing     , match             = ""     , fuzzRuns          = 100     , replay            = Nothing     , vmModifier        = id+    , dapp              = emptyDapp     , testParams        = params     } @@ -538,13 +539,14 @@     script = do       Stepper.evm . pushTrace . EntryTrace $         "test " <> testName <> " (" <> contractPath <> ")"-      initializeUnitTest opts+      initializeUnitTest opts testContract       void (runUnitTest opts testName (AbiTuple mempty))     ui0 =       UiVmState         { _uiVm             = vm0         , _uiVmNextStep     = script         , _uiVmSolc         = Just testContract+        , _uiVmDapp         = Nothing         , _uiVmStepCount    = 0         , _uiVmFirstState   = undefined         , _uiVmFetcher      = oracle

@@ -36,10 +36,9 @@   ) where  import EVM          (VM, Contract, Cache)-import EVM.Concrete (Word)-import EVM.Symbolic (litWord, SymWord, forceLit)+import EVM.Symbolic (litWord, forceLit) import EVM          (balance, nonce, storage, bytecode, env, contracts, contract, state, cache, fetched)-import EVM.Types    (Addr)+import EVM.Types    (Addr, Word, SymWord)  import qualified EVM @@ -121,7 +120,7 @@  storageFacts :: Addr -> Contract -> [Fact] storageFacts a x = case view storage x of-  EVM.Symbolic _ -> []+  EVM.Symbolic _ _ -> []   EVM.Concrete s -> map f (Map.toList s)   where     f :: (Word, SymWord) -> Fact

@@ -6,10 +6,9 @@  import Prelude hiding (Word) -import EVM.Types    (Addr, W256, hexText)-import EVM.Concrete (Word, w256)+import EVM.Types    (Addr, w256, W256, hexText, Word) import EVM.Symbolic (litWord)-import EVM          (EVM, Contract, Block, StorageModel, initialContract, nonce, balance, external)+import EVM          (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external) import qualified EVM.FeeSchedule as FeeSchedule  import qualified EVM@@ -79,31 +78,31 @@   x <- case q of     QueryCode addr -> do         m <- f (rpc "eth_getCode" [toRPC addr, toRPC n])-        return $ hexText <$> view _String <$> m+        return $ hexText . view _String <$> m     QueryNonce addr -> do         m <- f (rpc "eth_getTransactionCount" [toRPC addr, toRPC n])-        return $ readText <$> view _String <$> m+        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+        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+        return $ readText . view _String <$> m     QueryChainId -> do         m <- f (rpc "eth_chainId" [toRPC n])-        return $ readText <$> view _String <$> m+        return $ readText . view _String <$> m   return x   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+parseBlock j = do+  coinbase   <- readText <$> j ^? key "miner" . _String+  timestamp  <- litWord . readText <$> j ^? key "timestamp" . _String+  number     <- readText <$> j ^? key "number" . _String+  difficulty <- readText <$> j ^? key "difficulty" . _String   -- default codesize, default gas limit, default feescedule   return $ EVM.Block coinbase timestamp number difficulty 0xffffffff 0xffffffff FeeSchedule.istanbul @@ -156,11 +155,14 @@     (\s -> fetchSlotWithSession n url s addr slot)  http :: BlockNumber -> Text -> Fetcher-http n url = oracle Nothing (Just (n, url)) EVM.ConcreteS True+http n url = oracle Nothing (Just (n, url)) True +zero :: Fetcher+zero = oracle Nothing Nothing True+ -- smtsolving + (http or zero)-oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> StorageModel -> Bool -> Fetcher-oracle smtstate info model ensureConsistency q = do+oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher+oracle smtstate info ensureConsistency q = do   case q of     EVM.PleaseAskSMT branchcondition pathconditions continue ->       case smtstate of@@ -172,7 +174,7 @@      -- if we are using a symbolic storage model,     -- we generate a new array to the fetched contract here-    EVM.PleaseFetchContract addr continue -> do+    EVM.PleaseFetchContract addr model continue -> do       contract <- case info of                     Nothing -> return $ Just $ initialContract (EVM.RuntimeCode mempty)                     Just (n, url) -> fetchContractFrom n url addr@@ -180,19 +182,35 @@         Just x -> case model of           EVM.ConcreteS -> return $ continue x           EVM.InitialS  -> return $ continue $ x-             & set EVM.storage (EVM.Symbolic $ SBV.sListArray 0 [])+             & 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 []))+                               & 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)+                  & 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+    EVM.PleaseMakeUnique val pathconditions continue ->+          case smtstate of+            Nothing -> return $ continue Multiple+            Just state -> flip runReaderT state $ SBV.runQueryT $ do+              constrain $ sAnd $ pathconditions <> [val .== val] -- dummy proposition just to make sure `val` is defined when we do `getValue` later.+              checkSat >>= \case+                Sat -> do+                  val' <- getValue val+                  s    <- checksat (val ./= literal val')+                  case s of+                    Unsat -> pure $ continue $ Unique val'+                    _ -> pure $ continue Multiple+                Unsat -> pure $ continue InconsistentU+                Unk -> pure $ continue TimeoutU+                DSat _ -> error "unexpected DSAT"++     EVM.PleaseFetchSlot addr slot continue ->       case info of         Nothing -> return (continue 0)@@ -202,9 +220,6 @@            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@@ -235,8 +250,10 @@                Sat -> return EVM.Unknown                -- Explore both branches in case of timeout                Unk -> return EVM.Unknown+               DSat _ -> error "checkBranch: unexpected SMT result"      -- If the query times out, we simply explore both paths      Unk -> return EVM.Unknown+     DSat _ -> error "checkBranch: unexpected SMT result"  checkBranch pathconds branchcondition True = do   constrain pathconds@@ -250,6 +267,7 @@                 Sat -> return $ EVM.Case False                 -- Assume the negated condition is still possible.                 Unk -> return $ EVM.Case False+                DSat _ -> error "checkBranch: unexpected SMT result"      -- Sat means its possible for condition to hold      Sat -> -- is its negation also possible?             checksat (sNot branchcondition) >>= \case@@ -259,6 +277,8 @@                Sat -> return EVM.Unknown                -- Explore both branches in case of timeout                Unk -> return EVM.Unknown+               DSat _ -> error "checkBranch: unexpected SMT result"       -- If the query times out, we simply explore both paths      Unk -> return EVM.Unknown+     DSat _ -> error "Internal Error: unexpected SMT result"

@@ -50,6 +50,13 @@ -- Define an alias for FGL graphs with text nodes and unlabeled edges. type FileGraph = Fgl.Gr Text () +-- | Get field either inside 'attributes' object (combined-json format)+-- or directly.+getAttribute :: Text -> Value -> Maybe Value+getAttribute s v = case preview (key "attributes" . key s) v of+  Nothing -> preview (key s) v+  Just r  -> Just r+ -- Given the AST of a source file, resolve all its imported paths. importsFrom :: Value -> [Text] importsFrom ast =@@ -63,11 +70,14 @@     -- and if so, return its resolved import path.     resolveImport :: Value -> Maybe Text     resolveImport node =-      case preview (key "name") node of-        Just (String "ImportDirective") ->-          preview (key "attributes" . key "absolutePath" . _String) node+      case preview (key "nodeType") node of+        Just (String "ImportDirective") -> view _String <$> getAttribute "absolutePath" node         _ ->-          Nothing+          case preview (key "name") node of+            Just (String "ImportDirective") ->+              view _String <$> getAttribute "absolutePath" node+            _ ->+              Nothing    -- Now we just try to resolve import paths at all subnodes.   in mapMaybe resolveImport allNodes@@ -112,10 +122,10 @@       Map.fromList         $ indexed [ x | x <- xs, (snd x) `elem` xs' ]       where-        xs = mconcat $ fmap f $ Map.elems asts+        xs = concatMap f $ Map.elems asts         xs' = repeated $ fmap snd xs-        scope = preview (key "attributes" . key "scope" . _Integer)-        name = preview (key "attributes" . key "name" . _String)+        scope x = getAttribute "scope" x >>= preview _Integer+        name x = getAttribute "name" x >>= preview _String         id' = preview (key "id" . _Integer)         p x = (nodeIs "ContractDefinition" x || nodeIs "StructDefinition" x)           && (fromJust' "no contract/struct scope" $ scope x) `elem` topScopeIds@@ -130,11 +140,11 @@     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)+        scope x = getAttribute "scope" x >>= preview _Integer+        cname x = getAttribute "canonicalName" x >>= preview _String         id' = preview (key "id" . _Integer)         p x = (nodeIs "StructDefinition" x)-          && (fromJust' "line:137 nested struct" $ scope x) `Map.member` contractsAndStructsToRename+          && (fromJust' "nested struct" $ scope x) `Map.member` contractsAndStructsToRename         f ast =           [ let               id'' = fromJust' "no id for nested struct" $ id' node@@ -194,8 +204,8 @@       putStrLn (unpack pragma)       BS.putStr (mconcat sources) --- Construct a new Solidity version pragma for the highest mentioned version--- given a list of source file ASTs.+-- | 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@@ -218,10 +228,8 @@    where     isVersionPragma :: [Value] -> Bool-    isVersionPragma =-      \case-        String "solidity" : _ -> True-        _ -> False+    isVersionPragma (String "solidity" : _) = True+    isVersionPragma _ = False      pragmaComponents :: Value -> [[Value]]     pragmaComponents ast = components@@ -230,8 +238,9 @@         ps = filter (nodeIs "PragmaDirective") (universe ast)          components :: [[Value]]-        components = catMaybes $ fmap-          ((fmap toList) . preview (key "attributes" . key "literals" . _Array))+        components = catMaybes $+          fmap+          ((fmap toList) . (\x -> getAttribute "literals" x >>= preview _Array))           ps      -- Simple way to combine many SemVer ranges.  We don't actually@@ -272,6 +281,7 @@       isJust (preview (key "src") x)     hasRightName =       Just t == preview (key "name" . _String) x+      || Just t == preview (key "nodeType" . _String) x  stripImportsAndPragmas :: (ByteString, Int) -> Value -> (ByteString, Int) stripImportsAndPragmas bso ast = stripAstNodes bso ast p@@ -305,8 +315,8 @@ prefixContractAst castr cs bso ast = prefixAstNodes   where     bs = fst bso-    refDec = preview (key "attributes" . key "referencedDeclaration" . _Integer)-    name = preview (key "attributes" . key "name" . _String)+    refDec x = getAttribute "referencedDeclaration" x >>= preview _Integer+    name x = getAttribute "name" x >>= preview _String     id' = preview (key "id" . _Integer)      -- Is node top level defined type (contract/interface/struct)@@ -316,7 +326,7 @@     -- 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+        && (isJust $ refDec 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@@ -362,10 +372,8 @@        where         (start, end) = sourceRange v-        x :: Maybe (Int, Integer)-        x = case preview (key "name" . _String) v of-          Just t-            | t `elem` ["ContractDefinition", "StructDefinition"] ->+        f :: Text -> Maybe (Int, Integer)+        f t | t `elem` ["ContractDefinition", "StructDefinition"] =               let                 name' = encodeUtf8 $ fromJust' "no name for contract/struct" $ name v                 bs' = snd $ BS.splitAt (start + snd bso) bs@@ -374,12 +382,18 @@                   + (BS.length name')               in                 fmap ((,) pos) $ id' v-            | t `elem` ["UserDefinedTypeName", "Identifier"] ->+            | t `elem` ["UserDefinedTypeName", "Identifier"] =               fmap ((,) end) $ refDec v-            | otherwise ->+            | otherwise =+                error $ "internal error: not a contract reference: " ++ show t++        x :: Maybe (Int, Integer)+        x = case preview (key "nodeType" . _String) v of+          Just t -> f t+          Nothing -> case preview (key "name" . _String) v of+            Just t -> f t+            Nothing ->               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.

@@ -1,24 +1,29 @@ {-# Language DataKinds #-}-{-# LANGUAGE OverloadedStrings #-}+{-# Language ImplicitParams #-}+{-# Language TemplateHaskell #-} module EVM.Format where  import Prelude hiding (Word)--import EVM (VM, cheatCode, traceForest, traceData, Error (..))-import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..))-import EVM.Dapp (DappInfo, dappSolcByHash, dappSolcByName, showTraceLocation, dappEventMap)-import EVM.Concrete (Word (..), wordValue)-import EVM.Symbolic (maybeLitWord, len)-import EVM.Types (W256 (..), num, Buffer(..))+import qualified EVM+import EVM.Dapp (DappInfo (..), dappSolcByHash, dappAbiMap, showTraceLocation, dappEventMap)+import EVM.Dapp (DappContext (..), contextInfo, contextEnv)+import EVM.Concrete ( wordValue )+import EVM (VM, VMResult(..), cheatCode, traceForest, traceData, Error (..), result)+import EVM (Trace, TraceData (..), Log (..), Query (..), FrameContext (..), Storage(..))+import EVM.SymExec+import EVM.Symbolic (len, litWord)+import EVM.Types (maybeLitWord, Word (..), Whiff(..), SymWord(..), W256 (..), num)+import EVM.Types (Addr, Buffer(..), ByteStringS(..)) 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.ABI (Indexed (NotIndexed), getAbiSeq)+import EVM.ABI (parseTypeName, formatString)+import EVM.Solidity (SolcContract(..), contractName, abiMap) import EVM.Solidity (methodOutput, methodSignature, methodName)  import Control.Arrow ((>>>))-import Control.Lens (view, preview, ix, _2, to, _Just)+import Control.Lens (view, preview, ix, _2, to, makeLenses, over, each, (^?!)) import Data.Binary.Get (runGetOrFail)+import Data.Bits       (shiftR) import Data.ByteString (ByteString) import Data.ByteString.Builder (byteStringHex, toLazyByteString) import Data.ByteString.Lazy (toStrict, fromStrict)@@ -29,10 +34,10 @@ import Data.Text (Text, pack, unpack, intercalate) import Data.Text (dropEnd, splitOn) import Data.Text.Encoding (decodeUtf8, decodeUtf8')+import Data.Tree (Tree (Node)) import Data.Tree.View (showTree)-import Data.Vector (Vector, fromList)--import Numeric (showHex)+import Data.Vector (Vector)+import Data.Word (Word32)  import qualified Data.ByteString as BS import qualified Data.Char as Char@@ -61,13 +66,9 @@ 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 <> "\")"+  case Map.lookup (fromIntegral w) (view dappAbiMap dapp) of+    Nothing -> showDec Unsigned w+    Just x  -> "keccak(\"" <> view methodSignature x <> "\")"  humanizeInteger :: (Num a, Integral a, Show a) => a -> Text humanizeInteger =@@ -79,64 +80,82 @@   . Text.pack   . show --- TODO: make polymorphic-showAbiValues :: Vector AbiValue -> Text-showAbiValues vs =-  "(" <> intercalate ", " (toList (fmap showAbiValue vs)) <> ")"+showAbiValue :: (?context :: DappContext) => AbiValue -> Text+showAbiValue (AbiBytes _ bs) =+  formatBytes bs  -- opportunistically decodes recognisable strings+showAbiValue (AbiAddress addr) =+  let dappinfo = view contextInfo ?context+      contracts = view (contextEnv . EVM.contracts) ?context+      name = case (Map.lookup addr contracts) of+        Nothing -> ""+        Just contract ->+          let hash = view EVM.codehash contract+              solcContract = (preview (dappSolcByHash . ix hash . _2) dappinfo)+          in maybeContractName' solcContract+  in+    name <> "@" <> (pack $ show addr)+showAbiValue v = pack $ show v -showAbiArray :: Vector AbiValue -> Text-showAbiArray vs =-  "[" <> intercalate ", " (toList (fmap showAbiValue vs)) <> "]"+showAbiValues :: (?context :: DappContext) => Vector AbiValue -> Text+showAbiValues vs = parenthesise (textAbiValues vs) -showAbiValue :: AbiValue -> Text-showAbiValue (AbiUInt _ w) =-  pack $ show w-showAbiValue (AbiInt _ w) =-  pack $ show w-showAbiValue (AbiBool b) =-  pack $ show b-showAbiValue (AbiAddress w160) =-  pack $ "0x" ++ (showHex w160 "")-showAbiValue (AbiBytes _ bs) =-  formatBytes bs-showAbiValue (AbiBytesDynamic bs) =-  formatBinary bs-showAbiValue (AbiString bs) =-  formatQString bs-showAbiValue (AbiArray _ _ xs) =-  showAbiArray xs-showAbiValue (AbiArrayDynamic _ xs) =-  showAbiArray xs-showAbiValue (AbiTuple v) =-  showAbiValues v+textAbiValues :: (?context :: DappContext) => Vector AbiValue -> [Text]+textAbiValues vs = toList (fmap showAbiValue vs) +textValues :: (?context :: DappContext) => [AbiType] -> Buffer -> [Text]+textValues ts (SymbolicBuffer  _) = [pack $ show t | t <- ts]+textValues ts (ConcreteBuffer bs) =+  case runGetOrFail (getAbiSeq (length ts) ts) (fromStrict bs) of+    Right (_, _, xs) -> textAbiValues xs+    Left (_, _, _)   -> [formatBinary bs]++parenthesise :: [Text] -> Text+parenthesise ts = "(" <> intercalate ", " ts <> ")"++showValues :: (?context :: DappContext) => [AbiType] -> Buffer -> Text+showValues ts b = parenthesise $ textValues ts b++showValue :: (?context :: DappContext) => AbiType -> Buffer -> Text+showValue t b = head $ textValues [t] b++showCall :: (?context :: DappContext) => [AbiType] -> Buffer -> Text+showCall ts (SymbolicBuffer bs) = showValues ts $ SymbolicBuffer (drop 4 bs)+showCall ts (ConcreteBuffer bs) = showValues ts $ ConcreteBuffer (BS.drop 4 bs)++showError :: (?context :: DappContext) => ByteString -> Text+showError bs = case BS.take 4 bs of+  -- Method ID for Error(string)+  "\b\195y\160" -> showCall [AbiStringType] (ConcreteBuffer bs)+  _             -> formatBinary bs+++-- the conditions under which bytes will be decoded and rendered as a string isPrintable :: ByteString -> Bool isPrintable =   decodeUtf8' >>>-    either (const False)-      (Text.all (not . Char.isControl))+    either+      (const False)+      (Text.all (\c-> Char.isPrint c && (not . Char.isControl) c))  formatBytes :: ByteString -> Text formatBytes b =   let (s, _) = BS.spanEnd (== 0) b   in     if isPrintable s-    then formatQString s+    then formatBString s     else formatBinary b  formatSBytes :: Buffer -> Text formatSBytes (SymbolicBuffer b) = "<" <> pack (show (length b)) <> " symbolic bytes>" formatSBytes (ConcreteBuffer b) = formatBytes b -formatQString :: ByteString -> Text-formatQString = pack . show--formatString :: ByteString -> Text-formatString bs = decodeUtf8 (fst (BS.spanEnd (== 0) bs))+-- a string that came from bytes, displayed with special quotes+formatBString :: ByteString -> Text+formatBString b = mconcat [ "«",  Text.dropAround (=='"') (pack $ formatString b), "»" ]  formatSString :: Buffer -> Text formatSString (SymbolicBuffer bs) = "<" <> pack (show (length bs)) <> " symbolic bytes (string)>"-formatSString (ConcreteBuffer bs) = formatString bs+formatSString (ConcreteBuffer bs) = pack $ formatString bs  formatBinary :: ByteString -> Text formatBinary =@@ -147,63 +166,93 @@ formatSBinary (ConcreteBuffer bs) = formatBinary bs  showTraceTree :: DappInfo -> VM -> Text-showTraceTree dapp =-  traceForest-    >>> fmap (fmap (unpack . showTrace dapp))-    >>> concatMap showTree-    >>> pack+showTraceTree dapp vm =+  let forest = traceForest vm+      traces = fmap (fmap (unpack . showTrace dapp vm)) forest+  in pack $ concatMap showTree traces -showTrace :: DappInfo -> Trace -> Text-showTrace dapp trace =-  let+unindexed :: [(AbiType, Indexed)] -> [AbiType]+unindexed ts = [t | (t, NotIndexed) <- ts]++showTrace :: DappInfo -> VM -> Trace -> Text+showTrace dapp vm trace =+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  in let     pos =       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)))+        Left x -> " \x1b[1m" <> x <> "\x1b[0m"+        Right x -> " \x1b[1m(" <> x <> ")\x1b[0m"+    fullAbiMap = view dappAbiMap dapp   in case view traceData trace of     EventTrace (Log _ bytes topics) ->-      case topics of-        [] ->-          mconcat+      let logn = mconcat             [ "\x1b[36m"-            , "log0("-            , formatSBinary bytes-            , ")"+            , "log" <> (pack (show (length topics)))+            , parenthesise ((map (pack . show) topics) ++ [formatSBinary bytes])             , "\x1b[0m"             ] <> pos-        (topic:_) ->-          let unknownTopic =                    -- todo: catch ds-note-                   mconcat-                     [ "\x1b[36m"-                     , "log" <> (pack (show (length topics))) <> "("-                     , formatSBinary bytes <> ", "-                     , intercalate ", " (map (pack . show) topics) <> ")"-                     , "\x1b[0m"-                     ] <> pos--          in case maybeLitWord topic of-            Just top -> case Map.lookup (wordValue top) (view dappEventMap dapp) of-                 Just (Event name _ types) ->-                   mconcat-                     [ "\x1b[36m"-                     , name-                     , showValues [t | (t, NotIndexed) <- types] bytes-                     -- todo: show indexed-                     , "\x1b[0m"-                     ] <> pos-                 Nothing -> unknownTopic-            Nothing -> unknownTopic+          knownTopic name types = mconcat+            [ "\x1b[36m"+            , name+            , showValues (unindexed types) bytes+            -- todo: show indexed+            , "\x1b[0m"+            ] <> pos+          lognote sig usr = mconcat+            [ "\x1b[36m"+            , "LogNote"+            , parenthesise [sig, usr, "..."]+            , "\x1b[0m"+            ] <> pos+      in case topics of+        [] ->+          logn+        (t1:_) ->+          case maybeLitWord t1 of+            Just topic ->+              case Map.lookup (wordValue topic) (view dappEventMap dapp) of+                Just (Event name _ types) ->+                  knownTopic name types+                Nothing ->+                  case topics of+                    [_, t2, _, _] ->+                      -- check for ds-note logs.. possibly catching false positives+                      -- event LogNote(+                      --     bytes4   indexed  sig,+                      --     address  indexed  usr,+                      --     bytes32  indexed  arg1,+                      --     bytes32  indexed  arg2,+                      --     bytes             data+                      -- ) anonymous;+                      let+                        sig = fromIntegral $ shiftR (wordValue topic) 224 :: Word32+                        usr = case maybeLitWord t2 of+                          Just w ->+                            pack $ show $ (fromIntegral w :: Addr)+                          Nothing  ->+                            "<symbolic>"+                      in+                        case Map.lookup sig (view dappAbiMap dapp) of+                          Just m ->+                           lognote (view methodSignature m) usr+                          Nothing ->+                            logn+                    _ ->+                      logn+            Nothing ->+              logn      QueryTrace q ->       case q of-        PleaseFetchContract addr _ ->+        PleaseFetchContract addr _ _ ->           "fetch contract " <> pack (show addr) <> pos         PleaseFetchSlot addr slot _ ->           "fetch storage slot " <> pack (show slot) <> " from " <> pack (show addr) <> pos         PleaseAskSMT _ _ _ ->           "ask smt" <> pos+        PleaseMakeUnique _ _ _ ->+          "make unique value" <> pos+     ErrorTrace e ->       case e of         Revert out ->@@ -211,21 +260,17 @@         _ ->           "\x1b[91merror\x1b[0m " <> pack (show e) <> pos -    ReturnTrace out (CallContext _ _ _ _ hash (Just abi) _ _ _) ->-      case getAbiMethodOutput dapp hash abi of-        Nothing ->-          "← " <>-            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 ->+    ReturnTrace out (CallContext _ _ _ _ _ (Just abi) _ _ _) ->+      "← " <>+        case Map.lookup (fromIntegral abi) fullAbiMap of+          Just m  ->+            case unzip (view methodOutput m) of+              ([], []) ->                 formatSBinary out-        Just (_, t) ->-          "← " <> pack (show t) <> " " <> showValue t out+              (_, ts) ->+                showValues ts out+          Nothing ->+            formatSBinary out     ReturnTrace out (CallContext {}) ->       "← " <> formatSBinary out     ReturnTrace out (CreationContext {}) ->@@ -233,8 +278,11 @@      EntryTrace t ->       t-    FrameTrace (CreationContext hash _ _ ) ->-      "create " <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp) <> pos+    FrameTrace (CreationContext addr hash _ _ ) ->+      "create "+      <> maybeContractName (preview (dappSolcByHash . ix hash . _2) dapp)+      <> "@" <> pack (show addr)+      <> pos     FrameTrace (CallContext target context _ _ hash abi calldata _ _) ->       let calltype = if target == context                      then "call "@@ -246,7 +294,9 @@             <> pack "::"             <> case Map.lookup (fromIntegral (fromMaybe 0x00 abi)) fullAbiMap of                  Just m  ->-                   view methodName m+                   "\x1b[1m"+                   <> view methodName m+                   <> "\x1b[0m"                    <> showCall (catMaybes (getAbiTypes (view methodSignature m))) calldata                  Nothing ->                    formatSBinary calldata@@ -266,16 +316,6 @@             <> "\x1b[0m"             <> pos -getAbiMethodOutput-  :: DappInfo -> W256 -> Word -> Maybe (Text, AbiType)-getAbiMethodOutput dapp hash abi =-  -- Some typical ugly lens code. :'(-  preview-    ( dappSolcByHash . ix hash . _2 . abiMap-    . ix (fromIntegral abi) . methodOutput . _Just-    )-    dapp- getAbiTypes :: Text -> [Maybe AbiType] getAbiTypes abi = map (parseTypeName mempty) types   where@@ -283,34 +323,14 @@       filter (/= "") $         splitOn "," (dropEnd 1 (last (splitOn "(" abi))) -showCall :: [AbiType] -> Buffer -> Text-showCall ts (SymbolicBuffer bs) = showValues ts $ SymbolicBuffer (drop 4 bs)-showCall ts (ConcreteBuffer bs) = showValues ts $ ConcreteBuffer (BS.drop 4 bs)--showError :: ByteString -> Text-showError bs = case BS.take 4 bs of-  -- Method ID for Error(string)-  "\b\195y\160" -> showCall [AbiStringType] (ConcreteBuffer bs)-  _             -> formatBinary bs--showValues :: [AbiType] -> Buffer -> Text-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-    Left (_, _, _)   -> formatBinary bs--showValue :: AbiType -> Buffer -> Text-showValue t (SymbolicBuffer _) = "symbolic: " <> (pack $ show t)-showValue t (ConcreteBuffer bs) =-  case runGetOrFail (getAbi t) (fromStrict bs) of-    Right (_, _, x) -> showAbiValue x-    Left (_, _, _)  -> formatBinary bs- maybeContractName :: Maybe SolcContract -> Text maybeContractName =   maybe "<unknown contract>" (view (contractName . to contractNamePart)) +maybeContractName' :: Maybe SolcContract -> Text+maybeContractName' =+  maybe "" (view (contractName . to contractNamePart))+ maybeAbiName :: SolcContract -> Word -> Maybe Text maybeAbiName solc abi = preview (abiMap . ix (fromIntegral abi) . methodSignature) solc @@ -319,3 +339,113 @@  contractPathPart :: Text -> Text contractPathPart x = Text.split (== ':') x !! 0++prettyvmresult :: (?context :: DappContext) => VMResult -> String+prettyvmresult (EVM.VMFailure (EVM.Revert ""))  = "Revert"+prettyvmresult (EVM.VMFailure (EVM.Revert msg)) = "Revert" ++ (unpack $ showError msg)+prettyvmresult (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) = "Assertion violation"+prettyvmresult (EVM.VMFailure err) = "Failed: " <> show err+prettyvmresult (EVM.VMSuccess (ConcreteBuffer msg)) =+  if BS.null msg+  then "Stop"+  else "Return: " <> show (ByteStringS msg)+prettyvmresult (EVM.VMSuccess (SymbolicBuffer msg)) =+  "Return: " <> show (length msg) <> " symbolic bytes"++currentSolc :: DappInfo -> VM -> Maybe SolcContract+currentSolc dapp vm =+  let+    this = vm ^?! EVM.env . EVM.contracts . ix (view (EVM.state . EVM.contract) vm)+    h = view EVM.codehash this+  in+    preview (dappSolcByHash . ix h . _2) dapp++-- TODO: display in an 'act' format++-- TreeLine describes a singe line of the tree+-- it contains the indentation which is prefixed to it+-- and its content which contains the rest+data TreeLine = TreeLine {+  _indent   :: String,+  _content  :: String+  }++makeLenses ''TreeLine++-- SHOW TREE++showTreeIndentSymbol :: Bool      -- ^ isLastChild+                     -> Bool      -- ^ isTreeHead+                     -> String+showTreeIndentSymbol True  True  = "\x2514" -- └+showTreeIndentSymbol False True  = "\x251c" -- ├+showTreeIndentSymbol True  False = " "+showTreeIndentSymbol False False = "\x2502" -- │++flattenTree :: Int -> -- total number of cases+               Int -> -- case index+               Tree [String] ->+               [TreeLine]+-- this case should never happen for our use case, here for generality+flattenTree _ _ (Node [] _)  = []++flattenTree totalCases i (Node (x:xs) cs) = let+  isLastCase       = i + 1 == totalCases+  indenthead       = showTreeIndentSymbol isLastCase True <> " " <> show i <> " "+  indentchild      = showTreeIndentSymbol isLastCase False <> " "+  in TreeLine indenthead x+  : ((TreeLine indentchild <$> xs) ++ over (each . indent) ((<>) indentchild) (flattenForest cs))++flattenForest :: [Tree [String]] -> [TreeLine]+flattenForest forest = concat $ zipWith (flattenTree (length forest)) [0..] forest++leftpad :: Int -> String -> String+leftpad n = (<>) $ replicate n ' '++showTree' :: Tree [String] -> String+showTree' (Node s []) = unlines s+showTree' (Node _ children) =+  let+    treeLines = flattenForest children+    maxIndent = 2 + maximum (length . _indent <$> treeLines)+    showTreeLine (TreeLine colIndent colContent) =+      let indentSize = maxIndent - length colIndent+      in colIndent <> leftpad indentSize colContent+  in unlines $ showTreeLine <$> treeLines+++-- RENDER TREE++showStorage :: [(SymWord, SymWord)] -> [String]+showStorage = fmap (\(k, v) -> show k <> " => " <> show v)++showLeafInfo :: DappInfo -> BranchInfo -> [String]+showLeafInfo srcInfo (BranchInfo vm _) = let+  ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env }+  in let+  self    = view (EVM.state . EVM.contract) vm+  updates = case view (EVM.env . EVM.contracts) vm ^?! ix self . EVM.storage of+    Symbolic v _ -> v+    Concrete x -> [(litWord k,v) | (k, v) <- Map.toList x]+  showResult = [prettyvmresult res | Just res <- [view result vm]]+  in showResult+  ++ showStorage updates+  ++ [""]++showBranchInfoWithAbi :: DappInfo -> BranchInfo -> [String]+showBranchInfoWithAbi _ (BranchInfo _ Nothing) = [""]+showBranchInfoWithAbi srcInfo (BranchInfo vm (Just y)) =+  case y of+    (IsZero (Eq (Literal x) _)) ->+      let+        abimap = view abiMap <$> currentSolc srcInfo vm+        method = abimap >>= Map.lookup (num x)+      in [maybe (show y) (show . view methodSignature) method]+    y' -> [show y']++renderTree :: (a -> [String])+           -> (a -> [String])+           -> Tree a+           -> Tree [String]+renderTree showBranch showLeaf (Node b []) = Node (showBranch b ++ showLeaf b) []+renderTree showBranch showLeaf (Node b cs) = Node (showBranch b) (renderTree showBranch showLeaf <$> cs)

@@ -1,38 +0,0 @@-module EVM.Keccak (keccak, abiKeccak) where--import EVM.Types--import Control.Arrow ((>>>))--import Data.Bits-import Data.ByteString (ByteString)--import qualified Data.ByteString as BS-import Data.Word--import Crypto.Hash-import qualified Data.ByteArray as BA--keccakBytes :: ByteString -> ByteString-keccakBytes =-  (hash :: ByteString -> Digest Keccak_256)-    >>> BA.unpack-    >>> BS.pack---word32 :: [Word8] -> Word32-word32 xs = sum [ fromIntegral x `shiftL` (8*n)-                | (n, x) <- zip [0..] (reverse xs) ]--keccak :: ByteString -> W256-keccak =-  keccakBytes-    >>> BS.take 32-    >>> word--abiKeccak :: ByteString -> Word32-abiKeccak =-  keccakBytes-    >>> BS.take 4-    >>> BS.unpack-    >>> word32

@@ -4,9 +4,8 @@  module EVM.Patricia where -import EVM.Keccak import EVM.RLP-import EVM.Types+import EVM.Types hiding (Literal)  import Control.Monad.Free import Control.Monad.State

@@ -21,6 +21,7 @@   , methodOutput   , abiMap   , eventMap+  , storageLayout   , contractName   , constructorInputs   , creationCode@@ -28,18 +29,21 @@   , makeSrcMaps   , readSolc   , readJSON+  , readStdJSON+  , readCombinedJSON   , runtimeCode-  , snippetCache   , runtimeCodehash   , creationCodehash   , runtimeSrcmap   , creationSrcmap-  , contractAst   , sourceFiles   , sourceLines   , sourceAsts   , stripBytecodeMetadata   , signature+  , solc+  , Language(..)+  , stdjson   , parseMethodInput   , lineSubrange   , astIdMap@@ -47,15 +51,16 @@ ) where  import EVM.ABI-import EVM.Keccak import EVM.Types  import Control.Applicative-import Control.Lens         hiding (Indexed)-import Data.Aeson           (Value (..))+import Control.Monad+import Control.Lens         hiding (Indexed, (.=))+import Data.Aeson           (Value (..), ToJSON(..), (.=), object, encode) import Data.Aeson.Lens import Data.Scientific import Data.ByteString      (ByteString)+import Data.ByteString.Lazy (toStrict) import Data.Char            (isDigit) import Data.Foldable import Data.Map.Strict      (Map)@@ -65,7 +70,7 @@ import Data.Semigroup import Data.Sequence        (Seq) import Data.Text            (Text, pack, intercalate)-import Data.Text.Encoding   (encodeUtf8)+import Data.Text.Encoding   (encodeUtf8, decodeUtf8) import Data.Text.IO         (readFile, writeFile) import Data.Vector          (Vector) import Data.Word@@ -82,13 +87,14 @@ import qualified Data.Map.Strict        as Map import qualified Data.Text              as Text import qualified Data.Vector            as Vector+import Data.List (sort)  data StorageItem = StorageItem {   _type   :: SlotType,   _offset :: Int,   _slot   :: Int   } deriving (Show, Eq)-  + data SlotType   -- Note that mapping keys can only be elementary;   -- that excludes arrays, contracts, and mappings.@@ -99,19 +105,15 @@  instance Show SlotType where  show (StorageValue t) = show t- show (StorageMapping (s NonEmpty.:| ss) t) =-      "mapping("-        <> show s-        <> " => "-        <> foldr-             (\x y ->-               "mapping("-                 <> show x-                 <> " => "-                 <> y-                 <> ")")-             (show t) ss-        <> ")"+ show (StorageMapping s t) =+   foldr+   (\x y ->+       "mapping("+       <> show x+       <> " => "+       <> y+       <> ")")+   (show t) s  instance Read SlotType where   readsPrec _ ('m':'a':'p':'p':'i':'n':'g':'(':s) =@@ -134,19 +136,17 @@   , _storageLayout    :: Maybe (Map Text StorageItem)   , _runtimeSrcmap    :: Seq SrcMap   , _creationSrcmap   :: Seq SrcMap-  , _contractAst      :: Value   } deriving (Show, Eq, Generic)  data Method = Method-  { _methodOutput :: Maybe (Text, AbiType)+  { _methodOutput :: [(Text, AbiType)]   , _methodInputs :: [(Text, AbiType)]   , _methodName :: Text   , _methodSignature :: Text   } deriving (Show, Eq, Ord, Generic)  data SourceCache = SourceCache-  { _snippetCache :: Map (Int, Int) ByteString-  , _sourceFiles  :: Map Int (Text, ByteString)+  { _sourceFiles  :: Map Int (Text, ByteString)   , _sourceLines  :: Map Int (Vector ByteString)   , _sourceAsts   :: Map Text Value   } deriving (Show, Eq, Generic)@@ -155,7 +155,7 @@   _ <> _ = error "lol"  instance Monoid SourceCache where-  mempty = SourceCache mempty mempty mempty mempty+  mempty = SourceCache mempty mempty mempty  data JumpType = JumpInto | JumpFrom | JumpRegular   deriving (Show, Eq, Ord, Generic)@@ -232,13 +232,14 @@      go c (xs, state, p)                      = (xs, error ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p) -makeSourceCache :: [Text] -> Map Text Value -> IO SourceCache+makeSourceCache :: [(Text, Maybe ByteString)] -> Map Text Value -> IO SourceCache makeSourceCache paths asts = do-  xs <- mapM (BS.readFile . Text.unpack) paths+  let f (_,  Just content) = return content+      f (fp, Nothing) = BS.readFile $ Text.unpack fp+  xs <- mapM f paths   return $! SourceCache-    { _snippetCache = mempty-    , _sourceFiles =-        Map.fromList (zip [0..] (zip paths xs))+    { _sourceFiles =+        Map.fromList (zip [0..] (zip (fst <$> paths) xs))     , _sourceLines =         Map.fromList (zip [0 .. length paths - 1]                        (map (Vector.fromList . BS.split 0xa) xs))@@ -270,43 +271,46 @@ solidity :: Text -> Text -> IO (Maybe ByteString) solidity contract src = do   (json, path) <- solidity' src-  let Just (solc, _, _) = readJSON json-  return (solc ^? ix (path <> ":" <> contract) . creationCode)+  let Just (sol, _, _) = readJSON json+  return (sol ^? ix (path <> ":" <> contract) . creationCode)  solcRuntime :: Text -> Text -> IO (Maybe ByteString) solcRuntime contract src = do   (json, path) <- solidity' src-  let Just (solc, _, _) = readJSON json-  return (solc ^? ix (path <> ":" <> contract) . runtimeCode)+  let Just (sol, _, _) = readJSON json+  return (sol ^? ix (path <> ":" <> contract) . runtimeCode)  functionAbi :: Text -> IO Method functionAbi f = do   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")-  let Just (solc, _, _) = readJSON json-  case Map.toList $ solc ^?! ix (path <> ":ABI") . abiMap of+  let Just (sol, _, _) = readJSON json+  case Map.toList $ sol ^?! ix (path <> ":ABI") . abiMap of      [(_,b)] -> return b      _ -> error "hevm internal error: unexpected abi format"  force :: String -> Maybe a -> a force s = fromMaybe (error s) -readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [Text])-readJSON json = do-  contracts <--    f <$> (json ^? key "contracts" . _Object)-      <*> (fmap (fmap (^. _String)) $ json ^? key "sourceList" . _Array)+readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])+readJSON json = case json ^? key "sourceList" of+  Nothing -> readStdJSON json+  _ -> readCombinedJSON json++readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])+readCombinedJSON json = do+  contracts <- f <$> (json ^? key "contracts" . _Object)   sources <- toList . fmap (view _String) <$> json ^? key "sourceList" . _Array-  return (contracts, Map.fromList (HMap.toList asts), sources)+  return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | x <- sources])   where     asts = fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" . _Object)-    f x y = Map.fromList . map (g y) . HMap.toList $ x-    g _ (s, x) =+    f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x+    g s x =       let         theRuntimeCode = toCode (x ^?! key "bin-runtime" . _String)         theCreationCode = toCode (x ^?! key "bin" . _String)         abis =           toList ((x ^?! key "abi" . _String) ^?! _Array)-      in (s, SolcContract {+      in SolcContract {         _runtimeCode      = theRuntimeCode,         _creationCode     = theCreationCode,         _runtimeCodehash  = keccak (stripBytecodeMetadata theRuntimeCode),@@ -314,72 +318,109 @@         _runtimeSrcmap    = force "internal error: srcmap-runtime" (makeSrcMaps (x ^?! key "srcmap-runtime" . _String)),         _creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (x ^?! key "srcmap" . _String)),         _contractName = s,-        _contractAst =-          fromMaybe-            (error "JSON lacks abstract syntax trees.")-            (preview (ix (head (Text.split (== ':') s)) . key "AST") asts),+        _constructorInputs = mkConstructor abis,+        _abiMap       = mkAbiMap abis,+        _eventMap     = mkEventMap abis,+        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String+      } -        _constructorInputs =-          let-            isConstructor y =-              "constructor" == y ^?! key "type" . _String-          in-            case filter isConstructor abis of-              [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" . _Array))-              [] -> [] -- default constructor has zero inputs-              _  -> error "strange: contract has multiple constructors",+readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])+readStdJSON json = do+  contracts <- json ^? key "contracts" ._Object+  -- TODO: support the general case of "urls" and "content" in the standard json+  sources <- json ^? key "sources" . _Object+  let asts = force "JSON lacks abstract syntax trees." . preview (key "ast") <$> sources+      contractMap = f contracts+      contents src = (src, encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))+  return (fst <$> contractMap, Map.fromList (HMap.toList asts), contents <$> (sort $ HMap.keys sources))+  where+    f :: (AsValue s) => HMap.HashMap Text s -> (Map Text (SolcContract, (HMap.HashMap Text Text)))+    f x = Map.fromList . (concatMap g) . HMap.toList $ x+    g (s, x) = h s <$> HMap.toList (view _Object x)+    h s (c, x) = +      let+        evmstuff = x ^?! key "evm"+        runtime = evmstuff ^?! key "deployedBytecode"+        creation =  evmstuff ^?! key "bytecode"+        theRuntimeCode = toCode $ runtime ^?! key "object" . _String+        theCreationCode = toCode $ creation ^?! key "object" . _String+        srcContents :: Maybe (HMap.HashMap Text Text)+        srcContents = do metadata <- x ^? key "metadata" . _String+                         srcs <- metadata ^? key "sources" . _Object+                         return $ (view (key "content" . _String)) <$> (HMap.filter (isJust . preview (key "content")) srcs)+        abis = force ("abi key not found in " <> show x) $+          toList <$> x ^? key "abi" . _Array+      in (s <> ":" <> c, (SolcContract {+        _runtimeCode      = theRuntimeCode,+        _creationCode     = theCreationCode,+        _runtimeCodehash  = keccak (stripBytecodeMetadata theRuntimeCode),+        _creationCodehash = keccak (stripBytecodeMetadata theCreationCode),+        _runtimeSrcmap    = force "internal error: srcmap-runtime" (makeSrcMaps (runtime ^?! key "sourceMap" . _String)),+        _creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (creation ^?! key "sourceMap" . _String)),+        _contractName = s <> ":" <> c,+        _constructorInputs = mkConstructor abis,+        _abiMap        = mkAbiMap abis,+        _eventMap      = mkEventMap abis,+        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String+      }, fromMaybe mempty srcContents)) -        _abiMap       = Map.fromList $-          let-            relevant =-              filter (\y -> "function" == y ^?! key "type" . _String) abis-          in flip map relevant $-            \abi -> (-              abiKeccak (encodeUtf8 (signature abi)),-              Method-                { _methodName = abi ^?! key "name" . _String-                , _methodSignature = signature abi-                , _methodInputs =-                    map parseMethodInput-                      (toList (abi ^?! key "inputs" . _Array))-                , _methodOutput =-                    fmap parseMethodInput-                      (abi ^? key "outputs" . _Array . ix 0)-                }-            ),-        _eventMap     = Map.fromList $-          flip map (filter (\y -> "event" == y ^?! key "type" . _String)-                     . toList $ (x ^?! key "abi" . _String) ^?! _Array) $-            \abi ->-              ( keccak (encodeUtf8 (signature abi))-              , Event-                  (abi ^?! key "name" . _String)-                  (case abi ^?! key "anonymous" . _Bool of-                     True -> Anonymous-                     False -> NotAnonymous)-                  (map (\y -> ( force "internal error: type" (parseTypeName' y)-                              , if y ^?! key "indexed" . _Bool-                                then Indexed-                                else NotIndexed ))-                    (toList $ abi ^?! key "inputs" . _Array))-              ),-         _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String-      })+mkAbiMap :: [Value] -> Map Word32 Method+mkAbiMap abis = Map.fromList $+  let+    relevant = filter (\y -> "function" == y ^?! key "type" . _String) abis+    f abi =+      (abiKeccak (encodeUtf8 (signature abi)),+       Method { _methodName = abi ^?! key "name" . _String+              , _methodSignature = signature abi+              , _methodInputs = map parseMethodInput+                 (toList (abi ^?! key "inputs" . _Array))+              , _methodOutput = map parseMethodInput+                 (toList (abi ^?! key "outputs" . _Array))+              })+  in f <$> relevant +mkEventMap :: [Value] -> Map W256 Event+mkEventMap abis = Map.fromList $+  let+    relevant = filter (\y -> "event" == y ^?! key "type" . _String) abis+    f abi =+     ( keccak (encodeUtf8 (signature abi))+     , Event+       (abi ^?! key "name" . _String)+       (case abi ^?! key "anonymous" . _Bool of+         True -> Anonymous+         False -> NotAnonymous)+       (map (\y -> ( force "internal error: type" (parseTypeName' y)+     , if y ^?! key "indexed" . _Bool+       then Indexed+       else NotIndexed ))+       (toList $ abi ^?! key "inputs" . _Array))+     )+  in f <$> relevant++mkConstructor :: [Value] -> [(Text, AbiType)]+mkConstructor abis =+  let+    isConstructor y =+      "constructor" == y ^?! key "type" . _String+  in+    case filter isConstructor abis of+      [abi] -> map parseMethodInput (toList (abi ^?! key "inputs" . _Array))+      [] -> [] -- default constructor has zero inputs+      _  -> error "strange: contract has multiple constructors"+ mkStorageLayout :: Maybe Text -> Maybe (Map Text StorageItem) mkStorageLayout Nothing = Nothing-mkStorageLayout (Just json) = do items <- json ^? key "storage" . _Array-                                 types <- json ^? key "types"-                                 Map.fromList <$> mapM-                                    (\item -> do name <- item ^? key "label" . _String-                                                 offset <- item ^? key "offset" . _Number >>= toBoundedInteger-                                                 slot <- item ^? key "slot" . _String-                                                 typ <- item ^? key "type" . _String-                                                 slotType <- types ^?! key typ ^? key "label" . _String-                                                 return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot))--                                    )-                                    (Vector.toList items)+mkStorageLayout (Just json) = do+  items <- json ^? key "storage" . _Array+  types <- json ^? key "types"+  fmap Map.fromList $ (forM (Vector.toList items) $ \item ->+    do name <- item ^? key "label" . _String+       offset <- item ^? key "offset" . _Number >>= toBoundedInteger+       slot <- item ^? key "slot" . _String+       typ <- item ^? key "type" . _String+       slotType <- types ^?! key typ ^? key "label" . _String+       return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot)))  signature :: AsValue s => s -> Text signature abi =@@ -423,6 +464,52 @@       ""   return (x, pack path) +solc :: Language -> Text -> IO Text+solc lang src =+  withSystemTempFile "hevm.sol" $ \path handle -> do+    hClose handle+    writeFile path (stdjson lang src)+    Text.pack <$> readProcess+      "solc"+      ["--standard-json", path]+      ""++data Language = Solidity | Yul+  deriving (Show)++data StandardJSON = StandardJSON Language Text+-- more options later perhaps++instance ToJSON StandardJSON where+  toJSON (StandardJSON lang src) =+    object [ "language" .= show lang+           , "sources" .= object ["hevm.sol" .=+                                   object ["content" .= src]]+           , "settings" .=+             object [ "outputSelection" .=+                    object ["*" .= +                      object ["*" .= (toJSON+                              ["metadata" :: String,+                               "evm.bytecode",+                               "evm.deployedBytecode",+                               "abi",+                               "storageLayout",+                               "evm.bytecode.sourceMap",+                               "evm.bytecode.linkReferences",+                               "evm.bytecode.generatedSources",+                               "evm.deployedBytecode.sourceMap",+                               "evm.deployedBytecode.linkReferences",+                               "evm.deployedBytecode.generatedSources"+                              ]),+                              "" .= (toJSON ["ast" :: String])+                             ]+                            ]+                    ]+           ]+                               +stdjson :: Language -> Text -> Text+stdjson lang src = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src+ -- When doing CREATE and passing constructor arguments, Solidity loads -- the argument data via the creation bytecode, since there is no "calldata" -- for CREATE.@@ -478,15 +565,10 @@     tmp =        Map.fromList       . mapMaybe-        (\v ->-          case preview (key "src" . _String) v of-            Just src ->-              case map (readMaybe . Text.unpack) (Text.split (== ':') src) of-                [Just i, Just n, Just f] ->-                  Just ((i, n, f), v)-                _ ->-                  error "strange formatting of src field"-            _ ->-              Nothing)+        (\v -> do+          src <- preview (key "src" . _String) v+          [i, n, f] <- mapM (readMaybe . Text.unpack) (Text.split (== ':') src)+          return ((i, n, f), v)+        )       . Map.elems       $ astIds

@@ -6,6 +6,7 @@   , Stepper   , exec   , execFully+  , run   , runFully   , wait   , ask@@ -26,23 +27,17 @@  import Prelude hiding (fail) -import Control.Monad.Operational (Program(..), singleton, view, ProgramViewT(..), ProgramView)+import Control.Monad.Operational (Program, singleton, view, ProgramViewT(..), ProgramView) import Control.Monad.State.Strict (runState, liftIO, StateT) import qualified Control.Monad.State.Class as State import qualified EVM.Exec-import Control.Lens (use)-import Data.Binary.Get (runGetOrFail) import Data.Text (Text) import EVM.Types (Buffer)  import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose) import qualified EVM -import EVM.ABI (AbiType, AbiValue, getAbi) import qualified EVM.Fetch as Fetch--import Data.ByteString (ByteString)-import qualified Data.ByteString.Lazy as LazyByteString  -- | The instruction type of the operational monad data Action a where

@@ -9,58 +9,68 @@  import Control.Lens hiding (pre) import EVM hiding (Query, push)+import qualified EVM import EVM.Exec import qualified EVM.Fetch as Fetch import EVM.ABI import EVM.Stepper (Stepper) import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational-import EVM.Types hiding (Word)-import EVM.Symbolic (SymWord(..), sw256)-import EVM.Concrete (createAddress, Word)+import Control.Monad.State.Strict hiding (state)+import Data.Maybe (catMaybes, fromMaybe)+import EVM.Types+import EVM.Concrete (createAddress) import qualified EVM.FeeSchedule as FeeSchedule import Data.SBV.Trans.Control import Data.SBV.Trans hiding (distinct, Word) import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word) import Data.Vector (toList, fromList)+import Data.Tree -import Control.Monad.IO.Class-import qualified Control.Monad.State.Class as State import Data.ByteString (ByteString, pack) import qualified Data.ByteString.Lazy as Lazy import qualified Data.ByteString as BS import Data.Text (Text, splitOn, unpack)-import Control.Monad.State.Strict (runStateT, runState, StateT, get, put, zipWithM)+import Control.Monad.State.Strict (runState, get, put, zipWithM)+import qualified Control.Monad.State.Class as State import Control.Applicative  -- | Convenience functions for generating large symbolic byte strings-sbytes32, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8])+sbytes32, sbytes128, sbytes256, sbytes512, sbytes1024 :: Query ([SWord 8]) sbytes32 = toBytes <$> freshVar_ @ (WordN 256) sbytes128 = toBytes <$> freshVar_ @ (WordN 1024) sbytes256 = liftA2 (++) sbytes128 sbytes128 sbytes512 = liftA2 (++) sbytes256 sbytes256 sbytes1024 = liftA2 (++) sbytes512 sbytes512 +mkByte :: Query [SWord 8]+mkByte = do x <- freshVar_+            return [x]+ -- | Abstract calldata argument generation--- We don't assume input types are restricted to their proper range here;--- such assumptions should instead be given as preconditions.--- This could catch some interesting calldata mismanagement errors.-symAbiArg :: AbiType -> Query ([SWord 8], SWord 32)-symAbiArg (AbiUIntType n) | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32-                                                            return (x, 32)+symAbiArg :: AbiType -> Query ([SWord 8], W256)+symAbiArg (AbiUIntType n) | n `mod` 8 == 0 && n <= 256 =+  do x <- concatMapM (const mkByte) [0..(n `div` 8) - 1]+     return (padLeft' 32 x, 32)                           | otherwise = error "bad type" -symAbiArg (AbiIntType n)  | n `mod` 8 == 0 && n <= 256 = do x <- sbytes32-                                                            return (x, 32)+symAbiArg (AbiIntType n)  | n `mod` 8 == 0 && n <= 256 =+  do x <- concatMapM (const mkByte) [(0 :: Int) ..(n `div` 8) - 1]+     return (padLeft' 32 x, 32)+                           | otherwise = error "bad type"-symAbiArg AbiBoolType = do x <- sbytes32-                           return (x, 32)+symAbiArg AbiBoolType =+  do x <- mkByte+     return (padLeft' 32 x, 32) -symAbiArg AbiAddressType = do x <- sbytes32-                              return (x, 32)+symAbiArg AbiAddressType =+  do x <- concatMapM (const mkByte) [(0 :: Int)..19]+     return (padLeft' 32 x, 32) -symAbiArg (AbiBytesType n) | n <= 32 = do x <- sbytes32-                                          return (x, 32)+symAbiArg (AbiBytesType n) | n <= 32 =+  do x <- concatMapM (const mkByte) [0..n - 1]+     return (padLeft' 32 x, 32)+                            | otherwise = error "bad type"  -- TODO: is this encoding correct?@@ -81,7 +91,7 @@ -- with concrete arguments. -- Any argument given as "<symbolic>" or omitted at the tail of the list are -- kept symbolic.-symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], SWord 32)+symCalldata :: Text -> [AbiType] -> [String] -> Query ([SWord 8], W256) symCalldata sig typesignature concreteArgs =   let args = concreteArgs <> replicate (length typesignature - length concreteArgs)  "<symbolic>"       mkArg typ "<symbolic>" = symAbiArg typ@@ -97,18 +107,18 @@     case typesignature of       Nothing -> do cd <- sbytes256                     len <- freshVar_-                    return (cd, len, len .<= 256)+                    return (cd, var "calldataLength" len, (len .<= 256, Todo "calldatalength < 256" []))       Just (name, typs) -> do (cd, cdlen) <- symCalldata name typs concreteArgs-                              return (cd, cdlen, sTrue)+                              return (cd, S (Literal cdlen) (literal $ num cdlen), (sTrue, Todo "Trivial" []))   symstore <- case storagemodel of-    SymbolicS -> Symbolic <$> freshArray_ Nothing-    InitialS -> Symbolic <$> freshArray_ (Just 0)+    SymbolicS -> Symbolic [] <$> freshArray_ Nothing+    InitialS -> Symbolic [] <$> freshArray_ (Just 0)     ConcreteS -> return $ Concrete mempty   c <- SAddr <$> freshVar_-  value' <- sw256 <$> freshVar_-  return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' (SymbolicBuffer cd', cdlen) & over pathConditions ((<>) [cdconstraint])+  value' <- var "CALLVALUE" <$> freshVar_+  return $ loadSymVM (RuntimeCode x) symstore storagemodel c value' (SymbolicBuffer cd', cdlen) & over constraints ((<>) [cdconstraint]) -loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SWord 32) -> VM+loadSymVM :: ContractCode -> Storage -> StorageModel -> SAddr -> SymWord -> (Buffer, SymWord) -> VM loadSymVM x initStore model addr callvalue' calldata' =     (makeVm $ VMOpts     { vmoptContract = contractWithStore x initStore@@ -133,7 +143,52 @@     }) & set (env . contracts . at (createAddress ethrunAddress 1))              (Just (contractWithStore x initStore)) +data BranchInfo = BranchInfo+  { _vm                 :: VM,+    _branchCondition    :: Maybe Whiff+  } +doInterpret :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (Tree BranchInfo)+doInterpret fetcher maxIter vm = let+      f (vm', cs) = Node (BranchInfo (if length cs == 0 then vm' else vm) Nothing) cs+    in f <$> interpret' fetcher maxIter vm++interpret' :: Fetch.Fetcher -> Maybe Integer -> VM -> Query (VM, [(Tree BranchInfo)])+interpret' fetcher maxIter vm = let+  cont s = interpret' fetcher maxIter $ execState s vm+  in case view EVM.result vm of++    Nothing -> cont exec1++    Just (VMFailure (EVM.Query q@(PleaseAskSMT _ _ continue))) -> let+      codelocation = getCodeLocation vm+      iteration = num $ fromMaybe 0 $ view (iterations . at codelocation) vm+      -- as an optimization, we skip consulting smt+      -- if we've been at the location less than 5 times+      in if iteration < (max (fromMaybe 0 maxIter) 5)+         then cont $ continue EVM.Unknown+         else io (fetcher q) >>= cont++    Just (VMFailure (EVM.Query q)) -> io (fetcher q) >>= cont++    Just (VMFailure (Choose (EVM.PleaseChoosePath whiff continue)))+      -> case maxIterationsReached vm maxIter of+        Nothing -> let+          lvm = execState (continue True) vm+          rvm = execState (continue False) vm+          in do+            push 1+            (leftvm, left) <- interpret' fetcher maxIter lvm+            pop 1+            push 1+            (rightvm, right) <- interpret' fetcher maxIter rvm+            pop 1+            return (vm, [Node (BranchInfo leftvm (Just whiff)) left, Node (BranchInfo rightvm (Just whiff)) right])+        Just n -> cont $ continue (not n)++    Just _+      -> return (vm, [])+ -- | Interpreter which explores all paths at -- | branching points. -- | returns a list of possible final evm states@@ -159,34 +214,38 @@           exec >>= interpret fetcher maxIter . k         Stepper.Run ->           run >>= interpret fetcher maxIter . k-        Stepper.Ask (EVM.PleaseChoosePath continue) -> do+        Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do           vm <- get           case maxIterationsReached vm maxIter of-            Nothing -> do push 1-                          a <- interpret fetcher maxIter (Stepper.evm (continue True) >>= k)-                          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)+            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-          let performQuery =-                do m <- liftIO (fetcher q)-                   interpret fetcher maxIter (Stepper.evm m >>= k)+          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+              iteration <- num <$> fromMaybe 0 <$> use (iterations . at codelocation)++              -- if this is the first time we are branching at this point,+              -- explore both branches without consulting SMT.+              -- Exploring too many branches is a lot cheaper than+              -- consulting our SMT solver.+              if iteration < (max (fromMaybe 0 maxIter) 5)+              then interpret fetcher maxIter (Stepper.evm (continue EVM.Unknown) >>= k)+              else performQuery+             _ -> performQuery          Stepper.EVM m ->@@ -204,7 +263,7 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (VM, [VM]) VM)+checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM) checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)  checkAssertions :: Postcondition@@ -212,12 +271,13 @@   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse   _ -> sTrue -verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)+verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), 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 Nothing Nothing maybepost+    let preState = over constraints ((++) [(pre preStateRaw, Todo "assumptions" [])]) preStateRaw+    v <- verify preState Nothing Nothing maybepost+    return (v, preState)  pruneDeadPaths :: [VM] -> [VM] pruneDeadPaths =@@ -225,19 +285,45 @@     Just (VMFailure DeadPath) -> False     _ -> True +consistentPath :: VM -> Query (Maybe VM)+consistentPath vm = do+  resetAssertions+  constrain $ sAnd $ fst <$> view constraints vm+  checkSat >>= \case+    Sat -> return $ Just vm+    Unk -> return $ Just vm -- the path may still be consistent+    Unsat -> return Nothing+    DSat _ -> error "unexpected DSAT"++consistentTree :: Tree BranchInfo -> Query (Maybe (Tree BranchInfo))+consistentTree (Node (BranchInfo vm w) []) = do+  consistentPath vm >>= \case+    Nothing  -> return Nothing+    Just vm' -> return $ Just $ Node (BranchInfo vm' w) []+consistentTree (Node b xs) = do+  consistentChildren <- catMaybes <$> forM xs consistentTree+  if null consistentChildren then+    return Nothing+  else+    return $ Just (Node b consistentChildren)+++leaves :: Tree BranchInfo -> [VM]+leaves (Node x []) = [_vm x]+leaves (Node _ xs) = concatMap leaves xs+ -- | Symbolically execute the VM and check all endstates against the postcondition, if available.--- Returns `Right VM` if the postcondition can be violated, where `VM` is a prestate counterexample,--- or `Left (VM, [VM])`, a pair of `prestate` and post vm states.-verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (VM, [VM]) VM)+-- Returns `Right (Tree BranchInfo)` if the postcondition can be violated, or+-- or `Left (Tree BranchInfo)`, if the postcondition holds for all endstates.+verify :: VM -> Maybe Integer -> Maybe (Fetch.BlockNumber, Text) -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo)) verify preState maxIter rpcinfo maybepost = do-  let model = view (env . storageModel) preState   smtState <- queryState-  results <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) rpcinfo model False) maxIter Stepper.runFully) preState+  tree <- doInterpret (Fetch.oracle (Just smtState) rpcinfo False) maxIter preState   case maybepost of     (Just post) -> do-      let livePaths = pruneDeadPaths results+      let livePaths = pruneDeadPaths $ leaves tree       -- 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+          postC = sOr $ fmap (\postState -> (sAnd (fst <$> view constraints postState)) .&& sNot (post (preState, postState))) livePaths       -- is there any path which can possibly violate       -- the postcondition?       resetAssertions@@ -245,13 +331,14 @@       io $ putStrLn "checking postcondition..."       checkSat >>= \case         Unk -> do io $ putStrLn "postcondition query timed out"-                  return $ Left (preState, livePaths)+                  return $ Left tree         Unsat -> do io $ putStrLn "Q.E.D."-                    return $ Left (preState, livePaths)-        Sat -> return $ Right preState+                    return $ Left tree+        Sat -> return $ Right tree+        DSat _ -> error "unexpected DSAT"      Nothing -> do io $ putStrLn "Nothing to check"-                  return $ Left (preState, pruneDeadPaths results)+                  return $ Left tree  -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states. equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM)@@ -263,24 +350,24 @@       callvalue' = preStateA ^. state . callvalue       prestorage = preStateA ^?! env . contracts . ix preself . storage       (calldata', cdlen) = view (state . calldata) preStateA-      pathconds = view pathConditions preStateA-      preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set pathConditions pathconds+      pathconds = view constraints preStateA+      preStateB = loadSymVM (RuntimeCode bytecodeB) prestorage SymbolicS precaller callvalue' (calldata', cdlen) & set constraints pathconds    smtState <- queryState   push 1-  aVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateA+  aVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateA   pop 1   push 1-  bVMs <- fst <$> runStateT (interpret (Fetch.oracle (Just smtState) Nothing SymbolicS False) maxiter Stepper.runFully) preStateB+  bVMs <- doInterpret (Fetch.oracle (Just smtState) Nothing False) maxiter preStateB   pop 1   -- Check each pair of endstates for equality:-  let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths aVMs, b <- pruneDeadPaths bVMs]+  let differingEndStates = uncurry distinct <$> [(a,b) | a <- pruneDeadPaths (leaves aVMs), b <- pruneDeadPaths (leaves bVMs)]       distinct a b =-        let (aPath, bPath) = both' (view pathConditions) (a, b)+        let (aPath, bPath) = both' (view constraints) (a, b)             (aSelf, bSelf) = both' (view (state . contract)) (a, b)             (aEnv, bEnv) = both' (view (env . contracts)) (a, b)             (aResult, bResult) = both' (view result) (a, b)-            (Symbolic aStorage, Symbolic bStorage) = (view storage (aEnv ^?! ix aSelf), view storage (bEnv ^?! ix bSelf))+            (Symbolic _ aStorage, Symbolic _ bStorage) = (view storage (aEnv ^?! ix aSelf), view storage (bEnv ^?! ix bSelf))             differingResults = case (aResult, bResult) of                (Just (VMSuccess aOut), Just (VMSuccess bOut)) ->@@ -296,9 +383,9 @@                (Just _, Just _) -> sTrue -              _ -> error "Internal error during symbolic execution (should not be possible)"+              errormsg -> error $ show errormsg -        in sAnd aPath .&& sAnd bPath .&& differingResults+        in sAnd (fst <$> aPath) .&& sAnd (fst <$> bPath) .&& differingResults   -- If there exists a pair of endstates where this is not the case,   -- the following constraint is satisfiable   constrain $ sOr differingEndStates@@ -306,21 +393,22 @@   checkSat >>= \case      Unk -> error "solver said unknown!"      Sat -> return $ Right preStateA-     Unsat -> return $ Left (pruneDeadPaths aVMs, pruneDeadPaths bVMs)+     Unsat -> return $ Left (leaves aVMs, leaves bVMs)+     DSat _ -> error "unexpected DSAT"  both' :: (a -> b) -> (a, a) -> (b, b) both' f (x, y) = (f x, f y)  showCounterexample :: VM -> Maybe (Text, [AbiType]) -> Query () showCounterexample vm maybesig = do-  let (calldata', cdlen) = view (EVM.state . EVM.calldata) vm+  let (calldata', S _ cdlen) = view (EVM.state . EVM.calldata) vm       S _ cvalue = view (EVM.state . EVM.callvalue) vm       SAddr caller' = view (EVM.state . EVM.caller) vm   cdlen' <- num <$> getValue cdlen   calldatainput <- case calldata' of     SymbolicBuffer cd -> mapM (getValue.fromSized) (take cdlen' cd) >>= return . pack     ConcreteBuffer cd -> return $ BS.take cdlen' cd-  callvalue' <- num <$> getValue cvalue+  callvalue' <- getValue cvalue   caller'' <- num <$> getValue caller'   io $ do     putStrLn "Calldata:"

@@ -2,52 +2,40 @@ {-# Language DataKinds #-} {-# Language OverloadedStrings #-} {-# Language TypeApplications #-}+{-# Language ScopedTypeVariables #-}  module EVM.Symbolic where -import Prelude hiding  (Word)+import Prelude hiding  (Word, LT, GT) import qualified Data.ByteString as BS import Data.ByteString (ByteString) import Control.Lens hiding (op, (:<), (|>), (.>)) import Data.Maybe                   (fromMaybe, fromJust)  import EVM.Types-import EVM.Concrete (Word (..), Whiff(..)) import qualified EVM.Concrete as Concrete+import qualified Data.ByteArray       as BA import Data.SBV hiding (runSMT, newArray_, addAxiom, Word)----- | Symbolic words of 256 bits, possibly annotated with additional---   "insightful" information-data SymWord = S Whiff (SWord 256)---- | Convenience functions transporting between the concrete and symbolic realm-sw256 :: SWord 256 -> SymWord-sw256 = S Dull+import Data.SBV.Tools.Overflow+import Crypto.Hash (Digest, SHA256)+import qualified Crypto.Hash as Crypto -litWord :: Word -> (SymWord)+litWord :: Word -> SymWord litWord (C whiff a) = S whiff (literal $ toSizzle a) -w256lit :: W256 -> SymWord-w256lit = S Dull . literal . toSizzle- litAddr :: Addr -> SAddr litAddr = SAddr . literal . toSizzle -maybeLitWord :: SymWord -> Maybe Word-maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a)- maybeLitAddr :: SAddr -> Maybe Addr maybeLitAddr (SAddr a) = fmap fromSizzle (unliteral a)  maybeLitBytes :: [SWord 8] -> Maybe ByteString maybeLitBytes xs = fmap (\x -> BS.pack (fmap fromSized x)) (mapM unliteral xs) --- | Note: these forms are crude and in general,+-- | Note: the (force*) functions are crude and in general, -- the continuation passing style `forceConcrete` -- alternatives should be prefered for better error -- handling when used during EVM execution- forceLit :: SymWord -> Word forceLit (S whiff a) = case unliteral a of   Just c -> C whiff (fromSizzle c)@@ -60,48 +48,42 @@ forceBuffer (ConcreteBuffer b) = b forceBuffer (SymbolicBuffer b) = forceLitBytes b --- | Arithmetic operations on SymWord- sdiv :: SymWord -> SymWord -> SymWord-sdiv (S _ x) (S _ y) = let sx, sy :: SInt 256+sdiv (S a x) (S b y) = let sx, sy :: SInt 256                            sx = sFromIntegral x                            sy = sFromIntegral y-                       in sw256 $ sFromIntegral (sx `sQuot` sy)+                       in S (Div a b) (sFromIntegral (sx `sQuot` sy))  smod :: SymWord -> SymWord -> SymWord-smod (S _ x) (S _ y) = let sx, sy :: SInt 256+smod (S a x) (S b y) = let sx, sy :: SInt 256                            sx = sFromIntegral x                            sy = sFromIntegral y-                       in sw256 $ ite (y .== 0) 0 (sFromIntegral (sx `sRem` sy))+                       in S (Mod a b) $ ite (y .== 0) 0 (sFromIntegral (sx `sRem` sy))  addmod :: SymWord -> SymWord -> SymWord -> SymWord-addmod (S _ x) (S _ y) (S _ z) = let to512 :: SWord 256 -> SWord 512+addmod (S a x) (S b y) (S c z) = let to512 :: SWord 256 -> SWord 512                                      to512 = sFromIntegral-                                 in sw256 $ sFromIntegral $ ((to512 x) + (to512 y)) `sMod` (to512 z)+                                 in S (Todo "addmod" [a, b, c]) $ sFromIntegral $ ((to512 x) + (to512 y)) `sMod` (to512 z)  mulmod :: SymWord -> SymWord -> SymWord -> SymWord-mulmod (S _ x) (S _ y) (S _ z) = let to512 :: SWord 256 -> SWord 512+mulmod (S a x) (S b y) (S c z) = let to512 :: SWord 256 -> SWord 512                                      to512 = sFromIntegral-                                 in sw256 $ sFromIntegral $ ((to512 x) * (to512 y)) `sMod` (to512 z)+                                 in S (Todo "mulmod" [a, b, c]) $ sFromIntegral $ ((to512 x) * (to512 y)) `sMod` (to512 z) +-- | Signed less than slt :: SymWord -> SymWord -> SymWord-slt (S _ x) (S _ y) =-  sw256 $ ite (sFromIntegral x .< (sFromIntegral y :: (SInt 256))) 1 0+slt (S xw x) (S yw y) =+  iteWhiff (SLT xw yw) (sFromIntegral x .< (sFromIntegral y :: (SInt 256))) 1 0 +-- | Signed greater than sgt :: SymWord -> SymWord -> SymWord-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'+sgt (S xw x) (S yw y) =+  iteWhiff (SGT xw yw) (sFromIntegral x .> (sFromIntegral y :: (SInt 256))) 1 0 --- | Operations over symbolic memory (list of symbolic bytes)+-- * Operations over symbolic memory (list of symbolic bytes) swordAt :: Int -> [SWord 8] -> SymWord-swordAt i bs = sw256 . fromBytes $ truncpad 32 $ drop i bs+swordAt i bs = let bs' = truncpad 32 $ drop i bs+               in S (FromBytes (SymbolicBuffer bs')) (fromBytes bs')  readByteOrZero' :: Int -> [SWord 8] -> SWord 8 readByteOrZero' i bs = fromMaybe 0 (bs ^? ix i)@@ -122,7 +104,9 @@     a <> a' <> c <> b'  readMemoryWord' :: Word -> [SWord 8] -> SymWord-readMemoryWord' (C _ i) m = sw256 $ fromBytes $ truncpad 32 (drop (num i) m)+readMemoryWord' (C _ i) m =+  let bs = truncpad 32 (drop (num i) m)+  in S (FromBytes (SymbolicBuffer bs)) (fromBytes bs)  readMemoryWord32' :: Word -> [SWord 8] -> SWord 32 readMemoryWord32' (C _ i) m = fromBytes $ truncpad 4 (drop (num i) m)@@ -147,39 +131,36 @@     where walk []     _ acc = acc           walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) --- Generates a ridiculously large set of constraints (roughly 25k) when--- 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 = case (num <$> fromSized <$> unliteral ind, num <$> fromSized <$> unliteral bound) of+-- | Read 32 bytes from index from a bounded list of bytes.+readSWordWithBound :: SymWord -> Buffer -> SymWord -> SymWord+readSWordWithBound sind@(S _ ind) (SymbolicBuffer xs) (S _ bound) = case (num <$> maybeLitWord sind, num <$> fromSizzle <$> 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]]+  _ ->+    -- Generates a ridiculously large set of constraints (roughly 25k) when+    -- the index is symbolic, but it still seems (kind of) manageable+    -- for the solvers. -readSWordWithBound ind (ConcreteBuffer xs) bound =-  case fromSized <$> unliteral ind of-    Nothing -> readSWordWithBound ind (SymbolicBuffer (litBytes xs)) bound-    Just x' ->                                       +    -- The proper solution here is to use smt arrays instead.++    let boundedList = [ite (i .<= bound) x' 0 | (x', i) <- zip xs [1..]]+        res = [select' boundedList 0 (ind + j) | j <- [0..31]]+    in S (FromBytes $ SymbolicBuffer res) $ fromBytes res++readSWordWithBound sind (ConcreteBuffer xs) bound =+  case maybeLitWord sind of+    Nothing -> readSWordWithBound sind (SymbolicBuffer (litBytes xs)) bound+    Just x' ->        -- 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+         litWord $ Concrete.readMemoryWord x' xs  -- a whole foldable instance seems overkill, but length is always good to have! len :: Buffer -> Int len (SymbolicBuffer bs) = length bs len (ConcreteBuffer bs) = BS.length bs -grab :: Int -> Buffer -> Buffer-grab n (SymbolicBuffer bs) = SymbolicBuffer $ take n bs-grab n (ConcreteBuffer bs) = ConcreteBuffer $ BS.take n bs--ditch :: Int -> Buffer -> Buffer-ditch n (SymbolicBuffer bs) = SymbolicBuffer $ drop n bs-ditch n (ConcreteBuffer bs) = ConcreteBuffer $ BS.drop n bs- readByteOrZero :: Int -> Buffer -> SWord 8 readByteOrZero i (SymbolicBuffer bs) = readByteOrZero' i bs readByteOrZero i (ConcreteBuffer bs) = num $ Concrete.readByteOrZero i bs@@ -222,65 +203,115 @@ readSWord i (SymbolicBuffer x) = readSWord' i x readSWord i (ConcreteBuffer x) = num $ Concrete.readMemoryWord i x --- | Custom instances for SymWord, many of which have direct--- analogues for concrete words defined in Concrete.hs+-- * Uninterpreted functions -instance Show SymWord where-  show s@(S Dull _) = case maybeLitWord s of-    Nothing -> "<symbolic>"-    Just w  -> show w-  show (S (Var var) x) = var ++ ": " ++ show x-  show (S (InfixBinOp symbol x y) z) = show x ++ symbol ++ show y  ++ ": " ++ show z-  show (S (BinOp symbol x y) z) = symbol ++ show x ++ show y  ++ ": " ++ show z-  show (S (UnOp symbol x) z) = symbol ++ show x ++ ": " ++ show z-  show (S whiff x) = show whiff ++ ": " ++ show x+symSHA256N :: SInteger -> SInteger -> SWord 256+symSHA256N = uninterpret "sha256" -instance EqSymbolic SymWord where-  (.==) (S _ x) (S _ y) = x .== y+symkeccakN :: SInteger -> SInteger -> SWord 256+symkeccakN = uninterpret "keccak" -instance Num SymWord where-  (S _ x) + (S _ y) = sw256 (x + y)-  (S _ x) * (S _ y) = sw256 (x * y)-  abs (S _ x) = sw256 (abs x)-  signum (S _ x) = sw256 (signum x)-  fromInteger x = sw256 (fromInteger x)-  negate (S _ x) = sw256 (negate x)+toSInt :: [SWord 8] -> SInteger+toSInt bs = sum $ zipWith (\a (i :: Integer) -> sFromIntegral a * 256 ^ i) bs [0..] -instance Bits SymWord where-  (S _ x) .&. (S _ y) = sw256 (x .&. y)-  (S _ x) .|. (S _ y) = sw256 (x .|. y)-  (S _ x) `xor` (S _ y) = sw256 (x `xor` y)-  complement (S _ x) = sw256 (complement x)-  shift (S _ x) i = sw256 (shift x i)-  rotate (S _ x) i = sw256 (rotate x i)-  bitSize (S _ x) = bitSize x-  bitSizeMaybe (S _ x) = bitSizeMaybe x-  isSigned (S _ x) = isSigned x-  testBit (S _ x) i = testBit x i-  bit i = sw256 (bit i)-  popCount (S _ x) = popCount x -instance SDivisible SymWord where-  sQuotRem (S _ x) (S _ y) = let (a, b) = x `sQuotRem` y-                             in (sw256 a, sw256 b)-  sDivMod (S _ x) (S _ y) = let (a, b) = x `sDivMod` y-                             in (sw256 a, sw256 b)+-- | Although we'd like to define this directly as an uninterpreted function,+-- we cannot because [a] is not a symbolic type. We must convert the list into a suitable+-- symbolic type first. The only important property of this conversion is that it is injective.+-- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.+symkeccak' :: [SWord 8] -> SWord 256+symkeccak' bytes = case length bytes of+  0 -> literal $ toSizzle $ keccak ""+  n -> symkeccakN (num n) (toSInt bytes) -instance Mergeable SymWord where-  symbolicMerge a b (S _ x) (S _ y) = sw256 $ symbolicMerge a b x y-  select xs (S _ x) b = let ys = fmap (\(S _ y) -> y) xs-                        in sw256 $ select ys x b+symSHA256 :: [SWord 8] -> [SWord 8]+symSHA256 bytes = case length bytes of+  0 -> litBytes $ BS.pack $ BA.unpack $ (Crypto.hash BS.empty :: Digest SHA256)+  n -> toBytes $ symSHA256N (num n) (toSInt bytes) -instance Bounded SymWord where-  minBound = sw256 minBound-  maxBound = sw256 maxBound+rawVal :: SymWord -> SWord 256+rawVal (S _ v) = v -instance Eq SymWord where-  (S _ x) == (S _ y) = x == y+-- | Reconstruct the smt/sbv value from a whiff+-- Should satisfy (rawVal x .== whiffValue x)+whiffValue :: Whiff -> SWord 256+whiffValue w = case w of+  w'@(Todo _ _) -> error $ "unable to get value of " ++ show w'+  And x y       -> whiffValue x .&. whiffValue y+  Or x y        -> whiffValue x .|. whiffValue y+  Eq x y        -> ite (whiffValue x .== whiffValue y) 1 0+  LT x y        -> ite (whiffValue x .< whiffValue y) 1 0+  GT x y        -> ite (whiffValue x .> whiffValue y) 1 0+  ITE b x y     -> ite (whiffValue b .== 1) (whiffValue x) (whiffValue y)+  SLT x y       -> rawVal $ slt (S x (whiffValue x)) (S y (whiffValue y))+  SGT x y       -> rawVal $ sgt (S x (whiffValue x)) (S y (whiffValue y))+  IsZero x      -> ite (whiffValue x .== 0) 1 0+  SHL x y       -> sShiftLeft  (whiffValue x) (whiffValue y)+  SHR x y       -> sShiftRight (whiffValue x) (whiffValue y)+  SAR x y       -> sSignedShiftArithRight (whiffValue x) (whiffValue y)+  Add x y       -> whiffValue x + whiffValue y+  Sub x y       -> whiffValue x - whiffValue y+  Mul x y       -> whiffValue x * whiffValue y+  Div x y       -> whiffValue x `sDiv` whiffValue y+  Mod x y       -> whiffValue x `sMod` whiffValue y+  Exp x y       -> whiffValue x .^ whiffValue y+  Neg x         -> negate $ whiffValue x+  Var _ v       -> v+  FromKeccak (ConcreteBuffer bstr) -> literal $ num $ keccak bstr+  FromKeccak (SymbolicBuffer buf)  -> symkeccak' buf+  Literal x -> literal $ num $ x+  FromBytes buf -> rawVal $ readMemoryWord 0 buf+  FromStorage ind arr -> readArray arr (whiffValue ind)  -instance Enum SymWord where-  toEnum i = sw256 (toEnum i)-  fromEnum (S _ x) = fromEnum x+-- | Special cases that have proven useful in practice+simplifyCondition :: SBool -> Whiff -> SBool+simplifyCondition _ (IsZero (IsZero (IsZero a))) = whiffValue a .== 0 -instance OrdSymbolic SymWord where-  (.<) (S _ x) (S _ y) = (.<) x y+++-- | Overflow safe math can be difficult for smt solvers to deal with,+-- especially for 256-bit words. When we recognize terms arising from+-- overflow checks, we translate our queries into a more bespoke form,+-- outlined in:+-- Modular Bug-finding for Integer Overflows in the Large:+-- Sound, Efficient, Bit-precise Static Analysis+-- www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf+--+-- Addition overflow.+-- Written as+--    require (x <= (x + y))+-- or require (y <= (x + y))+-- or require (!(y < (x + y)))+simplifyCondition b (IsZero (IsZero (LT (Add x y) z))) =+  let x' = whiffValue x+      y' = whiffValue y+      z' = whiffValue z+      (_, overflow) = bvAddO x' y'+  in+    ite (x' .== z' .||+         y' .== z')+    overflow+    b++-- Multiplication overflow.+-- Written as+--    require (y == 0 || x * y / y == x)+-- or require (y == 0 || x == x * y / y)++-- proveWith cvc4 $ \x y z -> ite (y .== (z :: SWord 8)) (((x * y) `sDiv` z ./= x) .<=> (snd (bvMulO x y) .|| (z .== 0 .&& x .> 0))) (sTrue)+-- Q.E.D.+simplifyCondition b (IsZero (Eq x (Div (Mul y z) w))) =+  simplifyCondition b (IsZero (Eq (Div (Mul y z) w) x))+simplifyCondition b (IsZero (Eq (Div (Mul y z) w) x)) =+  let x' = whiffValue x+      y' = whiffValue y+      z' = whiffValue z+      w' = whiffValue w+      (_, overflow) = bvMulO y' z'+  in+    ite+    ((y' .== x' .&& z' .== w') .||+      (z' .== x' .&& y' .== w'))+    (overflow .|| (w' .== 0 .&& x' ./= 0))+    b+simplifyCondition b _ = b

@@ -12,9 +12,8 @@  import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)-import EVM.Symbolic (SymWord(..))-import EVM.SymExec (maxIterationsReached)-import EVM.Dapp (DappInfo, dappInfo)+import EVM.SymExec (maxIterationsReached, symCalldata)+import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..)) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) import EVM.Dapp (dappAstSrcMap) import EVM.Debug@@ -22,10 +21,9 @@ import EVM.Format (contractNamePart, contractPathPart, showTraceTree) import EVM.Hexdump (prettyHex) import EVM.Op-import EVM.Solidity+import EVM.Solidity hiding (storageLayout) import EVM.Types hiding (padRight)-import EVM.UnitTest (UnitTestOptions (..))-import EVM.UnitTest (initialUnitTestVm, initializeUnitTest, runUnitTest)+import EVM.UnitTest import EVM.StorageLayout  import EVM.Stepper (Stepper)@@ -35,6 +33,7 @@ import EVM.Fetch (Fetcher)  import Control.Lens+import Control.Monad.Trans.Reader import Control.Monad.State.Strict hiding (state)  import Data.Aeson.Lens@@ -44,10 +43,11 @@ import Data.Monoid ((<>)) import Data.Text (Text, pack) import Data.Text.Encoding (decodeUtf8)-import Data.List (sort, lookup)+import Data.List (sort, find) import Data.Version (showVersion) import Data.SBV hiding (solver) +import qualified Data.SBV.Internals as SBV import qualified Data.ByteString as BS import qualified Data.Map as Map import qualified Data.Text as Text@@ -78,13 +78,7 @@   , _uiStep         :: Int   , _uiSnapshots    :: Map Int (VM, Stepper ())   , _uiStepper      :: Stepper ()-  , _uiStackList    :: List Name (Int, (SymWord))-  , _uiBytecodeList :: List Name (Int, Op)-  , _uiTraceList    :: List Name Text-  , _uiSolidityList :: List Name (Int, ByteString)-  , _uiMessage      :: Maybe String   , _uiShowMemory   :: Bool-  , _uiSolc         :: Maybe SolcContract   , _uiTestOpts     :: UnitTestOptions   } @@ -152,9 +146,19 @@     eval (action Operational.:>>= k) =       case action of +        Stepper.Run -> do+          -- Have we reached the final result of this action?+          use (uiVm . result) >>= \case+            Just _ -> do+              -- Yes, proceed with the next action.+              vm <- use uiVm+              interpret mode (k vm)+            Nothing -> do+              -- No, keep performing the current action+              keepExecuting mode (Stepper.run >>= k)+         -- Stepper wants to keep executing?         Stepper.Exec -> do-           -- Have we reached the final result of this action?           use (uiVm . result) >>= \case             Just r ->@@ -162,32 +166,10 @@               interpret mode (k r)             Nothing -> do               -- No, keep performing the current action-              let restart = Stepper.exec >>= k--              case mode of-                Step 0 -> do-                  -- We come here when we've continued while stepping,-                  -- either from a query or from a return;-                  -- we should pause here and wait for the user.-                  pure (Continue restart)--                Step i -> do-                  -- Run one instruction and recurse-                  stepOneOpcode restart-                  interpret (Step (i - 1)) restart--                StepUntil p -> do-                  vm <- use uiVm-                  case p vm of-                    True ->-                      interpret (Step 0) restart-                    False -> do-                      -- Run one instruction and recurse-                      stepOneOpcode restart-                      interpret (StepUntil p) restart+              keepExecuting mode (Stepper.exec >>= k)          -- Stepper is waiting for user input from a query-        Stepper.Ask (EVM.PleaseChoosePath cont) -> do+        Stepper.Ask (PleaseChoosePath _ cont) -> do           -- ensure we aren't stepping past max iterations           vm <- use uiVm           case maxIterationsReached vm ?maxIter of@@ -206,6 +188,33 @@           assign uiVm vm1           interpret mode (Stepper.exec >> (k r)) +keepExecuting :: (?fetcher :: Fetcher+              ,   ?maxIter :: Maybe Integer)+              => StepMode+              -> Stepper a+              -> StateT UiVmState IO (Continuation a)+keepExecuting mode restart = case mode of+  Step 0 -> do+    -- We come here when we've continued while stepping,+    -- either from a query or from a return;+    -- we should pause here and wait for the user.+    pure (Continue restart)++  Step i -> do+    -- Run one instruction and recurse+    stepOneOpcode restart+    interpret (Step (i - 1)) restart++  StepUntil p -> do+    vm <- use uiVm+    if p vm+      then+        interpret (Step 0) restart+      else do+        -- Run one instruction and recurse+        stepOneOpcode restart+        interpret (StepUntil p) restart+ isUnitTestContract :: Text -> DappInfo -> Bool isUnitTestContract name dapp =   elem name (map fst (view dappUnitTests dapp))@@ -224,6 +233,9 @@       { oracle            = oracle'       , verbose           = Nothing       , maxIter           = maxIter'+      , smtTimeout        = Nothing+      , smtState          = Nothing+      , solver            = Nothing       , match             = ""       , fuzzRuns          = 1       , replay            = error "irrelevant"@@ -242,18 +254,11 @@  initUiVmState :: VM -> UnitTestOptions -> Stepper () -> UiVmState initUiVmState vm0 opts script =-  renderVm $   UiVmState     { _uiVm           = vm0     , _uiStepper      = script-    , _uiStackList    = undefined-    , _uiBytecodeList = undefined-    , _uiTraceList    = undefined-    , _uiSolidityList = undefined-    , _uiSolc         = currentSolc (dapp opts) vm0     , _uiStep         = 0     , _uiSnapshots    = singleton 0 (vm0, script)-    , _uiMessage      = Just "Creating unit test contract"     , _uiShowMemory   = False     , _uiTestOpts     = opts     }@@ -261,13 +266,16 @@  -- filters out fuzztests, unless they have -- explicitly been given an argument by `replay`-concreteTests :: UnitTestOptions -> (Text, [(Text, [AbiType])]) -> [(Text, Text)]-concreteTests UnitTestOptions{..} (contractname, tests) = case replay of-  Nothing -> [(contractname, fst x) | x <- tests,-                                      null $ snd x]-  Just (sig, _) -> [(contractname, fst x) | x <- tests,-                                            null (snd x) || fst x == sig]+debuggableTests :: UnitTestOptions -> (Text, [(Test, [AbiType])]) -> [(Text, Text)]+debuggableTests UnitTestOptions{..} (contractname, tests) = case replay of+  Nothing -> [(contractname, extractSig $ fst x) | x <- tests, not $ isFuzzTest x]+  Just (sig, _) -> [(contractname, extractSig $ fst x) | x <- tests, not (isFuzzTest x) || extractSig (fst x) == sig] +isFuzzTest :: (Test, [AbiType]) -> Bool+isFuzzTest (SymbolicTest _, _) = False+isFuzzTest (ConcreteTest _, []) = False+isFuzzTest (ConcreteTest _, _) = True+ main :: UnitTestOptions -> FilePath -> FilePath -> IO () main opts root jsonFilePath =   readSolc jsonFilePath >>=@@ -283,7 +291,7 @@                   TestPickerPane                   (Vec.fromList                    (concatMap-                    (concreteTests opts)+                    (debuggableTests opts)                     (view dappUnitTests dapp)))                   1             , _testPickerDapp = dapp@@ -307,14 +315,53 @@       continue (ViewVm (ui' & set uiStepper steps))   where     m = interpret mode (view uiStepper ui)-    nxt = runStateT (m <* modify renderVm) ui+    nxt = runStateT m ui +backstepUntil+  :: (?fetcher :: Fetcher+     ,?maxIter :: Maybe Integer)+  => (UiVmState -> Pred VM) -> UiVmState -> EventM n (Next UiState)+backstepUntil p s =+  case view uiStep s of+    0 -> continue (ViewVm s)+    n -> do+      s1 <- backstep s+      let+        -- find a previous vm that satisfies the predicate+        snapshots' = Data.Map.filter (p s1 . fst) (view uiSnapshots s1)+      case lookupLT n snapshots' of+        -- If no such vm exists, 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 the predicate doesn't hold+        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 . p s1))+ backstep   :: (?fetcher :: Fetcher      ,?maxIter :: Maybe Integer)   => UiVmState -> EventM n UiVmState backstep s = case view uiStep s of+  -- We're already at the first step; ignore command.   0 -> return s+  -- To step backwards, we revert to the previous snapshot+  -- and execute n - 1 `mod` snapshotInterval steps from there.++  -- We keep the current cache so we don't have to redo+  -- any blocking queries, and also the memory view.   n ->     let       (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)@@ -357,7 +404,7 @@   let opts = view uiTestOpts s       dapp' = dapp (view uiTestOpts s)       tests = concatMap-                (concreteTests opts)+                (debuggableTests opts)                 (view dappUnitTests dapp')   in case tests of     [] -> halt st@@ -408,25 +455,32 @@     suspendAndResume $       Readline.runInputT Readline.defaultSettings loop +-- todo refactor to zipper step forward -- Vm Overview: n - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [])) =-  case view (uiVm . result) s of-    Just _ -> continue (ViewVm s)-    _ -> takeStep s (Step 1)+  if isJust $ view (uiVm . result) s+  then continue (ViewVm s)+  else takeStep s (Step 1)  -- Vm Overview: N - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'N') [])) =-  takeStep s-    (StepUntil (isNextSourcePosition s))+  if isJust $ view (uiVm . result) s+  then continue (ViewVm s)+  else takeStep s+       (StepUntil (isNextSourcePosition s))  -- Vm Overview: C-n - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'n') [V.MCtrl])) =-  takeStep s+  if isJust $ view (uiVm . result) s+  then continue (ViewVm s)+  else takeStep s     (StepUntil (isNextSourcePositionWithoutEntering s))  -- Vm Overview: e - step appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'e') [])) =-  takeStep s+  if isJust $ view (uiVm . result) s+  then continue (ViewVm s)+  else takeStep s     (StepUntil (isExecutionHalted s))  -- Vm Overview: a - step@@ -452,88 +506,32 @@     n -> do       -- To step backwards, we revert to the previous snapshot       -- and execute n - 1 `mod` snapshotInterval steps from there.-      --+       -- We keep the current cache so we don't have to redo       -- any blocking queries, and also the memory view.       let         (step, (vm, stepper)) = fromJust $ lookupLT n (view uiSnapshots s)         s1 = s-          & set uiVm vm-          & set (uiVm . cache) (view (uiVm . cache) s)+          & set uiVm vm -- set the vm to the one from the snapshot+          & set (uiVm . cache) (view (uiVm . cache) s) -- persist the cache           & set uiStep step           & set uiStepper stepper         stepsToTake = n - step - 1        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: P - backstep to previous source+appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'P') [])) =+  backstepUntil isNextSourcePosition s --- 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: c-p - backstep to previous source avoiding CALL and CREATE+appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar 'p') [V.MCtrl])) =+  backstepUntil isNextSourcePositionWithoutEntering s  -- Vm Overview: 0 - choose no jump appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '0') [])) =   case view (uiVm . result) s of-    Just (VMFailure (Choose (PleaseChoosePath contin))) ->+    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->       takeStep (s & set uiStepper (Stepper.evm (contin True) >> (view uiStepper s)))         (Step 1)     _ -> continue (ViewVm s)@@ -541,7 +539,7 @@ -- Vm Overview: 1 - choose jump appEvent (ViewVm s) (VtyEvent (V.EvKey (V.KChar '1') [])) =   case view (uiVm . result) s of-    Just (VMFailure (Choose (PleaseChoosePath contin))) ->+    Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->       takeStep (s & set uiStepper (Stepper.evm (contin False) >> (view uiStepper s)))         (Step 1)     _ -> continue (ViewVm s)@@ -560,10 +558,9 @@ appEvent (ViewPicker s) (VtyEvent (V.EvKey V.KEnter [])) =   case listSelectedElement (view testPickerList s) of     Nothing -> error "nothing selected"-    Just (_, x) ->-      continue . ViewVm $-        initialUiVmStateForTest (view testOpts s) x---          (view testPickerDapp s) x+    Just (_, x) -> do+      initVm <- liftIO $ initialUiVmStateForTest (view testOpts s) x+      continue . ViewVm $ initVm  -- UnitTest Picker: (main) - render list appEvent (ViewPicker s) (VtyEvent e) = do@@ -574,12 +571,21 @@   continue (ViewPicker s')  -- Page: Down - scroll-appEvent s (VtyEvent (V.EvKey V.KDown [])) =-  vScrollBy (viewportScroll TracePane) 1 >> continue s+appEvent (ViewVm s) (VtyEvent (V.EvKey V.KDown [])) =+  if view uiShowMemory s then+    vScrollBy (viewportScroll TracePane) 1 >> continue (ViewVm s)+  else+    if isJust $ view (uiVm . result) s+    then continue (ViewVm s)+    else takeStep s+         (StepUntil (isNewTraceAdded s))  -- Page: Up - scroll-appEvent s (VtyEvent (V.EvKey V.KUp [])) =-  vScrollBy (viewportScroll TracePane) (-1) >> continue s+appEvent (ViewVm s) (VtyEvent (V.EvKey V.KUp [])) =+  if view uiShowMemory s then+    vScrollBy (viewportScroll TracePane) (-1) >> continue (ViewVm s)+  else+    backstepUntil isNewTraceAdded s  -- Page: C-f - Page down appEvent s (VtyEvent (V.EvKey (V.KChar 'f') [V.MCtrl])) =@@ -607,23 +613,29 @@ initialUiVmStateForTest   :: UnitTestOptions   -> (Text, Text)-  -> UiVmState-initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) =-  ui+  -> IO UiVmState+initialUiVmStateForTest opts@UnitTestOptions{..} (theContractName, theTestName) = do+  let state' = fromMaybe (error "Internal Error: missing smtState") smtState+  (buf, len) <- flip runReaderT state' $ SBV.runQueryT $ symCalldata theTestName types []+  let script = do+        Stepper.evm . pushTrace . EntryTrace $+          "test " <> theTestName <> " (" <> theContractName <> ")"+        initializeUnitTest opts testContract+        case test of+          ConcreteTest _ -> do+            let args = case replay of+                         Nothing -> emptyAbi+                         Just (sig, callData) ->+                           if theTestName == sig+                           then decodeAbiValue (AbiTupleType (Vec.fromList types)) callData+                           else emptyAbi+            void (runUnitTest opts theTestName args)+          SymbolicTest _ -> do+            Stepper.evm $ modify symbolify+            void (execSymTest opts theTestName (SymbolicBuffer buf, w256lit len)) -- S (Literal $ num len) (literal $ num len)))+  pure $ initUiVmState vm0 opts script   where-    Just typesig = lookup theTestName (unitTestMethods testContract)-    args = case replay of-      Nothing -> emptyAbi-      Just (sig, callData) ->-        if theTestName == sig-        then decodeAbiValue (AbiTupleType (Vec.fromList typesig)) callData-        else emptyAbi-    script = do-      Stepper.evm . pushTrace . EntryTrace $-        "test " <> theTestName <> " (" <> theContractName <> ")"-      initializeUnitTest opts-      void (runUnitTest opts theTestName args)-    ui = initUiVmState vm0 opts script+    Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract     Just testContract =       view (dappSolcByName . at theContractName) dapp     vm0 =@@ -661,8 +673,8 @@         "m      Toggle memory pane\n" <>         "0      Choose the branch which does not jump \n" <>         "1      Choose the branch which does jump \n" <>-        "Down   Scroll memory pane fwds\n" <>-        "Up     Scroll memory pane back\n" <>+        "Down   Step to next entry in the callstack / Scroll memory pane\n" <>+        "Up     Step to previous entry in the callstack / Scroll memory pane\n" <>         "C-f    Page memory pane fwds\n" <>         "C-b    Page memory pane back\n\n" <>         "Enter  Contracts browser"@@ -711,27 +723,27 @@                   , txt ("Storage: "  <> storageDisplay (view storage c))                   ]                 ]-          Just solc ->+          Just sol ->             hBox               [ borderWithLabel (txt "Contract information") . padBottom Max . padRight (Pad 2) $ vBox-                  [ txt "Name: " <+> txt (contractNamePart (view contractName solc))-                  , txt "File: " <+> txt (contractPathPart (view contractName solc))+                  [ txt "Name: " <+> txt (contractNamePart (view contractName sol))+                  , txt "File: " <+> txt (contractPathPart (view contractName sol))                   , txt " "                   , txt "Constructor inputs:"-                  , vBox . flip map (view constructorInputs solc) $+                  , vBox . flip map (view constructorInputs sol) $                       \(name, abiType) -> txt ("  " <> name <> ": " <> abiTypeSolidity abiType)                   , txt "Public methods:"-                  , vBox . flip map (sort (Map.elems (view abiMap solc))) $+                  , vBox . flip map (sort (Map.elems (view abiMap sol))) $                       \method -> txt ("  " <> view methodSignature method)                   , txt ("Storage:" <> storageDisplay (view storage c))                   ]               , borderWithLabel (txt "Storage slots") . padBottom Max . padRight Max $ vBox-                  (map txt (storageLayout dapp' solc))+                  (map txt (storageLayout dapp' sol))               ]       ]   ]   where storageDisplay (Concrete s) = pack ( show ( Map.toList s))-        storageDisplay (Symbolic _) = pack "<symbolic>"+        storageDisplay (Symbolic v _) = pack $ show v         dapp' = dapp (view (browserVm . uiTestOpts) ui)         Just (_, (_, c)) = listSelectedElement (view browserContractList ui) --        currentContract  = view (dappSolcByHash . ix ) dapp@@ -794,6 +806,13 @@   modifying uiVm (execState exec1)   modifying uiStep (+ 1) +isNewTraceAdded+  :: UiVmState -> Pred VM+isNewTraceAdded ui vm =+  let+    currentTraceTree = length <$> traceForest (view uiVm ui)+    newTraceTree = length <$> traceForest vm+  in currentTraceTree /= newTraceTree  isNextSourcePosition   :: UiVmState -> Pred VM@@ -833,82 +852,24 @@ currentSrcMap :: DappInfo -> VM -> Maybe SrcMap currentSrcMap dapp vm =   let-    this = vm ^?! env . contracts . ix (view (state . codeContract) vm)+    Just this = currentContract vm     i = (view opIxMap this) SVec.! (view (state . pc) vm)     h = view codehash this   in     case preview (dappSolcByHash . ix h) dapp of       Nothing ->         Nothing-      Just (Creation, solc) ->-        preview (creationSrcmap . ix i) solc-      Just (Runtime, solc) ->-        preview (runtimeSrcmap . ix i) solc--currentSolc :: DappInfo -> VM -> Maybe SolcContract-currentSolc dapp vm =-  let-    this = vm ^?! env . contracts . ix (view (state . contract) vm)-    h = view codehash this-  in-    preview (dappSolcByHash . ix h . _2) dapp--renderVm :: UiVmState -> UiVmState-renderVm ui = updateUiVmState ui (view uiVm ui)--updateUiVmState :: UiVmState -> VM -> UiVmState-updateUiVmState ui vm =-  let-    move = maybe id listMoveTo (vmOpIx vm)-    address = view (state . contract) vm-    message =-      case view result vm of-        Just (VMSuccess (ConcreteBuffer msg)) ->-          Just ("VMSuccess: " <> (show $ ByteStringS msg))-        Just (VMSuccess (SymbolicBuffer msg)) ->-          Just ("VMSuccess: <symbolicbuffer> " <> (show msg))-        Just (VMFailure (Revert msg)) ->-          Just ("VMFailure: " <> (show . ByteStringS $ msg))-        Just (VMFailure err) ->-          Just ("VMFailure: " <> show err)-        Nothing ->-          Just ("Executing EVM code in " <> show address)-    in ui-      & set uiVm vm-      & set uiStackList-          (list StackPane (Vec.fromList $ zip [1..] (view (state . stack) vm)) 2)-      & set uiBytecodeList-          (move $ list BytecodePane-             (view codeOps (fromJust (currentContract vm)))-             1)-      & set uiMessage message-      & set uiTraceList-          (list-            TracePane-            (Vec.fromList-              . Text.lines-              . showTraceTree dapp'-              $ vm)-            1)-      & set uiSolidityList-          (list SolidityPane-              (case currentSrcMap dapp' vm of-                Nothing -> mempty-                Just x ->-                  view (dappSources-                        . sourceLines-                        . ix (srcMapFile x)-                        . to (Vec.imap (,)))-                    dapp')-              1)-      where-        dapp' = dapp (view uiTestOpts ui)+      Just (Creation, sol) ->+        preview (creationSrcmap . ix i) sol+      Just (Runtime, sol) ->+        preview (runtimeSrcmap . ix i) sol  drawStackPane :: UiVmState -> UiWidget drawStackPane ui =   let     gasText = showWordExact (view (uiVm . state . gas) ui)     labelText = txt ("Gas available: " <> gasText <> "; stack:")+    stackList = list StackPane (Vec.fromList $ zip [(1 :: Int)..] (view (uiVm . state . stack) ui)) 2   in hBorderWithLabel labelText <=>     renderList       (\_ (i, x@(S _ w)) ->@@ -920,18 +881,40 @@                        Just u -> showWordExplanation (fromSizzle u) $ dapp (view uiTestOpts ui)))            ])       False-      (view uiStackList ui)+      stackList +message :: VM -> String+message vm =+  case view result vm of+    Just (VMSuccess (ConcreteBuffer msg)) ->+      "VMSuccess: " <> (show $ ByteStringS msg)+    Just (VMSuccess (SymbolicBuffer msg)) ->+      "VMSuccess: <symbolicbuffer> " <> (show msg)+    Just (VMFailure (Revert msg)) ->+      "VMFailure: " <> (show . ByteStringS $ msg)+    Just (VMFailure err) ->+      "VMFailure: " <> show err+    Nothing ->+      "Executing EVM code in " <> show (view (state . contract) vm)++ drawBytecodePane :: UiVmState -> UiWidget drawBytecodePane ui =-  hBorderWithLabel (case view uiMessage ui of { Nothing -> str ""; Just s -> str s }) <=>+  let+    vm = view uiVm ui+    move = maybe id listMoveTo $ vmOpIx vm+  in+    hBorderWithLabel (str $ message vm) <=>     Centered.renderList       (\active x -> if not active                     then withDefAttr dimAttr (opWidget x)                     else withDefAttr boldAttr (opWidget x))       False-      (view uiBytecodeList ui)+      (move $ list BytecodePane+        (view codeOps (fromJust (currentContract vm)))+        1) + dim :: Widget n -> Widget n dim = withDefAttr dimAttr @@ -945,30 +928,57 @@  drawTracePane :: UiVmState -> UiWidget drawTracePane s =-  case view uiShowMemory s of+  let vm = view uiVm s+      dapp' = dapp (view uiTestOpts s)+      traceList =+        list+          TracePane+          (Vec.fromList+            . Text.lines+            . showTraceTree dapp'+            $ vm)+          1++  in case view uiShowMemory s of     True ->       hBorderWithLabel (txt "Calldata")-      <=> str (prettyIfConcrete $ fst (view (uiVm . state . calldata) s))+      <=> str (prettyIfConcrete $ fst (view (state . calldata) vm))       <=> hBorderWithLabel (txt "Returndata")-      <=> str (prettyIfConcrete (view (uiVm . state . returndata) s))+      <=> str (prettyIfConcrete (view (state . returndata) vm))       <=> hBorderWithLabel (txt "Output")-      <=> str (maybe "" show (view (uiVm . result) s))+      <=> str (maybe "" show (view result vm))       <=> hBorderWithLabel (txt "Cache")-      <=> str (show (view (uiVm . cache . path) s))+      <=> str (show (view (cache . path) vm))+      <=> hBorderWithLabel (txt "Path Conditions")+      <=> (str $ show $ snd <$> view constraints vm)       <=> hBorderWithLabel (txt "Memory")       <=> viewport TracePane Vertical-            (str (prettyIfConcrete (view (uiVm . state . memory) s)))+            (str (prettyIfConcrete (view (state . memory) vm)))     False ->       hBorderWithLabel (txt "Trace")       <=> renderList             (\_ x -> txt x)             False-            (view uiTraceList s)+            (listMoveTo (length traceList) traceList) +solidityList :: VM -> DappInfo -> List Name (Int, ByteString)+solidityList vm dapp' =+  list SolidityPane+    (case currentSrcMap dapp' vm of+        Nothing -> mempty+        Just x ->+          view (dappSources+            . sourceLines+            . ix (srcMapFile x)+            . to (Vec.imap (,)))+          dapp')+    1+ drawSolidityPane :: UiVmState -> UiWidget drawSolidityPane ui =   let dapp' = dapp (view uiTestOpts ui)-  in case currentSrcMap dapp' (view uiVm ui) of+      vm = view uiVm ui+  in case currentSrcMap dapp' vm of     Nothing -> padBottom Max (hBorderWithLabel (txt "<no source map>"))     Just sm ->       case view (dappSources . sourceLines . at (srcMapFile sm)) dapp' of@@ -976,6 +986,8 @@         Just rows ->           let             subrange = lineSubrange rows (srcMapOffset sm, srcMapLength sm)+            fileName :: Maybe Text+            fileName = preview (dappSources . sourceFiles . ix (srcMapFile sm) . _1) dapp'             lineNo =               (snd . fromJust $                 (srcMapCodePos@@ -983,8 +995,7 @@                  sm)) - 1           in vBox             [ hBorderWithLabel $-                txt (maybe "<unknown>" contractPathPart-                      (preview (uiSolc . _Just . contractName) ui))+                txt (fromMaybe "<unknown>" fileName)                   <+> str (":" ++ show lineNo)                    -- Show the AST node type if present@@ -1007,7 +1018,7 @@                                   ])                 False                 (listMoveTo lineNo-                  (view uiSolidityList ui))+                  (solidityList vm dapp'))             ]  ifTallEnough :: Int -> Widget n -> Widget n -> Widget n

@@ -2,20 +2,26 @@  import Prelude hiding (Word) -import EVM.Concrete+import qualified EVM+import EVM (balance, initialContract) import EVM.FeeSchedule-import EVM.Keccak (keccak) import EVM.Precompiled (execute) import EVM.RLP+import EVM.Symbolic (forceLit)+import EVM.Types (keccak) import EVM.Types +import Control.Lens+ import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString)-import Data.Maybe (isNothing)+import Data.Map (Map)+import Data.Maybe (fromMaybe, isNothing, isJust)  import qualified Data.Aeson        as JSON import qualified Data.Aeson.Types  as JSON import qualified Data.ByteString   as BS+import qualified Data.Map          as Map  data Transaction = Transaction   { txData     :: ByteString,@@ -65,7 +71,7 @@                               rlpWord256 0x0,                               rlpWord256 0x0] -txGasCost :: FeeSchedule Word -> Transaction -> Word+txGasCost :: FeeSchedule Integer -> Transaction -> Integer txGasCost fs tx =   let calldata     = txData tx       zeroBytes    = BS.count 0 calldata@@ -90,3 +96,55 @@     return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value   parseJSON invalid =     JSON.typeMismatch "Transaction" invalid++accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract+accountAt a = (at a) . (to $ fromMaybe newAccount)++touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract+touchAccount a = Map.insertWith (flip const) a newAccount++newAccount :: EVM.Contract+newAccount = initialContract $ EVM.RuntimeCode mempty++-- | Increments origin nonce and pays gas deposit+setupTx :: Addr -> Addr -> Word -> Word -> Map Addr EVM.Contract -> Map Addr EVM.Contract+setupTx origin coinbase gasPrice gasLimit prestate =+  let gasCost = gasPrice * gasLimit+  in (Map.adjust ((over EVM.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

@@ -7,21 +7,28 @@  module EVM.Types where +import Prelude hiding  (Word, LT, GT)+ import Data.Aeson (FromJSON (..), (.:))  #if MIN_VERSION_aeson(1, 0, 0) import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..))+import Data.Aeson #endif -import Data.SBV+import Crypto.Hash+import Data.SBV hiding (Word) import Data.Kind import Data.Monoid ((<>)) import Data.Bifunctor (first) import Data.Char+import Data.List (intercalate)+import Data.Bifunctor (bimap) import Data.ByteString (ByteString) import Data.ByteString.Base16 as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString) import Data.ByteString.Lazy (toStrict)+import Control.Monad.State.Strict (liftM) import qualified Data.ByteString.Char8  as Char8 import Data.DoubleWord import Data.DoubleWord.TH@@ -29,13 +36,15 @@ import Data.Word (Word8) import Numeric (readHex, showHex) import Options.Generic+import Control.Arrow ((>>>)) -import qualified Data.Aeson          as JSON-import qualified Data.Aeson.Types    as JSON-import qualified Data.ByteString     as BS-import qualified Data.Serialize.Get  as Cereal-import qualified Data.Text           as Text-import qualified Data.Text.Encoding  as Text+import qualified Data.ByteArray       as BA+import qualified Data.Aeson           as JSON+import qualified Data.Aeson.Types     as JSON+import qualified Data.ByteString      as BS+import qualified Data.Serialize.Get   as Cereal+import qualified Data.Text            as Text+import qualified Data.Text.Encoding   as Text import qualified Text.Read  -- Some stuff for "generic programming", needed to create Word512@@ -45,31 +54,239 @@ mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256   [''Typeable, ''Data, ''Generic] ++data Buffer+  = ConcreteBuffer ByteString+  | SymbolicBuffer [SWord 8]+ newtype W256 = W256 Word256   deriving     ( Num, Integral, Real, Ord, Enum, Eq     , Bits, FiniteBits, Bounded, Generic     ) --- | convert between (WordN 256) and Word256-type family ToSizzle (t :: Type) :: Type where-    ToSizzle W256 = (WordN 256)-    ToSizzle Addr = (WordN 160)+data Word = C Whiff W256 --maybe to remove completely in the future --- | Conversion from a fixed-sized BV to a sized bit-vector.-class ToSizzleBV a where-   -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector,-   toSizzle :: a -> ToSizzle a+instance Show Word where+  show (C _ x) = show x -   default toSizzle :: (Num (ToSizzle a), Integral a) => (a -> ToSizzle a)-   toSizzle = fromIntegral+instance Read Word where+  readsPrec n s =+    case readsPrec n s of+      [(x, r)] -> [(C (Literal x) x, r)]+      _ -> [] +w256 :: W256 -> Word+w256 w = C (Literal w) w++instance Bits Word where+  (C a x) .&. (C b y) = C (And a b) (x .&. y)+  (C a x) .|. (C b y) = C (Or  a b) (x .|. y)+  (C a x) `xor` (C b y) = C (Todo "xor" [a, b]) (x `xor` y)+  complement (C a x) = C (Neg a) (complement x)+  shiftL (C a x) i = C (SHL a (Literal $ fromIntegral i)) (shiftL x i)+  shiftR (C a x) i = C (SHR a (Literal $ fromIntegral i)) (shiftR x i)+  rotate (C a x) i = C (Todo "rotate " [a]) (rotate x i) -- unused.+  bitSize (C _ x) = bitSize x+  bitSizeMaybe (C _ x) = bitSizeMaybe x+  isSigned (C _ x) = isSigned x+  testBit (C _ x) i = testBit x i+  bit i = w256 (bit i)+  popCount (C _ x) = popCount x++instance FiniteBits Word where+  finiteBitSize (C _ x) = finiteBitSize x+  countLeadingZeros (C _ x) = countLeadingZeros x+  countTrailingZeros (C _ x) = countTrailingZeros x++instance Bounded Word where+  minBound = w256 minBound+  maxBound = w256 maxBound++instance Eq Word where+  (C _ x) == (C _ y) = x == y++instance Enum Word where+  toEnum i = w256 (toEnum i)+  fromEnum (C _ x) = fromEnum x++instance Integral Word where+  quotRem (C _ x) (C _ y) =+    let (a, b) = quotRem x y+    in (w256 a, w256 b)+  toInteger (C _ x) = toInteger x++instance Num Word where+  (C a x) + (C b y) = C (Add a b) (x + y)+  (C a x) * (C b y) = C (Mul a b) (x * y)+  abs (C a x) = C (Todo "abs" [a]) (abs x)+  signum (C a x) = C (Todo "signum" [a]) (signum x)+  fromInteger x = C (Literal (fromInteger x)) (fromInteger x)+  negate (C a x) = C (Sub (Literal 0) a) (negate x)++instance Real Word where+  toRational (C _ x) = toRational x++instance Ord Word where+  compare (C _ x) (C _ y) = compare x y++newtype ByteStringS = ByteStringS ByteString deriving (Eq)++instance Show ByteStringS where+  show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x+    where+      fromBinary =+        Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex++instance Read ByteStringS where+    readsPrec _ ('0':'x':x) = [bimap ByteStringS (Text.unpack . Text.decodeUtf8) bytes]+       where bytes = BS16.decode (Text.encodeUtf8 (Text.pack x))+    readsPrec _ _ = []++instance JSON.ToJSON ByteStringS where+  toJSON = JSON.String . Text.pack . show++-- | Symbolic words of 256 bits, possibly annotated with additional+--   "insightful" information+data SymWord = S Whiff (SWord 256)++instance Show SymWord where+  show (S w _) = show w++var :: String -> SWord 256 -> SymWord+var name x = S (Var name x) x++-- | Custom instances for SymWord, many of which have direct+-- analogues for concrete words defined in Concrete.hs+instance EqSymbolic SymWord where+  (.==) (S _ x) (S _ y) = x .== y++instance Num SymWord where+  (S a x) + (S b y) = S (Add a b) (x + y)+  (S a x) * (S b y) = S (Mul a b) (x * y)+  abs (S a x) = S (Todo "abs" [a]) (abs x)+  signum (S a x) = S (Todo "signum" [a]) (signum x)+  fromInteger x = S (Literal (fromInteger x)) (fromInteger x)+  negate (S a x) = S (Neg a) (negate x)++instance Bits SymWord where+  (S a x) .&. (S b y) = S (And a b) (x .&. y)+  (S a x) .|. (S b y) = S (Or  a b) (x .|. y)+  (S a x) `xor` (S b y) = S (Todo "xor" [a, b]) (x `xor` y)+  complement (S a x) = S (Neg a) (complement x)+  shiftL (S a x) i = S (SHL a (Literal $ fromIntegral i)) (shiftL x i)+  shiftR (S a x) i = S (SHR a (Literal $ fromIntegral i)) (shiftR x i)+  rotate (S a x) i = S (Todo "rotate " [a]) (rotate x i) -- unused.+  bitSize (S _ x) = bitSize x+  bitSizeMaybe (S _ x) = bitSizeMaybe x+  isSigned (S _ x) = isSigned x+  testBit (S _ x) i = testBit x i+  bit i = w256lit (bit i)+  popCount (S _ x) = popCount x++-- sQuotRem and sDivMod are identical for SWord 256+-- prove $ \x y -> x `sQuotRem` (y :: SWord 256) .== x `sDivMod` y+-- Q.E.D.+instance SDivisible SymWord where+  sQuotRem (S x' x) (S y' y) = let (a, b) = x `sQuotRem` y+                               in (S (Div x' y') a, S (Mod x' y') b)+  sDivMod = sQuotRem++-- | Instead of supporting a Mergeable instance directly,+-- we use one which carries the Whiff around:+iteWhiff :: Whiff -> SBool -> SWord 256 -> SWord 256 -> SymWord+iteWhiff w b x y = S w (ite b x y)++instance Bounded SymWord where+  minBound = w256lit minBound+  maxBound = w256lit maxBound++instance Eq SymWord where+  (S _ x) == (S _ y) = x == y++instance Enum SymWord where+  toEnum i = w256lit (toEnum i)+  fromEnum (S _ x) = fromEnum x++-- | This type can give insight into the provenance of a term+-- which is useful, both for the aesthetic purpose of printing+-- terms in a richer way, but also do optimizations on the AST+-- instead of letting the SMT solver do all the heavy lifting.+data Whiff =+  Todo String [Whiff]+  -- booleans / bits+  | And  Whiff Whiff+  | Or   Whiff Whiff+  | Eq   Whiff Whiff+  | LT   Whiff Whiff+  | GT   Whiff Whiff+  | SLT  Whiff Whiff+  | SGT  Whiff Whiff+  | IsZero Whiff+  | ITE Whiff Whiff Whiff+  -- bits+  | SHL Whiff Whiff+  | SHR Whiff Whiff+  | SAR Whiff Whiff++  -- integers+  | Add  Whiff Whiff+  | Sub  Whiff Whiff+  | Mul  Whiff Whiff+  | Div  Whiff Whiff+  | Mod  Whiff Whiff+  | Exp  Whiff Whiff+  | Neg  Whiff+  | FromKeccak Buffer+  | FromBytes Buffer+  | FromStorage Whiff (SArray (WordN 256) (WordN 256))+  | Literal W256+  | Var String (SWord 256)++instance Show Whiff where+  show w =+    let+      infix' s x y = show x ++ s ++ show y+    in case w of+      Todo s args -> s ++ "(" ++ (intercalate "," (show <$> args)) ++ ")"+      And x y     -> infix' " and " x y+      Or x y      -> infix' " or " x y+      ITE b x y  -> "if " ++ show b ++ " then " ++ show x ++ " else " ++ show y+      Eq x y      -> infix' " == " x y+      LT x y      -> infix' " < " x y+      GT x y      -> infix' " > " x y+      SLT x y     -> infix' " s< " x y+      SGT x y     -> infix' " s> " x y+      IsZero x    -> "IsZero(" ++ show x ++ ")"+      SHL x y     -> infix' " << " x y+      SHR x y     -> infix' " << " x y+      SAR x y     -> infix' " a<< " x y+      Add x y     -> infix' " + " x y+      Sub x y     -> infix' " - " x y+      Mul x y     -> infix' " * " x y+      Div x y     -> infix' " / " x y+      Mod x y     -> infix' " % " x y+      Exp x y     -> infix' " ** " x y+      Neg x       -> "not " ++ show x+      Var v _     -> v+      FromKeccak buf -> "keccak(" ++ show buf ++ ")"+      Literal x -> show x+      FromBytes buf -> "FromBuffer " ++ show buf+      FromStorage l _ -> "SLOAD(" ++ show l ++ ")"++newtype Addr = Addr { addressWord160 :: Word160 }+  deriving (Num, Integral, Real, Ord, Enum, Eq, Bits, Generic)++newtype SAddr = SAddr { saddressWord160 :: SWord 160 }+  deriving (Num)+ -- | Capture the correspondence between sized and fixed-sized BVs+-- (This is blatant copypasta of `FromSized` from sbv, which just+-- happens to be defined up to 64 bits) type family FromSizzle (t :: Type) :: Type where    FromSizzle (WordN 256) = W256    FromSizzle (WordN 160) = Addr - -- | Conversion from a sized BV to a fixed-sized bit-vector. class FromSizzleBV a where    -- | Convert a sized bit-vector to the corresponding fixed-sized bit-vector,@@ -78,12 +295,32 @@     default fromSizzle :: (Num (FromSizzle a), Integral a) => a -> FromSizzle a    fromSizzle = fromIntegral- +++maybeLitWord :: SymWord -> Maybe Word+maybeLitWord (S whiff a) = fmap (C whiff . fromSizzle) (unliteral a)++-- | convert between (WordN 256) and Word256+type family ToSizzle (t :: Type) :: Type where+    ToSizzle W256 = (WordN 256)+    ToSizzle Addr = (WordN 160)++-- | Conversion from a fixed-sized BV to a sized bit-vector.+class ToSizzleBV a where+   -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector,+   toSizzle :: a -> ToSizzle a++   default toSizzle :: (Num (ToSizzle a), Integral a) => (a -> ToSizzle a)+   toSizzle = fromIntegral++ instance (ToSizzleBV W256) instance (FromSizzleBV (WordN 256)) instance (ToSizzleBV Addr) instance (FromSizzleBV (WordN 160)) +w256lit :: W256 -> SymWord+w256lit x = S (Literal x) $ literal $ toSizzle x  litBytes :: ByteString -> [SWord 8] litBytes bs = fmap (toSized . literal) (BS.unpack bs)@@ -92,11 +329,11 @@  -- | 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 Show Buffer where+  show (ConcreteBuffer b) = show $ ByteStringS b+  show (SymbolicBuffer b) = show (length b) ++ " bytes" + instance Semigroup Buffer where   ConcreteBuffer a <> ConcreteBuffer b = ConcreteBuffer (a <> b)   ConcreteBuffer a <> SymbolicBuffer b = SymbolicBuffer (litBytes a <> b)@@ -112,12 +349,7 @@   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) -newtype SAddr = SAddr { saddressWord160 :: SWord 160 }-  deriving (Num)- instance Read W256 where   readsPrec _ "0x" = [(0, "")]   readsPrec n s = first W256 <$> readsPrec n s@@ -125,36 +357,37 @@ instance Show W256 where   showsPrec _ s = ("0x" ++) . showHex s +instance JSON.ToJSON W256 where+  toJSON = JSON.String . Text.pack . show++instance JSON.ToJSON Word where+  toJSON (C _ x) = toJSON x+ instance Read Addr where   readsPrec _ ('0':'x':s) = readHex s   readsPrec _ s = readHex s  instance Show Addr where-  showsPrec _ s a =-    let h = showHex s a-    in "0x" ++ replicate (40 - length h) '0' ++ h+  showsPrec _ addr next =+    let hex = showHex addr next+        str = replicate (40 - length hex) '0' ++ hex+    in "0x" ++ toChecksumAddress str  instance Show SAddr where   show (SAddr a) = case unliteral a of     Nothing -> "<symbolic addr>"-    Just c -> show c+    Just c -> show $ fromSizzle c +-- https://eips.ethereum.org/EIPS/eip-55+toChecksumAddress :: String -> String+toChecksumAddress addr = zipWith transform nibbles addr+  where+    nibbles = unpackNibbles . BS.take 20 $ keccakBytes (Char8.pack addr)+    transform nibble = if nibble >= 8 then toUpper else id+ strip0x :: ByteString -> ByteString strip0x bs = if "0x" `Char8.isPrefixOf` bs then Char8.drop 2 bs else bs -newtype ByteStringS = ByteStringS ByteString deriving (Eq)--instance Show ByteStringS where-  show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x-    where-      fromBinary =-        Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex--instance Read ByteStringS where-    readsPrec _ ('0':'x':x) = [(ByteStringS $ fst bytes, Text.unpack . Text.decodeUtf8 $ snd bytes)]-       where bytes = BS16.decode (Text.encodeUtf8 (Text.pack x))-    readsPrec _ _ = []- instance FromJSON W256 where   parseJSON v = do     s <- Text.unpack <$> parseJSON v@@ -242,11 +475,15 @@ padRight :: Int -> ByteString -> ByteString padRight n xs = xs <> BS.replicate (n - BS.length xs) 0 +-- | Right padding  / truncating truncpad :: Int -> [SWord 8] -> [SWord 8] truncpad n xs = if m > n then take n xs                 else mappend xs (replicate (n - m) 0)   where m = length xs +padLeft' :: (Num a) => Int -> [a] -> [a]+padLeft' n xs = replicate (n - length xs) 0 <> xs+ word256 :: ByteString -> Word256 word256 xs = case Cereal.runGet m (padLeft 32 xs) of                Left _ -> error "internal error"@@ -303,4 +540,33 @@ packNibbles :: [Nibble] -> ByteString packNibbles [] = mempty packNibbles (n1:n2:ns) = BS.singleton (toByte n1 n2) <> packNibbles ns-packNibbles _ = error "cant pack odd number of nibbles"+packNibbles _ = error "can't pack odd number of nibbles"++-- Keccak hashing++keccakBytes :: ByteString -> ByteString+keccakBytes =+  (hash :: ByteString -> Digest Keccak_256)+    >>> BA.unpack+    >>> BS.pack++word32 :: [Word8] -> Word32+word32 xs = sum [ fromIntegral x `shiftL` (8*n)+                | (n, x) <- zip [0..] (reverse xs) ]++keccak :: ByteString -> W256+keccak =+  keccakBytes+    >>> BS.take 32+    >>> word++abiKeccak :: ByteString -> Word32+abiKeccak =+  keccakBytes+    >>> BS.take 4+    >>> BS.unpack+    >>> word32+++concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]+concatMapM f xs = liftM concat (mapM f xs)

@@ -1,4 +1,6 @@ {-# Language LambdaCase #-}+{-# Language DataKinds #-}+{-# Language ImplicitParams #-}  module EVM.UnitTest where @@ -13,8 +15,9 @@ import EVM.Exec import EVM.Format import EVM.Solidity+import EVM.SymExec import EVM.Types-import EVM.VMTest+import EVM.Transaction (initTx) import qualified EVM.Fetch  import qualified EVM.FeeSchedule as FeeSchedule@@ -31,14 +34,20 @@ import Control.Monad.Par.IO (runParIO)  import qualified Data.ByteString.Lazy as BSLazy+import qualified Data.SBV.Trans.Control as SBV (Query, getValue, resetAssertions)+import qualified Data.SBV.Internals as SBV (State)+import Data.Binary.Get    (runGet) import Data.ByteString    (ByteString) import Data.SBV    hiding (verbose)-import Data.Either        (isRight)+import Data.SBV.Control   (CheckSatResult(..), checkSat)+import Data.Decimal       (DecimalRaw(..))+import Data.Either        (isRight, lefts) import Data.Foldable      (toList) import Data.Map           (Map) import Data.Maybe         (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe) import Data.Monoid        ((<>)) import Data.Text          (isPrefixOf, stripSuffix, intercalate, Text, pack, unpack)+import Data.Text.Encoding (encodeUtf8) import Data.Word          (Word32) import System.Environment (lookupEnv) import System.IO          (hFlush, stdout)@@ -62,9 +71,12 @@ import Test.QuickCheck hiding (verbose)  data UnitTestOptions = UnitTestOptions-  { oracle     :: Query -> IO (EVM ())+  { oracle     :: EVM.Query -> IO (EVM ())   , verbose    :: Maybe Int   , maxIter    :: Maybe Integer+  , smtTimeout :: Maybe Integer+  , smtState   :: Maybe SBV.State+  , solver     :: Maybe Text   , match      :: Text   , fuzzRuns   :: Int   , replay     :: Maybe (Text, BSLazy.ByteString)@@ -110,8 +122,8 @@  -- | Assuming a constructor is loaded, this stepper will run the constructor -- to create the test contract, give it an initial balance, and run `setUp()'.-initializeUnitTest :: UnitTestOptions -> Stepper ()-initializeUnitTest UnitTestOptions { .. } = do+initializeUnitTest :: UnitTestOptions -> SolcContract -> Stepper ()+initializeUnitTest UnitTestOptions { .. } theContract = do    let addr = testAddress testParams @@ -124,15 +136,19 @@   -- Constructor is loaded; run until it returns code   void Stepper.execFully -  -- Give a balance to the test target   Stepper.evm $ do+    -- Give a balance to the test target     env . contracts . ix addr . balance += w256 (testBalanceCreate testParams) -    -- Initialize the test contract-    setupCall testParams "setUp()" emptyAbi-    popTrace-    pushTrace (EntryTrace "initialize test")+    -- call setUp(), if it exists, to initialize the test contract+    let theAbi = view abiMap theContract+        setUp  = abiKeccak (encodeUtf8 "setUp()") +    when (isJust (Map.lookup setUp theAbi)) $ do+      abiCall testParams "setUp()" emptyAbi+      popTrace+      pushTrace (EntryTrace "setUp()")+   -- Let `setUp()' run to completion   res <- Stepper.execFully   Stepper.evm $ case res of@@ -145,13 +161,13 @@ runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool runUnitTest a method args = do   x <- execTest a method args-  checkFailures a method args x+  checkFailures a method x  execTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool execTest UnitTestOptions { .. } method args = do   -- Set up the call to the test method   Stepper.evm $ do-    setupCall testParams method args+    abiCall testParams method args     pushTrace (EntryTrace method)   -- Try running the test method   Stepper.execFully >>= \case@@ -159,8 +175,8 @@     Left e -> Stepper.evm (pushTrace (ErrorTrace e)) >> pure True     _ -> pure False -checkFailures :: UnitTestOptions -> ABIMethod -> AbiValue -> Bool -> Stepper Bool-checkFailures UnitTestOptions { .. } method args bailed = do+checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool+checkFailures UnitTestOptions { .. } method bailed = do    -- Decide whether the test is supposed to fail or succeed   let shouldFail = "testFail" `isPrefixOf` method   if bailed then@@ -169,8 +185,8 @@     -- Ask whether any assertions failed     Stepper.evm $ do       popTrace-      setupCall testParams "failed()" args-    res <- Stepper.execFully -- >>= \(ConcreteBuffer bs) -> (Stepper.decode AbiBoolType bs)+      abiCall testParams "failed()" emptyAbi+    res <- Stepper.execFully     case res of       Right (ConcreteBuffer r) ->         let AbiBool failed = decodeAbiValue AbiBoolType (BSLazy.fromStrict r)@@ -181,7 +197,7 @@ fuzzTest :: UnitTestOptions -> Text -> [AbiType] -> VM -> Property fuzzTest opts sig types vm = forAllShow (genAbiValue (AbiTupleType $ Vector.fromList types)) (show . ByteStringS . encodeAbiValue)   $ \args -> ioProperty $-    fst <$> runStateT (interpret (oracle opts) (runUnitTest opts sig args)) vm+    fst <$> runStateT (EVM.Stepper.interpret (oracle opts) (runUnitTest opts sig args)) vm  tick :: Text -> IO () tick x = Text.putStr x >> hFlush stdout@@ -196,12 +212,12 @@ srcMapForOpLocation dapp (OpLocation hash opIx) =   case preview (dappSolcByHash . ix hash) dapp of     Nothing -> Nothing-    Just (codeType, solc) ->+    Just (codeType, sol) ->       let         vec =           case codeType of-            Runtime  -> view runtimeSrcmap solc-            Creation -> view creationSrcmap solc+            Runtime  -> view runtimeSrcmap sol+            Creation -> view creationSrcmap sol       in         preview (ix opIx) vec @@ -314,10 +330,10 @@   :: UnitTestOptions   -> Map Text SolcContract   -> SourceCache-  -> (Text, [(Text, [AbiType])])+  -> (Text, [(Test, [AbiType])])   -> IO (MultiSet SrcMap) coverageForUnitTestContract-  opts@(UnitTestOptions {..}) contractMap sources (name, testNames) = do+  opts@(UnitTestOptions {..}) contractMap _ (name, testNames) = do    -- Look for the wanted contract by name from the Solidity info   case preview (ix name) contractMap of@@ -331,20 +347,20 @@       (vm1, cov1) <-         execStateT           (interpretWithCoverage opts-            (Stepper.enter name >> initializeUnitTest opts))+            (Stepper.enter name >> initializeUnitTest opts theContract))           (vm0, mempty)        -- Define the thread spawner for test cases       let-        runOne (testName, _) = spawn_ . liftIO $ do-          (x, (_, cov)) <-+        runOne' (test, _) = spawn_ . liftIO $ do+          (_, (_, cov)) <-             runStateT-              (interpretWithCoverage opts (runUnitTest opts testName emptyAbi))+              (interpretWithCoverage opts (runUnitTest opts (extractSig test) emptyAbi))               (vm1, mempty)           pure cov       -- Run all the test cases in parallel and gather their coverages       covs <--        runParIO (mapM runOne testNames >>= mapM Par.get)+        runParIO (mapM runOne' testNames >>= mapM Par.get)        -- Sum up all the coverage counts       let cov2 = MultiSet.unions (cov1 : covs)@@ -354,14 +370,13 @@ runUnitTestContract   :: UnitTestOptions   -> Map Text SolcContract-  -> SourceCache-  -> (Text, [(Text, [AbiType])])-  -> IO [(Bool, VM)]+  -> (Text, [(Test, [AbiType])])+  -> SBV.Query [(Bool, VM)] runUnitTestContract-  opts@(UnitTestOptions {..}) contractMap sources (name, testSigs) = do+  opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do    -- Print a header-  putStrLn $ "Running " ++ show (length testSigs) ++ " tests for "+  liftIO $ putStrLn $ "Running " ++ show (length testSigs) ++ " tests for "     ++ unpack name    -- Look for the wanted contract by name from the Solidity info@@ -374,25 +389,25 @@       -- Construct the initial VM and begin the contract's constructor       let vm0 = initialUnitTestVm opts theContract       vm1 <--        execStateT-          (interpret oracle-            (Stepper.enter name >> initializeUnitTest opts))+        liftIO $ execStateT+          (EVM.Stepper.interpret oracle+            (Stepper.enter name >> initializeUnitTest opts theContract))           vm0        case view result vm1 of         Nothing -> error "internal error: setUp() did not end with a result"-        Just (VMFailure _) -> do-          Text.putStrLn "\x1b[31m[FAIL]\x1b[0m setUp()"+        Just (VMFailure _) -> liftIO $ do+          Text.putStrLn "\x1b[31m[BAIL]\x1b[0m setUp() "           tick "\n"           tick $ failOutput vm1 opts "setUp()"           pure [(False, vm1)]         Just (VMSuccess _) -> do           let-            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+            runCache :: ([(Either Text Text, VM)], VM) -> (Test, [AbiType])+                        -> SBV.Query ([(Either Text Text, VM)], VM)+            runCache (results, vm) (test, types) = do+              (t, r, vm') <- runTest opts vm (test, types)+              liftIO $ Text.putStrLn t               let vmCached = vm & set (cache . fetched) (view (cache . fetched) vm')               pure (((r, vm'): results), vmCached) @@ -403,17 +418,17 @@           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))+          liftIO $ do+            tick "\n"+            tick (Text.unlines (filter (not . Text.null) running))+            tick (Text.unlines (filter (not . Text.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+runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> SBV.Query (Text, Either Text Text, VM)+runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, []) = liftIO $ runOne opts vm testName emptyAbi+runTest opts@UnitTestOptions{..} vm (ConcreteTest testName, types) = liftIO $ case replay of   Nothing ->     fuzzRun opts vm testName types   Just (sig, callData) ->@@ -421,18 +436,19 @@     then runOne opts vm testName $       decodeAbiValue (AbiTupleType (Vector.fromList types)) callData     else fuzzRun opts vm testName types+runTest opts vm (SymbolicTest testName, types) = symRun opts vm testName types --- | Define the thread spawner for normal test cases +-- | 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))+      (EVM.Stepper.interpret oracle (execTest opts testName args))       vm   (success, vm'') <-     runStateT-      (interpret oracle (checkFailures opts testName args bailed)) vm'+      (EVM.Stepper.interpret oracle (checkFailures opts testName bailed)) vm'   if success   then      let gasSpent = num (testGasCall testParams) - view (state . gas) vm'@@ -444,8 +460,15 @@           , Right (passOutput vm'' opts testName)           , vm''           )-  else+  else if bailed then         pure+          ("\x1b[31m[BAIL]\x1b[0m "+           <> testName <> argInfo+          , Left (failOutput vm'' opts testName)+          , vm''+          )+      else+        pure           ("\x1b[31m[FAIL]\x1b[0m "            <> testName <> argInfo           , Left (failOutput vm'' opts testName)@@ -476,7 +499,7 @@           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+        vm' <- execStateT (EVM.Stepper.interpret oracle (runUnitTest opts testName abiValue)) vm         pure ("\x1b[31m[FAIL]\x1b[0m "                <> testName <> ". Counterexample: " <> ppOutput                <> "\nRun:\n dapp test --replay '(\"" <> testName <> "\",\""@@ -491,8 +514,124 @@               , vm               ) +-- | Define the thread spawner for symbolic tests+-- TODO: return a list of VM's+symRun :: UnitTestOptions -> VM -> Text -> [AbiType] -> SBV.Query (Text, Either Text Text, VM)+symRun opts@UnitTestOptions{..} concreteVm testName types = do+    SBV.resetAssertions+    let vm = symbolify concreteVm+    (cd, cdlen) <- symCalldata testName types []+    let cd' = (SymbolicBuffer cd, w256lit cdlen)+        shouldFail = "proveFail" `isPrefixOf` testName +    -- get all posible postVMs for the test method+    allPaths <- fst <$> runStateT+        (EVM.SymExec.interpret oracle maxIter (execSymTest opts testName cd')) vm+    let consistentPaths = flip filter allPaths $+          \(_, vm') -> case view result vm' of+            Just (VMFailure DeadPath) -> False+            _ -> True+    results <- forM consistentPaths $+      -- If the vm execution succeeded, check if the vm is reachable,+      -- and if any ds-test assertions were triggered+      -- Report a failure depending on the prefix of the test name +      -- If the vm execution failed, check if the vm is reachable, and if so,+      -- report a failure unless the test is supposed to fail.++      \(bailed, vm') -> do+        let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+        SBV.resetAssertions+        constrain $ sAnd (fst <$> view EVM.constraints vm')+        unless bailed $+          case view result vm' of+            Just (VMSuccess (SymbolicBuffer buf)) ->+              constrain $ litBytes (encodeAbiValue $ AbiBool $ not shouldFail) .== buf+            r -> error $ "unexpected return value: " ++ show r+        checkSat >>= \case+          Sat -> do+            prettyCd <- prettyCalldata cd' testName types+            let explorationFailed = case view result vm' of+                  Just (VMFailure e) -> case e of+                                          NotUnique _ -> True+                                          UnexpectedSymbolicArg -> True+                                          _ -> False+                  _ -> False+            return $+              if shouldFail && bailed && not explorationFailed+              then Right ()+              else Left (vm', prettyCd)+          Unsat -> return $ Right ()+          Unk -> return $ Left (vm', "unknown; query timeout")+          DSat _ -> error "Unexpected DSat"++    if null $ lefts results+    then+      return ("\x1b[32m[PASS]\x1b[0m " <> testName, Right "", vm)+    else+      return ("\x1b[31m[FAIL]\x1b[0m " <> testName, Left $ symFailure opts testName (lefts results), vm)++symFailure :: UnitTestOptions -> Text -> [(VM, Text)] -> Text+symFailure UnitTestOptions {..} testName failures' = mconcat+  [ "Failure: "+  , testName+  , "\n\n"+  , intercalate "\n" $ indentLines 2 . mkMsg <$> failures'+  ]+  where+    showRes vm = let Just res = view result vm in+                 case res of+                   VMFailure _ ->+                     let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+                     in prettyvmresult res+                   VMSuccess _ -> if "proveFail" `isPrefixOf` testName+                                  then "Successful execution"+                                  else "Failed: DSTest Assertion Violation"+    mkMsg (vm, cd) = pack $ unlines+      ["Counterexample:"+      ,""+      ,"  result:   " <> showRes vm+      ,"  calldata: " <> unpack cd+      , case verbose of+          Just _ -> unlines+            [ ""+            , unpack $ indentLines 2 (showTraceTree dapp vm)+            ]+          _ -> ""+      ]++prettyCalldata :: (?context :: DappContext) => (Buffer, SymWord) -> Text -> [AbiType]-> SBV.Query Text+prettyCalldata (buffer, S _ cdlen) sig types = do+  cdlen' <- num <$> SBV.getValue cdlen+  cd <- case buffer of+    SymbolicBuffer cd -> mapM (SBV.getValue . fromSized) (take cdlen' cd) <&> BS.pack+    ConcreteBuffer cd -> return $ BS.take cdlen' cd+  pure $ (head (Text.splitOn "(" sig)) <> showCall types (ConcreteBuffer cd)++execSymTest :: UnitTestOptions -> ABIMethod -> (Buffer, SymWord) -> Stepper (Bool, VM)+execSymTest opts@UnitTestOptions{ .. } method cd = do+  -- Set up the call to the test method+  Stepper.evm $ do+    makeTxCall testParams cd+    pushTrace (EntryTrace method)+  -- Try running the test method+  Stepper.runFully >>= \vm' -> case view result vm' of+    Just (VMFailure err) ->+      -- If we failed, put the error in the trace.+      Stepper.evm (pushTrace (ErrorTrace err)) >> (pure (True, vm'))+    Just (VMSuccess _) -> do+      postVm <- checkSymFailures opts+      pure (False, postVm)+    Nothing -> error "Internal Error: execSymTest: vm has not completed execution!"++checkSymFailures :: UnitTestOptions -> Stepper VM+checkSymFailures UnitTestOptions { .. } = do+  -- Ask whether any assertions failed+  Stepper.evm $ do+    popTrace+    abiCall testParams "failed()" emptyAbi+  Stepper.runFully+ indentLines :: Int -> Text -> Text indentLines n s =   let p = Text.replicate n " "@@ -500,92 +639,122 @@  passOutput :: VM -> UnitTestOptions -> Text -> Text passOutput vm UnitTestOptions { .. } testName =-  case verbose of-    Just 2 ->-      mconcat-        [ "Success: "-        , fromMaybe "" (stripSuffix "()" testName)-        , "\n"-        , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm))-        , indentLines 2 (showTraceTree dapp vm)-        , "\n"-        ]-    _ ->-      ""+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  in let v = fromMaybe 0 verbose+  in if (v > 1) then+    mconcat+      [ "Success: "+      , fromMaybe "" (stripSuffix "()" testName)+      , "\n"+      , if (v > 2) then indentLines 2 (showTraceTree dapp vm) else ""+      , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm))+      , "\n"+      ]+    else ""  failOutput :: VM -> UnitTestOptions -> Text -> Text-failOutput vm UnitTestOptions { .. } testName = mconcat+failOutput vm UnitTestOptions { .. } testName =+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  in mconcat   [ "Failure: "   , fromMaybe "" (stripSuffix "()" testName)   , "\n"-  , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm))   , case verbose of       Just _ -> indentLines 2 (showTraceTree dapp vm)       _ -> ""-+  , indentLines 2 (formatTestLogs (view dappEventMap dapp) (view logs vm))+  , "\n"   ] -formatTestLogs :: Map W256 Event -> Seq.Seq Log -> Text+formatTestLogs :: (?context :: DappContext) => Map W256 Event -> Seq.Seq Log -> Text formatTestLogs events xs =   case catMaybes (toList (fmap (formatTestLog events) xs)) of     [] -> "\n"     ys -> "\n" <> intercalate "\n" ys <> "\n\n" -formatTestLog :: Map W256 Event -> Log -> Maybe Text+-- Here we catch and render some special logs emitted by ds-test,+-- with the intent to then present them in a separate view to the+-- regular trace output.+formatTestLog :: (?context :: DappContext) => Map W256 Event -> Log -> Maybe Text formatTestLog _ (Log _ _ []) = Nothing formatTestLog events (Log _ args (topic:_)) =-  case maybeLitWord topic of+  case maybeLitWord topic >>= \t1 -> (Map.lookup (wordValue t1) events) of     Nothing -> Nothing-    Just t -> case (Map.lookup (wordValue t) events) of-                   Nothing -> Nothing-                   Just (Event name _ _) -> case name of-                     "log_bytes32" ->-                       Just $ formatSBytes args+    Just (Event name _ types) ->+      case (name <> parenthesise (abiTypeSolidity <$> (unindexed types))) of+        "log(string)" -> Just $ unquote $ showValue AbiStringType args -                     "log_named_bytes32" ->-                       let key = grab 32 args-                           val = ditch 32 args-                       in Just $ formatSString key <> ": " <> formatSBytes val+        -- log_named_x(string, x)+        "log_named_bytes32(string, bytes32)" -> log_named+        "log_named_address(string, address)" -> log_named+        "log_named_int(string, int256)"      -> log_named+        "log_named_uint(string, uint256)"    -> log_named+        "log_named_bytes(string, bytes)"     -> log_named+        "log_named_string(string, string)"   -> log_named -                     "log_named_address" ->-                       let key = grab 32 args-                           val = ditch 44 args-                       in Just $ formatSString key <> ": " <> formatSBinary val+        -- log_named_decimal_x(string, uint, x)+        "log_named_decimal_int(string, int256, uint256)"   -> log_named_decimal+        "log_named_decimal_uint(string, uint256, uint256)" -> log_named_decimal -                     "log_named_int" ->-                       let key = grab 32 args-                           val = case maybeLitWord (readMemoryWord 32 args) of-                             Just c -> showDec Signed (wordValue c)-                             Nothing -> "<symbolic int>"-                      in Just $ formatSString key <> ": " <> val+        -- log_x(x)+        "log_bytes32(bytes32)" -> log_unnamed+        "log_address(address)" -> log_unnamed+        "log_int(int256)"      -> log_unnamed+        "log_uint(uint256)"    -> log_unnamed+        "log_bytes(bytes)"     -> log_unnamed+        "log_string(string)"   -> log_unnamed -                     "log_named_uint" ->-                       let key = grab 32 args-                           val = case maybeLitWord (readMemoryWord 32 args) of-                             Just c -> showDec Unsigned (wordValue c)-                             Nothing -> "<symbolic uint>"-                       in Just $ formatSString key <> ": " <> val+        -- log_named_x(bytes32, x), as used in older versions of ds-test.+        -- bytes32 are opportunistically represented as strings in Format.hs+        "log_named_bytes32(bytes32, bytes32)" -> log_named+        "log_named_address(bytes32, address)" -> log_named+        "log_named_int(bytes32, int256)"      -> log_named+        "log_named_uint(bytes32, uint256)"    -> log_named --- TODO: event logs (bytes);--- TODO: event log_named_decimal_int  (bytes32 key, int val, uint decimals);--- TODO: event log_named_decimal_uint (bytes32 key, uint val, uint decimals);+        _ -> Nothing -                     _ -> Nothing+        where+          ts = unindexed types+          unquote = Text.dropAround (\c -> c == '"' || c == '«' || c == '»')+          log_unnamed =+            Just $ showValue (head ts) args+          log_named =+            let [key, val] = take 2 (textValues ts args)+            in Just $ unquote key <> ": " <> val+          showDecimal dec val =+            pack $ show $ Decimal (num dec) val+          log_named_decimal =+            case args of+              (ConcreteBuffer b) ->+                case toList $ runGet (getAbiSeq (length ts) ts) (BSLazy.fromStrict b) of+                  [key, (AbiUInt 256 val), (AbiUInt 256 dec)] ->+                    Just $ (unquote (showAbiValue key)) <> ": " <> showDecimal dec val+                  [key, (AbiInt 256 val), (AbiUInt 256 dec)] ->+                    Just $ (unquote (showAbiValue key)) <> ": " <> showDecimal dec val+                  _ -> Nothing+              (SymbolicBuffer _) -> Just "<symbolic decimal>" + word32Bytes :: Word32 -> ByteString word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]] -setupCall :: TestVMParams -> Text -> AbiValue -> EVM ()-setupCall TestVMParams{..} sig args = do+abiCall :: TestVMParams -> Text -> AbiValue -> EVM ()+abiCall params sig args =+  let cd = abiMethod sig args+      l = num . BS.length $ cd+  in makeTxCall params (ConcreteBuffer cd, litWord l)++makeTxCall :: TestVMParams -> (Buffer, SymWord) -> EVM ()+makeTxCall TestVMParams{..} cd = do   resetState   assign (tx . isCreate) False   loadContract testAddress-  assign (state . calldata) (ConcreteBuffer $ abiMethod sig args, literal . num . BS.length $ abiMethod sig args)+  assign (state . calldata) cd   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"+  when (originBal < (w256 testGasprice) * (w256 testGasCall)) $ error "insufficient balance for gas cost"   vm <- get   put $ initTx vm @@ -604,7 +773,7 @@            , vmoptGaslimit = testGasCreate            , vmoptCoinbase = testCoinbase            , vmoptNumber = testNumber-           , vmoptTimestamp = litWord $ w256 $ testTimestamp+           , vmoptTimestamp = litWord $ w256 testTimestamp            , vmoptBlockGaslimit = testGaslimit            , vmoptGasprice = testGasprice            , vmoptMaxCodeSize = testMaxCodeSize@@ -612,7 +781,7 @@            , vmoptSchedule = FeeSchedule.istanbul            , vmoptChainId = testChainId            , vmoptCreate = True-           , vmoptStorageModel = ConcreteS+           , vmoptStorageModel = ConcreteS -- TODO: support RPC            }     creator =       initialContract (RuntimeCode mempty)@@ -622,22 +791,31 @@     & set (env . contracts . at ethrunAddress) (Just creator)  -maybeM :: (Monad m) => b -> (a -> b) -> m (Maybe a) -> m b-maybeM def f mayb = do-  may <- mayb-  return $ maybe def f may+-- | takes a concrete VM and makes all storage symbolic+symbolify :: VM -> VM+symbolify vm =+  vm & over (env . contracts . each . storage) mkSymStorage+     & set (env . storageModel) InitialS+  where+    mkSymStorage :: Storage -> Storage+    mkSymStorage (Symbolic _ _) = error "should not happen"+    mkSymStorage (Concrete s) =+      let+        list = [(literal $ toSizzle k, v) | (C _ k, S _ v) <- Map.toList s]+        symlist = [(litWord k, v) | (k, v) <- Map.toList s]+      in Symbolic symlist $ sListArray 0 list  getParametersFromEnvironmentVariables :: Maybe Text -> IO TestVMParams getParametersFromEnvironmentVariables rpc = do-  block' <- maybeM EVM.Fetch.Latest (EVM.Fetch.BlockNumber . read) (lookupEnv "DAPP_TEST_NUMBER")+  block' <- maybe 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"+        Nothing -> error "Could not fetch block"         Just EVM.Block{..} -> return (  _coinbase-                                      , wordValue $ forceLit $ _timestamp+                                      , wordValue $ forceLit _timestamp                                       , wordValue _number                                       , wordValue _difficulty                                       )

@@ -12,6 +12,8 @@   , checkExpectation   ) where +import Prelude hiding (Word)+ import qualified EVM import EVM (contractcode, storage, origStorage, balance, nonce, Storage(..), initialContract) import qualified EVM.Concrete as EVM@@ -21,8 +23,6 @@ import EVM.Transaction import EVM.Types -import Data.SBV- import Control.Arrow ((***), (&&&)) import Control.Lens import Control.Monad@@ -30,7 +30,7 @@ import Data.Aeson ((.:), FromJSON (..)) import Data.Foldable (fold) import Data.Map (Map)-import Data.Maybe (fromMaybe, isNothing, isJust)+import Data.Maybe (fromMaybe, isNothing) import Data.Witherable (Filterable, catMaybes)  import qualified Data.Map          as Map@@ -63,15 +63,6 @@   , blockchainNetwork :: String   } deriving Show -accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract-accountAt a = (at a) . (to $ fromMaybe newAccount)--touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract-touchAccount a = Map.insertWith (flip const) a newAccount--newAccount :: EVM.Contract-newAccount = initialContract $ EVM.RuntimeCode mempty- splitEithers :: (Filterable f) => f (Either a b) -> (f a, f b) splitEithers =   (catMaybes *** catMaybes)@@ -99,7 +90,7 @@     check = checkContracts x     expected = testExpectation x     actual = view (EVM.env . EVM.contracts . to (fmap (clearZeroStorage.clearOrigStorage))) vm-    printStorage (EVM.Symbolic c) = show c+    printStorage (EVM.Symbolic _ c) = show c     printStorage (EVM.Concrete c) = show $ Map.toList c    putStr (unwords reason)@@ -145,7 +136,7 @@  clearZeroStorage :: EVM.Contract -> EVM.Contract clearZeroStorage c = case view storage c of-  EVM.Symbolic _ -> c+  EVM.Symbolic _ _ -> c   EVM.Concrete m -> let store = Map.filter (\x -> forceLit x /= 0) m                     in set EVM.storage (EVM.Concrete store) c @@ -166,16 +157,16 @@ instance FromJSON EVM.Contract where   parseJSON (JSON.Object v) = do     code <- (EVM.RuntimeCode <$> (hexText <$> v .: "code"))-    storage' <- Map.mapKeys EVM.w256 <$> v .: "storage"+    storage' <- Map.mapKeys 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'+       & balance .~ w256 balance'+       & nonce   .~ w256 nonce'+       & storage .~ EVM.Concrete (fmap (litWord . w256) storage')+       & origStorage .~ fmap w256 storage'    parseJSON invalid =     JSON.typeMismatch "Contract" invalid@@ -251,28 +242,28 @@       []        -> Left NoTxs       _         -> Left TooManyTxs     ([_], _) -> Left OldNetwork-    (_, _)        -> Left TooManyBlocks+    (_, _)   -> Left TooManyBlocks  fromBlockchainCase' :: Block -> Transaction                        -> Map Addr EVM.Contract -> Map Addr EVM.Contract                        -> Either BlockchainError Case fromBlockchainCase' block tx preState postState =   let isCreate = isNothing (txToAddr tx)-  in case (sender 1 tx, checkTx tx block preState) of+  in case (sender 1 tx, checkTx tx 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      = cd-         , vmoptValue         = litWord (EVM.w256 $ txValue tx)+         , vmoptValue         = litWord (w256 $ txValue tx)          , vmoptAddress       = toAddr          , vmoptCaller        = litAddr origin          , vmoptOrigin        = origin          , vmoptGas           = txGasLimit tx - fromIntegral (txGasCost feeSchedule tx)          , vmoptGaslimit      = txGasLimit tx          , vmoptNumber        = blockNumber block-         , vmoptTimestamp     = litWord $ EVM.w256 $ blockTimestamp block+         , vmoptTimestamp     = litWord $ w256 $ blockTimestamp block          , vmoptCoinbase      = blockCoinbase block          , vmoptDifficulty    = blockDifficulty block          , vmoptMaxCodeSize   = 24576@@ -295,7 +286,8 @@                       else maybe (EVM.RuntimeCode mempty) (view contractcode) toCode             cd = if isCreate                  then (mempty, 0)-                 else (ConcreteBuffer $ txData tx, literal . num . BS.length $ txData tx)+                 else let l = num . BS.length $ txData tx+                      in (ConcreteBuffer $ txData tx, litWord l)   validateTx :: Transaction -> Map Addr EVM.Contract -> Maybe ()@@ -303,14 +295,14 @@   origin        <- sender 1 tx   originBalance <- (view balance) <$> view (at origin) cs   originNonce   <- (view nonce)   <$> view (at origin) cs-  let gasDeposit = EVM.w256 $ (txGasPrice tx) * (txGasLimit tx)-  if gasDeposit + (EVM.w256 $ txValue tx) <= originBalance-    && (EVM.w256 $ txNonce tx) == originNonce+  let gasDeposit = w256 $ (txGasPrice tx) * (txGasLimit tx)+  if gasDeposit + (w256 $ txValue tx) <= originBalance+    && (w256 $ txNonce tx) == originNonce   then Just ()   else Nothing -checkTx :: Transaction -> Block -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)-checkTx tx block prestate = do+checkTx :: Transaction -> Map Addr EVM.Contract -> Maybe (Map Addr EVM.Contract)+checkTx tx prestate = do   origin <- sender 1 tx   validateTx tx prestate   let isCreate   = isNothing (txToAddr tx)@@ -330,46 +322,3 @@       & set (EVM.env . EVM.contracts) (checkContracts x)   in     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