Skip to content

Commit 5b32b7b

Browse files
geo2ageo2a
authored
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"}]}]}}}}}} ```
1 parent 974ab83 commit 5b32b7b

File tree

7 files changed

+133
-2
lines changed

7 files changed

+133
-2
lines changed

‎booster/tools/booster/Server.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -389,6 +389,7 @@ logLevelToKoreLogEntryMap =
389389
[ "DebugAttemptedRewriteRules"
390390
, "DebugAppliedLabeledRewriteRule"
391391
, "DebugAppliedRewriteRules"
392+
, "DebugRewriteRulesRemainder"
392393
, "DebugTerm"
393394
]
394395
)

‎kore/kore.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -352,6 +352,7 @@ library
352352
Kore.Log.DebugRewriteTrace
353353
Kore.Log.DebugSolver
354354
Kore.Log.DebugSubstitutionSimplifier
355+
Kore.Log.DebugRewriteRulesRemainder
355356
Kore.Log.DebugTransition
356357
Kore.Log.DebugUnification
357358
Kore.Log.DebugUnifyBottom

‎kore/src/Kore/Log/DebugAppliedRewriteRules.hs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,8 @@ instance Entry DebugAppliedRewriteRules where
6767
| null appliedRewriteRules = True
6868
| otherwise = False
6969
oneLineDoc DebugAppliedRewriteRules{appliedRewriteRules}
70-
| null appliedRewriteRules = mempty
70+
| null appliedRewriteRules =
71+
"failed to apply " <> pretty (length appliedRewriteRules) <> " rewrite rules"
7172
| otherwise =
7273
"applied " <> pretty (length appliedRewriteRules) <> " rewrite rules"
7374
oneLineJson DebugAppliedRewriteRules{appliedRewriteRules}

