Update hevm to 0.51.3 (#1090)

flake.nix

@@ -42,8 +42,8 @@
           pkgs.haskellPackages.callCabal2nix "hevm" (pkgs.fetchFromGitHub {
             owner = "ethereum";
             repo = "hevm";
-            rev = "release/0.50.5";
-            sha256 = "sha256-Vi6kL1nJdujfS1oePwqks1owVPlS5Dd5hAn0r8Rpw+k=";
+            rev = "release/0.51.3";
+            sha256 = "sha256-H6oURBGoQWSOuPhBB+UKg2UarVzXgv1tmfDBLnOtdhU=";
         }) { secp256k1 = pkgs.secp256k1; });
 
         echidna = with pkgs; lib.pipe

lib/Echidna.hs

@@ -9,9 +9,10 @@ import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import System.FilePath ((</>))
 
-import EVM hiding (Env)
+import EVM (cheatCode)
 import EVM.ABI (AbiValue(AbiAddress))
 import EVM.Solidity (SolcContract(..))
+import EVM.Types hiding (Env)
 
 import Echidna.ABI
 import Echidna.Etheno (loadEtheno, extractFromEtheno)

lib/Echidna/Campaign.hs

@@ -24,9 +24,9 @@ import Data.Set qualified as Set
 import Data.Text (Text)
 import System.Random (mkStdGen)
 
-import EVM hiding (Env, Frame(state))
+import EVM (bytecode, cheatCode)
 import EVM.ABI (getAbi, AbiType(AbiAddressType), AbiValue(AbiAddress))
-import EVM.Types (Addr, Expr(ConcreteBuf))
+import EVM.Types hiding (Env, Frame(state))
 
 import Echidna.ABI
 import Echidna.Exec

lib/Echidna/Config.hs

@@ -13,8 +13,7 @@ import Data.Set qualified as Set
 import Data.Text (isPrefixOf)
 import Data.Yaml qualified as Y
 
-import EVM (VM(..))
-import EVM.Types (W256)
+import EVM.Types (VM(..), W256)
 
 import Echidna.Test
 import Echidna.Types.Campaign

lib/Echidna/Deploy.hs

@@ -11,9 +11,8 @@ import Data.Either (fromRight)
 import Data.Text (Text, unlines)
 import Data.Text.Encoding (encodeUtf8)
 
-import EVM hiding (bytecode, Env)
 import EVM.Solidity
-import EVM.Types (Addr)
+import EVM.Types hiding (Env)
 
 import Echidna.Exec (execTx)
 import Echidna.Events (extractEvents)

lib/Echidna/Etheno.hs

@@ -11,7 +11,7 @@ import Control.Exception (Exception)
 import Control.Monad (void)
 import Control.Monad.Catch (MonadThrow, throwM)
 import Control.Monad.Fail qualified as M (MonadFail(..))
