Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

booster/library/Booster/CLOptions.hs

@@ -232,6 +232,10 @@ allowedLogLevels =
     , ("Depth", "Log the current depth of the state")
     , ("SMT", "Log the SMT-solver interactions")
     , ("ErrorDetails", "Log error conditions with extensive details")
+    ,
+        ( "EquationWarnings"
+        , "Log warnings indicating soft-violations of conditions, i.e. exceeding the equation recursion/iteration limit "
+        )
     ]
 
 levelToContext :: Map Text [ContextFilter]
@@ -279,6 +283,12 @@ levelToContext =
                 , [ctxt| booster>failure,abort |]
                 ]
             )
+        ,
+            ( "EquationWarnings"
+            ,
+                [ [ctxt| booster>(simplification *|function *)>warning |]
+                ]
+            )
         ]
 
 -- Partition provided log levels into standard and custom ones, and

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -84,8 +84,15 @@ throw = EquationT . lift . throwE
 catch_ ::
     Monad io => EquationT io a -> (EquationFailure -> EquationT io a) -> EquationT io a
 catch_ (EquationT op) hdlr = EquationT $ do
+    prior <- lift . lift $ get
     cfg <- ask
-    lift (runReaderT op cfg `catchE` (\e -> let EquationT fallBack = hdlr e in runReaderT fallBack cfg))
+    lift
+        ( runReaderT op cfg
+            `catchE` ( \e -> do
+                        let EquationT fallBack = hdlr e
+                        runReaderT (lift (lift (put prior)) >> fallBack) cfg
+                     )
+        )
 
 data EquationFailure
     = IndexIsNone Term
@@ -232,8 +239,8 @@ fromCache tag t = eqState $ Map.lookup t <$> gets (select tag . (.cache))
 
 logWarn :: LoggerMIO m => Text -> m ()
 logWarn msg =
-    logMessage' $
-        msg <> " For more details, enable full context logging '--log-context \"*\"'"
+    withContext "warning" $
+        logMessage msg
 
 checkForLoop :: LoggerMIO io => Term -> EquationT io ()
 checkForLoop t = do
@@ -965,5 +972,7 @@ simplifyConstraint' recurseIntoEvalBool = \case
         prior <- getState -- save prior state so we can revert
         eqState $ put prior{termStack = mempty, changed = False}
         result <- iterateEquations BottomUp PreferFunctions t
-        eqState $ put prior
+        -- reset change flag and term stack to prior values
+        -- (keep the updated cache and added predicates, if any)
+        eqState $ modify $ \s -> s{changed = prior.changed, termStack = prior.termStack}
         pure result