hevm 0.52.0 → 0.53.0

raw patch · 28 files changed

+8689/−7170 lines, 28 filesdep +MissingHdep +exceptionsdep +unliftio-corePVP ok

version bump matches the API change (PVP)

Dependencies added: MissingH, exceptions, unliftio-core

API changes (from Hackage documentation)

Files

• CHANGELOG.md +38/−0
• bench/bench.hs +11/−7
• cli/cli.hs +78/−64
• hevm.cabal +16/−6
• src/EVM.hs +2788/−2619
• src/EVM/ABI.hs +1/−1
• src/EVM/Effects.hs +123/−0
• src/EVM/Exec.hs +5/−5
• src/EVM/Expr.hs +223/−28
• src/EVM/Fetch.hs +14/−11
• src/EVM/Format.hs +83/−61
• src/EVM/Fuzz.hs +263/−0
• src/EVM/Keccak.hs +34/−19
• src/EVM/SMT.hs +100/−67
• src/EVM/Solidity.hs +22/−13
• src/EVM/Solvers.hs +107/−64
• src/EVM/Stepper.hs +30/−33
• src/EVM/SymExec.hs +156/−150
• src/EVM/Transaction.hs +1/−1
• src/EVM/Traversals.hs +4/−4
• src/EVM/Types.hs +133/−61
• src/EVM/UnitTest.hs +34/−35
• test/BlockchainTests.hs +6/−2
• test/EVM/Test/BlockchainTests.hs +60/−33
• test/EVM/Test/Tracing.hs +72/−65
• test/EVM/Test/Utils.hs +25/−6
• test/rpc.hs +25/−14
• test/test.hs +4237/−3801

@@ -1,3 +1,5 @@+## [0.53.0] - 2024-02-23+ # Changelog  All notable changes to this project will be documented in this file.@@ -5,6 +7,39 @@ 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). +## Changed++- Minimum distance requirements are now asserted for Keccak function calls. They assert that it's hard to generate two Keccak's that are less than 256 afar.+- Keccak concretization is now done only after all simplifications are performed. This helps with simplification pre-concretization+- Added an IllegalOverflow error in case the system tries to allocate a large amount of memory during+  abstract gas execution but concrete running. In these cases, the interpreter can out-of-heap+  as the only check is that the size allocated is less than $2**{64}$, but that is too large to fit in memory. Now,+  we check more stringently, and still return an IllegalOverflow+- Fixed `--root` option for the `test` subcommand++## Added++- Optimized smt queries that significantly improve performance when dealing with solidity mappings and arrays+- Support for using Bitwuzla as a solver+- More efficient encoding for failure in ds-test style tests+- Symbolic tests now support statically sized arrays as parameters+- `hevm test` now has a `num-solvers` parameter that controls how many solver instances to spawn+- New solc-specific simplification rules that should make the final Props a lot more readable+- Prop is now correctly ordered, better BufLength and Max simplifications of Expr,+  and further solc-specific simplifications of Expr+- Simplify earlier and don't check reachability for things statically determined to be FALSE+- New concrete fuzzer that can be controlled via `--num-cex-fuzz`+- Partial support for dynamic jumps when the jump destination can be computed+  given already available information+- Added three forking cheatcodes: `createFork`, `selectFork`, and `activeFork`++## Fixed++- Traces now correctly perform source mapping to display contract details+- Event traces now correctly display indexed arguments and argument names+- JSON reading of foundry JSONs was dependent on locale and did not work with many locales.+- CVC5 needs `--incremental` flag to work properly in abstraction-refinement mode+ ## [0.52.0] - 2023-10-26  This is a major breaking release that removes several user facing features and includes non trivial@@ -71,6 +106,7 @@ - `test` now falls back to displaying an unecoded bytestring for calldata when the model returned by the solver has a different length the length of the arguments in the test signature. - we now generate correct counterexamples for branches where only a subset of input variables are referenced by the path conditions - `vm.prank` now works correctly when passed a symbolic address+- `vm.prank` now works correctly when the next call transfers value - storage layout information will now be parsed from the output of `forge build` if it is available  ## API Changes@@ -109,9 +145,11 @@ - CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases - Better simplification of Eq IR elements - Run a toplevel constant folding reasoning system on branch conditions+- Global config via a monad, which should allow for more refactoring - `evalProp` is renamed to `simplifyProp` for consistency - Mem explosion in `writeWord` function was possible in case `offset` was close to 2^256. Fixed. - BufLength was not simplified via bufLength function. Fixed.+- Add and Mul are associative, let's use that to make Expr more canonical - `VMOpts` no longer takes an initial store, and instead takes a `baseState`   which can be either `EmptyBase` or `AbstractBase`. This controls whether   storage should be inialized as empty or fully abstract. Regardless of this

@@ -2,6 +2,7 @@  import GHC.Natural import Control.Monad+import Control.Monad.IO.Unlift import Data.Maybe import System.Environment (getEnv) @@ -19,6 +20,7 @@ import EVM.SymExec import EVM.Solidity import EVM.Solvers+import EVM.Effects import EVM.Format (hexByteString) import qualified EVM.Stepper as Stepper import qualified EVM.Fetch as Fetch@@ -67,16 +69,18 @@       if n `elem` ignored       then pure True       else do-        res <- runBCTest c+        res <- runApp $ runBCTest c         pure $ acc && res     ) True cases  -- | executes a single test case and returns a boolean value representing its success-runBCTest :: BCTests.Case -> IO Bool+runBCTest :: App m => BCTests.Case -> m Bool runBCTest x =  do-  vm0 <- BCTests.vmForCase x+  vm0 <- liftIO $ BCTests.vmForCase x   result <- Stepper.interpret (Fetch.zero 0 Nothing) vm0 Stepper.runFully+  writeTrace vm0+   maybeReason <- BCTests.checkExpectation False x result   pure $ isNothing maybeReason @@ -84,7 +88,7 @@ --- Helpers ----------------------------------------------------------------------------------------  -findPanics :: Solver -> Natural -> Integer -> ByteString -> IO ()+findPanics :: App m => Solver -> Natural -> Integer -> ByteString -> m () findPanics solver count iters c = do   _ <- withSolvers solver count Nothing $ \s -> do     let opts = defaultVeriOpts@@ -92,7 +96,7 @@           , askSmtIters = iters + 1           }     checkAssert s allPanicCodes c Nothing [] opts-  putStrLn "done"+  liftIO $ putStrLn "done"   -- constructs a benchmark suite that checks the given bytecode for reachable@@ -103,8 +107,8 @@ mkbench c name iters counts = localOption WallTime $ env c (bgroup name . bmarks)   where     bmarks c' = concat $ [-       [ bench ("cvc5-" <> show i) $ nfIO $ findPanics CVC5 i iters c'-       , bench ("z3-" <> show i) $ nfIO $ findPanics Z3 i iters c'+       [ bench ("cvc5-" <> show i) $ nfIO $ runApp $ findPanics CVC5 i iters c'+       , bench ("z3-" <> show i) $ nfIO $ runApp $ findPanics Z3 i iters c'        ]        | i <- counts      ]

@@ -8,6 +8,7 @@  import Control.Monad (when, forM_, unless) import Control.Monad.ST (RealWorld, stToIO)+import Control.Monad.IO.Unlift import Data.ByteString (ByteString) import Data.DoubleWord (Word256) import Data.List (intersperse)@@ -22,8 +23,7 @@ import Witch (unsafeInto) import Options.Generic as Options import Paths_hevm qualified as Paths-import System.IO (stderr)-import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist)+import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist, makeAbsolute) import System.FilePath ((</>)) import System.Exit (exitFailure, exitWith, ExitCode(..)) @@ -35,14 +35,16 @@ import GitHash import EVM.FeeSchedule (feeSchedule) import EVM.Fetch qualified as Fetch-import EVM.Format (hexByteString, strip0x, showTraceTree, formatExpr)+import EVM.Format (hexByteString, strip0x, formatExpr) import EVM.Solidity import EVM.Solvers import EVM.Stepper qualified import EVM.SymExec import EVM.Transaction qualified-import EVM.Types hiding (word)+import EVM.Types hiding (word, Env, Symbolic)+import EVM.Types qualified import EVM.UnitTest+import EVM.Effects  -- This record defines the program's command-line options -- automatically via the `optparse-generic` package.@@ -83,10 +85,13 @@       , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"       , 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"-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"+      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"+      , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour"+      , trace         :: w ::: Bool               <?> "Dump trace"       , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"       , 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)"+      , numCexFuzz    :: w ::: Integer            <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"       , 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"       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"@@ -100,10 +105,13 @@       , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"       , 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"-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"+      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"+      , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour"+      , trace         :: w ::: Bool             <?> "Dump trace"       , 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)"+      , numCexFuzz    :: w ::: Integer          <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"       , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"       , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"@@ -128,6 +136,7 @@       , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"       , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"       , chainid     :: w ::: Maybe W256        <?> "Env: chainId"+      , debug       :: w ::: Bool              <?> "Debug printing of internal behaviour"       , trace       :: w ::: Bool              <?> "Dump trace"       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"@@ -142,14 +151,18 @@       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"       , coverage      :: w ::: Bool                     <?> "Coverage analysis"       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"+      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"+      , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"+      , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour"+      , trace         :: w ::: Bool                     <?> "Dump trace"       , 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"       , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"       , abstractArithmetic    :: w ::: Bool             <?> "Use abstraction-refinement for complicated arithmetic functions such as MulMod. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"       , abstractMemory    :: w ::: Bool                      <?> "Use abstraction-refinement for Memory. This runs the solver first with abstraction turned on, and if it returns a potential counterexample, the counterexample is refined to make sure it is a counterexample for the actual (not the abstracted) problem"+      , numCexFuzz    :: w ::: Integer                  <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"       , 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@@ -186,54 +199,59 @@ main :: IO () main = do   cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"+  let env = Env { config = defaultConfig+    { dumpQueries = cmd.smtdebug+    , debug = cmd.debug+    , numCexFuzz = cmd.numCexFuzz+    , abstRefineMem = cmd.abstractMemory+    , abstRefineArith = cmd.abstractArithmetic+    , dumpTrace = cmd.trace+    } }   case cmd of     Version {} ->putStrLn getFullVersion     Symbolic {} -> do       root <- getRoot cmd-      withCurrentDirectory root $ assert cmd-    Equivalence {} -> equivalence cmd-    Exec {} ->-      launchExec cmd+      withCurrentDirectory root $ runEnv env $ assert cmd+    Equivalence {} -> runEnv env $ equivalence cmd+    Exec {} -> runEnv env $ launchExec cmd     Test {} -> do       root <- getRoot cmd-      withCurrentDirectory root $ do-        cores <- unsafeInto <$> getNumProcessors-        solver <- getSolver cmd-        withSolvers solver cores cmd.smttimeout $ \solvers -> do-          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)-              res <- unitTest testOpts out.contracts-              unless res exitFailure+      solver <- getSolver cmd+      cores <- liftIO $ unsafeInto <$> getNumProcessors+      let solverCount = fromMaybe cores cmd.numSolvers+      runEnv env $ withSolvers solver solverCount cmd.smttimeout $ \solvers -> do+        buildOut <- liftIO $ readBuildOutput root (getProjectType cmd)+        case buildOut of+          Left e -> liftIO $ 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 <- liftIO $ unitTestOptions cmd solvers (Just out)+            res <- unitTest testOpts out.contracts+            liftIO $ unless res exitFailure -equivalence :: Command Options.Unwrapped -> IO ()+equivalence :: App m => Command Options.Unwrapped -> m () equivalence cmd = do   let bytecodeA = hexByteString "--code" . strip0x $ cmd.codeA       bytecodeB = hexByteString "--code" . strip0x $ cmd.codeB       veriOpts = VeriOpts { simp = True-                          , debug = False                           , maxIter = cmd.maxIterations                           , askSmtIters = cmd.askSmtIterations                           , loopHeuristic = cmd.loopDetectionHeuristic-                          , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory                           , rpcInfo = Nothing                           }-  calldata <- buildCalldata cmd-  solver <- getSolver cmd+  calldata <- liftIO $ buildCalldata cmd+  solver <- liftIO $ getSolver cmd   withSolvers solver 3 Nothing $ \s -> do     res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata     case any isCex res of-      False -> do+      False -> liftIO $ do         putStrLn "No discrepancies found"         when (any isTimeout res) $ do           putStrLn "But timeout(s) occurred"           exitFailure-      True -> do+      True -> liftIO $ do         let cexs = mapMaybe getCex res         T.putStrLn . T.unlines $           [ "Not equivalent. The following inputs result in differing behaviours:"@@ -247,6 +265,7 @@                   Just s -> case T.unpack s of                               "z3" -> pure Z3                               "cvc5" -> pure CVC5+                              "bitwuzla" -> pure Bitwuzla                               input -> do                                 putStrLn $ "unrecognised solver: " <> input                                 exitFailure@@ -268,7 +287,7 @@ getProjectType cmd = fromMaybe Foundry cmd.projectType  getRoot :: Command Options.Unwrapped -> IO FilePath-getRoot cmd = maybe getCurrentDirectory pure (cmd.root)+getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)   -- | Builds a buffer representing calldata based on the given cli arguments@@ -289,29 +308,27 @@   -- If function signatures are known, they should always be given for best results.-assert :: Command Options.Unwrapped -> IO ()+assert :: App m => Command Options.Unwrapped -> m () assert cmd = do   let block'  = maybe Fetch.Latest Fetch.BlockNumber cmd.block       rpcinfo = (,) block' <$> cmd.rpc-  calldata <- buildCalldata cmd-  preState <- symvmFromCommand cmd calldata+  calldata <- liftIO $ buildCalldata cmd+  preState <- liftIO $ symvmFromCommand cmd calldata   let errCodes = fromMaybe defaultPanicCodes cmd.assertions-  cores <- unsafeInto <$> getNumProcessors+  cores <- liftIO $ unsafeInto <$> getNumProcessors   let solverCount = fromMaybe cores cmd.numSolvers-  solver <- getSolver cmd+  solver <- liftIO $ getSolver cmd   withSolvers solver solverCount cmd.smttimeout $ \solvers -> do     let opts = VeriOpts { simp = True-                        , debug = cmd.smtdebug                         , maxIter = cmd.maxIterations                         , askSmtIters = cmd.askSmtIterations                         , loopHeuristic = cmd.loopDetectionHeuristic-                        , abstRefineConfig = AbstRefineConfig cmd.abstractArithmetic cmd.abstractMemory                         , rpcInfo = rpcinfo     }     (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)     case res of       [Qed _] -> do-        putStrLn "\nQED: No reachable property violations discovered\n"+        liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"         showExtras solvers cmd calldata expr       _ -> do         let cexs = snd <$> mapMaybe getCex res@@ -330,25 +347,26 @@                  , "Could not determine reachability of the following end states:"                  , ""                  ] <> fmap (formatExpr) timeouts-        T.putStrLn $ T.unlines (counterexamples <> unknowns)+        liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)         showExtras solvers cmd calldata expr-        exitFailure+        liftIO $ exitFailure -showExtras :: SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> IO ()+showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m () showExtras solvers cmd calldata expr = do-  when cmd.showTree $ do+  when cmd.showTree $ liftIO $ do     putStrLn "=== Expression ===\n"     T.putStrLn $ formatExpr expr     putStrLn ""   when cmd.showReachableTree $ do     reached <- reachable solvers expr-    putStrLn "=== Reachable Expression ===\n"-    T.putStrLn (formatExpr . snd $ reached)-    putStrLn ""+    liftIO $ do+      putStrLn "=== Reachable Expression ===\n"+      T.putStrLn (formatExpr . snd $ reached)+      putStrLn ""   when cmd.getModels $ do-    putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"+    liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ===\n"     ms <- produceModels solvers expr-    forM_ ms (showModel (fst calldata))+    liftIO $ forM_ ms (showModel (fst calldata))  isTestOrLib :: Text -> Bool isTestOrLib file = T.isSuffixOf ".t.sol" file || areAnyPrefixOf ["src/test/", "src/tests/", "lib/"] file@@ -356,10 +374,10 @@ areAnyPrefixOf :: [Text] -> Text -> Bool areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes -launchExec :: Command Options.Unwrapped -> IO ()+launchExec :: App m => Command Options.Unwrapped -> m () launchExec cmd = do-  dapp <- getSrcInfo cmd-  vm <- vmFromCommand cmd+  dapp <- liftIO $ getSrcInfo cmd+  vm <- liftIO $ vmFromCommand cmd   let     block = maybe Fetch.Latest Fetch.BlockNumber cmd.block     rpcinfo = (,) block <$> cmd.rpc@@ -367,21 +385,18 @@   -- TODO: we shouldn't need solvers to execute this code   withSolvers Z3 0 Nothing $ \solvers -> do     vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully-    when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')+    writeTraceDapp dapp vm'     case vm'.result of-      Just (VMFailure (Revert msg)) -> do+      Just (VMFailure (Revert msg)) -> liftIO $ do         let res = case msg of                     ConcreteBuf bs -> bs                     _ -> "<symbolic>"         putStrLn $ "Revert: " <> (show $ ByteStringS res)         exitWith (ExitFailure 2)-      Just (VMFailure err) -> do+      Just (VMFailure err) -> liftIO $ do         putStrLn $ "Error: " <> show err         exitWith (ExitFailure 2)-      Just (Unfinished p) -> do-        putStrLn $ "Could not continue execution: " <> show p-        exitWith (ExitFailure 2)-      Just (VMSuccess buf) -> do+      Just (VMSuccess buf) -> liftIO $ do         let msg = case buf of               ConcreteBuf msg' -> msg'               _ -> "<symbolic>"@@ -390,7 +405,7 @@         internalError "no EVM result"  -- | Creates a (concrete) VM from command line options-vmFromCommand :: Command Options.Unwrapped -> IO (VM RealWorld)+vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld) vmFromCommand cmd = do   (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)@@ -481,7 +496,7 @@         addr f def = maybe def LitAddr (f cmd)         bytes f def = maybe def decipher (f cmd) -symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM RealWorld)+symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld) symvmFromCommand cmd calldata = do   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of     Nothing -> pure (SymAddr "miner",0,0,0)@@ -539,7 +554,7 @@       , address        = address       , caller         = caller       , origin         = origin-      , gas            = word64 (.gas) 0xffffffffffffffff+      , gas            = ()       , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff       , baseFee        = baseFee       , priorityFee    = word (.priorityFee) 0@@ -585,7 +600,6 @@          Nothing  -> Nothing     , maxIter = cmd.maxIterations     , askSmtIters = cmd.askSmtIterations-    , smtDebug = cmd.smtdebug     , smtTimeout = cmd.smttimeout     , solver = cmd.solver     , verbose = cmd.verbose

@@ -2,7 +2,7 @@ name:   hevm version:-  0.52.0+  0.53.0 synopsis:   Symbolic EVM Evaluator homepage:@@ -59,6 +59,8 @@     -Wno-orphans     -Wno-ambiguous-fields     -optc-Wno-ignored-attributes+    -fspecialize-aggressively+    -fexpose-all-unfoldings   default-language: GHC2021   default-extensions:     DuplicateRecordFields@@ -83,6 +85,7 @@     EVM.Expr,     EVM.SMT,     EVM.Solvers,+    EVM.Fuzz,     EVM.Exec,     EVM.Format,     EVM.Fetch,@@ -100,6 +103,7 @@     EVM.Types,     EVM.UnitTest,     EVM.Sign,+    EVM.Effects,   other-modules:     Paths_hevm   autogen-modules:@@ -178,7 +182,8 @@     stm                               >= 2.5.0 && < 2.6.0,     spawn                             >= 0.3 && < 0.4,     filepattern                       >= 0.1.2 && < 0.2,-    witch                             >= 1.1 && < 1.3+    witch                             >= 1.1 && < 1.3,+    unliftio-core                     >= 0.2.1.0   if !os(windows)     build-depends:       brick                           >= 1.4 && < 2.0,@@ -230,7 +235,8 @@     spawn,     optics-core,     githash                       >= 0.1.6 && < 0.2,-    witch+    witch,+    unliftio-core   if os(windows)     buildable: False @@ -281,7 +287,10 @@     operational,     optics-core,     optics-extra,-    witch+    witch,+    unliftio-core,+    exceptions,+    MissingH  library test-utils   import:@@ -319,7 +328,7 @@   main-is:     test.hs --- these tests require network access so we split them into a seperate test+-- these tests require network access so we split them into a separate test -- suite to make it easy to skip them when running nix-build test-suite rpc-tests   import:@@ -367,4 +376,5 @@     filemanip,     filepath,     containers,-    mtl+    mtl,+    unliftio-core

