Skip to content

Further contextual logging cleanup #3906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 22 commits into from
Jun 4, 2024
Merged

Further contextual logging cleanup #3906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
e2f08d6
Further contextual logging cleanup
goodlyrottenapple May 28, 2024
445c2ec
Format with fourmolu
invalid-email-address May 28, 2024
12063c7
merge master
goodlyrottenapple May 30, 2024
48450b4
Format with fourmolu
invalid-email-address May 30, 2024
84faeec
fix dev-tools
goodlyrottenapple May 30, 2024
3659b4e
cleanup
goodlyrottenapple May 31, 2024
2dc39b1
add rule detail to abort logging to be able to extract the rule labels
goodlyrottenapple May 31, 2024
c8fec60
Merge branch 'master' into sam/log-cleanup
goodlyrottenapple Jun 3, 2024
f315e4b
Merge branch 'master' into sam/log-cleanup
goodlyrottenapple Jun 3, 2024
7a955de
merge master
goodlyrottenapple Jun 3, 2024
c570d2a
hlint
goodlyrottenapple Jun 3, 2024
bc84f01
switch the booster analysus script to context logs
goodlyrottenapple Jun 3, 2024
adac16d
merge master
goodlyrottenapple Jun 4, 2024
553181e
merge master
goodlyrottenapple Jun 4, 2024
ed218f2
update failur contexts in docs
goodlyrottenapple Jun 4, 2024
0f3c702
tweak
goodlyrottenapple Jun 4, 2024
433f1bb
update golden files + tweak booster analysis script
goodlyrottenapple Jun 4, 2024
3bc0251
cleanup
goodlyrottenapple Jun 4, 2024
5ba358a
merge master
goodlyrottenapple Jun 4, 2024
b6b4f13
cleanup
goodlyrottenapple Jun 4, 2024
b7a1a07
cleanup
goodlyrottenapple Jun 4, 2024
3f126e2
remove redundant import
goodlyrottenapple Jun 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions booster/library/Booster/CLOptions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -269,6 +269,16 @@ levelToContext =
[ [ctxt| booster|kore>smt |]
]
)
,
( "Aborts"
,
[ [ctxt| booster>function*|simplification*|rewrite*,detail |]
, [ctxt| booster>function*|simplification*|rewrite*,abort |]
, [ctxt| booster>function*|simplification*|rewrite*,match,abort |]
, [ctxt| booster>function*|simplification*|rewrite*>failure,break |]
, [ctxt| booster>failure,abort |]
]
)
]

-- Partition provided log levels into standard and custom ones, and
Expand Down
5 changes: 1 addition & 4 deletions booster/library/Booster/Definition/Ceil.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ import Control.DeepSeq (NFData)
import Control.Monad (foldM)
import Control.Monad.Extra (concatMapM)
import Control.Monad.IO.Class (MonadIO (liftIO))
import Control.Monad.Logger (MonadLoggerIO)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Writer (runWriterT, tell)
import Data.ByteString.Char8 (isPrefixOf)
Expand Down Expand Up @@ -75,7 +74,6 @@ instance Pretty ComputeCeilSummary where

computeCeilsDefinition ::
LoggerMIO io =>
MonadLoggerIO io =>
Maybe LLVM.API ->
KoreDefinition ->
io (KoreDefinition, [ComputeCeilSummary])
Expand All @@ -93,7 +91,6 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do

computeCeilRule ::
LoggerMIO io =>
MonadLoggerIO io =>
Maybe LLVM.API ->
KoreDefinition ->
RewriteRule.RewriteRule "Rewrite" ->
Expand Down Expand Up @@ -147,7 +144,7 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
| otherwise = pure $ Just p
simplifyCeil _ other = pure $ Just other

computeCeil :: MonadLoggerIO io => Term -> EquationT io [Either Predicate Term]
computeCeil :: LoggerMIO io => Term -> EquationT io [Either Predicate Term]
computeCeil term@(SymbolApplication symbol _ args)
| symbol.attributes.symbolType
/= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =
Expand Down
109 changes: 37 additions & 72 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ import Control.Exception qualified as Exception
import Control.Monad
import Control.Monad.Extra (whenJust)
import Control.Monad.IO.Class
import Control.Monad.Logger.CallStack qualified as Log
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
import Crypto.Hash (SHA256 (..), hashWith)
import Data.Bifunctor (second)
Expand Down Expand Up @@ -96,7 +95,6 @@ import Kore.Syntax.Json.Types qualified as Syntax
respond ::
forall m.
LoggerMIO m =>
Log.MonadLoggerIO m =>
MVar ServerState ->
Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res)
respond stateVar =
Expand All @@ -123,10 +121,6 @@ respond stateVar =
unless (null unsupported) $ do
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
logMessage ("ignoring unsupported predicate parts" :: Text)
Log.logWarnNS
"booster"
"Execute: ignoring unsupported predicate parts"

