JSON logging cleanup #3881

goodlyrottenapple · 2024-05-20T15:41:54Z

Re-add the test-log-simplify-json rpc test with a much smaller footprint, as we want to just track the context logging format
Clean up the equation contexts a bit in booster, as we weren't consistently logging messages around functions/equations
Closes Context Logging: Shortcut options to select common context log subsets #3864 by adding a conversion from the old custom log levels to contextual log filters.
Closes Context logging: Migrate and clean up obsolete log levels #3866 by removing the SimplifyJson log level which has been replaced by -l Simplify --log-format json

…ptures the simplification context logs in JSON

geo2a · 2024-05-21T05:34:00Z

booster/library/Booster/Pattern/ApplyEquations.hs

        emitEquationTrace term eq.attributes.location eq.attributes.ruleLabel eq.attributes.uniqueId res
        handler
-            (\t -> setChanged >> pure t)
+            ( \t -> setChanged >> (withContext (LogContext eq) $ withContext "success" $ withTermContext t $ pure t)


I like this change. I think it fixes a bug in logging that I've found but haven't got to report yet.
The bug was that we would not emit 'success' messages for individual equations, and instead only emit a single 'success' message at the very end after attempting/applying all equations.

booster/test/rpc-integration/test-log-simplify-json/README.md

…log options

goodlyrottenapple · 2024-05-21T14:35:59Z

scripts/booster-integration-tests.sh

+        "log-simplify-json")
+            SERVER="${KORE_RPC_BOOSTER} --log-format json -l Simplify --log-file test-$name/simplify-log.txt" ./runDirectoryTest.sh test-$name $@
+            ;;


made several changes here, including adding the conversion from the original custom log levels tot he context filtering. Also renamed --simplification-log-file to just --log-file

goodlyrottenapple · 2024-05-21T14:36:55Z

booster/library/Booster/CLOptions.hs

    , ("SimplifyKore", "Log all simplification in kore-rpc")
    , ("SimplifySuccess", "Log successful simplifications (booster and kore-rpc)")
    , ("Depth", "Log the current depth of the state")
    , ("SMT", "Log the SMT-solver interactions")
    , ("ErrorDetails", "Log error conditions with extensive details")
    ]

+levelToContext :: Map Text [ContextFilter]


here are some of the common log filter we may want. Let me know if you think we should add any other ones

geo2a · 2024-05-21T14:49:28Z

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -860,13 +808,15 @@ applyEquations theory handler term = do
    processEquations [] =
        pure term -- nothing to do, term stays the same
    processEquations (eq : rest) = do
-        res <- applyEquation term eq
+        res <- withRuleContext eq $ applyEquation term eq
        emitEquationTrace term eq.attributes.location eq.attributes.ruleLabel eq.attributes.uniqueId res


Now that -l SImplify is re-implemented through the contextual logging, and the simplification RPC traces are to be remove in a pending PR, we are fee to drop the calls to emitEquationTrace, and the function itself too.

I was going to leave that for another pr, because we actually still log via the old logger interface within this function. Until we migrate our tools to contextual logging these may still be necessary?

Sounds good, let's keep it for now.

booster/test/rpc-integration/test-log-simplify-json/README.md

jberthold

From the comment about emitEquationTrace , I understand that you planned to follow up with another PR? Then we can merge this and leave the following to the next iteration:

There is some (more) dead code left to clean up
The context-log replacement for -l Aborts needs some more attention
Generally we should remove all old-style customLevels that have a replacement. This probably means removing most levels, except the Abort one as it is now. Once that is addressed, the levelFilter can just handle the standard Error,Warn,Info levels (but we should rather remove those, too).

jberthold · 2024-05-22T01:30:06Z

booster/library/Booster/CLOptions.hs

+            ( "Aborts"
+            ,
+                [ [ctxt| booster|kore>match,abort |]
+                ]
+            )


-l Aborts does something different than log aborted matching, it reports any condition that leads to an aborted result:

uncertain match

uncertain conditions

match of a rule that might not preserve definedness

In addition, it outputs the diff before and after kore-rpc simplification in (internal and external) simplify requests.

We could introduce an extra thing for the diff (there is no rigid use case for it), but we should make sure the logs for aborted rewrites have the same information as before so we can use them in the analysis script.

jberthold · 2024-05-22T01:35:28Z

booster/library/Booster/CLOptions.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE QuasiQuotes #-}


booster/library/Booster/CLOptions.hs

jberthold · 2024-05-22T01:50:52Z