-import Control.Monad.State.Strict (MonadState, get, put, execStateT, gets)
+import Control.Monad.State.Strict (MonadState, get, put, execStateT, gets, modify', execState)
 import Data.Aeson (FromJSON(..), (.:), withObject, eitherDecodeFileStrict)
 import Data.ByteString.Base16 qualified as BS16 (decode)
 import Data.ByteString.Char8 (ByteString)
@@ -26,7 +26,7 @@ import Text.Read (readMaybe)
 import EVM
 import EVM.ABI (AbiType(..), AbiValue(..), decodeAbiValue, selector)
 import EVM.Exec (exec)
-import EVM.Types (Addr, W256, Expr(ConcreteBuf))
+import EVM.Types
 
 import Echidna.Exec
 import Echidna.Transaction
@@ -168,19 +168,28 @@ execEthenoTxs :: (MonadState VM m, MonadFail m, MonadThrow m) => Etheno -> m ()
 execEthenoTxs et = do
   setupEthenoTx et
   vm <- get
-  res <- fromEVM exec
-  case (res, et) of
-    (_        , AccountCreated _)  -> pure ()
-    (Reversion,   _)               -> void $ put vm
-    (VMFailure (Query q), _)       -> crashWithQueryError q et
-    (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
-    (VMSuccess (ConcreteBuf bc),
-     ContractCreated _ ca _ _ _ _) -> do
-      #env % #contracts % at ca % _Just % #contractcode .= InitCode mempty mempty
-      fromEVM $ do
-        replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bc))
-        loadContract ca
-    _ -> pure ()
+  runFully vm
+  where
+  runFully vm = do
+    res <- fromEVM exec
+    case (res, et) of
+      (_        , AccountCreated _)  -> pure ()
+      (Reversion,   _)               -> void $ put vm
+      (HandleEffect (Query (PleaseAskSMT (Lit c) _ continue)), _) -> do
+        -- NOTE: this is not a real SMT query, we know it is concrete and can
+        -- resume right away. It is done this way to support iterations counting
+        -- in hevm.
+        modify' $ execState (continue (Case (c > 0)))
+        runFully vm
+      (HandleEffect (Query q), _)    -> crashWithQueryError q et
+      (VMFailure x, _)               -> vmExcept x >> M.fail "impossible"
+      (VMSuccess (ConcreteBuf bc),
+       ContractCreated _ ca _ _ _ _) -> do
+        #env % #contracts % at ca % _Just % #contractcode .= InitCode mempty mempty
+        fromEVM $ do
+          replaceCodeOfSelf (RuntimeCode (ConcreteRuntimeCode bc))
+          loadContract ca
+      _ -> pure ()
 
 -- | For an etheno txn, set up VM to execute txn
 setupEthenoTx :: MonadState VM m => Etheno -> m ()

lib/Echidna/Events.hs

@@ -13,12 +13,12 @@ import Data.Tree (flatten)
 import Data.Tree.Zipper (fromForest, TreePos, Empty)
 import Data.Vector (fromList)
 
-import EVM hiding (code)
+import EVM (traceForest)
 import EVM.ABI (Event(..), Indexed(..), decodeAbiValue, AbiType(..), AbiValue(..))
 import EVM.Dapp (DappContext(..), DappInfo(..))
 import EVM.Format (showValues, showError, contractNamePart)
 import EVM.Solidity (SolcContract(..))
-import EVM.Types (Expr(ConcreteBuf), W256, maybeLitWord)
+import EVM.Types
 
 import Echidna.Types.Buffer (forceLit, forceBuf)
 import Data.ByteString (ByteString)

lib/Echidna/Exec.hs

@@ -22,11 +22,12 @@ import Data.Vector qualified as V
 import Data.Vector.Unboxed.Mutable qualified as VMut
 import System.Process (readProcessWithExitCode)
 
-import EVM hiding (Env)
+import EVM (bytecode, replaceCodeOfSelf, loadContract, exec1, vmOpIx)
 import EVM.ABI
 import EVM.Exec (exec, vmForEthrunCreation)
 import EVM.Fetch qualified
-import EVM.Types (Expr(ConcreteBuf, Lit), hexText)
+import EVM.Format (hexText)
+import EVM.Types hiding (Env)
 
 import Echidna.Events (emptyEvents)
 import Echidna.RPC (safeFetchContractFrom, safeFetchSlotFrom)
@@ -43,7 +44,7 @@ import Echidna.Utility (getTimestamp, timePrefix)
 data ErrorClass = RevertE | IllegalE | UnknownE
 
 -- | Given an execution error, classify it. Mostly useful for nice @pattern@s ('Reversion', 'Illegal').
-classifyError :: Error -> ErrorClass
+classifyError :: EvmError -> ErrorClass
 classifyError = \case
   OutOfGas _ _         -> RevertE
   Revert _             -> RevertE
@@ -56,8 +57,8 @@ classifyError = \case
 
 -- | Extracts the 'Query' if there is one.
 getQuery :: VMResult -> Maybe Query
