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