Skip to content

Commit

Permalink
Re-factor simplify-implication to use matching
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a committed Jul 28, 2023
1 parent ef26fd1 commit f2d5974
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 61 deletions.
73 changes: 30 additions & 43 deletions library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down
55 changes: 37 additions & 18 deletions library/Booster/Pattern/Implication.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit f2d5974

Please sign in to comment.