hevm 0.50.3 → 0.50.4

raw patch · 28 files changed

+2363/−745 lines, 28 filesdep +base16dep −base16-bytestringdep ~operationalPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: base16

Dependencies removed: base16-bytestring

Dependency ranges changed: operational

API changes (from Hackage documentation)

Files

• CHANGELOG.md +25/−0
• bench/bench.hs +2/−2
• hevm-cli/hevm-cli.hs +62/−53
• hevm.cabal +32/−24
• src/EVM.hs +145/−332
• src/EVM/ABI.hs +20/−1
• src/EVM/Assembler.hs +109/−0
• src/EVM/Concrete.hs +0/−2
• src/EVM/Debug.hs +2/−0
• src/EVM/Expr.hs +70/−23
• src/EVM/Facts.hs +2/−2
• src/EVM/Format.hs +9/−9
• src/EVM/Hexdump.hs +1/−1
• src/EVM/Op.hs +252/−4
• src/EVM/SMT.hs +173/−76
• src/EVM/Sign.hs +77/−0
• src/EVM/Solidity.hs +6/−7
• src/EVM/Solvers.hs +84/−15
• src/EVM/SymExec.hs +31/−15
• src/EVM/TTY.hs +1/−1
• src/EVM/Transaction.hs +72/−24
• src/EVM/Traversals.hs +26/−0
• src/EVM/Types.hs +96/−35
• src/EVM/UnitTest.hs +0/−4
• test/BlockchainTests.hs +3/−3
• test/EVM/Tracing.hs +870/−0
• test/scripts/convert_trace_to_json.sh +4/−0
• test/test.hs +189/−112

@@ -5,11 +5,33 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [0.50.4] - 2023-03-17++### Fixed++- The `--solvers` cli option is now respected (previously we always used Z3)+- The `equivalence` command now fails with the correct status code when counterexamples are found+- The `equivalence` command now respects the given `--sig` argument+- Correct symbolic execution for the `SGT` opcode++### Changed++- The `equivalence` command now pretty prints discovered counterexamples++### Added++- Implemented a shrinking algorithm for counterexamples+- A new differential fuzzing test harness that compares the concrete semantics, as well as parts of the symbolic semantics against the geth evm implementation+- The `hevm` library can now be built on Windows systems.+- Support for function pointers in ABI+- `equivalence` can now be checked for fully or partially concrete calldata+ ## [0.50.3] - 2023-02-17  ### Fixed  - `hevm symbolic` exits with status code `1` if counterexamples or timeouts are found+- Calldata reads beyond calldata size are provably equal to zero.  ### Added @@ -18,6 +40,9 @@ - Improved simplification for arithmetic expressions - Construction of storage counterexamples based on the model returned by the SMT solver. - Static binaries for macos++### Changed+- SMT encoding of buffer length without using uninterpreted functions.  ## [0.50.2] - 2023-01-06 

