From 5481f26385a359c9e1f63ffc5eac48247c78f456 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 15 Oct 2024 14:50:14 +0200 Subject: [PATCH 01/36] Make substitution part of Pattern --- booster/library/Booster/JsonRpc.hs | 2 ++ booster/library/Booster/Pattern/ApplyEquations.hs | 4 ++-- booster/library/Booster/Pattern/Base.hs | 8 ++++++-- booster/library/Booster/Pattern/Binary.hs | 2 +- booster/library/Booster/Pattern/Implies.hs | 2 ++ booster/library/Booster/Pattern/Match.hs | 3 --- booster/library/Booster/Pattern/Rewrite.hs | 11 +++++++---- booster/library/Booster/Pattern/Util.hs | 1 + booster/library/Booster/Syntax/Json/Internalise.hs | 9 +++++++-- booster/tools/booster/Proxy.hs | 2 +- booster/unit-tests/Test/Booster/Pattern/Binary.hs | 2 +- 11 files changed, 30 insertions(+), 16 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 979da2e731..da486edcc8 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -137,6 +137,7 @@ respond stateVar request = { term = substituteInTerm substitution term , constraints = Set.fromList $ map (substituteInPredicate substitution) preds , ceilConditions = ceils + , substitution = mempty -- this is the ensures-substitution, leave empty } -- remember all variables used in the substitutions substVars = @@ -254,6 +255,7 @@ respond stateVar request = { term = substituteInTerm substitution pat.term , constraints = Set.map (substituteInPredicate substitution) pat.constraints , ceilConditions = pat.ceilConditions + , substitution = mempty -- this is the ensures-substitution, leave empty } ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case (Right newPattern, _) -> do diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index a410afebe0..590fc1234e 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -462,14 +462,14 @@ evaluatePattern' :: LoggerMIO io => Pattern -> EquationT io Pattern -evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do +evaluatePattern' pat@Pattern{term, ceilConditions, substitution} = withPatternContext pat $ do newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults -- after evaluating the term, evaluate all (existing and -- newly-acquired) constraints, once traverse_ simplifyAssumedPredicate . predicates =<< getState -- this may yield additional new constraints, left unevaluated evaluatedConstraints <- predicates <$> getState - pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions} + pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions, substitution} where -- when TooManyIterations exception occurred while evaluating the top-level term, -- i.e. not in a recursive evaluation of a side-condition, diff --git a/booster/library/Booster/Pattern/Base.hs b/booster/library/Booster/Pattern/Base.hs index a2b4661614..f8991bc259 100644 --- a/booster/library/Booster/Pattern/Base.hs +++ b/booster/library/Booster/Pattern/Base.hs @@ -36,6 +36,7 @@ import Data.Functor.Foldable import Data.Hashable (Hashable) import Data.Hashable qualified as Hashable import Data.List as List (foldl', foldl1', sort) +import Data.Map.Strict (Map) import Data.Set (Set) import Data.Set qualified as Set import GHC.Generics (Generic) @@ -761,19 +762,22 @@ pattern KSeq sort a = -------------------- +type Substitution = Map Variable Term + -- | A term (configuration) constrained by a number of predicates. data Pattern = Pattern { term :: Term , constraints :: !(Set Predicate) + , substitution :: Substitution , ceilConditions :: ![Ceil] } deriving stock (Eq, Ord, Show, Generic, Data) deriving anyclass (NFData) pattern Pattern_ :: Term -> Pattern -pattern Pattern_ t <- Pattern t _ _ +pattern Pattern_ t <- Pattern t _ _ _ where - Pattern_ t = Pattern t mempty mempty + Pattern_ t = Pattern t mempty mempty mempty pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term pattern ConsApplication sym sorts args <- diff --git a/booster/library/Booster/Pattern/Binary.hs b/booster/library/Booster/Pattern/Binary.hs index c398e33878..9f8f9d2ac7 100644 --- a/booster/library/Booster/Pattern/Binary.hs +++ b/booster/library/Booster/Pattern/Binary.hs @@ -564,7 +564,7 @@ decodePattern mDef = do preds <- forM preds' $ \case BPredicate pIdx -> Predicate <$> getTerm pIdx _ -> fail "Expecting a predicate" - pure $ Pattern trm (Set.fromList preds) mempty + pure $ Pattern trm (Set.fromList preds) mempty mempty _ -> fail "Expecting a term on the top of the stack" encodeMagicHeaderAndVersion :: Version -> Put diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 0dd5a33f0e..28251a71ca 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -111,12 +111,14 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = { term = substituteInTerm substitutionL patL.term , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints , ceilConditions = patL.ceilConditions + , substitution = substitutionL } substPatR = Pattern { term = substituteInTerm substitutionR patR.term , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints , ceilConditions = patR.ceilConditions + , substitution = substitutionR } SMT.isSat solver (Set.toList substPatL.constraints) >>= \case diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index dd8d82caa0..b5ae619179 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -8,7 +8,6 @@ module Booster.Pattern.Match ( MatchResult (..), MatchType (..), FailReason (..), - Substitution, matchTerms, checkSubsort, SortError (..), @@ -119,8 +118,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe SubjectVariableMatch t v -> hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t] -type Substitution = Map Variable Term - {- | Attempts to find a simple unifying substitution for the given terms. diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 39d6f71c2f..45e5bb91b1 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -63,7 +63,6 @@ import Booster.Pattern.Match ( MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess), MatchType (Rewrite), SortError, - Substitution, matchTerms, ) import Booster.Pattern.Pretty @@ -340,14 +339,17 @@ applyRule pat@Pattern{ceilConditions} rule = -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - newConstraints <- checkEnsures subst + ensuredConditions <- checkEnsures subst -- if a new constraint is going to be added, the equation cache is invalid - unless (null newConstraints) $ do + unless (null ensuredConditions) $ do withContextFor Equations . logMessage $ ("New path condition ensured, invalidating cache" :: Text) lift . RewriteT . lift . modify $ \s -> s{equations = mempty} + let isSubstitution = const False + (_newSubsitutionItems, newConstraints) = partition isSubstitution ensuredConditions + -- existential variables may be present in rule.rhs and rule.ensures, -- need to strip prefixes and freshen their names with respect to variables already -- present in the input pattern and in the unification substitution @@ -370,6 +372,7 @@ applyRule pat@Pattern{ceilConditions} rule = ( pat.constraints <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) ) + pat.substitution ceilConditions withContext CtxSuccess $ withPatternContext rewritten $ @@ -669,7 +672,7 @@ mkDiffTerms = \case * RewriteStuck: config could not be re-written by any rule, return current * RewriteFailed: rewriter cannot handle the case, return current - The actions are logged at the custom log level '"Rewrite"'. + The result also includes a @'Substitution'@ accumulated from the rules ensures clauses. This flow chart should represent the actions of this function: diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index c819db8758..0807d3f722 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -109,6 +109,7 @@ modifyVariables f p = Pattern { term = modifyVariablesInT f p.term , constraints = Set.map (modifyVariablesInP f) p.constraints + , substitution = Map.map (coerce $ modifyVariablesInT f) p.substitution , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions } diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index dbca5fb972..9b326cd85a 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -221,7 +221,7 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi pure $ IsPattern ( existentialVars - , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions} + , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = mempty} -- this is the ensures-substitution, leave empty , subst , unknown ) @@ -252,7 +252,12 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt pure $ TermAndPredicates - Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions} + Internal.Pattern + { term + , constraints = Set.fromList constrs + , ceilConditions + , substitution = mempty -- this is the ensures-substitution, leave empty + } substitution unsupported ) diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index edadbd7e0f..274bd0ef86 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -523,7 +523,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of pure $ Right ( ( Booster.toExecState - Pattern{term, ceilConditions, constraints = Set.fromList preds} + Pattern{term, ceilConditions, constraints = Set.fromList preds, substitution = sub} sub unsup Nothing diff --git a/booster/unit-tests/Test/Booster/Pattern/Binary.hs b/booster/unit-tests/Test/Booster/Pattern/Binary.hs index 931d803707..e5588fda77 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Binary.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Binary.hs @@ -67,7 +67,7 @@ genPredicate = <$> Gen.choice [pure TrueBool, pure FalseBool, genTerm] genPattern :: Gen Pattern -genPattern = (\t cs -> Pattern t cs mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) +genPattern = (\t cs -> Pattern t cs mempty mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) test_BinaryRoundTrips :: [TestTree] test_BinaryRoundTrips = From 1e7ce613908c66a32cc518799855753b3989bb65 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 15 Oct 2024 16:35:12 +0200 Subject: [PATCH 02/36] Do not invalidate cache twice when ensuring conditions --- booster/library/Booster/Pattern/Rewrite.hs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 45e5bb91b1..c25ab28adf 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -455,7 +455,7 @@ applyRule pat@Pattern{ceilConditions} rule = checkEnsures :: Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] checkEnsures matchingSubst = do - -- apply substitution to rule requires + -- apply substitution to rule ensures let ruleEnsures = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures newConstraints <- @@ -483,12 +483,6 @@ applyRule pat@Pattern{ceilConditions} rule = _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 smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) () From b491b85145d1c4e6a2d61e7acc16e7f1b2d61eb7 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 15 Oct 2024 18:24:16 +0200 Subject: [PATCH 03/36] Extract substitution items from ensured conditions --- booster/library/Booster/Pattern/Bool.hs | 16 ++++++- booster/library/Booster/Pattern/Rewrite.hs | 55 +++++++++++++++++++--- 2 files changed, 62 insertions(+), 9 deletions(-) diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 39dd2cacc3..dd107cce9d 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -10,6 +10,7 @@ module Booster.Pattern.Bool ( negateBool, splitBoolPredicates, splitAndBools, + destructEq, -- patterns pattern TrueBool, pattern FalseBool, @@ -36,18 +37,20 @@ import Booster.Definition.Attributes.Base ( pattern IsNotMacroOrAlias, ) import Booster.Pattern.Base ( - Pattern, + Pattern (..), Predicate (..), Symbol (Symbol), Term, - constraints, + Variable, pattern DomainValue, + pattern KSeq, pattern SortBool, pattern SortInt, pattern SortK, pattern SortKItem, pattern SortSet, pattern SymbolApplication, + pattern Var, ) import Booster.Pattern.Util (isConcrete) import Booster.SMT.Base (SExpr (Atom), SMTId (..)) @@ -206,3 +209,12 @@ splitAndBools :: Predicate -> [Predicate] splitAndBools p@(Predicate t) | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r] | otherwise = [p] + +-- | Pattern match on an equality predicate and try extracting a variable assignment +destructEq :: Predicate -> Maybe (Variable, Term) +destructEq = \case + Predicate (EqualsInt (Var x) t) -> Just (x, t) + Predicate (EqualsBool (Var x) t) -> Just (x, t) + Predicate + (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) + _ -> Nothing diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index c25ab28adf..a310d89990 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -37,7 +37,7 @@ import Data.List (intersperse, partition) import Data.List.NonEmpty (NonEmpty (..), toList) import Data.List.NonEmpty qualified as NE import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe) +import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe) import Data.Sequence (Seq, (|>)) import Data.Set qualified as Set import Data.Text as Text (Text, pack) @@ -50,9 +50,11 @@ import Booster.LLVM as LLVM (API) import Booster.Log import Booster.Pattern.ApplyEquations ( CacheTag (Equations), + Direction (..), EquationFailure (..), SimplifierCache (..), evaluatePattern, + evaluateTerm, simplifyConstraint, ) import Booster.Pattern.Base @@ -347,8 +349,7 @@ applyRule pat@Pattern{ceilConditions} rule = ("New path condition ensured, invalidating cache" :: Text) lift . RewriteT . lift . modify $ \s -> s{equations = mempty} - let isSubstitution = const False - (_newSubsitutionItems, newConstraints) = partition isSubstitution ensuredConditions + let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions -- existential variables may be present in rule.rhs and rule.ensures, -- need to strip prefixes and freshen their names with respect to variables already @@ -362,22 +363,62 @@ applyRule pat@Pattern{ceilConditions} rule = (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) rule.existentials + normalisedPatternSubst <- + lift $ normaliseSubstitution pat.constraints pat.substitution newSubsitution + -- modify the substitution to include the existentials - let substWithExistentials = subst `Map.union` existentialSubst + let substWithExistentials = subst <> existentialSubst let rewritten = Pattern - (substituteInTerm substWithExistentials rule.rhs) + (substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials $ rule.rhs) -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables ( pat.constraints - <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) + <> ( Set.fromList $ + map + (coerce . substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials . coerce) + newConstraints + ) ) - pat.substitution + normalisedPatternSubst ceilConditions withContext CtxSuccess $ withPatternContext rewritten $ return (rule, rewritten) where + -- extract substitution items from a list of generic predicates. Return empty substitution if none are found + partitionPredicates :: [Predicate] -> (Substitution, [Predicate]) + partitionPredicates ps = + let (substItems, normalPreds) = partition (isJust . destructEq) ps + in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) + + -- Given known predicates, a known substitution and a newly acquired substitution (from the ensures clause): + -- - apply the new substitution to the old substitution + -- - simplify the substituted old substitution, assuming known truth + -- - TODO check for loops? + -- - filter out possible trivial items + -- - finally, merge with the new substitution items and return + normaliseSubstitution :: + Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution + normaliseSubstitution knownTruth oldSubst newSubst = do + RewriteConfig{definition, llvmApi, smtSolver} <- RewriteT ask + let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst + simplifiedSubstitution <- + processResults + <$> traverse + (fmap fst . evaluateTerm BottomUp definition llvmApi smtSolver knownTruth) + substitutedOldSubst + pure (newSubst `Map.union` simplifiedSubstitution) -- new bindings take priority + where + processResults = + Map.fromList + . mapMaybe + ( \case + (var, Left _err) -> (var,) <$> Map.lookup var oldSubst + (var, Right simplified) -> Just (var, simplified) + ) + . Map.assocs + filterOutKnownConstraints :: Set.Set Predicate -> [Predicate] -> RewriteT io [Predicate] filterOutKnownConstraints priorKnowledge constraitns = do let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns From f98f4b5994b60b847cdeab1f8b6fae12fa01d30e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 15 Oct 2024 18:25:10 +0200 Subject: [PATCH 04/36] Include ensured substitution when externalising pattern --- .../Booster/Syntax/Json/Externalise.hs | 9 +- .../response-circular-equations.booster-dev | 204 ++++++++---------- ...response-concrete-substitution.booster-dev | 168 --------------- ...onse-symbolic-bottom-predicate.booster-dev | 51 ++++- ...response-symbolic-substitution.booster-dev | 168 --------------- 5 files changed, 134 insertions(+), 466 deletions(-) delete mode 100644 booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index 4c0ba5e8eb..0ab43c68d2 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -32,14 +32,15 @@ externalisePattern :: Internal.Pattern -> Map Internal.Variable Internal.Term -> (Syntax.KorePattern, Maybe Syntax.KorePattern, Maybe Syntax.KorePattern) -externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} substitutions = +externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - substitution = + substitutions = inputSubstitution <> ensuredSubstitution + externalisedSubstitution = if null substitutions then Nothing else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions - predicate = + externalisedPredicate = if null constraints && null ceilConditions then Nothing else @@ -47,7 +48,7 @@ externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} su multiAnd sort $ map (externalisePredicate sort) (Set.toList constraints) ++ map (externaliseCeil sort) ceilConditions - in (externaliseTerm term, predicate, substitution) + in (externaliseTerm term, externalisedPredicate, externalisedSubstitution) where multiAnd :: Syntax.Sort -> [Syntax.KorePattern] -> Syntax.KorePattern multiAnd _ [] = error "multiAnd: empty" diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index 259a441aeb..541a870442 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -66,13 +66,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -82,29 +82,13 @@ "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "43" } ] }, @@ -128,57 +112,6 @@ } }, "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - }, - "predicate": { "format": "KORE", "version": 1, "term": { @@ -193,7 +126,7 @@ "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -202,45 +135,29 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } }, { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -249,43 +166,94 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "Y", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "name": "Lbl'UndsPlus'Int'Unds'", "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "42" + } } ] } } ] } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + } } } } -} \ No newline at end of file +} diff --git a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev deleted file mode 100644 index 379ed33ccc..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev +++ /dev/null @@ -1,168 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 1, - "rule": "TEST.concrete-subst", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev index 8196839aaa..3508bd0d0a 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev @@ -67,7 +67,7 @@ "args": [ { "tag": "EVar", - "name": "X", + "name": "Y", "sort": { "tag": "SortApp", "name": "SortInt", @@ -111,6 +111,41 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Y", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + }, "predicate": { "format": "KORE", "version": 1, @@ -155,22 +190,22 @@ "sorts": [], "args": [ { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } }, { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" } ] } @@ -180,4 +215,4 @@ } } } -} \ No newline at end of file +} diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev deleted file mode 100644 index 5cf51a99bb..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev +++ /dev/null @@ -1,168 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 1, - "rule": "TEST.symbolic-subst", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file From b4502f9a65006bd0b59cc9a0e7bd7c2cda63cdd9 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 08:53:28 +0200 Subject: [PATCH 05/36] Update integration test output --- .../response-infeasible-branching.booster-dev | 48 ++++++----------- .../response-symbolic-bottom-predicate.json | 51 ++++++++++++++++--- .../response-test1.json | 41 +++++++++++++-- .../response-test2.json | 43 ++++++++++++++-- 4 files changed, 136 insertions(+), 47 deletions(-) diff --git a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev index ce99ad8ff6..c96f33b892 100644 --- a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev +++ b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev @@ -67,13 +67,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -96,14 +96,14 @@ ] } }, - "predicate": { + "substitution": { "format": "KORE", "version": 1, "term": { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -112,38 +112,22 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index 8196839aaa..3508bd0d0a 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -67,7 +67,7 @@ "args": [ { "tag": "EVar", - "name": "X", + "name": "Y", "sort": { "tag": "SortApp", "name": "SortInt", @@ -111,6 +111,41 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Y", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + } + }, "predicate": { "format": "KORE", "version": 1, @@ -155,22 +190,22 @@ "sorts": [], "args": [ { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } }, { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" } ] } @@ -180,4 +215,4 @@ } } } -} \ No newline at end of file +} diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json index caf1cf3ac9..53868dd52c 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json @@ -63,13 +63,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -92,6 +92,41 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" + } + } + }, "predicate": { "format": "KORE", "version": 1, diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json index 9d24d95c64..2cdb8abdac 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json @@ -63,13 +63,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -92,6 +92,41 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" + } + } + }, "predicate": { "format": "KORE", "version": 1, @@ -145,4 +180,4 @@ } } } -} +} \ No newline at end of file From aee79b7abd2162e48a22b1086ccdff50e2a5183d Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 13:49:59 +0200 Subject: [PATCH 06/36] Add substitution conversion helpers --- booster/library/Booster/Pattern/Bool.hs | 16 +++++++++++++++- .../library/Booster/Syntax/Json/Internalise.hs | 18 ++++-------------- 2 files changed, 19 insertions(+), 15 deletions(-) diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index dd107cce9d..0e5ba5fbaa 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -10,7 +10,9 @@ module Booster.Pattern.Bool ( negateBool, splitBoolPredicates, splitAndBools, + mkEq, destructEq, + asEquations, -- patterns pattern TrueBool, pattern FalseBool, @@ -25,6 +27,8 @@ module Booster.Pattern.Bool ( ) where import Data.ByteString.Char8 (ByteString) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map import Booster.Definition.Attributes.Base ( FunctionType (..), @@ -52,7 +56,7 @@ import Booster.Pattern.Base ( pattern SymbolApplication, pattern Var, ) -import Booster.Pattern.Util (isConcrete) +import Booster.Pattern.Util (isConcrete, sortOfTerm) import Booster.SMT.Base (SExpr (Atom), SMTId (..)) pattern HookedTotalFunction :: ByteString -> SymbolAttributes @@ -210,6 +214,12 @@ splitAndBools p@(Predicate t) | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r] | otherwise = [p] +mkEq :: Variable -> Term -> Predicate +mkEq x t = Predicate $ case sortOfTerm t of + SortInt -> EqualsInt (Var x) t + SortBool -> EqualsBool (Var x) t + otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t) + -- | Pattern match on an equality predicate and try extracting a variable assignment destructEq :: Predicate -> Maybe (Variable, Term) destructEq = \case @@ -218,3 +228,7 @@ destructEq = \case Predicate (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) _ -> Nothing + +-- | turns a substitution into a list of equations +asEquations :: Map Variable Term -> [Predicate] +asEquations = map (uncurry mkEq) . Map.assocs diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 9b326cd85a..2547eab58d 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -463,7 +463,7 @@ mkSubstitution initialSubst = Map.partition ((== 1) . length) $ Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst] equations = - [mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts] + [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts] in execState breakCycles (Map.map head substMap, equations) where breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) () @@ -477,20 +477,10 @@ mkSubstitution initialSubst = else do modify $ \(m, eqs) -> ( m `Map.withoutKeys` cycleNodes - , eqs <> (map (uncurry mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes) + , eqs <> (map (uncurry Internal.mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes) ) breakCycles -mkEq :: Internal.Variable -> Internal.Term -> Internal.Predicate -mkEq x t = Internal.Predicate $ case sortOfTerm t of - Internal.SortInt -> Internal.EqualsInt (Internal.Var x) t - Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t - otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t) - --- | turns a substitution into a list of equations -asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate] -asEquations = map (uncurry mkEq) . Map.assocs - internalisePred :: Flag "alias" -> Flag "subsorts" -> @@ -562,12 +552,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort pure [BoolPred $ Internal.Predicate $ Internal.NotBool x] (_, Internal.Var x, t) | x `Set.member` freeVariables t -> - pure [BoolPred $ mkEq x t] + pure [BoolPred $ Internal.mkEq x t] | otherwise -> pure [SubstitutionPred x t] (_, t, Internal.Var x) | x `Set.member` freeVariables t -> - pure [BoolPred $ mkEq x t] + pure [BoolPred $ Internal.mkEq x t] | otherwise -> pure [SubstitutionPred x t] (Internal.SortInt, _, _) -> From 0f6ccf54b9b35e9de5aed7e7f034881fb8fc2690 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 14:32:03 +0200 Subject: [PATCH 07/36] Build existential substitution together with the matching one --- booster/library/Booster/Pattern/Rewrite.hs | 107 +++++++++++++-------- 1 file changed, 67 insertions(+), 40 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index a310d89990..e09bcc39b6 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -304,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule = NE.toList remainder ) failRewrite $ RuleApplicationUnclear rule pat.term remainder - MatchSuccess substitution -> do + MatchSuccess matchingSubstitution -> do + -- existential variables may be present in rule.rhs and rule.ensures, + -- need to strip prefixes and freshen their names with respect to variables already + -- present in the input pattern and in the unification substitution + varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) + let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) + varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution + forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst + existentialSubst = + Map.fromSet + (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) + rule.existentials + combinedSubstitution = matchingSubstitution <> existentialSubst + withContext CtxSuccess $ do logMessage rule withContext CtxSubstitution $ logMessage $ WithJsonMessage ( object - ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)] + [ "substitution" + .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList combinedSubstitution) + ] ) $ renderOneLineText $ "Substitution:" <+> ( hsep $ intersperse "," $ map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ - Map.toList substitution + Map.toList combinedSubstitution ) - pure substitution + pure combinedSubstitution -- Also fail the whole rewrite if a rule applies but may introduce -- an undefined term. @@ -349,37 +364,29 @@ applyRule pat@Pattern{ceilConditions} rule = ("New path condition ensured, invalidating cache" :: Text) lift . RewriteT . lift . modify $ \s -> s{equations = mempty} + -- partition ensured constrains into substitution and predicates let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions - -- existential variables may be present in rule.rhs and rule.ensures, - -- need to strip prefixes and freshen their names with respect to variables already - -- present in the input pattern and in the unification substitution - varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) - let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) - varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst - forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst - existentialSubst = - Map.fromSet - (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) - rule.existentials - + -- merge existing substitution and newly acquired one, applying the latter to the former normalisedPatternSubst <- - lift $ normaliseSubstitution pat.constraints pat.substitution newSubsitution - - -- modify the substitution to include the existentials - let substWithExistentials = subst <> existentialSubst - + lift $ + normaliseSubstitution + pat.constraints + pat.substitution + newSubsitution + -- NOTE it is necessary to first apply the rule substitution and then the pattern/ensures substitution, but it is suboptimal to traverse the term twice. + -- TODO a substitution composition operator + let rewrittenTerm = substituteInTerm normalisedPatternSubst . substituteInTerm subst $ rule.rhs + substitutedNewConstraints = + Set.fromList $ + map + (coerce . substituteInTerm normalisedPatternSubst . substituteInTerm subst . coerce) + newConstraints let rewritten = Pattern - (substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials $ rule.rhs) + rewrittenTerm -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables - ( pat.constraints - <> ( Set.fromList $ - map - (coerce . substituteInTerm normalisedPatternSubst . substituteInTerm substWithExistentials . coerce) - newConstraints - ) - ) + (pat.constraints <> substitutedNewConstraints) normalisedPatternSubst ceilConditions withContext CtxSuccess $ @@ -396,7 +403,7 @@ applyRule pat@Pattern{ceilConditions} rule = -- - apply the new substitution to the old substitution -- - simplify the substituted old substitution, assuming known truth -- - TODO check for loops? - -- - filter out possible trivial items + -- - TODO filter out possible trivial items? -- - finally, merge with the new substitution items and return normaliseSubstitution :: Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution @@ -470,23 +477,36 @@ applyRule pat@Pattern{ceilConditions} rule = 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 + toCheck <- + lift $ + filterOutKnownConstraints + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + 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 + catMaybes + <$> mapM + ( checkConstraint + id + notAppliedIfBottom + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + ) + 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 + stillUnclear <- + lift $ + filterOutKnownConstraints + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + unclearRequires -- check unclear requires-clauses in the context of known constraints (priorKnowledge) solver <- lift $ RewriteT $ (.smtSolver) <$> ask - SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case - SMT.IsUnknown reason -> do - -- abort rewrite if a solver result was Unknown - withContext CtxAbort $ logMessage reason - smtUnclear stillUnclear + SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case + SMT.IsUnknown{} -> + smtUnclear stillUnclear -- 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) @@ -500,13 +520,20 @@ applyRule pat@Pattern{ceilConditions} rule = let ruleEnsures = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures newConstraints <- - catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures + catMaybes + <$> mapM + ( checkConstraint + id + trivialIfBottom + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + ) + ruleEnsures -- check all new constraints together with the known side constraints solver <- lift $ RewriteT $ (.smtSolver) <$> ask -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions. -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)). - (lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case + (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case SMT.IsInvalid -> do withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial From 7c7a4ba94f77c6b33b5086f9ff9ed9cb3f1b78d1 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 14:59:48 +0200 Subject: [PATCH 08/36] Fix imports --- booster/library/Booster/Syntax/Json/Internalise.hs | 1 - booster/library/Booster/Syntax/ParsedKore/Internalise.hs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 2547eab58d..1c9c77de98 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -24,7 +24,6 @@ module Booster.Syntax.Json.Internalise ( textToBS, trm, handleBS, - asEquations, TermOrPredicates (..), InternalisedPredicates (..), PatternOrTopOrBottom (..), diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 5c258cba73..d0b5262b5e 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -54,7 +54,7 @@ import Booster.Definition.Base as Def import Booster.Pattern.Base (Predicate (Predicate), Variable (..)) import Booster.Pattern.Base qualified as Def import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..)) -import Booster.Pattern.Bool (foldAndBool, pattern TrueBool) +import Booster.Pattern.Bool (asEquations, foldAndBool, pattern TrueBool) import Booster.Pattern.Index as Idx import Booster.Pattern.Pretty import Booster.Pattern.Util qualified as Util From 82f0955b6f4a5e1a25c3bb5eeef0d2cd61417239 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 19:29:06 +0200 Subject: [PATCH 09/36] Move partitionPredicates to Booster.Pattern.Bool --- booster/library/Booster/Pattern/Bool.hs | 9 +++++++++ booster/library/Booster/Pattern/Rewrite.hs | 8 +------- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 0e5ba5fbaa..f59305c494 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -13,6 +13,7 @@ module Booster.Pattern.Bool ( mkEq, destructEq, asEquations, + partitionPredicates, -- patterns pattern TrueBool, pattern FalseBool, @@ -27,8 +28,10 @@ module Booster.Pattern.Bool ( ) where import Data.ByteString.Char8 (ByteString) +import Data.List (partition) import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map +import Data.Maybe (isJust, mapMaybe) import Booster.Definition.Attributes.Base ( FunctionType (..), @@ -232,3 +235,9 @@ destructEq = \case -- | turns a substitution into a list of equations asEquations :: Map Variable Term -> [Predicate] asEquations = map (uncurry mkEq) . Map.assocs + +-- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found +partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate]) +partitionPredicates ps = + let (substItems, normalPreds) = partition (isJust . destructEq) ps + in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index e09bcc39b6..82f6fee0e0 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -37,7 +37,7 @@ import Data.List (intersperse, partition) import Data.List.NonEmpty (NonEmpty (..), toList) import Data.List.NonEmpty qualified as NE import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe) +import Data.Maybe (catMaybes, fromMaybe, mapMaybe) import Data.Sequence (Seq, (|>)) import Data.Set qualified as Set import Data.Text as Text (Text, pack) @@ -393,12 +393,6 @@ applyRule pat@Pattern{ceilConditions} rule = withPatternContext rewritten $ return (rule, rewritten) where - -- extract substitution items from a list of generic predicates. Return empty substitution if none are found - partitionPredicates :: [Predicate] -> (Substitution, [Predicate]) - partitionPredicates ps = - let (substItems, normalPreds) = partition (isJust . destructEq) ps - in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) - -- Given known predicates, a known substitution and a newly acquired substitution (from the ensures clause): -- - apply the new substitution to the old substitution -- - simplify the substituted old substitution, assuming known truth From 20c10ef70271011e65f2543dccd474bbcb817eff Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 13:50:35 +0200 Subject: [PATCH 10/36] Consider substitution as constraints in evaluatePattern Include substitution in known truth when simplifying --- .../library/Booster/Pattern/ApplyEquations.hs | 27 ++++++++-- .../response-test1.json | 51 ------------------- .../response-test2.json | 51 ------------------- 3 files changed, 24 insertions(+), 105 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 590fc1234e..20f0c34101 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -455,21 +455,42 @@ evaluatePattern :: Pattern -> io (Either EquationFailure Pattern, SimplifierCache) evaluatePattern def mLlvmLibrary smtSolver cache pat = - runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat + runEquationT + def + mLlvmLibrary + smtSolver + cache + -- interpret substitution as additional known constraints + (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + . evaluatePattern' + $ pat -- version for internal nested evaluation evaluatePattern' :: LoggerMIO io => Pattern -> EquationT io Pattern -evaluatePattern' pat@Pattern{term, ceilConditions, substitution} = withPatternContext pat $ do +evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults -- after evaluating the term, evaluate all (existing and -- newly-acquired) constraints, once traverse_ simplifyAssumedPredicate . predicates =<< getState -- this may yield additional new constraints, left unevaluated evaluatedConstraints <- predicates <$> getState - pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions, substitution} + -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints + -- into the simplifier state as known truth. Here the substitution will bubble-up as part of + -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities + -- in pat.predicate and pat.substitution), we discard the old substitution here + -- and extract a possible simplified one from evaluatedConstraints. + let (simplifiedSubsitution, simplifiedConstraints) = partitionPredicates (Set.toList evaluatedConstraints) + + pure + Pattern + { constraints = Set.fromList simplifiedConstraints + , term = newTerm + , ceilConditions + , substitution = simplifiedSubsitution + } where -- when TooManyIterations exception occurred while evaluating the top-level term, -- i.e. not in a recursive evaluation of a side-condition, diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json index 53868dd52c..f0938023a3 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json @@ -126,57 +126,6 @@ "value": "42" } } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] - } - } } } } diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json index 2cdb8abdac..8b9792046d 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json @@ -126,57 +126,6 @@ "value": "42" } } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] - } - } } } } From 8b6fbfd0619ff2158b0e2850c774d53f4923bbea Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 19:32:31 +0200 Subject: [PATCH 11/36] Delete obsolete booster-dev responses --- ...ponse-mutual-constraints-stuck.booster-dev | 134 ------------------ ...se-mutual-constraints-terminal.booster-dev | 119 ---------------- .../response-circular-equations.booster-dev | 51 ------- ...onse-symbolic-bottom-predicate.booster-dev | 67 --------- 4 files changed, 371 deletions(-) delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev deleted file mode 100644 index 12b421e0d0..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev +++ /dev/null @@ -1,134 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev deleted file mode 100644 index 92827d7008..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev +++ /dev/null @@ -1,119 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index 541a870442..6e34d0543d 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -202,57 +202,6 @@ } ] } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev index 3508bd0d0a..fe33f615ea 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev @@ -145,73 +145,6 @@ } } } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] - } - ] - } - } } } } From ac825e6eabe878d0429b43d7700eabedf0e9e87e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 16 Oct 2024 19:59:58 +0200 Subject: [PATCH 12/36] Include input substitution into the pattern --- booster/library/Booster/JsonRpc.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index da486edcc8..e834ca8003 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -137,7 +137,7 @@ respond stateVar request = { term = substituteInTerm substitution term , constraints = Set.fromList $ map (substituteInPredicate substitution) preds , ceilConditions = ceils - , substitution = mempty -- this is the ensures-substitution, leave empty + , substitution } -- remember all variables used in the substitutions substVars = @@ -255,7 +255,7 @@ respond stateVar request = { term = substituteInTerm substitution pat.term , constraints = Set.map (substituteInPredicate substitution) pat.constraints , ceilConditions = pat.ceilConditions - , substitution = mempty -- this is the ensures-substitution, leave empty + , substitution } ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case (Right newPattern, _) -> do @@ -290,7 +290,7 @@ respond stateVar request = mLlvmLibrary solver mempty - predicates + predicates -- TODO include ps.substitution? >>= \case (Right newPreds, _) -> do let predicateSort = From a6c7808ed54ddc6b6ce329c3e5a608b95443bc76 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 10:39:16 +0200 Subject: [PATCH 13/36] Extend Unknown type, abort on unsafe unknown ensures --- booster/library/Booster/Pattern/Rewrite.hs | 13 +++-- .../response-symbolic-bottom-predicate.json | 49 +++---------------- 2 files changed, 17 insertions(+), 45 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 82f6fee0e0..9256e812cd 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -307,7 +307,7 @@ applyRule pat@Pattern{ceilConditions} rule = MatchSuccess matchingSubstitution -> do -- existential variables may be present in rule.rhs and rule.ensures, -- need to strip prefixes and freshen their names with respect to variables already - -- present in the input pattern and in the unification substitution + -- present in the input pattern and in the matching substitution varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution @@ -499,8 +499,10 @@ applyRule pat@Pattern{ceilConditions} rule = -- check unclear requires-clauses in the context of known constraints (priorKnowledge) solver <- lift $ RewriteT $ (.smtSolver) <$> ask SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case - SMT.IsUnknown{} -> - smtUnclear stillUnclear -- abort rewrite if a solver result was Unknown + SMT.IsUnknown reason -> do + -- abort rewrite if a solver result was Unknown + withContext CtxAbort $ logMessage reason + smtUnclear stillUnclear SMT.IsInvalid -> do -- requires is actually false given the prior withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) @@ -528,6 +530,11 @@ applyRule pat@Pattern{ceilConditions} rule = -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions. -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)). (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case + SMT.IsUnknown SMT.ImplicationIndeterminate -> do + pure () + SMT.IsUnknown SMT.InconsistentGroundTruth -> do + withContext CtxWarn $ logMessage ("Ground truth is #Bottom." :: Text) + RewriteRuleAppT $ pure Trivial SMT.IsInvalid -> do withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index 3508bd0d0a..8dd09608d8 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -67,7 +67,7 @@ "args": [ { "tag": "EVar", - "name": "Y", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", @@ -111,41 +111,6 @@ ] } }, - "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - } - }, "predicate": { "format": "KORE", "version": 1, @@ -190,22 +155,22 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "1" }, { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - }, - "value": "1" + } } ] } From ffc4035cfba92c5feef24fab6369b5d6f23df23f Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 12:04:51 +0200 Subject: [PATCH 14/36] Include substitution when pretty-printing Pattern --- booster/library/Booster/Log.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index 5e862f8345..d4ec1e3b73 100644 --- a/booster/library/Booster/Log.hs +++ b/booster/library/Booster/Log.hs @@ -68,6 +68,7 @@ import Booster.Pattern.Base ( TermAttributes (hash), pattern AndTerm, ) +import Booster.Pattern.Bool (asEquations) import Booster.Pattern.Pretty import Booster.Prettyprinter (renderOneLineText) import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern) @@ -185,8 +186,8 @@ withTermContext t@(Term attrs _) m = m withPatternContext :: LoggerMIO m => Pattern -> m a -> m a -withPatternContext Pattern{term, constraints} m = - let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME +withPatternContext Pattern{term, constraints, substitution} m = + let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution in withTermContext t' m instance ToLogFormat KorePattern where From 32a84181040f6184812565d8d38d6534bdc18f66 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 12:20:33 +0200 Subject: [PATCH 15/36] Fix substitution externalisation --- booster/library/Booster/Syntax/Json/Externalise.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index 0ab43c68d2..f130a801d7 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -35,7 +35,7 @@ externalisePattern :: externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - substitutions = inputSubstitution <> ensuredSubstitution + substitutions = ensuredSubstitution <> inputSubstitution -- TODO ensuredSubstitution takes priority. Do we even need inputSubstitution? externalisedSubstitution = if null substitutions then Nothing From 7da0911f6821ee4cc0aa2ba165ff179b68eae5cb Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 12:23:59 +0200 Subject: [PATCH 16/36] Do not simplify substitution when normalising it --- booster/library/Booster/Pattern/Rewrite.hs | 32 ++++------------------ 1 file changed, 5 insertions(+), 27 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 9256e812cd..1c04ed7d1d 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -37,7 +37,7 @@ import Data.List (intersperse, partition) import Data.List.NonEmpty (NonEmpty (..), toList) import Data.List.NonEmpty qualified as NE import Data.Map qualified as Map -import Data.Maybe (catMaybes, fromMaybe, mapMaybe) +import Data.Maybe (catMaybes, fromMaybe) import Data.Sequence (Seq, (|>)) import Data.Set qualified as Set import Data.Text as Text (Text, pack) @@ -50,11 +50,9 @@ import Booster.LLVM as LLVM (API) import Booster.Log import Booster.Pattern.ApplyEquations ( CacheTag (Equations), - Direction (..), EquationFailure (..), SimplifierCache (..), evaluatePattern, - evaluateTerm, simplifyConstraint, ) import Booster.Pattern.Base @@ -371,7 +369,6 @@ applyRule pat@Pattern{ceilConditions} rule = normalisedPatternSubst <- lift $ normaliseSubstitution - pat.constraints pat.substitution newSubsitution -- NOTE it is necessary to first apply the rule substitution and then the pattern/ensures substitution, but it is suboptimal to traverse the term twice. @@ -395,31 +392,12 @@ applyRule pat@Pattern{ceilConditions} rule = where -- Given known predicates, a known substitution and a newly acquired substitution (from the ensures clause): -- - apply the new substitution to the old substitution - -- - simplify the substituted old substitution, assuming known truth - -- - TODO check for loops? - -- - TODO filter out possible trivial items? - -- - finally, merge with the new substitution items and return + -- - merge with the new substitution items and return normaliseSubstitution :: - Set.Set Predicate -> Substitution -> Substitution -> RewriteT io Substitution - normaliseSubstitution knownTruth oldSubst newSubst = do - RewriteConfig{definition, llvmApi, smtSolver} <- RewriteT ask + Substitution -> Substitution -> RewriteT io Substitution + normaliseSubstitution oldSubst newSubst = do let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst - simplifiedSubstitution <- - processResults - <$> traverse - (fmap fst . evaluateTerm BottomUp definition llvmApi smtSolver knownTruth) - substitutedOldSubst - pure (newSubst `Map.union` simplifiedSubstitution) -- new bindings take priority - where - processResults = - Map.fromList - . mapMaybe - ( \case - (var, Left _err) -> (var,) <$> Map.lookup var oldSubst - (var, Right simplified) -> Just (var, simplified) - ) - . Map.assocs - + pure (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority filterOutKnownConstraints :: Set.Set Predicate -> [Predicate] -> RewriteT io [Predicate] filterOutKnownConstraints priorKnowledge constraitns = do let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns From 9f1134376a67c942ee2d22fc97caf9644ea8d264 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 14:37:55 +0200 Subject: [PATCH 17/36] Kill redundant patterns --- booster/library/Booster/Pattern/Rewrite.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 1c04ed7d1d..0a63f41dc7 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -508,11 +508,6 @@ applyRule pat@Pattern{ceilConditions} rule = -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions. -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)). (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case - SMT.IsUnknown SMT.ImplicationIndeterminate -> do - pure () - SMT.IsUnknown SMT.InconsistentGroundTruth -> do - withContext CtxWarn $ logMessage ("Ground truth is #Bottom." :: Text) - RewriteRuleAppT $ pure Trivial SMT.IsInvalid -> do withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial From 9e47e06802b8d3949fd6d12c46551fbf6c5a3177 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 15:10:46 +0200 Subject: [PATCH 18/36] Move substitution-related stuff into a separate module Fix unit tests add test --- booster/library/Booster/JsonRpc.hs | 13 ++- booster/library/Booster/Log.hs | 2 +- .../library/Booster/Pattern/ApplyEquations.hs | 1 + booster/library/Booster/Pattern/Bool.hs | 38 +-------- booster/library/Booster/Pattern/Implies.hs | 14 ++-- booster/library/Booster/Pattern/Match.hs | 8 +- booster/library/Booster/Pattern/Rewrite.hs | 1 + .../library/Booster/Pattern/Substitution.hs | 84 +++++++++++++++++++ booster/library/Booster/Pattern/Util.hs | 24 ------ .../Booster/Syntax/Json/Internalise.hs | 1 + .../Booster/Syntax/ParsedKore/Internalise.hs | 13 +-- .../Test/Booster/Pattern/Substitution.hs | 84 +++++++++++++++++++ .../unit-tests/Test/Booster/Pattern/Util.hs | 56 ------------- 13 files changed, 199 insertions(+), 140 deletions(-) create mode 100644 booster/library/Booster/Pattern/Substitution.hs create mode 100644 booster/unit-tests/Test/Booster/Pattern/Substitution.hs diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index e834ca8003..189475787d 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite ( RewriteTrace (..), performRewrite, ) +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util ( freeVariables, sortOfPattern, sortOfTerm, - substituteInPredicate, - substituteInTerm, ) import Booster.Prettyprinter (renderText) import Booster.SMT.Interface qualified as SMT @@ -134,8 +133,8 @@ respond stateVar request = -- apply the given substitution before doing anything else let substPat = Pattern - { term = substituteInTerm substitution term - , constraints = Set.fromList $ map (substituteInPredicate substitution) preds + { term = Substitution.substituteInTerm substitution term + , constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds , ceilConditions = ceils , substitution } @@ -252,8 +251,8 @@ respond stateVar request = -- apply the given substitution before doing anything else let substPat = Pattern - { term = substituteInTerm substitution pat.term - , constraints = Set.map (substituteInPredicate substitution) pat.constraints + { term = Substitution.substituteInTerm substitution pat.term + , constraints = Set.map (Substitution.substituteInPredicate substitution) pat.constraints , ceilConditions = pat.ceilConditions , substitution } @@ -283,7 +282,7 @@ respond stateVar request = withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do logMessage ("ignoring unsupported predicate parts" :: Text) -- apply the given substitution before doing anything else - let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates + let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates withContext CtxConstraint $ ApplyEquations.simplifyConstraints def diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index d4ec1e3b73..8cf4e9b36d 100644 --- a/booster/library/Booster/Log.hs +++ b/booster/library/Booster/Log.hs @@ -68,8 +68,8 @@ import Booster.Pattern.Base ( TermAttributes (hash), pattern AndTerm, ) -import Booster.Pattern.Bool (asEquations) import Booster.Pattern.Pretty +import Booster.Pattern.Substitution (asEquations) import Booster.Prettyprinter (renderOneLineText) import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern) import Booster.Syntax.Json.Externalise (externaliseTerm) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 20f0c34101..166b18aaea 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -66,6 +66,7 @@ import Booster.Pattern.Bool import Booster.Pattern.Index qualified as Idx import Booster.Pattern.Match import Booster.Pattern.Pretty +import Booster.Pattern.Substitution import Booster.Pattern.Util import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index f59305c494..a232a86239 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/booster/library/Booster/Pattern/Bool.hs @@ -10,10 +10,6 @@ module Booster.Pattern.Bool ( negateBool, splitBoolPredicates, splitAndBools, - mkEq, - destructEq, - asEquations, - partitionPredicates, -- patterns pattern TrueBool, pattern FalseBool, @@ -28,10 +24,6 @@ module Booster.Pattern.Bool ( ) where import Data.ByteString.Char8 (ByteString) -import Data.List (partition) -import Data.Map.Strict (Map) -import Data.Map.Strict qualified as Map -import Data.Maybe (isJust, mapMaybe) import Booster.Definition.Attributes.Base ( FunctionType (..), @@ -48,18 +40,15 @@ import Booster.Pattern.Base ( Predicate (..), Symbol (Symbol), Term, - Variable, pattern DomainValue, - pattern KSeq, pattern SortBool, pattern SortInt, pattern SortK, pattern SortKItem, pattern SortSet, pattern SymbolApplication, - pattern Var, ) -import Booster.Pattern.Util (isConcrete, sortOfTerm) +import Booster.Pattern.Util (isConcrete) import Booster.SMT.Base (SExpr (Atom), SMTId (..)) pattern HookedTotalFunction :: ByteString -> SymbolAttributes @@ -216,28 +205,3 @@ splitAndBools :: Predicate -> [Predicate] splitAndBools p@(Predicate t) | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r] | otherwise = [p] - -mkEq :: Variable -> Term -> Predicate -mkEq x t = Predicate $ case sortOfTerm t of - SortInt -> EqualsInt (Var x) t - SortBool -> EqualsBool (Var x) t - otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t) - --- | Pattern match on an equality predicate and try extracting a variable assignment -destructEq :: Predicate -> Maybe (Variable, Term) -destructEq = \case - Predicate (EqualsInt (Var x) t) -> Just (x, t) - Predicate (EqualsBool (Var x) t) -> Just (x, t) - Predicate - (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) - _ -> Nothing - --- | turns a substitution into a list of equations -asEquations :: Map Variable Term -> [Predicate] -asEquations = map (uncurry mkEq) . Map.assocs - --- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found -partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate]) -partitionPredicates ps = - let (substItems, normalPreds) = partition (isJust . destructEq) ps - in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 28251a71ca..e7cdfad700 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -26,7 +26,8 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..)) import Booster.Pattern.Bool (pattern TrueBool) import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms) import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty') -import Booster.Pattern.Util (freeVariables, sortOfPattern, substituteInPredicate, substituteInTerm) +import Booster.Pattern.Substitution qualified as Substitution +import Booster.Pattern.Util (freeVariables, sortOfPattern) import Booster.Prettyprinter (renderDefault) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json (addHeader, prettyPattern) @@ -108,15 +109,15 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = -- apply the given substitution before doing anything else substPatL = Pattern - { term = substituteInTerm substitutionL patL.term - , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints + { term = Substitution.substituteInTerm substitutionL patL.term + , constraints = Set.map (Substitution.substituteInPredicate substitutionL) patL.constraints , ceilConditions = patL.ceilConditions , substitution = substitutionL } substPatR = Pattern - { term = substituteInTerm substitutionR patR.term - , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints + { term = Substitution.substituteInTerm substitutionR patR.term + , constraints = Set.map (Substitution.substituteInPredicate substitutionR) patR.constraints , ceilConditions = patR.ceilConditions , substitution = substitutionR } @@ -158,7 +159,8 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = 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 + Set.map (Substitution.substituteInPredicate subst) substPatR.constraints + `Set.difference` substPatL.constraints if null filteredConsequentPreds then diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index b5ae619179..b85985f7eb 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -36,12 +36,12 @@ import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition, KSet import Booster.Definition.Base import Booster.Pattern.Base import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util ( checkSymbolIsAc, freeVariables, isConstructorSymbol, sortOfTerm, - substituteInTerm, ) -- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong) @@ -665,7 +665,7 @@ matchMaps -- before matching map keys. enqueueMapProblem (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest) else do - let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals + let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals -- check for duplicate keys checkDuplicateKeys patternKeyVals patRest checkDuplicateKeys subjKeyVals subjRest @@ -782,13 +782,13 @@ bindVariable matchType var term@(Term termAttrs _) = do Nothing -> do let -- apply existing substitutions to term - term' = substituteInTerm currentSubst term + term' = Substitution.substituteInTerm currentSubst term when (var `Set.member` freeVariables term') $ failWith (VariableRecursion var term) let -- substitute in existing substitution terms currentSubst' = - Map.map (substituteInTerm $ Map.singleton var term') currentSubst + Map.map (Substitution.substituteInTerm $ Map.singleton var term') currentSubst newSubst = Map.insert var term' currentSubst' modify $ \s -> s{mSubstitution = newSubst} diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 0a63f41dc7..584000cb68 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -66,6 +66,7 @@ import Booster.Pattern.Match ( matchTerms, ) import Booster.Pattern.Pretty +import Booster.Pattern.Substitution import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs new file mode 100644 index 0000000000..fac9072927 --- /dev/null +++ b/booster/library/Booster/Pattern/Substitution.hs @@ -0,0 +1,84 @@ +{- | +Copyright : (c) Runtime Verification, 2024 +License : BSD-3-Clause + +Function to manipulate @'Substitution'@s and convert to/from @'Predicate'@s + +This module is intended to be imported qualified. +-} +module Booster.Pattern.Substitution ( + mkEq, + destructEq, + asEquations, + partitionPredicates, + compose, + substituteInPredicate, + substituteInTerm, +) where + +import Data.Bifunctor (bimap) +import Data.Coerce (coerce) +import Data.List (partition) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (fromMaybe, isJust, mapMaybe) +import Data.Set qualified as Set + +import Booster.Pattern.Base +import Booster.Pattern.Bool +import Booster.Pattern.Util (sortOfTerm) + +compose :: Substitution -> Substitution -> Substitution +compose newSubst oldSubst = + let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst + in (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority + +-- | Build an equality predicate form a variable assignment +mkEq :: Variable -> Term -> Predicate +mkEq x t = Predicate $ case sortOfTerm t of + SortInt -> EqualsInt (Var x) t + SortBool -> EqualsBool (Var x) t + otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t) + +{- | Pattern match on an equality predicate and try extracting a variable assignment. + This is a partial inverse of @'mkEq'@ +-} +destructEq :: Predicate -> Maybe (Variable, Term) +destructEq = \case + Predicate (EqualsInt (Var x) t) -> Just (x, t) + Predicate (EqualsBool (Var x) t) -> Just (x, t) + Predicate + (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) + _ -> Nothing + +-- | turns a substitution into a list of equations +asEquations :: Map Variable Term -> [Predicate] +asEquations = map (uncurry mkEq) . Map.assocs + +-- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found +partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate]) +partitionPredicates ps = + let (substItems, normalPreds) = partition (isJust . destructEq) ps + in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) + +substituteInTerm :: Substitution -> Term -> Term +substituteInTerm substitution = goSubst + where + targetSet = Map.keysSet substitution + goSubst t + | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t + | otherwise = case t of + Var v -> fromMaybe t (Map.lookup v substitution) + DomainValue{} -> t + SymbolApplication sym sorts args -> + SymbolApplication sym sorts $ map goSubst args + AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2) + Injection ss s sub -> Injection ss s (goSubst sub) + KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest) + KList def heads rest -> + KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest) + KSet def elements rest -> + KSet def (map goSubst elements) (goSubst <$> rest) + +substituteInPredicate :: Substitution -> Predicate -> Predicate +substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index 0807d3f722..00a496420a 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -6,8 +6,6 @@ module Booster.Pattern.Util ( substituteInSort, sortOfTerm, sortOfPattern, - substituteInTerm, - substituteInPredicate, modifyVariables, modifyVariablesInT, modifyVariablesInP, @@ -82,28 +80,6 @@ substituteInSort subst (SortApp n args) = sortOfPattern :: Pattern -> Sort sortOfPattern pat = sortOfTerm pat.term -substituteInTerm :: Map Variable Term -> Term -> Term -substituteInTerm substitution = goSubst - where - targetSet = Map.keysSet substitution - goSubst t - | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t - | otherwise = case t of - Var v -> fromMaybe t (Map.lookup v substitution) - DomainValue{} -> t - SymbolApplication sym sorts args -> - SymbolApplication sym sorts $ map goSubst args - AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2) - Injection ss s sub -> Injection ss s (goSubst sub) - KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest) - KList def heads rest -> - KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest) - KSet def elements rest -> - KSet def (map goSubst elements) (goSubst <$> rest) - -substituteInPredicate :: Map Variable Term -> Predicate -> Predicate -substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce - modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern modifyVariables f p = Pattern diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 1c9c77de98..ab8b2060d3 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -71,6 +71,7 @@ import Booster.Log (LoggerMIO, logMessage, withKorePatternContext) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Internal import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort) import Booster.Prettyprinter (renderDefault) import Booster.Syntax.Json (addHeader) diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index d0b5262b5e..9e80c3dca7 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -54,9 +54,10 @@ import Booster.Definition.Base as Def import Booster.Pattern.Base (Predicate (Predicate), Variable (..)) import Booster.Pattern.Base qualified as Def import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..)) -import Booster.Pattern.Bool (asEquations, foldAndBool, pattern TrueBool) +import Booster.Pattern.Bool (foldAndBool, pattern TrueBool) import Booster.Pattern.Index as Idx import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util qualified as Util import Booster.Prettyprinter hiding (attributes) import Booster.Syntax.Json.Internalise @@ -788,7 +789,7 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref DefinitionPatternError ref (NotSupported (head unsupported)) pure ( Util.modifyVariablesInT f term - , map (Util.modifyVariablesInP f) (preds <> asEquations substitution) + , map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution) ) internaliseRewriteRuleNoAlias :: @@ -970,7 +971,7 @@ internaliseCeil partialDef left right sortVars attrs = do internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p] let -- turn substitution-like predicates back into equations - constraints = internalPs.boolPredicates <> asEquations internalPs.substitution + constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution unsupported = internalPs.unsupported unless (null unsupported) $ throwE $ @@ -1017,7 +1018,7 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att argPairs <- mapM internaliseArg args let lhs = Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) $ - Util.substituteInTerm (Map.fromList argPairs) left + Substitution.substituteInTerm (Map.fromList argPairs) left (rhs, ensures) <- internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDef @@ -1049,7 +1050,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att { lhs , rhs , requires = - map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution) + map + (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) + (preds <> Substitution.asEquations substitution) , ensures , attributes , computedAttributes diff --git a/booster/unit-tests/Test/Booster/Pattern/Substitution.hs b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs new file mode 100644 index 0000000000..248a10f250 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE QuasiQuotes #-} + +module Test.Booster.Pattern.Substitution ( + test_subst, +) where + +import Data.Map qualified as Map +import Test.Tasty +import Test.Tasty.HUnit + +import Booster.Definition.Attributes.Base +import Booster.Pattern.Base +import Booster.Pattern.Substitution +import Booster.Syntax.Json.Internalise (trm) + +test_subst :: TestTree +test_subst = + testGroup + "Substitution" + [ testGroup + "Application" + [ test + "con1(X)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + ([trm| con1{}(X:SomeSort{}) |]) + ([trm| con1{}(con1{}(Y:SomeSort{})) |]) + , test + "con1(X)/\\con1(X)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(X:SomeSort{}) |])) + (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(con1{}(Y:SomeSort{})) |])) + , test + "con1(X)/\\con1(Y)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(Y:SomeSort{}) |])) + (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(Y:SomeSort{}) |])) + ] + , testGroup + "Composition" + [ testCase + "compose is idempotent" + $ (("X" |-> [trm| con1{}(Y:SomeSort{}) |]) `compose` ("X" |-> [trm| con1{}(Y:SomeSort{}) |])) + @?= ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + , testCase + "compose is transitive and saturating" + $ (("X" |-> [trm| Z:SomeSort{} |]) `compose` ("Y" |-> [trm| X:SomeSort{} |])) + @?= ("X" |-> [trm| Z:SomeSort{} |]) + <> ("Y" |-> [trm| Z:SomeSort{} |]) + ] + ] + +---------------------------------------- +-- Test fixture +test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree +test name substitutions term expected = + testCase name $ substituteInTerm substitutions term @?= expected + +someSort :: Sort +someSort = SortApp "SomeSort" [] + +(|->) :: VarName -> Term -> Substitution +(|->) v t = Map.fromList [(Variable someSort v, t)] + +asConstructor :: SymbolAttributes +asConstructor = + SymbolAttributes + Constructor + IsNotIdem + IsNotAssoc + IsNotMacroOrAlias + CanBeEvaluated + Nothing + Nothing + Nothing + +con1 :: Symbol +con1 = + Symbol + { name = "con1" + , sortVars = [] + , resultSort = someSort + , argSorts = [someSort] + , attributes = asConstructor + } diff --git a/booster/unit-tests/Test/Booster/Pattern/Util.hs b/booster/unit-tests/Test/Booster/Pattern/Util.hs index 110c542898..11f021c5dd 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Util.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Util.hs @@ -1,38 +1,14 @@ module Test.Booster.Pattern.Util ( - test_subst, test_freshen, ) where -import Data.Map qualified as Map import Data.Set qualified as Set import Test.Tasty import Test.Tasty.HUnit -import Booster.Definition.Attributes.Base import Booster.Pattern.Base import Booster.Pattern.Util -test_subst :: TestTree -test_subst = - testGroup - "Substitution" - [ test - "con1(X)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (app con1 [var "X" someSort]) - (app con1 [app con1 [var "Y" someSort]]) - , test - "con1(X)/\\con1(X)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (AndTerm (app con1 [var "X" someSort]) (app con1 [var "X" someSort])) - (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [app con1 [var "Y" someSort]])) - , test - "con1(X)/\\con1(Y)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (AndTerm (app con1 [var "X" someSort]) (app con1 [var "Y" someSort])) - (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [var "Y" someSort])) - ] - test_freshen :: TestTree test_freshen = testGroup @@ -53,38 +29,6 @@ test_freshen = ] ---------------------------------------- --- Test fixture -test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree -test name substitutions term expected = - testCase name $ substituteInTerm substitutions term @?= expected someSort :: Sort someSort = SortApp "SomeSort" [] - -var :: VarName -> Sort -> Term -var variableName variableSort = Var $ Variable{variableSort, variableName} - -app :: Symbol -> [Term] -> Term -app s = SymbolApplication s [] - -asConstructor :: SymbolAttributes -asConstructor = - SymbolAttributes - Constructor - IsNotIdem - IsNotAssoc - IsNotMacroOrAlias - CanBeEvaluated - Nothing - Nothing - Nothing - -con1 :: Symbol -con1 = - Symbol - { name = "con1" - , sortVars = [] - , resultSort = someSort - , argSorts = [someSort] - , attributes = asConstructor - } From ef7ea92f62a91fc5b1743cc6fc47fc45205d3644 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 15:38:12 +0200 Subject: [PATCH 19/36] Tweak substitution naming in applyRule --- booster/library/Booster/Pattern/Rewrite.hs | 41 ++++++++-------------- 1 file changed, 14 insertions(+), 27 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 584000cb68..bd946290de 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -279,8 +279,8 @@ applyRule pat@Pattern{ceilConditions} rule = getPrettyModifiers >>= \case ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do def <- lift getDefinition - -- unify terms - subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of + -- match term with rule's left-hand side + ruleSubstitution <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of MatchFailed (SubsortingError sortError) -> do withContext CtxError $ logPretty' @mods sortError failRewrite $ RewriteSortError rule pat.term sortError @@ -315,7 +315,7 @@ applyRule pat@Pattern{ceilConditions} rule = Map.fromSet (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) rule.existentials - combinedSubstitution = matchingSubstitution <> existentialSubst + ruleSubstitution = matchingSubstitution <> existentialSubst withContext CtxSuccess $ do logMessage rule @@ -324,7 +324,7 @@ applyRule pat@Pattern{ceilConditions} rule = $ WithJsonMessage ( object [ "substitution" - .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList combinedSubstitution) + .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList ruleSubstitution) ] ) $ renderOneLineText @@ -332,9 +332,9 @@ applyRule pat@Pattern{ceilConditions} rule = <+> ( hsep $ intersperse "," $ map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ - Map.toList combinedSubstitution + Map.toList ruleSubstitution ) - pure combinedSubstitution + pure ruleSubstitution -- Also fail the whole rewrite if a rule applies but may introduce -- an undefined term. @@ -351,11 +351,11 @@ applyRule pat@Pattern{ceilConditions} rule = rule.computedAttributes.notPreservesDefinednessReasons -- check required constraints from lhs: Stop if any is false, abort rewrite if indeterminate. - checkRequires subst + checkRequires ruleSubstitution -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - ensuredConditions <- checkEnsures subst + ensuredConditions <- checkEnsures ruleSubstitution -- if a new constraint is going to be added, the equation cache is invalid unless (null ensuredConditions) $ do @@ -366,39 +366,26 @@ applyRule pat@Pattern{ceilConditions} rule = -- partition ensured constrains into substitution and predicates let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions - -- merge existing substitution and newly acquired one, applying the latter to the former - normalisedPatternSubst <- - lift $ - normaliseSubstitution - pat.substitution - newSubsitution - -- NOTE it is necessary to first apply the rule substitution and then the pattern/ensures substitution, but it is suboptimal to traverse the term twice. - -- TODO a substitution composition operator - let rewrittenTerm = substituteInTerm normalisedPatternSubst . substituteInTerm subst $ rule.rhs + -- compose the existing substitution pattern and the newly acquired one + let modifiedPatternSubst = newSubsitution `compose` pat.substitution + + let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs substitutedNewConstraints = Set.fromList $ map - (coerce . substituteInTerm normalisedPatternSubst . substituteInTerm subst . coerce) + (coerce . substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) . coerce) newConstraints let rewritten = Pattern rewrittenTerm -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables (pat.constraints <> substitutedNewConstraints) - normalisedPatternSubst + modifiedPatternSubst -- ruleSubstitution is not needed, do not attach it to the result ceilConditions withContext CtxSuccess $ withPatternContext rewritten $ return (rule, rewritten) where - -- Given known predicates, a known substitution and a newly acquired substitution (from the ensures clause): - -- - apply the new substitution to the old substitution - -- - merge with the new substitution items and return - normaliseSubstitution :: - Substitution -> Substitution -> RewriteT io Substitution - normaliseSubstitution oldSubst newSubst = do - let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst - pure (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority filterOutKnownConstraints :: Set.Set Predicate -> [Predicate] -> RewriteT io [Predicate] filterOutKnownConstraints priorKnowledge constraitns = do let (knownTrue, toCheck) = partition (`Set.member` priorKnowledge) constraitns From 2f3017f4c2bbd4281f657fd4e8f6659d5293be59 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 15:51:13 +0200 Subject: [PATCH 20/36] Rename rule pattern internalisation function --- .../Booster/Syntax/ParsedKore/Internalise.hs | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 9e80c3dca7..4031315d62 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -766,18 +766,20 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom = sortVars attribs -{- | internalises a pattern and turns its contained substitution into - equations (predicates). Errors if any ceil conditions or - unsupported predicates are found. +{- | Internalises a pattern to be used as a rule left/right-hand side. + + Turns its contained substitution into predicates. + + Errors if any ceil conditions or unsupported predicates are found. -} -internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported :: +internaliseRulePattern :: KoreDefinition -> SourceRef -> Maybe [Id] -> (Variable -> Variable) -> Syntax.KorePattern -> Except DefinitionError (Def.Term, [Predicate]) -internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref maybeVars f t = do +internaliseRulePattern partialDefinition ref maybeVars f t = do (term, preds, ceilConditions, substitution, unsupported) <- withExcept (DefinitionPatternError ref) $ internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t @@ -806,7 +808,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do -- to avoid name clashes with patterns from the user; -- filter out literal `Top` constraints (lhs, requires) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDefinition ref Nothing @@ -817,7 +819,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDefinition ref Nothing @@ -873,14 +875,14 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs | Syntax.KJApp{} <- left = do -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) (lhs, requires) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) (Util.modifyVarName ("Eq#" <>)) $ Syntax.KJAnd left.sort [left, precond] (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) @@ -932,7 +934,7 @@ internaliseCeil :: internaliseCeil partialDef left right sortVars attrs = do -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) (lhs, _) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) @@ -1020,7 +1022,7 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) $ Substitution.substituteInTerm (Map.fromList argPairs) left (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) From b72baf915aff5ed88a9b7c11fe8d761b10291b3f Mon Sep 17 00:00:00 2001 From: github-actions Date: Thu, 17 Oct 2024 14:30:54 +0000 Subject: [PATCH 21/36] Format with fourmolu --- booster/unit-tests/Test/Booster/Pattern/Substitution.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/unit-tests/Test/Booster/Pattern/Substitution.hs b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs index 248a10f250..663bdd2a54 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Substitution.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs @@ -45,7 +45,7 @@ test_subst = "compose is transitive and saturating" $ (("X" |-> [trm| Z:SomeSort{} |]) `compose` ("Y" |-> [trm| X:SomeSort{} |])) @?= ("X" |-> [trm| Z:SomeSort{} |]) - <> ("Y" |-> [trm| Z:SomeSort{} |]) + <> ("Y" |-> [trm| Z:SomeSort{} |]) ] ] From a6f2dd92a9208f8db6a0172bfac661dde3f41b00 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 18 Oct 2024 15:10:17 +0200 Subject: [PATCH 22/36] Float mbSubstitution out, make pure Format with fourmolu --- .../Booster/Syntax/Json/Internalise.hs | 58 +++++++++---------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index ab8b2060d3..c90550ee30 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -481,6 +481,33 @@ mkSubstitution initialSubst = ) breakCycles +-- | Given a equality @'Term'@, decide if it can be interpreted as substitution. +mbSubstitution :: + Internal.Term -> InternalisedPredicate +mbSubstitution = \case + eq@(Internal.EqualsInt (Internal.Var x) e) + | x `Set.member` freeVariables e -> boolPred eq + | otherwise -> SubstitutionPred x e + eq@(Internal.EqualsInt e (Internal.Var x)) + | x `Set.member` freeVariables e -> boolPred eq + | otherwise -> SubstitutionPred x e + eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) -> + do + -- NB sorts do not have to agree! (could be subsorts) + if (x `Set.member` freeVariables e) + then boolPred eq + else SubstitutionPred x e + eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) -> + do + -- NB sorts do not have to agree! (could be subsorts) + if (x `Set.member` freeVariables e) + then boolPred eq + else SubstitutionPred x e + other -> + boolPred other + where + boolPred = BoolPred . Internal.Predicate + internalisePred :: Flag "alias" -> Flag "subsorts" -> @@ -542,9 +569,9 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort case (argS, a, b) of -- for "true" #Equals P, check whether P is in fact a substitution (Internal.SortBool, Internal.TrueBool, x) -> - mapM mbSubstitution [x] + pure [mbSubstitution x] (Internal.SortBool, x, Internal.TrueBool) -> - mapM mbSubstitution [x] + pure [mbSubstitution x] -- we could also detect NotBool (NEquals _) in "false" #Equals P (Internal.SortBool, Internal.FalseBool, x) -> pure [BoolPred $ Internal.Predicate $ Internal.NotBool x] @@ -602,33 +629,6 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort throwE (IncompatibleSorts (map externaliseSort [s1, s2])) zipWithM_ go args1 args2 - mbSubstitution :: Internal.Term -> Except PatternError InternalisedPredicate - mbSubstitution = \case - eq@(Internal.EqualsInt (Internal.Var x) e) - | x `Set.member` freeVariables e -> pure $ boolPred eq - | otherwise -> pure $ SubstitutionPred x e - eq@(Internal.EqualsInt e (Internal.Var x)) - | x `Set.member` freeVariables e -> pure $ boolPred eq - | otherwise -> pure $ SubstitutionPred x e - eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) -> - do - -- NB sorts do not have to agree! (could be subsorts) - pure $ - if (x `Set.member` freeVariables e) - then boolPred eq - else SubstitutionPred x e - eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) -> - do - -- NB sorts do not have to agree! (could be subsorts) - pure $ - if (x `Set.member` freeVariables e) - then boolPred eq - else SubstitutionPred x e - other -> - pure $ boolPred other - - boolPred = BoolPred . Internal.Predicate - ---------------------------------------- -- for use with withAssoc From a08f9377488fdd5dfbeec5db5a79603e27569f3b Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Fri, 18 Oct 2024 15:15:21 +0200 Subject: [PATCH 23/36] Reuse substitution internalisation code Handle with care --- .../library/Booster/Pattern/ApplyEquations.hs | 5 ++-- booster/library/Booster/Pattern/Rewrite.hs | 14 +++++------ .../Booster/Syntax/Json/Externalise.hs | 3 ++- .../Booster/Syntax/Json/Internalise.hs | 23 ++++++++++++++++++- 4 files changed, 34 insertions(+), 11 deletions(-) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 166b18aaea..a16b617696 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -71,6 +71,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) +import Booster.Syntax.Json.Internalise (extractSubsitution) import Booster.Util (Bound (..)) import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached)) import Kore.Util (showHashHex) @@ -483,11 +484,11 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities -- in pat.predicate and pat.substitution), we discard the old substitution here -- and extract a possible simplified one from evaluatedConstraints. - let (simplifiedSubsitution, simplifiedConstraints) = partitionPredicates (Set.toList evaluatedConstraints) + let (simplifiedSubsitution, simplifiedConstraints) = extractSubsitution (Set.toList evaluatedConstraints) pure Pattern - { constraints = Set.fromList simplifiedConstraints + { constraints = simplifiedConstraints , term = newTerm , ceilConditions , substitution = simplifiedSubsitution diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index bd946290de..7ff042cf50 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -71,6 +71,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) +import Booster.Syntax.Json.Internalise (extractSubsitution) import Booster.Util (Flag (..)) newtype RewriteT io a = RewriteT @@ -364,22 +365,21 @@ applyRule pat@Pattern{ceilConditions} rule = lift . RewriteT . lift . modify $ \s -> s{equations = mempty} -- partition ensured constrains into substitution and predicates - let (newSubsitution, newConstraints) = partitionPredicates ensuredConditions + let (newSubsitution, newConstraints) = extractSubsitution ensuredConditions -- compose the existing substitution pattern and the newly acquired one - let modifiedPatternSubst = newSubsitution `compose` pat.substitution + let (modifiedPatternSubst, leftoverConstraints) = extractSubsitution . asEquations $ newSubsitution `compose` pat.substitution let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs substitutedNewConstraints = - Set.fromList $ - map - (coerce . substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) . coerce) - newConstraints + Set.map + (coerce . substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) . coerce) + newConstraints let rewritten = Pattern rewrittenTerm -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables - (pat.constraints <> substitutedNewConstraints) + (pat.constraints <> substitutedNewConstraints <> leftoverConstraints) modifiedPatternSubst -- ruleSubstitution is not needed, do not attach it to the result ceilConditions withContext CtxSuccess $ diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index f130a801d7..7c75e7aaec 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -19,6 +19,7 @@ import Data.Text.Encoding qualified as Text import Booster.Pattern.Base (externaliseKmapUnsafe) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util (sortOfTerm) import Data.Map (Map) import Data.Map qualified as Map @@ -35,7 +36,7 @@ externalisePattern :: externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - substitutions = ensuredSubstitution <> inputSubstitution -- TODO ensuredSubstitution takes priority. Do we even need inputSubstitution? + substitutions = inputSubstitution <> (ensuredSubstitution `Substitution.compose` inputSubstitution) externalisedSubstitution = if null substitutions then Nothing diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index c90550ee30..37ccd84a02 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -35,6 +35,8 @@ module Booster.Syntax.Json.Internalise ( pattern CheckSubsorts, pattern IgnoreSubsorts, logPatternError, + -- substitution mining + extractSubsitution, -- for test only InternalisedPredicate (..), ) where @@ -52,7 +54,7 @@ import Data.Coerce (coerce) import Data.Foldable () import Data.Generics (extQ) import Data.Graph (SCC (..), stronglyConnComp) -import Data.List (foldl1', nub) +import Data.List (foldl', foldl1', nub) import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) @@ -508,6 +510,25 @@ mbSubstitution = \case where boolPred = BoolPred . Internal.Predicate +extractSubsitution :: + [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate) +extractSubsitution ps = + let (potentialSubstituion, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps + (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstituion + in (newSubstitution, Set.fromList $ leftoverPreds <> map unsafeFromBoolPred otherPreds) + where + partitionSubstitutionPreds = foldl' accumulate ([], []) + where + accumulate (accSubst, accOther) = \case + pSubst@SubstitutionPred{} -> (pSubst : accSubst, accOther) + pOther -> (accSubst, pOther : accOther) + + -- this conversion is safe withing this function since we pass Internal.Predicate as input + unsafeFromBoolPred :: InternalisedPredicate -> Internal.Predicate + unsafeFromBoolPred = \case + BoolPred p -> coerce p + _ -> error "extractSubsitution.unsafeFromBoolPred: impossible case" + internalisePred :: Flag "alias" -> Flag "subsorts" -> From 900e13d37ae10fa5e2bfc780363926ebdd861494 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 13:37:56 +0200 Subject: [PATCH 24/36] Do not override with old substitution when externalising --- booster/library/Booster/Syntax/Json/Externalise.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index 7c75e7aaec..3e3abd4e45 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -36,7 +36,8 @@ externalisePattern :: externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - substitutions = inputSubstitution <> (ensuredSubstitution `Substitution.compose` inputSubstitution) + -- inputSubstitution is probably not needed here at all + substitutions = ensuredSubstitution `Substitution.compose` inputSubstitution externalisedSubstitution = if null substitutions then Nothing From b4a3599c358e2098ee27189b8221642e6bbbf593 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 13:58:16 +0200 Subject: [PATCH 25/36] Update test-substitution --- .../test-substitutions/README.md | 1 + .../response-circular-equations.booster-dev | 83 +++++++--- ...onse-symbolic-bottom-predicate.booster-dev | 151 ------------------ 3 files changed, 60 insertions(+), 175 deletions(-) delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md index f6bf9f83bb..6180c4c7af 100644 --- a/booster/test/rpc-integration/test-substitutions/README.md +++ b/booster/test/rpc-integration/test-substitutions/README.md @@ -39,6 +39,7 @@ NB: Booster applies the given substitution before performing any action. - starts from `concrete-subst` - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1` - leading to end state with `X == 42` from the `ensures`-clause + - `booster-dev` return a trivial circular constraint `X ==Int X` * `state-symbolic-bottom-predicate.execute` - starts from `symbolic-subst` - with an equation that is instantly false: `X = 1 +Int X` diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index 6e34d0543d..337751c9c3 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -175,34 +175,69 @@ } }, "second": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "43" } } ] } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + } } } } -} +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev deleted file mode 100644 index fe33f615ea..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ /dev/null @@ -1,151 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "vacuous", - "depth": 0, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "symbolic-subst" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - } - } - } - } -} From 3b2b7d5f86bd280ca7061e2f175132250c7d0fea Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 14:06:52 +0200 Subject: [PATCH 26/36] Update test-questionmark-vars --- .../response-one-ques-substitution.json | 112 ++++++------ ...sponse-one-ques-substitution.kore-rpc-dev} | 112 ++++++------ ...ues.booster-dev => response-one-ques.json} | 0 .../response-one-ques.kore-rpc-dev | 121 ------------ ...er-dev => response-two-ques-external.json} | 0 .../response-two-ques-external.kore-rpc-dev | 124 ------------- ...ponse-two-ques-internal-with-counter.json} | 0 ...er-dev => response-two-ques-internal.json} | 0 .../response-two-ques-internal.kore-rpc-dev | 172 ------------------ 9 files changed, 112 insertions(+), 529 deletions(-) rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques-substitution.booster-dev => response-one-ques-substitution.kore-rpc-dev} (67%) rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques.booster-dev => response-one-ques.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-external.booster-dev => response-two-ques-external.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal-with-counter.booster-dev => response-two-ques-internal-with-counter.json} (100%) rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal.booster-dev => response-two-ques-internal.json} (100%) delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json index 44aefb1934..812dbd3a09 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json @@ -86,73 +86,63 @@ }, "patterns": [ { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] } - ] + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev similarity index 67% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev index 812dbd3a09..44aefb1934 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev @@ -86,63 +86,73 @@ }, "patterns": [ { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, + "tag": "And", "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } } - } + ] }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev deleted file mode 100644 index 8852423b90..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev +++ /dev/null @@ -1,121 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'Stop'State'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev deleted file mode 100644 index eb9ba3ab36..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev +++ /dev/null @@ -1,124 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev deleted file mode 100644 index a450b120fc..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev +++ /dev/null @@ -1,172 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - ] - } - } - } - } -} \ No newline at end of file From 598c8a459cf01e031527176328edadb7870a6ac4 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 14:15:08 +0200 Subject: [PATCH 27/36] Update test-a-to-f --- .../response-branching.kore-rpc-dev | 400 ------------------ 1 file changed, 400 deletions(-) delete mode 100644 booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev diff --git a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev b/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev deleted file mode 100644 index 0d2f7baef6..0000000000 --- a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev +++ /dev/null @@ -1,400 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "branching", - "depth": 0, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "next-states": [ - { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "c" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "rule-id": "3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e", - "rule-substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar0", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar1", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - } - ] - } - } - }, - { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "b" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "rule-id": "aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8", - "rule-substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar0", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar1", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - } - ] - } - } - } - ] - } -} \ No newline at end of file From bc72188027f48a6f4aca1b3b279ff98c9d1add7e Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 14:59:55 +0200 Subject: [PATCH 28/36] Remove dead code --- .../library/Booster/Pattern/Substitution.hs | 26 ++++--------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs index fac9072927..f2299ccf37 100644 --- a/booster/library/Booster/Pattern/Substitution.hs +++ b/booster/library/Booster/Pattern/Substitution.hs @@ -8,9 +8,7 @@ This module is intended to be imported qualified. -} module Booster.Pattern.Substitution ( mkEq, - destructEq, asEquations, - partitionPredicates, compose, substituteInPredicate, substituteInTerm, @@ -18,16 +16,19 @@ module Booster.Pattern.Substitution ( import Data.Bifunctor (bimap) import Data.Coerce (coerce) -import Data.List (partition) import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map -import Data.Maybe (fromMaybe, isJust, mapMaybe) +import Data.Maybe (fromMaybe) import Data.Set qualified as Set import Booster.Pattern.Base import Booster.Pattern.Bool import Booster.Pattern.Util (sortOfTerm) +{- | Compose substitutions: + - apply the left one to the assignments in the right one + - merge left with the result of above, left takes priority +-} compose :: Substitution -> Substitution -> Substitution compose newSubst oldSubst = let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst @@ -40,27 +41,10 @@ mkEq x t = Predicate $ case sortOfTerm t of SortBool -> EqualsBool (Var x) t otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t) -{- | Pattern match on an equality predicate and try extracting a variable assignment. - This is a partial inverse of @'mkEq'@ --} -destructEq :: Predicate -> Maybe (Variable, Term) -destructEq = \case - Predicate (EqualsInt (Var x) t) -> Just (x, t) - Predicate (EqualsBool (Var x) t) -> Just (x, t) - Predicate - (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) - _ -> Nothing - -- | turns a substitution into a list of equations asEquations :: Map Variable Term -> [Predicate] asEquations = map (uncurry mkEq) . Map.assocs --- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found -partitionPredicates :: [Predicate] -> (Map Variable Term, [Predicate]) -partitionPredicates ps = - let (substItems, normalPreds) = partition (isJust . destructEq) ps - in (Map.fromList . mapMaybe destructEq $ substItems, normalPreds) - substituteInTerm :: Substitution -> Term -> Term substituteInTerm substitution = goSubst where From b2ea0f8a82feef4298682c08a798539ddf1563d9 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 15:39:19 +0200 Subject: [PATCH 29/36] Use substitution in Implies --- booster/library/Booster/Pattern/Implies.hs | 8 +++++--- booster/library/Booster/SMT/Interface.hs | 3 ++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index e7cdfad700..81ef4a083b 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -122,7 +122,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = , substitution = substitutionR } - SMT.isSat solver (Set.toList substPatL.constraints) >>= \case + SMT.isSat solver (Set.toList substPatL.constraints) substPatL.substitution >>= \case SMT.IsUnsat -> let sort = externaliseSort $ sortOfPattern substPatL in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty @@ -159,8 +159,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do let filteredConsequentPreds = - Set.map (Substitution.substituteInPredicate subst) substPatR.constraints - `Set.difference` substPatL.constraints + Set.map + (Substitution.substituteInPredicate subst) + (substPatR.constraints <> (Set.fromList $ Substitution.asEquations substPatR.substitution)) + `Set.difference` (substPatL.constraints <> (Set.fromList $ Substitution.asEquations substPatL.substitution)) if null filteredConsequentPreds then diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 731562f2d4..962f3e5a1f 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -280,8 +280,9 @@ isSat :: Log.LoggerMIO io => SMT.SMTContext -> [Predicate] -> + Map Variable Term -> -- supplied substitution io (IsSatResult ()) -isSat ctxt ps = fmap void <$> (isSatReturnTransState ctxt ps mempty) +isSat ctxt ps subst = fmap void <$> (isSatReturnTransState ctxt ps subst) {- | Implementation of get-model request From f8f956f76f6d0acc3a549479faf452c930c64cba Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 17:21:16 +0200 Subject: [PATCH 30/36] Handle input substitution as part of Pattern --- booster/library/Booster/JsonRpc.hs | 45 +++++++++---------- booster/library/Booster/JsonRpc/Utils.hs | 11 +---- booster/library/Booster/Pattern/Implies.hs | 12 ++--- .../Booster/Syntax/Json/Externalise.hs | 10 ++--- .../Booster/Syntax/Json/Internalise.hs | 11 ++--- booster/tools/booster/Proxy.hs | 1 - 6 files changed, 37 insertions(+), 53 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 189475787d..c51c0547f7 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -44,7 +44,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..)) import Booster.LLVM as LLVM (API) import Booster.Log import Booster.Pattern.ApplyEquations qualified as ApplyEquations -import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable) +import Booster.Pattern.Base (Pattern (..), Sort (SortApp)) import Booster.Pattern.Base qualified as Pattern import Booster.Pattern.Implies (runImplies) import Booster.Pattern.Pretty @@ -166,7 +166,7 @@ respond stateVar request = result <- performRewrite rewriteConfig substPat SMT.finaliseSolver solver - pure $ execResponse req result substitution unsupported + pure $ execResponse req result unsupported RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar @@ -244,21 +244,21 @@ respond stateVar request = RpcError.CouldNotVerifyPattern $ map patternErrorToRpcError patternErrors -- term and predicate (pattern) - Right (TermAndPredicates pat substitution unsupported) -> do + Right (TermAndPredicates pat unsupported) -> do unless (null unsupported) $ do withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do logMessage ("ignoring unsupported predicate parts" :: Text) -- apply the given substitution before doing anything else let substPat = Pattern - { term = Substitution.substituteInTerm substitution pat.term - , constraints = Set.map (Substitution.substituteInPredicate substitution) pat.constraints + { term = Substitution.substituteInTerm pat.substitution pat.term + , constraints = Set.map (Substitution.substituteInPredicate pat.substitution) pat.constraints , ceilConditions = pat.ceilConditions - , substitution + , substitution = pat.substitution } ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case (Right newPattern, _) -> do - let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution + let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern tSort = externaliseSort (sortOfPattern newPattern) result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of [] -> term @@ -333,7 +333,7 @@ respond stateVar request = -- term and predicates were sent. Only work on predicates (boolPs, suppliedSubst) <- case things of - TermAndPredicates pat substitution unsupported -> do + TermAndPredicates pat unsupported -> do withContext CtxGetModel $ logMessage' ("ignoring supplied terms and only checking predicates" :: Text) @@ -342,7 +342,7 @@ respond stateVar request = logMessage' ("ignoring unsupported predicates" :: Text) withContext CtxDetail $ logMessage (Text.unwords $ map prettyPattern unsupported) - pure (Set.toList pat.constraints, substitution) + pure (Set.toList pat.constraints, pat.substitution) Predicates ps -> do unless (null ps.ceilPredicates && null ps.unsupported) $ do withContext CtxGetModel $ do @@ -473,10 +473,9 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} = execResponse :: RpcTypes.ExecuteRequest -> (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) -> - Map Variable Term -> [Syntax.KorePattern] -> Either ErrorObj (RpcTypes.API 'RpcTypes.Res) -execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of +execResponse req (d, traces, rr) unsupported = case rr of RewriteBranch p nexts -> Right $ RpcTypes.Execute @@ -484,10 +483,10 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Branching , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Just $ - map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $ + map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $ toList nexts , rule = Nothing , unknownPredicate = Nothing @@ -499,7 +498,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Stuck , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -511,7 +510,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.Vacuous , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -523,8 +522,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.CutPointRule , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing - , nextStates = Just [toExecState next originalSubstitution unsupported Nothing] + , state = toExecState p unsupported Nothing + , nextStates = Just [toExecState next unsupported Nothing] , rule = Just lbl , unknownPredicate = Nothing } @@ -535,7 +534,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.TerminalRule , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Nothing , rule = Just lbl , unknownPredicate = Nothing @@ -547,7 +546,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { reason = RpcTypes.DepthBound , depth , logs - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -564,7 +563,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of (logSuccessfulRewrites, logFailedRewrites) (RewriteStepFailed failure) in logs <|> abortRewriteLog - , state = toExecState p originalSubstitution unsupported Nothing + , state = toExecState p unsupported Nothing , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing @@ -587,8 +586,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of xs@(_ : _) -> Just xs toExecState :: - Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState -toExecState pat sub unsupported muid = + Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState +toExecState pat unsupported muid = RpcTypes.ExecuteState { term = addHeader t , predicate = addHeader <$> addUnsupported p @@ -598,7 +597,7 @@ toExecState pat sub unsupported muid = , ruleId = getUniqueId <$> muid } where - (t, p, s) = externalisePattern pat sub + (t, p, s) = externalisePattern pat termSort = externaliseSort $ sortOfPattern pat allUnsupported = Syntax.KJAnd termSort unsupported addUnsupported diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs index f27e3e7909..1a319cfd47 100644 --- a/booster/library/Booster/JsonRpc/Utils.hs +++ b/booster/library/Booster/JsonRpc/Utils.hs @@ -279,18 +279,9 @@ diffBy def pat1 pat2 = <> if null ps.unsupported then "" else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported) - renderBS (TermAndPredicates p m u) = + renderBS (TermAndPredicates p u) = ( BS.pack . renderDefault $ pretty (PrettyWithModifiers @['Decoded, 'Truncated] p) - <+> vsep - ( map - ( \(k, v) -> - pretty (PrettyWithModifiers @['Decoded, 'Truncated] k) - <+> "=" - <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v) - ) - (Map.toList m) - ) ) <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u) internalise = diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 81ef4a083b..df9ec6f3db 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -69,8 +69,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = in runExcept $ internalisePatternOrTopOrBottom DisallowAlias CheckSubsorts Nothing def existentials korePat - checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR = do - let freeVarsL = + checkImplies patL unsupportedL existsL patR unsupportedR existsR = do + let substitutionL = patL.substitution + substitutionR = patR.substitution + freeVarsL = ( freeVariables patL.term <> (Set.unions $ Set.map (freeVariables . coerce) patL.constraints) <> (Set.fromList $ Map.keys substitutionL) @@ -210,10 +212,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = (Right IsTop{}, _) -> pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $ "The check implication step expects the antecedent term to be function-like." - ( Right (IsPattern (existsL, patL, substitutionL, unsupportedL)) - , Right (IsPattern (existsR, patR, substitutionR, unsupportedR)) + ( Right (IsPattern (existsL, patL, unsupportedL)) + , Right (IsPattern (existsR, patR, unsupportedR)) ) -> - checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR + checkImplies patL unsupportedL existsL patR unsupportedR existsR (Right IsPattern{}, Right (IsTop sort)) -> implies' (Kore.Syntax.KJTop sort) sort antecedent.term consequent.term mempty (Right IsPattern{}, Right (IsBottom sort)) -> diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index 3e3abd4e45..2b7bf2494e 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -19,9 +19,7 @@ import Data.Text.Encoding qualified as Text import Booster.Pattern.Base (externaliseKmapUnsafe) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal -import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util (sortOfTerm) -import Data.Map (Map) import Data.Map qualified as Map import Kore.Syntax.Json.Types qualified as Syntax @@ -31,17 +29,15 @@ import Kore.Syntax.Json.Types qualified as Syntax -} externalisePattern :: Internal.Pattern -> - Map Internal.Variable Internal.Term -> (Syntax.KorePattern, Maybe Syntax.KorePattern, Maybe Syntax.KorePattern) -externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution = +externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution} = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term -- inputSubstitution is probably not needed here at all - substitutions = ensuredSubstitution `Substitution.compose` inputSubstitution externalisedSubstitution = - if null substitutions + if null substitution then Nothing - else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions + else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitution externalisedPredicate = if null constraints && null ceilConditions then Nothing diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 37ccd84a02..8299092bae 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -133,12 +133,11 @@ data TermOrPredicates -- = Either Predicate Pattern = Predicates InternalisedPredicates | TermAndPredicates Internal.Pattern - (Map Internal.Variable Internal.Term) [Syntax.KorePattern] deriving stock (Eq, Show) retractPattern :: TermOrPredicates -> Maybe Internal.Pattern -retractPattern (TermAndPredicates patt _ _) = Just patt +retractPattern (TermAndPredicates patt _) = Just patt retractPattern _ = Nothing -- main interface functions @@ -204,7 +203,7 @@ internalisePatternOrTopOrBottom :: Except PatternError ( PatternOrTopOrBottom - ([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern]) + ([Internal.Variable], Internal.Pattern, [Syntax.KorePattern]) ) internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do let exploded = explodeAnd p @@ -223,8 +222,7 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi pure $ IsPattern ( existentialVars - , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = mempty} -- this is the ensures-substitution, leave empty - , subst + , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = subst} , unknown ) where @@ -258,9 +256,8 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa { term , constraints = Set.fromList constrs , ceilConditions - , substitution = mempty -- this is the ensures-substitution, leave empty + , substitution = substitution } - substitution unsupported ) diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index 274bd0ef86..251728085b 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -524,7 +524,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of Right ( ( Booster.toExecState Pattern{term, ceilConditions, constraints = Set.fromList preds, substitution = sub} - sub unsup Nothing ) From c73a2c9d7aab46c0864a537bbd36b761c67d9f49 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 22 Oct 2024 17:32:19 +0200 Subject: [PATCH 31/36] Handle substitution better when simplifying standalone predicates --- booster/library/Booster/JsonRpc.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index c51c0547f7..6321815823 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -68,6 +68,7 @@ import Booster.Syntax.Json.Externalise import Booster.Syntax.Json.Internalise ( InternalisedPredicates (..), TermOrPredicates (..), + extractSubsitution, internalisePattern, internaliseTermOrPredicate, logPatternError, @@ -289,16 +290,17 @@ respond stateVar request = mLlvmLibrary solver mempty - predicates -- TODO include ps.substitution? + (predicates <> Substitution.asEquations ps.substitution) >>= \case - (Right newPreds, _) -> do + (Right simplified, _) -> do let predicateSort = fromMaybe (error "not a predicate") $ sortOfJson req.state.term + (simplifiedSubstitution, simplifiedPredicates) = extractSubsitution simplified result = - map (externalisePredicate predicateSort) newPreds + map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates) <> map (externaliseCeil predicateSort) ps.ceilPredicates - <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution) + <> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution) <> ps.unsupported pure $ Right (addHeader $ Syntax.KJAnd predicateSort result) From cc808a23ad5d25487fd82b0c59259fd260a36258 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 23 Oct 2024 08:45:56 +0200 Subject: [PATCH 32/36] Remove unused function modifyVariables --- booster/library/Booster/Pattern/Util.hs | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index 00a496420a..7f249d58ed 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -6,7 +6,6 @@ module Booster.Pattern.Util ( substituteInSort, sortOfTerm, sortOfPattern, - modifyVariables, modifyVariablesInT, modifyVariablesInP, modifyVarName, @@ -80,15 +79,6 @@ substituteInSort subst (SortApp n args) = sortOfPattern :: Pattern -> Sort sortOfPattern pat = sortOfTerm pat.term -modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern -modifyVariables f p = - Pattern - { term = modifyVariablesInT f p.term - , constraints = Set.map (modifyVariablesInP f) p.constraints - , substitution = Map.map (coerce $ modifyVariablesInT f) p.substitution - , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions - } - modifyVariablesInT :: (Variable -> Variable) -> Term -> Term modifyVariablesInT f = cata $ \case VarF v -> Var (f v) From f9f0d51c7f0fc6cb2a31b41f0a01e7803ffc6b61 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 23 Oct 2024 08:49:08 +0200 Subject: [PATCH 33/36] Fix typo --- booster/library/Booster/JsonRpc.hs | 4 ++-- booster/library/Booster/Pattern/ApplyEquations.hs | 4 ++-- booster/library/Booster/Pattern/Rewrite.hs | 6 +++--- booster/library/Booster/Syntax/Json/Internalise.hs | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 6321815823..6d824f66e9 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -68,7 +68,7 @@ import Booster.Syntax.Json.Externalise import Booster.Syntax.Json.Internalise ( InternalisedPredicates (..), TermOrPredicates (..), - extractSubsitution, + extractSubstitution, internalisePattern, internaliseTermOrPredicate, logPatternError, @@ -296,7 +296,7 @@ respond stateVar request = let predicateSort = fromMaybe (error "not a predicate") $ sortOfJson req.state.term - (simplifiedSubstitution, simplifiedPredicates) = extractSubsitution simplified + (simplifiedSubstitution, simplifiedPredicates) = extractSubstitution simplified result = map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates) <> map (externaliseCeil predicateSort) ps.ceilPredicates diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index a16b617696..53b801fcc2 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -71,7 +71,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter (renderOneLineText) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) -import Booster.Syntax.Json.Internalise (extractSubsitution) +import Booster.Syntax.Json.Internalise (extractSubstitution) import Booster.Util (Bound (..)) import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached)) import Kore.Util (showHashHex) @@ -484,7 +484,7 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities -- in pat.predicate and pat.substitution), we discard the old substitution here -- and extract a possible simplified one from evaluatedConstraints. - let (simplifiedSubsitution, simplifiedConstraints) = extractSubsitution (Set.toList evaluatedConstraints) + let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints) pure Pattern diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 7ff042cf50..cdfffe43cb 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -71,7 +71,7 @@ import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) -import Booster.Syntax.Json.Internalise (extractSubsitution) +import Booster.Syntax.Json.Internalise (extractSubstitution) import Booster.Util (Flag (..)) newtype RewriteT io a = RewriteT @@ -365,10 +365,10 @@ applyRule pat@Pattern{ceilConditions} rule = lift . RewriteT . lift . modify $ \s -> s{equations = mempty} -- partition ensured constrains into substitution and predicates - let (newSubsitution, newConstraints) = extractSubsitution ensuredConditions + let (newSubsitution, newConstraints) = extractSubstitution ensuredConditions -- compose the existing substitution pattern and the newly acquired one - let (modifiedPatternSubst, leftoverConstraints) = extractSubsitution . asEquations $ newSubsitution `compose` pat.substitution + let (modifiedPatternSubst, leftoverConstraints) = extractSubstitution . asEquations $ newSubsitution `compose` pat.substitution let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs substitutedNewConstraints = diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 8299092bae..d533575379 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -36,7 +36,7 @@ module Booster.Syntax.Json.Internalise ( pattern IgnoreSubsorts, logPatternError, -- substitution mining - extractSubsitution, + extractSubstitution, -- for test only InternalisedPredicate (..), ) where @@ -507,9 +507,9 @@ mbSubstitution = \case where boolPred = BoolPred . Internal.Predicate -extractSubsitution :: +extractSubstitution :: [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate) -extractSubsitution ps = +extractSubstitution ps = let (potentialSubstituion, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstituion in (newSubstitution, Set.fromList $ leftoverPreds <> map unsafeFromBoolPred otherPreds) From c974346efae820a7f3c136cc04699d6141c2bcbc Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 23 Oct 2024 11:02:19 +0200 Subject: [PATCH 34/36] Refactor extractSubstitution --- .../Booster/Syntax/Json/Internalise.hs | 27 +++++++++---------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index d533575379..4b670457f3 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -51,10 +51,11 @@ import Data.ByteString.Char8 (ByteString, isPrefixOf) import Data.ByteString.Char8 qualified as BS import Data.Char (isLower) import Data.Coerce (coerce) +import Data.Either (partitionEithers) import Data.Foldable () import Data.Generics (extQ) import Data.Graph (SCC (..), stronglyConnComp) -import Data.List (foldl', foldl1', nub) +import Data.List (foldl1', nub) import Data.Map (Map) import Data.Map qualified as Map import Data.Set (Set) @@ -510,21 +511,19 @@ mbSubstitution = \case extractSubstitution :: [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate) extractSubstitution ps = - let (potentialSubstituion, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps - (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstituion - in (newSubstitution, Set.fromList $ leftoverPreds <> map unsafeFromBoolPred otherPreds) + let (potentialSubstitution, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps + (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstitution + in (newSubstitution, Set.fromList $ leftoverPreds <> otherPreds) where - partitionSubstitutionPreds = foldl' accumulate ([], []) + partitionSubstitutionPreds = partitionEithers . map unpackBoolPred where - accumulate (accSubst, accOther) = \case - pSubst@SubstitutionPred{} -> (pSubst : accSubst, accOther) - pOther -> (accSubst, pOther : accOther) - - -- this conversion is safe withing this function since we pass Internal.Predicate as input - unsafeFromBoolPred :: InternalisedPredicate -> Internal.Predicate - unsafeFromBoolPred = \case - BoolPred p -> coerce p - _ -> error "extractSubsitution.unsafeFromBoolPred: impossible case" + unpackBoolPred :: InternalisedPredicate -> Either InternalisedPredicate Internal.Predicate + unpackBoolPred = \case + pSubst@SubstitutionPred{} -> Left pSubst + BoolPred p -> Right p + other -> + -- this case is impossible the input is a valid Internal.Predicate + error $ "extractSubstitution: unsupported predicate " <> show other internalisePred :: Flag "alias" -> From 9bcdc52c31e098d8c47919af6b0cf83de3a63dc8 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 23 Oct 2024 11:13:28 +0200 Subject: [PATCH 35/36] Bind the known constraints expressin --- booster/library/Booster/Pattern/Rewrite.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index cdfffe43cb..47c16b6321 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -435,12 +435,13 @@ applyRule pat@Pattern{ceilConditions} rule = -- apply substitution to rule requires let ruleRequires = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires + knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution) -- filter out any predicates known to be _syntactically_ present in the known prior toCheck <- lift $ filterOutKnownConstraints - (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + knownConstraints ruleRequires -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate. @@ -450,7 +451,7 @@ applyRule pat@Pattern{ceilConditions} rule = ( checkConstraint id notAppliedIfBottom - (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + knownConstraints ) toCheck @@ -459,7 +460,7 @@ applyRule pat@Pattern{ceilConditions} rule = stillUnclear <- lift $ filterOutKnownConstraints - (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + knownConstraints unclearRequires -- check unclear requires-clauses in the context of known constraints (priorKnowledge) @@ -481,13 +482,14 @@ applyRule pat@Pattern{ceilConditions} rule = -- apply substitution to rule ensures let ruleEnsures = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures + knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution) newConstraints <- catMaybes <$> mapM ( checkConstraint id trivialIfBottom - (pat.constraints <> (Set.fromList . asEquations $ pat.substitution)) + knownConstraints ) ruleEnsures From 58f64020651753dfec38ac5e0628ca049c0205bf Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 23 Oct 2024 11:47:18 +0200 Subject: [PATCH 36/36] Substitute in the internalisation functions directly --- booster/library/Booster/JsonRpc.hs | 14 ++--- booster/library/Booster/Pattern/Implies.hs | 59 +++++++------------ .../Booster/Syntax/Json/Internalise.hs | 38 +++++++++--- 3 files changed, 55 insertions(+), 56 deletions(-) diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 6d824f66e9..48dafb6cf2 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -131,7 +131,8 @@ respond stateVar request = [ req.logSuccessfulRewrites , req.logFailedRewrites ] - -- apply the given substitution before doing anything else + -- apply the given substitution before doing anything else, + -- as internalisePattern does not substitute let substPat = Pattern { term = Substitution.substituteInTerm substitution term @@ -245,19 +246,12 @@ respond stateVar request = RpcError.CouldNotVerifyPattern $ map patternErrorToRpcError patternErrors -- term and predicate (pattern) + -- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate Right (TermAndPredicates pat unsupported) -> do unless (null unsupported) $ do withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do logMessage ("ignoring unsupported predicate parts" :: Text) - -- apply the given substitution before doing anything else - let substPat = - Pattern - { term = Substitution.substituteInTerm pat.substitution pat.term - , constraints = Set.map (Substitution.substituteInPredicate pat.substitution) pat.constraints - , ceilConditions = pat.ceilConditions - , substitution = pat.substitution - } - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case + ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case (Right newPattern, _) -> do let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern tSort = externaliseSort (sortOfPattern newPattern) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index df9ec6f3db..92ec8d9cfb 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -26,7 +26,7 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..)) import Booster.Pattern.Bool (pattern TrueBool) import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms) import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty') -import Booster.Pattern.Substitution qualified as Substitution +import Booster.Pattern.Substitution (asEquations) import Booster.Pattern.Util (freeVariables, sortOfPattern) import Booster.Prettyprinter (renderDefault) import Booster.SMT.Interface qualified as SMT @@ -107,43 +107,26 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = map (pack . show) $ unsupportedL <> unsupportedR | otherwise -> do - let - -- apply the given substitution before doing anything else - substPatL = - Pattern - { term = Substitution.substituteInTerm substitutionL patL.term - , constraints = Set.map (Substitution.substituteInPredicate substitutionL) patL.constraints - , ceilConditions = patL.ceilConditions - , substitution = substitutionL - } - substPatR = - Pattern - { term = Substitution.substituteInTerm substitutionR patR.term - , constraints = Set.map (Substitution.substituteInPredicate substitutionR) patR.constraints - , ceilConditions = patR.ceilConditions - , substitution = substitutionR - } - - SMT.isSat solver (Set.toList substPatL.constraints) substPatL.substitution >>= \case + SMT.isSat solver (Set.toList patL.constraints) patL.substitution >>= \case SMT.IsUnsat -> - let sort = externaliseSort $ sortOfPattern substPatL + let sort = externaliseSort $ sortOfPattern patL in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty - _ -> checkImpliesMatchTerms existsL substPatL existsR substPatR + _ -> checkImpliesMatchTerms existsL patL existsR patR - checkImpliesMatchTerms existsL substPatL existsR substPatR = - case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of + checkImpliesMatchTerms existsL patL existsR patR = + case matchTerms Booster.Pattern.Match.Implies def patR.term patL.term of MatchFailed (SubsortingError sortError) -> pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ show sortError MatchFailed{} -> doesNotImply - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) MatchIndeterminate remainder -> - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case + ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case (Right simplifedSubstPatL, _) -> - if substPatL == simplifedSubstPatL + if patL == 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. @@ -156,22 +139,20 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ NonEmpty.toList remainder ) - else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR + else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR (Left err, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do let filteredConsequentPreds = - Set.map - (Substitution.substituteInPredicate subst) - (substPatR.constraints <> (Set.fromList $ Substitution.asEquations substPatR.substitution)) - `Set.difference` (substPatL.constraints <> (Set.fromList $ Substitution.asEquations substPatL.substitution)) + (patR.constraints <> (Set.fromList $ asEquations patR.substitution)) + `Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution)) if null filteredConsequentPreds then implies - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) subst else ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case @@ -179,9 +160,9 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = if all (== Predicate TrueBool) newPreds then implies - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) subst else -- here we conservatively abort -- an anlternative would be to return valid, putting the unknown constraints into the diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index 4b670457f3..591895b18d 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -141,7 +141,13 @@ retractPattern :: TermOrPredicates -> Maybe Internal.Pattern retractPattern (TermAndPredicates patt _) = Just patt retractPattern _ = Nothing --- main interface functions +{- | Internalise a @'Syntax.KorePattern'@ into the components constituting a @'Internal.Pattern'@ + + Note: This function will NOT apply the internalised @'Internal.Substitution'@ to the other components. + The callers of this function must decide if it is necessary to substitute. + Use @'internalisePatternOrTopOrBottom'@ or @'internaliseTermOrPredicate'@ that return an already + substituted @'Internal.Pattern'@. +-} internalisePattern :: Flag "alias" -> Flag "subsorts" -> @@ -153,7 +159,7 @@ internalisePattern :: ( Internal.Term , [Internal.Predicate] , [Internal.Ceil] - , Map Internal.Variable Internal.Term + , Internal.Substitution , [Syntax.KorePattern] ) internalisePattern allowAlias checkSubsorts sortVars definition p = do @@ -193,7 +199,11 @@ data PatternOrTopOrBottom a | IsPattern a deriving (Functor) --- main interface functions +{- | Internalise a @'Syntax.KorePattern'@ into @'Internal.Pattern'@, detecting and reporting trivial cases. + + Note: This function will apply the internalised @'Internal.Substitution'@ part of the pattern's constraints + to the term and constraints (but not the ceils). +-} internalisePatternOrTopOrBottom :: Flag "alias" -> Flag "subsorts" -> @@ -223,7 +233,12 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi pure $ IsPattern ( existentialVars - , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = subst} + , Internal.Pattern + { term = Internal.substituteInTerm subst term + , constraints = Set.map (Internal.substituteInPredicate subst) . Set.fromList $ preds + , ceilConditions + , substitution = subst + } , unknown ) where @@ -237,6 +252,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi Syntax.KJBottom{sort} : _ -> Just $ IsBottom sort _ : xs -> isBottom xs +{- | Internalise a @'Syntax.KorePattern'@ into either @'Internal.Pattern'@ + or @'[InternalisedPredicates]'@ if only terms of sort bool are present. + + Note: If this function successfully internalises a @'Internal.Pattern'@, it will apply the + @'Internal.Substitution'@ part to the term and constraints (but not the ceils). + + Otherwise, when we get predicates only, the substitution part + is not applied to the rest of the predicates. +-} internaliseTermOrPredicate :: Flag "alias" -> Flag "subsorts" -> @@ -254,10 +278,10 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa pure $ TermAndPredicates Internal.Pattern - { term - , constraints = Set.fromList constrs + { term = Internal.substituteInTerm substitution term + , constraints = Set.map (Internal.substituteInPredicate substitution) . Set.fromList $ constrs , ceilConditions - , substitution = substitution + , substitution } unsupported )