From 3d7e91d41f0a2db8a5516cb9a33f598620b94a11 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 15 Aug 2024 14:03:16 +0200 Subject: [PATCH] Georgy/refactor check requires (#4035) Refactor `applyRule` and `applyEquation` to check `requires`/`ensures` in separate functions. This will make reviewing https://github.com/runtimeverification/haskell-backend/pull/4022 easier. --- .../library/Booster/Pattern/ApplyEquations.hs | 183 ++++++++++-------- booster/library/Booster/Pattern/Rewrite.hs | 128 +++++++----- 2 files changed, 181 insertions(+), 130 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 0d5a28d16b..dc08a8e121 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -839,86 +839,15 @@ applyEquation term rule = Map.toList subst ) - -- instantiate the requires clause with the obtained substitution - let required = - concatMap - (splitBoolPredicates . coerce . substituteInTerm subst . coerce) - rule.requires - -- If the required condition is _syntactically_ present in - -- the prior (known constraints), we don't check it. - knownPredicates <- (.predicates) <$> lift getState - toCheck <- lift $ filterOutKnownConstraints knownPredicates required - - -- check the filtered requires clause conditions - unclearConditions <- - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) - ) - toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions - - solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig - - -- check any conditions that are still unclear with the SMT solver - -- (or abort if no solver is being used), abort if still unclear after - unless (null stillUnclear) $ - lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case - SMT.IsUnknown{} -> do - -- no solver or still unclear: abort - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText - ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) - ) - , IndeterminateCondition stillUnclear - ) - SMT.IsInvalid -> do - -- actually false given path condition: fail - let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ - renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) - , ConditionFalse failedP - ) - SMT.IsValid{} -> do - -- can proceed - pure () + -- check required constraints from lhs. + -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification), + -- see @handleSimplificationEquation@ and @handleFunctionEquation@ + checkRequires subst - -- check ensured conditions, filter any - -- true ones, prune if any is false - let ensured = - concatMap - (splitBoolPredicates . substituteInPredicate subst) - (Set.toList rule.ensures) - ensuredConditions <- - -- throws if an ensured condition found to be false - catMaybes - <$> mapM - ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) - ) - ensured - -- check all ensured conditions together with the path condition - lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case - SMT.IsInvalid -> do - let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions - throwE - ( \ctx -> - ctx . logMessage $ - WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $ - renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures) - , EnsuresFalse falseEnsures - ) - _ -> - pure () + -- check ensured conditions, filter any true ones, prune if any is false + ensuredConditions <- checkEnsures subst lift $ pushConstraints $ Set.fromList ensuredConditions + -- when a new path condition is added, invalidate the equation cache unless (null ensuredConditions) $ do withContextFor Equations . logMessage $ @@ -1013,6 +942,104 @@ applyEquation term rule = check $ Map.lookup Variable{variableSort = SortApp sortName [], variableName} subst + checkRequires :: + Substitution -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + () + checkRequires matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + -- instantiate the requires clause with the obtained substitution + let required = + concatMap + (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) + rule.requires + -- If the required condition is _syntactically_ present in + -- the prior (known constraints), we don't check it. + knownPredicates <- (.predicates) <$> lift getState + toCheck <- lift $ filterOutKnownConstraints knownPredicates required + + -- check the filtered requires clause conditions + unclearConditions <- + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Condition simplified to #Bottom." :: Text), ConditionFalse p) + ) + toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions + + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + + -- check any conditions that are still unclear with the SMT solver + -- (or abort if no solver is being used), abort if still unclear after + unless (null stillUnclear) $ + lift (SMT.checkPredicates solver knownPredicates mempty (Set.fromList stillUnclear)) >>= \case + SMT.IsUnknown{} -> do + -- no solver or still unclear: abort + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText + ( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear) + ) + , IndeterminateCondition stillUnclear + ) + SMT.IsInvalid -> do + -- actually false given path condition: fail + let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $ + renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP) + , ConditionFalse failedP + ) + SMT.IsValid{} -> do + -- can proceed + pure () + + checkEnsures :: + Substitution -> + ExceptT + ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) + (EquationT io) + [Predicate] + checkEnsures matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + let ensured = + concatMap + (splitBoolPredicates . substituteInPredicate matchingSubst) + (Set.toList rule.ensures) + ensuredConditions <- + -- throws if an ensured condition found to be false + catMaybes + <$> mapM + ( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p) + ) + ensured + + -- check all ensured conditions together with the path condition + solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig + knownPredicates <- (.predicates) <$> lift getState + lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case + SMT.IsInvalid -> do + let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions + throwE + ( \ctx -> + ctx . logMessage $ + WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $ + renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures) + , EnsuresFalse falseEnsures + ) + _ -> + pure () + pure ensuredConditions + -------------------------------------------------------------------- {- Simplification for boolean predicates diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 8f53d026a0..c7fe6f1005 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -63,6 +63,7 @@ import Booster.Pattern.Match ( MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess), MatchType (Rewrite), SortError, + Substitution, matchTerms, ) import Booster.Pattern.Pretty @@ -334,61 +335,12 @@ applyRule pat@Pattern{ceilConditions} rule = pat rule.computedAttributes.notPreservesDefinednessReasons - -- apply substitution to rule requires constraints and simplify (one by one - -- in isolation). Stop if false, abort rewrite if indeterminate. - let ruleRequires = - concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) rule.requires - notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied - -- filter out any predicates known to be _syntactically_ present in the known prior - let prior = pat.constraints - toCheck <- lift $ filterOutKnownConstraints prior ruleRequires - - unclearRequires <- - catMaybes <$> mapM (checkConstraint id notAppliedIfBottom prior) toCheck - - -- unclear conditions may have been simplified and - -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints prior unclearRequires - - -- check unclear requires-clauses in the context of known constraints (prior) - solver <- lift $ RewriteT $ (.smtSolver) <$> ask - - let smtUnclear = do - withContext CtxConstraint . withContext CtxAbort . logMessage $ - WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $ - renderOneLineText $ - "Uncertain about condition(s) in a rule:" - <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear) - failRewrite $ - RuleConditionUnclear rule . coerce . foldl1 AndTerm $ - map coerce stillUnclear - - SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear) >>= \case - SMT.IsUnknown{} -> - smtUnclear -- abort rewrite if a solver result was Unknown - SMT.IsInvalid -> do - -- requires is actually false given the prior - withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure NotApplied - SMT.IsValid -> - pure () -- can proceed + -- check required constraints from lhs: Stop if any is false, abort rewrite if indeterminate. + checkRequires subst -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - let ruleEnsures = - concatMap (splitBoolPredicates . coerce . substituteInTerm subst . coerce) $ - Set.toList rule.ensures - trivialIfBottom = RewriteRuleAppT $ pure Trivial - newConstraints <- - catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures - - -- check all new constraints together with the known side constraints - (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case - SMT.IsInvalid -> do - withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) - RewriteRuleAppT $ pure Trivial - _other -> - pure () + newConstraints <- checkEnsures subst -- if a new constraint is going to be added, the equation cache is invalid unless (null newConstraints) $ do @@ -438,6 +390,12 @@ applyRule pat@Pattern{ceilConditions} rule = failRewrite :: RewriteFailed "Rewrite" -> RewriteRuleAppT (RewriteT io) a failRewrite = lift . (throw) + notAppliedIfBottom :: RewriteRuleAppT (RewriteT io) a + notAppliedIfBottom = RewriteRuleAppT $ pure NotApplied + + trivialIfBottom :: RewriteRuleAppT (RewriteT io) a + trivialIfBottom = RewriteRuleAppT $ pure Trivial + checkConstraint :: (Predicate -> a) -> RewriteRuleAppT (RewriteT io) (Maybe a) -> @@ -459,6 +417,72 @@ applyRule pat@Pattern{ceilConditions} rule = Left UndefinedTerm{} -> onBottom Left _ -> pure $ Just $ onUnclear p + checkRequires :: + Substitution -> RewriteRuleAppT (RewriteT io) () + checkRequires matchingSubst = do + ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers + -- apply substitution to rule requires + let ruleRequires = + concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires + + -- filter out any predicates known to be _syntactically_ present in the known prior + toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires + + -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate. + unclearRequires <- + catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck + + -- unclear conditions may have been simplified and + -- could now be syntactically present in the path constraints, filter again + stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires + + -- check unclear requires-clauses in the context of known constraints (priorKnowledge) + solver <- lift $ RewriteT $ (.smtSolver) <$> ask + let smtUnclear = do + withContext CtxConstraint . withContext CtxAbort . logMessage $ + WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $ + renderOneLineText $ + "Uncertain about condition(s) in a rule:" + <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear) + failRewrite $ + RuleConditionUnclear rule . coerce . foldl1 AndTerm $ + map coerce stillUnclear + SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case + SMT.IsUnknown{} -> + smtUnclear -- abort rewrite if a solver result was Unknown + SMT.IsInvalid -> do + -- requires is actually false given the prior + withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) + RewriteRuleAppT $ pure NotApplied + SMT.IsValid -> + pure () -- can proceed + checkEnsures :: + Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] + checkEnsures matchingSubst = do + -- apply substitution to rule requires + let ruleEnsures = + concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) $ + Set.toList rule.ensures + newConstraints <- + catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures + + -- check all new constraints together with the known side constraints + solver <- lift $ RewriteT $ (.smtSolver) <$> ask + (lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case + SMT.IsInvalid -> do + withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) + RewriteRuleAppT $ pure Trivial + _other -> + pure () + + -- if a new constraint is going to be added, the equation cache is invalid + unless (null newConstraints) $ do + withContextFor Equations . logMessage $ + ("New path condition ensured, invalidating cache" :: Text) + + lift . RewriteT . lift . modify $ \s -> s{equations = mempty} + pure newConstraints + {- | Reason why a rewrite did not produce a result. Contains additional information for logging what happened during the rewrite. -}