Skip to content

Commit 98d840f

Browse files
geo2ageo2a
committed
Merge branch 'georgy/kore-context-logging' into georgy/better-kore-logging
2 parents ec980ea + d048a2a commit 98d840f

File tree

13 files changed

+205
-66
lines changed

13 files changed

+205
-66
lines changed

‎kore/app/rpc/Main.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ import Kore.Log (
3434
LoggerT,
3535
logInfo,
3636
parseKoreLogOptions,
37-
runKoreLogThreadSafe,
37+
runKoreLogThreadSafeLegacy,
3838
)
3939
import Kore.Log.ErrorException (
4040
handleSomeException,
@@ -149,7 +149,7 @@ mainWithOptions
149149
koreRpcServerRun localOptions
150150
& handleJust isInterrupt handleInterrupt
151151
& handle handleSomeException
152-
& runKoreLogThreadSafe
152+
& runKoreLogThreadSafeLegacy
153153
tmpDir
154154
koreLogOptions
155155
)

‎kore/kore.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -369,6 +369,7 @@ library
369369
Kore.Log.ErrorRewritesInstantiation
370370
Kore.Log.ErrorVerify
371371
Kore.Log.DebugAttemptUnification
372+
Kore.Log.DebugContext
372373
Kore.Log.JsonRpc
373374
Kore.Log.InfoExecBreadth
374375
Kore.Log.InfoExecDepth

‎kore/src/Kore/Equation/DebugEquation.hs

Lines changed: 54 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,8 @@ import Data.Aeson qualified as JSON
3232
import Data.Text (
3333
Text,
3434
)
35-
3635
import Data.Text qualified as Text
36+
import Data.Word (Word64)
3737
import Debug
3838
import GHC.Generics qualified as GHC
3939
import Generics.SOP qualified as SOP
@@ -62,6 +62,7 @@ import Kore.Rewrite.RewritingVariable (
6262
)
6363
import Kore.Unparser (Unparse (..))
6464
import Log
65+
import Numeric (showHex)
6566
import Prelude.Kore
6667
import Pretty (Pretty (..))
6768
import Pretty qualified
@@ -255,6 +256,31 @@ instance Pretty DebugAttemptEquation where
255256
pretty (DebugAttemptEquationResult _ (Right _)) =
256257
"equation is applicable"
257258

259+
isSimplification :: Equation a -> Bool
260+
isSimplification (Equation{attributes}) =
261+
case Attribute.simplification attributes of
262+
Attribute.IsSimplification{} -> True
263+
Attribute.NotSimplification -> False
264+
265+
failureDescription :: AttemptEquationError RewritingVariableName -> Text
266+
failureDescription err = shorten . Pretty.renderText . Pretty.layoutOneLine . Pretty.pretty $ err
267+
where
268+
shorten :: Text -> Text
269+
shorten msg =
270+
let cutoff = 500
271+
in if Text.length msg > cutoff then Text.take 500 msg <> ("...truncated" :: Text) else msg
272+
273+
showHashHex :: Int -> Text
274+
showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ Text.pack $ showHex w64 ""
275+
276+
ruleIdText :: Equation a -> Text
277+
ruleIdText equation =
278+
shortenRuleId $
279+
fromMaybe "UNKNOWN" (Attribute.getUniqueId . Attribute.uniqueId . attributes $ equation)
280+
where
281+
shortenRuleId :: Text -> Text
282+
shortenRuleId msg = Text.take 8 msg
283+
258284
instance Entry DebugAttemptEquation where
259285
entrySeverity _ = Debug
260286
contextDoc (DebugAttemptEquation equation _) =
@@ -264,47 +290,59 @@ instance Entry DebugAttemptEquation where
264290
, (\loc -> Pretty.hsep ["at", pretty loc]) <$> srcLoc equation
265291
]
266292
contextDoc _ = Nothing
293+
267294
helpDoc _ = "log equation application attempts"
268-
oneLineDoc (DebugAttemptEquation equation _) =
295+
296+
oneLineContextDoc = \case
297+
_entry@(DebugAttemptEquation equation term) ->
298+
let equationKindTxt = if isSimplification equation then "simplification" else "function"
299+
in [ Pretty.hsep ["term", Pretty.pretty . showHashHex $ hash term]
300+
, Pretty.hsep . map Pretty.pretty $ [equationKindTxt, ruleIdText equation]
301+
]
302+
(DebugAttemptEquationResult _ result) -> case result of
303+
Right{} -> ["success"]
304+
Left failure -> ["failure", Pretty.pretty $ failureDescription failure]
305+
306+
oneLineDoc (DebugAttemptEquation equation term) =
269307
maybe
270308
mempty
271-
(\loc -> Pretty.hsep ["applying equation at", pretty loc])
309+
( \loc ->
310+
Pretty.hsep . concat $
311+
[ ["[detail]"]
312+
, ["applying equation", Pretty.pretty (ruleIdText equation)]
313+
, ["at", pretty loc]
314+
, ["to term", Pretty.pretty . showHashHex $ hash term, unparse term]
315+
]
316+
)
272317
(srcLoc equation)
273-
oneLineDoc (DebugAttemptEquationResult _ (Left _)) = "equation is not applicable"
274-
oneLineDoc (DebugAttemptEquationResult _ (Right _)) = "equation is applicable"
318+
oneLineDoc (DebugAttemptEquationResult _ result) = case result of
319+
Right{} -> Pretty.brackets "success"
320+
Left failure -> Pretty.hsep [Pretty.brackets "failure", Pretty.pretty $ failureDescription failure]
275321

