Refactor RPC handling

cli/cli.hs

@@ -25,6 +25,7 @@ import Data.Text.IO qualified as T
 import Data.Version (showVersion)
 import Data.Word (Word64)
 import GHC.Conc (getNumProcessors)
+import GitHash
 import Numeric.Natural (Natural)
 import Optics.Core ((&), set)
 import Witch (unsafeInto)
@@ -43,7 +44,6 @@ import EVM.ABI (Sig(..))
 import EVM.Dapp (dappInfo, DappInfo, emptyDapp)
 import EVM.Expr qualified as Expr
 import EVM.Concrete qualified as Concrete
-import GitHash
 import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format (hexByteString, strip0x, formatExpr)
@@ -405,12 +405,11 @@ equivalence eqOpts cOpts = do
   when (isNothing bytecodeB) $ liftIO $ do
     putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
     exitFailure
-  let veriOpts = VeriOpts { iterConf = IterConfig {
+  let veriOpts = defaultVeriOpts { iterConf = IterConfig {
                             maxIter = parseMaxIters cOpts.maxIterations
                             , askSmtIters = cOpts.askSmtIterations
                             , loopHeuristic = cOpts.loopDetectionHeuristic
                             }
-                          , rpcInfo = mempty
                           }
   calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
   solver <- liftIO $ getSolver cOpts.solver
@@ -520,7 +519,7 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = do
                               , askSmtIters = cOpts.askSmtIterations
                               , loopHeuristic = cOpts.loopDetectionHeuristic
                               }
-                            , rpcInfo = mempty {Fetch.blockNumURL = blockUrlInfo}
+                            , rpcInfo = Fetch.RpcInfo blockUrlInfo
                             }
     let fetcher = Fetch.oracle solvers (Just sess) veriOpts.rpcInfo
     (expr, res) <- verify solvers fetcher veriOpts preState (checkAssertions errCodes)
@@ -576,7 +575,7 @@ launchExec cFileOpts execOpts cExecOpts cOpts = do
   let
     block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
     blockUrlInfo = (,) block <$> cExecOpts.rpc
-    rpcDat :: Fetch.RpcInfo = mempty { Fetch.blockNumURL = blockUrlInfo }
+    rpcDat :: Fetch.RpcInfo = Fetch.RpcInfo blockUrlInfo
 
   -- TODO: we shouldn't need solvers to execute this code
   withSolvers Z3 0 1 Nothing $ \solvers -> do
@@ -841,7 +840,7 @@ unitTestOptions testOpts cOpts solvers buildOutput = do
           (Just block, Just url) -> Just (Fetch.BlockNumber block, url)
           (Nothing, Just url) -> Just (Fetch.Latest, url)
           _ -> Nothing
-      rpcDat = Fetch.mkRpcInfo blockUrlInfo
+      rpcDat = Fetch.RpcInfo blockUrlInfo
   sess <- Fetch.mkSession cOpts.cacheDir testOpts.number
   params <- paramsFromRpc rpcDat sess
   let testn = params.number

src/EVM/Fetch.hs

@@ -8,8 +8,9 @@ module EVM.Fetch
   , RpcInfo (..)
   , RpcQuery (..)
   , EVM.Fetch.zero
+  , noRpc
+  , noRpcFetcher
   , BlockNumber (..)
-  , mkRpcInfo
   , mkSession
   , mkSessionWithoutCache
   , Session (..)
@@ -46,15 +47,14 @@ import Data.Bifunctor (first)
 import Control.Exception (try, SomeException)
 
 import Control.Monad.Trans.Maybe
-import Control.Applicative (Alternative(..))
 import Data.Aeson hiding (Error)
 import Data.Aeson.Optics
 import Data.ByteString qualified as BS
 import Data.Text (Text, unpack, pack)
 import Data.Text qualified as T
 import Data.Foldable (Foldable(..))
 import Data.Map.Strict qualified as Map