@@ -47,7 +47,7 @@  main :: IO () main = defaultMain-  [ mkbench erc20 "erc20" Nothing [1, 2, 4, 8, 16]+  [ mkbench erc20 "erc20" Nothing [1]   , mkbench (pure vat) "vat" Nothing [4]   , mkbench (pure deposit) "deposit" (Just 32) [4]   , mkbench (pure uniV2Pair) "uniV2" (Just 10) [4]@@ -59,7 +59,7 @@  debugContract :: ByteString -> IO () debugContract c = withSolvers CVC5 4 Nothing $ \solvers -> do-  let prestate = abstractVM Nothing [] c Nothing SymbolicS+  let prestate = abstractVM (mkCalldata Nothing []) c Nothing SymbolicS   void $ TTY.runFromVM solvers Nothing Nothing emptyDapp prestate  

@@ -15,7 +15,6 @@ import EVM.SymExec import EVM.Debug import qualified EVM.Expr as Expr-import EVM.SMT import EVM.Solvers import qualified EVM.TTY as TTY import EVM.Solidity@@ -36,7 +35,7 @@ import Control.Monad              (void, when, forM_, unless) import Control.Monad.State.Strict (execStateT, liftIO) import Data.ByteString            (ByteString)-import Data.List                  (intercalate, isSuffixOf)+import Data.List                  (intercalate, isSuffixOf, intersperse) import Data.Text                  (unpack, pack) import Data.Maybe                 (fromMaybe, mapMaybe) import Data.Version               (showVersion)@@ -109,6 +108,8 @@       { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"       , codeB         :: w ::: ByteString       <?> "Bytecode of the second program"       , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"+      , arg           :: w ::: [String]         <?> "Values to encode"+      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"       , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in milliseconds (default: 60000)"       , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"@@ -266,7 +267,8 @@     DappTest {} ->       withCurrentDirectory root $ do         cores <- num <$> getNumProcessors-        withSolvers Z3 cores cmd.smttimeout $ \solvers -> do+        solver <- getSolver cmd+        withSolvers solver cores cmd.smttimeout $ \solvers -> do           testFile <- findJsonFile cmd.jsonFile           testOpts <- unitTestOptions cmd solvers testFile           case (cmd.coverage, optsMode cmd) of@@ -307,19 +309,34 @@                           , askSmtIters = cmd.askSmtIterations                           , rpcInfo = Nothing                           }--  withSolvers Z3 3 Nothing $ \s -> do-    res <- equivalenceCheck s bytecodeA bytecodeB veriOpts Nothing-    case not (any isCex res) of+  calldata <- buildCalldata cmd+  solver <- getSolver cmd+  withSolvers solver 3 Nothing $ \s -> do+    res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata+    case any isCex res of       False -> do         putStrLn "No discrepancies found"         when (any isTimeout res) $ do           putStrLn "But timeout(s) occurred"           exitFailure       True -> do-        putStrLn $ "Not equivalent. Counterexample(s):" <> show res+        let cexs = mapMaybe getCex res+        T.putStrLn . T.unlines $+          [ "Not equivalent. The following inputs result in differing behaviours:"+          , "" , "-----", ""+          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap (formatCex (AbstractBuf "txdata")) cexs)         exitFailure +getSolver :: Command Options.Unwrapped -> IO Solver+getSolver cmd = case cmd.solver of+                  Nothing -> pure Z3+                  Just s -> case T.unpack s of+                              "z3" -> pure Z3+                              "cvc5" -> pure CVC5+                              input -> do+                                putStrLn $ "unrecognised solver: " <> input+                                exitFailure+ getSrcInfo :: Command Options.Unwrapped -> IO DappInfo getSrcInfo cmd =   let root = fromMaybe "." cmd.dappRoot@@ -332,42 +349,36 @@       Just (contractMap, sourceCache) ->         pure $ dappInfo root contractMap sourceCache --- Although it is tempting to fully abstract calldata and give any hints about--- the nature of the signature doing so results in significant time spent in--- consulting z3 about rather trivial matters. But with cvc5 it is quite--- pleasant! +-- | Builds a buffer representing calldata based on the given cli arguments+buildCalldata :: Command Options.Unwrapped -> IO (Expr Buf, [Prop])+buildCalldata cmd = case (cmd.calldata, cmd.sig) of+  -- fully abstract calldata+  (Nothing, Nothing) -> pure $ mkCalldata Nothing []+  -- fully concrete calldata+  (Just c, Nothing) -> pure (ConcreteBuf (hexByteString "bytes" . strip0x $ c), [])+  -- calldata according to given abi with possible specializations from the `arg` list+  (Nothing, Just sig') -> do+    method' <- functionAbi sig'+    pure $ mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) cmd.arg+  -- both args provided+  (_, _) -> do+    putStrLn "incompatible options provided: --calldata and --sig"+    exitFailure++ -- If function signatures are known, they should always be given for best results. assert :: Command Options.Unwrapped -> IO () assert cmd = do   let block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber cmd.block       rpcinfo = (,) block' <$> cmd.rpc-      decipher = hexByteString "bytes" . strip0x-  calldata' <- case (cmd.calldata, cmd.sig) of-    -- fully abstract calldata-    (Nothing, Nothing) -> pure-      ( AbstractBuf "txdata"-      -- assert that the length of the calldata is never more than 2^64-      -- this is way larger than would ever be allowed by the gas limit-      -- and avoids spurious counterexamples during abi decoding-      -- TODO: can we encode calldata as an array with a smaller length?-      , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))]-      )--    -- fully concrete calldata-    (Just c, Nothing) -> pure (ConcreteBuf (decipher c), [])-    -- calldata according to given abi with possible specializations from the `arg` list-    (Nothing, Just sig') -> do-      method' <- functionAbi sig'-      let typs = snd <$> method'.inputs-      pure $ symCalldata method'.methodSignature typs cmd.arg (AbstractBuf "txdata")-    _ -> error "incompatible options: calldata and abi"-+  calldata' <- buildCalldata cmd   preState <- symvmFromCommand cmd calldata'   let errCodes = fromMaybe defaultPanicCodes cmd.assertions   cores <- num <$> getNumProcessors   let solverCount = fromMaybe cores cmd.numSolvers-  withSolvers EVM.Solvers.Z3 solverCount cmd.smttimeout $ \solvers -> do+  solver <- getSolver cmd+  withSolvers solver solverCount cmd.smttimeout $ \solvers -> do     if cmd.debug then do       srcInfo <- getSrcInfo cmd       void $ TTY.runFromVM@@ -381,21 +392,23 @@       (expr, res) <- verify solvers opts preState (Just $ checkAssertions errCodes)       case res of         [Qed _] -> putStrLn "\nQED: No reachable property violations discovered\n"-        cexs -> do-          let counterexamples-                | null (getCexs cexs) = []+        _ -> do+          let cexs = snd <$> mapMaybe getCex res+              timeouts = mapMaybe getTimeout res+              counterexamples+                | null cexs = []                 | otherwise =                    [ ""                    , "Discovered the following counterexamples:"                    , ""-                   ] <> fmap (formatCex (fst calldata')) (getCexs cexs)+                   ] <> fmap (formatCex (fst calldata')) cexs               unknowns-                | null (getTimeouts cexs) = []+                | null timeouts = []                 | otherwise =                    [ ""                    , "Could not determine reachability of the following end states:"                    , ""-                   ] <> fmap (formatExpr) (getTimeouts cexs)+                   ] <> fmap (formatExpr) timeouts           T.putStrLn $ T.unlines (counterexamples <> unknowns)           exitFailure       when cmd.showTree $ do@@ -412,17 +425,13 @@         ms <- produceModels solvers expr         forM_ ms (showModel (fst calldata')) -getCexs :: [VerifyResult] -> [SMTCex]-getCexs = mapMaybe go-  where-    go (Cex cex) = Just $ snd cex-    go _ = Nothing+getCex :: ProofResult a b c -> Maybe b+getCex (Cex c) = Just c+getCex _ = Nothing -getTimeouts :: [VerifyResult] -> [Expr End]-getTimeouts = mapMaybe go-  where-    go (Timeout leaf) = Just leaf-    go _ = Nothing+getTimeout :: ProofResult a b c -> Maybe c+getTimeout (Timeout c) = Just c+getTimeout _ = Nothing  dappCoverage :: UnitTestOptions -> Mode -> String -> IO () dappCoverage opts _ solcFile =@@ -480,16 +489,16 @@             let res = case msg of                         ConcreteBuf bs -> bs                         _ -> "<symbolic>"-            print $ ByteStringS res+            putStrLn $ "Revert: " <> (show $ ByteStringS res)             exitWith (ExitFailure 2)           Just (EVM.VMFailure err) -> do-            print err+            putStrLn $ "Error: " <> show err             exitWith (ExitFailure 2)           Just (EVM.VMSuccess buf) -> do             let msg = case buf of                   ConcreteBuf msg' -> msg'                   _ -> "<symbolic>"-            print $ ByteStringS msg+            print $ "Return: " <> (show $ ByteStringS msg)             case cmd.state of               Nothing -> pure ()               Just path ->

@@ -2,7 +2,7 @@ name:   hevm version:-  0.50.3+  0.50.4 synopsis:   Ethereum virtual machine evaluator description:@@ -40,6 +40,7 @@   test/contracts/fail/cheatCodes.sol   test/contracts/fail/dsProveFail.sol   test/contracts/fail/invariantFail.sol+  test/scripts/convert_trace_to_json.sh  flag ci   description: Sets flags for compilation in CI@@ -76,6 +77,7 @@   exposed-modules:     EVM,     EVM.ABI,+    EVM.Assembler,     EVM.Concrete,     EVM.Dapp,     EVM.Debug,@@ -103,22 +105,22 @@     EVM.CSE,     EVM.Keccak,     EVM.Transaction,-    EVM.TTY,-    EVM.TTYCenteredList,     EVM.Types,     EVM.UnitTest,+    EVM.Sign,+  if !os(windows)+    exposed-modules:+      EVM.TTY,+      EVM.TTYCenteredList   other-modules:     Paths_hevm   autogen-modules:     Paths_hevm-  if flag(devel)-    ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans -j-  else-    ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans+  ghc-options: -Wall -Wno-deprecations -Wno-unticked-promoted-constructors -Wno-orphans+  if os(linux) || os(windows)+    extra-libraries: stdc++   extra-libraries:-    secp256k1, ff-  if os(linux)-     extra-libraries: stdc+++    secp256k1, ff, gmp   c-sources:     ethjet/tinykeccak.c, ethjet/ethjet.c   cxx-sources:@@ -144,13 +146,11 @@     unordered-containers              >= 0.2.10 && < 0.3,     vector                            >= 0.12.1 && < 0.13,     ansi-wl-pprint                    >= 0.6.9 && < 0.7,-    base16-bytestring                 >= 1.0.0 && < 2.0,-    brick                             >= 1.4 && < 1.5,+    base16                            >= 0.3.2.0 && < 0.3.3.0,     megaparsec                        >= 9.0.0 && < 10.0,     mtl                               >= 2.2.2 && < 2.3,     directory                         >= 1.3.3 && < 1.4,     filepath                          >= 1.4.2 && < 1.5,-    vty                               >= 5.37 && < 5.38,     cereal                            >= 0.5.8 && < 0.6,     cryptonite                        >= 0.30 && < 0.31,     memory                            >= 0.16.0 && < 0.20,@@ -180,6 +180,10 @@     spool                             >= 0.1 && < 0.2,     stm                               >= 2.5.0 && < 2.6.0,     spawn                             >= 0.3 && < 0.4+  if !os(windows)+    build-depends:+      brick                           >= 1.4 && < 1.5,+      vty                             >= 5.37 && < 5.38   hs-source-dirs:     src @@ -189,10 +193,7 @@     hevm-cli   main-is:     hevm-cli.hs-  if flag(devel)-    ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans -j-  else-    ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans+  ghc-options: -Wall -threaded -with-rtsopts=-N -Wno-unticked-promoted-constructors -Wno-orphans   other-modules:     Paths_hevm   if os(darwin)@@ -206,7 +207,7 @@     ansi-wl-pprint,     async,     base,-    base16-bytestring,+    base16,     binary,     brick,     bytestring,@@ -234,15 +235,14 @@     vty,     stm,     spawn+  if os(windows)+    buildable: False  --- Test Helpers ---  common test-base   import: shared-  if flag (devel)-    ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans -j-  else-    ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans+  ghc-options: -Wall -Wno-unticked-promoted-constructors -Wno-orphans   hs-source-dirs:     test   extra-libraries:@@ -257,7 +257,7 @@     quickcheck-instances,     aeson,     base,-    base16-bytestring,+    base16,     binary,     containers,     directory,@@ -285,21 +285,29 @@     stm >= 2.5.0,     spawn >= 0.3,     witherable,-    smt2-parser >= 0.1.0.1+    smt2-parser >= 0.1.0.1,+    operational  library test-utils   import:     test-base   exposed-modules:     EVM.TestUtils+  if os(windows)+    buildable: False  common test-common   import:     test-base+  if flag(devel)+    ghc-options: -threaded -with-rtsopts=-N   build-depends:     test-utils   other-modules:     EVM.TestUtils+    EVM.Tracing+  if os(windows)+    buildable: False   if os(darwin)     extra-libraries: c++     -- https://gitlab.haskell.org/ghc/ghc/-/issues/11829

@@ -1,7 +1,6 @@ {-# Language ImplicitParams #-} {-# Language DataKinds #-} {-# Language GADTs #-}-{-# Language StrictData #-} {-# Language TemplateHaskell #-}  module EVM where@@ -18,6 +17,7 @@ import EVM.Precompiled qualified import EVM.Solidity import EVM.Types hiding (IllegalOverflow, Error)+import EVM.Sign qualified  import Control.Lens hiding (op, (:<), (|>), (.>)) import Control.Monad.State.Strict hiding (state)@@ -49,12 +49,10 @@ import Data.Word (Word8, Word32, Word64) import Options.Generic as Options -import Crypto.Hash (Digest, SHA256, RIPEMD160, digestFromByteString)+import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..))-import Crypto.PubKey.ECC.Generate (generateQ)-import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..))  -- * Data types @@ -83,6 +81,7 @@   | NotUnique (Expr EWord)   | SMTTimeout   | FFI [AbiValue]+  | ReturnDataOutOfBounds   | NonceOverflow deriving instance Show Error @@ -104,7 +103,7 @@   , _logs           :: [Expr Log]   , _traces         :: Zipper.TreePos Zipper.Empty Trace   , _cache          :: Cache-  , _burned         :: Word64+  , _burned         :: {-# UNPACK #-} !Word64   , _iterations     :: Map CodeLocation Int   , _constraints    :: [Prop]   , _keccakEqs      :: [Prop]@@ -248,14 +247,14 @@   { _contract     :: Addr   , _codeContract :: Addr   , _code         :: ContractCode-  , _pc           :: Int+  , _pc           :: {-# UNPACK #-} !Int   , _stack        :: [Expr EWord]   , _memory       :: Expr Buf   , _memorySize   :: Word64   , _calldata     :: Expr Buf   , _callvalue    :: Expr EWord   , _caller       :: Expr EWord-  , _gas          :: Word64+  , _gas          :: {-# UNPACK #-} !Word64   , _returndata   :: Expr Buf   , _static       :: Bool   }@@ -391,8 +390,9 @@   , _baseFee     :: W256   , _maxCodeSize :: W256   , _schedule    :: FeeSchedule Word64-  } deriving Show+  } deriving (Show, Generic) + blankState :: FrameState blankState = FrameState   { _contract     = 0@@ -610,11 +610,10 @@                     fromMaybe (error "could not analyze symbolic code") $                       unlitByte $ ops V.! vm._state._pc -      case ?op of+      case getOp(?op) of -        -- op: PUSH-        x | x >= 0x60 && x <= 0x7f -> do-          let !n = num x - 0x60 + 1+        OpPush n' -> do+          let n = fromIntegral n'               !xs = case vm._state._code of                 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@@ -626,10 +625,8 @@               next               pushSym xs -        -- op: DUP-        x | x >= 0x80 && x <= 0x8f -> do-          let !i = x - 0x80 + 1-          case preview (ix (num i - 1)) stk of+        OpDup i ->+          case preview (ix (fromIntegral i - 1)) stk of             Nothing -> underrun             Just y ->               limitStack 1 $@@ -637,33 +634,29 @@                   next                   pushSym y -        -- op: SWAP-        x | x >= 0x90 && x <= 0x9f -> do-          let i = num (x - 0x90 + 1)-          if length stk < i + 1+        OpSwap i ->+          if length stk < (fromIntegral i) + 1             then underrun             else               burn g_verylow $ do                 next                 zoom (state . stack) $ do-                  assign (ix 0) (stk ^?! ix i)-                  assign (ix i) (stk ^?! ix 0)+                  assign (ix 0) (stk ^?! ix (fromIntegral i))+                  assign (ix (fromIntegral i)) (stk ^?! ix 0) -        -- op: LOG-        x | x >= 0xa0 && x <= 0xa4 ->+        OpLog n ->           notStatic $-          let n = (num x - 0xa0) in           case stk of             (xOffset':xSize':xs) ->-              if length xs < n+              if length xs < (fromIntegral n)               then underrun               else                 forceConcrete2 (xOffset', xSize') "LOG" $ \(xOffset, xSize) -> do-                    let (topics, xs') = splitAt n xs+                    let (topics, xs') = splitAt (fromIntegral n) xs                         bytes         = readMemory xOffset' xSize' vm                         logs'         = (LogEntry (litAddr self) bytes topics) : vm._logs                     burn (g_log + g_logdata * (num xSize) + num n * g_logtopic) $-                      accessMemoryRange fees xOffset xSize $ do+                      accessMemoryRange xOffset xSize $ do                         traceTopLog logs'                         next                         assign (state . stack) xs'@@ -671,74 +664,49 @@             _ ->               underrun -        -- op: STOP-        0x00 -> doStop+        OpStop -> doStop -        -- op: ADD-        0x01 -> stackOp2 (const g_verylow) (uncurry Expr.add)-        -- op: MUL-        0x02 -> stackOp2 (const g_low) (uncurry Expr.mul)-        -- op: SUB-        0x03 -> stackOp2 (const g_verylow) (uncurry Expr.sub)+        OpAdd -> stackOp2 g_verylow (uncurry Expr.add)+        OpMul -> stackOp2 g_low (uncurry Expr.mul)+        OpSub -> stackOp2 g_verylow (uncurry Expr.sub) -        -- op: DIV-        0x04 -> stackOp2 (const g_low) (uncurry Expr.div)+        OpDiv -> stackOp2 g_low (uncurry Expr.div) -        -- op: SDIV-        0x05 -> stackOp2 (const g_low) (uncurry Expr.sdiv)+        OpSdiv -> stackOp2 g_low (uncurry Expr.sdiv) -        -- op: MOD-        0x06 -> stackOp2 (const g_low) (uncurry Expr.mod)+        OpMod-> stackOp2 g_low (uncurry Expr.mod) -        -- op: SMOD-        0x07 -> stackOp2 (const g_low) (uncurry Expr.smod)-        -- op: ADDMOD-        0x08 -> stackOp3 (const g_mid) (uncurryN Expr.addmod)-        -- op: MULMOD-        0x09 -> stackOp3 (const g_mid) (uncurryN Expr.mulmod)+        OpSmod -> stackOp2 g_low (uncurry Expr.smod)+        OpAddmod -> stackOp3 g_mid (uncurryN Expr.addmod)+        OpMulmod -> stackOp3 g_mid (uncurryN Expr.mulmod) -        -- op: LT-        0x10 -> stackOp2 (const g_verylow) (uncurry Expr.lt)-        -- op: GT-        0x11 -> stackOp2 (const g_verylow) (uncurry Expr.gt)-        -- op: SLT-        0x12 -> stackOp2 (const g_verylow) (uncurry Expr.slt)-        -- op: SGT-        0x13 -> stackOp2 (const g_verylow) (uncurry Expr.sgt)+        OpLt -> stackOp2 g_verylow (uncurry Expr.lt)+        OpGt -> stackOp2 g_verylow (uncurry Expr.gt)+        OpSlt -> stackOp2 g_verylow (uncurry Expr.slt)+        OpSgt -> stackOp2 g_verylow (uncurry Expr.sgt) -        -- op: EQ-        0x14 -> stackOp2 (const g_verylow) (uncurry Expr.eq)-        -- op: ISZERO-        0x15 -> stackOp1 (const g_verylow) Expr.iszero+        OpEq -> stackOp2 g_verylow (uncurry Expr.eq)+        OpIszero -> stackOp1 g_verylow Expr.iszero -        -- op: AND-        0x16 -> stackOp2 (const g_verylow) (uncurry Expr.and)-        -- op: OR-        0x17 -> stackOp2 (const g_verylow) (uncurry Expr.or)-        -- op: XOR-        0x18 -> stackOp2 (const g_verylow) (uncurry Expr.xor)-        -- op: NOT-        0x19 -> stackOp1 (const g_verylow) Expr.not+        OpAnd -> stackOp2 g_verylow (uncurry Expr.and)+        OpOr -> stackOp2 g_verylow (uncurry Expr.or)+        OpXor -> stackOp2 g_verylow (uncurry Expr.xor)+        OpNot -> stackOp1 g_verylow Expr.not -        -- op: BYTE-        0x1a -> stackOp2 (const g_verylow) (\(i, w) -> Expr.padByte $ Expr.indexWord i w)+        OpByte -> stackOp2 g_verylow (\(i, w) -> Expr.padByte $ Expr.indexWord i w) -        -- op: SHL-        0x1b -> stackOp2 (const g_verylow) (uncurry Expr.shl)-        -- op: SHR-        0x1c -> stackOp2 (const g_verylow) (uncurry Expr.shr)-        -- op: SAR-        0x1d -> stackOp2 (const g_verylow) (uncurry Expr.sar)+        OpShl -> stackOp2 g_verylow (uncurry Expr.shl)+        OpShr -> stackOp2 g_verylow (uncurry Expr.shr)+        OpSar -> stackOp2 g_verylow (uncurry Expr.sar) -        -- op: SHA3         -- more accurately refered to as KECCAK-        0x20 ->+        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 (num xSize) 32) $-                    accessMemoryRange fees xOffset xSize $ do+                    accessMemoryRange xOffset xSize $ do                       (hash, invMap) <- case readMemory xOffset' xSize' vm of                                           ConcreteBuf bs -> do                                             let hash' = keccak' bs@@ -751,13 +719,11 @@                       (env . sha3Crack) <>= invMap             _ -> underrun -        -- op: ADDRESS-        0x30 ->+        OpAddress ->           limitStack 1 $             burn g_base (next >> push (num self)) -        -- op: BALANCE-        0x31 ->+        OpBalance ->           case stk of             (x':xs) -> forceConcrete x' "BALANCE" $ \x ->               accessAndBurn (num x) $@@ -768,50 +734,42 @@             [] ->               underrun -        -- op: ORIGIN-        0x32 ->+        OpOrigin ->           limitStack 1 . burn g_base $             next >> push (num vm._tx._origin) -        -- op: CALLER-        0x33 ->+        OpCaller ->           limitStack 1 . burn g_base $             next >> pushSym vm._state._caller -        -- op: CALLVALUE-        0x34 ->+        OpCallvalue ->           limitStack 1 . burn g_base $             next >> pushSym vm._state._callvalue -        -- op: CALLDATALOAD-        0x35 -> stackOp1 (const g_verylow) $+        OpCalldataload -> stackOp1 g_verylow $           \ind -> Expr.readWord ind vm._state._calldata -        -- op: CALLDATASIZE-        0x36 ->+        OpCalldatasize ->           limitStack 1 . burn g_base $             next >> pushSym (bufLength vm._state._calldata) -        -- op: CALLDATACOPY-        0x37 ->+        OpCalldatacopy ->           case stk of             (xTo' : xFrom : xSize' : xs) ->               forceConcrete2 (xTo', xSize') "CALLDATACOPY" $                 \(xTo, xSize) ->                   burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $-                    accessMemoryRange fees xTo xSize $ do+                    accessMemoryRange xTo xSize $ do                       next                       assign (state . stack) xs                       copyBytesToMemory vm._state._calldata xSize' xFrom xTo'             _ -> underrun -        -- op: CODESIZE-        0x38 ->+        OpCodesize ->           limitStack 1 . burn g_base $             next >> pushSym (codelen vm._state._code) -        -- op: CODECOPY-        0x39 ->+        OpCodecopy ->           case stk of             (memOffset' : codeOffset : n' : xs) ->               forceConcrete2 (memOffset', n') "CODECOPY" $@@ -821,20 +779,18 @@                     Just n'' ->                       if n'' <= ( (maxBound :: Word64) - g_verylow ) `div` g_copy * 32 then                         burn (g_verylow + g_copy * ceilDiv (num n) 32) $-                          accessMemoryRange fees memOffset n $ do+                          accessMemoryRange memOffset n $ do                             next                             assign (state . stack) xs                             copyBytesToMemory (toBuf vm._state._code) n' codeOffset memOffset'                       else vmError IllegalOverflow             _ -> underrun -        -- op: GASPRICE-        0x3a ->+        OpGasprice ->           limitStack 1 . burn g_base $             next >> push vm._tx._gasprice -        -- op: EXTCODESIZE-        0x3b ->+        OpExtcodesize ->           case stk of             (x':xs) -> case x' of               (Lit x) -> if x == num cheatCode@@ -855,8 +811,7 @@             [] ->               underrun -        -- op: EXTCODECOPY-        0x3c ->+        OpExtcodecopy ->           case stk of             ( extAccount'               : memOffset'@@ -868,29 +823,27 @@                   acc <- accessAccountForGas (num extAccount)                   let cost = if acc then g_warm_storage_read else g_cold_account_access                   burn (cost + g_copy * ceilDiv (num codeSize) 32) $-                    accessMemoryRange fees memOffset codeSize $+                    accessMemoryRange memOffset codeSize $                       fetchAccount (num extAccount) $ \c -> do                         next                         assign (state . stack) xs                         copyBytesToMemory (view bytecode c) codeSize' codeOffset memOffset'             _ -> underrun -        -- op: RETURNDATASIZE-        0x3d ->+        OpReturndatasize ->           limitStack 1 . burn g_base $             next >> pushSym (bufLength vm._state._returndata) -        -- op: RETURNDATACOPY-        0x3e ->+        OpReturndatacopy ->           case stk of             (xTo' : xFrom : xSize' :xs) -> forceConcrete2 (xTo', xSize') "RETURNDATACOPY" $               \(xTo, xSize) ->                 burn (g_verylow + g_copy * ceilDiv (num xSize) 32) $-                  accessMemoryRange fees xTo xSize $ do+                  accessMemoryRange xTo xSize $ do                     next                     assign (state . stack) xs -                    let jump True = vmError EVM.InvalidMemoryAccess+                    let jump True = vmError EVM.ReturnDataOutOfBounds                         jump False = copyBytesToMemory vm._state._returndata xSize' xFrom xTo'                      case (xFrom, bufLength vm._state._returndata) of@@ -903,8 +856,7 @@                         branch loc (Expr.or oob overflow) jump             _ -> underrun -        -- op: EXTCODEHASH-        0x3f ->+        OpExtcodehash ->           case stk of             (x':xs) -> forceConcrete x' "EXTCODEHASH" $ \x ->               accessAndBurn (num x) $ do@@ -917,97 +869,83 @@             [] ->               underrun -        -- op: BLOCKHASH-        0x40 -> do+        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 (const g_blockhash) $ \case+          stackOp1 g_blockhash $ \case             (Lit i) -> if i + 256 < vm._block._number || i >= vm._block._number                        then Lit 0                        else (num i :: Integer) & show & Char8.pack & keccak' & Lit             i -> BlockHash i -        -- op: COINBASE-        0x41 ->+        OpCoinbase ->           limitStack 1 . burn g_base $             next >> push (num vm._block._coinbase) -        -- op: TIMESTAMP-        0x42 ->+        OpTimestamp ->           limitStack 1 . burn g_base $             next >> pushSym vm._block._timestamp -        -- op: NUMBER-        0x43 ->+        OpNumber ->           limitStack 1 . burn g_base $             next >> push vm._block._number -        -- op: PREVRANDAO-        0x44 -> do+        OpPrevRandao -> do           limitStack 1 . burn g_base $             next >> push vm._block._prevRandao -        -- op: GASLIMIT-        0x45 ->+        OpGaslimit ->           limitStack 1 . burn g_base $             next >> push (num vm._block._gaslimit) -        -- op: CHAINID-        0x46 ->+        OpChainid ->           limitStack 1 . burn g_base $             next >> push vm._env._chainId -        -- op: SELFBALANCE-        0x47 ->+        OpSelfbalance ->           limitStack 1 . burn g_low $             next >> push this._balance -        -- op: BASEFEE-        0x48 ->+        OpBaseFee ->           limitStack 1 . burn g_base $             next >> push vm._block._baseFee -        -- op: POP-        0x50 ->+        OpPop ->           case stk of             (_:xs) -> burn g_base (next >> assign (state . stack) xs)             _      -> underrun -        -- op: MLOAD-        0x51 ->+        OpMload ->           case stk of             (x':xs) -> forceConcrete x' "MLOAD" $ \x ->               burn g_verylow $-                accessMemoryWord fees x $ do+                accessMemoryWord x $ do                   next                   assign (state . stack) (readWord (Lit x) mem : xs)             _ -> underrun -        -- op: MSTORE-        0x52 ->+        OpMstore ->           case stk of             (x':y:xs) -> forceConcrete x' "MSTORE index" $ \x ->               burn g_verylow $-                accessMemoryWord fees x $ do+                accessMemoryWord x $ do                   next                   assign (state . memory) (writeWord (Lit x) y mem)                   assign (state . stack) xs             _ -> underrun -        -- op: MSTORE8-        0x53 ->+        OpMstore8 ->           case stk of             (x':y:xs) -> forceConcrete x' "MSTORE8" $ \x ->               burn g_verylow $-                accessMemoryRange fees x 1 $ do+                accessMemoryRange x 1 $ do                   let yByte = indexWord (Lit 31) y                   next                   modifying (state . memory) (writeByte (Lit x) yByte)                   assign (state . stack) xs             _ -> underrun -        -- op: SLOAD-        0x54 ->+        OpSload ->           case stk of             (x:xs) -> do               acc <- accessStorageForGas self x@@ -1018,8 +956,7 @@                   assign (state . stack) (y:xs)             _ -> underrun -        -- op: SSTORE-        0x55 ->+        OpSstore ->           notStatic $           case stk of             (x:new:xs) ->@@ -1071,8 +1008,7 @@                          _ -> noop             _ -> underrun -        -- op: JUMP-        0x56 ->+        OpJump ->           case stk of             (x:xs) ->               burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->@@ -1081,8 +1017,7 @@                   Just i -> checkJump i xs             _ -> underrun -        -- op: JUMPI-        0x57 -> do+        OpJumpi -> do           case stk of             (x:y:xs) -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->                 burn g_high $@@ -1099,26 +1034,21 @@                         branch loc y jump             _ -> underrun -        -- op: PC-        0x58 ->+        OpPc ->           limitStack 1 . burn g_base $             next >> push (num vm._state._pc) -        -- op: MSIZE-        0x59 ->+        OpMsize ->           limitStack 1 . burn g_base $             next >> push (num vm._state._memorySize) -        -- op: GAS-        0x5a ->+        OpGas ->           limitStack 1 . burn g_base $             next >> push (num (vm._state._gas - g_base)) -        -- op: JUMPDEST-        0x5b -> burn g_jumpdest next+        OpJumpdest -> burn g_jumpdest next -        -- op: EXP-        0x0a ->+        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@@ -1132,16 +1062,14 @@                 state . stack .= Expr.exp base exponent' : xs             _ -> underrun -        -- op: SIGNEXTEND-        0x0b -> stackOp2 (const g_low) (uncurry Expr.sex)+        OpSignextend -> stackOp2 g_low (uncurry Expr.sex) -        -- op: CREATE-        0xf0 ->+        OpCreate ->           notStatic $           case stk of             (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') "CREATE" $               \(xValue, xOffset, xSize) -> do-                accessMemoryRange fees xOffset xSize $ do+                accessMemoryRange xOffset xSize $ do                   availableGas <- use (state . gas)                   let                     newAddr = createAddress self this._nonce@@ -1155,8 +1083,7 @@                     create self this (num gas') xValue xs newAddr initCode             _ -> underrun -        -- op: CALL-        0xf1 ->+        OpCall ->           case stk of             ( xGas'               : xTo@@ -1181,8 +1108,7 @@             _ ->               underrun -        -- op: CALLCODE-        0xf2 ->+        OpCallcode ->           case stk of             ( xGas'               : xTo@@ -1203,11 +1129,10 @@             _ ->               underrun -        -- op: RETURN-        0xf3 ->+        OpReturn ->           case stk of             (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') "RETURN" $ \(xOffset, xSize) ->-              accessMemoryRange fees xOffset xSize $ do+              accessMemoryRange xOffset xSize $ do                 let                   output = readMemory xOffset' xSize' vm                   codesize = fromMaybe (error "RETURN: cannot return dynamically sized abstract data")@@ -1239,8 +1164,7 @@                    finishFrame (FrameReturned output)             _ -> underrun -        -- op: DELEGATECALL-        0xf4 ->+        OpDelegatecall ->           case stk of             (xGas'              :xTo@@ -1254,8 +1178,7 @@                   touchAccount self             _ -> underrun -        -- op: CREATE2-        0xf5 -> notStatic $+        OpCreate2 -> notStatic $           case stk of             (xValue'              :xOffset'@@ -1263,7 +1186,7 @@              :xSalt'              :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') "CREATE2" $               \(xValue, xOffset, xSize, xSalt) ->-                accessMemoryRange fees xOffset xSize $ do+                accessMemoryRange xOffset xSize $ do                   availableGas <- use (state . gas)                    forceConcreteBuf (readMemory xOffset' xSize' vm) "CREATE2" $@@ -1275,8 +1198,7 @@                       burn (cost - gas') $ create self this gas' xValue xs newAddr (ConcreteBuf initCode)             _ -> underrun -        -- op: STATICCALL-        0xfa ->+        OpStaticcall ->           case stk of             (xGas'              :xTo@@ -1298,8 +1220,7 @@             _ ->               underrun -        -- op: SELFDESTRUCT-        0xff ->+        OpSelfdestruct ->           notStatic $           case stk of             [] -> underrun@@ -1322,16 +1243,15 @@                           doStop                    else doStop -        -- op: REVERT-        0xfd ->+        OpRevert ->           case stk of             (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') "REVERT" $ \(xOffset, xSize) ->-              accessMemoryRange fees xOffset xSize $ do+              accessMemoryRange xOffset xSize $ do                 let output = readMemory xOffset' xSize' vm                 finishFrame (FrameReverted output)             _ -> underrun -        xxx ->+        OpUnknown xxx ->           vmError (UnrecognizedOpcode xxx)  transfer :: Addr -> Addr -> W256 -> EVM ()@@ -1350,8 +1270,8 @@ callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue = do   vm <- get   let fees = vm._block._schedule-  accessMemoryRange fees xInOffset xInSize $-    accessMemoryRange fees xOutOffset xOutSize $ do+  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@@ -1996,51 +1916,28 @@       action "sign(uint256,bytes32)" $         \sig outOffset _ input -> case decodeStaticArgs 0 2 input of           [sk, hash] ->-            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> let-              curve = getCurveByName SEC_p256k1-              priv = PrivateKey curve (num sk')-              digest = digestFromByteString (word256Bytes hash')-            in do-              case digest of-                Nothing -> vmError (BadCheatCode sig)-                Just digest' -> do-                  let s = ethsign priv digest'-                      -- calculating the V value is pretty annoying if you-                      -- don't have access to the full X/Y coords of the-                      -- signature (which we don't get back from cryptonite).-                      -- Luckily since we use a fixed nonce (to avoid the-                      -- overhead of bringing randomness into the core EVM-                      -- semantics), it would appear that every signature we-                      -- produce has v == 28. Definitely a hack, and also bad-                      -- for code that somehow depends on the value of v, but-                      -- that seems acceptable for now.-                      v = 28-                      encoded = encodeAbiValue $-                        AbiTuple (RegularVector.fromList-                          [ AbiUInt 8 v-                          , AbiBytes 32 (word256Bytes . fromInteger $ sign_r s)-                          , AbiBytes 32 (word256Bytes . fromInteger $ sign_s s)-                          ])-                  assign (state . returndata) (ConcreteBuf encoded)-                  copyBytesToMemory (ConcreteBuf encoded) (Lit . num . BS.length $ encoded) (Lit 0) outOffset+            forceConcrete2 (sk, hash) "cannot sign symbolic data" $ \(sk', hash') -> do+              let (v,r,s) = EVM.Sign.sign hash' (toInteger sk')+                  encoded = encodeAbiValue $+                    AbiTuple (RegularVector.fromList+                      [ AbiUInt 8 $ num v+                      , AbiBytes 32 (word256Bytes r)+                      , AbiBytes 32 (word256Bytes s)+                      ])+              assign (state . returndata) (ConcreteBuf encoded)+              copyBytesToMemory (ConcreteBuf encoded) (Lit . num . 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' -> let-                curve = getCurveByName SEC_p256k1-                pubPoint = generateQ curve (num sk')-                encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger-              in do-                case pubPoint of-                  PointO -> do vmError (BadCheatCode sig)-                  Point x y -> do-                    -- See yellow paper #286-                    let-                      pub = BS.concat [ encodeInt x, encodeInt y ]-                      addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub-                    assign (state . returndata . word256At (Lit 0)) addr-                    assign (state . memory . word256At outOffset) addr+          [sk] -> forceConcrete sk "cannot derive address for a symbolic key" $ \sk' -> do+            let a = EVM.Sign.deriveAddr $ num sk'+            case a of+              Nothing -> vmError (BadCheatCode sig)+              Just address -> do+                let expAddr = litAddr address+                assign (state . returndata . word256At (Lit 0)) expAddr+                assign (state . memory . word256At outOffset) expAddr           _ -> vmError (BadCheatCode sig),        action "prank(address)" $@@ -2422,14 +2319,14 @@ -- * Memory helpers  accessUnboundedMemoryRange-  :: FeeSchedule Word64-  -> Word64+  :: Word64   -> Word64   -> EVM ()   -> EVM ()-accessUnboundedMemoryRange _ _ 0 continue = continue-accessUnboundedMemoryRange fees f l continue = do+accessUnboundedMemoryRange _ 0 continue = continue+accessUnboundedMemoryRange f l continue = do   m0 <- num <$> use (state . memorySize)+  fees <- gets (._block._schedule)   do     let m1 = 32 * ceilDiv (max m0 (f + l)) 32     burn (memoryCost fees m1 - memoryCost fees m0) $ do@@ -2437,23 +2334,22 @@       continue  accessMemoryRange-  :: FeeSchedule Word64-  -> W256+  :: W256   -> W256   -> EVM ()   -> EVM ()-accessMemoryRange _ _ 0 continue = continue-accessMemoryRange fees f l continue =+accessMemoryRange _ 0 continue = continue+accessMemoryRange f l continue =   case (,) <$> toWord64 f <*> toWord64 l of     Nothing -> vmError IllegalOverflow     Just (f64, l64) ->       if f64 + l64 < l64         then vmError IllegalOverflow-        else accessUnboundedMemoryRange fees f64 l64 continue+        else accessUnboundedMemoryRange f64 l64 continue  accessMemoryWord-  :: FeeSchedule Word64 -> W256 -> EVM () -> EVM ()-accessMemoryWord fees x = accessMemoryRange fees x 32+  :: W256 -> EVM () -> EVM ()+accessMemoryWord x = accessMemoryRange x 32  copyBytesToMemory   :: Expr Buf -> Expr EWord -> Expr EWord -> Expr EWord -> EVM ()@@ -2535,13 +2431,13 @@  stackOp1   :: (?op :: Word8)-  => ((Expr EWord) -> Word64)+  => Word64   -> ((Expr EWord) -> (Expr EWord))   -> EVM () stackOp1 cost f =   use (state . stack) >>= \case     (x:xs) ->-      burn (cost x) $ do+      burn cost $ do         next         let !y = f x         state . stack .= y : xs@@ -2550,13 +2446,13 @@  stackOp2   :: (?op :: Word8)-  => (((Expr EWord), (Expr EWord)) -> Word64)+  => Word64   -> (((Expr EWord), (Expr EWord)) -> (Expr EWord))   -> EVM () stackOp2 cost f =   use (state . stack) >>= \case     (x:y:xs) ->-      burn (cost (x, y)) $ do+      burn cost $ do         next         state . stack .= f (x, y) : xs     _ ->@@ -2564,13 +2460,13 @@  stackOp3   :: (?op :: Word8)-  => (((Expr EWord), (Expr EWord), (Expr EWord)) -> Word64)+  => Word64   -> (((Expr EWord), (Expr EWord), (Expr EWord)) -> (Expr EWord))   -> EVM () stackOp3 cost f =   use (state . stack) >>= \case     (x:y:z:xs) ->-      burn (cost (x, y, z)) $ do+      burn cost $ do       next       state . stack .= f (x, y, z) : xs     _ ->@@ -2692,89 +2588,6 @@       if length (vm ^. state . stack) >= length xs       then Map.fromList (zip xs (vm ^. state . stack))       else mempty---- | Reads-readOp :: Word8 -> [Expr Byte] -> Op-readOp x _  | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)-readOp x _  | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1)-readOp x _  | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0)-readOp x xs | x >= 0x60 && x <= 0x7f =-  let n = num $ x - 0x60 + 1-  in OpPush (readBytes n (Lit 0) (Expr.fromList $ V.fromList xs))-readOp x _ = case x of-  0x00 -> OpStop-  0x01 -> OpAdd-  0x02 -> OpMul-  0x03 -> OpSub-  0x04 -> OpDiv-  0x05 -> OpSdiv-  0x06 -> OpMod-  0x07 -> OpSmod-  0x08 -> OpAddmod-  0x09 -> OpMulmod-  0x0a -> OpExp-  0x0b -> OpSignextend-  0x10 -> OpLt-  0x11 -> OpGt-  0x12 -> OpSlt-  0x13 -> OpSgt-  0x14 -> OpEq-  0x15 -> OpIszero-  0x16 -> OpAnd-  0x17 -> OpOr-  0x18 -> OpXor-  0x19 -> OpNot-  0x1a -> OpByte-  0x1b -> OpShl-  0x1c -> OpShr-  0x1d -> OpSar-  0x20 -> OpSha3-  0x30 -> OpAddress-  0x31 -> OpBalance-  0x32 -> OpOrigin-  0x33 -> OpCaller-  0x34 -> OpCallvalue-  0x35 -> OpCalldataload-  0x36 -> OpCalldatasize-  0x37 -> OpCalldatacopy-  0x38 -> OpCodesize-  0x39 -> OpCodecopy-  0x3a -> OpGasprice-  0x3b -> OpExtcodesize-  0x3c -> OpExtcodecopy-  0x3d -> OpReturndatasize-  0x3e -> OpReturndatacopy-  0x3f -> OpExtcodehash-  0x40 -> OpBlockhash-  0x41 -> OpCoinbase-  0x42 -> OpTimestamp-  0x43 -> OpNumber-  0x44 -> OpPrevRandao-  0x45 -> OpGaslimit-  0x46 -> OpChainid-  0x47 -> OpSelfbalance-  0x50 -> OpPop-  0x51 -> OpMload-  0x52 -> OpMstore-  0x53 -> OpMstore8-  0x54 -> OpSload-  0x55 -> OpSstore-  0x56 -> OpJump-  0x57 -> OpJumpi-  0x58 -> OpPc-  0x59 -> OpMsize-  0x5a -> OpGas-  0x5b -> OpJumpdest-  0xf0 -> OpCreate-  0xf1 -> OpCall-  0xf2 -> OpCallcode-  0xf3 -> OpReturn-  0xf4 -> OpDelegatecall-  0xf5 -> OpCreate2-  0xfd -> OpRevert-  0xfa -> OpStaticcall-  0xff -> OpSelfdestruct-  _    -> OpUnknown x  -- Maps operation indicies into a pair of (bytecode index, operation) mkCodeOps :: ContractCode -> RegularVector.Vector (Int, Op)

@@ -101,6 +101,7 @@   | AbiArrayDynamic AbiType (Vector AbiValue)   | AbiArray        Int AbiType (Vector AbiValue)   | AbiTuple        (Vector AbiValue)+  | AbiFunction     BS.ByteString   deriving (Read, Eq, Ord, Generic)  -- | Pretty-print some 'AbiValue'.@@ -118,6 +119,7 @@     "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]"   show (AbiTuple v) =     "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")"+  show (AbiFunction b)       = show (ByteStringS b)  formatString :: ByteString -> String formatString bs =@@ -136,6 +138,7 @@   | AbiArrayDynamicType AbiType   | AbiArrayType        Int AbiType   | AbiTupleType        (Vector AbiType)+  | AbiFunctionType   deriving (Read, Eq, Ord, Generic)  instance Show AbiType where@@ -174,6 +177,7 @@   AbiArrayDynamic t _ -> AbiArrayDynamicType t   AbiArray n t _      -> AbiArrayType n t   AbiTuple v          -> AbiTupleType (abiValueType <$> v)+  AbiFunction _       -> AbiFunctionType  abiTypeSolidity :: AbiType -> Text abiTypeSolidity = \case@@ -187,6 +191,7 @@   AbiArrayDynamicType t -> abiTypeSolidity t <> "[]"   AbiArrayType n t      -> abiTypeSolidity t <> "[" <> pack (show n) <> "]"   AbiTupleType ts       -> "(" <> (Text.intercalate "," . Vector.toList $ abiTypeSolidity <$> ts) <> ")"+  AbiFunctionType       -> "function"  getAbi :: AbiType -> Get AbiValue getAbi t = label (Text.unpack (abiTypeSolidity t)) $@@ -224,6 +229,9 @@     AbiTupleType ts ->       AbiTuple <$> getAbiSeq (Vector.length ts) (Vector.toList ts) +    AbiFunctionType ->+      AbiFunction <$> getBytesWith256BitPadding (24 :: Int)+ putAbi :: AbiValue -> Put putAbi = \case   AbiUInt _ x ->@@ -256,6 +264,9 @@   AbiTuple v ->     putAbiSeq v +  AbiFunction b -> do+    putAbi (AbiBytes 24 b)+ -- | Decode a sequence type (e.g. tuple / array). Will fail for non sequence types getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue) getAbiSeq n ts = label "sequence" $ do@@ -308,6 +319,7 @@         AbiBool _    -> 32         AbiTuple v   -> sum (abiHeadSize <$> v)         AbiArray _ _ xs -> sum (abiHeadSize <$> xs)+        AbiFunction _ -> 32         _ -> error "impossible"  putAbiSeq :: Vector AbiValue -> Put@@ -370,6 +382,7 @@      , P.string "bytes" $> AbiBytesDynamicType     , P.string "tuple" $> AbiTupleType v+    , P.string "function" $> AbiFunctionType     ]    where@@ -430,6 +443,9 @@        replicateM n (scale (`div` 2) (genAbiValue t))    AbiTupleType ts ->      AbiTuple <$> mapM genAbiValue ts+   AbiFunctionType ->+     do xs <- replicateM 24 arbitrary+        pure (AbiFunction (BS.pack xs))   where     genUInt :: Int -> Gen Word256     genUInt n = arbitraryIntegralWithMax (2^n-1) :: Gen Word256@@ -471,6 +487,7 @@     AbiBool b -> AbiBool <$> shrink b     AbiAddress a -> [AbiAddress 0xacab, AbiAddress 0xdeadbeef, AbiAddress 0xbabeface]       <> (AbiAddress <$> shrinkIntegral a)+    AbiFunction b -> shrink $ AbiBytes 24 b   -- Bool synonym with custom read instance@@ -516,6 +533,8 @@   AbiArray n typ <$> do a <- listP (parseAbiValue typ)                         return $ Vector.fromList a parseAbiValue (AbiTupleType _) = error "tuple types not supported"+parseAbiValue AbiFunctionType = AbiFunction <$> do ByteStringS bytes <- bytesP+                                                   return bytes  listP :: ReadP a -> ReadP [a] listP parser = between (char '[') (char ']') ((do skipSpaces@@ -527,7 +546,7 @@ bytesP = do   _ <- string "0x"   hex <- munch isHexDigit-  case BS16.decode (encodeUtf8 (Text.pack hex)) of+  case BS16.decodeBase16 (encodeUtf8 (Text.pack hex)) of     Right d -> pure $ ByteStringS d     Left _ -> pfail 

@@ -0,0 +1,109 @@+{-|+Module      : Assembler+Description : Assembler for EVM opcodes used in the HEVM symbolic checker+-}++{-# LANGUAGE DataKinds #-}++module EVM.Assembler where++import EVM.Op+import EVM.Types+import qualified EVM.Expr as Expr++import qualified Data.Vector as V+import Data.Vector (Vector)++assemble :: [Op] -> Vector (Expr Byte)+assemble os = V.fromList $ concatMap go os+  where+    go :: Op -> [Expr Byte]+    go = \case+      OpStop -> [LitByte 0x00]+      OpAdd -> [LitByte 0x01]+      OpMul -> [LitByte 0x02]+      OpSub -> [LitByte 0x03]+      OpDiv -> [LitByte 0x04]+      OpSdiv -> [LitByte 0x05]+      OpMod -> [LitByte 0x06]+      OpSmod -> [LitByte 0x07]+      OpAddmod -> [LitByte 0x08]+      OpMulmod -> [LitByte 0x09]+      OpExp -> [LitByte 0x0A]+      OpSignextend -> [LitByte 0x0B]+      OpLt -> [LitByte 0x10]+      OpGt -> [LitByte 0x11]+      OpSlt -> [LitByte 0x12]+      OpSgt -> [LitByte 0x13]+      OpEq -> [LitByte 0x14]+      OpIszero -> [LitByte 0x15]+      OpAnd -> [LitByte 0x16]+      OpOr -> [LitByte 0x17]+      OpXor -> [LitByte 0x18]+      OpNot -> [LitByte 0x19]+      OpByte -> [LitByte 0x1A]+      OpShl -> [LitByte 0x1B]+      OpShr -> [LitByte 0x1C]+      OpSar -> [LitByte 0x1D]+      OpSha3 -> [LitByte 0x20]+      OpAddress -> [LitByte 0x30]+      OpBalance -> [LitByte 0x31]+      OpOrigin -> [LitByte 0x32]+      OpCaller -> [LitByte 0x33]+      OpCallvalue -> [LitByte 0x34]+      OpCalldataload -> [LitByte 0x35]+      OpCalldatasize -> [LitByte 0x36]+      OpCalldatacopy -> [LitByte 0x37]+      OpCodesize -> [LitByte 0x38]+      OpCodecopy -> [LitByte 0x39]+      OpGasprice -> [LitByte 0x3A]+      OpExtcodesize -> [LitByte 0x3B]+      OpExtcodecopy -> [LitByte 0x3C]+      OpReturndatasize -> [LitByte 0x3D]+      OpReturndatacopy -> [LitByte 0x3E]+      OpExtcodehash -> [LitByte 0x3F]+      OpBlockhash -> [LitByte 0x40]+      OpCoinbase -> [LitByte 0x41]+      OpTimestamp -> [LitByte 0x42]+      OpNumber -> [LitByte 0x43]+      OpPrevRandao -> [LitByte 0x44]+      OpGaslimit -> [LitByte 0x45]+      OpChainid -> [LitByte 0x46]+      OpSelfbalance -> [LitByte 0x47]+      OpBaseFee -> [LitByte 0x48]+      OpPop -> [LitByte 0x50]+      OpMload -> [LitByte 0x51]+      OpMstore -> [LitByte 0x52]+      OpMstore8 -> [LitByte 0x53]+      OpSload -> [LitByte 0x54]+      OpSstore -> [LitByte 0x55]+      OpJump -> [LitByte 0x56]+      OpJumpi -> [LitByte 0x57]+      OpPc -> [LitByte 0x58]+      OpMsize -> [LitByte 0x59]+      OpGas -> [LitByte 0x5A]+      OpJumpdest -> [LitByte 0x5B]+      OpCreate -> [LitByte 0xF0]+      OpCall -> [LitByte 0xF1]+      OpStaticcall -> [LitByte 0xFA]+      OpCallcode -> [LitByte 0xF2]+      OpReturn -> [LitByte 0xF3]+      OpDelegatecall -> [LitByte 0xF4]+      OpCreate2 -> [LitByte 0xF5]+      OpRevert -> [LitByte 0xFD]+      OpSelfdestruct -> [LitByte 0xFF]+      OpDup n ->+        if 1 <= n && n <= 16+        then [LitByte (0x80 + (n - 1))]+        else error $ "Internal Error: invalid argument to OpDup: " <> show n+      OpSwap n ->+        if 1 <= n && n <= 16+        then [LitByte (0x90 + (n - 1))]+        else error $ "Internal Error: invalid argument to OpSwap: " <> show n+      OpLog n ->+        if 0 <= n && n <= 4+        then [LitByte (0xA0 + n)]+        else error $ "Internal Error: invalid argument to OpLog: " <> show n+      -- we just always assemble OpPush into PUSH32+      OpPush wrd -> (LitByte 0x7f) : [Expr.indexWord (Lit i) wrd | i <- [0..31]]+      OpUnknown o -> [LitByte o]

@@ -1,5 +1,3 @@-{-# Language StrictData #-}- module EVM.Concrete where  import Prelude hiding (Word)

@@ -1,3 +1,5 @@+{-# Language DataKinds #-}+ module EVM.Debug where  import EVM          (Contract, nonce, balance, bytecode, codehash)

@@ -25,6 +25,7 @@ import qualified Data.Vector as V import qualified Data.Vector.Storable as VS import Data.Vector.Storable.ByteString+import Data.Semigroup (Any, Any(..), getAny)   -- ** Stack Ops ** ---------------------------------------------------------------------------------@@ -136,7 +137,7 @@   in if sx < sy then 1 else 0)  sgt :: Expr EWord -> Expr EWord -> Expr EWord-sgt = op2 SLT (\x y ->+sgt = op2 SGT (\x y ->   let sx, sy :: Int256       sx = fromIntegral x       sy = fromIntegral y@@ -224,11 +225,9 @@     then readByte (Lit $ x - (dstOffset - srcOffset)) src     else readByte i dst readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) (Lit size) _ dst)-  = if x < dstOffset || x >= dstOffset + size-    then readByte i dst-    else ReadByte (Lit x) buf-readByte i@(Lit x) buf@(CopySlice _ (Lit dstOffset) _ _ dst)-  = if x < dstOffset+  -- the byte we are trying to read is compeletely outside of the sliced reegion+  -- we check that there is no overflow and that addresses do not wrap around+  = if (x < dstOffset || x >= dstOffset + size) && (dstOffset <= dstOffset + size)     then readByte i dst     else ReadByte (Lit x) buf @@ -262,7 +261,8 @@   -- the region we are trying to read is enclosed in the sliced region   | idx >= dstOff && idx + 32 <= dstOff + size = readWord (Lit $ srcOff + (idx - dstOff)) src   -- the region we are trying to read is compeletely outside of the sliced reegion-  | idx >= dstOff + size || idx + 32 <= dstOff = readWord (Lit idx) dst+  -- we check that there is no overflow and that addresses do not wrap around+  | (idx >= dstOff + size || idx + 32 <= dstOff) && (dstOff<= dstOff + size) = readWord (Lit idx) dst   -- the region we are trying to read partially overlaps the sliced region   | otherwise = readWordFromBytes (Lit idx) b readWord i b = readWordFromBytes i b@@ -403,17 +403,24 @@ -- If there are any writes to abstract locations, or CopySlices with an -- abstract size or dstOffset, an abstract expresion will be returned. bufLength :: Expr Buf -> Expr EWord-bufLength buf = case go 0 buf of-                  Just len -> len-                  Nothing -> BufLength buf+bufLength = bufLengthEnv mempty False++bufLengthEnv :: Map.Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord+bufLengthEnv env useEnv buf = go (Lit 0) buf   where-    go :: W256 -> Expr Buf -> Maybe (Expr EWord)-    go l (ConcreteBuf b) = Just . Lit $ max (num . BS.length $ b) l-    go l (WriteWord (Lit idx) _ b) = go (max l (idx + 32)) b-    go l (WriteByte (Lit idx) _ b) = go (max l (idx + 1)) b-    go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (max (dstOffset + size) l) dst-    go _ _ = Nothing+    go :: Expr EWord -> Expr Buf -> Expr EWord+    go l (ConcreteBuf b) = EVM.Expr.max l (Lit (num . BS.length $ b))+    go l (AbstractBuf b) = 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 +    go l (GVar (BufVar a)) | useEnv =+      case Map.lookup a env of+        Just b -> go l b+        Nothing -> error "Internal error: cannot compute length of open expression"+    go l (GVar (BufVar a)) = EVM.Expr.max l (BufLength (GVar (BufVar a)))+ -- | If a buffer has a concrete prefix, we return it's length here concPrefix :: Expr Buf -> Maybe Integer concPrefix (CopySlice (Lit srcOff) (Lit _) (Lit _) src (ConcreteBuf "")) = do@@ -423,22 +430,44 @@     go :: W256 -> Expr Buf -> Maybe Integer     -- base cases     go _ (AbstractBuf _) = Nothing-    go l (ConcreteBuf b) = Just . num $ max (num . BS.length $ b) l+    go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l      -- writes to a concrete index-    go l (WriteWord (Lit idx) (Lit _) b) = go (max l (idx + 32)) b-    go l (WriteByte (Lit idx) (LitByte _) b) = go (max l (idx + 1)) b-    go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (max (dstOffset + size) l) dst+    go l (WriteWord (Lit idx) (Lit _) b) = go (Prelude.max l (idx + 32)) b+    go l (WriteByte (Lit idx) (LitByte _) b) = go (Prelude.max l (idx + 1)) b+    go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (Prelude.max (dstOffset + size) l) dst      -- writes to an abstract index are ignored     go l (WriteWord _ _ b) = go l b     go l (WriteByte _ _ b) = go l b     go _ (CopySlice _ _ _ _ _) = error "Internal Error: cannot compute a concrete prefix length for nested copySlice expressions"-    go _ (GVar _) = error "Internal error: cannot calculate minLength of an open expression"+    go _ (GVar _) = error "Internal error: cannot calculate a concrete prefix of an open expression" concPrefix (ConcreteBuf b) = Just (num . BS.length $ b) concPrefix e = error $ "Internal error: cannot compute a concrete prefix length for: " <> show e  +-- | Return the minimum possible length of a buffer. In the case of an+-- abstract buffer, it is the largest write that is made on a concrete+-- location. Parameterized by an environment for buffer variables.+minLength :: Map.Map Int (Expr Buf) -> Expr Buf -> Maybe Integer+minLength bufEnv = go 0+  where+    go :: W256 -> Expr Buf -> Maybe Integer+    -- base cases+    go l (AbstractBuf _) = if l == 0 then Nothing else Just $ num l+    go l (ConcreteBuf b) = Just . num $ Prelude.max (num . BS.length $ b) l+    -- writes to a concrete index+    go l (WriteWord (Lit idx) _ b) = go (Prelude.max l (idx + 32)) b+    go l (WriteByte (Lit idx) _ b) = go (Prelude.max l (idx + 1)) b+    go l (CopySlice _ (Lit dstOffset) (Lit size) _ dst) = go (Prelude.max (dstOffset + size) l) dst+    -- writes to an abstract index are ignored+    go l (WriteWord _ _ b) = go l b+    go l (WriteByte _ _ b) = go l b+    go l (CopySlice _ _ _ _ b) = go l b+    go l (GVar (BufVar a)) = do+      b <- Map.lookup a bufEnv+      go l b+ word256At   :: Functor f   => Expr EWord -> (Expr EWord -> f (Expr EWord))@@ -763,6 +792,9 @@     -- Double NOT is a no-op, since it's a bitwise inversion     go (EVM.Types.Not (EVM.Types.Not a)) = a +    go (Max (Lit 0) a) = a+    go (Min (Lit 0) _) = Lit 0+     go a = a  @@ -772,6 +804,10 @@ litAddr :: Addr -> Expr EWord litAddr = Lit . num +exprToAddr :: Expr EWord -> Maybe Addr+exprToAddr (Lit x) = Just (num x)+exprToAddr _ = Nothing+ litCode :: BS.ByteString -> [Expr Byte] litCode bs = fmap LitByte (BS.unpack bs) @@ -927,12 +963,23 @@ eqByte x y = EqByte x y  min :: Expr EWord -> Expr EWord -> Expr EWord-min (Lit x) (Lit y) = if x < y then Lit x else Lit y-min x y = Min x y+min x y = normArgs Min Prelude.min x y +max :: Expr EWord -> Expr EWord -> Expr EWord+max x y = normArgs Max Prelude.max x y+ numBranches :: Expr End -> Int numBranches (ITE _ t f) = numBranches t + numBranches f numBranches _ = 1  allLit :: [Expr Byte] -> Bool allLit = Data.List.and . fmap (isLitByte)++-- | True if the given expression contains any node that satisfies the+-- input predicate+containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool+containsNode p = getAny . foldExpr go (Any False)+  where+    go :: Expr a -> Any+    go node | p node  = Any True+    go _ = Any False

@@ -102,9 +102,9 @@   load = readMaybe . Char8.unpack  instance AsASCII ByteString where-  dump x = BS16.encode x <> "\n"+  dump x = BS16.encodeBase16' x <> "\n"   load x =-    case BS16.decode . mconcat . BS.split 10 $ x of+    case BS16.decodeBase16 . mconcat . BS.split 10 $ x of       Right y -> Just y       _       -> Nothing 

@@ -27,16 +27,16 @@ import Prelude hiding (Word)  import EVM qualified-import EVM (VM, cheatCode, traceForest, Error(..), Trace,-  TraceData(..), Query(..), FrameContext(..))-import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError(..),-  Indexed(NotIndexed), getAbiSeq, parseTypeName, formatString)+import EVM (VM, cheatCode, traceForest, Error (..), Trace, TraceData(..), Query(..), FrameContext(..))+import EVM.ABI (AbiValue (..), Event (..), AbiType (..), SolError (..),+  Indexed (NotIndexed), getAbiSeq, parseTypeName, formatString) import EVM.Dapp (DappContext(..), DappInfo(..), showTraceLocation) import EVM.Expr qualified as Expr import EVM.Hexdump (prettyHex)-import EVM.Solidity (SolcContract(..), Method(..))-import EVM.Types (maybeLitWord, W256(..), num, word, Expr(..), EType(..), Addr,+import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap)+import EVM.Types (maybeLitWord, W256(..),num, word, Expr(..), EType(..), Addr,   ByteStringS(..), Error(..))+ import Control.Arrow ((>>>)) import Control.Lens (preview, ix, _2) import Data.Binary.Get (runGetOrFail)@@ -366,14 +366,14 @@  prettyError :: EVM.Types.Error -> String prettyError= \case-  Invalid -> "Invalid Opcode"+  EVM.Types.Invalid -> "Invalid Opcode"   EVM.Types.IllegalOverflow -> "Illegal Overflow"-  SelfDestruct -> "Self Destruct"+  EVM.Types.SelfDestruct -> "Self Destruct"   EVM.Types.StackLimitExceeded -> "Stack limit exceeded"   EVM.Types.InvalidMemoryAccess -> "Invalid memory access"   EVM.Types.BadJumpDestination -> "Bad jump destination"   EVM.Types.StackUnderrun -> "Stack underrun"-  TmpErr err -> "Temp error: " <> err+  EVM.Types.TmpErr err -> "Temp error: " <> err   prettyvmresult :: (?context :: DappContext) => Expr End -> String

@@ -28,7 +28,7 @@ -- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -- -module EVM.Hexdump (prettyHex, simpleHex) where+module EVM.Hexdump (prettyHex, simpleHex, paddedShowHex) where  import Data.ByteString                       (ByteString) import qualified Data.ByteString       as B  (length, unpack)

@@ -1,16 +1,24 @@ {-# LANGUAGE DataKinds #-}  module EVM.Op-  ( Op (..)+  ( Op+  , GenericOp (..)   , opString+  , intToOpName+  , getOp+  , readOp   ) where +import EVM.Expr qualified as Expr import EVM.Types +import Data.Vector qualified as V import Data.Word (Word8) import Numeric (showHex) -data Op+type Op = GenericOp (Expr EWord)++data GenericOp a   = OpStop   | OpAdd   | OpMul@@ -87,10 +95,165 @@   | OpDup !Word8   | OpSwap !Word8   | OpLog !Word8-  | OpPush (Expr EWord)+  | OpPush a   | OpUnknown Word8-  deriving (Show, Eq)+  deriving (Show, Eq, Functor) +intToOpName:: Int -> String+intToOpName a =+  case a of+   0x00-> "STOP"+   0x01-> "ADD"+   0x02-> "MUL"+   0x03-> "SUB"+   0x04-> "DIV"+   0x05-> "SDIV"+   0x06-> "MOD"+   0x07-> "SMOD"+   0x08-> "ADDMOD"+   0x09-> "MULMOD"+   0x0a-> "EXP"+   0x0b-> "SIGNEXTEND"+   --+   0x10 -> "LT"+   0x11 -> "GT"+   0x12 -> "SLT"+   0x13 -> "SGT"+   0x14 -> "EQ"+   0x15 -> "ISZERO"+   0x16 -> "AND"+   0x17 -> "OR"+   0x18 -> "XOR"+   0x19 -> "NOT"+   0x1a -> "BYTE"+   0x1b -> "SHL"+   0x1c -> "SHR"+   0x1d -> "SAR"+   0x20 -> "SHA3"+   0x30 -> "ADDRESS"+   --+   0x31 -> "BALANCE"+   0x32 -> "ORIGIN"+   0x33 -> "CALLER"+   0x34 -> "CALLVALUE"+   0x35 -> "CALLDATALOAD"+   0x36 -> "CALLDATASIZE"+   0x37 -> "CALLDATACOPY"+   0x38 -> "CODESIZE"+   0x39 -> "CODECOPY"+   0x3a -> "GASPRICE"+   0x3b -> "EXTCODESIZE"+   0x3c -> "EXTCODECOPY"+   0x3d -> "RETURNDATASIZE"+   0x3e -> "RETURNDATACOPY"+   0x3f -> "EXTCODEHASH"+   0x40 -> "BLOCKHASH"+   0x41 -> "COINBASE"+   0x42 -> "TIMESTAMP"+   0x43 -> "NUMBER"+   0x44 -> "PREVRANDAO"+   0x45 -> "GASLIMIT"+   0x46 -> "CHAINID"+   0x47 -> "SELFBALANCE"+   0x48 -> "BASEFEE"+   0x50 -> "POP"+   0x51 -> "MLOAD"+   0x52 -> "MSTORE"+   0x53 -> "MSTORE8"+   0x54 -> "SLOAD"+   0x55 -> "SSTORE"+   0x56 -> "JUMP"+   0x57 -> "JUMPI"+   0x58 -> "PC"+   0x59 -> "MSIZE"+   0x5a -> "GAS"+   0x5b -> "JUMPDEST"+   --+   0x60 -> "PUSH1"+   0x61 -> "PUSH2"+   0x62 -> "PUSH3"+   0x63 -> "PUSH4"+   0x64 -> "PUSH5"+   0x65 -> "PUSH6"+   0x66 -> "PUSH7"+   0x67 -> "PUSH8"+   0x68 -> "PUSH9"+   0x69 -> "PUSH10"+   0x6a -> "PUSH11"+   0x6b -> "PUSH12"+   0x6c -> "PUSH13"+   0x6d -> "PUSH14"+   0x6e -> "PUSH15"+   0x6f -> "PUSH16"+   0x70 -> "PUSH17"+   0x71 -> "PUSH18"+   0x72 -> "PUSH19"+   0x73 -> "PUSH20"+   0x74 -> "PUSH21"+   0x75 -> "PUSH22"+   0x76 -> "PUSH23"+   0x77 -> "PUSH24"+   0x78 -> "PUSH25"+   0x79 -> "PUSH26"+   0x7a -> "PUSH27"+   0x7b -> "PUSH28"+   0x7c -> "PUSH29"+   0x7d -> "PUSH30"+   0x7e -> "PUSH31"+   0x7f -> "PUSH32"+   --+   0x80 -> "DUP1"+   0x81 -> "DUP2"+   0x82 -> "DUP3"+   0x83 -> "DUP4"+   0x84 -> "DUP5"+   0x85 -> "DUP6"+   0x86 -> "DUP7"+   0x87 -> "DUP8"+   0x88 -> "DUP9"+   0x89 -> "DUP10"+   0x8a -> "DUP11"+   0x8b -> "DUP12"+   0x8c -> "DUP13"+   0x8d -> "DUP14"+   0x8e -> "DUP15"+   0x8f -> "DUP16"+   --+   0x90 -> "SWAP1"+   0x91 -> "SWAP2"+   0x92 -> "SWAP3"+   0x93 -> "SWAP4"+   0x94 -> "SWAP5"+   0x95 -> "SWAP6"+   0x96 -> "SWAP7"+   0x97 -> "SWAP8"+   0x98 -> "SWAP9"+   0x99 -> "SWAP10"+   0x9a -> "SWAP11"+   0x9b -> "SWAP12"+   0x9c -> "SWAP13"+   0x9d -> "SWAP14"+   0x9e -> "SWAP15"+   0x9f -> "SWAP16"+   --+   0xa0 -> "LOG0"+   0xa1 -> "LOG1"+   0xa2 -> "LOG2"+   0xa3 -> "LOG3"+   0xa4 -> "LOG4"+   --+   0xf0 -> "CREATE"+   0xf1 -> "CALL"+   0xf2 -> "CALLCODE"+   0xf3 -> "RETURN"+   0xf4 -> "DELEGATECALL"+   0xf5 -> "CREATE2"+   0xfa -> "STATICCALL"+   0xfd -> "REVERT"+   0xfe -> "INVALID"+   0xff -> "SELFDESTRUCT"+   _ -> "UNKNOWN "+ opString :: (Integral a, Show a) => (a, Op) -> String opString (i, o) = let showPc x | x < 0x10 = '0' : showHex x ""                                | otherwise = showHex x ""@@ -177,3 +340,88 @@   OpUnknown x -> case x of     254 -> "INVALID"     _ -> "UNKNOWN " ++ (showHex x "")++readOp :: Word8 -> [Expr Byte] -> Op+readOp x xs =+  (\n -> Expr.readBytes (fromIntegral n) (Lit 0) (Expr.fromList $ V.fromList xs)) <$> getOp x++getOp :: Word8 -> GenericOp Word8+getOp x | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)+getOp x | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1)+getOp x | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0)+getOp x | x >= 0x60 && x <= 0x7f = OpPush (x - 0x60 + 1)+getOp x = case x of+  0x00 -> OpStop+  0x01 -> OpAdd+  0x02 -> OpMul+  0x03 -> OpSub+  0x04 -> OpDiv+  0x05 -> OpSdiv+  0x06 -> OpMod+  0x07 -> OpSmod+  0x08 -> OpAddmod+  0x09 -> OpMulmod+  0x0a -> OpExp+  0x0b -> OpSignextend+  0x10 -> OpLt+  0x11 -> OpGt+  0x12 -> OpSlt+  0x13 -> OpSgt+  0x14 -> OpEq+  0x15 -> OpIszero+  0x16 -> OpAnd+  0x17 -> OpOr+  0x18 -> OpXor+  0x19 -> OpNot+  0x1a -> OpByte+  0x1b -> OpShl+  0x1c -> OpShr+  0x1d -> OpSar+  0x20 -> OpSha3+  0x30 -> OpAddress+  0x31 -> OpBalance+  0x32 -> OpOrigin+  0x33 -> OpCaller+  0x34 -> OpCallvalue+  0x35 -> OpCalldataload+  0x36 -> OpCalldatasize+  0x37 -> OpCalldatacopy+  0x38 -> OpCodesize+  0x39 -> OpCodecopy+  0x3a -> OpGasprice+  0x3b -> OpExtcodesize+  0x3c -> OpExtcodecopy+  0x3d -> OpReturndatasize+  0x3e -> OpReturndatacopy+  0x3f -> OpExtcodehash+  0x40 -> OpBlockhash+  0x41 -> OpCoinbase+  0x42 -> OpTimestamp+  0x43 -> OpNumber+  0x44 -> OpPrevRandao+  0x45 -> OpGaslimit+  0x46 -> OpChainid+  0x47 -> OpSelfbalance+  0x48 -> OpBaseFee+  0x50 -> OpPop+  0x51 -> OpMload+  0x52 -> OpMstore+  0x53 -> OpMstore8+  0x54 -> OpSload+  0x55 -> OpSstore+  0x56 -> OpJump+  0x57 -> OpJumpi+  0x58 -> OpPc+  0x59 -> OpMsize+  0x5a -> OpGas+  0x5b -> OpJumpdest+  0xf0 -> OpCreate+  0xf1 -> OpCall+  0xf2 -> OpCallcode+  0xf3 -> OpReturn+  0xf4 -> OpDelegatecall+  0xf5 -> OpCreate2+  0xfd -> OpRevert+  0xfa -> OpStaticcall+  0xff -> OpSelfdestruct+  _    -> OpUnknown x

@@ -34,20 +34,22 @@ import qualified Data.Text.Lazy as T import Data.Text.Lazy.Builder import Data.Bifunctor (second)-import Data.Semigroup (Any, Any(..), getAny)  import EVM.Types import EVM.Traversals import EVM.CSE import EVM.Keccak-import EVM.Expr hiding (copySlice, writeWord, op1, op2, op3, drop)+import EVM.Expr (writeByte, bufLengthEnv, containsNode, bufLength, minLength)+import qualified EVM.Expr as Expr   -- ** Encoding ** ----------------------------------------------------------------------------------++ -- variable names in SMT that we want to get values for data CexVars = CexVars   { calldataV :: [Text]-  , buffersV :: [Text]+  , buffersV :: Map Text (Expr EWord) -- buffers and guesses at their maximum size   , storeReads :: [(Expr EWord, Expr EWord)] -- a list of relevant store reads   , blockContextV :: [Text]   , txContextV :: [Text]@@ -66,16 +68,49 @@       , txContextV = mempty       } +-- | A model for a buffer, either in it's compressed form (for storing parsed+-- models from a solver), or as a bytestring (for presentation to users)+data BufModel+  = Comp CompressedBuf+  | Flat ByteString+  deriving (Eq, Show)++-- | This representation lets us store buffers of arbitrary length without+-- exhausting the available memory, it closely matches the format used by+-- smt-lib when returning models for arrays+data CompressedBuf+  = Base { byte :: Word8, length :: W256}+  | Write { byte :: Word8, idx :: W256, next :: CompressedBuf }+  deriving (Eq, Show)+++-- | a final post shrinking cex, buffers here are all represented as concrete bytestrings data SMTCex = SMTCex   { vars :: Map (Expr EWord) W256-  , buffers :: Map (Expr Buf) ByteString+  , buffers :: Map (Expr Buf) BufModel   , store :: Map W256 (Map W256 W256)   , blockContext :: Map (Expr EWord) W256   , txContext :: Map (Expr EWord) W256   }   deriving (Eq, Show) -getVar :: EVM.SMT.SMTCex -> TS.Text -> W256+flattenBufs :: SMTCex -> Maybe SMTCex+flattenBufs cex = do+  bs <- mapM collapse cex.buffers+  pure $ cex { buffers = bs}++-- | Attemps to collapse a compressed buffer representation down to a flattened one+collapse :: BufModel -> Maybe BufModel+collapse model = case toBuf model of+  Just (ConcreteBuf b) -> Just $ Flat b+  _ -> Nothing+  where+    toBuf (Comp (Base b sz)) | sz <= 120_000_000 = Just . ConcreteBuf $ BS.replicate (num sz) b+    toBuf (Comp (Write b idx next)) = fmap (writeByte (Lit idx) (LitByte b)) (toBuf $ Comp next)+    toBuf (Flat b) = Just . ConcreteBuf $ b+    toBuf _ = Nothing++getVar :: SMTCex -> TS.Text -> W256 getVar cex name = fromJust $ Map.lookup (Var name) cex.vars  data SMT2 = SMT2 [Builder] CexVars@@ -101,16 +136,18 @@   where     compareFst (l, _) (r, _) = compare l r     encodeBuf n expr =-       fromLazyText ("(define-const buf" <> (T.pack . show $ n) <> " Buf ") <> exprToSMT expr <> ")"+      "(define-const buf" <> (fromString . show $ n) <> " Buf " <> exprToSMT expr <> ")\n" <> encodeBufLen n expr+    encodeBufLen n expr =+      "(define-const buf" <> (fromString . show $ n) <>"_length" <> " (_ BitVec 256) " <> exprToSMT (bufLengthEnv bufs True expr) <> ")"     encodeStore n expr =-       fromLazyText ("(define-const store" <> (T.pack . show $ n) <> " Storage ") <> exprToSMT expr <> ")"+       "(define-const store" <> (fromString . show $ n) <> " Storage " <> exprToSMT expr <> ")"  assertProps :: [Prop] -> SMT2 assertProps ps =   let encs = map propToSMT ps_elim       intermediates = declareIntermediates bufs stores in   prelude-  <> (declareBufs . nubOrd $ foldl (<>) [] allBufs)+  <> (declareBufs ps_elim bufs stores)   <> SMT2 [""] mempty   <> (declareVars . nubOrd $ foldl (<>) [] allVars)   <> SMT2 [""] mempty@@ -121,6 +158,7 @@   <> intermediates   <> SMT2 [""] mempty   <> keccakAssumes+  <> readAssumes   <> SMT2 [""] mempty   <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty   <> SMT2 [] mempty{storeReads = storageReads}@@ -128,7 +166,6 @@   where     (ps_elim, bufs, stores) = eliminateProps ps -    allBufs = fmap referencedBufs' ps_elim <> fmap referencedBufs bufVals <> fmap referencedBufs storeVals     allVars = fmap referencedVars' ps_elim <> fmap referencedVars bufVals <> fmap referencedVars storeVals     frameCtx = fmap referencedFrameContext' ps_elim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals     blockCtx = fmap referencedBlockContext' ps_elim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals@@ -142,6 +179,9 @@       = SMT2 ["; keccak assumptions"] mempty       <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (keccakAssumptions ps_elim bufVals storeVals)) mempty +    readAssumes+      = SMT2 ["; read assumptions"] mempty+        <> SMT2 (fmap (\p -> "(assert " <> propToSMT p <> ")") (assertReads ps_elim bufs stores)) mempty  referencedBufsGo :: Expr a -> [Builder] referencedBufsGo = \case@@ -154,7 +194,6 @@ referencedBufs' :: Prop -> [Builder] referencedBufs' prop = nubOrd $ foldProp referencedBufsGo [] prop - referencedVarsGo :: Expr a -> [Builder] referencedVarsGo = \case   Var s -> [fromText s]@@ -166,7 +205,6 @@ referencedVars' :: Prop -> [Builder] referencedVars' prop = nubOrd $ foldProp referencedVarsGo [] prop - referencedFrameContextGo :: Expr a -> [Builder] referencedFrameContextGo = \case   CallValue a -> [fromLazyText $ T.append "callvalue_" (T.pack . show $ a)]@@ -202,14 +240,6 @@ referencedBlockContext' :: Prop -> [Builder] referencedBlockContext' prop = nubOrd $ foldProp referencedBlockContextGo [] prop --isAbstractStorage :: Expr Storage -> Bool-isAbstractStorage = getAny . foldExpr go (Any False)-  where-    go :: Expr a -> Any-    go AbstractStore = Any True-    go _ = Any False- -- | This function overapproximates the reads from the abstract -- storage. Potentially, it can return locations that do not read a -- slot directly from the abstract store but from subsequent writes on@@ -221,19 +251,80 @@   where     go :: Expr a -> [(Expr EWord, Expr EWord)]     go = \case-      SLoad addr slot storage -> [(addr, slot) | isAbstractStorage storage]+      SLoad addr slot storage -> [(addr, slot) | containsNode isAbstractStore storage]       _ -> [] +    isAbstractStore AbstractStore = True+    isAbstractStore _ = False -declareBufs :: [Builder] -> SMT2-declareBufs names = SMT2 ("; buffers" : fmap declareBuf names <> ("; buffer lengths" : fmap declareLength names)) cexvars++findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]+findBufferAccess = foldl (foldTerm go) mempty   where-    declareBuf n = "(declare-const " <> n <> " (Array (_ BitVec 256) (_ BitVec 8)))"-    declareLength n = "(define-const " <> n <> "_length" <> " (_ BitVec 256) (bufLength " <> n <> "))"-    cexvars = mempty{buffersV = fmap toLazyText names}+    go :: Expr a -> [(Expr EWord, Expr EWord, Expr Buf)]+    go = \case+      ReadWord idx buf -> [(idx, Lit 32, buf)]+      ReadByte idx buf -> [(idx, Lit 1, buf)]+      CopySlice srcOff _ size src _  -> [(srcOff, size, src)]+      _ -> mempty +-- | Asserts that buffer reads beyond the size of the buffer are equal+-- to zero. Looks for buffer reads in the a list of given predicates+-- and the buffer and storage environments.+assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]+assertReads props benv senv = concatMap assertRead allReads+  where+    assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]+    assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))]+    assertRead (idx, Lit sz, buf) = fmap (\s -> PImpl (PGEq idx (bufLength buf)) (PEq (ReadByte idx buf) (LitByte (num s)))) [(0::Int)..num sz-1]+    assertRead (_, _, _) = error "Cannot generate assertions for accesses of symbolic size" --- Given a list of 256b VM variable names, create an SMT2 object with the variables declared+    allReads = filter keepRead $ nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv)++    -- discard constraints if we can statically determine that read is less than the buffer length+    keepRead (Lit idx, Lit size, buf) =+      case minLength benv buf of+        Just l | num (idx + size) <= l -> False+        _ -> True+    keepRead _ = True++-- | Finds the maximum read index for each abstract buffer in the input props+discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)+discoverMaxReads props benv senv = bufMap+  where+    allReads = nubOrd $ findBufferAccess props <> findBufferAccess (Map.elems benv) <> findBufferAccess (Map.elems senv)+    -- we can have buffers that are not read from but are still mentioned via BufLength in some branch condition+    -- we assign a default read hint of 4 to start with in these cases (since in most cases we will need at least 4 bytes to produce a counterexample)+    allBufs = Map.fromList . fmap (, Lit 4) . fmap toLazyText . nubOrd . concat $ fmap referencedBufs' props <> fmap referencedBufs (Map.elems benv) <> fmap referencedBufs (Map.elems senv)++    bufMap = Map.unionWith Expr.max (foldl addBound mempty allReads) allBufs++    addBound m (idx, size, buf) =+      case baseBuf buf of+        AbstractBuf b -> Map.insertWith Expr.max (T.fromStrict b) (Expr.add idx size) m+        _ -> m++    baseBuf :: Expr Buf -> Expr Buf+    baseBuf (AbstractBuf b) = AbstractBuf b+    baseBuf (ConcreteBuf b) = ConcreteBuf b+    baseBuf (GVar (BufVar a)) =+      case Map.lookup a benv of+        Just b -> baseBuf b+        Nothing -> error "Internal error: could not find buffer variable"+    baseBuf (WriteByte _ _ b) = baseBuf b+    baseBuf (WriteWord _ _ b) = baseBuf b+    baseBuf (CopySlice _ _ _ _ dst)= baseBuf dst++-- | Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached+declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2+declareBufs props bufEnv storeEnv = SMT2 ("; buffers" : fmap declareBuf allBufs <> ("; buffer lengths" : fmap declareLength allBufs)) cexvars+  where+    cexvars = mempty{buffersV = discoverMaxReads props bufEnv storeEnv}+    allBufs = fmap fromLazyText $ Map.keys cexvars.buffersV+    declareBuf n = "(declare-const " <> n <> " (Array (_ BitVec 256) (_ BitVec 8)))"+    declareLength n = "(declare-const " <> n <> "_length" <> " (_ BitVec 256))"++-- Given a list of variable names, create an SMT2 object with the variables declared declareVars :: [Builder] -> SMT2 declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars   where@@ -274,6 +365,8 @@   (declare-fun keccak (Buf) Word)   (declare-fun sha256 (Buf) Word) +  (define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))+   ; word indexing   (define-fun indexWord31 ((w Word)) Byte ((_ extract 7 0) w))   (define-fun indexWord30 ((w Word)) Byte ((_ extract 15 8) w))@@ -348,7 +441,6 @@   )    ; buffers-  (declare-fun bufLength (Buf) Word)   (define-const emptyBuf Buf ((as const Buf) #b00000000))    (define-fun readWord ((idx Word) (buf Buf)) Word@@ -499,12 +591,19 @@     let aenc = exprToSMT a         benc = exprToSMT b in     "(ite (bvule " <> aenc `sp` benc <> ") " <> aenc `sp` benc <> ")"+  Max a b ->+    let aenc = exprToSMT a+        benc = exprToSMT b in+    "(max " <> aenc `sp` benc <> ")"   LT a b ->     let cond = op2 "bvult" a b in     "(ite " <> cond `sp` one `sp` zero <> ")"   SLT a b ->     let cond = op2 "bvslt" a b in     "(ite " <> cond `sp` one `sp` zero <> ")"+  SGT a b ->+    let cond = op2 "bvsgt" a b in+    "(ite " <> cond `sp` one `sp` zero <> ")"   GT a b ->     let cond = op2 "bvugt" a b in     "(ite " <> cond `sp` one `sp` zero <> ")"@@ -575,7 +674,6 @@   ChainId -> "chainid"   BaseFee -> "basefee" -  -- TODO: make me binary...   LitByte b -> fromLazyText $ "(_ bv" <> T.pack (show (num b :: Integer)) <> " 8)"   IndexWord idx w -> case idx of     Lit n -> if n >= 0 && n < 32@@ -590,7 +688,9 @@   ConcreteBuf bs -> writeBytes bs mempty   AbstractBuf s -> fromText s   ReadWord idx prev -> op2 "readWord" idx prev-  BufLength b -> op1 "bufLength" b+  BufLength (AbstractBuf b) -> fromText b <> "_length"+  BufLength (GVar (BufVar n)) -> fromLazyText $ "buf" <> (T.pack . show $ n) <> "_length"+  BufLength b -> exprToSMT (bufLength b)   WriteByte idx val prev ->     let encIdx = exprToSMT idx         encVal = exprToSMT val@@ -660,6 +760,10 @@     let aenc = propToSMT a         benc = propToSMT b in     "(or " <> aenc <> " " <> benc <> ")"+  PImpl a b ->+    let aenc = propToSMT a+        benc = propToSMT b in+    "(=> " <> aenc <> " " <> benc <> ")"   PBool b -> if b then "true" else "false"   where     op2 op a b =@@ -677,9 +781,9 @@ copySlice srcOffset dstOffset size@(Lit _) src dst   | size == (Lit 0) = dst   | otherwise =-    let size' = (sub size (Lit 1))-        encDstOff = exprToSMT (add dstOffset size')-        encSrcOff = exprToSMT (add srcOffset size')+    let size' = (Expr.sub size (Lit 1))+        encDstOff = exprToSMT (Expr.add dstOffset size')+        encSrcOff = exprToSMT (Expr.add srcOffset size')         child = copySlice srcOffset dstOffset size' src dst in     "(store " <> child `sp` encDstOff `sp` "(select " <> src `sp` encSrcOff <> "))" copySlice _ _ _ _ _ = error "TODO: implement copySlice with a symbolically sized region"@@ -733,6 +837,7 @@  -- ** Cex parsing ** -------------------------------------------------------------------------------- + parseW256 :: SpecConstant -> W256 parseW256 = parseSC @@ -791,52 +896,44 @@           r -> parseErr r       pure $ Map.insert name val acc -getBufs :: (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr Buf) ByteString)-getBufs getVal names = foldM getBuf mempty names+-- | Queries the solver for models for each of the expressions representing the+-- max read index for a given buffer+queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord)  -> IO (Map Text W256)+queryMaxReads getVal maxReads = mapM (queryValue getVal) maxReads++-- | Gets the initial model for each buffer, these will often be much too large for our purposes+getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel)+getBufs getVal bufs = foldM getBuf mempty bufs   where-    getLength :: TS.Text -> IO Int+    getLength :: Text -> IO W256     getLength name = do-      val <- getVal (T.fromStrict name <> "_length")-      len <- case parseCommentFreeFileMsg getValueRes (T.toStrict val) of+      val <- getVal (name <> "_length ")+      pure $ case parseCommentFreeFileMsg getValueRes (T.toStrict val) of         Right (ResSpecific (parsed :| [])) -> case parsed of           (TermQualIdentifier (Unqualified (IdSymbol symbol)), (TermSpecConstant sc))-            -> if symbol == (name <> "_length")-               then pure $ parseW256 sc+            -> if symbol == (T.toStrict $ name <> "_length")+               then parseW256 sc                else error "Internal Error: solver did not return model for requested value"           res -> parseErr res         res -> parseErr res-      pure $ if len <= num (maxBound :: Int)-             then fromIntegral len-             else error $ "Internal Error: buffer: "-                       <> (TS.unpack name)-                       <> " is too large to be represented in a ByteString. Length: "-                       <> show len -    getBuf :: Map (Expr Buf) ByteString -> TS.Text -> IO (Map (Expr Buf) ByteString)+    getBuf :: Map (Expr Buf) BufModel -> Text -> IO (Map (Expr Buf) BufModel)     getBuf acc name = do-      -- Sometimes the solver gives us back a model for a Buffer that has every-      -- element set to some concrete value. This is impossible to represent as-      -- a concrete ByteString in haskell (or in any existing computer hardware :D),-      -- so we ask the solver to give us back a model for the length of-      -- this buffer and then use that to produce a shorter counterexample (by-      -- replicating the constant byte up to the length).       len <- getLength name-      val <- getVal (T.fromStrict name)+      val <- getVal name+       buf <- case parseCommentFreeFileMsg getValueRes (T.toStrict val) of         Right (ResSpecific (valParsed :| [])) -> case valParsed of           (TermQualIdentifier (Unqualified (IdSymbol symbol)), term)-            -> if symbol == name+            -> if (T.fromStrict symbol) == name                then pure $ parseBuf len term                else error "Internal Error: solver did not return model for requested value"           res -> error $ "Internal Error: cannot parse solver response: " <> show res         res -> error $ "Internal Error: cannot parse solver response: " <> show res-      let bs = case simplify buf of-                 ConcreteBuf b -> b-                 _ -> error "Internal Error: unable to parse solver response into a concrete buffer"-      pure $ Map.insert (AbstractBuf name) bs acc+      pure $ Map.insert (AbstractBuf $ T.toStrict name) buf acc -    parseBuf :: Int -> Term -> Expr Buf-    parseBuf len = go mempty+    parseBuf :: W256 -> Term -> BufModel+    parseBuf len = Comp . go mempty       where         go env = \case           -- constant arrays@@ -848,8 +945,8 @@               )             )) ((TermSpecConstant val :| [])))             -> case val of-                 SCHexadecimal "00" -> mempty-                 v -> ConcreteBuf $ BS.replicate len (parseW8 v)+                 SCHexadecimal "00" -> Base 0 0+                 v -> Base (parseW8 v) len            -- writing a byte over some array           (TermApplication@@ -859,7 +956,7 @@               pbase = go env base               pidx = parseW256 idx               pval = parseW8 val-            in writeByte (Lit pidx) (LitByte pval) pbase+            in Write pval pidx pbase            -- binding a new name           (TermLet ((VarBinding name bound) :| []) term) -> let@@ -890,8 +987,8 @@    -- then create a map by adding only the locations that are read by the program   foldM (\m (addr, slot) -> do-            addr' <- queryValue addr-            slot' <- queryValue slot+            addr' <- queryValue getVal addr+            slot' <- queryValue getVal slot             pure $ addElem addr' slot' m fun) Map.empty sreads    where@@ -903,17 +1000,17 @@         Nothing -> Map.insert addr (Map.singleton slot (fun addr slot)) store  -    queryValue :: Expr EWord -> IO W256-    queryValue (Lit w) = pure w-    queryValue w = do-      let expr = toLazyText $ exprToSMT w-      raw <- getVal expr-      case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of-        Right (ResSpecific (valParsed :| [])) ->-          case valParsed of-            (_, TermSpecConstant sc) -> pure $ parseW256 sc-            _ -> error "Internal Error: cannot parse model for storage index"-        r -> parseErr r+queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256+queryValue _ (Lit w) = pure w+queryValue getVal w = do+  let expr = toLazyText $ exprToSMT w+  raw <- getVal expr+  case parseCommentFreeFileMsg getValueRes (T.toStrict raw) of+    Right (ResSpecific (valParsed :| [])) ->+      case valParsed of+        (_, TermSpecConstant sc) -> pure $ parseW256 sc+        _ -> error $ "Internal Error: cannot parse model for: " <> show w+    r -> parseErr r   

@@ -0,0 +1,77 @@+{-|+Module      : Helper functions to sign a transaction and derive address from+Description :        for the EVM given a secret key+-}++module EVM.Sign where++import qualified Crypto.Hash as Crypto+import Data.Maybe (fromMaybe)+import Crypto.PubKey.ECC.ECDSA (signDigestWith, PrivateKey(..), Signature(..))+import Crypto.PubKey.ECC.Types (getCurveByName, CurveName(..), Point(..))+import Crypto.PubKey.ECC.Generate (generateQ)++import EVM.ABI (encodeAbiValue, AbiValue (..))+import qualified Data.ByteString   as BS+import EVM.Types+import EVM.Expr (exprToAddr)+import EVM.Precompiled+import Data.Word+++-- Given a secret key, generates the address+deriveAddr :: Integer -> Maybe Addr+deriveAddr sk = case pubPoint of+           PointO -> Nothing+           Point x y ->+             -- See yellow paper #286+               let pub = BS.concat [ encodeInt x, encodeInt y ]+                   addr = Lit . W256 . word256 . BS.drop 12 . BS.take 32 . keccakBytes $ pub+                in exprToAddr addr+         where+          curve = getCurveByName SEC_p256k1+          pubPoint = generateQ curve (num sk)+          encodeInt = encodeAbiValue . AbiUInt 256 . fromInteger++sign :: W256 -> Integer -> (Word8, W256, W256)+sign hash sk = (v, r, s)+  where+    -- setup curve params+    curve = getCurveByName SEC_p256k1+    priv = PrivateKey curve sk+    digest = fromMaybe+      (error $ "Internal Error: could produce a digest from " <> show hash)+      (Crypto.digestFromByteString (word256Bytes hash))++    -- sign message+    sig = ethsign priv digest+    r = num $ sign_r sig+    s = num lowS++    -- this is a little bit sad, but cryptonite doesn't give us back a v value+    -- so we compute it by guessing one, and then seeing if that gives us the right answer from ecrecover+    v = if ecrec 28 r s hash == deriveAddr sk+        then 28+        else 27++    -- we always use the lower S value to conform with EIP2 (re: ECDSA transaction malleability)+    -- https://eips.ethereum.org/EIPS/eip-2+    secpOrder = 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141 :: Integer+    lowS = if sign_s sig > secpOrder `div` 2+           then secpOrder - sign_s sig+           else sign_s sig++-- | We don't want to introduce the machinery needed to sign with a random nonce,+-- so we just use the same nonce every time (420). This is obviously very+-- insecure, but fine for testing purposes.+ethsign :: PrivateKey -> Crypto.Digest Crypto.Keccak_256 -> Signature+ethsign sk digest = go 420+  where+    go k = case signDigestWith k sk digest of+       Nothing  -> go (k + 1)+       Just sig -> sig++ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr+ecrec v r s e = num . word <$> EVM.Precompiled.execute 1 input 32+  where input = BS.concat (word256Bytes <$> [e, v, r, s])+

@@ -1,6 +1,5 @@ {-# Language DeriveAnyClass #-} {-# Language DataKinds #-}-{-# Language StrictData #-} {-# Language QuasiQuotes #-}  module EVM.Solidity@@ -178,11 +177,11 @@   deriving (Show, Eq, Ord, Generic)  data SrcMap = SM {-  srcMapOffset :: {-# UNPACK #-} Int,-  srcMapLength :: {-# UNPACK #-} Int,-  srcMapFile   :: {-# UNPACK #-} Int,+  srcMapOffset :: {-# UNPACK #-} !Int,+  srcMapLength :: {-# UNPACK #-} !Int,+  srcMapFile   :: {-# UNPACK #-} !Int,   srcMapJump   :: JumpType,-  srcMapModifierDepth :: {-# UNPACK #-} Int+  srcMapModifierDepth :: {-# UNPACK #-} !Int } deriving (Show, Eq, Ord, Generic)  data SrcMapParseState@@ -518,11 +517,11 @@ containsLinkerHole = regexMatches "__\\$[a-z0-9]{34}\\$__"  toCode :: Text -> ByteString-toCode t = case BS16.decode (encodeUtf8 t) of+toCode t = case BS16.decodeBase16 (encodeUtf8 t) of   Right d -> d   Left e -> if containsLinkerHole t             then error "unlinked libraries detected in bytecode"-            else error e+            else error $ Text.unpack e  solidity' :: Text -> IO (Text, Text) solidity' src = withSystemTempFile "hevm.sol" $ \path handle -> do

@@ -2,8 +2,6 @@ {-# Language GADTs #-} {-# Language PolyKinds #-} {-# Language ScopedTypeVariables #-}-{-# Language TypeApplications #-}-{-# Language QuasiQuotes #-}  {- |     Module: EVM.Solvers@@ -18,10 +16,13 @@ import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..)) import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan) import Control.Concurrent (forkIO, killThread)+import Control.Monad.State.Strict import Data.Char (isSpace)  import Data.Maybe (fromMaybe) import Data.Text.Lazy (Text)+import Data.Map (Map)+import qualified Data.Map as Map import qualified Data.Text as TS import qualified Data.Text.Lazy as T import qualified Data.Text.Lazy.IO as T@@ -29,6 +30,7 @@ import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..))  import EVM.SMT+import EVM.Types  -- | Supported solvers data Solver@@ -128,19 +130,7 @@         Right () -> do           sat <- sendLine inst "(check-sat)"           res <- case sat of-            "sat" -> do-              calldatamodels <- getVars parseVar (getValue inst) (fmap T.toStrict cexvars.calldataV)-              buffermodels <- getBufs (getValue inst) (fmap T.toStrict cexvars.buffersV)-              storagemodels <- getStore (getValue inst) cexvars.storeReads-              blockctxmodels <- getVars parseBlockCtx (getValue inst) (fmap T.toStrict cexvars.blockContextV)-              txctxmodels <- getVars parseFrameCtx (getValue inst) (fmap T.toStrict cexvars.txContextV)-              pure $ Sat $ SMTCex-                { vars = calldatamodels-                , buffers = buffermodels-                , store = storagemodels-                , blockContext = blockctxmodels-                , txContext = txctxmodels-                }+            "sat" -> Sat <$> getModel inst cexvars             "unsat" -> pure Unsat             "timeout" -> pure Unknown             "unknown" -> pure Unknown@@ -149,6 +139,85 @@        -- put the instance back in the list of available instances       writeChan availableInstances inst++getModel :: SolverInstance -> CexVars -> IO SMTCex+getModel inst cexvars = do+  -- get an initial version of the model from the solver+  initialModel <- getRaw+  -- get concrete values for each buffers max read index+  hints <- capHints <$> queryMaxReads (getValue inst) cexvars.buffersV+  -- check the sizes of buffer models and shrink if needed+  if bufsUsable initialModel+  then do+    pure (mkConcrete initialModel)+  else mkConcrete . snd <$> runStateT (shrinkModel hints) initialModel+  where+    getRaw :: IO SMTCex+    getRaw = do+      vars <- getVars parseVar (getValue inst) (fmap T.toStrict cexvars.calldataV)+      buffers <- getBufs (getValue inst) (Map.keys cexvars.buffersV)+      storage <- getStore (getValue inst) cexvars.storeReads+      blockctx <- getVars parseBlockCtx (getValue inst) (fmap T.toStrict cexvars.blockContextV)+      txctx <- getVars parseFrameCtx (getValue inst) (fmap T.toStrict cexvars.txContextV)+      pure $ SMTCex vars buffers storage blockctx txctx++    -- sometimes the solver might give us back a model for the max read index+    -- that is too high to be a useful cex (e.g. in the case of reads from a+    -- symbolic index), so we cap the max value of the starting point to be 1024+    capHints :: Map Text W256 -> Map Text W256+    capHints = fmap (min 1024)++    -- shrink all the buffers in a model+    shrinkModel :: Map Text W256 -> StateT SMTCex IO ()+    shrinkModel hints = do+      m <- get+      -- iterate over all the buffers in the model, and shrink each one in turn if needed+      forM_ (Map.keys m.buffers) $ \case+        AbstractBuf b -> do+          let name = T.fromStrict b+              hint = fromMaybe+                       (error $ "Internal Error: Could not find hint for buffer: " <> T.unpack name)+                       (Map.lookup name hints)+          shrinkBuf name hint+        _ -> error "Internal Error: Received model from solver for non AbstractBuf"++    -- starting with some guess at the max useful size for a buffer, cap+    -- it's size to that value, and ask the solver to check satisfiability. If+    -- it's still sat with the new constraint, leave that constraint on the+    -- stack and return a new model, if it's unsat, double the size of the hint+    -- and try again.+    shrinkBuf :: Text -> W256 -> StateT SMTCex IO ()+    shrinkBuf buf hint = do+      let encBound = "(_ bv" <> (T.pack $ show (num hint :: Integer)) <> " 256)"+      sat <- liftIO $ do+        sendLine' inst "(push)"+        sendLine' inst $ "(assert (bvule " <> buf <> "_length " <> encBound <> "))"+        sendLine inst "(check-sat)"+      case sat of+        "sat" -> do+          model <- liftIO getRaw+          put model+        "unsat" -> do+          liftIO $ sendLine' inst "(pop)"+          shrinkBuf buf (if hint == 0 then hint + 1 else hint * 2)+        _ -> error "TODO: HANDLE ERRORS"++    -- Collapses the abstract description of a models buffers down to a bytestring+    mkConcrete :: SMTCex -> SMTCex+    mkConcrete c = fromMaybe+      (error $ "Internal Error: counterexample contains buffers that are too large to be represented as a ByteString: " <> show c)+      (flattenBufs c)++    -- we set a pretty arbitrary upper limit (of 1024) to decide if we need to do some shrinking+    bufsUsable :: SMTCex -> Bool+    bufsUsable model = any (go . snd) (Map.toList model.buffers)+      where+        go (Flat _) = True+        go (Comp c) = case c of+          (Base _ sz) -> sz <= 1024+          -- TODO: do I need to check the write idx here?+          (Write _ idx next) -> idx <= 1024 && go (Comp next)+  -- | Arguments used when spawing a solver instance solverArgs :: Solver -> Maybe (Natural) -> [Text]

@@ -12,7 +12,8 @@ import EVM.Exec import qualified EVM.Fetch as Fetch import EVM.ABI-import EVM.SMT+import EVM.SMT (SMTCex(..), SMT2(..), assertProps, formatSMT2)+import qualified EVM.SMT as SMT import EVM.Solvers import EVM.Traversals import qualified EVM.Expr as Expr@@ -46,6 +47,9 @@ import GHC.Conc (getNumProcessors) import EVM.Format (indent, formatBinary) +-- | A method name, and the (ordered) types of it's arguments+data Sig = Sig Text [AbiType]+ data ProofResult a b c = Qed a | Cex b | Timeout c   deriving (Show, Eq) type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End)@@ -173,12 +177,9 @@                              s -> error $ "unsupported cd fragment: " <> show s  -abstractVM :: Maybe (Text, [AbiType]) -> [String] -> ByteString -> Maybe Precondition -> StorageModel -> VM-abstractVM typesignature concreteArgs contractCode maybepre storagemodel = finalVm+abstractVM :: (Expr Buf, [Prop]) -> ByteString -> Maybe Precondition -> StorageModel -> VM+abstractVM (cd, calldataProps) contractCode maybepre storagemodel = finalVm   where-    (calldata', calldataProps) = case typesignature of-                 Nothing -> (AbstractBuf "txdata", [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))])-                 Just (name, typs) -> symCalldata name typs concreteArgs (AbstractBuf "txdata")     store = case storagemodel of               SymbolicS -> AbstractStore               InitialS -> EmptyStore@@ -186,7 +187,7 @@     caller' = Caller 0     value' = CallValue 0     code' = RuntimeCode (ConcreteRuntimeCode contractCode)-    vm' = loadSymVM code' store caller' value' calldata' calldataProps+    vm' = loadSymVM code' store caller' value' cd calldataProps     precond = case maybepre of                 Nothing -> []                 Just p -> [p vm']@@ -299,7 +300,7 @@ type Postcondition = VM -> Expr End -> Prop  -checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult])+checkAssert :: SolverGroup -> [Word256] -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> IO (Expr End, [VerifyResult]) checkAssert solvers errs c signature' concreteArgs opts = verifyContract solvers c signature' concreteArgs opts SymbolicS Nothing (Just $ checkAssertions errs)  {- |Checks if an assertion violation has been encountered@@ -338,9 +339,21 @@ panicMsg :: Word256 -> ByteString panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err) -verifyContract :: SolverGroup -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])-verifyContract solvers theCode signature' concreteArgs opts storagemodel maybepre maybepost = do-  let preState = abstractVM signature' concreteArgs theCode maybepre storagemodel+-- | Builds a buffer representing calldata from the provided method description and concrete arguments+mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])+mkCalldata Nothing _ =+      ( AbstractBuf "txdata"+      -- assert that the length of the calldata is never more than 2^64+      -- this is way larger than would ever be allowed by the gas limit+      -- and avoids spurious counterexamples during abi decoding+      -- TODO: can we encode calldata as an array with a smaller length?+      , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))]+      )+mkCalldata (Just (Sig name types)) args = symCalldata name types args (AbstractBuf "txdata")++verifyContract :: SolverGroup -> ByteString -> Maybe Sig -> [String] -> VeriOpts -> StorageModel -> Maybe Precondition -> Maybe Postcondition -> IO (Expr End, [VerifyResult])+verifyContract solvers theCode signature concreteArgs opts storagemodel maybepre maybepost = do+  let preState = abstractVM (mkCalldata signature concreteArgs) theCode maybepre storagemodel   verify solvers opts preState maybepost  pruneDeadPaths :: [VM] -> [VM]@@ -518,8 +531,8 @@ -- We do this by asking the solver to find a common input for each pair of endstates that satisfies the path -- conditions for both sides and produces a differing output. If we can find such an input, then we have a clear -- equivalence break, and since we run this check for every pair of end states, the check is exhaustive.-equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> Maybe (Text, [AbiType]) -> IO [EquivResult]-equivalenceCheck solvers bytecodeA bytecodeB opts signature' = do+equivalenceCheck :: SolverGroup -> ByteString -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) -> IO [EquivResult]+equivalenceCheck solvers bytecodeA bytecodeB opts calldata' = do   case bytecodeA == bytecodeB of     True -> do       putStrLn "bytecodeA and bytecodeB are identical"@@ -563,7 +576,7 @@     getBranches bs = do       let         bytecode = if BS.null bs then BS.pack [0] else bs-        prestate = abstractVM signature' [] bytecode Nothing SymbolicS+        prestate = abstractVM calldata' bytecode Nothing SymbolicS       expr <- evalStateT (interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters runExpr) prestate       let simpl = if opts.simp then (Expr.simplify expr) else expr       pure $ flattenExpr simpl@@ -749,8 +762,11 @@  -- | Takes a buffer and a Cex and replaces all abstract values in the buf with concrete ones from the Cex subModel :: SMTCex -> Expr a -> Expr a-subModel c expr = subBufs c.buffers . subVars c.vars . subStore c.store . subVars c.blockContext . subVars c.txContext $ expr+subModel c expr = subBufs (fmap forceFlattened c.buffers) . subVars c.vars . subStore c.store . subVars c.blockContext . subVars c.txContext $ expr   where+    forceFlattened (SMT.Flat bs) = bs+    forceFlattened b@(SMT.Comp _) = forceFlattened $ fromMaybe (error $ "Internal Error: cannot flatten buffer: " <> show b) (SMT.collapse b)+     subVars model b = Map.foldlWithKey subVar b model     subVar :: Expr a -> Expr EWord -> W256 -> Expr a     subVar b var val = mapExpr go b

@@ -25,7 +25,7 @@ import EVM.Solvers (SolverGroup) import EVM.Op import EVM.Solidity hiding (storageLayout)-import EVM.Types hiding (padRight)+import EVM.Types hiding (padRight, Max) import EVM.UnitTest import EVM.Stepper (Stepper) import EVM.Stepper qualified as Stepper

@@ -5,34 +5,44 @@ import qualified EVM import EVM (balance, initialContract) import EVM.FeeSchedule-import EVM.Precompiled (execute) import EVM.RLP import EVM.Types import EVM.Expr (litAddr)- import Control.Lens+import EVM.Sign -import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString) import Data.Map (Map) import Data.Maybe (fromMaybe, isNothing, fromJust)+import GHC.Generics (Generic) +import Data.Aeson (FromJSON (..)) import qualified Data.Aeson        as JSON import qualified Data.Aeson.Types  as JSON import qualified Data.ByteString   as BS import qualified Data.Map          as Map import Data.Word (Word64)+import Numeric (showHex)  data AccessListEntry = AccessListEntry {   accessAddress :: Addr,   accessStorageKeys :: [W256]-} deriving Show+} deriving (Show, Generic) +instance JSON.ToJSON AccessListEntry+ data TxType = LegacyTransaction             | AccessListTransaction             | EIP1559Transaction-  deriving (Show, Eq)+  deriving (Show, Eq, Generic) +instance JSON.ToJSON TxType where+  toJSON t = case t of+               EIP1559Transaction    -> "0x2" -- EIP1559+               LegacyTransaction     -> "0x1" -- EIP2718+               AccessListTransaction -> "0x1" -- EIP2930++ data Transaction = Transaction {     txData     :: ByteString,     txGasLimit :: Word64,@@ -46,30 +56,68 @@     txType     :: TxType,     txAccessList :: [AccessListEntry],     txMaxPriorityFeeGas :: Maybe W256,-    txMaxFeePerGas :: Maybe W256-} deriving Show+    txMaxFeePerGas :: Maybe W256,+    txChainId  :: W256+} deriving (Show, Generic) +instance JSON.ToJSON Transaction where+  toJSON t = JSON.object [ ("input",             (JSON.toJSON (ByteStringS t.txData)))+                         , ("gas",               (JSON.toJSON $ "0x" ++ showHex (toInteger $ t.txGasLimit) ""))+                         , ("gasPrice",          (JSON.toJSON $ show $ fromJust $ t.txGasPrice))+                         , ("v",                 (JSON.toJSON $ show $ (t.txV)-27))+                         , ("r",                 (JSON.toJSON $ show $ t.txR))+                         , ("s",                 (JSON.toJSON $ show $ t.txS))+                         , ("to",                (JSON.toJSON $ t.txToAddr))+                         , ("nonce",             (JSON.toJSON $ show $ t.txNonce))+                         , ("value",             (JSON.toJSON $ show $ t.txValue))+                         , ("type",              (JSON.toJSON $ t.txType))+                         , ("accessList",        (JSON.toJSON $ t.txAccessList))+                         , ("maxPriorityFeePerGas", (JSON.toJSON $ show $ fromJust $ t.txMaxPriorityFeeGas))+                         , ("maxFeePerGas",      (JSON.toJSON $ show $ fromJust $ t.txMaxFeePerGas))+                         , ("chainId",           (JSON.toJSON $ show t.txChainId))+                         ]++emptyTransaction :: Transaction+emptyTransaction = Transaction { txData = mempty+                               , txGasLimit = 0+                               , txGasPrice = Nothing+                               , txNonce = 0+                               , txR = 0+                               , txS = 0+                               , txToAddr = Nothing+                               , txV = 0+                               , txValue = 0+                               , txType = EIP1559Transaction+                               , txAccessList = []+                               , txMaxPriorityFeeGas = Nothing+                               , txMaxFeePerGas = Nothing+                               , txChainId = 1+                               }+ -- | utility function for getting a more useful representation of accesslistentries -- duplicates only matter for gas computation txAccessMap :: Transaction -> Map Addr [W256] txAccessMap tx = ((Map.fromListWith (++)) . makeTups) tx.txAccessList   where makeTups = map (\ale -> (ale.accessAddress , ale.accessStorageKeys )) -ecrec :: W256 -> W256 -> W256 -> W256 -> Maybe Addr-ecrec v r s e = num . word <$> EVM.Precompiled.execute 1 input 32-  where input = BS.concat (word256Bytes <$> [e, v, r, s])--sender :: Int -> Transaction -> Maybe Addr-sender chainId tx = ecrec v' tx.txR  tx.txS hash-  where hash = keccak' (signingData chainId tx)+-- Given Transaction, it recovers the address that sent it+sender :: Transaction -> Maybe Addr+sender tx = ecrec v' tx.txR  tx.txS hash+  where hash = keccak' (signingData tx)         v    = tx.txV         v'   = if v == 27 || v == 28 then v                else 27 + v -signingData :: Int -> Transaction -> ByteString-signingData chainId tx =+sign :: Integer -> Transaction -> Transaction+sign sk tx = tx { txV = num v, txR = r, txS = s}+  where+    hash = keccak' $ signingData tx+    (v, r, s) = EVM.Sign.sign hash sk++signingData :: Transaction -> ByteString+signingData tx =   case tx.txType of-    LegacyTransaction -> if v == (chainId * 2 + 35) || v == (chainId * 2 + 36)+    LegacyTransaction -> if v == (tx.txChainId * 2 + 35) || v == (tx.txChainId * 2 + 36)       then eip155Data       else normalData     AccessListTransaction -> eip2930Data@@ -98,11 +146,11 @@                               to',                               rlpWord256 tx.txValue,                               BS tx.txData,-                              rlpWord256 (fromIntegral chainId),+                              rlpWord256 tx.txChainId,                               rlpWord256 0x0,                               rlpWord256 0x0]         eip1559Data = cons 0x02 $ rlpList [-          rlpWord256 (fromIntegral chainId),+          rlpWord256 tx.txChainId,           rlpWord256 tx.txNonce,           rlpWord256 maxPrio,           rlpWord256 maxFee,@@ -113,7 +161,7 @@           rlpAccessList]          eip2930Data = cons 0x01 $ rlpList [-          rlpWord256 (fromIntegral chainId),+          rlpWord256 tx.txChainId,           rlpWord256 tx.txNonce,           rlpWord256 gasPrice,           rlpWord256 (num tx.txGasLimit),@@ -165,15 +213,15 @@     value    <- wordField val "value"     txType   <- fmap (read :: String -> Int) <$> (val JSON..:? "type")     case txType of-      Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing+      Just 0x00 -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1       Just 0x01 -> do         accessListEntries <- (val JSON..: "accessList") >>= parseJSONList-        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing+        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value AccessListTransaction accessListEntries Nothing Nothing 1       Just 0x02 -> do         accessListEntries <- (val JSON..: "accessList") >>= parseJSONList-        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee+        return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value EIP1559Transaction accessListEntries maxPrio maxFee 1       Just _ -> fail "unrecognized custom transaction type"-      Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing+      Nothing -> return $ Transaction tdata gasLimit gasPrice nonce r s toAddr v value LegacyTransaction [] Nothing Nothing 1   parseJSON invalid =     JSON.typeMismatch "Transaction" invalid 

@@ -26,6 +26,7 @@       PNeg a -> go a       PAnd a b -> go a <> go b       POr a b -> go a <> go b+      PImpl a b -> go a <> go b  -- | Recursively folds a given function over a given expression -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle@@ -85,6 +86,7 @@       e@(Exp a b) -> f e <> (go a) <> (go b)       e@(SEx a b) -> f e <> (go a) <> (go b)       e@(Min a b) -> f e <> (go a) <> (go b)+      e@(Max a b) -> f e <> (go a) <> (go b)        -- booleans @@ -237,6 +239,7 @@   PNeg a -> PNeg (mapProp f a)   PAnd a b -> PAnd (mapProp f a) (mapProp f b)   POr a b -> POr (mapProp f a) (mapProp f b)+  PImpl a b -> PImpl (mapProp f a) (mapProp f b)  -- | Recursively applies a given function to every node in a given expr instance -- Recursion schemes do this & a lot more, but defining them over GADT's isn't worth the hassle@@ -379,6 +382,10 @@     a' <- mapExprM f a     b' <- mapExprM f b     f (Min a' b')+  Max a b -> do+    a' <- mapExprM f a+    b' <- mapExprM f b+    f (Max a' b')    -- booleans @@ -642,3 +649,22 @@     a' <- mapPropM f a     b' <- mapPropM f b     pure $ POr a' b'+  PImpl a b -> do+    a' <- mapPropM f a+    b' <- mapPropM f b+    pure $ PImpl a' b'+++-- | Generic operations over AST terms+class TraversableTerm a where+  mapTerm  :: (forall b. Expr b -> Expr b) -> a -> a+  foldTerm :: forall c. Monoid c => (forall b. Expr b -> c) -> c -> a -> c+++instance TraversableTerm (Expr a) where+  mapTerm = mapExpr+  foldTerm = foldExpr++instance TraversableTerm Prop where+  mapTerm = mapProp+  foldTerm = foldProp

@@ -11,40 +11,42 @@  import Prelude hiding  (Word, LT, GT) -import Data.Aeson+import Control.Arrow ((>>>)) import Crypto.Hash hiding (SHA256)-import Data.Map (Map)+import Data.Aeson+import Data.Aeson qualified as JSON+import Data.Aeson.Types qualified as JSON import Data.Bifunctor (first)+import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.))+import Data.ByteArray qualified as BA import Data.Char import Data.List (isPrefixOf, foldl') import Data.ByteString (ByteString)-import Data.ByteString.Base16 as BS16+import Data.ByteString qualified as BS+import Data.ByteString.Base16 qualified as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString)+import Data.ByteString.Char8 qualified as Char8 import Data.ByteString.Lazy (toStrict)-import qualified Data.ByteString.Char8  as Char8 import Data.Word (Word8, Word32, Word64)-import Data.Bits (Bits, FiniteBits, shiftR, shift, shiftL, (.&.), (.|.)) import Data.DoubleWord import Data.DoubleWord.TH+import Data.Map (Map) import Data.Maybe (fromMaybe)+import Data.Sequence qualified as Seq+import Data.Serialize qualified as Cereal+import Data.Text qualified as Text+import Data.Text.Encoding qualified as Text+import Data.Vector qualified as V import Numeric (readHex, showHex) import Options.Generic-import Control.Arrow ((>>>))+import EVM.Hexdump (paddedShowHex)+import Control.Monad -import qualified Data.ByteArray       as BA-import qualified Data.Aeson           as JSON-import qualified Data.Aeson.Types     as JSON-import qualified Data.ByteString      as BS-import qualified Data.Serialize.Get   as Cereal-import qualified Data.Text            as Text-import qualified Data.Text.Encoding   as Text-import qualified Data.Sequence        as Seq import qualified Text.Regex.TDFA      as Regex import qualified Text.Read  -- Some stuff for "generic programming", needed to create Word512 import Data.Data-import qualified Data.Vector as V  -- We need a 512-bit word for doing ADDMOD and MULMOD with full precision. mkUnpackedDoubleWord "Word512" ''Word256 "Int512" ''Int256 ''Word256@@ -144,13 +146,13 @@    -- identifiers -  Lit            :: W256 -> Expr EWord+  Lit            :: {-# UNPACK #-} !W256 -> Expr EWord   Var            :: Text -> Expr EWord   GVar           :: GVar a -> Expr a    -- bytes -  LitByte        :: Word8      -> Expr Byte+  LitByte        :: {-# UNPACK #-} !Word8 -> Expr Byte   IndexWord      :: Expr EWord -> Expr EWord -> Expr Byte   EqByte         :: Expr Byte  -> Expr Byte  -> Expr EWord @@ -166,10 +168,10 @@                  -> Expr EWord   -- control flow -  Revert              :: [Prop] -> Expr Buf -> Expr End-  Failure             :: [Prop] -> Error -> Expr End-  Return              :: [Prop] -> Expr Buf -> Expr Storage -> Expr End-  ITE                 :: Expr EWord -> Expr End -> Expr End -> Expr End+  Revert         :: [Prop] -> Expr Buf -> Expr End+  Failure        :: [Prop] -> Error -> Expr End+  Return         :: [Prop] -> Expr Buf -> Expr Storage -> Expr End+  ITE            :: Expr EWord -> Expr End -> Expr End -> Expr End    -- integers @@ -185,6 +187,7 @@   Exp            :: Expr EWord -> Expr EWord -> Expr EWord   SEx            :: Expr EWord -> Expr EWord -> Expr EWord   Min            :: Expr EWord -> Expr EWord -> Expr EWord+  Max            :: Expr EWord -> Expr EWord -> Expr EWord    -- booleans @@ -384,6 +387,7 @@   PNeg :: Prop -> Prop   PAnd :: Prop -> Prop -> Prop   POr :: Prop -> Prop -> Prop+  PImpl :: Prop -> Prop -> Prop   PBool :: Bool -> Prop deriving instance (Show Prop) @@ -430,6 +434,7 @@   PNeg a == PNeg b = a == b   PAnd a b == PAnd c d = a == c && b == d   POr a b == POr c d = a == c && b == d+  PImpl a b == PImpl c d = a == c && b == d   _ == _ = False  instance Ord Prop where@@ -445,6 +450,7 @@   PNeg a <= PNeg b = a <= b   PAnd a b <= PAnd c d = a <= c && b <= d   POr a b <= POr c d = a <= c && b <= d+  PImpl a b <= PImpl c d = a <= c && b <= d   _ <= _ = False  @@ -456,7 +462,7 @@ unlitByte (LitByte x) = Just x unlitByte _ = Nothing -newtype ByteStringS = ByteStringS ByteString deriving (Eq)+newtype ByteStringS = ByteStringS ByteString deriving (Eq, Generic)  instance Show ByteStringS where   show (ByteStringS x) = ("0x" ++) . Text.unpack . fromBinary $ x@@ -464,14 +470,22 @@       fromBinary =         Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex +instance JSON.FromJSON ByteStringS where+  parseJSON (JSON.String x) = case BS16.decodeBase16' x of+                                Left _ -> mzero+                                Right bs -> pure (ByteStringS bs)+  parseJSON _ = mzero+ instance JSON.ToJSON ByteStringS where-  toJSON = JSON.String . Text.pack . show+  toJSON (ByteStringS x) = JSON.String (Text.pack $ "0x" ++ (concatMap (paddedShowHex 2) . BS.unpack $ x))  newtype Addr = Addr { addressWord160 :: Word160 }   deriving     ( Num, Integral, Real, Ord, Enum     , Eq, Generic, Bits, FiniteBits     )+instance JSON.ToJSON Addr where+  toJSON = JSON.String . Text.pack . show  maybeLitWord :: Expr EWord -> Maybe W256 maybeLitWord (Lit w) = Just w@@ -485,8 +499,28 @@   showsPrec _ s = ("0x" ++) . showHex s  instance JSON.ToJSON W256 where-  toJSON = JSON.String . Text.pack . show+  toJSON x = JSON.String  $ Text.pack ("0x" ++ pad ++ cutshow)+    where+      cutshow = drop 2 $ show x+      pad = replicate (64 - length (cutshow)) '0' +newtype W64 = W64 Data.Word.Word64+  deriving+    ( Num, Integral, Real, Ord, Generic+    , Bits , FiniteBits, Enum, Eq , Bounded+    )+instance JSON.FromJSON W64++instance Read W64 where+  readsPrec _ "0x" = [(0, "")]+  readsPrec n s = first W64 <$> readsPrec n s++instance Show W64 where+  showsPrec _ s = ("0x" ++) . showHex s++instance JSON.ToJSON W64 where+  toJSON x = JSON.String  $ Text.pack $ show x+ instance Read Addr where   readsPrec _ ('0':'x':s) = readHex s   readsPrec _ s = readHex s@@ -497,6 +531,14 @@         str = replicate (40 - length hex) '0' ++ hex     in "0x" ++ toChecksumAddress str ++ drop 40 str +instance JSON.ToJSONKey Addr where+  toJSONKey = JSON.toJSONKeyText (addrKey)+    where+      addrKey :: Addr -> Text+      addrKey addr = Text.pack $ replicate (40 - length hex) '0' ++ hex+        where+          hex = show addr+ -- https://eips.ethereum.org/EIPS/eip-55 toChecksumAddress :: String -> String toChecksumAddress addr = zipWith transform nibbles addr@@ -552,13 +594,13 @@  hexByteString :: String -> ByteString -> ByteString hexByteString msg bs =-  case BS16.decode bs of+  case BS16.decodeBase16 bs of     Right x -> x     _ -> error ("invalid hex bytestring for " ++ msg)  hexText :: Text -> ByteString hexText t =-  case BS16.decode (Text.encodeUtf8 (Text.drop 2 t)) of+  case BS16.decodeBase16 (Text.encodeUtf8 (Text.drop 2 t)) of     Right x -> x     _ -> error ("invalid hex bytestring " ++ show t) @@ -597,9 +639,6 @@ padLeft :: Int -> ByteString -> ByteString padLeft n xs = BS.replicate (n - BS.length xs) 0 <> xs -padLeftStr :: Int -> String -> String-padLeftStr n xs = replicate (n - length xs) '0' <> xs- padRight :: Int -> ByteString -> ByteString padRight n xs = xs <> BS.replicate (n - BS.length xs) 0 @@ -616,6 +655,9 @@ padLeft' n xs = V.replicate (n - length xs) (LitByte 0) <> xs  word256 :: ByteString -> Word256+word256 xs | BS.length xs == 1 =+  -- optimize one byte pushes+  Word256 (Word128 0 0) (Word128 0 (fromIntegral $ BS.head xs)) word256 xs = case Cereal.runGet m (padLeft 32 xs) of                Left _ -> error "internal error"                Right x -> x@@ -624,14 +666,11 @@            b <- Cereal.getWord64be            c <- Cereal.getWord64be            d <- Cereal.getWord64be-           return $ fromHiAndLo (fromHiAndLo a b) (fromHiAndLo c d)+           pure $ Word256 (Word128 a b) (Word128 c d)  word :: ByteString -> W256 word = W256 . word256 -byteAt :: (Bits a, Bits b, Integral a, Num b) => a -> Int -> b-byteAt x j = num (x `shiftR` (j * 8)) .&. 0xff- fromBE :: (Integral a) => ByteString -> a fromBE xs = if xs == mempty then 0   else 256 * fromBE (BS.init xs)@@ -643,10 +682,12 @@   <> BS.pack [num $ x `mod` 256]  word256Bytes :: W256 -> ByteString-word256Bytes x = BS.pack [byteAt x (31 - i) | i <- [0..31]]+word256Bytes (W256 (Word256 (Word128 a b) (Word128 c d))) =+  Cereal.encode a <> Cereal.encode b <> Cereal.encode c <> Cereal.encode d  word160Bytes :: Addr -> ByteString-word160Bytes x = BS.pack [byteAt x.addressWord160 (19 - i) | i <- [0..19]]+word160Bytes (Addr (Word160 a (Word128 b c))) =+  Cereal.encode a <> Cereal.encode b <> Cereal.encode c  newtype Nibble = Nibble Word8   deriving ( Num, Integral, Real, Ord, Enum, Eq, Bounded, Generic)@@ -724,3 +765,23 @@     regex = Regex.makeRegexOpts compOpts execOpts (Text.unpack regexSource)   in     Regex.matchTest regex . Seq.fromList . Text.unpack++data VMTrace =+  VMTrace+  { tracePc      :: Int+  , traceOp      :: Int+  , traceStack   :: [W256]+  , traceMemSize :: Data.Word.Word64+  , traceDepth   :: Int+  , traceGas     :: Data.Word.Word64+  , traceError   :: Maybe String+  } deriving (Generic, Show)+instance JSON.ToJSON VMTrace where+  toEncoding = JSON.genericToEncoding JSON.defaultOptions+instance JSON.FromJSON VMTrace++bsToHex :: ByteString -> String+bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)++bssToBs :: ByteStringS -> ByteString+bssToBs (ByteStringS bs) = bs

@@ -926,10 +926,6 @@                   _ -> Nothing               _ -> Just "<symbolic decimal>" --word32Bytes :: Word32 -> ByteString-word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]]- abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM () abiCall params args =   let cd = case args of

