From f2d5974124d997ab123d897be109e89a2b821940 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 28 Jul 2023 15:17:00 +0200 Subject: [PATCH] Re-factor simplify-implication to use matching --- library/Booster/JsonRpc.hs | 73 +++++++++++--------------- library/Booster/Pattern/Implication.hs | 55 ++++++++++++------- 2 files changed, 67 insertions(+), 61 deletions(-) diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs index f319e5a8c..d6dc4c9e4 100644 --- a/library/Booster/JsonRpc.hs +++ b/library/Booster/JsonRpc.hs @@ -36,14 +36,14 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..)) import Booster.LLVM.Internal qualified as LLVM import Booster.Pattern.ApplyEquations qualified as ApplyEquations import Booster.Pattern.Base (Pattern (..), TermOrPredicate (..)) -import Booster.Pattern.Implication (ImplicationCheckResult (..), checkImplication) +import Booster.Pattern.Implication (ImplicationResult (..), simplifyImplication) import Booster.Pattern.Rewrite ( RewriteFailed (..), RewriteResult (..), RewriteTrace (..), performRewrite, ) -import Booster.Pattern.Util (sortOfPattern, substitutionAsPredicate) +import Booster.Pattern.Util (sortOfPattern) import Booster.Syntax.Json (KoreJson (..), addHeader, sortOfJson) import Booster.Syntax.Json.Externalise import Booster.Syntax.Json.Internalise (internalisePattern, internaliseTermOrPredicate) @@ -182,24 +182,16 @@ respond stateVar = (Left something, _traces) -> pure . Left . backendError RpcError.Aborted $ show something -- FIXME SimplifyImplies req -> withContext req._module $ \(def, mLlvmLibrary) -> do - let doTracing = + let internalisedAntecedent = + runExcept $ internalisePattern False Nothing def req.antecedent.term + internalisedConsequent = + runExcept $ internalisePattern False Nothing def req.consequent.term + doTracing = any (fromMaybe False) [ req.logSuccessfulSimplifications , req.logFailedSimplifications ] - mkTraces - | all not . catMaybes $ - [req.logSuccessfulSimplifications, req.logFailedSimplifications] = - const Nothing - | otherwise = - Just - . mapMaybe (mkLogEquationTrace (req.logSuccessfulSimplifications, req.logFailedSimplifications)) - . toList - let internalisedAntecedent = - runExcept $ internalisePattern False Nothing def req.antecedent.term - internalisedConsequent = - runExcept $ internalisePattern False Nothing def req.consequent.term case (internalisedAntecedent, internalisedConsequent) of (Left patternErrorsAntecedent, _) -> do Log.logError $ "Error internalising antecedent cterm: " <> Text.pack (show patternErrorsAntecedent) @@ -208,34 +200,29 @@ respond stateVar = Log.logError $ "Error internalising consequent cterm: " <> Text.pack (show patternErrorsConsequent) pure $ Left $ backendError CouldNotVerifyPattern patternErrorsConsequent (Right antecedentPattern, Right consequentPattern) -> do - Log.logInfoNS "booster" "Simplifying antecedent" - ApplyEquations.evaluatePattern doTracing def mLlvmLibrary antecedentPattern >>= \case - (Right newAntecedentPattern, antecedentTraces) -> do - Log.logInfoNS "booster" "Simplifying consequent" - ApplyEquations.evaluatePattern doTracing def mLlvmLibrary consequentPattern >>= \case - (Right newConsequentPattern, consequentTraces) -> do - Log.logInfoNS "booster" "Matching antecedent with consequent" - case checkImplication def newAntecedentPattern newConsequentPattern of - ImplicationValid subst -> - pure . Right . SimplifyImplies $ - SimplifyImpliesResult - { satisfiable = Sat - , substitution = - Just . addHeader $ - externalisePredicate - (externaliseSort $ sortOfPattern antecedentPattern) - (substitutionAsPredicate subst) - , logs = mkTraces antecedentTraces <> mkTraces consequentTraces - } - ImplicationSortError sortError -> do - pure . Left . backendError RpcError.Aborted $ show sortError - ImplicationUnknown matchFailureReason _constraints -> do - Log.logErrorNS "booster" (Text.pack . show $ matchFailureReason) - pure . Left . backendError RpcError.Aborted $ show matchFailureReason - (Left other, _consequentTraces) -> pure . Left . backendError RpcError.Aborted $ show other - (Left other, _antecedentTraces) -> pure . Left . backendError RpcError.Aborted $ show other -- FIX ME - - -- this case is only reachable if the cancel appeared as part of a batch request + Log.logInfoNS "booster" "Checking implication by simplification" + case simplifyImplication doTracing def mLlvmLibrary antecedentPattern consequentPattern of + ImplicationValid -> + pure . Right . SimplifyImplies $ + SimplifyImpliesResult + { satisfiable = Sat + , substitution = Nothing + , logs = mempty + } + ImplicationInvalid _ -> + pure . Right . SimplifyImplies $ + SimplifyImpliesResult + { satisfiable = Unsat + , substitution = Nothing + , logs = mempty + } + ImplicationUnknown _ -> + pure . Right . SimplifyImplies $ + SimplifyImpliesResult + { satisfiable = Unknown + , substitution = Nothing + , logs = mempty + } Cancel -> pure $ Left cancelUnsupportedInBatchMode -- using "Method does not exist" error code _ -> pure $ Left notImplemented diff --git a/library/Booster/Pattern/Implication.hs b/library/Booster/Pattern/Implication.hs index 876f6b130..e0327d066 100644 --- a/library/Booster/Pattern/Implication.hs +++ b/library/Booster/Pattern/Implication.hs @@ -5,28 +5,47 @@ Copyright : (c) Runtime Verification, 2023 License : BSD-3-Clause -} module Booster.Pattern.Implication ( - checkImplication, - ImplicationCheckResult (..), + simplifyImplication, + ImplicationResult (..), ) where import Booster.Definition.Base (KoreDefinition) -import Booster.Pattern.Base (Pattern (..), Predicate) -import Booster.Pattern.Unify qualified as Unify +import Booster.LLVM.Internal qualified as LLVM +import Booster.Pattern.Base (Pattern (..), Predicate, Term) +import Booster.Pattern.Match qualified as Match -data ImplicationCheckResult - = ImplicationValid Unify.Substitution - | ImplicationUnknown (Maybe Unify.FailReason) [Predicate] - | ImplicationSortError Unify.SortError +-- | Result of matching a pattern to a subject (unification, failure, or indeterminate) +data ImplicationResult + = ImplicationValid + | ImplicationInvalid ImplicationFailureReason + | ImplicationUnknown ImplicationUnknownReason + deriving stock (Eq, Show) --- | Attempt to check the implication between two patterns using matching and simplification rules -checkImplication :: KoreDefinition -> Pattern -> Pattern -> ImplicationCheckResult -checkImplication def antecedent consequent = - case Unify.unifyTerms def consequent.term antecedent.term of - Unify.UnificationSuccess subst -> +data ImplicationFailureReason + = MatchingFailed Match.MatchFailReason + | ConstraintSubsumptionFailed [Predicate] + deriving stock (Eq, Show) + +data ImplicationUnknownReason + = MatchingUnknown Term Term + | ConstraintSubsumptionUnknown [Predicate] + deriving stock (Eq, Show) + +-- | Check implication between two patterns using matching and simplification rules +simplifyImplication :: + Bool -> + KoreDefinition -> + Maybe LLVM.API -> + Pattern -> + Pattern -> + ImplicationResult +simplifyImplication _doTracing def _mLlvmLibrary antecedent consequent = + case Match.matchTerm def antecedent.term consequent.term of + Match.MatchSuccess _subst -> -- got substitution, let's now look at constraints case (antecedent.constraints, consequent.constraints) of - ([], []) -> ImplicationValid subst - (_, _) -> ImplicationUnknown Nothing (antecedent.constraints <> consequent.constraints) - Unify.UnificationFailed reason -> ImplicationUnknown (Just reason) [] - Unify.UnificationSortError sortError -> ImplicationSortError sortError - Unify.UnificationRemainder pairs -> error (show pairs) + ([], []) -> ImplicationValid + (_, _) -> + ImplicationUnknown $ ConstraintSubsumptionUnknown (antecedent.constraints <> consequent.constraints) + Match.MatchFailed reason -> ImplicationInvalid . MatchingFailed $ reason + Match.MatchIndeterminate antecedent_term consequent_term -> ImplicationUnknown $ MatchingUnknown antecedent_term consequent_term