Fixing staticcall abstraction, test case search, and commenting out bug with solidity

CHANGELOG.md

@@ -19,6 +19,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - We now try to simplify expressions fully before trying to cast them to a concrete value
   This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
   unnecessarily output
+- STATICCALL abstraction left incorrect stack, fixed
+- Not all testcases ran due to incorrect filtering, fixed
 
 ## [0.54.2] - 2024-12-12
 

src/EVM.hs

@@ -1011,21 +1011,20 @@ exec1 = do
                               assign #static True
                             touchAccount self
                             touchAccount callee
-            _ ->
-              underrun
-            where
-              fallback = do
-                -- Reset caller if needed
-                resetCaller <- use $ #state % #resetCaller
-                when resetCaller $ assign (#state % #overrideCaller) Nothing
-                -- overapproximate by returning a symbolic value
-                freshVar <- use #freshVar
-                assign #freshVar (freshVar + 1)
-                let freshVarExpr = Var ("staticcall-result-stack-" <> (pack . show) freshVar)
-                pushSym freshVarExpr
-                modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
-                assign (#state % #returndata) (AbstractBuf ("staticall-result-data-" <> (pack . show) freshVar))
-                next
+              where
+                fallback :: EVM t s ()
+                fallback = do
+                  -- Reset caller if needed
+                  resetCaller <- use $ #state % #resetCaller
+                  when resetCaller $ assign (#state % #overrideCaller) Nothing
+                  -- overapproximate by returning a symbolic value
+                  freshVar <- use #freshVar
+                  assign #freshVar (freshVar + 1)
+                  let freshVarExpr = Var ("staticcall-result-stack-" <> (pack . show) freshVar)
+                  modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) ))
+                  assign (#state % #returndata) (AbstractBuf ("staticall-result-data-" <> (pack . show) freshVar))
+                  next >> assign (#state % #stack) (freshVarExpr:xs)
+            _ -> underrun
 
         OpSelfdestruct ->
           notStatic $

src/EVM/SymExec.hs

@@ -680,13 +680,16 @@ equivalenceCheck
   -> (Expr Buf, [Prop])
   -> m [EquivResult]
 equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
+  conf <- readConfig
   case bytecodeA == bytecodeB of
     True -> liftIO $ do
       putStrLn "bytecodeA and bytecodeB are identical"
       pure [Qed ()]
     False -> do
       branchesA <- getBranches bytecodeA
       branchesB <- getBranches bytecodeB
+      when conf.debug $ liftIO $ do
+        putStrLn "bytecodeA and bytecodeB are different, checking for equivalence"
       equivalenceCheck' solvers branchesA branchesB
   where
     -- decompiles the given bytecode into a list of branches

test/test.hs

@@ -3926,6 +3926,10 @@ tests = testGroup "hevm"
                     , "unusedStoreEliminator/tstore.yul"
                     , "yulOptimizerTests/fullSuite/transient_storage.yul"
                     , "yulOptimizerTests/unusedPruner/transient_storage.yul"
+
+                    -- Bug in solidity, fized in newer versions:
+                    -- https://github.com/ethereum/solidity/issues/15397#event-14116827816
+                    , "no_move_transient_storage.yul"
                     ]
 
         solcRepo <- liftIO $ fromMaybe (internalError "cannot find solidity repo") <$> (lookupEnv "HEVM_SOLIDITY_REPO")
@@ -3944,7 +3948,7 @@ tests = testGroup "hevm"
                 False -> recursiveList ax (a:b)
           recursiveList [] b = pure b
         files <- liftIO $ recursiveList fullpaths []
-        let filesFiltered = filter (\file -> not $ any (`List.isSubsequenceOf` file) ignoredTests) files
+        let filesFiltered = filter (\file -> not $ any (`List.isInfixOf` file) ignoredTests) files
 
         -- Takes one file which follows the Solidity Yul optimizer unit tests format,
         -- extracts both the nonoptimized and the optimized versions, and checks equivalence.