hevm 0.54.2 → 0.55.1

raw patch · 30 files changed

+9757/−6314 lines, 30 filesdep +hspecdep +optparse-applicativedep +utf8-stringdep −with-utf8dep ~aesondep ~basedep ~bytestringPVP ok

version bump matches the API change (PVP)

Dependencies added: hspec, optparse-applicative, utf8-string

Dependencies removed: with-utf8

Dependency ranges changed: aeson, base, bytestring, directory, extra, filepath, githash, here, mtl, process, split, text

API changes (from Hackage documentation)

Files

• CHANGELOG.md +139/−0
• bench/bench-perf.hs +345/−0
• bench/bench.hs +1/−4
• cli/cli.hs +468/−329
• hevm.cabal +63/−10
• src/EVM.hs +375/−263
• src/EVM/ABI.hs +2/−1
• src/EVM/Dapp.hs +15/−20
• src/EVM/Effects.hs +12/−0
• src/EVM/Exec.hs +8/−7
• src/EVM/Expr.hs +387/−159
• src/EVM/Fetch.hs +44/−17
• src/EVM/Format.hs +45/−24
• src/EVM/Fuzz.hs +3/−3
• src/EVM/Keccak.hs +19/−14
• src/EVM/SMT.hs +101/−114
• src/EVM/Solidity.hs +71/−55
• src/EVM/Solvers.hs +200/−81
• src/EVM/Stepper.hs +18/−24
• src/EVM/SymExec.hs +484/−310
• src/EVM/Traversals.hs +2/−2
• src/EVM/Types.hs +223/−82
• src/EVM/UnitTest.hs +125/−103
• test/EVM/Test/BlockchainTests.hs +10/−5
• test/EVM/Test/Tracing.hs +60/−70
• test/EVM/Test/Utils.hs +8/−11
• test/clitest.hs +168/−0
• test/rpc.hs +8/−8
• test/scripts/convert_trace_to_json.sh +2/−1
• test/test.hs +6351/−4597

@@ -5,6 +5,145 @@ 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). +## Added+- When a staticcall is made to a contract that does not exist, we overapproximate+  and return symbolic values+- More simplification rules for Props+- JoinBytes simplification rule+- New simplification rule to help deal with abi.encodeWithSelector+- More simplification rules for Props+- Using the SMT solver to get a single concrete value for a symbolic expression+  and continue running, whenever possible+- STATICCALL abstraction is now performed in case of symbolic arguments+- Better error messages for JSON parsing+- Multiple solutions are allowed for a single symbolic expression, and they are+  generated via iterative calls to the SMT solver for quicker solving+- Aliasing works much better for symbolic and concrete addresses+- Constant propagation for symbolic values+- Allow reading bytecode via --code-file or --code-a-file/--code-b-file. Strips+  `\n`, spaces, and ignores leading `0x` to make it easier to use via e.g.+  `jq '.deplayedBytecode.object file.json > file.txt'` to parse Forge JSON output+  This alleviates the issue when the contract is large and does not fit the command line+  limit of 8192 characters+- Two more simplification rules: `ReadByte` & `ReadWord` when the `CopySlice`+  it is reading from is writing after the position being read, so the+  `CopySlice` can be ignored+- More simplification rules that help avoid symbolic copyslice in case of+  STATICCALL overapproximation+- Test to make sure we don't accidentally overapproximate a working, good STATICCALL+- Allow EXTCODESIZE/HASH, BALANCE to be abstracted to a symbolic value.+- Allow CALL to be extracted in case `--promise-no-reent` is given, promising+  no reentrancy of contracts. This may skip over reentrancy vulnerabilities+  but allows much more thorough exploration of the contract+- Allow controlling the max buffer sizes via --max-buf-size to something smaller than 2**64+  so we don't get too large buffers as counterexamples+- More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing+  CodeHash SMT representation+- Add deployment code flag to the `equivalenceCheck` function+- PNeg + PGT/PGEq/PLeq/PLT simplification rules+- We no longer dispatch Props to SMT that can be solved by a simplification+- Allow user to change the verbosity level via `--verb`. For the moment, this is only to+  print some warnings related to zero-address dereference and to print `hemv test`'s+  output in case of failure+- Simple test cases for the CLI+- Allow limiting the branch depth and width limitation via --max-depth and --max-width+- When there are zero solutions to a multi-solution query it means that the+  currently executed branch is in fact impossible. In these cases, unwind all+  frames and return a Revert with empty returndata.+- More rewrite rules for PEq, PNeg, missing eqByte call, and distributivity for And+- Allow changing of the prefix from "prove" via --prefix in `test` mode+- More complete simplification during interpretation+- SMT-based resolving of addresses now works for delegatecall and staticcall+  opcodes as well+- UNSAT cache is now in `Solvers.hs` and is therefore shared across all threads.+  Hence, it is now active even during branch queries.+- Rewrite rule to deal with some forms of argument packing by Solidity+  via masking+- More rewrite rules for (PLT (Lit 0) _) and (PEq (Lit 1) _)+- Simplification can now be turned off from the cli via --no-simplify+- When doing Keccak concretization, and simplification is enabled,+  we do both until fixedpoint+- When gathering Keccak axioms, we simplify the bytestring that+  the keccak is applied to+- More rewrite rules for MulMod, AddMod, SHL, SHR, SLT, and SignExtend+- PLEq is now concretized in case it can be computed+- More SignExtend test cases+- Rewrite rules to deal with specific exponentiation patterns+- Added missing simplification and concretization of the SAR instruction++## Fixed+- We now try to simplify expressions fully before trying to cast them to a concrete value+  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was+  unnecessarily output+- Not all testcases ran due to incorrect filtering, fixed+- Removed dead code related to IOAct in the now deprecated and removed debugger+- Base case of exponentiation to 0 was not handled, leading to infinite loop+- Better exponential simplification+- Dumping of END states (.prop) files is now default for `--debug`+- When cheatcode is missing, we produce a partial execution warning+- Size of calldata can be up to 2**64, not 256. This is now reflected in the documentation+- We now have less noise during test runs, and assert more about symbolic copyslice tests+- CopySlice rewrite rule is now less strict while still being sound+- Assumptions about reading from buffer after its size are now the same in all cases.+  Previously, they were too weak in case of reading 32 bytes.+- The equivalence checker now is able to prove that an empty store is+  equivalent to a store with all slots initialized to 0.+- Equivalence checking was incorrectly assuming that overapproximated values+  were sequentially equivalent. We now distinguish these symbolic values with+  `A-` and `B-`+- Buffer of all zeroes was interpreted as an empty buffer during parsing SMT model.+  The length of the buffer is now properly taken into account.+- It was possible to enter an infinite recursion when trying to shrink a buffer found by+  the SMT solver. We now properly detect that it is not possible to shrink the buffer.+- Pretty printing of buffers is now more robust. Instead of throwing an `internal error`,+  we now try best to print everything we can, and print an appropriate error message+  instead of crashing.+- We no longer produce duplicate SMT assertions regarding concrete keccak values.+- Ord is now correctly implemented for Prop.+- Signed and unsigned integers have more refined ranges.+- Symbolic interpretation of assertGe/Gt/Le/Lt over signed integers now works correctly.+- SignExtend is now correctly being constant-folded+- Some of our property-based testing was ineffective because of inadvertent+  simplification  happening before calling the SMT solver. This has now been fixed.+- When pranking an address, we used the non-pranked address' nonce+  to calculate the new address. This was incorrect, and lead to address clash,+  as the nonce was never incremented.+- We only report FAIL in `test` mode for assertion failures that match the+  string prefix "assertion failed", or match function selector Panic(uint256)+  with a parameter 0x1. Previously, `require(a==b, "reason")` was a cause for+  FAIL in case a!=b was possible. This has now been fixed.+- Out of bounds reads could occur in Haskell when trying to determine+  valid jump destinations. This has now been fixed.++## Changed+- Warnings now lead printing FAIL. This way, users don't accidentally think that+  their contract is correct when there were cases/branches that hevm could not+  fully explore. Printing of issues is also now much more organized+- Expressions that are commutative are now canonicalized to have the smaller+  value on the LHS. This can significantly help with simplifications, automatically+  determining when (Eq a b) is true when a==b modulo commutativity+- `hevm test`'s flag ` --verbose` is now `--verb`, which also increases verbosity+  for other elements of the system+- Add `--arrays-exp` to cvc5 options.+- We now use Options.Applicative and a rather different way of parsing CLI options.+  This should give us much better control over the CLI options and their parsing.+- block.number can now be symbolic. This only affects library use of hevm+- Removed `--smtoutput` since it was never used+- We now build with -DCMAKE_POLICY_VERSION_MINIMUM=3.5 libff, as cmake deprecated 3.5+- CheckSatResult has now been unified with ProofResult via SMTResult+- If counterexample would require a buffer that's larger than 1GB, we abandon+  shrinking it.+- If solver is not able to solve a query while attempting to shrink the model, we+  abandon the attempt gracefully instead of crashing with internal error.+- Buffers are now handled more lazily when inspecting a model, which avoids some+  unnecesary internal errors.+- EVM memory is now grown on demand using a 2x factor, to avoid repeated smaller+  increases which hurt concrete execution performance due to their linear cost.+- The concrete MCOPY implementation has been optimized to avoid freezing the whole+  EVM memory.+- We no longer accept `check` as a prefix for test cases by default.+- The way we print warnings for `symbolic` mode now matches that of `test` mode.+ ## [0.54.2] - 2024-12-12  ## Fixed

