{-# Language DataKinds #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , evmIO
  , entering
  , enter
  , interpret
  )
where

-- This module is an abstract definition of EVM steppers.
-- Steppers can be run as TTY debuggers or as CLI test runners.
--
-- The implementation uses the operational monad pattern
-- as the framework for monadic interpretation.

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

import qualified EVM

import qualified EVM.Fetch as Fetch
import EVM.Exec qualified

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

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

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

  -- | Wait for a query to be resolved
  Wait :: Query -> Action ()

  -- | Multiple things can happen
  Ask :: Choose -> Action ()

  -- | Embed a VM state transformation
  EVM  :: EVM a -> Action a

  -- | Perform an IO action
  IOAct :: StateT VM IO a -> Action a -- they should all just be this?

-- | Type alias for an operational monad of @Action@
type Stepper a = Program Action a

-- Singleton actions

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

-- | Run the VM until final result, resolving all queries
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
error forall a b. (a -> b) -> a -> b
$ [Char]
"Internal Error: partial execution encountered during concrete execution: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show PartialExec
x

-- | Run the VM until its final state
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
error [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
error [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)