Skip to content

Commit 71c8753

Browse files
authored
Merge pull request #925 from argotorg/rpc-refactor
Refactor RPC handling
2 parents d6e6e05 + 44c0dc9 commit 71c8753

File tree

9 files changed

+97
-160
lines changed

9 files changed

+97
-160
lines changed

cli/cli.hs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ import Data.Text.IO qualified as T
2525
import Data.Version (showVersion)
2626
import Data.Word (Word64)
2727
import GHC.Conc (getNumProcessors)
28+
import GitHash
2829
import Numeric.Natural (Natural)
2930
import Optics.Core ((&), set)
3031
import Witch (unsafeInto)
@@ -43,7 +44,6 @@ import EVM.ABI (Sig(..))
4344
import EVM.Dapp (dappInfo, DappInfo, emptyDapp)
4445
import EVM.Expr qualified as Expr
4546
import EVM.Concrete qualified as Concrete
46-
import GitHash
4747
import EVM.FeeSchedule (feeSchedule)
4848
import EVM.Fetch qualified as Fetch
4949
import EVM.Format (hexByteString, strip0x, formatExpr)
@@ -405,12 +405,11 @@ equivalence eqOpts cOpts = do
405405
when (isNothing bytecodeB) $ liftIO $ do
406406
putStrLn "Error: invalid or no bytecode for program B. Provide a valid one with --code-b or --code-b-file"
407407
exitFailure
408-
let veriOpts = VeriOpts { iterConf = IterConfig {
408+
let veriOpts = defaultVeriOpts { iterConf = IterConfig {
409409
maxIter = parseMaxIters cOpts.maxIterations
410410
, askSmtIters = cOpts.askSmtIterations
411411
, loopHeuristic = cOpts.loopDetectionHeuristic
412412
}
413-
, rpcInfo = mempty
414413
}
415414
calldata <- buildCalldata cOpts eqOpts.sig eqOpts.arg
416415
solver <- liftIO $ getSolver cOpts.solver
@@ -520,7 +519,7 @@ symbCheck cFileOpts sOpts cExecOpts cOpts = do
520519
, askSmtIters = cOpts.askSmtIterations
521520
, loopHeuristic = cOpts.loopDetectionHeuristic
522521
}
523-
, rpcInfo = mempty {Fetch.blockNumURL = blockUrlInfo}
522+
, rpcInfo = Fetch.RpcInfo blockUrlInfo
524523
}
525524
let fetcher = Fetch.oracle solvers (Just sess) veriOpts.rpcInfo
526525
(expr, res) <- verify solvers fetcher veriOpts preState (checkAssertions errCodes)
@@ -576,7 +575,7 @@ launchExec cFileOpts execOpts cExecOpts cOpts = do
576575
let
577576
block = maybe Fetch.Latest Fetch.BlockNumber cExecOpts.block
578577
blockUrlInfo = (,) block <$> cExecOpts.rpc
579-
rpcDat :: Fetch.RpcInfo = mempty { Fetch.blockNumURL = blockUrlInfo }
578+
rpcDat :: Fetch.RpcInfo = Fetch.RpcInfo blockUrlInfo
580579

581580
-- TODO: we shouldn't need solvers to execute this code
582581
withSolvers Z3 0 1 Nothing $ \solvers -> do
@@ -841,7 +840,7 @@ unitTestOptions testOpts cOpts solvers buildOutput = do
841840
(Just block, Just url) -> Just (Fetch.BlockNumber block, url)
842841
(Nothing, Just url) -> Just (Fetch.Latest, url)
843842
_ -> Nothing
844-
rpcDat = Fetch.mkRpcInfo blockUrlInfo
843+
rpcDat = Fetch.RpcInfo blockUrlInfo
845844
sess <- Fetch.mkSession cOpts.cacheDir testOpts.number
846845
params <- paramsFromRpc rpcDat sess
847846
let testn = params.number

src/EVM/Fetch.hs

Lines changed: 58 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,9 @@ module EVM.Fetch
88
, RpcInfo (..)
99
, RpcQuery (..)
1010
, EVM.Fetch.zero
11+
, noRpc
12+
, noRpcFetcher
1113
, BlockNumber (..)
12-
, mkRpcInfo
1314
, mkSession
1415
, mkSessionWithoutCache
1516
, Session (..)
@@ -46,15 +47,14 @@ import Data.Bifunctor (first)
4647
import Control.Exception (try, SomeException)
4748

