Adding missing location information to various warnings

kore/app/exec/Main.hs

@@ -118,14 +118,16 @@ import Kore.Log
     , SomeEntry (..)
     , WithLog
     , logEntry
-    , logWarning
     , parseKoreLogOptions
     , runKoreLog
     , unparseKoreLogOptions
     )
 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)

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

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

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)

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,26 +166,28 @@ instance From Symbol Attributes where
             , from . klabel
             , from . symbolKywd
             , from . noEvaluators
+            , from . sourceLocation
             ]
 
 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'

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) = "<no label>"
+
 -- | Kore identifier representing the @klabel@ attribute symbol.
 klabelId :: Id
 klabelId = "klabel"

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

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

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)

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

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