booster/tools/booster/Server.hs

 logLevelToKoreLogEntryMap =
    Map.fromList
        [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugTerm"])
-        , (LevelOther "SimplifyJson", ["DebugAttemptEquation", "DebugTerm"])


I think this is dead code. kore-rpc-dev has another copy of it which is still used (maybe not for a good reason, though?)

we still need to pass these (e.g. DebugAttemptEquation) to actually get context logging in the old backend, because it has multiple layers of filtering. We could just enable all of them tho...

jberthold · 2024-05-22T01:54:12Z

dev-tools/kore-rpc-dev/Server.hs

-getKoreEntriesForLevel :: LogLevel -> [Text.Text]
-getKoreEntriesForLevel level = concat . maybeToList $ Map.lookup level logLevelToKoreLogEntryMap
-


This probably makes the logLevelToKoreLogEntryMap dead code here, too.

scripts/booster-integration-tests.sh

Co-authored-by: Georgy Lukyanov <[email protected]>

goodlyrottenapple and others added 6 commits May 20, 2024 16:38

re-add a simpler rpc-integration/test-log-simplify-json test which ca…

0d280f0

…ptures the simplification context logs in JSON

update README

f406df9

Format with fourmolu

6153007

remove simplify-log.txt

790d638

update golden file

8be7db1

Merge branch 'master' into sam/json-logging-rpc-test

902e6c4

geo2a reviewed May 21, 2024

View reviewed changes

booster/test/rpc-integration/test-log-simplify-json/README.md Outdated Show resolved Hide resolved

goodlyrottenapple added 2 commits May 21, 2024 15:33

add log level to context filter conversions to bridge the old an new …

f59f7c7

…log options

Merge branch 'master' into sam/json-logging-rpc-test

502105f

goodlyrottenapple commented May 21, 2024

View reviewed changes

goodlyrottenapple marked this pull request as ready for review May 21, 2024 14:37

goodlyrottenapple requested review from geo2a and jberthold May 21, 2024 14:41

add SMT log to copntext log translation

e17ae96

geo2a reviewed May 21, 2024

View reviewed changes

booster/test/rpc-integration/test-log-simplify-json/README.md Outdated Show resolved Hide resolved

geo2a approved these changes May 21, 2024

View reviewed changes

jberthold approved these changes May 22, 2024

View reviewed changes

goodlyrottenapple and others added 5 commits May 22, 2024 10:14

Update booster/test/rpc-integration/test-log-simplify-json/README.md

db0ecf5

Co-authored-by: Georgy Lukyanov <[email protected]>

merge master

a6aabe8

misc fixes

3bf79a0

remove aborts for now

6e8a3da

Merge branch 'master' into sam/json-logging-rpc-test

acbf129

goodlyrottenapple merged commit e62fba2 into master May 22, 2024
7 checks passed

goodlyrottenapple deleted the sam/json-logging-rpc-test branch May 22, 2024 13:22

geo2a mentioned this pull request May 24, 2024

Create a minimal test for the JSON simplification logging #3830

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

JSON logging cleanup #3881

JSON logging cleanup #3881

Uh oh!

goodlyrottenapple commented May 20, 2024 •

edited

Loading

Uh oh!

geo2a May 21, 2024

Uh oh!

Uh oh!

goodlyrottenapple May 21, 2024

Uh oh!

goodlyrottenapple May 21, 2024

Uh oh!

geo2a May 21, 2024 •

edited

Loading

Uh oh!

goodlyrottenapple May 21, 2024

Uh oh!

geo2a May 21, 2024

Uh oh!

Uh oh!

jberthold left a comment

Uh oh!

jberthold May 22, 2024 •

edited

Loading

Uh oh!

jberthold May 22, 2024

Uh oh!

Uh oh!

jberthold May 22, 2024

Uh oh!

goodlyrottenapple May 22, 2024

Uh oh!

jberthold May 22, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

		getKoreEntriesForLevel :: LogLevel -> [Text.Text]
		getKoreEntriesForLevel level = concat . maybeToList $ Map.lookup level logLevelToKoreLogEntryMap

JSON logging cleanup #3881

JSON logging cleanup #3881

Uh oh!

Conversation

goodlyrottenapple commented May 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

geo2a May 21, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

jberthold May 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

goodlyrottenapple commented May 20, 2024 •

edited

Loading

geo2a May 21, 2024 •

edited

Loading

jberthold May 22, 2024 •

edited

Loading