4849
import Control.Monad.Trans.Maybe
49-
import Control.Applicative (Alternative(..))
5050
import Data.Aeson hiding (Error)
5151
import Data.Aeson.Optics
5252
import Data.ByteString qualified as BS
5353
import Data.Text (Text, unpack, pack)
5454
import Data.Text qualified as T
5555
import Data.Foldable (Foldable(..))
5656
import Data.Map.Strict qualified as Map
57-
import Data.Maybe (fromMaybe, isJust, fromJust)
57+
import Data.Maybe (fromMaybe, isJust, fromJust, isNothing)
5858
import Data.Vector qualified as RegularVector
5959
import Network.Wreq
6060
import Network.Wreq.Session qualified as NetSession
@@ -137,18 +137,11 @@ instance ToJSON RPCContract
137137

138138
instance FromJSON RPCContract
139139

140-
data RpcInfo = RpcInfo
141-
{ blockNumURL :: Maybe (BlockNumber, Text) -- ^ (block number, RPC url)
142-
}
140+
newtype RpcInfo = RpcInfo { blockNumURL :: Maybe (BlockNumber, Text)} -- ^ (block number, RPC url)
143141
deriving (Show)
144-
instance Semigroup RpcInfo where
145-
RpcInfo a1 <> RpcInfo b1 =
146-
RpcInfo (a1 <|> b1)
147-
instance Monoid RpcInfo where
148-
mempty = RpcInfo Nothing
149142

150-
mkRpcInfo :: Maybe (BlockNumber, Text) -> RpcInfo
151-
mkRpcInfo blockNumURL = RpcInfo blockNumURL
143+
noRpc :: RpcInfo
144+
noRpc = RpcInfo Nothing
152145

153146
rpc :: String -> [Value] -> Value
154147
rpc method args = object
@@ -422,7 +415,10 @@ zero :: Natural -> Maybe Natural -> Fetcher t m
422415
zero smtjobs smttimeout q = do
423416
sess <- mkSessionWithoutCache
424417
withSolvers Z3 smtjobs 1 smttimeout $ \s ->
425-
oracle s (Just sess) mempty q
418+
oracle s (Just sess) noRpc q
419+
420+
noRpcFetcher :: forall t m . App m => SolverGroup -> Fetcher t m
421+
noRpcFetcher sg = oracle sg Nothing noRpc
426422

427423
-- SMT solving + RPC data fetching + reading from environment
428424
oracle :: forall t m . App m => SolverGroup -> Maybe Session -> RpcInfo -> Fetcher t m
@@ -450,65 +446,60 @@ oracle solvers preSess rpcInfo q = do
450446
let pathconds = foldl' PAnd (PBool True) pathconditions
451447
continue <$> getSolutions solvers symExpr numBytes pathconds
452448

