diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index 993b232c4f..6211b84308 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -407,6 +407,30 @@ rhsSubstitute subst RHS { existentials, right, ensures } = where subst' = foldr (Map.delete . inject . variableName) subst existentials +renameExistentials + :: forall variable + . HasCallStack + => InternalVariable variable + => Map (SomeVariableName variable) (SomeVariable variable) + -> RHS variable + -> RHS variable +renameExistentials rename RHS { existentials, right, ensures } = + RHS + { existentials = + renameVariable <$> existentials + , right = TermLike.substitute subst right + , ensures = Predicate.substitute subst ensures + } + where + renameVariable + :: ElementVariable variable + -> ElementVariable variable + renameVariable var = + let name = SomeVariableNameElement . variableName $ var + in maybe var expectElementVariable + $ Map.lookup name rename + subst = TermLike.mkVar <$> rename + rhsForgetSimplified :: InternalVariable variable => RHS variable -> RHS variable rhsForgetSimplified RHS { existentials, right, ensures } = RHS @@ -871,26 +895,36 @@ instance UnifyingRule RulePattern where precondition = requires - refreshRule avoid' rule1@(RulePattern _ _ _ _ _) = - let avoid = FreeVariables.toNames avoid' - rename = refreshVariables (avoid <> exVars) originalFreeVariables - subst = TermLike.mkVar <$> rename - left' = TermLike.substitute subst left - antiLeft' = TermLike.substitute subst <$> antiLeft - requires' = Predicate.substitute subst requires - rhs' = rhsSubstitute subst rhs - rule2 = - rule1 - { left = left' - , antiLeft = antiLeft' - , requires = requires' - , rhs = rhs' - } - in (rename, rule2) + refreshRule stale0' rule0@(RulePattern _ _ _ _ _) = + let stale0 = FreeVariables.toNames stale0' + freeVariables0 = freeVariables rule0 + renaming1 = + refreshVariables stale0 + $ FreeVariables.toSet freeVariables0 + freeVariables1 = + FreeVariables.toSet freeVariables0 + & Set.map (renameVariable renaming1) + & foldMap FreeVariables.freeVariable + existentials0 = Set.fromList . map inject $ existentials $ rhs rule0 + stale1 = FreeVariables.toNames freeVariables1 <> stale0 + renamingExists = refreshVariables stale1 existentials0 + subst = TermLike.mkVar <$> renaming1 + rule1 = + RulePattern + { left = left rule0 & TermLike.substitute subst + , antiLeft = antiLeft rule0 & fmap (TermLike.substitute subst) + , requires = requires rule0 & Predicate.substitute subst + , rhs = + rhs rule0 + & renameExistentials renamingExists + & rhsSubstitute subst + , attributes = attributes rule0 + } + in (renaming1, rule1) where - RulePattern { left, antiLeft, requires, rhs } = rule1 - exVars = Set.fromList $ inject . variableName <$> existentials rhs - originalFreeVariables = freeVariables rule1 & FreeVariables.toSet + renameVariable map' var = + Map.lookup (variableName var) map' + & fromMaybe var mapRuleVariables adj rule1@(RulePattern _ _ _ _ _) = rule1 diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs index ddecb45503..f2402b9449 100644 --- a/kore/src/Kore/Strategies/Goal.hs +++ b/kore/src/Kore/Strategies/Goal.hs @@ -808,7 +808,7 @@ removeDestination lensRulePattern mkState goal = removeDestinationWorker :: RulePattern VariableName -> m (ProofState goal (RulePattern VariableName)) - removeDestinationWorker rulePattern = + removeDestinationWorker (snd . Step.refreshRule mempty -> rulePattern) = do removal <- removalPatterns destination configuration existentials when (isTop removal) (succeed . mkState $ rulePattern) @@ -902,11 +902,14 @@ deriveWith -> goal -> Strategy.TransitionT (Rule goal) m (ProofState goal goal) deriveWith lensRulePattern mkRule takeStep rewrites goal = - (\x -> getCompose $ x goal) - $ Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) - $ \config -> Compose $ withConfiguration config $ do - results <- takeStep rewrites config & lift - deriveResults mkRule results + getCompose + $ Lens.forOf lensRulePattern goal + $ \rulePattern -> + fmap (snd . Step.refreshRule mempty) + $ Lens.forOf RulePattern.leftPattern rulePattern + $ \config -> Compose $ withConfiguration config $ do + results <- takeStep rewrites config & lift + deriveResults mkRule results -- | Apply 'Rule's to the goal in sequence. deriveSeq diff --git a/kore/test/Test/Kore/Step/RulePattern.hs b/kore/test/Test/Kore/Step/RulePattern.hs index 5acd9f7b77..cee023f162 100644 --- a/kore/test/Test/Kore/Step/RulePattern.hs +++ b/kore/test/Test/Kore/Step/RulePattern.hs @@ -1,6 +1,6 @@ module Test.Kore.Step.RulePattern ( test_freeVariables - , test_refreshRulePattern + , test_refreshRule ) where import Prelude.Kore @@ -32,9 +32,9 @@ test_freeVariables = actual = freeVariables testRulePattern assertEqual "Expected free variables" expect actual -test_refreshRulePattern :: TestTree -test_refreshRulePattern = - testCase "Rename target variables" $ do +test_refreshRule :: [TestTree] +test_refreshRule = + [ testCase "Rename target variables" $ do let avoiding :: FreeVariables VariableName avoiding = freeVariables testRulePattern (renaming, rulePattern') = @@ -54,6 +54,26 @@ test_refreshRulePattern = assertBool "Expected no free variables in common with original RulePattern" (all notAvoided (FreeVariables.toList free')) + , testCase "no stale variables" $ do + let (renaming, _) = refreshRule mempty testRulePattern + assertBool "expected not to rename variables" (null renaming) + , testGroup "stale existentials" $ + let assertions (renaming, RulePattern { rhs }) = do + assertBool "expected to refresh existentials" + (notElem Mock.y $ existentials rhs) + assertBool "expected to substitute fresh variables" + ((/=) (mkElemVar Mock.y) $ right rhs) + assertBool "expected not to rename free variables" + (null renaming) + in + [ testCase "from outside" $ do + let stale = freeVariable (inject Mock.y) + assertions $ refreshRule stale testRulePattern + , testCase "from left-hand side" $ do + let input = testRulePattern { left = mkElemVar Mock.y } + assertions $ refreshRule mempty input + ] + ] testRulePattern :: RulePattern VariableName testRulePattern = diff --git a/test/issue-1909/Makefile b/test/issue-1909/Makefile new file mode 100644 index 0000000000..caa7b2e4b4 --- /dev/null +++ b/test/issue-1909/Makefile @@ -0,0 +1 @@ +include $(CURDIR)/../include.mk diff --git a/test/issue-1909/sum-spec.k b/test/issue-1909/sum-spec.k new file mode 100644 index 0000000000..bc0b793fd3 --- /dev/null +++ b/test/issue-1909/sum-spec.k @@ -0,0 +1,15 @@ +module VERIFICATION + imports TEST +endmodule + +module SUM-SPEC + import VERIFICATION + + rule loop(N:Int) => . ... + C:Int => ?_ + S:Int => ?S:Int + requires + N >=Int 0 + ensures + ?S ==Int S +Int N *Int C +Int (N -Int 1) *Int N /Int 2 +endmodule diff --git a/test/issue-1909/sum-spec.k.out.golden b/test/issue-1909/sum-spec.k.out.golden new file mode 100644 index 0000000000..e663cb04e1 --- /dev/null +++ b/test/issue-1909/sum-spec.k.out.golden @@ -0,0 +1 @@ +#True diff --git a/test/issue-1909/test.k b/test/issue-1909/test.k new file mode 100644 index 0000000000..782c588623 --- /dev/null +++ b/test/issue-1909/test.k @@ -0,0 +1,24 @@ +// Copyright (c) 2020 K Team. All Rights Reserved. + +module TEST-SYNTAX + imports INT + + syntax Pgm ::= loop ( Int ) +endmodule + +module TEST + imports TEST-SYNTAX + + configuration + $PGM:Pgm + 1 + 0 + + rule + loop(0) => . ... + rule + loop(Times:Int => Times -Int 1) ... + C:Int => C +Int 1 + S:Int => S +Int C + requires Times >Int 0 +endmodule