hevm 0.50.5 → 0.51.0

raw patch · 34 files changed

+2051/−1580 lines, 34 filesdep +filepatternPVP ok

version bump matches the API change (PVP)

Dependencies added: filepattern

API changes (from Hackage documentation)

Files

• CHANGELOG.md +25/−1
• hevm-cli/hevm-cli.hs +184/−185
• hevm.cabal +3/−2
• src/EVM.hs +118/−444
• src/EVM/ABI.hs +18/−23
• src/EVM/Dapp.hs +10/−12
• src/EVM/Debug.hs +3/−4
• src/EVM/Dev.hs +8/−7
• src/EVM/Expr.hs +12/−4
• src/EVM/Facts.hs +3/−4
• src/EVM/Fetch.hs +18/−36
• src/EVM/Format.hs +104/−41
• src/EVM/Op.hs +0/−83
• src/EVM/SMT.hs +1/−1
• src/EVM/Sign.hs +1/−1
• src/EVM/Solidity.hs +163/−78
• src/EVM/Solvers.hs +1/−1
• src/EVM/Stepper.hs +39/−34
• src/EVM/SymExec.hs +169/−112
• src/EVM/TTY.hs +49/−35
• src/EVM/Transaction.hs +9/−9
• src/EVM/Traversals.hs +7/−8
• src/EVM/Types.hs +670/−176
• src/EVM/UnitTest.hs +45/−46
• test/EVM/Test/BlockchainTests.hs +55/−55
• test/EVM/Test/Tracing.hs +37/−20
• test/EVM/Test/Utils.hs +63/−43
• test/contracts/fail/cheatCodes.sol +15/−0
• test/contracts/fail/dsProveFail.sol +1/−1
• test/contracts/pass/dsProvePass.sol +1/−1
• test/contracts/pass/invariants.sol +1/−1
• test/contracts/pass/rpc.sol +1/−1
• test/rpc.hs +32/−31
• test/test.hs +185/−80

@@ -5,7 +5,31 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [0.50.5] - 2023-03-18+## [0.51.0] - 2023-04-27++## Added++- `hevm` can now execute unit tests in foundry projects. Just run `hevm test` from the root of a foundry repo, and all unit tests will be executed (including prove tests).+- A new stack based loop detection heuristic+- Analysis of partial execution traces is now supported++## Changed++- `hevm dapp-test` has been replaced with `hevm test --project-type DappTools`.+- `hevm test` no longer supports parsing solidity output in the combined json format.+- The default value for `--ask-smt-iterations` has been changed to 1+- The SMT solver is never queried for branch conditions that do not occur in a loop (as determined by the loop detection heuristic)++## Fixed++- `--max-iterations` is respected in cases where path conditions have become inconsistent+- `--max-iterations` is now respected for loops with a concrete branch condition++## Fixed++- Fixed a bug where underflow was possible when transfering eth++## [0.50.5] - 2023-04-18  ## Changed 

