{-# 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)
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
, 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
}
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)
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
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