hevm 0.46.0 → 0.47.0

raw patch · 21 files changed

+633/−211 lines, 21 filesdep ~Decimaldep ~aesondep ~base16-bytestringPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: Decimal, aeson, base16-bytestring, brick, haskeline, here, megaparsec, tree-view, vty, witherable

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−0
• hevm-cli/hevm-cli.hs +19/−5
• hevm.cabal +12/−11
• src/EVM.hs +57/−11
• src/EVM/ABI.hs +20/−8
• src/EVM/Dapp.hs +61/−20
• src/EVM/Dev.hs +6/−0
• src/EVM/Emacs.hs +3/−4
• src/EVM/Exec.hs +1/−0
• src/EVM/Facts.hs +2/−2
• src/EVM/Fetch.hs +13/−2
• src/EVM/Format.hs +7/−5
• src/EVM/Solidity.hs +102/−25
• src/EVM/Stepper.hs +9/−0
• src/EVM/SymExec.hs +40/−7
• src/EVM/TTY.hs +29/−19
• src/EVM/Transaction.hs +1/−3
• src/EVM/Types.hs +2/−9
• src/EVM/UnitTest.hs +192/−45
• src/EVM/VMTest.hs +1/−0
• test/test.hs +40/−35

@@ -1,5 +1,21 @@ # hevm changelog +## 0.47.0 - 2021-07-01++- A new test runner for checking invariants against random reachable contract states.+- `hevm symbolic` can search for solc 0.8 style assertion violations, and a new `--assertions` flag+    has been added allowing users to customize which assertions should be reported+- A new cheatcode `ffi(string[])` that executes an arbitrary command in the system shell++### Changed++- Z3 is once again the default smt solver+- Updated nixpkgs to the `21.05` channel++### Fixed++- Sourcemaps for contracts containing `immutable` are now shown in the debug view.+ ## 0.46.0 - 2021-04-29  ### Added