‎kore/src/Kore/Log/DebugRewriteRulesRemainder.hs

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
{-# LANGUAGE RecordWildCards #-}
2+
{-# LANGUAGE NoStrict #-}
3+
{-# LANGUAGE NoStrictData #-}
4+
5+
{- |
6+
Copyright : (c) Runtime Verification, 2020-2021
7+
License : BSD-3-Clause
8+
-}
9+
module Kore.Log.DebugRewriteRulesRemainder (
10+
DebugRewriteRulesRemainder (..),
11+
debugRewriteRulesRemainder,
12+
) where
13+
14+
import Data.Aeson (Value (Array), object, toJSON, (.=))
15+
import Data.Text qualified as Text
16+
import Data.Vector (fromList)
17+
import Kore.Internal.Conditional qualified as Conditional
18+
import Kore.Internal.Pattern (
19+
Pattern,
20+
)
21+
import Kore.Internal.Predicate (
22+
Predicate,
23+
)
24+
import Kore.Internal.Predicate qualified as Predicate
25+
import Kore.Internal.TermLike qualified as TermLike
26+
import Kore.Internal.Variable (
27+
VariableName,
28+
toVariableName,
29+
)
30+
import Kore.Rewrite.RewritingVariable
31+
import Kore.Syntax.Json qualified as PatternJson
32+
import Kore.Unparser
33+
import Kore.Util (showHashHex)
34+
import Log
35+
import Prelude.Kore
36+
import Pretty (
37+
Pretty (..),
38+
)
39+
import Pretty qualified
40+
41+
{- This log entry will be emitted if, after unifying with rewrite rules,
42+
there is a satisfiable remainder condition -}
43+
data DebugRewriteRulesRemainder = DebugRewriteRulesRemainder
44+
{ configuration :: !(Pattern VariableName)
45+
-- ^ the state the rules unified with
46+
, rulesCount :: !Int
47+
-- ^ how many rules were unified
48+
, remainder :: !(Predicate RewritingVariableName)
49+
-- ^ the condition not covered by the rules
50+
}
51+
deriving stock (Show)
52+
53+
instance Pretty DebugRewriteRulesRemainder where
54+
pretty DebugRewriteRulesRemainder{..} =
55+
Pretty.vsep
56+
[ (Pretty.hsep . catMaybes)
57+
[ Just "The rules"
58+
, Just "produced a remainder"
59+
, Just . pretty $ remainder
60+
]
61+
, "On configuration:"
62+
, Pretty.indent 2 . unparse $ configuration
63+
]
64+
65+
instance Entry DebugRewriteRulesRemainder where
66+
entrySeverity _ = Debug
67+
helpDoc _ = "log rewrite rules remainder"
68+
69+
oneLineContextDoc
70+
DebugRewriteRulesRemainder{} = [remainderContextName]
71+
72+
oneLineContextJson
73+
DebugRewriteRulesRemainder{configuration, rulesCount} =
74+
Array $
75+
fromList
76+
[ toJSON remainderContextName
77+
, object
78+
[ "term" .= showHashHex (hash configuration)
79+
]
80+
, object
81+
[ "rules-count" .= Text.pack (show rulesCount)
82+
]
83+
]
84+
85+
oneLineDoc (DebugRewriteRulesRemainder{rulesCount, remainder}) =
86+
let context = [Pretty.brackets "detail"]
87+
logMsg =
88+
( Pretty.hsep
89+
[ "After applying "
90+
, pretty rulesCount
91+
, " rewrite rules"
92+
, "there is a satisfiable remainder condition: "
93+
, Pretty.group . pretty $ remainder
94+
]
95+
)
96+
in mconcat context <> logMsg
97+
98+
oneLineJson DebugRewriteRulesRemainder{remainder} =
99+
toJSON
100+
. PatternJson.fromPredicate sortBool
101+
. Predicate.mapVariables (pure toVariableName)
102+
$ remainder
103+
104+
remainderContextName :: Text.Text
105+
remainderContextName = "remainder"
106+
107+
sortBool :: TermLike.Sort
108+
sortBool =
109+
(TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
110+
111+
debugRewriteRulesRemainder ::
112+
MonadLog log =>
113+
Pattern RewritingVariableName ->
114+
Int ->
115+
Predicate RewritingVariableName ->
116+
log ()
117+
debugRewriteRulesRemainder pat rulesCount remainder =
118+
logEntry DebugRewriteRulesRemainder{..}
119+
where
120+
configuration = mapConditionalVariables TermLike.mapVariables pat
121+
mapConditionalVariables mapTermVariables =
122+
Conditional.mapVariables mapTermVariables (pure toVariableName)

‎kore/src/Kore/Log/Registry.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,9 @@ import Kore.Log.DebugProven (
6363
import Kore.Log.DebugRetrySolverQuery (
6464
DebugRetrySolverQuery,
6565
)
66+
import Kore.Log.DebugRewriteRulesRemainder (
67+
DebugRewriteRulesRemainder,
68+
)
6669
import Kore.Log.DebugRewriteTrace (
6770
DebugFinalPatterns,
6871
DebugInitialClaim,
@@ -229,6 +232,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
229232
, mk $ Proxy @DebugTransition
230233
, mk $ Proxy @DebugAppliedRewriteRules
231234
, mk $ Proxy @DebugAppliedLabeledRewriteRule
235+
, mk $ Proxy @DebugRewriteRulesRemainder
232236
, mk $ Proxy @DebugAttemptedRewriteRules
233237
, mk $ Proxy @DebugSubstitutionSimplifier
234238
, mk $ Proxy @WarnFunctionWithoutEvaluators

‎kore/src/Kore/Rewrite/RewriteStep.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ import Kore.Log.DebugAppliedRewriteRules (
4343
debugAppliedRewriteRules,
4444
)
4545
import Kore.Log.DebugCreatedSubstitution (debugCreatedSubstitution)
46+
import Kore.Log.DebugRewriteRulesRemainder (debugRewriteRulesRemainder)
4647
import Kore.Log.DebugRewriteTrace (
4748
debugRewriteTrace,
4849
)
@@ -323,6 +324,7 @@ finalizeRulesParallel
323324
-- NB: the UNKNOWN case will trigger an exception in SMT.evalPredicate, which will
324325
-- be caught by the top-level code in the RPC server and reported to the client
325326
_ -> do
327+
debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
326328
-- remainder condition is SAT: we are safe to explore
327329
-- the remainder branch, i.e. to evaluate the functions in the configuration
328330
-- with the remainder in the path condition and rewrite further

‎kore/src/Log/Entry.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ class (Show entry, Typeable entry) => Entry entry where
6666

6767
oneLineContextJson :: entry -> JSON.Value
6868
default oneLineContextJson :: entry -> JSON.Value
69-
oneLineContextJson _ = JSON.Array mempty
69+
oneLineContextJson entry = JSON.object ["entry" JSON..= entryTypeText (toEntry entry)]
7070

7171
oneLineContextDoc :: entry -> [Text]
7272
default oneLineContextDoc :: entry -> [Text]

0 commit comments

Comments
 (0)