Bug fix for symbolic narrowing (#1997)

* test_narrowing: Tests for symbolic narrowing

* Kore.Internal.Substitution.substitute

* Kore.Internal.Pattern.substitute

* getResultPattern: Apply renaming to right-hand side of substitution

The renaming from rule to (fresh) configuration variables is also applied to the
right-hand side of the substitution. The renaming was already applied to the
term and predicate, but the substitution was overlooked. This fixes a bug that
manifests when narrowing a symbolic configuration into another symbolic
configuration.

* test_narrowing: Also check remainders

* CHANGELOG

* Kore.Internal.Pattern.substitute: Note about denormalized Substitution

Author: ttuegel

kore/CHANGELOG.md

@@ -14,6 +14,9 @@ All notable changes to this project will be documented in this file.
 
 ### Fixed
 
+- A bug is fixed where variables introduced by symbolic narrowing could be
+  captured incorrectly.
+
 ## [0.25.0.0] - 2020-07-08
 
 ### Added

kore/src/Kore/Internal/Pattern.hs

@@ -28,6 +28,7 @@ module Kore.Internal.Pattern
     , simplifiedAttribute
     , assign
     , requireDefined
+    , substitute
     -- * Re-exports
     , Conditional (..)
     , Conditional.andCondition
@@ -40,6 +41,10 @@ module Kore.Internal.Pattern
 
 import Prelude.Kore
 
+import Data.Map.Strict
+    ( Map
+    )
+
 import Kore.Attribute.Pattern.FreeVariables
     ( freeVariables
     , getFreeElementVariables
@@ -350,3 +355,20 @@ requireDefined Conditional { term, predicate, substitution } =
         }
   where
     sort = termLikeSort term
+
+{- | Apply a normalized 'Substitution' to a 'Pattern'.
+
+The 'Substitution' of the result will not be normalized.
+
+ -}
+substitute
+    :: InternalVariable variable
+    => Map (SomeVariableName variable) (TermLike variable)
+    -> Pattern variable
+    -> Pattern variable
+substitute subst Conditional { term, predicate, substitution } =
+    Conditional
+    { term = TermLike.substitute subst term
+    , predicate = Predicate.substitute subst predicate
+    , substitution = Substitution.substitute subst substitution
+    }

kore/src/Kore/Internal/Substitution.hs

@@ -46,6 +46,7 @@ module Kore.Internal.Substitution
     , wrapNormalization
     , mkNormalization
     , applyNormalized
+    , substitute
     ) where
 
 import Prelude.Kore hiding
@@ -702,16 +703,30 @@ applyNormalized
 applyNormalized Normalization { normalized, denormalized } =
     Normalization
         { normalized
-        , denormalized =
-            mapAssignedTerm substitute <$> denormalized
+        , denormalized = mapAssignedTerm substitute' <$> denormalized
         }
   where
-    substitute =
+    substitute' =
         TermLike.substitute
         $ Map.mapKeys variableName
         $ Map.fromList
         $ map assignmentToPair normalized
 
