diff --git a/cli/cli.hs b/cli/cli.hs index 53bc34685..e5b817601 100644 --- a/cli/cli.hs +++ b/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 diff --git a/src/EVM/Fetch.hs b/src/EVM/Fetch.hs index aa96d51ee..687b1f945 100644 --- a/src/EVM/Fetch.hs +++ b/src/EVM/Fetch.hs @@ -8,8 +8,9 @@ module EVM.Fetch , RpcInfo (..) , RpcQuery (..) , EVM.Fetch.zero + , noRpc + , noRpcFetcher , BlockNumber (..) - , mkRpcInfo , mkSession , mkSessionWithoutCache , Session (..) @@ -46,7 +47,6 @@ 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 @@ -54,7 +54,7 @@ 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 diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 56f123a9a..0208d31fe 100644 --- a/src/EVM/SymExec.hs +++ b/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 diff --git a/test/EVM/Test/BlockchainTests.hs b/test/EVM/Test/BlockchainTests.hs index 160187285..c2c5b2569 100644 --- a/test/EVM/Test/BlockchainTests.hs +++ b/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 diff --git a/test/EVM/Test/FuzzSymExec.hs b/test/EVM/Test/FuzzSymExec.hs index c6469918e..0775333e5 100644 --- a/test/EVM/Test/FuzzSymExec.hs +++ b/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 diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs index a83f29a95..3073908d0 100644 --- a/test/EVM/Test/Utils.hs +++ b/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 diff --git a/test/clitest.hs b/test/clitest.hs index 33d12b8cb..17372de0b 100644 --- a/test/clitest.hs +++ b/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" \ No newline at end of file diff --git a/test/rpc.hs b/test/rpc.hs index d4db71724..f292aa482 100644 --- a/test/rpc.hs +++ b/test/rpc.hs @@ -82,15 +82,12 @@ tests = testGroup "rpc" -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code , test "weth-conc" $ do let - blockNum = 16198552 wad = 0x999999999999999999 calldata' = ConcreteBuf $ abiMethod "transfer(address,uint256)" (AbiTuple (V.fromList [AbiAddress (Addr 0xdead), AbiUInt 256 wad])) - rpcDat = Just (BlockNumber blockNum, testRpc) - rpcInfo :: RpcInfo = mempty { blockNumURL = rpcDat } sess <- mkSessionWithoutCache - vm <- weth9VM sess blockNum (calldata', []) + vm <- weth9VM sess testBlockNumber (calldata', []) postVm <- withSolvers Z3 1 1 Nothing $ \solvers -> - Stepper.interpret (oracle solvers (Just sess) rpcInfo) vm Stepper.runFully + Stepper.interpret (oracle solvers (Just sess) testRpcInfo) vm Stepper.runFully let wethStore = (fromJust $ Map.lookup (LitAddr 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2) postVm.env.contracts).storage wethStore' = case wethStore of @@ -109,20 +106,18 @@ tests = testGroup "rpc" , test "weth-sym" $ do calldata' <- symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata") let - blockNum = 16198552 postc _ (Failure _ _ (Revert _)) = PBool False postc _ _ = PBool True sess <- mkSession Nothing Nothing - vm <- weth9VM sess blockNum calldata' + vm <- weth9VM sess testBlockNumber calldata' (_, [Cex (_, model)]) <- withSolvers Z3 1 1 Nothing $ \s -> - let rpcInfo ::RpcInfo = mempty { blockNumURL = Just (BlockNumber blockNum, testRpc) } - in verify s (oracle s (Just sess) rpcInfo) (rpcVeriOpts (fromJust rpcInfo.blockNumURL)) (symbolify vm) postc + verify s (oracle s (Just sess) testRpcInfo) (defaultVeriOpts {rpcInfo = testRpcInfo}) (symbolify vm) postc liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648) ] ] -- call into WETH9 from 0xf04a... (a large holder) -weth9VM :: App m => Session -> W256 -> (Expr Buf, [Prop]) -> m (VM Concrete) +weth9VM :: App m => Session -> BlockNumber -> (Expr Buf, [Prop]) -> m (VM Concrete) weth9VM sess blockNum calldata' = do let caller' = LitAddr 0xf04a5cc80b1e94c69b48f5ee68a08cd2f09a7c3e @@ -130,15 +125,15 @@ weth9VM sess blockNum calldata' = do callvalue' = Lit 0 vmFromRpc sess blockNum calldata' callvalue' caller' weth9 -vmFromRpc :: App m => Session -> W256 -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> m (VM Concrete) +vmFromRpc :: App m => Session -> BlockNumber -> (Expr Buf, [Prop]) -> Expr EWord -> Expr EAddr -> Addr -> m (VM Concrete) vmFromRpc sess blockNum calldata callvalue caller address = do conf <- readConfig - ctrct <- liftIO $ fetchContractWithSession conf sess (BlockNumber blockNum) testRpc address >>= \case + ctrct <- liftIO $ fetchContractWithSession conf sess blockNum testRpc address >>= \case Nothing -> internalError $ "contract not found: " <> show address Just contract' -> pure contract' liftIO $ addFetchCache sess address ctrct - blk <- liftIO $ fetchBlockWithSession conf sess (BlockNumber blockNum) testRpc >>= \case + blk <- liftIO $ fetchBlockWithSession conf sess blockNum testRpc >>= \case Nothing -> internalError "could not fetch block" Just b -> pure b @@ -174,6 +169,8 @@ vmFromRpc sess blockNum calldata callvalue caller address = do testRpc :: Text testRpc = "https://eth-mainnet.alchemyapi.io/v2/vpeKFsEF6PHifHzdtcwXSDbhV3ym5Ro4" +testBlockNumber :: BlockNumber +testBlockNumber = BlockNumber 16198552 + testRpcInfo :: RpcInfo -testRpcInfo = let rpcDat = Just (BlockNumber 16198552, testRpc) - in mempty { blockNumURL = rpcDat } +testRpcInfo = RpcInfo $ Just (testBlockNumber, testRpc) diff --git a/test/test.hs b/test/test.hs index 40103da1b..e609064f3 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1891,7 +1891,7 @@ tests = testGroup "hevm" let calldata = (WriteWord (Lit 0x0) (Var "u") (ConcreteBuf ""), []) initVM <- liftIO $ stToIO $ abstractVM calldata initCode Nothing True let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased } - expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing mempty) iterConf initVM runExpr + expr <- Expr.simplify <$> interpret (Fetch.noRpcFetcher s) iterConf initVM runExpr assertBoolM "unexptected partial execution" (not $ Expr.containsNode isPartial expr) , test "mixed-concrete-symbolic-args" $ do Just c <- solcRuntime "C" @@ -1982,7 +1982,7 @@ tests = testGroup "hevm" withDefaultSolver $ \s -> do vm <- liftIO $ stToIO $ loadSymVM runtimecode (Lit 0) initCode False let iterConf = IterConfig {maxIter=Nothing, askSmtIters=1, loopHeuristic=StackBased } - expr <- Expr.simplify <$> interpret (Fetch.oracle s Nothing mempty) iterConf vm runExpr + expr <- Expr.simplify <$> interpret (Fetch.noRpcFetcher s) iterConf vm runExpr case expr of Partial _ _ (JumpIntoSymbolicCode _ _ _) -> assertBoolM "" True _ -> assertBoolM "did not encounter expected partial node" False @@ -2022,7 +2022,7 @@ tests = testGroup "hevm" , ("test/contracts/fail/symbolicFail.sol", "prove_symb_fail_allrev_selector.*", (False, False)) , ("test/contracts/fail/symbolicFail.sol", "prove_symb_fail_somerev_selector.*", (False, True))] forM_ cases $ \(testFile, match, expected) -> do - actual <- runForgeTestCustom testFile match Nothing Nothing False mempty + actual <- runForgeTestCustom testFile match Nothing Nothing False Fetch.noRpc putStrLnM $ "Test result for " <> testFile <> " match: " <> T.unpack match <> ": " <> show actual assertEqualM "Must match" expected actual , test "Trivial-Fail" $ do @@ -2055,14 +2055,14 @@ tests = testGroup "hevm" runForgeTest testFile "prove_trivial" >>= assertEqualM "prove_trivial" (False, False) runForgeTest testFile "prove_trivial_dstest" >>= assertEqualM "prove_trivial_dstest" (False, False) runForgeTest testFile "prove_add" >>= assertEqualM "prove_add" (False, True) - runForgeTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False mempty + runForgeTestCustom testFile "prove_smtTimeout" (Just 1) Nothing False Fetch.noRpc >>= assertEqualM "prove_smtTimeout" (True, False) runForgeTest testFile "prove_multi" >>= assertEqualM "prove_multi" (False, True) runForgeTest testFile "prove_distributivity" >>= assertEqualM "prove_distributivity" (False, True) , test "Loop-Tests" $ do let testFile = "test/contracts/pass/loops.sol" - runForgeTestCustom testFile "prove_loop" Nothing (Just 10) False mempty >>= assertEqualM "test result" (True, False) - runForgeTestCustom testFile "prove_loop" Nothing (Just 100) False mempty >>= assertEqualM "test result" (False, False) + runForgeTestCustom testFile "prove_loop" Nothing (Just 10) False Fetch.noRpc >>= assertEqualM "test result" (True, False) + runForgeTestCustom testFile "prove_loop" Nothing (Just 100) False Fetch.noRpc >>= assertEqualM "test result" (False, False) , test "Cheat-Codes-Pass" $ do let testFile = "test/contracts/pass/cheatCodes.sol" runForgeTest testFile ".*" >>= assertEqualM "test result" (True, False) @@ -4218,7 +4218,7 @@ tests = testGroup "hevm" <&> set (#state % #callvalue) (Lit 0) <&> over (#env % #contracts) (Map.insert aAddr (initialContract (RuntimeCode (ConcreteRuntimeCode a)))) - verify s (Fetch.oracle s Nothing mempty) defaultVeriOpts vm (checkAssertions defaultPanicCodes) + verify s (Fetch.noRpcFetcher s) defaultVeriOpts vm (checkAssertions defaultPanicCodes) let storeCex = cex.store testCex = case (Map.lookup cAddr storeCex, Map.lookup aAddr storeCex) of @@ -4294,7 +4294,7 @@ tests = testGroup "hevm" let yulsafeDistributivity = hex "6355a79a6260003560e01c14156016576015601f565b5b60006000fd60a1565b603d602d604435600435607c565b6039602435600435607c565b605d565b6052604b604435602435605d565b600435607c565b141515605a57fe5b5b565b6000828201821115151560705760006000fd5b82820190505b92915050565b6000818384048302146000841417151560955760006000fd5b82820290505b92915050565b" calldata <- mkCalldata (Just (Sig "distributivity(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])) [] vm <- liftIO $ stToIO $ abstractVM calldata yulsafeDistributivity Nothing False - (_, [Qed]) <- withDefaultSolver $ \s -> verify s (Fetch.oracle s Nothing mempty) defaultVeriOpts vm (checkAssertions defaultPanicCodes) + (_, [Qed]) <- withDefaultSolver $ \s -> verify s (Fetch.noRpcFetcher s) defaultVeriOpts vm (checkAssertions defaultPanicCodes) putStrLnM "Proven" , test "safemath-distributivity-sol" $ do