-import Data.Maybe (fromMaybe, isJust, fromJust)
+import Data.Maybe (fromMaybe, isJust, fromJust, isNothing)
 import Data.Vector qualified as RegularVector
 import Network.Wreq
 import Network.Wreq.Session qualified as NetSession
@@ -137,18 +137,11 @@ instance ToJSON RPCContract
 
 instance FromJSON RPCContract
 
-data RpcInfo = RpcInfo
-  { blockNumURL  :: Maybe (BlockNumber, Text) -- ^ (block number, RPC url)
-  }
+newtype RpcInfo = RpcInfo { blockNumURL  :: Maybe (BlockNumber, Text)} -- ^ (block number, RPC url)
   deriving (Show)
-instance Semigroup RpcInfo where
-  RpcInfo a1 <> RpcInfo b1 =
-    RpcInfo (a1 <|> b1)
-instance Monoid RpcInfo where
-  mempty = RpcInfo Nothing
 
-mkRpcInfo :: Maybe (BlockNumber, Text) -> RpcInfo
-mkRpcInfo blockNumURL = RpcInfo blockNumURL
+noRpc :: RpcInfo
+noRpc = RpcInfo Nothing
 
 rpc :: String -> [Value] -> Value
 rpc method args = object
@@ -422,7 +415,10 @@ zero :: Natural -> Maybe Natural -> Fetcher t m
 zero smtjobs smttimeout q = do
   sess <- mkSessionWithoutCache
   withSolvers Z3 smtjobs 1 smttimeout $ \s ->
-    oracle s (Just sess) mempty q
+    oracle s (Just sess) noRpc q
+
+noRpcFetcher :: forall t m . App m => SolverGroup -> Fetcher t m
+noRpcFetcher sg = oracle sg Nothing noRpc
 
 -- SMT solving + RPC data fetching + reading from environment
 oracle :: forall t m . App m => SolverGroup -> Maybe Session -> RpcInfo -> Fetcher t m
@@ -450,65 +446,60 @@ oracle solvers preSess rpcInfo q = do
          let pathconds = foldl' PAnd (PBool True) pathconditions
          continue <$> getSolutions solvers symExpr numBytes pathconds
 
