Merge pull request #620 from ethereum/overapproximate-staticcall

Overapproximate staticcall in case we can't resolve callee

Author: msooseth

CHANGELOG.md

@@ -6,6 +6,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ## Added
+- When a staticcall is made to a contract that does not exist, we overapproximate
+  and return symbolic values
+- More simplification rules for Props
 - JoinBytes simplification rule
 - New simplification rule to help deal with abi.encodeWithSelector
 - More simplification rules for Props

src/EVM.hs

@@ -165,6 +165,7 @@ makeVm o = do
     , currentFork = 0
     , labels = mempty
     , osEnv = mempty
+    , freshVar = 0
     }
     where
     env = Env
@@ -287,6 +288,17 @@ getOpW8 state = case state.code of
 getOpName :: forall (t :: VMType) s . FrameState t s -> [Char]
 getOpName state = intToOpName $ fromEnum $ getOpW8 state
 
+-- If the address is already in the cache, or can be obtained via API, return True
+-- otherwise, return False
+canFetchAccount :: forall (t :: VMType) s . VMOps t => Expr EAddr -> EVM t s (Bool)
+canFetchAccount addr = do
+  use (#env % #contracts % at addr) >>= \case
+    Just _ -> pure True
+    Nothing -> case addr of
+      LitAddr _ -> pure True
+      SymAddr _ -> pure False
+      GVar _ -> internalError "GVar not allowed here"
+
 -- | Executes the EVM one step
 exec1 :: forall (t :: VMType) s. VMOps t => EVM t s ()
 exec1 = do
@@ -982,26 +994,38 @@ exec1 = do
           case stk of
             xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs ->
               case wordToAddr xTo of
-                Nothing -> do
-                  loc <- codeloc
-                  let msg = "Unable to determine a call target"
-                  partial $ UnexpectedSymbolicArg (snd loc) opName msg [SomeExpr xTo]
-                Just xTo' ->
+                Nothing -> fallback
+                Just xTo' -> do
                   case gasTryFrom xGas of
                     Left _ -> vmError IllegalOverflow
-                    Right gas -> do
-                      overrideC <- use $ #state % #overrideCaller
-                      delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
-                        \callee -> do
-                          zoom #state $ do
-                            assign #callvalue (Lit 0)
-                            assign #caller $ fromMaybe self overrideC
-                            assign #contract callee
-                            assign #static True
-                          touchAccount self
-                          touchAccount callee
+                    Right gas -> canFetchAccount xTo' >>= \case
+                      False -> fallback
+                      True -> do
+                        overrideC <- use $ #state % #overrideCaller
+                        delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
+                          \callee -> do
+                            zoom #state $ do
+                              assign #callvalue (Lit 0)
+                              assign #caller $ fromMaybe self overrideC
+                              assign #contract callee
+                              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
 
         OpSelfdestruct ->
           notStatic $

src/EVM/Types.hs

@@ -670,6 +670,9 @@ data VM (t :: VMType) s = VM
   , currentFork    :: Int
   , labels         :: Map Addr Text
   , osEnv          :: Map String String
+  , freshVar       :: Int
+  -- ^ used to generate fresh symbolic variable names for overapproximations
+  --   during symbolic execution. See e.g. OpStaticcall
   }
   deriving (Generic)
 

test/test.hs

@@ -2060,10 +2060,197 @@ tests = testGroup "hevm"
           }
         }
         |]