let cutPoints = fromMaybe [] req.cutPointRules
terminals = fromMaybe [] req.terminalRules
mbDepth = fmap RpcTypes.getNat req.maxDepth
Expand Down Expand Up @@ -235,10 +229,6 @@ respond stateVar =
Left patternErrors -> do
forM_ patternErrors $ \patternError ->
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(prettyPattern req.state.term)
pure $
Left $
RpcError.backendError $
Expand All @@ -249,9 +239,6 @@ respond stateVar =
unless (null unsupported) $ do
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
logMessage ("ignoring unsupported predicate parts" :: Text)
Log.logWarnNS
"booster"
"Simplify: ignoring unsupported predicate parts"
-- apply the given substitution before doing anything else
let substPat =
Pattern
Expand Down Expand Up @@ -284,9 +271,6 @@ respond stateVar =
unless (null ps.unsupported) $ do
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
logMessage ("ignoring unsupported predicate parts" :: Text)
Log.logWarnNS
"booster"
"Simplify: ignoring unsupported predicate parts"
-- apply the given substitution before doing anything else
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
withContext "constraint" $
Expand Down Expand Up @@ -321,7 +305,8 @@ respond stateVar =
pure $ second mkSimplifyResponse result
RpcTypes.GetModel req -> withModule req._module $ \case
(_, _, Nothing) -> do
Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
withContext "get-model" $
logMessage' ("get-model request, not supported without SMT solver" :: Text)
pure $ Left RpcError.notImplemented
(def, _, Just smtOptions) -> do
let internalised =
Expand All @@ -330,64 +315,48 @@ respond stateVar =
case internalised of
Left patternErrors -> do
forM_ patternErrors $ \patternError ->
Log.logErrorNS "booster" $
"Error internalising cterm: " <> pack (show patternError)
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(prettyPattern req.state.term)
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern $
map patternErrorToRpcError patternErrors
-- various predicates obtained
Right things -> do
Log.logInfoNS "booster" "get-model request"
-- term and predicates were sent. Only work on predicates
(boolPs, suppliedSubst) <-
case things of
TermAndPredicates pat substitution unsupported -> do
Log.logWarnNS
"booster"
"get-model ignores supplied terms and only checks predicates"
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(renderText $ pretty pat.term)
withContext "get-model" $
logMessage' ("ignoring supplied terms and only checking predicates" :: Text)

unless (null unsupported) $ do
Log.logWarnNS
"booster"
" get-model: ignoring unsupported predicates"
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(Text.unlines $ map prettyPattern unsupported)
withContext "get-model" $ do
logMessage' ("ignoring unsupported predicates" :: Text)
withContext "detail" $
logMessage (Text.unwords $ map prettyPattern unsupported)
pure (Set.toList pat.constraints, substitution)
Predicates ps -> do
unless (null ps.ceilPredicates && null ps.unsupported) $ do
Log.logWarnNS
"booster"
"get-model: ignoring supplied ceils and unsupported predicates"
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
( Text.unlines $
map
(renderText . ("#Ceil:" <>) . pretty)
(Set.toList ps.ceilPredicates)
<> map prettyPattern ps.unsupported
)
withContext "get-model" $ do
logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
withContext "detail" $
logMessage
( Text.unlines $
map
(renderText . ("#Ceil:" <>) . pretty)
(Set.toList ps.ceilPredicates)
<> map prettyPattern ps.unsupported
)
pure (Set.toList ps.boolPredicates, ps.substitution)

smtResult <-
if null boolPs && Map.null suppliedSubst
then do
-- as per spec, no predicate, no answer
Log.logOtherNS
"booster"
(Log.LevelOther "SMT")
"No predicates or substitutions given, returning Unknown"
withContext "get-model" $
withContext "smt" $
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
pure $ Left SMT.Unknown
else do
solver <- SMT.initSolver def smtOptions
Expand All @@ -396,8 +365,10 @@ respond stateVar =
case result of
Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
Right response -> pure response
Log.logOtherNS "booster" (Log.LevelOther "SMT") $
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
withContext "get-model" $
withContext "smt" $
logMessage $
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
pure . Right . RpcTypes.GetModel $ case smtResult of
Left SMT.Unsat ->
RpcTypes.GetModelResult
Expand Down Expand Up @@ -449,15 +420,15 @@ respond stateVar =

