Recover from TooManyIterations when simplifying during rewriting
#3989
Conversation
|
No difference in KEVM performance as of commit |
|
No significant difference in Kontrol performance either. |
geo2a
requested review from
jberthold and
goodlyrottenapple
and removed request for
jberthold
| where | ||
| -- when TooManyIterations exception occurred while evaluating the top-level term, | ||
| -- i.e. not in a recursive evaluation of a side-condition, | ||
| -- it is safe to keep the partial result and ignore the exception. | ||
| -- Otherwise we would be throwing away useful work. | ||
| keepTopLevelResults :: LoggerMIO io => EquationFailure -> EquationT io Term | ||
| keepTopLevelResults = \case | ||
| err@(TooManyIterations recursionDepth _ _ partialResult) -> | ||
| case recursionDepth of | ||
| 0 -> pure partialResult | ||
| _ -> throw err | ||
| err -> throw err |
There was a problem hiding this comment.
After checking the code where we recurse into the evaluation,
haskell-backend/booster/library/Booster/Pattern/ApplyEquations.hs
Lines 931 to 939 in 034078d
I think it is probably fine without this additional
catch_. Of course it is safer the way you propose it.
There was a problem hiding this comment.
We still need the catch_ to get the simplified term, but I do agree that the recursion depth check is redundant. I've removed it.
| getRecusionDepth :: LoggerMIO io => EquationT io Int | ||
| getRecusionDepth = (length . (.recursionStack)) <$> getState |
There was a problem hiding this comment.
| getRecusionDepth :: LoggerMIO io => EquationT io Int | |
| getRecusionDepth = (length . (.recursionStack)) <$> getState | |
| getRecursionDepth :: LoggerMIO io => EquationT io Int | |
| getRecursionDepth = (length . (.recursionStack)) <$> getState |
| @@ -331,6 +335,10 @@ iterateEquations direction preference startTerm = do | |||
| config <- getConfig | |||
| currentCount <- countSteps | |||
| when (coerce currentCount > config.maxIterations) $ do | |||
| currentRecursionDepth <- getRecusionDepth | |||
There was a problem hiding this comment.
| currentRecursionDepth <- getRecusionDepth | |
| currentRecursionDepth <- getRecursionDepth |
| -- FIXME if this exception is caught in evaluatePattern', | ||
| -- then CtxAbort is a wrong context for it. | ||
| -- We should emit this log entry somewhere else. | ||
| withContext CtxAbort $ do | ||
| logWarn $ | ||
| renderOneLineText $ |
There was a problem hiding this comment.
We could probably log this in evaluatePattern' where we decide whether or not to use the final term.
The warning will still show up for recursive evaluations where we catch the exception, too. Maybe not useless to notify the user about it, though? (so we could just use CtxWarn).
There was a problem hiding this comment.
I've removed CtxAbort, so these will show up as warnings now.
geo2a
force-pushed
the
georgy/keep-simplifications
branch
from
b0c52a7 to
a3cc6a7
Compare
Booster's rewriting algorithm, upon getting stuck (or aborting due to
RuleApplicationUnclear), will try so simplify the configuration once and retry applying rules. When we cannot not finish simplifying the term due to aTooManyIterations, we throw the partial result away and fail.This PR handles the
TooManyIterationsexception and attempts applying rewrite rules to the partially simplified term.