Skip to content

Commit abceb59

Browse files
goodlyrottenapplegithub-actions
goodlyrottenapple
and
github-actions
authored
Further contextual logging cleanup (#3906)
More tweaks and cleanup of the contextual logs including: * Remove monad logger from booster code fully and add an "always show" flag to simulate info logs that should be always used no matter the context filter (use sparingly!!). the flag is set when logging via `logMessage'` (perhaps need a different name?). Fixes #3867 * Switch abort analysis to using the JSON context logs. This includes translating the required context filters into the previously used `-l Abort` log level, as well as using the new `count-aborts` (#3911) utility. Fixes #3865 * Introduce new `failure,break` and `failure,continue` nested contexts, which are emitted based on whether we are evaluating functions or simplifications. * Improve ceil analysis contextual logs --------- Co-authored-by: github-actions <[email protected]>
1 parent 7ff00a1 commit abceb59

File tree

20 files changed

+735
-885
lines changed

20 files changed

+735
-885
lines changed

‎booster/library/Booster/CLOptions.hs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,6 +269,16 @@ levelToContext =
269269
[ [ctxt| booster|kore>smt |]
270270
]
271271
)
272+
,
273+
( "Aborts"
274+
,
275+
[ [ctxt| booster>function*|simplification*|rewrite*,detail |]
276+
, [ctxt| booster>function*|simplification*|rewrite*,abort |]
277+
, [ctxt| booster>function*|simplification*|rewrite*,match,abort |]
278+
, [ctxt| booster>function*|simplification*|rewrite*>failure,break |]
279+
, [ctxt| booster>failure,abort |]
280+
]
281+
)
272282
]
273283

274284
-- Partition provided log levels into standard and custom ones, and

‎booster/library/Booster/Definition/Ceil.hs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ import Control.DeepSeq (NFData)
2222
import Control.Monad (foldM)
2323
import Control.Monad.Extra (concatMapM)
2424
import Control.Monad.IO.Class (MonadIO (liftIO))
25-
import Control.Monad.Logger (MonadLoggerIO)
2625
import Control.Monad.Trans.Class (lift)
2726
import Control.Monad.Trans.Writer (runWriterT, tell)
2827
import Data.ByteString.Char8 (isPrefixOf)
@@ -75,7 +74,6 @@ instance Pretty ComputeCeilSummary where
7574

7675
computeCeilsDefinition ::
7776
LoggerMIO io =>
78-
MonadLoggerIO io =>
7977
Maybe LLVM.API ->
8078
KoreDefinition ->
8179
io (KoreDefinition, [ComputeCeilSummary])
@@ -93,7 +91,6 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
9391

