Do not ignore --strategy all (#2231)

* Use LogicT instead of MaybeT

* Exit code

* Stylish

* Use seqstrict

* Update two golden files

* Update a golden file

* Update golden

* Import Foldable

* Move import Foldable

* Use gather

* Remove ObserveAllT

* Addressed comments

* Compile

Author: andreiburdusa

kore/src/Kore/Exec.hs

@@ -29,7 +29,6 @@ import Control.DeepSeq
     )
 import Control.Error
     ( note
-    , runMaybeT
     )
 import qualified Control.Lens as Lens
 import Control.Monad
@@ -41,7 +40,6 @@ import Control.Monad.Catch
 import Data.Coerce
     ( coerce
     )
-import qualified Data.List as List
 import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
@@ -76,6 +74,11 @@ import Kore.IndexedModule.Resolvers
     ( resolveInternalSymbol
     )
 import qualified Kore.Internal.Condition as Condition
+import Kore.Internal.MultiOr
+    ( make
+    )
+import qualified Kore.Internal.MultiOr as MultiOr
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -146,6 +149,7 @@ import Kore.Step.Search
 import qualified Kore.Step.Search as Search
 import Kore.Step.Simplification.Data
     ( MonadProf
+    , SimplifierT
     , evalSimplifier
     )
 import qualified Kore.Step.Simplification.Data as Simplifier
@@ -171,6 +175,7 @@ import Log
 import qualified Log
 import Logic
     ( LogicT
+    , observeAllT
     )
 import qualified Logic
 import SMT
@@ -189,7 +194,8 @@ newtype Initialized = Initialized { rewriteRules :: [Rewrite] }
 
 -- | Symbolic execution
 exec
