From 998eb072fa3fd7682868ac497edf1141e2e3ceae Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 20 Aug 2024 10:17:46 +0200 Subject: [PATCH] Make Z3 call optional in evaluatePattern --- booster/library/Booster/JsonRpc.hs | 39 +++++++----- .../library/Booster/Pattern/ApplyEquations.hs | 63 +++++++++++-------- booster/library/Booster/Pattern/Implies.hs | 41 +++++++----- booster/library/Booster/Pattern/Rewrite.hs | 3 +- 4 files changed, 87 insertions(+), 59 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 2dfd2d40a5..b2a1593564 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -154,6 +154,7 @@ respond stateVar request = mLlvmLibrary solver mempty + ApplyEquations.CheckConstraintsConsistent substPat case evaluatedInitialPattern of @@ -277,21 +278,29 @@ respond stateVar request = , constraints = Set.map (substituteInPredicate substitution) pat.constraints , ceilConditions = pat.ceilConditions } - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case - (Right newPattern, _) -> do - let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution - tSort = externaliseSort (sortOfPattern newPattern) - result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of - [] -> term - ps -> KoreJson.KJAnd tSort $ term : ps - pure $ Right (addHeader result) - (Left ApplyEquations.SideConditionFalse{}, _) -> do - let tSort = externaliseSort $ sortOfPattern pat - pure $ Right (addHeader $ KoreJson.KJBottom tSort) - (Left (ApplyEquations.EquationLoop _terms), _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" - (Left other, _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) + -- evaluate the pattern, checking the constrains for consistency + ApplyEquations.evaluatePattern + def + mLlvmLibrary + solver + mempty + ApplyEquations.CheckConstraintsConsistent + substPat + >>= \case + (Right newPattern, _) -> do + let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution + tSort = externaliseSort (sortOfPattern newPattern) + result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of + [] -> term + ps -> KoreJson.KJAnd tSort $ term : ps + pure $ Right (addHeader result) + (Left ApplyEquations.SideConditionFalse{}, _) -> do + let tSort = externaliseSort $ sortOfPattern pat + pure $ Right (addHeader $ KoreJson.KJBottom tSort) + (Left (ApplyEquations.EquationLoop _terms), _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected" + (Left other, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other) -- predicate only Right (Predicates ps) | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported -> diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 673f843947..f5f53e7a01 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -10,6 +10,8 @@ License : BSD-3-Clause module Booster.Pattern.ApplyEquations ( evaluateTerm, evaluatePattern, + pattern CheckConstraintsConsistent, + pattern NoCheckConstraintsConsistent, Direction (..), EquationT (..), runEquationT, @@ -70,7 +72,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) -import Booster.Util (Bound (..)) +import Booster.Util (Bound (..), Flag (..)) import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached)) import Kore.Util (showHashHex) @@ -443,6 +445,12 @@ evaluateTerm' :: EquationT io Term evaluateTerm' direction = iterateEquations direction PreferFunctions +pattern CheckConstraintsConsistent :: Flag "CheckConstraintsConsistent" +pattern CheckConstraintsConsistent = Flag True + +pattern NoCheckConstraintsConsistent :: Flag "CheckConstraintsConsistent" +pattern NoCheckConstraintsConsistent = Flag False + {- | Simplify a Pattern, processing its constraints independently. Returns either the first failure or the new pattern if no failure was encountered -} @@ -452,39 +460,42 @@ evaluatePattern :: Maybe LLVM.API -> SMT.SMTContext -> SimplifierCache -> + Flag "CheckConstraintsConsistent" -> Pattern -> io (Either EquationFailure Pattern, SimplifierCache) -evaluatePattern def mLlvmLibrary smtSolver cache pat = - runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat +evaluatePattern def mLlvmLibrary smtSolver cache doCheck pat = + runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' doCheck $ pat -- version for internal nested evaluation evaluatePattern' :: LoggerMIO io => + Flag "CheckConstraintsConsistent" -> Pattern -> EquationT io Pattern -evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do - solver <- (.smtSolver) <$> getConfig - -- check the pattern's constraints for satisfiability to ensure they are consistent - consistent <- - withContext CtxConstraint $ do - withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure () - consistent <- SMT.isSat solver (Set.toList constraints) - logMessage $ - "Constraints consistency check returns: " <> show consistent - pure consistent - case consistent of - SMT.IsUnsat -> do - -- the constraints are unsatisfiable, which means that the patten is Bottom - throw . SideConditionFalse . collapseAndBools $ constraints - SMT.IsUnknown{} -> do - -- unlikely case of an Unknown response to a consistency check. - -- continue to preserve the old behaviour. - withContext CtxConstraint . logWarn . Text.pack $ - "Constraints consistency UNKNOWN: " <> show consistent - pure () - SMT.IsSat{} -> - -- constraints are consistent, continue - pure () +evaluatePattern' doCheck pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do + when (coerce doCheck) $ do + solver <- (.smtSolver) <$> getConfig + -- check the pattern's constraints for satisfiability to ensure they are consistent + consistent <- + withContext CtxConstraint $ do + withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure () + consistent <- SMT.isSat solver (Set.toList constraints) + logMessage $ + "Constraints consistency check returns: " <> show consistent + pure consistent + case consistent of + SMT.IsUnsat -> do + -- the constraints are unsatisfiable, which means that the patten is Bottom + throw . SideConditionFalse . collapseAndBools $ constraints + SMT.IsUnknown{} -> do + -- unlikely case of an Unknown response to a consistency check. + -- continue to preserve the old behaviour. + withContext CtxConstraint . logWarn . Text.pack $ + "Constraints consistency UNKNOWN: " <> show consistent + pure () + SMT.IsSat{} -> + -- constraints are consistent, continue + pure () newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults -- after evaluating the term, evaluate all (existing and newly-acquired) constraints, once diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 0dd5a33f0e..5164971881 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -136,24 +136,31 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (externaliseExistTerm existsL substPatL.term) (externaliseExistTerm existsR substPatR.term) MatchIndeterminate remainder -> - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case - (Right simplifedSubstPatL, _) -> - if substPatL == simplifedSubstPatL - then -- we are being conservative here for now and returning an error. - -- since we have already simplified the LHS, we may want to eventually return implise, but the condition - -- will contain the remainder as an equality contraint, predicating the implication on that equality being true. + ApplyEquations.evaluatePattern + def + mLlvmLibrary + solver + mempty + ApplyEquations.CheckConstraintsConsistent + substPatL + >>= \case + (Right simplifedSubstPatL, _) -> + if substPatL == simplifedSubstPatL + then -- we are being conservative here for now and returning an error. + -- since we have already simplified the LHS, we may want to eventually return implise, but the condition + -- will contain the remainder as an equality contraint, predicating the implication on that equality being true. - pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ - "match remainder: " - <> renderDefault - ( hsep $ - punctuate comma $ - map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ - NonEmpty.toList remainder - ) - else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR - (Left err, _) -> - pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) + pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ + "match remainder: " + <> renderDefault + ( hsep $ + punctuate comma $ + map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ + NonEmpty.toList remainder + ) + else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR + (Left err, _) -> + pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do let filteredConsequentPreds = Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 40ef772b82..96531a8ee5 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -54,6 +54,7 @@ import Booster.Pattern.ApplyEquations ( SimplifierCache (..), evaluatePattern, simplifyConstraint, + pattern NoCheckConstraintsConsistent, ) import Booster.Pattern.Base import Booster.Pattern.Bool @@ -764,7 +765,7 @@ performRewrite rewriteConfig initialCache pat = do simplifyP p = withContext CtxSimplify $ do st <- get let cache = st.simplifierCache - evaluatePattern definition llvmApi smtSolver cache p >>= \(res, newCache) -> do + evaluatePattern definition llvmApi smtSolver cache NoCheckConstraintsConsistent p >>= \(res, newCache) -> do updateCache newCache case res of Right newPattern -> do