@@ -20,2622 +20,2791 @@ import EVM.Precompiled qualified import EVM.Solidity import EVM.Types-import EVM.Sign qualified-import EVM.Concrete qualified as Concrete--import Control.Monad.ST (ST)-import Control.Monad.State.Strict hiding (state)-import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)-import Data.ByteArray qualified as BA-import Data.ByteString (ByteString)-import Data.ByteString qualified as BS-import Data.ByteString.Lazy (fromStrict)-import Data.ByteString.Lazy qualified as LS-import Data.ByteString.Char8 qualified as Char8-import Data.Foldable (toList)-import Data.List (find)-import Data.Map.Strict (Map)-import Data.Map.Strict qualified as Map-import Data.Maybe (fromMaybe, fromJust, isJust)-import Data.Set (insert, member, fromList)-import Data.Sequence (Seq)-import Data.Sequence qualified as Seq-import Data.Text (unpack, pack)-import Data.Text.Encoding (decodeUtf8)-import Data.Tree-import Data.Tree.Zipper qualified as Zipper-import Data.Typeable-import Data.Vector qualified as V-import Data.Vector.Storable qualified as SV-import Data.Vector.Storable.Mutable qualified as SV-import Data.Vector.Unboxed qualified as VUnboxed-import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable-import Data.Word (Word8, Word32, Word64)-import Witch (into, tryFrom, unsafeInto)--import Crypto.Hash (Digest, SHA256, RIPEMD160)-import Crypto.Hash qualified as Crypto-import Crypto.Number.ModArithmetic (expFast)--blankState :: ST s (FrameState s)-blankState = do-  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0-  pure $ FrameState-    { contract     = LitAddr 0-    , codeContract = LitAddr 0-    , code         = RuntimeCode (ConcreteRuntimeCode "")-    , pc           = 0-    , stack        = mempty-    , memory-    , memorySize   = 0-    , calldata     = mempty-    , callvalue    = Lit 0-    , caller       = LitAddr 0-    , gas          = 0-    , returndata   = mempty-    , static       = False-    }---- | An "external" view of a contract's bytecode, appropriate for--- e.g. @EXTCODEHASH@.-bytecode :: Getter Contract (Maybe (Expr Buf))-bytecode = #code % to f-  where f (InitCode _ _) = Just mempty-        f (RuntimeCode (ConcreteRuntimeCode bs)) = Just $ ConcreteBuf bs-        f (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops-        f (UnknownCode _) = Nothing---- * Data accessors--currentContract :: VM s -> Maybe Contract-currentContract vm =-  Map.lookup vm.state.codeContract vm.env.contracts---- * Data constructors--makeVm :: VMOpts -> ST s (VM s)-makeVm o = do-  let txaccessList = o.txAccessList-      txorigin = o.origin-      txtoAddr = o.address-      initialAccessedAddrs = fromList $-           [txorigin, txtoAddr, o.coinbase]-        ++ (fmap LitAddr [1..9])-        ++ (Map.keys txaccessList)-      initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)-      touched = if o.create then [txorigin] else [txorigin, txtoAddr]-  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0-  pure $ VM-    { result = Nothing-    , frames = mempty-    , tx = TxState-      { gasprice = o.gasprice-      , gaslimit = o.gaslimit-      , priorityFee = o.priorityFee-      , origin = txorigin-      , toAddr = txtoAddr-      , value = o.value-      , substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty-      , isCreate = o.create-      , txReversion = Map.fromList ((o.address,o.contract):o.otherContracts)-      }-    , logs = []-    , traces = Zipper.fromForest []-    , block = Block-      { coinbase = o.coinbase-      , timestamp = o.timestamp-      , number = o.number-      , prevRandao = o.prevRandao-      , maxCodeSize = o.maxCodeSize-      , gaslimit = o.blockGaslimit-      , baseFee = o.baseFee-      , schedule = o.schedule-      }-    , state = FrameState-      { pc = 0-      , stack = mempty-      , memory-      , memorySize = 0-      , code = o.contract.code-      , contract = o.address-      , codeContract = o.address-      , calldata = fst o.calldata-      , callvalue = o.value-      , caller = o.caller-      , gas = o.gas-      , returndata = mempty-      , static = False-      }-    , env = Env-      { chainId = o.chainId-      , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)-      , freshAddresses = 0-      }-    , cache = Cache mempty mempty-    , burned = 0-    , constraints = snd o.calldata-    , keccakEqs = mempty-    , iterations = mempty-    , config = RuntimeConfig-      { allowFFI = o.allowFFI-      , overrideCaller = Nothing-      , baseState = o.baseState-      }-    }---- | Initialize an abstract contract with unknown code-unknownContract :: Expr EAddr -> Contract-unknownContract addr = Contract-  { code        = UnknownCode addr-  , storage     = AbstractStore addr-  , origStorage = AbstractStore addr-  , balance     = Balance addr-  , nonce       = Nothing-  , codehash    = hashcode (UnknownCode addr)-  , opIxMap     = mempty-  , codeOps     = mempty-  , external    = False-  }---- | Initialize an abstract contract with known code-abstractContract :: ContractCode -> Expr EAddr -> Contract-abstractContract code addr = Contract-  { code        = code-  , storage     = AbstractStore addr-  , origStorage = AbstractStore addr-  , balance     = Balance addr-  , nonce       = if isCreation code then Just 1 else Just 0-  , codehash    = hashcode code-  , opIxMap     = mkOpIxMap code-  , codeOps     = mkCodeOps code-  , external    = False-  }---- | Initialize an empty contract without code-emptyContract :: Contract-emptyContract = initialContract (RuntimeCode (ConcreteRuntimeCode ""))---- | Initialize empty contract with given code-initialContract :: ContractCode -> Contract-initialContract code = Contract-  { code        = code-  , storage     = ConcreteStore mempty-  , origStorage = ConcreteStore mempty-  , balance     = Lit 0-  , nonce       = if isCreation code then Just 1 else Just 0-  , codehash    = hashcode code-  , opIxMap     = mkOpIxMap code-  , codeOps     = mkCodeOps code-  , external    = False-  }--isCreation :: ContractCode -> Bool-isCreation = \case-  InitCode _ _  -> True-  RuntimeCode _ -> False-  UnknownCode _ -> False---- * Opcode dispatch (exec1)---- | Update program counter-next :: (?op :: Word8) => EVM s ()-next = modifying (#state % #pc) (+ (opSize ?op))---- | Executes the EVM one step-exec1 :: EVM s ()-exec1 = do-  vm <- get--  let-    -- Convenient aliases-    stk  = vm.state.stack-    self = vm.state.contract-    this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)--    fees@FeeSchedule {..} = vm.block.schedule--    doStop = finishFrame (FrameReturned mempty)--    litSelf = maybeLitAddr self--  if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0x9 then do-    -- call to precompile-    let ?op = 0x00 -- dummy value-    case bufLength vm.state.calldata of-      Lit calldatasize -> do-          copyBytesToMemory vm.state.calldata (Lit calldatasize) (Lit 0) (Lit 0)-          executePrecompile (fromJust litSelf) vm.state.gas 0 calldatasize 0 0 []-          vmx <- get-          case vmx.state.stack of-            x:_ -> case x of-              Lit 0 ->-                fetchAccount self $ \_ -> do-                  touchAccount self-                  vmError PrecompileFailure-              Lit _ ->-                fetchAccount self $ \_ -> do-                  touchAccount self-                  out <- use (#state % #returndata)-                  finishFrame (FrameReturned out)-              e -> partial $-                     UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])-            _ ->-              underrun-      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--    else do-      let ?op = case vm.state.code of-                  UnknownCode _ -> internalError "Cannot execute unknown code"-                  InitCode conc _ -> BS.index conc vm.state.pc-                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc-                  RuntimeCode (SymbolicRuntimeCode ops) ->-                    fromMaybe (internalError "could not analyze symbolic code") $-                      maybeLitByte $ ops V.! vm.state.pc--      case getOp (?op) of--        OpPush0 -> do-          limitStack 1 $-            burn g_base $ do-              next-              pushSym (Lit 0)--        OpPush n' -> do-          let n = into n'-              !xs = case vm.state.code of-                UnknownCode _ -> internalError "Cannot execute unknown code"-                InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm.state.pc) conc)-                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm.state.pc) bs-                RuntimeCode (SymbolicRuntimeCode ops) ->-                  let bytes = V.take n $ V.drop (1 + vm.state.pc) ops-                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes-          limitStack 1 $-            burn g_verylow $ do-              next-              pushSym xs--        OpDup i ->-          case preview (ix (into i - 1)) stk of-            Nothing -> underrun-            Just y ->-              limitStack 1 $-                burn g_verylow $ do-                  next-                  pushSym y--        OpSwap i ->-          if length stk < (into i) + 1-            then underrun-            else-              burn g_verylow $ do-                next-                zoom (#state % #stack) $ do-                  assign (ix 0) (stk ^?! ix (into i))-                  assign (ix (into i)) (stk ^?! ix 0)--        OpLog n ->-          notStatic $-          case stk of-            (xOffset':xSize':xs) ->-              if length xs < (into n)-              then underrun-              else-                forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do-                    bytes <- readMemory xOffset' xSize'-                    let (topics, xs') = splitAt (into n) xs-                        logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs-                    case (tryFrom xSize) of-                      (Right sz) ->-                        burn (g_log + g_logdata * sz + (into n) * g_logtopic) $-                          accessMemoryRange xOffset xSize $ do-                            traceTopLog logs'-                            next-                            assign (#state % #stack) xs'-                            assign #logs logs'-                      _ -> vmError IllegalOverflow-            _ ->-              underrun--        OpStop -> doStop--        OpAdd -> stackOp2 g_verylow Expr.add-        OpMul -> stackOp2 g_low Expr.mul-        OpSub -> stackOp2 g_verylow Expr.sub--        OpDiv -> stackOp2 g_low Expr.div--        OpSdiv -> stackOp2 g_low Expr.sdiv--        OpMod -> stackOp2 g_low Expr.mod--        OpSmod -> stackOp2 g_low Expr.smod-        OpAddmod -> stackOp3 g_mid Expr.addmod-        OpMulmod -> stackOp3 g_mid Expr.mulmod--        OpLt -> stackOp2 g_verylow Expr.lt-        OpGt -> stackOp2 g_verylow Expr.gt-        OpSlt -> stackOp2 g_verylow Expr.slt-        OpSgt -> stackOp2 g_verylow Expr.sgt--        OpEq -> stackOp2 g_verylow Expr.eq-        OpIszero -> stackOp1 g_verylow Expr.iszero--        OpAnd -> stackOp2 g_verylow Expr.and-        OpOr -> stackOp2 g_verylow Expr.or-        OpXor -> stackOp2 g_verylow Expr.xor-        OpNot -> stackOp1 g_verylow Expr.not--        OpByte -> stackOp2 g_verylow (\i w -> Expr.padByte $ Expr.indexWord i w)--        OpShl -> stackOp2 g_verylow Expr.shl-        OpShr -> stackOp2 g_verylow Expr.shr-        OpSar -> stackOp2 g_verylow Expr.sar--        -- more accurately refered to as KECCAK-        OpSha3 ->-          case stk of-            xOffset':xSize':xs ->-              forceConcrete xOffset' "sha3 offset must be concrete" $-                \xOffset -> forceConcrete xSize' "sha3 size must be concrete" $ \xSize ->-                  burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) $-                    accessMemoryRange xOffset xSize $ do-                      hash <- readMemory xOffset' xSize' >>= \case-                        ConcreteBuf bs -> do-                          let hash' = keccak' bs-                          eqs <- use #keccakEqs-                          assign #keccakEqs $-                            PEq (Lit hash') (Keccak (ConcreteBuf bs)):eqs-                          pure $ Lit hash'-                        buf -> pure $ Keccak buf-                      next-                      assign (#state % #stack) (hash : xs)-            _ -> underrun--        OpAddress ->-          limitStack 1 $-            burn g_base (next >> pushAddr self)--        OpBalance ->-          case stk of-            x:xs -> forceAddr x "BALANCE" $ \a ->-              accessAndBurn a $-                fetchAccount a $ \c -> do-                  next-                  assign (#state % #stack) xs-                  pushSym c.balance-            [] ->-              underrun--        OpOrigin ->-          limitStack 1 . burn g_base $-            next >> pushAddr vm.tx.origin--        OpCaller ->-          limitStack 1 . burn g_base $-            next >> pushAddr vm.state.caller--        OpCallvalue ->-          limitStack 1 . burn g_base $-            next >> pushSym vm.state.callvalue--        OpCalldataload -> stackOp1 g_verylow $-          \ind -> Expr.readWord ind vm.state.calldata--        OpCalldatasize ->-          limitStack 1 . burn g_base $-            next >> pushSym (bufLength vm.state.calldata)--        OpCalldatacopy ->-          case stk of-            xTo':xFrom:xSize':xs ->-              forceConcrete2 (xTo', xSize') "CALLDATACOPY" $-                \(xTo, xSize) ->-                  burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $-                    accessMemoryRange xTo xSize $ do-                      next-                      assign (#state % #stack) xs-                      copyBytesToMemory vm.state.calldata xSize' xFrom xTo'-            _ -> underrun--        OpCodesize ->-          limitStack 1 . burn g_base $-            next >> pushSym (codelen vm.state.code)--        OpCodecopy ->-          case stk of-            memOffset':codeOffset:n':xs ->-              forceConcrete2 (memOffset', n') "CODECOPY" $-                \(memOffset,n) -> do-                  case toWord64 n of-                    Nothing -> vmError IllegalOverflow-                    Just n'' ->-                      if n'' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then-                        burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) $-                          accessMemoryRange memOffset n $ do-                            next-                            assign (#state % #stack) xs-                            case toBuf vm.state.code of-                              Just b -> copyBytesToMemory b n' codeOffset memOffset'-                              Nothing -> internalError "Cannot produce a buffer from UnknownCode"-                      else vmError IllegalOverflow-            _ -> underrun--        OpGasprice ->-          limitStack 1 . burn g_base $-            next >> push vm.tx.gasprice--        OpExtcodesize ->-          case stk of-            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do-              let impl = accessAndBurn x $-                           fetchAccount x $ \c -> do-                             next-                             assign (#state % #stack) xs-                             case view bytecode c of-                               Just b -> pushSym (bufLength b)-                               Nothing -> pushSym $ CodeSize x-              case x of-                a@(LitAddr _) -> if a == cheatCode-                  then do-                    next-                    assign (#state % #stack) xs-                    pushSym (Lit 1)-                  else impl-                _ -> impl-            [] ->-              underrun--        OpExtcodecopy ->-          case stk of-            extAccount':memOffset':codeOffset:codeSize':xs ->-              forceConcrete2 (memOffset', codeSize') "EXTCODECOPY" $ \(memOffset, codeSize) -> do-                forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do-                  acc <- accessAccountForGas extAccount-                  let cost = if acc then g_warm_storage_read else g_cold_account_access-                  burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) $-                    accessMemoryRange memOffset codeSize $-                      fetchAccount extAccount $ \c -> do-                        next-                        assign (#state % #stack) xs-                        case view bytecode c of-                          Just b -> copyBytesToMemory b codeSize' codeOffset memOffset'-                          Nothing -> do-                            pc <- use (#state % #pc)-                            partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])-            _ -> underrun--        OpReturndatasize ->-          limitStack 1 . burn g_base $-            next >> pushSym (bufLength vm.state.returndata)--        OpReturndatacopy ->-          case stk of-            xTo':xFrom:xSize':xs -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $-              \(xTo, xSize) ->-                burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) $-                  accessMemoryRange xTo xSize $ do-                    next-                    assign (#state % #stack) xs--                    let jump True = vmError ReturnDataOutOfBounds-                        jump False = copyBytesToMemory vm.state.returndata xSize' xFrom xTo'--                    case (xFrom, bufLength vm.state.returndata) of-                      (Lit f, Lit l) ->-                        jump $ l < f + xSize || f + xSize < f-                      _ -> do-                        let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize')-                            overflow = Expr.lt (Expr.add xFrom xSize') (xFrom)-                        branch (Expr.or oob overflow) jump-            _ -> underrun--        OpExtcodehash ->-          case stk of-            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->-              accessAndBurn x $ do-                next-                assign (#state % #stack) xs-                fetchAccount x $ \c ->-                   if accountEmpty c-                     then push (W256 0)-                     else case view bytecode c of-                            Just b -> pushSym $ keccak b-                            Nothing -> pushSym $ CodeHash x-            [] ->-              underrun--        OpBlockhash -> do-          -- We adopt the fake block hash scheme of the VMTests,-          -- so that blockhash(i) is the hash of i as decimal ASCII.-          stackOp1 g_blockhash $ \case-            Lit i -> if i + 256 < vm.block.number || i >= vm.block.number-                     then Lit 0-                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit-            i -> BlockHash i--        OpCoinbase ->-          limitStack 1 . burn g_base $-            next >> pushAddr vm.block.coinbase--        OpTimestamp ->-          limitStack 1 . burn g_base $-            next >> pushSym vm.block.timestamp--        OpNumber ->-          limitStack 1 . burn g_base $-            next >> push vm.block.number--        OpPrevRandao -> do-          limitStack 1 . burn g_base $-            next >> push vm.block.prevRandao--        OpGaslimit ->-          limitStack 1 . burn g_base $-            next >> push (into vm.block.gaslimit)--        OpChainid ->-          limitStack 1 . burn g_base $-            next >> push vm.env.chainId--        OpSelfbalance ->-          limitStack 1 . burn g_low $-            next >> pushSym this.balance--        OpBaseFee ->-          limitStack 1 . burn g_base $-            next >> push vm.block.baseFee--        OpPop ->-          case stk of-            _:xs -> burn g_base (next >> assign (#state % #stack) xs)-            _    -> underrun--        OpMload ->-          case stk of-            x':xs -> forceConcrete x' "MLOAD" $ \x ->-              burn g_verylow $-                accessMemoryWord x $ do-                  next-                  buf <- readMemory (Lit x) (Lit 32)-                  let w = Expr.readWordFromBytes (Lit 0) buf-                  assign (#state % #stack) (w : xs)-            _ -> underrun--        OpMstore ->-          case stk of-            x':y:xs -> forceConcrete x' "MSTORE index" $ \x ->-              burn g_verylow $-                accessMemoryWord x $ do-                  next-                  gets (.state.memory) >>= \case-                    ConcreteMemory mem -> do-                      case y of-                        Lit w ->-                          writeMemory mem (unsafeInto x) (word256Bytes w)-                        _ -> do-                          -- copy out and move to symbolic memory-                          buf <- freezeMemory mem-                          assign (#state % #memory) (SymbolicMemory $ writeWord (Lit x) y buf)-                    SymbolicMemory mem ->-                      assign (#state % #memory) (SymbolicMemory $ writeWord (Lit x) y mem)-                  assign (#state % #stack) xs-            _ -> underrun--        OpMstore8 ->-          case stk of-            x':y:xs -> forceConcrete x' "MSTORE8" $ \x ->-              burn g_verylow $-                accessMemoryRange x 1 $ do-                  let yByte = indexWord (Lit 31) y-                  next-                  gets (.state.memory) >>= \case-                    ConcreteMemory mem -> do-                      case yByte of-                        LitByte byte ->-                          writeMemory mem (unsafeInto x) (BS.pack [byte])-                        _ -> do-                          -- copy out and move to symbolic memory-                          buf <- freezeMemory mem-                          assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte buf)-                    SymbolicMemory mem ->-                      assign (#state % #memory) (SymbolicMemory $ writeByte (Lit x) yByte mem)--                  assign (#state % #stack) xs-            _ -> underrun--        OpSload ->-          case stk of-            x:xs -> do-              acc <- accessStorageForGas self x-              let cost = if acc then g_warm_storage_read else g_cold_sload-              burn cost $-                accessStorage self x $ \y -> do-                  next-                  assign (#state % #stack) (y:xs)-            _ -> underrun--        OpSstore ->-          notStatic $-          case stk of-            x:new:xs ->-              accessStorage self x $ \current -> do-                availableGas <- use (#state % #gas)--                if availableGas <= g_callstipend then-                  finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))-                else do-                  let-                    original =-                      case Expr.simplify $ SLoad x this.origStorage of-                        Lit v -> v-                        _ -> 0-                    storage_cost =-                      case (maybeLitWord current, maybeLitWord new) of-                        (Just current', Just new') ->-                           if (current' == new') then g_sload-                           else if (current' == original) && (original == 0) then g_sset-                           else if (current' == original) then g_sreset-                           else g_sload--                        -- if any of the arguments are symbolic,-                        -- assume worst case scenario-                        _-> g_sset--                  acc <- accessStorageForGas self x-                  let cold_storage_cost = if acc then 0 else g_cold_sload-                  burn (storage_cost + cold_storage_cost) $ do-                    next-                    assign (#state % #stack) xs-                    modifying (#env % #contracts % ix self % #storage) (writeStorage x new)--                    case (maybeLitWord current, maybeLitWord new) of-                       (Just current', Just new') ->-                          unless (current' == new') $-                            if current' == original then-                              when (original /= 0 && new' == 0) $-                                refund (g_sreset + g_access_list_storage_key)-                            else do-                              when (original /= 0) $-                                if current' == 0-                                then unRefund (g_sreset + g_access_list_storage_key)-                                else when (new' == 0) $ refund (g_sreset + g_access_list_storage_key)-                              when (original == new') $-                                if original == 0-                                then refund (g_sset - g_sload)-                                else refund (g_sreset - g_sload)-                       -- if any of the arguments are symbolic,-                       -- don't change the refund counter-                       _ -> noop-            _ -> underrun--        OpJump ->-          case stk of-            x:xs ->-              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->-                case toInt x' of-                  Nothing -> vmError BadJumpDestination-                  Just i -> checkJump i xs-            _ -> underrun--        OpJumpi -> do-          case stk of-            (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->-                burn g_high $-                  let jump :: Bool -> EVM s ()-                      jump False = assign (#state % #stack) xs >> next-                      jump _    = case toInt x' of-                        Nothing -> vmError BadJumpDestination-                        Just i -> checkJump i xs-                  in branch y jump-            _ -> underrun--        OpPc ->-          limitStack 1 . burn g_base $-            next >> push (unsafeInto vm.state.pc)--        OpMsize ->-          limitStack 1 . burn g_base $-            next >> push (into vm.state.memorySize)--        OpGas ->-          limitStack 1 . burn g_base $-            next >> push (into (vm.state.gas - g_base))--        OpJumpdest -> burn g_jumpdest next--        OpExp ->-          -- NOTE: this can be done symbolically using unrolling like this:-          --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E-          --       However, it requires symbolic gas, since the gas depends on the exponent-          case stk of-            base:exponent':xs -> forceConcrete exponent' "EXP: symbolic exponent" $ \exponent ->-              let cost = if exponent == 0-                         then g_exp-                         else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)-              in burn cost $ do-                next-                (#state % #stack) .= Expr.exp base exponent' : xs-            _ -> underrun--        OpSignextend -> stackOp2 g_low Expr.sex--        OpCreate ->-          notStatic $-          case stk of-            xValue:xOffset':xSize':xs -> forceConcrete2 (xOffset', xSize') "CREATE" $-              \(xOffset, xSize) -> do-                accessMemoryRange xOffset xSize $ do-                  availableGas <- use (#state % #gas)-                  let-                    (cost, gas') = costOfCreate fees availableGas xSize False-                  newAddr <- createAddress self this.nonce-                  _ <- accessAccountForGas newAddr-                  burn cost $ do-                    initCode <- readMemory xOffset' xSize'-                    create self this xSize gas' xValue xs newAddr initCode-            _ -> underrun--        OpCall ->-          case stk of-            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALL" $-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->-                branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do-                  (if gt0 then notStatic else id) $-                    forceAddr xTo' "unable to determine a call target" $ \xTo ->-                      case tryFrom xGas of-                        Left _ -> vmError IllegalOverflow-                        Right gas ->-                          delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $-                            \callee -> do-                              let from' = fromMaybe self vm.config.overrideCaller-                              zoom #state $ do-                                assign #callvalue xValue-                                assign #caller from'-                                assign #contract callee-                              assign (#config % #overrideCaller) Nothing-                              touchAccount from'-                              touchAccount callee-                              transfer from' callee xValue-            _ ->-              underrun--        OpCallcode ->-          case stk of-            xGas':xTo':xValue:xInOffset':xInSize':xOutOffset':xOutSize':xs ->-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "CALLCODE" $-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->-                forceAddr xTo' "unable to determine a call target" $ \xTo ->-                  case tryFrom xGas of-                    Left _ -> vmError IllegalOverflow-                    Right gas ->-                      delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do-                        zoom #state $ do-                          assign #callvalue xValue-                          assign #caller $ fromMaybe self vm.config.overrideCaller-                        assign (#config % #overrideCaller) Nothing-                        touchAccount self-            _ ->-              underrun--        OpReturn ->-          case stk of-            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->-              accessMemoryRange xOffset xSize $ do-                output <- readMemory xOffset' xSize'-                let-                  codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")-                               . maybeLitWord . bufLength $ output-                  maxsize = vm.block.maxCodeSize-                  creation = case vm.frames of-                    [] -> vm.tx.isCreate-                    frame:_ -> case frame.context of-                       CreationContext {} -> True-                       CallContext {} -> False-                if creation-                then-                  if codesize > maxsize-                  then-                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))-                  else do-                    let frameReturned = burn (g_codedeposit * unsafeInto codesize) $-                                          finishFrame (FrameReturned output)-                        frameErrored = finishFrame $ FrameErrored InvalidFormat-                    case readByte (Lit 0) output of-                      LitByte 0xef -> frameErrored-                      LitByte _ -> frameReturned-                      y -> branch (Expr.eqByte y (LitByte 0xef)) $ \case-                          True -> frameErrored-                          False -> frameReturned-                else-                   finishFrame (FrameReturned output)-            _ -> underrun--        OpDelegatecall ->-          case stk of-            xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "DELEGATECALL" $-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) ->-                case wordToAddr xTo of-                  Nothing -> do-                    loc <- codeloc-                    let msg = "Unable to determine a call target"-                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]-                  Just xTo' ->-                    case tryFrom xGas of-                      Left _ -> vmError IllegalOverflow-                      Right gas ->-                        delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $-                          \_ -> touchAccount self-            _ -> underrun--        OpCreate2 -> notStatic $-          case stk of-            xValue:xOffset':xSize':xSalt':xs ->-              forceConcrete3 (xOffset', xSize', xSalt') "CREATE2" $-              \(xOffset, xSize, xSalt) ->-                accessMemoryRange xOffset xSize $ do-                  availableGas <- use (#state % #gas)-                  buf <- readMemory xOffset' xSize'-                  forceConcreteBuf buf "CREATE2" $-                    \initCode -> do-                      let-                        (cost, gas') = costOfCreate fees availableGas xSize True-                      newAddr <- create2Address self xSalt initCode-                      _ <- accessAccountForGas newAddr-                      burn cost $-                        create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode)-            _ -> underrun--        OpStaticcall ->-          case stk of-            xGas':xTo:xInOffset':xInSize':xOutOffset':xOutSize':xs ->-              forceConcrete5 (xGas', xInOffset', xInSize', xOutOffset', xOutSize') "STATICCALL" $-              \(xGas, xInOffset, xInSize, xOutOffset, xOutSize) -> do-                case wordToAddr xTo of-                  Nothing -> do-                    loc <- codeloc-                    let msg = "Unable to determine a call target"-                    partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]-                  Just xTo' ->-                    case tryFrom xGas of-                      Left _ -> vmError IllegalOverflow-                      Right gas ->-                        delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $-                          \callee -> do-                            zoom #state $ do-                              assign #callvalue (Lit 0)-                              assign #caller $ fromMaybe self (vm.config.overrideCaller)-                              assign #contract callee-                              assign #static True-                            assign (#config % #overrideCaller) Nothing-                            touchAccount self-                            touchAccount callee-            _ ->-              underrun--        OpSelfdestruct ->-          notStatic $-          case stk of-            [] -> underrun-            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case-              xTo@(LitAddr _) -> do-                acc <- accessAccountForGas xTo-                let cost = if acc then 0 else g_cold_account_access-                    funds = this.balance-                    recipientExists = accountExists xTo vm-                branch (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do-                  let c_new = if (not recipientExists) && hasFunds-                              then g_selfdestruct_newaccount-                              else 0-                  burn (g_selfdestruct + c_new + cost) $ do-                    selfdestruct self-                    touchAccount xTo--                    if hasFunds-                    then fetchAccount xTo $ \_ -> do-                           #env % #contracts % ix xTo % #balance %= (Expr.add funds)-                           assign (#env % #contracts % ix self % #balance) (Lit 0)-                           doStop-                    else do-                      doStop-              a -> do-                pc <- use (#state % #pc)-                partial $ UnexpectedSymbolicArg pc "trying to self destruct to a symbolic address" (wrap [a])--        OpRevert ->-          case stk of-            xOffset':xSize':_ -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->-              accessMemoryRange xOffset xSize $ do-                output <- readMemory xOffset' xSize'-                finishFrame (FrameReverted output)-            _ -> underrun--        OpUnknown xxx ->-          vmError $ UnrecognizedOpcode xxx--transfer :: Expr EAddr -> Expr EAddr -> Expr EWord -> EVM s ()-transfer _ _ (Lit 0) = pure ()-transfer src dst val = do-  sb <- preuse $ #env % #contracts % ix src % #balance-  db <- preuse $ #env % #contracts % ix dst % #balance-  baseState <- use (#config % #baseState)-  let mkc = case baseState of-              AbstractBase -> unknownContract-              EmptyBase -> const emptyContract-  case (sb, db) of-    -- both sender and recipient in state-    (Just srcBal, Just _) ->-      branch (Expr.gt val srcBal) $ \case-        True -> vmError $ BalanceTooLow val srcBal-        False -> do-          (#env % #contracts % ix src % #balance) %= (`Expr.sub` val)-          (#env % #contracts % ix dst % #balance) %= (`Expr.add` val)-    -- sender not in state-    (Nothing, Just _) -> do-      case src of-        LitAddr _ -> do-          (#env % #contracts) %= (Map.insert src (mkc src))-          transfer src dst val-        SymAddr _ -> do-          pc <- use (#state % #pc)-          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [src])-        GVar _ -> internalError "Unexpected GVar"-    -- recipient not in state-    (_ , Nothing) -> do-      case dst of-        LitAddr _ -> do-          (#env % #contracts) %= (Map.insert dst (mkc dst))-          transfer src dst val-        SymAddr _ -> do-          pc <- use (#state % #pc)-          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth to a symbolic address that is not present in the state" (wrap [dst])-        GVar _ -> internalError "Unexpected GVar"---- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.-callChecks-  :: (?op :: Word8)-  => Contract -> Word64 -> Expr EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]-   -- continuation with gas available for call-  -> (Word64 -> EVM s ())-  -> EVM s ()-callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do-  vm <- get-  let fees = vm.block.schedule-  accessMemoryRange xInOffset xInSize $-    accessMemoryRange xOutOffset xOutSize $ do-      availableGas <- use (#state % #gas)-      let recipientExists = accountExists xContext vm-      (cost, gas') <- costOfCall fees recipientExists xValue availableGas xGas xTo-      burn (cost - gas') $-        branch (Expr.gt xValue this.balance) $ \case-          True -> do-            assign (#state % #stack) (Lit 0 : xs)-            assign (#state % #returndata) mempty-            pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)-            next-          False ->-            if length vm.frames >= 1024-            then do-              assign (#state % #stack) (Lit 0 : xs)-              assign (#state % #returndata) mempty-              pushTrace $ ErrorTrace CallDepthLimitReached-              next-            else continue gas'--precompiledContract-  :: (?op :: Word8)-  => Contract-  -> Word64-  -> Addr-  -> Addr-  -> Expr EWord-  -> W256 -> W256 -> W256 -> W256-  -> [Expr EWord]-  -> EVM s ()-precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs-  = callChecks this xGas (LitAddr recipient) (LitAddr precompileAddr) xValue inOffset inSize outOffset outSize xs $ \gas' ->-    do-      executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs-      self <- use (#state % #contract)-      stk <- use (#state % #stack)-      pc' <- use (#state % #pc)-      result' <- use #result-      case result' of-        Nothing -> case stk of-          x:_ -> case maybeLitWord x of-            Just 0 ->-              pure ()-            Just 1 ->-              fetchAccount (LitAddr recipient) $ \_ -> do-                touchAccount self-                touchAccount (LitAddr recipient)-                transfer self (LitAddr recipient) xValue-            _ -> partial $-                   UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [x])-          _ -> underrun-        _ -> pure ()--executePrecompile-  :: (?op :: Word8)-  => Addr-  -> Word64 -> W256 -> W256 -> W256 -> W256 -> [Expr EWord]-  -> EVM s ()-executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do-  vm <- get-  input <- readMemory (Lit inOffset) (Lit inSize)-  let fees = vm.block.schedule-      cost = costOfPrecompile fees preCompileAddr input-      notImplemented = internalError $ "precompile at address " <> show preCompileAddr <> " not yet implemented"-      precompileFail = burn (gasCap - cost) $ do-                         assign (#state % #stack) (Lit 0 : xs)-                         pushTrace $ ErrorTrace PrecompileFailure-                         next-  if cost > gasCap then-    burn gasCap $ do-      assign (#state % #stack) (Lit 0 : xs)-      next-  else burn cost $-    case preCompileAddr of-      -- ECRECOVER-      0x1 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "ECRECOVER" $ \input' -> do-          case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of-            Nothing -> do-              -- return no output for invalid signature-              assign (#state % #stack) (Lit 1 : xs)-              assign (#state % #returndata) mempty-              next-            Just output -> do-              assign (#state % #stack) (Lit 1 : xs)-              assign (#state % #returndata) (ConcreteBuf output)-              copyBytesToMemory (ConcreteBuf output) (Lit outSize) (Lit 0) (Lit outOffset)-              next--      -- SHA2-256-      0x2 ->-        forceConcreteBuf input "SHA2-256" $ \input' -> do-          let-            hash = sha256Buf input'-            sha256Buf x = ConcreteBuf $ BA.convert (Crypto.hash x :: Digest SHA256)-          assign (#state % #stack) (Lit 1 : xs)-          assign (#state % #returndata) hash-          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)-          next--      -- RIPEMD-160-      0x3 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "RIPEMD160" $ \input' -> do-          let-            padding = BS.pack $ replicate 12 0-            hash' = BA.convert (Crypto.hash input' :: Digest RIPEMD160)-            hash  = ConcreteBuf $ padding <> hash'-          assign (#state % #stack) (Lit 1 : xs)-          assign (#state % #returndata) hash-          copyBytesToMemory hash (Lit outSize) (Lit 0) (Lit outOffset)-          next--      -- IDENTITY-      0x4 -> do-          assign (#state % #stack) (Lit 1 : xs)-          assign (#state % #returndata) input-          copyCallBytesToMemory input (Lit outSize) (Lit outOffset)-          next--      -- MODEXP-      0x5 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "MODEXP" $ \input' -> do-          let-            (lenb, lene, lenm) = parseModexpLength input'--            output = ConcreteBuf $-              if isZero (96 + lenb + lene) lenm input'-              then truncpadlit (unsafeInto lenm) (asBE (0 :: Int))-              else-                let-                  b = asInteger $ lazySlice 96 lenb input'-                  e = asInteger $ lazySlice (96 + lenb) lene input'-                  m = asInteger $ lazySlice (96 + lenb + lene) lenm input'-                in-                  padLeft (unsafeInto lenm) (asBE (expFast b e m))-          assign (#state % #stack) (Lit 1 : xs)-          assign (#state % #returndata) output-          copyBytesToMemory output (Lit outSize) (Lit 0) (Lit outOffset)-          next--      -- ECADD-      0x6 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "ECADD" $ \input' ->-          case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of-            Nothing -> precompileFail-            Just output -> do-              let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-              assign (#state % #stack) (Lit 1 : xs)-              assign (#state % #returndata) truncpaddedOutput-              copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-              next--      -- ECMUL-      0x7 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "ECMUL" $ \input' ->-          case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of-          Nothing -> precompileFail-          Just output -> do-            let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-            assign (#state % #stack) (Lit 1 : xs)-            assign (#state % #returndata) truncpaddedOutput-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-            next--      -- ECPAIRING-      0x8 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "ECPAIR" $ \input' ->-          case EVM.Precompiled.execute 0x8 input' 32 of-          Nothing -> precompileFail-          Just output -> do-            let truncpaddedOutput = ConcreteBuf $ truncpadlit 32 output-            assign (#state % #stack) (Lit 1 : xs)-            assign (#state % #returndata) truncpaddedOutput-            copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-            next--      -- BLAKE2-      0x9 ->-        -- TODO: support symbolic variant-        forceConcreteBuf input "BLAKE2" $ \input' -> do-          case (BS.length input', 1 >= BS.last input') of-            (213, True) -> case EVM.Precompiled.execute 0x9 input' 64 of-              Just output -> do-                let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output-                assign (#state % #stack) (Lit 1 : xs)-                assign (#state % #returndata) truncpaddedOutput-                copyBytesToMemory truncpaddedOutput (Lit outSize) (Lit 0) (Lit outOffset)-                next-              Nothing -> precompileFail-            _ -> precompileFail--      _ -> notImplemented--truncpadlit :: Int -> ByteString -> ByteString-truncpadlit n xs = if m > n then BS.take n xs-                   else BS.append xs (BS.replicate (n - m) 0)-  where m = BS.length xs--lazySlice :: W256 -> W256 -> ByteString -> LS.ByteString-lazySlice offset size bs =-  let bs' = LS.take (unsafeInto size) (LS.drop (unsafeInto offset) (fromStrict bs))-  in bs' <> LS.replicate (unsafeInto size - LS.length bs') 0--parseModexpLength :: ByteString -> (W256, W256, W256)-parseModexpLength input =-  let lenb = word $ LS.toStrict $ lazySlice  0 32 input-      lene = word $ LS.toStrict $ lazySlice 32 64 input-      lenm = word $ LS.toStrict $ lazySlice 64 96 input-  in (lenb, lene, lenm)----- checks if a range of ByteString bs starting at offset and length size is all zeros.-isZero :: W256 -> W256 -> ByteString -> Bool-isZero offset size bs =-  LS.all (== 0) $-    LS.take (unsafeInto size) $-      LS.drop (unsafeInto offset) $-        fromStrict bs--asInteger :: LS.ByteString -> Integer-asInteger xs = if xs == mempty then 0-  else 256 * asInteger (LS.init xs)-      + into (LS.last xs)---- * Opcode helper actions--noop :: Monad m => m ()-noop = pure ()--pushTo :: MonadState s m => Lens s s [a] [a] -> a -> m ()-pushTo f x = f %= (x :)--pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()-pushToSequence f x = f %= (Seq.|> x)--getCodeLocation :: VM s -> CodeLocation-getCodeLocation vm = (vm.state.contract, vm.state.pc)--query :: Query s -> EVM s ()-query = assign #result . Just . HandleEffect . Query--choose :: Choose s -> EVM s ()-choose = assign #result . Just . HandleEffect . Choose--branch :: forall s. Expr EWord -> (Bool -> EVM s ()) -> EVM s ()-branch cond continue = do-  loc <- codeloc-  pathconds <- use #constraints-  query $ PleaseAskSMT cond pathconds (choosePath loc)-  where-    condSimp = Expr.simplify cond-    choosePath :: CodeLocation -> BranchCondition -> EVM s ()-    choosePath loc (Case v) = do-      assign #result Nothing-      pushTo #constraints $ if v then Expr.simplifyProp (condSimp ./= Lit 0) else Expr.simplifyProp (condSimp .== Lit 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, stack))-      continue v-    -- Both paths are possible; we ask for more input-    choosePath loc Unknown =-      choose . PleaseChoosePath condSimp $ choosePath loc . Case---- | Construct RPC Query and halt execution until resolved-fetchAccount :: Expr EAddr -> (Contract -> EVM s ()) -> EVM s ()-fetchAccount addr continue =-  use (#env % #contracts % at addr) >>= \case-    Just c -> continue c-    Nothing -> case addr of-      SymAddr _ -> do-        pc <- use (#state % #pc)-        partial $ UnexpectedSymbolicArg pc "trying to access a symbolic address that isn't already present in storage" (wrap [addr])-      LitAddr a -> do-        use (#cache % #fetched % at a) >>= \case-          Just c -> do-            assign (#env % #contracts % at addr) (Just c)-            continue c-          Nothing -> do-            base <- use (#config % #baseState)-            assign (#result) . Just . HandleEffect . Query $-              PleaseFetchContract a base-                (\c -> do assign (#cache % #fetched % at a) (Just c)-                          assign (#env % #contracts % at addr) (Just c)-                          assign #result Nothing-                          continue c)-      GVar _ -> internalError "Unexpected GVar"--accessStorage-  :: Expr EAddr-  -> Expr EWord-  -> (Expr EWord -> EVM s ())-  -> EVM s ()-accessStorage addr slot continue = do-  use (#env % #contracts % at addr) >>= \case-    Just c ->-      case readStorage slot c.storage of-        Just x ->-          continue x-        Nothing ->-          if c.external then-            forceConcreteAddr addr "cannot read storage from symbolic addresses via rpc" $ \addr' ->-              forceConcrete slot "cannot read symbolic slots via RPC" $ \slot' -> do-                -- check if the slot is cached-                contract <- preuse (#cache % #fetched % ix addr')-                case contract of-                  Nothing -> internalError "contract marked external not found in cache"-                  Just fetched -> case readStorage (Lit slot') fetched.storage of-                              Nothing -> mkQuery addr' slot'-                              Just val -> continue val-          else do-            modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))-            continue $ Lit 0-    Nothing ->-      fetchAccount addr $ \_ ->-        accessStorage addr slot continue-  where-      mkQuery a s = query $-        PleaseFetchSlot a s-          (\x -> do-              modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x))-              modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))-              assign #result Nothing-              continue (Lit x))--accountExists :: Expr EAddr -> VM s -> Bool-accountExists addr vm =-  case Map.lookup addr vm.env.contracts of-    Just c -> not (accountEmpty c)-    Nothing -> False---- EIP 161-accountEmpty :: Contract -> Bool-accountEmpty c =-  case c.code of-    RuntimeCode (ConcreteRuntimeCode "") -> True-    RuntimeCode (SymbolicRuntimeCode b) -> null b-    _ -> False-  && c.nonce == (Just 0)-  -- TODO: handle symbolic balance...-  && c.balance == Lit 0---- * How to finalize a transaction-finalize :: EVM s ()-finalize = do-  let-    revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)-    revertSubstate   = assign (#tx % #substate) (SubState mempty mempty mempty mempty mempty)--  use #result >>= \case-    Just (VMFailure (Revert _)) -> do-      revertContracts-      revertSubstate-    Just (VMFailure _) -> do-      -- burn remaining gas-      assign (#state % #gas) 0-      revertContracts-      revertSubstate-    Just (VMSuccess output) -> do-      -- deposit the code from a creation tx-      pc' <- use (#state % #pc)-      creation <- use (#tx % #isCreate)-      createe  <- use (#state % #contract)-      createeExists <- (Map.member createe) <$> use (#env % #contracts)-      let onContractCode contractCode =-            when (creation && createeExists) $ replaceCode createe contractCode-      case output of-        ConcreteBuf bs ->-          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)-        _ ->-          case Expr.toList output of-            Nothing ->-              partial $-                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract lentgh" (wrap [output])-            Just ops ->-              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)-    _ ->-      internalError "Finalising an unfinished tx."--  -- compute and pay the refund to the caller and the-  -- corresponding payment to the miner-  block        <- use #block-  tx           <- use #tx-  gasRemaining <- use (#state % #gas)--  let-    sumRefunds   = sum (snd <$> tx.substate.refunds)-    gasUsed      = tx.gaslimit - gasRemaining-    cappedRefund = min (quot gasUsed 5) sumRefunds-    originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice-    minerPay     = tx.priorityFee * (into gasUsed)--  modifying (#env % #contracts)-     (Map.adjust (over #balance (Expr.add (Lit originPay))) tx.origin)-  modifying (#env % #contracts)-     (Map.adjust (over #balance (Expr.add (Lit minerPay))) block.coinbase)-  touchAccount block.coinbase--  -- perform state trie clearing (EIP 161), of selfdestructs-  -- and touched accounts. addresses are cleared if they have-  --    a) selfdestructed, or-  --    b) been touched and-  --    c) are empty.-  -- (see Yellow Paper "Accrued Substate")-  ---  -- remove any destructed addresses-  destroyedAddresses <- use (#tx % #substate % #selfdestructs)-  modifying (#env % #contracts)-    (Map.filterWithKey (\k _ -> (k `notElem` destroyedAddresses)))-  -- then, clear any remaining empty and touched addresses-  touchedAddresses <- use (#tx % #substate % #touchedAccounts)-  modifying (#env % #contracts)-    (Map.filterWithKey-      (\k a -> not ((k `elem` touchedAddresses) && accountEmpty a)))---- | Loads the selected contract as the current contract to execute-loadContract :: Expr EAddr -> State (VM s) ()-loadContract target =-  preuse (#env % #contracts % ix target % #code) >>=-    \case-      Nothing ->-        internalError "Call target doesn't exist"-      Just targetCode -> do-        assign (#state % #contract) target-        assign (#state % #code)     targetCode-        assign (#state % #codeContract) target--limitStack :: Int -> EVM s () -> EVM s ()-limitStack n continue = do-  stk <- use (#state % #stack)-  if length stk + n > 1024-    then vmError StackLimitExceeded-    else continue--notStatic :: EVM s () -> EVM s ()-notStatic continue = do-  bad <- use (#state % #static)-  if bad-    then vmError StateChangeWhileStatic-    else continue---- | Burn gas, failing if insufficient gas is available-burn :: Word64 -> EVM s () -> EVM s ()-burn n continue = do-  available <- use (#state % #gas)-  if n <= available-    then do-      #state % #gas %= (subtract n)-      #burned %= (+ n)-      continue-    else-      vmError (OutOfGas available n)--forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM s ()) -> EVM s ()-forceAddr n msg continue = case wordToAddr n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])-  Just c -> continue c--forceConcrete :: Expr EWord -> String -> (W256 -> EVM s ()) -> EVM s ()-forceConcrete n msg continue = case maybeLitWord n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])-  Just c -> continue c--forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM s ()) -> EVM s ()-forceConcreteAddr n msg continue = case maybeLitAddr n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])-  Just c -> continue c--forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM s ()) -> EVM s ()-forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of-  (Just c, Just d) -> continue (c,d)-  _ -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])--forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM s ()) -> EVM s ()-forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of-  (Just c, Just d) -> continue (c, d)-  _ -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])--forceConcrete3 :: (Expr EWord, Expr EWord, Expr EWord) -> String -> ((W256, W256, W256) -> EVM s ()) -> EVM s ()-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-    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 s ()) -> EVM s ()-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-    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 s ()) -> EVM s ()-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-    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 s ()) -> EVM s ()-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-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [k, l, m, n, o, p])--forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM s ()) -> EVM s ()-forceConcreteBuf (ConcreteBuf b) _ continue = continue b-forceConcreteBuf b msg _ = do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])---- * Substate manipulation-refund :: Word64 -> EVM s ()-refund n = do-  self <- use (#state % #contract)-  pushTo (#tx % #substate % #refunds) (self, n)--unRefund :: Word64 -> EVM s ()-unRefund n = do-  self <- use (#state % #contract)-  refs <- use (#tx % #substate % #refunds)-  assign (#tx % #substate % #refunds)-    (filter (\(a,b) -> not (a == self && b == n)) refs)--touchAccount :: Expr EAddr -> EVM s ()-touchAccount = pushTo ((#tx % #substate) % #touchedAccounts)--selfdestruct :: Expr EAddr -> EVM s ()-selfdestruct = pushTo ((#tx % #substate) % #selfdestructs)--accessAndBurn :: Expr EAddr -> EVM s () -> EVM s ()-accessAndBurn x cont = do-  FeeSchedule {..} <- use (#block % #schedule)-  acc <- accessAccountForGas x-  let cost = if acc then g_warm_storage_read else g_cold_account_access-  burn cost cont---- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)--- otherwise cold-accessAccountForGas :: Expr EAddr -> EVM s Bool-accessAccountForGas addr = do-  accessedAddrs <- use (#tx % #substate % #accessedAddresses)-  let accessed = member addr accessedAddrs-  assign (#tx % #substate % #accessedAddresses) (insert addr accessedAddrs)-  pure accessed---- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)--- otherwise cold-accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM s Bool-accessStorageForGas addr key = do-  accessedStrkeys <- use (#tx % #substate % #accessedStorageKeys)-  case maybeLitWord key of-    Just litword -> do-      let accessed = member (addr, litword) accessedStrkeys-      assign (#tx % #substate % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)-      pure accessed-    _ -> return False---- * Cheat codes---- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.--- Call this address using one of the cheatActions below to do--- special things, e.g. changing the block timestamp. Beware that--- these are necessarily hevm specific.-cheatCode :: Expr EAddr-cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")--cheat-  :: (?op :: Word8)-  => (W256, W256) -> (W256, W256)-  -> EVM s ()-cheat (inOffset, inSize) (outOffset, outSize) = do-  vm <- get-  input <- readMemory (Lit $ inOffset + 4) (Lit $ inSize - 4)-  abi <- readBytes 4 (Lit 0) <$> readMemory (Lit inOffset) (Lit 4)-  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input vm.env.contracts vm.tx.substate)-  case maybeLitWord abi of-    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])-    Just (unsafeInto -> abi') ->-      case Map.lookup abi' cheatActions of-        Nothing ->-          vmError (BadCheatCode abi')-        Just action -> do-            action (Lit outOffset) (Lit outSize) input-            popTrace-            next-            push 1--type CheatAction s = Expr EWord -> Expr EWord -> Expr Buf -> EVM s ()--cheatActions :: Map FunctionSelector (CheatAction s)-cheatActions =-  Map.fromList-    [ action "ffi(string[])" $-        \sig outOffset outSize input -> do-          vm <- get-          if vm.config.allowFFI then-            case decodeBuf [AbiArrayDynamicType AbiStringType] input of-              CAbi valsArr -> case valsArr of-                [AbiArrayDynamic AbiStringType strsV] ->-                  let-                    cmd = fmap-                            (\case-                              (AbiString a) -> unpack $ decodeUtf8 a-                              _ -> "")-                            (V.toList strsV)-                    cont bs = do-                      let encoded = ConcreteBuf bs-                      assign (#state % #returndata) encoded-                      copyBytesToMemory encoded outSize (Lit 0) outOffset-                      assign #result Nothing-                  in query (PleaseDoFFI cmd cont)-                _ -> vmError (BadCheatCode sig)-              _ -> vmError (BadCheatCode sig)-          else-            let msg = "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"-            in partial $ UnexpectedSymbolicArg vm.state.pc msg [],--      action "warp(uint256)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [x]  -> assign (#block % #timestamp) x-          _ -> vmError (BadCheatCode sig),--      action "deal(address,uint256)" $-        \sig _ _ input -> case decodeStaticArgs 0 2 input of-          [a, amt] ->-            forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->-              fetchAccount usr $ \_ -> do-                assign (#env % #contracts % ix usr % #balance) amt-          _ -> vmError (BadCheatCode sig),--      action "assume(bool)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [c] -> modifying #constraints ((:) (PEq c (Lit 1)))-          _ -> vmError (BadCheatCode sig),--      action "roll(uint256)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (#block % #number))-          _ -> vmError (BadCheatCode sig),--      action "store(address,bytes32,bytes32)" $-        \sig _ _ input -> case decodeStaticArgs 0 3 input of-          [a, slot, new] -> case wordToAddr a of-            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->-              modifying (#env % #contracts % ix a' % #storage) (writeStorage slot new)-            _ -> vmError (BadCheatCode sig)-          _ -> vmError (BadCheatCode sig),--      action "load(address,bytes32)" $-        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of-          [a, slot] -> case wordToAddr a of-            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->-              accessStorage a' slot $ \res -> do-                assign (#state % #returndata % word256At (Lit 0)) res-                let buf = writeWord (Lit 0) res (ConcreteBuf "")-                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset-            _ -> vmError (BadCheatCode sig)-          _ -> vmError (BadCheatCode sig),--      action "sign(uint256,bytes32)" $-        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of-          [sk, hash] ->-            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do-              let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')-                  encoded = encodeAbiValue $-                    AbiTuple (V.fromList-                      [ AbiUInt 8 $ into v-                      , AbiBytes 32 (word256Bytes r)-                      , AbiBytes 32 (word256Bytes s)-                      ])-              assign (#state % #returndata) (ConcreteBuf encoded)-              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset-          _ -> vmError (BadCheatCode sig),--      action "addr(uint256)" $-        \sig outOffset _ input -> case decodeStaticArgs 0 1 input of-          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do-            let a = EVM.Sign.deriveAddr $ into sk'-            case a of-              Nothing -> vmError (BadCheatCode sig)-              Just address -> do-                let expAddr = litAddr address-                assign (#state % #returndata % word256At (Lit 0)) expAddr-                let buf = ConcreteBuf $ word256Bytes (into address)-                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset-          _ -> vmError (BadCheatCode sig),--      action "prank(address)" $-        \sig _ _ input -> case decodeStaticArgs 0 1 input of-          [addr]  -> case wordToAddr addr of-            Just a -> assign (#config % #overrideCaller) (Just a)-            Nothing -> vmError (BadCheatCode sig)-          _ -> vmError (BadCheatCode sig)--    ]-  where-    action s f = (abiKeccak s, f (abiKeccak s))---- * General call implementation ("delegateCall")--- note that the continuation is ignored in the precompile case-delegateCall-  :: (?op :: Word8)-  => Contract -> Word64 -> Expr EAddr -> Expr EAddr -> Expr EWord -> W256 -> W256 -> W256 -> W256-  -> [Expr EWord]-  -> (Expr EAddr -> EVM s ())-  -> EVM s ()-delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue-  | isPrecompileAddr xTo-      = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $-          \(xTo', xContext') ->-            precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs-  | xTo == cheatCode = do-      assign (#state % #stack) xs-      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-  | otherwise =-      callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $-        \xGas -> do-          vm0 <- get-          fetchAccount xTo $ \target -> case target.code of-              UnknownCode _ -> do-                pc <- use (#state % #pc)-                partial $ UnexpectedSymbolicArg pc "call target has unknown code" (wrap [xTo])-              _ -> do-                burn xGas $ do-                  calldata <- readMemory (Lit xInOffset) (Lit xInSize)-                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory (Lit xInOffset) (Lit 4)-                  let newContext = CallContext-                                    { target    = xTo-                                    , context   = xContext-                                    , offset    = xOutOffset-                                    , size      = xOutSize-                                    , codehash  = target.codehash-                                    , callreversion = vm0.env.contracts-                                    , subState  = vm0.tx.substate-                                    , abi-                                    , calldata-                                    }-                  pushTrace (FrameTrace newContext)-                  next-                  vm1 <- get--                  pushTo #frames $ Frame-                    { state = vm1.state { stack = xs }-                    , context = newContext-                    }--                  let clearInitCode = \case-                        (InitCode _ _) -> InitCode mempty mempty-                        a -> a--                  newMemory <- ConcreteMemory <$> VUnboxed.Mutable.new 0-                  zoom #state $ do-                    assign #gas xGas-                    assign #pc 0-                    assign #code (clearInitCode target.code)-                    assign #codeContract xTo-                    assign #stack mempty-                    assign #memory newMemory-                    assign #memorySize 0-                    assign #returndata mempty-                    assign #calldata calldata-                  continue xTo---- -- * Contract creation---- EIP 684-collision :: Maybe Contract -> Bool-collision c' = case c' of-  Just c -> c.nonce /= Just 0 || case c.code of-    RuntimeCode (ConcreteRuntimeCode "") -> False-    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b-    _ -> True-  Nothing -> False--create :: (?op :: Word8)-  => Expr EAddr -> Contract-  -> W256 -> Word64 -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM s ()-create self this xSize xGas xValue xs newAddr initCode = do-  vm0 <- get-  if xSize > vm0.block.maxCodeSize * 2-  then do-    assign (#state % #stack) (Lit 0 : xs)-    assign (#state % #returndata) mempty-    vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize-  else if this.nonce == Just maxBound-  then do-    assign (#state % #stack) (Lit 0 : xs)-    assign (#state % #returndata) mempty-    pushTrace $ ErrorTrace NonceOverflow-    next-  else if length vm0.frames >= 1024-  then do-    assign (#state % #stack) (Lit 0 : xs)-    assign (#state % #returndata) mempty-    pushTrace $ ErrorTrace CallDepthLimitReached-    next-  else if collision $ Map.lookup newAddr vm0.env.contracts-  then burn xGas $ do-    assign (#state % #stack) (Lit 0 : xs)-    assign (#state % #returndata) mempty-    modifying (#env % #contracts % ix self % #nonce) (fmap ((+) 1))-    next-  -- do we have enough balance-  else branch (Expr.gt xValue this.balance) $ \case-      True -> do-        assign (#state % #stack) (Lit 0 : xs)-        assign (#state % #returndata) mempty-        pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance-        next-        touchAccount self-        touchAccount newAddr-      -- are we overflowing the nonce-      False -> burn xGas $ do-        case parseInitCode initCode of-          Nothing ->-            partial $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []-          Just c -> do-            let-              newContract = initialContract c-              newContext  =-                CreationContext { address   = newAddr-                                , codehash  = newContract.codehash-                                , createreversion = vm0.env.contracts-                                , substate  = vm0.tx.substate-                                }--            zoom (#env % #contracts) $ do-              oldAcc <- use (at newAddr)-              let oldBal = maybe (Lit 0) (.balance) oldAcc--              assign (at newAddr) (Just (newContract & #balance .~ oldBal))-              modifying (ix self % #nonce) (fmap ((+) 1))--            let-              resetStorage :: Expr Storage -> Expr Storage-              resetStorage = \case-                  ConcreteStore _ -> ConcreteStore mempty-                  AbstractStore a -> AbstractStore a-                  SStore _ _ p -> resetStorage p-                  GVar _  -> error "unexpected global variable"--            modifying (#env % #contracts % ix newAddr % #storage) resetStorage-            modifying (#env % #contracts % ix newAddr % #origStorage) resetStorage--            transfer self newAddr xValue--            pushTrace (FrameTrace newContext)-            next-            vm1 <- get-            pushTo #frames $ Frame-              { context = newContext-              , state   = vm1.state { stack = xs }-              }--            state <- lift blankState-            assign #state $ state-              { contract     = newAddr-              , codeContract = newAddr-              , code         = c-              , callvalue    = xValue-              , caller       = self-              , gas          = xGas-              }---- | Parses a raw Buf into an InitCode------ solidity implements constructor args by appending them to the end of--- the initcode. we support this internally by treating initCode as a--- concrete region (initCode) followed by a potentially symbolic region--- (arguments).------ when constructing a contract that has symbolic construcor args, we--- need to apply some heuristics to convert the (unstructured) initcode--- in memory into this structured representation. The (unsound, bad,--- hacky) way that we do this, is by: looking for the first potentially--- symbolic byte in the input buffer and then splitting it there into code / data.-parseInitCode :: Expr Buf -> Maybe ContractCode-parseInitCode (ConcreteBuf b) = Just (InitCode b mempty)-parseInitCode buf = if V.null conc-                    then Nothing-                    else Just $ InitCode (BS.pack $ V.toList conc) sym-  where-    conc = Expr.concretePrefix buf-    -- unsafeInto: findIndex will always be positive-    sym = Expr.drop (unsafeInto (V.length conc)) buf---- | Replace a contract's code, like when CREATE returns--- from the constructor code.-replaceCode :: Expr EAddr -> ContractCode -> EVM s ()-replaceCode target newCode =-  zoom (#env % #contracts % at target) $-    get >>= \case-      Just now -> case now.code of-        InitCode _ _ ->-          put . Just $-            ((initialContract newCode) :: Contract)-              { balance = now.balance-              , nonce = now.nonce-              , storage = now.storage-              }-        RuntimeCode _ ->-          internalError $ "Can't replace code of deployed contract " <> show target-        UnknownCode _ ->-          internalError "Can't replace unknown code"-      Nothing ->-        internalError "Can't replace code of nonexistent contract"--replaceCodeOfSelf :: ContractCode -> EVM s ()-replaceCodeOfSelf newCode = do-  vm <- get-  replaceCode vm.state.contract newCode--resetState :: EVM s ()-resetState = do-  state <- lift blankState-  modify' $ \vm -> vm { result = Nothing, frames = [], state }---- * VM error implementation--vmError :: EvmError -> EVM s ()-vmError e = finishFrame (FrameErrored e)--partial :: PartialExec -> EVM s ()-partial e = assign #result (Just (Unfinished e))--wrap :: Typeable a => [Expr a] -> [SomeExpr]-wrap = fmap SomeExpr--underrun :: EVM s ()-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 EvmError -- ^ Any other error-  deriving Show---- | This function defines how to pop the current stack frame in either of--- the ways specified by 'FrameResult'.------ It also handles the case when the current stack frame is the only one;--- in this case, we set the final '_result' of the VM execution.-finishFrame :: FrameResult -> EVM s ()-finishFrame how = do-  oldVm <- get--  case oldVm.frames of-    -- Is the current frame the only one?-    [] -> do-      case how of-          FrameReturned output -> assign #result . Just $ VMSuccess output-          FrameReverted buffer -> assign #result . Just $ VMFailure (Revert buffer)-          FrameErrored e       -> assign #result . Just $ VMFailure e-      finalize--    -- Are there some remaining frames?-    nextFrame : remainingFrames -> do--      -- Insert a debug trace.-      insertTrace $-        case how of-          FrameErrored e ->-            ErrorTrace e-          FrameReverted e ->-            ErrorTrace (Revert e)-          FrameReturned output ->-            ReturnTrace output nextFrame.context-      -- Pop to the previous level of the debug trace stack.-      popTrace--      -- Pop the top frame.-      assign #frames remainingFrames-      -- Install the state of the frame to which we shall return.-      assign #state nextFrame.state--      -- When entering a call, the gas allowance is counted as burned-      -- in advance; this unburns the remainder and adds it to the-      -- parent frame.-      let remainingGas = oldVm.state.gas-          reclaimRemainingGasAllowance = do-            modifying #burned (subtract remainingGas)-            modifying (#state % #gas) (+ remainingGas)--      -- Now dispatch on whether we were creating or calling,-      -- and whether we shall return, revert, or internalError(six cases).-      case nextFrame.context of--        -- Were we calling?-        CallContext _ _ (Lit -> outOffset) (Lit -> outSize) _ _ _ reversion substate' -> do--          -- Excerpt K.1. from the yellow paper:-          -- K.1. Deletion of an Account Despite Out-of-gas.-          -- At block 2675119, in the transaction 0xcf416c536ec1a19ed1fb89e4ec7ffb3cf73aa413b3aa9b77d60e4fd81a4296ba,-          -- an account at address 0x03 was called and an out-of-gas occurred during the call.-          -- Against the equation (197), this added 0x03 in the set of touched addresses, and this transaction turned σ[0x03] into ∅.--          -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert-          touched <- use (#tx % #substate % #touchedAccounts)--          let-            substate'' = over #touchedAccounts (maybe id cons (find (LitAddr 3 ==) touched)) substate'-            revertContracts = assign (#env % #contracts) reversion-            revertSubstate  = assign (#tx % #substate) substate''--          case how of-            -- Case 1: Returning from a call?-            FrameReturned output -> do-              assign (#state % #returndata) output-              copyCallBytesToMemory output outSize outOffset-              reclaimRemainingGasAllowance-              push 1--            -- Case 2: Reverting during a call?-            FrameReverted output -> do-              revertContracts-              revertSubstate-              assign (#state % #returndata) output-              copyCallBytesToMemory output outSize outOffset-              reclaimRemainingGasAllowance-              push 0--            -- Case 3: Error during a call?-            FrameErrored _ -> do-              revertContracts-              revertSubstate-              assign (#state % #returndata) mempty-              push 0-        -- Or were we creating?-        CreationContext _ _ reversion substate' -> do-          creator <- use (#state % #contract)-          let-            createe = oldVm.state.contract-            revertContracts = assign (#env % #contracts) reversion'-            revertSubstate  = assign (#tx % #substate) substate'--            -- persist the nonce through the reversion-            reversion' = (Map.adjust (over #nonce (fmap ((+) 1))) creator) reversion--          case how of-            -- Case 4: Returning during a creation?-            FrameReturned output -> do-              let onContractCode contractCode = do-                    replaceCode createe contractCode-                    assign (#state % #returndata) mempty-                    reclaimRemainingGasAllowance-                    pushAddr createe-              case output of-                ConcreteBuf bs ->-                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)-                _ ->-                  case Expr.toList output of-                    Nothing -> partial $-                      UnexpectedSymbolicArg-                        oldVm.state.pc-                        "runtime code cannot have an abstract length"-                        (wrap [output])-                    Just newCode -> do-                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)--            -- Case 5: Reverting during a creation?-            FrameReverted output -> do-              revertContracts-              revertSubstate-              assign (#state % #returndata) output-              reclaimRemainingGasAllowance-              push 0--            -- Case 6: Error during a creation?-            FrameErrored _ -> do-              revertContracts-              revertSubstate-              assign (#state % #returndata) mempty-              push 0----- * Memory helpers--accessUnboundedMemoryRange-  :: Word64-  -> Word64-  -> EVM s ()-  -> EVM s ()-accessUnboundedMemoryRange _ 0 continue = continue-accessUnboundedMemoryRange f l continue = do-  m0 <- use (#state % #memorySize)-  fees <- gets (.block.schedule)-  let m1 = 32 * ceilDiv (max m0 (f + l)) 32-  burn (memoryCost fees m1 - memoryCost fees m0) $ do-    assign (#state % #memorySize) m1-    continue--accessMemoryRange-  :: W256-  -> W256-  -> EVM s ()-  -> EVM s ()-accessMemoryRange _ 0 continue = continue-accessMemoryRange offs sz continue =-  case (,) <$> toWord64 offs <*> toWord64 sz of-    Nothing -> vmError IllegalOverflow-    Just (offs64, sz64) ->-      if offs64 + sz64 < sz64-        then vmError IllegalOverflow-        else accessUnboundedMemoryRange offs64 sz64 continue--accessMemoryWord-  :: W256 -> EVM s () -> EVM s ()-accessMemoryWord x = accessMemoryRange x 32--copyBytesToMemory-  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM s ()-copyBytesToMemory bs size srcOffset memOffset =-  if size == Lit 0 then noop-  else do-    gets (.state.memory) >>= \case-      ConcreteMemory mem ->-        case (bs, size, srcOffset, memOffset) of-          (ConcreteBuf b, Lit size', Lit srcOffset', Lit memOffset') -> do-            let src =-                  if srcOffset' >= unsafeInto (BS.length b) then-                    BS.replicate (unsafeInto size') 0-                  else-                    BS.take (unsafeInto size') $-                    padRight (unsafeInto size') $-                    BS.drop (unsafeInto srcOffset') b--            writeMemory mem (unsafeInto memOffset') src-          _ -> do-            -- copy out and move to symbolic memory-            buf <- freezeMemory mem-            assign (#state % #memory) $-              SymbolicMemory $ copySlice srcOffset memOffset size bs buf-      SymbolicMemory mem ->-        assign (#state % #memory) $-          SymbolicMemory $ copySlice srcOffset memOffset size bs mem--copyCallBytesToMemory-  :: Expr Buf -> Expr EWord -> Expr EWord -> EVM s ()-copyCallBytesToMemory bs size yOffset =-  copyBytesToMemory bs (Expr.min size (bufLength bs)) (Lit 0) yOffset--readMemory :: Expr EWord -> Expr EWord -> EVM s (Expr Buf)-readMemory offset' size' = do-  vm <- get-  case vm.state.memory of-    ConcreteMemory mem -> do-      case (offset', size') of-        (Lit offset, Lit size) -> do-          let memSize :: Word64 = unsafeInto (VUnboxed.Mutable.length mem)-          if size > Expr.maxBytes ||-             offset + size > Expr.maxBytes ||-             offset >= into memSize then-            -- reads past memory are all zeros-            pure $ ConcreteBuf $ BS.replicate (unsafeInto size) 0-          else do-            let pastEnd = (unsafeInto offset + unsafeInto size) - unsafeInto memSize-            let fromMemSize = if pastEnd > 0 then unsafeInto size - pastEnd else unsafeInto size--            buf <- VUnboxed.freeze $ VUnboxed.Mutable.slice (unsafeInto offset) fromMemSize mem-            let dataFromMem = BS.pack $ VUnboxed.toList buf-            pure $ ConcreteBuf $ dataFromMem <> BS.replicate pastEnd 0-        _ -> do-          buf <- freezeMemory mem-          pure $ copySlice offset' (Lit 0) size' buf mempty-    SymbolicMemory mem ->-      pure $ copySlice offset' (Lit 0) size' mem mempty---- * Tracing--withTraceLocation :: TraceData -> EVM s Trace-withTraceLocation x = do-  vm <- get-  let this = fromJust $ currentContract vm-  pure Trace-    { tracedata = x-    , contract = this-    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc-    }--pushTrace :: TraceData -> EVM s ()-pushTrace x = do-  trace <- withTraceLocation x-  modifying #traces $-    \t -> Zipper.children $ Zipper.insert (Node trace []) t--insertTrace :: TraceData -> EVM s ()-insertTrace x = do-  trace <- withTraceLocation x-  modifying #traces $-    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t--popTrace :: EVM s ()-popTrace =-  modifying #traces $-    \t -> case Zipper.parent t of-            Nothing -> internalError "internal internalError(trace root)"-            Just t' -> Zipper.nextSpace t'--zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a-zipperRootForest z =-  case Zipper.parent z of-    Nothing -> Zipper.toForest z-    Just z' -> zipperRootForest (Zipper.nextSpace z')--traceForest :: VM s -> Forest Trace-traceForest vm = zipperRootForest vm.traces--traceForest' :: Expr End -> Forest Trace-traceForest' (Success _ (Traces f _) _ _) = f-traceForest' (Partial _ (Traces f _) _) = f-traceForest' (Failure _ (Traces f _) _) = f-traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"-traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"--traceContext :: Expr End -> Map (Expr EAddr) Contract-traceContext (Success _ (Traces _ c) _ _) = c-traceContext (Partial _ (Traces _ c) _) = c-traceContext (Failure _ (Traces _ c) _) = c-traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"-traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"--traceTopLog :: [Expr Log] -> EVM s ()-traceTopLog [] = noop-traceTopLog ((LogEntry addr bytes topics) : _) = do-  trace <- withTraceLocation (EventTrace addr bytes topics)-  modifying #traces $-    \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)-traceTopLog ((GVar _) : _) = internalError "unexpected global variable"---- * Stack manipulation--push :: W256 -> EVM s ()-push = pushSym . Lit--pushSym :: Expr EWord -> EVM s ()-pushSym x = #state % #stack %= (x :)--pushAddr :: Expr EAddr -> EVM s ()-pushAddr (LitAddr x) = #state % #stack %= (Lit (into x) :)-pushAddr x@(SymAddr _) = #state % #stack %= (WAddr x :)-pushAddr (GVar _) = internalError "Unexpected GVar"--stackOp1-  :: (?op :: Word8)-  => Word64-  -> (Expr EWord -> Expr EWord)-  -> EVM s ()-stackOp1 cost f =-  use (#state % #stack) >>= \case-    x:xs ->-      burn cost $ do-        next-        let !y = f x-        #state % #stack .= y : xs-    _ ->-      underrun--stackOp2-  :: (?op :: Word8)-  => Word64-  -> (Expr EWord -> Expr EWord -> Expr EWord)-  -> EVM s ()-stackOp2 cost f =-  use (#state % #stack) >>= \case-    x:y:xs ->-      burn cost $ do-        next-        #state % #stack .= f x y : xs-    _ ->-      underrun--stackOp3-  :: (?op :: Word8)-  => Word64-  -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)-  -> EVM s ()-stackOp3 cost f =-  use (#state % #stack) >>= \case-    x:y:z:xs ->-      burn cost $ do-      next-      (#state % #stack) .= f x y z : xs-    _ ->-      underrun---- * Bytecode data functions--use' :: (VM s -> a) -> EVM s a-use' f = do-  vm <- get-  pure (f vm)--checkJump :: Int -> [Expr EWord] -> EVM s ()-checkJump x xs = noJumpIntoInitData x $ do-  vm <- get-  case isValidJumpDest vm x of-    True -> do-      #state % #stack .= xs-      #state % #pc .= x-    False -> vmError BadJumpDestination---- fails with partial if we're trying to jump into the symbolic region of an `InitCode`-noJumpIntoInitData :: Int -> EVM s () -> EVM s ()-noJumpIntoInitData idx cont = do-  vm <- get-  case vm.state.code of-    -- init code is totally concrete, so we don't return partial if we're-    -- jumping beyond the range of `ops`-    InitCode _ (ConcreteBuf "") -> cont-    -- init code has a symbolic region, so check if we're trying to jump into-    -- the symbolic region and return partial if we are-    InitCode ops _ -> if idx > BS.length ops-                      then partial $ JumpIntoSymbolicCode vm.state.pc idx-                      else cont-    -- we're not executing init code, so nothing to check here-    _ -> cont--isValidJumpDest :: VM s -> Int -> Bool-isValidJumpDest vm x = let-    code = vm.state.code-    self = vm.state.codeContract-    contract = fromMaybe-      (internalError "self not found in current contracts")-      (Map.lookup self vm.env.contracts)-    op = case code of-      UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"-      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.! x))--opSize :: Word8 -> Int-opSize x | x >= 0x60 && x <= 0x7f = into x - 0x60 + 2-opSize _                          = 1----  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 -> SV.Vector Int-mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code"-mkOpIxMap (InitCode conc _)-  = 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-      in m >> pure v-      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 >> SV.write v i j)-        go v (1, !i, !j, !m) _ =-          {- 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 >> SV.write v i j)-        go v (n, !i, !j, !m) _ =-          {- 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))-  = 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 maybeLitByte x of-          Just x' -> if x' >= 0x60 && x' <= 0x7f-            -- start of PUSH op ---                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)-            -- other data ---                     else (0,             i + 1, j + 1, m >> SV.write v i j)-          _ -> internalError $ "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 >> SV.write v i j)-        go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)---vmOp :: VM s -> Maybe Op-vmOp vm =-  let i  = vm ^. #state % #pc-      code' = vm ^. #state % #code-      (op, pushdata) = case code' of-        UnknownCode _ -> internalError "cannot get op from unknown code"-        InitCode xs' _ ->-          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')-        RuntimeCode (ConcreteRuntimeCode xs') ->-          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')-        RuntimeCode (SymbolicRuntimeCode xs') ->-          ( fromMaybe (internalError "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)--vmOpIx :: VM s -> Maybe Int-vmOpIx vm =-  do self <- currentContract vm-     self.opIxMap SV.!? vm.state.pc---- Maps operation indicies into a pair of (bytecode index, operation)-mkCodeOps :: ContractCode -> V.Vector (Int, Op)-mkCodeOps contractCode =-  let l = case contractCode of-            UnknownCode _ -> internalError "Cannot make codeOps for unknown code"-            InitCode bytes _ ->-              LitByte <$> (BS.unpack bytes)-            RuntimeCode (ConcreteRuntimeCode ops) ->-              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)-            RuntimeCode (SymbolicRuntimeCode ops) ->-              stripBytecodeMetadataSym $ V.toList ops-  in V.fromList . toList $ go 0 l-  where-    go !i !xs =-      case uncons xs of-        Nothing ->-          mempty-        Just (x, xs') ->-          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x-              j = opSize x'-          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)---- * Gas cost calculation helpers---- Gas cost function for CALL, transliterated from the Yellow Paper.-costOfCall-  :: FeeSchedule Word64-  -> Bool -> Expr EWord -> Word64 -> Word64 -> Expr EAddr-  -> EVM s (Word64, Word64)-costOfCall (FeeSchedule {..}) recipientExists (Lit xValue) availableGas xGas target = do-  acc <- accessAccountForGas target-  let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access-      c_new = if not recipientExists && xValue /= 0-            then g_newaccount-            else 0-      c_xfer = if xValue /= 0  then g_callvalue else 0-      c_extra = call_base_gas + c_xfer + c_new-      c_gascap =  if availableGas >= c_extra-                  then min xGas (allButOne64th (availableGas - c_extra))-                  else xGas-      c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap-  pure (c_gascap + c_extra, c_callgas)--- calls are free if value is symbolic :)-costOfCall _ _ _ _ _ _ = pure (0,0)---- Gas cost of create, including hash cost if needed-costOfCreate-  :: FeeSchedule Word64-  -> Word64 -> W256 -> Bool -> (Word64, Word64)-costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)-  where-    byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword-    createCost = g_create + codeCost-    codeCost   = byteCost * (ceilDiv (unsafeInto size) 32)-    initGas    = allButOne64th (availableGas - createCost)--concreteModexpGasFee :: ByteString -> Word64-concreteModexpGasFee input =-  if lenb < into (maxBound :: Word32) &&-     (lene < into (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&-     lenm < into (maxBound :: Word64)-  then-    max 200 ((multiplicationComplexity * iterCount) `div` 3)-  else-    maxBound -- TODO: this is not 100% correct, return Nothing on overflow-  where-    (lenb, lene, lenm) = parseModexpLength input-    ez = isZero (96 + lenb) lene input-    e' = word $ LS.toStrict $-      lazySlice (96 + lenb) (min 32 lene) input-    nwords :: Word64-    nwords = ceilDiv (unsafeInto $ max lenb lenm) 8-    multiplicationComplexity = nwords * nwords-    iterCount' :: Word64-    iterCount' | lene <= 32 && ez = 0-               | lene <= 32 = unsafeInto (log2 e')-               | e' == 0 = 8 * (unsafeInto lene - 32)-               | otherwise = unsafeInto (log2 e') + 8 * (unsafeInto lene - 32)-    iterCount = max iterCount' 1---- Gas cost of precompiles-costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64-costOfPrecompile (FeeSchedule {..}) precompileAddr input =-  let errorDynamicSize = internalError "precompile input cannot have a dynamic size"-      inputLen = case input of-                   ConcreteBuf bs -> unsafeInto $ BS.length bs-                   AbstractBuf _ -> errorDynamicSize-                   buf -> case bufLength buf of-                            Lit l -> unsafeInto l -- TODO: overflow-                            _ -> errorDynamicSize-  in case precompileAddr of-    -- ECRECOVER-    0x1 -> 3000-    -- SHA2-256-    0x2 -> (((inputLen + 31) `div` 32) * 12) + 60-    -- RIPEMD-160-    0x3 -> (((inputLen + 31) `div` 32) * 120) + 600-    -- IDENTITY-    0x4 -> (((inputLen + 31) `div` 32) * 3) + 15-    -- MODEXP-    0x5 -> case input of-             ConcreteBuf i -> concreteModexpGasFee i-             _ -> internalError "Unsupported symbolic modexp gas calc "-    -- ECADD-    0x6 -> g_ecadd-    -- ECMUL-    0x7 -> g_ecmul-    -- ECPAIRING-    0x8 -> (inputLen `div` 192) * g_pairing_point + g_pairing_base-    -- BLAKE2-    0x9 -> case input of-             ConcreteBuf i -> g_fround * (unsafeInto $ asInteger $ lazySlice 0 4 i)-             _ -> internalError "Unsupported symbolic blake2 gas calc"-    _ -> internalError $ "unimplemented precompiled contract " ++ show precompileAddr---- Gas cost of memory expansion-memoryCost :: FeeSchedule Word64 -> Word64 -> Word64-memoryCost FeeSchedule{..} byteCount =-  let-    wordCount = ceilDiv byteCount 32-    linearCost = g_memory * wordCount-    quadraticCost = div (wordCount * wordCount) 512-  in-    linearCost + quadraticCost--hashcode :: ContractCode -> Expr EWord-hashcode (UnknownCode a) = CodeHash a-hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args-hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)-hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops---- | The length of the code ignoring any constructor args.--- This represents the region that can contain executable opcodes-opslen :: ContractCode -> Int-opslen (UnknownCode _) = internalError "Cannot produce concrete opslen for unknown code"-opslen (InitCode ops _) = BS.length ops-opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops-opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops---- | The length of the code including any constructor args.--- This can return an abstract value-codelen :: ContractCode -> Expr EWord-codelen (UnknownCode a) = CodeSize a-codelen c@(InitCode {}) = case toBuf c of-  Just b -> bufLength b-  Nothing -> internalError "impossible"--- these are never going to be negative so unsafeInto is fine here-codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . unsafeInto $ BS.length ops-codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . unsafeInto $ length ops--toBuf :: ContractCode -> Maybe (Expr Buf)-toBuf (UnknownCode _) = Nothing-toBuf (InitCode ops args) = Just $ ConcreteBuf ops <> args-toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = Just $ ConcreteBuf ops-toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops--codeloc :: EVM s CodeLocation-codeloc = do-  vm <- get-  pure (vm.state.contract, vm.state.pc)--createAddress :: Expr EAddr -> Maybe W64 -> EVM s (Expr EAddr)-createAddress (LitAddr a) (Just n) = pure $ Concrete.createAddress a n-createAddress (GVar _) _ = internalError "Unexpected GVar"-createAddress _ _ = freshSymAddr--create2Address :: Expr EAddr -> W256 -> ByteString -> EVM s (Expr EAddr)-create2Address (LitAddr a) s b = pure $ Concrete.create2Address a s b-create2Address (SymAddr _) _ _ = freshSymAddr-create2Address (GVar _) _ _ = internalError "Unexpected GVar"--freshSymAddr :: EVM s (Expr EAddr)-freshSymAddr = do-  modifying (#env % #freshAddresses) (+ 1)-  n <- use (#env % #freshAddresses)-  pure $ SymAddr ("freshSymAddr" <> (pack $ show n))--isPrecompileAddr :: Expr EAddr -> Bool-isPrecompileAddr = \case-  LitAddr a -> 0x0 < a && a <= 0x09-  SymAddr _ -> False-  GVar _ -> internalError "Unexpected GVar"---- * Arithmetic--ceilDiv :: (Num a, Integral a) => a -> a -> a-ceilDiv m n = div (m + n - 1) n--allButOne64th :: (Num a, Integral a) => a -> a-allButOne64th n = n - div n 64--log2 :: FiniteBits b => b -> Int-log2 x = finiteBitSize x - 1 - countLeadingZeros x--writeMemory :: MutableMemory s -> Int -> ByteString -> EVM s ()-writeMemory memory offset buf = do-  memory' <- expandMemory (offset + BS.length buf)-  mapM_ (uncurry (VUnboxed.Mutable.write memory'))-        (zip [offset..] (BS.unpack buf))-  where-  expandMemory targetSize = do-    let toAlloc = targetSize - VUnboxed.Mutable.length memory-    if toAlloc > 0 then do-      memory' <- VUnboxed.Mutable.grow memory toAlloc-      assign (#state % #memory) (ConcreteMemory memory')-      pure memory'-    else-      pure memory--freezeMemory :: MutableMemory s -> EVM s (Expr Buf)-freezeMemory memory =-  ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.freeze memory+import EVM.Types qualified as Expr (Expr(Gas))+import EVM.Sign qualified+import EVM.Concrete qualified as Concrete++import Control.Monad.ST (ST)+import Control.Monad.State.Strict hiding (state)+import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)+import Data.ByteArray qualified as BA+import Data.ByteString (ByteString)+import Data.ByteString qualified as BS+import Data.ByteString.Lazy (fromStrict)+import Data.ByteString.Lazy qualified as LS+import Data.ByteString.Char8 qualified as Char8+import Data.Foldable (toList)+import Data.List (find)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (fromMaybe, fromJust, isJust)+import Data.Set (insert, member, fromList)+import Data.Sequence (Seq)+import Data.Sequence qualified as Seq+import Data.Text (unpack, pack)+import Data.Text.Encoding (decodeUtf8)+import Data.Tree+import Data.Tree.Zipper qualified as Zipper+import Data.Typeable+import Data.Vector qualified as V+import Data.Vector.Storable qualified as SV+import Data.Vector.Storable.Mutable qualified as SV+import Data.Vector.Unboxed qualified as VUnboxed+import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable+import Data.Word (Word8, Word32, Word64)+import Witch (into, tryFrom, unsafeInto)++import Crypto.Hash (Digest, SHA256, RIPEMD160)+import Crypto.Hash qualified as Crypto+import Crypto.Number.ModArithmetic (expFast)++blankState :: VMOps t => ST s (FrameState t s)+blankState = do+  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  pure $ FrameState+    { contract     = LitAddr 0+    , codeContract = LitAddr 0+    , code         = RuntimeCode (ConcreteRuntimeCode "")+    , pc           = 0+    , stack        = mempty+    , memory+    , memorySize   = 0+    , calldata     = mempty+    , callvalue    = Lit 0+    , caller       = LitAddr 0+    , gas          = initialGas+    , returndata   = mempty+    , static       = False+    }++-- | An "external" view of a contract's bytecode, appropriate for+-- e.g. @EXTCODEHASH@.+bytecode :: Getter Contract (Maybe (Expr Buf))+bytecode = #code % to f+  where f (InitCode _ _) = Just mempty+        f (RuntimeCode (ConcreteRuntimeCode bs)) = Just $ ConcreteBuf bs+        f (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops+        f (UnknownCode _) = Nothing++-- * Data accessors++currentContract :: VM t s -> Maybe Contract+currentContract vm =+  Map.lookup vm.state.codeContract vm.env.contracts++-- * Data constructors++makeVm :: VMOps t => VMOpts t -> ST s (VM t s)+makeVm o = do+  let txaccessList = o.txAccessList+      txorigin = o.origin+      txtoAddr = o.address+      initialAccessedAddrs = fromList $+           [txorigin, txtoAddr, o.coinbase]+        ++ (fmap LitAddr [1..9])+        ++ (Map.keys txaccessList)+      initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)+      touched = if o.create then [txorigin] else [txorigin, txtoAddr]+  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  pure $ VM+    { result = Nothing+    , frames = mempty+    , tx = TxState+      { gasprice = o.gasprice+      , gaslimit = o.gaslimit+      , priorityFee = o.priorityFee+      , origin = txorigin+      , toAddr = txtoAddr+      , value = o.value+      , substate = SubState mempty touched initialAccessedAddrs initialAccessedStorageKeys mempty+      , isCreate = o.create+      , txReversion = Map.fromList ((o.address,o.contract):o.otherContracts)+      }+    , logs = []+    , traces = Zipper.fromForest []+    , block = block+    , state = FrameState+      { pc = 0+      , stack = mempty+      , memory+      , memorySize = 0+      , code = o.contract.code+      , contract = o.address+      , codeContract = o.address+      , calldata = fst o.calldata+      , callvalue = o.value+      , caller = o.caller+      , gas = o.gas+      , returndata = mempty+      , static = False+      }+    , env = env+    , cache = cache+    , burned = initialGas+    , constraints = snd o.calldata+    , iterations = mempty+    , config = RuntimeConfig+      { allowFFI = o.allowFFI+      , overrideCaller = Nothing+      , baseState = o.baseState+      }+    , forks = Seq.singleton (ForkState env block cache "")+    , currentFork = 0+    }+    where+    env = Env+      { chainId = o.chainId+      , contracts = Map.fromList ((o.address,o.contract):o.otherContracts)+      , freshAddresses = 0+      , freshGasVals = 0+      }+    block = Block+      { coinbase = o.coinbase+      , timestamp = o.timestamp+      , number = o.number+      , prevRandao = o.prevRandao+      , maxCodeSize = o.maxCodeSize+      , gaslimit = o.blockGaslimit+      , baseFee = o.baseFee+      , schedule = o.schedule+      }+    cache = Cache mempty mempty++-- | Initialize an abstract contract with unknown code+unknownContract :: Expr EAddr -> Contract+unknownContract addr = Contract+  { code        = UnknownCode addr+  , storage     = AbstractStore addr Nothing+  , origStorage = AbstractStore addr Nothing+  , balance     = Balance addr+  , nonce       = Nothing+  , codehash    = hashcode (UnknownCode addr)+  , opIxMap     = mempty+  , codeOps     = mempty+  , external    = False+  }++-- | Initialize an abstract contract with known code+abstractContract :: ContractCode -> Expr EAddr -> Contract+abstractContract code addr = Contract+  { code        = code+  , storage     = AbstractStore addr Nothing+  , origStorage = AbstractStore addr Nothing+  , balance     = Balance addr+  , nonce       = if isCreation code then Just 1 else Just 0+  , codehash    = hashcode code+  , opIxMap     = mkOpIxMap code+  , codeOps     = mkCodeOps code+  , external    = False+  }++-- | Initialize an empty contract without code+emptyContract :: Contract+emptyContract = initialContract (RuntimeCode (ConcreteRuntimeCode ""))++-- | Initialize empty contract with given code+initialContract :: ContractCode -> Contract+initialContract code = Contract+  { code        = code+  , storage     = ConcreteStore mempty+  , origStorage = ConcreteStore mempty+  , balance     = Lit 0+  , nonce       = if isCreation code then Just 1 else Just 0+  , codehash    = hashcode code+  , opIxMap     = mkOpIxMap code+  , codeOps     = mkCodeOps code+  , external    = False+  }++isCreation :: ContractCode -> Bool+isCreation = \case+  InitCode _ _  -> True+  RuntimeCode _ -> False+  UnknownCode _ -> False++-- * Opcode dispatch (exec1)++-- | Update program counter+next :: (?op :: Word8) => EVM t s ()+next = modifying (#state % #pc) (+ (opSize ?op))++-- | Executes the EVM one step+exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()+exec1 = do+  vm <- get++  let+    -- Convenient aliases+    stk  = vm.state.stack+    self = vm.state.contract+    this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)++    fees@FeeSchedule {..} = vm.block.schedule++    doStop = finishFrame (FrameReturned mempty)++    litSelf = maybeLitAddr self++  if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0x9 then do+    -- call to precompile+    let ?op = 0x00 -- dummy value+    let calldatasize = bufLength vm.state.calldata+    copyBytesToMemory vm.state.calldata calldatasize (Lit 0) (Lit 0)+    executePrecompile (fromJust litSelf) vm.state.gas (Lit 0) calldatasize (Lit 0) (Lit 0) []+    vmx <- get+    case vmx.state.stack of+      x:_ -> case x of+        Lit 0 ->+          fetchAccount self $ \_ -> do+            touchAccount self+            vmError PrecompileFailure+        Lit _ ->+          fetchAccount self $ \_ -> do+            touchAccount self+            out <- use (#state % #returndata)+            finishFrame (FrameReturned out)+        e -> partial $+               UnexpectedSymbolicArg vmx.state.pc "precompile returned a symbolic value" (wrap [e])+      _ ->+        underrun++  else if vm.state.pc >= opslen vm.state.code+    then doStop++    else do+      let ?op = case vm.state.code of+                  UnknownCode _ -> internalError "Cannot execute unknown code"+                  InitCode conc _ -> BS.index conc vm.state.pc+                  RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs vm.state.pc+                  RuntimeCode (SymbolicRuntimeCode ops) ->+                    fromMaybe (internalError "could not analyze symbolic code") $+                      maybeLitByte $ ops V.! vm.state.pc++      case getOp (?op) of++        OpPush0 -> do+          limitStack 1 $+            burn g_base $ do+              next+              pushSym (Lit 0)++        OpPush n' -> do+          let n = into n'+              !xs = case vm.state.code of+                UnknownCode _ -> internalError "Cannot execute unknown code"+                InitCode conc _ -> Lit $ word $ padRight n $ BS.take n (BS.drop (1 + vm.state.pc) conc)+                RuntimeCode (ConcreteRuntimeCode bs) -> Lit $ word $ BS.take n $ BS.drop (1 + vm.state.pc) bs+                RuntimeCode (SymbolicRuntimeCode ops) ->+                  let bytes = V.take n $ V.drop (1 + vm.state.pc) ops+                  in readWord (Lit 0) $ Expr.fromList $ padLeft' 32 bytes+          limitStack 1 $+            burn g_verylow $ do+              next+              pushSym xs++        OpDup i ->+          case preview (ix (into i - 1)) stk of+            Nothing -> underrun+            Just y ->+              limitStack 1 $+                burn g_verylow $ do+                  next+                  pushSym y++        OpSwap i ->+          if length stk < (into i) + 1+            then underrun+            else+              burn g_verylow $ do+                next+                zoom (#state % #stack) $ do+                  assign (ix 0) (stk ^?! ix (into i))+                  assign (ix (into i)) (stk ^?! ix 0)++        OpLog n ->+          notStatic $+          case stk of+            (xOffset:xSize:xs) ->+              if length xs < (into n)+              then underrun+              else do+                bytes <- readMemory xOffset xSize+                let (topics, xs') = splitAt (into n) xs+                    logs'         = (LogEntry (WAddr self) bytes topics) : vm.logs+                burnLog xSize n $+                  accessMemoryRange xOffset xSize $ do+                    traceTopLog logs'+                    next+                    assign (#state % #stack) xs'+                    assign #logs logs'+            _ ->+              underrun++        OpStop -> doStop++        OpAdd -> stackOp2 g_verylow Expr.add+        OpMul -> stackOp2 g_low Expr.mul+        OpSub -> stackOp2 g_verylow Expr.sub++        OpDiv -> stackOp2 g_low Expr.div++        OpSdiv -> stackOp2 g_low Expr.sdiv++        OpMod -> stackOp2 g_low Expr.mod++        OpSmod -> stackOp2 g_low Expr.smod+        OpAddmod -> stackOp3 g_mid Expr.addmod+        OpMulmod -> stackOp3 g_mid Expr.mulmod++        OpLt -> stackOp2 g_verylow Expr.lt+        OpGt -> stackOp2 g_verylow Expr.gt+        OpSlt -> stackOp2 g_verylow Expr.slt+        OpSgt -> stackOp2 g_verylow Expr.sgt++        OpEq -> stackOp2 g_verylow Expr.eq+        OpIszero -> stackOp1 g_verylow Expr.iszero++        OpAnd -> stackOp2 g_verylow Expr.and+        OpOr -> stackOp2 g_verylow Expr.or+        OpXor -> stackOp2 g_verylow Expr.xor+        OpNot -> stackOp1 g_verylow Expr.not++        OpByte -> stackOp2 g_verylow (\i w -> Expr.padByte $ Expr.indexWord i w)++        OpShl -> stackOp2 g_verylow Expr.shl+        OpShr -> stackOp2 g_verylow Expr.shr+        OpSar -> stackOp2 g_verylow Expr.sar++        -- more accurately referred to as KECCAK+        OpSha3 ->+          case stk of+            xOffset:xSize:xs ->+              burnSha3 xSize $+                accessMemoryRange xOffset xSize $ do+                  hash <- readMemory xOffset xSize >>= \case+                    orig@(ConcreteBuf bs) ->+                      whenSymbolicElse+                        (pure $ Keccak orig)+                        (pure $ Lit (keccak' bs))+                    buf -> pure $ Keccak buf+                  next+                  assign (#state % #stack) (hash : xs)+            _ -> underrun++        OpAddress ->+          limitStack 1 $+            burn g_base (next >> pushAddr self)++        OpBalance ->+          case stk of+            x:xs -> forceAddr x "BALANCE" $ \a ->+              accessAndBurn a $+                fetchAccount a $ \c -> do+                  next+                  assign (#state % #stack) xs+                  pushSym c.balance+            [] ->+              underrun++        OpOrigin ->+          limitStack 1 . burn g_base $+            next >> pushAddr vm.tx.origin++        OpCaller ->+          limitStack 1 . burn g_base $+            next >> pushAddr vm.state.caller++        OpCallvalue ->+          limitStack 1 . burn g_base $+            next >> pushSym vm.state.callvalue++        OpCalldataload -> stackOp1 g_verylow $+          \ind -> Expr.readWord ind vm.state.calldata++        OpCalldatasize ->+          limitStack 1 . burn g_base $+            next >> pushSym (bufLength vm.state.calldata)++        OpCalldatacopy ->+          case stk of+            xTo:xFrom:xSize:xs ->+              burnCalldatacopy xSize $+                accessMemoryRange xTo xSize $ do+                  next+                  assign (#state % #stack) xs+                  copyBytesToMemory vm.state.calldata xSize xFrom xTo+            _ -> underrun++        OpCodesize ->+          limitStack 1 . burn g_base $+            next >> pushSym (codelen vm.state.code)++        OpCodecopy ->+          case stk of+            memOffset:codeOffset:n:xs ->+              burnCodecopy n $ do+                accessMemoryRange memOffset n $ do+                  next+                  assign (#state % #stack) xs+                  case toBuf vm.state.code of+                    Just b -> copyBytesToMemory b n codeOffset memOffset+                    Nothing -> internalError "Cannot produce a buffer from UnknownCode"+            _ -> underrun++        OpGasprice ->+          limitStack 1 . burn g_base $+            next >> push vm.tx.gasprice++        OpExtcodesize ->+          case stk of+            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do+              let impl = accessAndBurn x $+                           fetchAccount x $ \c -> do+                             next+                             assign (#state % #stack) xs+                             case view bytecode c of+                               Just b -> pushSym (bufLength b)+                               Nothing -> pushSym $ CodeSize x+              case x of+                a@(LitAddr _) -> if a == cheatCode+                  then do+                    next+                    assign (#state % #stack) xs+                    pushSym (Lit 1)+                  else impl+                _ -> impl+            [] ->+              underrun++        OpExtcodecopy ->+          case stk of+            extAccount':memOffset:codeOffset:codeSize:xs ->+              forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do+                burnExtcodecopy extAccount codeSize $+                  accessMemoryRange memOffset codeSize $+                    fetchAccount extAccount $ \c -> do+                      next+                      assign (#state % #stack) xs+                      case view bytecode c of+                        Just b -> copyBytesToMemory b codeSize codeOffset memOffset+                        Nothing -> do+                          pc <- use (#state % #pc)+                          partial $ UnexpectedSymbolicArg pc "Cannot copy from unknown code at" (wrap [extAccount])+            _ -> underrun++        OpReturndatasize ->+          limitStack 1 . burn g_base $+            next >> pushSym (bufLength vm.state.returndata)++        OpReturndatacopy ->+          case stk of+            xTo:xFrom:xSize:xs ->+              burnReturndatacopy xSize $+                accessMemoryRange xTo xSize $ do+                  next+                  assign (#state % #stack) xs++                  let jump True = vmError ReturnDataOutOfBounds+                      jump False = copyBytesToMemory vm.state.returndata xSize xFrom xTo++                  case (xFrom, bufLength vm.state.returndata, xSize) of+                    (Lit f, Lit l, Lit sz) ->+                      jump $ l < f + sz || f + sz < f+                    _ -> do+                      let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize)+                          overflow = Expr.lt (Expr.add xFrom xSize) (xFrom)+                      branch (Expr.or oob overflow) jump+            _ -> underrun++        OpExtcodehash ->+          case stk of+            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->+              accessAndBurn x $ do+                next+                assign (#state % #stack) xs+                fetchAccount x $ \c ->+                   if accountEmpty c+                     then push (W256 0)+                     else case view bytecode c of+                            Just b -> pushSym $ keccak b+                            Nothing -> pushSym $ CodeHash x+            [] ->+              underrun++        OpBlockhash -> do+          -- We adopt the fake block hash scheme of the VMTests,+          -- so that blockhash(i) is the hash of i as decimal ASCII.+          stackOp1 g_blockhash $ \case+            Lit i -> if i + 256 < vm.block.number || i >= vm.block.number+                     then Lit 0+                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit+            i -> BlockHash i++        OpCoinbase ->+          limitStack 1 . burn g_base $+            next >> pushAddr vm.block.coinbase++        OpTimestamp ->+          limitStack 1 . burn g_base $+            next >> pushSym vm.block.timestamp++        OpNumber ->+          limitStack 1 . burn g_base $+            next >> push vm.block.number++        OpPrevRandao -> do+          limitStack 1 . burn g_base $+            next >> push vm.block.prevRandao++        OpGaslimit ->+          limitStack 1 . burn g_base $+            next >> push (into vm.block.gaslimit)++        OpChainid ->+          limitStack 1 . burn g_base $+            next >> push vm.env.chainId++        OpSelfbalance ->+          limitStack 1 . burn g_low $+            next >> pushSym this.balance++        OpBaseFee ->+          limitStack 1 . burn g_base $+            next >> push vm.block.baseFee++        OpPop ->+          case stk of+            _:xs -> burn g_base (next >> assign (#state % #stack) xs)+            _    -> underrun++        OpMload ->+          case stk of+            x:xs ->+              burn g_verylow $+                accessMemoryWord x $ do+                  next+                  buf <- readMemory x (Lit 32)+                  let w = Expr.readWordFromBytes (Lit 0) buf+                  assign (#state % #stack) (w : xs)+            _ -> underrun++        OpMstore ->+          case stk of+            x:y:xs ->+              burn g_verylow $+                accessMemoryWord x $ do+                  next+                  gets (.state.memory) >>= \case+                    ConcreteMemory mem -> do+                      case y of+                        Lit w ->+                          copyBytesToMemory (ConcreteBuf (word256Bytes w)) (Lit 32) (Lit 0) x+                        _ -> do+                          -- copy out and move to symbolic memory+                          buf <- freezeMemory mem+                          assign (#state % #memory) (SymbolicMemory $ writeWord x y buf)+                    SymbolicMemory mem ->+                      assign (#state % #memory) (SymbolicMemory $ writeWord x y mem)+                  assign (#state % #stack) xs+            _ -> underrun++        OpMstore8 ->+          case stk of+            x:y:xs ->+              burn g_verylow $+                accessMemoryRange x (Lit 1) $ do+                  let yByte = indexWord (Lit 31) y+                  next+                  gets (.state.memory) >>= \case+                    ConcreteMemory mem -> do+                      case yByte of+                        LitByte byte ->+                          copyBytesToMemory (ConcreteBuf (BS.pack [byte])) (Lit 1) (Lit 0) x+                        _ -> do+                          -- copy out and move to symbolic memory+                          buf <- freezeMemory mem+                          assign (#state % #memory) (SymbolicMemory $ writeByte x yByte buf)+                    SymbolicMemory mem ->+                      assign (#state % #memory) (SymbolicMemory $ writeByte x yByte mem)++                  assign (#state % #stack) xs+            _ -> underrun++        OpSload ->+          case stk of+            x:xs -> do+              acc <- accessStorageForGas self x+              let cost = if acc then g_warm_storage_read else g_cold_sload+              burn cost $+                accessStorage self x $ \y -> do+                  next+                  assign (#state % #stack) (y:xs)+            _ -> underrun++        OpSstore ->+          notStatic $+          case stk of+            x:new:xs ->+              accessStorage self x $ \current -> do+                ensureGas g_callstipend $ do+                  let+                    original =+                      case Expr.concKeccakSimpExpr $ SLoad x this.origStorage of+                        Lit v -> v+                        _ -> 0+                    storage_cost =+                      case (maybeLitWord current, maybeLitWord new) of+                        (Just current', Just new') ->+                           if (current' == new') then g_sload+                           else if (current' == original) && (original == 0) then g_sset+                           else if (current' == original) then g_sreset+                           else g_sload++                        -- if any of the arguments are symbolic,+                        -- assume worst case scenario+                        _-> g_sset++                  acc <- accessStorageForGas self x+                  let cold_storage_cost = if acc then 0 else g_cold_sload+                  burn (storage_cost + cold_storage_cost) $ do+                    next+                    assign (#state % #stack) xs+                    modifying (#env % #contracts % ix self % #storage) (writeStorage x new)++                    case (maybeLitWord current, maybeLitWord new) of+                       (Just current', Just new') ->+                          unless (current' == new') $+                            if current' == original then+                              when (original /= 0 && new' == 0) $+                                refund (g_sreset + g_access_list_storage_key)+                            else do+                              when (original /= 0) $+                                if current' == 0+                                then unRefund (g_sreset + g_access_list_storage_key)+                                else when (new' == 0) $ refund (g_sreset + g_access_list_storage_key)+                              when (original == new') $+                                if original == 0+                                then refund (g_sset - g_sload)+                                else refund (g_sreset - g_sload)+                       -- if any of the arguments are symbolic,+                       -- don't change the refund counter+                       _ -> noop+            _ -> underrun++        OpJump ->+          case stk of+            x:xs ->+              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->+                case toInt x' of+                  Nothing -> vmError BadJumpDestination+                  Just i -> checkJump i xs+            _ -> underrun++        OpJumpi ->+          case stk of+            x:y:xs -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->+              burn g_high $+                let jump :: Bool -> EVM t s ()+                    jump False = assign (#state % #stack) xs >> next+                    jump _    = case toInt x' of+                      Nothing -> vmError BadJumpDestination+                      Just i -> checkJump i xs+                in branch y jump+            _ -> underrun++        OpPc ->+          limitStack 1 . burn g_base $+            next >> push (unsafeInto vm.state.pc)++        OpMsize ->+          limitStack 1 . burn g_base $+            next >> push (into vm.state.memorySize)++        OpGas ->+          limitStack 1 . burn g_base $+            next >> pushGas++        OpJumpdest -> burn g_jumpdest next++        OpExp ->+          -- NOTE: this can be done symbolically using unrolling like this:+          --       https://hackage.haskell.org/package/sbv-9.0/docs/src/Data.SBV.Core.Model.html#.%5E+          --       However, it requires symbolic gas, since the gas depends on the exponent+          case stk of+            base:exponent:xs ->+              burnExp exponent $ do+                next+                (#state % #stack) .= Expr.exp base exponent : xs+            _ -> underrun++        OpSignextend -> stackOp2 g_low Expr.sex++        OpCreate ->+          notStatic $+          case stk of+            xValue:xOffset:xSize:xs ->+              accessMemoryRange xOffset xSize $ do+                availableGas <- use (#state % #gas)+                let+                  (cost, gas') = costOfCreate fees availableGas xSize False+                newAddr <- createAddress self this.nonce+                _ <- accessAccountForGas newAddr+                burn' cost $ do+                  initCode <- readMemory xOffset xSize+                  create self this xSize gas' xValue xs newAddr initCode+            _ -> underrun++        OpCall ->+          case stk of+            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->+              branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do+                (if gt0 then notStatic else id) $+                  forceAddr xTo' "unable to determine a call target" $ \xTo ->+                    case gasTryFrom xGas of+                      Left _ -> vmError IllegalOverflow+                      Right gas ->+                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $+                          \callee -> do+                            let from' = fromMaybe self vm.config.overrideCaller+                            zoom #state $ do+                              assign #callvalue xValue+                              assign #caller from'+                              assign #contract callee+                            assign (#config % #overrideCaller) Nothing+                            touchAccount from'+                            touchAccount callee+                            transfer from' callee xValue+            _ ->+              underrun++        OpCallcode ->+          case stk of+            xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->+              forceAddr xTo' "unable to determine a call target" $ \xTo ->+                case gasTryFrom xGas of+                  Left _ -> vmError IllegalOverflow+                  Right gas ->+                    delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                      zoom #state $ do+                        assign #callvalue xValue+                        assign #caller $ fromMaybe self vm.config.overrideCaller+                      assign (#config % #overrideCaller) Nothing+                      touchAccount self+            _ ->+              underrun++        OpReturn ->+          case stk of+            xOffset:xSize:_ ->+              accessMemoryRange xOffset xSize $ do+                output <- readMemory xOffset xSize+                let+                  codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")+                               . maybeLitWord . bufLength $ output+                  maxsize = vm.block.maxCodeSize+                  creation = case vm.frames of+                    [] -> vm.tx.isCreate+                    frame:_ -> case frame.context of+                       CreationContext {} -> True+                       CallContext {} -> False+                if creation+                then+                  if codesize > maxsize+                  then+                    finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))+                  else do+                    let frameReturned = burn (g_codedeposit * unsafeInto codesize) $+                                          finishFrame (FrameReturned output)+                        frameErrored = finishFrame $ FrameErrored InvalidFormat+                    case readByte (Lit 0) output of+                      LitByte 0xef -> frameErrored+                      LitByte _ -> frameReturned+                      y -> branch (Expr.eqByte y (LitByte 0xef)) $ \case+                          True -> frameErrored+                          False -> frameReturned+                else+                   finishFrame (FrameReturned output)+            _ -> underrun++        OpDelegatecall ->+          case stk of+            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->+              case wordToAddr xTo of+                Nothing -> do+                  loc <- codeloc+                  let msg = "Unable to determine a call target"+                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]+                Just xTo' ->+                  case gasTryFrom xGas of+                    Left _ -> vmError IllegalOverflow+                    Right gas ->+                      delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $+                        \_ -> touchAccount self+            _ -> underrun++        OpCreate2 -> notStatic $+          case stk of+            xValue:xOffset:xSize:xSalt':xs ->+              forceConcrete xSalt' "CREATE2" $ \(xSalt) ->+                accessMemoryRange xOffset xSize $ do+                  availableGas <- use (#state % #gas)+                  buf <- readMemory xOffset xSize+                  forceConcreteBuf buf "CREATE2" $+                    \initCode -> do+                      let+                        (cost, gas') = costOfCreate fees availableGas xSize True+                      newAddr <- create2Address self xSalt initCode+                      _ <- accessAccountForGas newAddr+                      burn' cost $+                        create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode)+            _ -> underrun++        OpStaticcall ->+          case stk of+            xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->+              case wordToAddr xTo of+                Nothing -> do+                  loc <- codeloc+                  let msg = "Unable to determine a call target"+                  partial $ UnexpectedSymbolicArg (snd loc) msg [SomeExpr xTo]+                Just xTo' ->+                  case gasTryFrom xGas of+                    Left _ -> vmError IllegalOverflow+                    Right gas ->+                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $+                        \callee -> do+                          zoom #state $ do+                            assign #callvalue (Lit 0)+                            assign #caller $ fromMaybe self (vm.config.overrideCaller)+                            assign #contract callee+                            assign #static True+                          assign (#config % #overrideCaller) Nothing+                          touchAccount self+                          touchAccount callee+            _ ->+              underrun++        OpSelfdestruct ->+          notStatic $+          case stk of+            [] -> underrun+            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case+              xTo@(LitAddr _) -> do+                acc <- accessAccountForGas xTo+                let cost = if acc then 0 else g_cold_account_access+                    funds = this.balance+                    recipientExists = accountExists xTo vm+                branch (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do+                  let c_new = if (not recipientExists) && hasFunds+                              then g_selfdestruct_newaccount+                              else 0+                  burn (g_selfdestruct + c_new + cost) $ do+                    selfdestruct self+                    touchAccount xTo++                    if hasFunds+                    then fetchAccount xTo $ \_ -> do+                           #env % #contracts % ix xTo % #balance %= (Expr.add funds)+                           assign (#env % #contracts % ix self % #balance) (Lit 0)+                           doStop+                    else do+                      doStop+              a -> do+                pc <- use (#state % #pc)+                partial $ UnexpectedSymbolicArg pc "trying to self destruct to a symbolic address" (wrap [a])++        OpRevert ->+          case stk of+            xOffset:xSize:_ ->+              accessMemoryRange xOffset xSize $ do+                output <- readMemory xOffset xSize+                finishFrame (FrameReverted output)+            _ -> underrun++        OpUnknown xxx ->+          vmError $ UnrecognizedOpcode xxx++transfer :: VMOps t => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()+transfer _ _ (Lit 0) = pure ()+transfer src dst val = do+  sb <- preuse $ #env % #contracts % ix src % #balance+  db <- preuse $ #env % #contracts % ix dst % #balance+  baseState <- use (#config % #baseState)+  let mkc = case baseState of+              AbstractBase -> unknownContract+              EmptyBase -> const emptyContract+  case (sb, db) of+    -- both sender and recipient in state+    (Just srcBal, Just _) ->+      branch (Expr.gt val srcBal) $ \case+        True -> vmError $ BalanceTooLow val srcBal+        False -> do+          (#env % #contracts % ix src % #balance) %= (`Expr.sub` val)+          (#env % #contracts % ix dst % #balance) %= (`Expr.add` val)+    -- sender not in state+    (Nothing, Just _) -> do+      case src of+        LitAddr _ -> do+          (#env % #contracts) %= (Map.insert src (mkc src))+          transfer src dst val+        SymAddr _ -> do+          pc <- use (#state % #pc)+          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [src])+        GVar _ -> internalError "Unexpected GVar"+    -- recipient not in state+    (_ , Nothing) -> do+      case dst of+        LitAddr _ -> do+          (#env % #contracts) %= (Map.insert dst (mkc dst))+          transfer src dst val+        SymAddr _ -> do+          pc <- use (#state % #pc)+          partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth to a symbolic address that is not present in the state" (wrap [dst])+        GVar _ -> internalError "Unexpected GVar"++-- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.+callChecks+  :: forall (t :: VMType) s. (?op :: Word8, VMOps t)+  => Contract+  -> Gas t+  -> Expr EAddr+  -> Expr EAddr+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> [Expr EWord]+  -- continuation with gas available for call+  -> (Gas t -> EVM t s ())+  -> EVM t s ()+callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do+  vm <- get+  let fees = vm.block.schedule+  accessMemoryRange xInOffset xInSize $+    accessMemoryRange xOutOffset xOutSize $ do+      availableGas <- use (#state % #gas)+      let recipientExists = accountExists xContext vm+      let from = fromMaybe vm.state.contract vm.config.overrideCaller+      fromBal <- preuse $ #env % #contracts % ix from % #balance+      costOfCall fees recipientExists xValue availableGas xGas xTo $ \cost gas' -> do+        let checkCallDepth =+              if length vm.frames >= 1024+              then do+                assign (#state % #stack) (Lit 0 : xs)+                assign (#state % #returndata) mempty+                pushTrace $ ErrorTrace CallDepthLimitReached+                next+              else continue (toGas gas')+        case (fromBal, xValue) of+          -- we're not transferring any value, and can skip the balance check+          (_, Lit 0) -> burn (cost - gas') checkCallDepth++          -- from is in the state, we check if they have enough balance+          (Just fb, _) -> do+            burn (cost - gas') $+              branch (Expr.gt xValue fb) $ \case+                True -> do+                  assign (#state % #stack) (Lit 0 : xs)+                  assign (#state % #returndata) mempty+                  pushTrace $ ErrorTrace (BalanceTooLow xValue this.balance)+                  next+                False -> checkCallDepth++          -- from is not in the state, we insert it if safe to do so and run the checks again+          (Nothing, _) -> case from of+            LitAddr _ -> do+              -- insert an entry in the state+              let contract = case vm.config.baseState of+                    AbstractBase -> unknownContract from+                    EmptyBase -> emptyContract+              (#env % #contracts) %= (Map.insert from contract)+              -- run callChecks again+              callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue++            -- adding a symbolic address into the state here would be unsound (due to potential aliasing)+            SymAddr _ -> do+              pc <- use (#state % #pc)+              partial $ UnexpectedSymbolicArg pc "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [from])+            GVar _ -> internalError "Unexpected GVar"+++++precompiledContract+  :: (?op :: Word8, VMOps t)+  => Contract+  -> Gas t+  -> Addr+  -> Addr+  -> Expr EWord+  -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord+  -> [Expr EWord]+  -> EVM t s ()+precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs+  = callChecks this xGas (LitAddr recipient) (LitAddr precompileAddr) xValue inOffset inSize outOffset outSize xs $ \gas' ->+    do+      executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs+      self <- use (#state % #contract)+      stk <- use (#state % #stack)+      pc' <- use (#state % #pc)+      result' <- use #result+      case result' of+        Nothing -> case stk of+          x:_ -> case maybeLitWord x of+            Just 0 ->+              pure ()+            Just 1 ->+              fetchAccount (LitAddr recipient) $ \_ -> do+                touchAccount self+                touchAccount (LitAddr recipient)+                transfer self (LitAddr recipient) xValue+            _ -> partial $+                   UnexpectedSymbolicArg pc' "unexpected return value from precompile" (wrap [x])+          _ -> underrun+        _ -> pure ()++executePrecompile+  :: (?op :: Word8, VMOps t)+  => Addr+  -> Gas t -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord -> [Expr EWord]+  -> EVM t s ()+executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do+  vm <- get+  input <- readMemory inOffset inSize+  let fees = vm.block.schedule+      cost = costOfPrecompile fees preCompileAddr input+      notImplemented = internalError $ "precompile at address " <> show preCompileAddr <> " not yet implemented"+      precompileFail = burn' (subGas gasCap cost) $ do+                         assign (#state % #stack) (Lit 0 : xs)+                         pushTrace $ ErrorTrace PrecompileFailure+                         next+  if not (enoughGas cost gasCap) then+    burn' gasCap $ do+      assign (#state % #stack) (Lit 0 : xs)+      next+  else burn cost $+    case preCompileAddr of+      -- ECRECOVER+      0x1 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECRECOVER" $ \input' -> do+          case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of+            Nothing -> do+              -- return no output for invalid signature+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) mempty+              next+            Just output -> do+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) (ConcreteBuf output)+              copyBytesToMemory (ConcreteBuf output) outSize (Lit 0) outOffset+              next++      -- SHA2-256+      0x2 ->+        forceConcreteBuf input "SHA2-256" $ \input' -> do+          let+            hash = sha256Buf input'+            sha256Buf x = ConcreteBuf $ BA.convert (Crypto.hash x :: Digest SHA256)+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) hash+          copyBytesToMemory hash outSize (Lit 0) outOffset+          next++      -- RIPEMD-160+      0x3 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "RIPEMD160" $ \input' -> do+          let+            padding = BS.pack $ replicate 12 0+            hash' = BA.convert (Crypto.hash input' :: Digest RIPEMD160)+            hash  = ConcreteBuf $ padding <> hash'+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) hash+          copyBytesToMemory hash outSize (Lit 0) outOffset+          next++      -- IDENTITY+      0x4 -> do+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) input+          copyCallBytesToMemory input outSize outOffset+          next++      -- MODEXP+      0x5 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "MODEXP" $ \input' -> do+          let+            (lenb, lene, lenm) = parseModexpLength input'++            output = ConcreteBuf $+              if isZero (96 + lenb + lene) lenm input'+              then truncpadlit (unsafeInto lenm) (asBE (0 :: Int))+              else+                let+                  b = asInteger $ lazySlice 96 lenb input'+                  e = asInteger $ lazySlice (96 + lenb) lene input'+                  m = asInteger $ lazySlice (96 + lenb + lene) lenm input'+                in+                  padLeft (unsafeInto lenm) (asBE (expFast b e m))+          assign (#state % #stack) (Lit 1 : xs)+          assign (#state % #returndata) output+          copyBytesToMemory output outSize (Lit 0) outOffset+          next++      -- ECADD+      0x6 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECADD" $ \input' ->+          case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of+            Nothing -> precompileFail+            Just output -> do+              let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+              assign (#state % #stack) (Lit 1 : xs)+              assign (#state % #returndata) truncpaddedOutput+              copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset+              next++      -- ECMUL+      0x7 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECMUL" $ \input' ->+          case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+            assign (#state % #stack) (Lit 1 : xs)+            assign (#state % #returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset+            next++      -- ECPAIRING+      0x8 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "ECPAIR" $ \input' ->+          case EVM.Precompiled.execute 0x8 input' 32 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuf $ truncpadlit 32 output+            assign (#state % #stack) (Lit 1 : xs)+            assign (#state % #returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset+            next++      -- BLAKE2+      0x9 ->+        -- TODO: support symbolic variant+        forceConcreteBuf input "BLAKE2" $ \input' -> do+          case (BS.length input', 1 >= BS.last input') of+            (213, True) -> case EVM.Precompiled.execute 0x9 input' 64 of+              Just output -> do+                let truncpaddedOutput = ConcreteBuf $ truncpadlit 64 output+                assign (#state % #stack) (Lit 1 : xs)+                assign (#state % #returndata) truncpaddedOutput+                copyBytesToMemory truncpaddedOutput outSize (Lit 0) outOffset+                next+              Nothing -> precompileFail+            _ -> precompileFail++      _ -> notImplemented++truncpadlit :: Int -> ByteString -> ByteString+truncpadlit n xs = if m > n then BS.take n xs+                   else BS.append xs (BS.replicate (n - m) 0)+  where m = BS.length xs++lazySlice :: W256 -> W256 -> ByteString -> LS.ByteString+lazySlice offset size bs =+  let bs' = LS.take (unsafeInto size) (LS.drop (unsafeInto offset) (fromStrict bs))+  in bs' <> LS.replicate (unsafeInto size - LS.length bs') 0++parseModexpLength :: ByteString -> (W256, W256, W256)+parseModexpLength input =+  let lenb = word $ LS.toStrict $ lazySlice  0 32 input+      lene = word $ LS.toStrict $ lazySlice 32 64 input+      lenm = word $ LS.toStrict $ lazySlice 64 96 input+  in (lenb, lene, lenm)++--- checks if a range of ByteString bs starting at offset and length size is all zeros.+isZero :: W256 -> W256 -> ByteString -> Bool+isZero offset size bs =+  LS.all (== 0) $+    LS.take (unsafeInto size) $+      LS.drop (unsafeInto offset) $+        fromStrict bs++asInteger :: LS.ByteString -> Integer+asInteger xs = if xs == mempty then 0+  else 256 * asInteger (LS.init xs)+      + into (LS.last xs)++-- * Opcode helper actions++noop :: Monad m => m ()+noop = pure ()++pushTo :: MonadState s m => Lens s s [a] [a] -> a -> m ()+pushTo f x = f %= (x :)++pushToSequence :: MonadState s m => Setter s s (Seq a) (Seq a) -> a -> m ()+pushToSequence f x = f %= (Seq.|> x)++getCodeLocation :: VM t s -> CodeLocation+getCodeLocation vm = (vm.state.contract, vm.state.pc)++query :: Query t s -> EVM t s ()+query = assign #result . Just . HandleEffect . Query++choose :: Choose s -> EVM Symbolic s ()+choose = assign #result . Just . HandleEffect . Choose++-- | Construct RPC Query and halt execution until resolved+fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()+fetchAccount addr continue =+  use (#env % #contracts % at addr) >>= \case+    Just c -> continue c+    Nothing -> case addr of+      SymAddr _ -> do+        pc <- use (#state % #pc)+        partial $ UnexpectedSymbolicArg pc "trying to access a symbolic address that isn't already present in storage" (wrap [addr])+      LitAddr a -> do+        use (#cache % #fetched % at a) >>= \case+          Just c -> do+            assign (#env % #contracts % at addr) (Just c)+            continue c+          Nothing -> do+            base <- use (#config % #baseState)+            assign (#result) . Just . HandleEffect . Query $+              PleaseFetchContract a base+                (\c -> do assign (#cache % #fetched % at a) (Just c)+                          assign (#env % #contracts % at addr) (Just c)+                          assign #result Nothing+                          continue c)+      GVar _ -> internalError "Unexpected GVar"++accessStorage+  :: VMOps t => Expr EAddr+  -> Expr EWord+  -> (Expr EWord -> EVM t s ())+  -> EVM t s ()+accessStorage addr slot continue = do+  let slotConc = Expr.concKeccakSimpExpr slot+  use (#env % #contracts % at addr) >>= \case+    Just c ->+      -- Try first without concretization. Then if we get a Just, with concretization+      -- if both give a Just, should we `continue`.+      -- --> This is because readStorage can do smart rewrites, but only in case+      --     the expression is of a particular format, which can be destroyed by simplification.+      --     However, without concretization, it may not find things that are actually in the storage+      case readStorage slot c.storage of+        Just x -> case readStorage slotConc c.storage of+          Just _ -> continue x+          Nothing -> rpcCall c slotConc+        Nothing -> rpcCall c slotConc+    Nothing ->+      fetchAccount addr $ \_ ->+        accessStorage addr slot continue+  where+      rpcCall c slotConc = if c.external+        then forceConcreteAddr addr "cannot read storage from symbolic addresses via rpc" $ \addr' ->+          forceConcrete slotConc "cannot read symbolic slots via RPC" $ \slot' -> do+            -- check if the slot is cached+            contract <- preuse (#cache % #fetched % ix addr')+            case contract of+              Nothing -> internalError "contract marked external not found in cache"+              Just fetched -> case readStorage (Lit slot') fetched.storage of+                          Nothing -> mkQuery addr' slot'+                          Just val -> continue val+        else do+          modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))+          continue $ Lit 0+      mkQuery a s = query $+        PleaseFetchSlot a s+          (\x -> do+              modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x))+              modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))+              assign #result Nothing+              continue (Lit x))++accountExists :: Expr EAddr -> VM t s -> Bool+accountExists addr vm =+  case Map.lookup addr vm.env.contracts of+    Just c -> not (accountEmpty c)+    Nothing -> False++-- EIP 161+accountEmpty :: Contract -> Bool+accountEmpty c =+  case c.code of+    RuntimeCode (ConcreteRuntimeCode "") -> True+    RuntimeCode (SymbolicRuntimeCode b) -> null b+    _ -> False+  && c.nonce == (Just 0)+  -- TODO: handle symbolic balance...+  && c.balance == Lit 0++-- * How to finalize a transaction+finalize :: VMOps t => EVM t s ()+finalize = do+  let+    revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)+    revertSubstate   = assign (#tx % #substate) (SubState mempty mempty mempty mempty mempty)++  use #result >>= \case+    Just (VMFailure (Revert _)) -> do+      revertContracts+      revertSubstate+    Just (VMFailure _) -> do+      -- burn remaining gas+      assign (#state % #gas) initialGas+      revertContracts+      revertSubstate+    Just (VMSuccess output) -> do+      -- deposit the code from a creation tx+      pc' <- use (#state % #pc)+      creation <- use (#tx % #isCreate)+      createe  <- use (#state % #contract)+      createeExists <- (Map.member createe) <$> use (#env % #contracts)+      let onContractCode contractCode =+            when (creation && createeExists) $ replaceCode createe contractCode+      case output of+        ConcreteBuf bs ->+          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+        _ ->+          case Expr.toList output of+            Nothing ->+              partial $+                UnexpectedSymbolicArg pc' "runtime code cannot have an abstract length" (wrap [output])+            Just ops ->+              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)+    _ ->+      internalError "Finalising an unfinished tx."++  -- compute and pay the refund to the caller and the+  -- corresponding payment to the miner+  block <- use #block++  payRefunds++  touchAccount block.coinbase++  -- perform state trie clearing (EIP 161), of selfdestructs+  -- and touched accounts. addresses are cleared if they have+  --    a) selfdestructed, or+  --    b) been touched and+  --    c) are empty.+  -- (see Yellow Paper "Accrued Substate")+  --+  -- remove any destructed addresses+  destroyedAddresses <- use (#tx % #substate % #selfdestructs)+  modifying (#env % #contracts)+    (Map.filterWithKey (\k _ -> (k `notElem` destroyedAddresses)))+  -- then, clear any remaining empty and touched addresses+  touchedAddresses <- use (#tx % #substate % #touchedAccounts)+  modifying (#env % #contracts)+    (Map.filterWithKey+      (\k a -> not ((k `elem` touchedAddresses) && accountEmpty a)))++-- | Loads the selected contract as the current contract to execute+loadContract :: Expr EAddr -> State (VM t s) ()+loadContract target =+  preuse (#env % #contracts % ix target % #code) >>=+    \case+      Nothing ->+        internalError "Call target doesn't exist"+      Just targetCode -> do+        assign (#state % #contract) target+        assign (#state % #code)     targetCode+        assign (#state % #codeContract) target++limitStack :: VMOps t => Int -> EVM (t :: VMType) s () -> EVM t s ()+limitStack n continue = do+  stk <- use (#state % #stack)+  if length stk + n > 1024+    then vmError StackLimitExceeded+    else continue++notStatic :: VMOps t => EVM t s () -> EVM t s ()+notStatic continue = do+  bad <- use (#state % #static)+  if bad+    then vmError StateChangeWhileStatic+    else continue++forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()+forceAddr n msg continue = case wordToAddr n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()+forceConcrete n msg continue = case maybeLitWord n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()+forceConcreteAddr n msg continue = case maybeLitAddr n of+  Nothing -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])+  Just c -> continue c++forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()+forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of+  (Just c, Just d) -> continue (c,d)+  _ -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])++forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()+forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of+  (Just c, Just d) -> continue (c, d)+  _ -> do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])++forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()+forceConcreteBuf (ConcreteBuf b) _ continue = continue b+forceConcreteBuf b msg _ = do+    vm <- get+    partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [b])++-- * Substate manipulation+refund :: Word64 -> EVM t s ()+refund n = do+  self <- use (#state % #contract)+  pushTo (#tx % #substate % #refunds) (self, n)++unRefund :: Word64 -> EVM t s ()+unRefund n = do+  self <- use (#state % #contract)+  refs <- use (#tx % #substate % #refunds)+  assign (#tx % #substate % #refunds)+    (filter (\(a,b) -> not (a == self && b == n)) refs)++touchAccount :: Expr EAddr -> EVM t s ()+touchAccount = pushTo ((#tx % #substate) % #touchedAccounts)++selfdestruct :: Expr EAddr -> EVM t s ()+selfdestruct = pushTo ((#tx % #substate) % #selfdestructs)++accessAndBurn :: VMOps t => Expr EAddr -> EVM t s () -> EVM t s ()+accessAndBurn x cont = do+  FeeSchedule {..} <- use (#block % #schedule)+  acc <- accessAccountForGas x+  let cost = if acc then g_warm_storage_read else g_cold_account_access+  burn cost cont++-- | returns a wrapped boolean- if true, this address has been touched before in the txn (warm gas cost as in EIP 2929)+-- otherwise cold+accessAccountForGas :: Expr EAddr -> EVM t s Bool+accessAccountForGas addr = do+  accessedAddrs <- use (#tx % #substate % #accessedAddresses)+  let accessed = member addr accessedAddrs+  assign (#tx % #substate % #accessedAddresses) (insert addr accessedAddrs)+  pure accessed++-- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)+-- otherwise cold+accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool+accessStorageForGas addr key = do+  accessedStrkeys <- use (#tx % #substate % #accessedStorageKeys)+  case maybeLitWord key of+    Just litword -> do+      let accessed = member (addr, litword) accessedStrkeys+      assign (#tx % #substate % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)+      pure accessed+    _ -> pure False++-- * Cheat codes++-- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.+-- Call this address using one of the cheatActions below to do+-- special things, e.g. changing the block timestamp. Beware that+-- these are necessarily hevm specific.+cheatCode :: Expr EAddr+cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")++cheat+  :: (?op :: Word8, VMOps t)+  => (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord)+  -> EVM t s ()+cheat (inOffset, inSize) (outOffset, outSize) = do+  vm <- get+  input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))+  abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)+  pushTrace $ FrameTrace (CallContext cheatCode cheatCode inOffset inSize (Lit 0) (maybeLitWord abi) input vm.env.contracts vm.tx.substate)+  case maybeLitWord abi of+    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc "symbolic cheatcode selector" (wrap [abi])+    Just (unsafeInto -> abi') ->+      case Map.lookup abi' cheatActions of+        Nothing ->+          vmError (BadCheatCode abi')+        Just action -> do+            action outOffset outSize input+            popTrace+            next+            push 1++type CheatAction t s = Expr EWord -> Expr EWord -> Expr Buf -> EVM t s ()++cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)+cheatActions =+  Map.fromList+    [ action "ffi(string[])" $+        \sig outOffset outSize input -> do+          vm <- get+          if vm.config.allowFFI then+            case decodeBuf [AbiArrayDynamicType AbiStringType] input of+              CAbi valsArr -> case valsArr of+                [AbiArrayDynamic AbiStringType strsV] ->+                  let+                    cmd = fmap+                            (\case+                              (AbiString a) -> unpack $ decodeUtf8 a+                              _ -> "")+                            (V.toList strsV)+                    cont bs = do+                      let encoded = ConcreteBuf bs+                      assign (#state % #returndata) encoded+                      copyBytesToMemory encoded outSize (Lit 0) outOffset+                      assign #result Nothing+                  in query (PleaseDoFFI cmd cont)+                _ -> vmError (BadCheatCode sig)+              _ -> vmError (BadCheatCode sig)+          else+            let msg = "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"+            in partial $ UnexpectedSymbolicArg vm.state.pc msg [],++      action "warp(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [x]  -> assign (#block % #timestamp) x+          _ -> vmError (BadCheatCode sig),++      action "deal(address,uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 2 input of+          [a, amt] ->+            forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->+              fetchAccount usr $ \_ -> do+                assign (#env % #contracts % ix usr % #balance) amt+          _ -> vmError (BadCheatCode sig),++      action "assume(bool)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [c] -> modifying #constraints ((:) (PEq c (Lit 1)))+          _ -> vmError (BadCheatCode sig),++      action "roll(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [x] -> forceConcrete x "cannot roll to a symbolic block number" (assign (#block % #number))+          _ -> vmError (BadCheatCode sig),++      action "store(address,bytes32,bytes32)" $+        \sig _ _ input -> case decodeStaticArgs 0 3 input of+          [a, slot, new] -> case wordToAddr a of+            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->+              modifying (#env % #contracts % ix a' % #storage) (writeStorage slot new)+            _ -> vmError (BadCheatCode sig)+          _ -> vmError (BadCheatCode sig),++      action "load(address,bytes32)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of+          [a, slot] -> case wordToAddr a of+            Just a'@(LitAddr _) -> fetchAccount a' $ \_ ->+              accessStorage a' slot $ \res -> do+                assign (#state % #returndata % word256At (Lit 0)) res+                let buf = writeWord (Lit 0) res (ConcreteBuf "")+                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset+            _ -> vmError (BadCheatCode sig)+          _ -> vmError (BadCheatCode sig),++      action "sign(uint256,bytes32)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 2 input of+          [sk, hash] ->+            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do+              let (v,r,s) = EVM.Sign.sign hash' (into sk')+                  encoded = encodeAbiValue $+                    AbiTuple (V.fromList+                      [ AbiUInt 8 $ into v+                      , AbiBytes 32 (word256Bytes r)+                      , AbiBytes 32 (word256Bytes s)+                      ])+              assign (#state % #returndata) (ConcreteBuf encoded)+              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset+          _ -> vmError (BadCheatCode sig),++      action "addr(uint256)" $+        \sig outOffset _ input -> case decodeStaticArgs 0 1 input of+          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do+            let a = EVM.Sign.deriveAddr $ into sk'+            case a of+              Nothing -> vmError (BadCheatCode sig)+              Just address -> do+                let expAddr = litAddr address+                assign (#state % #returndata % word256At (Lit 0)) expAddr+                let buf = ConcreteBuf $ word256Bytes (into address)+                copyBytesToMemory buf (Lit 32) (Lit 0) outOffset+          _ -> vmError (BadCheatCode sig),++      action "prank(address)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [addr]  -> case wordToAddr addr of+            Just a -> assign (#config % #overrideCaller) (Just a)+            Nothing -> vmError (BadCheatCode sig)+          _ -> vmError (BadCheatCode sig),++      action "createFork(string)" $+        \sig outOffset _ input -> case decodeBuf [AbiStringType] input of+          CAbi valsArr -> case valsArr of+            [AbiString bytes] -> do+              forkId <- length <$> gets (.forks)+              let urlOrAlias = Char8.unpack bytes+              modify' $ \vm -> vm { forks = vm.forks Seq.|> ForkState vm.env vm.block vm.cache urlOrAlias }+              let encoded = encodeAbiValue $ AbiUInt 256 (fromIntegral forkId)+              assign (#state % #returndata) (ConcreteBuf encoded)+              copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset+            _ -> vmError (BadCheatCode sig)+          _ -> vmError (BadCheatCode sig),++      action "selectFork(uint256)" $+        \sig _ _ input -> case decodeStaticArgs 0 1 input of+          [forkId] ->+            forceConcrete forkId "forkId must be concrete" $ \(fromIntegral -> forkId') -> do+              saved <- Seq.lookup forkId' <$> gets (.forks)+              case saved of+                Just forkState -> do+                  vm <- get+                  let contractAddr = vm.state.contract+                  let callerAddr = vm.state.caller+                  fetchAccount contractAddr $ \contractAcct -> fetchAccount callerAddr $ \callerAcct -> do+                    let+                      -- the current contract is persisted across forks+                      newContracts = Map.insert callerAddr callerAcct $+                                     Map.insert contractAddr contractAcct forkState.env.contracts+                      newEnv = (forkState.env :: Env) { contracts = newContracts }++                    when (vm.currentFork /= forkId') $ do+                      modify' $ \vm' -> vm'+                        { env = newEnv+                        , block = forkState.block+                        , forks = Seq.adjust' (\state -> (state :: ForkState)+                            { env = vm.env, block = vm.block, cache = vm.cache }+                          ) vm.currentFork  vm.forks+                        , currentFork = forkId'+                        }+                Nothing ->+                  vmError (NonexistentFork forkId')+          _ -> vmError (BadCheatCode sig),++      action "activeFork()" $+        \_ outOffset _ _ -> do+          vm <- get+          let encoded = encodeAbiValue $ AbiUInt 256 (fromIntegral vm.currentFork)+          assign (#state % #returndata) (ConcreteBuf encoded)+          copyBytesToMemory (ConcreteBuf encoded) (Lit . unsafeInto . BS.length $ encoded) (Lit 0) outOffset+    ]+  where+    action s f = (abiKeccak s, f (abiKeccak s))++-- * General call implementation ("delegateCall")+-- note that the continuation is ignored in the precompile case+delegateCall+  :: (VMOps t, ?op :: Word8)+  => Contract+  -> Gas t+  -> Expr EAddr+  -> Expr EAddr+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> Expr EWord+  -> [Expr EWord]+  -> (Expr EAddr -> EVM t s ())+  -> EVM t s ()+delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue+  | isPrecompileAddr xTo+      = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $+          \(xTo', xContext') ->+            precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs+  | xTo == cheatCode = do+      assign (#state % #stack) xs+      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+  | otherwise =+      callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $+        \xGas -> do+          vm0 <- get+          fetchAccount xTo $ \target -> case target.code of+              UnknownCode _ -> do+                pc <- use (#state % #pc)+                partial $ UnexpectedSymbolicArg pc "call target has unknown code" (wrap [xTo])+              _ -> do+                burn' xGas $ do+                  calldata <- readMemory xInOffset xInSize+                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)+                  let newContext = CallContext+                                    { target    = xTo+                                    , context   = xContext+                                    , offset    = xOutOffset+                                    , size      = xOutSize+                                    , codehash  = target.codehash+                                    , callreversion = vm0.env.contracts+                                    , subState  = vm0.tx.substate+                                    , abi+                                    , calldata+                                    }+                  pushTrace (FrameTrace newContext)+                  next+                  vm1 <- get++                  pushTo #frames $ Frame+                    { state = vm1.state { stack = xs }+                    , context = newContext+                    }++                  let clearInitCode = \case+                        (InitCode _ _) -> InitCode mempty mempty+                        a -> a++                  newMemory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+                  zoom #state $ do+                    assign #gas xGas+                    assign #pc 0+                    assign #code (clearInitCode target.code)+                    assign #codeContract xTo+                    assign #stack mempty+                    assign #memory newMemory+                    assign #memorySize 0+                    assign #returndata mempty+                    assign #calldata calldata+                  continue xTo++-- -- * Contract creation++-- EIP 684+collision :: Maybe Contract -> Bool+collision c' = case c' of+  Just c -> c.nonce /= Just 0 || case c.code of+    RuntimeCode (ConcreteRuntimeCode "") -> False+    RuntimeCode (SymbolicRuntimeCode b) -> not $ null b+    _ -> True+  Nothing -> False++create :: forall t s. (?op :: Word8, VMOps t)+  => Expr EAddr -> Contract+  -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s ()+create self this xSize xGas xValue xs newAddr initCode = do+  vm0 <- get+  if xSize > Lit (vm0.block.maxCodeSize * 2)+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize+  else if this.nonce == Just maxBound+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace NonceOverflow+    next+  else if length vm0.frames >= 1024+  then do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    pushTrace $ ErrorTrace CallDepthLimitReached+    next+  else if collision $ Map.lookup newAddr vm0.env.contracts+  then burn' xGas $ do+    assign (#state % #stack) (Lit 0 : xs)+    assign (#state % #returndata) mempty+    modifying (#env % #contracts % ix self % #nonce) (fmap ((+) 1))+    next+  -- do we have enough balance+  else branch (Expr.gt xValue this.balance) $ \case+      True -> do+        assign (#state % #stack) (Lit 0 : xs)+        assign (#state % #returndata) mempty+        pushTrace $ ErrorTrace $ BalanceTooLow xValue this.balance+        next+        touchAccount self+        touchAccount newAddr+      -- are we overflowing the nonce+      False -> burn' xGas $ do+        case parseInitCode initCode of+          Nothing ->+            partial $ UnexpectedSymbolicArg vm0.state.pc "initcode must have a concrete prefix" []+          Just c -> do+            let+              newContract = initialContract c+              newContext  =+                CreationContext { address   = newAddr+                                , codehash  = newContract.codehash+                                , createreversion = vm0.env.contracts+                                , substate  = vm0.tx.substate+                                }++            zoom (#env % #contracts) $ do+              oldAcc <- use (at newAddr)+              let oldBal = maybe (Lit 0) (.balance) oldAcc++              assign (at newAddr) (Just (newContract & #balance .~ oldBal))+              modifying (ix self % #nonce) (fmap ((+) 1))++            let+              resetStorage :: Expr Storage -> Expr Storage+              resetStorage = \case+                  ConcreteStore _ -> ConcreteStore mempty+                  AbstractStore a Nothing -> AbstractStore a Nothing+                  SStore _ _ p -> resetStorage p+                  AbstractStore _ (Just _) -> internalError "unexpected logical store in EVM.hs"+                  GVar _  -> internalError "unexpected global variable"++            modifying (#env % #contracts % ix newAddr % #storage) resetStorage+            modifying (#env % #contracts % ix newAddr % #origStorage) resetStorage++            transfer self newAddr xValue++            pushTrace (FrameTrace newContext)+            next+            vm1 <- get+            pushTo #frames $ Frame+              { context = newContext+              , state   = vm1.state { stack = xs }+              }++            state :: FrameState t s <- lift blankState+            assign #state $ state+              { contract     = newAddr+              , codeContract = newAddr+              , code         = c+              , callvalue    = xValue+              , caller       = self+              , gas          = xGas+              }++-- | Parses a raw Buf into an InitCode+--+-- solidity implements constructor args by appending them to the end of+-- the initcode. we support this internally by treating initCode as a+-- concrete region (initCode) followed by a potentially symbolic region+-- (arguments).+--+-- when constructing a contract that has symbolic constructor args, we+-- need to apply some heuristics to convert the (unstructured) initcode+-- in memory into this structured representation. The (unsound, bad,+-- hacky) way that we do this, is by: looking for the first potentially+-- symbolic byte in the input buffer and then splitting it there into code / data.+parseInitCode :: Expr Buf -> Maybe ContractCode+parseInitCode (ConcreteBuf b) = Just (InitCode b mempty)+parseInitCode buf = if V.null conc+                    then Nothing+                    else Just $ InitCode (BS.pack $ V.toList conc) sym+  where+    conc = Expr.concretePrefix buf+    -- unsafeInto: findIndex will always be positive+    sym = Expr.drop (unsafeInto (V.length conc)) buf++-- | Replace a contract's code, like when CREATE returns+-- from the constructor code.+replaceCode :: Expr EAddr -> ContractCode -> EVM t s ()+replaceCode target newCode =+  zoom (#env % #contracts % at target) $+    get >>= \case+      Just now -> case now.code of+        InitCode _ _ ->+          put . Just $+            ((initialContract newCode) :: Contract)+              { balance = now.balance+              , nonce = now.nonce+              , storage = now.storage+              }+        RuntimeCode _ ->+          internalError $ "Can't replace code of deployed contract " <> show target+        UnknownCode _ ->+          internalError "Can't replace unknown code"+      Nothing ->+        internalError "Can't replace code of nonexistent contract"++replaceCodeOfSelf :: ContractCode -> EVM t s ()+replaceCodeOfSelf newCode = do+  vm <- get+  replaceCode vm.state.contract newCode++resetState :: VMOps t => EVM t s ()+resetState = do+  state <- lift blankState+  modify' $ \vm -> vm { result = Nothing, frames = [], state }++-- * VM error implementation++vmError :: VMOps t => EvmError -> EVM t s ()+vmError e = finishFrame (FrameErrored e)++wrap :: Typeable a => [Expr a] -> [SomeExpr]+wrap = fmap SomeExpr++underrun :: VMOps t => EVM t s ()+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 EvmError -- ^ Any other error+  deriving Show++-- | This function defines how to pop the current stack frame in either of+-- the ways specified by 'FrameResult'.+--+-- It also handles the case when the current stack frame is the only one;+-- in this case, we set the final '_result' of the VM execution.+finishFrame :: VMOps t => FrameResult -> EVM t s ()+finishFrame how = do+  oldVm <- get++  case oldVm.frames of+    -- Is the current frame the only one?+    [] -> do+      case how of+          FrameReturned output -> assign #result . Just $ VMSuccess output+          FrameReverted buffer -> assign #result . Just $ VMFailure (Revert buffer)+          FrameErrored e       -> assign #result . Just $ VMFailure e+      finalize++    -- Are there some remaining frames?+    nextFrame : remainingFrames -> do++      -- Insert a debug trace.+      insertTrace $+        case how of+          FrameErrored e ->+            ErrorTrace e+          FrameReverted e ->+            ErrorTrace (Revert e)+          FrameReturned output ->+            ReturnTrace output nextFrame.context+      -- Pop to the previous level of the debug trace stack.+      popTrace++      -- Pop the top frame.+      assign #frames remainingFrames+      -- Install the state of the frame to which we shall return.+      assign #state nextFrame.state++      -- Now dispatch on whether we were creating or calling,+      -- and whether we shall return, revert, or internalError(six cases).+      case nextFrame.context of++        -- Were we calling?+        CallContext _ _ outOffset outSize _ _ _ reversion substate' -> do++          -- Excerpt K.1. from the yellow paper:+          -- K.1. Deletion of an Account Despite Out-of-gas.+          -- At block 2675119, in the transaction 0xcf416c536ec1a19ed1fb89e4ec7ffb3cf73aa413b3aa9b77d60e4fd81a4296ba,+          -- an account at address 0x03 was called and an out-of-gas occurred during the call.+          -- Against the equation (197), this added 0x03 in the set of touched addresses, and this transaction turned σ[0x03] into ∅.++          -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert+          touched <- use (#tx % #substate % #touchedAccounts)++          let+            substate'' = over #touchedAccounts (maybe id cons (find (LitAddr 3 ==) touched)) substate'+            revertContracts = assign (#env % #contracts) reversion+            revertSubstate  = assign (#tx % #substate) substate''++          case how of+            -- Case 1: Returning from a call?+            FrameReturned output -> do+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize outOffset+              reclaimRemainingGasAllowance oldVm+              push 1++            -- Case 2: Reverting during a call?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) output+              copyCallBytesToMemory output outSize outOffset+              reclaimRemainingGasAllowance oldVm+              push 0++            -- Case 3: Error during a call?+            FrameErrored _ -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) mempty+              push 0+        -- Or were we creating?+        CreationContext _ _ reversion substate' -> do+          creator <- use (#state % #contract)+          let+            createe = oldVm.state.contract+            revertContracts = assign (#env % #contracts) reversion'+            revertSubstate  = assign (#tx % #substate) substate'++            -- persist the nonce through the reversion+            reversion' = (Map.adjust (over #nonce (fmap ((+) 1))) creator) reversion++          case how of+            -- Case 4: Returning during a creation?+            FrameReturned output -> do+              let onContractCode contractCode = do+                    replaceCode createe contractCode+                    assign (#state % #returndata) mempty+                    reclaimRemainingGasAllowance oldVm+                    pushAddr createe+              case output of+                ConcreteBuf bs ->+                  onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)+                _ ->+                  case Expr.toList output of+                    Nothing -> partial $+                      UnexpectedSymbolicArg+                        oldVm.state.pc+                        "runtime code cannot have an abstract length"+                        (wrap [output])+                    Just newCode -> do+                      onContractCode $ RuntimeCode (SymbolicRuntimeCode newCode)++            -- Case 5: Reverting during a creation?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) output+              reclaimRemainingGasAllowance oldVm+              push 0++            -- Case 6: Error during a creation?+            FrameErrored _ -> do+              revertContracts+              revertSubstate+              assign (#state % #returndata) mempty+              push 0+++-- * Memory helpers++accessUnboundedMemoryRange+  :: VMOps t => Word64+  -> Word64+  -> EVM t s ()+  -> EVM t s ()+accessUnboundedMemoryRange _ 0 continue = continue+accessUnboundedMemoryRange f l continue = do+  m0 <- use (#state % #memorySize)+  fees <- gets (.block.schedule)+  let m1 = 32 * ceilDiv (max m0 (f + l)) 32+  burn (memoryCost fees m1 - memoryCost fees m0) $ do+    assign (#state % #memorySize) m1+    continue++accessMemoryRange+  :: VMOps t+  => Expr EWord+  -> Expr EWord+  -> EVM t s ()+  -> EVM t s ()+accessMemoryRange _ (Lit 0) continue = continue+accessMemoryRange (Lit offs) (Lit sz) continue =+  case (,) <$> toWord64 offs <*> toWord64 sz of+    Nothing -> vmError IllegalOverflow+    Just (offs64, sz64) ->+      if offs64 + sz64 < sz64+        then vmError IllegalOverflow+        -- we need to limit these to <256MB because otherwise we could run out of memory+        -- in e.g. OpCalldatacopy and subsequent memory allocation when running with abstract gas.+        -- In these cases, the system would try to allocate a large (but <2**64 bytes) memory+        -- that leads to out-of-heap. Real-world scenarios cannot allocate 256MB of memory due to gas+        else if offs64 >= 0x0fffffff || sz64 >= 0x0fffffff+             then vmError IllegalOverflow+             else accessUnboundedMemoryRange offs64 sz64 continue+-- we just ignore gas if we get symbolic inputs+accessMemoryRange _ _ continue = continue++accessMemoryWord+  :: VMOps t => Expr EWord -> EVM t s () -> EVM t s ()+accessMemoryWord x = accessMemoryRange x (Lit 32)++copyBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM t s ()+copyBytesToMemory bs size srcOffset memOffset =+  if size == Lit 0 then noop+  else do+    gets (.state.memory) >>= \case+      ConcreteMemory mem ->+        case (bs, size, srcOffset, memOffset) of+          (ConcreteBuf b, Lit size', Lit srcOffset', Lit memOffset') -> do+            let src =+                  if srcOffset' >= unsafeInto (BS.length b) then+                    BS.replicate (unsafeInto size') 0+                  else+                    BS.take (unsafeInto size') $+                    padRight (unsafeInto size') $+                    BS.drop (unsafeInto srcOffset') b++            writeMemory mem (unsafeInto memOffset') src+          _ -> do+            -- copy out and move to symbolic memory+            buf <- freezeMemory mem+            assign (#state % #memory) $+              SymbolicMemory $ copySlice srcOffset memOffset size bs buf+      SymbolicMemory mem ->+        assign (#state % #memory) $+          SymbolicMemory $ copySlice srcOffset memOffset size bs mem++copyCallBytesToMemory+  :: Expr Buf -> Expr EWord -> Expr EWord -> EVM t s ()+copyCallBytesToMemory bs size yOffset =+  copyBytesToMemory bs (Expr.min size (bufLength bs)) (Lit 0) yOffset++readMemory :: Expr EWord -> Expr EWord -> EVM t s (Expr Buf)+readMemory offset' size' = do+  vm <- get+  case vm.state.memory of+    ConcreteMemory mem -> do+      case (offset', size') of+        (Lit offset, Lit size) -> do+          let memSize :: Word64 = unsafeInto (VUnboxed.Mutable.length mem)+          if size > Expr.maxBytes ||+             offset + size > Expr.maxBytes ||+             offset >= into memSize then+            -- reads past memory are all zeros+            pure $ ConcreteBuf $ BS.replicate (unsafeInto size) 0+          else do+            let pastEnd = (unsafeInto offset + unsafeInto size) - unsafeInto memSize+            let fromMemSize = if pastEnd > 0 then unsafeInto size - pastEnd else unsafeInto size++            buf <- VUnboxed.freeze $ VUnboxed.Mutable.slice (unsafeInto offset) fromMemSize mem+            let dataFromMem = BS.pack $ VUnboxed.toList buf+            pure $ ConcreteBuf $ dataFromMem <> BS.replicate pastEnd 0+        _ -> do+          buf <- freezeMemory mem+          pure $ copySlice offset' (Lit 0) size' buf mempty+    SymbolicMemory mem ->+      pure $ copySlice offset' (Lit 0) size' mem mempty++-- * Tracing++withTraceLocation :: TraceData -> EVM t s Trace+withTraceLocation x = do+  vm <- get+  let this = fromJust $ currentContract vm+  pure Trace+    { tracedata = x+    , contract = this+    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc+    }++pushTrace :: TraceData -> EVM t s ()+pushTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.children $ Zipper.insert (Node trace []) t++insertTrace :: TraceData -> EVM t s ()+insertTrace x = do+  trace <- withTraceLocation x+  modifying #traces $+    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t++popTrace :: EVM t s ()+popTrace =+  modifying #traces $+    \t -> case Zipper.parent t of+            Nothing -> internalError "internal internalError(trace root)"+            Just t' -> Zipper.nextSpace t'++zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a+zipperRootForest z =+  case Zipper.parent z of+    Nothing -> Zipper.toForest z+    Just z' -> zipperRootForest (Zipper.nextSpace z')++traceForest :: VM t s -> Forest Trace+traceForest vm = zipperRootForest vm.traces++traceForest' :: Expr End -> Forest Trace+traceForest' (Success _ (Traces f _) _ _) = f+traceForest' (Partial _ (Traces f _) _) = f+traceForest' (Failure _ (Traces f _) _) = f+traceForest' (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceForest' (GVar {}) = internalError"Internal Error: Unexpected GVar"++traceContext :: Expr End -> Map (Expr EAddr) Contract+traceContext (Success _ (Traces _ c) _ _) = c+traceContext (Partial _ (Traces _ c) _) = c+traceContext (Failure _ (Traces _ c) _) = c+traceContext (ITE {}) = internalError"Internal Error: ITE does not contain a trace"+traceContext (GVar {}) = internalError"Internal Error: Unexpected GVar"++traceTopLog :: [Expr Log] -> EVM t s ()+traceTopLog [] = noop+traceTopLog ((LogEntry addr bytes topics) : _) = do+  trace <- withTraceLocation (EventTrace addr bytes topics)+  modifying #traces $+    \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)+traceTopLog ((GVar _) : _) = internalError "unexpected global variable"++-- * Stack manipulation++push :: W256 -> EVM t s ()+push = pushSym . Lit++pushSym :: Expr EWord -> EVM t s ()+pushSym x = #state % #stack %= (x :)++pushAddr :: Expr EAddr -> EVM t s ()+pushAddr (LitAddr x) = #state % #stack %= (Lit (into x) :)+pushAddr x@(SymAddr _) = #state % #stack %= (WAddr x :)+pushAddr (GVar _) = internalError "Unexpected GVar"++stackOp1+  :: (?op :: Word8, VMOps t)+  => Word64+  -> (Expr EWord -> Expr EWord)+  -> EVM t s ()+stackOp1 cost f =+  use (#state % #stack) >>= \case+    x:xs ->+      burn cost $ do+        next+        let !y = f x+        #state % #stack .= y : xs+    _ ->+      underrun++stackOp2+  :: (?op :: Word8, VMOps t)+  => Word64+  -> (Expr EWord -> Expr EWord -> Expr EWord)+  -> EVM t s ()+stackOp2 cost f =+  use (#state % #stack) >>= \case+    x:y:xs ->+      burn cost $ do+        next+        #state % #stack .= f x y : xs+    _ ->+      underrun++stackOp3+  :: (?op :: Word8, VMOps t)+  => Word64+  -> (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord)+  -> EVM t s ()+stackOp3 cost f =+  use (#state % #stack) >>= \case+    x:y:z:xs ->+      burn cost $ do+      next+      (#state % #stack) .= f x y z : xs+    _ ->+      underrun++-- * Bytecode data functions++checkJump :: VMOps t => Int -> [Expr EWord] -> EVM t s ()+checkJump x xs = noJumpIntoInitData x $ do+  vm <- get+  case isValidJumpDest vm x of+    True -> do+      #state % #stack .= xs+      #state % #pc .= x+    False -> vmError BadJumpDestination++-- fails with partial if we're trying to jump into the symbolic region of an `InitCode`+noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t s ()+noJumpIntoInitData idx cont = do+  vm <- get+  case vm.state.code of+    -- init code is totally concrete, so we don't return partial if we're+    -- jumping beyond the range of `ops`+    InitCode _ (ConcreteBuf "") -> cont+    -- init code has a symbolic region, so check if we're trying to jump into+    -- the symbolic region and return partial if we are+    InitCode ops _ -> if idx > BS.length ops+                      then partial $ JumpIntoSymbolicCode vm.state.pc idx+                      else cont+    -- we're not executing init code, so nothing to check here+    _ -> cont++isValidJumpDest :: VM t s -> Int -> Bool+isValidJumpDest vm x = let+    code = vm.state.code+    self = vm.state.codeContract+    contract = fromMaybe+      (internalError "self not found in current contracts")+      (Map.lookup self vm.env.contracts)+    op = case code of+      UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"+      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.! x))++opSize :: Word8 -> Int+opSize x | x >= 0x60 && x <= 0x7f = into x - 0x60 + 2+opSize _                          = 1++--  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 -> SV.Vector Int+mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code"+mkOpIxMap (InitCode conc _)+  = 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+      in m >> pure v+      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 >> SV.write v i j)+        go v (1, !i, !j, !m) _ =+          {- 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 >> SV.write v i j)+        go v (n, !i, !j, !m) _ =+          {- 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))+  = 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 maybeLitByte x of+          Just x' -> if x' >= 0x60 && x' <= 0x7f+            -- start of PUSH op --+                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)+            -- other data --+                     else (0,             i + 1, j + 1, m >> SV.write v i j)+          _ -> internalError $ "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 >> SV.write v i j)+        go v (n, !i, !j, !m) _ =+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)+++vmOp :: VM t s -> Maybe Op+vmOp vm =+  let i  = vm ^. #state % #pc+      code' = vm ^. #state % #code+      (op, pushdata) = case code' of+        UnknownCode _ -> internalError "cannot get op from unknown code"+        InitCode xs' _ ->+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')+        RuntimeCode (ConcreteRuntimeCode xs') ->+          (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')+        RuntimeCode (SymbolicRuntimeCode xs') ->+          ( fromMaybe (internalError "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)++vmOpIx :: VM t s -> Maybe Int+vmOpIx vm =+  do self <- currentContract vm+     self.opIxMap SV.!? vm.state.pc++-- Maps operation indices into a pair of (bytecode index, operation)+mkCodeOps :: ContractCode -> V.Vector (Int, Op)+mkCodeOps contractCode =+  let l = case contractCode of+            UnknownCode _ -> internalError "Cannot make codeOps for unknown code"+            InitCode bytes _ ->+              LitByte <$> (BS.unpack bytes)+            RuntimeCode (ConcreteRuntimeCode ops) ->+              LitByte <$> (BS.unpack $ stripBytecodeMetadata ops)+            RuntimeCode (SymbolicRuntimeCode ops) ->+              stripBytecodeMetadataSym $ V.toList ops+  in V.fromList . toList $ go 0 l+  where+    go !i !xs =+      case uncons xs of+        Nothing ->+          mempty+        Just (x, xs') ->+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x+              j = opSize x'+          in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)++-- * Gas cost calculation helpers++concreteModexpGasFee :: ByteString -> Word64+concreteModexpGasFee input =+  if lenb < into (maxBound :: Word32) &&+     (lene < into (maxBound :: Word32) || (lenb == 0 && lenm == 0)) &&+     lenm < into (maxBound :: Word64)+  then+    max 200 ((multiplicationComplexity * iterCount) `div` 3)+  else+    maxBound -- TODO: this is not 100% correct, return Nothing on overflow+  where+    (lenb, lene, lenm) = parseModexpLength input+    ez = isZero (96 + lenb) lene input+    e' = word $ LS.toStrict $+      lazySlice (96 + lenb) (min 32 lene) input+    nwords :: Word64+    nwords = ceilDiv (unsafeInto $ max lenb lenm) 8+    multiplicationComplexity = nwords * nwords+    iterCount' :: Word64+    iterCount' | lene <= 32 && ez = 0+               | lene <= 32 = unsafeInto (log2 e')+               | e' == 0 = 8 * (unsafeInto lene - 32)+               | otherwise = unsafeInto (log2 e') + 8 * (unsafeInto lene - 32)+    iterCount = max iterCount' 1++-- Gas cost of precompiles+costOfPrecompile :: FeeSchedule Word64 -> Addr -> Expr Buf -> Word64+costOfPrecompile (FeeSchedule {..}) precompileAddr input =+  let errorDynamicSize = internalError "precompile input cannot have a dynamic size"+      inputLen = case input of+                   ConcreteBuf bs -> unsafeInto $ BS.length bs+                   AbstractBuf _ -> errorDynamicSize+                   buf -> case bufLength buf of+                            Lit l -> unsafeInto l -- TODO: overflow+                            _ -> errorDynamicSize+  in case precompileAddr of+    -- ECRECOVER+    0x1 -> 3000+    -- SHA2-256+    0x2 -> (((inputLen + 31) `div` 32) * 12) + 60+    -- RIPEMD-160+    0x3 -> (((inputLen + 31) `div` 32) * 120) + 600+    -- IDENTITY+    0x4 -> (((inputLen + 31) `div` 32) * 3) + 15+    -- MODEXP+    0x5 -> case input of+             ConcreteBuf i -> concreteModexpGasFee i+             _ -> internalError "Unsupported symbolic modexp gas calc "+    -- ECADD+    0x6 -> g_ecadd+    -- ECMUL+    0x7 -> g_ecmul+    -- ECPAIRING+    0x8 -> (inputLen `div` 192) * g_pairing_point + g_pairing_base+    -- BLAKE2+    0x9 -> case input of+             ConcreteBuf i -> g_fround * (unsafeInto $ asInteger $ lazySlice 0 4 i)+             _ -> internalError "Unsupported symbolic blake2 gas calc"+    _ -> internalError $ "unimplemented precompiled contract " ++ show precompileAddr++-- Gas cost of memory expansion+memoryCost :: FeeSchedule Word64 -> Word64 -> Word64+memoryCost FeeSchedule{..} byteCount =+  let+    wordCount = ceilDiv byteCount 32+    linearCost = g_memory * wordCount+    quadraticCost = div (wordCount * wordCount) 512+  in+    linearCost + quadraticCost++hashcode :: ContractCode -> Expr EWord+hashcode (UnknownCode a) = CodeHash a+hashcode (InitCode ops args) = keccak $ (ConcreteBuf ops) <> args+hashcode (RuntimeCode (ConcreteRuntimeCode ops)) = keccak (ConcreteBuf ops)+hashcode (RuntimeCode (SymbolicRuntimeCode ops)) = keccak . Expr.fromList $ ops++-- | The length of the code ignoring any constructor args.+-- This represents the region that can contain executable opcodes+opslen :: ContractCode -> Int+opslen (UnknownCode _) = internalError "Cannot produce concrete opslen for unknown code"+opslen (InitCode ops _) = BS.length ops+opslen (RuntimeCode (ConcreteRuntimeCode ops)) = BS.length ops+opslen (RuntimeCode (SymbolicRuntimeCode ops)) = length ops++-- | The length of the code including any constructor args.+-- This can return an abstract value+codelen :: ContractCode -> Expr EWord+codelen (UnknownCode a) = CodeSize a+codelen c@(InitCode {}) = case toBuf c of+  Just b -> bufLength b+  Nothing -> internalError "impossible"+-- these are never going to be negative so unsafeInto is fine here+codelen (RuntimeCode (ConcreteRuntimeCode ops)) = Lit . unsafeInto $ BS.length ops+codelen (RuntimeCode (SymbolicRuntimeCode ops)) = Lit . unsafeInto $ length ops++toBuf :: ContractCode -> Maybe (Expr Buf)+toBuf (UnknownCode _) = Nothing+toBuf (InitCode ops args) = Just $ ConcreteBuf ops <> args+toBuf (RuntimeCode (ConcreteRuntimeCode ops)) = Just $ ConcreteBuf ops+toBuf (RuntimeCode (SymbolicRuntimeCode ops)) = Just $ Expr.fromList ops++codeloc :: EVM t s CodeLocation+codeloc = do+  vm <- get+  pure (vm.state.contract, vm.state.pc)++createAddress :: Expr EAddr -> Maybe W64 -> EVM t s (Expr EAddr)+createAddress (LitAddr a) (Just n) = pure $ Concrete.createAddress a n+createAddress (GVar _) _ = internalError "Unexpected GVar"+createAddress _ _ = freshSymAddr++create2Address :: Expr EAddr -> W256 -> ByteString -> EVM t s (Expr EAddr)+create2Address (LitAddr a) s b = pure $ Concrete.create2Address a s b+create2Address (SymAddr _) _ _ = freshSymAddr+create2Address (GVar _) _ _ = internalError "Unexpected GVar"++freshSymAddr :: EVM t s (Expr EAddr)+freshSymAddr = do+  modifying (#env % #freshAddresses) (+ 1)+  n <- use (#env % #freshAddresses)+  pure $ SymAddr ("freshSymAddr" <> (pack $ show n))++isPrecompileAddr :: Expr EAddr -> Bool+isPrecompileAddr = \case+  LitAddr a -> 0x0 < a && a <= 0x09+  SymAddr _ -> False+  GVar _ -> internalError "Unexpected GVar"++-- * Arithmetic++ceilDiv :: (Num a, Integral a) => a -> a -> a+ceilDiv m n = div (m + n - 1) n++allButOne64th :: (Num a, Integral a) => a -> a+allButOne64th n = n - div n 64++log2 :: FiniteBits b => b -> Int+log2 x = finiteBitSize x - 1 - countLeadingZeros x++writeMemory :: MutableMemory s -> Int -> ByteString -> EVM t s ()+writeMemory memory offset buf = do+  memory' <- expandMemory (offset + BS.length buf)+  mapM_ (uncurry (VUnboxed.Mutable.write memory'))+        (zip [offset..] (BS.unpack buf))+  where+  expandMemory targetSize = do+    let toAlloc = targetSize - VUnboxed.Mutable.length memory+    if toAlloc > 0 then do+      memory' <- VUnboxed.Mutable.grow memory toAlloc+      assign (#state % #memory) (ConcreteMemory memory')+      pure memory'+    else+      pure memory++freezeMemory :: MutableMemory s -> EVM t s (Expr Buf)+freezeMemory memory =+  ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.freeze memory+++instance VMOps Symbolic where+  burn' _ continue = continue+  burnExp _ continue = continue+  burnSha3 _ continue = continue+  burnCalldatacopy _ continue = continue+  burnCodecopy _ continue = continue+  burnExtcodecopy _ _ continue = continue+  burnReturndatacopy _ continue = continue+  burnLog _ _ continue = continue++  initialGas = ()+  ensureGas _ continue = continue+  gasTryFrom _ = Right ()+  costOfCreate _ _ _ _ = ((), ())+  costOfCall _ _ _ _ _ _ continue = continue 0 0+  reclaimRemainingGasAllowance _ = pure ()+  payRefunds = pure ()+  pushGas = do+    modifying (#env % #freshGasVals) (+ 1)+    n <- use (#env % #freshGasVals)+    pushSym $ Expr.Gas n+  enoughGas _ _ = True+  subGas _ _ = ()+  toGas _ = ()+  whenSymbolicElse a _ = a++  partial e = assign #result (Just (Unfinished e))+  branch cond continue = do+    loc <- codeloc+    pathconds <- use #constraints+    query $ PleaseAskSMT cond pathconds (choosePath loc)+    where+      condSimp = Expr.simplify cond+      condSimpConc = Expr.concKeccakSimpExpr condSimp+      choosePath loc (Case v) = do+        assign #result Nothing+        pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0)+                                   else Expr.simplifyProp (condSimpConc .== Lit 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, stack))+        continue v+      -- Both paths are possible; we ask for more input+      choosePath loc Unknown =+        choose . PleaseChoosePath condSimp $ choosePath loc . Case++instance VMOps Concrete where+  burn' n continue = do+    available <- use (#state % #gas)+    if n <= available+      then do+        #state % #gas %= (subtract n)+        #burned %= (+ n)+        continue+      else+        vmError (OutOfGas available n)++  burnExp (forceLit -> exponent) continue = do+    FeeSchedule {..} <- gets (.block.schedule)+    let cost = if exponent == 0+          then g_exp+          else g_exp + g_expbyte * unsafeInto (ceilDiv (1 + log2 exponent) 8)+    burn cost continue++  burnSha3 (forceLit -> xSize) continue = do+    FeeSchedule {..} <- gets (.block.schedule)+    burn (g_sha3 + g_sha3word * ceilDiv (unsafeInto xSize) 32) continue++  burnCalldatacopy (forceLit -> xSize) continue = do+    FeeSchedule {..} <- gets (.block.schedule)+    burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue++  burnCodecopy (forceLit -> n) continue =+    case tryFrom n of+      Left _ -> vmError IllegalOverflow+      Right n' -> do+        FeeSchedule {..} <- gets (.block.schedule)+        if n' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then+          burn (g_verylow + g_copy * ceilDiv (unsafeInto n) 32) continue+        else vmError IllegalOverflow++  burnExtcodecopy extAccount (forceLit -> codeSize) continue = do+    FeeSchedule {..} <- gets (.block.schedule)+    acc <- accessAccountForGas extAccount+    let cost = if acc then g_warm_storage_read else g_cold_account_access+    burn (cost + g_copy * ceilDiv (unsafeInto codeSize) 32) continue++  burnReturndatacopy (forceLit -> xSize) continue = do+    FeeSchedule {..} <- gets (.block.schedule)+    burn (g_verylow + g_copy * ceilDiv (unsafeInto xSize) 32) continue++  burnLog (forceLit -> xSize) n continue = do+    case tryFrom xSize of+      Right sz -> do+        FeeSchedule {..} <- gets (.block.schedule)+        burn (g_log + g_logdata * sz + (into n) * g_logtopic) continue+      _ -> vmError IllegalOverflow++  initialGas = 0++  ensureGas amount continue = do+    availableGas <- use (#state % #gas)++    if availableGas <= amount then+      vmError (OutOfGas availableGas amount)+    else continue++  gasTryFrom (forceLit -> w256) =+    case tryFrom w256 of+      Left _ -> Left ()+      Right a -> Right a++  -- Gas cost of create, including hash cost if needed+  costOfCreate (FeeSchedule {..}) availableGas size hashNeeded = (createCost, initGas)+    where+      byteCost   = if hashNeeded then g_sha3word + g_initcodeword else g_initcodeword+      createCost = g_create + codeCost+      codeCost   = byteCost * (ceilDiv (unsafeInto (forceLit size)) 32)+      initGas    = allButOne64th (availableGas - createCost)++  -- Gas cost function for CALL, transliterated from the Yellow Paper.+  costOfCall (FeeSchedule {..}) recipientExists (forceLit -> xValue) availableGas xGas target continue = do+    acc <- accessAccountForGas target+    let call_base_gas = if acc then g_warm_storage_read else g_cold_account_access+        c_new = if not recipientExists && xValue /= 0+              then g_newaccount+              else 0+        c_xfer = if xValue /= 0  then g_callvalue else 0+        c_extra = call_base_gas + c_xfer + c_new+        c_gascap =  if availableGas >= c_extra+                    then min xGas (allButOne64th (availableGas - c_extra))+                    else xGas+        c_callgas = if xValue /= 0 then c_gascap + g_callstipend else c_gascap+    let (cost, gas') = (c_gascap + c_extra, c_callgas)+    continue cost gas'++  -- When entering a call, the gas allowance is counted as burned+  -- in advance; this unburns the remainder and adds it to the+  -- parent frame.+  reclaimRemainingGasAllowance oldVm = do+    let remainingGas = oldVm.state.gas+    modifying #burned (subtract remainingGas)+    modifying (#state % #gas) (+ remainingGas)++  payRefunds = do+    -- compute and pay the refund to the caller and the+    -- corresponding payment to the miner+    block        <- use #block+    tx           <- use #tx+    gasRemaining <- use (#state % #gas)++    let+      sumRefunds   = sum (snd <$> tx.substate.refunds)+      gasUsed      = tx.gaslimit - gasRemaining+      cappedRefund = min (quot gasUsed 5) sumRefunds+      originPay    = (into $ gasRemaining + cappedRefund) * tx.gasprice+      minerPay     = tx.priorityFee * (into gasUsed)++    modifying (#env % #contracts)+       (Map.adjust (over #balance (Expr.add (Lit originPay))) tx.origin)+    modifying (#env % #contracts)+       (Map.adjust (over #balance (Expr.add (Lit minerPay))) block.coinbase)++  pushGas = do+    vm <- get+    push (into vm.state.gas)++  enoughGas cost gasCap = cost <= gasCap++  subGas gasCap cost = gasCap - cost++  toGas = id++  whenSymbolicElse _ a = a++  partial _ = internalError "won't happen during concrete exec"++  branch (forceLit -> cond) continue = continue (cond > 0)++-- Create symbolic VM from concrete VM+symbolify :: VM Concrete s -> VM Symbolic s+symbolify vm =+  vm { result = symbolifyResult <$> vm.result+     , state  = symbolifyFrameState vm.state+     , frames = symbolifyFrame <$> vm.frames+     , burned = ()+     }++symbolifyFrameState :: FrameState Concrete s -> FrameState Symbolic s+symbolifyFrameState state = state { gas = () }++symbolifyFrame :: Frame Concrete s -> Frame Symbolic s+symbolifyFrame frame = frame { state = symbolifyFrameState frame.state }++symbolifyResult :: VMResult Concrete s -> VMResult Symbolic s+symbolifyResult result =+  case result of+    HandleEffect _ -> internalError "shouldn't happen"+    VMFailure e -> VMFailure e+    VMSuccess b -> VMSuccess b++forceLit :: Expr EWord -> W256+forceLit (Lit w) = w+forceLit _ = internalError "concrete vm, shouldn't ever happen"++burn :: VMOps t => Word64 -> EVM t s () -> EVM t s ()+burn = burn' . toGas

