HOTFIX invalidate cache when modifying known predicates

The change in #3953 introduced additional arguments to evaluation
functions which allow callers to supply some "known true" predicates
for the simplification and evaluation. However, doing so means that
the cache will get populated with associations that might only be true
if this known truth does not change.

The case in point was a predicate being cached as "true" because of an
earlier evaluation, and then _removed_ from the path condition.

This change removes returning the cache from any inteface functions
that take known truth arguments, and runs internal computations that
modify the predicates with a fresh empty cache.

Author: jberthold

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -210,8 +210,18 @@ countSteps = length . (.termStack) <$> getState
 pushTerm :: Monad io => Term -> EquationT io ()
 pushTerm t = eqState . modify $ \s -> s{termStack = t :<| s.termStack}
 
+-- pushing new constraints means the cache is stale
 pushConstraints :: Monad io => Set Predicate -> EquationT io ()
-pushConstraints ps = eqState . modify $ \s -> s{predicates = s.predicates <> ps}
+pushConstraints ps = eqState . modify $ \s -> s{predicates = s.predicates <> ps, cache = mempty}
+
+-- run an evaluation with a local empty cache (discarded afterwards)
+withoutCache :: Monad io => EquationT io a -> EquationT io a
+withoutCache action = do
+    prior <- getState
+    eqState $ put prior{cache = mempty}
+    a <- action
+    eqState $ modify $ \s -> s{cache = prior.cache}
+    pure a
 
 setChanged, resetChanged :: Monad io => EquationT io ()
 setChanged = eqState . modify $ \s -> s{changed = True}
@@ -333,6 +343,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do
                         , logger
                         , prettyModifiers
                         }
+    -- NB the returned cache assumes the known predicates
     pure (res, endState.cache)
 
 iterateEquations ::
@@ -432,9 +443,10 @@ evaluateTerm ::
     SMT.SMTContext ->
     Set Predicate ->
     Term ->
-    io (Either EquationFailure Term, SimplifierCache)
+    io (Either EquationFailure Term)
 evaluateTerm direction def llvmApi smtSolver knownPredicates =
-    runEquationT def llvmApi smtSolver mempty knownPredicates
+    fmap fst
+        . runEquationT def llvmApi smtSolver mempty knownPredicates
         . evaluateTerm' direction
 
 -- version for internal nested evaluation
@@ -447,6 +459,9 @@ evaluateTerm' direction = iterateEquations direction PreferFunctions
 
 {- | Simplify a Pattern, processing its constraints independently.
      Returns either the first failure or the new pattern if no failure was encountered
+
+   The returned cache may only be reused if pat.constraints are known
+   to remain true in the next usage context.
 -}
 evaluatePattern ::
     LoggerMIO io =>
@@ -476,7 +491,8 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
     -- after evaluating the term, evaluate all (existing and
     -- newly-acquired) constraints, once
-    traverse_ simplifyAssumedPredicate . predicates =<< getState
+    -- this runs with a local empty cache because it manipulates the known constraints
+    withoutCache (traverse_ simplifyAssumedPredicate . predicates =<< getState)
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
     -- break-up introduced symbolic _andBool_, filter-out trivial truth, de-duplicate
@@ -510,11 +526,12 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
         err -> throw err
 
 -- evaluate the given predicate assuming all others
+-- this manipulates the known predicates so it also resets the simplifier cache
 simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
 simplifyAssumedPredicate p = do
     allPs <- predicates <$> getState
     let otherPs = Set.delete p allPs
-    eqState $ modify $ \s -> s{predicates = otherPs}
+    eqState $ modify $ \s -> s{predicates = otherPs, cache = mempty}
     newP <- simplifyConstraint' True $ coerce p
     pushConstraints $ Set.singleton $ coerce newP
 
@@ -525,16 +542,16 @@ evaluateConstraints ::
     SMT.SMTContext ->
     SimplifierCache ->
     Set Predicate ->
-    io (Either EquationFailure (Set Predicate), SimplifierCache)
+    io (Either EquationFailure (Set Predicate))
 evaluateConstraints def mLlvmLibrary smtSolver cache =
-    runEquationT def mLlvmLibrary smtSolver cache mempty . evaluateConstraints'
+    fmap fst . runEquationT def mLlvmLibrary smtSolver cache mempty . evaluateConstraints'
 
 evaluateConstraints' ::
     LoggerMIO io =>
     Set Predicate ->
     EquationT io (Set Predicate)
