Log rewrite rule remainders (#3944)

This PR allows logging Kore's rewrite rule remainders in full.

Example log message with `'kore>remainder'`:
```
[kore][execute][remainder][detail] After applying  1  rewrite rules there is a satisfiable remainder condition:  \not{_}(\not{_}(\equals{SortInt{}, _}(ConfigVarCONTRACT'Unds'ID:SortInt{}, Lbl'UndsAnd-'Int'Unds'{}(\dv{SortInt{}}("1461501637330902918203684832716283019655932542975"), Lbllookup{}(ConfigVarCONTRACT'Unds'STORAGE:SortMap{}, \dv{SortInt{}}("1"))))))
```
and in json:
```
{"context":["kore","execute","remainder",{"term":"39a4b3d"},{"rules-count":"1"}],"message":{"format":"KORE","version":1,"term":{"tag":"Not","sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"Not","sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"first":{"tag":"EVar","name":"VarCONTRACT'Unds'ID","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"App","name":"Lbl'UndsAnd-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1461501637330902918203684832716283019655932542975"},{"tag":"App","name":"Lbllookup","sorts":[],"args":[{"tag":"EVar","name":"VarCONTRACT'Unds'STORAGE","sort":{"tag":"SortApp","name":"SortMap","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}]}]}}}}}}
```

booster/tools/booster/Server.hs

@@ -389,6 +389,7 @@ logLevelToKoreLogEntryMap =
                 [ "DebugAttemptedRewriteRules"
                 , "DebugAppliedLabeledRewriteRule"
                 , "DebugAppliedRewriteRules"
+                , "DebugRewriteRulesRemainder"
                 , "DebugTerm"
                 ]
             )

kore/kore.cabal

@@ -352,6 +352,7 @@ library
     Kore.Log.DebugRewriteTrace
     Kore.Log.DebugSolver
     Kore.Log.DebugSubstitutionSimplifier
+    Kore.Log.DebugRewriteRulesRemainder
     Kore.Log.DebugTransition
     Kore.Log.DebugUnification
     Kore.Log.DebugUnifyBottom

kore/src/Kore/Log/DebugAppliedRewriteRules.hs

@@ -67,7 +67,8 @@ instance Entry DebugAppliedRewriteRules where
         | null appliedRewriteRules = True
         | otherwise = False
     oneLineDoc DebugAppliedRewriteRules{appliedRewriteRules}
-        | null appliedRewriteRules = mempty
+        | null appliedRewriteRules =
+            "failed to apply " <> pretty (length appliedRewriteRules) <> " rewrite rules"
         | otherwise =
             "applied " <> pretty (length appliedRewriteRules) <> " rewrite rules"
     oneLineJson DebugAppliedRewriteRules{appliedRewriteRules}

kore/src/Kore/Log/DebugRewriteRulesRemainder.hs

