From 422fec411e3d9f3248e2655e4c0d2633b3ed9c94 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 24 Jan 2025 11:46:29 +0100 Subject: [PATCH] Having a go at implementing createSelectFork --- CHANGELOG.md | 1 + src/EVM.hs | 27 +++++++++++++++++++++++++++ src/EVM/Fetch.hs | 26 +++++++++++++------------- src/EVM/Types.hs | 7 ++++++- test/EVM/Test/BlockchainTests.hs | 10 ++++++++-- 5 files changed, 55 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d58b24a63..1b128d942 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 and continue running, whenever possible - STATICCALL abstraction is now performed in case of symbolic arguments - Better error messages for JSON parsing +- Added support for createSelectFork(string,uint256) ## Fixed - We now try to simplify expressions fully before trying to cast them to a concrete value diff --git a/src/EVM.hs b/src/EVM.hs index 4279fd273..0351d4639 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -67,6 +67,7 @@ import Witch (into, tryFrom, unsafeInto, tryInto) import Crypto.Hash (Digest, SHA256, RIPEMD160) import Crypto.Hash qualified as Crypto import Crypto.Number.ModArithmetic (expFast) +import Debug.Trace (traceM) blankState :: VMOps t => ST s (FrameState t s) blankState = do @@ -1407,6 +1408,13 @@ query q = assign #result $ Just $ HandleEffect (Query q) choose :: Choose s -> EVM Symbolic s () choose c = assign #result $ Just $ HandleEffect (Choose c) +fetchBlockFrom :: VMOps t => String -> W256 -> (Block -> EVM t s ()) -> EVM t s () +fetchBlockFrom url blockNo continue = do + assign (#result) . Just . HandleEffect . Query $ + PleaseFetchBlock url blockNo $ \c -> do + assign #result Nothing + continue c + -- | Construct RPC Query and halt execution until resolved fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s () fetchAccount addr continue = @@ -1900,6 +1908,25 @@ cheatActions = Map.fromList vmError (NonexistentFork forkId') _ -> vmError (BadCheatCode "selectFork(uint256) parameter decoding failed" sig) + , action "createSelectFork(string,uint256)" $ + \sig input -> case decodeBuf [AbiStringType, AbiUIntType 256] input of + CAbi [AbiString url, AbiUInt 256 blockNo] -> do + let blockNo' = fromIntegral blockNo + fetchBlockFrom (BS8.unpack url) blockNo' $ \block -> do + traceM $ "here, continuing with block:" <> show block + vm <- get + let forks = vm.forks Seq.|> ForkState vm.env block vm.cache (BS8.unpack url) + let forkId = length $ forks + modify' $ \vm' -> vm' + { env = vm.env + , block = block + , forks = forks + , currentFork = forkId + } + -- modify' $ \vm' -> vm' { env = vm.env, block = block } + frameReturn $ AbiUInt 256 (fromIntegral forkId) + _ -> vmError (BadCheatCode "createSelectFork(string,uint256) parameter decoding failed" sig) + , action "activeFork()" $ \_ _ -> do vm <- get diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index f6c23cc91..8d93b155c 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -23,12 +23,12 @@ import Data.Vector qualified as RegularVector import Network.Wreq import Network.Wreq.Session (Session) import Network.Wreq.Session qualified as Session -import Numeric.Natural (Natural) import System.Environment (lookupEnv, getEnvironment) import System.Process import Control.Monad.IO.Class import Control.Monad (when) import EVM.Effects +import Debug.Trace (traceM) -- | Abstract representation of an RPC fetch request data RpcQuery a where @@ -184,16 +184,6 @@ fetchChainIdFrom url = do sess <- Session.newAPISession fetchQuery Latest (fetchWithSession url sess) QueryChainId -http :: Natural -> Maybe Natural -> BlockNumber -> Text -> Fetcher t m s -http smtjobs smttimeout n url q = - withSolvers Z3 smtjobs 1 smttimeout $ \s -> - oracle s (Just (n, url)) q - -zero :: Natural -> Maybe Natural -> Fetcher t m s -zero smtjobs smttimeout q = - withSolvers Z3 smtjobs 1 smttimeout $ \s -> - oracle s Nothing q - -- smtsolving + (http or zero) oracle :: SolverGroup -> RpcInfo -> Fetcher t m s oracle solvers info q = do @@ -218,6 +208,7 @@ oracle solvers info q = do continue <$> getSolution solvers symAddr pathconds PleaseFetchContract addr base continue -> do + traceM $ "Fetching contract " <> show addr <> "base: " <> show base <> " from " <> show info contract <- case info of Nothing -> let c = case base of @@ -229,15 +220,24 @@ oracle solvers info q = do Just x -> pure $ continue x Nothing -> internalError $ "oracle error: " ++ show q - PleaseFetchSlot addr slot continue -> + PleaseFetchSlot addr slot continue -> do + traceM $ "Fetching slot " <> show slot <> " from " <> show info case info of Nothing -> pure (continue 0) - Just (n, url) -> + Just (n, url) -> do + traceM $ "Fetching slot " <> show slot <> " from " <> show url <> " at addr " <> show addr <> " at block " <> show n liftIO $ fetchSlotFrom n url addr slot >>= \case Just x -> pure (continue x) Nothing -> internalError $ "oracle error: " ++ show q + PleaseFetchBlock url blockNo continue -> do + traceM $ "Fetching block " <> show blockNo <> " from " <> show url + liftIO $ fetchBlockFrom (EVM.Fetch.BlockNumber blockNo) (pack url) >>= \case + Just block -> do + pure (continue block) + Nothing -> internalError $ "oracle error: " ++ show q + PleaseReadEnv variable continue -> do value <- liftIO $ lookupEnv variable pure . continue $ fromMaybe "" value diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index 13aac47f3..6bd68b171 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -593,6 +593,7 @@ deriving instance Show (Effect t s) data Query t s where PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s PleaseFetchSlot :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s + PleaseFetchBlock :: String -> W256 -> (Block -> EVM t s ()) -> Query t s PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s PleaseGetSol :: Expr EWord -> [Prop] -> (Maybe W256 -> EVM Symbolic s ()) -> Query Symbolic s PleaseDoFFI :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s @@ -609,11 +610,15 @@ data BranchCondition = Case Bool | Unknown instance Show (Query t s) where showsPrec _ = \case PleaseFetchContract addr base _ -> - (("") ++) + (("") ++) PleaseFetchSlot addr slot _ -> (("") ++) + PleaseFetchBlock url block _ -> + (("") ++) PleaseAskSMT condition constraints _ -> ((" + EVM.oracle s Nothing q + runVMTest :: App m => Case -> m () runVMTest x = do -- traceVsGeth fname name x vm0 <- liftIO $ vmForCase x - result <- EVM.Stepper.interpret (EVM.Fetch.zero 0 (Just 0)) vm0 EVM.Stepper.runFully + result <- EVM.Stepper.interpret zeroFetcher vm0 EVM.Stepper.runFully writeTrace result maybeReason <- checkExpectation x result liftIO $ forM_ maybeReason assertFailure @@ -189,7 +195,7 @@ runVMTest x = do traceVMTest :: App m => Case -> m [VMTrace] traceVMTest x = do vm0 <- liftIO $ vmForCase x - (_, (_, ts)) <- runStateT (interpretWithTrace (EVM.Fetch.zero 0 (Just 0)) EVM.Stepper.runFully) (vm0, []) + (_, (_, ts)) <- runStateT (interpretWithTrace zeroFetcher EVM.Stepper.runFully) (vm0, []) pure ts -- | given a path to a test file, a test case from within that file, and a trace from geth from running that test, compare the traces and show where we differ