From 3afe3f18a6f1f08f8db8acf34222c68eb65c80be Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Wed, 15 Jan 2025 18:15:14 +0100
Subject: [PATCH] Fixing bug in staticcall

Also:
- Adding one more exception due to bug in solidity
- Updating changelog
---
 CHANGELOG.md       |  2 ++
 src/EVM.hs         | 29 ++++++++++++++---------------
 src/EVM/SymExec.hs |  3 +++
 test/test.hs       |  6 +++++-
 4 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 13c927437..005b59e16 100644
--- a/CHANGELOG.md
+++ b/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
 
diff --git a/src/EVM.hs b/src/EVM.hs
index d53a7b754..4279fd273 100644
--- a/src/EVM.hs
+++ b/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 $
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 95db2849b..734c7ff5e 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -680,6 +680,7 @@ 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"
@@ -687,6 +688,8 @@ equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
     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
diff --git a/test/test.hs b/test/test.hs
index 3b1c60c6f..730cc9527 100644
--- a/test/test.hs
+++ b/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.