9492
computeCeilRule ::
9593
LoggerMIO io =>
96-
MonadLoggerIO io =>
9794
Maybe LLVM.API ->
9895
KoreDefinition ->
9996
RewriteRule.RewriteRule "Rewrite" ->
@@ -147,7 +144,7 @@ computeCeilRule mllvm def [email protected]{lhs, requires, rhs, attribut
147144
| otherwise = pure $ Just p
148145
simplifyCeil _ other = pure $ Just other
149146

150-
computeCeil :: MonadLoggerIO io => Term -> EquationT io [Either Predicate Term]
147+
computeCeil :: LoggerMIO io => Term -> EquationT io [Either Predicate Term]
151148
computeCeil term@(SymbolApplication symbol _ args)
152149
| symbol.attributes.symbolType
153150
/= Booster.Definition.Attributes.Base.Function Booster.Definition.Attributes.Base.Partial =

‎booster/library/Booster/JsonRpc.hs

Lines changed: 37 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ import Control.Exception qualified as Exception
2121
import Control.Monad
2222
import Control.Monad.Extra (whenJust)
2323
import Control.Monad.IO.Class
24-
import Control.Monad.Logger.CallStack qualified as Log
2524
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
2625
import Crypto.Hash (SHA256 (..), hashWith)
2726
import Data.Bifunctor (second)
@@ -96,7 +95,6 @@ import Kore.Syntax.Json.Types qualified as Syntax
9695
respond ::
9796
forall m.
9897
LoggerMIO m =>
99-
Log.MonadLoggerIO m =>
10098
MVar ServerState ->
10199
Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res)
102100
respond stateVar =
@@ -123,10 +121,6 @@ respond stateVar =
123121
unless (null unsupported) $ do
124122
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
125123
logMessage ("ignoring unsupported predicate parts" :: Text)
126-
Log.logWarnNS
127-
"booster"
128-
"Execute: ignoring unsupported predicate parts"
129-
130124
let cutPoints = fromMaybe [] req.cutPointRules
131125
terminals = fromMaybe [] req.terminalRules
132126
mbDepth = fmap RpcTypes.getNat req.maxDepth
@@ -235,10 +229,6 @@ respond stateVar =
235229
Left patternErrors -> do
236230
forM_ patternErrors $ \patternError ->
237231
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
238-
Log.logOtherNS
239-
"booster"
240-
(Log.LevelOther "ErrorDetails")
241-
(prettyPattern req.state.term)
242232
pure $
243233
Left $
244234
RpcError.backendError $
@@ -249,9 +239,6 @@ respond stateVar =
249239
unless (null unsupported) $ do
250240
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
251241
logMessage ("ignoring unsupported predicate parts" :: Text)
252-
Log.logWarnNS
253-
"booster"
254-
"Simplify: ignoring unsupported predicate parts"
255242
-- apply the given substitution before doing anything else
256243
let substPat =
257244
Pattern
@@ -284,9 +271,6 @@ respond stateVar =
284271
unless (null ps.unsupported) $ do
285272
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
286273
logMessage ("ignoring unsupported predicate parts" :: Text)
287-
Log.logWarnNS
288-
"booster"
289-
"Simplify: ignoring unsupported predicate parts"
290274
-- apply the given substitution before doing anything else
291275
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
292276
withContext "constraint" $
@@ -321,7 +305,8 @@ respond stateVar =
321305
pure $ second mkSimplifyResponse result
322306
RpcTypes.GetModel req -> withModule req._module $ \case
323307
(_, _, Nothing) -> do
324-
Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
308+
withContext "get-model" $
309+
logMessage' ("get-model request, not supported without SMT solver" :: Text)
325310
pure $ Left RpcError.notImplemented
326311
(def, _, Just smtOptions) -> do
327312
let internalised =
@@ -330,64 +315,48 @@ respond stateVar =
330315
case internalised of
331316
Left patternErrors -> do
332317
forM_ patternErrors $ \patternError ->
333-
Log.logErrorNS "booster" $
334-
"Error internalising cterm: " <> pack (show patternError)
335-
Log.logOtherNS
336-
"booster"
337-
(Log.LevelOther "ErrorDetails")
338-
(prettyPattern req.state.term)
318+
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
339319
pure $
340320
Left $
341321
RpcError.backendError $
342322
RpcError.CouldNotVerifyPattern $
343323
map patternErrorToRpcError patternErrors
344324
-- various predicates obtained
345325
Right things -> do
346-
Log.logInfoNS "booster" "get-model request"
347326
-- term and predicates were sent. Only work on predicates
348327
(boolPs, suppliedSubst) <-
349328
case things of
350329
TermAndPredicates pat substitution unsupported -> do
351-
Log.logWarnNS
352-
"booster"
353-
"get-model ignores supplied terms and only checks predicates"
354-
Log.logOtherNS
355-
"booster"
356-
(Log.LevelOther "ErrorDetails")
357-
(renderText $ pretty pat.term)
330+
withContext "get-model" $
331+
logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
332+
358333
unless (null unsupported) $ do
359-
Log.logWarnNS
360-
"booster"
361-
" get-model: ignoring unsupported predicates"
362-
Log.logOtherNS
363-
"booster"
364-
(Log.LevelOther "ErrorDetails")
365-
(Text.unlines $ map prettyPattern unsupported)
334+
withContext "get-model" $ do
335+
logMessage' ("ignoring unsupported predicates" :: Text)
336+
withContext "detail" $
337+
logMessage (Text.unwords $ map prettyPattern unsupported)
366338
pure (Set.toList pat.constraints, substitution)
367339
Predicates ps -> do
368340
unless (null ps.ceilPredicates && null ps.unsupported) $ do
369-
Log.logWarnNS
370-
"booster"
371-
"get-model: ignoring supplied ceils and unsupported predicates"
372-
Log.logOtherNS
373-
"booster"
374-
(Log.LevelOther "ErrorDetails")
375-
( Text.unlines $
376-
map
377-
(renderText . ("#Ceil:" <>) . pretty)
378-
(Set.toList ps.ceilPredicates)
379-
<> map prettyPattern ps.unsupported
380-
)
341+
withContext "get-model" $ do
342+
logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
343+
withContext "detail" $
344+
logMessage
345+
( Text.unlines $
346+
map
347+
(renderText . ("#Ceil:" <>) . pretty)
348+
(Set.toList ps.ceilPredicates)
349+
<> map prettyPattern ps.unsupported
350+
)
381351
pure (Set.toList ps.boolPredicates, ps.substitution)
382352