276322
oneLineJson = \case
277323
entry@(DebugAttemptEquation equation _) ->
278324
JSON.object
279325
[ "tag" JSON..= entryTypeText (toEntry entry)
280326
, "rule-id"
281-
JSON..= fromMaybe "UNKNOWN" (Attribute.getUniqueId . Attribute.uniqueId . attributes $ equation)
327+
JSON..= ruleIdText equation
282328
]
283329
_entry@(DebugAttemptEquationResult equation result) ->
284330
let resultInfo = case result of
285331
Right _ ->
286332
JSON.object
287333
[ "tag" JSON..= ("success" :: Text)
288-
, "rule-id" JSON..= ruleIdText
334+
, "rule-id" JSON..= ruleIdText equation
289335
]
290336
Left failure ->
291337
JSON.object
292338
[ "tag" JSON..= ("failure" :: Text)
293-
, "rule-id" JSON..= ruleIdText
339+
, "rule-id" JSON..= ruleIdText equation
294340
, "reason" JSON..= failureDescription failure
295341
]
296342
in JSON.object
297343
[ "tag" JSON..= ("simplification" :: Text)
298344
, "result" JSON..= resultInfo
299345
]
300-
where
301-
failureDescription :: AttemptEquationError RewritingVariableName -> Text
302-
failureDescription err = shortenText . Pretty.renderText . Pretty.layoutOneLine . Pretty.pretty $ err
303-
304-
shortenText :: Text -> Text
305-
shortenText msg = Text.take 500 msg <> ("...truncated" :: Text)
306-
307-
ruleIdText = fromMaybe "UNKNOWN" (Attribute.getUniqueId . Attribute.uniqueId . attributes $ equation)
308346

309347
-- | Log the result of attempting to apply an 'Equation'.
310348
debugAttemptEquationResult ::

