Update hevm to 9924e80dd0226c1f3e1eda651bbeb3558f419843

.github/scripts/install-libff.sh

@@ -35,9 +35,14 @@ if [ "$HOST_OS" = "Linux" ] && [ "$(uname -m)" = "aarch64" ]; then
 fi
 
 if [ "$HOST_OS" = "Windows" ]; then
-  ARGS+=("-G" "Ninja")
+  ARGS+=("-G" "Ninja" "-DCMAKE_TOOLCHAIN_FILE=$PWD/../.github/scripts/windows-ghc-toolchain.cmake")
   sed -i 's/find_library(GMP_LIBRARY gmp)/find_library(GMP_LIBRARY NAMES libgmp.a)/' CMakeLists.txt
 
+  # This ends up causing the system headers to be included with -I and
+  # thus they override the GHC mingw compiler ones. So this removes it
+  # and re-adds the include with idirafter via the toolchain file
+  sed -i '/INCLUDE_DIRECTORIES.*OPENSSL_INCLUDE_DIR/d' CMakeLists.txt
+
   # Apply windows-specific libff patch carried by hevm
   curl -fsSL https://raw.githubusercontent.com/ethereum/hevm/1abe4c79eeada928acc279b631c48eeb2a1376c2/.github/scripts/libff.patch | patch -p1
 fi

.github/scripts/windows-ghc-toolchain.cmake

@@ -0,0 +1,12 @@
+set(CMAKE_SYSTEM_NAME Windows)
+
+set(CMAKE_C_COMPILER "$ENV{HASKELL_MINGW_PATH}/bin/cc.exe")
+set(CMAKE_CXX_COMPILER "$ENV{HASKELL_MINGW_PATH}/bin/c++.exe")
+
+set(CMAKE_C_FLAGS "-idirafter $ENV{SYSTEM_MINGW_PATH}/include")
+set(CMAKE_CXX_FLAGS "-idirafter $ENV{SYSTEM_MINGW_PATH}/include")
+
+set(CMAKE_FIND_ROOT_PATH "$ENV{HASKELL_MINGW_PATH}")
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY BOTH)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE BOTH)

.github/workflows/ci.yml

@@ -40,6 +40,7 @@ jobs:
       - name: Get Packages (Windows)
         uses: msys2/setup-msys2@v2
         if: runner.os == 'Windows'
+        id: msys2
         with:
           msystem: CLANG64
           path-type: minimal
@@ -104,11 +105,16 @@ jobs:
         if: runner.os == 'Windows'
         run: |
           HASKELL_PATHS="$(cygpath -u "$GHC_PATH"):$(cygpath -u "$CABAL_PATH"):$(cygpath -u "$STACK_PATH")"
+          HASKELL_MINGW_PATH="$(cygpath -u "$GHC_PATH/../mingw")"
+          SYSTEM_MINGW_PATH="$(cygpath -m "$MSYS2_LOCATION/$MSYSTEM")"
           echo "HASKELL_PATHS=$HASKELL_PATHS" >> "$GITHUB_ENV"
+          echo "HASKELL_MINGW_PATH=$HASKELL_MINGW_PATH" >> "$GITHUB_ENV"
+          echo "SYSTEM_MINGW_PATH=$SYSTEM_MINGW_PATH" >> "$GITHUB_ENV"
         env:
           GHC_PATH: ${{ steps.stack.outputs.ghc-path }}
           CABAL_PATH: ${{ steps.stack.outputs.cabal-path }}
           STACK_PATH: ${{ steps.stack.outputs.stack-path }}
+          MSYS2_LOCATION: ${{ steps.msys2.outputs.msys2-location }}
 
       - name: Checkout
         uses: actions/checkout@v4
@@ -140,7 +146,7 @@ jobs:
       - name: Build Libraries
         run: |
           if [ "$HOST_OS" = "Windows" ]; then
-            export PATH="$(cygpath -u "$GHC_BIN_PATH/../mingw/bin"):$PATH"
+            export PATH="$(cygpath -u "$HASKELL_MINGW_PATH/bin"):$PATH"
           fi
           .github/scripts/install-libsecp256k1.sh
           .github/scripts/install-libff.sh

flake.nix

