Refactored to singleton logger by KlevisImeri · Pull Request #483 · ftsrg/theta

KlevisImeri · 2026-03-03T01:39:20Z

PR: Logger singleton

Read Logging.md

leventeBajczi

Thanks for the changes, I think these really help clear up the logging infrastructure of Theta!
I've skimmed through the changes, and these were my initial impressions. Please take a look -- but overall, I'm really happy with this PR.

leventeBajczi · 2026-03-04T08:09:21Z

Was this change deliberate?

I wrote this above in the pull request text:
Some other tests have been changes trying to fix issues which have to be reverted back like CFATest.

As mentioned this is "half pull" request. I just wanted to get an approval if turning it into a singleton is something desirable, so know I can spend more time fixing every detail and making ti nice.

leventeBajczi · 2026-03-04T08:11:24Z

+
+    @Parameter(
+            names = {"--grep", "-grep"},
+            description = "Log type pattern for the new logger API")


Saying "new" won't age well, just say "Log type pattern" -- also, add a line of documentation on its use with an example (either here as a comment, or in one of the doc markdown files)

Also, explicitly say that either this pattern, or -- if not given -- the loglevel takes effect, but never their conjunction.

leventeBajczi · 2026-03-04T08:14:10Z

    )
    if (expandingNode.state.isBottom()) {
-      logger.write(Logger.Level.VERBOSE, "Node is a dead end since its bottom%n")
+      Logger.verbose("Node is a dead end since its bottom%n")


if we're already changing this line, please fix the original typo (its -> it's / it is), even though I find the current literal meaning quite funny

leventeBajczi · 2026-03-04T08:19:03Z

I will need to take a closer look at this file. However, what I can already say, is that I don't like to see "yices" here -- that is very specific to one half-supported SMT solver. Can you give a reason why that is here, but no other solver is?

That is just me trying to use the logger and giving an example how I accept it to be used in the future. Yices is not special at all its just where I spend more time trying to find a workaround to the SSL expired certificate problem, and therefore I used the logger their more extensively so I can also use it as a concreate example. The main idea is that eventually every class will have a type. (and also subtypes with in the that class type, is a tree of types with "grep" used to query it).

Lets suppose that I want to get the logs inside the CegarChecker. I would put as type:

INFO_CEGARCHECKER -> create a func infoCegarChecker

MAINSTEP_CEGARCHECKER -> create a func mainstepCegarChecker

SUBSTEP_CEGARCHECKER -> create a func substepCegarChecker
when I initialize with Logger.init("MAINSTEP|SUBSTEP") I would have both the MAINSTEP_CEGARCHECKER, SUBSTEP_CEGARCHECKER (and all the other types that have a substring of MAINSTEP and SUBSTEP). But if I want only CEGARCHECKER then Logger.init("CEGARCHECKER") and it will show SUBSTEP_CEGARCHECKER, MAINSTEP_CEGARCHECKER and INFO_CEGARCHECKER.

Sorry I didn't do it justice explaining how it works. I will have to write better docs.

So, familiarizing myself with the logger, the main idea is that you have a more complex filtering than just a few levels of increasing verbosity. I think the filtering side (how you use --grep) is mostly clear to me.

My question is rather about how and where the possible values that are filtered are defined.

Here is what I understand about that:
I see the logTypes in the logger. I see that level is passed as a string to the log method and I see the enabled set. I can see that enabled just contains all matches of logTypes to the regex from --grep.

I think what Levi did not like (or will not like? :D ) is that someone implementing something new - let's say a new checker - will have to think about adding stuff in the logger. So the logger becomes cluttered with information from literally everywhere in Theta, and logTypes becomes huge.

I did not fully think the solution through, but I think there are roughly two directions:

the central logTypes collection of all the log types is avoided and these values should be distributed, e.g., per class/per file. Something like STMT_LABELs and things like that - an extra "utility" constant. Pro: if I develop a new checker, I just add a constant or two and I instantly have a working, customized logger; (BIG) Con: extra constant value in practically every file

I think the other solution is to just keep logTypes, expect it to be huge and try to make that usable and maintainable - put it in it's own file and somehow make it foolproof in a way so that I don't forget to add my new log values to the new log checker

Also, the question is: how much do we plan to fill up logTypes right now? Do we want to 1) go through a lot of places and add a lot of custom log types OR 2) do we do it gradually - e.g., you add what you needed (yices, cegar, whatever) and the next person who needs it elsewhere, say IC3, can add it there. I would prefer the latter - just with some really well shown / highlighted doc, so that people know that they can do this?