@@ -24,7 +24,7 @@    Nested sequences are encoded recursively with no special treatment. -  Calldata args are encoded as heterogenous sequences sans length prefix.+  Calldata args are encoded as heterogeneous sequences sans length prefix.  -} module EVM.ABI

@@ -0,0 +1,123 @@+{-|+Module      : Effects+Description : Domain specific effects++This module contains custom app specific mtl style effects for hevm+These are written in the style of the ReaderT over IO pattern [1].+Right now we only have a single `ReadConfig` effect, but over time hope to+migrate most usages of IO into custom effects here.++This framework would allow us to have multiple interpretations for effects+(e.g. a pure version for tests), but for now we interpret everything in IO+only.++[1]: https://www.fpcomplete.com/blog/readert-design-pattern/+-}++{-# Language RankNTypes #-}+{-# Language FlexibleInstances #-}+{-# Language KindSignatures #-}+{-# Language DataKinds #-}+{-# Language GADTs #-}+{-# Language DerivingStrategies #-}+{-# Language DuplicateRecordFields #-}+{-# Language NoFieldSelectors #-}+{-# Language ConstraintKinds #-}++module EVM.Effects where++import Control.Monad.Reader+import Control.Monad.IO.Unlift+import EVM.Dapp (DappInfo)+import EVM.Types (VM(..))+import Control.Monad.ST (RealWorld)+import Data.Text (Text)+import Data.Text.IO qualified as T+import System.IO (stderr)+import EVM.Format (showTraceTree)+import EVM (traceForest)+++-- Abstract Effects --------------------------------------------------------------------------------+-- Here we define the abstract interface for the effects that we wish to model+++-- Read from global config+class Monad m => ReadConfig m where+  readConfig ::  m Config++data Config = Config+  { dumpQueries     :: Bool+  , dumpExprs       :: Bool+  , dumpEndStates   :: Bool+  , debug           :: Bool+  , abstRefineArith :: Bool+  , abstRefineMem   :: Bool+  , dumpTrace       :: Bool+  , numCexFuzz      :: Integer+   -- Used to debug fuzzer in test.hs. It disables the SMT solver+   -- and uses the fuzzer ONLY to try to find a counterexample.+   -- Returns Unknown if the Cex cannot be found via fuzzing+  , onlyCexFuzz     :: Bool+  }+  deriving (Show, Eq)++defaultConfig :: Config+defaultConfig = Config+  { dumpQueries = False+  , dumpExprs = False+  , dumpEndStates = False+  , debug = False+  , abstRefineArith = False+  , abstRefineMem   = False+  , dumpTrace = False+  , numCexFuzz = 10+  , onlyCexFuzz  = False+  }++-- Write to the console+class Monad m => TTY m where+  writeOutput :: Text -> m ()+  writeErr :: Text -> m ()++writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m ()+writeTraceDapp dapp vm = do+  conf <- readConfig+  liftIO $ when conf.dumpTrace $ T.writeFile "VM.trace" (showTraceTree dapp vm)++writeTrace :: App m => VM t RealWorld -> m ()+writeTrace vm = do+  conf <- readConfig+  liftIO $ when conf.dumpTrace $ writeFile "VM.trace" (show $ traceForest vm)+++-- IO Interpretation -------------------------------------------------------------------------------+++newtype Env = Env+  { config :: Config+  }++defaultEnv :: Env+defaultEnv = Env { config = defaultConfig }++instance Monad m => ReadConfig (ReaderT Env m) where+  readConfig = do+    e <- ask+    pure e.config++instance (Monad m, MonadIO m) => TTY (ReaderT Env m) where+  writeOutput txt = liftIO $ T.putStrLn txt+  writeErr txt = liftIO $ T.hPutStr stderr txt++runEnv :: Env -> ReaderT Env m a -> m a+runEnv e a = runReaderT a e+++-- Helpful Aliases ---------------------------------------------------------------------------------+++type App m = (MonadUnliftIO m, ReadConfig m, TTY m)++runApp :: ReaderT Env m a -> m a+runApp = runEnv defaultEnv

@@ -14,7 +14,7 @@ ethrunAddress :: Addr ethrunAddress = Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72 -vmForEthrunCreation :: ByteString -> ST s (VM s)+vmForEthrunCreation :: VMOps t => ByteString -> ST s (VM t s) vmForEthrunCreation creationCode =   (makeVm $ VMOpts     { contract = initialContract (InitCode creationCode mempty)@@ -31,7 +31,7 @@     , blockGaslimit = 0     , gasprice = 0     , prevRandao = 42069-    , gas = 0xffffffffffffffff+    , gas = toGas 0xffffffffffffffff     , gaslimit = 0xffffffffffffffff     , baseFee = 0     , priorityFee = 0@@ -44,21 +44,21 @@     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode "")))) -exec :: EVM s (VMResult s)+exec :: VMOps t => EVM t s (VMResult t s) exec = do   vm <- get   case vm.result of     Nothing -> exec1 >> exec     Just r -> pure r -run :: EVM s (VM s)+run :: VMOps t => EVM t s (VM t s) run = do   vm <- get   case vm.result of     Nothing -> exec1 >> run     Just _ -> pure vm -execWhile :: (VM s -> Bool) -> State (VM s) Int+execWhile :: (VM t s -> Bool) -> State (VM t s) Int execWhile p = go 0   where     go i = do