@@ -52,8 +52,8 @@
         hevm = pkgs: pkgs.lib.pipe ((hsPkgs pkgs).callCabal2nix "hevm" (pkgs.fetchFromGitHub {
           owner = "ethereum";
           repo = "hevm";
-          rev = "release/0.54.2";
-          sha256 = "sha256-h0e6QeMBIUkyANYdrGjrqZ2M4fnODOB0gNPQtsrAiL8=";
+          rev = "9924e80dd0226c1f3e1eda651bbeb3558f419843";
+          sha256 = "sha256-HGvWD7AjqKinE/oYu9L4b2HetcKrO3B+hNCzJ761XAk=";
         }) { secp256k1 = pkgs.secp256k1; })
         ([
           pkgs.haskell.lib.compose.dontCheck

lib/Echidna/ABI.hs

@@ -191,7 +191,7 @@ getRandomInt :: MonadRandom m => Int -> m Integer
 getRandomInt n =
   getRandomR =<< Random.weighted
     [ ((-1023, 1023), 1)
-    , ((-1 * 2 ^ (n - 1), 2 ^ (n - 1) - 1), 9)
+    , (((-1) * 2 ^ (n - 1), 2 ^ (n - 1) - 1), 9)
     ]
 
 -- | Synthesize a random 'AbiValue' given its 'AbiType'. Doesn't use a dictionary.

lib/Echidna/Etheno.hs

@@ -25,6 +25,7 @@ import Text.Read (readMaybe)
 
 import EVM
 import EVM.ABI (AbiType(..), AbiValue(..), decodeAbiValue, selector)
+import EVM.Effects (defaultConfig)
 import EVM.Exec (exec)
 import EVM.Types
 
@@ -173,7 +174,7 @@ execEthenoTxs et = do
   runFully vm
   where
   runFully vm = do
-    res <- fromEVM exec
+    res <- fromEVM $ exec defaultConfig
     case (res, et) of
       (_        , AccountCreated _)  -> pure ()
       (Reversion,   _)               -> void $ put vm

lib/Echidna/Events.hs

@@ -17,6 +17,7 @@ import Data.Vector (fromList)
 import EVM (traceForest)
 import EVM.ABI (Event(..), Indexed(..), decodeAbiValue, AbiType(..), AbiValue(..))
 import EVM.Dapp (DappContext(..), DappInfo(..))
+import EVM.Expr (maybeLitWordSimp)
 import EVM.Format (showValues, showError, contractNamePart)
 import EVM.Solidity (SolcContract(..))
 import EVM.Types
@@ -37,7 +38,7 @@ extractEvents decodeErrors dappInfo vm =
   where
   showTrace trace =
     let ?context = DappContext { info = dappInfo, contracts = vm.env.contracts, labels = vm.labels } in
-    let codehash' = fromJust $ maybeLitWord trace.contract.codehash
+    let codehash' = fromJust $ maybeLitWordSimp trace.contract.codehash
         maybeContractName = maybeContractNameFromCodeHash dappInfo codehash'
     in case trace.tracedata of
       EventTrace addr bytes (topic:_) ->

lib/Echidna/Exec.hs

@@ -26,6 +26,7 @@ import System.Process qualified as P
 import EVM (bytecode, replaceCodeOfSelf, loadContract, exec1, vmOpIx, clearTStorages)
 import EVM.ABI
 import EVM.Dapp (DappInfo)
+import EVM.Effects (defaultConfig)
 import EVM.Exec (exec, vmForEthrunCreation)
 import EVM.Fetch qualified
 import EVM.Format (hexText, showTraceTree)
@@ -240,7 +241,7 @@ execTx
   => VM Concrete RealWorld
   -> Tx
   -> m ((VMResult Concrete RealWorld, Gas), VM Concrete RealWorld)
-execTx vm tx = runStateT (execTxWith (fromEVM exec) tx) vm
+execTx vm tx = runStateT (execTxWith (fromEVM (exec defaultConfig)) tx) vm
 
 -- | A type alias for the context we carry while executing instructions
 type CoverageContext = (Bool, Maybe (VMut.IOVector CoverageInfo, Int))
@@ -289,7 +290,7 @@ execTxWithCov tx = do
 
       -- | Execute one instruction on the EVM
       stepVM :: VM Concrete RealWorld -> IO (VM Concrete RealWorld)
-      stepVM = stToIO . execStateT exec1
+      stepVM = stToIO . execStateT (exec1 defaultConfig)
 
       -- | Add current location to the CoverageMap
       addCoverage :: VM Concrete RealWorld -> IO ()
@@ -339,6 +340,6 @@ initialVM :: Bool -> ST s (VM Concrete s)
 initialVM ffi = do
   vm <- vmForEthrunCreation mempty
   pure $ vm & #block % #timestamp .~ Lit initialTimestamp
-            & #block % #number .~ initialBlockNumber
+            & #block % #number .~ Lit initialBlockNumber
             & #env % #contracts .~ mempty -- fixes weird nonce issues
             & #config % #allowFFI .~ ffi

lib/Echidna/SourceAnalysis/Slither.hs

@@ -115,7 +115,7 @@ instance FromJSON SlitherInfo where
           :: Map ContractName (Map FunctionName [[Maybe AbiValue]])
           <- o .: "constants_used" >>= (traverse . traverse . traverse . traverse) parseConstant
         -- flatten [[AbiValue]], the array probably shouldn't be nested, fix it in Slither
-        let constantValues = (fmap . fmap) (catMaybes . concat) constantValues'
+        let constantValues = (fmap . fmap) (concatMap catMaybes) constantValues'
         functionsRelations <- o .: "functions_relations"
         generationGraph <-
           (traverse . traverse) (withObject "relations" (.: "impacts")) functionsRelations

lib/Echidna/SourceMapping.hs

@@ -11,8 +11,9 @@ import Data.Maybe (mapMaybe)
 import Data.Vector qualified as V
 import Echidna.Symbolic (forceWord)
 import EVM.Dapp (DappInfo(..), findSrc)
+import EVM.Expr (maybeLitByteSimp)
 import EVM.Solidity (SolcContract(..))
-import EVM.Types (Contract(..), ContractCode(..), RuntimeCode(..), W256, maybeLitByte)
+import EVM.Types (Contract(..), ContractCode(..), RuntimeCode(..), W256)
 
 -- | Map from contracts' codehashes to their compile-time codehash.
 -- This is relevant when the immutables solidity feature is used;
@@ -80,7 +81,7 @@ findSrcByMetadata contr dapp = find compareMetadata (snd <$> Map.elems dapp.solc
     (UnknownCode _) -> Nothing
     (InitCode c _) -> Just c
     (RuntimeCode (ConcreteRuntimeCode c)) -> Just c
-    (RuntimeCode (SymbolicRuntimeCode c)) -> Just $ BS.pack $ mapMaybe maybeLitByte $ V.toList c
+    (RuntimeCode (SymbolicRuntimeCode c)) -> Just $ BS.pack $ mapMaybe maybeLitByteSimp $ V.toList c
 
 getBytecodeMetadata :: ByteString -> ByteString
 getBytecodeMetadata bs =

lib/Echidna/SymExec.hs

@@ -29,13 +29,13 @@ import Echidna.Types.Solidity (SolConf(..))
 import EVM.ABI (AbiValue(..), AbiType(..), Sig(..), decodeAbiValue)
 import EVM.Expr (simplify)
 import EVM.Fetch qualified as Fetch
-import EVM.SMT (SMTCex(..), SMT2, assertProps)
+import EVM.SMT (SMT2, assertProps)
 import EVM (loadContract, resetState)
 import EVM.Effects (defaultEnv, defaultConfig)
 import EVM.Solidity (SolcContract(..), Method(..))
-import EVM.Solvers (withSolvers, Solver(Z3), CheckSatResult(Sat), SolverGroup, checkSat)
-import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, LoopHeuristic (Naive), flattenExpr, extractProps)
-import EVM.Types (Addr, VM(..), Frame(..), FrameState(..), VMType(..), Env(..), Expr(..), EType(..), Query(..), Prop(..), BranchCondition(..), W256, word256Bytes, word)
+import EVM.Solvers (withSolvers, Solver(Z3), SolverGroup, checkSat)
+import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, IterConfig(..), LoopHeuristic (Naive), flattenExpr, extractProps)
+import EVM.Types (Addr, VM(..), Frame(..), FrameState(..), VMType(..), Env(..), Expr(..), EType(..), Query(..), Prop(..), SMTCex(..), SMTResult, ProofResult(..), BranchCondition(..), W256, word256Bytes, word)
 import EVM.Traversals (mapExpr)
 import Control.Monad.ST (stToIO, RealWorld)
 import Control.Monad.State.Strict (execState, runStateT)
@@ -70,6 +70,7 @@ exploreContract conf contract tx vm = do
     timeout = Just (fromIntegral conf.campaignConf.symExecTimeout)
     maxIters = if isConc then Nothing else Just conf.campaignConf.symExecMaxIters
     askSmtIters = if isConc then 0 else conf.campaignConf.symExecAskSMTIters
+    iterConfig = IterConfig { maxIter = maxIters, askSmtIters = askSmtIters, loopHeuristic = Naive }
     rpcInfo = Nothing
     defaultSender = fromJust $ fmap (.dst) tx <|> Set.lookupMin conf.solConf.sender <|> Just 0
 
@@ -83,20 +84,19 @@ exploreContract conf contract tx vm = do
         let
           fetcher = concOrSymFetcher tx solvers rpcInfo
           dst = conf.solConf.contractAddr
-          calldata@(cd, constraints) = mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
-          vmSym = abstractVM calldata contract.runtimeCode Nothing False
-        vmSym' <- liftIO $ stToIO vmSym
+        calldata@(cd, constraints) <- mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+        vmSym <- liftIO $ stToIO $ abstractVM calldata contract.runtimeCode Nothing False
         vmReset <- liftIO $ snd <$> runStateT (fromEVM resetState) vm
         let vm' = vmReset & execState (loadContract (LitAddr dst))
                           & vmMakeSymbolic
                           & #constraints .~ constraints
                           & #state % #callvalue .~ TxValue
                           & #state % #caller .~ SymAddr "caller"
                           & #state % #calldata .~ cd
-                          & #env % #contracts .~ (Map.union vmSym'.env.contracts vm.env.contracts)
+                          & #env % #contracts .~ Map.union vmSym.env.contracts vm.env.contracts
         -- TODO we might want to switch vm's state.baseState value to to AbstractBase eventually.
         -- Doing so might mess up concolic execution.
-        exprInter <- interpret fetcher maxIters askSmtIters Naive vm' runExpr
+        exprInter <- interpret fetcher iterConfig vm' runExpr
         models <- liftIO $ mapConcurrently (checkSat solvers) $ manipulateExprInter isConc exprInter
         pure $ mapMaybe (modelToTx dst method conf.solConf.sender defaultSender) models
       liftIO $ putMVar resultChan $ concat res
@@ -137,6 +137,8 @@ vmMakeSymbolic vm
   , currentFork    = vm.currentFork
   , labels         = vm.labels
   , osEnv          = vm.osEnv
+  , freshVar       = vm.freshVar
+  , exploreDepth   = vm.exploreDepth
   }
 
 frameStateMakeSymbolic :: FrameState Concrete s -> FrameState Symbolic s
