Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change interpret to take vm arg instead of StateT #232

Merged
merged 2 commits into from Apr 18, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 2 additions & 2 deletions hevm-cli/hevm-cli.hs
Expand Up @@ -34,7 +34,7 @@ import qualified EVM.UnitTest
import GHC.Conc
import Optics.Core hiding (pre, Empty)
import Control.Monad (void, when, forM_, unless)
import Control.Monad.State.Strict (execStateT, liftIO)
import Control.Monad.State.Strict (liftIO)
import Data.ByteString (ByteString)
import Data.List (intercalate, isSuffixOf, intersperse)
import Data.Text (unpack, pack)
Expand Down Expand Up @@ -491,7 +491,7 @@ launchExec cmd = do
withSolvers Z3 0 Nothing $ \solvers -> do
case optsMode cmd of
Run -> do
vm' <- execStateT (EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) . void $ EVM.Stepper.execFully) vm
vm' <- EVM.Stepper.interpret (EVM.Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully
when cmd.trace $ T.hPutStr stderr (showTraceTree dapp vm')
case vm'.result of
Nothing ->
Expand Down
2 changes: 1 addition & 1 deletion src/EVM/Dev.hs
Expand Up @@ -402,7 +402,7 @@ initVm bs = vm

-- | Builds the Expr for the given evm bytecode object
buildExpr :: SolverGroup -> ByteString -> IO (Expr End)
buildExpr solvers bs = evalStateT (interpret (Fetch.oracle solvers Nothing) Nothing Nothing runExpr) (initVm bs)
buildExpr solvers bs = interpret (Fetch.oracle solvers Nothing) Nothing Nothing (initVm bs) runExpr

dai :: IO ByteString
dai = do
Expand Down
72 changes: 32 additions & 40 deletions src/EVM/Stepper.hs
@@ -1,4 +1,3 @@
{-# Language GADTs #-}
{-# Language DataKinds #-}

module EVM.Stepper
Expand All @@ -24,28 +23,24 @@ where
-- The implementation uses the operational monad pattern
-- as the framework for monadic interpretation.

import Prelude hiding (fail)

import Control.Monad.Operational (Program, singleton, view, ProgramViewT(..), ProgramView)
import Control.Monad.State.Strict (runState, liftIO, StateT)
import qualified Control.Monad.State.Class as State
import qualified EVM.Exec
import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view)
import Control.Monad.State.Strict (StateT, execState, runState, runStateT)
import Data.Text (Text)
import EVM.Types (Expr, EType(..))

import EVM (EVM, VM, VMResult (VMFailure, VMSuccess), Error (Query, Choose), Query, Choose)
import qualified EVM

import qualified EVM.Fetch as Fetch
import EVM qualified
import EVM.Exec qualified
import EVM.Fetch qualified as Fetch
import EVM.Types (Expr, EType(..))

-- | The instruction type of the operational monad
data Action a where

-- | Keep executing until an intermediate result is reached
Exec :: Action VMResult
Exec :: Action VMResult

-- | Keep executing until an intermediate state is reached
Run :: Action VM
Run :: Action VM

-- | Wait for a query to be resolved
Wait :: Query -> Action ()
Expand Down Expand Up @@ -118,31 +113,28 @@ entering t stepper = do
enter :: Text -> Stepper ()
enter t = evm (EVM.pushTrace (EVM.EntryTrace t))

interpret :: Fetch.Fetcher -> Stepper a -> StateT VM IO a
interpret fetcher =
eval . view

interpret :: Fetch.Fetcher -> VM -> Stepper a -> IO a
interpret fetcher vm = eval . view
where
eval
:: ProgramView Action a
-> StateT VM IO a

eval (Return x) =
pure x

eval (action :>>= k) =
case action of
Exec ->
(State.state . runState) EVM.Exec.exec >>= interpret fetcher . k
Run ->
(State.state . runState) EVM.Exec.run >>= interpret fetcher . k
Wait q ->
do m <- liftIO (fetcher q)
State.state (runState m) >> interpret fetcher (k ())
Ask _ ->
error "cannot make choices with this interpreter"
IOAct m ->
do m >>= interpret fetcher . k
EVM m -> do
r <- State.state (runState m)
interpret fetcher (k r)
eval :: ProgramView Action a -> IO a
eval (Return x) = pure x
eval (action :>>= k) =
case action of
Exec ->
let (r, vm') = runState EVM.Exec.exec vm
in interpret fetcher vm' (k r)
Run ->
let vm' = execState EVM.Exec.run vm
in interpret fetcher vm' (k vm')
Wait q -> do
m <- fetcher q
let vm' = execState m vm
interpret fetcher vm' (k ())
Ask _ ->
error "cannot make choices with this interpreter"
IOAct m -> do
(r, vm') <- runStateT m vm
interpret fetcher vm' (k r)
EVM m ->
let (r, vm') = runState m vm
in interpret fetcher vm' (k r)