Merge pull request #588 from ethereum/fix-finalize

EVM: finalize: fix handling of symbolic returndata

CHANGELOG.md

@@ -55,6 +55,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Fixed bug in SMT encoding that caused empty and all-zero byte arrays to be considered equal
   and hence lead to false negatives through trivially UNSAT SMT expressions
 - Respect --smt-timeout in equivalence checking
+- Fixed the handling of returndata with an abstract size during transaction finalization
 
 ## [0.53.0] - 2024-02-23
 

src/EVM.hs

@@ -1504,19 +1504,18 @@ finalize = do
       creation <- use (#tx % #isCreate)
       createe  <- use (#state % #contract)
       createeExists <- (Map.member createe) <$> use (#env % #contracts)
-      let onContractCode contractCode =
-            when (creation && createeExists) $ replaceCode createe contractCode
-      case output of
-        ConcreteBuf bs ->
-          onContractCode $ RuntimeCode (ConcreteRuntimeCode bs)
-        _ ->
-          case Expr.toList output of
-            Nothing -> do
-              state <- use #state
-              partial $
-                UnexpectedSymbolicArg pc' (getOpName state) "runtime code cannot have an abstract length" (wrap [output])
-            Just ops ->
-              onContractCode $ RuntimeCode (SymbolicRuntimeCode ops)
+      when (creation && createeExists) $
+        case output of
+          ConcreteBuf bs ->
+            replaceCode createe (RuntimeCode (ConcreteRuntimeCode bs))
+          _ ->
+            case Expr.toList output of
+              Nothing -> do
+                state <- use #state
+                partial $
+                  UnexpectedSymbolicArg pc' (getOpName state) "runtime code cannot have an abstract length" (wrap [output])
+              Just ops ->
+                replaceCode createe (RuntimeCode (SymbolicRuntimeCode ops))
     _ ->
       internalError "Finalising an unfinished tx."
 

test/test.hs

@@ -1834,6 +1834,20 @@ tests = testGroup "hevm"
          |]
        (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c (Just (Sig "f(uint256)" [AbiUIntType 256])) [] defaultVeriOpts
        putStrLnM "this should always be true, due to bitwise OR with positive value"
+     ,
+     test "abstract-returndata-size" $ do
+       Just c <- solcRuntime "C"
+         [i|
+         contract C {
+           function f(uint256 x) public pure {
+             assembly {
+                 return(0, x)
+             }
+           }
+         }
+         |]
+       expr <- withSolvers Z3 1 Nothing $ \s -> getExpr s c (Just (Sig "f(uint256)" [])) [] defaultVeriOpts
+       assertBoolM "The expression is partial" $ not $ Expr.containsNode isPartial expr
     ,
     -- CopySlice check
     -- uses identity precompiled contract (0x4) to copy memory