@@ -162,10 +164,10 @@ frameStateMakeSymbolic fs
 frameMakeSymbolic :: Frame Concrete s -> Frame Symbolic s
 frameMakeSymbolic fr = Frame { context = fr.context, state = frameStateMakeSymbolic fr.state }
 
-modelToTx :: Addr -> Method -> Set Addr -> Addr -> CheckSatResult -> Maybe Tx
+modelToTx :: Addr -> Method -> Set Addr -> Addr -> SMTResult -> Maybe Tx
 modelToTx dst method senders fallbackSender result =
   case result of
-    Sat cex ->
+    Cex cex ->
       let
         args = zipWith grabArg (snd <$> method.inputs) ["arg" <> T.pack (show n) | n <- [1..] :: [Int]]
 

lib/Echidna/Transaction.hs

@@ -198,4 +198,4 @@ setupTx tx@Tx{call} = fromEVM $ do
 advanceBlock :: Block -> (W256, W256) -> Block
 advanceBlock blk (t,b) =
   blk { timestamp = Lit (forceWord blk.timestamp + t)
-      , number = blk.number + b }
+      , number = Lit (forceWord blk.number + b) }

src/Main.hs

@@ -156,9 +156,9 @@ bool = maybeReader (f . map toLower) where
   f _ = Nothing
 
 options :: Parser Options
-options = Options
-  <$> (NE.fromList <$> some (argument str (metavar "FILES"
-    <> help "Solidity files to analyze")))
+options = Options . NE.fromList
+  <$> some (argument str (metavar "FILES"
+    <> help "Solidity files to analyze"))
   <*> optional (option auto $ long "workers"
     <> metavar "N"
     <> help "Number of workers to run")

stack.yaml

@@ -5,7 +5,7 @@ packages:
 
 extra-deps:
 - git: https://github.com/ethereum/hevm.git
-  commit: 037ff11779d0089378f01cb103db1171dc642be2
+  commit: 9924e80dd0226c1f3e1eda651bbeb3558f419843
 
 - smt2-parser-0.1.0.1@sha256:1e1a4565915ed851c13d1e6b8bb5185cf5d454da3b43170825d53e221f753d77,1421
 - spawn-0.3@sha256:b91e01d8f2b076841410ae284b32046f91471943dc799c1af77d666c72101f02,1162