case (internalised req.antecedent.term, internalised req.consequent.term) of
(Left patternError, _) -> do
Log.logDebug $ "Error internalising antecedent" <> Text.pack (show patternError)
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(_, Left patternError) -> do
Log.logDebug $ "Error internalising consequent" <> Text.pack (show patternError)
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
pure $
Left $
RpcError.backendError $
Expand All @@ -466,19 +437,16 @@ respond stateVar =
]
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
unless (null unsupportedL && null unsupportedR) $ do
Log.logWarnNS
"booster"
"Implies: aborting due to unsupported predicate parts"
logMessage'
("aborting due to unsupported predicate parts" :: Text)
unless (null unsupportedL) $
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(Text.unlines $ map prettyPattern unsupportedL)
withContext "detail" $
logMessage
(Text.unwords $ map prettyPattern unsupportedL)
unless (null unsupportedR) $
Log.logOtherNS
"booster"
(Log.LevelOther "ErrorDetails")
(Text.unlines $ map prettyPattern unsupportedR)
withContext "detail" $
logMessage
(Text.unwords $ map prettyPattern unsupportedR)
let
-- apply the given substitution before doing anything else
substPatL =
Expand Down Expand Up @@ -574,16 +542,13 @@ handleSmtError = JsonRpcHandler $ \case
SMT.GeneralSMTError err -> runtimeError "problem" err
SMT.SMTTranslationError err -> runtimeError "translation" err
SMT.SMTSolverUnknown reason premises preds -> do
Log.logErrorNS "booster" ("SMT returned `Unknown' with reason " <> reason)

let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
where
runtimeError prefix err = do
let msg = "SMT " <> prefix <> ": " <> err
Log.logErrorNS "booster" msg
pure $ RpcError.runtimeError msg

data ServerState = ServerState
Expand Down
22 changes: 17 additions & 5 deletions booster/library/Booster/Log.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,10 @@ import Booster.Pattern.Base (
import Booster.Prettyprinter (renderOneLineText)
import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
import Booster.Syntax.Json.Externalise (externaliseTerm)
import Booster.Util (Flag (..))
import Kore.JsonRpc.Types (rpcJsonConfig)
import Kore.Util (showHashHex)
import UnliftIO (MonadUnliftIO)

newtype Logger a = Logger (a -> IO ())

Expand All @@ -58,7 +60,7 @@ instance IsString LogContext where
fromString = LogContext . pack

data LogMessage where
LogMessage :: ToLogFormat a => [LogContext] -> a -> LogMessage
LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [LogContext] -> a -> LogMessage

class MonadIO m => LoggerMIO m where
getLogger :: m (Logger LogMessage)
Expand All @@ -85,13 +87,22 @@ instance MonadIO m => LoggerMIO (Control.Monad.Logger.NoLoggingT m) where
logMessage :: (LoggerMIO m, ToLogFormat a) => a -> m ()
logMessage a =
getLogger >>= \case
(Logger l) -> liftIO $ l $ LogMessage [] a
(Logger l) -> liftIO $ l $ LogMessage (Flag False) [] a

{- Log message which is always shown even when context filters are applied -}
logMessage' :: (LoggerMIO m, ToLogFormat a) => a -> m ()
logMessage' a =
getLogger >>= \case
(Logger l) -> liftIO $ l $ LogMessage (Flag True) [] a

logPretty :: (LoggerMIO m, Pretty a) => a -> m ()
logPretty = logMessage . renderOneLineText . pretty

withContext :: LoggerMIO m => LogContext -> m a -> m a
withContext c = withLogger (\(Logger l) -> Logger $ l . (\(LogMessage ctxt m) -> LogMessage (c : ctxt) m))
withContext c =
withLogger
( \(Logger l) -> Logger $ l . (\(LogMessage alwaysShown ctxt m) -> LogMessage alwaysShown (c : ctxt) m)
)

newtype TermCtxt = TermCtxt Int

Expand Down Expand Up @@ -174,14 +185,15 @@ newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a}
, MonadIO
, Control.Monad.Logger.MonadLogger
, Control.Monad.Logger.MonadLoggerIO
, MonadUnliftIO
)

instance MonadIO m => LoggerMIO (LoggerT m) where
getLogger = LoggerT ask
withLogger modL (LoggerT m) = LoggerT $ withReaderT modL m

textLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
textLogger l = Logger $ \(LogMessage ctxts msg) ->
textLogger l = Logger $ \(LogMessage _ ctxts msg) ->
let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts
in l $
"["
Expand All @@ -191,7 +203,7 @@ textLogger l = Logger $ \(LogMessage ctxts msg) ->
<> "\n"

jsonLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
jsonLogger l = Logger $ \(LogMessage ctxts msg) ->
jsonLogger l = Logger $ \(LogMessage _ ctxts msg) ->
let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts
in liftIO $
l $
Expand Down
Loading
Loading