More work on simplify-implication

runtimeverification · Jul 25, 2023 · 56c35eb · 56c35eb
1 parent 1d2e66d
commit 56c35eb
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 31 deletions.
diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -44,7 +44,6 @@ import Booster.Pattern.Rewrite (
     performRewrite,
  )
 import Booster.Pattern.Util (sortOfPattern, substitutionAsPredicate)
-import Booster.Prettyprinter (renderDefault)
 import Booster.Syntax.Json (KoreJson (..), addHeader, sortOfJson)
 import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (internalisePattern, internaliseTermOrPredicate)
@@ -183,8 +182,20 @@ respond stateVar =
                         (Left something, _traces) ->
                             pure . Left . backendError RpcError.Aborted $ show something -- FIXME
         SimplifyImplies req -> withContext req._module $ \(def, mLlvmLibrary) -> do
-            let logTraces =
-                    mapM_ (Log.logOther (Log.LevelOther "Simplify") . pack . renderDefault . pretty)
+            let 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 =
@@ -198,13 +209,11 @@ respond stateVar =
                     pure $ Left $ backendError CouldNotVerifyPattern patternErrorsConsequent
                 (Right antecedentPattern, Right consequentPattern) -> do
                     Log.logInfoNS "booster" "Simplifying antecedent"
-                    case ApplyEquations.traceSimplifyPattern def mLlvmLibrary antecedentPattern of
-                        Right (newAntecedentPattern, antecedentTraces) -> do
-                            logTraces $ filter (not . ApplyEquations.isMatchFailure) antecedentTraces
+                    ApplyEquations.evaluatePattern doTracing def mLlvmLibrary antecedentPattern >>= \case
+                        (Right newAntecedentPattern, antecedentTraces) -> do
                             Log.logInfoNS "booster" "Simplifying consequent"
-                            case ApplyEquations.traceSimplifyPattern def mLlvmLibrary consequentPattern of
-                                Right (newConsequentPattern, consequentTraces) -> do
-                                    logTraces $ filter (not . ApplyEquations.isMatchFailure) consequentTraces
+                            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 ->
@@ -216,14 +225,15 @@ respond stateVar =
                                                             externalisePredicate
                                                                 (externaliseSort $ sortOfPattern antecedentPattern)
                                                                 (substitutionAsPredicate subst)
-                                                    , logs = mempty
+                                                    , 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 -> pure . Left . backendError RpcError.Aborted $ show other
-                        Left other ->
-                            pure . Left . backendError RpcError.Aborted $ show other -- FIXME
+                                (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
         Cancel -> pure $ Left cancelUnsupportedInBatchMode

diff --git a/library/Booster/Pattern/ApplyEquations.hs b/library/Booster/Pattern/ApplyEquations.hs
@@ -15,7 +15,6 @@ module Booster.Pattern.ApplyEquations (
     isMatchFailure,
     isSuccess,
     simplifyConstraint,
-    traceSimplifyPattern,
 ) where
 
 import Control.Monad
@@ -669,20 +668,3 @@ simplifyConstraint' = \case
         result <- iterateEquations 100 TopDown PreferFunctions t
         EquationT $ lift $ lift $ put prior
         pure result
-
---------------------------------------------------------------------
-
-{- | Simplify a Pattern, processing its constraints independently.
-     Returns either the first failure or the new pattern if no failure was encountered
--}
-traceSimplifyPattern ::
-    KoreDefinition ->
-    Maybe LLVM.API ->
-    Pattern ->
-    Either EquationFailure (Pattern, [EquationTrace])
-traceSimplifyPattern def mLlvmLibrary Pattern{term, constraints} = do
-    (newTerm, termTraces) <- evaluateTerm TopDown def mLlvmLibrary term
-    simplified <- traverse (traceSimplifyConstraint def mLlvmLibrary) constraints
-    let newConstraints = map fst simplified
-        constraintsTraces = mconcat $ map snd simplified
-    pure (Pattern{constraints = newConstraints, term = newTerm}, termTraces <> constraintsTraces)
diff --git a/library/Booster/Pattern/Implication.hs b/library/Booster/Pattern/Implication.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+-}
+module Booster.Pattern.Implication (
+    checkImplication,
+    ImplicationCheckResult (..),
+) where
+
+import Booster.Definition.Base (KoreDefinition)
+import Booster.Pattern.Base (Pattern (..), Predicate)
+import Booster.Pattern.Unify qualified as Unify
+
+data ImplicationCheckResult
+    = ImplicationValid Unify.Substitution
+    | ImplicationUnknown (Maybe Unify.FailReason) [Predicate]
+    | ImplicationSortError Unify.SortError
+
+-- | 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 ->
+            -- 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)