(I'm curious about everyone's and anyone's input on this.)

leventeBajczi · 2026-03-04T08:28:54Z

        dataInitPrec,
        Z3LegacySolverFactory.getInstance(),
-        logger,
+        Logger,


Why pass it here at all? (this is also relevant for all other tests here)

Mainly I don't understand why some places had their logger parameters removed, and then here some just receive the singleton object. I think we should opt for one of these solutions.

I will eventually fix all those places. There are a lot of shortcuts I took. And I also have to do a better review myself. The main point was if the this type of "Logger API" is preferred,

KlevisImeri · 2026-03-04T09:26:10Z

Thanks for the changes, I think these really help clear up the logging infrastructure of Theta! I've skimmed through the changes, and these were my initial impressions. Please take a look -- but overall, I'm really happy with this PR.

This PR is barely finished I just wanted a review if the API is nice and fits theta's ecosystem and mindset.
If happy with the idea then I will fix every detail and have a complete nice PR, cause this one has a lot of "leftovers" which have to be cleaned up.
And also thank you for the review!

mondokm · 2026-03-04T15:55:17Z

Thank you for the PR, this is something that was needed for a while now:D

Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum
"LegacyLevel"
"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

mondokm · 2026-03-04T15:59:53Z

Thank you for the PR, this is something that was needed for a while now:D

Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum

"LegacyLevel"

"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

Also I think it would be better to arrive on one option instead of having "grep", "log" and "loglevel" on the CLI interfaces. We have proper versioning, so we don't necessarily have to stick to older CLI parameters.

AdamZsofi · 2026-03-04T20:36:17Z

Thank you for the PR, this is something that was needed for a while now:D
Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum

"LegacyLevel"

"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

Also I think it would be better to arrive on one option instead of having "grep", "log" and "loglevel" on the CLI interfaces. We have proper versioning, so we don't necessarily have to stick to older CLI parameters.

Maybe it's just nostalgia, but I would vouch to keep the current loglevel flag. :D But I agree that we should only have one flag. If it can do complex regex expressions then it can do simple ones as well, so maybe with a different syntax, but it can still express what the old levels expressed.

And I agree about being able to change the flag syntax due to versioning.

KlevisImeri · 2026-03-05T09:16:22Z

@AdamZsofi To implement the Legacy (old flags) I just translated them to the appropriate regex expressions for the "grep" API.

…disable support - Replace multiple Logger classes (BaseLogger, ConsoleLogger, FileLogger, NullLogger, UniqueWarningLogger) with a single Kotlin object Logger - Add Logger.enabled.kt / Logger.disabled.kt templates for compile-time logging toggle via -PnoLogging - Make Level enum public, remove isEnabled(String) overload - Update all call sites across analysis algorithms, CLI tools, tests, and solver installers to use the new Logger API - Fix corrupted StsMddCheckerTest.java (missing block comment opener) - Remove stale bin/.gitignore files - Add Logging.md documentation

KlevisImeri · 2026-04-07T01:50:00Z

I finished refactoring all the logger to a singleton:

Removed the legacy API completely
Wrote the Logging.md documentation
Refactored parts that the logger was beings passed as function parameter
Clean any bad leftovers from debugging.
Reviewed the whole pull request one more time.
Added the -PnoLogging build time flag so we can build with 0 logging overhead.

Another important thing is that I could see .gitignore files inside the **/bin/ i removed them from there and adde bin in the root .gitignore.

Refactored to the singleton logger but still some solver issues in tests

db5f0c3

AdamZsofi self-assigned this Mar 3, 2026

KlevisImeri marked this pull request as draft March 3, 2026 14:25

leventeBajczi reviewed Mar 4, 2026

View reviewed changes

KlevisImeri added 2 commits April 6, 2026 19:25

Merge master into refactor/singleton-logger

8e349ae

KlevisImeri marked this pull request as ready for review April 7, 2026 01:56

Conversation

KlevisImeri commented Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR: Logger singleton

Uh oh!

leventeBajczi left a comment

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!

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!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri Mar 4, 2026 • 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!

AdamZsofi Mar 4, 2026 • 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!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri commented Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mondokm commented Mar 4, 2026

Uh oh!

mondokm commented Mar 4, 2026

Uh oh!

AdamZsofi commented Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

KlevisImeri commented Mar 5, 2026

Uh oh!

KlevisImeri commented Apr 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

KlevisImeri commented Mar 3, 2026 •

edited

Loading

KlevisImeri Mar 4, 2026 •

edited

Loading

AdamZsofi Mar 4, 2026 •

edited

Loading

KlevisImeri commented Mar 4, 2026 •

edited

Loading

AdamZsofi commented Mar 4, 2026 •

edited

Loading

KlevisImeri commented Apr 7, 2026 •

edited

Loading