Kore.Exec.prove: Return all failing results (#496)

* Kore.Exec.prove: Return all failing results

Returning all failing results is very useful for debugging and exploration.

Instead of this implementation, we may want to consider printing a flat list of
patterns. The result is always a disjunction at the top, but because it is a
list of patterns, that disjunction can quickly become very deeply nested.

* Test.Kore.OnePath.Verification: Check for multiple results

kore/src/Kore/Exec.hs

@@ -59,12 +59,13 @@ import           Kore.Step.BaseStep
                  ( StepProof )
 import           Kore.Step.Pattern
 import           Kore.Step.Representation.ExpandedPattern
-                 ( CommonExpandedPattern, Predicated (..), toMLPattern )
+                 ( CommonExpandedPattern, Predicated (..) )
 import qualified Kore.Step.Representation.ExpandedPattern as ExpandedPattern
 import qualified Kore.Step.Representation.ExpandedPattern as Predicated
 import qualified Kore.Step.Representation.MultiOr as MultiOr
 import           Kore.Step.Representation.OrOfExpandedPattern
                  ( OrOfExpandedPattern )
+import qualified Kore.Step.Representation.OrOfExpandedPattern as OrOfExpandedPattern
 import           Kore.Step.Search
                  ( searchGraph )
 import qualified Kore.Step.Search as Search
@@ -196,16 +197,16 @@ prove limit definitionModule specModule = do
         axioms = fmap Axiom rewriteRules
         claims = fmap makeClaim specAxioms
 
-    result <- runExceptT
+    result <-
+        runExceptT
         $ verify
             tools
             simplifier
             substitutionSimplifier
             axiomIdToSimplifier
             (defaultStrategy claims axioms)
             (map (\x -> (x,limit)) (extractUntrustedClaims claims))
-
-    return $ Bifunctor.first toMLPattern result
+    return $ Bifunctor.first OrOfExpandedPattern.toStepPattern result
 
   where
     makeClaim (attributes, rule) = Claim { rule , attributes }

kore/src/Kore/OnePath/Verification.hs

@@ -16,16 +16,12 @@ module Kore.OnePath.Verification
     , verify
     ) where
 
-import Control.Monad.IO.Class
-       ( liftIO )
-import Control.Monad.Reader
-       ( ask )
-import Control.Monad.Trans.Except
-       ( ExceptT, throwE )
-import Data.Proxy
-       ( Proxy (..) )
-import Numeric.Natural
-       ( Natural )
+import qualified Control.Monad as Monad
+import           Control.Monad.Trans.Except
+                 ( ExceptT, throwE )
+import           Data.Maybe
+import           Numeric.Natural
+                 ( Natural )
 
 import qualified Control.Monad.Trans as Monad.Trans
 import           Data.Limit
@@ -34,7 +30,7 @@ import qualified Data.Limit as Limit
 import           Kore.AST.Common
                  ( Variable )
 import           Kore.AST.MetaOrObject
-                 ( IsMetaOrObject (..), MetaOrObject (..) )
+                 ( MetaOrObject (..) )
 import qualified Kore.Attribute.Axiom as Attribute
 import           Kore.IndexedModule.MetadataTools
                  ( MetadataTools )
@@ -57,13 +53,17 @@ import           Kore.Step.Representation.ExpandedPattern as ExpandedPattern
                  ( fromPurePattern )
 import           Kore.Step.Representation.ExpandedPattern as Predicated
                  ( Predicated (..) )
+import qualified Kore.Step.Representation.MultiOr as MultiOr
+import           Kore.Step.Representation.OrOfExpandedPattern
+                 ( CommonOrOfExpandedPattern )
 import           Kore.Step.Simplification.Data
-                 ( Environment (proveClaim), PredicateSubstitutionSimplifier,
-                 Simplifier, StepPatternSimplifier )
+                 ( PredicateSubstitutionSimplifier, Simplifier,
+                 StepPatternSimplifier )
 import           Kore.Step.StepperAttributes
                  ( StepperAttributes )
 import           Kore.Step.Strategy
                  ( Strategy, pickFinal, runStrategy )