-evaluateConstraints' constraints = do
-    pushConstraints constraints
+evaluateConstraints' constraints = withoutCache $ do
+    pushConstraints constraints -- invalidates the cache
     -- evaluate all existing constraints, once
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
@@ -1074,10 +1091,6 @@ applyEquation term rule =
     This is used during rewriting to simplify side conditions of rules
     (to decide whether or not a rule can apply, not to retain the
     ensured conditions).
-
-    If and as soon as this function is used inside equation
-    application, it needs to run within the same 'EquationT' context
-    so we can detect simplification loops and avoid monad nesting.
 -}
 simplifyConstraint ::
     LoggerMIO io =>
@@ -1087,9 +1100,13 @@ simplifyConstraint ::
     SimplifierCache ->
     Set Predicate ->
     Predicate ->
-    io (Either EquationFailure Predicate, SimplifierCache)
-simplifyConstraint def mbApi smt cache knownPredicates (Predicate p) = do
-    runEquationT def mbApi smt cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
+    io (Either EquationFailure Predicate)
+simplifyConstraint def mbApi smt cache knownPredicates =
+    fmap fst
+        . runEquationT def mbApi smt cache knownPredicates
+        . (coerce <$>)
+        . simplifyConstraint' True
+        . coerce
 
 simplifyConstraints ::
     LoggerMIO io =>

booster/library/Booster/Pattern/Implies.hs

@@ -151,7 +151,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                 else -- FIXME This is incomplete because patL.constraints are not assumed in the check.
 
                                     ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
-                                        (Right newPreds, _) ->
+                                        Right newPreds ->
                                             if all (== Predicate TrueBool) newPreds
                                                 then
                                                     implies
@@ -161,7 +161,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                                         subst
                                                 else -- here we conservatively abort (incomplete)
                                                     pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constraints"
-                                        (Left other, _) ->
+                                        Left other ->
                                             pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
 
             case (internalised antecedent.term, internalised consequent.term) of

booster/library/Booster/Pattern/Rewrite.hs

@@ -539,12 +539,10 @@ applyRule pat@Pattern{ceilConditions} rule =
         RewriteRuleAppT (RewriteT io) (Maybe a)
     checkConstraint onUnclear onBottom knownPredicates p = do
         RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
-        RewriteState{cache = oldCache} <- lift . RewriteT . lift $ get
-        (simplified, cache) <-
+        RewriteState{cache} <- lift . RewriteT . lift $ get
+        simplified <-
             withContext CtxConstraint $
-                simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p
-        -- update cache
-        lift $ updateRewriterCache cache
+                simplifyConstraint definition llvmApi smtSolver cache knownPredicates p
         case simplified of
             Right (Predicate FalseBool) -> onBottom
             Right (Predicate TrueBool) -> pure Nothing

booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs

@@ -97,7 +97,7 @@ test_evaluateFunction =
   where
     eval direction t = do
         ns <- noSolver
-        runNoLoggingT $ fst <$> evaluateTerm direction funDef Nothing ns mempty t
+        runNoLoggingT $ evaluateTerm direction funDef Nothing ns mempty t
 
     isTooManyIterations (Left (TooManyIterations _n _ _)) = pure ()
     isTooManyIterations (Left err) = assertFailure $ "Unexpected error " <> show err
@@ -126,7 +126,7 @@ test_simplify =
   where
     simpl direction t = do
         ns <- noSolver
-        runNoLoggingT $ fst <$> evaluateTerm direction simplDef Nothing ns mempty t
+        runNoLoggingT $ evaluateTerm direction simplDef Nothing ns mempty t
     a = var "A" someSort
 
 test_simplifyPattern :: TestTree
@@ -223,7 +223,7 @@ test_simplifyConstraint =
     simpl t =
         do
             ns <- noSolver
-            runNoLoggingT $ fst <$> simplifyConstraint testDefinition Nothing ns mempty mempty t
+            runNoLoggingT $ simplifyConstraint testDefinition Nothing ns mempty mempty t
 
 test_errors :: TestTree
 test_errors =
@@ -236,7 +236,7 @@ test_errors =
                 loopTerms =
                     [f $ app con1 [a], f $ app con2 [a], f $ app con3 [a, a], f $ app con1 [a]]
             ns <- noSolver
-            isLoop loopTerms =<< (runNoLoggingT $ fst <$> evaluateTerm TopDown loopDef Nothing ns mempty subj)
+            isLoop loopTerms =<< (runNoLoggingT $ evaluateTerm TopDown loopDef Nothing ns mempty subj)
         ]
   where
     isLoop ts (Left (EquationLoop ts')) = ts @?= ts'