Emit a warning when kore-exec exceeds the depth limit (#2461)

* New log entry

* Emit Warning

* Format with stylish-haskell

* Update kore.cabal

Use `hpack -f kore` to regenerate kore.cabal

* Fix merge conflicts

* Add test for WarnDepthLimitExceeded

Test the warning emitted by exec when the depth limit is exceeded
by using a new MonadLog instance, called TestLog, that saves log entries
in its state

* Fix unrelated test name

* Format with stylish-haskell

* Materialize Nix expressions

Co-authored-by: andreiburdusa <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: andreiburdusa

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 2efec6a0024031e0d72609be302ec5298405ab977cfd1fac26ad002a0327ef18
+-- hash: 07e8077838828e32133511c3586cca1bb5973f27bc8cc2240aecfe790484d785
 
 name:           kore
 version:        0.41.0.0
@@ -224,6 +224,7 @@ library
       Kore.Log.Registry
       Kore.Log.SQLite
       Kore.Log.WarnBoundedModelChecker
+      Kore.Log.WarnDepthLimitExceeded
       Kore.Log.WarnFunctionWithoutEvaluators
       Kore.Log.WarnIfLowProductivity
       Kore.Log.WarnRetrySolverQuery

kore/src/Kore/Exec.hs

@@ -109,6 +109,9 @@ import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
     )
+import Kore.Log.WarnDepthLimitExceeded
+    ( warnDepthLimitExceeded
+    )
 import Kore.Log.WarnTrivialClaim
 import qualified Kore.ModelChecker.Bounded as Bounded
 import Kore.Reachability
@@ -254,7 +257,7 @@ exec
                         & lift
                 Strategy.leavesM
                     updateQueue
-                    (Strategy.unfoldTransition transit)
+                    (unfoldTransition transit)
                     ( limitedExecutionStrategy depthLimit
                     , (ExecDepth 0, Start initialConfig)
                     )
@@ -284,6 +287,9 @@ exec
     -- are internalized.
     metadataTools = MetadataTools.build verifiedModule
     initialSort = termLikeSort initialTerm
+    unfoldTransition transit (instrs, config) = do
+        when (null instrs) $ forM_ depthLimit warnDepthLimitExceeded
+        Strategy.unfoldTransition transit (instrs, config)
 
 {- | Modify a 'TransitionRule' to track the depth of the execution graph.
  -}

kore/src/Kore/Log/Registry.hs

@@ -113,6 +113,9 @@ import Kore.Log.InfoReachability
 import Kore.Log.WarnBoundedModelChecker
     ( WarnBoundedModelChecker
     )
+import Kore.Log.WarnDepthLimitExceeded
+    ( WarnDepthLimitExceeded
+    )
 import Kore.Log.WarnFunctionWithoutEvaluators
     ( WarnFunctionWithoutEvaluators
     )
@@ -181,6 +184,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
         , mk $ Proxy @WarnFunctionWithoutEvaluators
         , mk $ Proxy @WarnSymbolSMTRepresentation
         , mk $ Proxy @WarnStuckClaimState
+        , mk $ Proxy @WarnDepthLimitExceeded
         , mk $ Proxy @WarnBoundedModelChecker
         , mk $ Proxy @WarnIfLowProductivity
         , mk $ Proxy @WarnTrivialClaim

kore/src/Kore/Log/WarnDepthLimitExceeded.hs

@@ -0,0 +1,44 @@
+{- |
+Copyright   : (c) Runtime Verification, 2019
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnDepthLimitExceeded
+    ( WarnDepthLimitExceeded (..)
+    , warnDepthLimitExceeded
+    ) where
+
+import Prelude.Kore
+
+import Debug
+import Log
+import Numeric.Natural
+    ( Natural
+    )
+import Pretty
+    ( Pretty
+    , pretty
+    )
+import qualified Pretty
+
+newtype WarnDepthLimitExceeded =
+    WarnDepthLimitExceeded { limitExceeded :: Natural }
+    deriving (Show, Eq)
+
+instance Debug WarnDepthLimitExceeded where
+    debugPrec w = \_ -> Pretty.pretty . show $ w
+
+instance Diff WarnDepthLimitExceeded where
+    diffPrec = diffPrecEq
+instance Pretty WarnDepthLimitExceeded where
+    pretty (WarnDepthLimitExceeded n) =
+        Pretty.hsep
+            [ "The depth limit", pretty n, "was exceeded."]
+
+instance Entry WarnDepthLimitExceeded where
+    entrySeverity _ = Warning
+    helpDoc _ = "warn when depth limit is exceeded"
+
+warnDepthLimitExceeded :: MonadLog log => Natural -> log ()
+warnDepthLimitExceeded = logEntry . WarnDepthLimitExceeded

kore/test/Test/Kore/Exec.hs

@@ -4,13 +4,23 @@ module Test.Kore.Exec
     , test_searchPriority
     , test_searchExceedingBreadthLimit
     , test_execGetExitCode
+    , test_execDepthLimitExceeded
     ) where
 
 import Prelude.Kore
 
 import Test.Tasty
 
 import Control.Exception as Exception
