Merge pull request #904 from argotorg/execution-refactor

EVM: Separate symbolic and concrete handling of SLOAD

Author: blishko

src/EVM.hs

@@ -727,13 +727,21 @@ exec1 conf = do
 
         OpSload -> {-# SCC "OpSload" #-}
           case stk of
-            x:xs -> do
-              acc <- accessStorageForGas self x
-              let cost = if acc then g_warm_storage_read else g_cold_sload
-              burn cost $
-                accessStorage self x $ \y -> do
-                  next
-                  assign' (#state % #stack) (y:xs)
+            x:xs ->
+              let
+                finalizeLoad readValue = do next; assign' (#state % #stack) (readValue:xs)
+
+                symbolicRead :: EVM t s () = if this.external
+                  then accessStorage self x finalizeLoad
+                  else finalizeLoad $ Expr.readStorage' (Expr.concKeccakOnePass x) this.storage
+
+                concreteRead :: EVM t s () = do
+                  acc <- accessStorageForGas self (forceLit x)
+                  let cost = if acc then g_warm_storage_read else g_cold_sload
+                  burn cost $ if this.external
+                    then accessStorage self x finalizeLoad
+                    else finalizeLoad $ Lit $ accessConcreteStorage this.storage (forceLit x)
+              in whenSymbolicElse symbolicRead concreteRead
             _ -> underrun
 
         OpSstore -> {-# SCC "OpSstore" #-}
@@ -748,12 +756,6 @@ exec1 conf = do
 
                 concreteSstore :: EVM t s () = do
                   let
-                    accessConcreteStorage :: Expr Storage -> W256 -> W256
-                    accessConcreteStorage storage slot' =
-                      case storage of
-                        (ConcreteStore m) -> fromMaybe 0 $ Map.lookup slot' m
-                        _ -> internalError "Storage must be concrete"
-
                     slot = forceLit x
                     currentVal = accessConcreteStorage this.storage slot
                     newVal = forceLit new
@@ -765,7 +767,7 @@ exec1 conf = do
                           | (currentVal == originalVal) = g_sreset
                           | otherwise = g_sload
 
-                    acc <- accessStorageForGas self x
+                    acc <- accessStorageForGas self slot
                     let cold_storage_cost = if acc then 0 else g_cold_sload
                     burn (storage_cost + cold_storage_cost) $ do
                       updateVMState
@@ -1412,6 +1414,12 @@ fetchAccountWithFallback addr fallback continue =
             continue c
       GVar _ -> internalError "Unexpected GVar"
 
+accessConcreteStorage :: Expr Storage -> W256 -> W256
+accessConcreteStorage storage slot' =
+  case storage of
+    (ConcreteStore m) -> fromMaybe 0 $ Map.lookup slot' m
+    _ -> internalError "Storage must be concrete"
+
 accessStorage :: forall s t . (?conf :: Config, VMOps t, Typeable t) => Expr EAddr
   -> Expr EWord
   -> (Expr EWord -> EVM t s ())
@@ -1746,15 +1754,12 @@ accessAccountForGas addr = do
 
 -- | returns a wrapped boolean- if true, this slot has been touched before in the txn (warm gas cost as in EIP 2929)
 -- otherwise cold
-accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool
+accessStorageForGas :: Expr EAddr -> W256 -> EVM t s Bool
 accessStorageForGas addr key = do
   accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys)
-  case maybeLitWordSimp key of
-    Just litword -> do
-      let accessed = member (addr, litword) accessedStrkeys
-      assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)
-      pure accessed
-    _ -> pure False
+  let accessed = member (addr, key) accessedStrkeys
+  unless accessed $ assign (#tx % #subState % #accessedStorageKeys) (insert (addr, key) accessedStrkeys)
+  pure accessed
 
 -- * Cheat codes