@@ -0,0 +1,122 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NoStrict #-}
+{-# LANGUAGE NoStrictData #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2020-2021
+License     : BSD-3-Clause
+-}
+module Kore.Log.DebugRewriteRulesRemainder (
+    DebugRewriteRulesRemainder (..),
+    debugRewriteRulesRemainder,
+) where
+
+import Data.Aeson (Value (Array), object, toJSON, (.=))
+import Data.Text qualified as Text
+import Data.Vector (fromList)
+import Kore.Internal.Conditional qualified as Conditional
+import Kore.Internal.Pattern (
+    Pattern,
+ )
+import Kore.Internal.Predicate (
+    Predicate,
+ )
+import Kore.Internal.Predicate qualified as Predicate
+import Kore.Internal.TermLike qualified as TermLike
+import Kore.Internal.Variable (
+    VariableName,
+    toVariableName,
+ )
+import Kore.Rewrite.RewritingVariable
+import Kore.Syntax.Json qualified as PatternJson
+import Kore.Unparser
+import Kore.Util (showHashHex)
+import Log
+import Prelude.Kore
+import Pretty (
+    Pretty (..),
+ )
+import Pretty qualified
+
+{- This log entry will be emitted if, after unifying with rewrite rules,
+   there is a satisfiable remainder condition  -}
+data DebugRewriteRulesRemainder = DebugRewriteRulesRemainder
+    { configuration :: !(Pattern VariableName)
+    -- ^ the state the rules unified with
+    , rulesCount :: !Int
+    -- ^ how many rules were unified
+    , remainder :: !(Predicate RewritingVariableName)
+    -- ^ the condition not covered by the rules
+    }
+    deriving stock (Show)
+
+instance Pretty DebugRewriteRulesRemainder where
+    pretty DebugRewriteRulesRemainder{..} =
+        Pretty.vsep
+            [ (Pretty.hsep . catMaybes)
+                [ Just "The rules"
+                , Just "produced a remainder"
+                , Just . pretty $ remainder
+                ]
+            , "On configuration:"
+            , Pretty.indent 2 . unparse $ configuration
+            ]
+
+instance Entry DebugRewriteRulesRemainder where
+    entrySeverity _ = Debug
+    helpDoc _ = "log rewrite rules remainder"
+
+    oneLineContextDoc
+        DebugRewriteRulesRemainder{} = [remainderContextName]
+
+    oneLineContextJson
+        DebugRewriteRulesRemainder{configuration, rulesCount} =
+            Array $
+                fromList
+                    [ toJSON remainderContextName
+                    , object
+                        [ "term" .= showHashHex (hash configuration)
+                        ]
+                    , object
+                        [ "rules-count" .= Text.pack (show rulesCount)
+                        ]
+                    ]
+
+    oneLineDoc (DebugRewriteRulesRemainder{rulesCount, remainder}) =
+        let context = [Pretty.brackets "detail"]
+            logMsg =
+                ( Pretty.hsep
+                    [ "After applying "
+                    , pretty rulesCount
+                    , " rewrite rules"
+                    , "there is a satisfiable remainder condition: "
+                    , Pretty.group . pretty $ remainder
+                    ]
+                )
+         in mconcat context <> logMsg
+
+    oneLineJson DebugRewriteRulesRemainder{remainder} =
+        toJSON
+            . PatternJson.fromPredicate sortBool
+            . Predicate.mapVariables (pure toVariableName)
+            $ remainder
+
+remainderContextName :: Text.Text
+remainderContextName = "remainder"
+
+sortBool :: TermLike.Sort
+sortBool =
+    (TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
+
+debugRewriteRulesRemainder ::
+    MonadLog log =>
+    Pattern RewritingVariableName ->
+    Int ->
+    Predicate RewritingVariableName ->
+    log ()
+debugRewriteRulesRemainder pat rulesCount remainder =
+    logEntry DebugRewriteRulesRemainder{..}
+  where
+    configuration = mapConditionalVariables TermLike.mapVariables pat
+    mapConditionalVariables mapTermVariables =
+        Conditional.mapVariables mapTermVariables (pure toVariableName)

kore/src/Kore/Log/Registry.hs

@@ -63,6 +63,9 @@ import Kore.Log.DebugProven (
 import Kore.Log.DebugRetrySolverQuery (
     DebugRetrySolverQuery,
  )
+import Kore.Log.DebugRewriteRulesRemainder (
+    DebugRewriteRulesRemainder,
+ )
 import Kore.Log.DebugRewriteTrace (
     DebugFinalPatterns,
     DebugInitialClaim,
@@ -229,6 +232,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
             , mk $ Proxy @DebugTransition
             , mk $ Proxy @DebugAppliedRewriteRules
             , mk $ Proxy @DebugAppliedLabeledRewriteRule
+            , mk $ Proxy @DebugRewriteRulesRemainder
             , mk $ Proxy @DebugAttemptedRewriteRules
             , mk $ Proxy @DebugSubstitutionSimplifier
             , mk $ Proxy @WarnFunctionWithoutEvaluators

kore/src/Kore/Rewrite/RewriteStep.hs

@@ -43,6 +43,7 @@ import Kore.Log.DebugAppliedRewriteRules (
     debugAppliedRewriteRules,
  )
 import Kore.Log.DebugCreatedSubstitution (debugCreatedSubstitution)
+import Kore.Log.DebugRewriteRulesRemainder (debugRewriteRulesRemainder)
 import Kore.Log.DebugRewriteTrace (
     debugRewriteTrace,
  )
@@ -323,6 +324,7 @@ finalizeRulesParallel
                     -- NB: the UNKNOWN case will trigger an exception in SMT.evalPredicate, which will
                     --     be caught by the top-level code in the RPC server and reported to the client
                     _ -> do
+                        debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
                         -- remainder condition is SAT: we are safe to explore
                         -- the remainder branch, i.e. to evaluate the functions in the configuration
                         -- with the remainder in the path condition and rewrite further

kore/src/Log/Entry.hs

@@ -66,7 +66,7 @@ class (Show entry, Typeable entry) => Entry entry where
 
     oneLineContextJson :: entry -> JSON.Value
     default oneLineContextJson :: entry -> JSON.Value
-    oneLineContextJson _ = JSON.Array mempty
+    oneLineContextJson entry = JSON.object ["entry" JSON..= entryTypeText (toEntry entry)]
 
     oneLineContextDoc :: entry -> [Text]
     default oneLineContextDoc :: entry -> [Text]