453-
PleaseFetchContract addr base continue -> withSession addr (continue (nothingContract base addr)) $ \sess -> do
454-
conf <- readConfig
455-
cache <- liftIO $ readMVar sess.sharedCache
456-
case Map.lookup addr cache.contractCache of
457-
Just c -> do
458-
when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached contract at " ++ show addr
459-
pure $ continue $ makeContractFromRPC c
460-
Nothing -> do
461-
when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
462-
contract <- case rpcInfo.blockNumURL of
463-
Nothing -> do
464-
liftIO $ putStrLn $ "Warning: no RPC info provided, returning empty contract for address: " <> show addr
465-
pure $ Just $ nothingContract base addr
466-
Just (block, url) -> liftIO $ fmap (fmap makeContractFromRPC) $ fetchContractWithSession conf sess block url addr
467-
case contract of
468-
Just x -> pure $ continue x
469-
Nothing -> internalError $ "oracle error: " ++ show q
470-
471-
PleaseFetchSlot addr slot continue -> withSession addr (continue 0)$ \sess -> do
472-
conf <- readConfig
473-
cache <- liftIO $ readMVar sess.sharedCache
474-
case Map.lookup (addr, slot) cache.slotCache of
475-
Just s -> do
476-
when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached slot value for slot " <> show slot <> " at " <> show addr
477-
pure $ continue s
478-
Nothing -> do
479-
when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
480-
case rpcInfo.blockNumURL of
481-
Nothing -> do
482-
liftIO $ putStrLn $ "Warning: no RPC info provided, returning 0 for slot at address: " <> show addr
483-
pure $ continue 0
484-
Just (block, url) -> do
485-
n <- liftIO $ getLatestBlockNum conf sess block url
486-
ret <- liftIO $ fetchSlotWithSession sess.sess n url addr slot
487-
when (isJust ret) $ let val = fromJust ret in
488-
liftIO $ modifyMVar_ sess.sharedCache $ \c ->
489-
pure $ c { slotCache = Map.insert (addr, slot) val c.slotCache }
490-
case ret of
491-
Just x -> pure $ continue x
492-
Nothing -> internalError $ "oracle error: " ++ show q
449+
PleaseFetchContract addr base continue
450+
| isAddressSpecial addr -> pure $ continue nothingContract
451+
| isNothing rpcInfo.blockNumURL -> pure $ continue nothingContract
452+
| otherwise -> do
453+
let sess = fromMaybe (internalError $ "oracle: no session provided for fetch addr: " ++ show addr) preSess
454+
conf <- readConfig
455+
cache <- liftIO $ readMVar sess.sharedCache
456+
case Map.lookup addr cache.contractCache of
457+
Just c -> do
458+
when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached contract at " ++ show addr
459+
pure $ continue $ makeContractFromRPC c
460+
Nothing -> do
461+
when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
462+
let (block, url) = fromJust rpcInfo.blockNumURL
463+
contract <- liftIO $ fmap (fmap makeContractFromRPC) $ fetchContractWithSession conf sess block url addr
464+
case contract of
465+
Just x -> pure $ continue x
466+
Nothing -> internalError $ "oracle error: " ++ show q
467+
where
468+
nothingContract = case base of
469+
AbstractBase -> unknownContract (LitAddr addr)
470+
EmptyBase -> emptyContract
471+
472+
PleaseFetchSlot addr slot continue
473+
| isAddressSpecial addr -> pure $ continue 0
474+
| isNothing rpcInfo.blockNumURL -> pure $ continue 0
475+
| otherwise -> do
476+
let sess = fromMaybe (internalError $ "oracle: no session provided for fetch addr: " ++ show addr) preSess
477+
conf <- readConfig
478+
cache <- liftIO $ readMVar sess.sharedCache
479+
case Map.lookup (addr, slot) cache.slotCache of
480+
Just s -> do
481+
when (conf.debug) $ liftIO $ putStrLn $ "-> Using cached slot value for slot " <> show slot <> " at " <> show addr
482+
pure $ continue s
483+
Nothing -> do
484+
when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
485+
let (block, url) = fromJust rpcInfo.blockNumURL
486+
n <- liftIO $ getLatestBlockNum conf sess block url
487+
ret <- liftIO $ fetchSlotWithSession sess.sess n url addr slot
488+
when (isJust ret) $ let val = fromJust ret in
489+
liftIO $ modifyMVar_ sess.sharedCache $ \c ->
490+
pure $ c { slotCache = Map.insert (addr, slot) val c.slotCache }
491+
case ret of
492+
Just x -> pure $ continue x
493+
Nothing -> internalError $ "oracle error: " ++ show q
493494

494495
PleaseReadEnv variable continue -> do
495496
value <- liftIO $ lookupEnv variable
496497
pure . continue $ fromMaybe "" value
497498

498499
where
499-
nothingContract base addr =
500-
case base of
501-
AbstractBase -> unknownContract (LitAddr addr)
502-
EmptyBase -> emptyContract
503-
withSession addr def f =
504-
case addr of
505-
-- special values such as 0, 0xdeadbeef, 0xacab, hevm cheatcodes, and the precompile addresses
506-
-- do not require a session, there is nothing deployed there, it's way too small or special, RPC would be pointless
507-
a | a <= 0xdeadbeef -> pure def
508-
0x7109709ECfa91a80626fF3989D68f67F5b1DD12D -> pure def
509-
_ -> case preSess of
510-
Just sess -> f sess
511-
Nothing -> internalError $ "oracle: no session provided for fetch addr: " ++ show addr
500+
-- special values such as 0, 0xdeadbeef, 0xacab, hevm cheatcodes, and the precompile addresses
501+
isAddressSpecial addr = addr <= 0xdeadbeef || addr == 0x7109709ECfa91a80626fF3989D68f67F5b1DD12D
502+
512503

