Skip to content

Add details to evaluation aborts that cause warnings #3851

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 2 commits into from
May 7, 2024
Merged

Add details to evaluation aborts that cause warnings #3851

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
246a187
Add details to evaluation aborts that cause warnings
jberthold May 7, 2024
a76b162
Merge branch 'master' into 3849-add-detail-logs-for-warnings
jberthold May 7, 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
60 changes: 37 additions & 23 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ module Booster.Pattern.ApplyEquations (
simplifyConstraint,
simplifyConstraints,
SimplifierCache,
logWarn,
) where

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

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

checkForLoop :: MonadLoggerIO io => Term -> EquationT io ()
checkForLoop t = do
EquationState{termStack} <- getState
whenJust (Seq.elemIndexL t termStack) $ \i -> do
withContext "abort" $
withContext "abort" . withContext "detail" $
logMessage $
renderOneLineText $
"Equation loop:"
"Equation loop detected:"
<+> hsep
( intersperse "," $
map (\(Term attrs _) -> "term" <+> pretty (showHashHex attrs.hash)) $
Expand Down Expand Up @@ -451,9 +451,14 @@ iterateEquations direction preference startTerm = do
checkCounter counter = do
config <- getConfig
when (counter > config.maxRecursion) $ do
let msg =
"Recursion limit exceeded. The limit can be increased by restarting the server with '--equation-max-recursion N'."
withContext "abort" $ logMessage msg
let msg, details :: Text
msg =
"Recursion limit exceeded. The limit can be increased by \
\ restarting the server with '--equation-max-recursion N'."
details =
"Recursion limit exceeded. \
\Previous \"term*detail\" messages show the terms involved."
withContext "abort" . withContext "detail" $ logMessage details
logWarn msg
throw . TooManyRecursions . (.recursionStack) =<< getState

Expand All @@ -465,10 +470,10 @@ iterateEquations direction preference startTerm = do
currentCount <- countSteps
when (coerce currentCount > config.maxIterations) $ do
let msg =
renderOneLineText $
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
withContext "abort" $ logMessage msg
logWarn msg
"Unable to finish evaluation in" <+> pretty currentCount <+> "iterations."
withContext "abort" . withContext "detail" . logMessage . renderOneLineText $
msg <+> "Final term:" <+> pretty currentTerm
logWarn $ renderOneLineText msg
throw $
TooManyIterations currentCount startTerm currentTerm
pushTerm currentTerm
Expand Down Expand Up @@ -498,14 +503,16 @@ llvmSimplify term = do
where
evalLlvm definition api cb t@(Term attributes _)
| attributes.isEvaluated = pure t
| isConcrete t && attributes.canBeEvaluated = do
| isConcrete t && attributes.canBeEvaluated = withContext "llvm" $ do
LLVM.simplifyTerm api definition t (sortOfTerm t)
>>= \case
Left (LlvmError e) -> do
withContext "llvm" $ withContext "abort" $ logMessage $ Text.decodeUtf8 e
logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e <> "."
let msg = "LLVM backend error detected: " <> Text.decodeUtf8 e
details = msg <> " while evaluating " <> renderOneLineText (pretty t)
withContext "abort" . withContext "detail" $ logMessage details
logWarn msg
throw $ UndefinedTerm t $ LlvmError e
Right result -> withContext "llvm" $ do
Right result -> do
when (result /= t) $ do
setChanged
withContext "success" $
Expand Down Expand Up @@ -693,12 +700,15 @@ applyHooksAndEquations pref term = do
case term of
SymbolApplication sym _sorts args
| Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do
withContext (LogContext $ "hook " <> maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook)
$ either
(\e -> withContext "abort" (logMessage e) >> logWarn e >> throw (InternalError e))
checkChanged
. runExcept
$ hook args
let hookName = maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook
onError e = do
withContext "abort" . withContext "detail" . logMessage $
e <> " while evaluating " <> renderOneLineText (pretty term)
logWarn e
throw (InternalError e)
withContext (LogContext $ "hook " <> hookName) $
either onError checkChanged $
runExcept (hook args)
_other -> pure Nothing

-- for the (unlikely) case that a built-in reproduces itself, we
Expand Down Expand Up @@ -1074,8 +1084,12 @@ simplifyConstraint' recurseIntoEvalBool = \case
withContext "llvm" $
LLVM.simplifyBool api t >>= \case
Left (LlvmError e) -> do
withContext "abort" $ logMessage $ Text.decodeUtf8 e
logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e <> "."
let msg =
"LLVM backend error detected: " <> Text.decodeUtf8 e
details =
msg <> " while evaluating " <> renderOneLineText (pretty t)
withContext "abort" . withContext "detail" $ logMessage details
logWarn msg
throw $ UndefinedTerm t $ LlvmError e
Right res -> do
let result =
Expand Down
21 changes: 7 additions & 14 deletions booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -740,21 +740,14 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
logSimplify "Term is undefined, pruning"
emitRewriteTrace $ RewriteSimplified [] (Just r)
pure Nothing
-- NB any errors here might be caused by simplifying one
-- of the constraints, so we cannot use partial results
-- and have to return the original on errors.
Left r@(TooManyIterations n start result) -> do
ApplyEquations.logWarn $ "Simplification unable to finish in " <> prettyText n <> " steps."
logOtherNS
"booster"
(LevelOther "ErrorDetails")
( Text.unlines
[ "Start term: " <> prettyText start
, "End term: " <> prettyText result
]
)
-- could output term before and after at debug or custom log level
Left r@(TooManyIterations n _start _result) -> do
logSimplify $
"Unable to simplify in " <> Text.pack (show n) <> " iterations, returning original"
-- warning has been printed inside ApplyEquation.evaluatePattern
emitRewriteTrace $ RewriteSimplified [] (Just r)
-- NB start/result in this error are terms and might come
-- from simplifying one of the constraints. Therefore, the
-- original pattern must be returned.
pure $ Just p
Left r@(EquationLoop (t : ts)) -> do
logError "Equation evaluation loop"
Expand Down