Attempt no. 2 at fixing rule-substitution (#3939)

Fixes #3912? There were three further issues that I identified: * When we have a `VarX` in both the rule and configuration, internally they are distinguished by a different constructor. However, when externalising, this tag was lost. This PR prepends "Rule" to any rule variables and "Eq" to any Equation vars, leaving the original name for all config vars. * After match/unification, there is some further processing before the substitution is applied. We are now capturing the simplified/normalised substitution just before it's applied and emitted in a debug message (via `debugCreatedSubstitution`). This should ensure that the substitution is the correct one. * The substitution being returned contained both the mappings from rule variables to subterms of the configuration, as well as learned predicates about equalities between configuration variables and values. The latter are emitted in the `rule-predicate` field and should not be present in `rule-substitution`.
runtimeverification · Jun 17, 2024 · 4b24eba · 4b24eba
1 parent a96eba0
commit 4b24eba
Show file tree

Hide file tree

Showing 7 changed files with 39 additions and 21 deletions.
diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
@@ -81,11 +81,12 @@ import Kore.Rewrite (
 import Kore.Rewrite.ClaimPattern qualified as ClaimPattern
 import Kore.Rewrite.RewriteStep (EnableAssumeInitialDefined (..))
 import Kore.Rewrite.RewritingVariable (
-    RewritingVariableName,
+    RewritingVariableName (..),
     getRewritingPattern,
     getRewritingVariable,
     isSomeConfigVariable,
     isSomeEquationVariable,
+    isSomeRuleVariable,
     mkRewritingPattern,
     mkRewritingTerm,
  )
@@ -386,7 +387,14 @@ respond serverState moduleName runSMT =
                                         else Just $ Kore.Syntax.Json.fromTermLike $ foldl TermLike.mkAnd pr' $ map toEquals predsFromSub
                              in ( getRewritingPattern p'
                                 , finalPr
-                                , PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable sub
+                                , PatternJson.fromSubstitution sort
+                                    $ Substitution.mapVariables
+                                        ( pure $ \case
+                                            ConfigVariableName v -> v
+                                            RuleVariableName v@SomeVariable.VariableName{base = TermLike.Id{getId = nm, idLocation = loc}} -> v{SomeVariable.base = TermLike.Id{getId = "Rule" <> nm, idLocation = loc}}
+                                            EquationVariableName v@SomeVariable.VariableName{base = TermLike.Id{getId = nm, idLocation = loc}} -> v{SomeVariable.base = TermLike.Id{getId = "Eq" <> nm, idLocation = loc}}
+                                        )
+                                    $ Substitution.filter isSomeRuleVariable sub
                                 , rid
                                 )
 

diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs
@@ -108,7 +108,12 @@ finalizeAppliedRule ::
     RulePattern RewritingVariableName ->
     -- | Conditions of applied rule
     Condition RewritingVariableName ->
-    LogicT Simplifier (Pattern RewritingVariableName)
+    LogicT
+        Simplifier
+        ( Substitution.Substitution
+            RewritingVariableName
+        , Pattern RewritingVariableName
+        )
 finalizeAppliedRule
     sideCondition
     renamedRule
@@ -133,7 +138,7 @@ finalizeAppliedRule
         ruleRHS = Rule.rhs renamedRule
 
         catchSimplifiesToBottom srt = \case
-            [] -> return $ pure $ mkBottom srt
+            [] -> return (mempty, pure $ mkBottom srt)
             xs -> Logic.scatter xs
 
 {- | Combine all the conditions to apply rule and construct the result.
@@ -153,7 +158,12 @@ constructConfiguration ::
     Condition RewritingVariableName ->
     -- | Final configuration
     Pattern RewritingVariableName ->
-    LogicT Simplifier (Pattern RewritingVariableName)
+    LogicT
+        Simplifier
+        ( Substitution.Substitution
+            RewritingVariableName
+        , Pattern RewritingVariableName
+        )
 constructConfiguration
     sideCondition
     appliedCondition
@@ -181,7 +191,7 @@ constructConfiguration
         -- TODO (thomas.tuegel): Should the final term be simplified after
         -- substitution?
         debugCreatedSubstitution substitution (termLikeSort finalTerm)
-        return (finalTerm' `Pattern.withCondition` finalCondition)
+        return (substitution, finalTerm' `Pattern.withCondition` finalCondition)
 
 finalizeAppliedClaim ::
     -- | SideCondition containing metadata
@@ -190,7 +200,7 @@ finalizeAppliedClaim ::
     ClaimPattern ->
     -- | Conditions of applied rule
     Condition RewritingVariableName ->
-    LogicT Simplifier (Pattern RewritingVariableName)
+    LogicT Simplifier (Substitution.Substitution RewritingVariableName, Pattern RewritingVariableName)
 finalizeAppliedClaim sideCondition renamedRule appliedCondition =
     -- `constructConfiguration` may simplify the configuration to bottom
     -- we want to "catch" this and return a #bottom Pattern
@@ -210,7 +220,7 @@ finalizeAppliedClaim sideCondition renamedRule appliedCondition =
     ClaimPattern{right} = renamedRule
 
     catchSimplifiesToBottom srt = \case
-        [] -> return $ pure $ mkBottom srt
+        [] -> return (mempty, pure $ mkBottom srt)
         xs -> Logic.scatter xs
 
 type UnifyingRuleWithRepresentation representation rule =
@@ -226,7 +236,7 @@ type UnifyingRuleWithRepresentation representation rule =
 type FinalizeApplied rule =
     rule ->
     Condition RewritingVariableName ->
-    LogicT Simplifier (Pattern RewritingVariableName)
+    LogicT Simplifier (Substitution.Substitution RewritingVariableName, Pattern RewritingVariableName)
 
 finalizeRule ::
     UnifyingRuleWithRepresentation representation rule =>
@@ -256,9 +266,9 @@ finalizeRule
                     unificationCondition
             checkSubstitutionCoverage initial (toRule <$> unifiedRule)
             let renamedRule = Conditional.term unifiedRule
-            final <- finalizeApplied renamedRule applied
+            (subst, final) <- finalizeApplied renamedRule applied
             let result = resetResultPattern initialVariables final
-            return Step.Result{appliedRule = unifiedRule, result}
+            return Step.Result{appliedRule = unifiedRule{substitution = subst}, result}
 
 -- | Finalizes a list of applied rules into 'Results'.
 type Finalizer rule =

diff --git a/kore/src/Kore/Rewrite/RewritingVariable.hs b/kore/src/Kore/Rewrite/RewritingVariable.hs
@@ -3,7 +3,7 @@ Copyright   : (c) Runtime Verification, 2020-2021
 License     : BSD-3-Clause
 -}
 module Kore.Rewrite.RewritingVariable (
-    RewritingVariableName,
+    RewritingVariableName (..),
     RewritingVariable,
     isEquationVariable,
     isConfigVariable,

diff --git a/test/rpc-server/execute/branching-prune-unsat-remainder/response.golden b/test/rpc-server/execute/branching-prune-unsat-remainder/response.golden
diff --git a/test/rpc-server/execute/branching/definition.kore b/test/rpc-server/execute/branching/definition.kore
@@ -715,23 +715,23 @@ module TEST
         \top{SortK{}}())))
   [UNIQUE'Unds'ID{}("651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2305,8,2305,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/j993pnk64sgpw2qm7408ixnagfkknjzd-k-6.0.181-af105e4141030abe25055854fc02205be4ed223c-maven/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")]
 
-// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(V) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("b","State"))~>_DotVar2),_Gen5),_DotVar0) requires `_==Int_`(V,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b), label(TEST.AB), org.kframework.attributes.Location(Location(17,14,17,67)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
+// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(X) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("b","State"))~>_DotVar2),_Gen5),_DotVar0) requires `_==Int_`(X,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b), label(TEST.AB), org.kframework.attributes.Location(Location(17,14,17,67)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
   axiom{} \rewrites{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-        Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarV:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
+        Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarX:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
         \equals{SortBool{},SortGeneratedTopCell{}}(
-        Lbl'UndsEqlsEqls'Int'Unds'{}(VarV:SortInt{},\dv{SortInt{}}("0")),
+        Lbl'UndsEqlsEqls'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0")),
         \dv{SortBool{}}("true"))),
       \and{SortGeneratedTopCell{}} (
       Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("b")),Var'Unds'DotVar2:SortK{})),Var'Unds'Gen5:SortValCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()))
   [UNIQUE'Unds'ID{}("79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b"), label{}("TEST.AB"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(17,14,17,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")]
 
-// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(V) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("c","State"))~>_DotVar2),_Gen5),_DotVar0) requires `notBool_`(`_==Int_`(V,#token("0","Int"))) ensures #token("true","Bool") [UNIQUE_ID(6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d), label(TEST.AC), org.kframework.attributes.Location(Location(18,14,18,77)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
+// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(X) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("c","State"))~>_DotVar2),_Gen5),_DotVar0) requires `notBool_`(`_==Int_`(X,#token("0","Int"))) ensures #token("true","Bool") [UNIQUE_ID(6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d), label(TEST.AC), org.kframework.attributes.Location(Location(18,14,18,77)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
   axiom{} \rewrites{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-        Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarV:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
+        Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarX:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
         \equals{SortBool{},SortGeneratedTopCell{}}(
-        LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarV:SortInt{},\dv{SortInt{}}("0"))),
+        LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0"))),
         \dv{SortBool{}}("true"))),
       \and{SortGeneratedTopCell{}} (
       Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("c")),Var'Unds'DotVar2:SortK{})),Var'Unds'Gen5:SortValCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()))