@@ -2,6 +2,8 @@  {-# Language CPP #-} {-# Language DataKinds #-}+{-# Language StandaloneDeriving #-}+{-# Language DeriveAnyClass #-} {-# Language FlexibleInstances #-} {-# Language DeriveGeneric #-} {-# Language GADTs #-}@@ -60,6 +62,7 @@ import Data.Text.IO               (hPutStr) import Data.Maybe                 (fromMaybe, fromJust) import Data.Version               (showVersion)+import Data.DoubleWord            (Word256) import Data.SBV hiding (Word, solver, verbose, name) import Data.SBV.Control hiding (Version, timeout, create) import System.IO                  (hFlush, stdout, stderr)@@ -126,6 +129,7 @@       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"+      , assertions    :: w ::: Maybe [Word256]    <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"       }   | Equivalence -- prove equivalence between two programs       { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"@@ -171,6 +175,7 @@       , debug         :: w ::: Bool                     <?> "Run interactively"       , jsontrace     :: w ::: Bool                     <?> "Print json trace output at every step"       , fuzzRuns      :: w ::: Maybe Int                <?> "Number of times to run fuzz tests"+      , depth         :: w ::: Maybe Int                <?> "Number of transactions to explore"       , replay        :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"@@ -182,6 +187,7 @@       , maxIterations :: w ::: Maybe Integer            <?> "Number of times we may revisit a particular branching point"       , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc4"       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"+      , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"       }   | BcTest -- Run an Ethereum Blockhain/GeneralState test       { file      :: w ::: String    <?> "Path to .json test file"@@ -229,6 +235,9 @@ -- parseField instance for (Text, ByteString) instance Options.ParseField (Text, ByteString) +deriving instance Options.ParseField Word256+deriving instance Options.ParseField [Word256]+ instance Options.ParseRecord (Command Options.Wrapped) where   parseRecord =     Options.parseRecordWithModifiers Options.lispCaseModifiers@@ -284,6 +293,7 @@     , EVM.UnitTest.smtState = Just state     , EVM.UnitTest.verbose = verbose cmd     , EVM.UnitTest.match = pack $ fromMaybe ".*" (match cmd)+    , EVM.UnitTest.maxDepth = depth cmd     , EVM.UnitTest.fuzzRuns = fromMaybe 100 (fuzzRuns cmd)     , EVM.UnitTest.replay = do         arg' <- replay cmd@@ -291,6 +301,7 @@     , EVM.UnitTest.vmModifier = vmModifier     , EVM.UnitTest.testParams = params     , EVM.UnitTest.dapp = srcInfo+    , EVM.UnitTest.allowFFI = ffi cmd     }  main :: IO ()@@ -425,7 +436,7 @@ runSMTWithTimeOut solver maybeTimeout smtdebug symb   | solver == Just "cvc4" = runwithcvc4   | solver == Just "z3" = runwithz3-  | solver == Nothing = runwithcvc4+  | solver == Nothing = runwithz3   | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"  where timeout = fromMaybe 30000 maybeTimeout        runwithz3 = runSMTWith z3{SBV.verbose=smtdebug} $ (setTimeOut timeout) >> symb@@ -503,7 +514,8 @@   else     runSMTWithTimeOut (solver cmd) (smttimeout cmd) (smtdebug cmd) $ query $ do       preState <- symvmFromCommand cmd-      verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case+      let errCodes = fromMaybe defaultPanicCodes (assertions cmd)+      verify preState (maxIterations cmd) rpcinfo (Just $ checkAssertions errCodes) >>= \case         Right tree -> do           io $ putStrLn "Assertion violation found."           showCounterexample preState maybesig@@ -757,7 +769,8 @@           , EVM.vmoptChainId       = word chainid 1           , EVM.vmoptCreate        = create cmd           , EVM.vmoptStorageModel  = ConcreteS-          , EVM.vmoptTxAccessList  = mempty -- TODO: support me soon        +          , EVM.vmoptTxAccessList  = mempty -- TODO: support me soon+          , EVM.vmoptAllowFFI      = False           }         word f def = fromMaybe def (f cmd)         addr f def = fromMaybe def (f cmd)@@ -769,7 +782,7 @@   (miner,blockNum,diff) <- case rpc cmd of     Nothing -> return (0,0,0)     Just url -> io $ EVM.Fetch.fetchBlockFrom block' url >>= \case-      Nothing -> error $ "Could not fetch block"+      Nothing -> error "Could not fetch block"       Just EVM.Block{..} -> return (_coinbase                                    , wordValue _number                                    , wordValue _difficulty@@ -827,7 +840,7 @@                         & set EVM.external    (view EVM.external contract')      (_, _, Just c)  ->-      return $ (EVM.initialContract . codeType $ decipher c)+      return (EVM.initialContract . codeType $ decipher c)     (_, _, Nothing) ->       error "must provide at least (rpc + address) or code" @@ -864,6 +877,7 @@       , EVM.vmoptCreate        = create cmd       , EVM.vmoptStorageModel  = fromMaybe SymbolicS (storageModel cmd)       , EVM.vmoptTxAccessList  = mempty+      , EVM.vmoptAllowFFI      = False       }     word f def = fromMaybe def (f cmd)     addr f def = fromMaybe def (f cmd)

@@ -2,7 +2,7 @@ name:   hevm version:-  0.46.0+  0.47.0 synopsis:   Ethereum virtual machine evaluator description:@@ -81,14 +81,14 @@     ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h   build-depends:     QuickCheck                        >= 2.13.2 && < 2.15,-    Decimal                           == 0.5.1,+    Decimal                           >= 0.5.1 && < 0.6,     containers                        >= 0.6.0 && < 0.7,     deepseq                           >= 1.4.4 && < 1.5,     time                              >= 1.8.0 && < 1.11,     transformers                      >= 0.5.6 && < 0.6,-    tree-view                         == 0.5,+    tree-view                         >= 0.5 && < 0.6,     abstract-par                      >= 0.3.3 && < 0.4,-    aeson                             >= 1.4.6 && < 1.5,+    aeson                             >= 1.5.6 && < 1.6,     bytestring                        >= 0.10.8 && < 0.11,     scientific                        >= 0.3.6 && < 0.4,     binary                            >= 0.8.6 && < 0.9,@@ -96,20 +96,20 @@     unordered-containers              >= 0.2.10 && < 0.3,     vector                            >= 0.12.1 && < 0.13,     ansi-wl-pprint                    >= 0.6.9 && < 0.7,-    base16-bytestring                 >= 0.1.1 && < 0.2,-    brick                             >= 0.47.1 && < 0.56,-    megaparsec                        >= 7.0.5 && < 8.1,+    base16-bytestring                 >= 1.0.0 && < 2.0,+    brick                             >= 0.58 && < 0.63,+    megaparsec                        >= 9.0.0 && < 10.0,     mtl                               >= 2.2.2 && < 2.3,     directory                         >= 1.3.3 && < 1.4,     filepath                          >= 1.4.2 && < 1.5,-    vty                               >= 5.25.1 && < 5.31,+    vty                               >= 5.25.1 && < 5.34,     cereal                            >= 0.5.8 && < 0.6,     cryptonite                        >= 0.27 && < 0.29,     memory                            >= 0.14.18 && < 0.16,     data-dword                        >= 0.3.1 && < 0.4,     fgl                               >= 5.7.0 && < 5.8,     free                              >= 5.1.3 && < 5.2,-    haskeline                         >= 0.7.4 && < 0.8,+    haskeline                         >= 0.8.0 && < 0.9,     process                           >= 1.6.5 && < 1.7,     lens                              >= 4.17.1 && < 4.20,     lens-aeson                        >= 1.0.2 && < 1.2,@@ -125,10 +125,11 @@     semver-range                      >= 0.2.7 && < 0.3,     temporary                         >= 1.3 && < 1.4,     text-format                       >= 0.3.2 && < 0.4,-    witherable                        >= 0.3.5 && < 0.4,+    witherable                        >= 0.3.5 && < 0.5,     wreq                              >= 0.5.3 && < 0.6,     regex-tdfa                        >= 1.2.3 && < 1.4,-    base                              >= 4.9 && < 5+    base                              >= 4.9 && < 5,+    here                              >= 1.2.13 && < 1.3,   hs-source-dirs:     src   default-language:

@@ -17,6 +17,9 @@  import Data.SBV hiding (Word, output, Unknown) import Data.Proxy (Proxy(..))+import Data.Text (unpack)+import Data.Text.Encoding (decodeUtf8, encodeUtf8)+import qualified Data.Vector as V import EVM.ABI import EVM.Types import EVM.Solidity@@ -49,6 +52,7 @@ import qualified Data.Map.Strict      as Map import qualified Data.Sequence        as Seq import qualified Data.Tree.Zipper     as Zipper+import qualified Data.Vector          as V import qualified Data.Vector.Storable as Vector import qualified Data.Vector.Storable.Mutable as Vector @@ -87,6 +91,7 @@   | DeadPath   | NotUnique Whiff   | SMTTimeout+  | FFI AbiVals deriving instance Show Error  -- | The possible result states of a VM@@ -110,12 +115,13 @@   , _burned         :: Word   , _constraints    :: [(SBool, Whiff)]   , _iterations     :: Map CodeLocation Int+  , _allowFFI       :: Bool   }   deriving (Show)  data Trace = Trace-  { _traceCodehash :: W256-  , _traceOpIx     :: Maybe Int+  { _traceOpIx     :: Int+  , _traceContract :: Contract   , _traceData     :: TraceData   }   deriving (Show)@@ -135,6 +141,7 @@   PleaseMakeUnique    :: SymVal a => SBV a -> [SBool] -> (IsUnique a -> EVM ()) -> Query   PleaseFetchSlot     :: Addr -> Word -> (Word -> EVM ()) -> Query   PleaseAskSMT        :: SBool -> [SBool] -> (BranchCondition -> EVM ()) -> Query+  PleaseDoFFI         :: [String] -> (ByteString -> EVM ()) -> Query  data Choose where   PleaseChoosePath    :: Whiff -> (Bool -> EVM ()) -> Choose@@ -155,6 +162,8 @@       (("<EVM.Query: make value "         ++ show val ++ " unique in context "         ++ show constraints ++ ">") ++)+    PleaseDoFFI cmd _ ->+      (("<EVM.Query: do ffi: " ++ (show cmd)) ++)  instance Show Choose where   showsPrec _ = \case@@ -203,6 +212,7 @@   , vmoptCreate :: Bool   , vmoptStorageModel :: StorageModel   , vmoptTxAccessList :: Map Addr [W256]+  , vmoptAllowFFI :: Bool   } deriving Show  -- | A log entry@@ -288,6 +298,18 @@   | RuntimeCode Buffer  -- ^ "Instance" code, after contract creation   deriving (Show) +-- runtime err when used for symbolic code+instance Eq ContractCode where+  (InitCode x) == (InitCode y) = forceBuffer x == forceBuffer y+  (RuntimeCode x) == (RuntimeCode y) = forceBuffer x == forceBuffer y+  _ == _ = False++-- runtime err when used for symbolic code+instance Ord ContractCode where+  compare x y = compare (forceBuffer (buf x)) (forceBuffer (buf y))+    where buf (InitCode z) = z+          buf (RuntimeCode z) = z+ -- | A contract can either have concrete or symbolic storage -- depending on what type of execution we are doing data Storage@@ -424,14 +446,14 @@ -- * Data constructors  makeVm :: VMOpts -> VM-makeVm o = +makeVm o =   let txaccessList = vmoptTxAccessList o       txorigin = vmoptOrigin o       txtoAddr = vmoptAddress o       initialAccessedAddrs = fromList $ [txorigin, txtoAddr] ++ [1..9] ++ (Map.keys txaccessList)       initialAccessedStorageKeys = fromList $ foldMap (uncurry (map . (,))) (Map.toList txaccessList)       touched = if vmoptCreate o then [txorigin] else [txorigin, txtoAddr]-  in +  in   VM   { _result = Nothing   , _frames = mempty@@ -485,6 +507,7 @@   , _burned = 0   , _constraints = []   , _iterations = mempty+  , _allowFFI = vmoptAllowFFI o   } where theCode = case _contractcode (vmoptContract o) of             InitCode b    -> b             RuntimeCode b -> b@@ -1574,8 +1597,8 @@       Unique a -> do         assign result Nothing         cont (C w $ fromSizzle a)-      InconsistentU -> vmError $ DeadPath-      TimeoutU -> vmError $ SMTTimeout+      InconsistentU -> vmError DeadPath+      TimeoutU -> vmError SMTTimeout       Multiple -> vmError $ NotUnique w   Just a -> cont a @@ -1939,7 +1962,30 @@ cheatActions :: Map Word32 CheatAction cheatActions =   Map.fromList-    [ action "warp(uint256)" $+    [ action "ffi(string[])" $+        \sig outOffset outSize input -> do+          vm <- get+          if view EVM.allowFFI vm then+            case decodeBuffer [AbiArrayDynamicType AbiStringType] input of+              CAbi valsArr -> case valsArr of+                [AbiArrayDynamic AbiStringType strsV] ->+                  let+                    cmd = (flip fmap) (V.toList strsV) (\case+                      (AbiString a) -> unpack $ decodeUtf8 a+                      _ -> "")+                    cont bs = do+                      let encoded = ConcreteBuffer bs+                      assign (state . returndata) encoded+                      copyBytesToMemory encoded outSize 0 outOffset+                      assign result Nothing+                  in assign result (Just . VMFailure . Query $ (PleaseDoFFI cmd cont))+                _ -> vmError (BadCheatCode sig)+              _ -> vmError (BadCheatCode sig)+          else+            let msg = encodeUtf8 "ffi disabled: run again with --ffi if you want to allow tests to call external scripts"+            in vmError . Revert $ abiMethod "Error(string)" (AbiTuple . V.fromList $ [AbiString msg]),++      action "warp(uint256)" $         \sig _ _ input -> case decodeStaticArgs input of           [x]  -> assign (block . timestamp) x           _ -> vmError (BadCheatCode sig),@@ -2111,7 +2157,7 @@   then do     assign (state . stack) (0 : xs)     assign (state . returndata) mempty-    pushTrace $ ErrorTrace $ CallDepthLimitReached+    pushTrace $ ErrorTrace CallDepthLimitReached     next   else if collision $ view (env . contracts . at newAddr) vm0   then burn xGas $ do@@ -2271,7 +2317,7 @@            -- In other words, we special case address 0x03 and keep it in the set of touched accounts during revert           touched <- use (tx . substate . touchedAccounts)-          +           let             substate'' = over touchedAccounts (maybe id cons (find ((==) 3) touched)) substate'             revertContracts = assign (env . contracts) reversion@@ -2408,8 +2454,8 @@       currentContract vm   pure Trace     { _traceData = x-    , _traceCodehash = view codehash this-    , _traceOpIx = (view opIxMap this) Vector.!? (view (state . pc) vm)+    , _traceContract = this+    , _traceOpIx = fromMaybe 0 $ (view opIxMap this) Vector.!? (view (state . pc) vm)     }  pushTrace :: TraceData -> EVM ()

@@ -63,6 +63,7 @@ import Data.Binary.Put    (Put, runPut, putWord8, putWord32be) import Data.Bits          (shiftL, shiftR, (.&.)) import Data.ByteString    (ByteString)+import Data.Char          (isHexDigit) import Data.DoubleWord    (Word256, Int256, signedWord) import Data.Functor       (($>)) import Data.Text          (Text, pack, unpack)@@ -70,18 +71,19 @@ import Data.Vector        (Vector, toList) import Data.Word          (Word32) import Data.List          (intercalate)-import Data.SBV           (SWord, fromBytes)+import Data.SBV           (fromBytes) import GHC.Generics  import Test.QuickCheck hiding ((.&.), label) import Text.ParserCombinators.ReadP import Control.Applicative -import qualified Data.ByteString       as BS-import qualified Data.ByteString.Char8 as Char8-import qualified Data.ByteString.Lazy  as BSLazy-import qualified Data.Text             as Text-import qualified Data.Vector           as Vector+import qualified Data.ByteString        as BS+import qualified Data.ByteString.Base16 as BS16+import qualified Data.ByteString.Char8  as Char8+import qualified Data.ByteString.Lazy   as BSLazy+import qualified Data.Text              as Text+import qualified Data.Vector            as Vector  import qualified Text.Megaparsec      as P import qualified Text.Megaparsec.Char as P@@ -250,6 +252,7 @@   AbiTuple v ->     putAbiSeq v +-- | Decode a sequence type (e.g. tuple / array). Will fail for non sequence types getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue) getAbiSeq n ts = label "sequence" $ do   hs <- label "sequence head" (getAbiHead n ts)@@ -491,9 +494,9 @@                                 return $ AbiBool (w /= 0))                             <|> (do Boolz b <- readS_to_P reads                                     return $ AbiBool b)-parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- readS_to_P reads+parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- bytesP                                                    return bytes-parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- readS_to_P reads+parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- bytesP                                                            return bytes parseAbiValue AbiStringType = AbiString <$> do Char8.pack <$> readS_to_P reads parseAbiValue (AbiArrayDynamicType typ) =@@ -510,7 +513,16 @@                                                   skipSpaces                                                   return a) `sepBy` (char ',')) +bytesP :: ReadP ByteStringS+bytesP = do+  string "0x"+  hex <- munch isHexDigit+  case BS16.decode (encodeUtf8 (Text.pack hex)) of+    Right d -> pure $ ByteStringS d+    Left d -> pfail+ data AbiVals = NoVals | CAbi [AbiValue] | SAbi [SymWord]+  deriving (Show)  decodeBuffer :: [AbiType] -> Buffer -> AbiVals decodeBuffer tps (ConcreteBuffer b)