-    PleaseFetchContract addr base continue -> withSession addr (continue (nothingContract base addr)) $ \sess -> do
-      conf <- readConfig
-      cache <- liftIO $ readMVar sess.sharedCache
-      case Map.lookup addr cache.contractCache of
-        Just c -> do
-          when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached contract at " ++ show addr
-          pure $ continue $ makeContractFromRPC c
-        Nothing -> do
-          when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
-          contract <- case rpcInfo.blockNumURL of
-            Nothing -> do
-              liftIO $ putStrLn $ "Warning: no RPC info provided, returning empty contract for address: " <> show addr
-              pure $ Just $ nothingContract base addr
-            Just (block, url) -> liftIO $ fmap (fmap makeContractFromRPC) $ fetchContractWithSession conf sess block url addr
-          case contract of
-            Just x -> pure $ continue x
-            Nothing -> internalError $ "oracle error: " ++ show q
-
-    PleaseFetchSlot addr slot continue -> withSession addr (continue 0)$ \sess -> do
-      conf <- readConfig
-      cache <- liftIO $ readMVar sess.sharedCache
-      case Map.lookup (addr, slot) cache.slotCache of
-        Just s -> do
-          when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached slot value for slot " <> show slot <> " at " <> show addr
-          pure $ continue s
-        Nothing -> do
-          when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
-          case rpcInfo.blockNumURL of
-            Nothing -> do
-              liftIO $ putStrLn $ "Warning: no RPC info provided, returning 0 for slot at address: " <> show addr
-              pure $ continue 0
-            Just (block, url) -> do
-              n <- liftIO $ getLatestBlockNum conf sess block url
-              ret <- liftIO $ fetchSlotWithSession sess.sess n url addr slot
-              when (isJust ret) $ let val = fromJust ret in
-                liftIO $ modifyMVar_ sess.sharedCache $ \c ->
-                  pure $ c { slotCache = Map.insert (addr, slot) val c.slotCache }
-              case ret of
-                Just x  -> pure $ continue x
-                Nothing -> internalError $ "oracle error: " ++ show q
+    PleaseFetchContract addr base continue
+      | isAddressSpecial addr -> pure $ continue nothingContract
+      | isNothing rpcInfo.blockNumURL -> pure $ continue nothingContract
+      | otherwise -> do
+        let sess = fromMaybe (internalError $ "oracle: no session provided for fetch addr: " ++ show addr) preSess
+        conf <- readConfig
+        cache <- liftIO $ readMVar sess.sharedCache
+        case Map.lookup addr cache.contractCache of
+          Just c -> do
+            when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached contract at " ++ show addr
+            pure $ continue $ makeContractFromRPC c
+          Nothing -> do
+            when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
+            let (block, url) = fromJust rpcInfo.blockNumURL
+            contract <- liftIO $ fmap (fmap makeContractFromRPC) $ fetchContractWithSession conf sess block url addr
+            case contract of
+              Just x -> pure $ continue x
+              Nothing -> internalError $ "oracle error: " ++ show q
+      where
+        nothingContract = case base of
+          AbstractBase -> unknownContract (LitAddr addr)
+          EmptyBase -> emptyContract
+
+    PleaseFetchSlot addr slot continue
+      | isAddressSpecial addr -> pure $ continue 0
+      | isNothing rpcInfo.blockNumURL -> pure $ continue 0
+      | otherwise -> do
+        let sess = fromMaybe (internalError $ "oracle: no session provided for fetch addr: " ++ show addr) preSess
+        conf <- readConfig
+        cache <- liftIO $ readMVar sess.sharedCache
+        case Map.lookup (addr, slot) cache.slotCache of
+          Just s -> do
+            when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached slot value for slot " <> show slot <> " at " <> show addr
+            pure $ continue s
+          Nothing -> do
+            when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
+            let (block, url) = fromJust rpcInfo.blockNumURL
+            n <- liftIO $ getLatestBlockNum conf sess block url
+            ret <- liftIO $ fetchSlotWithSession sess.sess n url addr slot
+            when (isJust ret) $ let val = fromJust ret in
+              liftIO $ modifyMVar_ sess.sharedCache $ \c ->
+                pure $ c { slotCache = Map.insert (addr, slot) val c.slotCache }
+            case ret of
+              Just x  -> pure $ continue x
+              Nothing -> internalError $ "oracle error: " ++ show q
 
     PleaseReadEnv variable continue -> do
       value <- liftIO $ lookupEnv variable
       pure . continue $ fromMaybe "" value
 
     where
-      nothingContract base addr =
-        case base of
-          AbstractBase -> unknownContract (LitAddr addr)
-          EmptyBase -> emptyContract
-      withSession addr def f =
-        case addr of
-          -- special values such as 0, 0xdeadbeef, 0xacab, hevm cheatcodes, and the precompile addresses
-          -- do not require a session, there is nothing deployed there, it's way too small or special, RPC would be pointless
-          a | a <= 0xdeadbeef -> pure def
-          0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> pure def
-          _ -> case preSess of
-            Just sess  -> f sess
-            Nothing -> internalError $ "oracle: no session provided for fetch addr: " ++ show addr
+      -- special values such as 0, 0xdeadbeef, 0xacab, hevm cheatcodes, and the precompile addresses
+      isAddressSpecial addr = addr <= 0xdeadbeef || addr == 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D  
+
 
 getSolutions :: forall m . App m => SolverGroup -> Expr EWord -> Int -> Prop -> m (Maybe [W256])
 getSolutions solvers symExprPreSimp numBytes pathconditions = do

src/EVM/SymExec.hs