383353
smtResult <-
384354
if null boolPs && Map.null suppliedSubst
385355
then do
386356
-- as per spec, no predicate, no answer
387-
Log.logOtherNS
388-
"booster"
389-
(Log.LevelOther "SMT")
390-
"No predicates or substitutions given, returning Unknown"
357+
withContext "get-model" $
358+
withContext "smt" $
359+
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
391360
pure $ Left SMT.Unknown
392361
else do
393362
solver <- SMT.initSolver def smtOptions
@@ -396,8 +365,10 @@ respond stateVar =
396365
case result of
397366
Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
398367
Right response -> pure response
399-
Log.logOtherNS "booster" (Log.LevelOther "SMT") $
400-
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
368+
withContext "get-model" $
369+
withContext "smt" $
370+
logMessage $
371+
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
401372
pure . Right . RpcTypes.GetModel $ case smtResult of
402373
Left SMT.Unsat ->
403374
RpcTypes.GetModelResult
@@ -449,15 +420,15 @@ respond stateVar =
449420

450421
case (internalised req.antecedent.term, internalised req.consequent.term) of
451422
(Left patternError, _) -> do
452-
Log.logDebug $ "Error internalising antecedent" <> Text.pack (show patternError)
423+
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
453424
pure $
454425
Left $
455426
RpcError.backendError $
456427
RpcError.CouldNotVerifyPattern
457428
[ patternErrorToRpcError patternError
458429
]
459430
(_, Left patternError) -> do
460-
Log.logDebug $ "Error internalising consequent" <> Text.pack (show patternError)
431+
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
461432
pure $
462433
Left $
463434
RpcError.backendError $
@@ -466,19 +437,16 @@ respond stateVar =
466437
]
467438
(Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
468439
unless (null unsupportedL && null unsupportedR) $ do
469-
Log.logWarnNS
470-
"booster"
471-
"Implies: aborting due to unsupported predicate parts"
440+
logMessage'
441+
("aborting due to unsupported predicate parts" :: Text)
472442
unless (null unsupportedL) $
473-
Log.logOtherNS
474-
"booster"
475-
(Log.LevelOther "ErrorDetails")
476-
(Text.unlines $ map prettyPattern unsupportedL)
443+
withContext "detail" $
444+
logMessage
445+
(Text.unwords $ map prettyPattern unsupportedL)
477446
unless (null unsupportedR) $
478-
Log.logOtherNS
479-
"booster"
480-
(Log.LevelOther "ErrorDetails")
481-
(Text.unlines $ map prettyPattern unsupportedR)
447+
withContext "detail" $
448+
logMessage
449+
(Text.unwords $ map prettyPattern unsupportedR)
482450
let
483451
-- apply the given substitution before doing anything else
484452
substPatL =
@@ -574,16 +542,13 @@ handleSmtError = JsonRpcHandler $ \case
574542
SMT.GeneralSMTError err -> runtimeError "problem" err
575543
SMT.SMTTranslationError err -> runtimeError "translation" err
576544
SMT.SMTSolverUnknown reason premises preds -> do
577-
Log.logErrorNS "booster" ("SMT returned `Unknown' with reason " <> reason)
578-
579545
let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
580546
externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
581547
allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
582548
pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
583549
where
584550
runtimeError prefix err = do
585551
let msg = "SMT " <> prefix <> ": " <> err
586-
Log.logErrorNS "booster" msg
587552
pure $ RpcError.runtimeError msg
588553

589554
data ServerState = ServerState

‎booster/library/Booster/Log.hs

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,10 @@ import Booster.Pattern.Base (
4343
import Booster.Prettyprinter (renderOneLineText)
4444
import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
4545
import Booster.Syntax.Json.Externalise (externaliseTerm)
46+
import Booster.Util (Flag (..))
4647
import Kore.JsonRpc.Types (rpcJsonConfig)
4748
import Kore.Util (showHashHex)
49+
import UnliftIO (MonadUnliftIO)
4850

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

@@ -58,7 +60,7 @@ instance IsString LogContext where
5860
fromString = LogContext . pack
5961

6062
data LogMessage where
61-
LogMessage :: ToLogFormat a => [LogContext] -> a -> LogMessage
63+
LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [LogContext] -> a -> LogMessage
6264

6365
class MonadIO m => LoggerMIO m where
6466
getLogger :: m (Logger LogMessage)
@@ -85,13 +87,22 @@ instance MonadIO m => LoggerMIO (Control.Monad.Logger.NoLoggingT m) where
8587
logMessage :: (LoggerMIO m, ToLogFormat a) => a -> m ()
8688
logMessage a =
8789
getLogger >>= \case
88-
(Logger l) -> liftIO $ l $ LogMessage [] a
90+
(Logger l) -> liftIO $ l $ LogMessage (Flag False) [] a
91+
92+
{- Log message which is always shown even when context filters are applied -}
93+
logMessage' :: (LoggerMIO m, ToLogFormat a) => a -> m ()
94+
logMessage' a =
95+
getLogger >>= \case
96+
(Logger l) -> liftIO $ l $ LogMessage (Flag True) [] a
8997

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

93101
withContext :: LoggerMIO m => LogContext -> m a -> m a
94-
withContext c = withLogger (\(Logger l) -> Logger $ l . (\(LogMessage ctxt m) -> LogMessage (c : ctxt) m))
102+
withContext c =
103+
withLogger
104+
( \(Logger l) -> Logger $ l . (\(LogMessage alwaysShown ctxt m) -> LogMessage alwaysShown (c : ctxt) m)
105+
)
95106

96107
newtype TermCtxt = TermCtxt Int
97108

@@ -174,14 +185,15 @@ newtype LoggerT m a = LoggerT {unLoggerT :: ReaderT (Logger LogMessage) m a}
174185
, MonadIO
175186
, Control.Monad.Logger.MonadLogger
176187
, Control.Monad.Logger.MonadLoggerIO
188+
, MonadUnliftIO
177189
)
178190

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

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

193205
jsonLogger :: (Control.Monad.Logger.LogStr -> IO ()) -> Logger LogMessage
194-
jsonLogger l = Logger $ \(LogMessage ctxts msg) ->
206+
jsonLogger l = Logger $ \(LogMessage _ ctxts msg) ->
195207
let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts
196208
in liftIO $
197209
l $

0 commit comments

Comments
 (0)