{-|
Module      : Effects
Description : Domain specific effects

This module contains custom app specific mtl style effects for hevm
These are written in the style of the ReaderT over IO pattern [1].
Right now we only have a single `ReadConfig` effect, but over time hope to
migrate most usages of IO into custom effects here.

This framework would allow us to have multiple interpretations for effects
(e.g. a pure version for tests), but for now we interpret everything in IO
only.

[1]: https://www.fpcomplete.com/blog/readert-design-pattern/
-}

{-# Language RankNTypes #-}
{-# Language FlexibleInstances #-}
{-# Language KindSignatures #-}
{-# Language DataKinds #-}
{-# Language GADTs #-}
{-# Language DerivingStrategies #-}
{-# Language DuplicateRecordFields #-}
{-# Language NoFieldSelectors #-}
{-# Language ConstraintKinds #-}

module EVM.Effects where

import Control.Monad.Reader
import Control.Monad.IO.Unlift
import EVM.Dapp (DappInfo)
import EVM.Types (VM(..))
import Control.Monad.ST (RealWorld)
import Data.Text (Text)
import Data.Text.IO qualified as T
import System.IO (stderr)
import EVM.Format (showTraceTree)
import EVM (traceForest)


-- Abstract Effects --------------------------------------------------------------------------------
-- Here we define the abstract interface for the effects that we wish to model


-- Read from global config
class Monad m => ReadConfig m where
  readConfig ::  m Config

data Config = Config
  { Config -> Bool
dumpQueries     :: Bool
  , Config -> Bool
dumpExprs       :: Bool
  , Config -> Bool
dumpEndStates   :: Bool
  , Config -> Bool
debug           :: Bool
  , Config -> Bool
abstRefineArith :: Bool
  , Config -> Bool
abstRefineMem   :: Bool
  , Config -> Bool
dumpTrace       :: Bool
  , Config -> Integer
numCexFuzz      :: Integer
   -- Used to debug fuzzer in test.hs. It disables the SMT solver
   -- and uses the fuzzer ONLY to try to find a counterexample.
   -- Returns Unknown if the Cex cannot be found via fuzzing
  , Config -> Bool
onlyCexFuzz     :: Bool
  }
  deriving (Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
(Int -> Config -> ShowS)
-> (Config -> String) -> ([Config] -> ShowS) -> Show Config
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Config -> ShowS
showsPrec :: Int -> Config -> ShowS
$cshow :: Config -> String
show :: Config -> String
$cshowList :: [Config] -> ShowS
showList :: [Config] -> ShowS
Show, Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
/= :: Config -> Config -> Bool
Eq)

defaultConfig :: Config
defaultConfig :: Config
defaultConfig = Config
  { $sel:dumpQueries:Config :: Bool
dumpQueries = Bool
False
  , $sel:dumpExprs:Config :: Bool
dumpExprs = Bool
False
  , $sel:dumpEndStates:Config :: Bool
dumpEndStates = Bool
False
  , $sel:debug:Config :: Bool
debug = Bool
False
  , $sel:abstRefineArith:Config :: Bool
abstRefineArith = Bool
False
  , $sel:abstRefineMem:Config :: Bool
abstRefineMem   = Bool
False
  , $sel:dumpTrace:Config :: Bool
dumpTrace = Bool
False
  , $sel:numCexFuzz:Config :: Integer
numCexFuzz = Integer
10
  , $sel:onlyCexFuzz:Config :: Bool
onlyCexFuzz  = Bool
False
  }

-- Write to the console
class Monad m => TTY m where
  writeOutput :: Text -> m ()
  writeErr :: Text -> m ()

writeTraceDapp :: App m => DappInfo -> VM t RealWorld -> m ()
writeTraceDapp :: forall (m :: * -> *) (t :: VMType).
App m =>
DappInfo -> VM t RealWorld -> m ()
writeTraceDapp DappInfo
dapp VM t RealWorld
vm = do
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpTrace (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Text -> IO ()
T.writeFile String
"VM.trace" (DappInfo -> VM t RealWorld -> Text
forall (t :: VMType) s. DappInfo -> VM t s -> Text
showTraceTree DappInfo
dapp VM t RealWorld
vm)

writeTrace :: App m => VM t RealWorld -> m ()
writeTrace :: forall (m :: * -> *) (t :: VMType). App m => VM t RealWorld -> m ()
writeTrace VM t RealWorld
vm = do
  Config
conf <- m Config
forall (m :: * -> *). ReadConfig m => m Config
readConfig
  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Config
conf.dumpTrace (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
"VM.trace" (Forest Trace -> String
forall a. Show a => a -> String
show (Forest Trace -> String) -> Forest Trace -> String
forall a b. (a -> b) -> a -> b
$ VM t RealWorld -> Forest Trace
forall (t :: VMType) s. VM t s -> Forest Trace
traceForest VM t RealWorld
vm)


-- IO Interpretation -------------------------------------------------------------------------------


newtype Env = Env
  { Env -> Config
config :: Config
  }

defaultEnv :: Env
defaultEnv :: Env
defaultEnv = Env { $sel:config:Env :: Config
config = Config
defaultConfig }

instance Monad m => ReadConfig (ReaderT Env m) where
  readConfig :: ReaderT Env m Config
readConfig = do
    Env
e <- ReaderT Env m Env
forall r (m :: * -> *). MonadReader r m => m r
ask
    Config -> ReaderT Env m Config
forall a. a -> ReaderT Env m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
e.config

instance (Monad m, MonadIO m) => TTY (ReaderT Env m) where
  writeOutput :: Text -> ReaderT Env m ()
writeOutput Text
txt = IO () -> ReaderT Env m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env m ()) -> IO () -> ReaderT Env m ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn Text
txt
  writeErr :: Text -> ReaderT Env m ()
writeErr Text
txt = IO () -> ReaderT Env m ()
forall a. IO a -> ReaderT Env m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT Env m ()) -> IO () -> ReaderT Env m ()
forall a b. (a -> b) -> a -> b
$ Handle -> Text -> IO ()
T.hPutStr Handle
stderr Text
txt

runEnv :: Env -> ReaderT Env m a -> m a
runEnv :: forall (m :: * -> *) a. Env -> ReaderT Env m a -> m a
runEnv Env
e ReaderT Env m a
a = ReaderT Env m a -> Env -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Env m a
a Env
e


-- Helpful Aliases ---------------------------------------------------------------------------------


type App m = (MonadUnliftIO m, ReadConfig m, TTY m)

runApp :: ReaderT Env m a -> m a
runApp :: forall (m :: * -> *) a. ReaderT Env m a -> m a
runApp = Env -> ReaderT Env m a -> m a
forall (m :: * -> *) a. Env -> ReaderT Env m a -> m a
runEnv Env
defaultEnv