From 5b32b7b9a3133aacbd9f8fc6ce2e6dc2d0bc63a0 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 20 Jun 2024 09:02:40 +0200 Subject: [PATCH] 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 | 1 + kore/kore.cabal | 1 + kore/src/Kore/Log/DebugAppliedRewriteRules.hs | 3 +- .../Kore/Log/DebugRewriteRulesRemainder.hs | 122 ++++++++++++++++++ kore/src/Kore/Log/Registry.hs | 4 + kore/src/Kore/Rewrite/RewriteStep.hs | 2 + kore/src/Log/Entry.hs | 2 +- 7 files changed, 133 insertions(+), 2 deletions(-) create mode 100644 kore/src/Kore/Log/DebugRewriteRulesRemainder.hs diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index ac19dfe651..f61487cf4d 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -389,6 +389,7 @@ logLevelToKoreLogEntryMap = [ "DebugAttemptedRewriteRules" , "DebugAppliedLabeledRewriteRule" , "DebugAppliedRewriteRules" + , "DebugRewriteRulesRemainder" , "DebugTerm" ] ) diff --git a/kore/kore.cabal b/kore/kore.cabal index 4037842519..d9dfa723f7 100644 --- a/kore/kore.cabal +++ b/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 diff --git a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs index b80deac92e..8aa8dc28f2 100644 --- a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs +++ b/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} diff --git a/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs b/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs new file mode 100644 index 0000000000..187b7bdfd9 --- /dev/null +++ b/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) diff --git a/kore/src/Kore/Log/Registry.hs b/kore/src/Kore/Log/Registry.hs index a3fc08f8d5..5b4c1cf5e6 100644 --- a/kore/src/Kore/Log/Registry.hs +++ b/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 diff --git a/kore/src/Kore/Rewrite/RewriteStep.hs b/kore/src/Kore/Rewrite/RewriteStep.hs index dcc67efbee..cbd7747123 100644 --- a/kore/src/Kore/Rewrite/RewriteStep.hs +++ b/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 diff --git a/kore/src/Log/Entry.hs b/kore/src/Log/Entry.hs index a9192835e2..f10ddbe012 100644 --- a/kore/src/Log/Entry.hs +++ b/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]