@@ -352,7 +352,7 @@                        -> Either BlockchainError Case fromBlockchainCase' block tx preState postState =   let isCreate = isNothing tx.txToAddr in-  case (sender 1 tx, checkTx tx block preState) of+  case (sender tx, checkTx tx block preState) of       (Nothing, _) -> Left SignatureUnverified       (_, Nothing) -> Left (if isCreate then FailedCreate else InvalidTx)       (Just origin, Just checkState) -> Right $ Case@@ -420,7 +420,7 @@ validateTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe () validateTx tx block cs = do   let cs' = Map.map fst cs-  origin        <- sender 1 tx+  origin        <- sender tx   originBalance <- (view balance) <$> view (at origin) cs'   originNonce   <- (view nonce)   <$> view (at origin) cs'   let gasDeposit = (effectiveprice tx block.blockBaseFee) * (num tx.txGasLimit)@@ -431,7 +431,7 @@  checkTx :: Transaction -> Block -> Map Addr (EVM.Contract, Storage) -> Maybe (Map Addr (EVM.Contract, Storage)) checkTx tx block prestate = do-  origin <- sender 1 tx+  origin <- sender tx   validateTx tx block prestate   let isCreate   = isNothing tx.txToAddr       senderNonce = view (accountAt origin . nonce) (Map.map fst prestate)