@@ -205,11 +205,11 @@ -- | Extracts the byte at a given index from a Buf. -- -- We do our best to return a concrete value wherever possible, but fallback to--- an abstract expresion if nescessary. Note that a Buf is an infinite+-- an abstract expression if necessary. Note that a Buf is an infinite -- structure, so reads outside of the bounds of a ConcreteBuf return 0. This is -- inline with the semantics of calldata and memory, but not of returndata. --- fuly concrete reads+-- fully concrete reads readByte :: Expr EWord -> Expr Buf -> Expr Byte readByte (Lit x) (ConcreteBuf b)   = if x <= unsafeInto (maxBound :: Int) && i < BS.length b@@ -235,7 +235,7 @@     then readByte (Lit $ x - (dstOffset - srcOffset)) src     else readByte i dst readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) (Lit size) _ dst)-  -- the byte we are trying to read is compeletely outside of the sliced region+  -- the byte we are trying to read is completely outside of the sliced region   = if x - dstOffset >= size     then readByte i dst     else ReadByte (Lit x) buf@@ -269,7 +269,7 @@ readWord (Lit idx) b@(CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst)   -- the region we are trying to read is enclosed in the sliced region   | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src-  -- the region we are trying to read is compeletely outside of the sliced region+  -- the region we are trying to read is completely outside of the sliced region   | (idx - dstOff) >= size && (idx - dstOff) <= (maxBound :: W256) - 31 = readWord (Lit idx) dst   -- the region we are trying to read partially overlaps the sliced region   | otherwise = readWordFromBytes (Lit idx) b@@ -343,7 +343,7 @@ -- copying 32 bytes can be rewritten to a WriteWord on dst (e.g. CODECOPY of args during constructors) copySlice srcOffset dstOffset (Lit 32) src dst = writeWord dstOffset (readWord srcOffset src) dst --- concrete indicies & abstract src (may produce a concrete result if we are+-- concrete indices & abstract src (may produce a concrete result if we are -- copying from a concrete region of src) copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf dst)   | dstOffset < maxBytes, size < maxBytes, srcOffset + (size-1) > srcOffset = let@@ -355,7 +355,7 @@        else CopySlice s d sz src ds   | otherwise = CopySlice s d sz src ds --- abstract indicies+-- abstract indices copySlice srcOffset dstOffset size src dst = CopySlice srcOffset dstOffset size src dst  @@ -412,7 +412,7 @@ -- | Returns the length of a given buffer -- -- If there are any writes to abstract locations, or CopySlices with an--- abstract size or dstOffset, an abstract expresion will be returned.+-- abstract size or dstOffset, an abstract expression will be returned. bufLength :: Expr Buf -> Expr EWord bufLength = bufLengthEnv mempty False @@ -421,7 +421,7 @@   where     go :: Expr EWord -> Expr Buf -> Expr EWord     go l (ConcreteBuf b) = EVM.Expr.max l (Lit (unsafeInto . BS.length $ b))-    go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b))+    go l (AbstractBuf b) = EVM.Expr.max l (BufLength (AbstractBuf b))     go l (WriteWord idx _ b) = go (EVM.Expr.max l (add idx (Lit 32))) b     go l (WriteByte idx _ b) = go (EVM.Expr.max l (add idx (Lit 1))) b     go l (CopySlice _ dstOffset size _ dst) = go (EVM.Expr.max l (add dstOffset size)) dst@@ -473,12 +473,12 @@     inputLen = case bufLength b of       Lit s -> if s > maxIdx         then internalError "concretePrefix: input buffer size exceeds 500mb"-        -- unafeInto: s is <= 500,000,000+        -- unsafeInto: s is <= 500,000,000         else Just (unsafeInto s)       _ -> Nothing -    -- recursively reads succesive bytes from `b` until we reach a symbolic-    -- byte returns the larged index read from and a reference to the mutable+    -- recursively reads successive bytes from `b` until we reach a symbolic+    -- byte returns the large index read from and a reference to the mutable     -- vec (might not be the same as the input because of the call to grow)     go :: forall s . Int -> MVector s Word8 -> ST s (Int, MVector s Word8)     go i v@@ -529,7 +529,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 maybeLitByte $ bs-  -- we want to minimize the size of the resulting expresion, so we do two passes:+  -- we want to minimize the size of the resulting expression, so we do two passes:   --   1. write all concrete bytes to some base buffer   --   2. write all symbolic writes on top of this buffer   -- this is safe because each write in the input vec is to a single byte at a distinct location@@ -612,7 +612,7 @@   where     go :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)     go _ (GVar _) = internalError "Can't read from a GVar"-    go slot s@(AbstractStore _) = Just $ SLoad slot s+    go slot s@(AbstractStore _ _) = Just $ SLoad slot s     go (Lit l) (ConcreteStore s) = Lit <$> Map.lookup l s     go slot store@(ConcreteStore _) = Just $ SLoad slot store     go slot s@(SStore prevSlot val prev) = case (prevSlot, slot) of@@ -640,12 +640,16 @@        -- the chance of adding a value <= 2^32 to any given keccack output       -- leading to an overflow is effectively zero. the chance of an overflow-      -- occuring here is 2^32/2^256 = 2^-224, which is close enough to zero+      -- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero       -- for our purposes. This lets us completely simplify reads from write       -- chains involving writes to arrays at literal offsets.       (Lit a, Add (Lit b) (Keccak _) ) | a < 256, b < maxW32 -> go slot prev-      (Add (Lit a) (Keccak _) , Lit b) | a < 256, b < maxW32 -> go slot prev+      (Add (Lit a) (Keccak _) , Lit b) | b < 256, a < maxW32 -> go slot prev +      --- NOTE these are needed to succeed in rewriting arrays with a variable index+      -- (Lit a, Add (Keccak _) (Var _) ) | a < 256 -> go slot prev+      -- (Add (Keccak _) (Var _) , Lit b) | b < 256 -> go slot prev+       -- Finding two Keccaks that are < 256 away from each other should be VERY hard       -- This simplification allows us to deal with maps of structs       (Add (Lit a2) (Keccak _), Add (Lit b2) (Keccak _)) | a2 /= b2, abs(a2-b2) < 256 -> go slot prev@@ -690,6 +694,7 @@ pattern Keccak64Bytes <- Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) _ (ConcreteBuf ""))  -- storage slots for arrays are determined by (keccak(bytes32(id)) + offset)+-- note that `normArgs` puts the Lit as the 2nd argument to `Add` pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord pattern ArraySlotWithOffset id offset = Add (Keccak (ConcreteBuf id)) offset @@ -755,14 +760,138 @@  getAddr :: Expr Storage -> Maybe (Expr EAddr) getAddr (SStore _ _ p) = getAddr p-getAddr (AbstractStore a) = Just a+getAddr (AbstractStore a _) = Just a getAddr (ConcreteStore _) = Nothing getAddr (GVar _) = internalError "cannot determine addr of a GVar" +getLogicalIdx :: Expr Storage -> Maybe W256+getLogicalIdx (SStore _ _ p) = getLogicalIdx p+getLogicalIdx (AbstractStore _ idx) = idx+getLogicalIdx (ConcreteStore _) = Nothing+getLogicalIdx (GVar _) = internalError "cannot determine addr of a GVar" + -- ** Whole Expression Simplification ** -----------------------------------------------------------  +data StorageType = SmallSlot | Array | Map | Mixed | UNK+  deriving (Show, Eq)++safeToDecompose :: Expr a -> Bool+safeToDecompose inp = result /= Mixed+  where+    result = execState (safeToDecomposeRunner inp) UNK++    safeToDecomposeRunner :: forall a. Expr a -> State StorageType ()+    safeToDecomposeRunner a = go a++    go :: forall b. Expr b -> State StorageType ()+    go e@(SLoad (MappingSlot {}) _) = setMap e+    go e@(SLoad (ArraySlotZero {}) _) = setArray e+    go e@(SLoad (ArraySlotWithOffset {}) _) = setArray e+    go e@(SLoad (Lit x) _) | x < 256 = setSmall e+    go e@(SLoad _ _) = setMixed e+    go e@(SStore (MappingSlot {}) _ _) = setMap e+    go e@(SStore (ArraySlotZero {}) _ _) = setArray e+    go e@(SStore (ArraySlotWithOffset {}) _ _) = setArray e+    go e@(SStore (Lit x) _ _) | x < 256 = setSmall e+    go e@(SStore _ _ _) = setMixed e+    go _ = pure ()++    -- Helper functions for detecting mixed load/store+    setMixed _ = do+      put Mixed+      pure ()+    setMap _ = do+      s <- get+      case s of+        Array -> put Mixed+        SmallSlot -> put Mixed+        UNK -> put Map+        _ -> pure ()+      pure ()+    setArray _ = do+      s <- get+      case s of+        Map -> put Mixed+        SmallSlot -> put Mixed+        UNK -> put Array+        _ -> pure ()+      pure ()+    setSmall _ = do+      s <- get+      case s of+        Map -> put Mixed+        Array -> put Mixed+        UNK -> put SmallSlot+        _ -> pure ()+      pure ()++-- | Splits storage into logical sub-stores if (1) all SLoad->SStore* chains are one of:+--     (1a) Lit < 256, (1b) MappingSlot, (1c) ArraySlotWithOffset, (1d) ArraySlotZero+--  and (2) there is no mixing of different types (e.g. Map with Array) within+--  the same SStore -> SLoad* chain, and (3) there is no mixing of different array/map slots.+--+--  Mixing (2) and (3) are attempted to be prevented (if possible) as part of the rewrites+--  done by the `readStorage` function that is ran before this. If there is still mixing here,+--  we abort with a Nothing.+--+--  We do NOT rewrite stand-alone `SStore`-s (i.e. SStores that are not read), since+--  they are often used to describe a post-state, and are not dispatched as-is to+--  the solver+decomposeStorage :: Expr a -> Maybe (Expr a)+decomposeStorage = go+  where+    go :: Expr a -> Maybe (Expr a)+    go e@(SLoad origKey store) = if Prelude.not (safeToDecompose e) then Nothing else tryRewrite origKey store+    go e = Just e++    tryRewrite :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)+    tryRewrite origKey store = case inferLogicalIdx origKey of+      Just (idx, key) -> do+        base <- setLogicalBase idx store+        pure (SLoad key base)+      _ -> Nothing++    -- NOTE: we use (Maybe W256) for idx here, because for small slot numbers we want to keep the+    -- Logical Store value a Nothing+    inferLogicalIdx :: Expr EWord -> Maybe (Maybe W256, Expr EWord)+    inferLogicalIdx = \case+      Lit a | a >= 256 -> Nothing+      Lit a -> Just (Nothing, Lit a)+      (MappingSlot idx key) | BS.length idx == 64 -> Just (Just $ idxToWord idx, key)+      (ArraySlotWithOffset idx offset) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, offset)+      (ArraySlotZero idx) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, Lit 0)+      _ -> Nothing++    idxToWord :: ByteString -> W256+    idxToWord = W256 . word256 . (BS.takeEnd 32)+    -- Arrays take the whole `id` and keccak it. It's supposed to be 64B+    idxToWord64 :: ByteString -> W256+    idxToWord64 = W256 . word256 . (BS.takeEnd 64)++    -- Updates the logical base store of the given expression if it is safe to do so+    setLogicalBase :: Maybe W256 -> Expr Storage -> Maybe (Expr Storage)++    -- abstract bases get their logical idx set to the new value+    setLogicalBase idx (AbstractStore addr _) = Just $ AbstractStore addr idx+    setLogicalBase idx (SStore i v s) = do+      b <- setLogicalBase idx s+      (idx2, key2) <- inferLogicalIdx i+      if idx == idx2 then Just (SStore key2 v b) else Nothing++    -- empty concrete base is safe to reuse without any rewriting+    setLogicalBase _ s@(ConcreteStore m) | Map.null m = Just s++    -- if the existing base is concrete but we have writes to only keys < 256+    -- then we can safely rewrite the base to an empty ConcreteStore (safe because we assume keccack(x) > 256)+    setLogicalBase _ (ConcreteStore store) =+      if all (< 256) (Map.keys store)+      then Just (ConcreteStore mempty)+      else Nothing+    setLogicalBase _ (GVar _) = internalError "Unexpected GVar"++ -- | Simple recursive match based AST simplification -- Note: may not terminate! simplify :: Expr a -> Expr a@@ -780,6 +909,9 @@     go (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x0) _ dst) = dst      -- simplify storage+    go (Keccak (ConcreteBuf bs)) = case BS.length bs == 64 of+      True -> MappingSlot bs (Lit $ word bs)+      False -> Keccak (ConcreteBuf bs)     go (SLoad slot store) = readStorage' slot store     go (SStore slot val store) = writeStorage slot val store @@ -832,6 +964,8 @@     go (EVM.Types.GEq a b) = leq b a     go (EVM.Types.LEq a b) = EVM.Types.IsZero (gt a b)     go (IsZero a) = iszero a+    go (SLT a@(Lit _) b@(Lit _)) = slt a b+    go (SGT a b) = SLT b a      -- syntactic Eq reduction     go (Eq (Lit a) (Lit b))@@ -870,10 +1004,21 @@     -- (a+(c-b))     -- In other words, subtraction is just adding a much larger number.     --    So 3-1 mod 6 = 3+(6-1) mod 6 = 3+5 mod 6 = 5+3 mod 6 = 2-    go (Sub (Sub orig (Lit x)) (Lit y)) = Sub orig (Lit (y+x))-    go (Sub (Add orig (Lit x)) (Lit y)) = Sub orig (Lit (y-x))-    go (Add (Add orig (Lit x)) (Lit y)) = Add orig (Lit (y+x))-    go (Add (Sub orig (Lit x)) (Lit y)) = Add orig (Lit (y-x))+    -- Notice: all Add is normalized, hence the 1st argument is+    --    expected to be Lit, if any. Hence `orig` needs to be the+    --    2nd argument for Add. However, Sub is not normalized+    go (Add (Lit x) (Add (Lit y) orig)) = add (Lit (x+y)) orig+    -- add + sub NOTE: every combination of Sub is needed (2)+    go (Add (Lit x) (Sub (Lit y) orig)) = sub (Lit (x+y)) orig+    go (Add (Lit x) (Sub orig (Lit y))) = add (Lit (x-y)) orig+    -- sub + sub NOTE: every combination of Sub is needed (2x2)+    go (Sub (Lit x) (Sub (Lit y) orig)) = add (Lit (x-y)) orig+    go (Sub (Lit x) (Sub orig (Lit y))) = sub (Lit (x+y)) orig+    go (Sub (Sub (Lit x) orig) (Lit y)) = sub (Lit (x-y)) orig+    go (Sub (Sub orig (Lit x)) (Lit y)) = sub orig (Lit (x+y))+    -- sub + add NOTE: every combination of Sub is needed (2)+    go (Sub (Lit x) (Add (Lit y) orig)) = sub (Lit (x-y)) orig+    go (Sub (Add (Lit x) orig) (Lit y) ) = add (Lit (x-y)) orig      -- redundant add / sub     go (Sub (Add a b) c)@@ -881,6 +1026,12 @@       | b == c = a       | otherwise = sub (add a b) c +    -- Add is associative. We are doing left-growing trees because LIT is+    -- arranged to the left. This way, they accumulate in all combinations.+    -- See `sim-assoc-add` test cases in test.hs+    go (Add a (Add b c)) = add (add a b) c+    go (Add (Add (Lit a) x) (Lit b)) = add (Lit (a+b)) x+     -- add / sub identities     go (Add a b)       | b == (Lit 0) = a@@ -940,18 +1091,23 @@     go (EVM.Types.Not (EVM.Types.Not a)) = a      -- Some trivial min / max eliminations-    go (Max a b) = case (a, b) of-                    (Lit 0, _) -> b-                    _ -> EVM.Expr.max a b+    go (Max a b) = EVM.Expr.max a b     go (Min a b) = case (a, b) of                      (Lit 0, _) -> Lit 0                      _ -> EVM.Expr.min a b +    -- Mul is associative. We are doing left-growing trees because LIT is+    -- arranged to the left. This way, they accumulate in all combinations.+    -- See `sim-assoc-add` test cases in test.hs+    go (Mul a (Mul b c)) = mul (mul a b) c+    go (Mul (Mul (Lit a) x) (Lit b)) = mul (Lit (a*b)) x+     -- Some trivial mul eliminations     go (Mul a b) = case (a, b) of                      (Lit 0, _) -> Lit 0                      (Lit 1, _) -> b                      _ -> mul a b+     -- Some trivial div eliminations     go (Div (Lit 0) _) = Lit 0 -- divide 0 by anything (including 0) is zero in EVM     go (Div _ (Lit 0)) = Lit 0 -- divide anything by 0 is zero in EVM@@ -983,6 +1139,7 @@     canBeSat = constFoldProp simplified  -- | Evaluate the provided proposition down to its most concrete result+-- Also simplifies the inner Expr, if it exists simplifyProp :: Prop -> Prop simplifyProp prop =   let new = mapProp' go (simpInnerExpr prop)@@ -990,7 +1147,7 @@   where     go :: Prop -> Prop -    -- LT/LEq comparisions+    -- LT/LEq comparisons     go (PLT  (Var _) (Lit 0)) = PBool False     go (PLEq (Lit 0) (Var _)) = PBool True     go (PLT  (Lit val) (Var _)) | val == maxLit = PBool False@@ -999,12 +1156,16 @@     go (PLEq (Lit l) (Lit r)) = PBool (l <= r)     go (PLEq a (Max b _)) | a == b = PBool True     go (PLEq a (Max _ b)) | a == b = PBool True+    go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)+    go (PLT (Lit 0) (Eq a b)) = PEq a b      -- negations     go (PNeg (PBool b)) = PBool (Prelude.not b)     go (PNeg (PNeg a)) = a      -- solc specific stuff+    go (PEq (IsZero (Eq a b)) (Lit 0)) = PEq a b+    go (PEq (IsZero (IsZero (Eq a b))) (Lit 0)) = PNeg (PEq a b)      -- iszero(a) -> (a == 0)     -- iszero(iszero(a))) -> ~(a == 0) -> a > 0@@ -1071,7 +1232,7 @@  -- removes redundant (constant True/False) props remRedundantProps :: [Prop] -> [Prop]-remRedundantProps p = collapseFalse . filter (\x -> x /= PBool True) . nubOrd $ p+remRedundantProps p = nubOrd $ collapseFalse . filter (\x -> x /= PBool True) $ p   where     collapseFalse ps = if isJust $ find (== PBool False) ps then [PBool False] else ps @@ -1137,7 +1298,7 @@ -- Simplify masked reads: -- -----                reads across the mask boundry+--                reads across the mask boundary --                return an abstract expression --                            │ --                            │@@ -1161,7 +1322,7 @@ --                    indexWord 31 reads from the LSB -- indexWord i@(Lit idx) e@(And (Lit mask) w)-  -- if the mask is all 1s then read from the undelrying word+  -- if the mask is all 1s then read from the underlying word   -- we need this case to avoid overflow   | mask == fullWordMask = indexWord (Lit idx) w   -- if the index is a read from the masked region then read from the underlying word@@ -1176,7 +1337,7 @@   , isByteAligned mask   , idx < unmaskedBytes     = LitByte 0-  -- if the mask is not a power of 2, or it does not align with a byte boundry return an abstract expression+  -- if the mask is not a power of 2, or it does not align with a byte boundary return an abstract expression   | idx <= 31 = IndexWord i e   -- reads outside the range of the source word return 0   | otherwise = LitByte 0@@ -1270,6 +1431,8 @@ min x y = normArgs Min Prelude.min x y  max :: Expr EWord -> Expr EWord -> Expr EWord+max (Lit 0) y = y+max x (Lit 0) = x max x y = normArgs Max Prelude.max x y  numBranches :: Expr End -> Int@@ -1309,6 +1472,7 @@     oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat     go :: Prop -> State ConstState ()     go x = case x of+        -- PEq         PEq (Lit l) a -> do           s <- get           case Map.lookup a s.values of@@ -1319,6 +1483,16 @@               let vs' = Map.insert a l s.values               put $ s{values=vs'}         PEq a b@(Lit _) -> go (PEq b a)+        -- PNeg+        PNeg (PEq (Lit l) a) -> do+          s <- get+          case Map.lookup a s.values of+            Just l2 -> case l==l2 of+                True -> put ConstState {canBeSat=False, values=mempty}+                False -> pure ()+            Nothing -> pure()+        PNeg (PEq a b@(Lit _)) -> go $ PNeg (PEq b a)+        -- Others         PAnd a b -> do           go a           go b@@ -1333,3 +1507,24 @@           put $ s{canBeSat=(s2.canBeSat && (v1 || v2))}         PBool False -> put $ ConstState {canBeSat=False, values=mempty}         _ -> pure ()++-- Concretize & simplify Keccak expressions until fixed-point.+concKeccakSimpExpr :: Expr a -> Expr a+concKeccakSimpExpr orig = untilFixpoint ((mapExpr concKeccakOnePass) . simplify) orig++-- Only concretize Keccak in Props+-- Needed because if it also simplified, we may not find some simplification errors, as+-- simplification would always be ON+concKeccakProps :: [Prop] -> [Prop]+concKeccakProps orig = untilFixpoint (map (mapProp concKeccakOnePass)) orig++-- Simplifies in case the input to the Keccak is of specific array/map format and+--            can be simplified into a concrete value+-- Turns (Keccak ConcreteBuf) into a Lit+concKeccakOnePass :: Expr a -> Expr a+concKeccakOnePass (Keccak (ConcreteBuf bs)) = Lit (keccak' bs)+concKeccakOnePass orig@(Keccak (CopySlice (Lit 0) (Lit 0) (Lit 64) orig2@(WriteWord (Lit 0) _ (ConcreteBuf bs)) (ConcreteBuf ""))) =+  case (BS.length bs, (copySlice (Lit 0) (Lit 0) (Lit 64) (simplify orig2) (ConcreteBuf ""))) of+    (64, ConcreteBuf a) -> Lit (keccak' a)+    _ -> orig+concKeccakOnePass x = x

@@ -27,6 +27,8 @@ import Network.Wreq.Session qualified as Session import Numeric.Natural (Natural) import System.Process+import Control.Monad.IO.Class+import EVM.Effects  -- | Abstract representation of an RPC fetch request data RpcQuery a where@@ -182,23 +184,23 @@   sess <- Session.newAPISession   fetchQuery Latest (fetchWithSession url sess) QueryChainId -http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher s+http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s http smtjobs smttimeout n url q =   withSolvers Z3 smtjobs smttimeout $ \s ->     oracle s (Just (n, url)) q -zero :: Natural -> Maybe Natural -> Fetcher s+zero :: Natural -> Maybe Natural -> Fetcher t m s zero smtjobs smttimeout q =   withSolvers Z3 smtjobs smttimeout $ \s ->     oracle s Nothing q  -- smtsolving + (http or zero)-oracle :: SolverGroup -> RpcInfo -> Fetcher s+oracle :: SolverGroup -> RpcInfo -> Fetcher t m s oracle solvers info q = do   case q of     PleaseDoFFI vals continue -> case vals of        cmd : args -> do-          (_, stdout', _) <- readProcessWithExitCode cmd args ""+          (_, stdout', _) <- liftIO $ readProcessWithExitCode cmd args ""           pure . continue . encodeAbiValue $             AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout'])        _ -> internalError (show vals)@@ -215,7 +217,7 @@             AbstractBase -> unknownContract (LitAddr addr)             EmptyBase -> emptyContract           in pure $ Just c-        Just (n, url) -> fetchContractFrom n url addr+        Just (n, url) -> liftIO $ fetchContractFrom n url addr       case contract of         Just x -> pure $ continue x         Nothing -> internalError $ "oracle error: " ++ show q@@ -224,27 +226,28 @@       case info of         Nothing -> pure (continue 0)         Just (n, url) ->-         fetchSlotFrom n url addr slot >>= \case+         liftIO $ fetchSlotFrom n url addr slot >>= \case            Just x  -> pure (continue x)            Nothing ->              internalError $ "oracle error: " ++ show q -type Fetcher s = Query s -> IO (EVM s ())+type Fetcher t m s = App m => Query t s -> m (EVM t s ())  -- | 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 BranchCondition+checkBranch :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition checkBranch solvers branchcondition pathconditions = do-  checkSat solvers (assertProps abstRefineDefault [(branchcondition .&& pathconditions)]) >>= \case+  conf <- readConfig+  liftIO $ checkSat solvers (assertProps conf [(branchcondition .&& pathconditions)]) >>= \case     -- the condition is unsatisfiable     Unsat -> -- if pathconditions are consistent then the condition must be false       pure $ Case False     -- Sat means its possible for condition to hold-    Sat _ -> -- is its negation also possible?-      checkSat solvers (assertProps abstRefineDefault [(pathconditions .&& (PNeg branchcondition))]) >>= \case+    Sat _ -> do -- is its negation also possible?+      checkSat solvers (assertProps conf [(pathconditions .&& (PNeg branchcondition))]) >>= \case         -- No. The condition must hold         Unsat -> pure $ Case True         -- Yes. Both branches possible

@@ -5,6 +5,7 @@   ( formatExpr   , formatSomeExpr   , formatPartial+  , formatProp   , contractNamePart   , contractPathPart   , showError@@ -17,7 +18,6 @@   , showWordExact   , showWordExplanation   , parenthesise-  , unindexed   , showValue   , textValues   , showAbiValue@@ -38,7 +38,7 @@ import EVM.Types import EVM (traceForest, traceForest', traceContext, cheatCode) import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..))-import EVM.Dapp (DappContext(..), DappInfo(..), showTraceLocation)+import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation) import EVM.Expr qualified as Expr import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap) @@ -53,10 +53,10 @@ import Data.Char qualified as Char import Data.DoubleWord (signedWord) import Data.Foldable (toList)-import Data.List (isPrefixOf)+import Data.List (isPrefixOf, sort) import Data.Map (Map) import Data.Map qualified as Map-import Data.Maybe (catMaybes, fromMaybe, fromJust)+import Data.Maybe (catMaybes, fromMaybe) import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn) import Data.Text qualified as T import Data.Text.Encoding qualified as T@@ -111,15 +111,9 @@ showAbiValue (AbiBytesDynamic bs) = formatBytes bs showAbiValue (AbiBytes _ bs) = formatBinary bs showAbiValue (AbiAddress addr) =-  let dappinfo = ?context.info-      contracts = ?context.env-      name = case Map.lookup (LitAddr addr) contracts of+  let name = case Map.lookup (LitAddr addr) ?context.env of         Nothing -> ""-        Just contract ->-          let hash = maybeLitWord contract.codehash-          in case hash of-               Just h -> maybeContractName' (preview (ix h % _2) dappinfo.solcByHash)-               Nothing -> ""+        Just contract -> maybeContractName' (findSrc contract ?context.info)   in     name <> "@" <> (pack $ show addr) showAbiValue v = pack $ show v@@ -190,7 +184,7 @@ formatSBinary (AbstractBuf t) = "<" <> t <> " abstract buf>" formatSBinary _ = internalError "formatSBinary: implement me" -showTraceTree :: DappInfo -> VM s -> Text+showTraceTree :: DappInfo -> VM t s -> Text showTraceTree dapp vm =   let forest = traceForest vm       traces = fmap (fmap (unpack . showTrace dapp (vm.env.contracts))) forest@@ -203,9 +197,6 @@       traces = fmap (fmap (unpack . showTrace dapp (traceContext leaf))) forest   in pack $ concatMap showTree traces -unindexed :: [(Text, AbiType, Indexed)] -> [AbiType]-unindexed ts = [t | (_, t, NotIndexed) <- ts]- showTrace :: DappInfo -> Map (Expr EAddr) Contract -> Trace -> Text showTrace dapp env trace =   let ?context = DappContext { info = dapp, env = env }@@ -214,37 +205,17 @@       case showTraceLocation dapp trace of         Left x -> " \x1b[1m" <> x <> "\x1b[0m"         Right x -> " \x1b[1m(" <> x <> ")\x1b[0m"-    fullAbiMap = dapp.abiMap   in case trace.tracedata of     EventTrace _ bytes topics ->-      let logn = mconcat-            [ "\x1b[36m"-            , "log" <> (pack (show (length topics)))-            , parenthesise ((map (pack . show) topics) ++ [formatSBinary bytes])-            , "\x1b[0m"-            ] <> pos-          knownTopic name types = mconcat-            [ "\x1b[36m"-            , name-            , showValues (unindexed types) bytes-            -- todo: show indexed-            , "\x1b[0m"-            ] <> pos-          lognote sig usr = mconcat-            [ "\x1b[36m"-            , "LogNote"-            , parenthesise [sig, usr, "..."]-            , "\x1b[0m"-            ] <> pos-      in case topics of+      case topics of         [] ->           logn-        (t1:_) ->-          case maybeLitWord t1 of+        firstTopic:restTopics ->+          case maybeLitWord firstTopic of             Just topic ->               case Map.lookup topic dapp.eventMap of-                Just (Event name _ types) ->-                  knownTopic name types+                Just (Event name _ argInfos) ->+                  showEvent name argInfos restTopics                 Nothing ->                   case topics of                     [_, t2, _, _] ->@@ -273,7 +244,56 @@                       logn             Nothing ->               logn+      where+        logn = mconcat+          [ "\x1b[36m"+          , "log" <> (pack (show (length topics)))+          , parenthesise ((map (pack . show) topics) ++ [formatSBinary bytes])+          , "\x1b[0m"+          ] <> pos +        showEvent eventName argInfos indexedTopics = mconcat+          [ "\x1b[36m"+          , eventName+          , parenthesise (snd <$> sort (unindexedArgs <> indexedArgs))+          , "\x1b[0m"+          ] <> pos+          where+          -- We maintain the original position of event arguments since indexed+          -- and not indexed arguments can be interleaved.+          unindexedArgs :: [(Int, Text)]+          unindexedArgs =+            let (positions, names, abiTypes) = unzip3 (filterArgInfos NotIndexed)+            in zip positions (zipWith withName names (textValues abiTypes bytes))++          indexedArgs :: [(Int, Text)]+          indexedArgs =+            let (positions, names, abiTypes) = unzip3 (filterArgInfos Indexed)+            in zip positions (zipWith withName names (zipWith showTopic abiTypes indexedTopics))+            where+            showTopic :: AbiType -> Expr EWord -> Text+            showTopic abiType topic =+              case maybeLitWord (Expr.concKeccakSimpExpr topic) of+                Just w -> head $ textValues [abiType] (ConcreteBuf (word256Bytes w))+                _ -> "<symbolic>"++          withName :: Text -> Text -> Text+          withName "" value = value+          withName argName value = argName <> "=" <> value++          filterArgInfos :: Indexed -> [(Int, Text, AbiType)]+          filterArgInfos which =+            [ (i, argName, argType) | (i, (argName, argType, indexed)) <- zip [0..] argInfos+                                    , indexed == which+            ]++        lognote sig usr = mconcat+          [ "\x1b[36m"+          , "LogNote"+          , parenthesise [sig, usr, "..."]+          , "\x1b[0m"+          ] <> pos+     ErrorTrace e ->       case e of         Revert out ->@@ -281,9 +301,9 @@         _ ->           "\x1b[91merror\x1b[0m " <> pack (show e) <> pos -    ReturnTrace out (CallContext _ _ _ _ _ (Just abi) _ _ _) ->+    ReturnTrace out (CallContext { abi = Just abi }) ->       "← " <>-        case Map.lookup (unsafeInto abi) fullAbiMap of+        case Map.lookup (unsafeInto abi) dapp.abiMap of           Just m  ->             case unzip m.output of               ([], []) ->@@ -299,29 +319,23 @@       in "← " <> formatExpr l <> " bytes of code"     EntryTrace t ->       t-    FrameTrace (CreationContext addr (Lit hash) _ _ ) -> -- FIXME: irrefutable pattern-      "create "-      <> maybeContractName (preview (ix hash % _2) dapp.solcByHash)-      <> "@" <> formatAddr addr-      <> pos-    FrameTrace (CreationContext addr _ _ _ ) ->+    FrameTrace (CreationContext { address }) ->       "create "-      <> "<unknown contract>"-      <> "@" <> formatAddr addr+      <> maybeContractName (findSrcFromAddr address)+      <> "@" <> formatAddr address       <> pos-    FrameTrace (CallContext target context _ _ hash abi calldata _ _) ->+    FrameTrace (CallContext { target, context, abi, calldata }) ->       let calltype = if target == context                      then "call "                      else "delegatecall "-          hash' = fromJust $ maybeLitWord hash-      in case preview (ix hash' % _2) dapp.solcByHash of+      in case findSrcFromAddr target of         Nothing ->           calltype             <> case target of                  LitAddr 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> "HEVM"                  _ -> formatAddr target             <> pack "::"-            <> case Map.lookup (unsafeInto (fromMaybe 0x00 abi)) fullAbiMap of+            <> case Map.lookup (unsafeInto (fromMaybe 0x00 abi)) dapp.abiMap of                  Just m  ->                    "\x1b[1m"                    <> m.name@@ -344,6 +358,10 @@                  (abi >>= fmap getAbiTypes . maybeAbiName solc)             <> "\x1b[0m"             <> pos+    where+    findSrcFromAddr addr = do+      contract <- Map.lookup addr env+      findSrc contract dapp  formatAddr :: Expr EAddr -> Text formatAddr = \case@@ -397,6 +415,7 @@   ReturnDataOutOfBounds -> "Return data out of bounds"   NonceOverflow -> "Nonce overflow"   BadCheatCode a -> "Bad cheat code: sig: " <> show a+  NonexistentFork a -> "Fork ID does not exist: " <> show a  prettyvmresult :: Expr End -> String prettyvmresult (Failure _ _ (Revert (ConcreteBuf ""))) = "Revert"@@ -668,12 +687,13 @@           , indent 2 $ formatExpr slot           , "val:"           , indent 2 $ formatExpr val+          , "store:"+          , indent 2 $ formatExpr prev                     ]         , ")"-        , formatExpr prev         ]-      AbstractStore a ->-        "(AbstractStore " <> formatExpr a <> ")"+      AbstractStore a idx ->+        "(AbstractStore " <> formatExpr a <> " " <> T.pack (show idx) <> ")"       ConcreteStore s -> if null s         then "(ConcreteStore <empty>)"         else T.unlines@@ -695,9 +715,10 @@           , "size:      " <> formatExpr size           , "src:"           , indent 2 $ formatExpr src+          , "dst:"+          , indent 2 $ formatExpr dst           ]         , ")"-        , formatExpr dst         ]       WriteWord idx val buf -> T.unlines         [ "(WriteWord"@@ -706,18 +727,19 @@           , indent 2 $ formatExpr idx           , "val:"           , indent 2 $ formatExpr val+          , "buf:"+          , indent 2 $ formatExpr buf           ]         , ")"-        , formatExpr buf         ]       WriteByte idx val buf -> T.unlines         [ "(WriteByte"         , indent 2 $ T.unlines           [ "idx: " <> formatExpr idx           , "val: " <> formatExpr val+          , "buf: " <> formatExpr buf           ]         , ")"-        , formatExpr buf         ]       ConcreteBuf bs -> case bs of         "" -> "(ConcreteBuf \"\")"