513504
getSolutions :: forall m . App m => SolverGroup -> Expr EWord -> Int -> Prop -> m (Maybe [W256])
514505
getSolutions solvers symExprPreSimp numBytes pathconditions = do

src/EVM/SymExec.hs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -105,12 +105,9 @@ data VeriOpts = VeriOpts
105105
defaultVeriOpts :: VeriOpts
106106
defaultVeriOpts = VeriOpts
107107
{ iterConf = defaultIterConf
108-
, rpcInfo = mempty
108+
, rpcInfo = Fetch.noRpc
109109
}
110110

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

test/EVM/Test/BlockchainTests.hs

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -99,17 +99,16 @@ prepareTests = do
9999
rootDir <- liftIO rootDirectory
100100
liftIO $ putStrLn $ "Loading and parsing json files from ethereum-tests from " <> show rootDir
101101
cases <- liftIO allTestCases
102-
session <- EVM.Fetch.mkSessionWithoutCache
103-
groups <- forM (Map.toList cases) (\(f, subtests) -> testGroup (makeRelative rootDir f) <$> (process subtests session))
102+
groups <- forM (Map.toList cases) (\(f, subtests) -> testGroup (makeRelative rootDir f) <$> (process subtests))
104103
liftIO $ putStrLn "Loaded."
105104
pure $ testGroup "ethereum-tests" groups
106105
where
107-
process :: forall m . App m => (Map String Case) -> EVM.Fetch.Session -> m [TestTree]
108-
process tests session = forM (Map.toList tests) $ runTest session
106+
process :: forall m . App m => (Map String Case) -> m [TestTree]
107+
process tests = forM (Map.toList tests) runTest
109108

110-
runTest :: App m => EVM.Fetch.Session -> (String, Case) -> m TestTree
111-
runTest session (name, x) = do
112-
let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.oracle s (Just session) mempty q
109+
runTest :: App m => (String, Case) -> m TestTree
110+
runTest (name, x) = do
111+
let fetcher q = withSolvers Z3 0 1 (Just 0) $ \s -> EVM.Fetch.noRpcFetcher s q
113112
exec <- toIO $ runVMTest fetcher x
114113
pure $ testCase' name exec
115114
testCase' :: String -> Assertion -> TestTree

test/EVM/Test/FuzzSymExec.hs

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ concretely through Expr.simplify, then check that against evmtool's output.
1313
module EVM.Test.FuzzSymExec where
1414

1515
import Control.Monad (when)
16+
import Control.Monad.IO.Unlift
1617
import Control.Monad.ST (ST, stToIO, RealWorld)
1718
import Control.Monad.State.Strict (StateT(..))
1819
import Control.Monad.Reader (ReaderT)
@@ -29,6 +30,7 @@ import Data.Word (Word8, Word64)
2930
import GHC.Generics (Generic)
3031
import GHC.IO.Exception (ExitCode(ExitSuccess))
3132
import Numeric (showHex)
33+
import Optics.Core hiding (pre)
3234
import System.Directory (removeDirectoryRecursive)
3335
import System.FilePath ((</>))
3436
import System.IO.Temp (getCanonicalTemporaryDirectory, createTempDirectory)
@@ -42,8 +44,6 @@ import Test.Tasty.HUnit (assertEqual, testCase)
4244
import Test.Tasty.QuickCheck hiding (Failure, Success)
4345
import Witch (into, unsafeInto)
4446

45-
import Optics.Core hiding (pre)
46-
4747
import EVM (makeVm, initialContract, symbolify)
4848
import EVM.Assembler (assemble)
4949
import EVM.Expr qualified as Expr
@@ -60,7 +60,6 @@ import EVM.Traversals (mapExpr)
6060
import EVM.Transaction qualified
6161
import EVM.Types hiding (Env)
6262
import EVM.Effects
63-
import Control.Monad.IO.Unlift
6463
import EVM.Tracing (interpretWithTrace, VMTraceStep(..), VMTraceStepResult(..))
6564