-getQuery (VMFailure (Query q)) = Just q
-getQuery _                     = Nothing
+getQuery (HandleEffect (Query q)) = Just q
+getQuery _ = Nothing
 
 -- | Matches execution errors that just cause a reversion.
 pattern Reversion :: VMResult
@@ -68,7 +69,7 @@ pattern Illegal :: VMResult
 pattern Illegal <- VMFailure (classifyError -> IllegalE)
 
 -- | Given an execution error, throw the appropriate exception.
-vmExcept :: MonadThrow m => Error -> m ()
+vmExcept :: MonadThrow m => EvmError -> m ()
 vmExcept e = throwM $
   case VMFailure e of {Illegal -> IllegalExec e; _ -> UnknownFailure e}
 
@@ -77,7 +78,7 @@ vmExcept e = throwM $
 execTxWith
   :: (MonadIO m, MonadState s m, MonadReader Env m)
   => Lens' s VM
-  -> (Error -> m ())
+  -> (EvmError -> m ())
   -> m VMResult
   -> Tx
   -> m (VMResult, Gas)
@@ -120,7 +121,7 @@ execTxWith l onErr executeTx tx = do
                 ret <- liftIO $ safeFetchContractFrom rpcBlock rpcUrl addr
                 case ret of
                   -- TODO: fix hevm to not return an empty contract in case of an error
-                  Just contract | contract.contractcode /= EVM.RuntimeCode (EVM.ConcreteRuntimeCode "") -> do
+                  Just contract | contract.contractcode /= RuntimeCode (ConcreteRuntimeCode "") -> do
                     metaCacheRef <- asks (.metadataCache)
                     metaCache <- liftIO $ readIORef metaCacheRef
                     let bc = forceBuf (contract ^. bytecode)
@@ -182,6 +183,16 @@ execTxWith l onErr executeTx tx = do
         l %= execState (continuation encodedResponse)
         runFully
 
+      Just (PleaseAskSMT (Lit c) _ continue) -> do
+        -- NOTE: this is not a real SMT query, we know it is concrete and can
+        -- resume right away. It is done this way to support iterations counting
+        -- in hevm.
+        l %= execState (continue (Case (c > 0)))
+        runFully
+
+      Just q@(PleaseAskSMT {}) ->
+        error $ "Unexpected SMT query: " <> show q
+
       -- No queries to answer, the tx is fully executed and the result is final
       _ -> pure vmResult
 

lib/Echidna/Output/Source.hs