+{- | Apply a 'Map' from names to terms to a substitution.
+
+The given mapping will be applied only to the right-hand sides of the
+substitutions (see 'mapAssignedTerm').  The result will not be a normalized
+'Substitution'.
+
+ -}
+substitute
+    :: InternalVariable variable
+    => Map (SomeVariableName variable) (TermLike variable)
+    -> Substitution variable
+    -> Substitution variable
+substitute subst =
+    wrap . (map . mapAssignedTerm) (TermLike.substitute subst) . unwrap
+
 {- | @toPredicate@ constructs a 'Predicate' equivalent to 'Substitution'.
 
 An empty substitution list returns a true predicate. A non-empty substitution

kore/src/Kore/Rewriting/RewritingVariable.hs

@@ -210,11 +210,7 @@ getResultPattern initial config@Conditional { substitution } =
         . Map.map (TermLike.mkVar . mkUnifiedConfigVariable)
         $ refreshVariables avoiding introduced
     renamed :: Pattern RewritingVariableName
-    renamed =
-        filtered
-            { term = TermLike.substitute renaming (term filtered)
-            , predicate = Predicate.substitute renaming (predicate filtered)
-            }
+    renamed = filtered & Pattern.substitute renaming
 
 {- | Prepare a rule for unification or matching with the configuration.
 

kore/test/Test/Kore/Internal/Pattern.hs

@@ -30,6 +30,7 @@ import Test.Kore.Internal.TermLike hiding
     , mapVariables
     , markSimplified
     , simplifiedAttribute
+    , substitute
     )
 import Test.Kore.Variables.V
 import Test.Kore.Variables.W

kore/test/Test/Kore/Internal/Substitution.hs

@@ -1,10 +1,11 @@
 module Test.Kore.Internal.Substitution
     ( test_substitution
     , test_toPredicate
+    , test_substitute
     -- * Re-exports
     , TestAssignment
     , TestSubstitution
-    , module Kore.Internal.Substitution
+    , module Substitution
     , module Test.Kore.Internal.TermLike
     ) where
 
@@ -14,9 +15,10 @@ import Prelude.Kore hiding
 
 import Test.Tasty
 
+import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 
-import Kore.Internal.Substitution
+import Kore.Internal.Substitution as Substitution
 import Kore.TopBottom
     ( isBottom
     , isTop
@@ -39,6 +41,8 @@ import Test.Kore.Internal.TermLike hiding
     , mapVariables
     , markSimplified
     , simplifiedAttribute
+    , substitute
+    , test_substitute
     )
 import qualified Test.Kore.Step.MockSymbols as Mock
 import Test.Tasty.HUnit.Ext
@@ -361,3 +365,33 @@ pr1 =
 a, b :: Sort -> ElementVariable'
 a = fmap ElementVariableName . Variable (VariableName (testId "a") mempty)
 b = fmap ElementVariableName . Variable (VariableName (testId "b") mempty)
+
+test_substitute :: [TestTree]
+test_substitute =
+    [ testGroup "is denormalized"
+        [ testCase "Denormalized" $ do
+            let input = wrap [assign (inject Mock.x) Mock.a]
+                actual = Substitution.substitute Map.empty input
+            assertDenormalized actual
+        , testCase "Normalized" $ do
+            let input = unsafeWrap [(inject Mock.x, Mock.a)]
+                actual = Substitution.substitute Map.empty input
+            assertDenormalized actual
+        ]
+    , testCase "applies to right-hand side" $ do
+        let input = wrap [assign (inject Mock.x) (Mock.f (mkElemVar Mock.y))]
+            subst = Map.singleton (inject $ variableName Mock.y) Mock.a
+            expect = wrap [assign (inject Mock.x) (Mock.f Mock.a)]
+            actual = Substitution.substitute subst input
+        assertEqual "" expect actual
+    , testCase "does not apply to left-hand side" $ do
+        let input = wrap [assign (inject Mock.x) (Mock.f (mkElemVar Mock.y))]
+            subst = Map.singleton (inject $ variableName Mock.x) Mock.a
+            expect = input
+            actual = Substitution.substitute subst input
+        assertEqual "" expect actual
+    ]
+
+assertDenormalized :: HasCallStack => Substitution VariableName -> Assertion
+assertDenormalized =
+    assertBool "expected denormalized substitution" . (not . isNormalized)

kore/test/Test/Kore/Step/RewriteStep.hs

@@ -5,6 +5,7 @@ module Test.Kore.Step.RewriteStep
     , test_applyRewriteRule_
     , test_applyRewriteRulesParallel
     , test_applyRewriteRulesSequence
+    , test_narrowing
     ) where
 
 import Prelude.Kore
@@ -41,6 +42,7 @@ import Kore.Internal.Predicate as Predicate
     , makeTruePredicate
     , makeTruePredicate_
     )
+import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
 import Kore.Rewriting.RewritingVariable
@@ -738,6 +740,57 @@ test_applyRewriteRule_ =
             )
             (Mock.sigma (mkElemVar Mock.x) (mkElemVar Mock.y))
 
+{- | Tests for symbolic narrowing.
+
+Narrowing happens when a variable in a symbolic configuration is instantiated
+with a particular value.
+
+ -}
+test_narrowing :: [TestTree]
+test_narrowing =
+    [ testCase "applyRewriteRulesParallel" $ do
+        actual <- apply axiom (Pattern.fromTermLike initial)
+        let results = OrPattern.fromPatterns [result]
+        checkResults results actual
+        let remainders = OrPattern.fromPatterns [remainder]
+        checkRemainders remainders actual
+    , testCase "getResultPattern" $ do
+        let resultRewriting =
+                Pattern.withCondition (Mock.sigma Mock.b (mkElemVar xRule))
+                $ Condition.fromSingleSubstitution
+                $ Substitution.assign
+                    (inject xConfig)
+                    (Mock.sigma Mock.a (mkElemVar xRule))
+            initialVariables = FreeVariables.freeVariable (inject xConfig)
+            actual = getResultPattern initialVariables resultRewriting
+        assertEqual "" result actual
+    ]
+  where
+    apply rule config = applyRewriteRulesParallel config [rule]
+    x = Mock.x
+    x' = traverse (\name -> nextName name name) x & fromJust
+    xConfig = mkElementConfigVariable x
+    xRule = mkElementRuleVariable x
+    initial = mkElemVar x
+    -- The significance of this axiom is that it narrows the initial term and
+    -- introduces a new variable.
+    axiom =
+        RewriteRule $ rulePattern
+            (Mock.sigma Mock.a (mkElemVar x))
+            (Mock.sigma Mock.b (mkElemVar x))
+    result =
+        Pattern.withCondition (Mock.sigma Mock.b (mkElemVar x'))
+        $ Condition.fromSingleSubstitution
+        $ Substitution.assign (inject x) (Mock.sigma Mock.a (mkElemVar x'))
+    remainder =
+        Pattern.withCondition initial
+        $ Condition.fromPredicate
+        $ Predicate.makeNotPredicate
+        $ Predicate.makeExistsPredicate x'
+        $ Predicate.makeEqualsPredicate_
+            (mkElemVar x)
+            (Mock.sigma Mock.a (mkElemVar x'))
+
 -- | Apply the 'RewriteRule's to the configuration.
 applyRewriteRulesParallel
     :: TestPattern