-    ::  ( MonadIO smt
+    :: forall smt
+    .   ( MonadIO smt
         , MonadLog smt
         , MonadSMT smt
         , MonadMask smt
@@ -207,8 +213,8 @@ exec breadthLimit verifiedModule strategy initialTerm =
     evalSimplifier verifiedModule' $ do
         initialized <- initialize verifiedModule
         let Initialized { rewriteRules } = initialized
-        (execDepth, finalConfig) <-
-            getFinalConfigOf $ do
+        finals <-
+            getFinalConfigsOf $ do
                 initialConfig <-
                     Pattern.simplify SideCondition.top
                         (Pattern.fromTermLike initialTerm)
@@ -234,21 +240,22 @@ exec breadthLimit verifiedModule strategy initialTerm =
                     ( strategy rewriteRules
                     , (ExecDepth 0, mkRewritingPattern initialConfig)
                     )
-        infoExecDepth execDepth
-        let finalConfig' = getRewritingPattern finalConfig
-        exitCode <- getExitCode verifiedModule finalConfig'
-        let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig'
+        let (depths, finalConfigs) = unzip finals
+        infoExecDepth (maximum depths)
+        let finalConfigs' = make $ getRewritingPattern <$> finalConfigs
+        exitCode <- getExitCode verifiedModule finalConfigs'
+        let finalTerm = forceSort initialSort $ OrPattern.toTermLike finalConfigs'
         return (exitCode, finalTerm)
   where
     dropStrategy = snd
-    -- Get the first final configuration of an execution graph.
-    getFinalConfigOf = takeFirstResult >=> orElseBottom
-      where
-        takeResult = snd
-        takeFirstResult act =
-            Logic.observeT (takeResult <$> lift act) & runMaybeT
-        orElseBottom =
-            pure . fromMaybe (ExecDepth 0, mkRewritingPattern (Pattern.bottomOf initialSort))
+    getFinalConfigsOf
+        :: LogicT
+            (SimplifierT smt)
+            ( [Strategy (Prim (RewriteRule RewritingVariableName))]
+            , (ExecDepth, Pattern RewritingVariableName)
+            )
+        -> SimplifierT smt [(ExecDepth, Pattern RewritingVariableName)]
+    getFinalConfigsOf act = observeAllT $ fmap snd act
     verifiedModule' =
         IndexedModule.mapPatterns
             -- TODO (thomas.tuegel): Move this into Kore.Builtin
@@ -277,33 +284,42 @@ trackExecDepth transit prim (execDepth, execState) = do
 
 -- | Project the value of the exit cell, if it is present.
 getExitCode
-    :: (MonadIO simplifier, MonadSimplify simplifier)
+    :: forall simplifier
+    .  (MonadIO simplifier, MonadSimplify simplifier)
     => VerifiedModule StepperAttributes
     -- ^ The main module
-    -> Pattern VariableName
+    -> OrPattern.OrPattern VariableName
     -- ^ The final configuration(s) of execution
     -> simplifier ExitCode
-getExitCode indexedModule finalConfig =
+getExitCode indexedModule configs =
     takeExitCode $ \mkExitCodeSymbol -> do
         let mkGetExitCode t = mkApplySymbol (mkExitCodeSymbol []) [t]
-        exitCodePattern <-
-            Pattern.simplifyTopConfiguration (mkGetExitCode <$> finalConfig)
-            >>= Logic.scatter
-        case Pattern.term exitCodePattern of
-            Builtin_ (Domain.BuiltinInt (Domain.InternalInt _ exit))
-              | exit == 0 -> return ExitSuccess
-              | otherwise -> return $ ExitFailure $ fromInteger exit
-            _ -> return $ ExitFailure 111
+        exitCodePatterns <-
+            do
+                config <- Logic.scatter configs
+                Pattern.simplifyTopConfiguration (mkGetExitCode <$> config)
+                    >>= Logic.scatter
+            & MultiOr.observeAllT
+        let exitCode =
+                case toList (MultiOr.map Pattern.term exitCodePatterns) of
+                    [exitTerm] -> extractExit exitTerm
+                    _      -> ExitFailure 111
+        return exitCode
   where
+    extractExit = \case
+        Builtin_ (Domain.BuiltinInt (Domain.InternalInt _ exit))
+          | exit == 0 -> ExitSuccess
+          | otherwise -> ExitFailure (fromInteger exit)
+        _ -> ExitFailure 111
+
     resolve = resolveInternalSymbol indexedModule . noLocationId
+
+    takeExitCode
+        :: (([Sort] -> Symbol) -> simplifier ExitCode)
+        -> simplifier ExitCode
     takeExitCode act =
-        case resolve "LblgetExitCode" of
-            Nothing -> pure ExitSuccess
-            Just mkGetExitCodeSymbol -> do
-                exitCodes <- Logic.observeAllT (act mkGetExitCodeSymbol)
-                case List.nub exitCodes of
-                    [exit] -> pure exit
-                    _      -> pure $ ExitFailure 111
+        resolve "LblgetExitCode"
+        & maybe (pure ExitSuccess) act
 
 -- | Symbolic search
 search

kore/src/Kore/Internal/MultiOr.hs

@@ -266,8 +266,8 @@ The result is simplified with the 'filterOr' function.
 
 -}
 mergeAll
-    :: (Ord term, TopBottom term)
-    => [MultiOr term]
+    :: (Ord term, TopBottom term, Foldable f)
+    => f (MultiOr term)
     -> MultiOr term
 mergeAll ors =
     filterOr (foldl' mergeGeneric (make []) ors)

test/imp/imp.k

@@ -27,8 +27,8 @@ argument, because we want to give it a short-circuit semantics. */
 
   syntax AExp  ::= Int | Id | "?Int"
                  | "-" Int                    [format(%1%2)]
-                 | AExp "/" AExp              [left, strict, color(pink)]
-                 > AExp "+" AExp              [left, strict, color(pink)]
+                 | AExp "/" AExp              [left, seqstrict, color(pink)]
+                 > AExp "+" AExp              [left, seqstrict, color(pink)]
                  | "(" AExp ")"               [bracket]
   syntax BExp  ::= Bool
                  | AExp "<=" AExp             [seqstrict, latex({#1}\leq{#2}), color(pink)]

test/imp/impossible-branch.imp.out.golden

@@ -1,16 +1,33 @@
-  <T>
-    <k>
-      .
-    </k>
-    <state>
-      r |-> 0
-      x |-> ?I:Int
-      y |-> ?I0:Int
-    </state>
-  </T>
-#And
-  {
-    false
-  #Equals
-    ?I <=Int ?I0
-  }
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        r |-> 0
+        x |-> ?I:Int
+        y |-> ?I0:Int
+      </state>
+    </T>
+  #And
+    {
+      false
+    #Equals
+      ?I <=Int ?I0
+    }
+#Or
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        r |-> 0
+        x |-> ?I:Int
+        y |-> ?I0:Int
+      </state>
+    </T>
+  #And
+    {
+      true
+    #Equals
+      ?I <=Int ?I0
+    }

test/imp/max-symbolic.imp.out.golden

@@ -1,23 +1,95 @@
-  <T>
-    <k>
-      .
-    </k>
-    <state>
-      max |-> ?I:Int
-      x |-> ?I:Int
-      y |-> ?I0:Int
-      z |-> ?I1:Int
-    </state>
-  </T>
-#And
-  {
-    false
-  #Equals
-    ?I <=Int ?I0
-  }
-#And
-  {
-    false
-  #Equals
-    ?I <=Int ?I1
-  }
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        max |-> ?I0:Int
+        x |-> ?I:Int
+        y |-> ?I0:Int
+        z |-> ?I1:Int
+      </state>
+    </T>
+  #And
+    {
+      false
+    #Equals
+      ?I0 <=Int ?I1
+    }
+  #And
+    {
+      true
+    #Equals
+      ?I <=Int ?I0
+    }
+#Or
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        max |-> ?I1:Int
+        x |-> ?I:Int
+        y |-> ?I0:Int
+        z |-> ?I1:Int
+      </state>
+    </T>
+  #And
+    {
+      false
+    #Equals
+      ?I <=Int ?I0
+    }
+  #And
+    {
+      true
+    #Equals
+      ?I <=Int ?I1
+    }
+#Or
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        max |-> ?I1:Int
+        x |-> ?I:Int
+        y |-> ?I0:Int
+        z |-> ?I1:Int
+      </state>
+    </T>
+  #And
+    {
+      true
+    #Equals
+      ?I0 <=Int ?I1
+    }
+  #And
+    {
+      true
+    #Equals
+      ?I <=Int ?I0
+    }
+#Or
+    <T>
+      <k>
+        .
+      </k>
+      <state>
+        max |-> ?I:Int
+        x |-> ?I:Int
+        y |-> ?I0:Int
+        z |-> ?I1:Int
+      </state>
+    </T>
+  #And
+    {
+      false
+    #Equals
+      ?I <=Int ?I0
+    }
+  #And
+    {
+      false
+    #Equals
+      ?I <=Int ?I1
+    }

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

@@ -1,9 +1,19 @@
-  <k>
-    I:Int ~> .
-  </k>
-#And
-  {
-    Some I
-  #Equals
-    f ( )
-  }
+    <k>
+      I:Int ~> .
+    </k>
+  #And
+    {
+      Some I
+    #Equals
+      f ( )
+    }
+#Or
+    <k>
+      true ~> .
+    </k>
+  #And
+    {
+      None
+    #Equals
+      f ( )
+    }

test/search/initial.search.out.golden

@@ -1,3 +1,7 @@
-<k>
-  final2 ~> .
-</k>
+  <k>
+    final1 ~> .
+  </k>
+#Or
+  <k>
+    final2 ~> .
+  </k>