@@ -3,27 +3,28 @@  module EVM.Dapp where -import EVM (Trace, traceCodehash, traceOpIx, Env)+import EVM (Trace, traceContract, traceOpIx, ContractCode(..), Contract(..), codehash, contractcode) import EVM.ABI (Event, AbiType) import EVM.Debug (srcMapCodePos)-import EVM.Solidity (SolcContract, CodeType (..), SourceCache (..), SrcMap, Method)-import EVM.Solidity (contractName, methodInputs)-import EVM.Solidity (runtimeCodehash, creationCodehash, abiMap)-import EVM.Solidity (runtimeSrcmap, sourceAsts, creationSrcmap, eventMap)-import EVM.Solidity (methodSignature, astIdMap, astSrcMap)-import EVM.Types (W256, abiKeccak)+import EVM.Solidity+import EVM.Types (W256, abiKeccak, keccak, Buffer(..), Addr)+import EVM.Concrete +import Data.ByteString (ByteString)+import qualified Data.ByteString as BS import Data.Aeson (Value) import Data.Bifunctor (first) import Data.Text (Text, isPrefixOf, pack, unpack) import Data.Text.Encoding (encodeUtf8)-import Data.Map (Map, toList)+import Data.Map (Map, toList, elems)+import Data.List (sort) import Data.Maybe (isJust, fromJust) import Data.Word (Word32)  import Control.Arrow ((>>>)) import Control.Lens +import Data.List (find) import qualified Data.Map        as Map import qualified Data.Sequence   as Seq import qualified Text.Regex.TDFA as Regex@@ -32,6 +33,7 @@   { _dappRoot       :: FilePath   , _dappSolcByName :: Map Text SolcContract   , _dappSolcByHash :: Map W256 (CodeType, SolcContract)+  , _dappSolcByCode :: [(Code, SolcContract)] -- for contracts with `immutable` vars.   , _dappSources    :: SourceCache   , _dappUnitTests  :: [(Text, [(Test, [AbiType])])]   , _dappAbiMap     :: Map Word32 Method@@ -40,12 +42,20 @@   , _dappAstSrcMap  :: SrcMap -> Maybe Value   } +-- | bytecode modulo immutables, to identify contracts+data Code =+  Code {+    raw :: ByteString,+    immutableLocations :: [Reference]+  }+  deriving Show+ data DappContext = DappContext   { _contextInfo :: DappInfo-  , _contextEnv  :: Env+  , _contextEnv  :: Map Addr Contract   } -data Test = ConcreteTest Text | SymbolicTest Text+data Test = ConcreteTest Text | SymbolicTest Text | InvariantTest Text  makeLenses ''DappInfo makeLenses ''DappContext@@ -59,6 +69,7 @@   let     solcs = Map.elems solcByName     astIds = astIdMap $ snd <$> toList (view sourceAsts sources)+    immutables = filter ((/=) mempty . _immutableReferences) solcs    in DappInfo     { _dappRoot = root@@ -72,7 +83,9 @@           mappend            (f runtimeCodehash  Runtime)            (f creationCodehash Creation)-+      -- contracts with immutable locations can't be id by hash+    , _dappSolcByCode =+      [(Code (_runtimeCode x) (concat $ elems $ _immutableReferences x), x) | x <- immutables]       -- Sum up the ABI maps from all the contracts.     , _dappAbiMap   = mconcat (map (view abiMap) solcs)     , _dappEventMap = mconcat (map (view eventMap) solcs)@@ -98,12 +111,13 @@ unitTestMarkerAbi = abiKeccak (encodeUtf8 "IS_TEST()")  findAllUnitTests :: [SolcContract] -> [(Text, [(Test, [AbiType])])]-findAllUnitTests = findUnitTests ".*:.*\\.(test|prove).*"+findAllUnitTests = findUnitTests ".*:.*\\.(test|prove|invariant).*"  mkTest :: Text -> Maybe Test mkTest sig   | "test" `isPrefixOf` sig = Just (ConcreteTest sig)   | "prove" `isPrefixOf` sig = Just (SymbolicTest sig)+  | "invariant" `isPrefixOf` sig = Just (InvariantTest sig)   | otherwise = Nothing  regexMatches :: Text -> Text -> Bool@@ -144,19 +158,46 @@ extractSig :: Test -> Text extractSig (ConcreteTest sig) = sig extractSig (SymbolicTest sig) = sig+extractSig (InvariantTest sig) = sig  traceSrcMap :: DappInfo -> Trace -> Maybe SrcMap traceSrcMap dapp trace =   let-    h = view traceCodehash trace+    h = view traceContract trace     i = view traceOpIx trace-  in case preview (dappSolcByHash . ix h) dapp of-    Nothing ->-      Nothing-    Just (Creation, solc) ->-      i >>= \i' -> preview (creationSrcmap . ix i') solc-    Just (Runtime, solc) ->-      i >>= \i' -> preview (runtimeSrcmap . ix i') solc+  in srcMap dapp h i++srcMap :: DappInfo -> Contract -> Int -> Maybe SrcMap+srcMap dapp contr opIndex = do+  sol <- findSrc contr dapp+  case view contractcode contr of+    (InitCode _) ->+      preview (creationSrcmap . ix opIndex) sol+    (RuntimeCode _) ->+      preview (runtimeSrcmap . ix opIndex) sol++findSrc :: Contract -> DappInfo -> Maybe SolcContract+findSrc c dapp = case preview (dappSolcByHash . ix (view codehash c)) dapp of+  Just (_, v) -> Just v+  Nothing -> lookupCode (view contractcode c) dapp+++lookupCode :: ContractCode -> DappInfo -> Maybe SolcContract+lookupCode (InitCode (SymbolicBuffer _)) _ = Nothing -- TODO: srcmaps for symbolic bytecode+lookupCode (RuntimeCode (SymbolicBuffer _)) _ = Nothing -- TODO: srcmaps for symbolic bytecode+lookupCode (InitCode (ConcreteBuffer c)) a =+  snd <$> preview (dappSolcByHash . ix (keccak (stripBytecodeMetadata c))) a+lookupCode (RuntimeCode (ConcreteBuffer c)) a =+  case snd <$> preview (dappSolcByHash . ix (keccak (stripBytecodeMetadata c))) a of+    Just x -> return x+    Nothing -> snd <$> find (compareCode c . fst) (view dappSolcByCode a)++compareCode :: ByteString -> Code -> Bool+compareCode raw (Code template locs) =+  let holes' = sort [(start, len) | (Reference start len) <- locs]+      insert at' len' bs = writeMemory (BS.replicate len' 0) (fromIntegral len') 0 (fromIntegral at') bs+      refined = foldr (\(start, len) acc -> insert start len acc) raw holes'+  in BS.length raw == BS.length template && template == refined  showTraceLocation :: DappInfo -> Trace -> Either Text Text showTraceLocation dapp trace =

@@ -72,6 +72,8 @@         , vmModifier = loadFacts         , dapp = emptyDapp         , testParams = params+        , maxDepth = Nothing+        , allowFFI = False         }     readSolc path >>=       \case@@ -129,6 +131,8 @@         , vmModifier = loadFacts         , dapp = emptyDapp         , testParams = params+        , maxDepth = Nothing+        , allowFFI = False         }     EVM.TTY.main testOpts root path @@ -247,6 +251,8 @@              State.state (runState m) >> interpretWithTrace fetcher (k ())         EVM.Stepper.Ask _ ->           error "cannot make choices with this interpretWithTraceer"+        EVM.Stepper.IOAct m ->+          m >>= interpretWithTrace fetcher . k         EVM.Stepper.EVM m -> do           r <- State.state (runState m)           interpretWithTrace fetcher (k r)

@@ -289,9 +289,6 @@   case currentSrcMap dapp vm of     Nothing -> False     Just sm ->-      case view (dappSources . sourceFiles . at (srcMapFile sm)) dapp of-        Nothing -> False-        Just _ ->           let             (currentFileName, currentLineNumber) =               fromJust (srcMapCodePos (view dappSources dapp) sm)@@ -323,7 +320,7 @@   fromMaybe noMap $ do     dapp <- view uiVmDapp s     sm <- currentSrcMap dapp (view uiVm s)-    (fileName, _) <- view (dappSources . sourceFiles . at (srcMapFile sm)) dapp+    let (fileName, _) = view (dappSources . sourceFiles) dapp !! srcMapFile sm     pure . output $       L [ A "step"         , L [A ("vm" :: Text), sexp (view uiVm s)]@@ -520,6 +517,8 @@     , vmModifier        = id     , dapp              = emptyDapp     , testParams        = params+    , maxDepth          = Nothing+    , allowFFI          = False     }  initialStateForTest

@@ -41,6 +41,7 @@     , vmoptCreate = False     , vmoptStorageModel = ConcreteS     , vmoptTxAccessList = mempty+    , vmoptAllowFFI = False     }) & set (env . contracts . at ethrunAddress)              (Just (initialContract (RuntimeCode mempty))) 

@@ -108,12 +108,12 @@   dump x = BS16.encode x <> "\n"   load x =     case BS16.decode . mconcat . BS.split 10 $ x of-      (y, "") -> Just y+      Right y -> Just y       _       -> Nothing  contractFacts :: Addr -> Contract -> [Fact] contractFacts a x = case view bytecode x of-  ConcreteBuffer b -> +  ConcreteBuffer b ->     storageFacts a x ++     [ BalanceFact a (view balance x)     , NonceFact   a (view nonce x)

@@ -6,6 +6,7 @@  import Prelude hiding (Word) +import EVM.ABI import EVM.Types    (Addr, w256, W256, hexText, Word, Buffer(..)) import EVM.Symbolic (litWord) import EVM          (IsUnique(..), EVM, Contract, Block, initialContract, nonce, balance, external)@@ -21,16 +22,19 @@ import Data.SBV.Trans hiding (Word) import Data.Aeson import Data.Aeson.Lens-import Data.ByteString (ByteString)+import qualified Data.ByteString as BS import Data.Text (Text, unpack, pack)++import qualified Data.Vector as RegularVector import Network.Wreq import Network.Wreq.Session (Session)+import System.Process  import qualified Network.Wreq.Session as Session  -- | Abstract representation of an RPC fetch request data RpcQuery a where-  QueryCode    :: Addr         -> RpcQuery ByteString+  QueryCode    :: Addr         -> RpcQuery BS.ByteString   QueryBlock   ::                 RpcQuery Block   QueryBalance :: Addr         -> RpcQuery W256   QueryNonce   :: Addr         -> RpcQuery W256@@ -164,6 +168,13 @@ oracle :: Maybe SBV.State -> Maybe (BlockNumber, Text) -> Bool -> Fetcher oracle smtstate info ensureConsistency q = do   case q of+    EVM.PleaseDoFFI vals continue -> case vals of+       cmd : args -> do+          (_, stdout', _) <- readProcessWithExitCode cmd args ""+          pure . continue . encodeAbiValue $+            AbiTuple (RegularVector.fromList [ AbiBytesDynamic . hexText . pack $ stdout'])+       _ -> error (show vals)+     EVM.PleaseAskSMT branchcondition pathconditions continue ->       case smtstate of         Nothing -> return $ continue EVM.Unknown