@@ -0,0 +1,345 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}++module Main where++import Control.Monad.State.Strict (liftIO)+import Data.ByteString.UTF8 as BSU +import Data.Either+import Data.Function+import Data.Maybe+import Data.String.Here+import EVM+import EVM.ABI+import EVM.Effects (App, runApp)+import EVM.Fetch qualified as Fetch+import EVM.Solidity+import EVM.Stepper qualified as Stepper+import EVM.Transaction qualified+import EVM.Types+import EVM.UnitTest+import Test.Tasty.Bench+import Control.Monad.ST+import EVM.FeeSchedule (feeSchedule)++-- benchmark hevm using tasty-bench++vmFromRawByteString :: App m => ByteString -> m (VM Concrete RealWorld)+vmFromRawByteString bs = liftIO $+  bs+    & ConcreteRuntimeCode+    & RuntimeCode+    & initialContract+    & vm0+    & stToIO+    & fmap EVM.Transaction.initTx++vm0 :: Contract -> ST s (VM Concrete s)+vm0 c = makeVm $ vm0Opts c++vm0Opts :: Contract -> VMOpts Concrete+vm0Opts c =+  VMOpts+    { contract = c,+      calldata = (ConcreteBuf "", []),+      value = Lit 0xfffffffffffff, -- balance+      baseState = EmptyBase,+      address = LitAddr 0xacab,+      caller = LitAddr 0,+      origin = LitAddr 0,+      gas = 0xffffffffffffffff,+      baseFee = 0,+      priorityFee = 0,+      gaslimit = 0xffffffffffffffff,+      coinbase = LitAddr 0,+      number = Lit 0,+      timestamp = Lit 0,+      blockGaslimit = 0xffffffffffffffff,+      gasprice = 0,+      maxCodeSize = 0xffffffff,+      prevRandao = 0,+      schedule = feeSchedule,+      chainId = 1,+      create = False,+      txAccessList = mempty, -- TODO: support me soon+      allowFFI = False,+      otherContracts = [],+      freshAddresses = 0,+      beaconRoot = 0+    }++vmOptsToTestVMParams :: VMOpts Concrete -> TestVMParams+vmOptsToTestVMParams v =+  TestVMParams+    { address = v.address,+      caller = v.caller,+      origin = v.origin,+      gasCreate = v.gas,+      gasCall = v.gas,+      baseFee = v.baseFee,+      priorityFee = v.priorityFee,+      balanceCreate = case v.value of+        Lit x -> x+        _ -> 0,+      coinbase = v.coinbase,+      number = case v.number of+        Lit x -> x+        _ -> 0,+      timestamp = case v.timestamp of+        Lit x -> x+        _ -> 0,+      gaslimit = v.gaslimit,+      gasprice = v.gasprice,+      maxCodeSize = v.maxCodeSize,+      prevrandao = v.prevRandao,+      chainId = v.chainId+    }++callMainForBytecode :: App m => ByteString -> m (Either EvmError (Expr 'Buf))+callMainForBytecode bs = do+  vm <- vmFromRawByteString bs+  Stepper.interpret (Fetch.zero 0 Nothing) vm (Stepper.evm (abiCall (vmOptsToTestVMParams (vm0Opts (initialContract (RuntimeCode (ConcreteRuntimeCode bs))))) (Left ("main()", emptyAbi))) >> Stepper.execFully)++benchMain :: (String, ByteString) -> Benchmark+benchMain (name, bs) = bench name $ nfIO $ runApp $ (\x -> if isRight x then () else internalError "failed") <$> callMainForBytecode bs++mkBench :: (Int -> IO a) -> [Int] -> IO [(String, a)]+mkBench f l = mapM (\n -> (show n,) <$> f n) l++main :: IO ()+main = do+  let f (name, prog, limit) = do+        ll <- mkBench prog [2 ^ n | n :: Int <- [1 .. fromMaybe 14 limit]]+        pure $ bgroup name (benchMain <$> ll)+  let benchmarks = [ +                     ("loop", simpleLoop, Nothing)+                   , ("primes", primes, Nothing)+                   , ("hashes", hashes, Nothing)+                   , ("hashmem", hashmem, Nothing)+                   , ("balanceTransfer", balanceTransfer, Nothing)+                   , ("funcCall", funcCall, Nothing)+                   , ("contractCreation", contractCreation, Nothing)+                   , ("contractCreationMem", contractCreationMem, Nothing)+                   , ("arrayCreationMem", arrayCreationMem, Just 9)+                   , ("mapStorage", mapStorage, Nothing)+                   , ("swapOperations", swapOperations, Nothing)+                   ]+  defaultMain =<< mapM f benchmarks+  ++-- Loop that adds up n numbers+simpleLoop :: Int -> IO ByteString+simpleLoop n = do+  let src =+        [i|+          contract A {+            function main() public {+              uint256 acc = 0;+              for (uint i = 0; i < ${n}; i++) {+                acc += i;+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Computes prime numbers and stores them up to n+primes :: Int -> IO ByteString+primes n = do+  let src =+        [i|+          contract A {+            mapping (uint => uint) public primes;+            function isPrime (uint n) public returns (bool) {+              if (n == 2) {+                return true;+              }+              if (n % 2 == 0) {+                return false;+              }+              for (uint i = 3; i * i < n; i += 2) {+                if (n % i == 0) {+                  return false;+                }+              }+              return true;+            }+            +            function main() public {+              uint n = 0;+              for (uint i = 0; i < ${n}; i++) {+                if (isPrime(i)) {+                  primes[n++] = i;+                }+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Program that repeatedly hashes a value+hashes :: Int -> IO ByteString+hashes n = do+  let src =+        [i|+          contract A {+            function main() public {+              bytes32 h = 0;+              for (uint i = 0; i < ${n}; i++) {+                h = keccak256(abi.encode(h));+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Program that repeatedly hashes a value and stores it in a map+hashmem :: Int -> IO ByteString+hashmem n = do+  let src =+        [i|+          contract A {+            mapping (uint256 => uint256) public map;+            function main() public {+              uint256 h = 0;+              for (uint i = 0; i < ${n}; i++) {+                uint256 x = h;+                h = uint256(keccak256(abi.encode(h)));+                map[x] = h;+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Transfer ETH to an address n times+balanceTransfer :: Int -> IO ByteString+balanceTransfer n = do+  let src =+        [i|+          contract A {+            function main() public {+              address payable to = payable(address(0x8A8eAFb1cf62BfBeb1741769DAE1a9dd47996192)); +              for (uint i = 0; i < ${n}; i++) {+                to.transfer(1);+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Call a public function n times+funcCall :: Int -> IO ByteString+funcCall n = do+  let src =+        [i|+          contract A {+            uint256 public acc;+            function f(uint256 x) public {+              acc += x;+            }+            function main() public {+              for (uint i = 0; i < ${n}; i++) {+                f(i);+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Creates n contracts+contractCreation :: Int -> IO ByteString+contractCreation n = do+  let src =+        [i|+          contract B { }+          contract A {+            B public b;+            function main() public {+              for (uint i = 0; i < ${n}; i++) {+                b = new B();+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Create n contracts with a string in them+contractCreationMem :: Int -> IO ByteString+contractCreationMem n = do+  let src =+        [i|+          contract B { string m = "the quick brown fox jumps over the lazy dog"; }+          contract A {+            B public b;+            function main() public {+              for (uint i = 0; i < ${n}; i++) {+                b = new B();+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Create large array in memory+arrayCreationMem :: Int -> IO ByteString+arrayCreationMem n = do+  let src =+        [i|+          struct C { int24 a; int24 b; uint256 c; uint128 d; }+          contract A {+            function work() public returns (C[] memory ret) {+                ret = new C[](${n});+                for(uint a = 0; a < ${n}; a++) {+                    ret[a] = C({a:1, b:1, c:0xffffffffffffff, d:5});+                }+                return ret;+            }+            function main() public {+              for (uint i = 0; i < ${n}; i++) {+                C[] memory ret = work();+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Create large map in storage+mapStorage :: Int -> IO ByteString+mapStorage n = do+  let src =+        [i|+          struct C { uint256 a; uint256 b; }+          contract A {+            mapping(uint256 => mapping(uint256 => C)) m;+            function main() public {+              for (uint i = 0; i < ${n}; i++) {+                m[i][${n}-i] = C(i, ${n});+              }+            }+          }+        |]+  fmap fromJust (runApp $ solcRuntime "A" src)++-- Do many swaps+swapOperations :: Int -> IO ByteString+swapOperations n = do+  let src =+        [i|+          contract A {+            function main() public pure {+                (uint a0, uint a1, uint a2, uint a3, uint a4, uint a5, uint a6, uint a7, uint a8, uint a9, uint a10, uint a11, uint a12, uint a13, uint a14, uint a15) = (1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16);+                for (uint i = 0; i < ${n}; i++) {+                    (a0, a15) = (a15, a0);+                    (a1, a14) = (a14, a1);+                    (a2, a13) = (a13, a2);+                    (a3, a12) = (a12, a3);+                    (a4, a11) = (a11, a4);+                    (a5, a10) = (a10, a5);+                    (a6, a9) = (a9, a6);+                    (a7, a8) = (a8, a7);+                }+            }+        }+        |]+  fmap fromJust (runApp $ solcRuntime' "A" src True)

@@ -92,10 +92,7 @@ findPanics :: App m => Solver -> Natural -> Integer -> ByteString -> m () findPanics solver count iters c = do   _ <- withSolvers solver count 1 Nothing $ \s -> do-    let opts = defaultVeriOpts-          { maxIter = Just iters-          , askSmtIters = iters + 1-          }+    let opts = defaultVeriOpts { iterConf = defaultIterConf {maxIter = Just iters, askSmtIters = iters + 1 }}     checkAssert s allPanicCodes c Nothing [] opts   liftIO $ putStrLn "done" 

@@ -3,16 +3,20 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE OverloadedStrings #-}  module Main where  import Control.Monad (when, forM_, unless) import Control.Monad.ST (RealWorld, stToIO) import Control.Monad.IO.Unlift+import Control.Exception (try, IOException) import Data.ByteString (ByteString)+import qualified Data.ByteString.Lazy as BS+import qualified Data.ByteString.Char8 as BC import Data.DoubleWord (Word256)-import Data.List (intersperse)-import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing)+import Data.List (intersperse, intercalate)+import Data.Maybe (fromMaybe, mapMaybe, fromJust, isNothing, isJust) import Data.Text qualified as T import Data.Text.IO qualified as T import Data.Version (showVersion)@@ -21,12 +25,14 @@ import Numeric.Natural (Natural) import Optics.Core ((&), set) import Witch (unsafeInto)-import Options.Generic as Options+import Options.Generic as OptionsGeneric+import Options.Applicative as Options import Paths_hevm qualified as Paths import System.Directory (withCurrentDirectory, getCurrentDirectory, doesDirectoryExist, makeAbsolute) import System.FilePath ((</>)) import System.Exit (exitFailure, exitWith, ExitCode(..))-import Main.Utf8 (withUtf8)+import Data.List.Split (splitOn)+import Text.Read (readMaybe)  import EVM (initialContract, abstractContract, makeVm) import EVM.ABI (Sig(..))@@ -46,155 +52,243 @@ import EVM.Types qualified import EVM.UnitTest import EVM.Effects+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)  data AssertionType = DSTest | Forge-  deriving (Eq, Show, Read, ParseField)+  deriving (Eq, Show, Read) --- This record defines the program's command-line options--- automatically via the `optparse-generic` package.-data Command w-  = Symbolic -- Symbolically explore an abstract program, or specialized with specified env & calldata-  -- vm opts-      { code          :: w ::: Maybe ByteString <?> "Program bytecode"-      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"-      , address       :: w ::: Maybe Addr       <?> "Tx: address"-      , caller        :: w ::: Maybe Addr       <?> "Tx: caller"-      , origin        :: w ::: Maybe Addr       <?> "Tx: origin"-      , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"-      , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"-      , nonce         :: w ::: Maybe Word64     <?> "Nonce of origin"-      , gas           :: w ::: Maybe Word64     <?> "Tx: gas amount"-      , number        :: w ::: Maybe W256       <?> "Block: number"-      , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"-      , basefee       :: w ::: Maybe W256       <?> "Block: base fee"-      , priorityFee   :: w ::: Maybe W256       <?> "Tx: priority fee"-      , gaslimit      :: w ::: Maybe Word64     <?> "Tx: gas limit"-      , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"-      , create        :: w ::: Bool             <?> "Tx: creation"-      , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"-      , prevRandao    :: w ::: Maybe W256       <?> "Block: prevRandao"-      , chainid       :: w ::: Maybe W256       <?> "Env: chainId"-  -- remote state opts-      , rpc           :: w ::: Maybe URL        <?> "Fetch state from a remote node"-      , block         :: w ::: Maybe W256       <?> "Block state is be fetched from"+projectTypeParser :: Parser ProjectType+projectTypeParser = option auto (long "project-type" <> showDefault <> value Foundry <> help "Is this a CombinedJSON or Foundry project") -  -- symbolic execution opts-      , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"-      , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"-      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"-      , arg           :: w ::: [String]           <?> "Values to encode"-      , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"-      , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"-      , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"-      , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"-      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"-      , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"-      , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour, and dump internal expressions"-      , trace         :: w ::: Bool               <?> "Dump trace"-      , assertions    :: w ::: Maybe [Word256]    <?> "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)"-      , askSmtIterations :: w ::: Integer         <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      , numCexFuzz    :: w ::: Integer            <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"-      , numSolvers    :: w ::: Maybe Natural      <?> "Number of solver instances to use (default: number of cpu cores)"-      , solverThreads :: w ::: Maybe Natural      <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      , noDecompose   :: w ::: Bool               <?> "Don't decompose storage slots into separate arrays"-      }-  | Equivalence -- prove equivalence between two programs-      { codeA         :: w ::: ByteString       <?> "Bytecode of the first program"-      , codeB         :: w ::: ByteString       <?> "Bytecode of the second program"-      , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"-      , arg           :: w ::: [String]         <?> "Values to encode"-      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"-      , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"-      , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"-      , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"-      , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"-      , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour, and dump internal expressions"-      , trace         :: w ::: Bool             <?> "Dump trace"-      , askSmtIterations :: w ::: Integer       <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      , numCexFuzz    :: w ::: Integer          <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"-      , numSolvers    :: w ::: Maybe Natural    <?> "Number of solver instances to use (default: number of cpu cores)"-      , solverThreads :: w ::: Maybe Natural    <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"-      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      , noDecompose   :: w ::: Bool             <?> "Don't decompose storage slots into separate arrays"-      }-  | Exec -- Execute a given program with specified env & calldata-      { code        :: w ::: Maybe ByteString  <?> "Program bytecode"-      , calldata    :: w ::: Maybe ByteString  <?> "Tx: calldata"-      , address     :: w ::: Maybe Addr        <?> "Tx: address"-      , caller      :: w ::: Maybe Addr        <?> "Tx: caller"-      , origin      :: w ::: Maybe Addr        <?> "Tx: origin"-      , coinbase    :: w ::: Maybe Addr        <?> "Block: coinbase"-      , value       :: w ::: Maybe W256        <?> "Tx: Eth amount"-      , nonce       :: w ::: Maybe Word64      <?> "Nonce of origin"-      , gas         :: w ::: Maybe Word64      <?> "Tx: gas amount"-      , number      :: w ::: Maybe W256        <?> "Block: number"-      , timestamp   :: w ::: Maybe W256        <?> "Block: timestamp"-      , basefee     :: w ::: Maybe W256        <?> "Block: base fee"-      , priorityFee :: w ::: Maybe W256        <?> "Tx: priority fee"-      , gaslimit    :: w ::: Maybe Word64      <?> "Tx: gas limit"-      , gasprice    :: w ::: Maybe W256        <?> "Tx: gas price"-      , create      :: w ::: Bool              <?> "Tx: creation"-      , maxcodesize :: w ::: Maybe W256        <?> "Block: max code size"-      , prevRandao  :: w ::: Maybe W256        <?> "Block: prevRandao"-      , chainid     :: w ::: Maybe W256        <?> "Env: chainId"-      , debug         :: w ::: Bool            <?> "Debug printing of internal behaviour, and dump internal expressions"-      , trace       :: w ::: Bool              <?> "Dump trace"-      , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"-      , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"-      , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"-      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"-      }-  | Test -- Run Foundry unit tests-      { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"-      , assertionType :: w ::: Maybe AssertionType <?> "Assertions as per Forge or DSTest (default: Forge)"-      , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"-      , number        :: w ::: Maybe W256               <?> "Block: number"-      , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"-      , coverage      :: w ::: Bool                     <?> "Coverage analysis"-      , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"-      , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"-      , solverThreads :: w ::: Maybe Natural            <?> "Number of threads for each solver instance. Only respected for Z3 (default: 1)"-      , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"-      , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour, and dump internal expressions"-      , trace         :: w ::: Bool                     <?> "Dump trace"-      , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"-      , smttimeout    :: w ::: Maybe Natural            <?> "Timeout given to SMT solver in seconds (default: 300)"-      , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point. For no bound, set -1 (default: 5)"-      , loopDetectionHeuristic :: w ::: LoopHeuristic   <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"-      , noDecompose   :: w ::: Bool                     <?> "Don't decompose storage slots into separate arrays"-      , numCexFuzz    :: w ::: Integer                  <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"-      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"-      }-  | Version+sigParser :: Parser (Maybe Text)+sigParser = (optional $ strOption $ long "sig" <> help "Signature of types to decode/encode") -  deriving (Options.Generic)+argParser :: Parser [String]+argParser = (many $ strOption $ long "arg" <> help "Value(s) to encode. Can be given multiple times, once for each argument") -type URL = Text+createParser :: Parser Bool+createParser = switch $ long "create" <> help "Tx: creation" +rpcParser :: Parser (Maybe URL)+rpcParser = (optional $ strOption $ long "rpc" <> help "Fetch state from a remote node") --- For some reason haskell can't derive a--- parseField instance for (Text, ByteString)-instance Options.ParseField (Text, ByteString)+data CommonOptions = CommonOptions+  { askSmtIterations ::Integer+  , loopDetectionHeuristic ::LoopHeuristic+  , noDecompose   ::Bool+  , solver        ::Text+  , debug         ::Bool+  , calldata      ::Maybe ByteString+  , trace         ::Bool+  , verb          ::Int+  , root          ::Maybe String+  , assertionType ::AssertionType+  , solverThreads ::Natural+  , smttimeout    ::Natural+  , smtdebug      ::Bool+  , numSolvers    ::Maybe Natural+  , numCexFuzz    ::Integer+  , maxIterations ::Integer+  , promiseNoReent::Bool+  , maxBufSize    ::Int+  , maxWidth      ::Int+  , maxDepth      ::Maybe Int+  , noSimplify    ::Bool+  } -deriving instance Options.ParseField Word256-deriving instance Options.ParseField [Word256]+commonOptions :: Parser CommonOptions+commonOptions = CommonOptions+  <$> option auto ( long "ask-smt-iterations" <> value 1 <>+    help "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability")+  <*> option auto (long "loop-detection-heuristic" <> showDefault <> value StackBased <>+    help "Which heuristic should be used to determine if we are in a loop: StackBased or Naive")+  <*> (switch $ long "no-decompose"         <> help "Don't decompose storage slots into separate arrays")+  <*> (strOption $ long "solver"            <> value "z3" <> help "Used SMT solver: z3, cvc5, or bitwuzla")+  <*> (switch $ long "debug"                <> help "Debug printing of internal behaviour, and dump internal expressions")+  <*> (optional $ strOption $ long "calldata" <> help "Tx: calldata")+  <*> (switch $ long "trace"                <> help "Dump trace")+  <*> (option auto $ long "verb"            <> showDefault <> value 1 <> help "Append call trace: {1} failures {2} all")+  <*> (optional $ strOption $ long "root"   <> help "Path to  project root directory")+  <*> (option auto $ long "assertion-type"  <> showDefault <> value Forge <> help "Assertions as per Forge or DSTest")+  <*> (option auto $ long "solver-threads"  <> showDefault <> value 1 <> help "Number of threads for each solver instance. Only respected for Z3")+  <*> (option auto $ long "smttimeout"      <> value 300 <> help "Timeout given to SMT solver in seconds")+  <*> (switch $ long "smtdebug"             <> help "Print smt queries sent to the solver")+  <*> (optional $ option auto $ long "num-solvers" <> help "Number of solver instances to use (default: number of cpu cores)")+  <*> (option auto $ long "num-cex-fuzz"    <> showDefault <> value 3 <> help "Number of fuzzing tries to do to generate a counterexample")+  <*> (option auto $ long "max-iterations"  <> showDefault <> value 5 <> help "Number of times we may revisit a particular branching point. For no bound, set -1")+  <*> (switch $ long "promise-no-reent"     <> help "Promise no reentrancy is possible into the contract(s) being examined")+  <*> (option auto $ long "max-buf-size"    <> value 64 <> help "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)")+  <*> (option auto $ long "max-width"      <> showDefault <> value 100 <> help "Max number of concrete values to explore when encountering a symbolic value. This is a form of branch width limitation per symbolic value")+  <*> (optional $ option auto $ long "max-depth" <> help "Limit maximum depth of branching during exploration (default: unlimited)")+  <*> (switch $ long "no-simplify" <> help "Don't perform simplification of expressions") -instance Options.ParseRecord (Command Options.Wrapped) where-  parseRecord =-    Options.parseRecordWithModifiers Options.lispCaseModifiers+data CommonExecOptions = CommonExecOptions+  { address       ::Maybe Addr+  , caller        ::Maybe Addr+  , origin        ::Maybe Addr+  , coinbase      ::Maybe Addr+  , value         ::Maybe W256+  , nonce         ::Maybe Word64+  , gas           ::Maybe Word64+  , number        ::Maybe W256+  , timestamp     ::Maybe W256+  , basefee       ::Maybe W256+  , priorityFee   ::Maybe W256+  , gaslimit      ::Maybe Word64+  , gasprice      ::Maybe W256+  , maxcodesize   ::Maybe W256+  , prevRandao    ::Maybe W256+  , chainid       ::Maybe W256+  , rpc           ::Maybe URL+  , block         ::Maybe W256+} +commonExecOptions :: Parser CommonExecOptions+commonExecOptions = CommonExecOptions+  <$> (optional $ option auto $ long "address"       <> help "Tx: address")+  <*> (optional $ option auto $ long "caller"        <> help "Tx: caller")+  <*> (optional $ option auto $ long "origin"        <> help "Tx: origin")+  <*> (optional $ option auto $ long "coinbase"      <> help "Block: coinbase")+  <*> (optional $ option auto $ long "value"         <> help "Tx: Eth amount")+  <*> (optional $ option auto $ long "nonce"         <> help "Nonce of origin")+  <*> (optional $ option auto $ long "gas"           <> help "Tx: gas amount")+  <*> (optional $ option auto $ long "number"        <> help "Block: number")+  <*> (optional $ option auto $ long "timestamp"     <> help "Block: timestamp")+  <*> (optional $ option auto $ long "basefee"       <> help "Block: base fee")+  <*> (optional $ option auto $ long "priority-fee"  <> help "Tx: priority fee")+  <*> (optional $ option auto $ long "gaslimit"      <> help "Tx: gas limit")+  <*> (optional $ option auto $ long "gasprice"      <> help "Tx: gas price")+  <*> (optional $ option auto $ long "maxcodesize"   <> help "Block: max code size")+  <*> (optional $ option auto $ long "prev-randao"   <> help "Block: prevRandao")+  <*> (optional $ option auto $ long "chainid"       <> help "Env: chainId")+  <*> rpcParser+  <*> (optional $ option auto $ long "block"         <> help "Block state is be fetched from")++data CommonFileOptions = CommonFileOptions+ { code        ::Maybe ByteString+ , codeFile    ::Maybe String+ }++commonFileOptions :: Parser CommonFileOptions+commonFileOptions = CommonFileOptions+  <$> (optional $ strOption $ long "code" <> help "Program bytecode")+  <*> (optional $ strOption $ long "code-file" <> help "Program bytecode in a file")++data TestOptions = TestOptions+  { projectType   ::ProjectType+  , rpc           ::Maybe URL+  , number        ::Maybe W256+  , coverage      ::Bool+  , match         ::Maybe String+  , prefix        ::String+  , ffi           ::Bool+  }++testOptions :: Parser TestOptions+testOptions = TestOptions+  <$> projectTypeParser+  <*> rpcParser+  <*> (optional $ option auto $ long "number" <> help "Block: number")+  <*> (switch $ long "coverage" <> help "Coverage analysis")+  <*> (optional $ strOption $ long "match" <> help "Test case filter - only run methods matching regex")+  <*> (strOption $ long "prefix"  <> showDefault <> value "prove" <> help "Prefix for test cases to prove")+  <*> (switch $ long "ffi" <> help "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)")+++data EqOptions = EqOptions+  { codeA         ::Maybe ByteString+  , codeB         ::Maybe ByteString+  , codeAFile     ::Maybe String+  , codeBFile     ::Maybe String+  , sig           ::Maybe Text+  , arg           ::[String]+  , create        ::Bool+  }++eqOptions :: Parser EqOptions+eqOptions = EqOptions+  <$> (optional $ strOption $ long "code-a"      <> help "Bytecode of the first program")+  <*> (optional $ strOption $ long "code-b"      <> help "Bytecode of the second program")+  <*> (optional $ strOption $ long "code-a-file" <> help "First program's bytecode in a file")+  <*> (optional $ strOption $ long "code-b-file" <> help "Second program's bytecode in a file")+  <*> sigParser+  <*> argParser+  <*> createParser++data SymbolicOptions = SymbolicOptions+  { projectType       ::ProjectType+  , initialStorage    ::Maybe InitialStorage+  , getModels         ::Bool+  , showTree          ::Bool+  , showReachableTree ::Bool+  , assertions        ::Maybe String+  , sig               ::Maybe Text+  , arg               ::[String]+  , create            ::Bool+  }++symbolicOptions :: Parser SymbolicOptions+symbolicOptions = SymbolicOptions+  <$> projectTypeParser+  <*> (optional $ option auto $ long "initial-storage" <> help "Starting state for storage: Empty, Abstract (default Abstract)")+  <*> (switch $ long "get-models" <> help "Print example testcase for each execution path")+  <*> (switch $ long "show-tree" <> help "Print branches explored in tree view")+  <*> (switch $ long "show-reachable-tree" <> showDefault <> help "Print only reachable branches explored in tree view")+  <*> (optional $ strOption $ long "assertions" <> help "Comma separated list of solc panic codes to check for (default: user defined assertion violations only)")+  <*> sigParser+  <*> argParser+  <*> createParser++data ExecOptions = ExecOptions+  { projectType   ::ProjectType+  , create :: Bool+  }+execOptions :: Parser ExecOptions+execOptions = ExecOptions+  <$> projectTypeParser+  <*> createParser++-- Combined options data type+data Command+  = Symbolic   CommonFileOptions SymbolicOptions CommonExecOptions CommonOptions+  | Equal      EqOptions CommonOptions+  | Test       TestOptions  CommonOptions+  | Exec       CommonFileOptions ExecOptions CommonExecOptions CommonOptions+  | Version++-- Parser for the subcommands+commandParser :: Parser Command+commandParser = subparser+  ( command "test"+      (info (Test <$> testOptions <*> commonOptions <**> helper)+        (progDesc "Prove Foundry unit tests prefixed with `prove` by default"+        <> footer "For more help: https://hevm.dev/std-test-tutorial.html" ))+  <> command "equivalence"+      (info (Equal <$> eqOptions <*> commonOptions <**> helper)+        (progDesc "Prove equivalence between two programs"+        <> footer "For more help: https://hevm.dev/equivalence-checking-tutorial.html" ))+  <> command "symbolic"+      (info (Symbolic <$> commonFileOptions <*> symbolicOptions <*> commonExecOptions <*> commonOptions <**> helper)+        (progDesc "Symbolically explore an abstract program"+        <> footer "For more help, see: https://hevm.dev/symbolic-execution-tutorial.html" ))+  <> command "exec"+      (info (Exec <$> commonFileOptions <*> execOptions <*> commonExecOptions <*> commonOptions <**> helper)+        (progDesc "Concretely execute a given program"+        <> footer "For more help, see https://hevm.dev/exec.html" ))+  <> command "version"+      (info (pure Version)+        (progDesc "Show the version of the tool"))+  )++type URL = Text++deriving instance OptionsGeneric.ParseField Word256+deriving instance OptionsGeneric.ParseField [Word256]+ data InitialStorage   = Empty   | Abstract-  deriving (Show, Read, Options.ParseField)+  deriving (Show, Read, OptionsGeneric.ParseField)  getFullVersion :: [Char] getFullVersion = showVersion Paths.version <> " [" <> gitVersion <> "]"@@ -205,165 +299,219 @@       Left _ -> "no git revision present"  main :: IO ()-main = withUtf8 $ do-  cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"-  let env = Env { config = defaultConfig-    { dumpQueries = cmd.smtdebug-    , debug = cmd.debug-    , dumpExprs = cmd.debug-    , numCexFuzz = cmd.numCexFuzz-    , dumpTrace = cmd.trace-    , decomposeStorage = Prelude.not cmd.noDecompose-    } }+main = do+  cmd <- execParser $ info (commandParser <**> helper)+    ( Options.fullDesc+    <> progDesc "hevm, a symbolic and concrete EVM bytecode execution framework"+    <> footer "See https://hevm.dev for more information"+    )+   case cmd of-    Version {} ->putStrLn getFullVersion-    Symbolic {} -> do-      root <- getRoot cmd-      withCurrentDirectory root $ runEnv env $ assert cmd-    Equivalence {} -> runEnv env $ equivalence cmd-    Exec {} -> runEnv env $ launchExec cmd-    Test {} -> do-      root <- getRoot cmd-      solver <- getSolver cmd+    Symbolic cFileOpts symbOpts cExecOpts cOpts -> do+      env <- makeEnv cOpts+      root <- getRoot cOpts+      withCurrentDirectory root $ runEnv env $ symbCheck cFileOpts symbOpts cExecOpts cOpts+    Equal eqOpts cOpts -> do+      env <- makeEnv cOpts+      runEnv env $ equivalence eqOpts cOpts+    Test testOpts cOpts -> do+      env <- makeEnv cOpts+      root <- getRoot cOpts+      solver <- getSolver cOpts.solver       cores <- liftIO $ unsafeInto <$> getNumProcessors-      let solverCount = fromMaybe cores cmd.numSolvers-      runEnv env $ withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do-        buildOut <- readBuildOutput root (getProjectType cmd)+      let solverCount = fromMaybe cores cOpts.numSolvers+      runEnv env $ withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do+        buildOut <- readBuildOutput root testOpts.projectType         case buildOut of           Left e -> liftIO $ do             putStrLn $ "Error: " <> e             exitFailure           Right out -> do             -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?-            testOpts <- liftIO $ unitTestOptions cmd solvers (Just out)-            res <- unitTest testOpts out.contracts-            liftIO $ unless res exitFailure+            unitTestOpts <- liftIO $ unitTestOptions testOpts cOpts solvers (Just out)+            res <- unitTest unitTestOpts out.contracts+            liftIO $ unless (uncurry (&&) res) exitFailure+    Exec cFileOpts execOpts cExecOpts cOpts-> do+      env <- makeEnv cOpts+      runEnv env $ launchExec cFileOpts execOpts cExecOpts cOpts+    Version {} ->putStrLn getFullVersion+  where+    makeEnv :: CommonOptions -> IO Env+    makeEnv cOpts = do+      when (cOpts.maxBufSize > 64) $ do+        putStrLn "Error: maxBufSize must be less than or equal to 64. That limits buffers to a size of 2^64, which is more than enough for practical purposes"+        exitFailure+      when (cOpts.maxBufSize < 0) $ do+        putStrLn "Error: maxBufSize must be at least 0. Negative values do not make sense. A value of zero means at most 1 byte long buffers"+        exitFailure+      pure Env { config = defaultConfig+        { dumpQueries = cOpts.smtdebug+        , debug = cOpts.debug+        , dumpEndStates = cOpts.debug+        , dumpExprs = cOpts.debug+        , numCexFuzz = cOpts.numCexFuzz+        , dumpTrace = cOpts.trace+        , decomposeStorage = Prelude.not cOpts.noDecompose+        , promiseNoReent = cOpts.promiseNoReent+        , maxBufSize = cOpts.maxBufSize+        , maxWidth = cOpts.maxWidth+        , maxDepth = cOpts.maxDepth+        , verb = cOpts.verb+        , simp = Prelude.not cOpts.noSimplify+        } } -equivalence :: App m => Command Options.Unwrapped -> m ()-equivalence cmd = do-  let bytecodeA' = hexByteString $ strip0x cmd.codeA-      bytecodeB' = hexByteString $ strip0x cmd.codeB-  if (isNothing bytecodeA') then liftIO $ do-    putStrLn $ "Error, invalid bytecode for program A: " <> show cmd.codeA++getCode :: Maybe String -> Maybe ByteString -> IO (Maybe ByteString)+getCode fname code = do+  when (isJust fname && isJust code) $ do+    putStrLn "Error: Cannot provide both a file and code"     exitFailure-  else if (isNothing bytecodeB') then liftIO $ do-    putStrLn $ "Error, invalid bytecode for program B: " <> show cmd.codeB+  case fname of+    Nothing -> pure $ fmap strip code+    Just f -> do+      result <- try (BS.readFile f) :: IO (Either IOException BS.ByteString)+      case result of+        Left e -> do+          putStrLn $ "Error reading file: " <> show e+          exitFailure+        Right content -> do+          pure $ Just $ strip (BS.toStrict content)+  where+    strip = BC.filter (\c -> c /= ' ' && c /= '\n' && c /= '\r' && c /= '\t' && c /= '"')++equivalence :: App m => EqOptions -> CommonOptions -> m ()+equivalence eqOpts cOpts = do+  bytecodeA' <- liftIO $ getCode eqOpts.codeAFile eqOpts.codeA+  bytecodeB' <- liftIO $ getCode eqOpts.codeBFile eqOpts.codeB+  let bytecodeA = decipher bytecodeA'+  let bytecodeB = decipher bytecodeB'+  when (isNothing bytecodeA) $ liftIO $ do+    putStrLn "Error: invalid or no bytecode for program A. Provide a valid one with --code-a or --code-a-file"     exitFailure-  else do-    let bytecodeA = fromJust bytecodeA'-        bytecodeB = fromJust bytecodeB'-        veriOpts = VeriOpts { simp = True-                            , maxIter = parseMaxIters cmd.maxIterations-                            , askSmtIters = cmd.askSmtIterations-                            , loopHeuristic = cmd.loopDetectionHeuristic-                            , rpcInfo = Nothing+  when (isNothing bytecodeB) $ liftIO $ do+    putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"+    exitFailure+  let veriOpts = VeriOpts { iterConf = IterConfig {+                            maxIter = parseMaxIters cOpts.maxIterations+                            , askSmtIters = cOpts.askSmtIterations+                            , loopHeuristic = cOpts.loopDetectionHeuristic                             }-    calldata <- liftIO $ buildCalldata cmd-    solver <- liftIO $ getSolver cmd-    cores <- liftIO $ unsafeInto <$> getNumProcessors-    let solverCount = fromMaybe cores cmd.numSolvers-    withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do-      res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata-      case any isCex res of-        False -> liftIO $ do-          putStrLn "No discrepancies found"-          when (any isUnknown res || any isError res) $ do-            putStrLn "But the following issues occurred:"-            forM_ (groupIssues (filter isError res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str-            forM_ (groupIssues (filter isUnknown res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str-            exitFailure-        True -> liftIO $ do-          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") Nothing) cexs)-          exitFailure+                          , rpcInfo = Nothing+                          }+  calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg+  solver <- liftIO $ getSolver cOpts.solver+  cores <- liftIO $ unsafeInto <$> getNumProcessors+  let solverCount = fromMaybe cores cOpts.numSolvers+  withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \s -> do+    eq <- equivalenceCheck s (fromJust bytecodeA) (fromJust bytecodeB) veriOpts calldata eqOpts.create+    let anyIssues =  not (null eq.partials) || any (isUnknown . fst) eq.res  || any (isError . fst) eq.res+    liftIO $ case (any (isCex . fst) eq.res, anyIssues) of+      (False, False) -> putStrLn "   \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"+      (True, _)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"+      (_, True)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts may not behave equivalently"+    liftIO $ printWarnings eq.partials (map fst eq.res) "the contracts under test"+    case any (isCex . fst) eq.res of+      False -> liftIO $ do+        when anyIssues exitFailure+        putStrLn "No discrepancies found"+      True -> liftIO $ do+        let cexes = mapMaybe getCexP eq.res+        T.putStrLn . T.unlines $+          [ "Not equivalent. The following inputs result in differing behaviours:"+          , "" , "-----", ""+          ] <> (intersperse (T.unlines [ "", "-----" ]) $ fmap formatCexes cexes)+        exitFailure+  where+    decipher = maybe Nothing (hexByteString . strip0x)+    getCexP :: (ProofResult a b, String) -> Maybe (a, String)+    getCexP (Cex c, reason) = Just (c, reason)+    getCexP _ = Nothing+    formatCexes (cex, reason) = formatCex (AbstractBuf "txdata") Nothing cex <> "Difference: " <> T.pack reason -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-                              "bitwuzla" -> pure Bitwuzla-                              input -> do-                                putStrLn $ "unrecognised solver: " <> input-                                exitFailure+getSolver :: Text -> IO Solver+getSolver s = case T.unpack s of+  "z3" -> pure Z3+  "cvc5" -> pure CVC5+  "bitwuzla" -> pure Bitwuzla+  input -> do+    putStrLn $ "unrecognised solver: " <> input+    exitFailure -getSrcInfo :: App m => Command Options.Unwrapped -> m DappInfo-getSrcInfo cmd = do-  root <- liftIO $ getRoot cmd+getSrcInfo :: App m => ExecOptions -> CommonOptions -> m DappInfo+getSrcInfo execOpts cOpts = do+  root <- liftIO $ getRoot cOpts   conf <- readConfig   liftIO $ withCurrentDirectory root $ do-    outExists <- doesDirectoryExist (root </> "out")+    outExists <- doesDirectoryExist (root System.FilePath.</> "out")     if outExists     then do-      buildOutput <- runEnv Env {config = conf} $ readBuildOutput root (getProjectType cmd)+      buildOutput <- runEnv Env {config = conf} $ readBuildOutput root execOpts.projectType       case buildOutput of         Left _ -> pure emptyDapp         Right o -> pure $ dappInfo root o     else pure emptyDapp -getProjectType :: Command Options.Unwrapped -> ProjectType-getProjectType cmd = fromMaybe Foundry cmd.projectType--getRoot :: Command Options.Unwrapped -> IO FilePath-getRoot cmd = maybe getCurrentDirectory makeAbsolute (cmd.root)+getRoot :: CommonOptions -> IO FilePath+getRoot cmd = maybe getCurrentDirectory makeAbsolute cmd.root -parseMaxIters :: Maybe Integer -> Maybe Integer-parseMaxIters i = if num < 0 then Nothing else Just num-  where-    num = fromMaybe (5::Integer) i+parseMaxIters :: Integer -> Maybe Integer+parseMaxIters num = if num < 0 then Nothing else Just num  -- | 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+buildCalldata :: App m => CommonOptions -> Maybe Text -> [String] -> m (Expr Buf, [Prop])+buildCalldata cOpts sig arg = case (cOpts.calldata, sig) of   -- fully abstract calldata-  (Nothing, Nothing) -> pure $ mkCalldata Nothing []+  (Nothing, Nothing) -> mkCalldata Nothing []   -- fully concrete calldata   (Just c, Nothing) -> do     let val = hexByteString $ strip0x c-    if (isNothing val) then do+    if (isNothing val) then liftIO $ do       putStrLn $ "Error, invalid calldata: " <>  show c       exitFailure     else pure (ConcreteBuf (fromJust val), [])   -- 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+    method' <- liftIO $ functionAbi sig'+    mkCalldata (Just (Sig method'.methodSignature (snd <$> method'.inputs))) arg   -- both args provided-  (_, _) -> do+  (_, _) -> liftIO $ do     putStrLn "incompatible options provided: --calldata and --sig"     exitFailure   -- If function signatures are known, they should always be given for best results.-assert :: App m => Command Options.Unwrapped -> m ()-assert cmd = do-  let block'  = maybe Fetch.Latest Fetch.BlockNumber cmd.block-      rpcinfo = (,) block' <$> cmd.rpc-  calldata <- liftIO $ buildCalldata cmd-  preState <- liftIO $ symvmFromCommand cmd calldata-  let errCodes = fromMaybe defaultPanicCodes cmd.assertions+symbCheck :: App m => CommonFileOptions -> SymbolicOptions -> CommonExecOptions -> CommonOptions -> m ()+symbCheck cFileOpts sOpts cExecOpts cOpts = do+  let block' = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block+      rpcinfo = (,) block' <$> cExecOpts.rpc+  calldata <- buildCalldata cOpts sOpts.sig sOpts.arg+  preState <- liftIO $ symvmFromCommand cExecOpts sOpts cFileOpts calldata+  errCodes <- case sOpts.assertions of+    Nothing -> pure defaultPanicCodes+    Just s -> case (mapM readMaybe $ splitOn "," s) of+      Nothing -> liftIO $ do+        putStrLn $ "Error: invalid assertion codes: " <> s+        exitFailure+      Just codes -> pure codes+  when (cOpts.verb > 0) $ liftIO $ putStrLn $ "Using assertion code(s): " <> intercalate "," (map show errCodes)   cores <- liftIO $ unsafeInto <$> getNumProcessors-  let solverCount = fromMaybe cores cmd.numSolvers-  solver <- liftIO $ getSolver cmd-  withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \solvers -> do-    let veriOpts = VeriOpts { simp = True-                        , maxIter = parseMaxIters cmd.maxIterations-                        , askSmtIters = cmd.askSmtIterations-                        , loopHeuristic = cmd.loopDetectionHeuristic-                        , rpcInfo = rpcinfo-    }+  let solverCount = fromMaybe cores cOpts.numSolvers+  solver <- liftIO $ getSolver cOpts.solver+  withSolvers solver solverCount cOpts.solverThreads (Just cOpts.smttimeout) $ \solvers -> do+    let veriOpts = VeriOpts { iterConf = IterConfig {+                              maxIter = parseMaxIters cOpts.maxIterations+                              , askSmtIters = cOpts.askSmtIterations+                              , loopHeuristic = cOpts.loopDetectionHeuristic+                              }+                            , rpcInfo = rpcinfo+                            }     (expr, res) <- verify solvers veriOpts preState (Just $ checkAssertions errCodes)     case res of-      [Qed _] -> do+      [Qed] -> do         liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"-        showExtras solvers cmd calldata expr+        showExtras solvers sOpts calldata expr       _ -> do         let cexs = snd <$> mapMaybe getCex res-            smtUnknowns = mapMaybe getUnknown res             counterexamples               | null cexs = []               | otherwise =@@ -371,30 +519,24 @@                  , ("Discovered the following " <> (T.pack $ show (length cexs)) <> " counterexample(s):")                  , ""                  ] <> fmap (formatCex (fst calldata) Nothing) cexs-            unknowns-              | null smtUnknowns = []-              | otherwise =-                 [ ""-                 , "Could not determine reachability of the following end state(s):"-                 , ""-                 ] <> fmap (formatExpr) smtUnknowns-        liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)-        showExtras solvers cmd calldata expr+        liftIO $ T.putStrLn $ T.unlines counterexamples+        liftIO $ printWarnings [expr] res "symbolically"+        showExtras solvers sOpts calldata expr         liftIO exitFailure -showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()-showExtras solvers cmd calldata expr = do-  when cmd.showTree $ liftIO $ do+showExtras :: App m => SolverGroup ->SymbolicOptions -> (Expr Buf, [Prop]) -> Expr End -> m ()+showExtras solvers sOpts calldata expr = do+  when sOpts.showTree $ liftIO $ do     putStrLn "=== Expression ===\n"     T.putStrLn $ formatExpr expr     putStrLn ""-  when cmd.showReachableTree $ do+  when sOpts.showReachableTree $ do     reached <- reachable solvers expr     liftIO $ do-      putStrLn "=== Reachable Expression ===\n"+      putStrLn "=== Potentially Reachable Expression ===\n"       T.putStrLn (formatExpr . snd $ reached)       putStrLn ""-  when cmd.getModels $ do+  when sOpts.getModels $ do     liftIO $ putStrLn $ "=== Models for " <> show (Expr.numBranches expr) <> " branches ==="     ms <- produceModels solvers expr     liftIO $ forM_ ms (showModel (fst calldata))@@ -405,13 +547,13 @@ areAnyPrefixOf :: [Text] -> Text -> Bool areAnyPrefixOf prefixes t = any (flip T.isPrefixOf t) prefixes -launchExec :: App m => Command Options.Unwrapped -> m ()-launchExec cmd = do-  dapp <- getSrcInfo cmd-  vm <- liftIO $ vmFromCommand cmd+launchExec :: App m => CommonFileOptions -> ExecOptions -> CommonExecOptions -> CommonOptions -> m ()+launchExec cFileOpts execOpts cExecOpts cOpts = do+  dapp <- getSrcInfo execOpts cOpts+  vm <- liftIO $ vmFromCommand cOpts cExecOpts cFileOpts execOpts   let-    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block-    rpcinfo = (,) block <$> cmd.rpc+    block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block+    rpcinfo = (,) block <$> cExecOpts.rpc    -- TODO: we shouldn't need solvers to execute this code   withSolvers Z3 0 1 Nothing $ \solvers -> do@@ -436,10 +578,10 @@         internalError "no EVM result"  -- | Creates a (concrete) VM from command line options-vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld)-vmFromCommand cmd = do-  (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of-    Nothing -> pure (LitAddr 0,Lit 0,0,0,0)+vmFromCommand :: CommonOptions -> CommonExecOptions -> CommonFileOptions -> ExecOptions -> IO (VM Concrete RealWorld)+vmFromCommand cOpts cExecOpts cFileOpts execOpts= do+  (miner,ts,baseFee,blockNum,prevRan) <- case cExecOpts.rpc of+    Nothing -> pure (LitAddr 0,Lit 0,0,Lit 0,0)     Just url -> Fetch.fetchBlockFrom block url >>= \case       Nothing -> do         putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url@@ -451,10 +593,11 @@                              , prevRandao                              ) -  contract <- case (cmd.rpc, cmd.address, cmd.code) of+  codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code+  contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of     (Just url, Just addr', Just c) -> do       let code = hexByteString $ strip0x c-      if (isNothing code) then do+      if isNothing code then do         putStrLn $ "Error, invalid code: " <> show c         exitFailure       else@@ -489,7 +632,7 @@       putStrLn "Error, must provide at least (rpc + address) or code"       exitFailure -  let ts' = case maybeLitWord ts of+  let ts' = case maybeLitWordSimp ts of         Just t -> t         Nothing -> internalError "unexpected symbolic timestamp when executing vm test" @@ -501,24 +644,24 @@     pure $ EVM.Transaction.initTx vm   where         bsCallData = bytes (.calldata) (pure "")-        block   = maybe Fetch.Latest Fetch.BlockNumber cmd.block-        value   = word (.value) 0+        block   = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block+        val     = word (.value) 0         caller  = addr (.caller) (LitAddr 0)         origin  = addr (.origin) (LitAddr 0)         calldata = ConcreteBuf $ fromJust bsCallData         decipher = hexByteString . strip0x-        mkCode bs = if cmd.create+        mkCode bs = if execOpts.create                     then InitCode bs mempty                     else RuntimeCode (ConcreteRuntimeCode bs)-        address = if cmd.create-                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddr origin) (W64 $ word64 (.nonce) 0))+        address = if execOpts.create+                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))                   else addr (.address) (LitAddr 0xacab)          vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts           { contract       = c           , otherContracts = []           , calldata       = (calldata, [])-          , value          = Lit value+          , value          = Lit val           , address        = address           , caller         = caller           , origin         = origin@@ -527,7 +670,7 @@           , priorityFee    = word (.priorityFee) 0           , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff           , coinbase       = addr (.coinbase) miner-          , number         = word (.number) blockNum+          , number         = maybe blockNum Lit cExecOpts.number           , timestamp      = Lit $ word (.timestamp) ts           , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff           , gasprice       = word (.gasprice) 0@@ -535,22 +678,22 @@           , prevRandao     = word (.prevRandao) prevRan           , schedule       = feeSchedule           , chainId        = word (.chainid) 1-          , create         = (.create) cmd+          , create         = (.create) execOpts           , baseState      = EmptyBase           , txAccessList   = mempty -- TODO: support me soon           , allowFFI       = False           , freshAddresses = 0           , beaconRoot     = 0           }-        word f def = fromMaybe def (f cmd)-        word64 f def = fromMaybe def (f cmd)-        addr f def = maybe def LitAddr (f cmd)-        bytes f def = maybe def decipher (f cmd)+        word f def = fromMaybe def (f cExecOpts)+        word64 f def = fromMaybe def (f cExecOpts)+        addr f def = maybe def LitAddr (f cExecOpts)+        bytes f def = maybe def decipher (f cOpts) -symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)-symvmFromCommand cmd calldata = do-  (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of-    Nothing -> pure (SymAddr "miner",0,0,0)+symvmFromCommand :: CommonExecOptions -> SymbolicOptions -> CommonFileOptions -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)+symvmFromCommand cExecOpts sOpts cFileOpts calldata = do+  (miner,blockNum,baseFee,prevRan) <- case cExecOpts.rpc of+    Nothing -> pure (SymAddr "miner",Lit 0,0,0)     Just url -> Fetch.fetchBlockFrom block url >>= \case       Nothing -> do         putStrLn $ "Error, Could not fetch block" <> show block <> " from URL: " <> show url@@ -562,24 +705,25 @@                              )    let-    caller = maybe (SymAddr "caller") LitAddr cmd.caller-    ts = maybe Timestamp Lit cmd.timestamp-    callvalue = maybe TxValue Lit cmd.value-    storageBase = maybe AbstractBase parseInitialStorage (cmd.initialStorage)+    caller = maybe (SymAddr "caller") LitAddr cExecOpts.caller+    ts = maybe Timestamp Lit cExecOpts.timestamp+    callvalue = maybe TxValue Lit cExecOpts.value+    storageBase = maybe AbstractBase parseInitialStorage (sOpts.initialStorage) -  contract <- case (cmd.rpc, cmd.address, cmd.code) of+  codeWrapped <- getCode cFileOpts.codeFile cFileOpts.code+  contract <- case (cExecOpts.rpc, cExecOpts.address, codeWrapped) of     (Just url, Just addr', _) ->       Fetch.fetchContractFrom block url addr' >>= \case         Nothing -> do           putStrLn "Error, contract not found."           exitFailure-        Just contract' -> case cmd.code of+        Just contract' -> case codeWrapped of               Nothing -> pure contract'               -- if both code and url is given,               -- fetch the contract and overwrite the code               Just c -> do                 let c' = decipher c-                if (isNothing c') then do+                if isNothing c' then do                   putStrLn $ "Error, invalid code: " <> show c                   exitFailure                 else pure $ do@@ -591,7 +735,7 @@      (_, _, Just c)  -> do       let c' = decipher c-      if (isNothing c') then do+      if isNothing c' then do         putStrLn $ "Error, invalid code: " <> show c         exitFailure       else case storageBase of@@ -607,9 +751,9 @@    where     decipher = hexByteString . strip0x-    block = maybe Fetch.Latest Fetch.BlockNumber cmd.block+    block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block     origin = eaddr (.origin) (SymAddr "origin")-    mkCode bs = if cmd.create+    mkCode bs = if sOpts.create                    then InitCode bs mempty                    else RuntimeCode (ConcreteRuntimeCode bs)     address = eaddr (.address) (SymAddr "entrypoint")@@ -626,7 +770,7 @@       , baseFee        = baseFee       , priorityFee    = word (.priorityFee) 0       , coinbase       = eaddr (.coinbase) miner-      , number         = word (.number) blockNum+      , number         = maybe blockNum Lit cExecOpts.number       , timestamp      = ts       , blockGaslimit  = word64 (.gaslimit) 0xffffffffffffffff       , gasprice       = word (.gasprice) 0@@ -634,49 +778,44 @@       , prevRandao     = word (.prevRandao) prevRan       , schedule       = feeSchedule       , chainId        = word (.chainid) 1-      , create         = (.create) cmd+      , create         = (.create) sOpts       , baseState      = baseState       , txAccessList   = mempty       , allowFFI       = False       , freshAddresses = 0       , beaconRoot     = 0       }-    word f def = fromMaybe def (f cmd)-    word64 f def = fromMaybe def (f cmd)-    eaddr f def = maybe def LitAddr (f cmd)+    word f def = fromMaybe def (f cExecOpts)+    word64 f def = fromMaybe def (f cExecOpts)+    eaddr f def = maybe def LitAddr (f cExecOpts) -unitTestOptions :: Command Options.Unwrapped -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)-unitTestOptions cmd solvers buildOutput = do-  root <- getRoot cmd+unitTestOptions :: TestOptions -> CommonOptions -> SolverGroup -> Maybe BuildOutput -> IO (UnitTestOptions RealWorld)+unitTestOptions testOpts cOpts solvers buildOutput = do+  root <- getRoot cOpts   let srcInfo = maybe emptyDapp (dappInfo root) buildOutput--  let rpcinfo = case (cmd.number, cmd.rpc) of+  let rpcinfo = case (testOpts.number, testOpts.rpc) of           (Just block, Just url) -> Just (Fetch.BlockNumber block, url)           (Nothing, Just url) -> Just (Fetch.Latest, url)           _ -> Nothing   params <- paramsFromRpc rpcinfo--  let-    testn = params.number-    block' = if 0 == testn+  let testn = params.number+      block' = if 0 == testn        then Fetch.Latest        else Fetch.BlockNumber testn-   pure UnitTestOptions     { solvers = solvers-    , rpcInfo = case cmd.rpc of+    , rpcInfo = case testOpts.rpc of          Just url -> Just (block', url)          Nothing  -> Nothing-    , maxIter = parseMaxIters cmd.maxIterations-    , askSmtIters = cmd.askSmtIterations-    , smtTimeout = cmd.smttimeout-    , solver = cmd.solver-    , verbose = cmd.verbose-    , match = T.pack $ fromMaybe ".*" cmd.match+    , maxIter = parseMaxIters cOpts.maxIterations+    , askSmtIters = cOpts.askSmtIterations+    , smtTimeout = Just cOpts.smttimeout+    , match = T.pack $ fromMaybe ".*" testOpts.match+    , prefix = T.pack testOpts.prefix     , testParams = params     , dapp = srcInfo-    , ffiAllowed = cmd.ffi-    , checkFailBit = (fromMaybe Forge cmd.assertionType) == DSTest+    , ffiAllowed = testOpts.ffi+    , checkFailBit = cOpts.assertionType == DSTest     } parseInitialStorage :: InitialStorage -> BaseState parseInitialStorage Empty = EmptyBase

@@ -2,7 +2,7 @@ name:   hevm version:-  0.54.2+  0.55.1 synopsis:   Symbolic EVM Evaluator description:@@ -12,7 +12,7 @@ license:   AGPL-3.0-only author:-  dxo, Martin Lundfall, Mikael Brockman+  dxo, Martin Lundfall, Mikael Brockman, Martin Blicha, Zoe Paraskevopoulou, Mate Soos maintainer:   git@d-xo.org category:@@ -89,6 +89,7 @@  library   import: shared+  default-language: GHC2021   exposed-modules:     EVM,     EVM.ABI,@@ -146,11 +147,11 @@     containers                        >= 0.6.0 && < 0.7,     transformers                      >= 0.5 && < 0.7,     tree-view                         >= 0.5 && < 0.6,-    aeson                             >= 2.0.0 && < 2.2,-    bytestring                        >= 0.11.3.1 && < 0.12,+    aeson                             >= 2.0.0 && < 2.3,+    bytestring                        >= 0.11.3.1 && < 0.13,     scientific                        >= 0.3.6 && < 0.4,     binary                            >= 0.8.6 && < 0.9,-    text                              >= 1.2.3 && < 2.1,+    text                              >= 1.2.3 && < 2.2,     unordered-containers              >= 0.2.10 && < 0.3,     vector                            >= 0.12.1 && < 0.14,     base16                            >= 1.0 && < 1.1,@@ -190,6 +191,7 @@  executable hevm   import: shared+  default-language: GHC2021   hs-source-dirs:     cli   main-is:@@ -203,21 +205,23 @@     base,     bytestring,     data-dword,-    directory,+    directory                         >= 1.3.6 && < 1.4,     filepath,     hevm,     optparse-generic,+    optparse-applicative              >= 0.18.0.0 && < 0.20.0.0,     text,     optics-core,-    githash,+    githash                           >= 0.1.5 && < 0.2,     witch,     unliftio-core,-    with-utf8,+    split,  --- Test Helpers ---  common test-base   import: shared+  default-language: GHC2021   hs-source-dirs:     test   other-modules:@@ -231,12 +235,10 @@     base,     containers,     directory,-    extra,     bytestring,     filemanip,     filepath,     hevm,-    here,     mtl,     process,     tasty,@@ -256,6 +258,7 @@  library test-utils   import: test-base+  default-language: GHC2021   exposed-modules:     EVM.Test.Utils     EVM.Test.Tracing@@ -263,6 +266,7 @@  common test-common   import: test-base+  default-language: GHC2021   if flag(devel)     ghc-options: -threaded -with-rtsopts=-N   build-depends:@@ -276,6 +280,7 @@  test-suite test   import: test-common+  default-language: GHC2021   type:     exitcode-stdio-1.0   main-is:@@ -284,6 +289,8 @@     base16,     binary,     data-dword,+    extra,+    here,     time,     regex @@ -291,6 +298,7 @@ -- suite to make it easy to skip them when running nix-build test-suite rpc-tests   import: test-common+  default-language: GHC2021   type:     exitcode-stdio-1.0   main-is:@@ -298,15 +306,36 @@  test-suite ethereum-tests   import: test-common+  default-language: GHC2021   type:     exitcode-stdio-1.0   main-is:     BlockchainTests.hs +test-suite cli-test+  type:+    exitcode-stdio-1.0+  default-language: GHC2021+  hs-source-dirs:+    test+  main-is:+    clitest.hs+  build-depends:+    base,+    hevm,+    hspec,+    process,+    text,+    bytestring,+    filepath,+    split,+    here,+ --- Benchmarks ---  benchmark bench   import: shared+  default-language: GHC2021   type:     exitcode-stdio-1.0   main-is:@@ -331,3 +360,27 @@     filepath,     containers,     unliftio-core++benchmark bench-perf+  import: shared+  default-language: GHC2021+  type:+    exitcode-stdio-1.0+  main-is:+    bench-perf.hs+  hs-source-dirs:+    bench+  ghc-options:+    -O2 -threaded -with-rtsopts=-N -fproc-alignment=64+  other-modules:+    Paths_hevm+  autogen-modules:+    Paths_hevm+  build-depends:+    base,+    here,+    hevm,+    mtl,+    tasty-bench,+    test-utils,+    utf8-string

@@ -9,7 +9,6 @@ import Optics.State import Optics.State.Operators import Optics.Zoom-import Optics.Operators.Unsafe  import EVM.ABI import EVM.Expr (readStorage, writeStorage, readByte, readWord, writeWord,@@ -24,6 +23,8 @@ import EVM.Sign qualified import EVM.Concrete qualified as Concrete import EVM.CheatsTH+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp)+import EVM.Effects (Config (..))  import Control.Monad (unless, when) import Control.Monad.ST (ST)@@ -45,7 +46,7 @@ import Data.List.Split (splitOn) import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map-import Data.Maybe (fromMaybe, fromJust, isJust)+import Data.Maybe (fromMaybe, fromJust, isJust, isNothing) import Data.Set (insert, member, fromList) import Data.Sequence (Seq) import Data.Sequence qualified as Seq@@ -55,10 +56,9 @@ import Data.Tree.Zipper qualified as Zipper import Data.Typeable import Data.Vector qualified as V-import Data.Vector.Storable qualified as SV-import Data.Vector.Storable.Mutable qualified as SV-import Data.Vector.Unboxed qualified as VUnboxed-import Data.Vector.Unboxed.Mutable qualified as VUnboxed.Mutable+import Data.Vector.Storable qualified as VS+import Data.Vector.Storable.Mutable qualified as VS.Mutable+import Data.Vector.Storable.ByteString (vectorToByteString) import Data.Word (Word8, Word32, Word64) import Text.Read (readMaybe) import Witch (into, tryFrom, unsafeInto, tryInto)@@ -69,7 +69,7 @@  blankState :: VMOps t => ST s (FrameState t s) blankState = do-  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  memory <- ConcreteMemory <$> VS.Mutable.new 0   pure $ FrameState     { contract     = LitAddr 0     , codeContract = LitAddr 0@@ -116,7 +116,7 @@         ++ (Map.keys txaccessList)       initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)       touched = if o.create then [txorigin] else [txorigin, txtoAddr]-  memory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+  memory <- ConcreteMemory <$> VS.Mutable.new 0   pure $ setEIP4788Storage o $ VM     { result = Nothing     , frames = mempty@@ -164,6 +164,8 @@     , currentFork = 0     , labels = mempty     , osEnv = mempty+    , freshVar = 0+    , exploreDepth = 0     }     where     env = Env@@ -281,14 +283,14 @@       RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs state.pc       RuntimeCode (SymbolicRuntimeCode ops) ->         fromMaybe (internalError "could not analyze symbolic code") $-          maybeLitByte $ ops V.! state.pc+          maybeLitByteSimp $ ops V.! state.pc  getOpName :: forall (t :: VMType) s . FrameState t s -> [Char] getOpName state = intToOpName $ fromEnum $ getOpW8 state  -- | Executes the EVM one step-exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()-exec1 = do+exec1 :: forall (t :: VMType) s. (VMOps t) => Config ->  EVM t s ()+exec1 conf = do   vm <- get    let@@ -296,12 +298,9 @@     stk  = vm.state.stack     self = vm.state.contract     this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)-     fees@FeeSchedule {..} = vm.block.schedule-     doStop = finishFrame (FrameReturned mempty)--    litSelf = maybeLitAddr self+    litSelf = maybeLitAddrSimp self    if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0xa then do     -- call to precompile@@ -321,8 +320,7 @@             touchAccount self             out <- use (#state % #returndata)             finishFrame (FrameReturned out)-        e -> partial $-               UnexpectedSymbolicArg vmx.state.pc (getOpName vmx.state) "precompile returned a symbolic value" (wrap [e])+        e -> unexpectedSymArg "precompile returned a symbolic value" [e]       _ ->         underrun @@ -330,9 +328,8 @@     then doStop      else do+      let ?conf = conf       let ?op = getOpW8 vm.state-      let opName = getOpName vm.state-       case getOp (?op) of          OpPush0 -> do@@ -365,14 +362,16 @@                   pushSym y          OpSwap i ->-          if length stk < (into i) + 1-            then underrun-            else+          case (stk ^? ix_i, stk ^? ix_0) of+            (Just ei, Just e0) ->               burn g_verylow $ do                 next                 zoom (#state % #stack) $ do-                  assign (ix 0) (stk ^?! ix (into i))-                  assign (ix (into i)) (stk ^?! ix 0)+                  ix_i .= e0+                  ix_0 .= ei+            _ -> underrun+          where+            (ix_i, ix_0) = (ix (into i), ix 0)          OpLog n ->           notStatic $@@ -450,14 +449,13 @@          OpBalance ->           case stk of-            x:xs -> forceAddr x "BALANCE" $ \a ->+            x:xs -> forceAddr x (freshVarFallback xs) $ \a ->               accessAndBurn a $-                fetchAccount a $ \c -> do+                fetchAccountWithFallback a (freshVarFallback xs) $ \c -> do                   next                   assign (#state % #stack) xs                   pushSym c.balance-            [] ->-              underrun+            [] -> underrun          OpOrigin ->           limitStack 1 . burn g_base $@@ -510,9 +508,9 @@          OpExtcodesize ->           case stk of-            x':xs -> forceAddr x' "EXTCODESIZE" $ \x -> do+            x':xs -> forceAddr x' (freshVarFallback xs) $ \x -> do               let impl = accessAndBurn x $-                           fetchAccount x $ \c -> do+                           fetchAccountWithFallback x (freshVarFallback xs) $ \c -> do                              next                              assign (#state % #stack) xs                              case view bytecode c of@@ -532,7 +530,7 @@         OpExtcodecopy ->           case stk of             extAccount':memOffset:codeOffset:codeSize:xs ->-              forceAddr extAccount' "EXTCODECOPY" $ \extAccount -> do+              forceAddr extAccount' (unexpectedSymArgW "EXTCODECOPY") $ \extAccount -> do                 burnExtcodecopy extAccount codeSize $                   accessMemoryRange memOffset codeSize $                     fetchAccount extAccount $ \c -> do@@ -540,9 +538,7 @@                       assign (#state % #stack) xs                       case view bytecode c of                         Just b -> copyBytesToMemory b codeSize codeOffset memOffset-                        Nothing -> do-                          pc <- use (#state % #pc)-                          partial $ UnexpectedSymbolicArg pc opName "Cannot copy from unknown code at" (wrap [extAccount])+                        Nothing -> unexpectedSymArg "Cannot copy from unknown code at" [extAccount]             _ -> underrun          OpReturndatasize ->@@ -566,16 +562,16 @@                     _ -> do                       let oob = Expr.lt (bufLength vm.state.returndata) (Expr.add xFrom xSize)                           overflow = Expr.lt (Expr.add xFrom xSize) (xFrom)-                      branch (Expr.or oob overflow) jump+                      branch conf.maxDepth (Expr.or oob overflow) jump             _ -> underrun          OpExtcodehash ->           case stk of-            x':xs -> forceAddr x' "EXTCODEHASH" $ \x ->+            x':xs -> forceAddr x' (freshVarFallback xs) $ \x ->               accessAndBurn x $ do-                next-                assign (#state % #stack) xs-                fetchAccount x $ \c ->+                fetchAccountWithFallback x (freshVarFallback xs) $ \c -> do+                   next+                   assign (#state % #stack) xs                    if accountEmpty c                      then push (W256 0)                      else case view bytecode c of@@ -585,13 +581,21 @@               underrun          OpBlockhash -> do-          -- We adopt the fake block hash scheme of the VMTests,-          -- so that blockhash(i) is the hash of i as decimal ASCII.           stackOp1 g_blockhash $ \case-            Lit i -> if i + 256 < vm.block.number || i >= vm.block.number-                     then Lit 0-                     else (into i :: Integer) & show & Char8.pack & keccak' & Lit+            Lit i -> case vm.block.number of+              Lit vmBlockNumber ->+                if i + 256 < vmBlockNumber || i >= vmBlockNumber+                -- blockhash is 0 if block is too old or too new as per EVM spec+                then Lit 0+                -- We adopt the fake block hash scheme of the VMTests,+                -- so that blockhash(i) is the hash of i as decimal ASCII.+                else fakeBlockHash i+              -- For symbolic block numbers, we don't know if it's too old or too new,+              -- so we return fake block hash+              _ -> fakeBlockHash i             i -> BlockHash i+            where+              fakeBlockHash i = (into i :: Integer) & show & Char8.pack & keccak' & Lit          OpCoinbase ->           limitStack 1 . burn g_base $@@ -603,7 +607,7 @@          OpNumber ->           limitStack 1 . burn g_base $-            next >> push vm.block.number+            next >> pushSym vm.block.number          OpPrevRandao -> do           limitStack 1 . burn g_base $@@ -670,9 +674,9 @@             mcopy sz srcOff dstOff = do                   m <- gets (.state.memory)                   case m of-                    ConcreteMemory mem -> do-                      buf <- freezeMemory mem-                      copyBytesToMemory buf sz srcOff dstOff+                    ConcreteMemory _ -> do+                      buf <- readMemory srcOff sz+                      copyBytesToMemory buf sz (Lit 0) dstOff                     SymbolicMemory mem -> do                       assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem) @@ -741,7 +745,7 @@                         Lit v -> v                         _ -> 0                     storage_cost =-                      case (maybeLitWord current, maybeLitWord new) of+                      case (maybeLitWordSimp current, maybeLitWordSimp new) of                         (Just current', Just new') ->                            if (current' == new') then g_sload                            else if (current' == original) && (original == 0) then g_sset@@ -759,7 +763,7 @@                     assign (#state % #stack) xs                     modifying (#env % #contracts % ix self % #storage) (writeStorage x new) -                    case (maybeLitWord current, maybeLitWord new) of+                    case (maybeLitWordSimp current, maybeLitWordSimp new) of                        (Just current', Just new') ->                           unless (current' == new') $                             if current' == original then@@ -801,7 +805,7 @@         OpJump ->           case stk of             x:xs ->-              burn g_mid $ forceConcrete x "JUMP: symbolic jumpdest" $ \x' ->+              burn g_mid $ forceConcreteLimitSz x 2 "JUMP: symbolic jumpdest" $ \x' ->                 case tryInto x' of                   Left _ -> vmError BadJumpDestination                   Right i -> checkJump i xs@@ -809,14 +813,14 @@          OpJumpi ->           case stk of-            x:y:xs -> forceConcrete x "JUMPI: symbolic jumpdest" $ \x' ->+            x:y:xs -> forceConcreteLimitSz x 2 "JUMPI: symbolic jumpdest" $ \x' ->               burn g_high $                 let jump :: Bool -> EVM t s ()                     jump False = assign (#state % #stack) xs >> next                     jump _    = case tryInto x' of                       Left _ -> vmError BadJumpDestination                       Right i -> checkJump i xs-                in branch y jump+                in branch conf.maxDepth y jump             _ -> underrun          OpPc ->@@ -861,7 +865,12 @@                   assign (#state % #overrideCaller) Nothing                   assign (#state % #resetCaller) False -                newAddr <- createAddress from' this.nonce+                touchAddress from'+                nonce <- zoom (#env % #contracts) $ do+                  contr <- use (at from')+                  pure $ (\c -> c.nonce) =<< contr++                newAddr <- createAddress from' nonce                 _ <- accessAccountForGas newAddr                 burn' cost $ do                   initCode <- readMemory xOffset xSize@@ -871,14 +880,18 @@         OpCall ->           case stk of             xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->-              branch (Expr.gt xValue (Lit 0)) $ \gt0 -> do+              branch conf.maxDepth (Expr.gt xValue (Lit 0)) $ \gt0 -> do+                let addrFallback = if conf.promiseNoReent then const fallback+                                   else unexpectedSymArgW "unable to determine a call target"                 (if gt0 then notStatic else id) $-                  forceAddr xTo' "unable to determine a call target" $ \xTo ->+                  forceAddr xTo' addrFallback $ \xTo ->                     case gasTryFrom xGas of                       Left _ -> vmError IllegalOverflow                       Right gas -> do                         overrideC <- use $ #state % #overrideCaller-                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $+                        let delegateFallback = if conf.promiseNoReent then const fallback+                                               else unknownCode+                        delegateCall this gas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs delegateFallback $                           \callee -> do                             let from' = fromMaybe self overrideC                             zoom #state $ do@@ -888,24 +901,23 @@                             touchAccount from'                             touchAccount callee                             transfer from' callee xValue-            _ ->-              underrun+              where fallback = freshBufFallback xs+            _ -> underrun          OpCallcode ->           case stk of             xGas:xTo':xValue:xInOffset:xInSize:xOutOffset:xOutSize:xs ->-              forceAddr xTo' "unable to determine a call target" $ \xTo ->+              forceAddr xTo' (unexpectedSymArgW "unable to determine a call target") $ \xTo ->                 case gasTryFrom xGas of                   Left _ -> vmError IllegalOverflow                   Right gas -> do                     overrideC <- use $ #state % #overrideCaller-                    delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ \_ -> do+                    delegateCall this gas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs unknownCode $ \_ -> do                       zoom #state $ do                         assign #callvalue xValue                         assign #caller $ fromMaybe self overrideC                       touchAccount self-            _ ->-              underrun+            _ -> underrun          OpReturn ->           case stk of@@ -914,7 +926,7 @@                 output <- readMemory xOffset xSize                 let                   codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")-                               . maybeLitWord . bufLength $ output+                               . maybeLitWordSimp . bufLength $ output                   maxsize = vm.block.maxCodeSize                   creation = case vm.frames of                     [] -> vm.tx.isCreate@@ -933,7 +945,7 @@                     case readByte (Lit 0) output of                       LitByte 0xef -> frameErrored                       LitByte _ -> frameReturned-                      y -> branch (Expr.eqByte y (LitByte 0xef)) $ \case+                      y -> branch conf.maxDepth (Expr.eqByte y (LitByte 0xef)) $ \case                           True -> frameErrored                           False -> frameReturned                 else@@ -943,16 +955,13 @@         OpDelegatecall ->           case stk of             xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->-              case wordToAddr xTo of-                Nothing -> do-                  loc <- codeloc-                  let msg = "Unable to determine a call target"-                  partial $ UnexpectedSymbolicArg (snd loc) opName msg [SomeExpr xTo]-                Just xTo' ->+              forceAddr xTo (const $ unexpectedSymArg "unable to determine a call target" [xTo]) $ \xTo' ->                   case gasTryFrom xGas of                     Left _ -> vmError IllegalOverflow                     Right gas ->-                      delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $+                      -- NOTE: we don't update overrideCaller in this case because+                      -- forge-std doesn't. see: https://github.com/foundry-rs/foundry/pull/8863+                      delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs unknownCode $                         \_ -> touchAccount self             _ -> underrun @@ -972,6 +981,8 @@                         assign (#state % #overrideCaller) Nothing                         assign (#state % #resetCaller) False +                      touchAddress from'+                       let (cost, gas') = costOfCreate fees availableGas xSize True                       newAddr <- create2Address self xSalt initCode                       _ <- accessAccountForGas newAddr@@ -982,33 +993,28 @@         OpStaticcall ->           case stk of             xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->-              case wordToAddr xTo of-                Nothing -> do-                  loc <- codeloc-                  let msg = "Unable to determine a call target"-                  partial $ UnexpectedSymbolicArg (snd loc) opName msg [SomeExpr xTo]-                Just xTo' ->-                  case gasTryFrom xGas of-                    Left _ -> vmError IllegalOverflow-                    Right gas -> do-                      overrideC <- use $ #state % #overrideCaller-                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $-                        \callee -> do-                          zoom #state $ do-                            assign #callvalue (Lit 0)-                            assign #caller $ fromMaybe self overrideC-                            assign #contract callee-                            assign #static True-                          touchAccount self-                          touchAccount callee-            _ ->-              underrun+              forceAddr xTo (const fallback) $ \xTo' -> case gasTryFrom xGas of+                Left _ -> vmError IllegalOverflow+                Right gas -> do+                  overrideC <- use $ #state % #overrideCaller+                  delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs (const fallback) $+                    \callee -> do+                      zoom #state $ do+                        assign #callvalue (Lit 0)+                        assign #caller $ fromMaybe self overrideC+                        assign #contract callee+                        assign #static True+                      touchAccount self+                      touchAccount callee+                where+                  fallback = freshBufFallback xs+            _ -> underrun          OpSelfdestruct ->           notStatic $           case stk of             [] -> underrun-            (xTo':_) -> forceAddr xTo' "SELFDESTRUCT" $ \case+            (xTo':_) -> forceAddr xTo' (unexpectedSymArgW "SELFDESTRUCT") $ \case               xTo@(LitAddr _) -> do                 cc <- gets (.tx.subState.createdContracts)                 let createdThisTr = self `member` cc@@ -1016,7 +1022,7 @@                 let cost = if acc then 0 else g_cold_account_access                     funds = this.balance                     recipientExists = accountExists xTo vm-                branch (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do+                branch conf.maxDepth (Expr.iszero $ Expr.eq funds (Lit 0)) $ \hasFunds -> do                   let c_new = if (not recipientExists) && hasFunds                               then g_selfdestruct_newaccount                               else 0@@ -1033,9 +1039,7 @@                       doStop                     else                       doStop-              a -> do-                pc <- use (#state % #pc)-                partial $ UnexpectedSymbolicArg pc opName "trying to self destruct to a symbolic address" (wrap [a])+              a -> unexpectedSymArg "trying to self destruct to a symbolic address" [a]          OpRevert ->           case stk of@@ -1045,22 +1049,17 @@                 finishFrame (FrameReverted output)             _ -> underrun -        OpUnknown xxx ->-          vmError $ UnrecognizedOpcode xxx+        OpUnknown xxx -> vmError $ UnrecognizedOpcode xxx -transfer :: VMOps t => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s ()+transfer :: (VMOps t, ?conf::Config) => Expr EAddr -> Expr EAddr -> Expr EWord -> EVM t s () transfer _ _ (Lit 0) = pure () transfer src dst val = do   sb <- preuse $ #env % #contracts % ix src % #balance   db <- preuse $ #env % #contracts % ix dst % #balance-  baseState <- use (#config % #baseState)-  let mkc = case baseState of-              AbstractBase -> unknownContract-              EmptyBase -> const emptyContract   case (sb, db) of     -- both sender and recipient in state     (Just srcBal, Just _) ->-      branch (Expr.gt val srcBal) $ \case+      branch (?conf).maxDepth (Expr.gt val srcBal) $ \case         True -> vmError $ BalanceTooLow val srcBal         False -> do           (#env % #contracts % ix src % #balance) %= (`Expr.sub` val)@@ -1069,28 +1068,22 @@     (Nothing, Just _) -> do       case src of         LitAddr _ -> do-          (#env % #contracts) %= (Map.insert src (mkc src))+          touchAddress src           transfer src dst val-        SymAddr _ -> do-          pc <- use (#state % #pc)-          state <- use #state-          partial $ UnexpectedSymbolicArg pc (getOpName state) "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [src])+        SymAddr _ -> unexpectedSymArg "Attempting to transfer eth from a symbolic address that is not present in the state" [src]         GVar _ -> internalError "Unexpected GVar"     -- recipient not in state     (_ , Nothing) -> do       case dst of         LitAddr _ -> do-          (#env % #contracts) %= (Map.insert dst (mkc dst))+          touchAddress dst           transfer src dst val-        SymAddr _ -> do-          pc <- use (#state % #pc)-          state <- use #state-          partial $ UnexpectedSymbolicArg pc (getOpName state) "Attempting to transfer eth to a symbolic address that is not present in the state" (wrap [dst])+        SymAddr _ -> unexpectedSymArg "Attempting to transfer eth to a symbolic address that is not present in the state" [dst]         GVar _ -> internalError "Unexpected GVar"  -- | Checks a *CALL for failure; OOG, too many callframes, memory access etc. callChecks-  :: forall (t :: VMType) s. (?op :: Word8, VMOps t)+  :: forall (t :: VMType) s. (?op :: Word8, ?conf :: Config, VMOps t)   => Contract   -> Gas t   -> Expr EAddr@@ -1129,7 +1122,7 @@           -- from is in the state, we check if they have enough balance           (Just fb, _) -> do             burn (cost - gas') $-              branch (Expr.gt xValue fb) $ \case+              branch (?conf).maxDepth (Expr.gt xValue fb) $ \case                 True -> do                   assign (#state % #stack) (Lit 0 : xs)                   assign (#state % #returndata) mempty@@ -1149,14 +1142,11 @@               callChecks this xGas xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs continue              -- adding a symbolic address into the state here would be unsound (due to potential aliasing)-            SymAddr _ -> do-              pc <- use (#state % #pc)-              state <- use #state-              partial $ UnexpectedSymbolicArg pc (getOpName state) "Attempting to transfer eth from a symbolic address that is not present in the state" (wrap [from])+            SymAddr _ -> unexpectedSymArg "Attempting to transfer eth from a symbolic address that is not present in the state" [from]             GVar _ -> internalError "Unexpected GVar"  precompiledContract-  :: (?op :: Word8, VMOps t)+  :: (?conf :: Config, ?op :: Word8, VMOps t)   => Contract   -> Gas t   -> Addr@@ -1171,12 +1161,10 @@       executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs       self <- use (#state % #contract)       stk <- use (#state % #stack)-      pc' <- use (#state % #pc)       result' <- use #result-      vm <- get       case result' of         Nothing -> case stk of-          x:_ -> case maybeLitWord x of+          x:_ -> case maybeLitWordSimp x of             Just 0 ->               pure ()             Just 1 ->@@ -1184,8 +1172,7 @@                 touchAccount self                 touchAccount (LitAddr recipient)                 transfer self (LitAddr recipient) xValue-            _ -> partial $-                   UnexpectedSymbolicArg pc' (getOpName vm.state) "unexpected return value from precompile" (wrap [x])+            _ -> unexpectedSymArg "unexpected return value from precompile" [x]           _ -> underrun         _ -> pure () @@ -1380,21 +1367,36 @@ getCodeLocation vm = (vm.state.contract, vm.state.pc)  query :: Query t s -> EVM t s ()-query = assign #result . Just . HandleEffect . Query+query q = assign #result $ Just $ HandleEffect (Query q) -choose :: Choose s -> EVM Symbolic s ()-choose = assign #result . Just . HandleEffect . Choose+runBoth :: Maybe Int -> Int -> RunBoth s -> EVM Symbolic s ()+runBoth depthLimit exploreDepth c = do+  if (isNothing depthLimit || (exploreDepth < fromJust depthLimit)) then do+    assign #result $ Just $ HandleEffect (RunBoth c)+  else do+    vm <- get+    assign #result $ Just $ Unfinished (BranchTooDeep {pc = vm.state.pc}) --- | Construct RPC Query and halt execution until resolved+runAll :: Maybe Int -> Int -> RunAll s -> EVM Symbolic s ()+runAll depthLimit exploreDepth c = do+  if (isNothing depthLimit || (exploreDepth < fromJust depthLimit)) then do+    assign #result $ Just $ HandleEffect (RunAll c)+  else do+    vm <- get+    assign #result $ Just $ Unfinished (BranchTooDeep {pc = vm.state.pc})+ fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s () fetchAccount addr continue =+  let fallback = unexpectedSymArgW "trying to access a symbolic address that isn't already present in storage"+  in fetchAccountWithFallback addr fallback continue++-- | Construct RPC Query and halt execution until resolved+fetchAccountWithFallback :: VMOps t => Expr EAddr -> (Expr EAddr -> EVM t s ()) -> (Contract -> EVM t s ()) -> EVM t s ()+fetchAccountWithFallback addr fallback continue =   use (#env % #contracts % at addr) >>= \case     Just c -> continue c     Nothing -> case addr of-      SymAddr _ -> do-        pc <- use (#state % #pc)-        state <- use #state-        partial $ UnexpectedSymbolicArg pc (getOpName state) "trying to access a symbolic address that isn't already present in storage" (wrap [addr])+      SymAddr _ -> fallback addr       LitAddr a -> do         use (#cache % #fetched % at a) >>= \case           Just c -> do@@ -1403,15 +1405,15 @@           Nothing -> do             base <- use (#config % #baseState)             assign (#result) . Just . HandleEffect . Query $-              PleaseFetchContract a base-                (\c -> do assign (#cache % #fetched % at a) (Just c)-                          assign (#env % #contracts % at addr) (Just c)-                          assign #result Nothing-                          continue c)+              PleaseFetchContract a base $ \c -> do+                assign (#cache % #fetched % at a) (Just c)+                assign (#env % #contracts % at addr) (Just c)+                assign #result Nothing+                continue c       GVar _ -> internalError "Unexpected GVar"  accessStorage-  :: VMOps t => Expr EAddr+  :: (?conf :: Config, VMOps t) => Expr EAddr   -> Expr EWord   -> (Expr EWord -> EVM t s ())   -> EVM t s ()@@ -1446,13 +1448,11 @@         else do           modifying (#env % #contracts % ix addr % #storage) (writeStorage slot (Lit 0))           continue $ Lit 0-      mkQuery a s = query $-        PleaseFetchSlot a s-          (\x -> do+      mkQuery a s = query $ PleaseFetchSlot a s $ \x -> do               modifying (#cache % #fetched % ix a % #storage) (writeStorage (Lit s) (Lit x))               modifying (#env % #contracts % ix (LitAddr a) % #storage) (writeStorage (Lit s) (Lit x))               assign #result Nothing-              continue (Lit x))+              continue $ Lit x  accessTStorage   :: VMOps t => Expr EAddr@@ -1494,6 +1494,16 @@   -- TODO: handle symbolic balance...   && c.balance == Lit 0 +-- Adds constraints such that two symbolic addresses cannot alias each other+-- and symbolic addresses cannot alias concrete addresses+addAliasConstraints :: EVM t s ()+addAliasConstraints = do+  vm <- get+  let addrConstr = noClash $ Map.keys vm.env.contracts+  modifying #constraints ((++) addrConstr)+  where+    noClash addrs = [a ./= b | a <- addrs, b <- addrs, Expr.isSymAddr b, a < b]+ -- * How to finalize a transaction finalize :: VMOps t => EVM t s () finalize = do@@ -1501,6 +1511,7 @@     revertContracts  = use (#tx % #txReversion) >>= assign (#env % #contracts)     revertSubstate   = assign (#tx % #subState) (SubState mempty mempty mempty mempty mempty mempty) +  addAliasConstraints   use #result >>= \case     Just (VMFailure (Revert _)) -> do       revertContracts@@ -1513,22 +1524,16 @@     Just (VMSuccess output) -> do       clearTStorages       -- deposit the code from a creation tx-      pc' <- use (#state % #pc)       creation <- use (#tx % #isCreate)       createe  <- use (#state % #contract)       createeExists <- (Map.member createe) <$> use (#env % #contracts)       when (creation && createeExists) $         case output of-          ConcreteBuf bs ->-            replaceCode createe (RuntimeCode (ConcreteRuntimeCode bs))+          ConcreteBuf bs -> replaceCode createe (RuntimeCode (ConcreteRuntimeCode bs))           _ ->             case Expr.toList output of-              Nothing -> do-                state <- use #state-                partial $-                  UnexpectedSymbolicArg pc' (getOpName state) "runtime code cannot have an abstract length" (wrap [output])-              Just ops ->-                replaceCode createe (RuntimeCode (SymbolicRuntimeCode ops))+              Nothing -> unexpectedSymArg "runtime code cannot have an abstract length" [output]+              Just ops -> replaceCode createe (RuntimeCode (SymbolicRuntimeCode ops))     _ ->       internalError "Finalising an unfinished tx." @@ -1583,46 +1588,97 @@     then vmError StateChangeWhileStatic     else continue -forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()-forceAddr n msg continue = case wordToAddr n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])+-- Ensures the account `addr` exists on the VM environment.+-- Useful when `addr` needs to e.g. keep a eth balance or+-- be the source of contract deployments via pranks+touchAddress :: VMOps t => Expr EAddr -> EVM t s ()+touchAddress addr = do+  baseState <- use (#config % #baseState)+  let mkc = case baseState of+              AbstractBase -> unknownContract+              EmptyBase -> const emptyContract+  (#env % #contracts) %= (Map.insertWith (\_ e -> e) addr (mkc addr))++forceAddr :: (?conf :: Config, VMOps t) =>+  Expr EWord+  -> (Expr EWord -> EVM t s ())+  -> (Expr EAddr -> EVM t s ())+  -> EVM t s ()+forceAddr n fallback continue = case wordToAddr n of+  Nothing -> manySolutions (?conf).maxDepth n 20 $ \case+    Just sol -> continue $ LitAddr (truncateToAddr sol)+    Nothing -> fallback n   Just c -> continue c -forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()-forceConcrete n msg continue = case maybeLitWord n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])+unexpectedSymArg :: (Typeable a, VMOps t) => String -> [Expr a] -> EVM t s ()+unexpectedSymArg msg n = do+  pc <- use (#state % #pc)+  state <- use #state+  let opName = getOpName state+  partial $ UnexpectedSymbolicArg pc opName msg (wrap n)++unexpectedSymArgW :: (Typeable a, VMOps t) => String -> Expr a -> EVM t s ()+unexpectedSymArgW msg n = unexpectedSymArg msg [n]++unknownCode :: VMOps t => Expr EAddr -> EVM t s ()+unknownCode n = unexpectedSymArg "call target has unknown code" [n]++freshBufFallback :: (?conf :: Config, VMOps t, ?op :: Word8) => [Expr EWord] -> EVM t s ()+freshBufFallback xs = do+  -- Reset caller if needed+  resetCaller <- use $ #state % #resetCaller+  when resetCaller $ assign (#state % #overrideCaller) Nothing+  -- overapproximate by returning a symbolic value+  freshVar <- use #freshVar+  assign #freshVar (freshVar + 1)+  let opName = pack $ show $ getOp ?op+  let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)+  modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))+  let freshReturndataExpr = AbstractBuf (opName <> "-result-data-fresh-" <> (pack . show) freshVar)+  modifying #constraints ((:) (PLEq (bufLength freshReturndataExpr) (Lit (2 ^ ?conf.maxBufSize))))+  assign (#state % #returndata) freshReturndataExpr+  next >> assign (#state % #stack) (freshVarExpr:xs)++freshVarFallback:: (VMOps t, ?op :: Word8) => [Expr EWord] -> Expr a -> EVM t s ()+freshVarFallback xs _ = do+  -- Reset caller if needed+  resetCaller <- use $ #state % #resetCaller+  when resetCaller $ assign (#state % #overrideCaller) Nothing+  -- overapproximate by returning a symbolic value+  freshVar <- use #freshVar+  assign #freshVar (freshVar + 1)+  let opName = pack $ show $ getOp ?op+  let freshVarExpr = Var (opName <> "-result-stack-fresh-" <> (pack . show) freshVar)+  next >> assign (#state % #stack) (freshVarExpr:xs)++forceConcrete :: (?conf :: Config, VMOps t) => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()+forceConcrete n = forceConcreteLimitSz n 32++forceConcreteLimitSz :: (?conf :: Config, VMOps t) => Expr EWord -> Int -> String -> (W256 -> EVM t s ()) -> EVM t s ()+forceConcreteLimitSz n bytes msg continue = case maybeLitWordSimp n of+  Nothing -> manySolutions (?conf).maxDepth n bytes $ maybe fallback continue   Just c -> continue c+  where fallback = unexpectedSymArg msg [n] -forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()-forceConcreteAddr n msg continue = case maybeLitAddr n of-  Nothing -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])+forceConcreteAddr :: (?conf :: Config, VMOps t) => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()+forceConcreteAddr n msg continue = case maybeLitAddrSimp n of+  Nothing -> manySolutions (?conf).maxDepth (WAddr n) 20 $ maybe fallback $ \c -> continue (truncateToAddr c)   Just c -> continue c+  where fallback = unexpectedSymArg msg [n]  forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()-forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of+forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of   (Just c, Just d) -> continue (c,d)-  _ -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n, m])+  _ -> unexpectedSymArg msg [n, m]  forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()-forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of+forceConcrete2 (n,m) msg continue = case (maybeLitWordSimp n, maybeLitWordSimp m) of   (Just c, Just d) -> continue (c, d)-  _ -> do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n, m])+  _ -> unexpectedSymArg msg [n, m]  forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s () forceConcreteBuf (ConcreteBuf b) _ continue = continue b-forceConcreteBuf b msg _ = do-    vm <- get-    partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [b])+forceConcreteBuf b msg _ = unexpectedSymArg msg [b]  -- * Substate manipulation refund :: Word64 -> EVM t s ()@@ -1664,7 +1720,7 @@ accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool accessStorageForGas addr key = do   accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys)-  case maybeLitWord key of+  case maybeLitWordSimp key of     Just litword -> do       let accessed = member (addr, litword) accessedStrkeys       assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)@@ -1681,7 +1737,7 @@ cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")  cheat-  :: (?op :: Word8, VMOps t)+  :: forall t s . (?conf :: Config, ?op :: Word8, VMOps t)   => Gas t -> (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> [Expr EWord]   -> EVM t s () cheat gas (inOffset, inSize) (outOffset, outSize) xs = do@@ -1689,7 +1745,7 @@   input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))   calldata <- readMemory inOffset inSize   abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)-  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWord abi) calldata vm.env.contracts vm.tx.subState+  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWordSimp abi) calldata vm.env.contracts vm.tx.subState    pushTrace $ FrameTrace newContext   next@@ -1698,16 +1754,25 @@                     { state = vm1.state { stack = xs }                     , context = newContext                     }-  case maybeLitWord abi of-    Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])-    Just (unsafeInto -> abi') ->+  case maybeLitWordSimp abi of+    -- 4-byte function selector+    Nothing -> manySolutions (?conf).maxDepth abi 4 $ \case+      Just concAbi -> runCheat concAbi input+      Nothing -> unexpectedSymArg "symbolic cheatcode selector" [abi]+    Just concAbi -> runCheat concAbi input+  where+    runCheat :: W256 -> Expr 'Buf -> EVM t s ()+    runCheat abi input =  do+      let abi' = unsafeInto abi       case Map.lookup abi' cheatActions of-        Nothing -> vmError (BadCheatCode "Cannot understand cheatcode." abi')+        Nothing -> do+          vm <- get+          partial $ CheatCodeMissing vm.state.pc abi'         Just action -> action input  type CheatAction t s = Expr Buf -> EVM t s () -cheatActions :: VMOps t => Map FunctionSelector (CheatAction t s)+cheatActions :: (?conf :: Config, VMOps t) => Map FunctionSelector (CheatAction t s) cheatActions = Map.fromList   [ action "ffi(string[])" $       \sig input -> do@@ -1727,9 +1792,7 @@                 in query (PleaseDoFFI cmd vm.osEnv cont)               _ -> vmError (BadCheatCode "ffi(string[]) decoding of string failed" sig)             _ -> vmError (BadCheatCode "ffi(string[]) parameter decoding failed" sig)-        else-          let msg = "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"-          in partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg []+        else unexpectedSymArg "ffi disabled: run again with --ffi if you want to allow tests to call external scripts" ([] :: [Expr EWord])    , action "warp(uint256)" $       \sig input -> case decodeStaticArgs 0 1 input of@@ -1741,7 +1804,7 @@   , action "deal(address,uint256)" $       \sig input -> case decodeStaticArgs 0 2 input of         [a, amt] ->-          forceAddr a "vm.deal: cannot decode target into an address" $ \usr ->+          forceAddr a (unexpectedSymArgW "vm.deal: cannot decode target into an address") $ \usr ->             fetchAccount usr $ \_ -> do               assign (#env % #contracts % ix usr % #balance) amt               doStop@@ -1756,8 +1819,8 @@    , action "roll(uint256)" $       \sig input -> case decodeStaticArgs 0 1 input of-        [x] -> forceConcrete x "cannot roll to a symbolic block number" $ \block -> do-          assign (#block % #number) block+        [x] -> do+          assign (#block % #number) x           doStop         _ -> vmError (BadCheatCode "roll(uint256) parameter decoding failed" sig) @@ -1918,7 +1981,7 @@         SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of           Lit 1 -> frameRevert "assertion failed"           Lit 0 -> doStop-          ew -> branch ew $ \case+          ew -> branch (?conf).maxDepth ew $ \case             True -> frameRevert "assertion failed"             False -> doStop         k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig@@ -1929,7 +1992,7 @@         SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of           Lit 0 -> frameRevert "assertion failed"           Lit 1 -> doStop-          ew -> branch ew $ \case+          ew -> branch (?conf).maxDepth ew $ \case             False -> frameRevert "assertion failed"             True -> doStop         k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig@@ -1948,13 +2011,13 @@   , action "assertNotEq(string,string)"   $ assertNotEq (AbiStringType)   --   , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)-  , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)+  , action "assertLt(int256,int256)"   $ assertSLt (AbiIntType 256)   , action "assertLe(uint256,uint256)" $ assertLe (AbiUIntType 256)-  , action "assertLe(int256,int256)"   $ assertLe (AbiIntType 256)+  , action "assertLe(int256,int256)"   $ assertSLe (AbiIntType 256)   , action "assertGt(uint256,uint256)" $ assertGt (AbiUIntType 256)-  , action "assertGt(int256,int256)"   $ assertGt (AbiIntType 256)+  , action "assertGt(int256,int256)"   $ assertSGt (AbiIntType 256)   , action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)-  , action "assertGe(int256,int256)"   $ assertGe (AbiIntType 256)+  , action "assertGe(int256,int256)"   $ assertSGe (AbiIntType 256)   ]   where     action s f = (abiKeccak s, f (abiKeccak s))@@ -2005,22 +2068,25 @@         SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ exprComp ew1 ew2)) of           Lit 0 -> doStop           Lit _ -> revertErr ew1 ew2 invComp-          ew -> branch ew $ \case+          ew -> branch (?conf).maxDepth ew $ \case             False -> doStop             True -> revertErr ew1 ew2 invComp         abivals -> vmError (BadCheatCode (paramDecodeErr abitype name abivals) sig)-    assertEq = genAssert (==) Expr.eq "!=" "assertEq"+    assertEq =    genAssert (==) Expr.eq "!=" "assertEq"     assertNotEq = genAssert (/=) (\a b -> Expr.iszero $ Expr.eq a b) "==" "assertNotEq"-    assertLt = genAssert (<) Expr.lt ">=" "assertLt"-    assertGt = genAssert (>) Expr.gt "<=" "assertGt"-    assertLe = genAssert (<=) Expr.leq ">" "assertLe"-    assertGe = genAssert (>=) Expr.geq "<" "assertGe"-+    assertLt =    genAssert (<)  Expr.lt ">=" "assertLt"+    assertSLt =   genAssert (<)  Expr.slt ">=" "assertLt"+    assertGt =    genAssert (>)  Expr.gt "<=" "assertGt"+    assertSGt =   genAssert (>)  Expr.sgt "<=" "assertGt"+    assertLe =    genAssert (<=) Expr.leq ">" "assertLe"+    assertSLe =   genAssert (<=) (\a b -> Expr.iszero $ Expr.sgt a b) ">" "assertLe"+    assertGe =    genAssert (>=) Expr.geq "<" "assertGe"+    assertSGe =   genAssert (>=) (\a b -> Expr.iszero $ Expr.slt a b) "<" "assertGe"  -- * General call implementation ("delegateCall") -- note that the continuation is ignored in the precompile case delegateCall-  :: (VMOps t, ?op :: Word8)+  :: (VMOps t, ?op :: Word8, ?conf :: Config)   => Contract   -> Gas t   -> Expr EAddr@@ -2031,9 +2097,10 @@   -> Expr EWord   -> Expr EWord   -> [Expr EWord]-  -> (Expr EAddr -> EVM t s ())+  -> (Expr EAddr -> EVM t s ()) -- fallback+  -> (Expr EAddr -> EVM t s ()) -- continue   -> EVM t s ()-delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue+delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs fallback continue   | isPrecompileAddr xTo       = forceConcreteAddr2 (xTo, xContext) "Cannot call precompile with symbolic addresses" $           \(xTo', xContext') ->@@ -2046,15 +2113,12 @@           resetCaller <- use $ #state % #resetCaller           when resetCaller $ assign (#state % #overrideCaller) Nothing           vm0 <- get-          fetchAccount xTo $ \target -> case target.code of-              UnknownCode _ -> do-                pc <- use (#state % #pc)-                state <- use #state-                partial $ UnexpectedSymbolicArg pc (getOpName state) "call target has unknown code" (wrap [xTo])+          fetchAccountWithFallback xTo fallback $ \target -> case target.code of+              UnknownCode _ -> fallback xTo               _ -> do                 burn' xGas $ do                   calldata <- readMemory xInOffset xInSize-                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)+                  abi <- maybeLitWordSimp . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)                   let newContext = CallContext                                     { target    = xTo                                     , context   = xContext@@ -2078,7 +2142,7 @@                         (InitCode _ _) -> InitCode mempty mempty                         a -> a -                  newMemory <- ConcreteMemory <$> VUnboxed.Mutable.new 0+                  newMemory <- ConcreteMemory <$> VS.Mutable.new 0                   zoom #state $ do                     assign #gas xGas                     assign #pc 0@@ -2104,28 +2168,35 @@     _ -> True   Nothing -> False -create :: forall t s. (?op :: Word8, VMOps t)+create :: forall t s. (?op :: Word8, ?conf::Config, VMOps t)   => Expr EAddr -> Contract   -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s () create self this xSize xGas xValue xs newAddr initCode = do   vm0 <- get+  -- are we exceeding the max init code size   if xSize > Lit (vm0.block.maxCodeSize * 2)   then do     assign (#state % #stack) (Lit 0 : xs)     assign (#state % #returndata) mempty     vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize+  -- are we overflowing the nonce   else if this.nonce == Just maxBound   then do     assign (#state % #stack) (Lit 0 : xs)     assign (#state % #returndata) mempty     pushTrace $ ErrorTrace NonceOverflow     next+  -- are we overflowing the stack   else if length vm0.frames >= 1024   then do     assign (#state % #stack) (Lit 0 : xs)     assign (#state % #returndata) mempty     pushTrace $ ErrorTrace CallDepthLimitReached     next+  -- are we deploying to an address that already has a contract?+  -- note: the symbolic interpreter generates constraints ensuring that+  -- symbolic storage keys cannot alias other storage keys, making this check+  -- safe to perform statically   else if collision $ Map.lookup newAddr vm0.env.contracts   then burn' xGas $ do     assign (#state % #stack) (Lit 0 : xs)@@ -2133,7 +2204,7 @@     modifying (#env % #contracts % ix self % #nonce) (fmap ((+) 1))     next   -- do we have enough balance-  else branch (Expr.gt xValue this.balance) $ \case+  else branch (?conf).maxDepth (Expr.gt xValue this.balance) $ \case       True -> do         assign (#state % #stack) (Lit 0 : xs)         assign (#state % #returndata) mempty@@ -2144,8 +2215,7 @@       -- are we overflowing the nonce       False -> burn' xGas $ do         case parseInitCode initCode of-          Nothing ->-            partial $ UnexpectedSymbolicArg vm0.state.pc (getOpName vm0.state) "initcode must have a concrete prefix" []+          Nothing -> unexpectedSymArg "initcode must have a concrete prefix" ([] :: [Expr EWord])           Just c -> do             let               newContract = initialContract c@@ -2267,6 +2337,15 @@   | FrameErrored EvmError -- ^ Any other error   deriving Show +finishAllFramesAndStop :: VMOps t => EVM t s ()+finishAllFramesAndStop = do+  vm <- get+  case vm.frames of+    [] -> finishFrame (FrameReturned mempty)+    _ -> do+      finishFrame (FrameReturned mempty)+      finishAllFramesAndStop+ -- | This function defines how to pop the current stack frame in either of -- the ways specified by 'FrameResult'. --@@ -2461,8 +2540,7 @@             assign (#state % #memory) $               SymbolicMemory $ copySlice srcOffset memOffset size bs buf       SymbolicMemory mem ->-        assign (#state % #memory) $-          SymbolicMemory $ copySlice srcOffset memOffset size bs mem+        assign (#state % #memory) $ SymbolicMemory $ copySlice srcOffset memOffset size bs mem  copyCallBytesToMemory   :: Expr Buf -> Expr EWord -> Expr EWord -> EVM t s ()@@ -2476,7 +2554,7 @@     ConcreteMemory mem -> do       case (offset', size') of         (Lit offset, Lit size) -> do-          let memSize :: Word64 = unsafeInto (VUnboxed.Mutable.length mem)+          let memSize :: Word64 = unsafeInto (VS.Mutable.length mem)           if size > Expr.maxBytes ||              offset + size > Expr.maxBytes ||              offset >= into memSize then@@ -2486,8 +2564,8 @@             let pastEnd = (unsafeInto offset + unsafeInto size) - unsafeInto memSize             let fromMemSize = if pastEnd > 0 then unsafeInto size - pastEnd else unsafeInto size -            buf <- VUnboxed.freeze $ VUnboxed.Mutable.slice (unsafeInto offset) fromMemSize mem-            let dataFromMem = BS.pack $ VUnboxed.toList buf+            buf <- VS.freeze $ VS.Mutable.slice (unsafeInto offset) fromMemSize mem+            let dataFromMem = vectorToByteString buf             pure $ ConcreteBuf $ dataFromMem <> BS.replicate pastEnd 0         _ -> do           buf <- freezeMemory mem@@ -2504,7 +2582,7 @@   pure Trace     { tracedata = x     , contract = this-    , opIx = fromMaybe 0 $ this.opIxMap SV.!? vm.state.pc+    , opIx = fromMaybe 0 $ this.opIxMap VS.!? vm.state.pc     }  pushTrace :: TraceData -> EVM t s ()@@ -2651,10 +2729,12 @@       UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"       InitCode ops _ -> BS.indexMaybe ops x       RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x-      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte+      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByteSimp   in case op of        Nothing -> False-       Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))+       Just b -> 0x5b == b && (isJust $ contract.opIxMap VS.!? x)+         && (isJust $ contract.codeOps V.!? (contract.opIxMap VS.! x))+         && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap VS.! x))  opSize :: Word8 -> Int opSize x | x >= 0x60 && x <= 0x7f = into x - 0x60 + 2@@ -2663,10 +2743,10 @@ --  i of the resulting vector contains the operation index for -- the program counter value i.  This is needed because source map -- entries are per operation, not per byte.-mkOpIxMap :: ContractCode -> SV.Vector Int+mkOpIxMap :: ContractCode -> VS.Vector Int mkOpIxMap (UnknownCode _) = internalError "Cannot build opIxMap for unknown code" mkOpIxMap (InitCode conc _)-  = SV.create $ SV.new (BS.length conc) >>= \v ->+  = VS.create $ VS.Mutable.new (BS.length conc) >>= \v ->       -- Loop over the byte string accumulating a vector-mutating action.       -- This is somewhat obfuscated, but should be fast.       let (_, _, _, m) = BS.foldl' (go v) (0 :: Word8, 0, 0, pure ()) conc@@ -2674,34 +2754,34 @@       where         -- concrete case         go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =-          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> SV.write v i j)+          {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> VS.Mutable.write v i j)         go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> VS.Mutable.write v i j)         go v (0, !i, !j, !m) _ =-          {- Other op. -}         (0,            i + 1, j + 1, m >> SV.write v i j)+          {- Other op. -}         (0,            i + 1, j + 1, m >> VS.Mutable.write v i j)         go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> VS.Mutable.write v i j)  mkOpIxMap (RuntimeCode (ConcreteRuntimeCode ops)) =   mkOpIxMap (InitCode ops mempty) -- a bit hacky  mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))-  = SV.create $ SV.new (length ops) >>= \v ->+  = VS.create $ VS.Mutable.new (length ops) >>= \v ->       let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)       in m >> pure v       where-        go v (0, !i, !j, !m) x = case maybeLitByte x of+        go v (0, !i, !j, !m) x = case maybeLitByteSimp x of           Just x' -> if x' >= 0x60 && x' <= 0x7f             -- start of PUSH op ---                     then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)+                     then (x' - 0x60 + 1, i + 1, j,     m >> VS.Mutable.write v i j)             -- other data ---                     else (0,             i + 1, j + 1, m >> SV.write v i j)+                     else (0,             i + 1, j + 1, m >> VS.Mutable.write v i j)           _ -> internalError $ "cannot analyze symbolic code:\nx: " <> show x <> " i: " <> show i <> " j: " <> show j          go v (1, !i, !j, !m) _ =-          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> SV.write v i j)+          {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> VS.Mutable.write v i j)         go v (n, !i, !j, !m) _ =-          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> SV.write v i j)+          {- PUSH data. -}        (n - 1,        i + 1, j,     m >> VS.Mutable.write v i j)   vmOp :: VM t s -> Maybe Op@@ -2715,7 +2795,7 @@         RuntimeCode (ConcreteRuntimeCode xs') ->           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')         RuntimeCode (SymbolicRuntimeCode xs') ->-          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')+          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByteSimp $ xs' V.! i , V.toList $ V.drop i xs')   in if (opslen code' < i)      then Nothing      else Just (readOp op pushdata)@@ -2723,7 +2803,7 @@ vmOpIx :: VM t s -> Maybe Int vmOpIx vm =   do self <- currentContract vm-     self.opIxMap SV.!? vm.state.pc+     self.opIxMap VS.!? vm.state.pc  -- Maps operation indices into a pair of (bytecode index, operation) mkCodeOps :: ContractCode -> V.Vector (Int, Op)@@ -2743,7 +2823,7 @@         Nothing ->           mempty         Just (x, xs') ->-          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByteSimp x               j = opSize x'           in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs) @@ -2890,13 +2970,21 @@ writeMemory :: MutableMemory s -> Int -> ByteString -> EVM t s () writeMemory memory offset buf = do   memory' <- expandMemory (offset + BS.length buf)-  mapM_ (uncurry (VUnboxed.Mutable.write memory'))+  mapM_ (uncurry (VS.Mutable.write memory'))         (zip [offset..] (BS.unpack buf))   where-  expandMemory targetSize = do-    let toAlloc = targetSize - VUnboxed.Mutable.length memory+  expandMemory requiredSize = do+    let currentSize = VS.Mutable.length memory+    let toAlloc = requiredSize - currentSize     if toAlloc > 0 then do-      memory' <- VUnboxed.Mutable.grow memory toAlloc+      -- As grow does a larger *copy* of the vector on a new place,+      -- we double the vector size to avoid the performance impact+      -- that would happen with repeated small expansion operations.+      let growthFactor = 2+      let targetSize = requiredSize * growthFactor+      -- Always grow at least 8k+      let toGrow = max 8192 $ targetSize - currentSize+      memory' <- VS.Mutable.grow memory toGrow       assign (#state % #memory) (ConcreteMemory memory')       pure memory'     else@@ -2904,7 +2992,7 @@  freezeMemory :: MutableMemory s -> EVM t s (Expr Buf) freezeMemory memory =-  ConcreteBuf . BS.pack . VUnboxed.toList <$> VUnboxed.freeze memory+  ConcreteBuf . vectorToByteString <$> VS.freeze memory   instance VMOps Symbolic where@@ -2927,21 +3015,22 @@   pushGas = do     modifying (#env % #freshGasVals) (+ 1)     n <- use (#env % #freshGasVals)-    pushSym $ Expr.Gas n+    pushSym $ Expr.Gas "" n   enoughGas _ _ = True   subGas _ _ = ()   toGas _ = ()   whenSymbolicElse a _ = a -  partial e = assign #result (Just (Unfinished e))-  branch cond continue = do+  partial e = assign #result $ Just (Unfinished e)+  branch depthLimit cond continue = do     loc <- codeloc     pathconds <- use #constraints-    query $ PleaseAskSMT cond pathconds (choosePath loc)+    vm <- get+    query $ PleaseAskSMT cond pathconds (runBothPaths loc vm.exploreDepth)     where       condSimp = Expr.simplify cond       condSimpConc = Expr.concKeccakSimpExpr condSimp-      choosePath loc (Case v) = do+      runBothPaths loc _ (Case v) = do         assign #result Nothing         pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0)                                    else Expr.simplifyProp (condSimpConc .== Lit 0)@@ -2951,9 +3040,36 @@         assign (#iterations % at loc) (Just (iteration + 1, stack))         continue v       -- Both paths are possible; we ask for more input-      choosePath loc Unknown =-        choose . PleaseChoosePath condSimp $ choosePath loc . Case+      runBothPaths loc exploreDepth UnknownBranch =+        (runBoth depthLimit exploreDepth ) . PleaseRunBoth condSimp $ (runBothPaths loc exploreDepth) . Case +  -- numBytes allows us to specify how many bytes of the returned value is relevant+  -- if it's e.g.a JUMP, only 2 bytes can be relevant. This allows us to avoid+  -- getting solutions that are nonsensical+  manySolutions depthLimit ewordExpr numBytes continue = do+    pathconds <- use #constraints+    vm <- get+    query $ PleaseGetSols ewordExpr numBytes pathconds $ \case+      Just concVals -> do+        assign #result Nothing+        case concVals of+          -- zero solutions means that we are in a branch that's not possible+          -- so revert all frames and stop all execution on this branch+          [] -> finishAllFramesAndStop+          [val] -> do+            assign #result Nothing+            pushTo #constraints $ Expr.simplifyProp (ewordExpr .== (Lit val))+            continue $ Just val+          _ -> runAll depthLimit vm.exploreDepth $ PleaseRunAll ewordExpr concVals runAllPaths+      Nothing -> do+        assign #result Nothing+        continue Nothing+    where+      runAllPaths val = do+        assign #result Nothing+        pushTo #constraints $ Expr.simplifyProp (ewordExpr .== Lit val)+        continue $ Just val+ instance VMOps Concrete where   burn' n continue = do     available <- use (#state % #gas)@@ -3076,16 +3192,12 @@     push (into vm.state.gas)    enoughGas cost gasCap = cost <= gasCap-   subGas gasCap cost = gasCap - cost-   toGas = id-   whenSymbolicElse _ a = a-   partial _ = internalError "won't happen during concrete exec"--  branch (forceLit -> cond) continue = continue (cond > 0)+  branch _ (forceLit -> cond) continue = continue (cond > 0)+  manySolutions _ _ _ = internalError "SMT solver should never be needed in concrete mode"  -- Create symbolic VM from concrete VM symbolify :: VM Concrete s -> VM Symbolic s

@@ -60,6 +60,7 @@  import EVM.Expr (readWord, isLitWord) import EVM.Types+import EVM.Expr (maybeLitWordSimp)  import Control.Applicative ((<|>)) import Control.Monad (replicateM, replicateM_, forM_, void)@@ -511,7 +512,7 @@   else     let       vs = decodeStaticArgs 0 (length tps) buf-      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)+      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWordSimp vs)     in if not (all isLitWord vs)        then SAbi vs        else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of

