{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Crux.Log (
Logs,
OutputConfig(..)
, outputHandle
, quiet
, CruxLogMessage(..)
, LogDoc(..)
, LogProofObligation(..)
, SayWhat(..)
, SayLevel(..)
, SupportsCruxLogMessage
, cruxLogMessageToSayWhat
, cruxLogTag
, logException
, logGoal
, logSimResult
, say
, sayCrux
, withCruxLogMessage
, output
, outputLn
, logToStd
) where
import Control.Exception ( SomeException, bracket_, )
import Control.Lens ( Getter, view )
import qualified Data.Aeson as JSON
import Data.Aeson.TH ( deriveToJSON )
import qualified Data.Text as T
import Data.Text.IO as TIO ( hPutStr, hPutStrLn )
import Data.Version ( Version, showVersion )
import Data.Word ( Word64 )
import GHC.Generics ( Generic )
import qualified Lumberjack as LJ
import Prettyprinter ( SimpleDocStream )
import Prettyprinter.Render.Text ( renderStrict )
import System.Console.ANSI
( Color(..), ColorIntensity(..), ConsoleIntensity(..), ConsoleLayer(..)
, SGR(..), hSetSGR )
import System.IO ( Handle, hPutStr, hPutStrLn )
import Crux.Types
( CruxSimulationResult, ProvedGoals, SayLevel(..), SayWhat(..) )
import Crux.Version ( version )
import Lang.Crucible.Backend ( ProofGoal(..), ProofObligation )
import What4.Expr.Builder ( ExprBuilder )
import What4.LabeledPred ( labeledPred, labeledPredMsg )
newtype LogDoc = LogDoc (SimpleDocStream ())
instance JSON.ToJSON LogDoc where
toJSON :: LogDoc -> Value
toJSON (LogDoc SimpleDocStream ()
doc) = Text -> Value
JSON.String (SimpleDocStream () -> Text
forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream ()
doc)
data LogProofObligation =
forall t st fs.
LogProofObligation (ProofObligation (ExprBuilder t st fs))
instance JSON.ToJSON LogProofObligation where
toJSON :: LogProofObligation -> Value
toJSON (LogProofObligation ProofObligation (ExprBuilder t st fs)
g) =
let
goal :: LabeledPred (Expr t BaseBoolType) SimError
goal = ProofGoal
(CrucibleAssumptions (Expr t))
(LabeledPred (Expr t BaseBoolType) SimError)
-> LabeledPred (Expr t BaseBoolType) SimError
forall asmp goal. ProofGoal asmp goal -> goal
proofGoal ProofObligation (ExprBuilder t st fs)
ProofGoal
(CrucibleAssumptions (Expr t))
(LabeledPred (Expr t BaseBoolType) SimError)
g
in
[Pair] -> Value
JSON.object [ Key
"labeledPred" Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
JSON..= Expr t BaseBoolType -> String
forall a. Show a => a -> String
show (Getting
(Expr t BaseBoolType)
(LabeledPred (Expr t BaseBoolType) SimError)
(Expr t BaseBoolType)
-> LabeledPred (Expr t BaseBoolType) SimError
-> Expr t BaseBoolType
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Expr t BaseBoolType)
(LabeledPred (Expr t BaseBoolType) SimError)
(Expr t BaseBoolType)
forall pred msg pred' (f :: * -> *).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred LabeledPred (Expr t BaseBoolType) SimError
goal)
, Key
"labeledPredMsg" Key -> String -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
JSON..= SimError -> String
forall a. Show a => a -> String
show (Getting
SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
-> LabeledPred (Expr t BaseBoolType) SimError -> SimError
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
SimError (LabeledPred (Expr t BaseBoolType) SimError) SimError
forall pred msg msg' (f :: * -> *).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg LabeledPred (Expr t BaseBoolType) SimError
goal)
]
data CruxLogMessage
= AttemptingProvingVCs
| Checking [FilePath]
| DisablingBranchCoverageRequiresPathSatisfiability
| DisablingProfilingIncompatibleWithPathSplitting
| EndedGoal Integer
| FoundCounterExample
| Help LogDoc
| PathsUnexplored Int
| ProofObligations [LogProofObligation]
| SimulationComplete
| SimulationTimedOut
| SkippingUnsatCoresBecauseMCSatEnabled
| StartedGoal Integer
| TotalPathsExplored Word64
| UnsupportedTimeoutFor String
| Version T.Text Version
deriving ((forall x. CruxLogMessage -> Rep CruxLogMessage x)
-> (forall x. Rep CruxLogMessage x -> CruxLogMessage)
-> Generic CruxLogMessage
forall x. Rep CruxLogMessage x -> CruxLogMessage
forall x. CruxLogMessage -> Rep CruxLogMessage x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxLogMessage -> Rep CruxLogMessage x
from :: forall x. CruxLogMessage -> Rep CruxLogMessage x
$cto :: forall x. Rep CruxLogMessage x -> CruxLogMessage
to :: forall x. Rep CruxLogMessage x -> CruxLogMessage
Generic)
$(deriveToJSON JSON.defaultOptions ''CruxLogMessage)
type SupportsCruxLogMessage msgs =
( ?injectCruxLogMessage :: CruxLogMessage -> msgs )
withCruxLogMessage ::
(SupportsCruxLogMessage CruxLogMessage => a) -> a
withCruxLogMessage :: forall a. (SupportsCruxLogMessage CruxLogMessage => a) -> a
withCruxLogMessage SupportsCruxLogMessage CruxLogMessage => a
a =
let ?injectCruxLogMessage = SupportsCruxLogMessage CruxLogMessage
CruxLogMessage -> CruxLogMessage
forall a. a -> a
id in a
SupportsCruxLogMessage CruxLogMessage => a
a
cruxLogTag :: T.Text
cruxLogTag :: Text
cruxLogTag = Text
"Crux"
cruxNoisily :: T.Text -> SayWhat
cruxNoisily :: Text -> SayWhat
cruxNoisily = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Noisily Text
cruxLogTag
cruxOK :: T.Text -> SayWhat
cruxOK :: Text -> SayWhat
cruxOK = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
OK Text
cruxLogTag
cruxSimply :: T.Text -> SayWhat
cruxSimply :: Text -> SayWhat
cruxSimply = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
cruxLogTag
cruxWarn :: T.Text -> SayWhat
cruxWarn :: Text -> SayWhat
cruxWarn = SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Warn Text
cruxLogTag
cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat
cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat
cruxLogMessageToSayWhat CruxLogMessage
AttemptingProvingVCs =
Text -> SayWhat
cruxSimply Text
"Attempting to prove verification conditions."
cruxLogMessageToSayWhat (Checking [String]
files) =
Text -> SayWhat
cruxNoisily (Text
"Checking " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " (String -> Text
T.pack (String -> Text) -> [String] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
files))
cruxLogMessageToSayWhat CruxLogMessage
DisablingBranchCoverageRequiresPathSatisfiability =
Text -> SayWhat
cruxWarn
Text
"Branch coverage requires enabling path satisfiability checking. Coverage measurement is disabled!"
cruxLogMessageToSayWhat CruxLogMessage
DisablingProfilingIncompatibleWithPathSplitting =
Text -> SayWhat
cruxWarn
Text
"Path splitting strategies are incompatible with Crucible profiling. Profiling is disabled!"
cruxLogMessageToSayWhat (EndedGoal {}) = SayWhat
SayNothing
cruxLogMessageToSayWhat CruxLogMessage
FoundCounterExample =
Text -> SayWhat
cruxOK Text
"Counterexample found, skipping remaining goals"
cruxLogMessageToSayWhat (Help (LogDoc SimpleDocStream ()
doc)) =
Text -> SayWhat
cruxOK (SimpleDocStream () -> Text
forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream ()
doc)
cruxLogMessageToSayWhat (PathsUnexplored Int
numberOfPaths) =
Text -> SayWhat
cruxWarn
( [Text] -> Text
T.unwords
[ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
numberOfPaths,
Text
"paths remaining not explored: program might not be fully verified"
]
)
cruxLogMessageToSayWhat (ProofObligations {}) = SayWhat
SayNothing
cruxLogMessageToSayWhat CruxLogMessage
SimulationComplete =
Text -> SayWhat
cruxNoisily Text
"Simulation complete."
cruxLogMessageToSayWhat CruxLogMessage
SimulationTimedOut =
Text -> SayWhat
cruxWarn
Text
"Simulation timed out! Program might not be fully verified!"
cruxLogMessageToSayWhat CruxLogMessage
SkippingUnsatCoresBecauseMCSatEnabled =
Text -> SayWhat
cruxWarn Text
"Warning: skipping unsat cores because MC-SAT is enabled."
cruxLogMessageToSayWhat (StartedGoal {}) = SayWhat
SayNothing
cruxLogMessageToSayWhat (TotalPathsExplored Word64
i) =
Text -> SayWhat
cruxSimply (Text
"Total paths explored: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Word64 -> String
forall a. Show a => a -> String
show Word64
i))
cruxLogMessageToSayWhat (UnsupportedTimeoutFor String
backend) =
Text -> SayWhat
cruxWarn
(String -> Text
T.pack (String
"Goal timeout requested but not supported by " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
backend))
cruxLogMessageToSayWhat (Version Text
nm Version
ver) =
Text -> SayWhat
cruxOK
( String -> Text
T.pack
( [String] -> String
unwords
[ String
"version: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
version String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
",",
Text -> String
T.unpack Text
nm,
String
"version: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (Version -> String
showVersion Version
ver)
]
)
)
say ::
Logs msgs =>
( ?injectMessage :: msg -> msgs ) =>
msg -> IO ()
say :: forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
say = LogAction IO msgs -> msgs -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (Getting (LogAction IO msgs) (OutputConfig msgs) (LogAction IO msgs)
-> OutputConfig msgs -> LogAction IO msgs
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (LogAction IO msgs) (OutputConfig msgs) (LogAction IO msgs)
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(LogAction IO msgs -> f (LogAction IO msgs))
-> OutputConfig msgs -> f (OutputConfig msgs)
logMsg Logs msgs
OutputConfig msgs
?outputConfig) (msgs -> IO ()) -> (msg -> msgs) -> msg -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ?injectMessage::msg -> msgs
msg -> msgs
?injectMessage
sayCrux ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxLogMessage -> IO ()
sayCrux :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
msg =
let ?injectMessage = SupportsCruxLogMessage msgs
?injectMessage::CruxLogMessage -> msgs
CruxLogMessage -> msgs
?injectCruxLogMessage in
CruxLogMessage -> IO ()
forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
say CruxLogMessage
msg
logException :: Logs msgs => SomeException -> IO ()
logException :: forall msgs. Logs msgs => SomeException -> IO ()
logException = LogAction IO SomeException -> SomeException -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> LogAction IO SomeException
forall msgs. OutputConfig msgs -> LogAction IO SomeException
_logExc Logs msgs
OutputConfig msgs
?outputConfig)
logSimResult :: Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult :: forall msgs. Logs msgs => Bool -> CruxSimulationResult -> IO ()
logSimResult Bool
showFailedGoals = LogAction IO CruxSimulationResult -> CruxSimulationResult -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
forall msgs.
OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
_logSimResult Logs msgs
OutputConfig msgs
?outputConfig Bool
showFailedGoals)
logGoal :: Logs msgs => ProvedGoals -> IO ()
logGoal :: forall msgs. Logs msgs => ProvedGoals -> IO ()
logGoal = LogAction IO ProvedGoals -> ProvedGoals -> IO ()
forall (m :: * -> *) msg. LogAction m msg -> msg -> m ()
LJ.writeLog (OutputConfig msgs -> LogAction IO ProvedGoals
forall msgs. OutputConfig msgs -> LogAction IO ProvedGoals
_logGoal Logs msgs
OutputConfig msgs
?outputConfig)
type Logs msgs = ( ?outputConfig :: OutputConfig msgs )
data OutputConfig msgs =
OutputConfig { forall msgs. OutputConfig msgs -> Handle
_outputHandle :: Handle
, forall msgs. OutputConfig msgs -> Bool
_quiet :: Bool
, forall msgs. OutputConfig msgs -> LogAction IO msgs
_logMsg :: LJ.LogAction IO msgs
, forall msgs. OutputConfig msgs -> LogAction IO SomeException
_logExc :: LJ.LogAction IO SomeException
, forall msgs.
OutputConfig msgs -> Bool -> LogAction IO CruxSimulationResult
_logSimResult :: Bool -> LJ.LogAction IO CruxSimulationResult
, forall msgs. OutputConfig msgs -> LogAction IO ProvedGoals
_logGoal :: LJ.LogAction IO ProvedGoals
}
outputHandle :: Getter (OutputConfig msgs) Handle
outputHandle :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Handle -> f Handle
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f Handle -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Handle -> f Handle
f (OutputConfig msgs -> Handle
forall msgs. OutputConfig msgs -> Handle
_outputHandle OutputConfig msgs
o)
quiet :: Getter (OutputConfig msgs) Bool
quiet :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Bool -> f Bool) -> OutputConfig msgs -> f (OutputConfig msgs)
quiet Bool -> f Bool
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f Bool -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f Bool
f (OutputConfig msgs -> Bool
forall msgs. OutputConfig msgs -> Bool
_quiet OutputConfig msgs
o)
logMsg :: Getter (OutputConfig msgs) (LJ.LogAction IO msgs)
logMsg :: forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(LogAction IO msgs -> f (LogAction IO msgs))
-> OutputConfig msgs -> f (OutputConfig msgs)
logMsg LogAction IO msgs -> f (LogAction IO msgs)
f OutputConfig msgs
o = OutputConfig msgs
o OutputConfig msgs -> f (LogAction IO msgs) -> f (OutputConfig msgs)
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LogAction IO msgs -> f (LogAction IO msgs)
f (OutputConfig msgs -> LogAction IO msgs
forall msgs. OutputConfig msgs -> LogAction IO msgs
_logMsg OutputConfig msgs
o)
logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec = \case
SayWhat SayLevel
lvl Text
frm Text
msg ->
let sayer :: Text -> IO ()
sayer = case SayLevel
lvl of
SayLevel
OK -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Green (Handle, Bool)
outSpec
SayLevel
Warn -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Yellow (Handle, Bool)
errSpec
SayLevel
Fail -> Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
Red (Handle, Bool)
errSpec
SayLevel
Simply -> (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
outSpec
SayLevel
Noisily -> (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
outSpec
colOut :: Color -> (Handle, Bool) -> Text -> IO ()
colOut Color
clr (Handle
hndl, Bool
True) Text
l =
do IO () -> IO () -> IO () -> IO ()
forall a b c. IO a -> IO b -> IO c -> IO c
bracket_
(Handle -> [SGR] -> IO ()
hSetSGR Handle
hndl [ ConsoleIntensity -> SGR
SetConsoleIntensity ConsoleIntensity
BoldIntensity
, ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
clr])
(Handle -> [SGR] -> IO ()
hSetSGR Handle
hndl [SGR
Reset])
(Handle -> Text -> IO ()
TIO.hPutStr Handle
hndl (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
frm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] ")
Handle -> Text -> IO ()
TIO.hPutStrLn Handle
hndl Text
l
colOut Color
_ hSpec :: (Handle, Bool)
hSpec@(Handle
_, Bool
False) Text
l = (Handle, Bool) -> Text -> IO ()
straightOut (Handle, Bool)
hSpec Text
l
straightOut :: (Handle, Bool) -> Text -> IO ()
straightOut (Handle
hndl, Bool
_) Text
l = do Handle -> Text -> IO ()
TIO.hPutStr Handle
hndl (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
frm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] "
Handle -> Text -> IO ()
TIO.hPutStrLn Handle
hndl Text
l
in (Text -> IO ()) -> [Text] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Text -> IO ()
sayer ([Text] -> IO ()) -> [Text] -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
msg
SayMore SayWhat
s1 SayWhat
s2 -> do (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec SayWhat
s1
(Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()
logToStd (Handle, Bool)
outSpec (Handle, Bool)
errSpec SayWhat
s2
SayWhat
SayNothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
output :: Logs msgs => String -> IO ()
output :: forall msgs. Logs msgs => String -> IO ()
output String
str = Handle -> String -> IO ()
System.IO.hPutStr (Getting Handle (OutputConfig msgs) Handle
-> OutputConfig msgs -> Handle
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Logs msgs
OutputConfig msgs
?outputConfig) String
str
outputLn :: Logs msgs => String -> IO ()
outputLn :: forall msgs. Logs msgs => String -> IO ()
outputLn String
str = Handle -> String -> IO ()
System.IO.hPutStrLn (Getting Handle (OutputConfig msgs) Handle
-> OutputConfig msgs -> Handle
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Handle (OutputConfig msgs) Handle
forall msgs (f :: * -> *).
(Contravariant f, Functor f) =>
(Handle -> f Handle) -> OutputConfig msgs -> f (OutputConfig msgs)
outputHandle Logs msgs
OutputConfig msgs
?outputConfig) String
str