Skip to content

Commit

Permalink
Fixing up rpc
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Oct 9, 2023
1 parent a3e0e6d commit 2b28a25
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 12 deletions.
3 changes: 1 addition & 2 deletions bench/bench.hs
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,8 @@ import qualified EVM.Fetch as Fetch

import EVM.Test.BlockchainTests qualified as BCTests


benchEnv :: Env
benchEnv = Env { config = Config { dumpQueries = True } }
benchEnv = Env { config = Config { dumpQueries = False } }

main :: IO ()
main = defaultMain
Expand Down
32 changes: 22 additions & 10 deletions test/rpc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,17 @@ import EVM.Stepper qualified as Stepper
import EVM.SymExec
import EVM.Test.Utils
import EVM.Solidity (ProjectType(..))
import EVM.Types hiding (BlockNumber)
import EVM.Types hiding (BlockNumber, Env)
import Control.Monad.ST (stToIO, RealWorld)
import Control.Monad.Reader (ReaderT)
import Control.Monad.IO.Unlift
import EVM.Effects

rpcEnv :: Env
rpcEnv = Env { config = Config { dumpQueries = False } }

test :: TestName -> ReaderT Env IO () -> TestTree
test a b = testCase a $ runEnv rpcEnv b

main :: IO ()
main = defaultMain tests
Expand Down Expand Up @@ -60,18 +69,20 @@ tests = testGroup "rpc"
]
, testGroup "execution with remote state"
-- execute against remote state from a ds-test harness
[ testCase "dapp-test" $ do
[ test "dapp-test" $ do
let testFile = "test/contracts/pass/rpc.sol"
runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry >>= assertEqual "test result" True
-- runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry >>= assertEqual "test result" True
res <- runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry
liftIO $ assertEqual "test result" True res

-- concretely exec "transfer" on WETH9 using remote rpc
-- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code
, testCase "weth-conc" $ do
, test "weth-conc" $ do
let
blockNum = 16198552
wad = 0x999999999999999999
calldata' = ConcreteBuf $ abiMethod "transfer(address,uint256)" (AbiTuple (V.fromList [AbiAddress (Addr 0xdead), AbiUInt 256 wad]))
vm <- weth9VM blockNum (calldata', [])
vm <- liftIO $ weth9VM blockNum (calldata', [])
postVm <- withSolvers Z3 1 Nothing $ \solvers ->
Stepper.interpret (oracle solvers (Just (BlockNumber blockNum, testRpc))) vm Stepper.runFully
let
Expand All @@ -83,21 +94,22 @@ tests = testGroup "rpc"
msg = case postVm.result of
Just (VMSuccess m) -> m
_ -> internalError "VMSuccess expected"
assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)
assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad)
liftIO $ do
assertEqual "should succeed" msg (ConcreteBuf $ word256Bytes 0x1)
assertEqual "should revert" receiverBal (W256 $ 2595433725034301 + wad)

-- symbolically exec "transfer" on WETH9 using remote rpc
-- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code
, testCase "weth-sym" $ do
, test "weth-sym" $ do
let
blockNum = 16198552
calldata' = symCalldata "transfer(address,uint256)" [AbiAddressType, AbiUIntType 256] ["0xdead"] (AbstractBuf "txdata")
postc _ (Failure _ _ (Revert _)) = PBool False
postc _ _ = PBool True
vm <- weth9VM blockNum calldata'
vm <- liftIO $ weth9VM blockNum calldata'
(_, [Cex (_, model)]) <- withSolvers Z3 1 Nothing $ \solvers ->
verify solvers (rpcVeriOpts (BlockNumber blockNum, testRpc)) vm (Just postc)
assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
liftIO $ assertBool "model should exceed caller balance" (getVar model "arg2" >= 695836005599316055372648)
]
]

Expand Down

0 comments on commit 2b28a25

Please sign in to comment.