@@ -5,8 +5,8 @@  module Main where -import qualified EVM import EVM.Concrete (createAddress)+import EVM (initialContract, makeVm) import qualified EVM.FeeSchedule as FeeSchedule import qualified EVM.Fetch import qualified EVM.Stepper@@ -19,7 +19,8 @@ import EVM.Solidity import EVM.Expr (litAddr) import EVM.Types hiding (word)-import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract, getParametersFromEnvironmentVariables, dappTest)+import EVM.Format (hexByteString, strip0x)+import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract, getParametersFromEnvironmentVariables, unitTest) import EVM.Dapp (findUnitTests, dappInfo, DappInfo, emptyDapp) import GHC.Natural import EVM.Format (showTraceTree, formatExpr)@@ -36,13 +37,13 @@ import Control.Monad              (void, when, forM_, unless) import Control.Monad.State.Strict (liftIO) import Data.ByteString            (ByteString)-import Data.List                  (intercalate, isSuffixOf, intersperse)-import Data.Text                  (unpack, pack)+import Data.List                  (intersperse)+import Data.Text                  (pack) import Data.Maybe                 (fromMaybe, mapMaybe) import Data.Version               (showVersion) import Data.DoubleWord            (Word256) import System.IO                  (stderr)-import System.Directory           (withCurrentDirectory, listDirectory)+import System.Directory           (withCurrentDirectory, getCurrentDirectory) import System.Exit                (exitFailure, exitWith, ExitCode(..))  import qualified Data.ByteString        as ByteString@@ -87,8 +88,8 @@       , cache         :: w ::: Maybe String     <?> "Path to rpc cache repository"    -- symbolic execution opts-      , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"-      , dappRoot      :: w ::: Maybe String       <?> "Path to dapp project root directory (default: . )"+      , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract, Concrete <STORE> (default Abstract)"       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"       , arg           :: w ::: [String]           <?> "Values to encode"@@ -101,8 +102,9 @@       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"       , assertions    :: w ::: Maybe [Word256]    <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"-      , askSmtIterations :: w ::: Maybe Integer   <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"+      , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"       , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"+      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"       }   | Equivalence -- prove equivalence between two programs       { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"@@ -115,41 +117,42 @@       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"-      , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"+      , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"+      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"       }   | Exec -- Execute a given program with specified env & calldata-      { code        :: w ::: Maybe ByteString <?> "Program bytecode"-      , calldata    :: w ::: Maybe ByteString <?> "Tx: calldata"-      , address     :: w ::: Maybe Addr       <?> "Tx: address"-      , caller      :: w ::: Maybe Addr       <?> "Tx: caller"-      , origin      :: w ::: Maybe Addr       <?> "Tx: origin"-      , coinbase    :: w ::: Maybe Addr       <?> "Block: coinbase"-      , value       :: w ::: Maybe W256       <?> "Tx: Eth amount"-      , nonce       :: w ::: Maybe W256       <?> "Nonce of origin"-      , gas         :: w ::: Maybe Word64     <?> "Tx: gas amount"-      , number      :: w ::: Maybe W256       <?> "Block: number"-      , timestamp   :: w ::: Maybe W256       <?> "Block: timestamp"-      , basefee     :: w ::: Maybe W256       <?> "Block: base fee"-      , priorityFee :: w ::: Maybe W256       <?> "Tx: priority fee"-      , gaslimit    :: w ::: Maybe Word64     <?> "Tx: gas limit"-      , gasprice    :: w ::: Maybe W256       <?> "Tx: gas price"-      , create      :: w ::: Bool             <?> "Tx: creation"-      , maxcodesize :: w ::: Maybe W256       <?> "Block: max code size"-      , prevRandao  :: w ::: Maybe W256       <?> "Block: prevRandao"-      , 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"-      , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"-      , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"-      , jsonFile    :: w ::: Maybe String     <?> "Filename or path to dapp build output (default: out/*.solc.json)"-      , dappRoot    :: w ::: Maybe String     <?> "Path to dapp project root directory (default: . )"+      { code        :: w ::: Maybe ByteString  <?> "Program bytecode"+      , calldata    :: w ::: Maybe ByteString  <?> "Tx: calldata"+      , address     :: w ::: Maybe Addr        <?> "Tx: address"+      , caller      :: w ::: Maybe Addr        <?> "Tx: caller"+      , origin      :: w ::: Maybe Addr        <?> "Tx: origin"+      , coinbase    :: w ::: Maybe Addr        <?> "Block: coinbase"+      , value       :: w ::: Maybe W256        <?> "Tx: Eth amount"+      , nonce       :: w ::: Maybe W256        <?> "Nonce of origin"+      , gas         :: w ::: Maybe Word64      <?> "Tx: gas amount"+      , number      :: w ::: Maybe W256        <?> "Block: number"+      , timestamp   :: w ::: Maybe W256        <?> "Block: timestamp"+      , basefee     :: w ::: Maybe W256        <?> "Block: base fee"+      , priorityFee :: w ::: Maybe W256        <?> "Tx: priority fee"+      , gaslimit    :: w ::: Maybe Word64      <?> "Tx: gas limit"+      , gasprice    :: w ::: Maybe W256        <?> "Tx: gas price"+      , create      :: w ::: Bool              <?> "Tx: creation"+      , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"+      , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"+      , 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"+      , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"+      , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"+      , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"+      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"       }-  | 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: . )"+  | Test -- Run DSTest unit tests+      { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"       , 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"@@ -167,7 +170,8 @@       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"       , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"-      , askSmtIterations :: w ::: Maybe Integer         <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"+      , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"+      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"       }   | Version @@ -199,7 +203,7 @@   | x.jsontrace = JsonTrace   | otherwise = Run -applyCache :: (Maybe String, Maybe String) -> IO (EVM.VM -> EVM.VM)+applyCache :: (Maybe String, Maybe String) -> IO (VM -> VM) applyCache (state, cache) =   let applyState = flip Facts.apply       applyCache' = flip Facts.applyCache@@ -217,13 +221,10 @@       stateFacts <- Git.loadFacts (Git.RepoAt statePath)       pure $ (applyState stateFacts) . (applyCache' cacheFacts) -unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> String -> IO UnitTestOptions-unitTestOptions cmd solvers testFile = do-  let root = fromMaybe "." cmd.dappRoot-  srcInfo <- readSolc testFile >>= \case-    Nothing -> error "Could not read .sol.json file"-    Just (contractMap, sourceCache) ->-      pure $ dappInfo root contractMap sourceCache+unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> Maybe BuildOutput -> IO UnitTestOptions+unitTestOptions cmd solvers buildOutput = do+  root <- getRoot cmd+  let srcInfo = maybe emptyDapp (dappInfo root) buildOutput    vmModifier <- applyCache (cmd.state, cmd.cache) @@ -262,47 +263,36 @@ main :: IO () main = do   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"-  let-    root = fromMaybe "." cmd.dappRoot   case cmd of     Version {} -> putStrLn (showVersion Paths.version)-    Symbolic {} -> withCurrentDirectory root $ assert cmd+    Symbolic {} -> do+      root <- getRoot cmd+      withCurrentDirectory root $ assert cmd     Equivalence {} -> equivalence cmd-    Exec {} -> launchExec cmd-    DappTest {} ->+    Exec {} ->+      launchExec cmd+    Test {} -> do+      root <- getRoot cmd       withCurrentDirectory root $ do         cores <- num <$> getNumProcessors         solver <- getSolver cmd         withSolvers solver cores cmd.smttimeout $ \solvers -> do-          testFile <- findJsonFile cmd.jsonFile-          testOpts <- unitTestOptions cmd solvers testFile-          case (cmd.coverage, optsMode cmd) of-            (False, Run) -> do-              res <- dappTest testOpts testFile cmd.cache-              unless res exitFailure-            (False, Debug) -> liftIO $ TTY.main testOpts root testFile-            (False, JsonTrace) -> error "json traces not implemented for dappTest"-            (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) testFile+          buildOut <- readBuildOutput root (getProjectType cmd)+          case buildOut of+            Left e -> do+              putStrLn $ "Error: " <> e+              exitFailure+            Right out -> do+              -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?+              testOpts <- unitTestOptions cmd solvers (Just out)+              case (cmd.coverage, optsMode cmd) of+                (False, Run) -> do+                  res <- unitTest testOpts out.contracts cmd.cache+                  unless res exitFailure+                (False, Debug) -> liftIO $ TTY.main testOpts root (Just out)+                (False, JsonTrace) -> error "json traces not implemented for dappTest"+                (True, _) -> liftIO $ dappCoverage testOpts (optsMode cmd) out -findJsonFile :: Maybe String -> IO String-findJsonFile (Just s) = pure s-findJsonFile Nothing = do-  outFiles <- listDirectory "out"-  case filter (isSuffixOf ".sol.json") outFiles of-    [x] -> pure ("out/" ++ x)-    [] ->-      error $ concat-        [ "No `*.sol.json' file found in `./out'.\n"-        , "Maybe you need to run `dapp build'.\n"-        , "You can specify a file with `--json-file'."-        ]-    xs ->-      error $ concat-        [ "Multiple `*.sol.json' files found in `./out'.\n"-        , "Specify one using `--json-file'.\n"-        , "Files found: "-        , intercalate ", " xs-        ]  equivalence :: Command Options.Unwrapped -> IO () equivalence cmd = do@@ -312,6 +302,7 @@                           , debug = False                           , maxIter = cmd.maxIterations                           , askSmtIters = cmd.askSmtIterations+                          , loopHeuristic = cmd.loopDetectionHeuristic                           , rpcInfo = Nothing                           }   calldata <- buildCalldata cmd@@ -343,18 +334,21 @@                                 exitFailure  getSrcInfo :: Command Options.Unwrapped -> IO DappInfo-getSrcInfo cmd =-  let root = fromMaybe "." cmd.dappRoot-  in case cmd.jsonFile of-    Nothing ->-      pure emptyDapp-    Just json -> readSolc json >>= \case-      Nothing ->-        pure emptyDapp-      Just (contractMap, sourceCache) ->-        pure $ dappInfo root contractMap sourceCache+getSrcInfo cmd = do+  root <- getRoot cmd+  withCurrentDirectory root $ do+    buildOutput <- readBuildOutput root (getProjectType cmd)+    case buildOutput of+      Left _ -> pure emptyDapp+      Right o -> pure $ dappInfo root o +getProjectType :: Command Options.Unwrapped -> ProjectType+getProjectType cmd = fromMaybe Foundry cmd.projectType +getRoot :: Command Options.Unwrapped -> IO FilePath+getRoot cmd = maybe getCurrentDirectory pure (cmd.root)++ -- | Builds a buffer representing calldata based on the given cli arguments buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop]) buildCalldata cmd = case (cmd.calldata, cmd.sig) of@@ -393,7 +387,14 @@         srcInfo         preState     else do-      let opts = VeriOpts { simp = True, debug = cmd.smtdebug, maxIter = cmd.maxIterations, askSmtIters = cmd.askSmtIterations, rpcInfo = rpcinfo}+      let opts = VeriOpts {+        simp = True,+        debug = cmd.smtdebug,+        maxIter = cmd.maxIterations,+        askSmtIters = cmd.askSmtIterations,+        loopHeuristic = cmd.loopDetectionHeuristic,+        rpcInfo = rpcinfo+      }       (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)       case res of         [Qed _] -> do@@ -444,34 +445,29 @@ getTimeout (Timeout c) = Just c getTimeout _ = Nothing -dappCoverage :: UnitTestOptions -> Mode -> String -> IO ()-dappCoverage opts _ solcFile =-  readSolc solcFile >>=-    \case-      Just (contractMap, sourceCache) -> do-        let unitTests = findUnitTests opts.match $ Map.elems contractMap-        covs <- mconcat <$> mapM-          (coverageForUnitTestContract opts contractMap sourceCache) unitTests-        let-          dapp = dappInfo "." contractMap sourceCache-          f (k, vs) = do-            when (shouldPrintCoverage opts.covMatch k) $ do-              putStr ("\x1b[0m" ++ "————— hevm coverage for ") -- Prefixed with color reset-              putStrLn (unpack k ++ " —————")-              putStrLn ""-              forM_ vs $ \(n, bs) -> do-                case ByteString.find (\x -> x /= 0x9 && x /= 0x20 && x /= 0x7d) bs of-                  Nothing -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)-                  Just _ ->-                    case n of-                      -1 -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)-                      0  -> putStr "\x1b[31m" -- Red (Uncovered)-                      _  -> putStr "\x1b[32m" -- Green (Covered)-                Char8.putStrLn bs-              putStrLn ""-        mapM_ f (Map.toList (coverageReport dapp covs))-      Nothing ->-        error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'")+dappCoverage :: UnitTestOptions -> Mode -> BuildOutput -> IO ()+dappCoverage opts _ bo@(BuildOutput (Contracts cs) cache) = do+  let unitTests = findUnitTests opts.match $ Map.elems cs+  covs <- mconcat <$> mapM+    (coverageForUnitTestContract opts cs cache) unitTests+  let+    dapp = dappInfo "." bo+    f (k, vs) = do+      when (shouldPrintCoverage opts.covMatch (T.pack k)) $ do+        putStr ("\x1b[0m" ++ "————— hevm coverage for ") -- Prefixed with color reset+        putStrLn (k ++ " —————")+        putStrLn ""+        forM_ vs $ \(n, bs) -> do+          case ByteString.find (\x -> x /= 0x9 && x /= 0x20 && x /= 0x7d) bs of+            Nothing -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)+            Just _ ->+              case n of+                -1 -> putStr "\x1b[38;5;240m" -- Gray (Coverage status isn't relevant)+                0  -> putStr "\x1b[31m" -- Red (Uncovered)+                _  -> putStr "\x1b[32m" -- Green (Covered)+          Char8.putStrLn bs+        putStrLn ""+  mapM_ f (Map.toList (coverageReport dapp covs))  shouldPrintCoverage :: Maybe Text -> Text -> Bool shouldPrintCoverage (Just covMatch) file = regexMatches covMatch file@@ -494,18 +490,19 @@         vm' <- EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully         when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')         case vm'.result of-          Nothing ->-            error "internal error; no EVM result"-          Just (EVM.VMFailure (EVM.Revert msg)) -> do+          Just (VMFailure (Revert msg)) -> do             let res = case msg of                         ConcreteBuf bs -> bs                         _ -> "<symbolic>"             putStrLn $ "Revert: " <> (show $ ByteStringS res)             exitWith (ExitFailure 2)-          Just (EVM.VMFailure err) -> do+          Just (VMFailure err) -> do             putStrLn $ "Error: " <> show err             exitWith (ExitFailure 2)-          Just (EVM.VMSuccess buf) -> do+          Just (Unfinished p) -> do+            putStrLn $ "Could not continue execution: " <> show p+            exitWith (ExitFailure 2)+          Just (VMSuccess buf) -> do             let msg = case buf of                   ConcreteBuf msg' -> msg'                   _ -> "<symbolic>"@@ -518,6 +515,8 @@               Nothing -> pure ()               Just path ->                 Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts vm'.cache)+          _ ->+            error "Internal error: no EVM result"        Debug -> void $ TTY.runFromVM solvers rpcinfo Nothing dapp vm       --JsonTrace -> void $ execStateT (interpretWithTrace fetcher EVM.Stepper.runFully) vm@@ -526,7 +525,7 @@            rpcinfo = (,) block <$> cmd.rpc  -- | Creates a (concrete) VM from command line options-vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM+vmFromCommand :: Command Options.Unwrapped -> IO VM vmFromCommand cmd = do   withCache <- applyCache (cmd.state, cmd.cache) @@ -534,7 +533,7 @@     Nothing -> return (0,Lit 0,0,0,0)     Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case       Nothing -> error "Could not fetch block"-      Just EVM.Block{..} -> return ( coinbase+      Just Block{..} -> return ( coinbase                                    , timestamp                                    , baseFee                                    , number@@ -550,7 +549,7 @@           -- if both code and url is given,           -- fetch the contract and overwrite the code           return $-            EVM.initialContract  (mkCode $ hexByteString "--code" $ strip0x c)+            initialContract  (mkCode $ hexByteString "--code" $ strip0x c)               & set #balance  (contract.balance)               & set #nonce    (contract.nonce)               & set #external (contract.external)@@ -563,12 +562,12 @@      (_, _, Just c)  ->       return $-        EVM.initialContract (mkCode $ hexByteString "--code" $ strip0x c)+        initialContract (mkCode $ hexByteString "--code" $ strip0x c)      (_, _, Nothing) ->       error "must provide at least (rpc + address) or code" -  let ts' = case unlit ts of+  let ts' = case maybeLitWord ts of         Just t -> t         Nothing -> error "unexpected symbolic timestamp when executing vm test" @@ -581,49 +580,49 @@         calldata = ConcreteBuf $ bytes (.calldata) ""         decipher = hexByteString "bytes" . strip0x         mkCode bs = if cmd.create-                    then EVM.InitCode bs mempty-                    else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)+                    then InitCode bs mempty+                    else RuntimeCode (ConcreteRuntimeCode bs)         address = if cmd.create               then addr (.address) (createAddress origin (word (.nonce) 0))               else addr (.address) 0xacab -        vm0 baseFee miner ts blockNum prevRan c = EVM.makeVm $ EVM.VMOpts-          { contract       = c-          , calldata       = (calldata, [])-          , value          = Lit value-          , address        = address-          , caller         = litAddr caller-          , origin         = origin-          , gas            = word64 (.gas) 0xffffffffffffffff-          , baseFee        = baseFee-          , priorityFee    = word (.priorityFee) 0-          , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff-          , coinbase       = addr (.coinbase) miner-          , number         = word (.number) blockNum-          , timestamp      = Lit $ word (.timestamp) ts-          , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff-          , gasprice       = word (.gasprice) 0-          , maxCodeSize    = word (.maxcodesize) 0xffffffff-          , prevRandao     = word (.prevRandao) prevRan-          , schedule       = FeeSchedule.berlin-          , chainId        = word (.chainid) 1-          , create         = (.create) cmd+        vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts+          { contract      = c+          , calldata      = (calldata, [])+          , value         = Lit value+          , address       = address+          , caller        = litAddr caller+          , origin        = origin+          , gas           = word64 (.gas) 0xffffffffffffffff+          , baseFee       = baseFee+          , priorityFee   = word (.priorityFee) 0+          , gaslimit      = word64 (.gaslimit) 0xffffffffffffffff+          , coinbase      = addr (.coinbase) miner+          , number        = word (.number) blockNum+          , timestamp     = Lit $ word (.timestamp) ts+          , blockGaslimit = word64 (.gaslimit) 0xffffffffffffffff+          , gasprice      = word (.gasprice) 0+          , maxCodeSize   = word (.maxcodesize) 0xffffffff+          , prevRandao    = word (.prevRandao) prevRan+          , schedule      = FeeSchedule.berlin+          , chainId       = word (.chainid) 1+          , create        = (.create) cmd           , initialStorage = EmptyStore-          , txAccessList   = mempty -- TODO: support me soon-          , allowFFI       = False+          , txAccessList  = mempty -- TODO: support me soon+          , allowFFI      = False           }         word f def = fromMaybe def (f cmd)         word64 f def = fromMaybe def (f cmd)         addr f def = fromMaybe def (f cmd)         bytes f def = maybe def decipher (f cmd) -symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (EVM.VM)+symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM) symvmFromCommand cmd calldata = do   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of     Nothing -> return (0,0,0,0)     Just url -> EVM.Fetch.fetchBlockFrom block url >>= \case       Nothing -> error "Could not fetch block"-      Just EVM.Block{..} -> return ( coinbase+      Just Block{..} -> return ( coinbase                                    , number                                    , baseFee                                    , prevRandao@@ -648,7 +647,7 @@               Nothing -> contract'               -- if both code and url is given,               -- fetch the contract and overwrite the code-              Just c -> EVM.initialContract (mkCode $ decipher c)+              Just c -> initialContract (mkCode $ decipher c)                         -- TODO: fix this                         -- & set EVM.origStorage (view EVM.origStorage contract')                         & set #balance     (contract'.balance)@@ -656,7 +655,7 @@                         & set #external    (contract'.external)      (_, _, Just c)  ->-      return (EVM.initialContract . mkCode $ decipher c)+      return (initialContract . mkCode $ decipher c)     (_, _, Nothing) ->       error "must provide at least (rpc + address) or code" @@ -668,35 +667,35 @@     block   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block     origin  = addr (.origin) 0     mkCode bs = if cmd.create-                   then EVM.InitCode bs mempty-                   else EVM.RuntimeCode (EVM.ConcreteRuntimeCode bs)+                   then InitCode bs mempty+                   else RuntimeCode (ConcreteRuntimeCode bs)     address = if cmd.create           then addr (.address) (createAddress origin (word (.nonce) 0))           else addr (.address) 0xacab-    vm0 baseFee miner ts blockNum prevRan cd callvalue caller c = EVM.makeVm $ EVM.VMOpts-      { contract       = c-      , calldata       = cd-      , value          = callvalue-      , address        = address-      , caller         = caller-      , origin         = origin-      , gas            = word64 (.gas) 0xffffffffffffffff-      , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff-      , baseFee        = baseFee-      , priorityFee    = word (.priorityFee) 0-      , coinbase       = addr (.coinbase) miner-      , number         = word (.number) blockNum-      , timestamp      = ts-      , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff-      , gasprice       = word (.gasprice) 0-      , maxCodeSize    = word (.maxcodesize) 0xffffffff-      , prevRandao     = word (.prevRandao) prevRan-      , schedule       = FeeSchedule.berlin-      , chainId        = word (.chainid) 1-      , create         = (.create) cmd+    vm0 baseFee miner ts blockNum prevRan cd callvalue caller c = makeVm $ VMOpts+      { contract      = c+      , calldata      = cd+      , value         = callvalue+      , address       = address+      , caller        = caller+      , origin        = origin+      , gas           = word64 (.gas) 0xffffffffffffffff+      , gaslimit      = word64 (.gaslimit) 0xffffffffffffffff+      , baseFee       = baseFee+      , priorityFee   = word (.priorityFee) 0+      , coinbase      = addr (.coinbase) miner+      , number        = word (.number) blockNum+      , timestamp     = ts+      , blockGaslimit = word64 (.gaslimit) 0xffffffffffffffff+      , gasprice      = word (.gasprice) 0+      , maxCodeSize   = word (.maxcodesize) 0xffffffff+      , prevRandao    = word (.prevRandao) prevRan+      , schedule      = FeeSchedule.berlin+      , chainId       = word (.chainid) 1+      , create        = (.create) cmd       , initialStorage = maybe AbstractStore parseInitialStorage (cmd.initialStorage)-      , txAccessList   = mempty-      , allowFFI       = False+      , txAccessList  = mempty+      , allowFFI      = False       }     word f def = fromMaybe def (f cmd)     addr f def = fromMaybe def (f cmd)

@@ -2,7 +2,7 @@ name:   hevm version:-  0.50.5+  0.51.0 synopsis:   Ethereum virtual machine evaluator description:@@ -185,7 +185,8 @@     word-wrap                         >= 0.5 && < 0.6,     spool                             >= 0.1 && < 0.2,     stm                               >= 2.5.0 && < 2.6.0,-    spawn                             >= 0.3 && < 0.4+    spawn                             >= 0.3 && < 0.4,+    filepattern                       >= 0.1.2 && < 0.2   if !os(windows)     build-depends:       brick                           >= 1.4 && < 1.5,

@@ -1,21 +1,17 @@ {-# Language ImplicitParams #-} {-# Language UndecidableInstances #-}-{-# Language TemplateHaskell #-} {-# Language ScopedTypeVariables #-} {-# Language GADTs #-} {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE TypeApplications #-}  module EVM where  import Prelude hiding (log, exponent, GT, LT)  import Optics.Core-import Optics.TH import Optics.State import Optics.State.Operators import Optics.Zoom@@ -30,7 +26,7 @@ import EVM.Op import EVM.Precompiled qualified import EVM.Solidity-import EVM.Types hiding (IllegalOverflow, Error)+import EVM.Types import EVM.Sign qualified  import Control.Monad.State.Strict hiding (state)@@ -46,7 +42,7 @@ import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.Maybe (fromMaybe, fromJust)-import Data.Set (Set, insert, member, fromList)+import Data.Set (insert, member, fromList) import Data.Sequence (Seq) import Data.Sequence qualified as Seq import Data.Text (unpack)@@ -54,325 +50,16 @@ import Data.Tree import Data.Tree.Zipper qualified as Zipper import Data.Tuple.Curry-import Data.Vector qualified as RegularVector+import Data.Typeable import Data.Vector qualified as V-import Data.Vector.Storable (Vector)-import Data.Vector.Storable qualified as Vector-import Data.Vector.Storable.Mutable qualified as Vector+import Data.Vector.Storable qualified as SV+import Data.Vector.Storable.Mutable qualified as SV import Data.Word (Word8, Word32, Word64)-import Options.Generic as Options  import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) --- * Data types---- | EVM failure modes-data Error-  = BalanceTooLow W256 W256-  | UnrecognizedOpcode Word8-  | SelfDestruction-  | StackUnderrun-  | BadJumpDestination-  | Revert (Expr Buf)-  | OutOfGas Word64 Word64-  | BadCheatCode FunctionSelector-  | StackLimitExceeded-  | IllegalOverflow-  | Query Query-  | Choose Choose-  | StateChangeWhileStatic-  | InvalidMemoryAccess-  | CallDepthLimitReached-  | MaxCodeSizeExceeded W256 W256-  | InvalidFormat-  | PrecompileFailure-  | forall a . UnexpectedSymbolicArg Int String [Expr a]-  | DeadPath-  | NotUnique (Expr EWord)-  | SMTTimeout-  | FFI [AbiValue]-  | ReturnDataOutOfBounds-  | NonceOverflow-deriving instance Show Error---- | The possible result states of a VM-data VMResult-  = VMFailure Error -- ^ An operation failed-  | VMSuccess (Expr Buf) -- ^ Reached STOP, RETURN, or end-of-code--deriving instance Show VMResult---- | The state of a stepwise EVM execution-data VM = VM-  { result         :: Maybe VMResult-  , state          :: FrameState-  , frames         :: [Frame]-  , env            :: Env-  , block          :: Block-  , tx             :: TxState-  , logs           :: [Expr Log]-  , traces         :: Zipper.TreePos Zipper.Empty Trace-  , cache          :: Cache-  , burned         :: {-# UNPACK #-} !Word64-  , iterations     :: Map CodeLocation Int-  , constraints    :: [Prop]-  , keccakEqs      :: [Prop]-  , allowFFI       :: Bool-  , overrideCaller :: Maybe Addr-  }-  deriving (Show, Generic)--data Trace = Trace-  { opIx      :: Int-  , contract  :: Contract-  , tracedata :: TraceData-  }-  deriving (Show, Generic)--data TraceData-  = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]-  | FrameTrace FrameContext-  | QueryTrace Query-  | ErrorTrace Error-  | EntryTrace Text-  | ReturnTrace (Expr Buf) FrameContext-  deriving (Show, Generic)---- | Queries halt execution until resolved through RPC calls or SMT queries-data Query where-  PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query-  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM ()) -> Query-  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query-  PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query--data Choose where-  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM ()) -> Choose--instance Show Query where-  showsPrec _ = \case-    PleaseFetchContract addr _ ->-      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)-    PleaseFetchSlot addr slot _ ->-      (("<EVM.Query: fetch slot "-        ++ show slot ++ " for "-        ++ show addr ++ ">") ++)-    PleaseAskSMT condition constraints _ ->-      (("<EVM.Query: ask SMT about "-        ++ show condition ++ " in context "-        ++ show constraints ++ ">") ++)-    PleaseDoFFI cmd _ ->-      (("<EVM.Query: do ffi: " ++ (show cmd)) ++)--instance Show Choose where-  showsPrec _ = \case-    PleaseChoosePath _ _ ->-      (("<EVM.Choice: waiting for user to select path (0,1)") ++)---- | Alias for the type of e.g. @exec1@.-type EVM a = State VM a--type CodeLocation = (Addr, Int)---- | The possible return values of a SMT query-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-  { fetchedContracts :: Map Addr Contract,-    fetchedStorage :: Map W256 (Map W256 W256),-    path :: Map (CodeLocation, Int) Bool-  } deriving (Show, Generic)---- | A way to specify an initial VM state-data VMOpts = VMOpts-  { contract :: Contract-  , calldata :: (Expr Buf, [Prop])-  , initialStorage :: Expr Storage-  , value :: Expr EWord-  , priorityFee :: W256-  , address :: Addr-  , caller :: Expr EWord-  , origin :: Addr-  , gas :: Word64-  , gaslimit :: Word64-  , number :: W256-  , timestamp :: Expr EWord-  , coinbase :: Addr-  , prevRandao :: W256-  , maxCodeSize :: W256-  , blockGaslimit :: Word64-  , gasprice :: W256-  , baseFee :: W256-  , schedule :: FeeSchedule Word64-  , chainId :: W256-  , create :: Bool-  , txAccessList :: Map Addr [W256]-  , allowFFI :: Bool-  } deriving Show----- | An entry in the VM's "call/create stack"-data Frame = Frame-  { context :: FrameContext-  , state   :: FrameState-  }-  deriving (Show)---- | Call/create info-data FrameContext-  = CreationContext-    { address         :: Addr-    , codehash        :: Expr EWord-    , createreversion :: Map Addr Contract-    , substate        :: SubState-    }-  | CallContext-    { target        :: Addr-    , context       :: Addr-    , offset        :: W256-    , size          :: W256-    , codehash      :: Expr EWord-    , abi           :: Maybe W256-    , calldata      :: Expr Buf-    , callreversion :: (Map Addr Contract, Expr Storage)-    , subState      :: SubState-    }-  deriving (Show, Generic)---- | The "registers" of the VM along with memory and data stack-data FrameState = FrameState-  { contract     :: Addr-  , codeContract :: Addr-  , code         :: ContractCode-  , pc           :: {-# UNPACK #-} !Int-  , stack        :: [Expr EWord]-  , memory       :: Expr Buf-  , memorySize   :: Word64-  , calldata     :: Expr Buf-  , callvalue    :: Expr EWord-  , caller       :: Expr EWord-  , gas          :: {-# UNPACK #-} !Word64-  , returndata   :: Expr Buf-  , static       :: Bool-  }-  deriving (Show, Generic)---- | The state that spans a whole transaction-data TxState = TxState-  { gasprice    :: W256-  , gaslimit    :: Word64-  , priorityFee :: W256-  , origin      :: Addr-  , toAddr      :: Addr-  , value       :: Expr EWord-  , substate    :: SubState-  , isCreate    :: Bool-  , txReversion :: Map Addr Contract-  }-  deriving (Show)---- | The "accrued substate" across a transaction-data SubState = SubState-  { selfdestructs       :: [Addr]-  , touchedAccounts     :: [Addr]-  , accessedAddresses   :: Set Addr-  , accessedStorageKeys :: Set (Addr, W256)-  , refunds             :: [(Addr, Word64)]-  -- 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-  by instructions like @EXTCODEHASH@, so we distinguish these two-  code types.--  The definition follows the structure of code output by solc. We need to use-  some heuristics here to deal with symbolic data regions that may be present-  in the bytecode since the fully abstract case is impractical:--  - initcode has concrete code, followed by an abstract data "section"-  - runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)--  hopefully we do not have to deal with dynamic immutable before we get a real data section...--}-data ContractCode-  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation-  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation-  deriving (Show, Ord)---- | We have two variants here to optimize the fully concrete case.--- ConcreteRuntimeCode just wraps a ByteString--- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).-data RuntimeCode-  = ConcreteRuntimeCode ByteString-  | SymbolicRuntimeCode (V.Vector (Expr Byte))-  deriving (Show, Eq, Ord)---- runtime err when used for symbolic code-instance Eq ContractCode where-  InitCode a b  == InitCode c d  = a == c && b == d-  RuntimeCode x == RuntimeCode y = x == y-  _ == _ = False---- | The state of a contract-data Contract = Contract-  { contractcode :: ContractCode-  , balance      :: W256-  , nonce        :: W256-  , codehash     :: Expr EWord-  , opIxMap      :: Vector Int-  , codeOps      :: RegularVector.Vector (Int, Op)-  , external     :: Bool-  }-  deriving (Show)---- | Various environmental data-data Env = Env-  { contracts    :: Map Addr Contract-  , chainId      :: W256-  , storage      :: Expr Storage-  , origStorage  :: Map W256 (Map W256 W256)-  , sha3Crack    :: Map W256 ByteString-  }-  deriving (Show, Generic)----- | Data about the block-data Block = Block-  { coinbase    :: Addr-  , timestamp   :: Expr EWord-  , number      :: W256-  , prevRandao  :: W256-  , gaslimit    :: Word64-  , baseFee     :: W256-  , maxCodeSize :: W256-  , schedule    :: FeeSchedule Word64-  } deriving (Show, Generic)---makeFieldLabelsNoPrefix ''VM-makeFieldLabelsNoPrefix ''FrameState-makeFieldLabelsNoPrefix ''TxState-makeFieldLabelsNoPrefix ''SubState-makeFieldLabelsNoPrefix ''Cache-makeFieldLabelsNoPrefix ''Trace-makeFieldLabelsNoPrefix ''VMOpts-makeFieldLabelsNoPrefix ''Frame-makeFieldLabelsNoPrefix ''FrameContext-makeFieldLabelsNoPrefix ''Contract-makeFieldLabelsNoPrefix ''Env-makeFieldLabelsNoPrefix ''Block- blankState :: FrameState blankState = FrameState   { contract     = 0@@ -398,35 +85,6 @@         f (RuntimeCode (ConcreteRuntimeCode bs)) = ConcreteBuf bs         f (RuntimeCode (SymbolicRuntimeCode ops)) = Expr.fromList ops -instance Semigroup Cache where-  a <> b = Cache-    { fetchedContracts = Map.unionWith unifyCachedContract a.fetchedContracts b.fetchedContracts-    , fetchedStorage = Map.unionWith unifyCachedStorage a.fetchedStorage b.fetchedStorage-    , path = mappend a.path b.path-    }--unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256-unifyCachedStorage _ _ = undefined---- only intended for use in Cache merges, where we expect--- everything to be Concrete-unifyCachedContract :: Contract -> Contract -> Contract-unifyCachedContract _ _ = undefined-  {--unifyCachedContract a b = a & set storage merged-  where merged = case (view storage a, view storage b) of-                   (ConcreteStore sa, ConcreteStore sb) ->-                     ConcreteStore (mappend sa sb)-                   _ ->-                     view storage a-   -}--instance Monoid Cache where-  mempty = Cache { fetchedContracts = mempty,-                   fetchedStorage = mempty,-                   path = mempty-                 }- -- * Data accessors  currentContract :: VM -> Maybe Contract@@ -560,11 +218,12 @@                   touchAccount self                   out <- use (#state % #returndata)                   finishFrame (FrameReturned out)-              e -> vmError $-                UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" [e]+              e -> partial $+                     UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])             _ ->               underrun-      e -> vmError $ UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" [e]+      e -> partial $+             UnexpectedSymbolicArg vm.state.pc "cannot call precompiles with symbolic data" (wrap [e])    else if vm.state.pc >= opslen vm.state.code     then doStop@@ -575,7 +234,7 @@                   RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc                   RuntimeCode (SymbolicRuntimeCode ops) ->                     fromMaybe (error "could not analyze symbolic code") $-                      unlitByte $ ops V.! vm.state.pc+                      maybeLitByte $ ops V.! vm.state.pc        case getOp(?op) of @@ -807,7 +466,7 @@                     next                     assign (#state % #stack) xs -                    let jump True = vmError EVM.ReturnDataOutOfBounds+                    let jump True = vmError ReturnDataOutOfBounds                         jump False = copyBytesToMemory vm.state.returndata xSize' xFrom xTo'                      case (xFrom, bufLength vm.state.returndata) of@@ -979,7 +638,7 @@             x:xs ->               burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->                 case toInt x' of-                  Nothing -> vmError EVM.BadJumpDestination+                  Nothing -> vmError BadJumpDestination                   Just i -> checkJump i xs             _ -> underrun @@ -990,14 +649,11 @@                   let jump :: Bool -> EVM ()                       jump False = assign (#state % #stack) xs >> next                       jump _    = case toInt x' of-                        Nothing -> vmError EVM.BadJumpDestination+                        Nothing -> vmError BadJumpDestination                         Just i -> checkJump i xs-                  in case maybeLitWord y of-                    Just y' -> jump (0 /= y')-                    -- if the jump condition is symbolic, we explore both sides-                    Nothing -> do-                      loc <- codeloc-                      branch loc y jump+                  in do+                    loc <- codeloc+                    branch loc y jump             _ -> underrun          OpPc ->@@ -1062,9 +718,9 @@                       assign #caller (litAddr from')                       assign #contract callee                     assign #overrideCaller Nothing-                    transfer from' callee xValue-                    touchAccount self+                    touchAccount from'                     touchAccount callee+                    transfer from' callee xValue             _ ->               underrun @@ -1089,7 +745,7 @@                 let                   output = readMemory xOffset' xSize' vm                   codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data")-                               . unlit . bufLength $ output+                               . maybeLitWord . bufLength $ output                   maxsize = vm.block.maxCodeSize                   creation = case vm.frames of                     [] -> vm.tx.isCreate@@ -1192,13 +848,20 @@             _ -> underrun          OpUnknown xxx ->-          vmError (UnrecognizedOpcode xxx)+          vmError $ UnrecognizedOpcode xxx  transfer :: Addr -> Addr -> W256 -> EVM ()-transfer xFrom xTo xValue =-  zoom (#env % #contracts) $ do-    (ix xFrom % #balance) %= (subtract xValue)-    (ix xTo % #balance) %= (+ xValue)+transfer _ _ 0 = pure ()+transfer xFrom xTo xValue = do+    sb <- preuse $ #env % #contracts % ix xFrom % #balance+    case sb of+      Just srcBal ->+        if xValue > srcBal+        then vmError $ BalanceTooLow xValue srcBal+        else do+          (#env % #contracts % ix xFrom % #balance) %= (subtract xValue)+          (#env % #contracts % ix xTo % #balance) %= (+ xValue)+      Nothing -> vmError $ BalanceTooLow xValue 0  -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc. callChecks@@ -1220,7 +883,7 @@         then do           assign (#state % #stack) (Lit 0 : xs)           assign (#state % #returndata) mempty-          pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance+          pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)           next         else if length vm.frames >= 1024              then do@@ -1258,7 +921,7 @@               transfer self recipient xValue               touchAccount self               touchAccount recipient-          _ -> vmError $ UnexpectedSymbolicArg pc' "unexpected return value from precompile" [x]+          _ -> partial $ UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [x])         _ -> underrun       _ -> pure () @@ -1452,24 +1115,28 @@ getCodeLocation :: VM -> CodeLocation getCodeLocation vm = (vm.state.contract, vm.state.pc) +query :: Query -> EVM ()+query = assign #result . Just . HandleEffect . Query++choose :: Choose -> EVM ()+choose = assign #result . Just . HandleEffect . Choose+ branch :: CodeLocation -> Expr EWord -> (Bool -> EVM ()) -> EVM () branch loc cond continue = do   pathconds <- use #constraints-  assign #result . Just . VMFailure . Query $ PleaseAskSMT cond pathconds choosePath+  query $ PleaseAskSMT cond pathconds choosePath   where     choosePath (Case v) = do       assign #result Nothing       pushTo #constraints $ if v then (cond ./= Lit 0) else (cond .== Lit 0)-      iteration <- use (#iterations % at loc % non 0)+      (iteration, _) <- use (#iterations % at loc % non (0,[]))+      stack <- use (#state % #stack)       assign (#cache % #path % at (loc, iteration)) (Just v)-      assign (#iterations % at loc) (Just (iteration + 1))+      assign (#iterations % at loc) (Just (iteration + 1, stack))       continue v     -- Both paths are possible; we ask for more input     choosePath Unknown =-      assign #result . Just . VMFailure . Choose . PleaseChoosePath cond $ choosePath . Case-    -- None of the paths are possible; fail this branch-    choosePath Inconsistent = vmError DeadPath-+      choose . PleaseChoosePath cond $ choosePath . Case  -- | Construct RPC Query and halt execution until resolved fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()@@ -1482,7 +1149,7 @@           assign (#env % #contracts % at addr) (Just c)           continue c         Nothing -> do-          assign (#result) . Just . VMFailure $ Query $+          assign (#result) . Just . HandleEffect . Query $             PleaseFetchContract addr               (\c -> do assign (#cache % #fetchedContracts % at addr) (Just c)                         assign (#env % #contracts % at addr) (Just c)@@ -1518,7 +1185,7 @@       fetchAccount addr $ \_ ->         accessStorage addr slot continue   where-      mkQuery s = assign #result . Just . VMFailure . Query $+      mkQuery s = query $                     PleaseFetchSlot addr s                       (\x -> do                           modifying (#cache % #fetchedStorage % ix (num addr)) (Map.insert s x)@@ -1550,9 +1217,7 @@     revertSubstate   = assign (#tx % #substate) (SubState mempty mempty mempty mempty mempty)    use #result >>= \case-    Nothing ->-      error "Finalising an unfinished tx."-    Just (VMFailure (EVM.Revert _)) -> do+    Just (VMFailure (Revert _)) -> do       revertContracts       revertSubstate     Just (VMFailure _) -> do@@ -1574,9 +1239,12 @@         _ ->           case Expr.toList output of             Nothing ->-              vmError $ UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" [output]+              partial $+                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" (wrap [output])             Just ops ->               onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)+    _ ->+      error "Finalising an unfinished tx."    -- compute and pay the refund to the caller and the   -- corresponding payment to the miner@@ -1601,7 +1269,7 @@   -- pay out the block reward, recreating the miner if necessary   preuse (#env % #contracts % ix block.coinbase) >>= \case     Nothing -> modifying (#env % #contracts)-      (Map.insert block.coinbase (initialContract (EVM.RuntimeCode (ConcreteRuntimeCode ""))))+      (Map.insert block.coinbase (initialContract (RuntimeCode (ConcreteRuntimeCode ""))))     Just _  -> noop   modifying (#env % #contracts)     (Map.adjust (over #balance (+ blockReward)) block.coinbase)@@ -1639,7 +1307,7 @@ limitStack n continue = do   stk <- use (#state % #stack)   if length stk + n > 1024-    then vmError EVM.StackLimitExceeded+    then vmError StackLimitExceeded     else continue  notStatic :: EVM () -> EVM ()@@ -1665,7 +1333,7 @@ forceConcrete n msg continue = case maybeLitWord n of   Nothing -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [n]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])   Just c -> continue c  forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM ()) -> EVM ()@@ -1673,41 +1341,41 @@   (Just c, Just d) -> continue (c, d)   _ -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [n, m]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])  forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM ()) -> EVM () forceConcrete3 (k,n,m) msg continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of   (Just c, Just d, Just f) -> continue (c, d, f)   _ -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, n, m]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, n, m])  forceConcrete4 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256) -> EVM ()) -> EVM () forceConcrete4 (k,l,n,m) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of   (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)   _ -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, n, m]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, n, m])  forceConcrete5 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256) -> EVM ()) -> EVM () forceConcrete5 (k,l,m,n,o) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of   (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)   _ -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, m, n, o]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o])  forceConcrete6 :: (Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256, W256, W256, W256) -> EVM ()) -> EVM () forceConcrete6 (k,l,m,n,o,p) msg continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of   (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)   _ -> do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [k, l, m, n, o, p]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o, p])  forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM ()) -> EVM () forceConcreteBuf (ConcreteBuf b) _ continue = continue b forceConcreteBuf b msg _ = do     vm <- get-    vmError $ UnexpectedSymbolicArg vm.state.pc msg [b]+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])  -- * Substate manipulation refund :: Word64 -> EVM ()@@ -1776,7 +1444,7 @@     abi = readBytes 4 (Lit inOffset) mem     input = readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4) vm   case maybeLitWord abi of-    Nothing -> vmError $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" [abi]+    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])     Just (fromIntegral -> abi') ->       case Map.lookup abi' cheatActions of         Nothing ->@@ -1809,12 +1477,12 @@                       assign (#state % #returndata) encoded                       copyBytesToMemory encoded outSize (Lit 0) outOffset                       assign #result Nothing-                  in assign #result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont))+                  in query (PleaseDoFFI cmd cont)                 _ -> vmError (BadCheatCode sig)               _ -> vmError (BadCheatCode sig)           else             let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"-            in vmError . EVM.Revert . ConcreteBuf $+            in vmError . Revert . ConcreteBuf $               abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]),        action "warp(uint256)" $@@ -1850,7 +1518,7 @@             forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do               let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')                   encoded = encodeAbiValue $-                    AbiTuple (RegularVector.fromList+                    AbiTuple (V.fromList                       [ AbiUInt 8 $ num v                       , AbiBytes 32 (word256Bytes r)                       , AbiBytes 32 (word256Bytes s)@@ -1913,7 +1581,7 @@                                     , subState  = vm0.tx.substate                                     , abi =                                         if xInSize >= 4-                                        then case unlit $ readBytes 4 (Lit xInOffset) vm0.state.memory+                                        then case maybeLitWord $ readBytes 4 (Lit xInOffset) vm0.state.memory                                              of Nothing -> Nothing                                                 Just abi -> Just $ num abi                                         else Nothing@@ -1999,11 +1667,11 @@           prefixLen <- Expr.concPrefix initCode           prefix <- Expr.toList $ Expr.take (num prefixLen) initCode           let sym = Expr.drop (num prefixLen) initCode-          conc <- mapM unlitByte prefix+          conc <- mapM maybeLitByte prefix           pure $ InitCode (BS.pack $ V.toList conc) sym     case contract' of       Nothing ->-        vmError $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []+        partial $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []       Just c -> do         let           newContract = initialContract c@@ -2081,17 +1749,23 @@  -- * VM error implementation -vmError :: Error -> EVM ()+vmError :: EvmError -> EVM () vmError e = finishFrame (FrameErrored e) +partial :: PartialExec -> EVM ()+partial e = assign #result (Just (Unfinished e))++wrap :: Typeable a => [Expr a] -> [SomeExpr]+wrap = fmap SomeExpr+ underrun :: EVM ()-underrun = vmError EVM.StackUnderrun+underrun = vmError StackUnderrun  -- | A stack frame can be popped in three ways. data FrameResult   = FrameReturned (Expr Buf) -- ^ STOP, RETURN, or no more code   | FrameReverted (Expr Buf) -- ^ REVERT-  | FrameErrored Error -- ^ Any other error+  | FrameErrored EvmError -- ^ Any other error   deriving Show  -- | This function defines how to pop the current stack frame in either of@@ -2108,7 +1782,7 @@     [] -> do       case how of           FrameReturned output -> assign #result . Just $ VMSuccess output-          FrameReverted buffer -> assign #result . Just $ VMFailure (EVM.Revert buffer)+          FrameReverted buffer -> assign #result . Just $ VMFailure (Revert buffer)           FrameErrored e       -> assign #result . Just $ VMFailure e       finalize @@ -2121,7 +1795,7 @@           FrameErrored e ->             ErrorTrace e           FrameReverted e ->-            ErrorTrace (EVM.Revert e)+            ErrorTrace (Revert e)           FrameReturned output ->             ReturnTrace output nextFrame.context       -- Pop to the previous level of the debug trace stack.@@ -2212,11 +1886,11 @@                   onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)                 _ ->                   case Expr.toList output of-                    Nothing -> vmError $+                    Nothing -> partial $                       UnexpectedSymbolicArg                         oldVm.state.pc                         "runtime code cannot have an abstract length"-                        [output]+                        (wrap [output])                     Just newCode -> do                       onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode) @@ -2300,7 +1974,7 @@   pure Trace     { tracedata = x     , contract = this-    , opIx = fromMaybe 0 $ this.opIxMap Vector.!? vm.state.pc+    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc     }  pushTrace :: TraceData -> EVM ()@@ -2399,27 +2073,27 @@  checkJump :: Int -> [Expr EWord] -> EVM () checkJump x xs = do-  theCode <- use (#state % #code)-  self <- use (#state % #codeContract)-  codeOps <- preuse (#env % #contracts % ix self % #codeOps)-  opIxMap <- preuse (#env % #contracts % ix self % #opIxMap)-  case (codeOps, opIxMap) of-    (Just co, Just opMap) -> do-      let op = case theCode of-            InitCode ops _ -> BS.indexMaybe ops x-            RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x-            RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= unlitByte-      case op of-        Nothing -> vmError EVM.BadJumpDestination-        Just b ->-          if 0x5b == b && OpJumpdest == snd (co RegularVector.! (opMap Vector.! num x))-             then do-               #state % #stack .= xs-               #state % #pc .= num x-             else-               vmError EVM.BadJumpDestination-    (_, _) -> error "Internal Error: self not found in current contracts"+  vm <- get+  case isValidJumpDest vm x of+    True -> do+      #state % #stack .= xs+      #state % #pc .= num x+    False -> vmError BadJumpDestination +isValidJumpDest :: VM -> Int -> Bool+isValidJumpDest vm x = let+    code = vm.state.code+    self = vm.state.codeContract+    contract = fromMaybe+      (error "Internal Error: self not found in current contracts")+      (Map.lookup self vm.env.contracts)+    op = case code of+      InitCode ops _ -> BS.indexMaybe ops x+      RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x+      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte+  in case op of+       Nothing -> False+       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! num x))  opSize :: Word8 -> Int opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2@@ -2428,9 +2102,9 @@ --  i of the resulting vector contains the operation index for -- the program counter value i.  This is needed because source map -- entries are per operation, not per byte.-mkOpIxMap :: ContractCode -> Vector Int+mkOpIxMap :: ContractCode -> SV.Vector Int mkOpIxMap (InitCode conc _)-  = Vector.create $ Vector.new (BS.length conc) >>= \v ->+  = SV.create $ SV.new (BS.length conc) >>= \v ->       -- Loop over the byte string accumulating a vector-mutating action.       -- This is somewhat obfuscated, but should be fast.       let (_, _, _, m) = BS.foldl' (go v) (0 :: Word8, 0, 0, pure ()) conc@@ -2438,34 +2112,34 @@       where         -- concrete case         go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =-          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)+          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> SV.write v i j)         go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)         go v (0, !i, !j, !m) _ =-          {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)+          {- Other op. -}         (0,            i + 1, j + 1, m >> SV.write v i j)         go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)  mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =   mkOpIxMap (InitCode ops mempty) -- a bit hacky  mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))-  = Vector.create $ Vector.new (length ops) >>= \v ->+  = SV.create $ SV.new (length ops) >>= \v ->       let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)       in m >> pure v       where-        go v (0, !i, !j, !m) x = case unlitByte x of+        go v (0, !i, !j, !m) x = case maybeLitByte x of           Just x' -> if x' >= 0x60 && x' <= 0x7f             -- start of PUSH op ---                     then (x' - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)+                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)             -- other data ---                     else (0,             i + 1, j + 1, m >> Vector.write v i j)+                     else (0,             i + 1, j + 1, m >> SV.write v i j)           _ -> error $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j          go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)         go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)   vmOp :: VM -> Maybe Op@@ -2478,7 +2152,7 @@         RuntimeCode (ConcreteRuntimeCode xs') ->           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')         RuntimeCode (SymbolicRuntimeCode xs') ->-          ( fromMaybe (error "unexpected symbolic code") . unlitByte $ xs' V.! i , V.toList $ V.drop i xs')+          ( fromMaybe (error "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')   in if (opslen code' < i)      then Nothing      else Just (readOp op pushdata)@@ -2486,10 +2160,10 @@ vmOpIx :: VM -> Maybe Int vmOpIx vm =   do self <- currentContract vm-     self.opIxMap Vector.!? vm.state.pc+     self.opIxMap SV.!? vm.state.pc  -- Maps operation indicies into a pair of (bytecode index, operation)-mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)+mkCodeOps :: ContractCode -> V.Vector (Int, Op) mkCodeOps contractCode =   let l = case contractCode of             InitCode bytes _ ->@@ -2498,14 +2172,14 @@               LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)             RuntimeCode (SymbolicRuntimeCode ops) ->               stripBytecodeMetadataSym $ V.toList ops-  in RegularVector.fromList . toList $ go 0 l+  in V.fromList . toList $ go 0 l   where     go !i !xs =       case uncons xs of         Nothing ->           mempty         Just (x, xs') ->-          let x' = fromMaybe (error "unexpected symbolic code argument") $ unlitByte x+          let x' = fromMaybe (error "unexpected symbolic code argument") $ maybeLitByte x               j = opSize x'           in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs) 

@@ -68,11 +68,11 @@ import Data.Char          (isHexDigit) import Data.DoubleWord    (Word256, Int256, signedWord) import Data.Functor       (($>))-import Data.Text          (Text, pack, unpack)-import Data.Text.Encoding (encodeUtf8, decodeUtf8')+import Data.Text          (Text)+import Data.List          (intercalate)+import Data.Text.Encoding (encodeUtf8) import Data.Vector        (Vector, toList) import Data.Word          (Word32)-import Data.List          (intercalate) import Data.Maybe         (mapMaybe) import GHC.Generics @@ -90,6 +90,7 @@ import qualified Text.Megaparsec      as P import qualified Text.Megaparsec.Char as P + data AbiValue   = AbiUInt         Int Word256   | AbiInt          Int Int256@@ -121,12 +122,6 @@     "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")"   show (AbiFunction b)       = show (ByteStringS b) -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@@ -156,6 +151,20 @@ data SolError  = SolError Text [AbiType]   deriving (Show, Ord, Eq, Generic) +abiTypeSolidity :: AbiType -> Text+abiTypeSolidity = \case+  AbiUIntType n         -> "uint" <> Text.pack (show n)+  AbiIntType n          -> "int" <> Text.pack (show n)+  AbiAddressType        -> "address"+  AbiBoolType           -> "bool"+  AbiBytesType n        -> "bytes" <> Text.pack (show n)+  AbiBytesDynamicType   -> "bytes"+  AbiStringType         -> "string"+  AbiArrayDynamicType t -> abiTypeSolidity t <> "[]"+  AbiArrayType n t      -> abiTypeSolidity t <> "[" <> Text.pack (show n) <> "]"+  AbiTupleType ts       -> "(" <> (Text.intercalate "," . Vector.toList $ abiTypeSolidity <$> ts) <> ")"+  AbiFunctionType       -> "function"+ abiKind :: AbiType -> AbiKind abiKind = \case   AbiBytesDynamicType   -> Dynamic@@ -178,20 +187,6 @@   AbiArray n t _      -> AbiArrayType n t   AbiTuple v          -> AbiTupleType (abiValueType <$> v)   AbiFunction _       -> AbiFunctionType--abiTypeSolidity :: AbiType -> Text-abiTypeSolidity = \case-  AbiUIntType n         -> "uint" <> pack (show n)-  AbiIntType n          -> "int" <> pack (show n)-  AbiAddressType        -> "address"-  AbiBoolType           -> "bool"-  AbiBytesType n        -> "bytes" <> pack (show n)-  AbiBytesDynamicType   -> "bytes"-  AbiStringType         -> "string"-  AbiArrayDynamicType t -> abiTypeSolidity t <> "[]"-  AbiArrayType n t      -> abiTypeSolidity t <> "[" <> pack (show n) <> "]"-  AbiTupleType ts       -> "(" <> (Text.intercalate "," . Vector.toList $ abiTypeSolidity <$> ts) <> ")"-  AbiFunctionType       -> "function"  getAbi :: AbiType -> Get AbiValue getAbi t = label (Text.unpack (abiTypeSolidity t)) $

@@ -1,11 +1,10 @@ module EVM.Dapp where -import EVM (Trace(..), ContractCode(..), Contract(..), RuntimeCode (..))-import EVM.ABI (Event, AbiType, SolError) import EVM.Concrete import EVM.Debug (srcMapCodePos) import EVM.Solidity-import EVM.Types (W256, abiKeccak, keccak', Addr, regexMatches, unlit, unlitByte, FunctionSelector)+import EVM.Types+import EVM.ABI  import Control.Arrow ((>>>)) import Data.Aeson (Value)@@ -52,11 +51,10 @@ instance Show Test where   show t = unpack $ extractSig t -dappInfo-  :: FilePath -> Map Text SolcContract -> SourceCache -> DappInfo-dappInfo root solcByName sources =+dappInfo :: FilePath -> BuildOutput -> DappInfo+dappInfo root (BuildOutput (Contracts cs) sources) =   let-    solcs = Map.elems solcByName+    solcs = Map.elems cs     astIds = astIdMap $ snd <$> Map.toList sources.asts     immutables = filter ((/=) mempty . (.immutableReferences)) solcs @@ -64,7 +62,7 @@     { root = root     , unitTests = findAllUnitTests solcs     , sources = sources-    , solcByName = solcByName+    , solcByName = cs     , solcByHash =         let           f g k = Map.fromList [(g x, (k, x)) | x <- solcs]@@ -85,7 +83,7 @@     }  emptyDapp :: DappInfo-emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty)+emptyDapp = dappInfo "" mempty  -- Dapp unit tests are detected by searching within abi methods -- that begin with "test" or "prove", that are in a contract with@@ -153,7 +151,7 @@  findSrc :: Contract -> DappInfo -> Maybe SolcContract findSrc c dapp = do-  hash <- unlit c.codehash+  hash <- maybeLitWord c.codehash   case Map.lookup hash dapp.solcByHash of     Just (_, v) -> Just v     Nothing -> lookupCode c.contractcode dapp@@ -167,7 +165,7 @@     Just x -> return x     Nothing -> snd <$> find (compareCode c . fst) a.solcByCode lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let-    code = BS.pack $ mapMaybe unlitByte $ V.toList c+    code = BS.pack $ mapMaybe maybeLitByte $ V.toList c   in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of     Just x -> return x     Nothing -> snd <$> find (compareCode code . fst) a.solcByCode@@ -187,4 +185,4 @@       case srcMapCodePos dapp.sources sm of         Nothing -> Left "<source not found>"         Just (fileName, lineIx) ->-          Right (fileName <> ":" <> pack (show lineIx))+          Right (pack fileName <> ":" <> pack (show lineIx))

@@ -2,16 +2,15 @@  module EVM.Debug where -import EVM          (Contract, bytecode)+import EVM          (bytecode) import EVM.Solidity (SrcMap(..), SourceCache(..))-import EVM.Types    (Addr)+import EVM.Types    (Contract, Addr) import EVM.Expr     (bufLength)  import Control.Arrow   (second) import Optics.Core import Data.ByteString (ByteString) import Data.Map        (Map)-import Data.Text       (Text)  import qualified Data.ByteString       as ByteString import qualified Data.Map              as Map@@ -43,7 +42,7 @@     (map (\(a, b) -> (text (show a), prettyContract b))      (Map.toList x)) -srcMapCodePos :: SourceCache -> SrcMap -> Maybe (Text, Int)+srcMapCodePos :: SourceCache -> SrcMap -> Maybe (FilePath, Int) srcMapCodePos cache sm =   fmap (second f) $ cache.files ^? ix sm.file   where

@@ -43,24 +43,25 @@   withCurrentDirectory root $ do     cores <- num <$> getNumProcessors     let testFile = root <> "/out/dapp.sol.json"+    Right (BuildOutput contracts _) <- readSolc DappTools root testFile     withSolvers Z3 cores Nothing $ \solvers -> do       opts <- testOpts solvers root testFile-      res <- dappTest opts testFile Nothing+      res <- unitTest opts contracts Nothing       unless res exitFailure  testOpts :: SolverGroup -> FilePath -> FilePath -> IO UnitTestOptions testOpts solvers root testFile = do-  srcInfo <- readSolc testFile >>= \case-    Nothing -> error "Could not read .sol.json file"-    Just (contractMap, sourceCache) ->-      pure $ dappInfo root contractMap sourceCache+  srcInfo <- readSolc DappTools root testFile >>= \case+    Left e -> error e+    Right out ->+      pure $ dappInfo root out    params <- getParametersFromEnvironmentVariables Nothing   pure EVM.UnitTest.UnitTestOptions     { EVM.UnitTest.solvers = solvers     , EVM.UnitTest.rpcInfo = Nothing     , EVM.UnitTest.maxIter = Nothing-    , EVM.UnitTest.askSmtIters = Nothing+    , EVM.UnitTest.askSmtIters = 1     , EVM.UnitTest.smtTimeout = Nothing     , EVM.UnitTest.smtDebug = False     , EVM.UnitTest.solver = Nothing@@ -402,7 +403,7 @@  -- | Builds the Expr for the given evm bytecode object buildExpr :: SolverGroup -> ByteString -> IO (Expr End)-buildExpr solvers bs = interpret (Fetch.oracle solvers Nothing) Nothing Nothing (initVm bs) runExpr+buildExpr solvers bs = interpret (Fetch.oracle solvers Nothing) Nothing 1 Naive (initVm bs) runExpr  dai :: IO ByteString dai = do

@@ -275,7 +275,7 @@ readWordFromBytes i@(Lit idx) buf = let     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]   in if Prelude.and . (fmap isLitByte) $ bytes-     then Lit (bytesToW256 . mapMaybe unlitByte $ bytes)+     then Lit (bytesToW256 . mapMaybe maybeLitByte $ bytes)      else ReadWord i buf readWordFromBytes idx buf = ReadWord idx buf @@ -341,7 +341,7 @@     sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]]     tl = BS.drop (num dstOffset + num size) dst     in if Prelude.and . (fmap isLitByte) $ sl-       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe unlitByte) $ sl) <> tl+       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByte) $ sl) <> tl        else CopySlice s d sz src ds   | otherwise = CopySlice s d sz src ds @@ -495,7 +495,7 @@  fromList :: V.Vector (Expr Byte) -> Expr Buf fromList bs = case Prelude.and (fmap isLitByte bs) of-  True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe unlitByte $ bs+  True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByte $ bs   -- we want to minimize the size of the resulting expresion, so we do two passes:   --   1. write all concrete bytes to some base buffer   --   2. write all symbolic writes on top of this buffer@@ -796,6 +796,14 @@     go o@(LT (Max (Lit a) _) (Lit b))       | a >= b = Lit 0       | otherwise = o+    go o@(SLT (Sub (Max (Lit a) _) (Lit b)) (Lit c))+      = let sa, sb, sc :: Int256+            sa = fromIntegral a+            sb = fromIntegral b+            sc = fromIntegral c+        in if sa >= sb && sa - sb >= sc+           then Lit 0+           else o      go a = a @@ -947,7 +955,7 @@  joinBytes :: [Expr Byte] -> Expr EWord joinBytes bs-  | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe unlitByte) $ bs+  | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByte) $ bs   | otherwise = let       bytes = padBytesLeft 32 bs     in JoinBytes

@@ -32,10 +32,9 @@   , fileToFact   ) where -import EVM          (VM, Contract, Cache) import EVM          (bytecode)-import EVM.Types    (Addr, W256, Expr(..), num) import EVM.Expr     (writeStorage, litAddr)+import EVM.Types  import qualified EVM @@ -160,7 +159,7 @@ apply1 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (#env % #contracts % at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))+      assign (#env % #contracts % at addr) (Just (EVM.initialContract (RuntimeCode (ConcreteRuntimeCode blob))))       when (vm.state.contract == addr) $ EVM.loadContract addr     StorageFact {..} ->       vm & over (#env % #storage) (writeStorage (litAddr addr) (Lit which) (Lit what))@@ -173,7 +172,7 @@ apply2 vm fact =   case fact of     CodeFact    {..} -> flip execState vm $ do-      assign (#cache % #fetchedContracts % at addr) (Just (EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode blob))))+      assign (#cache % #fetchedContracts % at addr) (Just (EVM.initialContract (RuntimeCode (ConcreteRuntimeCode blob))))       when (vm.state.contract == addr) $ EVM.loadContract addr     StorageFact {..} -> let         store = vm.cache.fetchedStorage

@@ -6,14 +6,13 @@ import Prelude hiding (Word)  import EVM.ABI-import EVM.Types    (Addr, W256, hexText, Expr(Lit), Expr(..), Prop(..), (.&&), (./=)) import EVM.SMT import EVM.Solvers-import EVM          (EVM, Contract, Block, initialContract)+import EVM.Types+import EVM.Format (hexText)+import EVM        (initialContract) import qualified EVM.FeeSchedule as FeeSchedule -import qualified EVM- import Optics.Core  import Control.Monad.Trans.Maybe@@ -115,7 +114,7 @@   return x  -parseBlock :: (AsValue s, Show s) => s -> Maybe EVM.Block+parseBlock :: (AsValue s, Show s) => s -> Maybe Block parseBlock j = do   coinbase   <- readText <$> j ^? key "miner" % _String   timestamp  <- Lit . readText <$> j ^? key "timestamp" % _String@@ -135,7 +134,7 @@      (Nothing, Just _, Just d) -> d      _ -> error "Internal Error: block contains both difficulty and prevRandao"   -- default codesize, default gas limit, default feescedule-  return $ EVM.Block coinbase timestamp number prd gasLimit (fromMaybe 0 baseFee) 0xffffffff FeeSchedule.berlin+  return $ Block coinbase timestamp number prd gasLimit (fromMaybe 0 baseFee) 0xffffffff FeeSchedule.berlin  fetchWithSession :: Text -> Session -> Value -> IO (Maybe Value) fetchWithSession url sess x = do@@ -154,7 +153,7 @@   theBalance <- MaybeT $ fetch (QueryBalance addr)    return $-    initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode theCode))+    initialContract (RuntimeCode (ConcreteRuntimeCode theCode))       & set #nonce    theNonce       & set #balance  theBalance       & set #external True@@ -203,46 +202,29 @@ oracle :: SolverGroup -> RpcInfo -> Fetcher oracle solvers info q = do   case q of-    EVM.PleaseDoFFI vals continue -> case vals of+    PleaseDoFFI vals continue -> case vals of        cmd : args -> do           (_, stdout', _) <- readProcessWithExitCode cmd args ""           pure . continue . encodeAbiValue $             AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout'])        _ -> error (show vals) -    EVM.PleaseAskSMT branchcondition pathconditions continue -> do+    PleaseAskSMT branchcondition pathconditions continue -> do          let pathconds = foldl' PAnd (PBool True) pathconditions          -- Is is possible to satisfy the condition?          continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds      -- if we are using a symbolic storage model,     -- we generate a new array to the fetched contract here-    EVM.PleaseFetchContract addr continue -> do+    PleaseFetchContract addr continue -> do       contract <- case info of-                    Nothing -> return $ Just $ initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))+                    Nothing -> return $ Just $ initialContract (RuntimeCode (ConcreteRuntimeCode ""))                     Just (n, url) -> fetchContractFrom n url addr       case contract of         Just x -> return $ continue x         Nothing -> error ("oracle error: " ++ show q) -    --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 ->+    PleaseFetchSlot addr slot continue ->       case info of         Nothing -> return (continue 0)         Just (n, url) ->@@ -251,29 +233,29 @@            Nothing ->              error ("oracle error: " ++ show q) -type Fetcher = EVM.Query -> IO (EVM ())+type Fetcher = Query -> IO (EVM ())  -- | Checks which branches are satisfiable, checking the pathconditions for consistency -- if the third argument is true. -- When in debug mode, we do not want to be able to navigate to dead paths, -- but for normal execution paths with inconsistent pathconditions -- will be pruned anyway.-checkBranch :: SolverGroup -> Prop -> Prop -> IO EVM.BranchCondition+checkBranch :: SolverGroup -> Prop -> Prop -> IO BranchCondition checkBranch solvers branchcondition pathconditions = do   checkSat solvers (assertProps [(branchcondition .&& pathconditions)]) >>= \case      -- the condition is unsatisfiable      Unsat -> -- if pathconditions are consistent then the condition must be false-            return $ EVM.Case False+            return $ Case False      -- Sat means its possible for condition to hold      Sat _ -> -- is its negation also possible?             checkSat solvers (assertProps [(pathconditions .&& (PNeg branchcondition))]) >>= \case                -- No. The condition must hold-               Unsat -> return $ EVM.Case True+               Unsat -> return $ Case True                -- Yes. Both branches possible-               Sat _ -> return EVM.Unknown+               Sat _ -> return EVM.Types.Unknown                -- Explore both branches in case of timeout-               Unknown -> return EVM.Unknown+               EVM.Solvers.Unknown -> return EVM.Types.Unknown                Error e -> error $ "Internal Error: SMT Solver returned with an error: " <> T.unpack e      -- If the query times out, we simply explore both paths-     Unknown -> return EVM.Unknown+     EVM.Solvers.Unknown -> return EVM.Types.Unknown      Error e -> error $ "Internal Error: SMT Solver returned with an error: " <> T.unpack e

@@ -3,6 +3,8 @@  module EVM.Format   ( formatExpr+  , formatSomeExpr+  , formatPartial   , contractNamePart   , contractPathPart   , showError@@ -22,20 +24,22 @@   , formatBytes   , formatBinary   , indent+  , strip0x+  , strip0x'+  , hexByteString+  , hexText+  , bsToHex   ) where  import Prelude hiding (Word) -import EVM qualified-import EVM (VM, cheatCode, traceForest, Error (..), Trace, TraceData(..), Query(..), FrameContext(..))-import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError (..),-  Indexed (NotIndexed), getAbiSeq, parseTypeName, formatString)+import EVM.Types+import EVM (cheatCode, traceForest)+import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..)) import EVM.Dapp (DappContext(..), DappInfo(..), showTraceLocation) import EVM.Expr qualified as Expr-import EVM.Hexdump (prettyHex)+import EVM.Hexdump (prettyHex, paddedShowHex) import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap)-import EVM.Types (maybeLitWord, W256(..),num, word, Expr(..), EType(..), Addr,-  ByteStringS(..), Error(..), FunctionSelector)  import Control.Arrow ((>>>)) import Optics.Core@@ -48,14 +52,17 @@ import Data.Char qualified as Char import Data.DoubleWord (signedWord) import Data.Foldable (toList)+import Data.List (isPrefixOf) import Data.Map qualified as Map import Data.Maybe (catMaybes, fromMaybe, fromJust) import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn) import Data.Text qualified as T-import Data.Text.Encoding (decodeUtf8, decodeUtf8')+import Data.Text.Encoding qualified as T import Data.Tree.View (showTree) import Data.Vector (Vector) import Numeric (showHex)+import Data.ByteString.Char8 qualified as Char8+import Data.ByteString.Base16 qualified as BS16  data Signedness = Signed | Unsigned   deriving (Show)@@ -153,7 +160,7 @@ -- the conditions under which bytes will be decoded and rendered as a string isPrintable :: ByteString -> Bool isPrintable =-  decodeUtf8' >>>+  T.decodeUtf8' >>>     either       (const False)       (T.all (\c-> Char.isPrint c && (not . Char.isControl) c))@@ -172,7 +179,7 @@  formatBinary :: ByteString -> Text formatBinary =-  (<>) "0x" . decodeUtf8 . toStrict . toLazyByteString . byteStringHex+  (<>) "0x" . T.decodeUtf8 . toStrict . toLazyByteString . byteStringHex  formatSBinary :: Expr Buf -> Text formatSBinary (ConcreteBuf bs) = formatBinary bs@@ -271,7 +278,7 @@      ErrorTrace e ->       case e of-        EVM.Revert out ->+        Revert out ->           "\x1b[91merror\x1b[0m " <> "Revert " <> showError out <> pos         _ ->           "\x1b[91merror\x1b[0m " <> pack (show e) <> pos@@ -362,29 +369,39 @@ contractPathPart :: Text -> Text contractPathPart x = T.split (== ':') x !! 0 -prettyError :: EVM.Types.Error -> String-prettyError= \case-  EVM.Types.Invalid -> "Invalid Opcode"-  EVM.Types.IllegalOverflow -> "Illegal Overflow"-  EVM.Types.SelfDestruct -> "Self Destruct"-  EVM.Types.StackLimitExceeded -> "Stack limit exceeded"-  EVM.Types.InvalidMemoryAccess -> "Invalid memory access"-  EVM.Types.BadJumpDestination -> "Bad jump destination"-  EVM.Types.StackUnderrun -> "Stack underrun"-  EVM.Types.TmpErr err -> "Temp error: " <> err-+prettyError :: EvmError -> String+prettyError = \case+  IllegalOverflow -> "Illegal overflow"+  SelfDestruction -> "Self destruct"+  StackLimitExceeded -> "Stack limit exceeded"+  InvalidMemoryAccess -> "Invalid memory access"+  BadJumpDestination -> "Bad jump destination"+  StackUnderrun -> "Stack underrun"+  BalanceTooLow a b -> "Balance too low. value: " <> show a <> " balance: " <> show b+  UnrecognizedOpcode a -> "Unrecognized opcode: " <> show a+  Revert (ConcreteBuf msg) -> "Revert: " <> (T.unpack $ formatBinary msg)+  Revert _ -> "Revert: <symbolic>"+  OutOfGas a b -> "Out of gas: have: " <> show a <> " need: " <> show b+  StateChangeWhileStatic -> "State change while static"+  CallDepthLimitReached -> "Call depth limit reached"+  MaxCodeSizeExceeded a b -> "Max code size exceeded: max: " <> show a <> " actual: " <> show b+  InvalidFormat -> "Invalid Format"+  PrecompileFailure -> "Precompile failure"+  ReturnDataOutOfBounds -> "Return data out of bounds"+  NonceOverflow -> "Nonce overflow"+  BadCheatCode a -> "Bad cheat code: sig: " <> show a -prettyvmresult :: (?context :: DappContext) => Expr End -> String-prettyvmresult (EVM.Types.Revert _ (ConcreteBuf "")) = "Revert"-prettyvmresult (EVM.Types.Revert _ msg) = "Revert: " ++ (unpack $ showError msg)-prettyvmresult (EVM.Types.Return _ (ConcreteBuf msg) _) =+prettyvmresult :: Expr End -> String+prettyvmresult (Failure _ (Revert (ConcreteBuf ""))) = "Revert"+prettyvmresult (Success _ (ConcreteBuf msg) _) =   if BS.null msg   then "Stop"   else "Return: " <> show (ByteStringS msg)-prettyvmresult (EVM.Types.Return _ _ _) =+prettyvmresult (Success _ _ _) =   "Return: <symbolic>" prettyvmresult (Failure _ err) = prettyError err-prettyvmresult e = error "Internal Error: Invalid Result: " <> show e+prettyvmresult (Partial _ p) = T.unpack $ formatPartial p+prettyvmresult r = error $ "Internal Error: Invalid result: " <> show r  indent :: Int -> Text -> Text indent n = rstrip . T.unlines . fmap (T.replicate n (T.pack [' ']) <>) . T.lines@@ -392,6 +409,31 @@ rstrip :: Text -> Text rstrip = T.reverse . T.dropWhile (=='\n') . T.reverse +formatError :: EvmError -> Text+formatError = \case+  Revert buf -> T.unlines+    [ "(Revert"+    , indent 2 $ formatExpr buf+    , ")"+    ]+  e -> T.pack $ show e++formatPartial :: PartialExec -> Text+formatPartial = \case+  (UnexpectedSymbolicArg pc msg args) -> T.unlines+    [ "Unexpected Symbolic Arguments to Opcode"+    , indent 2 $ T.unlines+      [ "msg: " <> T.pack (show msg)+      , "program counter: " <> T.pack (show pc)+      , "arguments: "+      , indent 2 $ T.unlines . fmap formatSomeExpr $ args+      ]+    ]+  MaxIterationsReached pc addr -> T.pack $ "Max Iterations Reached in contract: " <> show addr <> " pc: " <> show pc++formatSomeExpr :: SomeExpr -> Text+formatSomeExpr (SomeExpr e) = formatExpr e+ formatExpr :: Expr a -> Text formatExpr = go   where@@ -405,19 +447,7 @@         , indent 2 (formatExpr t)         , indent 2 (formatExpr f)         , ")"]-      EVM.Types.Revert asserts buf -> case buf of-        ConcreteBuf "" -> "(Revert " <> formatExpr buf <> ")"-        _ -> T.unlines-          [ "(Revert"-          , indent 2 $ T.unlines-            [ "Code:"-            , indent 2 (formatExpr buf)-            , "Assertions:"-            , indent 2 $ T.pack $ show asserts-            ]-          , ")"-          ]-      Return asserts buf store -> T.unlines+      Success asserts buf store -> T.unlines         [ "(Return"         , indent 2 $ T.unlines           [ "Data:"@@ -430,6 +460,16 @@           ]         , ")"         ]+      Failure asserts err -> T.unlines+        [ "(Failure"+        , indent 2 $ T.unlines+          [ "Error:"+          , indent 2 $ formatError err+          , "Assertions:"+          , indent 2 $ T.pack $ show asserts+          ]+        , ")"+        ]        IndexWord idx val -> T.unlines         [ "(IndexWord"@@ -544,3 +584,26 @@        ]        a -> T.pack $ show a++strip0x :: ByteString -> ByteString+strip0x bs = if "0x" `Char8.isPrefixOf` bs then Char8.drop 2 bs else bs++strip0x' :: String -> String+strip0x' s = if "0x" `isPrefixOf` s then drop 2 s else s++hexByteString :: String -> ByteString -> ByteString+hexByteString msg bs =+  case BS16.decodeBase16 bs of+    Right x -> x+    _ -> error ("invalid hex bytestring for " ++ msg)++hexText :: Text -> ByteString+hexText t =+  case BS16.decodeBase16 (T.encodeUtf8 (T.drop 2 t)) of+    Right x -> x+    _ -> error ("invalid hex bytestring " ++ show t)++bsToHex :: ByteString -> String+bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)++

@@ -16,89 +16,6 @@ import Data.Word (Word8) import Numeric (showHex) -type Op = GenericOp (Expr EWord)--data GenericOp a-  = OpStop-  | OpAdd-  | OpMul-  | OpSub-  | OpDiv-  | OpSdiv-  | OpMod-  | OpSmod-  | OpAddmod-  | OpMulmod-  | OpExp-  | OpSignextend-  | OpLt-  | OpGt-  | OpSlt-  | OpSgt-  | OpEq-  | OpIszero-  | OpAnd-  | OpOr-  | OpXor-  | OpNot-  | OpByte-  | OpShl-  | OpShr-  | OpSar-  | OpSha3-  | OpAddress-  | OpBalance-  | OpOrigin-  | OpCaller-  | OpCallvalue-  | OpCalldataload-  | OpCalldatasize-  | OpCalldatacopy-  | OpCodesize-  | OpCodecopy-  | OpGasprice-  | OpExtcodesize-  | OpExtcodecopy-  | OpReturndatasize-  | OpReturndatacopy-  | OpExtcodehash-  | OpBlockhash-  | OpCoinbase-  | OpTimestamp-  | OpNumber-  | OpPrevRandao-  | OpGaslimit-  | OpChainid-  | OpSelfbalance-  | OpBaseFee-  | OpPop-  | OpMload-  | OpMstore-  | OpMstore8-  | OpSload-  | OpSstore-  | OpJump-  | OpJumpi-  | OpPc-  | OpMsize-  | OpGas-  | OpJumpdest-  | OpCreate-  | OpCall-  | OpStaticcall-  | OpCallcode-  | OpReturn-  | OpDelegatecall-  | OpCreate2-  | OpRevert-  | OpSelfdestruct-  | OpDup !Word8-  | OpSwap !Word8-  | OpLog !Word8-  | OpPush a-  | OpUnknown Word8-  deriving (Show, Eq, Functor)- intToOpName:: Int -> String intToOpName a =   case a of

@@ -329,7 +329,7 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars   where     declare n = "(declare-const " <> n <> " (_ BitVec 256))"-    cexvars = mempty{ calldata = fmap toLazyText names }+    cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names }   declareFrameContext :: [Builder] -> SMT2

@@ -11,7 +11,7 @@ import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..)) import Crypto.PubKey.ECC.Generate (generateQ) -import EVM.ABI (encodeAbiValue, AbiValue (..))+import EVM.ABI (encodeAbiValue, AbiValue(..)) import qualified Data.ByteString   as BS import EVM.Types import EVM.Expr (exprToAddr)

@@ -1,4 +1,6 @@ {-# Language DeriveAnyClass #-}+{-# Language DerivingStrategies #-}+{-# Language GeneralisedNewtypeDeriving #-} {-# Language DataKinds #-} {-# Language QuasiQuotes #-} @@ -11,6 +13,9 @@   , yulRuntime   , JumpType (..)   , SolcContract (..)+  , Contracts (..)+  , ProjectType (..)+  , BuildOutput (..)   , StorageItem (..)   , SourceCache (..)   , SrcMap (..)@@ -19,12 +24,12 @@   , SlotType (..)   , Reference(..)   , Mutability(..)+  , readBuildOutput   , functionAbi   , makeSrcMaps   , readSolc   , readJSON   , readStdJSON-  , readCombinedJSON   , stripBytecodeMetadata   , stripBytecodeMetadataSym   , signature@@ -40,7 +45,7 @@ ) where  import EVM.ABI-import EVM.Types+import EVM.Types hiding (Success)  import Optics.Core import Optics.Operators.Unsafe@@ -62,27 +67,30 @@ import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.HashMap.Strict qualified as HMap-import Data.List (sort, isPrefixOf, isInfixOf, elemIndex, tails, findIndex)+import Data.List (sort, isPrefixOf, isInfixOf, isSuffixOf, elemIndex, tails, findIndex) import Data.List.NonEmpty (NonEmpty) import Data.List.NonEmpty qualified as NonEmpty import Data.Maybe import Data.Semigroup import Data.Sequence (Seq) import Data.String.Here qualified as Here-import Data.Text (Text, pack, intercalate)-import Data.Text qualified as Text+import Data.Text (pack, intercalate)+import Data.Text qualified as T import Data.Text.Encoding (encodeUtf8, decodeUtf8) import Data.Text.IO (readFile, writeFile) import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Word (Word8)-import GHC.Generics (Generic)+import Options.Generic import Prelude hiding (readFile, writeFile)+import System.FilePattern.Directory+import System.FilePath.Posix import System.IO hiding (readFile, writeFile) import System.IO.Temp import System.Process import Text.Read (readMaybe) + data StorageItem = StorageItem   { slotType :: SlotType   , offset :: Int@@ -110,15 +118,15 @@    (show t) s  instance Read SlotType where-  readsPrec _ ('m':'a':'p':'p':'i':'n':'g':'(':s) =-    let (lhs,rhs) = case Text.splitOn " => " (pack s) of+  readsPrec _ t@('m':'a':'p':'p':'i':'n':'g':'(':s) =+    let (lhs,rhs) = case T.splitOn " => " (pack s) of           (l:r) -> (l,r)-          _ -> error "could not parse storage item"+          _ -> error $ "could not parse storage item: " <> t         first = fromJust $ parseTypeName mempty lhs-        target = fromJust $ parseTypeName mempty (Text.replace ")" "" (last rhs))-        rest = fmap (fromJust . (parseTypeName mempty . (Text.replace "mapping(" ""))) (take (length rhs - 1) rhs)+        target = fromJust $ parseTypeName mempty (T.replace ")" "" (last rhs))+        rest = fmap (fromJust . (parseTypeName mempty . (T.replace "mapping(" ""))) (take (length rhs - 1) rhs)     in [(StorageMapping (first NonEmpty.:| rest) target, "")]-  readsPrec _ s = [(StorageValue $ fromMaybe (error "could not parse storage item") (parseTypeName mempty (pack s)),"")]+  readsPrec _ s = [(StorageValue $ fromMaybe (error $ "could not parse storage item: " <> s) (parseTypeName mempty (pack s)),"")]  data SolcContract = SolcContract   { runtimeCodehash  :: W256@@ -151,9 +159,43 @@   | Payable    -- ^ function accepts Ether  deriving (Show, Eq, Ord, Generic) +-- | A mapping from contract identifiers (filepath:name) to a SolcContract object+newtype Contracts = Contracts (Map Text SolcContract)+  deriving newtype (Show, Eq, Semigroup, Monoid)++-- | A mapping from contract identifiers (filepath:name) to their ast json+newtype Asts = Asts (Map Text Value)+  deriving newtype (Show, Eq, Semigroup, Monoid)++-- | Solidity source files are identified either by their location in the vfs, or by a src map identifier+data SrcFile = SrcFile+  { id :: Int+  , filepath :: FilePath+  }+  deriving (Show, Eq, Ord)++-- | A mapping from source files to (maybe) their contents+newtype Sources = Sources (Map SrcFile (Maybe ByteString))+  deriving newtype (Show, Eq, Semigroup, Monoid)++data BuildOutput = BuildOutput+  { contracts :: Contracts+  , sources   :: SourceCache+  }+  deriving (Show, Eq)++instance Semigroup BuildOutput where+  (BuildOutput a b) <> (BuildOutput c d) = BuildOutput (a <> c) (b <> d)+instance Monoid BuildOutput where+  mempty = BuildOutput mempty mempty++-- | The various project types understood by hevm+data ProjectType = DappTools | Foundry+  deriving (Eq, Show, Read, ParseField)+ data SourceCache = SourceCache-  { files  :: [(Text, ByteString)]-  , lines  :: [(Vector ByteString)]+  { files  :: Map Int (FilePath, ByteString)+  , lines  :: Map Int (Vector ByteString)   , asts   :: Map Text Value   } deriving (Show, Eq, Generic) @@ -170,7 +212,7 @@     typeMismatch "Transaction" invalid  instance Semigroup SourceCache where-  _ <> _ = error "lol"+  SourceCache a b c <> SourceCache d e f = SourceCache (a <> d) (b <> e) (c <> f)  instance Monoid SourceCache where   mempty = SourceCache mempty mempty mempty@@ -201,7 +243,7 @@ -- Obscure but efficient parser for the Solidity sourcemap format. makeSrcMaps :: Text -> Maybe (Seq SrcMap) makeSrcMaps = (\case (_, Fe, _) -> Nothing; x -> Just (done x))-             . Text.foldl' (flip go) (mempty, F1 [] 1, SM 0 0 0 JumpRegular 0)+             . T.foldl' (flip go) (mempty, F1 [] 1, SM 0 0 0 JumpRegular 0)   where     done (xs, s, p) = let (xs', _, _) = go ';' (xs, s, p) in xs'     readR = read . reverse@@ -244,16 +286,45 @@     go ';' (xs, F5 a b c j ds, _)              = let p' = SM a b c j (readR ds) in -- solc >=0.6                                                  (xs |> p', F1 [] 1, p') -    go c (xs, state, p)                      = (xs, error ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p)+    go c (xs, state, p)                        = (xs, error ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p) -makeSourceCache :: [(Text, Maybe ByteString)] -> Map Text Value -> IO SourceCache-makeSourceCache paths asts = do-  let f (_,  Just content) = return content-      f (fp, Nothing) = BS.readFile $ Text.unpack fp-  xs <- mapM f paths+-- | Reads all solc ouput json files found under the provided filepath and returns them merged into a BuildOutput+readBuildOutput :: FilePath -> ProjectType -> IO (Either String BuildOutput)+readBuildOutput root DappTools = do+  let outDir = root <> "/out/"+  jsons <- findJsonFiles outDir+  case jsons of+    [x] -> readSolc DappTools root (outDir <> x)+    [] -> pure . Left $ "no json files found in: " <> outDir+    _ -> pure . Left $ "multiple json files found in: " <> outDir+readBuildOutput root Foundry = do+  let outDir = root <> "/out/"+  jsons <- findJsonFiles (root <> "/out")+  case (filterMetadata jsons) of+    [] -> pure . Left $ "no json files found in: " <> outDir+    js -> do+      outputs <- sequence <$> mapM (readSolc Foundry root) ((fmap ((<>) (outDir))) js)+      pure . (fmap mconcat) $ outputs++-- | Finds all json files under the provided filepath, searches recursively+findJsonFiles :: FilePath -> IO [FilePath]+findJsonFiles root = getDirectoryFiles root ["**/*.json"]++-- | Filters out metadata json files+filterMetadata :: [FilePath] -> [FilePath]+filterMetadata = filter (not . isSuffixOf ".metadata.json")++makeSourceCache :: FilePath -> Sources -> Asts -> IO SourceCache+makeSourceCache root (Sources sources) (Asts asts) = do+  files <- Map.fromList <$> forM (Map.toList sources) (\x@(SrcFile id' fp, _) -> do+      contents <- case x of+        (_,  Just content) -> return content+        (SrcFile _ _, Nothing) -> BS.readFile (root <> "/" <> fp)+      pure (id', (fp, contents))+    )   return $! SourceCache-    { files = zip (fst <$> paths) xs-    , lines = map (Vector.fromList . BS.split 0xa) xs+    { files = files+    , lines = fmap (Vector.fromList . BS.split 0xa . snd) files     , asts  = asts     } @@ -269,20 +340,20 @@     then Nothing     else Just (s1 - s2, min (s2 + n2 - s1) n1) -readSolc :: FilePath -> IO (Maybe (Map Text SolcContract, SourceCache))-readSolc fp =-  (readJSON <$> readFile fp) >>=+readSolc :: ProjectType -> FilePath -> FilePath -> IO (Either String BuildOutput)+readSolc pt root fp =+  (readJSON pt (T.pack $ takeBaseName fp) <$> readFile fp) >>=     \case-      Nothing -> return Nothing+      Nothing -> pure . Left $ "unable to parse: " <> fp       Just (contracts, asts, sources) -> do-        sourceCache <- makeSourceCache sources asts-        return (Just (contracts, sourceCache))+        sourceCache <- makeSourceCache root sources asts+        return (Right (BuildOutput contracts sourceCache))  yul :: Text -> Text -> IO (Maybe ByteString) yul contract src = do   (json, path) <- yul' src   let f = (json ^?! key "contracts") ^?! key (Key.fromText path)-      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)+      c = f ^?! key (Key.fromText $ if T.null contract then "object" else contract)       bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" % _String   pure $ toCode <$> (Just bytecode) @@ -290,26 +361,26 @@ yulRuntime contract src = do   (json, path) <- yul' src   let f = (json ^?! key "contracts") ^?! key (Key.fromText path)-      c = f ^?! key (Key.fromText $ if Text.null contract then "object" else contract)+      c = f ^?! key (Key.fromText $ if T.null contract then "object" else contract)       bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" % _String   pure $ toCode <$> (Just bytecode)  solidity :: Text -> Text -> IO (Maybe ByteString) solidity contract src = do   (json, path) <- solidity' src-  let (sol, _, _) = fromJust $ readJSON json+  let (Contracts sol, _, _) = fromJust $ readStdJSON json   pure $ Map.lookup (path <> ":" <> contract) sol <&> (.creationCode)  solcRuntime :: Text -> Text -> IO (Maybe ByteString) solcRuntime contract src = do   (json, path) <- solidity' src-  let (sol, _, _) = fromJust $ readJSON json+  let (Contracts sol, _, _) = fromJust $ readStdJSON json   pure $ Map.lookup (path <> ":" <> contract) sol <&> (.runtimeCode)  functionAbi :: Text -> IO Method functionAbi f = do   (json, path) <- solidity' ("contract ABI { function " <> f <> " public {}}")-  let (sol, _, _) = fromJust $ readJSON json+  let (Contracts sol, _, _) = fromJust $ readStdJSON json   case Map.toList $ (fromJust (Map.lookup (path <> ":ABI") sol)).abiMap of      [(_,b)] -> return b      _ -> error "hevm internal error: unexpected abi format"@@ -317,52 +388,62 @@ force :: String -> Maybe a -> a force s = fromMaybe (error s) -readJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])-readJSON json = case json ^? key "sourceList" of-  Nothing -> readStdJSON json-  _ -> readCombinedJSON json+readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)+readJSON DappTools _ json = readStdJSON json+readJSON Foundry contractName json = readFoundryJSON contractName json --- deprecate me soon-readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])-readCombinedJSON json = do-  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" % _Object)-  sources <- toList . fmap (preview _String) <$> json ^? key "sourceList" % _Array-  return (contracts, Map.fromList (HMap.toList asts), [ (x, Nothing) | Just x <- sources])-  where-    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" % _Object)-    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 $ case (x ^?! key "abi") ^? _Array of-                 Just v -> v                                       -- solc >= 0.8-                 Nothing -> (x ^?! key "abi" % _String) ^?! _Array -- solc <  0.8-      in SolcContract {-        runtimeCode      = theRuntimeCode,-        creationCode     = theCreationCode,-        runtimeCodehash  = keccak' (stripBytecodeMetadata theRuntimeCode),-        creationCodehash = keccak' (stripBytecodeMetadata theCreationCode),-        runtimeSrcmap    = force "internal error: srcmap-runtime" (makeSrcMaps (x ^?! key "srcmap-runtime" % _String)),-        creationSrcmap   = force "internal error: srcmap" (makeSrcMaps (x ^?! key "srcmap" % _String)),-        contractName = s,-        constructorInputs = mkConstructor abis,-        abiMap       = mkAbiMap abis,-        eventMap     = mkEventMap abis,-        errorMap     = mkErrorMap abis,-        storageLayout = mkStorageLayout $ x ^? key "storage-layout",-        immutableReferences = mempty -- TODO: deprecate combined-json-      }+-- | Reads a foundry json output+readFoundryJSON :: Text -> Text -> Maybe (Contracts, Asts, Sources)+readFoundryJSON contractName json = do+  runtime <- json ^? key "deployedBytecode"+  runtimeCode <- toCode . strip0x'' <$> runtime ^? key "object" % _String+  runtimeSrcMap <- makeSrcMaps =<< runtime ^? key "sourceMap" % _String -readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])+  creation <- json ^? key "bytecode"+  creationCode <- toCode . strip0x'' <$> creation ^? key "object" % _String+  creationSrcMap <- makeSrcMaps =<< creation ^? key "sourceMap" % _String++  ast <- json ^? key "ast"+  path <- ast ^? key "absolutePath" % _String++  abi <- toList <$> json ^? key "abi" % _Array++  id' <- num <$> json ^? key "id" % _Integer++  let contract = SolcContract+        { runtimeCodehash     = keccak' (stripBytecodeMetadata runtimeCode)+        , creationCodehash    = keccak' (stripBytecodeMetadata creationCode)+        , runtimeCode         = runtimeCode+        , creationCode        = creationCode+        , contractName        = path <> ":" <> contractName+        , abiMap              = mkAbiMap abi+        , eventMap            = mkEventMap abi+        , errorMap            = mkErrorMap abi+        , runtimeSrcmap       = runtimeSrcMap+        , creationSrcmap      = creationSrcMap+        , constructorInputs   = mkConstructor abi+        , storageLayout       = mempty -- TODO: foundry doesn't expose this?+        , immutableReferences = mempty -- TODO: foundry doesn't expose this?+        }+  return ( Contracts $ Map.singleton (path <> ":" <> contractName) contract+         , Asts      $ Map.singleton path ast+         , Sources   $ Map.singleton (SrcFile id' (T.unpack path)) Nothing+         )++-- | Parses the standard json output from solc+readStdJSON :: Text -> Maybe (Contracts, Asts, Sources) readStdJSON json = do   contracts <- KeyMap.toHashMapText <$> json ^? key "contracts" % _Object   -- TODO: support the general case of "urls" and "content" in the standard json   sources <- KeyMap.toHashMapText <$>  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))+      getId src = num $ (force "" $ HMap.lookup src sources) ^?! key "id" % _Integer+      contents src = (SrcFile (getId src) (T.unpack src), encodeUtf8 <$> HMap.lookup src (mconcat $ Map.elems $ snd <$> contractMap))+  return ( Contracts $ fst <$> contractMap+         , Asts      $ Map.fromList (HMap.toList asts)+         , Sources   $ Map.fromList $ 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@@ -480,7 +561,7 @@        slot <- item ^? key "slot" % _String        typ <- Key.fromText <$> item ^? key "type" % _String        slotType <- types ^?! key typ ^? key "label" % _String-       return (name, StorageItem (read $ Text.unpack slotType) offset (read $ Text.unpack slot)))+       return (name, StorageItem (read $ T.unpack slotType) offset (read $ T.unpack slot)))  signature :: AsValue s => s -> Text signature abi =@@ -525,7 +606,7 @@   Right d -> d   Left e -> if containsLinkerHole t             then error "unlinked libraries detected in bytecode"-            else error $ Text.unpack e+            else error $ T.unpack e  solidity' :: Text -> IO (Text, Text) solidity' src = withSystemTempFile "hevm.sol" $ \path handle -> do@@ -597,7 +678,7 @@   withSystemTempFile "hevm.sol" $ \path handle -> do     hClose handle     writeFile path (stdjson lang src)-    Text.pack <$> readProcess+    T.pack <$> readProcess       "solc"       ["--standard-json", path]       ""@@ -662,7 +743,7 @@ stripBytecodeMetadataSym b =   let     concretes :: [Maybe Word8]-    concretes = unlitByte <$> b+    concretes = maybeLitByte <$> b     bzzrs :: [[Maybe Word8]]     bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs@@ -712,8 +793,12 @@       . mapMaybe         (\v -> do           src <- preview (key "src" % _String) v-          [i, n, f] <- mapM (readMaybe . Text.unpack) (Text.split (== ':') src)+          [i, n, f] <- mapM (readMaybe . T.unpack) (T.split (== ':') src)           return ((i, n, f), v)         )       . Map.elems       $ astIds++-- needs to be here not Format due to cyclic module deps+strip0x'' :: Text -> Text+strip0x'' s = if "0x" `T.isPrefixOf` s then T.drop 2 s else s