-      let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256])
+      let sig = Just (Sig "checkval(uint8)" [AbiUIntType 8])
       (res, [Qed _]) <- withDefaultSolver $ \s ->
         checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
       putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+    , test "staticcall-check-orig" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        contract Target {
+            function add(uint256 x, uint256 y) external pure returns (uint256) {
+              unchecked {
+                return x + y;
+              }
+            }
+        }
+
+        contract C {
+            function checkval(uint256 x, uint256 y) public {
+                Target t = new Target();
+                address realAddr = address(t);
+                bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y);
+                (bool success, bytes memory returnData) = realAddr.staticcall(data);
+                assert(success);
+
+                uint result = abi.decode(returnData, (uint256));
+                uint expected;
+                unchecked {
+                  expected = x + y;
+                }
+                assert(result == expected);
+            }
+        }
+        |]
+      let sig = Just (Sig "checkval(uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of counterexamples" 0 numCexes
+      assertEqualM "number of errors" 0 numErrs
+      assertEqualM "number of qed-s" 1 numQeds
+    , test "staticcall-check-orig2" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        contract Target {
+            function add(uint256 x, uint256 y) external pure returns (uint256) {
+              assert(1 == 0);
+            }
+        }
+        contract C {
+            function checkval(uint256 x, uint256 y) public {
+                Target t = new Target();
+                address realAddr = address(t);
+                bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y);
+                (bool success, bytes memory returnData) = realAddr.staticcall(data);
+                assert(success);
+            }
+        }
+        |]
+      let sig = Just (Sig "checkval(uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      -- let cexesExt = map (snd . fromJust . extractCex) ret
+      -- putStrLnM $ "Cexes: \n" <> (unlines $ map ("-> " ++) (map show cexesExt))
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of counterexamples" 1 numCexes
+      assertEqualM "number of errors" 0 numErrs
+      assertEqualM "number of qed-s" 0 numQeds
+    , test "staticcall-check-symbolic1" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        contract C {
+            function checkval(address inputAddr, uint256 x, uint256 y) public {
+                bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y);
+                (bool success, bytes memory returnData) = inputAddr.staticcall(data);
+                assert(success);
+            }
+        }
+        |]
+      let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      -- There are 2 CEX-es, in contrast to the above (staticcall-check-orig2).
+      -- This is because with one CEX, the return DATA
+      -- is empty, and in the other, the return data is non-empty (but symbolic)
+      assertEqualM "number of counterexamples" 2 numCexes
+      assertEqualM "number of errors" 0 numErrs
+      assertEqualM "number of qed-s" 0 numQeds
+    -- This checks that calling a symbolic address with staticcall will ALWAYS return 0/1
+    -- which is the semantic of the EVM. We insert a  constraint over the return value
+    -- even when overapproximation is used, as below.
+    , test "staticcall-check-symbolic-yul" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        contract C {
+            function checkval(address inputAddr, uint256 x, uint256 y) public {
+            uint success;
+            assembly {
+              // Allocate memory for the call data
+              let callData := mload(0x40)
+
+              // Function signature for "add(uint256,uint256)" is "0x771602f7"
+              mstore(callData, 0x771602f700000000000000000000000000000000000000000000000000000000)
+
+              // Store the parameters x and y
+              mstore(add(callData, 4), x)
+              mstore(add(callData, 36), y)
+
+              // Perform the static call
+              success := staticcall(
+                  gas(),          // Forward all available gas
+                  inputAddr,      // Address to call
+                  callData,       // Input data location
+                  68,             // Input data size (4 bytes for function signature + 32 bytes each for x and y)
+                  0,              // Output data location (0 means we don't care about the output)
+                  0               // Output data size
+              )
+              }
+              assert(success <= 1);
+          }
+        }
+        |]
+      let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of counterexamples" 0 numCexes -- no counterexamples, because it is always  0/1
+      assertEqualM "number of errors" 0 numErrs
+      assertEqualM "number of qed-s" 1 numQeds
+    , test "staticcall-check-symbolic2" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        contract C {
+            function checkval(address inputAddr, uint256 x, uint256 y) public {
+                bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y);
+                (bool success, bytes memory returnData) = inputAddr.staticcall(data);
+                assert(success);
+
+                uint result = abi.decode(returnData, (uint256));
+                uint expected;
+                unchecked {
+                  expected = x + y;
+                }
+                assert(result == expected);
+            }
+        }
+        |]
+      let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of counterexamples" 2 numCexes
+      assertEqualM "number of errors" 1 numErrs
+      assertEqualM "number of qed-s" 0 numQeds
+     , test "jump-symbolic" $ do
+      Just c <- solcRuntime "C"
+        [i|
+        // Target contract with a view function
+        contract Target {
+        }
+
+        // Caller contract using staticcall
+        contract C {
+            function checkval(address inputAddr, uint256 x, uint256 y) public {
+                Target t = new Target();
+                address realAddr = address(t);
+
+                bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y);
+                (bool success, bytes memory returnData) = inputAddr.staticcall(data);
+                assert(success == true);
+            }
+        }
+        |]
+      let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
+      (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+      putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths"
+      let numCexes = sum $ map (fromEnum . isCex) ret
+      let numErrs = sum $ map (fromEnum . isError) ret
+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of counterexamples" numCexes 2
+      assertEqualM "number of symbolic copy errors" numErrs 0
+      assertEqualM "number of qed-s" numQeds 0
      ,
      test "opcode-mul-assoc" $ do
         Just c <- solcRuntime "MyContract"