From 6f298f676059fd1e33e6fd63b24e155e46b6a312 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Wed, 10 Mar 2021 16:48:39 +0200 Subject: [PATCH 01/10] WIP --- Dockerfile | 2 +- kore/src/Kore/Exec.hs | 10 ++++---- kore/src/Kore/Step.hs | 53 ++++++++++++++++++++++++------------------- 3 files changed, 36 insertions(+), 29 deletions(-) diff --git a/Dockerfile b/Dockerfile index 7f7f417372..e2a39a5e96 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,5 +1,5 @@ ARG K_COMMIT -FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT} +FROM runtimeverificationinc/kframework-k:ubuntu-focal-${K_COMMIT} ENV TZ=America/Chicago RUN ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \ diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index a937b241f8..659b16e327 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -24,6 +24,7 @@ module Kore.Exec import Prelude.Kore +import Control.Error (hoistMaybe) import Control.Concurrent.MVar import Control.DeepSeq ( deepseq @@ -259,6 +260,7 @@ exec infoExecDepth (maximum depths) let finalConfigs' = MultiOr.make + $ catMaybes $ extractProgramState <$> finalConfigs exitCode <- getExitCode verifiedModule finalConfigs' @@ -407,11 +409,9 @@ search executionGraph <- runStrategy' (Start initialPattern) let - match target config1 config2 = - Search.matchWith - target - config1 - (extractProgramState config2) + match target config1 config2 = do + extracted <- hoistMaybe $ extractProgramState config2 + Search.matchWith target config1 extracted solutionsLists <- searchGraph searchConfig diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs index 5457bbb217..d99d39ee68 100644 --- a/kore/src/Kore/Step.hs +++ b/kore/src/Kore/Step.hs @@ -6,6 +6,8 @@ Strategy-based interface to rule application (step-wise execution). -} +{-# LANGUAGE Strict #-} + module Kore.Step ( ExecutionMode (..) , ProgramState (..) @@ -89,6 +91,8 @@ data ProgramState a | Remaining !a -- ^ The configuration is a remainder resulting -- from rewrite rule application. + | Bottom + -- ^ The execution step yields no children deriving (Eq, Ord, Show) deriving (Functor) deriving (GHC.Generic) @@ -111,11 +115,13 @@ instance Unparse a => Pretty (ProgramState a) where [ "remaining:" , Pretty.indent 4 $ unparse a ] + pretty Bottom = "\\bottom" -extractProgramState :: ProgramState a -> a -extractProgramState (Rewritten a) = a -extractProgramState (Remaining a) = a -extractProgramState (Start a) = a +extractProgramState :: ProgramState a -> Maybe a +extractProgramState (Rewritten a) = Just a +extractProgramState (Remaining a) = Just a +extractProgramState (Start a) = Just a +extractProgramState Bottom = Nothing retractRemaining :: ProgramState a -> Maybe a retractRemaining (Remaining a) = Just a @@ -184,13 +190,16 @@ transitionRule rewriteGroups = transitionRuleWorker transitionRuleWorker _ Begin (Rewritten a) = pure $ Start a transitionRuleWorker _ Begin (Remaining _) = empty transitionRuleWorker _ Begin state@(Start _) = pure state + transitionRuleWorker _ Begin Bottom = empty transitionRuleWorker _ Simplify (Rewritten patt) = - Rewritten <$> transitionSimplify patt + transitionSimplify Rewritten patt transitionRuleWorker _ Simplify (Remaining patt) = - Remaining <$> transitionSimplify patt + transitionSimplify Remaining patt transitionRuleWorker _ Simplify (Start patt) = - Start <$> transitionSimplify patt + transitionSimplify Start patt + transitionRuleWorker _ Simplify Bottom = + empty transitionRuleWorker mode Rewrite (Remaining patt) = transitionRewrite mode patt @@ -198,39 +207,35 @@ transitionRule rewriteGroups = transitionRuleWorker transitionRewrite mode patt transitionRuleWorker _ Rewrite state@(Rewritten _) = pure state + transitionRuleWorker _ Rewrite Bottom = + empty - transitionSimplify config = do + transitionSimplify prim config = do configs <- lift $ Pattern.simplifyTopConfiguration config filteredConfigs <- SMT.Evaluator.filterMultiOr configs - asum (pure <$> toList filteredConfigs) + if filteredConfigs == mempty + then pure Bottom + else prim <$> asum (pure <$> toList filteredConfigs) - transitionRewrite All patt = - transitionAllRewrite patt - transitionRewrite Any patt = - transitionAnyRewrite patt + transitionRewrite All patt = transitionAllRewrite patt + transitionRewrite Any patt = transitionAnyRewrite patt transitionAllRewrite config = foldM transitionRewrite' (Remaining config) rewriteGroups where transitionRewrite' applied rewrites | Just config' <- retractRemaining applied = - Step.applyRewriteRulesParallel - rewrites - config' + Step.applyRewriteRulesParallel rewrites config' & lift >>= deriveResults >>= simplifyRemainder | otherwise = pure applied - simplifyRemainder (Remaining p) = - Remaining <$> transitionSimplify p + simplifyRemainder (Remaining p) = transitionSimplify Remaining p simplifyRemainder p = return p transitionAnyRewrite config = do let rules = concat rewriteGroups - results <- - Step.applyRewriteRulesSequence - config - rules + results <- Step.applyRewriteRulesSequence config rules deriveResults results deriveResults @@ -238,7 +243,9 @@ deriveResults => Result.Results (w (RulePattern variable)) a -> TransitionT (RewriteRule variable) m (ProgramState a) deriveResults Result.Results { results, remainders } = - addResults results <|> addRemainders remainders + if null results && null remainders + then pure Bottom + else addResults results <|> addRemainders remainders where addResults results' = asum (addResult <$> results') addResult Result.Result { appliedRule, result } = do From a58406a7b242bd1c6de13641b3ba4bcfaab126f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Wed, 10 Mar 2021 16:50:38 +0200 Subject: [PATCH 02/10] Test --- test/issue-2445/1.test | 1 + test/issue-2445/1.test.out.golden | 1 + test/issue-2445/Makefile | 2 ++ test/issue-2445/test.k | 6 ++++++ 4 files changed, 10 insertions(+) create mode 100644 test/issue-2445/1.test create mode 100644 test/issue-2445/1.test.out.golden create mode 100644 test/issue-2445/Makefile create mode 100644 test/issue-2445/test.k diff --git a/test/issue-2445/1.test b/test/issue-2445/1.test new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/test/issue-2445/1.test @@ -0,0 +1 @@ +1 diff --git a/test/issue-2445/1.test.out.golden b/test/issue-2445/1.test.out.golden new file mode 100644 index 0000000000..88b8f237d0 --- /dev/null +++ b/test/issue-2445/1.test.out.golden @@ -0,0 +1 @@ +#Bottom diff --git a/test/issue-2445/Makefile b/test/issue-2445/Makefile new file mode 100644 index 0000000000..382792481e --- /dev/null +++ b/test/issue-2445/Makefile @@ -0,0 +1,2 @@ +DEF = test +include $(CURDIR)/../include.mk diff --git a/test/issue-2445/test.k b/test/issue-2445/test.k new file mode 100644 index 0000000000..72664fbeba --- /dev/null +++ b/test/issue-2445/test.k @@ -0,0 +1,6 @@ +module TEST + imports INT + syntax FOO ::= "foo" + configuration foo ~> $PGM:Int + rule foo => #Bottom ... +endmodule \ No newline at end of file From dc788598a455c3086fa97182c847f3a3c9f75beb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Wed, 10 Mar 2021 16:50:55 +0200 Subject: [PATCH 03/10] Undo: Dockerfile --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e2a39a5e96..7f7f417372 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,5 +1,5 @@ ARG K_COMMIT -FROM runtimeverificationinc/kframework-k:ubuntu-focal-${K_COMMIT} +FROM runtimeverificationinc/kframework-k:ubuntu-bionic-${K_COMMIT} ENV TZ=America/Chicago RUN ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \ From 00214e04b67b718be58e3ba3ecee2d043f8b4c2f Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Wed, 10 Mar 2021 14:53:29 +0000 Subject: [PATCH 04/10] Format with stylish-haskell --- kore/src/Kore/Exec.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 659b16e327..58431fb316 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -24,11 +24,13 @@ module Kore.Exec import Prelude.Kore -import Control.Error (hoistMaybe) import Control.Concurrent.MVar import Control.DeepSeq ( deepseq ) +import Control.Error + ( hoistMaybe + ) import qualified Control.Lens as Lens import Control.Monad ( (>=>) From 62073f10efe323d068d36e8d992f95d57f6aa610 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Thu, 11 Mar 2021 11:56:08 +0200 Subject: [PATCH 05/10] Remove Strict pragma --- kore/src/Kore/Step.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs index d99d39ee68..537f108ba7 100644 --- a/kore/src/Kore/Step.hs +++ b/kore/src/Kore/Step.hs @@ -6,8 +6,6 @@ Strategy-based interface to rule application (step-wise execution). -} -{-# LANGUAGE Strict #-} - module Kore.Step ( ExecutionMode (..) , ProgramState (..) From f33c65beff2cb159937c6f6105b9d76c201a044e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Thu, 11 Mar 2021 16:20:42 +0200 Subject: [PATCH 06/10] Test: --search-final --- test/issue-2445/Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/issue-2445/Makefile b/test/issue-2445/Makefile index 382792481e..685066e8f8 100644 --- a/test/issue-2445/Makefile +++ b/test/issue-2445/Makefile @@ -1,2 +1,5 @@ DEF = test include $(CURDIR)/../include.mk + +2.test.out: \ + KRUN_OPTS += --search-final \ No newline at end of file From 6fd8bcc5aa4e2afc0e62ba4686d5533e57f1eef3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Thu, 11 Mar 2021 16:23:19 +0200 Subject: [PATCH 07/10] Test: --search-final (also add 2.test and 2.test.golden) --- test/issue-2445/2.test | 1 + test/issue-2445/2.test.out.golden | 1 + 2 files changed, 2 insertions(+) create mode 100644 test/issue-2445/2.test create mode 100644 test/issue-2445/2.test.out.golden diff --git a/test/issue-2445/2.test b/test/issue-2445/2.test new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/test/issue-2445/2.test @@ -0,0 +1 @@ +1 diff --git a/test/issue-2445/2.test.out.golden b/test/issue-2445/2.test.out.golden new file mode 100644 index 0000000000..88b8f237d0 --- /dev/null +++ b/test/issue-2445/2.test.out.golden @@ -0,0 +1 @@ +#Bottom From beb430eb613a0813a75bd97625fd84404addb4dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Mon, 15 Mar 2021 11:52:21 +0200 Subject: [PATCH 08/10] Use isBottom instead of comparing to mempty --- kore/src/Kore/Step.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs index 537f108ba7..59915d7420 100644 --- a/kore/src/Kore/Step.hs +++ b/kore/src/Kore/Step.hs @@ -77,6 +77,7 @@ import Pretty ( Pretty ) import qualified Pretty +import Kore.TopBottom (isBottom) {- | The program's state during symbolic execution. -} @@ -211,7 +212,7 @@ transitionRule rewriteGroups = transitionRuleWorker transitionSimplify prim config = do configs <- lift $ Pattern.simplifyTopConfiguration config filteredConfigs <- SMT.Evaluator.filterMultiOr configs - if filteredConfigs == mempty + if isBottom filteredConfigs then pure Bottom else prim <$> asum (pure <$> toList filteredConfigs) From 00ee8cd9dd81bfdd42a02f7712ed6ba47476b567 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Mon, 15 Mar 2021 09:54:42 +0000 Subject: [PATCH 09/10] Format with stylish-haskell --- kore/src/Kore/Step.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Step.hs b/kore/src/Kore/Step.hs index 59915d7420..389e4c2298 100644 --- a/kore/src/Kore/Step.hs +++ b/kore/src/Kore/Step.hs @@ -70,6 +70,9 @@ import Kore.Step.Strategy hiding ( transitionRule ) import qualified Kore.Step.Strategy as Strategy +import Kore.TopBottom + ( isBottom + ) import Kore.Unparser ( Unparse (..) ) @@ -77,7 +80,6 @@ import Pretty ( Pretty ) import qualified Pretty -import Kore.TopBottom (isBottom) {- | The program's state during symbolic execution. -} From d922c7e50b6293e90994add9ac1985c337997652 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20Burdu=C8=99a?= Date: Tue, 16 Mar 2021 15:03:27 +0200 Subject: [PATCH 10/10] Rebuild