Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

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
                                 )
 

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 =

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,

test/rpc-server/execute/branching-prune-unsat-remainder/response.golden

@@ -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{}}()))