@@ -0,0 +1,870 @@+{-|+Module      : Tracing+Description : Tests to fuzz concrete tracing, and symbolic execution++Functions here are used to generate traces for the concrete+execution of HEVM and check that against evmtool from go-ehereum. Re-using some+of this code, we also generate a symbolic expression then evaluate it+concretely through Expr.simplify, then check that against evmtool's output.+-}++{-# Language DataKinds #-}+{-# Language DuplicateRecordFields #-}+{-# LANGUAGE DeriveGeneric #-}++module EVM.Tracing where++import Data.ByteString (ByteString)+import System.Directory+import System.IO+import qualified Data.Word+import GHC.Generics+import Numeric (showHex)+import qualified Paths_hevm as Paths++import Prelude hiding (fail, LT, GT)++import qualified Data.ByteString as BS+import Data.Maybe+import Data.List qualified (length)+import Test.Tasty+import Test.Tasty.QuickCheck hiding (Failure)+import Test.QuickCheck.Instances.Text()+import Test.QuickCheck.Instances.Natural()+import Test.QuickCheck.Instances.ByteString()+import Test.QuickCheck (elements)+import Test.Tasty.HUnit+import qualified Data.Aeson as JSON+import Data.Aeson ((.:), (.:?))+import Data.ByteString.Char8 qualified as Char8++import qualified Control.Monad (when)+import qualified Control.Monad.Operational as Operational (view, ProgramViewT(..), ProgramView)+import Control.Monad.State.Strict hiding (state)+import Control.Monad.State.Strict qualified as State+import Control.Lens hiding (List, pre, (.>), re, op)++import qualified Data.Vector as Vector+import qualified Data.Map.Strict as Map++import EVM hiding (allowFFI)+import EVM.SymExec+import EVM.Assembler+import EVM.Op hiding (getOp)+import EVM.Exec+import EVM.Types+import EVM.Traversals+import EVM.Concrete (createAddress)+import qualified EVM.FeeSchedule as FeeSchedule+import EVM.Solvers+import qualified EVM.Expr as Expr+import qualified Data.Text.IO as T+import qualified EVM.Stepper as Stepper+import qualified EVM.Fetch as Fetch+import System.Process+import qualified EVM.Transaction+import EVM.Format (formatBinary)+import EVM.Sign (deriveAddr)+import GHC.IO.Exception (ExitCode(ExitSuccess))++data VMTraceResult =+  VMTraceResult+  { out  :: ByteStringS+  , gasUsed :: Data.Word.Word64+  } deriving (Generic, Show)++instance JSON.ToJSON VMTraceResult where+  toEncoding = JSON.genericToEncoding JSON.defaultOptions++data EVMToolTrace =+  EVMToolTrace+    { pc :: Int+    , op :: Int+    , gas :: W256+    , memSize :: Integer+    , depth :: Int+    , refund :: Int+    , opName :: String+    , stack :: [W256]+    , error :: Maybe String+    } deriving (Generic, Show)++instance JSON.FromJSON EVMToolTrace where+  parseJSON = JSON.withObject "EVMToolTrace" $ \v -> EVMToolTrace+    <$> v .: "pc"+    <*> v .: "op"+    <*> v .: "gas"+    <*> v .: "memSize"+    <*> v .: "depth"+    <*> v .: "refund"+    <*> v .: "opName"+    <*> v .: "stack"+    <*> v .:? "error"++mkBlockHash:: Int -> Expr 'EWord+mkBlockHash x = (num x :: Integer) & show & Char8.pack & EVM.Types.keccak' & Lit++blockHashesDefault :: Map.Map Int W256+blockHashesDefault = Map.fromList [(x, forceLit $ mkBlockHash x) | x<- [1..256]]++data EVMToolOutput =+  EVMToolOutput+    { output :: ByteStringS+    , gasUsed :: W256+    , time :: Integer+    } deriving (Generic, Show)++instance JSON.FromJSON EVMToolOutput++data EVMToolTraceOutput =+  EVMToolTraceOutput+    { trace :: [EVMToolTrace]+    , output :: EVMToolOutput+    } deriving (Generic, Show)++instance JSON.FromJSON EVMToolTraceOutput++data EVMToolEnv = EVMToolEnv+  { coinbase    :: Addr+  , timestamp   :: Expr EWord+  , number      :: W256+  , prevRandao  :: W256+  , gasLimit    :: Data.Word.Word64+  , baseFee     :: W256+  , maxCodeSize :: W256+  , schedule    :: FeeSchedule.FeeSchedule Data.Word.Word64+  , blockHashes :: Map.Map Int W256+  } deriving (Show, Generic)++instance JSON.ToJSON EVMToolEnv where+  toJSON b = JSON.object [ ("currentCoinBase"  , (JSON.toJSON $ b.coinbase))+                         , ("currentDifficulty", (JSON.toJSON $ b.prevRandao))+                         , ("currentGasLimit"  , (JSON.toJSON ("0x" ++ showHex (toInteger $ b.gasLimit) "")))+                         , ("currentNumber"    , (JSON.toJSON $ b.number))+                         , ("currentTimestamp" , (JSON.toJSON tstamp))+                         , ("currentBaseFee"   , (JSON.toJSON $ b.baseFee))+                         , ("blockHashes"      , (JSON.toJSON $ b.blockHashes))+                         ]+              where+                tstamp :: W256+                tstamp = case (b.timestamp) of+                              Lit a -> a+                              _ -> error "Timestamp needs to be a Lit"++emptyEvmToolEnv :: EVMToolEnv+emptyEvmToolEnv = EVMToolEnv { coinbase = 0+                             , timestamp = Lit 0+                             , number     = 0+                             , prevRandao = 42069+                             , gasLimit   = 0xffffffffffffffff+                             , baseFee    = 0+                             , maxCodeSize= 0xffffffff+                             , schedule   = FeeSchedule.berlin+                             , blockHashes = mempty+                             }++data EVMToolReceipt =+  EVMToolReceipt+    { _type :: String+    , root :: String+    , status :: String+    , cumulativeGasUsed :: String+    , logsBloom :: String+    , logs :: Maybe String+    , transactionHash :: String+    , contractAddress :: String+    , gasUsed :: String+    , blockHash :: String+    , transactionIndex :: String+    } deriving (Generic, Show)++instance JSON.FromJSON EVMToolReceipt where+    parseJSON = JSON.withObject "EVMReceipt" $ \v -> EVMToolReceipt+        <$> v .: "type"+        <*> v .: "root"+        <*> v .: "status"+        <*> v .: "cumulativeGasUsed"+        <*> v .: "logsBloom"+        <*> v .: "logs"+        <*> v .: "transactionHash"+        <*> v .: "contractAddress"+        <*> v .: "gasUsed"+        <*> v .: "blockHash"+        <*> v .: "transactionIndex"++data EVMToolResult =+  EVMToolResult+  { stateRoot :: String+  , txRoot :: String+  , receiptsRoot :: String+  , logsHash :: String+  , logsBloom :: String+  , receipts :: [EVMToolReceipt]+  , currentDifficulty :: String+  , gasUsed :: String+  , rejected :: Maybe [EVMRejected]+  } deriving (Generic, Show)++instance JSON.FromJSON EVMToolResult++data EVMRejected =+  EVMRejected+    { index :: Int+    , err :: String+    } deriving (Generic, Show)++instance JSON.FromJSON EVMRejected where+  parseJSON = JSON.withObject "EVMRejected" $ \v -> EVMRejected+    <$> v .: "index"+    <*> v .: "error"++data EVMToolAlloc =+  EVMToolAlloc+  { balance :: W256+  , code :: ByteString+  , nonce :: W64+  } deriving (Generic)++instance JSON.ToJSON EVMToolAlloc where+  toJSON b = JSON.object [ ("balance" , (JSON.toJSON $ show b.balance))+                         , ("code", (JSON.toJSON $ ByteStringS b.code))+                         , ("nonce", (JSON.toJSON $ b.nonce))+                         ]++emptyEVMToolAlloc :: EVMToolAlloc+emptyEVMToolAlloc = EVMToolAlloc { balance = 0+                                 , code = mempty+                                 , nonce = 0+                                 }+-- Sets up common parts such as TX, origin contract, and environment that can+-- later be used to create & execute either an evmtool (from go-ethereum) or an+-- HEVM transaction. Some elements here are hard-coded such as the secret key,+-- which are currently not being fuzzed.+evmSetup :: OpContract -> ByteString -> Int -> (EVM.Transaction.Transaction, EVMToolEnv, EVMToolAlloc, Addr, Addr, Integer)+evmSetup contr txData gaslimitExec = (txn, evmEnv, contrAlloc, fromAddress, toAddress, sk)+  where+    contrLits = assemble $ getOpData contr+    toW8fromLitB :: Expr 'Byte -> Data.Word.Word8+    toW8fromLitB (LitByte a) = a+    toW8fromLitB _ = error "Cannot convert non-litB"++    bitcode = BS.pack . Vector.toList $ toW8fromLitB <$> contrLits+    contrAlloc = EVMToolAlloc{ balance = 0xa493d65e20984bc+                             , code = bitcode+                             , nonce = 0x48+                             }+    txn = EVM.Transaction.Transaction+      { txData     = txData+      , txGasLimit = fromIntegral gaslimitExec+      , txGasPrice = Just 1+      , txNonce    = 172+      , txToAddr   = Just 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192+      , txR        = 0 -- will be fixed when we sign+      , txS        = 0 -- will be fixed when we sign+      , txV        = 0 -- will be fixed when we sign+      , txValue    = 0 -- setting this > 0 fails because HEVM doesn't handle value sent in toplevel transaction+      , txType     = EVM.Transaction.EIP1559Transaction+      , txAccessList = []+      , txMaxPriorityFeeGas =  Just 1+      , txMaxFeePerGas = Just 1+      , txChainId = 1+      }+    evmEnv = EVMToolEnv { coinbase   =  0xff+                        , timestamp   =  Lit 0x3e8+                        , number      =  0x0+                        , prevRandao  =  0x0+                        , gasLimit    =  fromIntegral gaslimitExec+                        , baseFee     =  0x0+                        , maxCodeSize =  0xfffff+                        , schedule    =  FeeSchedule.berlin+                        , blockHashes =  blockHashesDefault+                        }+    sk = 0xDC38EE117CAE37750EB1ECC5CFD3DE8E85963B481B93E732C5D0CB66EE6B0C9D+    fromAddress :: Addr+    fromAddress = fromJust $ deriveAddr sk+    toAddress :: Addr+    toAddress = 0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192++getHEVMRet :: OpContract -> ByteString -> Int -> IO (Either (EVM.Error, [VMTrace]) (Expr 'End, [VMTrace], VMTraceResult))+getHEVMRet contr txData gaslimitExec = do+  let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec+  hevmRun <- runCodeWithTrace Nothing evmEnv contrAlloc txn (fromAddress, toAddress)+  return hevmRun++getEVMToolRet :: OpContract -> ByteString -> Int -> IO (Maybe EVMToolResult)+getEVMToolRet contr txData gaslimitExec = do+  let (txn, evmEnv, contrAlloc, fromAddress, toAddress, sk) = evmSetup contr txData gaslimitExec+      txs = [EVM.Transaction.sign sk txn]+      walletAlloc = EVMToolAlloc{ balance = 0x5ffd4878be161d74+                                , code = BS.empty+                                , nonce = 0xac+                                }+      alloc :: Map.Map Addr EVMToolAlloc+      alloc = Map.fromList ([ (fromAddress, walletAlloc), (toAddress, contrAlloc)])+  JSON.encodeFile "txs.json" txs+  JSON.encodeFile "alloc.json" alloc+  JSON.encodeFile "env.json" evmEnv+  (exitCode, evmtoolStdout, evmtoolStderr) <- readProcessWithExitCode "evm" [ "transition"+                               ,"--input.alloc" , "alloc.json"+                               , "--input.env" , "env.json"+                               , "--input.txs" , "txs.json"+                               , "--output.alloc" , "alloc-out.json"+                               , "--trace.returndata=true"+                               , "--trace" , "trace.json"+                               , "--output.result", "result.json"+                               ] ""+  Control.Monad.when (exitCode /= ExitSuccess) $ do+                   putStrLn $ "evmtool exited with code " <> show exitCode+                   putStrLn $ "evmtool stderr output:" <> show evmtoolStderr+                   putStrLn $ "evmtool stdout output:" <> show evmtoolStdout+  evmtoolResult <- JSON.decodeFileStrict "result.json" :: IO (Maybe EVMToolResult)+  return evmtoolResult++-- Compares traces of evmtool (from go-ethereum) and HEVM+compareTraces :: [VMTrace] -> [EVMToolTrace] -> IO (Bool)+compareTraces hevmTrace evmTrace = go hevmTrace evmTrace+  where+    go :: [VMTrace] -> [EVMToolTrace] -> IO (Bool)+    go [] [] = pure True+    go (a:ax) (b:bx) = do+      let aOp = a.traceOp+          bOp = b.op+          aPc = a.tracePc+          bPc = b.pc+          aStack = a.traceStack+          bStack = b.stack+          aGas = fromIntegral a.traceGas+          bGas = b.gas+      if aGas /= bGas then do+                          putStrLn "GAS doesn't match:"+                          putStrLn $ "HEVM's gas   : " <> (show aGas)+                          putStrLn $ "evmtool's gas: " <> (show bGas)+                          else+                          -- putStrLn $ "Gas match   : " <> (show aGas)+                          return ()+      if aOp /= bOp || aPc /= bPc then+                          putStrLn $ "HEVM: " <> (intToOpName aOp) <> " (pc " <> (show aPc) <> ") --- evmtool " <> (intToOpName bOp) <> " (pc " <> (show bPc) <> ")"+                          else+                          -- putStrLn $ "trace element match. " <> (intToOpName aOp) <> " pc: " <> (show aPc)+                          return ()++      Control.Monad.when (isJust b.error) $ do+                           putStrLn $ "Error by evmtool: " <> (show b.error)+                           putStrLn $ "Error by HEVM   : " <> (show a.traceError)++      Control.Monad.when (aStack /= bStack) $ do+                          putStrLn "stacks don't match:"+                          putStrLn $ "HEVM's stack   : " <> (show aStack)+                          putStrLn $ "evmtool's stack: " <> (show bStack)+      if aOp == bOp && aStack == bStack && aPc == bPc && aGas == bGas then go ax bx+      else pure False+++    go a@(_:_) [] = do+      putStrLn $ "Traces don't match. HEVM's trace is longer by:" <> (show a)+      pure False+    go [] [b] = do+      -- evmtool produces ONE more trace element of the error+      -- hevm on the other hand stops and doens't produce one more+      if isJust b.error then pure True+                           else do+                             putStrLn $ "Traces don't match. HEVM's trace is longer by:" <> (show b)+                             pure False+    go [] b@(_:_) = do+      putStrLn $ "Traces don't match. evmtool's trace is longer by:" <> (show b)+      pure False++getTraceFileName :: EVMToolResult -> String+getTraceFileName evmtoolResult = traceFileName+  where+    txName = ((evmtoolResult.receipts) !! 0).transactionHash+    traceFileName = "trace-0-" ++ txName ++ ".jsonl"++getTraceOutput :: Maybe EVMToolResult -> IO (Maybe EVMToolTraceOutput)+getTraceOutput evmtoolResult =+  case evmtoolResult of+    Nothing -> pure Nothing+    Just res -> do+      let traceFileName = getTraceFileName res+      convertPath <- Paths.getDataFileName "test/scripts/convert_trace_to_json.sh"+      (exitcode, _, _) <- readProcessWithExitCode "bash" [convertPath, getTraceFileName res] ""+      case exitcode of+        ExitSuccess -> JSON.decodeFileStrict (traceFileName ++ ".json") :: IO (Maybe EVMToolTraceOutput)+        _ -> pure Nothing++deleteTraceOutputFiles :: Maybe EVMToolResult -> IO ()+deleteTraceOutputFiles evmtoolResult =+  case evmtoolResult of+    Nothing -> return ()+    Just res -> do+      let traceFileName = getTraceFileName res+      System.Directory.removeFile traceFileName+      System.Directory.removeFile (traceFileName ++ ".json")++-- Create symbolic VM from concrete VM+symbolify :: VM -> VM+symbolify vm = vm { _state = vm._state { _calldata = AbstractBuf "calldata" } }++-- | Takes a runtime code and calls it with the provided calldata+--   Uses evmtool's alloc and transaction to set up the VM correctly+runCodeWithTrace :: Fetch.RpcInfo -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> IO (Either (EVM.Error, [VMTrace]) ((Expr 'End, [VMTrace], VMTraceResult)))+runCodeWithTrace rpcinfo evmEnv alloc txn (fromAddr, toAddress) = withSolvers Z3 0 Nothing $ \solvers -> do+  let origVM = vmForRuntimeCode code' calldata' evmEnv alloc txn (fromAddr, toAddress)+      calldata' = ConcreteBuf txn.txData+      code' = alloc.code+      buildExpr :: SolverGroup -> VM -> IO (Expr End)+      buildExpr s vm = evalStateT (interpret (Fetch.oracle s Nothing) Nothing Nothing runExpr) vm++  expr <- buildExpr solvers $ symbolify origVM+  (res, (vm, trace)) <- runStateT (interpretWithTrace (Fetch.oracle solvers rpcinfo) Stepper.execFully) (origVM, [])+  case res of+    Left x -> pure $ Left (x, trace)+    Right _ -> pure $ Right (expr, trace, vmres vm)++vmForRuntimeCode :: ByteString -> Expr Buf -> EVMToolEnv -> EVMToolAlloc -> EVM.Transaction.Transaction -> (Addr, Addr) -> VM+vmForRuntimeCode runtimecode calldata' evmToolEnv alloc txn (fromAddr, toAddress) =+  let contr = initialContract (RuntimeCode (ConcreteRuntimeCode runtimecode))+      contrWithBal = contr { _balance = alloc.balance }+  in+  (makeVm $ VMOpts+    { vmoptContract = contrWithBal+    , vmoptCalldata = (calldata', [])+    , vmoptValue = Lit txn.txValue+    , vmoptStorageBase = Concrete+    , vmoptAddress =  toAddress+    , vmoptCaller = Expr.litAddr fromAddr+    , vmoptOrigin = fromAddr+    , vmoptCoinbase = evmToolEnv.coinbase+    , vmoptNumber = evmToolEnv.number+    , vmoptTimestamp = evmToolEnv.timestamp+    , vmoptGasprice = fromJust txn.txGasPrice+    , vmoptGas = txn.txGasLimit - fromIntegral (EVM.Transaction.txGasCost evmToolEnv.schedule txn)+    , vmoptGaslimit = txn.txGasLimit+    , vmoptBlockGaslimit = evmToolEnv.gasLimit+    , vmoptPrevRandao = evmToolEnv.prevRandao+    , vmoptBaseFee = evmToolEnv.baseFee+    , vmoptPriorityFee = fromJust txn.txMaxPriorityFeeGas+    , vmoptMaxCodeSize = evmToolEnv.maxCodeSize+    , vmoptSchedule = evmToolEnv.schedule+    , vmoptChainId = txn.txChainId+    , vmoptCreate = False+    , vmoptTxAccessList = mempty+    , vmoptAllowFFI = False+    }) & set (EVM.env . contracts . at ethrunAddress)+             (Just (initialContract (RuntimeCode (ConcreteRuntimeCode BS.empty))))+       & set (state . calldata) calldata'++runCode :: Fetch.RpcInfo -> ByteString -> Expr Buf -> IO (Maybe (Expr Buf))+runCode rpcinfo code' calldata' = withSolvers Z3 0 Nothing $ \solvers -> do+  let origVM = vmForRuntimeCode code' calldata' emptyEvmToolEnv emptyEVMToolAlloc EVM.Transaction.emptyTransaction (ethrunAddress, createAddress ethrunAddress 1)+  res <- evalStateT (Stepper.interpret (Fetch.oracle solvers rpcinfo) Stepper.execFully) origVM+  pure $ case res of+    Left _ -> Nothing+    Right b -> Just b++vmtrace :: VM -> VMTrace+vmtrace vm =+  let+    -- Convenience function to access parts of the current VM state.+    -- Arcane type signature needed to avoid monomorphism restriction.+    the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a+    the f g = Control.Lens.view (f . g) vm+    memsize = the state memorySize+  in VMTrace { tracePc = the state EVM.pc+             , traceOp = num $ getOp vm+             , traceGas = the state EVM.gas+             , traceMemSize = memsize+             -- increment to match geth format+             , traceDepth = 1 + length (Control.Lens.view frames vm)+             -- reverse to match geth format+             , traceStack = reverse $ forceLit <$> the state EVM.stack+             , traceError = readoutError vm._result+             }+  where+    readoutError :: Maybe VMResult -> Maybe String+    readoutError Nothing = Nothing+    readoutError (Just (VMSuccess _)) = Nothing+    readoutError (Just (VMFailure e)) = case e of+      -- NOTE: error text made to closely match go-ethereum's errors.go file+      OutOfGas {}             -> Just "out of gas"+      -- TODO "contract creation code storage out of gas" not handled+      CallDepthLimitReached   -> Just "max call depth exceeded"+      BalanceTooLow {}        -> Just "insufficient balance for transfer"+      -- TODO "contract address collision" not handled+      EVM.Revert {}           -> Just "execution reverted"+      -- TODO "max initcode size exceeded" not handled+      MaxCodeSizeExceeded {}  -> Just "max code size exceeded"+      EVM.BadJumpDestination  -> Just "invalid jump destination"+      StateChangeWhileStatic  -> Just "write protection"+      ReturnDataOutOfBounds   -> Just "return data out of bounds"+      EVM.IllegalOverflow     -> Just "gas uint64 overflow"+      UnrecognizedOpcode op   -> Just $ "invalid opcode: " <> show op+      EVM.NonceOverflow       -> Just "nonce uint64 overflow"+      EVM.StackUnderrun       -> Just "stack underflow"+      EVM.StackLimitExceeded  -> Just "stack limit reached"+      EVM.InvalidMemoryAccess -> Just "write protection"+      err                     -> Just $ "HEVM error: " <> show err++vmres :: VM -> VMTraceResult+vmres vm =+  let+    gasUsed' = Control.Lens.view (tx . txgaslimit) vm - Control.Lens.view (state . EVM.gas) vm+    res = case Control.Lens.view result vm of+      Just (VMSuccess (ConcreteBuf b)) -> (ByteStringS b)+      Just (VMSuccess x) -> error $ "unhandled: " <> (show x)+      Just (VMFailure (EVM.Revert (ConcreteBuf b))) -> (ByteStringS b)+      Just (VMFailure _) -> ByteStringS mempty+      _ -> ByteStringS mempty+  in VMTraceResult+     { out = res+     , gasUsed = gasUsed'+     }++type TraceState = (VM, [VMTrace])++execWithTrace :: StateT TraceState IO VMResult+execWithTrace = do+  _ <- runWithTrace+  fromJust <$> use (_1 . result)++runWithTrace :: StateT TraceState IO VM+runWithTrace = do+  -- This is just like `exec` except for every instruction evaluated,+  -- we also increment a counter indexed by the current code location.+  vm0 <- use _1+  case vm0._result of+    Nothing -> do+      State.modify (\(a, b) -> (a, b ++ [vmtrace vm0]))+      zoom _1 (State.state (runState exec1))+      runWithTrace+    Just (VMSuccess _) -> pure vm0+    Just (VMFailure _) -> do+      -- Update error text for last trace element+      (a, b) <- State.get+      let updatedElem = (last b) {traceError = (vmtrace vm0).traceError}+          updatedTraces = take ((Data.List.length b)-1) b ++ [updatedElem]+      State.put (a, updatedTraces)+      pure vm0++interpretWithTrace+  :: Fetch.Fetcher+  -> Stepper.Stepper a+  -> StateT TraceState IO a+interpretWithTrace fetcher =+  eval . Operational.view++  where+    eval+      :: Operational.ProgramView Stepper.Action a+      -> StateT TraceState IO a++    eval (Operational.Return x) =+      pure x++    eval (action Operational.:>>= k) =+      case action of+        Stepper.Exec ->+          execWithTrace >>= interpretWithTrace fetcher . k+        Stepper.Run ->+          runWithTrace >>= interpretWithTrace fetcher . k+        Stepper.Wait q ->+          do m <- liftIO (fetcher q)+             zoom _1 (State.state (runState m)) >> interpretWithTrace fetcher (k ())+        Stepper.Ask _ ->+          error "cannot make choice in this interpreter"+        Stepper.IOAct q ->+          zoom _1 (StateT (runStateT q)) >>= interpretWithTrace fetcher . k+        Stepper.EVM m ->+          zoom _1 (State.state (runState m)) >>= interpretWithTrace fetcher . k++data OpContract = OpContract [Op]+instance Show OpContract where+  show (OpContract a) = "OpContract " ++ (show a)++getOpData :: OpContract-> [Op]+getOpData (OpContract x) = x++instance Arbitrary OpContract where+  arbitrary = fmap OpContract (sized genContract)++removeExtcalls :: OpContract -> OpContract+removeExtcalls (OpContract ops) = OpContract (filter (noStorageNoExtcalls) ops)+  where+    noStorageNoExtcalls :: Op -> Bool+    noStorageNoExtcalls o = case o of+                               -- Extrenal info functions+                               OpExtcodecopy -> False+                               OpExtcodehash -> False+                               OpExtcodesize -> False+                               OpAddress -> False+                               OpOrigin -> False+                               OpCaller -> False+                               OpCoinbase -> False+                               OpCreate -> False+                               OpCreate2 -> False+                               -- External call functions+                               OpDelegatecall -> False+                               OpStaticcall -> False+                               OpCall -> False+                               OpCallcode -> False+                               -- Not interesting+                               OpBalance -> False+                               OpSelfdestruct -> False+                               _ -> True++getJumpDests :: [Op] -> [Int]+getJumpDests ops = go ops 0 []+    where+      go :: [Op] -> Int -> [Int] -> [Int]+      go [] _ dests = dests+      go (a:ax) pos dests = case a of+                       OpJumpdest -> go ax (pos+1) (pos:dests)+                       OpPush _ -> go ax (pos+33) dests+                       -- We'll fix these up later to add a Push in between, hence they are 34 bytes+                       OpJump -> go ax (pos+34) dests+                       OpJumpi -> go ax (pos+34) dests+                       -- everything else is 1 byte+                       _ -> go ax (pos+1) dests++fixContractJumps :: OpContract -> IO OpContract+fixContractJumps (OpContract ops) = do+  let+    addedOps = ops++[OpJumpdest]+    jumpDests = getJumpDests addedOps+    -- always end on an OpJumpdest so we don't have an issue with a "later" position+    ops2 = fixup addedOps 0 []+    -- original set of operations, the set of jumpDests NOW valid, current position, return value+    fixup :: [Op] -> Int -> [Op] -> IO [Op]+    fixup [] _ ret = pure ret+    fixup (a:ax) pos ret = case a of+      OpJumpi -> do+        let filtDests = (filter (> pos) jumpDests)+        rndPos <- randItem filtDests+        fixup ax (pos+34) (ret++[(OpPush (Lit (fromInteger (fromIntegral rndPos)))), (OpJumpi)])+      OpJump -> do+        let filtDests = (filter (> pos) jumpDests)+        rndPos <- randItem filtDests+        fixup ax (pos+34) (ret++[(OpPush (Lit (fromInteger (fromIntegral rndPos)))), (OpJump)])+      myop@(OpPush _) -> fixup ax (pos+33) (ret++[myop])+      myop -> fixup ax (pos+1) (ret++[myop])+  fmap OpContract ops2++genPush :: Int -> Gen [Op]+genPush n = vectorOf n onePush+  where+    onePush :: Gen Op+    onePush  = do+      p <- chooseInt (1, 10)+      pure $ OpPush (Lit (fromIntegral p))++genContract :: Int -> Gen [Op]+genContract n = do+    y <- chooseInt (3, 6)+    pushes <- genPush y+    normalOps <- vectorOf (3*n+40) genOne+    addReturn <- chooseInt (0, 10)+    let contr = pushes ++ normalOps+    if addReturn < 10 then pure $ contr++[OpPush (Lit 0x40), OpPush (Lit 0x0), OpReturn]+                      else pure contr+  where+    genOne :: Gen Op+    genOne = frequency [+      -- math ops+      (200, frequency [+          (1, pure OpAdd)+        , (1, pure OpMul)+        , (1, pure OpSub)+        , (1, pure OpDiv)+        , (1, pure OpSdiv)+        , (1, pure OpMod)+        , (1, pure OpSmod)+        , (1, pure OpAddmod)+        , (1, pure OpMulmod)+        , (1, pure OpExp)+        , (1, pure OpSignextend)+        , (1, pure OpLt)+        , (1, pure OpGt)+        , (1, pure OpSlt)+        , (1, pure OpSgt)+        , (1, pure OpSha3)+      ])+      -- Comparison & binary ops+      , (200, frequency [+          (1, pure OpEq)+        , (1, pure OpIszero)+        , (1, pure OpAnd)+        , (1, pure OpOr)+        , (1, pure OpXor)+        , (1, pure OpNot)+        , (1, pure OpByte)+        , (1, pure OpShl)+        , (1, pure OpShr)+        , (1, pure OpSar)+      ])+      -- calldata+      , (800, pure OpCalldataload)+      , (200, pure OpCalldatacopy)+      -- Get some info+      , (100, frequency [+          (10, pure OpAddress)+        , (10, pure OpBalance)+        , (10, pure OpOrigin)+        , (10, pure OpCaller)+        , (10, pure OpCallvalue)+        , (10, pure OpCalldatasize)+        , (10, pure OpCodesize)+        , (10, pure OpGasprice)+        , (10, pure OpReturndatasize)+        , (10, pure OpReturndatacopy)+        , (10, pure OpExtcodehash)+        , (10, pure OpBlockhash)+        , (10, pure OpCoinbase)+        , (10, pure OpTimestamp)+        , (10, pure OpNumber)+        , (10, pure OpPrevRandao)+        , (10, pure OpGaslimit)+        , (10, pure OpChainid)+        , (10, pure OpSelfbalance)+        , (10, pure OpBaseFee)+        , (10, pure OpPc)+        , (10, pure OpMsize)+        , (10, pure OpGas)+        , (10, pure OpExtcodesize)+        , (10, pure OpCodecopy)+        , (10, pure OpExtcodecopy)+      ])+      -- memory manip+      , (1200, frequency [+          (50, pure OpMload)+        , (50, pure OpMstore)+        , (1, pure OpMstore8)+      ])+      -- storage manip+      , (100, frequency [+          (1, pure OpSload)+        , (1, pure OpSstore)+      ])+      -- Jumping around+      , (20, frequency [+            (1, pure OpJump)+          , (10, pure OpJumpi)+      ])+      -- calling out+      , (1, frequency [+          (1, pure OpStaticcall)+        , (1, pure OpCall)+        , (1, pure OpCallcode)+        , (1, pure OpDelegatecall)+        , (1, pure OpCreate)+        , (1, pure OpCreate2)+        , (1, pure OpSelfdestruct)+      ])+      -- manipulate stack+      , (13000, frequency [+          (1, pure OpPop)+        , (400, do+            -- x <- arbitrary+            large <- chooseInt (0, 100)+            x <- if large == 0 then chooseBoundedIntegral (0::W256, (2::W256)^(256::W256)-1)+                               else chooseBoundedIntegral (0, 10)+            pure $ OpPush (Lit (fromIntegral x)))+        , (10, do+            x <- chooseInt (1, 10)+            pure $ OpDup (fromIntegral x))+        , (10, do+            x <- chooseInt (1, 10)+            pure $ OpSwap (fromIntegral x))+      ])]+      -- End states+      -- , (1, frequency [+      --    (1, pure OpStop)+      --  , (10, pure OpReturn)+      --  , (10, pure OpRevert)+      -- ])++forceLit :: Expr EWord -> W256+forceLit (Lit x) = x+forceLit _ = undefined++randItem :: [a] -> IO a+randItem = generate . Test.QuickCheck.elements++getOp :: VM -> Data.Word.Word8+getOp vm =+  let pcpos  = vm ^. state . EVM.pc+      code' = vm ^. state . EVM.code+      xs = case code' of+        InitCode _ _ -> error "InitCode instead of RuntimeCode"+        RuntimeCode (ConcreteRuntimeCode xs') -> BS.drop pcpos xs'+        RuntimeCode (SymbolicRuntimeCode _) -> error "RuntimeCode is symbolic"+  in if xs == BS.empty then 0+                       else BS.head xs++tests :: TestTree+tests = testGroup "contract-quickcheck-run"+    [ testProperty "random-contract-concrete-call" $ \(contr :: OpContract) -> ioProperty $ do+        txDataRaw <- generate $ sized $ \n -> vectorOf (10*n+5) $ chooseInt (0,255)+        gaslimitExec <- generate $ chooseInt (40000, 0xffff)+        let txData = BS.pack $ toEnum <$> txDataRaw+        -- TODO: By removing external calls, we fuzz less+        --       It should work also when we external calls. Removing for now.+        contrFixed <- fixContractJumps $ removeExtcalls contr+        evmtoolResult <- getEVMToolRet contrFixed txData gaslimitExec+        hevmRun <- getHEVMRet contrFixed txData gaslimitExec+        (Just evmtoolTraceOutput) <- getTraceOutput evmtoolResult+        case hevmRun of+          (Right (expr, hevmTrace, hevmTraceResult)) -> do+            let+              concretize :: Expr a -> Expr Buf -> Expr a+              concretize a c = mapExpr go a+                where+                  go :: Expr a -> Expr a+                  go = \case+                             AbstractBuf "calldata" -> c+                             y -> y+              concretizedExpr = concretize expr (ConcreteBuf txData)+              simplConcExpr = Expr.simplify concretizedExpr+              getReturnVal :: Expr End -> Maybe ByteString+              getReturnVal (Return _ (ConcreteBuf bs) _) = Just bs+              getReturnVal _ = Nothing+              simplConcrExprRetval = getReturnVal simplConcExpr+            traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace)+            -- putStrLn $ "HEVM trace   : " <> show hevmTrace+            -- putStrLn $ "evmtool trace: " <> show (evmtoolTraceOutput.toTrace)+            assertEqual "Traces and gas must match" traceOK True+            let resultOK = evmtoolTraceOutput.output.output == hevmTraceResult.out+            if resultOK then do+              putStrLn $ "HEVM & evmtool's outputs match: '" <> (bsToHex $ bssToBs evmtoolTraceOutput.output.output) <> "'"+              if isNothing simplConcrExprRetval || (fromJust simplConcrExprRetval) == (bssToBs hevmTraceResult.out)+                 then do+                   putStr "OK, symbolic interpretation -> concrete calldata -> Expr.simplify gives the same answer."+                   if isNothing simplConcrExprRetval then putStrLn ", but it was a Nothing, so not strong equivalence"+                                                     else putStrLn ""+                 else do+                   putStrLn $ "concretized expr           : " <> (show concretizedExpr)+                   putStrLn $ "simplified concretized expr: " <> (show simplConcExpr)+                   putStrLn $ "return value computed      : " <> (show simplConcrExprRetval)+                   putStrLn $ "evmtool's return value     : " <> (show hevmTraceResult.out)+                   assertEqual "Simplified, concretized expression must match evmtool's output." True False+            else do+              putStrLn $ "Name of trace file: " <> (getTraceFileName $ fromJust evmtoolResult)+              putStrLn $ "HEVM result  :" <> (show hevmTraceResult)+              T.putStrLn $ "HEVM result: " <> (formatBinary $ bssToBs hevmTraceResult.out)+              T.putStrLn $ "evm result : " <> (formatBinary $ bssToBs evmtoolTraceOutput.output.output)+              putStrLn $ "HEVM result len: " <> (show (BS.length $ bssToBs hevmTraceResult.out))+              putStrLn $ "evm result  len: " <> (show (BS.length $ bssToBs evmtoolTraceOutput.output.output))+            assertEqual "Contract exec successful. HEVM & evmtool's outputs must match" resultOK True+          Left (evmerr, hevmTrace) -> do+            putStrLn $ "HEVM contract exec issue: " <> (show evmerr)+            -- putStrLn $ "evmtool result was: " <> show (fromJust evmtoolResult)+            -- putStrLn $ "output by evmtool is: '" <> bsToHex evmtoolTraceOutput.toOutput.output <> "'"+            traceOK <- compareTraces hevmTrace (evmtoolTraceOutput.trace)+            assertEqual "Traces and gas must match" traceOK True+        System.Directory.removeFile "txs.json"+        System.Directory.removeFile "alloc-out.json"+        System.Directory.removeFile "alloc.json"+        System.Directory.removeFile "result.json"+        System.Directory.removeFile "env.json"+        deleteTraceOutputFiles evmtoolResult+    ]+

@@ -0,0 +1,4 @@+#!/usr/bin/env bash++num=$(wc -l "$1" | cut -d " " -f 1)+awk -v ll="$num" 'BEGIN {print "{\"trace\": [" } {if (NR!=ll) {print $0; if (NR!=ll-1) {print ","}} else {print "], \"output\":" $0}} END{print "}"}' "$1" > "$1.json"

@@ -1,7 +1,7 @@-{-# Language GADTs #-}-{-# Language NumericUnderscores #-} {-# Language QuasiQuotes #-} {-# Language DataKinds #-}+{-# Language DuplicateRecordFields #-}+{-# LANGUAGE DeriveGeneric #-}  module Main where @@ -9,8 +9,8 @@ import Data.ByteString (ByteString) import Data.Bits hiding (And, Xor) import System.Directory+import System.IO import GHC.Natural-import Control.Monad import Text.RE.TDFA.String import Text.RE.Replace import Data.Time@@ -19,10 +19,10 @@ import Prelude hiding (fail, LT, GT)  import qualified Data.ByteString as BS-import qualified Data.ByteString.Base16 as Hex+import qualified Data.ByteString.Base16 as BS16 import Data.Maybe import Data.Typeable-import Data.List (elemIndex)+import Data.List qualified (elemIndex) import Data.DoubleWord import Test.Tasty import Test.Tasty.QuickCheck hiding (Failure)@@ -32,9 +32,10 @@ import Test.Tasty.HUnit import Test.Tasty.Runners hiding (Failure) import Test.Tasty.ExpectedFailure+import EVM.Tracing qualified -import Control.Monad.State.Strict (execState, runState)-import Control.Lens hiding (List, pre, (.>), re)+import Control.Monad.State.Strict hiding (state)+import Control.Lens hiding (List, pre, (.>), re, op)  import qualified Data.Vector as Vector import Data.String.Here@@ -43,7 +44,7 @@ import Data.Binary.Put (runPut) import Data.Binary.Get (runGetOrFail) -import EVM+import EVM hiding (allowFFI) import EVM.SymExec import EVM.ABI import EVM.Exec@@ -72,7 +73,9 @@  tests :: TestTree tests = testGroup "hevm"-  [ testGroup "StorageTests"+  [+  EVM.Tracing.tests+  , testGroup "StorageTests"     [ testCase "read-from-sstore" $ assertEqual ""         (Lit 0xab)         (Expr.readStorage' (Lit 0x0) (Lit 0x0) (SStore (Lit 0x0) (Lit 0x0) (Lit 0xab) AbstractStore))@@ -355,29 +358,37 @@      , testProperty "abi encoding vs. solidity" $ withMaxSuccess 20 $ forAll (arbitrary >>= genAbiValue) $       \y -> ioProperty $ do-          -- traceM ("encoding: " ++ (show y) ++ " : " ++ show (abiValueType y))           Just encoded <- runStatements [i| x = abi.encode(a);|]             [y] AbiBytesDynamicType           let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of                 AbiTuple (Vector.toList -> [e]) -> e                 _ -> error "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])-          -- traceM ("encoded (solidity): " ++ show solidityEncoded)-          -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))           assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)      , testProperty "abi encoding vs. solidity (2 args)" $ withMaxSuccess 20 $ forAll (arbitrary >>= bothM genAbiValue) $       \(x', y') -> ioProperty $ do-          -- traceM ("encoding: " ++ (show x') ++ ", " ++ (show y')  ++ " : " ++ show (abiValueType x') ++ ", " ++ show (abiValueType y'))           Just encoded <- runStatements [i| x = abi.encode(a, b);|]             [x', y'] AbiBytesDynamicType           let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of                 AbiTuple (Vector.toList -> [e]) -> e                 _ -> error "AbiTuple expected"           let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [x',y'])-          -- traceM ("encoded (solidity): " ++ show solidityEncoded)-          -- traceM ("encoded (hevm): " ++ show (AbiBytesDynamic hevmEncoded))           assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)++    -- we need a separate test for this because the type of a function is "function() external" in solidity but just "function" in the abi:+    , testProperty "abi encoding vs. solidity (function pointer)" $ withMaxSuccess 20 $ forAll (genAbiValue AbiFunctionType) $+      \y -> ioProperty $ do+          Just encoded <- runFunction [i|+              function foo(function() external a) public pure returns (bytes memory x) {+                x = abi.encode(a);+              }+            |] (abiMethod "foo(function)" (AbiTuple (Vector.singleton y)))+          let solidityEncoded = case decodeAbiValue (AbiTupleType $ Vector.fromList [AbiBytesDynamicType]) (BS.fromStrict encoded) of+                AbiTuple (Vector.toList -> [e]) -> e+                _ -> error "AbiTuple expected"+          let hevmEncoded = encodeAbiValue (AbiTuple $ Vector.fromList [y])+          assertEqual "abi encoding mismatch" solidityEncoded (AbiBytesDynamic hevmEncoded)     ]    , testGroup "Precompiled contracts"@@ -456,7 +467,7 @@         (json, path') <- solidity' srccode         let (solc', _, _) = fromJust $ readJSON json             initCode :: ByteString-            initCode = (fromJust $ solc' ^? ix (path' <> ":A")).creationCode+            initCode = (solc' ^?! ix (path' <> ":A")).creationCode         -- add constructor arguments         assertEqual "constructor args screwed up metadata stripping" (stripBytecodeMetadata (initCode <> encodeAbiValue (AbiUInt 256 1))) (stripBytecodeMetadata initCode)     ]@@ -499,7 +510,7 @@              }             }            |]-       (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+       (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts        assertEqual "Must be 0" 0 $ getVar ctr "arg1"        putStrLn  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")      ,@@ -512,7 +523,7 @@               }              }             |]-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x11] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         let x = getVar ctr "arg1"         let y = getVar ctr "arg2" @@ -529,10 +540,22 @@               }              }             |]-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x12] c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         assertEqual "Division by 0 needs b=0" (getVar ctr "arg2") 0         putStrLn "expected counterexample found"      ,+      testCase "unused-args-fail" $ do+         Just c <- solcRuntime "C"+             [i|+             contract C {+               function fun(uint256 a) public pure {+                 assert(false);+               }+             }+             |]+         (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x1] c Nothing [] debugVeriOpts+         putStrLn "expected counterexample found"+      ,      testCase "enum-conversion-fail" $ do         Just c <- solcRuntime "MyContract"             [i|@@ -543,7 +566,7 @@               }              }             |]-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x21] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         assertBool "Enum is only defined for 0 and 1" $ (getVar ctr "arg1") > 1         putStrLn "expected counterexample found"      ,@@ -564,7 +587,7 @@               }              }             |]-        a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just ("fun(uint8)", [AbiUIntType 8])) [] defaultVeriOpts+        a <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x31] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts         print $ length a         print $ show a         putStrLn "expected counterexample found"@@ -581,8 +604,8 @@               }              }             |]-        (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just ("fun(uint8)", [AbiUIntType 8])) [] defaultVeriOpts-        assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1+        (_, [Cex (_, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x32] c (Just (Sig "fun(uint8)" [AbiUIntType 8])) [] defaultVeriOpts+        -- assertBool "Access must be beyond element 2" $ (getVar ctr "arg1") > 1         putStrLn "expected counterexample found"       ,       -- TODO the system currently does not allow for symbolic array size allocation@@ -595,7 +618,7 @@               }              }             |]-        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x41] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x41] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "expected counterexample found"       ,       -- TODO the system currently does not allow for symbolic JUMP@@ -615,7 +638,7 @@               }              }             |]-        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x51] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x51] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "expected counterexample found"  ] @@ -675,7 +698,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256)", [AbiIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256)" [AbiIntType 256])) [] defaultVeriOpts         putStrLn "Require works as expected"      ,      testCase "ITE-with-bitwise-AND" $ do@@ -695,7 +718,7 @@          }          |]        -- should find a counterexample-       (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+       (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts        putStrLn "expected counterexample found"      ,      testCase "ITE-with-bitwise-OR" $ do@@ -713,7 +736,7 @@            }          }          |]-       (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+       (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts        putStrLn "this should always be true, due to bitwise OR with positive value"     ,     -- CopySlice check@@ -747,7 +770,7 @@           , askSmtIters = Nothing           , rpcInfo = Nothing           }-        calldata' = Just ("checkval(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])+        calldata' = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])       (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->         checkAssert s defaultPanicCodes c calldata' [] opts       putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"@@ -767,7 +790,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts         putStrLn "SAR works as expected"      ,      testCase "opcode-sar-pos" $ do@@ -784,7 +807,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts         putStrLn "SAR works as expected"      ,      testCase "opcode-sar-fixedval-pos" $ do@@ -801,7 +824,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts         putStrLn "SAR works as expected"      ,      testCase "opcode-sar-fixedval-neg" $ do@@ -818,7 +841,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(int256,int256)", [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(int256,int256)" [AbiIntType 256, AbiIntType 256])) [] defaultVeriOpts         putStrLn "SAR works as expected"      ,      testCase "opcode-div-zero-1" $ do@@ -835,7 +858,7 @@               }             }             |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "sdiv works as expected"       ,      testCase "opcode-div-zero-2" $ do@@ -852,7 +875,7 @@               }             }             |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "sdiv works as expected"      ,      testCase "opcode-sdiv-zero-1" $ do@@ -869,7 +892,7 @@               }             }             |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "sdiv works as expected"       ,      testCase "opcode-sdiv-zero-2" $ do@@ -886,9 +909,22 @@               }             }             |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "sdiv works as expected"       ,+     testCase "signed-overflow-checks" $ do+        Just c <- solcRuntime "C"+            [i|+            contract C {+              function fun(uint160 a) external {+                  int256 j = int256(uint256(a)) + 1;+                  assert(false);+              }+            }+            |]+        (_, [Cex _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint160)" [AbiUIntType 160])) [] defaultVeriOpts+        putStrLn "expected cex discovered"+      ,      testCase "opcode-signextend-neg" $ do         Just c <- solcRuntime "MyContract"             [i|@@ -908,7 +944,7 @@               }             }             |]-        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _])  <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts         putStrLn "signextend works as expected"       ,      testCase "opcode-signextend-pos-nochop" $ do@@ -926,7 +962,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts         putStrLn "signextend works as expected"       ,       testCase "opcode-signextend-pos-chopped" $ do@@ -944,7 +980,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts         putStrLn "signextend works as expected"       ,       -- when b is too large, value is unchanged@@ -962,7 +998,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint8)", [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint8)" [AbiUIntType 256, AbiUIntType 8])) [] defaultVeriOpts         putStrLn "signextend works as expected"      ,      testCase "opcode-shl" $ do@@ -980,7 +1016,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         putStrLn "SAR works as expected"      ,      testCase "opcode-xor-cancel" $ do@@ -997,7 +1033,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         putStrLn "XOR works as expected"       ,       testCase "opcode-xor-reimplement" $ do@@ -1013,7 +1049,7 @@               }              }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts         putStrLn "XOR works as expected"       ,       testCase "opcode-addmod-no-overflow" $ do@@ -1036,7 +1072,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint8,uint8,uint8)", [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts         putStrLn "ADDMOD is fine on NON overflow values"       ,       testCase "opcode-mulmod-no-overflow" $ do@@ -1059,7 +1095,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint8,uint8,uint8)", [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint8,uint8,uint8)" [AbiUIntType 8, AbiUIntType 8, AbiUIntType 8])) [] defaultVeriOpts         putStrLn "MULMOD is fine on NON overflow values"       ,       testCase "opcode-div-res-zero-on-div-by-zero" $ do@@ -1076,7 +1112,7 @@               }             }             |]-        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint16)", [AbiUIntType 16])) [] defaultVeriOpts+        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint16)" [AbiUIntType 16])) [] defaultVeriOpts         putStrLn "DIV by zero is zero"       ,       -- Somewhat tautological since we are asserting the precondition@@ -1094,15 +1130,16 @@                                        [x', y'] -> (x', y')                                        _ -> error "expected 2 args"                         in (x .<= Expr.add x y)+                        -- TODO check if it's needed                            .&& view (state . callvalue) preVM .== Lit 0             post prestate leaf =               let (x, y) = case getStaticAbiArgs 2 prestate of                              [x', y'] -> (x', y')                              _ -> error "expected 2 args"               in case leaf of-                   Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)+                   EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Add x y)                    _ -> PBool True-        (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)+        (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"      , @@ -1120,16 +1157,16 @@                                        _ -> error "expected 2 args"                         in (x .<= Expr.add x y)                            .&& (x .== y)-                           .&& view (state . callvalue) preVM .== Lit 0+                           .&& Control.Lens.view (state . callvalue) preVM .== Lit 0             post prestate leaf =               let (_, y) = case getStaticAbiArgs 2 prestate of                              [x', y'] -> (x', y')                              _ -> error "expected 2 args"               in case leaf of-                   Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)+                   EVM.Types.Return _ b _ -> (ReadWord (Lit 0) b) .== (Mul (Lit 2) y)                    _ -> PBool True         (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s ->-          verifyContract s safeAdd (Just ("add(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)+          verifyContract s safeAdd (Just (Sig "add(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"       ,       testCase "summary storage writes" $ do@@ -1145,17 +1182,17 @@             }           }           |]-        let pre vm = Lit 0 .== view (state . callvalue) vm+        let pre vm = Lit 0 .== Control.Lens.view (state . callvalue) vm             post prestate leaf =               let y = case getStaticAbiArgs 1 prestate of                         [y'] -> y'                         _ -> error "expected 1 arg"-                  this = Expr.litAddr $ view (state . codeContract) prestate-                  prex = Expr.readStorage' this (Lit 0) (view (env . storage) prestate)+                  this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate+                  prex = Expr.readStorage' this (Lit 0) (Control.Lens.view (EVM.env . EVM.storage) prestate)               in case leaf of-                Return _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)+                EVM.Types.Return _ _ postStore -> Expr.add prex (Expr.mul (Lit 2) y) .== (Expr.readStorage' this (Lit 0) postStore)                 _ -> PBool True-        (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)+        (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)         putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         -- tests how whiffValue handles Neg via application of the triple IsZero simplification rule@@ -1180,7 +1217,7 @@                     }                     |]             Just c <- yulRuntime "Neg" src-            (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("hello(address)", [AbiAddressType])) [] defaultVeriOpts+            (res, [Qed _]) <- withSolvers Z3 4 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "hello(address)" [AbiAddressType])) [] defaultVeriOpts             putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "catch-storage-collisions-noproblem" $ do@@ -1199,22 +1236,22 @@               }             }             |]-          let pre vm = (Lit 0) .== view (state . callvalue) vm+          let pre vm = (Lit 0) .== Control.Lens.view (state . callvalue) vm               post prestate poststate =                 let (x,y) = case getStaticAbiArgs 2 prestate of                         [x',y'] -> (x',y')                         _ -> error "expected 2 args"-                    this = Expr.litAddr $ view (state . codeContract) prestate-                    prestore =  view (env . storage) prestate+                    this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate+                    prestore =  Control.Lens.view (EVM.env . EVM.storage) prestate                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     Return _ _ poststore -> let+                     EVM.Types.Return _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty                      _ -> PBool True-          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)+          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)           putStrLn "Correct, this can never fail"         ,         -- Inspired by these `msg.sender == to` token bugs@@ -1233,22 +1270,22 @@               }             }             |]-          let pre vm = (Lit 0) .== view (state . callvalue) vm+          let pre vm = (Lit 0) .== Control.Lens.view (state . callvalue) vm               post prestate poststate =                 let (x,y) = case getStaticAbiArgs 2 prestate of                         [x',y'] -> (x',y')                         _ -> error "expected 2 args"-                    this = Expr.litAddr $ view (state . codeContract) prestate-                    prestore =  view (env . storage) prestate+                    this = Expr.litAddr $ Control.Lens.view (state . codeContract) prestate+                    prestore =  Control.Lens.view (EVM.env . EVM.storage) prestate                     prex = Expr.readStorage' this x prestore                     prey = Expr.readStorage' this y prestore                 in case poststate of-                     Return _ _ poststore -> let+                     EVM.Types.Return _ _ poststore -> let                            postx = Expr.readStorage' this x poststore                            posty = Expr.readStorage' this y poststore                        in Expr.add prex prey .== Expr.add postx posty                      _ -> PBool True-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts SymbolicS (Just pre) (Just post)           let x = getVar ctr "arg1"           let y = getVar ctr "arg2"           putStrLn $ "y:" <> show y@@ -1265,7 +1302,7 @@               }              }             |]-          (_, [Cex (l, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo()", [])) [] defaultVeriOpts+          (_, [Cex (l, _)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo()" [])) [] defaultVeriOpts           assertEqual "incorrect revert msg" l (EVM.Types.Revert [] (ConcreteBuf $ panicMsg 0x01))         ,         testCase "simple-assert-2" $ do@@ -1277,7 +1314,7 @@               }              }             |]-          (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [(Cex (_, ctr))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           assertEqual "Must be 10" 10 $ getVar ctr "arg1"           putStrLn "Got 10 Cex, as expected"         ,@@ -1291,9 +1328,9 @@               }              }             |]-          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           let ints = map (flip getVar "arg1") [a,b]-          assertBool "0 must be one of the Cex-es" $ isJust $ elemIndex 0 ints+          assertBool "0 must be one of the Cex-es" $ isJust $ Data.List.elemIndex 0 ints           putStrLn "expected 2 counterexamples found, one Cex is the 0 value"         ,         testCase "assert-fail-notequal" $ do@@ -1306,7 +1343,7 @@               }              }             |]-          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex (_, a), Cex (_, b)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           let x = getVar a "arg1"           let y = getVar b "arg1"           assertBool "At least one has to be 0, to go through the first assert" (x == 0 || y == 0)@@ -1322,7 +1359,7 @@               }              }             |]-          (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex _, Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn "expected 2 counterexamples found"         ,         testCase "assert-2nd-arg" $ do@@ -1334,7 +1371,7 @@               }              }             |]-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("fun(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "fun(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           assertEqual "Must be 666" 666 $ getVar ctr "arg2"           putStrLn "Found arg2 Ctx to be 666"         ,@@ -1351,7 +1388,7 @@               }             }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         -- We zero out everything but the LSB byte. However, byte(31,x) takes the LSB byte@@ -1368,7 +1405,7 @@               }             }             |]-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           assertBool "last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff) > 0           putStrLn "Expected counterexample found"         ,@@ -1386,7 +1423,7 @@               }             }             |]-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           assertBool "second to last byte must be non-zero" $ ((Data.Bits..&.) (getVar ctr "arg1") 0xff00) > 0           putStrLn "Expected counterexample found"         ,@@ -1405,7 +1442,7 @@               }             }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         -- Bitwise OR operation test@@ -1421,7 +1458,7 @@               }             }             |]-          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn "When OR-ing with full 1's we should get back full 1's"         ,         -- Bitwise OR operation test@@ -1438,7 +1475,7 @@               }             }             |]-          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn "When OR-ing with a byte of 1's, we should get 1's back there"         ,         testCase "Deposit contract loop (z3)" $ do@@ -1460,7 +1497,7 @@               }              }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "deposit(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "Deposit-contract-loop-error-version" $ do@@ -1482,7 +1519,7 @@               }              }             |]-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) [] defaultVeriOpts+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s allPanicCodes c (Just (Sig "deposit(uint8)" [AbiUIntType 8])) [] defaultVeriOpts           assertEqual "Must be 255" 255 $ getVar ctr "arg1"           putStrLn  $ "expected counterexample found, and it's correct: " <> (show $ getVar ctr "arg1")         ,@@ -1544,7 +1581,7 @@               }             }             |]-          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("foo(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "foo(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn "div/mod/sdiv/smod by zero works as expected during constant propagation"         ,         testCase "check-asm-byte-oob" $ do@@ -1571,7 +1608,7 @@               }             }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "injectivity of keccak all pairs (32 bytes)" $ do@@ -1589,7 +1626,7 @@               }             }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "injectivity of keccak contrapositive (32 bytes)" $ do@@ -1602,7 +1639,7 @@               }             }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "injectivity of keccak (64 bytes)" $ do@@ -1614,7 +1651,7 @@               }             }             |]-          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) [] defaultVeriOpts+          (_, [Cex (_, ctr)]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256,uint256,uint256)" (replicate 4 (AbiUIntType 256)))) [] defaultVeriOpts           let x = getVar ctr "arg1"           let y = getVar ctr "arg2"           let w = getVar ctr "arg3"@@ -1623,7 +1660,7 @@           assertEqual "w==z for hash collision" w z           putStrLn "expected counterexample found"         ,-        expectFail $ testCase "calldata beyond calldatasize is 0 (z3)" $ do+        testCase "calldata beyond calldatasize is 0 (symbolic calldata)" $ do           Just c <- solcRuntime "A"             [i|             contract A {@@ -1640,6 +1677,43 @@           (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,+        testCase "calldata beyond calldatasize is 0 (concrete dalldata prefix)" $ do+          Just c <- solcRuntime "A"+            [i|+            contract A {+              function f(uint256 z) public pure {+                uint y;+                assembly {+                  let x := calldatasize()+                  y := calldataload(x)+                }+                assert(y == 0);+              }+            }+            |]+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts+          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"+        ,+        testCase "calldata symbolic access" $ do+          Just c <- solcRuntime "A"+            [i|+            contract A {+              function f(uint256 z) public pure {+                uint x; uint y;+                assembly {+                  y := calldatasize()+                }+                require(z >= y);+                assembly {+                  x := calldataload(z)+                }+                assert(x == 0);+              }+            }+            |]+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts+          putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"+        ,         testCase "keccak soundness" $ do           Just c <- solcRuntime "C"             [i|@@ -1653,7 +1727,7 @@             |]            -- should find a counterexample-          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn "expected counterexample found"         ,         testCase "multiple-contracts" $ do@@ -1676,10 +1750,10 @@           Just c <- solcRuntime "C" code'           Just a <- solcRuntime "A" code'           (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> do-            let vm0 = abstractVM (Just ("call_A()", [])) [] c Nothing SymbolicS+            let vm0 = abstractVM (mkCalldata (Just (Sig "call_A()" [])) []) c Nothing SymbolicS             let vm = vm0                   & set (state . callvalue) (Lit 0)-                  & over (env . contracts)+                  & over (EVM.env . contracts)                        (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a))))             verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes) @@ -1713,7 +1787,7 @@                 uint public x;               }             |]-          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("call_A()", [])) [] defaultVeriOpts+          (_, [Cex _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "call_A()" [])) [] defaultVeriOpts           putStrLn "expected counterexample found"         ,         testCase "keccak concrete and sym agree" $ do@@ -1727,7 +1801,7 @@                 }               }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("kecc(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "kecc(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         testCase "keccak concrete and sym injectivity" $ do@@ -1739,12 +1813,12 @@                 }               }             |]-          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("f(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (res, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           putStrLn $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"         ,         ignoreTest $ testCase "safemath distributivity (yul)" $ do           let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"-          let vm =  abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity Nothing SymbolicS+          let vm =  abstractVM (mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) []) yulsafeDistributivity Nothing SymbolicS           (_, [Qed _]) <-  withSolvers Z3 1 Nothing $ \s -> verify s defaultVeriOpts vm (Just $ checkAssertions defaultPanicCodes)           putStrLn "Proven"         ,@@ -1770,7 +1844,7 @@               }             |] -          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts+          (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] defaultVeriOpts           putStrLn "Proven"         ,         testCase "storage-cex-1" $ do@@ -1784,7 +1858,7 @@               }             }             |]-          (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           let addr =  W256 $ num $ createAddress ethrunAddress 1               testCex = Map.size cex.store == 1 &&                         case Map.lookup addr cex.store of@@ -1807,7 +1881,7 @@               }             }             |]-          (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts+          (_, [(Cex (_, cex))]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s [0x01] c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts           let addr = W256 $ num $ createAddress ethrunAddress 1               a = getVar cex "arg1"               testCex = Map.size cex.store == 1 &&@@ -1831,7 +1905,7 @@               }             }             |]-          (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just ("fun(uint256)", [AbiUIntType 256])) [] defaultVeriOpts ConcreteS Nothing (Just $ checkAssertions [0x01])+          (_, [Cex (_, cex)]) <- withSolvers Z3 1 Nothing $ \s -> verifyContract s c (Just (Sig "fun(uint256)" [AbiUIntType 256])) [] defaultVeriOpts ConcreteS Nothing (Just $ checkAssertions [0x01])           let testCex = Map.null cex.store           assertBool "Did not find expected storage cex" testCex           putStrLn "Expected counterexample found"@@ -1860,7 +1934,7 @@           }           |]         withSolvers Z3 3 Nothing $ \s -> do-          a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts Nothing+          a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])           assertBool "Must have a difference" (any isCex a)       ,       testCase "eq-sol-exp-qed" $ do@@ -1885,7 +1959,7 @@               }           |]         withSolvers Z3 3 Nothing $ \s -> do-          a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts Nothing+          a <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing [])           assertEqual "Must have no difference" [Qed ()] a           return ()       ,@@ -1913,7 +1987,7 @@           |]         withSolvers Z3 3 Nothing $ \s -> do           let myVeriOpts = VeriOpts{ simp = True, debug = False, maxIter = Just 2, askSmtIters = Just 2, rpcInfo = Nothing}-          a <- equivalenceCheck s aPrgm bPrgm myVeriOpts Nothing+          a <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing [])           assertEqual "Must be different" (any isCex a) True           return ()       , testCase "eq-all-yul-optimization-tests" $ do@@ -2176,7 +2250,7 @@           Just bPrgm <- yul "" $ T.pack $ unlines filteredBSym           procs <- getNumProcessors           withSolvers CVC5 (num procs) (Just 100) $ \s -> do-            res <- equivalenceCheck s aPrgm bPrgm myVeriOpts Nothing+            res <- equivalenceCheck s aPrgm bPrgm myVeriOpts (mkCalldata Nothing [])             end <- getCurrentTime             case any isCex res of               False -> do@@ -2211,7 +2285,9 @@          Sat _ -> False          Error _ -> False +-- | Takes a runtime code and calls it with the provided calldata +-- | Takes a creation code and some calldata, runs the creation code, and calls the resulting contract with the provided calldata runSimpleVM :: ByteString -> ByteString -> Maybe ByteString runSimpleVM x ins = case loadVM x of                       Nothing -> Nothing@@ -2220,23 +2296,24 @@                             (VMSuccess (ConcreteBuf bs), _) -> Just bs                             _ -> Nothing +-- | Takes a creation code and returns a vm with the result of executing the creation code loadVM :: ByteString -> Maybe VM loadVM x =     case runState exec (vmForEthrunCreation x) of        (VMSuccess (ConcreteBuf targetCode), vm1) -> do-         let target = view (state . contract) vm1+         let target = Control.Lens.view (state . contract) vm1              vm2 = execState (replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode targetCode))) vm1          return $ snd $ flip runState vm2                 (do resetState-                    assign (state . gas) 0xffffffffffffffff -- kludge+                    assign (state . EVM.gas) 0xffffffffffffffff -- kludge                     loadContract target)        _ -> Nothing  hex :: ByteString -> ByteString hex s =-  case Hex.decode s of+  case BS16.decodeBase16 s of     Right x -> x-    Left e -> error e+    Left e -> error $ T.unpack e  singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s =@@ -2283,7 +2360,7 @@  getStaticAbiArgs :: Int -> VM -> [Expr EWord] getStaticAbiArgs n vm =-  let cd = view (state . calldata) vm+  let cd = Control.Lens.view (state . calldata) vm   in decodeStaticArgs 4 n cd  -- includes shaving off 4 byte function sig@@ -2378,13 +2455,13 @@  genEnd :: Int -> Gen (Expr End) genEnd 0 = oneof- [ pure $ Failure [] Invalid+ [ pure $ Failure [] EVM.Types.Invalid  , pure $ Failure [] EVM.Types.IllegalOverflow- , pure $ Failure [] SelfDestruct+ , pure $ Failure [] EVM.Types.SelfDestruct  ] genEnd sz = oneof  [ fmap (EVM.Types.Revert []) subBuf- , liftM3 Return (return []) subBuf subStore+ , liftM3 EVM.Types.Return (return []) subBuf subStore  , liftM3 ITE subWord subEnd subEnd  ]  where