@@ -105,12 +105,9 @@ data VeriOpts = VeriOpts
 defaultVeriOpts :: VeriOpts
 defaultVeriOpts = VeriOpts
   { iterConf = defaultIterConf
-  , rpcInfo = mempty
+  , rpcInfo = Fetch.noRpc
   }
 
-rpcVeriOpts :: (Fetch.BlockNumber, Text) -> VeriOpts
-rpcVeriOpts info = defaultVeriOpts { rpcInfo  = mempty { Fetch.blockNumURL = Just info }}
-
 extractCex :: VerifyResult -> Maybe (Expr End, SMTCex)
 extractCex (Cex c) = Just c
 extractCex _ = Nothing
@@ -840,7 +837,7 @@ equivalenceCheck solvers sess bytecodeA bytecodeB opts calldata create = do
       conf <- readConfig
       let bytecode = if BS.null bs then BS.pack [0] else bs
       prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create
-      expr <- interpret (Fetch.oracle solvers sess mempty) opts.iterConf prestate runExpr
+      expr <- interpret (Fetch.oracle solvers sess Fetch.noRpc) opts.iterConf prestate runExpr
       let simpl = if conf.simp then Expr.simplify expr else expr
       pure $ flattenExpr simpl
     oneQedOrNoQed :: EqIssues -> EqIssues

test/EVM/Test/BlockchainTests.hs

@@ -99,17 +99,16 @@ prepareTests = do
   rootDir <- liftIO rootDirectory
   liftIO $ putStrLn $ "Loading and parsing json files from ethereum-tests from " <> show rootDir
   cases <- liftIO allTestCases
-  session <- EVM.Fetch.mkSessionWithoutCache
-  groups <- forM (Map.toList cases) (\(f, subtests) -> testGroup (makeRelative rootDir f) <$> (process subtests session))
+  groups <- forM (Map.toList cases) (\(f, subtests) -> testGroup (makeRelative rootDir f) <$> (process subtests))
   liftIO $ putStrLn "Loaded."
   pure $ testGroup "ethereum-tests" groups
   where
-    process :: forall m . App m => (Map String Case) -> EVM.Fetch.Session -> m [TestTree]
-    process tests session = forM (Map.toList tests) $ runTest session
+    process :: forall m . App m => (Map String Case) -> m [TestTree]
+    process tests = forM (Map.toList tests) runTest
 
-    runTest :: App m => EVM.Fetch.Session -> (String, Case) -> m TestTree
-    runTest session (name, x) = do
-      let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.oracle s (Just session) mempty q
+    runTest :: App m => (String, Case) -> m TestTree
+    runTest (name, x) = do
+      let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.noRpcFetcher s q
       exec <- toIO $ runVMTest fetcher x
       pure $ testCase' name exec
     testCase' :: String -> Assertion -> TestTree

test/EVM/Test/FuzzSymExec.hs

@@ -13,6 +13,7 @@ concretely through Expr.simplify, then check that against evmtool's output.
 module EVM.Test.FuzzSymExec where
 
 import Control.Monad (when)
+import Control.Monad.IO.Unlift
 import Control.Monad.ST (ST, stToIO, RealWorld)
 import Control.Monad.State.Strict (StateT(..))
 import Control.Monad.Reader (ReaderT)
@@ -29,6 +30,7 @@ import Data.Word (Word8, Word64)
 import GHC.Generics (Generic)
 import GHC.IO.Exception (ExitCode(ExitSuccess))
 import Numeric (showHex)
+import Optics.Core hiding (pre)
 import System.Directory (removeDirectoryRecursive)
 import System.FilePath ((</>))
 import System.IO.Temp (getCanonicalTemporaryDirectory, createTempDirectory)
@@ -42,8 +44,6 @@ import Test.Tasty.HUnit (assertEqual, testCase)
 import Test.Tasty.QuickCheck hiding (Failure, Success)
 import Witch (into, unsafeInto)
 
