Skip to content

Commit 538d079

Browse files
jbertholdjberthold
authored
Add details to evaluation aborts that cause warnings (#3851)
For warnings during evaluation/simplification, the warning message advises users to use a certain log context. This PR changes the recommended log context to `*abort*detail`, for which informative details have been added in all call sites of `logWarn`. At the same time, the warning about too many iterations was duplicated in the `Rewrite` module, and was therefore downgraded to `Simplify` level there. Fixes #3849
1 parent eb0ec76 commit 538d079

File tree

2 files changed

+44
-37
lines changed

2 files changed

+44
-37
lines changed

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 37 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,6 @@ module Booster.Pattern.ApplyEquations (
2929
simplifyConstraint,
3030
simplifyConstraints,
3131
SimplifierCache,
32-
logWarn,
3332
) where
3433

3534
import Control.Applicative (Alternative (..))
@@ -384,16 +383,17 @@ fromCache tag t = eqState $ Map.lookup t <$> gets (select tag . (.cache))
384383

385384
logWarn :: MonadLogger m => Text -> m ()
386385
logWarn msg =
387-
logWarnNS "booster" $ msg <> " For more details, enable context logging '--log-context \"*abort\"'"
386+
logWarnNS "booster" $
387+
msg <> " For more details, enable context logging '--log-context \"*abort*detail\"'"
388388

389389
checkForLoop :: MonadLoggerIO io => Term -> EquationT io ()
390390
checkForLoop t = do
391391
EquationState{termStack} <- getState
392392
whenJust (Seq.elemIndexL t termStack) $ \i -> do
393-
withContext "abort" $
393+
withContext "abort" . withContext "detail" $
394394
logMessage $
395395
renderOneLineText $
396-
"Equation loop:"
396+
"Equation loop detected:"
397397
<+> hsep
398398
( intersperse "," $
399399
map (\(Term attrs _) -> "term" <+> pretty (showHashHex attrs.hash)) $
@@ -451,9 +451,14 @@ iterateEquations direction preference startTerm = do
451451
checkCounter counter = do
452452
config <- getConfig
453453
when (counter > config.maxRecursion) $ do
454-
let msg =
455-
"Recursion limit exceeded. The limit can be increased by restarting the server with '--equation-max-recursion N'."
456-
withContext "abort" $ logMessage msg
454+
let msg, details :: Text
455+
msg =
456+
"Recursion limit exceeded. The limit can be increased by \
457+
\ restarting the server with '--equation-max-recursion N'."
458+
details =
459+
"Recursion limit exceeded. \
460+
\Previous \"term*detail\" messages show the terms involved."
461+
withContext "abort" . withContext "detail" $ logMessage details
457462
logWarn msg
458463
throw . TooManyRecursions . (.recursionStack) =<< getState
459464

@@ -465,10 +470,10 @@ iterateEquations direction preference startTerm = do
465470
currentCount <- countSteps
466471
when (coerce currentCount > config.maxIterations) $ do
467472
let msg =
468-
renderOneLineText $
469-
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
470-
withContext "abort" $ logMessage msg
471-
logWarn msg
473+
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
474+
withContext "abort" . withContext "detail" . logMessage . renderOneLineText $
475+
msg <+> "Final term:" <+> pretty currentTerm
476+
logWarn $ renderOneLineText msg
472477
throw $
473478
TooManyIterations currentCount startTerm currentTerm
474479
pushTerm currentTerm
@@ -498,14 +503,16 @@ llvmSimplify term = do
498503
where
499504
evalLlvm definition api cb t@(Term attributes _)
500505
| attributes.isEvaluated = pure t
501-
| isConcrete t && attributes.canBeEvaluated = do
506+
| isConcrete t && attributes.canBeEvaluated = withContext "llvm" $ do
502507
LLVM.simplifyTerm api definition t (sortOfTerm t)
503508
>>= \case
504509
Left (LlvmError e) -> do
505-
withContext "llvm" $ withContext "abort" $ logMessage $ Text.decodeUtf8 e
506-
logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e <> "."
510+
let msg = "LLVM backend error detected: " <> Text.decodeUtf8 e
511+
details = msg <> " while evaluating " <> renderOneLineText (pretty t)
512+
withContext "abort" . withContext "detail" $ logMessage details
513+
logWarn msg
507514
throw $ UndefinedTerm t $ LlvmError e
508-
Right result -> withContext "llvm" $ do
515+
Right result -> do
509516
when (result /= t) $ do
510517
setChanged
511518
withContext "success" $
@@ -693,12 +700,15 @@ applyHooksAndEquations pref term = do
693700
case term of
694701
SymbolApplication sym _sorts args
695702
| Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do
696-
withContext (LogContext $ "hook " <> maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook)
697-
$ either
698-
(\e -> withContext "abort" (logMessage e) >> logWarn e >> throw (InternalError e))
699-
checkChanged
700-
. runExcept
701-
$ hook args
703+
let hookName = maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook
704+
onError e = do
705+
withContext "abort" . withContext "detail" . logMessage $
706+
e <> " while evaluating " <> renderOneLineText (pretty term)
707+
logWarn e
708+
throw (InternalError e)
709+
withContext (LogContext $ "hook " <> hookName) $
710+
either onError checkChanged $
711+
runExcept (hook args)
702712
_other -> pure Nothing
703713

704714
-- for the (unlikely) case that a built-in reproduces itself, we
@@ -1074,8 +1084,12 @@ simplifyConstraint' recurseIntoEvalBool = \case
10741084
withContext "llvm" $
10751085
LLVM.simplifyBool api t >>= \case
10761086
Left (LlvmError e) -> do
1077-
withContext "abort" $ logMessage $ Text.decodeUtf8 e
1078-
logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e <> "."
1087+
let msg =
1088+
"LLVM backend error detected: " <> Text.decodeUtf8 e
1089+
details =
1090+
msg <> " while evaluating " <> renderOneLineText (pretty t)
1091+
withContext "abort" . withContext "detail" $ logMessage details
1092+
logWarn msg
10791093
throw $ UndefinedTerm t $ LlvmError e
10801094
Right res -> do
10811095
let result =

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -740,21 +740,14 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
740740
logSimplify "Term is undefined, pruning"
741741
emitRewriteTrace $ RewriteSimplified [] (Just r)
742742
pure Nothing
743-
-- NB any errors here might be caused by simplifying one
744-
-- of the constraints, so we cannot use partial results
745-
-- and have to return the original on errors.
746-
Left r@(TooManyIterations n start result) -> do
747-
ApplyEquations.logWarn $ "Simplification unable to finish in " <> prettyText n <> " steps."
748-
logOtherNS
749-
"booster"
750-
(LevelOther "ErrorDetails")
751-
( Text.unlines
752-
[ "Start term: " <> prettyText start
753-
, "End term: " <> prettyText result
754-
]
755-
)
756-
-- could output term before and after at debug or custom log level
743+
Left r@(TooManyIterations n _start _result) -> do
744+
logSimplify $
745+
"Unable to simplify in " <> Text.pack (show n) <> " iterations, returning original"
746+
-- warning has been printed inside ApplyEquation.evaluatePattern
757747
emitRewriteTrace $ RewriteSimplified [] (Just r)
748+
-- NB start/result in this error are terms and might come
749+
-- from simplifying one of the constraints. Therefore, the
750+
-- original pattern must be returned.
758751
pure $ Just p
759752
Left r@(EquationLoop (t : ts)) -> do
760753
logError "Equation evaluation loop"

0 commit comments

Comments
 (0)