From e510dd89d2998e36b8475011ef1ca4e8ff3b652f Mon Sep 17 00:00:00 2001 From: Artur Cygan Date: Thu, 23 Nov 2023 11:34:57 +0100 Subject: [PATCH] Limit VMResult cases when concrete --- cli/cli.hs | 3 -- src/EVM.hs | 70 ++++++++++++++++++++-------------------- src/EVM/Stepper.hs | 20 +++--------- src/EVM/Types.hs | 27 +++++++++------- src/EVM/UnitTest.hs | 2 +- test/EVM/Test/Tracing.hs | 17 ++++------ test/test.hs | 15 +++++---- 7 files changed, 69 insertions(+), 85 deletions(-) diff --git a/cli/cli.hs b/cli/cli.hs index b943d821c..b11fc0e9f 100644 --- a/cli/cli.hs +++ b/cli/cli.hs @@ -397,9 +397,6 @@ launchExec cmd = do Just (VMFailure err) -> liftIO $ do putStrLn $ "Error: " <> show err exitWith (ExitFailure 2) - Just (Unfinished p) -> liftIO $ do - putStrLn $ "Could not continue execution: " <> show p - exitWith (ExitFailure 2) Just (VMSuccess buf) -> liftIO $ do let msg = case buf of ConcreteBuf msg' -> msg' diff --git a/src/EVM.hs b/src/EVM.hs index 879b4f5f6..f276b8163 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1251,32 +1251,11 @@ getCodeLocation vm = (vm.state.contract, vm.state.pc) query :: Query t s -> EVM t s () query = assign #result . Just . HandleEffect . Query -choose :: Choose t s -> EVM t s () +choose :: Choose s -> EVM Symbolic s () choose = assign #result . Just . HandleEffect . Choose -branch :: forall t s. Expr EWord -> (Bool -> EVM t s ()) -> EVM t s () -branch cond continue = do - loc <- codeloc - pathconds <- use #constraints - query $ PleaseAskSMT cond pathconds (choosePath loc) - where - condSimp = Expr.simplify cond - condSimpConc = Expr.concKeccakSimpExpr condSimp - choosePath :: CodeLocation -> BranchCondition -> EVM t s () - choosePath loc (Case v) = do - assign #result Nothing - pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0) else Expr.simplifyProp (condSimpConc .== Lit 0) - (iteration, _) <- use (#iterations % at loc % non (0,[])) - stack <- use (#state % #stack) - assign (#cache % #path % at (loc, iteration)) (Just v) - assign (#iterations % at loc) (Just (iteration + 1, stack)) - continue v - -- Both paths are possible; we ask for more input - choosePath loc Unknown = - choose . PleaseChoosePath condSimp $ choosePath loc . Case - -- | Construct RPC Query and halt execution until resolved -fetchAccount :: Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s () +fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s () fetchAccount addr continue = use (#env % #contracts % at addr) >>= \case Just c -> continue c @@ -1300,7 +1279,7 @@ fetchAccount addr continue = GVar _ -> internalError "Unexpected GVar" accessStorage - :: Expr EAddr + :: VMOps t => Expr EAddr -> Expr EWord -> (Expr EWord -> EVM t s ()) -> EVM t s () @@ -1448,42 +1427,42 @@ notStatic continue = do then vmError StateChangeWhileStatic else continue -forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s () +forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s () forceAddr n msg continue = case wordToAddr n of Nothing -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n]) Just c -> continue c -forceConcrete :: Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s () +forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s () forceConcrete n msg continue = case maybeLitWord n of Nothing -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n]) Just c -> continue c -forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s () +forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s () forceConcreteAddr n msg continue = case maybeLitAddr n of Nothing -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n]) Just c -> continue c -forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s () +forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s () forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of (Just c, Just d) -> continue (c,d) _ -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m]) -forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s () +forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s () forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of (Just c, Just d) -> continue (c, d) _ -> do vm <- get partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m]) -forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s () +forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s () forceConcreteBuf (ConcreteBuf b) _ continue = continue b forceConcreteBuf b msg _ = do vm <- get @@ -1910,9 +1889,6 @@ resetState = do vmError :: VMOps t => EvmError -> EVM t s () vmError e = finishFrame (FrameErrored e) -partial :: PartialExec -> EVM t s () -partial e = assign #result (Just (Unfinished e)) - wrap :: Typeable a => [Expr a] -> [SomeExpr] wrap = fmap SomeExpr @@ -2281,7 +2257,7 @@ checkJump x xs = noJumpIntoInitData x $ do False -> vmError BadJumpDestination -- fails with partial if we're trying to jump into the symbolic region of an `InitCode` -noJumpIntoInitData :: Int -> EVM t s () -> EVM t s () +noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t s () noJumpIntoInitData idx cont = do vm <- get case vm.state.code of @@ -2589,6 +2565,27 @@ instance VMOps Symbolic where toGas _ = () whenSymbolicElse a _ = a + partial e = assign #result (Just (Unfinished e)) + branch cond continue = do + loc <- codeloc + pathconds <- use #constraints + query $ PleaseAskSMT cond pathconds (choosePath loc) + where + condSimp = Expr.simplify cond + condSimpConc = Expr.concKeccakSimpExpr condSimp + choosePath loc (Case v) = do + assign #result Nothing + pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0) + else Expr.simplifyProp (condSimpConc .== Lit 0) + (iteration, _) <- use (#iterations % at loc % non (0,[])) + stack <- use (#state % #stack) + assign (#cache % #path % at (loc, iteration)) (Just v) + assign (#iterations % at loc) (Just (iteration + 1, stack)) + continue v + -- Both paths are possible; we ask for more input + choosePath loc Unknown = + choose . PleaseChoosePath condSimp $ choosePath loc . Case + instance VMOps Concrete where burn' n continue = do available <- use (#state % #gas) @@ -2718,6 +2715,10 @@ instance VMOps Concrete where whenSymbolicElse _ a = a + partial _ = internalError "won't happen during concrete exec" + + branch (forceLit -> cond) continue = continue (cond > 0) + -- Create symbolic VM from concrete VM symbolify :: VM Concrete s -> VM Symbolic s symbolify vm = @@ -2739,7 +2740,6 @@ symbolifyResult result = HandleEffect _ -> internalError "shouldn't happen" VMFailure e -> VMFailure e VMSuccess b -> VMSuccess b - Unfinished p -> Unfinished p forceLit :: Expr EWord -> W256 forceLit (Lit w) = w diff --git a/src/EVM/Stepper.hs b/src/EVM/Stepper.hs index dc424c63d..678b5d162 100644 --- a/src/EVM/Stepper.hs +++ b/src/EVM/Stepper.hs @@ -34,7 +34,6 @@ import EVM.Types import Control.Monad.ST (stToIO, RealWorld) import Control.Monad.IO.Class import EVM.Effects -import EVM.Expr (concKeccakSimpExpr) -- | The instruction type of the operational monad data Action t s a where @@ -46,7 +45,7 @@ data Action t s a where Wait :: Query t s -> Action t s () -- | Multiple things can happen - Ask :: Choose t s -> Action t s () + Ask :: Choose s -> Action Symbolic s () -- | Embed a VM state transformation EVM :: EVM t s a -> Action t s a @@ -68,7 +67,7 @@ run = exec >> evm get wait :: Query t s -> Stepper t s () wait = singleton . Wait -ask :: Choose t s -> Stepper t s () +ask :: Choose s -> Stepper Symbolic s () ask = singleton . Ask evm :: EVM t s a -> Stepper t s a @@ -78,19 +77,15 @@ evmIO :: IO a -> Stepper t s a evmIO = singleton . IOAct -- | Run the VM until final result, resolving all queries -execFully :: Stepper t s (Either EvmError (Expr Buf)) +execFully :: Stepper Concrete s (Either EvmError (Expr Buf)) execFully = exec >>= \case HandleEffect (Query q) -> wait q >> execFully - HandleEffect (Choose q) -> - ask q >> execFully VMFailure x -> pure (Left x) VMSuccess x -> pure (Right x) - Unfinished x - -> internalError $ "partial execution encountered during concrete execution: " <> show x -- | Run the VM until its final state runFully :: Stepper t s (VM t s) @@ -123,19 +118,12 @@ interpret fetcher vm = eval . view Exec -> do (r, vm') <- liftIO $ stToIO $ runStateT EVM.Exec.exec vm interpret fetcher vm' (k r) - Wait (PleaseAskSMT expr _ continue) -> case (concKeccakSimpExpr expr) of - Lit c -> do - (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case (c > 0))) vm - interpret fetcher vm' (k r) - _ -> internalError $ "cannot handle symbolic branch conditions in this interpreter: " <> show expr Wait q -> do m <- fetcher q vm' <- liftIO $ stToIO $ execStateT m vm interpret fetcher vm' (k ()) - Ask _ -> - internalError "cannot make choices with this interpreter" IOAct m -> do - r <- liftIO $ m + r <- liftIO m interpret fetcher vm (k r) EVM m -> do (r, vm') <- liftIO $ stToIO $ runStateT m vm diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index ebd017f01..bdfffedf9 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -546,21 +546,21 @@ data PartialExec deriving (Show, Eq, Ord) -- | Effect types used by the vm implementation for side effects & control flow -data Effect t s - = Query (Query t s) - | Choose (Choose t s) +data Effect t s where + Query :: Query t s -> Effect t s + Choose :: Choose s -> Effect Symbolic s deriving instance Show (Effect t s) -- | Queries halt execution until resolved through RPC calls or SMT queries 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 - PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM t s ()) -> Query t s + PleaseAskSMT :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s PleaseDoFFI :: [String] -> (ByteString -> EVM t s ()) -> Query t s -- | Execution could proceed down one of two branches -data Choose t s where - PleaseChoosePath :: Expr EWord -> (Bool -> EVM t s ()) -> Choose t s +data Choose s where + PleaseChoosePath :: Expr EWord -> (Bool -> EVM Symbolic s ()) -> Choose s -- | The possible return values of a SMT query data BranchCondition = Case Bool | Unknown @@ -581,17 +581,17 @@ instance Show (Query t s) where PleaseDoFFI cmd _ -> ((" ((" VMResult Symbolic s -- ^ Execution could not continue further + VMFailure :: EvmError -> VMResult t s -- ^ An operation failed + VMSuccess :: (Expr Buf) -> VMResult t s -- ^ Reached STOP, RETURN, or end-of-code + HandleEffect :: (Effect t s) -> VMResult t s -- ^ An effect must be handled for execution to continue deriving instance Show (VMResult t s) @@ -796,6 +796,9 @@ class VMOps (t :: VMType) where whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a + partial :: PartialExec -> EVM t s () + branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s () + -- Bytecode Representations ------------------------------------------------------------------------ diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs index 41e99e2a6..a3d2ad362 100644 --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -110,7 +110,7 @@ unitTest opts (Contracts cs) = do -- | Assuming a constructor is loaded, this stepper will run the constructor -- to create the test contract, give it an initial balance, and run `setUp()'. -initializeUnitTest :: VMOps t => UnitTestOptions s -> SolcContract -> Stepper t s () +initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s () initializeUnitTest opts theContract = do let addr = opts.testParams.address diff --git a/test/EVM/Test/Tracing.hs b/test/EVM/Test/Tracing.hs index d772484d9..5d0ba62dc 100644 --- a/test/EVM/Test/Tracing.hs +++ b/test/EVM/Test/Tracing.hs @@ -576,17 +576,12 @@ interpretWithTrace fetcher = case action of Stepper.Exec -> execWithTrace >>= interpretWithTrace fetcher . k - Stepper.Wait q -> case q of - PleaseAskSMT (Lit x) _ continue -> - interpretWithTrace fetcher (Stepper.evm (continue (Case (x > 0))) >>= k) - _ -> do - m <- State.lift $ fetcher q - vm <- use _1 - vm' <- liftIO $ stToIO $ State.execStateT m vm - assign _1 vm' - interpretWithTrace fetcher (k ()) - Stepper.Ask _ -> - internalError "cannot make choice in this interpreter" + Stepper.Wait q -> do + m <- State.lift $ fetcher q + vm <- use _1 + vm' <- liftIO $ stToIO $ State.execStateT m vm + assign _1 vm' + interpretWithTrace fetcher (k ()) Stepper.IOAct q -> liftIO q >>= interpretWithTrace fetcher . k Stepper.EVM m -> do diff --git a/test/test.hs b/test/test.hs index 89bfab753..08e8921d7 100644 --- a/test/test.hs +++ b/test/test.hs @@ -3544,7 +3544,7 @@ runSimpleVM x ins = do vm' = set (#state % #calldata) calldata vm res <- Stepper.interpret (Fetch.zero 0 Nothing) vm' Stepper.execFully case res of - (Right (ConcreteBuf bs)) -> pure $ Just bs + Right (ConcreteBuf bs) -> pure $ Just bs s -> internalError $ show s -- | Takes a creation code and returns a vm with the result of executing the creation code @@ -3553,18 +3553,19 @@ loadVM x = do vm <- liftIO $ stToIO $ vmForEthrunCreation x vm1 <- Stepper.interpret (Fetch.zero 0 Nothing) vm Stepper.runFully case vm1.result of - Just (VMSuccess (ConcreteBuf targetCode)) -> do - let target = vm1.state.contract - vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode >> Stepper.run) - writeTrace vm2 - pure $ Just vm2 - _ -> pure Nothing + Just (VMSuccess (ConcreteBuf targetCode)) -> do + let target = vm1.state.contract + vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode) + writeTrace vm2 + pure $ Just vm2 + _ -> pure Nothing where prepVm target targetCode = Stepper.evm $ do replaceCodeOfSelf (RuntimeCode $ ConcreteRuntimeCode targetCode) resetState assign (#state % #gas) 0xffffffffffffffff -- kludge execState (loadContract target) <$> get >>= put + get hex :: ByteString -> ByteString hex s =