Distinguish \bottom from stuck states (#2451)

* WIP

* Test

* Undo: Dockerfile

* Format with stylish-haskell

* Remove Strict pragma

* Test: --search-final

* Test: --search-final (also add 2.test and 2.test.golden)

* Use isBottom instead of comparing to mempty

* Format with stylish-haskell

* Rebuild

Co-authored-by: andreiburdusa <andreiburdusa@users.noreply.github.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

Author: andreiburdusa

kore/src/Kore/Exec.hs

@@ -28,6 +28,9 @@ import Control.Concurrent.MVar
 import Control.DeepSeq
     ( deepseq
     )
+import Control.Error
+    ( hoistMaybe
+    )
 import qualified Control.Lens as Lens
 import Control.Monad
     ( (>=>)
@@ -259,6 +262,7 @@ exec
         infoExecDepth (maximum depths)
         let finalConfigs' =
                 MultiOr.make
+                $ catMaybes
                 $ extractProgramState
                 <$> finalConfigs
         exitCode <- getExitCode verifiedModule finalConfigs'
@@ -407,11 +411,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

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 (..)
     )
@@ -89,6 +92,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 +116,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,61 +191,62 @@ 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
     transitionRuleWorker mode Rewrite (Start patt) =
         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 isBottom filteredConfigs
+            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
     :: Comonad w
     => 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

test/issue-2445/1.test

@@ -0,0 +1 @@
+1

test/issue-2445/1.test.out.golden

@@ -0,0 +1 @@
+#Bottom

test/issue-2445/2.test

@@ -0,0 +1 @@
+1

test/issue-2445/2.test.out.golden

@@ -0,0 +1 @@
+#Bottom

test/issue-2445/Makefile

@@ -0,0 +1,5 @@
+DEF = test
+include $(CURDIR)/../include.mk
+
+2.test.out: \
+	KRUN_OPTS += --search-final

test/issue-2445/test.k

@@ -0,0 +1,6 @@
+module TEST
+    imports INT
+    syntax FOO ::= "foo"
+    configuration <k> foo ~> $PGM:Int </k>
+    rule <k> foo => #Bottom ... </k>
+endmodule