@@ -84,7 +84,7 @@   formatBytes bs  -- opportunistically decodes recognisable strings showAbiValue (AbiAddress addr) =   let dappinfo = view contextInfo ?context-      contracts = view (contextEnv . EVM.contracts) ?context+      contracts = view contextEnv ?context       name = case (Map.lookup addr contracts) of         Nothing -> ""         Just contract ->@@ -175,7 +175,7 @@  showTrace :: DappInfo -> VM -> Trace -> Text showTrace dapp vm trace =-  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts }   in let     pos =       case showTraceLocation dapp trace of@@ -247,10 +247,12 @@           "fetch contract " <> pack (show addr) <> pos         PleaseFetchSlot addr slot _ ->           "fetch storage slot " <> pack (show slot) <> " from " <> pack (show addr) <> pos-        PleaseAskSMT _ _ _ ->+        PleaseAskSMT {} ->           "ask smt" <> pos-        PleaseMakeUnique _ _ _ ->+        PleaseMakeUnique {} ->           "make unique value" <> pos+        PleaseDoFFI cmd _ ->+          "execute ffi " <> pack (show cmd) <> pos      ErrorTrace e ->       case e of@@ -420,7 +422,7 @@  showLeafInfo :: DappInfo -> BranchInfo -> [String] showLeafInfo srcInfo (BranchInfo vm _) = let-  ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env }+  ?context = DappContext { _contextInfo = srcInfo, _contextEnv = vm ^?! EVM.env . EVM.contracts }   in let   self    = view (EVM.state . EVM.contract) vm   updates = case view (EVM.env . EVM.contracts) vm ^?! ix self . EVM.storage of

@@ -3,6 +3,7 @@ {-# Language StrictData #-} {-# Language TemplateHaskell #-} {-# Language OverloadedStrings #-}+{-# Language QuasiQuotes #-}  module EVM.Solidity   ( solidity@@ -16,10 +17,13 @@   , CodeType (..)   , Method (..)   , SlotType (..)+  , Reference(..)+  , Mutability(..)   , methodName   , methodSignature   , methodInputs   , methodOutput+  , methodMutability   , abiMap   , eventMap   , storageLayout@@ -59,7 +63,9 @@ import Control.Applicative import Control.Monad import Control.Lens         hiding (Indexed, (.=))-import Data.Aeson           (Value (..), ToJSON(..), (.=), object, encode)+import qualified Data.String.Here as Here+import Data.Aeson hiding (json)+import Data.Aeson.Types import Data.Aeson.Lens import Data.Scientific import Data.ByteString      (ByteString)@@ -76,7 +82,6 @@ import Data.Text.Encoding   (encodeUtf8, decodeUtf8) import Data.Text.IO         (readFile, writeFile) import Data.Vector          (Vector)-import Data.Word import GHC.Generics         (Generic) import Prelude hiding       (readFile, writeFile) import System.IO hiding     (readFile, writeFile)@@ -136,6 +141,7 @@   , _constructorInputs :: [(Text, AbiType)]   , _abiMap           :: Map Word32 Method   , _eventMap         :: Map W256 Event+  , _immutableReferences :: Map W256 [Reference]   , _storageLayout    :: Maybe (Map Text StorageItem)   , _runtimeSrcmap    :: Seq SrcMap   , _creationSrcmap   :: Seq SrcMap@@ -146,14 +152,34 @@   , _methodInputs :: [(Text, AbiType)]   , _methodName :: Text   , _methodSignature :: Text+  , _methodMutability :: Mutability   } deriving (Show, Eq, Ord, Generic) +data Mutability+  = Pure       -- ^ specified to not read blockchain state+  | View       -- ^ specified to not modify the blockchain state+  | NonPayable -- ^ function does not accept Ether - the default+  | Payable    -- ^ function accepts Ether+ deriving (Show, Eq, Ord, Generic)+ data SourceCache = SourceCache-  { _sourceFiles  :: Map Int (Text, ByteString)-  , _sourceLines  :: Map Int (Vector ByteString)+  { _sourceFiles  :: [(Text, ByteString)]+  , _sourceLines  :: [(Vector ByteString)]   , _sourceAsts   :: Map Text Value   } deriving (Show, Eq, Generic) +data Reference = Reference+  { _refStart :: Int,+    _refLength :: Int+  } deriving (Show, Eq)++instance FromJSON Reference where+  parseJSON (Object v) = Reference+    <$> v .: "start"+    <*> v .: "length"+  parseJSON invalid =+    typeMismatch "Transaction" invalid+ instance Semigroup SourceCache where   _ <> _ = error "lol" @@ -241,13 +267,9 @@       f (fp, Nothing) = BS.readFile $ Text.unpack fp   xs <- mapM f paths   return $! SourceCache-    { _sourceFiles =-        Map.fromList (zip [0..] (zip (fst <$> paths) xs))-    , _sourceLines =-        Map.fromList (zip [0 .. length paths - 1]-                       (map (Vector.fromList . BS.split 0xa) xs))-    , _sourceAsts =-        asts+    { _sourceFiles = zip (fst <$> paths) xs+    , _sourceLines = map (Vector.fromList . BS.split 0xa) xs+    , _sourceAsts  = asts     }  lineSubrange ::@@ -299,6 +321,7 @@   Nothing -> readStdJSON json   _ -> readCombinedJSON json +-- deprecate me soon readCombinedJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)]) readCombinedJSON json = do   contracts <- f <$> (json ^? key "contracts" . _Object)@@ -324,7 +347,8 @@         _constructorInputs = mkConstructor abis,         _abiMap       = mkAbiMap abis,         _eventMap     = mkEventMap abis,-        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String+        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String,+        _immutableReferences = mempty -- TODO: deprecate combined-json       }  readStdJSON :: Text -> Maybe (Map Text SolcContract, Map Text Value, [(Text, Maybe ByteString)])@@ -340,13 +364,14 @@     f :: (AsValue s) => HMap.HashMap Text s -> (Map Text (SolcContract, (HMap.HashMap Text Text)))     f x = Map.fromList . (concatMap g) . HMap.toList $ x     g (s, x) = h s <$> HMap.toList (view _Object x)-    h s (c, x) = +    h :: Text -> (Text, Value) -> (Text, (SolcContract, HMap.HashMap Text Text))+    h s (c, x) =       let         evmstuff = x ^?! key "evm"         runtime = evmstuff ^?! key "deployedBytecode"         creation =  evmstuff ^?! key "bytecode"-        theRuntimeCode = toCode $ runtime ^?! key "object" . _String-        theCreationCode = toCode $ creation ^?! key "object" . _String+        theRuntimeCode = toCode $ fromMaybe "" $ runtime ^? key "object" . _String+        theCreationCode = toCode $ fromMaybe "" $ creation ^? key "object" . _String         srcContents :: Maybe (HMap.HashMap Text Text)         srcContents = do metadata <- x ^? key "metadata" . _String                          srcs <- metadata ^? key "sources" . _Object@@ -364,7 +389,12 @@         _constructorInputs = mkConstructor abis,         _abiMap        = mkAbiMap abis,         _eventMap      = mkEventMap abis,-        _storageLayout = mkStorageLayout $ x ^? key "storage-layout" . _String+        _storageLayout = mkStorageLayout $ x ^? key "storageLayout" . _String,+        _immutableReferences = fromMaybe mempty $+          do x' <- runtime ^? key "immutableReferences"+             case fromJSON x' of+               Success a -> return a+               _ -> Nothing       }, fromMaybe mempty srcContents))  mkAbiMap :: [Value] -> Map Word32 Method@@ -379,6 +409,8 @@                  (toList (abi ^?! key "inputs" . _Array))               , _methodOutput = map parseMethodInput                  (toList (abi ^?! key "outputs" . _Array))+              , _methodMutability = parseMutability+                 (abi ^?! key "stateMutability" . _String)               })   in f <$> relevant @@ -417,7 +449,7 @@ mkStorageLayout (Just json) = do   items <- json ^? key "storage" . _Array   types <- json ^? key "types"-  fmap Map.fromList $ (forM (Vector.toList items) $ \item ->+  fmap Map.fromList (forM (Vector.toList items) $ \item ->     do name <- item ^? key "label" . _String        offset <- item ^? key "offset" . _Number >>= toBoundedInteger        slot <- item ^? key "slot" . _String@@ -446,6 +478,13 @@     (x ^?! key "type" . _String)   where parseComponents = fmap $ snd . parseMethodInput +parseMutability :: Text -> Mutability+parseMutability "view" = View+parseMutability "pure" = Pure+parseMutability "nonpayable" = NonPayable+parseMutability "payable" = Payable+parseMutability _ = error "unknown function mutability"+ -- This actually can also parse a method output! :O parseMethodInput :: AsValue s => s -> (Text, AbiType) parseMethodInput x =@@ -454,16 +493,53 @@   )  toCode :: Text -> ByteString-toCode = fst . BS16.decode . encodeUtf8+toCode t = case BS16.decode (encodeUtf8 t) of+  Right d -> d+  Left e -> error e  solidity' :: Text -> IO (Text, Text) solidity' src = withSystemTempFile "hevm.sol" $ \path handle -> do   hClose handle-  writeFile path ("pragma solidity ^0.6.7;\n" <> src)+  writeFile path ("//SPDX-License-Identifier: UNLICENSED\n" <> "pragma solidity ^0.8.6;\n" <> src)+  writeFile (path <> ".json")+    [Here.i|+    {+      "language": "Solidity",+      "sources": {+        ${path}: {+          "urls": [+            ${path}+          ]+        }+      },+      "settings": {+        "outputSelection": {+          "*": {+            "*": [+              "metadata",+              "evm.bytecode",+              "evm.deployedBytecode",+              "abi",+              "storageLayout",+              "evm.bytecode.sourceMap",+              "evm.bytecode.linkReferences",+              "evm.bytecode.generatedSources",+              "evm.deployedBytecode.sourceMap",+              "evm.deployedBytecode.linkReferences",+              "evm.deployedBytecode.generatedSources"+            ],+            "": [+              "ast"+            ]+          }+        }+      }+    }+    |]   x <- pack <$>     readProcess       "solc"-      ["--combined-json=bin-runtime,bin,srcmap,srcmap-runtime,abi,ast,storage-layout", path]+      ["--allow-paths", path, "--standard-json", (path <> ".json")]       ""   return (x, pack path) @@ -490,7 +566,7 @@                                    object ["content" .= src]]            , "settings" .=              object [ "outputSelection" .=-                    object ["*" .= +                    object ["*" .=                       object ["*" .= (toJSON                               ["metadata" :: String,                                "evm.bytecode",@@ -502,14 +578,15 @@                                "evm.bytecode.generatedSources",                                "evm.deployedBytecode.sourceMap",                                "evm.deployedBytecode.linkReferences",-                               "evm.deployedBytecode.generatedSources"+                               "evm.deployedBytecode.generatedSources",+                               "evm.deployedBytecode.immutableReferences"                               ]),                               "" .= (toJSON ["ast" :: String])                              ]                             ]                     ]            ]-                               + stdjson :: Language -> Text -> Text stdjson lang src = decodeUtf8 $ toStrict $ encode $ StandardJSON lang src @@ -536,9 +613,9 @@ stripBytecodeMetadataSym b =   let     concretes :: [Maybe Word8]-    concretes = (fmap fromSized) <$> unliteral <$> b+    concretes = (fmap fromSized) . unliteral <$> b     bzzrs :: [[Maybe Word8]]-    bzzrs = fmap (Just) <$> BS.unpack <$> knownBzzrPrefixes+    bzzrs = fmap (Just) . BS.unpack <$> knownBzzrPrefixes     candidates = (flip Data.List.isInfixOf concretes) <$> bzzrs   in case elemIndex True candidates of     Nothing -> b

@@ -11,6 +11,7 @@   , wait   , ask   , evm+  , evmIO   , entering   , enter   , interpret@@ -57,6 +58,9 @@   -- | Embed a VM state transformation   EVM  :: EVM a   -> Action a +  -- | Perform an IO action+  IOAct :: StateT VM IO a -> Action a -- they should all just be this?+ -- | Type alias for an operational monad of @Action@ type Stepper a = Program Action a @@ -77,6 +81,9 @@ evm :: EVM a -> Stepper a evm = singleton . EVM +evmIO :: StateT VM IO a -> Stepper a+evmIO = singleton . IOAct+ -- | Run the VM until final result, resolving all queries execFully :: Stepper (Either Error Buffer) execFully =@@ -136,6 +143,8 @@              State.state (runState m) >> interpret fetcher (k ())         Ask _ ->           error "cannot make choices with this interpreter"+        IOAct m ->+          do m >>= interpret fetcher . k         EVM m -> do           r <- State.state (runState m)           interpret fetcher (k r)

@@ -4,7 +4,6 @@  module EVM.SymExec where - import Prelude hiding (Word)  import Control.Lens hiding (pre)@@ -26,12 +25,12 @@ import Data.SBV hiding (runSMT, newArray_, addAxiom, distinct, sWord8s, Word) import Data.Vector (toList, fromList) import Data.Tree+import Data.DoubleWord (Word256)  import Data.ByteString (ByteString, pack) import qualified Data.ByteString.Lazy as Lazy import qualified Data.ByteString as BS import Data.Text (Text, splitOn, unpack)-import Control.Monad.State.Strict (runState, get, put, zipWithM) import qualified Control.Monad.State.Class as State import Control.Applicative @@ -141,6 +140,7 @@     , vmoptCreate = False     , vmoptStorageModel = model     , vmoptTxAccessList = mempty+    , vmoptAllowFFI = False     }) & set (env . contracts . at (createAddress ethrunAddress 1))              (Just (contractWithStore x initStore)) @@ -215,6 +215,8 @@           exec >>= interpret fetcher maxIter . k         Stepper.Run ->           run >>= interpret fetcher maxIter . k+        Stepper.IOAct q ->+          mapStateT io q >>= interpret fetcher maxIter . k         Stepper.Ask (EVM.PleaseChoosePath _ continue) -> do           vm <- get           case maxIterationsReached vm maxIter of@@ -264,14 +266,45 @@ type Precondition = VM -> SBool type Postcondition = (VM, VM) -> SBool -checkAssert :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)-checkAssert c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just checkAssertions)+checkAssert :: [Word256] -> ByteString -> Maybe (Text, [AbiType]) -> [String] -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM)+checkAssert errs c signature' concreteArgs = verifyContract c signature' concreteArgs SymbolicS (const sTrue) (Just $ checkAssertions errs) -checkAssertions :: Postcondition-checkAssertions (_, out) = case view result out of+{- |Checks if an assertion violation has been encountered++  hevm recognises the following as an assertion violation:++  1. the invalid opcode (0xfe) (solc < 0.8)+  2. a revert with a reason of the form `abi.encodeWithSelector("Panic(uint256)", code)`, where code is one of the following (solc >= 0.8):+    - 0x00: Used for generic compiler inserted panics.+    - 0x01: If you call assert with an argument that evaluates to false.+    - 0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block.+    - 0x12; If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0).+    - 0x21: If you convert a value that is too big or negative into an enum type.+    - 0x22: If you access a storage byte array that is incorrectly encoded.+    - 0x31: If you call .pop() on an empty array.+    - 0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0).+    - 0x41: If you allocate too much memory or create an array that is too large.+    - 0x51: If you call a zero-initialized variable of internal function type.++  see: https://docs.soliditylang.org/en/v0.8.6/control-structures.html?highlight=Panic#panic-via-assert-and-error-via-require+-}+checkAssertions :: [Word256] -> Postcondition+checkAssertions errs (_, out) = case view result out of   Just (EVM.VMFailure (EVM.UnrecognizedOpcode 254)) -> sFalse+  Just (EVM.VMFailure (EVM.Revert msg)) -> if msg `elem` (fmap panicMsg errs) then sFalse else sTrue   _ -> sTrue +-- |By default hevm checks for all assertions except those which result from arithmetic overflow+defaultPanicCodes :: [Word256]+defaultPanicCodes = [ 0x00, 0x01, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51 ]++allPanicCodes :: [Word256]+allPanicCodes = [ 0x00, 0x01, 0x11, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51 ]++-- |Produces the revert message for solc >=0.8 assertion violations+panicMsg :: Word256 -> ByteString+panicMsg err = (selector "Panic(uint256)") <> (encodeAbiValue $ AbiUInt 256 err)+ verifyContract :: ByteString -> Maybe (Text, [AbiType]) -> [String] -> StorageModel -> Precondition -> Maybe Postcondition -> Query (Either (Tree BranchInfo) (Tree BranchInfo), VM) verifyContract theCode signature' concreteArgs storagemodel pre maybepost = do     preStateRaw <- abstractVM signature' concreteArgs theCode  storagemodel@@ -344,7 +377,7 @@ -- | Compares two contract runtimes for trace equivalence by running two VMs and comparing the end states. equivalenceCheck :: ByteString -> ByteString -> Maybe Integer -> Maybe (Text, [AbiType]) -> Query (Either ([VM], [VM]) VM) equivalenceCheck bytecodeA bytecodeB maxiter signature' = do-  let +  let     bytecodeA' = if BS.null bytecodeA then BS.pack [0] else bytecodeA     bytecodeB' = if BS.null bytecodeB then BS.pack [0] else bytecodeB   preStateA <- abstractVM signature' [] bytecodeA' SymbolicS