6665
data EVMToolTrace =
@@ -283,7 +282,7 @@ getHEVMRet
283282
=> OpContract -> ByteString -> Int -> m (Either (EvmError, [VMTraceStep]) (Expr 'End, [VMTraceStep], VMTraceStepResult))
284283
getHEVMRet contr txData gaslimitExec = do
285284
let (txn, evmEnv, contrAlloc, fromAddress, toAddress, _) = evmSetup contr txData gaslimitExec
286-
runCodeWithTrace mempty evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
285+
runCodeWithTrace Fetch.noRpc evmEnv contrAlloc txn (LitAddr fromAddress) (LitAddr toAddress)
287286

288287
getEVMToolRet :: FilePath -> OpContract -> ByteString -> Int -> IO (Maybe EVMToolResult)
289288
getEVMToolRet evmDir contr txData gaslimitExec = do

test/EVM/Test/Utils.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ import EVM.Effects
2323
import Data.Maybe (fromMaybe)
2424
import EVM.Types (internalError)
2525
import System.Environment (lookupEnv)
26-
import EVM.Fetch (RpcInfo)
26+
import EVM.Fetch (RpcInfo, noRpc)
2727
import EVM.Fetch qualified as Fetch
2828

2929
-- Returns tuple of (No cex, No warnings)
@@ -46,7 +46,7 @@ runForgeTestCustom testFile match timeout maxIter ffiAllowed rpcinfo = do
4646
runForgeTest
4747
:: (MonadMask m, App m)
4848
=> FilePath -> Text -> m (Bool, Bool)
49-
runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True mempty
49+
runForgeTest testFile match = runForgeTestCustom testFile match Nothing Nothing True noRpc
5050

5151
testOpts :: forall m . App m => SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> m (UnitTestOptions)
5252
testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do

test/clitest.hs

Lines changed: 1 addition & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -246,49 +246,4 @@ main = do
246246
["--rpc", "http://mock.mock", "--prefix", "test_attack_symbolic"
247247
, "--number", "10307563", "--cache-dir", "test/contracts/fail/"]
248248
stdout `shouldContain` "[FAIL]"
249-
stderr `shouldNotContain` "CallStack"
250-
it "nowarn-rpc-empty-precompile-symbolic" $ do
251-
Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
252-
contract C {
253-
function computeHash() public view {
254-
bytes memory data = hex"68656c6c6f";
255-
(bool success,) = address(2).staticcall(data); //SHA precompile
256-
assert(success);
257-
}
258-
}
259-
|])
260-
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", Types.bsToHex c] ""
261-
stdout `shouldNotContain` "Warning: no RPC info provided"
262-
it "warn-rpc-empty-unknown-addr-symbolic" $ do
263-
Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
264-
contract C {
265-
function computeHash() public view {
266-
bytes memory data = hex"68656c6c6f";
267-
(bool success,) = address(878492734777777).staticcall(data);
268-
assert(success);
269-
}
270-
}
271-
|])
272-
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", Types.bsToHex c] ""
273-
stdout `shouldContain` "Warning: no RPC info provided"
274-
it "warn-rpc-empty-unknown-addr-equiv" $ do
275-
Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
276-
contract C {
277-
function computeHash() public view {
278-
bytes memory data = hex"68656c6c6f";
279-
(bool success,) = address(8492734777777).staticcall(data);
280-
assert(success);
281-
}
282-
}
283-
|])
284-
Just c2 <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
285-
contract C {
286-
function computeHash() public view {
287-
bytes memory data = hex"68656c6c6f";
288-
(bool success,) = address(923741898892).staticcall(data);
289-
assert(success);
290-
}
291-
}
292-
|])
293-
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "equivalence", "--code-a", Types.bsToHex c, "--code-b", Types.bsToHex c2] ""
294-
stdout `shouldContain` "Warning: no RPC info provided"
249+
stderr `shouldNotContain` "CallStack"

0 commit comments

Comments
 (0)