‎kore/src/Kore/JsonRpc.hs

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ import Kore.JsonRpc.Server (
6363
)
6464
import Kore.JsonRpc.Types
6565
import Kore.JsonRpc.Types.Log
66+
import Kore.Log.DebugContext qualified as Log
6667
import Kore.Log.DecidePredicateUnknown (
6768
DecidePredicateUnknown (..),
6869
externaliseDecidePredicateUnknown,
@@ -161,21 +162,22 @@ respond serverState moduleName runSMT =
161162
traversalResult <-
162163
liftIO
163164
( runSMT (Exec.metadataTools serializedModule) lemmas $
164-
Exec.rpcExec
165-
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
166-
(coerce stepTimeout)
167-
( if fromMaybe False movingAverageStepTimeout
168-
then EnableMovingAverage
169-
else DisableMovingAverage
170-
)
171-
( if fromMaybe False assumeStateDefined
172-
then EnableAssumeInitialDefined
173-
else DisableAssumeInitialDefined
174-
)
175-
tracingEnabled
176-
serializedModule
177-
(toStopLabels cutPointRules terminalRules)
178-
verifiedPattern
165+
Log.logWhile (Log.DebugContext "execute") $
166+
Exec.rpcExec
167+
(maybe Unlimited (\(Depth n) -> Limit n) maxDepth)
168+
(coerce stepTimeout)
169+
( if fromMaybe False movingAverageStepTimeout
170+
then EnableMovingAverage
171+
else DisableMovingAverage
172+
)
173+
( if fromMaybe False assumeStateDefined
174+
then EnableAssumeInitialDefined
175+
else DisableAssumeInitialDefined
176+
)
177+
tracingEnabled
178+
serializedModule
179+
(toStopLabels cutPointRules terminalRules)
180+
verifiedPattern
179181
)
180182

181183
stop <- liftIO $ getTime Monotonic
@@ -437,6 +439,7 @@ respond serverState moduleName runSMT =
437439
(logs, result) <-
438440
liftIO
439441
. runSMT (Exec.metadataTools serializedModule) lemmas
442+
. Log.logWhile (Log.DebugContext "implies")
440443
. (evalInSimplifierContext (fromMaybe False logSuccessfulSimplifications) serializedModule)
441444
. runExceptT
442445
$ Claim.checkSimpleImplication
@@ -520,6 +523,7 @@ respond serverState moduleName runSMT =
520523
(logs, result) <-
521524
liftIO
522525
. runSMT (Exec.metadataTools serializedModule) lemmas
526+
. Log.logWhile (Log.DebugContext "simplify")
523527
. evalInSimplifierContext (fromMaybe False logSuccessfulSimplifications) serializedModule
524528
$ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt
525529

@@ -616,6 +620,7 @@ respond serverState moduleName runSMT =
616620
serializedModule <-
617621
liftIO
618622
. runSMT metadataTools lemmas
623+
. Log.logWhile (Log.DebugContext "add-module")
619624
$ Exec.makeSerializedModule newModule
620625
internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache
621626

@@ -674,6 +679,7 @@ respond serverState moduleName runSMT =
674679
else
675680
liftIO
676681
. runSMT tools lemmas
682+
. Log.logWhile (Log.DebugContext "get-model")
677683
. SMT.Evaluator.getModelFor tools
678684
$ NonEmpty.fromList preds
679685

‎kore/src/Kore/Log.hs

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module Kore.Log (
1515
Colog.logTextStderr,
1616
Colog.logTextHandle,
1717
runKoreLog,
18-
runKoreLogThreadSafe,
18+
runKoreLogThreadSafeLegacy,
1919
WithTimestamp (..),
2020
withTimestamp,
2121
withSmtSolverLogger,
@@ -241,13 +241,21 @@ runKoreLog reportDirectory options loggerT =
241241
withLoggerLegacy reportDirectory options $ runLoggerT loggerT
242242

243243
-- | Run a 'LoggerT' with the given options, using `swappableLogger` to make it thread safe.
244-
runKoreLogThreadSafe :: FilePath -> KoreLogOptions -> LoggerT IO a -> IO a
245-
runKoreLogThreadSafe reportDirectory options loggerT =
244+
runKoreLogThreadSafeLegacy :: FilePath -> KoreLogOptions -> LoggerT IO a -> IO a
245+
runKoreLogThreadSafeLegacy reportDirectory options loggerT =
246246
withLoggerLegacy reportDirectory options $ \actualLogAction -> do
247247
mvarLogAction <- newMVar actualLogAction
248248
let swapLogAction = swappableLogger mvarLogAction
249249
runLoggerT loggerT swapLogAction
250250

251+
-- -- | Run a 'LoggerT' with the given options, using `swappableLogger` to make it thread safe.
252+
-- runKoreLogThreadSafe :: KoreLogOptions -> LoggerT IO a -> IO a
253+
-- runKoreLogThreadSafe options loggerT =
254+
-- withLogger options $ \actualLogAction -> do
255+
-- mvarLogAction <- newMVar actualLogAction
256+
-- let swapLogAction = swappableLogger mvarLogAction
257+
-- runLoggerT loggerT swapLogAction
258+
251259
{- | The default Kore logger used by the legacy backend.
252260
253261
Creates a kore logger which:

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,7 @@ instance Pretty DebugAppliedRewriteRules where
6060
instance Entry DebugAppliedRewriteRules where
6161
entrySeverity _ = Debug
6262
helpDoc _ = "log applied rewrite rules"
63-
oneLineDoc DebugAppliedRewriteRules{appliedRewriteRules} =
64-
Pretty.hsep $ pretty <$> appliedRewriteRules
63+
oneLineDoc (DebugAppliedRewriteRules{}) = "success"
6564

6665
debugAppliedRewriteRules ::
6766
MonadLog log =>
@@ -105,7 +104,7 @@ instance Pretty DebugAppliedLabeledRewriteRule where
105104
instance Entry DebugAppliedLabeledRewriteRule where
106105
entrySeverity _ = Debug
107106
helpDoc _ = "log applied rewrite rule with label"
108-
oneLineDoc DebugAppliedLabeledRewriteRule{sourceLocation} = pretty sourceLocation
107+
oneLineDoc (DebugAppliedLabeledRewriteRule{}) = "[success]"
109108

110109
debugAppliedLabeledRewriteRule ::
111110
MonadLog log =>

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ instance Entry DebugAttemptUnification where
3838
entrySeverity _ = Debug
3939
contextDoc _ = Just "while attempting unification"
4040
oneLineDoc _ = "DebugAttemptUnification"
41+
oneLineContextDoc _ = ["unify"]
4142
helpDoc _ = "log unification attempts"
4243

4344
instance Pretty DebugAttemptUnification where

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

Lines changed: 50 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,15 @@ License : BSD-3-Clause
99
module Kore.Log.DebugAttemptedRewriteRules (
1010
DebugAttemptedRewriteRules (..),
1111
debugAttemptedRewriteRule,
12+
whileDebugAttemptRewriteRule,
1213
) where
1314

1415
import Data.Text (Text)
16+
import Data.Text qualified as Text
17+
import Data.Word (Word64)
1518
import Kore.Attribute.Axiom (
1619
SourceLocation,
20+
UniqueId (..),
1721
)
1822
import Kore.Internal.Conditional qualified as Conditional
1923
import Kore.Internal.Pattern (
@@ -27,6 +31,7 @@ import Kore.Internal.Variable (
2731
import Kore.Rewrite.RewritingVariable
2832
import Kore.Unparser
2933
import Log
34+
import Numeric (showHex)
3035
import Prelude.Kore
3136
import Pretty (
3237
Pretty (..),
@@ -35,6 +40,7 @@ import Pretty qualified
3540

3641
data DebugAttemptedRewriteRules = DebugAttemptedRewriteRules
3742
{ configuration :: !(Pattern VariableName)
43+
, ruleId :: !UniqueId
3844
, label :: !(Maybe Text)
3945
, attemptedRewriteRule :: !SourceLocation
4046
}
@@ -53,19 +59,60 @@ instance Pretty DebugAttemptedRewriteRules where
5359
, Pretty.indent 2 . unparse $ configuration
5460
]
5561

62+
showHashHex :: Int -> Text
63+
showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ Text.pack $ showHex w64 ""
64+
65+
shortenRuleId :: Text -> Text
66+
shortenRuleId msg = Text.take 8 msg
67+
68+
shortRuleIdTxt :: UniqueId -> Text
69+
shortRuleIdTxt = shortenRuleId . fromMaybe "UNKNWON" . getUniqueId
70+
5671
instance Entry DebugAttemptedRewriteRules where
5772
entrySeverity _ = Debug
5873
helpDoc _ = "log attempted rewrite rules"
59-
oneLineDoc DebugAttemptedRewriteRules{attemptedRewriteRule} =
60-
pretty attemptedRewriteRule
74+
75+
oneLineContextDoc = \case
76+
(DebugAttemptedRewriteRules{configuration, ruleId, label}) ->
77+
[ Pretty.hsep ["term", Pretty.pretty . showHashHex $ hash configuration]
78+
, Pretty.hsep . map Pretty.pretty $
79+
["rewrite", shortRuleIdTxt ruleId, fromMaybe "" label]
80+
]
81+
82+
oneLineDoc entry@(DebugAttemptedRewriteRules{configuration, label, ruleId, attemptedRewriteRule}) =
83+
let context = map Pretty.brackets (oneLineContextDoc entry <> ["detail"])
84+
logMsg =
85+
( Pretty.hsep . concat $
86+
[ ["attempting to apply rewrite rule", Pretty.pretty (shortRuleIdTxt ruleId), Pretty.pretty label]
87+
, ["at", Pretty.pretty attemptedRewriteRule]
88+
, ["to term", Pretty.pretty . showHashHex $ hash configuration, Pretty.group $ unparse configuration]
89+
]
90+
)
91+
in mconcat context <> logMsg
92+
93+
whileDebugAttemptRewriteRule ::
94+
MonadLog log =>
95+
Pattern RewritingVariableName ->
96+
UniqueId ->
97+
Maybe Text ->
98+
SourceLocation ->
99+
log a ->
100+
log a
101+
whileDebugAttemptRewriteRule initial ruleId label attemptedRewriteRule =
102+
logWhile (DebugAttemptedRewriteRules{..})
103+
where
104+
configuration = mapConditionalVariables TermLike.mapVariables initial
105+
mapConditionalVariables mapTermVariables =
106+
Conditional.mapVariables mapTermVariables (pure toVariableName)
61107

62108
debugAttemptedRewriteRule ::
63109
MonadLog log =>
64110
Pattern RewritingVariableName ->
111+
UniqueId ->
65112
Maybe Text ->
66113
SourceLocation ->
67114
log ()
68-
debugAttemptedRewriteRule initial label attemptedRewriteRule =
115+
debugAttemptedRewriteRule initial ruleId label attemptedRewriteRule =
69116
logEntry DebugAttemptedRewriteRules{..}
70117
where
71118
configuration = mapConditionalVariables TermLike.mapVariables initial

0 commit comments

Comments
 (0)