{-# LANGUAGE DataKinds #-}
module EVM.Stepper
( Action (..)
, Stepper
, exec
, execFully
, run
, runFully
, wait
, ask
, evm
, evmIO
, enter
, interpret
)
where
import Control.Monad.Operational (Program, ProgramViewT(..), ProgramView, singleton, view)
import Control.Monad.State.Strict (execStateT, runStateT, get)
import Data.Text (Text)
import EVM qualified
import EVM.Exec qualified
import EVM.Fetch qualified as Fetch
import EVM.Types
import Control.Monad.ST (stToIO, RealWorld)
data Action s a where
Exec :: Action s (VMResult s)
Wait :: Query s -> Action s ()
Ask :: Choose s -> Action s ()
EVM :: EVM s a -> Action s a
IOAct :: IO a -> Action s a
type Stepper s a = Program (Action s) a
exec :: Stepper s (VMResult s)
exec :: forall s. Stepper s (VMResult s)
exec = Action s (VMResult s) -> ProgramT (Action s) Identity (VMResult s)
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action s (VMResult s)
forall s. Action s (VMResult s)
Exec
run :: Stepper s (VM s)
run :: forall s. Stepper s (VM s)
run = Stepper s (VMResult s)
forall s. Stepper s (VMResult s)
exec Stepper s (VMResult s)
-> ProgramT (Action s) Identity (VM s)
-> ProgramT (Action s) Identity (VM s)
forall a b.
ProgramT (Action s) Identity a
-> ProgramT (Action s) Identity b -> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> EVM s (VM s) -> ProgramT (Action s) Identity (VM s)
forall s a. EVM s a -> Stepper s a
evm EVM s (VM s)
forall s (m :: * -> *). MonadState s m => m s
get
wait :: Query s -> Stepper s ()
wait :: forall s. Query s -> Stepper s ()
wait = Action s () -> ProgramT (Action s) Identity ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action s () -> ProgramT (Action s) Identity ())
-> (Query s -> Action s ())
-> Query s
-> ProgramT (Action s) Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Query s -> Action s ()
forall s. Query s -> Action s ()
Wait
ask :: Choose s -> Stepper s ()
ask :: forall s. Choose s -> Stepper s ()
ask = Action s () -> ProgramT (Action s) Identity ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action s () -> ProgramT (Action s) Identity ())
-> (Choose s -> Action s ())
-> Choose s
-> ProgramT (Action s) Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Choose s -> Action s ()
forall s. Choose s -> Action s ()
Ask
evm :: EVM s a -> Stepper s a
evm :: forall s a. EVM s a -> Stepper s a
evm = Action s a -> ProgramT (Action s) Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action s a -> ProgramT (Action s) Identity a)
-> (EVM s a -> Action s a)
-> EVM s a
-> ProgramT (Action s) Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EVM s a -> Action s a
forall s a. EVM s a -> Action s a
EVM
evmIO :: IO a -> Stepper s a
evmIO :: forall a s. IO a -> Stepper s a
evmIO = Action s a -> ProgramT (Action s) Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action s a -> ProgramT (Action s) Identity a)
-> (IO a -> Action s a) -> IO a -> ProgramT (Action s) Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> Action s a
forall a s. IO a -> Action s a
IOAct
execFully :: Stepper s (Either EvmError (Expr Buf))
execFully :: forall s. Stepper s (Either EvmError (Expr 'Buf))
execFully =
Stepper s (VMResult s)
forall s. Stepper s (VMResult s)
exec Stepper s (VMResult s)
-> (VMResult s
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf)))
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a b.
ProgramT (Action s) Identity a
-> (a -> ProgramT (Action s) Identity b)
-> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
HandleEffect (Query Query s
q) ->
Query s -> Stepper s ()
forall s. Query s -> Stepper s ()
wait Query s
q Stepper s ()
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a b.
ProgramT (Action s) Identity a
-> ProgramT (Action s) Identity b -> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper s (Either EvmError (Expr 'Buf))
execFully
HandleEffect (Choose Choose s
q) ->
Choose s -> Stepper s ()
forall s. Choose s -> Stepper s ()
ask Choose s
q Stepper s ()
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a b.
ProgramT (Action s) Identity a
-> ProgramT (Action s) Identity b -> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall s. Stepper s (Either EvmError (Expr 'Buf))
execFully
VMFailure EvmError
x ->
Either EvmError (Expr 'Buf)
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT (Action s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvmError -> Either EvmError (Expr 'Buf)
forall a b. a -> Either a b
Left EvmError
x)
VMSuccess Expr 'Buf
x ->
Either EvmError (Expr 'Buf)
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT (Action s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr 'Buf -> Either EvmError (Expr 'Buf)
forall a b. b -> Either a b
Right Expr 'Buf
x)
Unfinished PartialExec
x
-> [Char]
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a. HasCallStack => [Char] -> a
internalError ([Char]
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf)))
-> [Char]
-> ProgramT (Action s) Identity (Either EvmError (Expr 'Buf))
forall a b. (a -> b) -> a -> b
$ [Char]
"partial execution encountered during concrete execution: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> PartialExec -> [Char]
forall a. Show a => a -> [Char]
show PartialExec
x
runFully :: Stepper s (VM s)
runFully :: forall s. Stepper s (VM s)
runFully = do
VM s
vm <- Stepper s (VM s)
forall s. Stepper s (VM s)
run
case VM s
vm.result of
Maybe (VMResult s)
Nothing -> [Char] -> Stepper s (VM s)
forall a. HasCallStack => [Char] -> a
internalError [Char]
"should not occur"
Just (HandleEffect (Query Query s
q)) ->
Query s -> Stepper s ()
forall s. Query s -> Stepper s ()
wait Query s
q Stepper s () -> Stepper s (VM s) -> Stepper s (VM s)
forall a b.
ProgramT (Action s) Identity a
-> ProgramT (Action s) Identity b -> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper s (VM s)
forall s. Stepper s (VM s)
runFully
Just (HandleEffect (Choose Choose s
q)) ->
Choose s -> Stepper s ()
forall s. Choose s -> Stepper s ()
ask Choose s
q Stepper s () -> Stepper s (VM s) -> Stepper s (VM s)
forall a b.
ProgramT (Action s) Identity a
-> ProgramT (Action s) Identity b -> ProgramT (Action s) Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper s (VM s)
forall s. Stepper s (VM s)
runFully
Just VMResult s
_ ->
VM s -> Stepper s (VM s)
forall a. a -> ProgramT (Action s) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VM s
vm
enter :: Text -> Stepper s ()
enter :: forall s. Text -> Stepper s ()
enter Text
t = EVM s () -> Stepper s ()
forall s a. EVM s a -> Stepper s a
evm (TraceData -> EVM s ()
forall s. TraceData -> EVM s ()
EVM.pushTrace (Text -> TraceData
EntryTrace Text
t))
interpret :: Fetch.Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret :: forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm = ProgramView (Action RealWorld) a -> IO a
forall a. ProgramView (Action RealWorld) a -> IO a
eval (ProgramView (Action RealWorld) a -> IO a)
-> (Stepper RealWorld a -> ProgramView (Action RealWorld) a)
-> Stepper RealWorld a
-> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper RealWorld a -> ProgramView (Action RealWorld) a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view
where
eval :: ProgramView (Action RealWorld) a -> IO a
eval :: forall a. ProgramView (Action RealWorld) a -> IO a
eval (Return a
x) = a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
eval (Action RealWorld b
action :>>= b -> ProgramT (Action RealWorld) Identity a
k) =
case Action RealWorld b
action of
Action RealWorld b
Exec -> do
(VMResult RealWorld
r, VM RealWorld
vm') <- ST RealWorld (VMResult RealWorld, VM RealWorld)
-> IO (VMResult RealWorld, VM RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VMResult RealWorld, VM RealWorld)
-> IO (VMResult RealWorld, VM RealWorld))
-> ST RealWorld (VMResult RealWorld, VM RealWorld)
-> IO (VMResult RealWorld, VM RealWorld)
forall a b. (a -> b) -> a -> b
$ StateT (VM RealWorld) (ST RealWorld) (VMResult RealWorld)
-> VM RealWorld -> ST RealWorld (VMResult RealWorld, VM RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (VM RealWorld) (ST RealWorld) (VMResult RealWorld)
forall s. EVM s (VMResult s)
EVM.Exec.exec VM RealWorld
vm
Fetcher RealWorld
-> VM RealWorld -> ProgramT (Action RealWorld) Identity a -> IO a
forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm' (b -> ProgramT (Action RealWorld) Identity a
k b
VMResult RealWorld
r)
Wait (PleaseAskSMT (Lit W256
c) [Prop]
_ BranchCondition -> EVM RealWorld ()
continue) -> do
(()
r, VM RealWorld
vm') <- ST RealWorld ((), VM RealWorld) -> IO ((), VM RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld ((), VM RealWorld) -> IO ((), VM RealWorld))
-> ST RealWorld ((), VM RealWorld) -> IO ((), VM RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM RealWorld () -> VM RealWorld -> ST RealWorld ((), VM RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BranchCondition -> EVM RealWorld ()
continue (Bool -> BranchCondition
Case (W256
c W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0))) VM RealWorld
vm
Fetcher RealWorld
-> VM RealWorld -> ProgramT (Action RealWorld) Identity a -> IO a
forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm' (b -> ProgramT (Action RealWorld) Identity a
k b
()
r)
Wait (PleaseAskSMT Expr 'EWord
c [Prop]
_ BranchCondition -> EVM RealWorld ()
_) ->
[Char] -> IO a
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO a) -> [Char] -> IO a
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot handle symbolic branch conditions in this interpreter: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Expr 'EWord -> [Char]
forall a. Show a => a -> [Char]
show Expr 'EWord
c
Wait Query RealWorld
q -> do
EVM RealWorld ()
m <- Fetcher RealWorld
fetcher Query RealWorld
q
VM RealWorld
vm' <- ST RealWorld (VM RealWorld) -> IO (VM RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (VM RealWorld) -> IO (VM RealWorld))
-> ST RealWorld (VM RealWorld) -> IO (VM RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM RealWorld () -> VM RealWorld -> ST RealWorld (VM RealWorld)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT EVM RealWorld ()
m VM RealWorld
vm
Fetcher RealWorld
-> VM RealWorld -> ProgramT (Action RealWorld) Identity a -> IO a
forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm' (b -> ProgramT (Action RealWorld) Identity a
k ())
Ask Choose RealWorld
_ ->
[Char] -> IO a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot make choices with this interpreter"
IOAct IO b
m -> do
b
r <- IO b
m
Fetcher RealWorld
-> VM RealWorld -> ProgramT (Action RealWorld) Identity a -> IO a
forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm (b -> ProgramT (Action RealWorld) Identity a
k b
r)
EVM EVM RealWorld b
m -> do
(b
r, VM RealWorld
vm') <- ST RealWorld (b, VM RealWorld) -> IO (b, VM RealWorld)
forall a. ST RealWorld a -> IO a
stToIO (ST RealWorld (b, VM RealWorld) -> IO (b, VM RealWorld))
-> ST RealWorld (b, VM RealWorld) -> IO (b, VM RealWorld)
forall a b. (a -> b) -> a -> b
$ EVM RealWorld b -> VM RealWorld -> ST RealWorld (b, VM RealWorld)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT EVM RealWorld b
m VM RealWorld
vm
Fetcher RealWorld
-> VM RealWorld -> ProgramT (Action RealWorld) Identity a -> IO a
forall a.
Fetcher RealWorld -> VM RealWorld -> Stepper RealWorld a -> IO a
interpret Fetcher RealWorld
fetcher VM RealWorld
vm' (b -> ProgramT (Action RealWorld) Identity a
k b
r)