@@ -4,6 +4,7 @@ import EVM.Concrete import EVM.Solidity import EVM.Types+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp)  import Control.Arrow ((>>>), second) import Data.Aeson (Value)@@ -26,7 +27,6 @@   , solcByHash :: Map W256 (CodeType, SolcContract)   , solcByCode :: [(Code, SolcContract)] -- for contracts with `immutable` vars.   , sources    :: SourceCache-  , unitTests  :: [(Text, [Sig])]   , abiMap     :: Map FunctionSelector Method   , eventMap   :: Map W256 Event   , errorMap   :: Map W256 SolError@@ -56,7 +56,6 @@    in DappInfo     { root = root-    , unitTests = findAllUnitTests solcs     , sources = sources     , solcByName = cs     , solcByHash =@@ -91,37 +90,33 @@ unitTestMarkerAbi :: FunctionSelector unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()") -findAllUnitTests :: [SolcContract] -> [(Text, [Sig])]-findAllUnitTests = findUnitTests ".*:.*\\.(check|prove).*"--mkSig :: Method -> Maybe Sig-mkSig method-  | "prove" `isPrefixOf` testname = Just (Sig testname argtypes)-  | "check" `isPrefixOf` testname = Just (Sig testname argtypes)+mkSig :: Text -> Method -> Maybe Sig+mkSig prefix method+  | prefix `isPrefixOf` testname = Just (Sig testname argtypes)   | otherwise = Nothing   where     testname = method.name     argtypes = snd <$> method.inputs -findUnitTests :: Text -> ([SolcContract] -> [(Text, [Sig])])-findUnitTests match =+findUnitTests :: Text -> Text -> ([SolcContract] -> [(Text, [Sig])])+findUnitTests prefix match =   concatMap $ \c ->     case Map.lookup unitTestMarkerAbi c.abiMap of       Nothing -> []       Just _  ->-        let testNames = unitTestMethodsFiltered (regexMatches match) c+        let testNames = unitTestMethodsFiltered prefix (regexMatches match) c         in [(c.contractName, testNames) | not (BS.null c.runtimeCode) && not (null testNames)] -unitTestMethodsFiltered :: (Text -> Bool) -> (SolcContract -> [Sig])-unitTestMethodsFiltered matcher c =+unitTestMethodsFiltered :: Text -> (Text -> Bool) -> (SolcContract -> [Sig])+unitTestMethodsFiltered prefix matcher c =   let testName (Sig n _) = c.contractName <> "." <> n-  in filter (matcher . testName) (unitTestMethods c)+  in filter (matcher . testName) (unitTestMethods prefix c) -unitTestMethods :: SolcContract -> [Sig]-unitTestMethods =+unitTestMethods :: Text -> SolcContract -> [Sig]+unitTestMethods prefix =   (.abiMap)   >>> Map.elems-  >>> mapMaybe mkSig+  >>> mapMaybe (mkSig prefix)  traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap traceSrcMap dapp trace = srcMap dapp trace.contract trace.opIx@@ -138,7 +133,7 @@  findSrc :: Contract -> DappInfo -> Maybe SolcContract findSrc c dapp = do-  hash <- maybeLitWord c.codehash+  hash <- maybeLitWordSimp c.codehash   case Map.lookup hash dapp.solcByHash of     Just (_, v) -> Just v     Nothing -> lookupCode c.code dapp@@ -153,7 +148,7 @@     Just x -> pure x     Nothing -> snd <$> find (compareCode c . fst) a.solcByCode lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let-    code = BS.pack $ mapMaybe maybeLitByte $ V.toList c+    code = BS.pack $ mapMaybe maybeLitByteSimp $ V.toList c   in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of     Just x -> pure x     Nothing -> snd <$> find (compareCode code . fst) a.solcByCode

@@ -43,6 +43,12 @@    -- Returns Unknown if the Cex cannot be found via fuzzing   , onlyCexFuzz      :: Bool   , decomposeStorage :: Bool+  , promiseNoReent   :: Bool+  , maxBufSize       :: Int+  , maxWidth         :: Int+  , maxDepth         :: Maybe Int+  , verb             :: Int+  , simp             :: Bool   }   deriving (Show, Eq) @@ -56,6 +62,12 @@   , numCexFuzz = 10   , onlyCexFuzz  = False   , decomposeStorage = True+  , promiseNoReent = False+  , maxBufSize = 64+  , maxWidth = 100+  , maxDepth = Nothing+  , verb = 0+  , simp = True   }  -- Write to the console