+import qualified Kore.TopBottom as TopBottom
 
 {- | Wrapper for a rewrite rule that should be used as a claim.
 -}
@@ -113,7 +113,7 @@ verify
     -- ^ List of claims, together with a maximum number of verification steps
     -- for each.
     -> ExceptT
-        (CommonExpandedPattern level)
+        (CommonOrOfExpandedPattern level)
         Simplifier
         ()
 verify
@@ -193,7 +193,7 @@ verifyClaim
         )
     -> (RewriteRule level Variable, Limit Natural)
     -> ExceptT
-        (CommonExpandedPattern level)
+        (CommonOrOfExpandedPattern level)
         Simplifier
         ()
 verifyClaim
@@ -202,12 +202,8 @@ verifyClaim
     substitutionSimplifier
     axiomIdToSimplifier
     strategyBuilder
-    (rule@(RewriteRule RulePattern {left, right, requires}), stepLimit)
+    ((RewriteRule RulePattern {left, right, requires}), stepLimit)
   = do
-    pc <- proveClaim <$> ask
-    liftIO' $ case isMetaOrObject (Proxy @level) of
-        IsObject -> pc rule
-        IsMeta -> pure ()
     let
         strategy =
             Limit.takeWithin
@@ -226,14 +222,10 @@ verifyClaim
         ( startPattern, mempty )
     let
         finalNodes = pickFinal executionGraph
-        nonBottomNodes = filter notBottom (map fst finalNodes)
-        notBottom StrategyPattern.Bottom = False
-        notBottom _ = True
-    case nonBottomNodes of
-        [] -> return ()
-        StrategyPattern.RewritePattern p : _ -> throwE p
-        StrategyPattern.Stuck p : _ -> throwE p
-        StrategyPattern.Bottom : _ -> error "Unexpected bottom pattern."
-  where
-    liftIO' :: IO () -> ExceptT (CommonExpandedPattern level) Simplifier ()
-    liftIO' = liftIO
+        remainingNodes =
+            MultiOr.make $ mapMaybe getRemainingNode (fst <$> finalNodes)
+          where
+            getRemainingNode (StrategyPattern.RewritePattern p) = Just p
+            getRemainingNode (StrategyPattern.Stuck          p) = Just p
+            getRemainingNode StrategyPattern.Bottom             = Nothing
+    Monad.unless (TopBottom.isBottom remainingNodes) (throwE remainingNodes)

kore/src/Kore/Step/Representation/OrOfExpandedPattern.hs

@@ -18,6 +18,7 @@ module Kore.Step.Representation.OrOfExpandedPattern
     , isTrue
     , makeFromSinglePurePattern
     , toExpandedPattern
+    , toStepPattern
     , toPredicate
     ) where
 
@@ -122,6 +123,26 @@ toExpandedPattern multiOr
             , substitution = mempty
             }
 
+{-| Transforms an 'OrOfExpandedPattern' into a 'StepPattern'.
+-}
+toStepPattern
+    ::  ( MetaOrObject level
+        , SortedVariable variable
+        , Ord (variable level)
+        , Show (variable level)
+        , Unparse (variable level)
+        )
+    => OrOfExpandedPattern level variable -> StepPattern level variable
+toStepPattern multiOr =
+    case MultiOr.extractPatterns multiOr of
+        [] -> mkBottom_
+        [patt] -> ExpandedPattern.toMLPattern patt
+        patt : patts ->
+            foldl'
+                (\x y -> mkOr x (ExpandedPattern.toMLPattern y))
+                (ExpandedPattern.toMLPattern patt)
+                patts
+
 {-| Transforms an 'OrOfPredicate' into a 'Predicate'. -}
 toPredicate
     ::  ( MetaOrObject level

kore/test/Test/Kore/OnePath/Verification.hs

@@ -37,7 +37,10 @@ import           Kore.Step.Representation.ExpandedPattern
 import           Kore.Step.Representation.ExpandedPattern as Predicated
                  ( Predicated (..) )
 import           Kore.Step.Representation.ExpandedPattern as ExpandedPattern
-                 ( CommonExpandedPattern, fromPurePattern )
+                 ( fromPurePattern )
+import qualified Kore.Step.Representation.MultiOr as MultiOr
+import           Kore.Step.Representation.OrOfExpandedPattern
+                 ( CommonOrOfExpandedPattern )
 import           Kore.Step.Simplification.Data
                  ( evalSimplifier )
 import qualified Kore.Step.Simplification.Simplifier as Simplifier
@@ -63,7 +66,7 @@ test_onePathVerification =
             [simpleAxiom Mock.a Mock.b]
             [simpleClaim Mock.a Mock.b]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.a)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.a])
             actual
     , testCase "Runs one step" $ do
         -- Axiom: a => b
