{-# 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 = Action VMResult -> Stepper VMResult
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VMResult
Exec
run :: Stepper VM
run :: Stepper VM
run = Action VM -> Stepper VM
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton Action VM
Run
wait :: Query -> Stepper ()
wait :: Query -> Stepper ()
wait = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Query -> Action ()) -> Query -> Stepper ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Query -> Action ()
Wait
ask :: Choose -> Stepper ()
ask :: Choose -> Stepper ()
ask = Action () -> Stepper ()
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action () -> Stepper ())
-> (Choose -> Action ()) -> Choose -> Stepper ()
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 = Action a -> ProgramT Action Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> ProgramT Action Identity a)
-> (EVM a -> Action a) -> EVM a -> ProgramT Action Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EVM a -> Action a
forall a. EVM a -> Action a
EVM
evmIO :: StateT VM IO a -> Stepper a
evmIO :: forall a. StateT VM IO a -> Stepper a
evmIO = Action a -> ProgramT Action Identity a
forall (instr :: * -> *) a (m :: * -> *).
instr a -> ProgramT instr m a
singleton (Action a -> ProgramT Action Identity a)
-> (StateT VM IO a -> Action a)
-> StateT VM IO a
-> ProgramT Action Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT VM IO a -> Action a
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 Stepper VMResult
-> (VMResult -> Stepper (Either EvmError (Expr 'Buf)))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> (a -> ProgramT Action Identity b) -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
HandleEffect (Query Query
q) ->
Query -> Stepper ()
wait Query
q Stepper ()
-> Stepper (Either EvmError (Expr 'Buf))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
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 Stepper ()
-> Stepper (Either EvmError (Expr 'Buf))
-> Stepper (Either EvmError (Expr 'Buf))
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper (Either EvmError (Expr 'Buf))
execFully
VMFailure EvmError
x ->
Either EvmError (Expr 'Buf)
-> Stepper (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT Action 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)
-> Stepper (Either EvmError (Expr 'Buf))
forall a. a -> ProgramT Action 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] -> Stepper (Either EvmError (Expr 'Buf))
forall a. HasCallStack => [Char] -> a
internalError ([Char] -> Stepper (Either EvmError (Expr 'Buf)))
-> [Char] -> Stepper (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 VM
runFully :: Stepper VM
runFully = do
VM
vm <- Stepper VM
run
case VM
vm.result of
Maybe VMResult
Nothing -> [Char] -> Stepper VM
forall a. HasCallStack => [Char] -> a
internalError [Char]
"should not occur"
Just (HandleEffect (Query Query
q)) ->
Query -> Stepper ()
wait Query
q Stepper () -> Stepper VM -> Stepper VM
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
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 Stepper () -> Stepper VM -> Stepper VM
forall a b.
ProgramT Action Identity a
-> ProgramT Action Identity b -> ProgramT Action Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stepper VM
runFully
Just VMResult
_ ->
VM -> Stepper VM
forall a. a -> ProgramT Action Identity a
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
EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm (TraceData -> EVM ()
EVM.pushTrace (Text -> TraceData
EntryTrace Text
t))
a
x <- Stepper a
stepper
EVM () -> Stepper ()
forall a. EVM a -> Stepper a
evm EVM ()
EVM.popTrace
a -> Stepper a
forall a. a -> ProgramT Action Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
enter :: Text -> Stepper ()
enter :: Text -> Stepper ()
enter Text
t = EVM () -> Stepper ()
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 = ProgramView Action a -> IO a
forall a. ProgramView Action a -> IO a
eval (ProgramView Action a -> IO a)
-> (Stepper a -> ProgramView Action a) -> Stepper a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stepper a -> ProgramView Action a
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) = a -> IO a
forall a. a -> IO a
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') = State VM VMResult -> VM -> (VMResult, VM)
forall s a. State s a -> s -> (a, s)
runState State VM VMResult
EVM.Exec.exec VM
vm
in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
VMResult
r)
Action b
Run ->
let vm' :: VM
vm' = State VM VM -> VM -> VM
forall s a. State s a -> s -> s
execState State VM VM
EVM.Exec.run VM
vm
in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
VM
vm')
Wait (PleaseAskSMT (Lit W256
c) [Prop]
_ BranchCondition -> EVM ()
continue) ->
let (()
r, VM
vm') = EVM () -> VM -> ((), VM)
forall s a. State s a -> s -> (a, s)
runState (BranchCondition -> EVM ()
continue (Bool -> BranchCondition
Case (W256
c W256 -> W256 -> Bool
forall a. Ord a => a -> a -> Bool
> W256
0))) VM
vm
in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
()
r)
Wait Query
q -> do
EVM ()
m <- Fetcher
fetcher Query
q
let vm' :: VM
vm' = EVM () -> VM -> VM
forall s a. State s a -> s -> s
execState EVM ()
m VM
vm
Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k ())
Ask Choose
_ ->
[Char] -> IO a
forall a. HasCallStack => [Char] -> a
internalError [Char]
"cannot make choices with this interpreter"
IOAct StateT VM IO b
m -> do
(b
r, VM
vm') <- StateT VM IO b -> VM -> IO (b, VM)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT VM IO b
m VM
vm
Fetcher -> VM -> ProgramT Action Identity a -> IO a
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') = EVM b -> VM -> (b, VM)
forall s a. State s a -> s -> (a, s)
runState EVM b
m VM
vm
in Fetcher -> VM -> ProgramT Action Identity a -> IO a
forall a. Fetcher -> VM -> Stepper a -> IO a
interpret Fetcher
fetcher VM
vm' (b -> ProgramT Action Identity a
k b
r)