@@ -10,6 +10,7 @@ import Data.Maybe (isNothing) import Optics.Core import Control.Monad.ST (ST)+import EVM.Effects (Config)  ethrunAddress :: Addr ethrunAddress = Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72@@ -26,7 +27,7 @@     , caller = LitAddr ethrunAddress     , origin = LitAddr ethrunAddress     , coinbase = LitAddr 0-    , number = 0+    , number = Lit 0     , timestamp = Lit 0     , blockGaslimit = 0     , gasprice = 0@@ -46,18 +47,18 @@     }) <&> set (#env % #contracts % at (LitAddr ethrunAddress))              (Just (initialContract (RuntimeCode (ConcreteRuntimeCode "")))) -exec :: VMOps t => EVM t s (VMResult t s)-exec = do+exec :: (VMOps t) => Config -> EVM t s (VMResult t s)+exec conf = do   vm <- get   case vm.result of-    Nothing -> exec1 >> exec+    Nothing -> exec1 conf >> exec conf     Just r -> pure r -run :: VMOps t => EVM t s (VM t s)-run = do+run :: (VMOps t) => Config -> EVM t s (VM t s)+run conf = do   vm <- get   case vm.result of-    Nothing -> exec1 >> run+    Nothing -> exec1 conf >> run conf     Just _ -> pure vm  execWhile :: (VM t s -> Bool) -> State (VM t s) Int

@@ -15,6 +15,7 @@ import Data.ByteString qualified as BS import Data.DoubleWord (Int256, Word256(Word256), Word128(Word128)) import Data.List+import Data.Map qualified as LMap import Data.Map.Strict qualified as Map import Data.Maybe (mapMaybe, isJust, fromMaybe) import Data.Semigroup (Any, Any(..), getAny)@@ -39,6 +40,12 @@ maxLit :: W256 maxLit = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff +maxLitSigned :: W256+maxLitSigned = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff++minLitSigned :: W256+minLitSigned = 0x1000000000000000000000000000000000000000000000000000000000000000+ -- ** Stack Ops ** ---------------------------------------------------------------------------------  @@ -60,14 +67,11 @@ op3 _ concrete (Lit x) (Lit y) (Lit z) = Lit (concrete x y z) op3 symbolic _ x y z = symbolic x y z --- | If a given binary op is commutative, then we always force Lits to the lhs if--- only one argument is a Lit. This makes writing pattern matches in the--- simplifier easier.+-- | If a given binary op is commutative, then we always order the arguments.+-- This makes writing pattern matches in the simplifier easier.+-- It will also force Lit to be the 1st argument, since Lit is the 1st element of Expr (see Types.hs). normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord-normArgs sym conc l r = case (l, r) of-  (Lit _, _) -> doOp l r-  (_, Lit _) -> doOp r l-  _ -> doOp l r+normArgs sym conc l r = if l <= r then doOp l r else doOp r l   where     doOp = op2 sym conc @@ -105,14 +109,12 @@  addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord addmod = op3 AddMod (\x y z ->-  if z == 0-  then 0+  if z == 0 then 0   else fromIntegral $ (into @Word512 x + into y) `Prelude.mod` into z)  mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord mulmod = op3 MulMod (\x y z ->-  if z == 0-  then 0+  if z == 0 then 0   else fromIntegral $ (into @Word512 x * into y) `Prelude.mod` into z)  exp :: Expr EWord -> Expr EWord -> Expr EWord@@ -195,7 +197,7 @@ sar = op2 SAR (\x y ->   let msb = testBit y 255       asSigned = fromIntegral y :: Int256-  in if x > 256 then+  in if x >= 255 then        if msb then maxBound else 0      else        fromIntegral $ shiftR asSigned (fromIntegral x))@@ -205,12 +207,20 @@  peq :: (Typeable a) => Expr a -> Expr a -> Prop peq (Lit x) (Lit y) = PBool (x == y)-peq a@(Lit _) b = PEq a b-peq a b@(Lit _) = PEq b a -- we always put concrete values on LHS+peq (LitAddr x) (LitAddr y) = PBool (x == y)+peq (LitByte x) (LitByte y) = PBool (x == y)+peq (ConcreteBuf x) (ConcreteBuf y) = PBool (x == y) peq a b   | a == b = PBool True-  | otherwise = PEq a b+  | otherwise = let args = sort [a, b]+     in PEq (args !! 0) (args !! 1) +pleq :: Expr EWord -> Expr EWord -> Prop+pleq (Lit a) (Lit b) = PBool (a <= b)+pleq a b+  | a == b = PBool True+  | otherwise = PLEq a b+ -- ** Bufs ** --------------------------------------------------------------------------------------  @@ -242,6 +252,9 @@            (Lit _) -> indexWord (Lit $ x - idx) val            _ -> IndexWord (Lit $ x - idx) val     else readByte i src+-- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from dst+readByte i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x =+  readByte i dst readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst)   = if x - dstOffset < size     then readByte (Lit $ x - (dstOffset - srcOffset)) src@@ -278,6 +291,9 @@     -- we do not have enough information to statically determine whether or not     -- the region we want to read overlaps the WriteWord     _ -> readWordFromBytes idx b+-- reading a Word that is lower than the dstOffset-32 of a CopySlice, so it's just reading from dst+readWord i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset >= x+32 =+  readWord i dst readWord (Lit idx) b@(CopySlice (Lit srcOff) (Lit dstOff) (Lit size) src dst)   -- the region we are trying to read is enclosed in the sliced region   | (idx - dstOff) < size && 32 <= size - (idx - dstOff) = readWord (Lit $ srcOff + (idx - dstOff)) src@@ -297,7 +313,7 @@ readWordFromBytes i@(Lit idx) buf = let     bytes = [readByte (Lit i') buf | i' <- [idx .. idx + 31]]   in if all isLitByte bytes-     then Lit (bytesToW256 . mapMaybe maybeLitByte $ bytes)+     then Lit (bytesToW256 . mapMaybe maybeLitByteSimp $ bytes)      else ReadWord i buf readWordFromBytes idx buf = ReadWord idx buf @@ -351,8 +367,8 @@     hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst     sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]]     tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst-    in if Prelude.and . (fmap isLitByte) $ sl-       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByte) $ sl) <> tl+    in if all isLitByte sl+       then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByteSimp) $ sl) <> tl        else CopySlice s d sz src ds   | otherwise = CopySlice s d sz src ds @@ -529,8 +545,8 @@   _ -> Nothing  fromList :: V.Vector (Expr Byte) -> Expr Buf-fromList bs = case Prelude.and (fmap isLitByte bs) of-  True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByte $ bs+fromList bs = case all isLitByte bs of+  True -> ConcreteBuf . vectorToByteString . VS.convert $ V.map getLitByte bs   -- we want to minimize the size of the resulting expression, so we do two passes:   --   1. write all concrete bytes to some base buffer   --   2. write all symbolic writes on top of this buffer@@ -538,17 +554,21 @@   -- runs in O(2n) time, and has pretty minimal allocation & copy overhead in   -- the concrete part (a single preallocated vec, with no copies)   False -> V.ifoldl' applySymWrites (ConcreteBuf concreteBytes) bs-    where-      concreteBytes :: ByteString-      concreteBytes = vectorToByteString $ VS.generate (V.length bs) (\idx ->-        case bs V.! idx of-          LitByte b -> b-          _ -> 0)+  where+    getLitByte :: (Expr Byte) -> Word8+    getLitByte (LitByte w) = w+    getLitByte _ = internalError "Impossible!" -      applySymWrites :: Expr Buf -> Int -> Expr Byte -> Expr Buf-      applySymWrites buf _ (LitByte _) = buf-      applySymWrites buf idx by = WriteByte (Lit $ unsafeInto idx) by buf+    concreteBytes :: ByteString+    concreteBytes = vectorToByteString $ VS.generate (V.length bs) (\idx ->+      case bs V.! idx of+        LitByte b -> b+        _ -> 0) +    applySymWrites :: Expr Buf -> Int -> Expr Byte -> Expr Buf+    applySymWrites buf _ (LitByte _) = buf+    applySymWrites buf idx by = WriteByte (Lit $ unsafeInto idx) by buf+ instance Semigroup (Expr Buf) where   (ConcreteBuf a) <> (ConcreteBuf b) = ConcreteBuf $ a <> b   a <> b = copySlice (Lit 0) (bufLength a) (bufLength b) b a@@ -617,7 +637,7 @@ -- test for an example where this happens. Note that decomposition solves this, though late in -- the simplification lifecycle (just before SMT generation, which can be too late) readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)-readStorage w st = go (simplify w) st+readStorage w st = go (simplifyNoLitToKeccak w) (simplifyNoLitToKeccak st)   where     go :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)     go _ (GVar _) = internalError "Can't read from a GVar"@@ -627,21 +647,23 @@     go slot s@(SStore prevSlot val prev) = case (prevSlot, slot) of       -- if address and slot match then we return the val in this write       _ | prevSlot == slot -> Just val--      -- if the slots don't match (see previous guard) and are lits, we can skip this write-      (Lit _, Lit _) -> go slot prev+      (a, b) | surelyEqual a b -> Just val+      (a, b) | surelyNotEqual a b -> go slot prev        -- slot is for a map + map -> skip write-      (MappingSlot idA _, MappingSlot idB _)       | BS.length idB == 64 && BS.length idA == 64 && idsDontMatch idA idB  -> go slot prev-      (MappingSlot idA keyA, MappingSlot idB keyB) | BS.length idB == 64 && BS.length idA == 64 && surelyNotEq keyA keyB -> go slot prev+      (MappingSlot idA _, MappingSlot idB _)       | isMap' idB, isMap' idA, idsDontMatch idA idB  -> go slot prev+      (MappingSlot idA keyA, MappingSlot idB keyB) | isMap' idB, isMap' idA, surelyNotEqual keyA keyB -> go slot prev        -- special case of array + map -> skip write-      (ArraySlotWithOffs idA _, Keccak   k)      | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev-      (ArraySlotZero idA, Keccak k)              | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev+      (ArraySlotWithOffs idA _, Keccak k)          | isMap k, isArray idA -> go slot prev+      (ArraySlotWithOffs2 idA _ _, Keccak k)       | isMap k, isArray idA -> go slot prev+      (ArraySlotZero idA, Keccak k)                | isMap k, isArray idA -> go slot prev        -- special case of map + array -> skip write-      (Keccak k, ArraySlotWithOffs idA _)      | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev-      (ArraySlotWithOffs idA _, Keccak k)      | bufLength k == Lit 64 && BS.length idA == 32 -> go slot prev+      (Keccak k, ArraySlotWithOffs idA _)          | isMap k, isArray idA -> go slot prev+      (Keccak k, ArraySlotWithOffs2 idA _ _)       | isMap k, isArray idA -> go slot prev+      (ArraySlotWithOffs idA _, Keccak k)          | isMap k, isArray idA -> go slot prev+      (ArraySlotWithOffs2 idA _ _, Keccak k)       | isMap k, isArray idA -> go slot prev        -- Fixed SMALL value will never match Keccak (well, it might, but that's VERY low chance)       (Lit a, Keccak _) | a < 256 -> go slot prev@@ -652,12 +674,8 @@       -- occurring here is 2^32/2^256 = 2^-224, which is close enough to zero       -- for our purposes. This lets us completely simplify reads from write       -- chains involving writes to arrays at literal offsets.-      (Lit a, Add (Lit b) (Keccak _) ) | a < 256, b < maxW32 -> go slot prev-      (Add (Lit a) (Keccak _) , Lit b) | b < 256, a < maxW32 -> go slot prev--      --- NOTE these are needed to succeed in rewriting arrays with a variable index-      -- (Lit a, Add (Keccak _) (Var _) ) | a < 256 -> go slot prev-      -- (Add (Keccak _) (Var _) , Lit b) | b < 256 -> go slot prev+      (Lit a, Add (Lit b) (Keccak _)) | a < 256, b < maxW32 -> go slot prev+      (Add (Lit a) (Keccak _) ,Lit b) | b < 256, a < maxW32 -> go slot prev        -- Finding two Keccaks that are < 256 away from each other should be VERY hard       -- This simplification allows us to deal with maps of structs@@ -665,48 +683,65 @@       (Add (Lit a2) (Keccak _), (Keccak _)) | a2 > 0, a2 < 256 -> go slot prev       ((Keccak _), Add (Lit b2) (Keccak _)) | b2 > 0, b2 < 256 -> go slot prev -      -- case of array + array, but different id's or different concrete offsets       -- zero offs vs zero offs-      (ArraySlotZero idA, ArraySlotZero idB)                   | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev+      (ArraySlotZero idA, ArraySlotZero idB)                   | isArray idA, isArray idB, idA /= idB -> go slot prev+       -- zero offs vs non-zero offs-      (ArraySlotZero idA, ArraySlotWithOffs idB _)             | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev-      (ArraySlotZero idA, ArraySlotWithOffs idB (Lit offB))    | BS.length idA == 32, BS.length idB == 32, offB /= 0  -> go slot prev+      (ArraySlotZero idA, ArraySlotWithOffs idB _)             | isArray idA, isArray idB, idA /= idB -> go slot prev+      (ArraySlotZero idA, ArraySlotWithOffs idB (Lit offB))    | isArray idA, idA == idB, offB /= 0  -> go slot prev+      (ArraySlotZero idA, ArraySlotWithOffs2 idB _ _)          | isArray idA, isArray idB, idA /= idB -> go slot prev+       -- non-zero offs vs zero offs-      (ArraySlotWithOffs idA _, ArraySlotZero idB)             | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev-      (ArraySlotWithOffs idA (Lit offA), ArraySlotZero idB)    | BS.length idA == 32, BS.length idB == 32, offA /= 0  -> go slot prev-      -- non-zero offs vs non-zero offs-      (ArraySlotWithOffs idA _, ArraySlotWithOffs idB _)       | BS.length idA == 32, BS.length idB == 32, idA /= idB -> go slot prev+      (ArraySlotWithOffs idA _, ArraySlotZero idB)             | isArray idA, isArray idB, idA /= idB -> go slot prev+      (ArraySlotWithOffs idA (Lit offA), ArraySlotZero idB)    | isArray idA, idA == idB, offA /= 0  -> go slot prev -      (ArraySlotWithOffs idA offA, ArraySlotWithOffs idB offB) | BS.length idA == 32, BS.length idB == 32, surelyNotEq offA offB -> go slot prev+      -- non-zero offs vs non-zero offs, different ids+      (ArraySlotWithOffs idA _, ArraySlotWithOffs idB _)       | isArray idA, isArray idB, idA /= idB -> go slot prev +      -- non-zero offs vs non-zero offs, same ids+      (ArraySlotWithOffs idA a, ArraySlotWithOffs idB b)                       | isArray idA, idA == idB,+        surelyNotEqual a b -> go slot prev+      (ArraySlotWithOffs idB offB2, ArraySlotWithOffs2 idA offA1 offA2)        | isArray idA, idA == idB,+        surelyNotEqual (Add (Lit offA1) offA2) offB2 -> go slot prev+      (ArraySlotWithOffs2 idA offA1 offA2, ArraySlotWithOffs idB offB2)        | isArray idA, idA == idB,+        surelyNotEqual (Add (Lit offA1) offA2) offB2 -> go slot prev+      (ArraySlotWithOffs2 idA offA1 offA2, ArraySlotWithOffs2 idB offB1 offB2) | isArray idA, idA == idB,+        surelyNotEqual (Add (Lit offA1) offA2) (Add (Lit offB1) offB2) -> go slot prev+       -- we are unable to determine statically whether or not we can safely move deeper in the write chain, so return an abstract term       _ -> Just $ SLoad slot s -    surelyNotEq :: Expr a -> Expr a -> Bool-    surelyNotEq (Lit a) (Lit b) = a /= b-    -- never equal: x+y (y is concrete) vs x+z (z is concrete), y!=z-    surelyNotEq (Add (Lit l1) v1) (Add (Lit l2) v2) = l1 /= l2 && v1 == v2-    -- never equal: x+y (y is concrete, non-zero) vs x-    surelyNotEq v1 (Add (Lit l2) v2) = l2 /= 0 && v1 == v2-    surelyNotEq (Add (Lit l1) v1) v2 = l1 /= 0 && v1 == v2-    surelyNotEq _ _ = False-     maxW32 :: W256     maxW32 = into (maxBound :: Word32)+    isArray :: ByteString -> Bool+    isArray b = BS.length b == 32+    isMap :: Expr Buf -> Bool+    isMap b = bufLength b == Lit 64+    isMap' :: ByteString -> Bool+    isMap' b = BS.length b == 64+    surelyNotEqual :: Expr EWord -> Expr EWord -> Bool+    surelyNotEqual a b = case (simplifyNoLitToKeccak (Sub a b)) of+      Lit k | k > 0 -> True+      _ -> False+    surelyEqual :: Expr EWord -> Expr EWord -> Bool+    surelyEqual a b = simplifyNoLitToKeccak (Sub a b) == Lit 0 + -- storage slots for maps are determined by (keccak (bytes32(key) ++ bytes32(id))) pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord pattern MappingSlot idx key = Keccak (WriteWord (Lit 0) key (ConcreteBuf idx))  -- storage slots for arrays are determined by (keccak(bytes32(id)) + offset)--- note that `normArgs` puts the Lit as the 2nd argument to `Add`+-- note that `normArgs` puts the Lit as the 1st argument to `Add` pattern ArraySlotWithOffs :: ByteString -> Expr EWord -> Expr EWord-pattern ArraySlotWithOffs id offset = Add (Keccak (ConcreteBuf id)) offset+pattern ArraySlotWithOffs id offset = Add offset (Keccak (ConcreteBuf id)) +pattern ArraySlotWithOffs2 :: ByteString -> W256 -> Expr EWord -> Expr EWord+pattern ArraySlotWithOffs2 id offs1 offs2 = Add (Lit offs1) (Add offs2 (Keccak (ConcreteBuf id)))+ -- special pattern to match the 0th element because the `Add` term gets simplified out pattern ArraySlotZero :: ByteString -> Expr EWord pattern ArraySlotZero id = Keccak (ConcreteBuf id)- -- checks if two mapping ids match or not idsDontMatch :: ByteString -> ByteString -> Bool idsDontMatch a b = BS.length a >= 64 && BS.length b >= 64 && diff32to64Byte a b@@ -720,25 +755,38 @@ slotPos :: Word8 -> ByteString slotPos pos = BS.pack ((replicate 31 (0::Word8))++[pos]) --- | Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)-structureArraySlots :: Expr a -> Expr a-structureArraySlots e = mapExpr go e+-- Optimized litToArrayPreimage using the pre-computed map+litToArrayPreimage :: W256 -> Maybe (Word8, W256)+litToArrayPreimage val =+  -- Find the largest 'imageHashKey' in our map such that 'imageHashKey <= val'.+  case Map.lookupLE val preImageLookupMap of+    Just (foundImageHashKey, array_id) ->+      -- 'foundImageHashKey' is one of the keccak hashes from preImagesSource.+      -- 'array_id' is the original Word8 (0-255) that produced this hash.++      -- We have found an 'foundImageHashKey' such that 'foundImageHashKey <= val'.+      -- Now we must check if 'val' is also within the 256-byte range starting at 'foundImageHashKey',+      -- i.e., 'val <= foundImageHashKey + 255'.+      if val <= foundImageHashKey + 255 then+        Just (array_id, val - foundImageHashKey) -- Return the id and the offset from the hash+      else+        -- 'val' is greater than the upper bound for 'foundImageHashKey'.+        -- Since 'foundImageHashKey' was the largest key <= 'val', no other+        -- (smaller) key in the map could satisfy the condition for its interval if this one doesn't.+        Nothing+    Nothing ->+      -- No key in 'preImageLookupMap' is less than or equal to 'val'.+      -- This implies 'val' is smaller than all computed 'image' hashes.+      Nothing++litToKeccak :: Expr a -> Expr a+litToKeccak e = mapExpr go e   where     go :: Expr a -> Expr a     go orig@(Lit key) = case litToArrayPreimage key of       Just (array, offset) -> ArraySlotWithOffs (slotPos array) (Lit offset)       _ -> orig-    go a = a---- Takes in value, checks if it's within 256 of a pre-computed array hash value--- if it is, it returns (array_number, offset)-litToArrayPreimage :: W256 -> Maybe (Word8, W256)-litToArrayPreimage val = go preImages-  where-    go :: [(W256, Word8)] -> Maybe (Word8, W256)-    go ((image, preimage):ax) = if val >= image && val-image <= 255 then Just (preimage, val-image)-                                                                    else go ax-    go [] = Nothing+    go otherNode = otherNode  -- | Writes a value to a key in a storage expression. --@@ -816,6 +864,7 @@                                   Lit 64 -> setMap e                                   _ -> setMixed e     go e@(SLoad (ArraySlotWithOffs x _) _) = if BS.length x == 32 then setArray e else setMixed e+    go e@(SLoad (ArraySlotWithOffs2 x _ _) _) = if BS.length x == 32 then setArray e else setMixed e     go e@(SLoad (Lit x) _) | x < 256 = setSmall e     go e@(SLoad _ _) = setMixed e     go e@(SStore (MappingSlot x _) _ _) = if BS.length x == 64 then setMap e else setMixed e@@ -824,6 +873,7 @@                                   Lit 64 -> setMap e                                   _ -> setMixed e     go e@(SStore (ArraySlotWithOffs x _) _ _) = if BS.length x == 32 then setArray e else setMixed e+    go e@(SStore (ArraySlotWithOffs2 x _ _) _ _) = if BS.length x == 32 then setArray e else setMixed e     go e@(SStore (Lit x) _ _) | x < 256 = setSmall e     go e@(SStore _ _ _) = setMixed e     go _ = pure ()@@ -897,6 +947,7 @@       (MappingSlot idx key) | BS.length idx == 64 -> Just (Just $ idxToWord idx, key)       -- arrays       (ArraySlotWithOffs idx offset) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, offset)+      (ArraySlotWithOffs2 idx offs1 offs2) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, Add (Lit offs1) offs2)       (ArraySlotZero idx) | BS.length idx == 32 -> Just (Just $ idxToWord64 idx, Lit 0)       _ -> Nothing @@ -935,9 +986,12 @@ -- | Simple recursive match based AST simplification -- Note: may not terminate! simplify :: Expr a -> Expr a-simplify e = if (mapExpr go e == e)-               then e-               else simplify (mapExpr go (structureArraySlots e))+simplify e = untilFixpoint (simplifyNoLitToKeccak . litToKeccak) e++simplifyNoLitToKeccak :: Expr a -> Expr a+simplifyNoLitToKeccak l@(Lit _) = l+simplifyNoLitToKeccak s@(ConcreteStore _) = s+simplifyNoLitToKeccak e = untilFixpoint (mapExpr go) e   where     go :: Expr a -> Expr a @@ -947,6 +1001,12 @@      -- redundant CopySlice     go (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x0) _ dst) = dst+    -- We write over dst with data from src. As long as we read from where we write, and+    --    it's the same size, we can just skip the 2nd CopySlice+    go (CopySlice readOff dstOff size2 (CopySlice srcOff writeOff size1 src _) dst) |+      size1 == size2 && readOff == writeOff = CopySlice srcOff dstOff size1 src dst+    -- overwrite empty buf with a buf, return is the buf+    go (CopySlice (Lit 0) (Lit 0) (BufLength src1) src2 (ConcreteBuf "")) | src1 == src2 = src1      -- simplify storage     go (SLoad slot store) = readStorage' slot store@@ -992,21 +1052,26 @@             where simplifiedBuf = BS.take (unsafeInto (n+sz)) buf     go (CopySlice a b c d f) = copySlice a b c d f +    go (JoinBytes (LitByte a0)  (LitByte a1)  (LitByte a2)  (LitByte a3)+      (LitByte a4)  (LitByte a5)  (LitByte a6)  (LitByte a7)+      (LitByte a8)  (LitByte a9)  (LitByte a10) (LitByte a11)+      (LitByte a12) (LitByte a13) (LitByte a14) (LitByte a15)+      (LitByte a16) (LitByte a17) (LitByte a18) (LitByte a19)+      (LitByte a20) (LitByte a21) (LitByte a22) (LitByte a23)+      (LitByte a24) (LitByte a25) (LitByte a26) (LitByte a27)+      (LitByte a28) (LitByte a29) (LitByte a30) (LitByte a31)) =+        let b =  map fromIntegral [a0, a1, a2, a3 ,a4, a5, a6, a7+                                  ,a8, a9, a10, a11 ,a12, a13, a14, a15+                                  ,a16, a17, a18, a19 ,a20, a21, a22, a23+                                  ,a24, a25, a26, a27 ,a28, a29, a30, a31]+        in Lit (constructWord256 b)+     go (IndexWord a b) = indexWord a b -    -- LT-    go (EVM.Types.LT (Lit a) (Lit b))-      | a < b = Lit 1-      | otherwise = Lit 0-    go (EVM.Types.LT _ (Lit 0)) = Lit 0-    go (EVM.Types.LT a (Lit 1)) = iszero a -    -- normalize all comparisons in terms of LT-    go (EVM.Types.GT a b) = lt b a-    go (EVM.Types.GEq a b) = leq b a-    go (EVM.Types.LEq a b) = iszero (lt b a)-    go (SLT a@(Lit _) b@(Lit _)) = slt a b-    go (SGT a b) = SLT b a+    go (SEx a (SEx a2 b)) | a == a2  = sex a b+    go (SEx _ (Lit 0)) = Lit 0+    go (SEx a b) = sex a b      -- IsZero     go (IsZero (IsZero (IsZero a))) = iszero a@@ -1030,23 +1095,16 @@       | x == 0 = b       | otherwise = a +    -- Masking as as per Solidity bit-packing of e.g. function parameters+    go (And (Lit mask1) (Or (And (Lit mask2) _) x)) | (mask1 .&. mask2 == 0)+         = And (Lit mask1) x+     -- address masking     go (And (Lit 0xffffffffffffffffffffffffffffffffffffffff) a@(WAddr _)) = a      -- literal addresses     go (WAddr (LitAddr a)) = Lit $ into a -    -- XOR normalization-    go (Xor a  b) = EVM.Expr.xor a b--    -- simple div/mod/add/sub-    go (Div o1@(Lit _)  o2@(Lit _)) = EVM.Expr.div  o1 o2-    go (SDiv o1@(Lit _) o2@(Lit _)) = EVM.Expr.sdiv o1 o2-    go (Mod o1@(Lit _)  o2@(Lit _)) = EVM.Expr.mod  o1 o2-    go (SMod o1@(Lit _) o2@(Lit _)) = EVM.Expr.smod o1 o2-    go (Add o1@(Lit _)  o2@(Lit _)) = EVM.Expr.add  o1 o2-    go (Sub o1@(Lit _)  o2@(Lit _)) = EVM.Expr.sub  o1 o2-     -- Mod     go (Mod _ (Lit 0)) = Lit 0     go (SMod _ (Lit 0)) = Lit 0@@ -1055,6 +1113,21 @@     go (Mod (Lit 0) _) = Lit 0     go (SMod (Lit 0) _) = Lit 0 +    -- MulMod+    go (MulMod (Lit 0) _ _) = Lit 0+    go (MulMod _ (Lit 0) _) = Lit 0+    go (MulMod _ _ (Lit 0)) = Lit 0+    go (MulMod a b c) = mulmod a b c++    -- AddMod+    go (AddMod (Lit 0) a b) = Mod a b+    go (AddMod a (Lit 0) b) = Mod a b+    go (AddMod _ _ (Lit 0)) = Lit 0+    go (AddMod a b c) = addmod a b c++    -- Triple And (must be before 3-way sort below)+    go (And (Lit a) (And (Lit b) c)) = And (EVM.Expr.and (Lit a) (Lit b)) c+     -- double add/sub.     -- Notice that everything is done mod 2**256. So for example:     -- (a-b)+c observes the same arithmetic equalities as we are used to@@ -1067,7 +1140,6 @@     -- Notice: all Add is normalized, hence the 1st argument is     --    expected to be Lit, if any. Hence `orig` needs to be the     --    2nd argument for Add. However, Sub is not normalized-    go (Add (Lit x) (Add (Lit y) orig)) = add (Lit (x+y)) orig     -- add + sub NOTE: every combination of Sub is needed (2)     go (Add (Lit x) (Sub (Lit y) orig)) = sub (Lit (x+y)) orig     go (Add (Lit x) (Sub orig (Lit y))) = add (Lit (x-y)) orig@@ -1080,18 +1152,52 @@     go (Sub (Lit x) (Add (Lit y) orig)) = sub (Lit (x-y)) orig     go (Sub (Add (Lit x) orig) (Lit y) ) = add (Lit (x-y)) orig +    -- Add+Add / Mul+Mul / Xor+Xor simplifications, taking+    --     advantage of associativity and commutativity+    -- Since Lit is smallest in the ordering, it will always be the first argument+    --     hence these will collect Lits. See `simp-assoc..` tests+    go (Add (Lit a) (Add (Lit b) x)) = add (Lit (a+b)) x+    go (Mul (Lit a) (Mul (Lit b) x)) = mul (Lit (a*b)) x+    go (Xor (Lit a) (Xor (Lit b) x)) = EVM.Expr.xor (Lit (Data.Bits.xor a b)) x+    go (Add (Add a b) c) = add (l !! 0) (add (l !! 1) (l !! 2))+      where l = sort [a, b, c]+    go (Add a (Add b c)) = add (l !! 0) (add (l !! 1) (l !! 2))+      where l = sort [a, b, c]+    go (Mul (Mul a b) c) = mul (l !! 0) (mul (l !! 1) (l !! 2))+      where l = sort [a, b, c]+    go (Mul a (Mul b c)) = mul (l !! 0) (mul (l !! 1) (l !! 2))+      where l = sort [a, b, c]+    go (Xor (Xor a b) c) = x (l !! 0) (x (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            x = EVM.Expr.xor+    go (Xor a (Xor b c)) = x (l !! 0) (x (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            x = EVM.Expr.xor+    go (Or (Or a b) c) = o (l !! 0) (o (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            o = EVM.Expr.or+    go (Or a (Or b c)) = o (l !! 0) (o (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            o = EVM.Expr.or+    go (And (And a b) c) = an (l !! 0) (an (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            an = EVM.Expr.and+    go (And a (And b c)) = an (l !! 0) (an (l !! 1) (l !! 2))+      where l = sort [a, b, c]+            an = EVM.Expr.and++    -- A special pattern sometimes generated from Solidity that uses exponentiation to simulate bit shift.+    -- We can rewrite the exponentiation into a bit-shift under certain conditions.+    go (Exp (Lit 0x100) offset@(Mul (Lit a) (Mod _ (Lit b))))+      | a * b <= 32 && (maxWord256 `Prelude.div` a) > b = shl (mul (Lit 8) offset) (Lit 1)+    go (Exp (Lit 0x100) offset@(Mod _ (Lit 32))) = (shl (mul (Lit 8) offset)) (Lit 1)+     -- redundant add / sub     go (Sub (Add a b) c)       | a == c = b       | b == c = a       | otherwise = sub (add a b) c -    -- Add is associative. We are doing left-growing trees because LIT is-    -- arranged to the left. This way, they accumulate in all combinations.-    -- See `sim-assoc-add` test cases in test.hs-    go (Add a (Add b c)) = add (add a b) c-    go (Add (Add (Lit a) x) (Lit b)) = add (Lit (a+b)) x-     -- add / sub identities     go (Add a b)       | b == (Lit 0) = a@@ -1102,19 +1208,25 @@       | b == (Lit 0) = a       | otherwise = sub a b -    -- SHL / SHR by 0+    -- XOR normalization+    go (Xor a  b) = EVM.Expr.xor a b++    go (EqByte a b) = eqByte a b++    -- SHL / SHR / SAR     go (SHL a v)       | a == (Lit 0) = v+      | v == (Lit 0) = v       | otherwise = shl a v     go (SHR a v)       | a == (Lit 0) = v+      | v == (Lit 0) = v       | otherwise = shr a v--    -- doubled And-    go o@(And a (And b c))-      | a == c = (And a b)-      | a == b = (And b c)-      | otherwise = o+    go (SAR _ (Lit v)) | v == maxBound = Lit v+    go (SAR a v)+       | a == (Lit 0) = v+       | v == (Lit 0) = v+       | otherwise = sar a v      -- Bitwise AND & OR. These MUST preserve bitwise equivalence     go (And a b)@@ -1155,11 +1267,6 @@                      (Lit 0, _) -> Lit 0                      _ -> EVM.Expr.min a b -    -- Mul is associative. We are doing left-growing trees because LIT is-    -- arranged to the left. This way, they accumulate in all combinations.-    -- See `sim-assoc-add` test cases in test.hs-    go (Mul a (Mul b c)) = mul (mul a b) c-    go (Mul (Mul (Lit a) x) (Lit b)) = mul (Lit (a*b)) x      -- Some trivial mul eliminations     go (Mul a b) = case (a, b) of@@ -1175,6 +1282,12 @@     go (SDiv _ (Lit 0)) = Lit 0 -- divide anything by 0 is zero in EVM     go (SDiv a (Lit 1)) = a     -- NOTE: Div x x is NOT 1, because Div 0 0 is 0, not 1.+    --+    go (Exp _ (Lit 0)) = Lit 1 -- everything, including 0, to the power of 0 is 1+    go (Exp a (Lit 1)) = a -- everything, including 0, to the power of 1 is itself+    go (Exp (Lit 1) _) = Lit 1 -- 1 to any value (including 0) is 1+    -- NOTE: we can't simplify (Lit 0)^k. If k is 0 it's 1, otherwise it's 0.+    --       this is encoded in SMT.hs instead, via an SMT "ite"      -- If a >= b then the value of the `Max` expression can never be < b     go o@(LT (Max (Lit a) _) (Lit b))@@ -1189,6 +1302,29 @@            then Lit 0            else o +    -- normalize all comparisons in terms of (S)LT+    go (EVM.Types.GT a b) = lt b a+    go (EVM.Types.GEq a b) = leq b a+    go (EVM.Types.LEq a b) = iszero (lt b a)+    go (SGT a b) = slt b a++    -- LT+    go (EVM.Types.LT _ (Lit 0)) = Lit 0+    go (EVM.Types.LT a (Lit 1)) = iszero a+    go (EVM.Types.LT (Lit 0) a) = iszero (Eq (Lit 0) a)+    go (EVM.Types.LT a b) = lt a b++    -- SLT+    go (SLT _ (Lit a)) | a == minLitSigned = Lit 0+    go (SLT (Lit a) _) | a == maxLitSigned = Lit 0+    go (SLT a b) = slt a b++    -- simple div/mod/add/sub+    go (Div  o1 o2) = EVM.Expr.div  o1 o2+    go (SDiv o1 o2) = EVM.Expr.sdiv o1 o2+    go (Mod  o1 o2) = EVM.Expr.mod  o1 o2+    go (SMod o1 o2) = EVM.Expr.smod o1 o2+     go a = a  @@ -1198,9 +1334,12 @@ simplifyProps :: [Prop] -> [Prop] simplifyProps ps = if cannotBeSat then [PBool False] else simplified   where-    simplified = remRedundantProps . map simplifyProp . flattenProps $ ps-    cannotBeSat = isUnsat simplified+    simplified = untilFixpoint goOne ps+    cannotBeSat = PBool False `elem` simplified+    goOne :: [Prop] -> [Prop]+    goOne = remRedundantProps . map simplifyProp . constPropagate . flattenProps + -- | Evaluate the provided proposition down to its most concrete result -- Also simplifies the inner Expr, if it exists simplifyProp :: Prop -> Prop@@ -1210,29 +1349,60 @@   where     go :: Prop -> Prop -    -- LT/LEq comparisons+    -- Rewrite PGT/GEq to PLT/PLEq     go (PGT a b) = PLT b a     go (PGEq a b) = PLEq b a++    -- PLT/PLEq comparisons     go (PLT  (Var _) (Lit 0)) = PBool False     go (PLEq (Lit 0) _) = PBool True     go (PLEq (WAddr _) (Lit 1461501637330902918203684832716283019655932542975)) = PBool True     go (PLEq _ (Lit x)) | x == maxLit = PBool True     go (PLT  (Lit val) (Var _)) | val == maxLit = PBool False     go (PLEq (Var _) (Lit val)) | val == maxLit = PBool True+    go (PLT a b) | a == b = PBool False     go (PLT (Lit l) (Lit r)) = PBool (l < r)+    go (PLEq a b) | a == b = PBool True     go (PLEq (Lit l) (Lit r)) = PBool (l <= r)     go (PLEq a (Max b _)) | a == b = PBool True     go (PLEq a (Max _ b)) | a == b = PBool True     go (PLEq (Sub a b) c) | a == c = PLEq b a     go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)     go (PLT (Lit 0) (Eq a b)) = peq a b+    go (PLEq a b) = pleq a b +    -- when it's PLT but comparison on the RHS then it's just (PEq 1 RHS)+    go (PLT (Lit 0) (a@LT {})) = peq (Lit 1) a+    go (PLT (Lit 0) (a@LEq {})) = peq (Lit 1) a+    go (PLT (Lit 0) (a@SLT {})) = peq (Lit 1) a+    go (PLT (Lit 0) (a@GT {})) = peq (Lit 1) a+    go (PLT (Lit 0) (a@GEq {})) = peq (Lit 1) a+    go (PLT (Lit 0) (a@SGT {})) = peq (Lit 1) a+    go (POr (PLEq a1 (Lit b)) (PLEq (Lit c) a2)) | a1 == a2 && c == b+1 = PBool True+     -- negations     go (PNeg (PBool b)) = PBool (Prelude.not b)     go (PNeg (PNeg a)) = a+    go (PNeg (PGT a b)) = PLEq a b+    go (PNeg (PGEq a b)) = PLT a b+    go (PNeg (PLT a b)) = PGEq a b+    go (PNeg (PLEq a b)) = PGT a b+    go (PNeg (PAnd a b)) = POr (PNeg a) (PNeg b)+    go (PNeg (POr a b)) = PAnd (PNeg a) (PNeg b)+    go (PNeg (PEq (Lit 1) (IsZero b))) = PEq (Lit 0) (IsZero b) +    -- Empty buf+    go (PEq (Lit 0) (BufLength k)) = peq k (ConcreteBuf "")+    go (PEq (Lit 0) (Or a b)) = peq a (Lit 0) `PAnd` peq b (Lit 0)++    -- PEq rewrites (notice -- GT/GEq is always rewritten to LT by simplify)+    go (PEq (Lit 1) (IsZero (LT a b))) = PLT a b+    go (PEq (Lit 1) (IsZero (LEq a b))) = PLEq a b+    go (PEq (Lit 0) (IsZero a)) = PLT (Lit 0) a+    go (PEq a1 (Add a2 y)) | a1 == a2 = peq y (Lit 0)+     -- solc specific stuff-    go (PEq (Lit 0) (IsZero (IsZero (Eq a b)))) = PNeg (peq a b)+    go (PLT (Lit 0) (IsZero (Eq a b))) = PNeg (peq a b)      -- iszero(a) -> (a == 0)     -- iszero(iszero(a))) -> ~(a == 0) -> a > 0@@ -1266,18 +1436,18 @@     go (PImpl (PBool True) b) = b     go (PImpl (PBool False) _) = PBool True -    -- Double negation-    go (PEq (Lit 0) (IsZero (Eq a b))) = peq a b-    go (PEq (Lit 0) (IsZero (LT a b))) = PLT a b-    go (PEq (Lit 0) (IsZero (GT a b))) = PGT a b-    go (PEq (Lit 0) (IsZero (LEq a b))) = PLEq a b-    go (PEq (Lit 0) (IsZero (GEq a b))) = PGEq a b+    -- Double negation (no need for GT/GEq, as it's rewritten to LT/LEq)      -- Eq     go (PEq (Lit 0) (Eq a b)) = PNeg (peq a b)     go (PEq (Lit 1) (Eq a b)) = peq a b     go (PEq (Lit 0) (Sub a b)) = peq a b     go (PEq (Lit 0) (LT a b)) = PLEq b a+    go (PEq (Lit 0) (LEq a b)) = PLT b a+    go (PEq (Lit 1) (LT a b)) = PLT a b+    go (PEq (Lit 1) (LEq a b)) = PLEq a b+    go (PEq (Lit 1) (GT a b)) = PGT a b+    go (PEq (Lit 1) (GEq a b)) = PGEq a b     go (PEq l r) = peq l r      go p = p@@ -1326,13 +1496,10 @@  -- TODO: make this smarter, probably we will need to use the solver here? wordToAddr :: Expr EWord -> Maybe (Expr EAddr)-wordToAddr = go . simplify-  where-    go :: Expr EWord -> Maybe (Expr EAddr)-    go = \case-      WAddr a -> Just a-      Lit a -> Just $ LitAddr (truncateToAddr a)-      _ -> Nothing+wordToAddr e = case (concKeccakSimpExpr e) of+  WAddr a -> Just a+  Lit a -> Just $ LitAddr (truncateToAddr a)+  _ -> Nothing  litCode :: BS.ByteString -> [Expr Byte] litCode bs = fmap LitByte (BS.unpack bs)@@ -1367,6 +1534,10 @@   Partial {} -> True   _ -> False +isSymAddr :: Expr EAddr -> Bool+isSymAddr (SymAddr _) = True+isSymAddr _ = False+ -- | Returns the byte at idx from the given word. indexWord :: Expr EWord -> Expr EWord -> Expr Byte -- Simplify masked reads:@@ -1420,6 +1591,11 @@     fullWordMask = (2 ^ (256 :: W256)) - 1     unmaskedBytes = fromIntegral $ (countLeadingZeros mask) `Prelude.div` 8     isByteAligned m = (countLeadingZeros m) `Prelude.mod` 8 == 0+-- This pattern happens in Solidity for function selectors. Since Lit 0xfff... (28 bytes of 0xff)+-- is masking the function selector, it can be simplified to just the function selector bytes. Remember,+-- indexWord takes the MSB i-th byte when called with (indexWord i).+indexWord (Lit a) (Or funSel (And (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffff) _)) | a < 4 =+  indexWord (Lit a) funSel indexWord (Lit idx) (Lit w)   | idx <= 31 = LitByte . fromIntegral $ shiftR w (248 - unsafeInto idx * 8)   | otherwise = LitByte 0@@ -1484,7 +1660,7 @@  joinBytes :: [Expr Byte] -> Expr EWord joinBytes bs-  | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByte) $ bs+  | all isLitByte bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs   | otherwise = let       bytes = padBytesLeft 32 bs     in JoinBytes@@ -1499,7 +1675,7 @@  eqByte :: Expr Byte -> Expr Byte -> Expr EWord eqByte (LitByte x) (LitByte y) = Lit $ if x == y then 1 else 0-eqByte x y = EqByte x y+eqByte x y = if x < y then EqByte x y else EqByte y x  min :: Expr EWord -> Expr EWord -> Expr EWord min x y = normArgs Min Prelude.min x y@@ -1514,7 +1690,7 @@ numBranches _ = 1  allLit :: [Expr Byte] -> Bool-allLit = Data.List.and . fmap (isLitByte)+allLit = all isLitByte  -- | True if the given expression contains any node that satisfies the -- input predicate@@ -1526,64 +1702,89 @@     go _ = Any False  inRange :: Int -> Expr EWord -> Prop-inRange sz e = PAnd (PGEq e (Lit 0)) (PLEq e (Lit $ 2 ^ sz - 1))+inRange sz e = if sz == 256 then PBool True else PLEq e (Lit $ 2 ^ sz - 1) +inRangeSigned :: Int -> Expr EWord -> Prop+inRangeSigned sz e = ((PLEq e (Lit $ 2 ^ (sz - 1) - 1)) `POr` (PGEq e $ Lit $ ((2 ^ sz) - 2 ^ (sz -  1))))  -- | images of keccak(bytes32(x)) where 0 <= x < 256 preImages :: [(W256, Word8)] preImages = [(keccak' (word256Bytes . into $ i), i) | i <- [0..255]] +-- | images of keccak(bytes32(x)) where 0 <= x < 256+preImageLookupMap :: Map.Map W256 Word8+preImageLookupMap = Map.fromList preImages data ConstState = ConstState   { values :: Map.Map (Expr EWord) W256   , canBeSat :: Bool   }   deriving (Show) --- | Checks if a conjunction of propositions is definitely unsatisfiable-isUnsat :: [Prop] -> Bool-isUnsat ps = Prelude.not $ oneRun ps (ConstState mempty True)+-- | Performs constant propagation+constPropagate :: [Prop] -> [Prop]+constPropagate ps =+ let consts = collectConsts ps (ConstState mempty True)+ in if consts.canBeSat then substitute consts ps ++ fixVals consts+    else [PBool False]   where-    oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat+    -- Fixes the values of the constants+    fixVals :: ConstState -> [Prop]+    fixVals cs = Map.foldrWithKey (\k v acc -> peq (Lit v) k : acc) [] cs.values++    -- Substitutes the constants in the props.+    -- NOTE: will create PEq (Lit x) (Lit x) if x is a constant+    --       hence we need the fixVals function to add them back in+    substitute :: ConstState -> [Prop] -> [Prop]+    substitute cs ps2 = map (mapProp (subsGo cs)) ps2+    subsGo :: ConstState -> Expr a-> Expr a+    subsGo cs (Var v) = case Map.lookup (Var v) cs.values of+      Just x -> Lit x+      Nothing -> Var v+    subsGo _ x = x++    -- Collects all the constants in the given props, and sets canBeSat to False if UNSAT+    collectConsts ps2 startState = execState (mapM go ps2) startState     go :: Prop -> State ConstState ()     go = \case-        -- PEq         PEq (Lit l) a -> do           s <- get           case Map.lookup a s.values of             Just l2 -> unless (l==l2) $ put ConstState {canBeSat=False, values=mempty}             Nothing -> modify (\s' -> s'{values=Map.insert a l s'.values})         PEq a b@(Lit _) -> go (PEq b a)-        -- PNeg         PNeg (PEq (Lit l) a) -> do           s <- get           case Map.lookup a s.values of             Just l2 -> when (l==l2) $ put ConstState {canBeSat=False, values=mempty}             Nothing -> pure ()         PNeg (PEq a b@(Lit _)) -> go $ PNeg (PEq b a)-        -- Others         PAnd a b -> do           go a           go b         POr a b -> do           s <- get           let-            v1 = oneRun [a] s-            v2 = oneRun [b] s-          unless v1 $ go b-          unless v2 $ go a+            v1 = collectConsts [a] s+            v2 = collectConsts [b] s+          unless v1.canBeSat $ go b+          unless v2.canBeSat $ go a         PBool False -> put $ ConstState {canBeSat=False, values=mempty}         _ -> pure ()  -- Concretize & simplify Keccak expressions until fixed-point. concKeccakSimpExpr :: Expr a -> Expr a-concKeccakSimpExpr orig = untilFixpoint ((mapExpr concKeccakOnePass) . simplify) orig+concKeccakSimpExpr orig = untilFixpoint (simplifyNoLitToKeccak . (mapExpr concKeccakOnePass)) (simplify orig) --- Only concretize Keccak in Props+-- Concretize Keccak in Props, but don't simplify -- Needed because if it also simplified, we may not find some simplification errors, as -- simplification would always be ON concKeccakProps :: [Prop] -> [Prop] concKeccakProps orig = untilFixpoint (map (mapProp concKeccakOnePass)) orig +-- As above, but also simplify, to fixedpoint+concKeccakSimpProps :: [Prop] -> [Prop]+concKeccakSimpProps orig = untilFixpoint (simplifyProps . map (mapProp concKeccakOnePass)) orig+ -- Simplifies in case the input to the Keccak is of specific array/map format and --            can be simplified into a concrete value -- Turns (Keccak ConcreteBuf) into a Lit@@ -1616,3 +1817,30 @@ -- Commutative operators should have the constant on the LHS checkLHSConst :: Expr a -> Bool checkLHSConst a = isJust $ mapExprM_ lhsConstHelper a++maybeLitByteSimp :: Expr Byte -> Maybe Word8+maybeLitByteSimp (LitByte x) = Just x+maybeLitByteSimp e = case concKeccakSimpExpr e of+  LitByte x -> Just x+  _ -> Nothing++maybeLitWordSimp :: Expr EWord -> Maybe W256+maybeLitWordSimp (Lit w) = Just w+maybeLitWordSimp (WAddr (LitAddr w)) = Just (into w)+maybeLitWordSimp e = case concKeccakSimpExpr e of+  Lit w -> Just w+  WAddr (LitAddr w) -> Just (into w)+  _ -> Nothing++maybeLitAddrSimp :: Expr EAddr -> Maybe Addr+maybeLitAddrSimp (LitAddr a) = Just a+maybeLitAddrSimp e = case concKeccakSimpExpr e of+  LitAddr a -> Just a+  _ -> Nothing++maybeConcStoreSimp :: Expr Storage -> Maybe (LMap.Map W256 W256)+maybeConcStoreSimp (ConcreteStore s) = Just s+maybeConcStoreSimp e = case concKeccakSimpExpr e of+  ConcreteStore s -> Just s+  _ -> Nothing+

@@ -27,7 +27,9 @@ import System.Environment (lookupEnv, getEnvironment) import System.Process import Control.Monad.IO.Class+import Control.Monad (when) import EVM.Effects+import qualified EVM.Expr as Expr  -- | Abstract representation of an RPC fetch request data RpcQuery a where@@ -113,7 +115,7 @@ parseBlock j = do   coinbase   <- LitAddr . readText <$> j ^? key "miner" % _String   timestamp  <- Lit . readText <$> j ^? key "timestamp" % _String-  number     <- readText <$> j ^? key "number" % _String+  number     <- Lit . readText <$> j ^? key "number" % _String   gasLimit   <- readText <$> j ^? key "gasLimit" % _String   let    baseFee = readText <$> j ^? key "baseFeePerGas" % _String@@ -183,11 +185,7 @@   sess <- Session.newAPISession   fetchQuery Latest (fetchWithSession url sess) QueryChainId -http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s-http smtjobs smttimeout n url q =-  withSolvers Z3 smtjobs 1 smttimeout $ \s ->-    oracle s (Just (n, url)) q-+-- Only used for testing (test.hs, BlockchainTests.hs) zero :: Natural -> Maybe Natural -> Fetcher t m s zero smtjobs smttimeout q =   withSolvers Z3 smtjobs 1 smttimeout $ \s ->@@ -212,7 +210,14 @@          -- Is is possible to satisfy the condition?          continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds +    PleaseGetSols symExpr numBytes pathconditions continue -> do+         let pathconds = foldl' PAnd (PBool True) pathconditions+         continue <$> getSolutions solvers symExpr numBytes pathconds+     PleaseFetchContract addr base continue -> do+      conf <- readConfig+      when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr+      when (addr == 0 && conf.verb > 0) $ liftIO $ putStrLn "Warning: fetching contract at address 0"       contract <- case info of         Nothing -> let           c = case base of@@ -224,7 +229,10 @@         Just x -> pure $ continue x         Nothing -> internalError $ "oracle error: " ++ show q -    PleaseFetchSlot addr slot continue ->+    PleaseFetchSlot addr slot continue -> do+      conf <- readConfig+      when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)+      when (addr == 0 && conf.verb > 0) $ liftIO $ putStrLn "Warning: fetching slot from a contract at address 0"       case info of         Nothing -> pure (continue 0)         Just (n, url) ->@@ -239,6 +247,24 @@  type Fetcher t m s = App m => Query t s -> m (EVM t s ()) +getSolutions :: forall m . App m => SolverGroup -> Expr EWord -> Int -> Prop -> m (Maybe [W256])+getSolutions solvers symExprPreSimp numBytes pathconditions = do+  conf <- readConfig+  liftIO $ do+    let symExpr = Expr.concKeccakSimpExpr symExprPreSimp+    -- when conf.debug $ putStrLn $ "Collecting solutions to symbolic query: " <> show symExpr+    ret <- collectSolutions symExpr pathconditions conf+    case ret of+      Nothing -> pure Nothing+      Just r -> case length r of+        0 -> pure Nothing+        _ -> pure $ Just r+    where+      collectSolutions :: Expr EWord -> Prop -> Config -> IO (Maybe [W256])+      collectSolutions symExpr conds conf = do+        let smt2 = assertProps conf [(PEq (Var "multiQueryVar") symExpr) .&& conds]+        checkMulti solvers smt2 $ MultiSol { maxSols = conf.maxWidth , numBytes = numBytes , var = "multiQueryVar" }+ -- | Checks which branches are satisfiable, checking the pathconditions for consistency -- if the third argument is true. -- When in debug mode, we do not want to be able to navigate to dead paths,@@ -246,19 +272,20 @@ -- will be pruned anyway. checkBranch :: App m => SolverGroup -> Prop -> Prop -> m BranchCondition checkBranch solvers branchcondition pathconditions = do-  conf <- readConfig-  liftIO $ checkSat solvers (assertProps conf [(branchcondition .&& pathconditions)]) >>= \case+  let props = [pathconditions .&& branchcondition]+  checkSatWithProps solvers props >>= \case     -- the condition is unsatisfiable-    Unsat -> -- if pathconditions are consistent then the condition must be false+    (Qed, _) -> -- if pathconditions are consistent then the condition must be false       pure $ Case False     -- Sat means its possible for condition to hold-    Sat _ -> do -- is its negation also possible?-      checkSat solvers (assertProps conf [(pathconditions .&& (PNeg branchcondition))]) >>= \case+    (Cex {}, _) -> do -- is its negation also possible?+      let propsNeg = [pathconditions .&& (PNeg branchcondition)]+      checkSatWithProps solvers propsNeg >>= \case         -- No. The condition must hold-        Unsat -> pure $ Case True+        (Qed, _) -> pure $ Case True         -- Yes. Both branches possible-        Sat _ -> pure EVM.Types.Unknown-    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths-        _ -> pure EVM.Types.Unknown+        (Cex {}, _) -> pure UnknownBranch+        -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths+        _ -> pure UnknownBranch     -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths-    _ -> pure EVM.Types.Unknown+    _ -> pure UnknownBranch

@@ -4,7 +4,10 @@   ( formatExpr   , formatSomeExpr   , formatPartial+  , formatPartialShort   , formatProp+  , formatState+  , formatError   , contractNamePart   , contractPathPart   , showError@@ -28,7 +31,6 @@   , strip0x'   , hexByteString   , hexText-  , bsToHex   , showVal   ) where @@ -38,8 +40,9 @@ import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..)) import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation) import EVM.Expr qualified as Expr-import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap)+import EVM.Solidity (SolcContract(..), Method(..)) import EVM.Types+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)  import Control.Arrow ((>>>)) import Optics.Core@@ -56,7 +59,7 @@ import Data.Foldable (toList) import Data.List (isPrefixOf, sort) import Data.Map qualified as Map-import Data.Maybe (catMaybes, fromMaybe)+import Data.Maybe (catMaybes, fromMaybe, listToMaybe) import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn) import Data.Text qualified as T import Data.Text.Encoding qualified as T@@ -121,6 +124,13 @@     Left (_, _, _)   -> [formatBinary bs] textValues ts _ = fmap (const "<symbolic>") ts +textValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text+textValue ts (ConcreteBuf bs) =+  case runGetOrFail (getAbiSeq 1 [ts]) (fromStrict bs) of+    Right (_, _, xs) -> fromMaybe (internalError "impossible empty list") $ listToMaybe $ textAbiValues xs+    Left (_, _, _)   -> formatBinary bs+textValue _ _ = "<symbolic>"+ parenthesise :: [Text] -> Text parenthesise ts = "(" <> intercalate ", " ts <> ")" @@ -128,7 +138,7 @@ showValues ts b = parenthesise $ textValues ts b  showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text-showValue t b = head $ textValues [t] b+showValue t b = textValue t b  showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text showCall ts (ConcreteBuf bs) = showValues ts $ ConcreteBuf (BS.drop 4 bs)@@ -211,7 +221,7 @@         [] ->           logn         firstTopic:restTopics ->-          case maybeLitWord firstTopic of+          case maybeLitWordSimp firstTopic of             Just topic ->               case Map.lookup topic dapp.eventMap of                 Just (Event name _ argInfos) ->@@ -229,7 +239,7 @@                       -- ) anonymous;                       let                         sig = unsafeInto $ shiftR topic 224 :: FunctionSelector-                        usr = case maybeLitWord t2 of+                        usr = case maybeLitWordSimp t2 of                           Just w ->                             pack $ show (unsafeInto w :: Addr)                           Nothing  ->@@ -274,8 +284,8 @@             where             showTopic :: AbiType -> Expr EWord -> Text             showTopic abiType topic =-              case maybeLitWord (Expr.concKeccakSimpExpr topic) of-                Just w -> head $ textValues [abiType] (ConcreteBuf (word256Bytes w))+              case maybeLitWordSimp (Expr.concKeccakSimpExpr topic) of+                Just w -> textValue abiType (ConcreteBuf (word256Bytes w))                 _ -> "<symbolic>"            withName :: Text -> Text -> Text@@ -369,7 +379,7 @@         case (findSrc contract ?context.info) of           Just x -> Just (contractNamePart x.contractName)           Nothing -> Nothing-    label = case do litAddr <- maybeLitAddr addr+    label = case do litAddr <- maybeLitAddrSimp addr                     Map.lookup litAddr ?context.labels of               Nothing -> ""               Just l -> "[" <> "\x1b[1m" <> l <> "\x1b[0m" <> "]"@@ -457,7 +467,7 @@  formatPartial :: PartialExec -> Text formatPartial = \case-  (UnexpectedSymbolicArg pc opcode msg args) -> T.unlines+  UnexpectedSymbolicArg pc opcode msg args -> T.unlines     [ "Unexpected Symbolic Arguments to Opcode"     , indent 2 $ T.unlines       [ "msg: " <> T.pack (show msg)@@ -469,10 +479,31 @@     ]   MaxIterationsReached pc addr -> "Max Iterations Reached in contract: " <> formatAddr addr <> " pc: " <> pack (show pc) <> " To increase the maximum, set a fixed large (or negative) value for `--max-iterations` on the command line"   JumpIntoSymbolicCode pc idx -> "Encountered a jump into a potentially symbolic code region while executing initcode. pc: " <> pack (show pc) <> " jump dst: " <> pack (show idx)+  CheatCodeMissing pc selector ->T.unlines+    [ "Cheat code not recognized"+    , "program counter: " <> T.pack (show pc)+    , "function selector: " <> T.pack (show selector)+    ]+  BranchTooDeep pc -> T.unlines ["Branches too deep at program counter: " <> pack (show pc)] +formatPartialShort :: PartialExec -> Text+formatPartialShort = \case+  UnexpectedSymbolicArg _ opcode _ _ -> "Unexpected symbolic arguments to opcode: " <> T.pack opcode+  MaxIterationsReached {}            -> "Max iterations reached"+  JumpIntoSymbolicCode {}            -> "Encountered a jump into a potentially symbolic code region while executing initcode"+  CheatCodeMissing _ selector        -> "Cheat code not recognized: " <> T.pack (show selector)+  BranchTooDeep pc                   -> "Branches too deep at program counter: " <> pack (show pc)+ formatSomeExpr :: SomeExpr -> Text-formatSomeExpr (SomeExpr e) = formatExpr e+formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e +formatState :: Map.Map (Expr EAddr) (Expr EContract) -> Text+formatState store = indent 2 $ T.unlines (fmap (\(k,v) ->+              T.unlines+                [ formatExpr k <> ":"+                , indent 2 $ formatExpr v+                ]) (Map.toList store))+ formatExpr :: Expr a -> Text formatExpr = go   where@@ -494,17 +525,10 @@       Success asserts _ buf store -> T.unlines         [ "(Success"         , indent 2 $ T.unlines-          [ "Data:"-          , indent 2 $ formatExpr buf+          [ "Data:" , indent 2 $ formatExpr buf           , ""-          , "State:"-          , indent 2 $ T.unlines (fmap (\(k,v) ->-              T.unlines-                [ formatExpr k <> ":"-                , indent 2 $ formatExpr v-                ]) (Map.toList store))-          , "Assertions:"-          , indent 2 . T.unlines $ fmap formatProp asserts+          , "State:", formatState store+          , "Assertions:", indent 2 . T.unlines $ fmap formatProp asserts           ]         , ")"         ]@@ -837,9 +861,6 @@   case BS16.decodeBase16Untyped (T.encodeUtf8 (T.drop 2 t)) of     Right x -> x     _ -> internalError $ "invalid hex bytestring " ++ show t--bsToHex :: ByteString -> String-bsToHex bs = concatMap (paddedShowHex 2) (BS.unpack bs)  showVal :: AbiValue -> Text showVal (AbiBytes _ bs) = formatBytes bs

@@ -15,7 +15,7 @@  import EVM.Expr qualified as Expr import EVM.Expr (bytesToW256)-import EVM.SMT qualified as SMT (BufModel(..), SMTCex(..))+import EVM.Types qualified as SMT import EVM.Traversals import EVM.Types (Prop(..), W256, Expr(..), EType(..), internalError, keccak') @@ -27,7 +27,7 @@ tryCexFuzz :: [Prop] -> Integer -> (Maybe (SMT.SMTCex)) tryCexFuzz prePs tries = unGen (testVals tries) (mkQCGen 0) 1337   where-    ps = Expr.simplifyProps $ Expr.concKeccakProps prePs+    ps = Expr.concKeccakSimpProps prePs     vars = extractVars ps     bufs = extractBufs ps     stores = extractStorage ps@@ -39,7 +39,7 @@       storeVals <- getStores stores       let         ret = filterCorrectKeccak $ map (substituteEWord varvals . substituteBuf bufVals . substituteStores storeVals) ps-        retSimp = Expr.simplifyProps $ Expr.concKeccakProps ret+        retSimp = Expr.concKeccakSimpProps ret       if null retSimp then pure $ Just (SMT.SMTCex {                                     vars = varvals                                     , addrs = mempty

@@ -63,10 +63,10 @@ keccakAssumptions ps bufs stores = injectivity <> minValue <> minDiffOfPairs   where     (_, st) = runState (findKeccakPropsExprs ps bufs stores) initState--    keccakPairs = uniquePairs (Set.toList st.keccakExprs)+    ks = Set.toList $ Set.map concretizeKeccakParam st.keccakExprs+    keccakPairs = uniquePairs ks     injectivity = map injProp keccakPairs-    minValue = map minProp (Set.toList st.keccakExprs)+    minValue = map minProp ks     minDiffOfPairs = map minDistance keccakPairs      where       minDistance :: (Expr EWord, Expr EWord) -> Prop@@ -76,23 +76,28 @@           req2 = (PGEq (Sub kb ka) (Lit 256))       minDistance _ = internalError "expected Keccak expression" -compute :: forall a. Expr a -> [Prop]+concretizeKeccakParam :: Expr EWord -> Expr EWord+concretizeKeccakParam (Keccak buf) = Keccak (concKeccakSimpExpr buf)+concretizeKeccakParam _ = internalError "Cannot happen"++compute :: forall a. Expr a -> Set Prop compute = \case   e@(Keccak buf) -> do     let b = simplify buf     case keccak b of-      lit@(Lit _) -> [PEq lit e]-      _ -> []-  _ -> []+      lit@(Lit _) -> Set.singleton (PEq lit (concretizeKeccakParam e))+      _ -> Set.empty+  _ -> Set.empty -computeKeccakExpr :: forall a. Expr a -> [Prop]-computeKeccakExpr e = foldExpr compute [] e+computeKeccakExpr :: forall a. Expr a -> Set Prop+computeKeccakExpr e = foldExpr compute Set.empty e -computeKeccakProp :: Prop -> [Prop]-computeKeccakProp p = foldProp compute [] p+computeKeccakProp :: Prop -> Set Prop+computeKeccakProp p = foldProp compute Set.empty p  keccakCompute :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop] keccakCompute ps buf stores =-  concatMap computeKeccakProp ps <>-  concatMap computeKeccakExpr buf <>-  concatMap computeKeccakExpr stores+  Set.toList $+    (foldMap computeKeccakProp ps) <>+    (foldMap computeKeccakExpr buf) <>+    (foldMap computeKeccakExpr stores)

@@ -9,15 +9,16 @@ import Prelude hiding (LT, GT)  import Control.Monad-import Data.Containers.ListUtils (nubOrd)+import Data.Containers.ListUtils (nubOrd, nubInt) import Data.ByteString (ByteString) import Data.ByteString qualified as BS import Data.List qualified as List import Data.List.NonEmpty (NonEmpty((:|))) import Data.List.NonEmpty qualified as NonEmpty import Data.String.Here-import Data.Maybe (fromJust, fromMaybe, isJust)+import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe) import Data.Either.Extra (fromRight')+import Data.Foldable (fold) import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map import Data.Set (Set)@@ -27,6 +28,7 @@ import Data.Text qualified as TS import Data.Text.Lazy qualified as T import Data.Text.Lazy.Builder+import Data.Text.Read (decimal) import Language.SMT2.Parser (getValueRes, parseCommentFreeFileMsg) import Language.SMT2.Syntax (Symbol, SpecConstant(..), GeneralRes(..), Term(..), QualIdentifier(..), Identifier(..), Sort(..), Index(..), VarBinding(..)) import Numeric (readHex, readBin)@@ -75,58 +77,7 @@       , txContext = 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-  , addrs :: Map (Expr EAddr) Addr-  , buffers :: Map (Expr Buf) BufModel-  , store :: Map (Expr EAddr) (Map W256 W256)-  , blockContext :: Map (Expr EWord) W256-  , txContext :: Map (Expr EWord) W256-  }-  deriving (Eq, Show)--instance Semigroup SMTCex where-  a <> b = SMTCex-    { vars = a.vars <> b.vars-    , addrs = a.addrs <> b.addrs-    , buffers = a.buffers <> b.buffers-    , store = a.store <> b.store-    , blockContext = a.blockContext <> b.blockContext-    , txContext = a.txContext <> b.txContext-    }--instance Monoid SMTCex where-  mempty = SMTCex-    { vars = mempty-    , addrs = mempty-    , buffers = mempty-    , store = mempty-    , blockContext = mempty-    , txContext = mempty-    }--flattenBufs :: SMTCex -> Maybe SMTCex-flattenBufs cex = do-  bs <- mapM collapse cex.buffers-  pure $ cex{ buffers = bs }- -- | Attempts to collapse a compressed buffer representation down to a flattened one collapse :: BufModel -> Maybe BufModel collapse model = case toBuf model of@@ -141,6 +92,7 @@ getVar :: SMTCex -> TS.Text -> W256 getVar cex name = fromJust $ Map.lookup (Var name) cex.vars +-- Props are ONLY for pretty printing the query Props data SMT2 = SMT2 [Builder] CexVars [Prop]   deriving (Eq, Show) @@ -164,7 +116,7 @@       sorted = List.sortBy compareFst $ Map.toList $ encSs <> encBs   decls <- mapM snd sorted   let smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty):decls-  pure $ foldr (<>) mempty smt2+  pure $ fold smt2   where     compareFst (l, _) (r, _) = compare l r     encodeBuf n expr = do@@ -178,20 +130,16 @@       storage <- exprToSMT expr       pure $ SMT2 ["(define-fun store" <> (fromString . show $ n) <> " () Storage " <> storage <> ")"] mempty mempty -data AbstState = AbstState-  { words :: Map (Expr EWord) Int-  , count :: Int-  }-  deriving (Show)- smt2Line :: Builder -> SMT2 smt2Line txt = SMT2 [txt] mempty mempty -assertProps :: Config -> [Prop] -> Err SMT2 -- simplify to rewrite sload/sstore combos--- notice: it is VERY important not to concretize, because Keccak assumptions---         will be generated by assertPropsNoSimp, and that needs unconcretized Props-assertProps conf ps = assertPropsNoSimp (decompose . Expr.simplifyProps $ ps)+-- notice: it is VERY important not to concretize early, because Keccak assumptions+--         need unconcretized Props+assertProps :: Config -> [Prop] -> Err SMT2+assertProps conf ps =+  if not conf.simp then assertPropsHelper False ps+  else assertPropsHelper True (decompose . Expr.simplifyProps $ ps)   where     decompose :: [Prop] -> [Prop]     decompose props = if conf.decomposeStorage && safeExprs && safeProps@@ -202,13 +150,13 @@         safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props         safeProps = all Expr.safeToDecomposeProp props + -- Note: we need a version that does NOT call simplify, -- because we make use of it to verify the correctness of our simplification -- passes through property-based testing.-assertPropsNoSimp :: [Prop] -> Err SMT2-assertPropsNoSimp psPreConc = do+assertPropsHelper :: Bool -> [Prop]  -> Err SMT2+assertPropsHelper simp psPreConc = do  encs <- mapM propToSMT psElim- smt <- mapM propToSMT props  intermediates <- declareIntermediates bufs stores  readAssumes' <- readAssumes  keccakAssertions' <- keccakAssertions@@ -217,7 +165,7 @@  pure $ prelude   <> (declareAbstractStores abstractStores)   <> smt2Line ""-  <> (declareAddrs addresses)+  <> declareConstrainAddrs addresses   <> smt2Line ""   <> (declareBufs toDeclarePsElim bufs stores)   <> smt2Line ""@@ -231,40 +179,30 @@   <> smt2Line ""   <> keccakAssertions'   <> readAssumes'+  <> gasOrder   <> smt2Line ""-  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) mempty mempty-  <> SMT2 smt mempty mempty-  <> SMT2 mempty mempty { storeReads = storageReads } mempty-  <> SMT2 mempty mempty psPreConc+  <> SMT2 (fmap (\p -> "(assert " <> p <> ")") encs) (cexInfo storageReads) ps    where-    ps = Expr.concKeccakProps psPreConc+    ps = if simp then Expr.concKeccakSimpProps psPreConc else Expr.concKeccakProps psPreConc     (psElim, bufs, stores) = eliminateProps ps-    abst@(AbstState exprToInt _) = AbstState mempty 0 -    props = map toProp (Map.toList exprToInt)-      where-      toProp :: (Expr EWord, Int) -> Prop-      toProp (e, num) = PEq e (Var (TS.pack ("abst_" ++ (show num))))-     -- Props storing info that need declaration(s)     toDeclarePs     = ps <> keccAssump <> keccComp     toDeclarePsElim = psElim <> keccAssump <> keccComp      -- vars, frames, and block contexts in need of declaration-    allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals <> [abstrVars abst]+    allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals     frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals     blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals--    abstrVars :: AbstState -> [Builder]-    abstrVars (AbstState b _) = map ((\v->fromString ("abst_" ++ show v)) . snd) (Map.toList b)+    gasOrder = enforceGasOrder psPreConc      -- Buf, Storage, etc. declarations needed     bufVals = Map.elems bufs     storeVals = Map.elems stores     storageReads = Map.unionsWith (<>) $ fmap findStorageReads toDeclarePs     abstractStores = Set.toList $ Set.unions (fmap referencedAbstractStores toDeclarePs)-    addresses = Set.toList $ Set.unions (fmap referencedWAddrs toDeclarePs)+    addresses = Set.toList $ Set.unions (fmap referencedAddrs toDeclarePs)      -- Keccak assertions: concrete values, distance between pairs, injectivity, etc.     --      This will make sure concrete values of Keccak are asserted, if they can be computed (i.e. can be concretized)@@ -283,6 +221,10 @@       assumps <- mapM assertSMT $ assertReads psElim bufs stores       pure $ smt2Line "; read assumptions" <> SMT2 assumps mempty mempty +    cexInfo :: Map (Expr 'EAddr, Maybe W256) (Set (Expr 'EWord)) -> CexVars+    cexInfo a = mempty { storeReads = a }++ referencedAbstractStores :: TraversableTerm a => a -> Set Builder referencedAbstractStores term = foldTerm go mempty term   where@@ -290,11 +232,11 @@       AbstractStore s idx -> Set.singleton (storeName s idx)       _ -> mempty -referencedWAddrs :: TraversableTerm a => a -> Set Builder-referencedWAddrs term = foldTerm go mempty term+referencedAddrs :: TraversableTerm a => a -> Set Builder+referencedAddrs term = foldTerm go mempty term   where     go = \case-      WAddr(a@(SymAddr _)) -> Set.singleton (formatEAddr a)+      SymAddr a -> Set.singleton (formatEAddr (SymAddr a))       _ -> mempty  referencedBufs :: TraversableTerm a => a -> [Builder]@@ -318,9 +260,10 @@   where     go :: Expr a -> [(Builder, [Prop])]     go = \case-      TxValue -> [(fromString "txvalue", [])]-      v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]-      Gas {} -> internalError "TODO: GAS"+      o@TxValue -> [(fromRight' $ exprToSMT o, [])]+      o@(Balance _) -> [(fromRight' $ exprToSMT o, [PLT o (Lit $ 2 ^ (96 :: Int))])]+      o@(Gas _ _) -> [(fromRight' $ exprToSMT o, [])]+      o@(CodeHash (LitAddr _)) -> [(fromRight' $ exprToSMT o, [])]       _ -> []  referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]@@ -370,11 +313,10 @@ -- 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+assertReads props benv senv = nubOrd $ concatMap assertRead allReads   where     assertRead :: (Expr EWord, Expr EWord, Expr Buf) -> [Prop]     assertRead (_, Lit 0, _) = []-    assertRead (idx, Lit 32, buf) = [PImpl (PGEq idx (bufLength buf)) (PEq (ReadWord idx buf) (Lit 0))]     assertRead (idx, Lit sz, buf) = [PImpl (PGEq (Expr.add idx $ Lit offset) (bufLength buf)) (PEq (ReadByte (Expr.add idx $ Lit offset) buf) (LitByte 0)) | offset <- [(0::W256).. sz-1]]     assertRead (_, _, _) = internalError "Cannot generate assertions for accesses of symbolic size" @@ -431,12 +373,36 @@     cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names }  -- Given a list of variable names, create an SMT2 object with the variables declared-declareAddrs :: [Builder] -> SMT2-declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cexvars mempty+declareConstrainAddrs :: [Builder] -> SMT2+declareConstrainAddrs names = SMT2 (["; concrete and symbolic addresses"] <> fmap declare names <> fmap assume names) cexvars mempty   where     declare n = "(declare-fun " <> n <> " () Addr)"+    -- assume that symbolic addresses do not collide with the zero address or precompiles+    assume n = "(assert (bvugt " <> n <> " (_ bv9 160)))"     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names } +-- The gas is a tuple of (prefix, index). Within each prefix, the gas is strictly decreasing as the+-- index increases. This function gets a map of Prefix -> [Int], and for each prefix,+-- enforces the order+enforceGasOrder :: [Prop] -> SMT2+enforceGasOrder ps = SMT2 (["; gas ordering"] <> (concatMap (uncurry order) indices)) mempty mempty+  where+    order :: TS.Text -> [Int] -> [Builder]+    order prefix n = consecutivePairs (nubInt n) >>= \(x, y)->+      -- The GAS instruction itself costs gas, so it's strictly decreasing+      ["(assert (bvugt " <> fromRight' (exprToSMT (Gas prefix x)) <> " " <>+        fromRight' ((exprToSMT (Gas prefix y))) <> "))"]+    consecutivePairs :: [Int] -> [(Int, Int)]+    consecutivePairs [] = []+    consecutivePairs l@(_:t) = zip l t+    indices = Map.toList $ toMapOfLists $ concatMap (foldProp go mempty) ps+    toMapOfLists :: [(TS.Text, Int)] -> Map.Map TS.Text [Int]+    toMapOfLists = foldr (\(k, v) acc -> Map.insertWith (++) k [v] acc) Map.empty+    go :: Expr a -> [(TS.Text, Int)]+    go e = case e of+      Gas prefix v -> [(prefix, v)]+      _ -> []+ declareFrameContext :: [(Builder, [Prop])] -> Err SMT2 declareFrameContext names = do   decls <- concatMapM declare names@@ -704,9 +670,14 @@   Add a b -> op2 "bvadd" a b   Sub a b -> op2 "bvsub" a b   Mul a b -> op2 "bvmul" a b-  Exp a b -> case b of-               Lit b' -> expandExp a b'-               _ -> Left "cannot encode symbolic exponentiation into SMT"+  Exp a b -> case a of+    -- Lit 1 has already been handled via Expr.simplify+    Lit 0 -> do+      benc <- exprToSMT b+      pure $ "(ite (= " <> benc `sp` zero <> " ) " <> one `sp` zero <> ")"+    _ -> case b of+      Lit b' -> expandExp a b'+      _ -> Left $ "Cannot encode symbolic exponent into SMT. Offending symbolic value: " <> show b   Min a b -> do     aenc <- exprToSMT a     benc <- exprToSMT b@@ -756,18 +727,18 @@     aExp <- exprToSMT a     bExp <- exprToSMT b     cExp <- exprToSMT c-    let aLift = "(concat (_ bv0 256) " <> aExp <> ")"-        bLift = "(concat (_ bv0 256) " <> bExp <> ")"-        cLift = "(concat (_ bv0 256) " <> cExp <> ")"-    pure $ "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvmul " <> aLift `sp` bLift <> ")" <> cLift <> ")))"+    let aLift = "((_ zero_extend 256) " <> aExp <> ")"+        bLift = "((_ zero_extend 256) " <> bExp <> ")"+        cLift = "((_ zero_extend 256) " <> cExp <> ")"+    pure $ "(ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 256) ((_ extract 255 0) (bvurem (bvmul " <> aLift `sp` bLift <> ")" <> cLift <> ")))"   AddMod a b c -> do     aExp <- exprToSMT a     bExp <- exprToSMT b     cExp <- exprToSMT c-    let aLift = "(concat (_ bv0 256) " <> aExp <> ")"-        bLift = "(concat (_ bv0 256) " <> bExp <> ")"-        cLift = "(concat (_ bv0 256) " <> cExp <> ")"-    pure $ "((_ extract 255 0) (ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 512) (bvurem (bvadd " <> aLift `sp` bLift <> ")" <> cLift <> ")))"+    let aLift = "((_ zero_extend 1) " <> aExp <> ")"+        bLift = "((_ zero_extend 1) " <> bExp <> ")"+        cLift = "((_ zero_extend 1) " <> cExp <> ")"+    pure $ "(ite (= " <> cExp <> " (_ bv0 256)) (_ bv0 256) ((_ extract 255 0) (bvurem (bvadd " <> aLift `sp` bLift <> ")" <> cLift <> ")))"   EqByte a b -> do     cond <- op2 "=" a b     pure $ "(ite " <> cond `sp` one `sp` zero <> ")"@@ -844,6 +815,9 @@     encPrev <- exprToSMT prev     pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")"   SLoad idx store -> op2 "select" store idx+  LitAddr n -> pure $ fromLazyText $ "(_ bv" <> T.pack (show (into n :: Integer)) <> " 160)"+  CodeHash a@(LitAddr _) -> pure $ fromLazyText "codehash_" <> formatEAddr a+  Gas prefix var -> pure $ fromLazyText $ "gas_" <> T.pack (TS.unpack prefix) <> T.pack (show var)    a -> internalError $ "TODO: implement: " <> show a   where@@ -920,6 +894,8 @@ -- | Unrolls an exponentiation into a series of multiplications expandExp :: Expr EWord -> W256 -> Err Builder expandExp base expnt+  -- in EVM, anything (including 0) to the power of 0 is 1+  | expnt == 0 = pure one   | expnt == 1 = exprToSMT base   | otherwise = do     b <- exprToSMT base@@ -929,9 +905,11 @@ -- | Concatenates a list of bytes into a larger bitvector concatBytes :: [Expr Byte] -> Err Builder concatBytes bytes = do-  let bytesRev = reverse bytes-  a2 <- exprToSMT (head bytesRev)-  foldM wrap a2 $ tail bytesRev+  case List.uncons $ reverse bytes of+    Nothing -> Left "unexpected empty bytes"+    Just (h, t) -> do+      a2 <- exprToSMT h+      foldM wrap a2 t   where     wrap :: Builder -> Expr a -> Err Builder     wrap inner byte = do@@ -990,9 +968,14 @@ parseW8 :: SpecConstant -> Word8 parseW8 = parseSC +readOrError :: (Num a, Eq a) => ReadS a -> TS.Text -> a+readOrError reader val = fst . headErr . reader . T.unpack . T.fromStrict $ val+  where+    headErr x = fromMaybe (internalError "error reading empty result") $ listToMaybe x+ parseSC :: (Num a, Eq a) => SpecConstant -> a-parseSC (SCHexadecimal a) = fst . head . Numeric.readHex . T.unpack . T.fromStrict $ a-parseSC (SCBinary a) = fst . head . Numeric.readBin . T.unpack . T.fromStrict $ a+parseSC (SCHexadecimal a) = readOrError Numeric.readHex a+parseSC (SCBinary a) = readOrError Numeric.readBin a parseSC sc = internalError $ "cannot parse: " <> show sc  parseErr :: (Show a) => a -> b@@ -1007,6 +990,11 @@   | Just a <- TS.stripPrefix "symaddr_" name = SymAddr a   | otherwise = internalError $ "cannot parse: " <> show name +textToInt :: TS.Text -> Int+textToInt text = case decimal text of+  Right (value, _) -> value+  Left _ -> internalError $ "cannot parse '" <> (TS.unpack text) <> "' into an Int"+ parseBlockCtx :: TS.Text -> Expr EWord parseBlockCtx "origin" = Origin parseBlockCtx "coinbase" = Coinbase@@ -1016,12 +1004,13 @@ parseBlockCtx "gaslimit" = GasLimit parseBlockCtx "chainid" = ChainId parseBlockCtx "basefee" = BaseFee-parseBlockCtx t = internalError $ "cannot parse " <> (TS.unpack t) <> " into an Expr"+parseBlockCtx val = internalError $ "cannot parse '" <> (TS.unpack val) <> "' into an Expr"  parseTxCtx :: TS.Text -> Expr EWord parseTxCtx name   | name == "txvalue" = TxValue   | Just a <- TS.stripPrefix "balance_" name = Balance (parseEAddr a)+  | Just a <- TS.stripPrefix "codehash_" name = CodeHash (parseEAddr a)   | otherwise = internalError $ "cannot parse " <> (TS.unpack name) <> " into an Expr"  getAddrs :: (TS.Text -> Expr EAddr) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EAddr) Addr)@@ -1095,9 +1084,7 @@                 :| [SortSymbol (IdIndexed "BitVec" (IxNumeral "8" :| []))]               )             )) ((TermSpecConstant val :| [])))-            -> case val of-                 SCHexadecimal "00" -> Base 0 0-                 v -> Base (parseW8 v) len+            -> Base (parseW8 val) len            -- writing a byte over some array           (TermApplication

@@ -4,6 +4,7 @@ module EVM.Solidity   ( solidity   , solcRuntime+  , solcRuntime'   , yul   , yulRuntime   , JumpType (..)@@ -20,6 +21,7 @@   , Reference(..)   , Mutability(..)   , readBuildOutput+  , readFilteredBuildOutput   , functionAbi   , makeSrcMaps   , readSolc@@ -44,12 +46,13 @@  import Optics.Core import Optics.Operators.Unsafe-import EVM.Effects;+import EVM.Effects+import EVM.Expr (maybeLitByteSimp)  import Control.Applicative import Control.Monad import Control.Monad.IO.Unlift-import Data.Aeson hiding (json)+import Data.Aeson (encode) import Data.Aeson.Types import Data.Aeson.Optics import Data.Aeson.Key qualified as Key@@ -84,7 +87,7 @@ import System.Process import Text.Read (readMaybe) import Witch (unsafeInto)-+import Data.Either.Extra (maybeToEither)  data StorageItem = StorageItem   { slotType :: SlotType@@ -284,17 +287,22 @@     go c (xs, state, p)                        = (xs, internalError ("srcmap: y u " ++ show c ++ " in state" ++ show state ++ "?!?"), p)  -- | Reads all solc output json files found under the provided filepath and returns them merged into a BuildOutput-readBuildOutput :: App m => FilePath -> ProjectType -> m (Either String BuildOutput)-readBuildOutput root CombinedJSON = do+readBuildOutput :: App m => FilePath -> ProjectType -> m (Err BuildOutput)+readBuildOutput root projectType = readFilteredBuildOutput root (const True) projectType++readFilteredBuildOutput :: App m => FilePath -> (FilePath -> Bool) -> ProjectType -> m (Err BuildOutput)+readFilteredBuildOutput root jsonFilter CombinedJSON = do   let outDir = root </> "out"-  jsons <- liftIO $ findJsonFiles outDir+  allJsons <- liftIO $ findJsonFiles outDir+  let jsons = filter jsonFilter allJsons   case jsons of     [x] -> readSolc CombinedJSON root (outDir </> x)     [] -> pure . Left $ "no json files found in: " <> outDir     _ -> pure . Left $ "multiple json files found in: " <> outDir-readBuildOutput root _ = do+readFilteredBuildOutput root jsonFilter _ = do   let outDir = root </> "out"-  jsons <- liftIO $ findJsonFiles outDir+  allJsons <- liftIO $ findJsonFiles outDir+  let jsons = filter jsonFilter allJsons   case (filterMetadata jsons) of     [] -> pure . Left $ "no json files found in: " <> outDir     js -> do@@ -341,7 +349,7 @@     then Nothing     else Just (s1 - s2, min (s2 + n2 - s1) n1) -readSolc :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)+readSolc :: App m => ProjectType -> FilePath -> FilePath -> m (Err BuildOutput) readSolc pt root fp = do   -- NOTE: we cannot and must not use Data.Text.IO.readFile because that takes the locale   --       and may fail with very strange errors when the JSON it's reading@@ -349,16 +357,17 @@   fileContents <- liftIO $ fmap Data.Text.Encoding.decodeUtf8 $ Data.ByteString.readFile fp   let contractName = T.pack $ takeBaseName fp   case readJSON pt contractName fileContents of-      Nothing -> pure . Left $ "unable to parse " <> show pt <> " project JSON: " <> fp <> " Contract: " <> show contractName-      Just (contracts, asts, sources) -> do+      Left err -> pure . Left $ "unable to parse " <> show pt <> " project JSON: " <> fp+        <> " Contract: " <> show contractName <> "\nError: " <> err+      Right (contracts, asts, sources) -> do         conf <- readConfig-        when (conf.debug) $ liftIO $ putStrLn $ "Parsed constract: " <> show contractName <> " file: " <> fp+        when (conf.debug) $ liftIO $ putStrLn $ "Parsed contract: " <> show contractName <> " file: " <> fp         sourceCache <- liftIO $ makeSourceCache root sources asts         pure (Right (BuildOutput contracts sourceCache))  yul :: Text -> Text -> IO (Maybe ByteString) yul contractName src = do-  json <- solc Yul src+  json <- solc Yul src False   let f = (json ^?! key "contracts") ^?! key (Key.fromText "hevm.sol")       c = f ^?! key (Key.fromText $ if T.null contractName then "object" else contractName)       bytecode = c ^?! key "evm" ^?! key "bytecode" ^?! key "object" % _String@@ -366,7 +375,7 @@  yulRuntime :: Text -> Text -> IO (Maybe ByteString) yulRuntime contractName src = do-  json <- solc Yul src+  json <- solc Yul src False   let f = (json ^?! key "contracts") ^?! key (Key.fromText "hevm.sol")       c = f ^?! key (Key.fromText $ if T.null contractName then "object" else contractName)       bytecode = c ^?! key "evm" ^?! key "deployedBytecode" ^?! key "object" % _String@@ -376,28 +385,34 @@   :: (MonadUnliftIO m)   => Text -> Text -> m (Maybe ByteString) solidity contract src = liftIO $ do-  json <- solc Solidity src+  json <- solc Solidity src False   let (Contracts sol, _, _) = fromJust $ readStdJSON json   pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.creationCode) -solcRuntime+solcRuntime'   :: App m-  => Text -> Text -> m (Maybe ByteString)-solcRuntime contract src = do+  => Text -> Text -> Bool -> m (Maybe ByteString)+solcRuntime' contract src viaIR = do   conf <- readConfig   liftIO $ do-    json <- solc Solidity src+    json <- solc Solidity src viaIR     when conf.dumpExprs $ liftIO $ Data.Text.IO.writeFile "compiled_code.json" json     case readStdJSON json of       Just (Contracts sol, _, _) -> pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.runtimeCode)       Nothing -> internalError $ "unable to parse solidity output:\n" <> (T.unpack json) +solcRuntime+  :: App m+  => Text -> Text -> m (Maybe ByteString)+solcRuntime contract src = solcRuntime' contract src False+ functionAbi :: Text -> IO Method functionAbi f = do-  json <- solc Solidity ("contract ABI { function " <> f <> " public {}}")+  json <- solc Solidity ("contract ABI { function " <> f <> " public {}}") False   let (Contracts sol, _, _) = fromMaybe-                                (internalError . T.unpack $ "unable to parse solc output:\n" <> json)-                                (readStdJSON json)+        (internalError . T.unpack $ "while trying to parse function signature `"+          <> f <> "`, unable to parse solc output:\n" <> json)+        (readStdJSON json)   case Map.toList (fromJust (Map.lookup "hevm.sol:ABI" sol)).abiMap of     [(_,b)] -> pure b     _ -> internalError "unexpected abi format"@@ -405,31 +420,31 @@ force :: String -> Maybe a -> a force s = fromMaybe (internalError s) -readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)+readJSON :: ProjectType -> Text -> Text -> Err (Contracts, Asts, Sources) readJSON CombinedJSON _ json = readCombinedJSON json readJSON _ contractName json = readFoundryJSON contractName json  -- | Reads a foundry json output-readFoundryJSON :: Text -> Text -> Maybe (Contracts, Asts, Sources)+readFoundryJSON :: Text -> Text -> Err (Contracts, Asts, Sources) readFoundryJSON contractName json = do-  runtime <- json ^? key "deployedBytecode"-  runtimeCode <- (toCode contractName) . strip0x'' <$> runtime ^? key "object" % _String+  runtime <- maybeToEither "missing 'deployedBytecode' field" $ json ^? key "deployedBytecode"+  runtimeCode <- maybeToEither "missing 'deployedBytecode.object' field" $+    (toCode contractName) . strip0x'' <$> runtime ^? key "object" % _String   runtimeSrcMap <- case runtime ^? key "sourceMap" % _String of-    Nothing -> makeSrcMaps ""-    smap -> makeSrcMaps =<< smap+    Nothing -> Right $ force "Source map creation error" $ makeSrcMaps ""  -- sourceMap is optional+    Just smap -> maybeToEither "invalid sourceMap format" $ makeSrcMaps smap -  creation <- json ^? key "bytecode"-  creationCode <- (toCode contractName) . strip0x'' <$> creation ^? key "object" % _String+  creation <- maybeToEither "missing 'bytecode' field" $ json ^? key "bytecode"+  creationCode <- maybeToEither "missing 'bytecode.object' field" $+    (toCode contractName) . strip0x'' <$> creation ^? key "object" % _String   creationSrcMap <- case creation ^? key "sourceMap" % _String of-    Nothing -> makeSrcMaps ""-    smap -> makeSrcMaps =<< smap--  ast <- json ^? key "ast"-  path <- ast ^? key "absolutePath" % _String--  abi <- toList <$> json ^? key "abi" % _Array+    Nothing -> Right $ force "Source map creation error" $ makeSrcMaps ""  -- sourceMap is optional+    Just smap -> maybeToEither "invalid sourceMap format" $ makeSrcMaps smap -  id' <- unsafeInto <$> json ^? key "id" % _Integer+  ast <- maybeToEither "missing 'ast' field. Recompile with `forge clean && forge build --ast`" $ json ^? key "ast"+  path <- maybeToEither "missing 'ast.absolutePath' field" $ ast ^? key "absolutePath" % _String+  abi <- maybeToEither "missing or invalid 'abi' array" $ toList <$> json ^? key "abi" % _Array+  id' <- maybeToEither "missing or invalid 'id' field" $ unsafeInto <$> json ^? key "id" % _Integer    let contract = SolcContract         { runtimeCodehash     = keccak' (stripBytecodeMetadata runtimeCode)@@ -446,10 +461,10 @@         , storageLayout       = mkStorageLayout $ json ^? key "storageLayout"         , immutableReferences = mempty -- TODO: foundry doesn't expose this?         }-  pure ( Contracts $ Map.singleton (path <> ":" <> contractName) contract-         , Asts      $ Map.singleton path ast-         , Sources   $ Map.singleton (SrcFile id' (T.unpack path)) Nothing-         )+  Right ( Contracts $ Map.singleton (path <> ":" <> contractName) contract+        , Asts      $ Map.singleton path ast+        , Sources   $ Map.singleton (SrcFile id' (T.unpack path)) Nothing+        )  -- | Parses the standard json output from solc readStdJSON :: Text -> Maybe (Contracts, Asts, Sources)@@ -507,18 +522,18 @@       }, fromMaybe mempty srcContents))  -- deprecate me soon-readCombinedJSON :: Text -> Maybe (Contracts, Asts, Sources)+readCombinedJSON :: Text -> Err (Contracts, Asts, Sources) readCombinedJSON json = do-  contracts <- f . KeyMap.toHashMapText <$> (json ^? key "contracts" % _Object)-  sources <- toList . fmap (preview _String) <$> json ^? key "sourceList" % _Array+  contracts <- maybeToEither "missing or invalid 'contracts' field" $ f . KeyMap.toHashMapText <$> (json ^? key "contracts" % _Object)+  sources <- maybeToEither "missing or invalid 'sourceList' field" $ toList . fmap (preview _String) <$> json ^? key "sourceList" % _Array+  astsPre <- maybeToEither "JSON lacks abstract syntax trees (ast). Recompile with `forge clean && forge build --ast`" $ json ^? key "sources" % _Object   pure ( Contracts contracts-       , Asts (Map.fromList (HMap.toList asts))+       , Asts (Map.fromList (HMap.toList (KeyMap.toHashMapText astsPre)))        , Sources $ Map.fromList $            (\(path, id') -> (SrcFile id' (T.unpack path), Nothing)) <$>              zip (catMaybes sources) [0..]        )   where-    asts = KeyMap.toHashMapText $ fromMaybe (error "JSON lacks abstract syntax trees.") (json ^? key "sources" % _Object)     f x = Map.fromList . HMap.toList $ HMap.mapWithKey g x     g s x =       let@@ -667,21 +682,22 @@             then error $ T.unpack ("Error toCode: unlinked libraries detected in bytecode, in " <> contractName)             else error $ T.unpack ("Error toCode:" <> e <> ", in " <> contractName) -solc :: Language -> Text -> IO Text-solc lang src = T.pack <$> readProcess "solc" ["--standard-json"] (T.unpack $ stdjson lang src)+solc :: Language -> Text -> Bool -> IO Text+solc lang src viaIR = T.pack <$> readProcess "solc" ["--standard-json"] (T.unpack $ stdjson lang src viaIR)  data Language = Solidity | Yul   deriving (Show) -data StandardJSON = StandardJSON Language Text+data StandardJSON = StandardJSON Language Text Bool -- more options later perhaps  instance ToJSON StandardJSON where-  toJSON (StandardJSON lang src) =+  toJSON (StandardJSON lang src viaIR) =     object [ "language" .= show lang            , "sources" .= object ["hevm.sol" .= object ["content" .= src]]            , "settings" .=-             object [ "outputSelection" .=+             object [ "viaIR" .= viaIR+                    , "outputSelection" .=                     object ["*" .=                       object ["*" .= (toJSON                               ["metadata" :: String,@@ -703,8 +719,8 @@                     ]            ] -stdjson :: Language -> Text -> Text-stdjson lang src = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src+stdjson :: Language -> Text -> Bool -> Text+stdjson lang src viaIR = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src viaIR  -- | When doing CREATE and passing constructor arguments, Solidity loads -- the argument data via the creation bytecode, since there is no "calldata"@@ -729,7 +745,7 @@ stripBytecodeMetadataSym b =   let     concretes :: [Maybe Word8]-    concretes = maybeLitByte <$> b+    concretes = maybeLitByteSimp <$> b     bzzrs :: [[Maybe Word8]]     bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs

@@ -10,14 +10,17 @@ import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..)) import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan) import Control.Concurrent (forkIO, killThread)+import Control.Concurrent.STM (writeTChan, newTChan, TChan, tryReadTChan, atomically) import Control.Monad import Control.Monad.State.Strict import Control.Monad.IO.Unlift import Data.Char (isSpace) import Data.Map (Map) import Data.Map qualified as Map+import Data.Set (Set, isSubsetOf, fromList) import Data.Maybe (fromMaybe, isJust, fromJust) import Data.Either (isLeft)+import Data.Text qualified as TStrict import Data.Text.Lazy (Text) import Data.Text.Lazy qualified as T import Data.Text.Lazy.IO qualified as T@@ -26,9 +29,12 @@ import Witch (into) import EVM.Effects import EVM.Fuzz (tryCexFuzz)+import Data.Bits ((.&.))+import Numeric (showHex)+import EVM.Expr (simplifyProps)  import EVM.SMT-import EVM.Types (W256, Expr(AbstractBuf), internalError, Err, getError, getNonError)+import EVM.Types  -- | Supported solvers data Solver@@ -55,117 +61,229 @@ -- | A channel representing a group of solvers newtype SolverGroup = SolverGroup (Chan Task) --- | A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written-data Task = Task-  { script :: SMT2-  , resultChan :: Chan CheckSatResult+data MultiSol = MultiSol+  { maxSols :: Int+  , numBytes :: Int+  , var :: String   } --- | The result of a call to (check-sat)-data CheckSatResult-  = Sat SMTCex-  | Unsat-  | Unknown String-  | Error String+-- | A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written+data Task = TaskSingle SingleData | TaskMulti MultiData++newtype CacheEntry = CacheEntry [Prop]   deriving (Show, Eq) -isSat :: CheckSatResult -> Bool-isSat (Sat _) = True-isSat _ = False+data MultiData = MultiData+  { smt2 :: SMT2+  , multiSol :: MultiSol+  , resultChan :: Chan (Maybe [W256])+  } -isUnsat :: CheckSatResult -> Bool-isUnsat Unsat = True-isUnsat _ = False+data SingleData = SingleData+  { smt2 :: SMT2+  , props :: Maybe [Prop]+  , resultChan :: Chan SMTResult+  } -checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult-checkSat (SolverGroup taskQueue) script = do-  if isLeft script then pure $ Error $ getError script+-- returns True if a is a superset of any of the sets in bs+supersetAny :: Set Prop -> [Set Prop] -> Bool+supersetAny a bs = any (`isSubsetOf` a) bs++checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])+checkMulti (SolverGroup taskq) smt2 multiSol = do+  if isLeft smt2 then pure Nothing   else do     -- prepare result channel     resChan <- newChan     -- send task to solver group-    writeChan taskQueue (Task (getNonError script) resChan)+    writeChan taskq (TaskMulti (MultiData (getNonError smt2) multiSol resChan))     -- collect result     readChan resChan -writeSMT2File :: SMT2 -> Int -> IO ()-writeSMT2File smt2 count =+checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (SMTResult, Err SMT2)+checkSatWithProps sg props = do+  conf <- readConfig+  let psSimp = if conf.simp then simplifyProps props else props+  if psSimp == [PBool False] then pure (Qed, Right mempty)+  else do+    let smt2 = assertProps conf psSimp+    if isLeft smt2 then+      let err = getError smt2 in pure (Error err, Left err)+    else do+      res <- liftIO $ checkSat sg (Just props) smt2+      pure (res, Right (getNonError smt2))++-- When props is Nothing, the cache will not be filled or used+checkSat :: SolverGroup -> Maybe [Prop] -> Err SMT2 -> IO SMTResult+checkSat (SolverGroup taskq) props smt2 = do+  if isLeft smt2 then pure $ Error $ getError smt2+  else do+    -- prepare result channel+    resChan <- newChan+    -- send task to solver group+    writeChan taskq (TaskSingle (SingleData (getNonError smt2) props resChan))+    -- collect result+    readChan resChan++writeSMT2File :: SMT2 -> String -> IO ()+writeSMT2File smt2 postfix = do     let content = formatSMT2 smt2 <> "\n\n(check-sat)"-    in T.writeFile ("query-" <> (show count) <> ".smt2") content+    T.writeFile ("query-" <> postfix <> ".smt2") content  withSolvers :: App m => Solver -> Natural -> Natural -> Maybe Natural -> (SolverGroup -> m a) -> m a withSolvers solver count threads timeout cont = do     -- spawn solvers     instances <- mapM (const $ liftIO $ spawnSolver solver threads timeout) [1..count]     -- spawn orchestration thread-    taskQueue <- liftIO newChan+    taskq <- liftIO newChan+    cacheq <- liftIO . atomically $ newTChan     availableInstances <- liftIO newChan     liftIO $ forM_ instances (writeChan availableInstances)-    orchestrate' <- toIO $ orchestrate taskQueue availableInstances 0+    orchestrate' <- toIO $ orchestrate taskq cacheq availableInstances [] 0     orchestrateId <- liftIO $ forkIO orchestrate'      -- run continuation with task queue-    res <- cont (SolverGroup taskQueue)+    res <- cont (SolverGroup taskq)      -- cleanup and return results     liftIO $ mapM_ (stopSolver) instances     liftIO $ killThread orchestrateId     pure res   where-    orchestrate :: App m => Chan Task -> Chan SolverInstance -> Int -> m b-    orchestrate queue avail fileCounter = do-      task <- liftIO $ readChan queue-      inst <- liftIO $ readChan avail-      runTask' <- toIO $ runTask task inst avail fileCounter-      _ <- liftIO $ forkIO runTask'-      orchestrate queue avail (fileCounter + 1)+    orchestrate :: App m => Chan Task -> TChan CacheEntry -> Chan SolverInstance -> [Set Prop] -> Int -> m b+    orchestrate taskq cacheq avail knownUnsat fileCounter = do+      conf <- readConfig+      mx <- liftIO . atomically $ tryReadTChan cacheq+      case mx of+        Just (CacheEntry props)  -> do+          let knownUnsat' = (fromList props):knownUnsat+          when conf.debug $ liftIO $ putStrLn "   adding UNSAT cache"+          orchestrate taskq cacheq avail knownUnsat' fileCounter+        Nothing -> do+          task <- liftIO $ readChan taskq+          case task of+            TaskSingle (SingleData _ props r) | isJust props && supersetAny (fromList (fromJust props)) knownUnsat -> do+              liftIO $ writeChan r Qed+              when conf.debug $ liftIO $ putStrLn "   Qed found via cache!"+              orchestrate taskq cacheq avail knownUnsat fileCounter+            _ -> do+              inst <- liftIO $ readChan avail+              runTask' <- case task of+                TaskSingle (SingleData smt2 props r) -> toIO $ getOneSol smt2 props r cacheq inst avail fileCounter+                TaskMulti (MultiData smt2 multiSol r) -> toIO $ getMultiSol smt2 multiSol r inst avail fileCounter+              _ <- liftIO $ forkIO runTask'+              orchestrate taskq cacheq avail knownUnsat (fileCounter + 1) -    runTask :: (MonadIO m, ReadConfig m) => Task -> SolverInstance -> Chan SolverInstance -> Int -> m ()-    runTask (Task smt2@(SMT2 cmds cexvars ps) r) inst availableInstances fileCounter = do+getMultiSol :: forall m. (MonadIO m, ReadConfig m) => SMT2 -> MultiSol -> (Chan (Maybe [W256])) -> SolverInstance -> Chan SolverInstance -> Int -> m ()+getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCounter = do+  conf <- readConfig+  when conf.dumpQueries $ liftIO $ writeSMT2File smt2 (show fileCounter)+  -- reset solver and send all lines of provided script+  out <- liftIO $ sendScript inst ("(reset)" : cmds)+  case out of+    Left err -> liftIO $ do+      when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)+      writeChan r Nothing+    Right _ -> do+      sat <- liftIO $ sendLine inst "(check-sat)"+      when conf.dumpQueries $ liftIO $ writeSMT2File smt2 (show fileCounter <> "-origquery")+      subRun [] smt2 sat+  -- put the instance back in the list of available instances+  liftIO $ writeChan availableInstances inst+  where+    maskFromBytesCount k+      | k <= 32 = (2 ^ (8 * k) - 1)+      | otherwise = internalError "Byte length exceeds 256-bit capacity"+    subRun :: (MonadIO m, ReadConfig m) => [W256] -> SMT2 -> Text -> m ()+    subRun vals fullSmt sat = do       conf <- readConfig-      let fuzzResult = tryCexFuzz ps conf.numCexFuzz-      liftIO $ do-        when (conf.dumpQueries) $ writeSMT2File smt2 fileCounter-        if (isJust fuzzResult)-          then do-            when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)-            writeChan r (Sat $ fromJust fuzzResult)-          else if not conf.onlyCexFuzz then do-            when (conf.debug) $ putStrLn "   Fuzzing failed to find a Cex"-            -- reset solver and send all lines of provided script-            out <- sendScript inst (SMT2 ("(reset)" : cmds) mempty ps)-            case out of-              -- if we got an error then return it-              Left e -> writeChan r (Error $ "Error while writing SMT to solver: " <> T.unpack e)-              -- otherwise call (check-sat), parse the result, and send it down the result channel-              Right () -> do-                sat <- sendLine inst "(check-sat)"-                res <- do-                    case sat of-                      "unsat" -> pure Unsat-                      "timeout" -> pure $ Unknown "Result timeout by SMT solver"-                      "unknown" -> pure $ Unknown "Result unknown by SMT solver"-                      "sat" -> Sat <$> getModel inst cexvars-                      _ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat-                writeChan r res+      case sat of+        "unsat" -> liftIO $ do+          when conf.debug $ putStrLn $ "No more solutions to query, returning: " <> show vals+          liftIO $ writeChan r (Just vals)+        "timeout" -> liftIO $ do+           when conf.debug $ putStrLn "Timeout inside SMT solver."+           writeChan r Nothing+        "unknown" -> liftIO $ do+           when conf.debug $ putStrLn "Unknown result by SMT solver."+           writeChan r Nothing+        "sat" -> do+          if length vals >= multiSol.maxSols then liftIO $ do+            when conf.debug $ putStrLn "Too many solutions to symbolic query."+            writeChan r Nothing           else do-            when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"-            writeChan r $ Error "Option onlyCexFuzz enabled, not running SMT"+            cex <- liftIO $ getModel inst cexvars+            case Map.lookup (Var (TStrict.pack multiSol.var)) cex.vars of+              Just v -> do+                let hexMask = maskFromBytesCount multiSol.numBytes+                    maskedVal = v .&. hexMask+                    toSMT n = show (into n :: Integer)+                    maskedVar = "(bvand " <> multiSol.var <> " (_ bv" <> toSMT hexMask <> " 256))"+                    restrict = "(assert (not (= " <> maskedVar <> " (_ bv" <> toSMT maskedVal <> " 256))))"+                    newSmt = fullSmt <> SMT2 [(fromString restrict)] mempty mempty+                when conf.debug $ liftIO $ putStrLn $ "Got one solution to symbolic query, val: 0x" <> (showHex maskedVal "") <>+                  " now have " <> show (length vals + 1) <> " solution(s), max is: " <> show multiSol.maxSols+                when conf.dumpQueries $ liftIO $ writeSMT2File newSmt (show fileCounter <> "-sol" <> show (length vals))+                out <- liftIO $ sendLine inst (T.pack restrict)+                case out of+                  "success" -> do+                    out2 <- liftIO $ sendLine inst  (T.pack "(check-sat)")+                    subRun (maskedVal:vals) newSmt out2+                  err -> liftIO $ do+                    when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)+                    writeChan r Nothing+              Nothing -> internalError $ "variable " <>  multiSol.var <> " not part of model (i.e. cex) ... that's not possible"+        err -> liftIO $ do+          when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)+          writeChan r Nothing -        -- put the instance back in the list of available instances-        writeChan availableInstances inst+getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> SolverInstance -> Chan SolverInstance -> Int -> m ()+getOneSol smt2@(SMT2 cmds cexvars ps) props r cacheq inst availableInstances fileCounter = do+  conf <- readConfig+  let fuzzResult = tryCexFuzz ps conf.numCexFuzz+  liftIO $ do+    when (conf.dumpQueries) $ writeSMT2File smt2 (show fileCounter)+    if (isJust fuzzResult)+      then do+        when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)+        writeChan r (Cex $ fromJust fuzzResult)+      else if Prelude.not conf.onlyCexFuzz then do+        -- reset solver and send all lines of provided script+        out <- sendScript inst ("(reset)" : cmds)+        case out of+          -- if we got an error then return it+          Left e -> writeChan r (Error $ "Error while writing SMT to solver: " <> T.unpack e)+          -- otherwise call (check-sat), parse the result, and send it down the result channel+          Right () -> do+            sat <- sendLine inst "(check-sat)"+            res <- do+                case sat of+                  "unsat" -> do+                    when (isJust props) $ liftIO . atomically $ writeTChan cacheq (CacheEntry (fromJust props))+                    pure Qed+                  "timeout" -> pure $ Unknown "Result timeout by SMT solver"+                  "unknown" -> pure $ Unknown "Result unknown by SMT solver"+                  "sat" -> Cex <$> getModel inst cexvars+                  _ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat+            writeChan r res+      else do+        when (conf.debug) $ putStrLn "Fuzzing failed to find a Cex, not trying SMT due to onlyCexFuzz"+        writeChan r $ Error "Option onlyCexFuzz enabled, not running SMT" +    -- 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.buffers   -- 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+  then pure initialModel+  else do+    -- get concrete values for each buffers max read index+    hints <- capHints <$> queryMaxReads (getValue inst) cexvars.buffers+    snd <$> runStateT (shrinkModel hints) initialModel   where     getRaw :: IO SMTCex     getRaw = do@@ -205,24 +323,24 @@     shrinkBuf :: Text -> W256 -> StateT SMTCex IO ()     shrinkBuf buf hint = do       let encBound = "(_ bv" <> (T.pack $ show (into hint :: Integer)) <> " 256)"-      sat <- liftIO $ do+      answer <- liftIO $ do         checkCommand inst "(push 1)"         checkCommand inst $ "(assert (bvule " <> buf <> "_length " <> encBound <> "))"         sendLine inst "(check-sat)"-      case sat of+      case answer of         "sat" -> do           model <- liftIO getRaw           put model         "unsat" -> do           liftIO $ checkCommand inst "(pop 1)"-          shrinkBuf buf (if hint == 0 then hint + 1 else hint * 2)-        e -> internalError $ "Unexpected solver output: " <> (T.unpack e)+          let nextHint = if hint == 0 then 1 else hint * 2+          if nextHint < hint || nextHint > 1_073_741_824+            then pure () -- overflow or over 1GB+            else shrinkBuf buf nextHint+        _ -> do -- unexpected answer -> clean up and do not change the model+          liftIO $ checkCommand inst "(pop 1)"+          pure () -    -- Collapses the abstract description of a models buffers down to a bytestring-    mkConcrete :: SMTCex -> SMTCex-    mkConcrete c = fromMaybe-      (internalError $ "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@@ -259,6 +377,7 @@     , "--interactive"     , "--incremental"     , "--tlimit-per=" <> mkTimeout timeout+    , "--arrays-exp"     ]   Custom _ -> [] @@ -292,8 +411,8 @@ stopSolver (SolverInstance _ stdin stdout process) = cleanupProcess (Just stdin, Just stdout, Nothing, process)  -- | Sends a list of commands to the solver. Returns the first error, if there was one.-sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())-sendScript solver (SMT2 cmds _ _) = do+sendScript :: SolverInstance -> [Builder] -> IO (Either Text ())+sendScript solver cmds = do   let sexprs = splitSExpr $ fmap toLazyText cmds   go sexprs   where