+import Control.Monad.Catch
+    ( MonadCatch
+    , MonadMask
+    , MonadThrow
+    )
+import Control.Monad.State.Strict
+    ( StateT (..)
+    )
+import qualified Control.Monad.State.Strict as State
 import Data.Default
     ( def
     )
@@ -27,6 +37,7 @@ import System.Exit
     ( ExitCode (..)
     )
 
+import qualified Data.Bifunctor as Bifunctor
 import Data.Limit
     ( Limit (..)
     )
@@ -51,6 +62,7 @@ import Kore.Internal.Predicate
     )
 import Kore.Internal.TermLike
 import qualified Kore.Internal.TermLike as TermLike
+import Kore.Log.WarnDepthLimitExceeded
 import Kore.Step
     ( ExecutionMode (..)
     )
@@ -69,6 +81,9 @@ import Kore.Step.Search
     ( SearchType (..)
     )
 import qualified Kore.Step.Search as Search
+import Kore.Step.Simplification.Data
+    ( MonadProf
+    )
 import Kore.Step.Strategy
     ( LimitExceeded (..)
     )
@@ -78,6 +93,12 @@ import Kore.Syntax.Definition hiding
     )
 import qualified Kore.Syntax.Definition as Syntax
 import qualified Kore.Verified as Verified
+import Log
+    ( Entry (..)
+    , MonadLog (..)
+    , SomeEntry
+    )
+import qualified SMT
 
 import Test.Kore
 import qualified Test.Kore.IndexedModule.MockMetadataTools as Mock
@@ -123,6 +144,53 @@ test_execPriority = testCase "execPriority" $ actual >>= assertEqual "" expected
     inputPattern = applyToNoArgs mySort "a"
     expected = (ExitSuccess, applyToNoArgs mySort "d")
 
+newtype TestLog a = TestLog ( StateT [SomeEntry] SMT.NoSMT a )
+    deriving newtype (Functor, Applicative, Monad)
+    deriving newtype (State.MonadState [SomeEntry], MonadIO, SMT.MonadSMT)
+    deriving newtype (MonadThrow, MonadCatch, MonadMask, MonadProf)
+
+instance MonadLog TestLog where
+    logEntry entry = State.modify (toEntry entry :)
+    logWhile entry (TestLog state) =
+        TestLog $ State.mapStateT addEntry state
+      where
+        addEntry :: SMT.NoSMT (a, [SomeEntry]) -> SMT.NoSMT (a, [SomeEntry])
+        addEntry = fmap $ Bifunctor.second (toEntry entry :)
+
+runTestLog :: TestLog a -> IO [SomeEntry]
+runTestLog (TestLog state) = runNoSMT $ State.execStateT state []
+
+test_execDepthLimitExceeded :: TestTree
+test_execDepthLimitExceeded = testCase "exec exceeds depth limit"
+    $ do
+        entries <- actual
+        let actualDepthWarnings =
+                catMaybes $ fromEntry @WarnDepthLimitExceeded <$> entries
+            expectedWarning = WarnDepthLimitExceeded 1
+        assertEqual "" [expectedWarning] actualDepthWarnings
+  where
+    actual =
+        exec
+            (Limit 1)
+            Unlimited
+            verifiedModule
+            Any
+            inputPattern
+        & runTestLog
+    verifiedModule = verifiedMyModule Module
+        { moduleName = ModuleName "MY-MODULE"
+        , moduleSentences =
+            [ asSentence mySortDecl
+            , asSentence $ constructorDecl "a"
+            , asSentence $ constructorDecl "b"
+            , functionalAxiom "a"
+            , functionalAxiom "b"
+            , simpleRewriteAxiom "a" "b"
+            ]
+        , moduleAttributes = Attributes []
+        }
+    inputPattern = applyToNoArgs mySort "a"
+
 test_exec :: TestTree
 test_exec = testCase "exec" $ actual >>= assertEqual "" expected
   where

kore/test/Test/Kore/Step/Simplification/Overloading.hs

@@ -210,7 +210,7 @@ test_unifyOverloading =
                     (Mock.sortInjectionSubSubToTop Mock.aSubSubsort)
                 )
             )
-        , narrows "qqdirect overload vs. variable, left side; var direct"
+        , narrows "direct overload vs. variable, left side; var direct"
             ( Mock.topOverload (Mock.sortInjectionOtherToTop Mock.aOtherSort)
             , Mock.sortInjectionSubToTop (mkElemVar Mock.xConfigSubSort)
             )

nix/kore.nix.d/kore.nix

@@ -283,6 +283,7 @@
           "Kore/Log/Registry"
           "Kore/Log/SQLite"
           "Kore/Log/WarnBoundedModelChecker"
+          "Kore/Log/WarnDepthLimitExceeded"
           "Kore/Log/WarnFunctionWithoutEvaluators"
           "Kore/Log/WarnIfLowProductivity"
           "Kore/Log/WarnRetrySolverQuery"