diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index a71d41e579..82b0bdd97f 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -118,7 +118,6 @@ import Kore.Log , SomeEntry (..) , WithLog , logEntry - , logWarning , parseKoreLogOptions , runKoreLog , unparseKoreLogOptions @@ -126,6 +125,9 @@ import Kore.Log import Kore.Log.ErrorException ( errorException ) +import Kore.Log.WarnBoundedModelChecker + ( warnBoundedModelChecker + ) import Kore.Log.WarnIfLowProductivity ( warnIfLowProductivity ) @@ -770,8 +772,8 @@ koreBmc execOptions proveOptions = do graphSearch case checkResult of Bounded.Proved -> return success - Bounded.Unknown -> do - logWarning "The pattern does not terminate within the bound." + Bounded.Unknown claim -> do + warnBoundedModelChecker claim return success Bounded.Failed final -> return (failure final) lift $ renderResult execOptions (unparse final) diff --git a/kore/kore.cabal b/kore/kore.cabal index 45ef7b20eb..9af5844480 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -4,7 +4,7 @@ cabal-version: 2.2 -- -- see: https://github.com/sol/hpack -- --- hash: 7e4a37b77d7b81a22960b085c7c033ee8536b5990c1d4567ffca224c79a1e2aa +-- hash: c7335f234ff802f2b2d42c8970fd41a6fa133676b9afa09d411e6222e1120d42 name: kore version: 0.39.0.0 @@ -223,6 +223,7 @@ library Kore.Log.KoreLogOptions Kore.Log.Registry Kore.Log.SQLite + Kore.Log.WarnBoundedModelChecker Kore.Log.WarnFunctionWithoutEvaluators Kore.Log.WarnIfLowProductivity Kore.Log.WarnRetrySolverQuery diff --git a/kore/src/Kore/ASTVerifier/AttributesVerifier.hs b/kore/src/Kore/ASTVerifier/AttributesVerifier.hs index 13392e7987..5dd4d7d4bc 100644 --- a/kore/src/Kore/ASTVerifier/AttributesVerifier.hs +++ b/kore/src/Kore/ASTVerifier/AttributesVerifier.hs @@ -42,7 +42,7 @@ import Kore.AST.AstWithLocation ( locationFromAst ) import qualified Kore.Attribute.Parser as Attribute.Parser -import qualified Kore.Attribute.Symbol as Attribute +import qualified Kore.Attribute.Symbol as Attribute.Symbol import Kore.Error import Kore.IndexedModule.IndexedModule import Kore.IndexedModule.Resolvers @@ -149,7 +149,7 @@ verifyNoHookAttribute attributes = do verifyNoHookedSupersort :: MonadError (Error VerifyError) error - => IndexedModule Verified.Pattern Attribute.Symbol attrs + => IndexedModule Verified.Pattern Attribute.Symbol.Symbol attrs -> Attribute.Axiom SymbolOrAlias VariableName -> [Subsort.Subsort] -> error () @@ -176,7 +176,7 @@ verifyNoHookedSupersort indexedModule axiom subsorts = do verifyAxiomAttributes :: forall error attrs . MonadError (Error VerifyError) error - => IndexedModule Verified.Pattern Attribute.Symbol attrs + => IndexedModule Verified.Pattern Attribute.Symbol.Symbol attrs -> Attribute.Axiom SymbolOrAlias VariableName -> error (Attribute.Axiom Internal.Symbol.Symbol VariableName) verifyAxiomAttributes indexedModule axiom = do @@ -214,15 +214,15 @@ verifyAxiomAttributes indexedModule axiom = do verifySymbolAttributes :: forall error a . MonadError (Error VerifyError) error - => IndexedModule Verified.Pattern Attribute.Symbol a - -> Attribute.Symbol - -> error Attribute.Symbol + => IndexedModule Verified.Pattern Attribute.Symbol.Symbol a + -> Attribute.Symbol.Symbol + -> error Attribute.Symbol.Symbol verifySymbolAttributes _ attrs = return attrs verifySortAttributes :: forall error a . MonadError (Error VerifyError) error - => IndexedModule Verified.Pattern Attribute.Symbol a - -> Attribute.Symbol - -> error Attribute.Symbol + => IndexedModule Verified.Pattern Attribute.Symbol.Symbol a + -> Attribute.Symbol.Symbol + -> error Attribute.Symbol.Symbol verifySortAttributes _ attrs = return attrs diff --git a/kore/src/Kore/ASTVerifier/DefinitionVerifier.hs b/kore/src/Kore/ASTVerifier/DefinitionVerifier.hs index c55ce5f4a6..f642a7d5cb 100644 --- a/kore/src/Kore/ASTVerifier/DefinitionVerifier.hs +++ b/kore/src/Kore/ASTVerifier/DefinitionVerifier.hs @@ -44,7 +44,7 @@ import Kore.ASTVerifier.ModuleVerifier import Kore.ASTVerifier.Verifier import qualified Kore.Attribute.Axiom as Attribute import Kore.Attribute.Parser as Attribute.Parser -import qualified Kore.Attribute.Symbol as Attribute +import qualified Kore.Attribute.Symbol as Attribute.Symbol import qualified Kore.Builtin as Builtin import Kore.Error import Kore.IndexedModule.IndexedModule @@ -91,7 +91,7 @@ verifyAndIndexDefinition -> ParsedDefinition -> Either (Error VerifyError) - (Map.Map ModuleName (VerifiedModule Attribute.Symbol)) + (Map.Map ModuleName (VerifiedModule Attribute.Symbol.Symbol)) verifyAndIndexDefinition builtinVerifiers definition = do (indexedModules, _defaultNames) <- verifyAndIndexDefinitionWithBase @@ -127,7 +127,7 @@ verifyAndIndexDefinitionWithBase implicitModule :: ImplicitIndexedModule Verified.Pattern - Attribute.Symbol + Attribute.Symbol.Symbol (Attribute.Axiom Internal.Symbol.Symbol VariableName) implicitModule = ImplicitIndexedModule implicitIndexedModule parsedModules = modulesByName (definitionModules definition) diff --git a/kore/src/Kore/Attribute/Symbol.hs b/kore/src/Kore/Attribute/Symbol.hs index efd02e0d49..39afdc6254 100644 --- a/kore/src/Kore/Attribute/Symbol.hs +++ b/kore/src/Kore/Attribute/Symbol.hs @@ -83,6 +83,7 @@ import Kore.Attribute.Parser import Kore.Attribute.Smthook import Kore.Attribute.Smtlib import Kore.Attribute.SortInjection +import Kore.Attribute.SourceLocation import Kore.Attribute.Symbol.Anywhere import Kore.Attribute.Symbol.Klabel import Kore.Attribute.Symbol.Memo @@ -119,6 +120,8 @@ data Symbol = , klabel :: !Klabel , symbolKywd :: !SymbolKywd , noEvaluators :: !NoEvaluators + , sourceLocation :: !SourceLocation + -- ^ Location in the original (source) file. } deriving (Eq, Ord, Show) deriving (GHC.Generic) @@ -145,6 +148,7 @@ instance ParseAttributes Symbol where >=> typed @Klabel (parseAttribute attr) >=> typed @SymbolKywd (parseAttribute attr) >=> typed @NoEvaluators (parseAttribute attr) + >=> typed @SourceLocation (parseAttribute attr) instance From Symbol Attributes where from = @@ -162,6 +166,7 @@ instance From Symbol Attributes where , from . klabel , from . symbolKywd , from . noEvaluators + , from . sourceLocation ] type StepperAttributes = Symbol @@ -169,19 +174,20 @@ type StepperAttributes = Symbol defaultSymbolAttributes :: Symbol defaultSymbolAttributes = Symbol - { function = def - , functional = def - , constructor = def - , injective = def - , sortInjection = def - , anywhere = def - , hook = def - , smtlib = def - , smthook = def - , memo = def - , klabel = def - , symbolKywd = def - , noEvaluators = def + { function = def + , functional = def + , constructor = def + , injective = def + , sortInjection = def + , anywhere = def + , hook = def + , smtlib = def + , smthook = def + , memo = def + , klabel = def + , symbolKywd = def + , noEvaluators = def + , sourceLocation = def } -- | See also: 'defaultSymbolAttributes' diff --git a/kore/src/Kore/Attribute/Symbol/Klabel.hs b/kore/src/Kore/Attribute/Symbol/Klabel.hs index 0f1afb0314..8b671e2e81 100644 --- a/kore/src/Kore/Attribute/Symbol/Klabel.hs +++ b/kore/src/Kore/Attribute/Symbol/Klabel.hs @@ -19,6 +19,7 @@ import qualified GHC.Generics as GHC import Kore.Attribute.Parser as Parser import Kore.Debug +import Pretty -- | @Klabel@ represents the @klabel@ attribute for symbols. newtype Klabel = Klabel { getKlabel :: Maybe Text } @@ -31,6 +32,10 @@ newtype Klabel = Klabel { getKlabel :: Maybe Text } instance Default Klabel where def = Klabel Nothing +instance Pretty Klabel where + pretty (Klabel (Just text)) = pretty text + pretty (Klabel Nothing) = "" + -- | Kore identifier representing the @klabel@ attribute symbol. klabelId :: Id klabelId = "klabel" diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index fcb42b9d2d..daa004e0b9 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -532,7 +532,7 @@ boundedModelCheck -> VerifiedModule StepperAttributes -- ^ The spec module -> Strategy.GraphSearchOrder - -> smt (Bounded.CheckResult (TermLike VariableName)) + -> smt (Bounded.CheckResult (TermLike VariableName) (ImplicationRule VariableName)) boundedModelCheck breadthLimit depthLimit definitionModule specModule searchOrder = evalSimplifier definitionModule $ do initialized <- initializeAndSimplify definitionModule diff --git a/kore/src/Kore/Log/Registry.hs b/kore/src/Kore/Log/Registry.hs index 9e4f6cd987..1a00760ade 100644 --- a/kore/src/Kore/Log/Registry.hs +++ b/kore/src/Kore/Log/Registry.hs @@ -110,6 +110,9 @@ import Kore.Log.InfoProofDepth import Kore.Log.InfoReachability ( InfoReachability ) +import Kore.Log.WarnBoundedModelChecker + ( WarnBoundedModelChecker + ) import Kore.Log.WarnFunctionWithoutEvaluators ( WarnFunctionWithoutEvaluators ) @@ -178,6 +181,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()] , mk $ Proxy @WarnFunctionWithoutEvaluators , mk $ Proxy @WarnSymbolSMTRepresentation , mk $ Proxy @WarnStuckClaimState + , mk $ Proxy @WarnBoundedModelChecker , mk $ Proxy @WarnIfLowProductivity , mk $ Proxy @WarnTrivialClaim , mk $ Proxy @WarnRetrySolverQuery diff --git a/kore/src/Kore/Log/WarnBoundedModelChecker.hs b/kore/src/Kore/Log/WarnBoundedModelChecker.hs new file mode 100644 index 0000000000..40cb034b48 --- /dev/null +++ b/kore/src/Kore/Log/WarnBoundedModelChecker.hs @@ -0,0 +1,45 @@ +{- | +Copyright : (c) Runtime Verification, 2021 +License : NCSA + +-} + +module Kore.Log.WarnBoundedModelChecker + ( WarnBoundedModelChecker (..) + , warnBoundedModelChecker + ) where + +import Prelude.Kore + +import Kore.Attribute.SourceLocation +import Kore.Internal.TermLike +import Kore.Step.RulePattern + ( ImplicationRule + ) +import Log +import Pretty + ( Pretty + ) +import qualified Pretty + +newtype WarnBoundedModelChecker + = WarnBoundedModelChecker (ImplicationRule VariableName) + deriving Show + +instance Pretty WarnBoundedModelChecker where + pretty (WarnBoundedModelChecker claim) = + Pretty.hsep + [ "The claim was not proven within the bound:" + , Pretty.pretty (from @_ @SourceLocation claim) + ] + +instance Entry WarnBoundedModelChecker where + entrySeverity _ = Warning + helpDoc _ = "warn when the bounded model checker does not terminate within the given bound" + +warnBoundedModelChecker + :: MonadLog log + => ImplicationRule VariableName + -> log () +warnBoundedModelChecker claim = + logEntry (WarnBoundedModelChecker claim) diff --git a/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs b/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs index b8ed55eeb7..72d712f7ec 100644 --- a/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs +++ b/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs @@ -13,9 +13,11 @@ import Prelude.Kore import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC - +import qualified Kore.Attribute.Symbol as Attribute + ( Symbol (..) + ) import Kore.Internal.Symbol - ( Symbol + ( Symbol (..) , noEvaluators ) import Kore.Unparser @@ -44,9 +46,18 @@ instance SOP.HasDatatypeInfo WarnFunctionWithoutEvaluators instance Pretty WarnFunctionWithoutEvaluators where pretty WarnFunctionWithoutEvaluators { symbol } = + let Symbol { symbolAttributes } = symbol in + let Attribute.Symbol { klabel, sourceLocation } = symbolAttributes in Pretty.vsep [ "No evaluators for function symbol:" - , Pretty.indent 4 (unparse symbol) + , Pretty.indent 4 $ Pretty.hsep + [ unparse symbol + , Pretty.parens $ Pretty.pretty klabel + ] + , Pretty.hsep + [ "defined at:" + , Pretty.pretty sourceLocation + ] ] instance Entry WarnFunctionWithoutEvaluators where diff --git a/kore/src/Kore/Log/WarnStuckClaimState.hs b/kore/src/Kore/Log/WarnStuckClaimState.hs index 6d2c527848..0d54b5799d 100644 --- a/kore/src/Kore/Log/WarnStuckClaimState.hs +++ b/kore/src/Kore/Log/WarnStuckClaimState.hs @@ -12,6 +12,8 @@ module Kore.Log.WarnStuckClaimState import Prelude.Kore +import Kore.Attribute.SourceLocation +import Kore.Reachability.SomeClaim import Log import Pretty ( Pretty @@ -24,26 +26,32 @@ The warning message distinguishes for the user the ways that a proof can be stuc -} data WarnStuckClaimState - = TermsUnifiableStuck + = TermsUnifiableStuck !SomeClaim -- ^ The terms of the left- and right-hand sides do not unify, -- and the left-hand side cannot be rewritten any further. - | TermsNotUnifiableStuck + | TermsNotUnifiableStuck !SomeClaim -- ^ The left- and right-hand side terms are unifiable, but the left-hand side -- condition does not imply the right-hand side condition. deriving Show instance Pretty WarnStuckClaimState where - pretty TermsUnifiableStuck = - "The proof has reached the final configuration, but the claimed implication is not valid." - pretty TermsNotUnifiableStuck = - "The claim cannot be rewritten further, and the claimed implication is not valid." + pretty (TermsUnifiableStuck claim) = + Pretty.hsep + [ "The proof has reached the final configuration, but the claimed implication is not valid. Location:" + , Pretty.pretty (from claim :: SourceLocation) + ] + pretty (TermsNotUnifiableStuck claim) = + Pretty.hsep + [ "The claim cannot be rewritten further, and the claimed implication is not valid." + , Pretty.pretty (from claim :: SourceLocation) + ] instance Entry WarnStuckClaimState where entrySeverity _ = Warning helpDoc _ = "distinguish the ways a proof can become stuck" -warnStuckClaimStateTermsUnifiable :: MonadLog log => log () -warnStuckClaimStateTermsUnifiable = logEntry TermsUnifiableStuck +warnStuckClaimStateTermsUnifiable :: MonadLog log => SomeClaim -> log () +warnStuckClaimStateTermsUnifiable = logEntry . TermsUnifiableStuck -warnStuckClaimStateTermsNotUnifiable :: MonadLog log => log () -warnStuckClaimStateTermsNotUnifiable = logEntry TermsNotUnifiableStuck +warnStuckClaimStateTermsNotUnifiable :: MonadLog log => SomeClaim -> log () +warnStuckClaimStateTermsNotUnifiable = logEntry . TermsNotUnifiableStuck diff --git a/kore/src/Kore/ModelChecker/Bounded.hs b/kore/src/Kore/ModelChecker/Bounded.hs index 5e40c4e495..1ed835254c 100644 --- a/kore/src/Kore/ModelChecker/Bounded.hs +++ b/kore/src/Kore/ModelChecker/Bounded.hs @@ -66,12 +66,12 @@ import Numeric.Natural ( Natural ) -data CheckResult patt +data CheckResult patt claim = Proved -- ^ Property is proved within the bound. | Failed !patt -- ^ Counter example is found within the bound. - | Unknown + | Unknown !claim -- ^ Result is unknown within the bound. deriving (Show) @@ -104,12 +104,12 @@ checkClaim -> (ImplicationRule VariableName, Limit Natural) -- a claim to check, together with a maximum number of verification steps -- for each. - -> m (CheckResult (TermLike VariableName)) + -> m (CheckResult (TermLike VariableName) (ImplicationRule VariableName)) checkClaim breadthLimit strategyBuilder searchOrder - (ImplicationRule RulePattern { left, rhs = RHS { right } }, depthLimit) + (rule@(ImplicationRule RulePattern { left, rhs = RHS { right } }), depthLimit) = do let ApplyAlias_ Alias { aliasConstructor = alias } [prop] = right @@ -150,14 +150,14 @@ checkClaim checkFinalNodes :: [CommonProofState] - -> CheckResult (TermLike VariableName) + -> CheckResult (TermLike VariableName) (ImplicationRule VariableName) checkFinalNodes nodes = foldl' checkFinalNodesHelper Proved nodes where checkFinalNodesHelper Proved ProofState.Proven = Proved checkFinalNodesHelper Proved (ProofState.Unprovable config) = Failed (Pattern.toTermLike config) - checkFinalNodesHelper Proved _ = Unknown - checkFinalNodesHelper Unknown (ProofState.Unprovable config) = + checkFinalNodesHelper Proved _ = Unknown rule + checkFinalNodesHelper (Unknown _) (ProofState.Unprovable config) = Failed (Pattern.toTermLike config) - checkFinalNodesHelper Unknown _ = Unknown + checkFinalNodesHelper (Unknown _) _ = Unknown rule checkFinalNodesHelper (Failed config) _ = Failed config diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs index 61b4e95162..dcff3ca242 100644 --- a/kore/src/Kore/Reachability/Claim.hs +++ b/kore/src/Kore/Reachability/Claim.hs @@ -104,10 +104,6 @@ import Kore.Internal.TermLike , termLikeSort ) import Kore.Log.InfoReachability -import Kore.Log.WarnStuckClaimState - ( warnStuckClaimStateTermsNotUnifiable - , warnStuckClaimStateTermsUnifiable - ) import Kore.Reachability.ClaimState hiding ( claimState ) @@ -329,11 +325,9 @@ transitionRule claims axiomGroups = transitionRuleWorker case result of Implied -> pure Proven NotImpliedStuck a -> do - warnStuckClaimStateTermsUnifiable pure (Stuck a) NotImplied a | isRemainder claimState -> do - warnStuckClaimStateTermsNotUnifiable pure (Stuck a) | otherwise -> pure (Claimed a) | otherwise = pure claimState diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index bcfad73bf9..6e5c8557b1 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -90,6 +90,7 @@ import Kore.Log.DebugClaimState import Kore.Log.DebugProven import Kore.Log.InfoExecBreadth import Kore.Log.InfoProofDepth +import Kore.Log.WarnStuckClaimState import Kore.Log.WarnTrivialClaim import Kore.Reachability.Claim import Kore.Reachability.ClaimState @@ -409,6 +410,7 @@ transitionRule' transitionRule' claims axioms = \prim proofState -> deepseq proofState (transitionRule claims axiomGroups + & withWarnings & profTransitionRule & withConfiguration & withDebugClaimState @@ -420,6 +422,22 @@ transitionRule' claims axioms = \prim proofState -> where axiomGroups = groupSortOn Attribute.Axiom.getPriorityOfAxiom axioms +withWarnings + :: forall m + . MonadSimplify m + => CommonTransitionRule m + -> CommonTransitionRule m +withWarnings rule prim claimState = do + claimState' <- rule prim claimState + case prim of + Prim.CheckImplication | ClaimState.Stuck _ <- claimState' -> + case claimState of + ClaimState.Remaining claim -> warnStuckClaimStateTermsNotUnifiable claim + ClaimState.Claimed claim -> warnStuckClaimStateTermsUnifiable claim + _ -> return () + _ -> return () + return claimState' + profTransitionRule :: forall m . MonadProf m diff --git a/kore/src/Kore/Step/RulePattern.hs b/kore/src/Kore/Step/RulePattern.hs index bfb9774d25..cd395cd40d 100644 --- a/kore/src/Kore/Step/RulePattern.hs +++ b/kore/src/Kore/Step/RulePattern.hs @@ -504,6 +504,9 @@ newtype ImplicationRule variable = deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug, Diff) +instance From (ImplicationRule variable) Attribute.SourceLocation where + from (ImplicationRule rule) = from rule + instance InternalVariable variable => Unparse (ImplicationRule variable) diff --git a/kore/test/Test/Kore/Internal/Symbol.hs b/kore/test/Test/Kore/Internal/Symbol.hs index ed95e38fdc..da7684ce58 100644 --- a/kore/test/Test/Kore/Internal/Symbol.hs +++ b/kore/test/Test/Kore/Internal/Symbol.hs @@ -8,6 +8,7 @@ import qualified Hedgehog.Gen as Gen import qualified Data.Default as Default +import Kore.Attribute.SourceLocation import qualified Kore.Attribute.Symbol as Attribute import Kore.Internal.ApplicationSorts import Kore.Internal.Symbol @@ -50,6 +51,7 @@ symbolAttributeGen = <*> klabelAttributeGen <*> symbolKywdAttributeGen <*> noEvaluatorsAttributeGen + <*> sourceLocationAttributeGen functionAttributeGen :: Gen Attribute.Function functionAttributeGen = Attribute.Function <$> Gen.bool @@ -89,3 +91,6 @@ symbolKywdAttributeGen = Attribute.SymbolKywd <$> Gen.bool noEvaluatorsAttributeGen :: Gen Attribute.NoEvaluators noEvaluatorsAttributeGen = Attribute.NoEvaluators <$> Gen.bool + +sourceLocationAttributeGen :: Gen Kore.Attribute.SourceLocation.SourceLocation +sourceLocationAttributeGen = pure Default.def diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index 03091b9020..04b2001b51 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -282,6 +282,7 @@ "Kore/Log/KoreLogOptions" "Kore/Log/Registry" "Kore/Log/SQLite" + "Kore/Log/WarnBoundedModelChecker" "Kore/Log/WarnFunctionWithoutEvaluators" "Kore/Log/WarnIfLowProductivity" "Kore/Log/WarnRetrySolverQuery"