From 8ffa6f2033b47d06fe614b581c8d1e490c6de8a1 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 19 Jul 2020 20:21:19 -0500 Subject: [PATCH 1/7] test_narrowing: Tests for symbolic narrowing --- kore/test/Test/Kore/Step/RewriteStep.hs | 42 +++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index a33a103d45..68770d6a1f 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/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 @@ -738,6 +739,47 @@ 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 + , 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')) + -- | Apply the 'RewriteRule's to the configuration. applyRewriteRulesParallel :: TestPattern From 102d9f8d126f379176aa51893326844cdfb3741d Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 11:33:29 -0500 Subject: [PATCH 2/7] Kore.Internal.Substitution.substitute --- kore/src/Kore/Internal/Substitution.hs | 21 +++++++++-- kore/test/Test/Kore/Internal/Substitution.hs | 38 ++++++++++++++++++-- 2 files changed, 54 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs index fb98717503..8238750a71 100644 --- a/kore/src/Kore/Internal/Substitution.hs +++ b/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 diff --git a/kore/test/Test/Kore/Internal/Substitution.hs b/kore/test/Test/Kore/Internal/Substitution.hs index 1aa1cffa49..72820c0e0d 100644 --- a/kore/test/Test/Kore/Internal/Substitution.hs +++ b/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) From c6fd52cac794470ad430001bf4744477672e57a9 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 11:40:30 -0500 Subject: [PATCH 3/7] Kore.Internal.Pattern.substitute --- kore/src/Kore/Internal/Pattern.hs | 20 ++++++++++++++++++++ kore/test/Test/Kore/Internal/Pattern.hs | 1 + 2 files changed, 21 insertions(+) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index b62316bb80..ff2caa0c27 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/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,18 @@ requireDefined Conditional { term, predicate, substitution } = } where sort = termLikeSort term + +{- | Apply a normalized 'Substitution' to a 'Pattern'. + + -} +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 + } diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index 593a42b517..750e7c3980 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/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 From afb19f343af433d3d53db9b2fc3c11cd5ffbb8a8 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 11:41:15 -0500 Subject: [PATCH 4/7] 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. --- kore/src/Kore/Rewriting/RewritingVariable.hs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kore/src/Kore/Rewriting/RewritingVariable.hs b/kore/src/Kore/Rewriting/RewritingVariable.hs index 2e416e91d2..ffb75aabb9 100644 --- a/kore/src/Kore/Rewriting/RewritingVariable.hs +++ b/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. From 38f00f1c02b8cd474fefc682a9635ed9e33a7658 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 13:13:09 -0500 Subject: [PATCH 5/7] test_narrowing: Also check remainders --- kore/test/Test/Kore/Step/RewriteStep.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/kore/test/Test/Kore/Step/RewriteStep.hs b/kore/test/Test/Kore/Step/RewriteStep.hs index 68770d6a1f..10d86372dc 100644 --- a/kore/test/Test/Kore/Step/RewriteStep.hs +++ b/kore/test/Test/Kore/Step/RewriteStep.hs @@ -42,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 @@ -751,6 +752,8 @@ test_narrowing = 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)) @@ -779,6 +782,14 @@ test_narrowing = 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 From a5cbaf7d0e0718a7243d11eb3db0a98570b3e0e9 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 20 Jul 2020 13:15:39 -0500 Subject: [PATCH 6/7] CHANGELOG --- kore/CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kore/CHANGELOG.md b/kore/CHANGELOG.md index b89ec48a83..98bfdce401 100644 --- a/kore/CHANGELOG.md +++ b/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 From d873e1950a1556daecd50ef8e419f4b8eaf607e4 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Tue, 21 Jul 2020 11:14:35 -0500 Subject: [PATCH 7/7] Kore.Internal.Pattern.substitute: Note about denormalized Substitution --- kore/src/Kore/Internal/Pattern.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index ff2caa0c27..21b792e9a5 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -358,6 +358,8 @@ requireDefined Conditional { term, predicate, substitution } = {- | Apply a normalized 'Substitution' to a 'Pattern'. +The 'Substitution' of the result will not be normalized. + -} substitute :: InternalVariable variable