-import Optics.Core hiding (pre)
-
 import EVM (makeVm, initialContract, symbolify)
 import EVM.Assembler (assemble)
 import EVM.Expr qualified as Expr
@@ -60,7 +60,6 @@ import EVM.Traversals (mapExpr)
 import EVM.Transaction qualified
 import EVM.Types hiding (Env)
 import EVM.Effects
-import Control.Monad.IO.Unlift
 import EVM.Tracing (interpretWithTrace, VMTraceStep(..), VMTraceStepResult(..))
 
 data EVMToolTrace =
@@ -283,7 +282,7 @@ getHEVMRet
   => OpContract -> ByteString -> Int -> m (Either (EvmError, [VMTraceStep]) (Expr 'End, [VMTraceStep], VMTraceStepResult))
 getHEVMRet contr txData gaslimitExec = do
   let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec
-  runCodeWithTrace mempty evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
+  runCodeWithTrace Fetch.noRpc evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
 
 getEVMToolRet :: FilePath -> OpContract -> ByteString -> Int -> IO (Maybe EVMToolResult)
 getEVMToolRet evmDir contr txData gaslimitExec = do

test/EVM/Test/Utils.hs

@@ -23,7 +23,7 @@ import EVM.Effects
 import Data.Maybe (fromMaybe)
 import EVM.Types (internalError)
 import System.Environment (lookupEnv)
-import EVM.Fetch (RpcInfo)
+import EVM.Fetch (RpcInfo, noRpc)
 import EVM.Fetch qualified as Fetch
 
 -- Returns tuple of (No cex, No warnings)
@@ -46,7 +46,7 @@ runForgeTestCustom testFile match timeout maxIter ffiAllowed rpcinfo = do
 runForgeTest
   :: (MonadMask m, App m)
   => FilePath -> Text -> m (Bool, Bool)
-runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True mempty
+runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True noRpc
 
 testOpts :: forall m . App m => SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> m (UnitTestOptions)
 testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do

test/clitest.hs

@@ -246,49 +246,4 @@ main = do
           ["--rpc", "http://mock.mock", "--prefix", "test_attack_symbolic"
           , "--number", "10307563", "--cache-dir", "test/contracts/fail/"]
         stdout `shouldContain` "[FAIL]"
-        stderr `shouldNotContain` "CallStack"
-      it "nowarn-rpc-empty-precompile-symbolic" $ do
-        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
-          contract C {
-            function computeHash() public view {
-                bytes memory data = hex"68656c6c6f";
-                (bool success,) = address(2).staticcall(data); //SHA precompile
-                assert(success);
-            }
-          }
-         |])
-        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", Types.bsToHex c] ""
-        stdout `shouldNotContain` "Warning: no RPC info provided"
-      it "warn-rpc-empty-unknown-addr-symbolic" $ do
-        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
-          contract C {
-            function computeHash() public view {
-                bytes memory data = hex"68656c6c6f";
-                (bool success,) = address(878492734777777).staticcall(data);
-                assert(success);
-            }
-          }
-         |])
-        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", Types.bsToHex c] ""
-        stdout `shouldContain` "Warning: no RPC info provided"
-      it "warn-rpc-empty-unknown-addr-equiv" $ do
-        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
-          contract C {
-            function computeHash() public view {
-                bytes memory data = hex"68656c6c6f";
-                (bool success,) = address(8492734777777).staticcall(data);
-                assert(success);
-            }
-          }
-         |])
-        Just c2 <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
-          contract C {
-            function computeHash() public view {
-                bytes memory data = hex"68656c6c6f";
-                (bool success,) = address(923741898892).staticcall(data);
-                assert(success);
-            }
-          }
-         |])
-        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "equivalence", "--code-a", Types.bsToHex c, "--code-b", Types.bsToHex c2] ""
-        stdout `shouldContain` "Warning: no RPC info provided"
+        stderr `shouldNotContain` "CallStack"