@@ -30,7 +30,7 @@ import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))  import EVM.SMT-import EVM.Types+import EVM.Types hiding (Unknown)  -- | Supported solvers data Solver

@@ -26,12 +26,12 @@ import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view) import Control.Monad.State.Strict (StateT, execState, runState, runStateT) import Data.Text (Text)+import EVM.Types -import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose)-import EVM qualified+import qualified EVM++import qualified EVM.Fetch as Fetch import EVM.Exec qualified-import EVM.Fetch qualified as Fetch-import EVM.Types (Expr, EType(..))  -- | The instruction type of the operational monad data Action a where@@ -78,63 +78,68 @@ evmIO = singleton . IOAct  -- | Run the VM until final result, resolving all queries-execFully :: Stepper (Either Error (Expr Buf))+execFully :: Stepper (Either EvmError (Expr Buf)) execFully =   exec >>= \case-    VMFailure (Query q) ->+    HandleEffect (Query q) ->       wait q >> execFully-    VMFailure (Choose q) ->+    HandleEffect (Choose q) ->       ask q >> execFully     VMFailure x ->       pure (Left x)     VMSuccess x ->       pure (Right x)+    Unfinished x+      -> error $ "Internal Error: partial execution encountered during concrete execution: " <> show x  -- | Run the VM until its final state-runFully :: Stepper EVM.VM+runFully :: Stepper VM runFully = do   vm <- run   case vm.result of     Nothing -> error "should not occur"-    Just (VMFailure (Query q)) ->+    Just (HandleEffect (Query q)) ->       wait q >> runFully-    Just (VMFailure (Choose q)) ->+    Just (HandleEffect (Choose q)) ->       ask q >> runFully     Just _ ->       pure vm  entering :: Text -> Stepper a -> Stepper a entering t stepper = do-  evm (EVM.pushTrace (EVM.EntryTrace t))+  evm (EVM.pushTrace (EntryTrace t))   x <- stepper   evm EVM.popTrace   pure x  enter :: Text -> Stepper ()-enter t = evm (EVM.pushTrace (EVM.EntryTrace t))+enter t = evm (EVM.pushTrace (EntryTrace t))  interpret :: Fetch.Fetcher -> VM -> Stepper a -> IO a interpret fetcher vm = eval . view   where-  eval :: ProgramView Action a -> IO a-  eval (Return x) = pure x-  eval (action :>>= k) =-    case action of-      Exec ->-        let (r, vm') = runState EVM.Exec.exec vm-        in interpret fetcher vm' (k r)-      Run ->-        let vm' = execState EVM.Exec.run vm-        in interpret fetcher vm' (k vm')-      Wait q -> do-        m <- fetcher q-        let vm' = execState m vm-        interpret fetcher vm' (k ())-      Ask _ ->-        error "cannot make choices with this interpreter"-      IOAct m -> do-        (r, vm') <- runStateT m vm-        interpret fetcher vm' (k r)-      EVM m ->-        let (r, vm') = runState m vm-        in interpret fetcher vm' (k r)+    eval :: ProgramView Action a -> IO a+    eval (Return x) = pure x+    eval (action :>>= k) =+      case action of+        Exec ->+          let (r, vm') = runState EVM.Exec.exec vm+          in interpret fetcher vm' (k r)+        Run ->+          let vm' = execState EVM.Exec.run vm+          in interpret fetcher vm' (k vm')+        Wait (PleaseAskSMT (Lit c) _ continue) ->+          let (r, vm') = runState (continue (Case (c > 0))) vm+          in interpret fetcher vm' (k r)+        Wait q -> do+          m <- fetcher q+          let vm' = execState m vm+          interpret fetcher vm' (k ())+        Ask _ ->+          error "cannot make choices with this interpreter"+        IOAct m -> do+          (r, vm') <- runStateT m vm+          interpret fetcher vm' (k r)+        EVM m ->+          let (r, vm') = runState m vm+          in interpret fetcher vm' (k r)

@@ -1,51 +1,61 @@+{-# Language TupleSections #-}+{-# Language DeriveAnyClass #-} {-# Language DataKinds #-}  module EVM.SymExec where -import Control.Concurrent.Async (concurrently, mapConcurrently)-import Control.Concurrent.Spawn (parMapIO, pool)-import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)-import Control.Monad.Operational qualified as Operational-import Control.Monad.State.Strict-import Data.Bifunctor (second)-import Data.ByteString (ByteString)-import Data.ByteString qualified as BS-import Data.DoubleWord (Word256)-import Data.List (foldl', sortBy)-import Data.Map (Map)-import Data.Map qualified as Map-import Data.Maybe-import Data.Set (Set, isSubsetOf, size)-import Data.Set qualified as Set-import Data.Text (Text)-import Data.Text qualified as T-import Data.Text.IO qualified as T-import Data.Text.Lazy qualified as TL-import Data.Text.Lazy.IO qualified as TL+import Prelude hiding (Word)+ import Data.Tuple (swap)-import GHC.Conc (getNumProcessors) import Optics.Core--import EVM hiding (Query, Revert, bytecode)-import EVM qualified-import EVM.ABI-import EVM.Concrete (createAddress)+import EVM hiding (push, bytecode, query, wrap) import EVM.Exec-import EVM.Expr qualified as Expr-import EVM.FeeSchedule qualified as FeeSchedule-import EVM.Fetch qualified as Fetch-import EVM.Format (formatExpr, indent, formatBinary)+import qualified EVM.Fetch as Fetch+import EVM.ABI import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)-import EVM.SMT qualified as SMT+import qualified EVM.SMT as SMT import EVM.Solvers-import EVM.Stepper (Stepper)-import EVM.Stepper qualified as Stepper import EVM.Traversals+import qualified EVM.Expr as Expr+import EVM.Stepper (Stepper)+import qualified EVM.Stepper as Stepper+import qualified Control.Monad.Operational as Operational+import Control.Monad.State.Strict hiding (state) import EVM.Types+import EVM.Concrete (createAddress)+import qualified EVM.FeeSchedule as FeeSchedule+import Data.DoubleWord (Word256)+import Control.Concurrent.Async+import Data.Maybe+import Data.Containers.ListUtils+import Data.List (foldl', sortBy)+import Data.ByteString (ByteString)+import qualified Data.ByteString as BS+import Data.Bifunctor (second)+import Data.Map (Map)+import qualified Data.Map as Map+import qualified Data.Text as T+import qualified Data.Text.IO as T+import qualified Data.Text.Lazy as TL+import qualified Data.Text.Lazy.IO as TL+import EVM.Format (formatExpr, formatPartial)+import Data.Set (Set, isSubsetOf, size)+import qualified Data.Set as Set+import Control.Concurrent.Spawn (parMapIO, pool)+import Control.Concurrent.STM (atomically, TVar, readTVarIO, readTVar, newTVarIO, writeTVar)+import GHC.Conc (getNumProcessors)+import EVM.Format (indent, formatBinary)+import Options.Generic as Options + -- | A method name, and the (ordered) types of it's arguments data Sig = Sig Text [AbiType] +data LoopHeuristic+  = Naive+  | StackBased+  deriving (Eq, Show, Read, ParseField, ParseFields, ParseRecord, Generic)+ data ProofResult a b c = Qed a | Cex b | Timeout c   deriving (Show, Eq) type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)@@ -67,7 +77,8 @@   { simp :: Bool   , debug :: Bool   , maxIter :: Maybe Integer-  , askSmtIters :: Maybe Integer+  , askSmtIters :: Integer+  , loopHeuristic :: LoopHeuristic   , rpcInfo :: Fetch.RpcInfo   }   deriving (Eq, Show)@@ -77,7 +88,8 @@   { simp = True   , debug = False   , maxIter = Nothing-  , askSmtIters = Nothing+  , askSmtIters = 1+  , loopHeuristic = StackBased   , rpcInfo = Nothing   } @@ -234,11 +246,12 @@ interpret   :: Fetch.Fetcher   -> Maybe Integer -- max iterations-  -> Maybe Integer -- ask smt iterations+  -> Integer -- ask smt iterations+  -> LoopHeuristic   -> VM   -> Stepper (Expr End)   -> IO (Expr End)-interpret fetcher maxIter askSmtIters vm =+interpret fetcher maxIter askSmtIters heuristic vm =   eval . Operational.view   where   eval@@ -251,68 +264,105 @@     case action of       Stepper.Exec -> do         let (r, vm') = runState exec vm-        interpret fetcher maxIter askSmtIters vm' (k r)+        interpret fetcher maxIter askSmtIters heuristic vm' (k r)       Stepper.Run -> do         let vm' = execState exec vm-        interpret fetcher maxIter askSmtIters vm' (k vm')+        interpret fetcher maxIter askSmtIters heuristic vm' (k vm')       Stepper.IOAct q -> do         (r, vm') <- runStateT q vm-        interpret fetcher maxIter askSmtIters vm' (k r)-      Stepper.Ask (EVM.PleaseChoosePath cond continue) ->-        case maxIterationsReached vm maxIter of-          Nothing -> do-            (a, b) <- concurrently-              (let (ra, vma) = runState (continue True) vm { result = Nothing }-               in interpret fetcher maxIter askSmtIters vma (k ra))-              (let (rb, vmb) = runState (continue False) vm { result = Nothing }-               in interpret fetcher maxIter askSmtIters vmb (k rb))+        interpret fetcher maxIter askSmtIters heuristic vm' (k r)+      Stepper.Ask (PleaseChoosePath cond continue) -> do+        (a, b) <- concurrently+          (let (ra, vma) = runState (continue True) vm { result = Nothing }+           in interpret fetcher maxIter askSmtIters heuristic vma (k ra))+          (let (rb, vmb) = runState (continue False) vm { result = Nothing }+           in interpret fetcher maxIter askSmtIters heuristic vmb (k rb)) -            pure $ ITE cond a b-          Just n -> do-            -- Let's escape the loop. We give no guarantees at this point-            let (r, vm') = runState (continue (not n)) vm { result = Nothing }-            interpret fetcher maxIter askSmtIters vm' (k r)+        pure $ ITE cond a b       Stepper.Wait q -> do         let performQuery = do               m <- liftIO (fetcher q)               let (r, vm') = runState m vm-              interpret fetcher maxIter askSmtIters vm' (k r)+              interpret fetcher maxIter askSmtIters heuristic vm' (k r)          case q of-          PleaseAskSMT _ _ continue -> do-            let-              codelocation = getCodeLocation vm-              iteration = num . fromMaybe 0 $ Map.lookup codelocation vm.iterations+          PleaseAskSMT cond _ continue -> do+            case cond of+              -- is the condition concrete?+              Lit c ->+                -- have we reached max iterations, are we inside a loop?+                case (maxIterationsReached vm maxIter, isLoopHead heuristic vm) of+                  -- Yes. return a partial leaf+                  (Just _, Just True) ->+                    pure $ Partial vm.keccakEqs $ MaxIterationsReached vm.state.pc vm.state.contract+                  -- No. keep executing+                  _ ->+                    let (r, vm') = runState (continue (Case (c > 0))) vm+                    in interpret fetcher maxIter askSmtIters heuristic vm' (k r) -            -- 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 < fromMaybe 5 askSmtIters then do-              let (r, vm') = runState (continue EVM.Unknown) vm-              interpret fetcher maxIter askSmtIters vm' (k r)-            else performQuery+              -- the condition is symbolic+              _ ->+                -- are in we a loop, have we hit maxIters, have we hit askSmtIters?+                case (isLoopHead heuristic vm, askSmtItersReached vm askSmtIters, maxIterationsReached vm maxIter) of+                  -- we're in a loop and maxIters has been reached+                  (Just True, _, Just n) -> do+                    -- continue execution down the opposite branch than the one that+                    -- got us to this point and return a partial leaf for the other side+                    let (r, vm') = runState (continue (Case $ not n)) vm+                    a <- interpret fetcher maxIter askSmtIters heuristic vm' (k r)+                    pure $ ITE cond a (Partial vm.keccakEqs (MaxIterationsReached vm.state.pc vm.state.contract))+                  -- we're in a loop and askSmtIters has been reached+                  (Just True, True, _) ->+                    -- ask the smt solver about the loop condition+                    performQuery+                  -- otherwise just try both branches and don't ask the solver+                  _ ->+                    let (r, vm') = runState (continue EVM.Types.Unknown) vm+                    in interpret fetcher maxIter askSmtIters heuristic vm' (k r)            _ -> performQuery        Stepper.EVM m -> do         let (r, vm') = runState m vm-        interpret fetcher maxIter askSmtIters vm' (k r)+        interpret fetcher maxIter askSmtIters heuristic vm' (k r)  maxIterationsReached :: VM -> Maybe Integer -> Maybe Bool maxIterationsReached _ Nothing = Nothing maxIterationsReached vm (Just maxIter) =   let codelocation = getCodeLocation vm-      iters = view (at codelocation % non 0) vm.iterations+      (iters, _) = view (at codelocation % non (0, [])) vm.iterations   in if num maxIter <= iters      then Map.lookup (codelocation, iters - 1) vm.cache.path      else Nothing +askSmtItersReached :: VM -> Integer -> Bool+askSmtItersReached vm askSmtIters = let+    codelocation = getCodeLocation vm+    (iters, _) = view (at codelocation % non (0, [])) vm.iterations+  in askSmtIters <= num iters +{- | Loop head detection heuristic++ The main thing we wish to differentiate between, are actual loop heads, and branch points inside of internal functions that are called multiple times.++ One way to do this is to observe that for internal functions, the compiler must always store a stack item representing the location that it must jump back to. If we compare the stack at the time of the previous visit, and the time of the current visit, and notice that this location has changed, then we can guess that the location is a jump point within an internal function instead of a loop (where such locations should be constant between iterations).++ This heuristic is not perfect, and can certainly be tricked, but should generally be good enough for most compiler generated and non pathological user generated loops.+ -}+isLoopHead :: LoopHeuristic -> VM -> Maybe Bool+isLoopHead Naive _ = Just True+isLoopHead StackBased vm = let+    loc = getCodeLocation vm+    oldIters = Map.lookup loc vm.iterations+    isValid (Lit wrd) = wrd <= num (maxBound :: Int) && isValidJumpDest vm (num wrd)+    isValid _ = False+  in case oldIters of+       Just (_, oldStack) -> Just $ filter isValid oldStack == filter isValid vm.state.stack+       Nothing -> Nothing+ type Precondition = VM -> Prop type Postcondition = VM -> Expr End -> Prop - checkAssert   :: SolverGroup   -> [Word256]@@ -345,8 +395,8 @@ -} checkAssertions :: [Word256] -> Postcondition checkAssertions errs _ = \case-  Revert _ (ConcreteBuf msg) -> PBool $ msg `notElem` (fmap panicMsg errs)-  Revert _ b -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)+  Failure _ (Revert (ConcreteBuf msg)) -> PBool $ msg `notElem` (fmap panicMsg errs)+  Failure _ (Revert b) -> foldl' PAnd (PBool True) (fmap (PNeg . PEq b . ConcreteBuf . panicMsg) errs)   _ -> PBool True  -- | By default hevm only checks for user-defined assertions@@ -388,44 +438,29 @@   let preState = abstractVM (mkCalldata signature' concreteArgs) theCode maybepre initStore   in verify solvers opts preState maybepost -pruneDeadPaths :: [VM] -> [VM]-pruneDeadPaths =-  filter $ \vm -> case vm.result of-    Just (VMFailure DeadPath) -> False-    _ -> True- -- | Stepper that parses the result of Stepper.runFully into an Expr End runExpr :: Stepper.Stepper (Expr End) runExpr = do   vm <- Stepper.runFully   let asserts = vm.keccakEqs   pure $ case vm.result of-    Nothing -> error "Internal Error: vm in intermediate state after call to runFully"-    Just (VMSuccess buf) -> Return asserts buf vm.env.storage-    Just (VMFailure e) -> case e of-      UnrecognizedOpcode _ -> Failure asserts Invalid-      SelfDestruction -> Failure asserts SelfDestruct-      EVM.StackLimitExceeded -> Failure asserts EVM.Types.StackLimitExceeded-      EVM.IllegalOverflow -> Failure asserts EVM.Types.IllegalOverflow-      EVM.Revert buf -> EVM.Types.Revert asserts buf-      EVM.InvalidMemoryAccess -> Failure asserts EVM.Types.InvalidMemoryAccess-      EVM.BadJumpDestination -> Failure asserts EVM.Types.BadJumpDestination-      EVM.StackUnderrun -> Failure asserts EVM.Types.StackUnderrun-      e' -> Failure asserts $ EVM.Types.TmpErr (show e')+    Just (VMSuccess buf) -> Success asserts buf vm.env.storage+    Just (VMFailure e) -> Failure asserts e+    Just (Unfinished p) -> Partial asserts p+    _ -> error "Internal Error: vm in intermediate state after call to runFully"  -- | Converts a given top level expr into a list of final states and the -- associated path conditions for each state. flattenExpr :: Expr End -> [Expr End] flattenExpr = go []   where-  go :: [Prop] -> Expr End -> [Expr End]-  go pcs = \case-    ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f-    Failure _ (TmpErr s) -> error s-    GVar _ -> error "cannot flatten an Expr containing a GVar"-    Revert ps msg -> [Revert (ps <> pcs) msg]-    Return ps msg store -> [Return (ps <> pcs) msg store]-    Failure ps e -> [Failure (ps <> pcs) e]+    go :: [Prop] -> Expr End -> [Expr End]+    go pcs = \case+      ITE c t f -> go (PNeg ((PEq c (Lit 0))) : pcs) t <> go (PEq c (Lit 0) : pcs) f+      Success ps msg store -> [Success (ps <> pcs) msg store]+      Failure ps e -> [Failure (ps <> pcs) e]+      Partial ps p -> [Partial (ps <> pcs) p]+      GVar _ -> error "cannot flatten an Expr containing a GVar"  -- | Strips unreachable branches from a given expr -- Returns a list of executed SMT queries alongside the reduced expression for debugging purposes@@ -505,12 +540,23 @@ extractProps :: Expr End -> [Prop] extractProps = \case   ITE _ _ _ -> []-  Revert asserts _ -> asserts-  Return asserts _ _ -> asserts+  Success asserts _ _ -> asserts   Failure asserts _ -> asserts+  Partial asserts _ -> asserts   GVar _ -> error "cannot extract props from a GVar" +isPartial :: Expr a -> Bool+isPartial (Partial _ _) = True+isPartial _ = False +getPartials :: [Expr End] -> [PartialExec]+getPartials = mapMaybe go+  where+    go :: Expr End -> Maybe PartialExec+    go = \case+      Partial _ p -> Just p+      _ -> Nothing+ -- | Symbolically execute the VM and check all endstates against the -- postcondition, if available. verify@@ -522,7 +568,7 @@ verify solvers opts preState maybepost = do   putStrLn "Exploring contract" -  exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters preState runExpr+  exprInter <- interpret (Fetch.oracle solvers opts.rpcInfo) opts.maxIter opts.askSmtIters opts.loopHeuristic preState runExpr   when opts.debug $ T.writeFile "unsimplified.expr" (formatExpr exprInter)    putStrLn "Simplifying expression"@@ -531,12 +577,19 @@    putStrLn $ "Explored contract (" <> show (Expr.numBranches expr) <> " branches)" +  let flattened = flattenExpr expr+  when (any isPartial flattened) $ do+    T.putStrLn ""+    T.putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"+    T.putStrLn ""+    T.putStrLn . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . getPartials $ flattened+   case maybepost of     Nothing -> pure (expr, [Qed ()])     Just post -> do       let         -- Filter out any leaves that can be statically shown to be safe-        canViolate = flip filter (flattenExpr expr) $+        canViolate = flip filter flattened $           \leaf -> case evalProp (post preState leaf) of             PBool True -> False             _ -> True@@ -587,6 +640,13 @@     False -> do       branchesA <- getBranches bytecodeA       branchesB <- getBranches bytecodeB++      when (any isPartial branchesA || any isPartial branchesB) $ do+        putStrLn ""+        putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"+        putStrLn ""+        T.putStrLn . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . nubOrd $ ((getPartials branchesA) <> (getPartials branchesB))+       let allPairs = [(a,b) | a <- branchesA, b <- branchesB]       putStrLn $ "Found " <> show (length allPairs) <> " total pairs of endstates" @@ -624,7 +684,7 @@       let         bytecode = if BS.null bs then BS.pack [0] else bs         prestate = abstractVM calldata' bytecode Nothing AbstractStore-      expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters prestate runExpr+      expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr       let simpl = if opts.simp then (Expr.simplify expr) else expr       pure $ flattenExpr simpl @@ -670,23 +730,20 @@     distinct aEnd bEnd =       let         differingResults = case (aEnd, bEnd) of-          (Return _ aOut aStore, Return _ bOut bStore) ->+          (Success _ aOut aStore, Success _ bOut bStore) ->             if aOut == bOut && aStore == bStore             then PBool False             else aStore ./= bStore .|| aOut ./= bOut-          (Return {}, _) -> PBool True-          (_, Return {}) -> PBool True-          (Revert _ a, Revert _ b) -> if a == b then PBool False else a ./= b-          (Revert _ _, _) -> PBool True-          (_, Revert _ _) -> PBool True-          (Failure _ (TmpErr s), _) -> error $ "Unhandled error: " <> s-          (_, Failure _ (TmpErr s)) -> error $ "Unhandled error: " <> s-          (Failure _ erra, Failure _ errb) -> if erra==errb then PBool False else PBool True+          (Failure _ (Revert a), Failure _ (Revert b)) -> if a == b then PBool False else a ./= b+          (Failure _ a, Failure _ b) -> if a == b then PBool False else PBool True+          -- partial end states can't be compared to actual end states, so we always ignore them+          (Partial {}, _) -> PBool False+          (_, Partial {}) -> PBool False           (ITE _ _ _, _) -> error "Expressions must be flattened"           (_, ITE _ _ _) -> error "Expressions must be flattened"           (a, b) -> if a == b                     then PBool False-                    else error $ "Internal Error: Unimplemented. Left: " <> show a <> " Right: " <> show b+                    else PBool True       in case differingResults of         -- if the end states are the same, then they can never produce a         -- different result under any circumstances

@@ -13,10 +13,10 @@ import Brick.Widgets.List  import EVM-import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi)+import EVM.ABI (decodeAbiValue, emptyAbi, abiTypeSolidity, AbiType(..)) import EVM.SymExec (maxIterationsReached, symCalldata) import EVM.Expr (simplify)-import EVM.Dapp (DappInfo(..), dappInfo, Test, extractSig, Test(..), srcMap, unitTestMethods)+import EVM.Dapp (DappInfo(..), emptyDapp, dappInfo, Test, extractSig, Test(..), srcMap, unitTestMethods) import EVM.Debug import EVM.Fetch (Fetcher) import EVM.Fetch qualified as Fetch@@ -44,7 +44,7 @@ import Data.ByteString qualified as BS import Data.List (sort, find) import Data.Maybe (isJust, fromJust, fromMaybe, isNothing)-import Data.Map (Map, insert, lookupLT, singleton, filter)+import Data.Map (Map, insert, lookupLT, singleton, filter, (!?)) import Data.Map qualified as Map import Data.Text (Text, pack) import Data.Text qualified as T@@ -175,6 +175,8 @@             Just n -> interpret mode (Stepper.evm (cont (not n)) >>= k)          -- Stepper wants to make a query and wait for the results?+        Stepper.Wait (PleaseAskSMT (Lit c) _ continue) ->+          interpret mode (Stepper.evm (continue (Case (c > 0))) >>= k)         Stepper.Wait q -> do           do m <- liftIO (?fetcher q)              interpret mode (Stepper.evm m >>= k)@@ -236,7 +238,7 @@       , rpcInfo       = rpcInfo       , verbose       = Nothing       , maxIter       = maxIter'-      , askSmtIters   = Nothing+      , askSmtIters   = 1       , smtTimeout    = Nothing       , smtDebug      = False       , solver        = Nothing@@ -284,30 +286,25 @@ isFuzzTest (ConcreteTest _, _) = True isFuzzTest (InvariantTest _, _) = True -main :: UnitTestOptions -> FilePath -> FilePath -> IO ()-main opts root jsonFilePath =-  readSolc jsonFilePath >>=-    \case-      Nothing ->-        error "Failed to read Solidity JSON"-      Just (contractMap, sourceCache) -> do-        let-          dapp = dappInfo root contractMap sourceCache-          ui = ViewPicker $ UiTestPickerState-            { tests =-                list-                  TestPickerPane-                  (Vec.fromList-                   (concatMap-                    (debuggableTests opts)-                    dapp.unitTests))-                  1-            , dapp = dapp-            , opts = opts-            }-        v <- mkVty-        _ <- customMain v mkVty Nothing (app opts) (ui :: UiState)-        return ()+main :: UnitTestOptions -> FilePath -> Maybe BuildOutput -> IO ()+main opts root buildOutput = do+  let+    dapp = maybe emptyDapp (dappInfo root) buildOutput+    ui = ViewPicker $ UiTestPickerState+      { tests =+          list+            TestPickerPane+            (Vec.fromList+             (concatMap+              (debuggableTests opts)+              dapp.unitTests))+            1+      , dapp = dapp+      , opts = opts+      }+  v <- mkVty+  _ <- customMain v mkVty Nothing (app opts) (ui :: UiState)+  return ()  takeStep   :: (?fetcher :: Fetcher@@ -400,6 +397,11 @@       (traverseOf $ _ViewContracts % #contracts)       (handleListEvent e)     pure ()+  ViewPicker _s -> do+    Brick.zoom+      (traverseOf $ _ViewPicker % #tests)+      (handleListEvent e)+    pure()   _ -> pure ()  -- Contracts: Up - list up@@ -409,6 +411,11 @@     Brick.zoom       (traverseOf $ _ViewContracts % #contracts)       (handleListEvent e)+  ViewPicker _s -> do+    Brick.zoom+      (traverseOf $ _ViewPicker % #tests)+      (handleListEvent e)+    pure()   _ -> pure ()  -- Vm Overview: Esc - return to test picker or exit@@ -558,7 +565,7 @@ appEvent (VtyEvent (V.EvKey (V.KChar '0') [])) = get >>= \case   ViewVm s ->     case view (#vm % #result) s of-      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->+      Just (HandleEffect (Choose (PleaseChoosePath _ contin))) ->         takeStep (s & set #stepper (Stepper.evm (contin True) >> s.stepper))           (Step 1)       _ -> pure ()@@ -568,7 +575,7 @@ appEvent (VtyEvent (V.EvKey (V.KChar '1') [])) = get >>= \case   ViewVm s ->     case s.vm.result of-      Just (VMFailure (Choose (PleaseChoosePath _ contin))) ->+      Just (HandleEffect (Choose (PleaseChoosePath _ contin))) ->         takeStep (s & set #stepper (Stepper.evm (contin False) >> s.stepper))           (Step 1)       _ -> pure ()@@ -865,7 +872,7 @@          vBox            [ withHighlight True (str ("#" ++ show i ++ " "))                <+> ourWrap (Text.unpack $ prettyIfConcreteWord w)-           , dim (txt ("   " <> case unlit w of+           , dim (txt ("   " <> case maybeLitWord w of                        Nothing -> ""                        Just u -> showWordExplanation u ui.testOpts.dapp))            ])@@ -879,10 +886,14 @@       "VMSuccess: " <> (show $ ByteStringS msg)     Just (VMSuccess (msg)) ->       "VMSuccess: <symbolicbuffer> " <> (show msg)-    Just (VMFailure (EVM.Revert msg)) ->+    Just (VMFailure (Revert msg)) ->       "VMFailure: " <> (show msg)     Just (VMFailure err) ->       "VMFailure: " <> show err+    Just (Unfinished p) ->+      "Could not continue execution: " <> show p+    Just (HandleEffect e) ->+      "Handling side effect: " <> show e     Nothing ->       "Executing EVM code in " <> show vm.state.contract @@ -982,10 +993,13 @@     Nothing -> padBottom Max (hBorderWithLabel (txt "<no source map>"))     Just sm ->           let-            rows = dappSrcs.lines !! sm.file-            subrange = lineSubrange rows (sm.offset, sm.length)+            rows = dappSrcs.lines !? sm.file+            subrange :: Int -> Maybe (Int, Int)+            subrange i = do+              rs <- rows+              lineSubrange rs (sm.offset, sm.length) i             fileName :: Maybe Text-            fileName = preview (ix sm.file % _1) dapp.sources.files+            fileName = T.pack . fst <$> (dapp.sources.files !? sm.file)             lineNo :: Maybe Int             lineNo = ((\a -> Just (a - 1)) . snd) =<< srcMapCodePos dapp.sources sm           in vBox

@@ -2,11 +2,11 @@  import Prelude hiding (Word) -import qualified EVM import EVM (initialContract) import EVM.FeeSchedule import EVM.RLP import EVM.Types+import EVM.Format (hexText) import EVM.Expr (litAddr) import EVM.Sign @@ -201,7 +201,7 @@  instance FromJSON Transaction where   parseJSON (JSON.Object val) = do-    tdata    <- dataField val "data"+    tdata    <- hexText <$> (val JSON..: "data")     gasLimit <- word64Field val "gasLimit"     gasPrice <- fmap read <$> val JSON..:? "gasPrice"     maxPrio  <- fmap read <$> val JSON..:? "maxPriorityFeePerGas"@@ -226,17 +226,17 @@   parseJSON invalid =     JSON.typeMismatch "Transaction" invalid -accountAt :: Addr -> Getter (Map Addr EVM.Contract) EVM.Contract+accountAt :: Addr -> Getter (Map Addr Contract) Contract accountAt a = (at a) % (to $ fromMaybe newAccount) -touchAccount :: Addr -> Map Addr EVM.Contract -> Map Addr EVM.Contract+touchAccount :: Addr -> Map Addr Contract -> Map Addr Contract touchAccount a = Map.insertWith (flip const) a newAccount -newAccount :: EVM.Contract-newAccount = initialContract $ EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")+newAccount :: Contract+newAccount = initialContract $ RuntimeCode (ConcreteRuntimeCode "")  -- | Increments origin nonce and pays gas deposit-setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr EVM.Contract -> Map Addr EVM.Contract+setupTx :: Addr -> Addr -> W256 -> Word64 -> Map Addr Contract -> Map Addr Contract setupTx origin coinbase gasPrice gasLimit prestate =   let gasCost = gasPrice * (num gasLimit)   in (Map.adjust ((over #nonce   (+ 1))@@ -247,7 +247,7 @@ -- | 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 -> VM initTx vm = let     toAddr   = vm.state.contract     origin   = vm.tx.origin@@ -259,7 +259,7 @@     preState = setupTx origin coinbase gasPrice gasLimit vm.env.contracts     oldBalance = view (accountAt toAddr % #balance) preState     creation = vm.tx.isCreate-    initState = (case unlit value of+    initState = (case maybeLitWord value of       Just v -> ((Map.adjust (over #balance (subtract v))) origin)               . (Map.adjust (over #balance (+ v))) toAddr       Nothing -> id)

@@ -67,10 +67,10 @@        -- control flow -      e@(Revert a b) -> f e <> (foldl (foldProp f) mempty a) <> (go b)-      e@(Return a b c) -> f e <> (foldl (foldProp f) mempty a) <> (go b) <> (go c)-      e@(ITE a b c) -> f e <> (go a) <> (go b) <> (go c)+      e@(Success a b c) -> f e <> (foldl (foldProp f) mempty a) <> (go b) <> (go c)       e@(Failure a _) -> f e <> (foldl (foldProp f) mempty a)+      e@(Partial a _) -> f e <> (foldl (foldProp f) mempty a)+      e@(ITE a b c) -> f e <> (go a) <> (go b) <> (go c)        -- integers @@ -314,15 +314,14 @@   Failure a b -> do     a' <- mapM (mapPropM f) a     f (Failure a' b)-  Revert a b -> do+  Partial a b -> do     a' <- mapM (mapPropM f) a-    b' <- mapExprM f b-    f (Revert a' b')-  Return a b c -> do+    f (Partial a' b)+  Success a b c -> do     a' <- mapM (mapPropM f) a     b' <- mapExprM f b     c' <- mapExprM f c-    f (Return a' b' c')+    f (Success a' b' c')    ITE a b c -> do     a' <- mapExprM f a

@@ -1,4 +1,5 @@ {-# Language CPP #-}+{-# Language UndecidableInstances #-} {-# Language TemplateHaskell #-} {-# Language TypeApplications #-} {-# LANGUAGE GADTs #-}@@ -12,6 +13,7 @@ import Prelude hiding  (Word, LT, GT)  import Control.Arrow ((>>>))+import Control.Monad.State.Strict hiding (state) import Crypto.Hash hiding (SHA256) import Data.Aeson import Data.Aeson qualified as JSON@@ -20,45 +22,69 @@ import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.)) import Data.ByteArray qualified as BA import Data.Char-import Data.List (isPrefixOf, foldl')+import Data.List (foldl') import Data.ByteString (ByteString) import Data.ByteString qualified as BS import Data.ByteString.Base16 qualified as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString) import Data.ByteString.Char8 qualified as Char8 import Data.ByteString.Lazy (toStrict)+import Data.Data import Data.Word (Word8, Word32, Word64) import Data.DoubleWord import Data.DoubleWord.TH import Data.Map (Map)+import qualified Data.Map as Map import Data.Maybe (fromMaybe)+import Data.Set (Set) import Data.Sequence qualified as Seq import Data.Serialize qualified as Cereal-import Data.Text qualified as Text-import Data.Text.Encoding qualified as Text+import Data.Text qualified as T+import Data.Text.Encoding qualified as T import Data.Vector qualified as V+import Data.Vector.Storable qualified as SV import Numeric (readHex, showHex) import Options.Generic+import Optics.TH import EVM.Hexdump (paddedShowHex)-import Control.Monad+import EVM.FeeSchedule (FeeSchedule (..))+import Data.Tree.Zipper qualified as Zipper  import qualified Text.Regex.TDFA      as Regex import qualified Text.Read --- Some stuff for "generic programming", needed to create Word512-import Data.Data +-- Template Haskell --------------------------------------------------------------------------++ -- We need a 512-bit word for doing ADDMOD and MULMOD with full precision. mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256   [''Typeable, ''Data, ''Generic]  -newtype W256 = W256 Word256-  deriving-    ( Num, Integral, Real, Ord, Bits-    , Generic, FiniteBits, Enum, Eq , Bounded-    )+-- Symbolic IR ------------------------------------------------------------------------------------- +-- phantom type tags for AST construction+data EType+  = Buf+  | Storage+  | Log+  | EWord+  | Byte+  | End+  deriving (Typeable)+++-- Variables refering to a global environment+data GVar (a :: EType) where+  BufVar :: Int -> GVar Buf+  StoreVar :: Int -> GVar Storage++deriving instance Show (GVar a)+deriving instance Eq (GVar a)+deriving instance Ord (GVar a)++ {- |   Expr implements an abstract respresentation of an EVM program @@ -108,39 +134,6 @@   type level shenanigans tends to complicate implementation, we skip this for   now. -}---- phantom type tags for AST construction-data EType-  = Buf-  | Storage-  | Log-  | EWord-  | Byte-  | End-  deriving (Typeable)---- EVM errors-data Error-  = Invalid-  | IllegalOverflow-  | StackLimitExceeded-  | InvalidMemoryAccess-  | BadJumpDestination-  | StackUnderrun-  | SelfDestruct-  | TmpErr String-  deriving (Show, Eq, Ord)---- Variables refering to a global environment-data GVar (a :: EType) where-  BufVar :: Int -> GVar Buf-  StoreVar :: Int -> GVar Storage--deriving instance Show (GVar a)-deriving instance Eq (GVar a)-deriving instance Ord (GVar a)-- data Expr (a :: EType) where    -- identifiers@@ -155,7 +148,6 @@   IndexWord      :: Expr EWord -> Expr EWord -> Expr Byte   EqByte         :: Expr Byte  -> Expr Byte  -> Expr EWord -  -- TODO: rm readWord in favour of this?   JoinBytes      :: Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte                  -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte                  -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte@@ -165,11 +157,12 @@                  -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte                  -> Expr Byte -> Expr Byte -> Expr Byte -> Expr Byte                  -> Expr EWord+   -- control flow -  Revert         :: [Prop] -> Expr Buf -> Expr End-  Failure        :: [Prop] -> Error -> Expr End-  Return         :: [Prop] -> Expr Buf -> Expr Storage -> Expr End+  Partial        :: [Prop] -> PartialExec -> Expr End+  Failure        :: [Prop] -> EvmError -> Expr End+  Success        :: [Prop] -> Expr Buf -> Expr Storage -> Expr End   ITE            :: Expr EWord -> Expr End -> Expr End -> Expr End    -- integers@@ -372,6 +365,44 @@ deriving instance Eq (Expr a) deriving instance Ord (Expr a) ++-- Existential Wrapper -----------------------------------------------------------------------------+++data SomeExpr = forall a . Typeable a => SomeExpr (Expr a)++deriving instance Show SomeExpr++instance Eq SomeExpr where+  SomeExpr (a :: Expr b) == SomeExpr (c :: Expr d) =+    case eqT @b @d of+      Just Refl -> a == c+      Nothing -> False++instance Ord SomeExpr where+  compare (SomeExpr (a :: Expr b)) (SomeExpr (c :: Expr d)) =+    case eqT @b @d of+      Just Refl -> compare a c+      Nothing -> compare (toNum a) (toNum c)++toNum :: (Typeable a) => Expr a -> Int+toNum (_ :: Expr a) =+  case eqT @a @Buf of+    Just Refl -> 1+    Nothing -> case eqT @a @Storage of+      Just Refl -> 2+      Nothing -> case eqT @a @Log of+        Just Refl -> 3+        Nothing -> case eqT @a @EWord of+          Just Refl -> 4+          Nothing -> case eqT @a @Byte of+            Just Refl -> 5+            Nothing -> 6+++-- Propostions -------------------------------------------------------------------------------------++ -- The language of assertable expressions. -- This is useful when generating SMT queries based on Expr instances, since -- the translation of Eq and other boolean operators from Expr to SMT is an@@ -452,26 +483,479 @@   PImpl a b <= PImpl c d = a <= c && b <= d   _ <= _ = False ++-- Errors ------------------------------------------------------------------------------------------+++-- | Core EVM Error Types+data EvmError+  = BalanceTooLow W256 W256+  | UnrecognizedOpcode Word8+  | SelfDestruction+  | StackUnderrun+  | BadJumpDestination+  | Revert (Expr Buf)+  | OutOfGas Word64 Word64+  | StackLimitExceeded+  | IllegalOverflow+  | StateChangeWhileStatic+  | InvalidMemoryAccess+  | CallDepthLimitReached+  | MaxCodeSizeExceeded W256 W256+  | InvalidFormat+  | PrecompileFailure+  | ReturnDataOutOfBounds+  | NonceOverflow+  | BadCheatCode FunctionSelector+  deriving (Show, Eq, Ord)++-- | Sometimes we can only partially execute a given program+data PartialExec+  = UnexpectedSymbolicArg  { pc :: Int, msg  :: String, args  :: [SomeExpr] }+  | MaxIterationsReached  { pc :: Int, addr :: Addr }+  deriving (Show, Eq, Ord)++-- | Effect types used by the vm implementation for side effects & control flow+data Effect+  = Query Query+  | Choose Choose+deriving instance Show Effect++-- | Queries halt execution until resolved through RPC calls or SMT queries+data Query where+  PleaseFetchContract :: Addr -> (Contract -> EVM ()) -> Query+  PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM ()) -> Query+  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM ()) -> Query+  PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query++-- | Execution could proceed down one of two branches+data Choose where+  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM ()) -> Choose++-- | The possible return values of a SMT query+data BranchCondition = Case Bool | Unknown+  deriving Show++instance Show Query where+  showsPrec _ = \case+    PleaseFetchContract addr _ ->+      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)+    PleaseFetchSlot addr slot _ ->+      (("<EVM.Query: fetch slot "+        ++ show slot ++ " for "+        ++ show addr ++ ">") ++)+    PleaseAskSMT condition constraints _ ->+      (("<EVM.Query: ask SMT about "+        ++ show condition ++ " in context "+        ++ show constraints ++ ">") ++)+    PleaseDoFFI cmd _ ->+      (("<EVM.Query: do ffi: " ++ (show cmd)) ++)++instance Show Choose where+  showsPrec _ = \case+    PleaseChoosePath _ _ ->+      (("<EVM.Choice: waiting for user to select path (0,1)") ++)++-- | The possible result states of a VM+data VMResult+  = VMFailure EvmError     -- ^ An operation failed+  | VMSuccess (Expr Buf)   -- ^ Reached STOP, RETURN, or end-of-code+  | HandleEffect Effect    -- ^ An effect must be handled for execution to continue+  | Unfinished PartialExec -- ^ Execution could not continue further++deriving instance Show VMResult+++-- VM State ----------------------------------------------------------------------------------------+++-- | The state of a stepwise EVM execution+data VM = VM+  { result         :: Maybe VMResult+  , state          :: FrameState+  , frames         :: [Frame]+  , env            :: Env+  , block          :: Block+  , tx             :: TxState+  , logs           :: [Expr Log]+  , traces         :: Zipper.TreePos Zipper.Empty Trace+  , cache          :: Cache+  , burned         :: {-# UNPACK #-} !Word64+  , iterations     :: Map CodeLocation (Int, [Expr EWord]) -- ^ how many times we've visited a loc, and what the contents of the stack were when we were there last+  , constraints    :: [Prop]+  , keccakEqs      :: [Prop]+  , allowFFI       :: Bool+  , overrideCaller :: Maybe Addr+  }+  deriving (Show, Generic)++-- | Alias for the type of e.g. @exec1@.+type EVM a = State VM a++-- | An entry in the VM's "call/create stack"+data Frame = Frame+  { context :: FrameContext+  , state   :: FrameState+  }+  deriving (Show)++-- | Call/create info+data FrameContext+  = CreationContext+    { address         :: Addr+    , codehash        :: Expr EWord+    , createreversion :: Map Addr Contract+    , substate        :: SubState+    }+  | CallContext+    { target        :: Addr+    , context       :: Addr+    , offset        :: W256+    , size          :: W256+    , codehash      :: Expr EWord+    , abi           :: Maybe W256+    , calldata      :: Expr Buf+    , callreversion :: (Map Addr Contract, Expr Storage)+    , subState      :: SubState+    }+  deriving (Show, Generic)++-- | The "accrued substate" across a transaction+data SubState = SubState+  { selfdestructs       :: [Addr]+  , touchedAccounts     :: [Addr]+  , accessedAddresses   :: Set Addr+  , accessedStorageKeys :: Set (Addr, W256)+  , refunds             :: [(Addr, Word64)]+  -- in principle we should include logs here, but do not for now+  }+  deriving (Show)++-- | The "registers" of the VM along with memory and data stack+data FrameState = FrameState+  { contract     :: Addr+  , codeContract :: Addr+  , code         :: ContractCode+  , pc           :: {-# UNPACK #-} !Int+  , stack        :: [Expr EWord]+  , memory       :: Expr Buf+  , memorySize   :: Word64+  , calldata     :: Expr Buf+  , callvalue    :: Expr EWord+  , caller       :: Expr EWord+  , gas          :: {-# UNPACK #-} !Word64+  , returndata   :: Expr Buf+  , static       :: Bool+  }+  deriving (Show, Generic)++-- | The state that spans a whole transaction+data TxState = TxState+  { gasprice    :: W256+  , gaslimit    :: Word64+  , priorityFee :: W256+  , origin      :: Addr+  , toAddr      :: Addr+  , value       :: Expr EWord+  , substate    :: SubState+  , isCreate    :: Bool+  , txReversion :: Map Addr Contract+  }+  deriving (Show)++-- | When doing symbolic execution, we have three different+-- ways to model the storage of contracts. This determines+-- not only the initial contract storage model but also how+-- RPC or state fetched contracts will be modeled.+data StorageModel+  = ConcreteS    -- ^ Uses `Concrete` Storage. Reading / Writing from abstract+                 -- locations causes a runtime failure. Can be nicely combined with RPC.++  | SymbolicS    -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,+                 -- but always done using an SMT array with no default value.++  | InitialS     -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,+                 -- but always done using an SMT array with 0 as the default value.++  deriving (Read, Show)++instance ParseField StorageModel++-- | Various environmental data+data Env = Env+  { contracts    :: Map Addr Contract+  , chainId      :: W256+  , storage      :: Expr Storage+  , origStorage  :: Map W256 (Map W256 W256)+  , sha3Crack    :: Map W256 ByteString+  }+  deriving (Show, Generic)++-- | Data about the block+data Block = Block+  { coinbase    :: Addr+  , timestamp   :: Expr EWord+  , number      :: W256+  , prevRandao  :: W256+  , gaslimit    :: Word64+  , baseFee     :: W256+  , maxCodeSize :: W256+  , schedule    :: FeeSchedule Word64+  } deriving (Show, Generic)++-- | The state of a contract+data Contract = Contract+  { contractcode :: ContractCode+  , balance      :: W256+  , nonce        :: W256+  , codehash     :: Expr EWord+  , opIxMap      :: SV.Vector Int+  , codeOps      :: V.Vector (Int, Op)+  , external     :: Bool+  }+  deriving (Show)+++-- Bytecode Representations ------------------------------------------------------------------------+++-- | A unique id for a given pc+type CodeLocation = (Addr, Int)++-- | The cache is data that can be persisted for efficiency:+-- any expensive query that is constant at least within a block.+data Cache = Cache+  { fetchedContracts :: Map Addr Contract+  , fetchedStorage :: Map W256 (Map W256 W256)+  , path :: Map (CodeLocation, Int) Bool+  } deriving (Show, Generic)++instance Semigroup Cache where+  a <> b = Cache+    { fetchedContracts = Map.unionWith unifyCachedContract a.fetchedContracts b.fetchedContracts+    , fetchedStorage = Map.unionWith unifyCachedStorage a.fetchedStorage b.fetchedStorage+    , path = mappend a.path b.path+    }++instance Monoid Cache where+  mempty = Cache { fetchedContracts = mempty+                 , fetchedStorage = mempty+                 , path = mempty+                 }++unifyCachedStorage :: Map W256 W256 -> Map W256 W256 -> Map W256 W256+unifyCachedStorage _ _ = undefined++-- only intended for use in Cache merges, where we expect+-- everything to be Concrete+unifyCachedContract :: Contract -> Contract -> Contract+unifyCachedContract _ _ = undefined+  {-+unifyCachedContract a b = a & set storage merged+  where merged = case (view storage a, view storage b) of+                   (ConcreteStore sa, ConcreteStore sb) ->+                     ConcreteStore (mappend sa sb)+                   _ ->+                     view storage a+   -}+++-- Bytecode Representations ------------------------------------------------------------------------+++{- |+  A contract is either in creation (running its "constructor") or+  post-creation, and code in these two modes is treated differently+  by instructions like @EXTCODEHASH@, so we distinguish these two+  code types.++  The definition follows the structure of code output by solc. We need to use+  some heuristics here to deal with symbolic data regions that may be present+  in the bytecode since the fully abstract case is impractical:++  - initcode has concrete code, followed by an abstract data "section"+  - runtimecode has a fixed length, but may contain fixed size symbolic regions (due to immutable)++  hopefully we do not have to deal with dynamic immutable before we get a real data section...+-}+data ContractCode+  = InitCode ByteString (Expr Buf) -- ^ "Constructor" code, during contract creation+  | RuntimeCode RuntimeCode -- ^ "Instance" code, after contract creation+  deriving (Show, Ord)++-- | We have two variants here to optimize the fully concrete case.+-- ConcreteRuntimeCode just wraps a ByteString+-- SymbolicRuntimeCode is a fixed length vector of potentially symbolic bytes, which lets us handle symbolic pushdata (e.g. from immutable variables in solidity).+data RuntimeCode+  = ConcreteRuntimeCode ByteString+  | SymbolicRuntimeCode (V.Vector (Expr Byte))+  deriving (Show, Eq, Ord)++-- runtime err when used for symbolic code+instance Eq ContractCode where+  InitCode a b  == InitCode c d  = a == c && b == d+  RuntimeCode x == RuntimeCode y = x == y+  _ == _ = False+++-- Execution Traces --------------------------------------------------------------------------------+++data Trace = Trace+  { opIx      :: Int+  , contract  :: Contract+  , tracedata :: TraceData+  }+  deriving (Show, Generic)++data TraceData+  = EventTrace (Expr EWord) (Expr Buf) [Expr EWord]+  | FrameTrace FrameContext+  | QueryTrace Query+  | ErrorTrace EvmError+  | EntryTrace Text+  | ReturnTrace (Expr Buf) FrameContext+  deriving (Show, Generic)+++-- VM Initialization -------------------------------------------------------------------------------+++-- | A specification for an initial VM state+data VMOpts = VMOpts+  { contract :: Contract+  , calldata :: (Expr Buf, [Prop])+  , initialStorage :: Expr Storage+  , value :: Expr EWord+  , priorityFee :: W256+  , address :: Addr+  , caller :: Expr EWord+  , origin :: Addr+  , gas :: Word64+  , gaslimit :: Word64+  , number :: W256+  , timestamp :: Expr EWord+  , coinbase :: Addr+  , prevRandao :: W256+  , maxCodeSize :: W256+  , blockGaslimit :: Word64+  , gasprice :: W256+  , baseFee :: W256+  , schedule :: FeeSchedule Word64+  , chainId :: W256+  , create :: Bool+  , txAccessList :: Map Addr [W256]+  , allowFFI :: Bool+  } deriving Show+++-- Opcodes -----------------------------------------------------------------------------------------+++type Op = GenericOp (Expr EWord)++data GenericOp a+  = OpStop+  | OpAdd+  | OpMul+  | OpSub+  | OpDiv+  | OpSdiv+  | OpMod+  | OpSmod+  | OpAddmod+  | OpMulmod+  | OpExp+  | OpSignextend+  | OpLt+  | OpGt+  | OpSlt+  | OpSgt+  | OpEq+  | OpIszero+  | OpAnd+  | OpOr+  | OpXor+  | OpNot+  | OpByte+  | OpShl+  | OpShr+  | OpSar+  | OpSha3+  | OpAddress+  | OpBalance+  | OpOrigin+  | OpCaller+  | OpCallvalue+  | OpCalldataload+  | OpCalldatasize+  | OpCalldatacopy+  | OpCodesize+  | OpCodecopy+  | OpGasprice+  | OpExtcodesize+  | OpExtcodecopy+  | OpReturndatasize+  | OpReturndatacopy+  | OpExtcodehash+  | OpBlockhash+  | OpCoinbase+  | OpTimestamp+  | OpNumber+  | OpPrevRandao+  | OpGaslimit+  | OpChainid+  | OpSelfbalance+  | OpBaseFee+  | OpPop+  | OpMload+  | OpMstore+  | OpMstore8+  | OpSload+  | OpSstore+  | OpJump+  | OpJumpi+  | OpPc+  | OpMsize+  | OpGas+  | OpJumpdest+  | OpCreate+  | OpCall+  | OpStaticcall+  | OpCallcode+  | OpReturn+  | OpDelegatecall+  | OpCreate2+  | OpRevert+  | OpSelfdestruct+  | OpDup !Word8+  | OpSwap !Word8+  | OpLog !Word8+  | OpPush a+  | OpUnknown Word8+  deriving (Show, Eq, Functor)+++-- Function Selectors ------------------------------------------------------------------------------++ -- | https://docs.soliditylang.org/en/v0.8.19/abi-spec.html#function-selector newtype FunctionSelector = FunctionSelector { unFunctionSelector :: Word32 }   deriving (Num, Eq, Ord, Real, Enum, Integral) instance Show FunctionSelector where show s = "0x" <> showHex s "" -unlit :: Expr EWord -> Maybe W256-unlit (Lit x) = Just x-unlit _ = Nothing -unlitByte :: Expr Byte -> Maybe Word8-unlitByte (LitByte x) = Just x-unlitByte _ = Nothing+-- ByteString wrapper ------------------------------------------------------------------------------ ++-- Newtype wrapper for ByteString to allow custom instances newtype ByteStringS = ByteStringS ByteString deriving (Eq, Generic)  instance Show ByteStringS where-  show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x+  show (ByteStringS x) = ("0x" ++) . T.unpack . fromBinary $ x     where       fromBinary =-        Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex+        T.decodeUtf8 . toStrict . toLazyByteString . byteStringHex  instance JSON.FromJSON ByteStringS where   parseJSON (JSON.String x) = case BS16.decodeBase16' x of@@ -480,20 +964,19 @@   parseJSON _ = mzero  instance JSON.ToJSON ByteStringS where-  toJSON (ByteStringS x) = JSON.String (Text.pack $ "0x" ++ (concatMap (paddedShowHex 2) . BS.unpack $ x))+  toJSON (ByteStringS x) = JSON.String (T.pack $ "0x" ++ (concatMap (paddedShowHex 2) . BS.unpack $ x)) -newtype Addr = Addr { addressWord160 :: Word160 }++-- Word256 wrapper ---------------------------------------------------------------------------------+++-- Newtype wrapper around Word256 to allow custom instances+newtype W256 = W256 Word256   deriving-    ( Num, Integral, Real, Ord, Enum-    , Eq, Generic, Bits, FiniteBits+    ( Num, Integral, Real, Ord, Bits+    , Generic, FiniteBits, Enum, Eq , Bounded     )-instance JSON.ToJSON Addr where-  toJSON = JSON.String . Text.pack . show -maybeLitWord :: Expr EWord -> Maybe W256-maybeLitWord (Lit w) = Just w-maybeLitWord _ = Nothing- instance Read W256 where   readsPrec _ "0x" = [(0, "")]   readsPrec n s = first W256 <$> readsPrec n s@@ -502,11 +985,37 @@   showsPrec _ s = ("0x" ++) . showHex s  instance JSON.ToJSON W256 where-  toJSON x = JSON.String  $ Text.pack ("0x" ++ pad ++ cutshow)+  toJSON x = JSON.String  $ T.pack ("0x" ++ pad ++ cutshow)     where       cutshow = drop 2 $ show x       pad = replicate (64 - length (cutshow)) '0' +instance FromJSON W256 where+  parseJSON v = do+    s <- T.unpack <$> parseJSON v+    case reads s of+      [(x, "")]  -> return x+      _          -> fail $ "invalid hex word (" ++ s ++ ")"++instance FromJSONKey W256 where+  fromJSONKey = FromJSONKeyTextParser $ \s ->+    case reads (T.unpack s) of+      [(x, "")]  -> return x+      _          -> fail $ "invalid word (" ++ T.unpack s ++ ")"++wordField :: JSON.Object -> Key -> JSON.Parser W256+wordField x f = ((readNull 0) . T.unpack)+                  <$> (x .: f)++instance ParseField W256+instance ParseFields W256+instance ParseRecord W256 where+  parseRecord = fmap getOnly parseRecord+++-- Word64 wrapper ----------------------------------------------------------------------------------++ newtype W64 = W64 Data.Word.Word64   deriving     ( Num, Integral, Real, Ord, Generic@@ -522,8 +1031,22 @@   showsPrec _ s = ("0x" ++) . showHex s  instance JSON.ToJSON W64 where-  toJSON x = JSON.String  $ Text.pack $ show x+  toJSON x = JSON.String  $ T.pack $ show x +word64Field :: JSON.Object -> Key -> JSON.Parser Word64+word64Field x f = ((readNull 0) . T.unpack)+                  <$> (x .: f)+++-- Addresses ---------------------------------------------------------------------------------------+++newtype Addr = Addr { addressWord160 :: Word160 }+  deriving+    ( Num, Integral, Real, Ord, Enum+    , Eq, Generic, Bits, FiniteBits+    )+ instance Read Addr where   readsPrec _ ('0':'x':s) = readHex s   readsPrec _ s = readHex s@@ -534,14 +1057,6 @@         str = replicate (40 - length hex) '0' ++ hex     in "0x" ++ toChecksumAddress str ++ drop 40 str -instance JSON.ToJSONKey Addr where-  toJSONKey = JSON.toJSONKeyText (addrKey)-    where-      addrKey :: Addr -> Text-      addrKey addr = Text.pack $ replicate (40 - length hex) '0' ++ hex-        where-          hex = show addr- -- https://eips.ethereum.org/EIPS/eip-55 toChecksumAddress :: String -> String toChecksumAddress addr = zipWith transform nibbles addr@@ -549,113 +1064,69 @@     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--strip0x' :: String -> String-strip0x' s = if "0x" `isPrefixOf` s then drop 2 s else s--instance FromJSON W256 where-  parseJSON v = do-    s <- Text.unpack <$> parseJSON v-    case reads s of-      [(x, "")]  -> return x-      _          -> fail $ "invalid hex word (" ++ s ++ ")"+instance JSON.ToJSON Addr where+  toJSON = JSON.String . T.pack . show  instance FromJSON Addr where   parseJSON v = do-    s <- Text.unpack <$> parseJSON v+    s <- T.unpack <$> parseJSON v     case reads s of       [(x, "")] -> return x       _         -> fail $ "invalid address (" ++ s ++ ")" -#if MIN_VERSION_aeson(1, 0, 0)--instance FromJSONKey W256 where-  fromJSONKey = FromJSONKeyTextParser $ \s ->-    case reads (Text.unpack s) of-      [(x, "")]  -> return x-      _          -> fail $ "invalid word (" ++ Text.unpack s ++ ")"+instance JSON.ToJSONKey Addr where+  toJSONKey = JSON.toJSONKeyText (addrKey)+    where+      addrKey :: Addr -> Text+      addrKey addr = T.pack $ replicate (40 - length hex) '0' ++ hex+        where+          hex = show addr  instance FromJSONKey Addr where   fromJSONKey = FromJSONKeyTextParser $ \s ->-    case reads (Text.unpack s) of+    case reads (T.unpack s) of       [(x, "")] -> return x-      _         -> fail $ "invalid word (" ++ Text.unpack s ++ ")"+      _         -> fail $ "invalid word (" ++ T.unpack s ++ ")" -#endif+addrField :: JSON.Object -> Key -> JSON.Parser Addr+addrField x f = (read . T.unpack) <$> (x .: f) -instance ParseField W256-instance ParseFields W256-instance ParseRecord W256 where-  parseRecord = fmap getOnly parseRecord+addrFieldMaybe :: JSON.Object -> Key -> JSON.Parser (Maybe Addr)+addrFieldMaybe x f = (Text.Read.readMaybe . T.unpack) <$> (x .: f)  instance ParseField Addr instance ParseFields Addr instance ParseRecord Addr where   parseRecord = fmap getOnly parseRecord -hexByteString :: String -> ByteString -> ByteString-hexByteString msg bs =-  case BS16.decodeBase16 bs of-    Right x -> x-    _ -> error ("invalid hex bytestring for " ++ msg) -hexText :: Text -> ByteString-hexText t =-  case BS16.decodeBase16 (Text.encodeUtf8 (Text.drop 2 t)) of-    Right x -> x-    _ -> error ("invalid hex bytestring " ++ show t)+-- Nibbles ----------------------------------------------------------------------------------------- -readN :: Integral a => String -> a-readN s = fromIntegral (read s :: Integer) -readNull :: Read a => a -> String -> a-readNull x = fromMaybe x . Text.Read.readMaybe+-- | A four bit value+newtype Nibble = Nibble Word8+  deriving ( Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic) -wordField :: JSON.Object -> Key -> JSON.Parser W256-wordField x f = ((readNull 0) . Text.unpack)-                  <$> (x .: f)+instance Show Nibble where+  show = (:[]) . intToDigit . num -word64Field :: JSON.Object -> Key -> JSON.Parser Word64-word64Field x f = ((readNull 0) . Text.unpack)-                  <$> (x .: f) -addrField :: JSON.Object -> Key -> JSON.Parser Addr-addrField x f = (read . Text.unpack) <$> (x .: f)+-- Conversions ------------------------------------------------------------------------------------- -addrFieldMaybe :: JSON.Object -> Key -> JSON.Parser (Maybe Addr)-addrFieldMaybe x f = (Text.Read.readMaybe . Text.unpack) <$> (x .: f) -dataField :: JSON.Object -> Key -> JSON.Parser ByteString-dataField x f = hexText <$> (x .: f)- toWord512 :: W256 -> Word512 toWord512 (W256 x) = fromHiAndLo 0 x  fromWord512 :: Word512 -> W256 fromWord512 x = W256 (loWord x) -num :: (Integral a, Num b) => a -> b-num = fromIntegral--padLeft :: Int -> ByteString -> ByteString-padLeft n xs = BS.replicate (n - BS.length xs) 0 <> xs--padRight :: Int -> ByteString -> ByteString-padRight n xs = xs <> BS.replicate (n - BS.length xs) 0--padRight' :: Int -> String -> String-padRight' n xs = xs <> replicate (n - 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+maybeLitByte :: Expr Byte -> Maybe Word8+maybeLitByte (LitByte x) = Just x+maybeLitByte _ = Nothing -padLeft' :: Int -> V.Vector (Expr Byte) -> V.Vector (Expr Byte)-padLeft' n xs = V.replicate (n - length xs) (LitByte 0) <> xs+maybeLitWord :: Expr EWord -> Maybe W256+maybeLitWord (Lit w) = Just w+maybeLitWord _ = Nothing  word256 :: ByteString -> Word256 word256 xs | BS.length xs == 1 =@@ -692,12 +1163,6 @@ word160Bytes (Addr (Word160 a (Word128 b c))) =   Cereal.encode a <> Cereal.encode b <> Cereal.encode c -newtype Nibble = Nibble Word8-  deriving ( Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic)--instance Show Nibble where-  show = (:[]) . intToDigit . num- -- Get first and second Nibble from byte hi, lo :: Word8 -> Nibble hi b = Nibble $ b `shiftR` 4@@ -728,8 +1193,17 @@     then let (W256 (Word256 _ (Word128 _ n'))) = n in Just (fromIntegral n')     else Nothing --- Keccak hashing+bssToBs :: ByteStringS -> ByteString+bssToBs (ByteStringS bs) = bs +-- | This just overflows silently, and is generally a terrible footgun, should be removed+num :: (Integral a, Num b) => a -> b+num = fromIntegral+++-- Keccak hashing ----------------------------------------------------------------------------------++ keccakBytes :: ByteString -> ByteString keccakBytes =   (hash :: ByteString -> Digest Keccak_256)@@ -754,8 +1228,10 @@     >>> word32     >>> FunctionSelector --- Utils +-- Utils -------------------------------------------------------------------------------------------++ concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b] concatMapM f xs = fmap concat (mapM f xs) @@ -766,26 +1242,44 @@       Regex.defaultCompOpt { Regex.lastStarGreedy = True }     execOpts =       Regex.defaultExecOpt { Regex.captureGroups = False }-    regex = Regex.makeRegexOpts compOpts execOpts (Text.unpack regexSource)+    regex = Regex.makeRegexOpts compOpts execOpts (T.unpack regexSource)   in-    Regex.matchTest regex . Seq.fromList . Text.unpack+    Regex.matchTest regex . Seq.fromList . T.unpack -data VMTrace =-  VMTrace-  { tracePc      :: Int-  , traceOp      :: Int-  , traceStack   :: [W256]-  , traceMemSize :: Data.Word.Word64-  , traceDepth   :: Int-  , traceGas     :: Data.Word.Word64-  , traceError   :: Maybe String-  } deriving (Generic, Show)-instance JSON.ToJSON VMTrace where-  toEncoding = JSON.genericToEncoding JSON.defaultOptions-instance JSON.FromJSON VMTrace+readNull :: Read a => a -> String -> a+readNull x = fromMaybe x . Text.Read.readMaybe -bsToHex :: ByteString -> String-bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)+padLeft :: Int -> ByteString -> ByteString+padLeft n xs = BS.replicate (n - BS.length xs) 0 <> xs -bssToBs :: ByteStringS -> ByteString-bssToBs (ByteStringS bs) = bs+padLeft' :: Int -> V.Vector (Expr Byte) -> V.Vector (Expr Byte)+padLeft' n xs = V.replicate (n - length xs) (LitByte 0) <> xs++padRight :: Int -> ByteString -> ByteString+padRight n xs = xs <> BS.replicate (n - BS.length xs) 0++padRight' :: Int -> String -> String+padRight' n xs = xs <> replicate (n - length xs) '0'++-- We need this here instead of Format for cyclic import reasons...+formatString :: ByteString -> String+formatString bs =+  case T.decodeUtf8' (fst (BS.spanEnd (== 0) bs)) of+    Right s -> "\"" <> T.unpack s <> "\""+    Left _ -> "❮utf8 decode failed❯: " <> (show $ ByteStringS bs)++-- Optics ------------------------------------------------------------------------------------------+++makeFieldLabelsNoPrefix ''VM+makeFieldLabelsNoPrefix ''FrameState+makeFieldLabelsNoPrefix ''TxState+makeFieldLabelsNoPrefix ''SubState+makeFieldLabelsNoPrefix ''Cache+makeFieldLabelsNoPrefix ''Trace+makeFieldLabelsNoPrefix ''VMOpts+makeFieldLabelsNoPrefix ''Frame+makeFieldLabelsNoPrefix ''FrameContext+makeFieldLabelsNoPrefix ''Contract+makeFieldLabelsNoPrefix ''Env+makeFieldLabelsNoPrefix ''Block

@@ -5,7 +5,7 @@  import Prelude hiding (Word) -import EVM hiding (Unknown, path)+import EVM import EVM.ABI import EVM.Concrete import EVM.SMT@@ -21,9 +21,8 @@ import EVM.Fetch qualified as Fetch import EVM.Format import EVM.Solidity-import EVM.SymExec qualified as SymExec-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts)-import EVM.Types hiding (Failure)+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts(..))+import EVM.Types import EVM.Transaction (initTx) import EVM.RLP import EVM.Stepper (Stepper, interpret)@@ -63,14 +62,15 @@ import GHC.Natural import System.Environment (lookupEnv) import System.IO (hFlush, stdout)-import Test.QuickCheck hiding (verbose)+import Test.QuickCheck hiding (verbose, Success, Failure)+import qualified Test.QuickCheck as QC  data UnitTestOptions = UnitTestOptions   { rpcInfo     :: Fetch.RpcInfo   , solvers     :: SolverGroup   , verbose     :: Maybe Int   , maxIter     :: Maybe Integer-  , askSmtIters :: Maybe Integer+  , askSmtIters :: Integer   , smtDebug    :: Bool   , maxDepth    :: Maybe Int   , smtTimeout  :: Maybe Natural@@ -122,36 +122,31 @@ -- | Generate VeriOpts from UnitTestOptions makeVeriOpts :: UnitTestOptions -> VeriOpts makeVeriOpts opts =-   defaultVeriOpts { SymExec.debug = opts.smtDebug-                   , SymExec.maxIter = opts.maxIter-                   , SymExec.askSmtIters = opts.askSmtIters-                   , SymExec.rpcInfo = opts.rpcInfo+   defaultVeriOpts { debug = opts.smtDebug+                   , maxIter = opts.maxIter+                   , askSmtIters = opts.askSmtIters+                   , rpcInfo = opts.rpcInfo                    } --- | Top level CLI endpoint for dapp-test-dappTest :: UnitTestOptions -> String -> Maybe String -> IO Bool-dappTest opts solcFile cache' = do-  out <- liftIO $ readSolc solcFile-  case out of-    Just (contractMap, _) -> do-      let unitTests = findUnitTests opts.match $ 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-            evmcache = mconcat [vm.cache | vm <- vms]-          in-            liftIO $ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts evmcache)--      return $ and passing+-- | Top level CLI endpoint for hevm test+unitTest :: UnitTestOptions -> Contracts -> Maybe String -> IO Bool+unitTest opts (Contracts cs) cache' = do+  let unitTests = findUnitTests opts.match $ Map.elems cs+  results <- concatMapM (runUnitTestContract opts cs) unitTests+  let (passing, vms) = unzip results+  case cache' of     Nothing ->-      error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'")+      pure ()+    Just path ->+      -- merge all of the post-vm caches and save into the state+      let+        evmcache = mconcat [vm.cache | vm <- vms]+      in+        liftIO $ Git.saveFacts (Git.RepoAt path) (Facts.cacheFacts evmcache) +  return $ and passing + -- | 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 -> SolcContract -> Stepper ()@@ -317,6 +312,8 @@           execWithCoverage >>= interpretWithCoverage opts . k         Stepper.Run ->           runWithCoverage >>= interpretWithCoverage opts . k+        Stepper.Wait (PleaseAskSMT (Lit c) _ continue) ->+          interpretWithCoverage opts (Stepper.evm (continue (Case (c > 0))) >>= k)         Stepper.Wait q ->           do m <- liftIO ((Fetch.oracle solvers rpcInfo) q)              zoom _1 (State.state (runState m)) >> interpretWithCoverage opts (k ())@@ -330,13 +327,13 @@ coverageReport   :: DappInfo   -> MultiSet SrcMap-  -> Map Text (Vector (Int, ByteString))+  -> Map FilePath (Vector (Int, ByteString)) coverageReport dapp cov =   let     sources :: SourceCache     sources = dapp.sources -    allPositions :: Set (Text, Int)+    allPositions :: Set (FilePath, Int)     allPositions =       ( Set.fromList       . mapMaybe (srcMapCodePos sources)@@ -348,17 +345,17 @@         )       ) -    srcMapCov :: MultiSet (Text, Int)+    srcMapCov :: MultiSet (FilePath, Int)     srcMapCov = MultiSet.mapMaybe (srcMapCodePos sources) cov -    linesByName :: Map Text (Vector ByteString)+    linesByName :: Map FilePath (Vector ByteString)     linesByName =       Map.fromList $ zipWith           (\(name, _) lines' -> (name, lines'))-          sources.files-          sources.lines+          (Map.elems sources.files)+          (Map.elems sources.lines) -    f :: Text -> Vector ByteString -> Vector (Int, ByteString)+    f :: FilePath -> Vector ByteString -> Vector (Int, ByteString)     f name =       Vector.imap         (\i bs ->@@ -439,7 +436,6 @@         Stepper.evm get        case vm1.result of-        Nothing -> error "internal error: setUp() did not end with a result"         Just (VMFailure _) -> liftIO $ do           Text.putStrLn "\x1b[31m[BAIL]\x1b[0m setUp() "           tick "\n"@@ -469,6 +465,7 @@             tick (Text.unlines bailing)            pure [(isRight r, vm) | (r, vm) <- details]+        _ -> error "internal error: setUp() did not end with a result"   runTest :: UnitTestOptions -> VM -> (Test, [AbiType]) -> IO (Text, Either Text Text, VM)@@ -685,7 +682,7 @@                  , maxShrinks      = maxBound                  }   quickCheckWithResult args (fuzzTest opts testName types vm) >>= \case-    Success numTests _ _ _ _ _ ->+    QC.Success numTests _ _ _ _ _ ->       pure ("\x1b[32m[PASS]\x1b[0m "              <> testName <> " (runs: " <> (pack $ show numTests) <> ")"              -- this isn't the post vm we actually want, as we@@ -693,7 +690,7 @@            , Right (passOutput vm opts testName)            , vm            )-    Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->+    QC.Failure _ _ _ _ _ _ _ _ _ _ failCase _ _ ->       let abiValue = decodeAbiValue (AbiTupleType (Vector.fromList types)) $ BSLazy.fromStrict $ hexText (pack $ concat failCase)           ppOutput = pack $ show abiValue       in do@@ -729,11 +726,13 @@                    .|| (readStorage' (litAddr cheatCode) (Lit 0x6661696c65640000000000000000000000000000000000000000000000000000) store .== Lit 1)         postcondition = curry $ case shouldFail of           True -> \(_, post) -> case post of-                                  Return _ _ store -> failed store+                                  Success _ _ store -> failed store                                   _ -> PBool True           False -> \(_, post) -> case post of-                                   Return _ _ store -> PNeg (failed store)-                                   _ -> PBool False+                                   Success _ _ store -> PNeg (failed store)+                                   Failure _ _ -> PBool False+                                   Partial _ _ -> PBool True+                                   _ -> error "Internal Error: Invalid leaf node"      vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcInfo) vm $       Stepper.evm $ do@@ -764,7 +763,7 @@     where       ctx = DappContext { info = dapp, env = mempty }       showRes = \case-                       Return _ _ _ -> if "proveFail" `isPrefixOf` testName+                       Success _ _ _ -> if "proveFail" `isPrefixOf` testName                                       then "Successful execution"                                       else "Failed: DSTest Assertion Violation"                        res ->@@ -999,7 +998,7 @@       Nothing  -> return (0,Lit 0,0,0,0,0)       Just url -> Fetch.fetchBlockFrom block' url >>= \case         Nothing -> error "Could not fetch block"-        Just EVM.Block{..} -> return (  coinbase+        Just Block{..} -> return (  coinbase                                       , timestamp                                       , number                                       , prevRandao

@@ -2,18 +2,18 @@  import Prelude hiding (Word) -import EVM qualified-import EVM (initialContract)+import EVM (initialContract, makeVm) import EVM.Concrete qualified as EVM import EVM.Dapp (emptyDapp) import EVM.Expr (litAddr) import EVM.FeeSchedule qualified import EVM.Fetch qualified+import EVM.Format (hexText) import EVM.Stepper qualified import EVM.Solvers (withSolvers, Solver(Z3)) import EVM.Transaction import EVM.TTY qualified as TTY-import EVM.Types+import EVM.Types hiding (Block, Case)  import Control.Arrow ((***), (&&&)) import Optics.Core@@ -53,15 +53,15 @@   } deriving Show  data Case = Case-  { vmOpts      :: EVM.VMOpts-  , checkContracts  :: Map Addr (EVM.Contract, Storage)-  , testExpectation :: Map Addr (EVM.Contract, Storage)+  { vmOpts      :: VMOpts+  , checkContracts  :: Map Addr (Contract, Storage)+  , testExpectation :: Map Addr (Contract, Storage)   } deriving Show  data BlockchainCase = BlockchainCase   { blocks  :: [Block]-  , pre     :: Map Addr (EVM.Contract, Storage)-  , post    :: Map Addr (EVM.Contract, Storage)+  , pre     :: Map Addr (Contract, Storage)+  , post    :: Map Addr (Contract, Storage)   , network :: String   } deriving Show @@ -157,10 +157,10 @@   . (fmap fst &&& fmap snd)   . (fmap (preview _Left &&& preview _Right)) -checkStateFail :: Bool -> Case -> EVM.VM -> (Bool, Bool, Bool, Bool) -> IO String+checkStateFail :: Bool -> Case -> VM -> (Bool, Bool, Bool, Bool) -> IO String checkStateFail diff x vm (okMoney, okNonce, okData, okCode) = do   let-    printContracts :: Map Addr (EVM.Contract, Storage) -> IO ()+    printContracts :: Map Addr (Contract, Storage) -> IO ()     printContracts cs = putStrLn $ Map.foldrWithKey (\k (c, s) acc ->       acc ++ show k ++ " : "                    ++ (show . toInteger  $ (view #nonce c)) ++ " "@@ -190,7 +190,7 @@     printContracts actual   pure (unwords reason) -checkExpectation :: Bool -> Case -> EVM.VM -> IO (Maybe String)+checkExpectation :: Bool -> Case -> VM -> IO (Maybe String) checkExpectation diff x vm = do   let expectation = x.testExpectation       (okState, b2, b3, b4, b5) = checkExpectedContracts vm expectation@@ -200,24 +200,24 @@     Just <$> checkStateFail diff x vm (b2, b3, b4, b5)  -- quotient account state by nullness-(~=) :: Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage) -> Bool+(~=) :: Map Addr (Contract, Storage) -> Map Addr (Contract, Storage) -> Bool (~=) cs1 cs2 =-    let nullAccount = EVM.initialContract (EVM.RuntimeCode (EVM.ConcreteRuntimeCode ""))+    let nullAccount = EVM.initialContract (RuntimeCode (ConcreteRuntimeCode ""))         padNewAccounts cs ks = Map.union cs $ Map.fromList [(k, (nullAccount, mempty)) | k <- ks]         padded_cs1 = padNewAccounts cs1 (Map.keys cs2)         padded_cs2 = padNewAccounts cs2 (Map.keys cs1)     in and $ zipWith (===) (Map.elems padded_cs1) (Map.elems padded_cs2) -(===) :: (EVM.Contract, Storage) -> (EVM.Contract, Storage) -> Bool+(===) :: (Contract, Storage) -> (Contract, Storage) -> Bool (c1, s1) === (c2, s2) =   codeEqual && storageEqual && (c1 ^. #balance == c2 ^. #balance) && (c1 ^. #nonce ==  c2 ^. #nonce)   where     storageEqual = s1 == s2     codeEqual = case (c1 ^. #contractcode, c2 ^. #contractcode) of-      (EVM.RuntimeCode a', EVM.RuntimeCode b') -> a' == b'+      (RuntimeCode a', RuntimeCode b') -> a' == b'       _ -> error "unexpected code" -checkExpectedContracts :: EVM.VM -> Map Addr (EVM.Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool)+checkExpectedContracts :: VM -> Map Addr (Contract, Storage) -> (Bool, Bool, Bool, Bool, Bool) checkExpectedContracts vm expected =   let cs = zipWithStorages $ vm ^. #env % #contracts -- . to (fmap (clearZeroStorage.clearOrigStorage))       expectedCs = clearStorage <$> expected@@ -237,23 +237,23 @@       SStore {} -> mempty -- error "SStore, should this be handled?"       GVar _ -> error "unexpected global variable" -clearStorage :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearStorage :: (Contract, Storage) -> (Contract, Storage) clearStorage (c, _) = (c, mempty) -clearBalance :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearBalance :: (Contract, Storage) -> (Contract, Storage) clearBalance (c, s) = (set #balance 0 c, s) -clearNonce :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)+clearNonce :: (Contract, Storage) -> (Contract, Storage) clearNonce (c, s) = (set #nonce 0 c, s) -clearCode :: (EVM.Contract, Storage) -> (EVM.Contract, Storage)-clearCode (c, s) = (set #contractcode (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) c, s)+clearCode :: (Contract, Storage) -> (Contract, Storage)+clearCode (c, s) = (set #contractcode (RuntimeCode (ConcreteRuntimeCode "")) c, s) -newtype ContractWithStorage = ContractWithStorage (EVM.Contract, Storage)+newtype ContractWithStorage = ContractWithStorage (Contract, Storage)  instance FromJSON ContractWithStorage where   parseJSON (JSON.Object v) = do-    code <- (EVM.RuntimeCode . EVM.ConcreteRuntimeCode <$> (hexText <$> v .: "code"))+    code <- (RuntimeCode . ConcreteRuntimeCode <$> (hexText <$> v .: "code"))     storage' <- v .: "storage"     balance' <- v .: "balance"     nonce'   <- v .: "nonce"@@ -288,7 +288,7 @@   parseJSON invalid =     JSON.typeMismatch "Block" invalid -parseContracts :: Which -> JSON.Object -> JSON.Parser (Map Addr (EVM.Contract, Storage))+parseContracts :: Which -> JSON.Object -> JSON.Parser (Map Addr (Contract, Storage)) parseContracts w v =   (Map.map unwrap) <$> (v .: which >>= parseJSON)   where which = case w of@@ -339,7 +339,7 @@     (_, _)   -> Left TooManyBlocks  fromBlockchainCase' :: Block -> Transaction-                       -> Map Addr (EVM.Contract, Storage) -> Map Addr (EVM.Contract, Storage)+                       -> Map Addr (Contract, Storage) -> Map Addr (Contract, Storage)                        -> Either BlockchainError Case fromBlockchainCase' block tx preState postState =   let isCreate = isNothing tx.toAddr in@@ -347,30 +347,30 @@       (Nothing, _) -> Left SignatureUnverified       (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)       (Just origin, Just checkState) -> Right $ Case-        (EVM.VMOpts-         { contract       = EVM.initialContract theCode-         , calldata       = (cd, [])-         , value          = Lit tx.value-         , address        = toAddr-         , caller         = litAddr origin+        (VMOpts+         { contract      = EVM.initialContract theCode+         , calldata      = (cd, [])+         , value         = Lit tx.value+         , address       = toAddr+         , caller        = litAddr origin          , initialStorage = EmptyStore-         , origin         = origin-         , gas            = tx.gasLimit  - fromIntegral (txGasCost feeSchedule tx)-         , baseFee        = block.baseFee-         , priorityFee    = priorityFee tx block.baseFee-         , gaslimit       = tx.gasLimit-         , number         = block.number-         , timestamp      = Lit block.timestamp-         , coinbase       = block.coinbase-         , prevRandao     = block.difficulty-         , maxCodeSize    = 24576-         , blockGaslimit  = block.gasLimit-         , gasprice       = effectiveGasPrice-         , schedule       = feeSchedule-         , chainId        = 1-         , create         = isCreate-         , txAccessList   = txAccessMap tx-         , allowFFI       = False+         , origin        = origin+         , gas           = tx.gasLimit  - fromIntegral (txGasCost feeSchedule tx)+         , baseFee       = block.baseFee+         , priorityFee   = priorityFee tx block.baseFee+         , gaslimit      = tx.gasLimit+         , number        = block.number+         , timestamp     = Lit block.timestamp+         , coinbase      = block.coinbase+         , prevRandao    = block.difficulty+         , maxCodeSize   = 24576+         , blockGaslimit = block.gasLimit+         , gasprice      = effectiveGasPrice+         , schedule      = feeSchedule+         , chainId       = 1+         , create        = isCreate+         , txAccessList  = txAccessMap tx+         , allowFFI      = False          })         checkState         postState@@ -380,8 +380,8 @@             feeSchedule = EVM.FeeSchedule.berlin             toCode = Map.lookup toAddr preState             theCode = if isCreate-                      then EVM.InitCode tx.txdata mempty-                      else maybe (EVM.RuntimeCode (EVM.ConcreteRuntimeCode "")) (view #contractcode . fst) toCode+                      then InitCode tx.txdata mempty+                      else maybe (RuntimeCode (ConcreteRuntimeCode "")) (view #contractcode . fst) toCode             effectiveGasPrice = effectiveprice tx block.baseFee             cd = if isCreate                  then mempty@@ -408,7 +408,7 @@      EIP1559Transaction -> fromJust tx.maxFeePerGas      _ -> fromJust tx.gasPrice -validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe ()+validateTx :: Transaction -> Block -> Map Addr (Contract, Storage) -> Maybe () validateTx tx block cs = do   let cs' = Map.map fst cs   origin        <- sender tx@@ -420,7 +420,7 @@   then Just ()   else Nothing -checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage))+checkTx :: Transaction -> Block -> Map Addr (Contract, Storage) -> Maybe (Map Addr (Contract, Storage)) checkTx tx block prestate = do   origin <- sender tx   validateTx tx block prestate@@ -429,18 +429,18 @@       toAddr      = fromMaybe (EVM.createAddress origin senderNonce) tx.toAddr       prevCode    = view (accountAt toAddr % #contractcode) (Map.map fst prestate)       prevNonce   = view (accountAt toAddr % #nonce) (Map.map fst prestate)-  if isCreate && ((case prevCode of {EVM.RuntimeCode (EVM.ConcreteRuntimeCode b) -> not (BS.null b); _ -> True}) || (prevNonce /= 0))+  if isCreate && ((case prevCode of {RuntimeCode (ConcreteRuntimeCode b) -> not (BS.null b); _ -> True}) || (prevNonce /= 0))   then mzero   else     return prestate -vmForCase :: Case -> EVM.VM+vmForCase :: Case -> VM vmForCase x =   let     a = x.checkContracts     cs = Map.map fst a     st = Map.mapKeys num $ Map.map snd a-    vm = EVM.makeVm x.vmOpts+    vm = makeVm x.vmOpts       & set (#env % #contracts) cs       & set (#env % #storage) (ConcreteStore st)       & set (#env % #origStorage) st

@@ -28,7 +28,7 @@ import Data.Maybe import Data.List qualified (length) import Test.Tasty-import Test.Tasty.QuickCheck hiding (Failure)+import Test.Tasty.QuickCheck hiding (Failure, Success) import Test.QuickCheck.Instances.Text() import Test.QuickCheck.Instances.Natural() import Test.QuickCheck.Instances.ByteString()@@ -55,6 +55,7 @@ import EVM.Op hiding (getOp) import EVM.Exec import EVM.Types+import EVM.Format (bsToHex) import EVM.Traversals import EVM.Concrete (createAddress) import qualified EVM.FeeSchedule as FeeSchedule@@ -69,6 +70,21 @@ import EVM.Sign (deriveAddr) import GHC.IO.Exception (ExitCode(ExitSuccess)) +data VMTrace =+  VMTrace+  { tracePc      :: Int+  , traceOp      :: Int+  , traceStack   :: [W256]+  , traceMemSize :: Data.Word.Word64+  , traceDepth   :: Int+  , traceGas     :: Data.Word.Word64+  , traceError   :: Maybe String+  } deriving (Generic, Show)++instance JSON.ToJSON VMTrace where+  toEncoding = JSON.genericToEncoding JSON.defaultOptions+instance JSON.FromJSON VMTrace+ data VMTraceResult =   VMTraceResult   { out  :: ByteStringS@@ -287,7 +303,7 @@     toAddress :: Addr     toAddress = 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192 -getHEVMRet :: OpContract -> ByteString -> Int -> IO (Either (EVM.Error, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult))+getHEVMRet :: OpContract -> ByteString -> Int -> IO (Either (EvmError, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult)) getHEVMRet contr txData gaslimitExec = do   let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec   hevmRun <- runCodeWithTrace Nothing evmEnv contrAlloc txn (fromAddress, toAddress)@@ -409,13 +425,13 @@  -- | Takes a runtime code and calls it with the provided calldata --   Uses evmtool's alloc and transaction to set up the VM correctly-runCodeWithTrace :: Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> IO (Either (EVM.Error, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult)))+runCodeWithTrace :: Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> IO (Either (EvmError, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult))) runCodeWithTrace rpcinfo evmEnv alloc txn (fromAddr, toAddress) = withSolvers Z3 0 Nothing $ \solvers -> do   let origVM = vmForRuntimeCode code' calldata' evmEnv alloc txn (fromAddr, toAddress)       calldata' = ConcreteBuf txn.txdata       code' = alloc.code       buildExpr :: SolverGroup -> VM -> IO (Expr End)-      buildExpr s vm = interpret (Fetch.oracle s Nothing) Nothing Nothing vm runExpr+      buildExpr s vm = interpret (Fetch.oracle s Nothing) Nothing 1 Naive vm runExpr    expr <- buildExpr solvers $ symbolify origVM   (res, (vm, trace)) <- runStateT (interpretWithTrace (Fetch.oracle solvers rpcinfo) Stepper.execFully) (origVM, [])@@ -480,8 +496,6 @@              }   where     readoutError :: Maybe VMResult -> Maybe String-    readoutError Nothing = Nothing-    readoutError (Just (VMSuccess _)) = Nothing     readoutError (Just (VMFailure e)) = case e of       -- NOTE: error text made to closely match go-ethereum's errors.go file       OutOfGas {}             -> Just "out of gas"@@ -489,19 +503,20 @@       CallDepthLimitReached   -> Just "max call depth exceeded"       BalanceTooLow {}        -> Just "insufficient balance for transfer"       -- TODO "contract address collision" not handled-      EVM.Revert {}           -> Just "execution reverted"+      Revert {}           -> Just "execution reverted"       -- TODO "max initcode size exceeded" not handled       MaxCodeSizeExceeded {}  -> Just "max code size exceeded"-      EVM.BadJumpDestination  -> Just "invalid jump destination"+      BadJumpDestination  -> Just "invalid jump destination"       StateChangeWhileStatic  -> Just "write protection"       ReturnDataOutOfBounds   -> Just "return data out of bounds"-      EVM.IllegalOverflow     -> Just "gas uint64 overflow"+      IllegalOverflow     -> Just "gas uint64 overflow"       UnrecognizedOpcode op   -> Just $ "invalid opcode: " <> show op-      EVM.NonceOverflow       -> Just "nonce uint64 overflow"-      EVM.StackUnderrun       -> Just "stack underflow"-      EVM.StackLimitExceeded  -> Just "stack limit reached"-      EVM.InvalidMemoryAccess -> Just "write protection"+      NonceOverflow       -> Just "nonce uint64 overflow"+      StackUnderrun       -> Just "stack underflow"+      StackLimitExceeded  -> Just "stack limit reached"+      InvalidMemoryAccess -> Just "write protection"       err                     -> Just $ "HEVM error: " <> show err+    readoutError _ = Nothing  vmres :: VM -> VMTraceResult vmres vm =@@ -510,7 +525,7 @@     res = case vm.result of       Just (VMSuccess (ConcreteBuf b)) -> (ByteStringS b)       Just (VMSuccess x) -> error $ "unhandled: " <> (show x)-      Just (VMFailure (EVM.Revert (ConcreteBuf b))) -> (ByteStringS b)+      Just (VMFailure (Revert (ConcreteBuf b))) -> (ByteStringS b)       Just (VMFailure _) -> ByteStringS mempty       _ -> ByteStringS mempty   in VMTraceResult@@ -535,7 +550,6 @@       State.modify (\(a, b) -> (a, b ++ [vmtrace vm0]))       zoom _1 (State.state (runState exec1))       runWithTrace-    Just (VMSuccess _) -> pure vm0     Just (VMFailure _) -> do       -- Update error text for last trace element       (a, b) <- State.get@@ -543,6 +557,7 @@           updatedTraces = take ((Data.List.length b)-1) b ++ [updatedElem]       State.put (a, updatedTraces)       pure vm0+    Just _ -> pure vm0  interpretWithTrace   :: Fetch.Fetcher@@ -565,9 +580,12 @@           execWithTrace >>= interpretWithTrace fetcher . k         Stepper.Run ->           runWithTrace >>= interpretWithTrace fetcher . k-        Stepper.Wait q ->-          do m <- liftIO (fetcher q)-             zoom _1 (State.state (runState m)) >> interpretWithTrace fetcher (k ())+        Stepper.Wait q -> case q of+          PleaseAskSMT (Lit x) _ continue ->+            interpretWithTrace fetcher (Stepper.evm (continue (Case (x > 0))) >>= k)+          _ -> do+            m <- liftIO (fetcher q)+            zoom _1 (State.state (runState m)) >> interpretWithTrace fetcher (k ())         Stepper.Ask _ ->           error "cannot make choice in this interpreter"         Stepper.IOAct q ->@@ -823,7 +841,7 @@               concretizedExpr = concretize expr (ConcreteBuf txData)               simplConcExpr = Expr.simplify concretizedExpr               getReturnVal :: Expr End -> Maybe ByteString-              getReturnVal (Return _ (ConcreteBuf bs) _) = Just bs+              getReturnVal (Success _ (ConcreteBuf bs) _) = Just bs               getReturnVal _ = Nothing               simplConcrExprRetval = getReturnVal simplConcExpr             traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace)@@ -865,4 +883,3 @@         System.Directory.removeFile "env.json"         deleteTraceOutputFiles evmtoolResult     ]-

@@ -2,15 +2,16 @@  module EVM.Test.Utils where +import Data.String.Here import Data.Text-import qualified Data.Text as T-import qualified Data.Text.IO as T+import GHC.IO.Handle (hClose) import qualified Paths_hevm as Paths-import Data.String.Here import System.Directory import System.IO.Temp-import GHC.IO.Handle (hClose)-import System.Process (readProcess)+import System.Process+import System.Exit+import qualified Data.Text as T+import qualified Data.Text.IO as T  import EVM.Solidity import EVM.Solvers@@ -19,42 +20,32 @@ import EVM.Fetch (RpcInfo) import qualified EVM.TTY as TTY -runDappTestCustom :: FilePath -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO Bool-runDappTestCustom testFile match maxIter ffiAllowed rpcinfo = do-  root <- Paths.getDataDir-  (json, _) <- compileWithDSTest testFile-  --T.writeFile "output.json" json-  withCurrentDirectory root $ do-    withSystemTempFile "output.json" $ \file handle -> do-      hClose handle-      T.writeFile file json-      withSolvers Z3 1 Nothing $ \solvers -> do-        opts <- testOpts solvers root json match maxIter ffiAllowed rpcinfo-        dappTest opts file Nothing+runSolidityTestCustom :: FilePath -> Text -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> IO Bool+runSolidityTestCustom testFile match maxIter ffiAllowed rpcinfo projectType = do+  withSystemTempDirectory "dapp-test" $ \root -> do+    compile projectType root testFile >>= \case+      Left e -> error e+      Right bo@(BuildOutput contracts _) -> do+        withSolvers Z3 1 Nothing $ \solvers -> do+          opts <- testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo+          unitTest opts contracts Nothing -runDappTest :: FilePath -> Text -> IO Bool-runDappTest testFile match = runDappTestCustom testFile match Nothing True Nothing+runSolidityTest :: FilePath -> Text -> IO Bool+runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing True Nothing Foundry -debugDappTest :: FilePath -> RpcInfo -> IO ()-debugDappTest testFile rpcinfo = do-  root <- Paths.getDataDir-  (json, _) <- compileWithDSTest testFile-  --TIO.writeFile "output.json" json-  withCurrentDirectory root $ do-    withSystemTempFile "output.json" $ \file handle -> do-      hClose handle-      T.writeFile file json-      withSolvers Z3 1 Nothing $ \solvers -> do-        opts <- testOpts solvers root json ".*" Nothing True rpcinfo-        TTY.main opts root file+debugSolidityTest :: FilePath -> RpcInfo -> IO ()+debugSolidityTest testFile rpcinfo = do+  withSystemTempDirectory "dapp-test" $ \root -> do+    compile DappTools root testFile >>= \case+      Left e -> error e+      Right bo -> do+        withSolvers Z3 1 Nothing $ \solvers -> do+          opts <- testOpts solvers root (Just bo) ".*" Nothing True rpcinfo+          TTY.main opts root (Just bo) -testOpts :: SolverGroup -> FilePath -> Text -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO UnitTestOptions-testOpts solvers root solcJson match maxIter allowFFI rpcinfo = do-  srcInfo <- case readJSON solcJson of-               Nothing -> error "Could not read solc json"-               Just (contractMap, asts, sources) -> do-                 sourceCache <- makeSourceCache sources asts-                 pure $ dappInfo root contractMap sourceCache+testOpts :: SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO UnitTestOptions+testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do+  let srcInfo = maybe emptyDapp (dappInfo root) buildOutput    params <- getParametersFromEnvironmentVariables Nothing @@ -62,7 +53,7 @@     { solvers = solvers     , rpcInfo = rpcinfo     , maxIter = maxIter-    , askSmtIters = Nothing+    , askSmtIters = 1     , smtDebug = False     , smtTimeout = Nothing     , solver = Nothing@@ -78,7 +69,35 @@     , ffiAllowed = allowFFI     } -compileWithDSTest :: FilePath -> IO (Text, Text)+compile :: ProjectType -> FilePath -> FilePath -> IO (Either String BuildOutput)+compile DappTools root src = do+  json <- compileWithDSTest src+  createDirectory (root <> "/out")+  T.writeFile (root <> "/out/dapp.sol.json") json+  readBuildOutput root DappTools+compile Foundry root src = do+  createDirectory (root <> "/src")+  writeFile (root <> "/src/unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src+  initLib (root <> "/lib/ds-test") "test/contracts/lib/test.sol" "test.sol"+  initLib (root <> "/lib/tokens") "test/contracts/lib/erc20.sol" "erc20.sol"+  r@(res,_,_) <- readProcessWithExitCode "forge" ["build", "--root", root] ""+  case res of+    ExitFailure _ -> pure . Left $ "compilation failed: " <> show r+    ExitSuccess -> readBuildOutput root Foundry+  where+    initLib :: FilePath -> FilePath -> FilePath -> IO ()+    initLib tld srcFile dstFile = do+      createDirectoryIfMissing True (tld <> "/src")+      writeFile (tld <> "/src/" <> dstFile) =<< readFile =<< Paths.getDataFileName srcFile+      _ <- readProcessWithExitCode "git" ["init", tld] ""+      callProcess "git" ["config", "--file", tld <> "/.git/config", "user.name", "'hevm'"]+      callProcess "git" ["config", "--file", tld <> "/.git/config", "user.email", "'hevm@hevm.dev'"]+      callProcess "git" ["--git-dir", tld <> "/.git", "--work-tree", tld, "add", tld]+      _ <- readProcessWithExitCode "git" ["--git-dir", tld <> "/.git", "--work-tree", tld, "--no-gpg-sign", "commit", "-m"] ""+      pure ()++-- We don't want to depend on dapptools here, so we cheat and just call solc with the same options that dapp itself uses+compileWithDSTest :: FilePath -> IO Text compileWithDSTest src =   withSystemTempFile "input.json" $ \file handle -> do     hClose handle@@ -94,10 +113,10 @@           "ds-test/test.sol": {             "content": ${dsTest}           },-          "lib/erc20.sol": {+          "tokens/erc20.sol": {             "content": ${erc20}           },-          "test.sol": {+          "unit-tests.sol": {             "content": ${testFile}           }         },@@ -133,4 +152,5 @@         "solc"         ["--allow-paths", file, "--standard-json", file]         ""-    return (x, T.pack testFilePath)+    return x+

@@ -8,8 +8,13 @@     function sign(uint256,bytes32) external returns (uint8,bytes32,bytes32);     function addr(uint256) external returns (address);     function ffi(string[] calldata) external returns (bytes memory);+    function prank(address) external; } +contract Payable {+    function hi() public payable {}+}+ contract TestFailCheatCodes is DSTest {     Hevm hevm = Hevm(HEVM_ADDRESS); @@ -20,5 +25,15 @@          // should revert if --ffi hasn't been passed to hevm...         hevm.ffi(inputs);+    }++    function test_prank_underflow() public {+        address from = address(0x1312);+        uint amt = 10;++        Payable target = new Payable();++        hevm.prank(from);+        target.hi{value : amt}();     } }

@@ -1,5 +1,5 @@ import "ds-test/test.sol";-import "lib/erc20.sol";+import "tokens/erc20.sol";  contract SolidityTest is DSTest {     ERC20 token;

@@ -1,5 +1,5 @@ import "ds-test/test.sol";-import "lib/erc20.sol";+import "tokens/erc20.sol";  contract ConstructorArg {     address immutable public a;

@@ -1,5 +1,5 @@ import "ds-test/test.sol";-import "lib/erc20.sol";+import "tokens/erc20.sol";  contract InvariantTest is DSTest {     ERC20 token;

@@ -1,5 +1,5 @@ import {DSTest} from "ds-test/test.sol";-import {ERC20} from "lib/erc20.sol";+import {ERC20} from "tokens/erc20.sol";  contract C is DSTest {     // BAL: https://etherscan.io/address/0xba100000625a3754423978a60c9317c58a424e3D#code

@@ -10,7 +10,7 @@ import Data.Text (Text) import Data.Vector qualified as V -import EVM+import EVM (makeVm) import EVM.ABI import EVM.Fetch import EVM.SMT@@ -18,6 +18,7 @@ import EVM.Stepper qualified as Stepper import EVM.SymExec import EVM.Test.Utils+import EVM.Solidity (ProjectType(..)) import EVM.Types hiding (BlockNumber)  main :: IO ()@@ -30,7 +31,7 @@         let block = BlockNumber 15537392         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case                       Nothing -> error "Could not fetch block"-                      Just EVM.Block{..} -> return ( coinbase+                      Just Block{..} -> return ( coinbase                                                    , number                                                    , baseFee                                                    , prevRandao@@ -44,7 +45,7 @@         let block = BlockNumber 16184420         (cb, numb, basefee, prevRan) <- fetchBlockFrom block testRpc >>= \case                       Nothing -> error "Could not fetch block"-                      Just EVM.Block{..} -> return ( coinbase+                      Just Block{..} -> return ( coinbase                                                    , number                                                    , baseFee                                                    , prevRandao@@ -59,7 +60,7 @@     -- execute against remote state from a ds-test harness     [ testCase "dapp-test" $ do         let testFile = "test/contracts/pass/rpc.sol"-        runDappTestCustom testFile ".*" Nothing False testRpcInfo >>= assertEqual "test result" True+        runSolidityTestCustom testFile ".*" Nothing False testRpcInfo Foundry >>= assertEqual "test result" True      -- concretely exec "transfer" on WETH9 using remote rpc     -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code@@ -89,7 +90,7 @@         let           blockNum = 16198552           calldata' = symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata")-          postc _ (EVM.Types.Revert _ _) = PBool False+          postc _ (Failure _ (Revert _)) = PBool False           postc _ _ = PBool True         vm <- weth9VM blockNum calldata'         (_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->@@ -99,7 +100,7 @@   ]  -- call into WETH9 from 0xf04a... (a large holder)-weth9VM :: W256 -> (Expr Buf, [Prop]) -> IO (EVM.VM)+weth9VM :: W256 -> (Expr Buf, [Prop]) -> IO VM weth9VM blockNum calldata' = do   let     caller' = Lit 0xf04a5cc80b1e94c69b48f5ee68a08cd2f09a7c3e@@ -107,7 +108,7 @@     callvalue' = Lit 0   vmFromRpc blockNum calldata' callvalue' caller' weth9 -vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EWord -> Addr -> IO (EVM.VM)+vmFromRpc :: W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EWord -> Addr -> IO VM vmFromRpc blockNum calldata' callvalue' caller' address' = do   ctrct <- fetchContractFrom (BlockNumber blockNum) testRpc address' >>= \case         Nothing -> error $ "contract not found: " <> show address'@@ -117,30 +118,30 @@     Nothing -> error "could not fetch block"     Just b -> pure b -  pure $ EVM.makeVm $ EVM.VMOpts-    { EVM.contract       = ctrct-    , EVM.calldata       = calldata'-    , EVM.value          = callvalue'-    , EVM.address        = address'-    , EVM.caller         = caller'-    , EVM.origin         = 0xacab-    , EVM.gas            = 0xffffffffffffffff-    , EVM.gaslimit       = 0xffffffffffffffff-    , EVM.baseFee        = blk.baseFee-    , EVM.priorityFee    = 0-    , EVM.coinbase       = blk.coinbase-    , EVM.number         = blk.number-    , EVM.timestamp      = blk.timestamp-    , EVM.blockGaslimit  = blk.gaslimit-    , EVM.gasprice       = 0-    , EVM.maxCodeSize    = blk.maxCodeSize-    , EVM.prevRandao     = blk.prevRandao-    , EVM.schedule       = blk.schedule-    , EVM.chainId        = 1-    , EVM.create         = False-    , EVM.initialStorage = EmptyStore-    , EVM.txAccessList   = mempty-    , EVM.allowFFI       = False+  pure $ makeVm $ VMOpts+    { contract      = ctrct+    , calldata      = calldata'+    , value         = callvalue'+    , address       = address'+    , caller        = caller'+    , origin        = 0xacab+    , gas           = 0xffffffffffffffff+    , gaslimit      = 0xffffffffffffffff+    , baseFee       = blk.baseFee+    , priorityFee   = 0+    , coinbase      = blk.coinbase+    , number        = blk.number+    , timestamp     = blk.timestamp+    , blockGaslimit = blk.gaslimit+    , gasprice      = 0+    , maxCodeSize   = blk.maxCodeSize+    , prevRandao    = blk.prevRandao+    , schedule      = blk.schedule+    , chainId       = 1+    , create        = False+    , initialStorage = EmptyStore+    , txAccessList  = mempty+    , allowFFI      = False     }  testRpc :: Text

@@ -25,12 +25,12 @@ import Data.List qualified (elemIndex) import Data.DoubleWord import Test.Tasty-import Test.Tasty.QuickCheck hiding (Failure)+import Test.Tasty.QuickCheck hiding (Failure, Success) import Test.QuickCheck.Instances.Text() import Test.QuickCheck.Instances.Natural() import Test.QuickCheck.Instances.ByteString() import Test.Tasty.HUnit-import Test.Tasty.Runners hiding (Failure)+import Test.Tasty.Runners hiding (Failure, Success) import Test.Tasty.ExpectedFailure import EVM.Test.Tracing qualified as Tracing @@ -46,7 +46,7 @@ import Data.Binary.Put (runPut) import Data.Binary.Get (runGetOrFail) -import EVM+import EVM hiding (choose) import EVM.SymExec import EVM.ABI import EVM.Exec@@ -55,11 +55,14 @@ import EVM.RLP import EVM.Solidity import EVM.Types+import EVM.Format (hexText) import EVM.Traversals import EVM.Concrete (createAddress) import EVM.SMT hiding (one) import EVM.Solvers import qualified EVM.Expr as Expr+import qualified EVM.Stepper as Stepper+import qualified EVM.Fetch as Fetch import qualified Data.Text as T import Data.List (isSubsequenceOf) import EVM.Test.Utils@@ -104,12 +107,12 @@             vm1 = execState (EVM.accessStorage 0 (Lit 0) (pure . pure ())) vm             -- it should fetch the contract first             vm2 = case vm1.result of-                    Just (VMFailure (Query (PleaseFetchContract _addr continue))) ->+                    Just (HandleEffect (Query (PleaseFetchContract _addr continue))) ->                       execState (continue dummyContract) vm1                     _ -> error "unexpected result"             -- then it should fetch the slow             vm3 = case vm2.result of-                    Just (VMFailure (Query (PleaseFetchSlot _addr _slot continue))) ->+                    Just (HandleEffect (Query (PleaseFetchSlot _addr _slot continue))) ->                       execState (continue 1337) vm2                     _ -> error "unexpected result"             -- perform the same access as for vm1@@ -353,7 +356,7 @@           Right ("", _, x') -> x' == x           _ -> False     ]-  , testGroup "Solidity expressions"+  , testGroup "Solidity-Expressions"     [ testCase "Trivial" $         SolidityCall "x = 3;" []           ===> AbiUInt 256 3@@ -477,8 +480,7 @@                 |]          (json, path') <- solidity' srccode-        let (solc', _, _) = fromJust $ readJSON json-            initCode :: ByteString+        let (Contracts solc', _, _) = fromJust $ readStdJSON json             initCode = (solc' ^?! ix (path' <> ":A")).creationCode         -- add constructor arguments         assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode)@@ -565,7 +567,7 @@                }              }              |]-         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] debugVeriOpts+         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] defaultVeriOpts          putStrLn "expected counterexample found"       ,      testCase "enum-conversion-fail" $ do@@ -620,8 +622,8 @@         -- assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1         putStrLn "expected counterexample found"       ,-      -- TODO the system currently does not allow for symbolic array size allocation-      expectFail $ testCase "alloc-too-much" $ do+      -- Note: we catch the assertion here, even though we are only able to explore partially+      testCase "alloc-too-much" $ do         Just c <- solcRuntime "MyContract"             [i|             contract MyContract {@@ -630,7 +632,8 @@               }              }             |]-        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s ->+          checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "expected counterexample found"       ,       -- TODO the system currently does not allow for symbolic JUMP@@ -654,50 +657,153 @@         putStrLn "expected counterexample found"  ] -  , testGroup "Dapp Tests"+  , testGroup "Dapp-Tests"     [ testCase "Trivial-Pass" $ do         let testFile = "test/contracts/pass/trivial.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True+    , testCase "DappTools" $ do+        -- quick smokecheck to make sure that we can parse dapptools style build outputs+        let cases =+              [ ("test/contracts/pass/trivial.sol", ".*", True)+              , ("test/contracts/pass/invariants.sol", "invariantTestThisBal", True)+              , ("test/contracts/pass/dsProvePass.sol", "proveEasy", True)+              , ("test/contracts/fail/trivial.sol", ".*", False)+              , ("test/contracts/fail/invariantFail.sol", "invariantCount", False)+              , ("test/contracts/fail/dsProveFail.sol", "prove_add", False)+              ]+        results <- forM cases $ \(testFile, match, expected) -> do+          actual <- runSolidityTestCustom testFile match Nothing False Nothing DappTools+          pure (actual == expected)+        assertBool "test result" (and results)     , testCase "Trivial-Fail" $ do         let testFile = "test/contracts/fail/trivial.sol"-        runDappTest testFile "testFalse" >>= assertEqual "test result" False+        runSolidityTest testFile "testFalse" >>= assertEqual "test result" False     , testCase "Abstract" $ do         let testFile = "test/contracts/pass/abstract.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     , testCase "Constantinople" $ do         let testFile = "test/contracts/pass/constantinople.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     , testCase "Prove-Tests-Pass" $ do         let testFile = "test/contracts/pass/dsProvePass.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     , testCase "Prove-Tests-Fail" $ do         let testFile = "test/contracts/fail/dsProveFail.sol"-        runDappTest testFile "prove_trivial" >>= assertEqual "test result" False-        runDappTest testFile "prove_add" >>= assertEqual "test result" False-        --runDappTest testFile "prove_smtTimeout" >>= assertEqual "test result" False-        runDappTest testFile "prove_multi" >>= assertEqual "test result" False-        runDappTest testFile "prove_mul" >>= assertEqual "test result" False+        runSolidityTest testFile "prove_trivial" >>= assertEqual "test result" False+        runSolidityTest testFile "prove_add" >>= assertEqual "test result" False+        --runSolidityTest testFile "prove_smtTimeout" >>= assertEqual "test result" False+        runSolidityTest testFile "prove_multi" >>= assertEqual "test result" False+        runSolidityTest testFile "prove_mul" >>= assertEqual "test result" False         -- TODO: implement overflow checking optimizations and enable, currently this runs forever-        --runDappTest testFile "prove_distributivity" >>= assertEqual "test result" False-        runDappTest testFile "prove_transfer" >>= assertEqual "test result" False+        --runSolidityTest testFile "prove_distributivity" >>= assertEqual "test result" False+        runSolidityTest testFile "prove_transfer" >>= assertEqual "test result" False     , testCase "Loop-Tests" $ do         let testFile = "test/contracts/pass/loops.sol"-        runDappTestCustom testFile "prove_loop" (Just 10) False Nothing >>= assertEqual "test result" True-        runDappTestCustom testFile "prove_loop" (Just 100) False Nothing >>= assertEqual "test result" False+        runSolidityTestCustom testFile "prove_loop" (Just 10) False Nothing Foundry >>= assertEqual "test result" True+        runSolidityTestCustom testFile "prove_loop" (Just 100) False Nothing Foundry >>= assertEqual "test result" False     , testCase "Invariant-Tests-Pass" $ do         let testFile = "test/contracts/pass/invariants.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     , testCase "Invariant-Tests-Fail" $ do         let testFile = "test/contracts/fail/invariantFail.sol"-        runDappTest testFile "invariantFirst" >>= assertEqual "test result" False-        runDappTest testFile "invariantCount" >>= assertEqual "test result" False+        runSolidityTest testFile "invariantFirst" >>= assertEqual "test result" False+        runSolidityTest testFile "invariantCount" >>= assertEqual "test result" False     , testCase "Cheat-Codes-Pass" $ do         let testFile = "test/contracts/pass/cheatCodes.sol"-        runDappTest testFile ".*" >>= assertEqual "test result" True+        runSolidityTest testFile ".*" >>= assertEqual "test result" True     , testCase "Cheat-Codes-Fail" $ do         let testFile = "test/contracts/fail/cheatCodes.sol"-        runDappTestCustom testFile "testBadFFI" Nothing False Nothing >>= assertEqual "test result" False+        runSolidityTestCustom testFile "testBadFFI" Nothing False Nothing Foundry >>= assertEqual "test result" False+        runSolidityTestCustom testFile "test_prank_underflow" Nothing False Nothing Foundry >>= assertEqual "test result" False     ]+  , testGroup "max-iterations"+    [ testCase "concrete-loops-reached" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun() external payable returns (uint) {+                uint count = 0;+                for (uint i = 0; i < 5; i++) count++;+                return count;+              }+            }+            |]+        let sig = Just $ Sig "fun()" []+            opts = defaultVeriOpts{ maxIter = Just 3 }+        (e, [Qed _]) <- withSolvers Z3 1 Nothing $+          \s -> checkAssert s defaultPanicCodes c sig [] opts+        assertBool "The expression is not partial" $ isPartial e+    , testCase "concrete-loops-not-reached" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun() external payable returns (uint) {+                uint count = 0;+                for (uint i = 0; i < 5; i++) count++;+                return count;+              }+            }+            |]++        let sig = Just $ Sig "fun()" []+            opts = defaultVeriOpts{ maxIter = Just 6 }+        (e, [Qed _]) <- withSolvers Z3 1 Nothing $+          \s -> checkAssert s defaultPanicCodes c sig [] opts+        assertBool "The expression is partial" $ not $ isPartial e+    , testCase "symbolic-loops-reached" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun(uint j) external payable returns (uint) {+                uint count = 0;+                for (uint i = 0; i < j; i++) count++;+                return count;+              }+            }+            |]+        (e, [Qed _]) <- withSolvers Z3 1 Nothing $+          \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] (defaultVeriOpts{ maxIter = Just 5 })+        assertBool "The expression is not partial" $ Expr.containsNode isPartial e+    , testCase "inconsistent-paths" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun(uint j) external payable returns (uint) {+                require(j <= 3);+                uint count = 0;+                for (uint i = 0; i < j; i++) count++;+                return count;+              }+            }+            |]+        let sig = Just $ Sig "fun(uint256)" [AbiUIntType 256]+            -- we dont' ask the solver about the loop condition until we're+            -- already in an inconsistent path (i == 5, j <= 3, i < j), so we+            -- will continue looping here until we hit max iterations+            opts = defaultVeriOpts{ maxIter = Just 10, askSmtIters = 5 }+        (e, [Qed _]) <- withSolvers Z3 1 Nothing $+          \s -> checkAssert s defaultPanicCodes c sig [] opts+        assertBool "The expression is not partial" $ Expr.containsNode isPartial e+    , testCase "symbolic-loops-not-reached" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun(uint j) external payable returns (uint) {+                require(j <= 3);+                uint count = 0;+                for (uint i = 0; i < j; i++) count++;+                return count;+              }+            }+            |]+        let sig = Just $ Sig "fun(uint256)" [AbiUIntType 256]+            -- askSmtIters is low enough here to avoid the inconsistent path+            -- conditions, so we never hit maxIters+            opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 1 }+        (e, [Qed _]) <- withSolvers Z3 1 Nothing $+          \s -> checkAssert s defaultPanicCodes c sig [] opts+        assertBool "The expression is partial" $ not (Expr.containsNode isPartial e)+    ]   , testGroup "Symbolic execution"       [      testCase "require-test" $ do@@ -774,17 +880,9 @@           }         }         |]-      let-        opts = VeriOpts-          { simp = False-          , debug = False-          , maxIter = Nothing-          , askSmtIters = Nothing-          , rpcInfo = Nothing-          }-        calldata' = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])+      let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])       (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->-        checkAssert s defaultPanicCodes c calldata' [] opts+        checkAssert s defaultPanicCodes c sig [] defaultVeriOpts       putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"      ,      -- TODO look at tests here for SAR: https://github.com/dapphub/dapptools/blob/01ef8ea418c3fe49089a44d56013d8fcc34a1ec2/src/dapp-tests/pass/constantinople.sol#L250@@ -1149,7 +1247,7 @@                              [x', y'] -> (x', y')                              _ -> error "expected 2 args"               in case leaf of-                   EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)+                   Success _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)                    _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"@@ -1175,7 +1273,7 @@                              [x', y'] -> (x', y')                              _ -> error "expected 2 args"               in case leaf of-                   EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)+                   Success _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)                    _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->           verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)@@ -1202,7 +1300,7 @@                   this = Expr.litAddr $ prestate.state.codeContract                   prex = Expr.readStorage' this (Lit 0) prestate.env.storage               in case leaf of-                EVM.Types.Return _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)+                Success _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)                 _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts AbstractStore (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"@@ -1258,7 +1356,7 @@                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     EVM.Types.Return _ _ poststore -> let+                     Success _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty@@ -1292,7 +1390,7 @@                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     EVM.Types.Return _ _ poststore -> let+                     Success _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty@@ -1314,7 +1412,7 @@               }              }             |]-          (_, [Cex (EVM.Types.Revert _ msg, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts+          (_, [Cex (Failure _ (Revert msg), _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts           assertEqual "incorrect revert msg" msg (ConcreteBuf $ panicMsg 0x01)         ,         testCase "simple-assert-2" $ do@@ -1998,15 +2096,14 @@               }           |]         withSolvers Z3 3 Nothing $ \s -> do-          let myVeriOpts = VeriOpts{ simp = True, debug = False, maxIter = Just 2, askSmtIters = Just 2, rpcInfo = Nothing}-          a <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing [])+          a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])           assertEqual "Must be different" (any isCex a) True           return ()       , testCase "eq-all-yul-optimization-tests" $ do-        let myVeriOpts = VeriOpts{ simp = True, debug = False, maxIter = Just 5, askSmtIters = Just 20, rpcInfo = Nothing }-            ignoredTests = [+        let opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 20, loopHeuristic = Naive }+            ignoredTests =                     -- unbounded loop ---                    "commonSubexpressionEliminator/branches_for.yul"+                    [ "commonSubexpressionEliminator/branches_for.yul"                     , "conditionalSimplifier/no_opt_if_break_is_not_last.yul"                     , "conditionalUnsimplifier/no_opt_if_break_is_not_last.yul"                     , "expressionSimplifier/inside_for.yul"@@ -2221,7 +2318,7 @@                 False -> recursiveList ax (a:b)           recursiveList [] b = pure b         files <- recursiveList fullpaths []-        let filesFiltered = filter (\file -> not $ any (\filt -> Data.List.isSubsequenceOf filt file) ignoredTests) files+        let filesFiltered = filter (\file -> not $ any (`isSubsequenceOf` file) ignoredTests) files          -- Takes one file which follows the Solidity Yul optimizer unit tests format,         -- extracts both the nonoptimized and the optimized versions, and checks equivalence.@@ -2250,7 +2347,7 @@             filteredBSym = symbolicMem [ replaceAll "" $ x *=~[re|^//|] | x <- onlyAfter [re|^// step:|] unfiltered, not $ x =~ [re|^$|] ]           start <- getCurrentTime           putStrLn $ "Checking file: " <> f-          when myVeriOpts.debug $ do+          when opts.debug $ do             putStrLn "-------------Original Below-----------------"             mapM_ putStrLn unfiltered             putStrLn "------------- Filtered A + Symb below-----------------"@@ -2262,7 +2359,7 @@           Just bPrgm <- yul "" $ T.pack $ unlines filteredBSym           procs <- getNumProcessors           withSolvers CVC5 (num procs) (Just 100) $ \s -> do-            res <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing [])+            res <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing [])             end <- getCurrentTime             case any isCex res of               False -> do@@ -2300,26 +2397,34 @@ -- | Takes a runtime code and calls it with the provided calldata  -- | Takes a creation code and some calldata, runs the creation code, and calls the resulting contract with the provided calldata-runSimpleVM :: ByteString -> ByteString -> Maybe ByteString-runSimpleVM x ins = case loadVM x of-                      Nothing -> Nothing-                      Just vm -> let calldata' = (ConcreteBuf ins)-                       in case runState (assign (#state % #calldata) calldata' >> exec) vm of-                            (VMSuccess (ConcreteBuf bs), _) -> Just bs-                            _ -> Nothing+runSimpleVM :: ByteString -> ByteString -> IO (Maybe ByteString)+runSimpleVM x ins = do+  loadVM x >>= \case+    Nothing -> pure Nothing+    Just vm -> do+     let calldata = (ConcreteBuf ins)+         vm' = set (#state % #calldata) calldata vm+     res <- Stepper.interpret (Fetch.zero 0 Nothing) vm' Stepper.execFully+     case res of+       (Right (ConcreteBuf bs)) -> pure $ Just bs+       s -> error $ show s  -- | Takes a creation code and returns a vm with the result of executing the creation code-loadVM :: ByteString -> Maybe VM-loadVM x =-    case runState exec (vmForEthrunCreation x) of-       (VMSuccess (ConcreteBuf targetCode), vm1) -> do-         let target = vm1.state.contract-             vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode targetCode))) vm1-         return $ snd $ flip runState vm2-                (do resetState-                    assign (#state % #gas) 0xffffffffffffffff -- kludge-                    loadContract target)-       _ -> Nothing+loadVM :: ByteString -> IO (Maybe VM)+loadVM x = do+  vm1 <- Stepper.interpret (Fetch.zero 0 Nothing) (vmForEthrunCreation x) Stepper.runFully+  case vm1.result of+     Just (VMSuccess (ConcreteBuf targetCode)) -> do+       let target = vm1.state.contract+       vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode >> Stepper.run)+       pure $ Just vm2+     _ -> pure Nothing+  where+    prepVm target targetCode = Stepper.evm $ do+      replaceCodeOfSelf (RuntimeCode $ ConcreteRuntimeCode targetCode)+      resetState+      assign (#state % #gas) 0xffffffffffffffff -- kludge+      loadContract target  hex :: ByteString -> ByteString hex s =@@ -2348,7 +2453,7 @@ runFunction :: Text -> ByteString -> IO (Maybe ByteString) runFunction c input = do   Just x <- singleContract "X" c-  return $ runSimpleVM x input+  runSimpleVM x input  runStatements   :: Text -> [AbiValue] -> AbiType@@ -2467,13 +2572,13 @@  genEnd :: Int -> Gen (Expr End) genEnd 0 = oneof- [ pure $ Failure [] EVM.Types.Invalid- , pure $ Failure [] EVM.Types.IllegalOverflow- , pure $ Failure [] EVM.Types.SelfDestruct+ [ fmap (Failure [] . UnrecognizedOpcode) arbitrary+ , pure $ Failure [] IllegalOverflow+ , pure $ Failure [] SelfDestruction  ] genEnd sz = oneof- [ fmap (EVM.Types.Revert []) subBuf- , liftM3 EVM.Types.Return (return []) subBuf subStore+ [ fmap (Failure [] . Revert) subBuf+ , liftM3 Success (return []) subBuf subStore  , liftM3 ITE subWord subEnd subEnd  ]  where