{-# LANGUAGE DataKinds #-}

module EVM.Stepper
  ( Action (..)
  , Stepper
  , exec
  , execFully
  , run
  , runFully
  , wait
  , ask
  , evm
  , evmIO
  , 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 (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)

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

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

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

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

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

  -- | Perform an IO action
  IOAct :: IO a -> Action s a

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

-- Singleton actions

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

-- | Run the VM until final result, resolving all queries
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

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