@@ -80,7 +83,21 @@ test_onePathVerification =
             [simpleAxiom Mock.a Mock.b]
             [simpleClaim Mock.a Mock.b]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.b)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.b])
+            actual
+    , testCase "Returns multiple results" $ do
+        -- Axiom: a => b or c
+        -- Claim: a => d
+        -- Expected: error [b, c]
+        actual <- runVerification
+            metadataTools
+            (Limit 1)
+            [simpleAxiom Mock.a (mkOr Mock.b Mock.c)]
+            [simpleClaim Mock.a Mock.d]
+        assertEqualWithExplanation ""
+            (Left . MultiOr.make $
+                ExpandedPattern.fromPurePattern <$> [Mock.b, Mock.c]
+            )
             actual
     , testCase "Verifies one claim" $ do
         -- Axiom: a => b
@@ -105,7 +122,7 @@ test_onePathVerification =
             , simpleClaim Mock.a Mock.b
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.a)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.a])
             actual
     , testCase "Verifies one claim multiple steps" $ do
         -- Axiom: a => b
@@ -171,12 +188,15 @@ test_onePathVerification =
             ]
             [simpleClaim (Mock.functionalConstr10 (mkVar Mock.x)) Mock.b]
         assertEqualWithExplanation ""
-            (Left Predicated
-                { term = Mock.functionalConstr11 (mkVar Mock.x)
-                , predicate =
-                    makeNotPredicate (makeEqualsPredicate (mkVar Mock.x) Mock.a)
-                , substitution = mempty
-                }
+            (Left $ MultiOr.make
+                [ Predicated
+                    { term = Mock.functionalConstr11 (mkVar Mock.x)
+                    , predicate =
+                        makeNotPredicate
+                            (makeEqualsPredicate (mkVar Mock.x) Mock.a)
+                    , substitution = mempty
+                    }
+                ]
             )
             actual
     , testCase "Verifies two claims" $ do
@@ -217,7 +237,7 @@ test_onePathVerification =
             , simpleClaim Mock.d Mock.e
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.c)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.c])
             actual
     , testCase "fails second of two claims" $ do
         -- Axiom: a => b
@@ -237,7 +257,7 @@ test_onePathVerification =
             , simpleClaim Mock.d Mock.c
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.e)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.e])
             actual
     , testCase "second proves first but fails" $ do
         -- Axiom: a => b
@@ -255,7 +275,7 @@ test_onePathVerification =
             , simpleClaim Mock.b Mock.c
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.b)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.b])
             actual
     , testCase "first proves second but fails" $ do
         -- Axiom: a => b
@@ -273,7 +293,7 @@ test_onePathVerification =
             , simpleClaim Mock.a Mock.d
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.b)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.b])
             actual
     , testCase "trusted second proves first" $ do
         -- Axiom: a => b
@@ -332,7 +352,7 @@ test_onePathVerification =
             , simpleClaim Mock.b Mock.e
             ]
         assertEqualWithExplanation ""
-            (Left $ ExpandedPattern.fromPurePattern Mock.e)
+            (Left $ MultiOr.make [ExpandedPattern.fromPurePattern Mock.e])
             actual
     ]
   where
@@ -390,7 +410,7 @@ runVerification
     -> Limit Natural
     -> [OnePath.Axiom level]
     -> [OnePath.Claim level]
-    -> IO (Either (CommonExpandedPattern level) ())
+    -> IO (Either (CommonOrOfExpandedPattern level) ())
 runVerification
     metadataTools
     stepLimit