From 7c8fbfbd25962043fecaa9b4df69f297137d4b32 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 11 Mar 2019 12:19:57 -0500 Subject: [PATCH] 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 | 9 ++-- kore/src/Kore/OnePath/Verification.hs | 54 ++++++++----------- .../Representation/OrOfExpandedPattern.hs | 21 ++++++++ kore/test/Test/Kore/OnePath/Verification.hs | 52 ++++++++++++------ 4 files changed, 85 insertions(+), 51 deletions(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index c672f3a47b..70afe06c36 100644 --- a/kore/src/Kore/Exec.hs +++ b/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,7 +197,8 @@ prove limit definitionModule specModule = do axioms = fmap Axiom rewriteRules claims = fmap makeClaim specAxioms - result <- runExceptT + result <- + runExceptT $ verify tools simplifier @@ -204,8 +206,7 @@ prove limit definitionModule specModule = do 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 } diff --git a/kore/src/Kore/OnePath/Verification.hs b/kore/src/Kore/OnePath/Verification.hs index 68538962d6..0bd8f9b986 100644 --- a/kore/src/Kore/OnePath/Verification.hs +++ b/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) diff --git a/kore/src/Kore/Step/Representation/OrOfExpandedPattern.hs b/kore/src/Kore/Step/Representation/OrOfExpandedPattern.hs index 280db9935f..4b305a73bd 100644 --- a/kore/src/Kore/Step/Representation/OrOfExpandedPattern.hs +++ b/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 diff --git a/kore/test/Test/Kore/OnePath/Verification.hs b/kore/test/Test/Kore/OnePath/Verification.hs index 9b3d13df3c..0e7793d848 100644 --- a/kore/test/Test/Kore/OnePath/Verification.hs +++ b/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