@@ -1,8 +1,11 @@
+{-# LANGUAGE ViewPatterns #-}
+
 module Echidna.Output.Source where
 
 import Prelude hiding (writeFile)
 
 import Data.Aeson (ToJSON(..), FromJSON(..), withText)
+import Data.ByteString qualified as BS
 import Data.Foldable
 import Data.List (nub, sort)
 import Data.Maybe (fromMaybe, mapMaybe)
@@ -28,8 +31,6 @@ import Echidna.Types.Coverage (OpIx, unpackTxResults, CoverageMap)
 import Echidna.Types.Tx (TxResult(..))
 import Echidna.Types.Signature (getBytecodeMetadata)
 
-type FilePathText = Text
-
 saveCoverages
   :: [CoverageFileType]
   -> Int
@@ -78,20 +79,18 @@ coverageFileExtension Txt = ".txt"
 ppCoveredCode :: CoverageFileType -> SourceCache -> [SolcContract] -> CoverageMap -> IO Text
 ppCoveredCode fileType sc cs s | null s = pure "Coverage map is empty"
   | otherwise = do
-  let allFiles = zipWith (\(srcPath, _rawSource) srcLines -> (srcPath, V.map decodeUtf8 srcLines))
-                   sc.files
-                   sc.lines
-      -- ^ Collect all the possible lines from all the files
+  -- List of covered lines during the fuzzing campaing
   covLines <- srcMapCov sc s cs
-      -- ^ List of covered lines during the fuzzing campaing
   let
+    -- Collect all the possible lines from all the files
+    allFiles = (\(path, src) -> (path, V.fromList (decodeUtf8 <$> BS.split 0xa src))) <$> Map.elems sc.files
+    -- Excludes lines such as comments or blanks
     runtimeLinesMap = buildRuntimeLinesMap sc cs
-    -- ^ Excludes lines such as comments or blanks
+    -- Pretty print individual file coverage
     ppFile (srcPath, srcLines) =
       let runtimeLines = fromMaybe mempty $ Map.lookup srcPath runtimeLinesMap
           marked = markLines fileType srcLines runtimeLines (fromMaybe Map.empty (Map.lookup srcPath covLines))
       in T.unlines (changeFileName srcPath : changeFileLines (V.toList marked))
-    -- ^ Pretty print individual file coverage
     topHeader = case fileType of
       Lcov -> "TN:\n"
       Html -> "<style> code { white-space: pre-wrap; display: block; background-color: #eee; }" <>
@@ -102,7 +101,7 @@ ppCoveredCode fileType sc cs s | null s = pure "Coverage map is empty"
               "</style>"
       Txt  -> ""
     -- ^ Text to add to top of the file
-    changeFileName fn = case fileType of
+    changeFileName (T.pack -> fn) = case fileType of
       Lcov -> "SF:" <> fn
       Html -> "<b>" <> HTML.text fn <> "</b>"
       Txt  -> fn
@@ -158,11 +157,11 @@ getMarker ErrorOutOfGas = 'o'
 getMarker _             = 'e'
 
 -- | Given a source cache, a coverage map, a contract returns a list of covered lines
-srcMapCov :: SourceCache -> CoverageMap -> [SolcContract] -> IO (Map FilePathText (Map Int [TxResult]))
+srcMapCov :: SourceCache -> CoverageMap -> [SolcContract] -> IO (Map FilePath (Map Int [TxResult]))
 srcMapCov sc covMap contracts = do
   Map.unionsWith Map.union <$> mapM linesCovered contracts
   where
-  linesCovered :: SolcContract -> IO (Map Text (Map Int [TxResult]))
+  linesCovered :: SolcContract -> IO (Map FilePath (Map Int [TxResult]))
   linesCovered c =
     case Map.lookup (getBytecodeMetadata c.runtimeCode) covMap of
       Just vec -> VU.foldl' (\acc covInfo -> case covInfo of
@@ -193,7 +192,7 @@ srcMapForOpLocation contract opIx =
 
 -- | Builds a Map from file paths to lines that can be executed, this excludes
 -- for example lines with comments
-buildRuntimeLinesMap :: SourceCache -> [SolcContract] -> Map Text (S.Set Int)
+buildRuntimeLinesMap :: SourceCache -> [SolcContract] -> Map FilePath (S.Set Int)
 buildRuntimeLinesMap sc contracts =
   Map.fromListWith (<>)
     [(k, S.singleton v) | (k, v) <- mapMaybe (srcMapCodePos sc) srcMaps]

lib/Echidna/RPC.hs

@@ -14,9 +14,9 @@ import Network.HTTP.Simple (HttpException)
 import System.Environment
 import Text.Read (readMaybe)
 
-import EVM (Contract(..), ContractCode(RuntimeCode), RuntimeCode (..), initialContract)
+import EVM (initialContract)
 import EVM.Fetch qualified
-import EVM.Types (Addr, W256)
+import EVM.Types
 
 import Echidna.Orphans.JSON ()
 import Echidna.Types (emptyAccount)

lib/Echidna/Shrink.hs

@@ -8,7 +8,7 @@ import Control.Monad.State.Strict (MonadIO)
 import Data.Set qualified as Set
 import Data.List qualified as List
 
-import EVM (VM)
+import EVM.Types (VM)
 
 import Echidna.Events (extractEvents)
 import Echidna.Exec