@@ -13,7 +13,7 @@ import EVM import EVM.ABI (abiTypeSolidity, decodeAbiValue, AbiType(..), emptyAbi) import EVM.SymExec (maxIterationsReached, symCalldata)-import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..))+import EVM.Dapp (DappInfo, dappInfo, Test, extractSig, Test(..), srcMap) import EVM.Dapp (dappUnitTests, unitTestMethods, dappSolcByName, dappSolcByHash, dappSources) import EVM.Dapp (dappAstSrcMap) import EVM.Debug@@ -24,6 +24,7 @@ import EVM.Solidity hiding (storageLayout) import EVM.Types hiding (padRight) import EVM.UnitTest+import EVM.RLP (RLP(..)) import EVM.StorageLayout  import EVM.Stepper (Stepper)@@ -32,7 +33,7 @@  import EVM.Fetch (Fetcher) -import Control.Lens+import Control.Lens hiding (List) import Control.Monad.Trans.Reader import Control.Monad.State.Strict hiding (state) @@ -180,6 +181,10 @@           do m <- liftIO (?fetcher q)              interpret mode (Stepper.evm m >>= k) +        -- Stepper wants to make a query and wait for the results?+        Stepper.IOAct q -> do+          zoom uiVm (StateT (runStateT q)) >>= interpret mode . k+         -- Stepper wants to modify the VM.         Stepper.EVM m -> do           vm <- use uiVm@@ -235,12 +240,14 @@       , smtTimeout        = Nothing       , smtState          = Nothing       , solver            = Nothing+      , maxDepth          = Nothing       , match             = ""       , fuzzRuns          = 1       , replay            = error "irrelevant"       , vmModifier        = id       , testParams        = error "irrelevant"       , dapp              = dappinfo+      , allowFFI          = False       }     ui0 = initUiVmState vm opts (void Stepper.execFully) @@ -274,6 +281,7 @@ isFuzzTest (SymbolicTest _, _) = False isFuzzTest (ConcreteTest _, []) = False isFuzzTest (ConcreteTest _, _) = True+isFuzzTest (InvariantTest _, _) = True  main :: UnitTestOptions -> FilePath -> FilePath -> IO () main opts root jsonFilePath =@@ -631,7 +639,16 @@             void (runUnitTest opts theTestName args)           SymbolicTest _ -> do             Stepper.evm $ modify symbolify-            void (execSymTest opts theTestName (SymbolicBuffer buf, w256lit len)) -- S (Literal $ num len) (literal $ num len)))+            void (execSymTest opts theTestName (SymbolicBuffer buf, w256lit len))+          InvariantTest _ -> do+            targets <- getTargetContracts opts+            let randomRun = explorationStepper opts theTestName [] targets (List []) (fromMaybe 20 maxDepth)+            void $ case replay of+              Nothing -> randomRun+              Just (sig, cd) ->+                if theTestName == sig+                then explorationStepper opts theTestName (decodeCalls cd) targets (List []) (length (decodeCalls cd))+                else randomRun   pure $ initUiVmState vm0 opts script   where     Just (test, types) = find (\(test',_) -> extractSig test' == theTestName) $ unitTestMethods testContract@@ -851,15 +868,8 @@ currentSrcMap :: DappInfo -> VM -> Maybe SrcMap currentSrcMap dapp vm = do   this <- currentContract vm-  let-    i = (view opIxMap this) SVec.! (view (state . pc) vm)-    h = view codehash this-  srcmap <- preview (dappSolcByHash . ix h) dapp-  case srcmap of-    (Creation, sol) ->-      preview (creationSrcmap . ix i) sol-    (Runtime, sol) ->-      preview (runtimeSrcmap . ix i) sol+  i <- (view opIxMap this) SVec.!? (view (state . pc) vm)+  srcMap dapp this i  drawStackPane :: UiVmState -> UiWidget drawStackPane ui =@@ -974,22 +984,22 @@ drawSolidityPane :: UiVmState -> UiWidget drawSolidityPane ui =   let dapp' = dapp (view uiTestOpts ui)+      dappSrcs = view dappSources dapp'       vm = view uiVm ui   in case currentSrcMap dapp' vm of     Nothing -> padBottom Max (hBorderWithLabel (txt "<no source map>"))     Just sm ->-      case view (dappSources . sourceLines . at (srcMapFile sm)) dapp' of-        Nothing -> padBottom Max (hBorderWithLabel (txt "<source not found>"))-        Just rows ->           let+            rows = (_sourceLines dappSrcs) !! srcMapFile sm             subrange = lineSubrange rows (srcMapOffset sm, srcMapLength sm)             fileName :: Maybe Text             fileName = preview (dappSources . sourceFiles . ix (srcMapFile sm) . _1) dapp'-            lineNo =-              (snd . fromJust $+            lineNo :: Maybe Int+            lineNo = maybe Nothing (\a -> Just (a - 1))+              (snd <$>                 (srcMapCodePos                  (view dappSources dapp')-                 sm)) - 1+                 sm))           in vBox             [ hBorderWithLabel $                 txt (fromMaybe "<unknown>" fileName)@@ -1014,7 +1024,7 @@                                   , withHighlight False (txt z)                                   ])                 False-                (listMoveTo lineNo+                ((maybe id listMoveTo lineNo)                   (solidityList vm dapp'))             ] 

@@ -8,15 +8,13 @@ import EVM.Precompiled (execute) import EVM.RLP import EVM.Symbolic (forceLit)-import EVM.Types (keccak) import EVM.Types  import Control.Lens  import Data.Aeson (FromJSON (..)) import Data.ByteString (ByteString)-import Data.Map (Map, keys)-import Data.Set (fromList)+import Data.Map (Map) import Data.Maybe (fromMaybe, isNothing, isJust)  import qualified Data.Aeson        as JSON

@@ -9,7 +9,6 @@  import Prelude hiding  (Word, LT, GT) -import Data.Aeson (FromJSONKey (..), FromJSONKeyFunction (..)) import Data.Aeson import Crypto.Hash import Data.SBV hiding (Word)@@ -17,7 +16,6 @@ import Data.Bifunctor (first) import Data.Char import Data.List (intercalate)-import Data.Bifunctor (bimap) import Data.ByteString (ByteString) import Data.ByteString.Base16 as BS16 import Data.ByteString.Builder (byteStringHex, toLazyByteString)@@ -131,11 +129,6 @@       fromBinary =         Text.decodeUtf8 . toStrict . toLazyByteString . byteStringHex -instance Read ByteStringS where-    readsPrec _ ('0':'x':x) = [bimap ByteStringS (Text.unpack . Text.decodeUtf8) bytes]-       where bytes = BS16.decode (Text.encodeUtf8 (Text.pack x))-    readsPrec _ _ = []- instance JSON.ToJSON ByteStringS where   toJSON = JSON.String . Text.pack . show @@ -424,13 +417,13 @@ hexByteString :: String -> ByteString -> ByteString hexByteString msg bs =   case BS16.decode bs of-    (x, "") -> x+    Right x -> x     _ -> error ("invalid hex bytestring for " ++ msg)  hexText :: Text -> ByteString hexText t =   case BS16.decode (Text.encodeUtf8 (Text.drop 2 t)) of-    (x, "") -> x+    Right x -> x     _ -> error ("invalid hex bytestring " ++ show t)  readN :: Integral a => String -> a

@@ -18,6 +18,7 @@ import EVM.SymExec import EVM.Types import EVM.Transaction (initTx)+import EVM.RLP import qualified EVM.Fetch  import qualified EVM.FeeSchedule as FeeSchedule@@ -26,7 +27,7 @@ import qualified EVM.Stepper as Stepper import qualified Control.Monad.Operational as Operational -import Control.Lens hiding (Indexed)+import Control.Lens hiding (Indexed, elements, List) import Control.Monad.State.Strict hiding (state) import qualified Control.Monad.State.Strict as State @@ -44,7 +45,7 @@ import Data.Either        (isRight, lefts) import Data.Foldable      (toList) import Data.Map           (Map)-import Data.Maybe         (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe)+import Data.Maybe         (fromMaybe, catMaybes, fromJust, isJust, fromMaybe, mapMaybe, isNothing) import Data.Text          (isPrefixOf, stripSuffix, intercalate, Text, pack, unpack) import Data.Text.Encoding (encodeUtf8) import System.Environment (lookupEnv)@@ -72,6 +73,7 @@   { oracle     :: EVM.Query -> IO (EVM ())   , verbose    :: Maybe Int   , maxIter    :: Maybe Integer+  , maxDepth   :: Maybe Int   , smtTimeout :: Maybe Integer   , smtState   :: Maybe SBV.State   , solver     :: Maybe Text@@ -81,6 +83,7 @@   , vmModifier :: VM -> VM   , dapp       :: DappInfo   , testParams :: TestVMParams+  , allowFFI   :: Bool   }  data TestVMParams = TestVMParams@@ -143,7 +146,7 @@         setUp  = abiKeccak (encodeUtf8 "setUp()")      when (isJust (Map.lookup setUp theAbi)) $ do-      abiCall testParams "setUp()" emptyAbi+      abiCall testParams (Left ("setUp()", emptyAbi))       popTrace       pushTrace (EntryTrace "setUp()") @@ -158,21 +161,39 @@ -- will run the specified test method and return whether it succeeded. runUnitTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool runUnitTest a method args = do-  x <- execTest a method args+  x <- execTestStepper a method args   checkFailures a method x -execTest :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool-execTest UnitTestOptions { .. } method args = do+execTestStepper :: UnitTestOptions -> ABIMethod -> AbiValue -> Stepper Bool+execTestStepper UnitTestOptions { .. } methodName' method = do   -- Set up the call to the test method   Stepper.evm $ do-    abiCall testParams method args-    pushTrace (EntryTrace method)+    abiCall testParams (Left (methodName', method))+    pushTrace (EntryTrace methodName')   -- Try running the test method   Stepper.execFully >>= \case      -- If we failed, put the error in the trace.-    Left e -> Stepper.evm (pushTrace (ErrorTrace e)) >> pure True+    Left e -> Stepper.evm (pushTrace (ErrorTrace e) >> popTrace) >> pure True     _ -> pure False +exploreStep :: UnitTestOptions -> ByteString -> Stepper Bool+exploreStep UnitTestOptions{..} bs = do+  Stepper.evm $ do+    cs <- use (env . contracts)+    abiCall testParams (Right bs)+    let (Method _ inputs sig _ _) = fromMaybe (error "unknown abi call") $ Map.lookup (num $ word $ BS.take 4 bs) (view dappAbiMap dapp)+        types = snd <$> inputs+    let ?context = DappContext dapp cs+    this <- fromMaybe (error "unknown target") <$> (use (env . contracts . at (testAddress testParams)))+    let name = maybe "" (contractNamePart . view contractName) $ lookupCode (view contractcode this) dapp+    pushTrace (EntryTrace (name <> "." <> sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")" <> showCall types (ConcreteBuffer bs)))+  -- Try running the test method+  Stepper.execFully >>= \case+     -- If we failed, put the error in the trace.+    Left e -> Stepper.evm (pushTrace (ErrorTrace e) >> popTrace) >> pure True+    _ -> pure False++ checkFailures :: UnitTestOptions -> ABIMethod -> Bool -> Stepper Bool checkFailures UnitTestOptions { .. } method bailed = do    -- Decide whether the test is supposed to fail or succeed@@ -183,7 +204,7 @@     -- Ask whether any assertions failed     Stepper.evm $ do       popTrace-      abiCall testParams "failed()" emptyAbi+      abiCall testParams $ Left ("failed()", emptyAbi)     res <- Stepper.execFully     case res of       Right (ConcreteBuffer r) ->@@ -202,22 +223,18 @@  -- | This is like an unresolved source mapping. data OpLocation = OpLocation-  { srcCodehash :: !W256-  , srcOpIx     :: !Int-  } deriving (Eq, Ord, Show)+  { srcContract :: Contract+  , srcOpIx :: Int+  } deriving (Show) +instance Eq OpLocation where+  (==) (OpLocation a b) (OpLocation a' b') = b == b' && view contractcode a == view contractcode a'++instance Ord OpLocation where+  compare (OpLocation a b) (OpLocation a' b') = compare (view contractcode a, b) (view contractcode a', b')+ srcMapForOpLocation :: DappInfo -> OpLocation -> Maybe SrcMap-srcMapForOpLocation dapp (OpLocation hash opIx) =-  case preview (dappSolcByHash . ix hash) dapp of-    Nothing -> Nothing-    Just (codeType, sol) ->-      let-        vec =-          case codeType of-            Runtime  -> view runtimeSrcmap sol-            Creation -> view creationSrcmap sol-      in-        preview (ix opIx) vec+srcMapForOpLocation dapp (OpLocation contr opIx) = srcMap dapp contr opIx  type CoverageState = (VM, MultiSet OpLocation) @@ -228,7 +245,7 @@       error "internal error: why no contract?"     Just c ->       OpLocation-        (view codehash c)+        c         (fromMaybe (error "internal error: op ix") (vmOpIx vm))  execWithCoverage :: StateT CoverageState IO VMResult@@ -274,6 +291,8 @@              zoom _1 (State.state (runState m)) >> interpretWithCoverage opts (k ())         Stepper.Ask _ ->           error "cannot make choice in this interpreter"+        Stepper.IOAct q ->+          zoom _1 (StateT (runStateT q)) >>= interpretWithCoverage opts . k         Stepper.EVM m ->           zoom _1 (State.state (runState m)) >>= interpretWithCoverage opts . k @@ -301,15 +320,12 @@     srcMapCov :: MultiSet (Text, Int)     srcMapCov = MultiSet.mapMaybe (srcMapCodePos sources) cov -    -- linesByName :: Map Text (Vector ByteString)+    linesByName :: Map Text (Vector ByteString)     linesByName =-      ( Map.fromList-      . map-          (\(k, v) ->-             (fst (fromJust (Map.lookup k (view sourceFiles sources))), v))-      . Map.toList-      $ view sourceLines sources-      )+      Map.fromList $ zipWith+          (\(name, _) lines' -> (name, lines'))+          (view sourceFiles sources)+          (view sourceLines sources)      f :: Text -> Vector ByteString -> Vector (Int, ByteString)     f name =@@ -435,15 +451,143 @@       decodeAbiValue (AbiTupleType (Vector.fromList types)) callData     else fuzzRun opts vm testName types runTest opts vm (SymbolicTest testName, types) = symRun opts vm testName types+runTest opts@UnitTestOptions{..} vm (InvariantTest testName, []) = liftIO $ case replay of+  Nothing -> exploreRun opts vm testName []+  Just (sig, cds) ->+    if sig == testName+    then exploreRun opts vm testName (decodeCalls cds)+    else exploreRun opts vm testName []+runTest _ _ (InvariantTest _, types) = error $ "invariant testing with arguments: " <> show types <> " is not implemented (yet!)" +type ExploreTx = (Addr, Addr, ByteString, W256)++decodeCalls :: BSLazy.ByteString -> [ExploreTx]+decodeCalls b = fromMaybe (error "could not decode replay data") $ do+  List v <- rlpdecode $ BSLazy.toStrict b+  return $ flip fmap v $ \(List [BS caller', BS target, BS cd, BS ts]) -> (num (word caller'), num (word target), cd, word ts)+++explorationStepper :: UnitTestOptions -> ABIMethod -> [ExploreTx] -> [Addr] -> RLP -> Int -> Stepper (Bool, RLP)+explorationStepper _ _ _ _ history 0  = return (True, history)+explorationStepper opts@UnitTestOptions{..} testName replayData targets (List history) i = do+ (caller', target, cd, timestamp') <-+   case preview (ix (i - 1)) replayData of+     Just v -> return v+     Nothing ->+      Stepper.evmIO $ do+       vm <- get+       let cs = view (env . contracts) vm+           noCode c = case view contractcode c of+             RuntimeCode c' -> len c' == 0+             _ -> False+           mutable m = view methodMutability m `elem` [NonPayable, Payable]+           knownAbis :: Map Addr SolcContract+           knownAbis =+             -- exclude contracts without code+             Map.filter (not . BS.null . view runtimeCode) $+             -- exclude contracts without state changing functions+             Map.filter (not . null . Map.filter mutable . view abiMap) $+             -- exclude testing abis+             Map.filter (isNothing . preview (abiMap . ix unitTestMarkerAbi)) $+             -- pick all contracts with known compiler artifacts+             fmap fromJust (Map.filter isJust $ Map.fromList [(addr, lookupCode (view contractcode c) dapp) | (addr, c)  <- Map.toList cs])+           selected = [(addr,+                        fromMaybe (error ("no src found for: " <> show addr)) $ lookupCode (view contractcode (fromMaybe (error $ "contract not found: " <> show addr) $ Map.lookup addr cs)) dapp)+                       | addr  <- targets]+       -- go to IO and generate a random valid call to any known contract+       liftIO $ do+         -- select random contract+         (target, solcInfo) <- generate $ elements (if null targets then Map.toList knownAbis else selected)+         -- choose a random mutable method+         (_, (Method _ inputs sig _ _)) <- generate (elements $ Map.toList $ Map.filter mutable $ view abiMap solcInfo)+         let types = snd <$> inputs+         -- set the caller to a random address with 90% probability, 10% known EOA address+         let knownEOAs = Map.keys $ Map.filter noCode cs+         AbiAddress caller' <-+           if null knownEOAs+           then generate $ genAbiValue AbiAddressType+           else generate $ frequency+             [ (90, genAbiValue AbiAddressType)+             , (10, AbiAddress <$> elements knownEOAs)+             ]+         -- make a call with random valid data to the function+         args <- generate $ genAbiValue (AbiTupleType $ Vector.fromList types)+         let cd = abiMethod (sig <> "(" <> intercalate "," ((pack . show) <$> types) <> ")") args+         -- increment timestamp with random amount+         timepassed <- num <$> generate (arbitrarySizedNatural :: Gen Word32)+         let ts = fromMaybe (error "symbolic timestamp not supported here") $ maybeLitWord $ view (block . timestamp) vm+         return (caller', target, cd, num ts + timepassed)+ let opts' = opts { testParams = testParams {testAddress = target, testCaller = caller', testTimestamp = timestamp'}}+     thisCallRLP = List [BS $ word160Bytes caller', BS $ word160Bytes target, BS cd, BS $ word256Bytes timestamp']+ -- set the timestamp+ Stepper.evm $ assign (block . timestamp) (w256lit timestamp')+ -- perform the call+ bailed <- exploreStep opts' cd+ Stepper.evm popTrace+ let newHistory = if bailed then List history else List (thisCallRLP:history)+     opts'' = opts {testParams = testParams {testTimestamp = timestamp'}}+     carryOn = explorationStepper opts'' testName replayData targets newHistory (i - 1)+ -- if we didn't revert, run the test function+ if bailed+ then carryOn+ else+   do x <- runUnitTest opts'' testName emptyAbi+      if x+      then carryOn+      else pure (False, List (thisCallRLP:history))+explorationStepper _ _ _ _ _ _  = error "malformed rlp"++getTargetContracts :: UnitTestOptions -> Stepper [Addr]+getTargetContracts UnitTestOptions{..} = do+  vm <- Stepper.evm $ get+  let Just contract = currentContract vm+      theAbi = view abiMap $ fromJust $ lookupCode (view contractcode contract) dapp+      setUp  = abiKeccak (encodeUtf8 "targetContracts()")+  case Map.lookup setUp theAbi of+    Nothing -> return []+    Just _ -> do+      Stepper.evm $ abiCall testParams (Left ("targetContracts()", emptyAbi))+      res <- Stepper.execFully+      case res of+        Right (ConcreteBuffer r) ->+          let AbiTuple vs = decodeAbiValue (AbiTupleType (Vector.fromList [AbiArrayDynamicType AbiAddressType])) (BSLazy.fromStrict r)+              [AbiArrayDynamic AbiAddressType targets] = Vector.toList vs+          in return $ fmap (\(AbiAddress a) -> a) (Vector.toList targets)+        _ -> error "internal error: unexpected failure code"++exploreRun :: UnitTestOptions -> VM -> ABIMethod -> [ExploreTx] -> IO (Text, Either Text Text, VM)+exploreRun opts@UnitTestOptions{..} initialVm testName replayTxs = do+  (targets, _) <- runStateT (EVM.Stepper.interpret oracle (getTargetContracts opts)) initialVm+  let depth = fromMaybe 20 maxDepth+  ((x, counterex), vm') <-+    if null replayTxs+    then+    foldM (\a@((success, _), _) _ ->+                       if success+                       then runStateT (EVM.Stepper.interpret oracle (explorationStepper opts testName [] targets (List []) depth)) initialVm+                       else pure a)+                       ((True, (List [])), initialVm)  -- no canonical "post vm"+                       [0..fuzzRuns]+    else runStateT (EVM.Stepper.interpret oracle (explorationStepper opts testName replayTxs targets (List []) (length replayTxs))) initialVm+  if x+  then return ("\x1b[32m[PASS]\x1b[0m " <> testName <>  " (runs: " <> (pack $ show fuzzRuns) <>", depth: " <> pack (show depth) <> ")",+               Right (passOutput vm' opts testName), vm') -- no canonical "post vm"+  else let replayText = if null replayTxs+                        then "\nReplay data: '(" <> pack (show testName) <> ", " <> pack (show (show (ByteStringS $ rlpencode counterex))) <> ")'"+                        else " (replayed)"+       in return ("\x1b[31m[FAIL]\x1b[0m " <> testName <> replayText, Left  (failOutput vm' opts testName), vm')++execTest :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Bool, VM)+execTest opts@UnitTestOptions{..} vm testName args =+  runStateT+    (EVM.Stepper.interpret oracle (execTestStepper opts testName args))+    vm+ -- | Define the thread spawner for normal test cases runOne :: UnitTestOptions -> VM -> ABIMethod -> AbiValue -> IO (Text, Either Text Text, VM) runOne opts@UnitTestOptions{..} vm testName args = do   let argInfo = pack (if args == emptyAbi then "" else " with arguments: " <> show args)-  (bailed, vm') <--    runStateT-      (EVM.Stepper.interpret oracle (execTest opts testName args))-      vm+  (bailed, vm') <- execTest opts vm testName args   (success, vm'') <-     runStateT       (EVM.Stepper.interpret oracle (checkFailures opts testName bailed)) vm'@@ -538,7 +682,7 @@       -- report a failure unless the test is supposed to fail.        \(bailed, vm') -> do-        let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+        let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts }         SBV.resetAssertions         constrain $ sAnd (fst <$> view EVM.constraints vm')         unless bailed $@@ -580,7 +724,7 @@     showRes vm = let Just res = view result vm in                  case res of                    VMFailure _ ->-                     let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+                     let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts}                      in prettyvmresult res                    VMSuccess _ -> if "proveFail" `isPrefixOf` testName                                   then "Successful execution"@@ -627,7 +771,7 @@   -- Ask whether any assertions failed   Stepper.evm $ do     popTrace-    abiCall testParams "failed()" emptyAbi+    abiCall testParams (Left ("failed()", emptyAbi))   Stepper.runFully  indentLines :: Int -> Text -> Text@@ -637,7 +781,7 @@  passOutput :: VM -> UnitTestOptions -> Text -> Text passOutput vm UnitTestOptions { .. } testName =-  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts }   in let v = fromMaybe 0 verbose   in if (v > 1) then     mconcat@@ -652,7 +796,7 @@  failOutput :: VM -> UnitTestOptions -> Text -> Text failOutput vm UnitTestOptions { .. } testName =-  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env }+  let ?context = DappContext { _contextInfo = dapp, _contextEnv = vm ^?! EVM.env . EVM.contracts}   in mconcat   [ "Failure: "   , fromMaybe "" (stripSuffix "()" testName)@@ -736,9 +880,11 @@ word32Bytes :: Word32 -> ByteString word32Bytes x = BS.pack [byteAt x (3 - i) | i <- [0..3]] -abiCall :: TestVMParams -> Text -> AbiValue -> EVM ()-abiCall params sig args =-  let cd = abiMethod sig args+abiCall :: TestVMParams -> Either (Text, AbiValue) ByteString -> EVM ()+abiCall params args =+  let cd = case args of+        Left (sig, args') -> abiMethod sig args'+        Right b -> b       l = num . BS.length $ cd   in makeTxCall params (ConcreteBuffer cd, litWord l) @@ -781,6 +927,7 @@            , vmoptCreate = True            , vmoptStorageModel = ConcreteS -- TODO: support RPC            , vmoptTxAccessList = mempty -- TODO: support unit test access lists???+           , vmoptAllowFFI = allowFFI            }     creator =       initialContract (RuntimeCode mempty)

@@ -285,6 +285,7 @@          , vmoptCreate        = isCreate          , vmoptStorageModel  = EVM.ConcreteS          , vmoptTxAccessList  = txAccessMap tx+         , vmoptAllowFFI      = False          })         checkState         postState

@@ -3,7 +3,6 @@ {-# Language ScopedTypeVariables #-} {-# Language LambdaCase #-} {-# Language QuasiQuotes #-}-{-# Language TypeSynonymInstances #-} {-# Language FlexibleInstances #-} {-# Language GeneralizedNewtypeDeriving #-} {-# Language DataKinds #-}@@ -18,7 +17,7 @@  import qualified Data.Text as Text import qualified Data.ByteString as BS-import qualified Data.ByteString.Lazy as BS (fromStrict, toStrict)+import qualified Data.ByteString.Lazy as BS (fromStrict) import qualified Data.ByteString.Base16 as Hex import Test.Tasty import Test.Tasty.QuickCheck@@ -67,7 +66,7 @@     , testCase "Arithmetic" $ do         SolidityCall "x = a + 1;"           [AbiUInt 256 1] ===> AbiUInt 256 2-        SolidityCall "x = a - 1;"+        SolidityCall "unchecked { x = a - 1; }"           [AbiUInt 8 0] ===> AbiUInt 8 255      , testCase "keccak256()" $@@ -252,7 +251,7 @@           }           |]         bs <- runSMTWith cvc4 $ query $ do-          (Right _, vm) <- checkAssert factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+          (Right _, vm) <- checkAssert defaultPanicCodes factor (Just ("factor(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           case view (state . calldata . _1) vm of             SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs             ConcreteBuffer _ -> error "unexpected"@@ -267,8 +266,10 @@           contract A {             uint x;             function f(uint256 y) public {-               x += y;-               x += y;+               unchecked {+                 x += y;+                 x += y;+               }             }           }           |]@@ -320,7 +321,7 @@           (Right _, vm) <- verifyContract c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) [] SymbolicS pre (Just post)           case view (state . calldata . _1) vm of             SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs-            ConcreteBuffer bs -> error "unexpected"+            ConcreteBuffer _ -> error "unexpected"          let [AbiUInt 256 x, AbiUInt 256 y] = decodeAbiValues [AbiUIntType 256, AbiUIntType 256] bs         assertEqual "Catch storage collisions" x y@@ -344,7 +345,7 @@               }              }             |]-          (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []+          (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,                 testCase "Deposit contract loop (cvc4)" $ do@@ -366,7 +367,7 @@               }              }             |]-          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("deposit(uint256)", [AbiUIntType 256])) []+          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("deposit(uint256)", [AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,         testCase "Deposit contract loop (error version)" $ do@@ -389,7 +390,7 @@              }             |]           bs <- runSMT $ query $ do-            (Right _, vm) <- checkAssert c (Just ("deposit(uint8)", [AbiUIntType 8])) []+            (Right _, vm) <- checkAssert allPanicCodes c (Just ("deposit(uint8)", [AbiUIntType 8])) []             case view (state . calldata . _1) vm of               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs               ConcreteBuffer _ -> error "unexpected"@@ -408,7 +409,7 @@           |]         (Left res, _) <- runSMTWith z3 $ do           setTimeOut 5000-          query $ checkAssert c Nothing []+          query $ checkAssert defaultPanicCodes c Nothing []         putStrLn $ "successfully explored: " <> show (length res) <> " paths"         , @@ -421,7 +422,7 @@               }             }             |]-          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+          (Left res, _) <- runSMTWith cvc4 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,         testCase "injectivity of keccak (32 bytes)" $ do@@ -433,7 +434,7 @@               }             }             |]-          (Left res, _) <- runSMTWith z3 $ query $ checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+          (Left res, _) <- runSMTWith z3 $ query $ checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"        , @@ -447,7 +448,7 @@             }             |]           bs <- runSMTWith z3 $ query $ do-            (Right _, vm) <- checkAssert c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []+            (Right _, vm) <- checkAssert defaultPanicCodes c (Just ("f(uint256,uint256,uint256,uint256)", replicate 4 (AbiUIntType 256))) []             case view (state . calldata . _1) vm of               SymbolicBuffer bs -> BS.pack <$> mapM (getValue.fromSized) bs               ConcreteBuffer _ -> error "unexpected"@@ -479,7 +480,7 @@             |]           Left res <- runSMTWith z3 $ do             setTimeOut 5000-            query $ fst <$> checkAssert c Nothing []+            query $ fst <$> checkAssert defaultPanicCodes c Nothing []           putStrLn $ "successfully explored: " <> show (length res) <> " paths"         ,@@ -496,8 +497,8 @@               }             |]           -- should find a counterexample-          Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []-          putStrLn $ "found counterexample:"+          Right _ <- runSMTWith cvc4 $ query $ fst <$> checkAssert defaultPanicCodes c (Just ("f(uint256,uint256)", [AbiUIntType 256, AbiUIntType 256])) []+          putStrLn "found counterexample:"         ,@@ -520,7 +521,7 @@               aAddr = Addr 0x35D1b3F3D7966A1DFe207aa4514C12a259A0492B           Just c <- solcRuntime "C" code           Just a <- solcRuntime "A" code-          Right cex <- runSMT $ query $ do+          Right _ <- runSMT $ query $ do             vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS             store <- freshArray (show aAddr) Nothing             let vm = vm0@@ -528,8 +529,8 @@                   & over (env . contracts)                        (Map.insert aAddr (initialContract (RuntimeCode $ ConcreteBuffer a) &                                            set EVM.storage (EVM.Symbolic [] store)))-            verify vm Nothing Nothing (Just checkAssertions)-          putStrLn $ "found counterexample:"+            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+          putStrLn "found counterexample:"       ,          testCase "calling unique contracts (read from storage)" $ do           let code =@@ -549,11 +550,11 @@                   }                 |]           Just c <- solcRuntime "C" code-          Right cex <- runSMT $ query $ do+          Right _ <- runSMT $ query $ do             vm0 <- abstractVM (Just ("call_A()", [])) [] c SymbolicS             let vm = vm0 & set (state . callvalue) 0-            verify vm Nothing Nothing (Just checkAssertions)-          putStrLn $ "found counterexample:"+            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+          putStrLn "found counterexample:"       ,           testCase "keccak concrete and sym agree" $ do@@ -571,15 +572,15 @@           Left _ <- runSMT $ query $ do             vm0 <- abstractVM (Just ("kecc(uint256)", [AbiUIntType 256])) [] c SymbolicS             let vm = vm0 & set (state . callvalue) 0-            verify vm Nothing Nothing (Just checkAssertions)-          putStrLn $ "found counterexample:"+            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+          putStrLn "found counterexample:"        , testCase "safemath distributivity (yul)" $ do           Left _ <- runSMTWith cvc4 $ query $ do             let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b"             vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] yulsafeDistributivity SymbolicS-            verify vm Nothing Nothing (Just checkAssertions)-          putStrLn $ "Proven"+            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+          putStrLn "Proven"        , testCase "safemath distributivity (sol)" $ do           let code =@@ -590,10 +591,14 @@                       }                        function add(uint x, uint y) internal pure returns (uint z) {-                          require((z = x + y) >= x, "ds-math-add-overflow");+                          unchecked {+                            require((z = x + y) >= x, "ds-math-add-overflow");+                          }                       }                       function mul(uint x, uint y) internal pure returns (uint z) {-                          require(y == 0 || (z = x * y) / y == x, "ds-math-mul-overflow");+                          unchecked {+                            require(y == 0 || (z = x * y) / y == x, "ds-math-mul-overflow");+                          }                       }                  }                 |]@@ -601,8 +606,8 @@            Left _ <- runSMTWith z3 $ query $ do             vm <- abstractVM (Just ("distributivity(uint256,uint256,uint256)", [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] c SymbolicS-            verify vm Nothing Nothing (Just checkAssertions)-          putStrLn $ "Proven"+            verify vm Nothing Nothing (Just $ checkAssertions defaultPanicCodes)+          putStrLn "Proven"      ]   , testGroup "Equivalence checking"@@ -620,7 +625,7 @@         let aPrgm = hex "602060006000376000805160008114601d5760018114602457fe6029565b8191506029565b600191505b50600160015250"             bPrgm = hex "6020600060003760005160008114601c5760028114602057fe6021565b6021565b5b506001600152"         runSMTWith z3 $ query $ do-          Right counterexample <- equivalenceCheck aPrgm bPrgm Nothing Nothing+          Right _ <- equivalenceCheck aPrgm bPrgm Nothing Nothing           return ()      ]@@ -652,8 +657,8 @@ hex :: ByteString -> ByteString hex s =   case Hex.decode s of-    (x, "") -> x-    _ -> error "internal error"+    Right x -> x+    Left e -> error e  singleContract :: Text -> Text -> IO (Maybe ByteString) singleContract x s =@@ -753,4 +758,4 @@   b  <- f a   b' <- f a'   return (b, b')-  +