Skip to content

Refactored to singleton logger #483

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
KlevisImeri wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Refactored to singleton logger #483

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
db5f0c3
Refactored to the singleton logger but still some solver issues in tests
KlevisImeri Mar 3, 2026
8e349ae
Merge master into refactor/singleton-logger
KlevisImeri Apr 6, 2026
1cc8a7a
Refactor logging system to singleton Logger object with compile-time …
KlevisImeri Apr 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ hs_err_pid*

.gradle/
build/
bin/
dest/

# Eclipse
Expand Down
7 changes: 7 additions & 0 deletions doc/Coding-conventions.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,13 @@ See [Build.md](Build.md). For the formatting rules, check [java-common.gradle.kt
* **AVOID** platform specific constructs. For example, prefer `System.lineSeparator()` over `\r\n` or `\n`.
* **CONSIDER** using `getClass().getSimpleName()` to print the name of a class in its `toString()`. This way, if the class is renamed, `toString()` will also adapt.

## Loggin
* **DO** use the singleton `Logger` for all logging (e.g., `Logger.info(...)`, `Logger.mainStep(...)`).
* **DO** use `*Once` variants (`warnOnce`, `infoOnce`, `errorOnce`) for messages that should only appear once.
* **DO NOT** use `System.out.println` or `System.err.println` for logging.

For details, see [Logging.md](Logging.md).

# References

1. Joshua Bloch: Effective Java (2nd edition)
Expand Down
122 changes: 122 additions & 0 deletions doc/Logging.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,122 @@
# Logging

Theta uses a singleton `Logger` object for all logging. It is defined in the `hu.bme.mit.theta.common.logging` package.

## Initialization

`Logger.init()` must be called once before any logging. It accepts a case-insensitive regex pattern that selects which log levels to enable.

```java
Logger.init("ERROR|WARN|RESULT|BENCHMARK|MAINSTEP|SUBSTEP");
```

To enable all log levels, use the `Logger.ALL` constant:

```java
Logger.init(Logger.ALL);
```

By default, output goes to stderr. To log to a file instead:

```java
Logger.init("ERROR|WARN|INFO", "/path/to/logfile.log");
```

## Log Levels

| Method | Level Name | Use Case |
|--------|-----------|----------|
| `Logger.error(...)` | ERROR | Errors and failures |
| `Logger.errorOnce(...)` | ERROR | Errors that should only appear once |
| `Logger.warn(...)` | WARN | Warnings |
| `Logger.warnOnce(...)` | WARN | Warnings that should only appear once |
| `Logger.result(...)` | RESULT | Final verification results |
| `Logger.benchmark(...)` | BENCHMARK | Timing and performance metrics |
| `Logger.mainStep(...)` | MAINSTEP | Major algorithm steps (e.g., CEGAR iterations) |
| `Logger.subStep(...)` | SUBSTEP | Sub-steps within a major step |
| `Logger.info(...)` | INFO | General information |
| `Logger.infoOnce(...)` | INFO | Information that should only appear once |
| `Logger.detail(...)` | DETAIL | Detailed information |
| `Logger.verbose(...)` | VERBOSE | Verbose output |
| `Logger.solverDebug(...)` | DEBUG_SOLVER | Solver communication debug |
| `Logger.debug(...)` | DEBUG | General debug output |

## Formatting

All log methods accept printf-style format strings:

```java
Logger.info("Found %d items in %s", count, name);
Logger.mainStep("Starting iteration %d", iteration);
```

For messages without arguments, the format string is used directly without `String.format` overhead:

```java
Logger.info("Starting analysis");
```

## *Once Variants

`warnOnce`, `infoOnce`, and `errorOnce` deduplicate messages. The same formatted message is only logged once per session, regardless of how many times the method is called.

```java
Logger.warnOnce("Unsupported feature X in %s", file);
```

This is useful for warnings inside loops or frequently called methods where the same warning would otherwise be repeated many times.

## Checking Enabled Levels

Use `Logger.isEnabled(...)` to guard expensive operations before logging:

```java
if (Logger.isEnabled(Logger.Level.VERBOSE)) {
Logger.verbose("Complex state: %s", expensiveToString());
}
```

## Disabling Logging at Build Time

To compile a release build with all logging completely eliminated:

```bash
./gradlew build -PnoLogging
```

This replaces the `Logger` implementation with empty method bodies at compile time. Every `Logger.*` call becomes a no-op with zero runtime overhead -- no stack traces, no formatting, no I/O. The `init()` call is also a no-op, so existing code does not need to change.

The default build (without `-PnoLogging`) includes full logging support.

## Adding a New Log Level

1. Add an entry to the `Level` enum in `subprojects/common/common/src/main/templates/Logger.enabled.kt`:

```kotlin
MY_LEVEL("MY_LEVEL"),
```

2. Add a convenience method in the same file:

```kotlin
@JvmStatic
fun myLevel(format: String, vararg args: Any?) {
if (!requireInit()) return
log(Level.MY_LEVEL, format, *args)
}
```

3. Add the level name to the `ALL` constant:

```kotlin
const val ALL = "ERROR|WARN|RESULT|BENCHMARK|MAINSTEP|SUBSTEP|INFO|DETAIL|VERBOSE|DEBUG_SOLVER|MY_LEVEL"
```

4. Add the matching empty method to `subprojects/common/common/src/main/templates/Logger.disabled.kt`:

```kotlin
@JvmStatic
fun myLevel(format: String, vararg args: Any?) {}
```

5. Users can now enable it via the pattern: `Logger.init("ERROR|MY_LEVEL")`.
2 changes: 0 additions & 2 deletions subprojects/cfa/cfa-analysis/bin/.gitignore
View file
Open in desktop

This file was deleted.

58 changes: 16 additions & 42 deletions ...cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/config/CfaConfigBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,7 @@
import hu.bme.mit.theta.cfa.analysis.prec.GlobalCfaPrecRefiner;
import hu.bme.mit.theta.cfa.analysis.prec.LocalCfaPrec;
import hu.bme.mit.theta.cfa.analysis.prec.LocalCfaPrecRefiner;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;

import hu.bme.mit.theta.solver.Solver;
import hu.bme.mit.theta.solver.SolverFactory;
import java.util.Set;
Expand All @@ -65,7 +64,6 @@ public class CfaConfigBuilder {
private final SolverFactory refinementSolverFactory;
private final Domain domain;
private final Refinement refinement;
private Logger logger = NullLogger.getInstance();
private Search search = Search.BFS;
private PredSplit predSplit = PredSplit.WHOLE;
private PrecGranularity precGranularity = PrecGranularity.GLOBAL;
Expand Down Expand Up @@ -93,11 +91,6 @@ public CfaConfigBuilder(
this.refinementSolverFactory = refinementSolverFactory;
}

public CfaConfigBuilder logger(final Logger logger) {
this.logger = logger;
return this;
}

public CfaConfigBuilder search(final Search search) {
this.search = search;
return this;
Expand Down Expand Up @@ -173,8 +166,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
BW_BIN_ITP {
Expand All @@ -190,8 +182,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
SEQ_ITP {
Expand All @@ -207,8 +198,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
MULTI_SEQ {
Expand All @@ -229,8 +219,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
UNSAT_CORE {
Expand All @@ -246,8 +235,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getVarsRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
UCB {
Expand All @@ -263,8 +251,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_WP {
Expand All @@ -285,8 +272,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_SP {
Expand All @@ -307,8 +293,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_WP_LV {
Expand All @@ -329,8 +314,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_SP_LV {
Expand All @@ -351,8 +335,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_IT_WP {
Expand All @@ -373,8 +356,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_IT_SP {
Expand All @@ -395,8 +377,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_IT_WP_LV {
Expand All @@ -417,8 +398,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
},
NWT_IT_SP_LV {
Expand All @@ -439,8 +419,7 @@ ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> getRefiner(
builderStrategy
.getPrecGranularity()
.createRefiner(builderStrategy.getItpRefToPrec()),
builderStrategy.getPruneStrategy(),
builderStrategy.getLogger());
builderStrategy.getPruneStrategy());
}
};

Expand Down Expand Up @@ -629,10 +608,6 @@ protected PruneStrategy getPruneStrategy() {
return pruneStrategy;
}

protected Logger getLogger() {
return logger;
}

public abstract CfaPrec<P> createInitPrec();

public CfaLts getLts(CFA.Loc errLoc) {
Expand All @@ -652,13 +627,12 @@ public CfaConfig<CfaState<S>, CfaAction, CfaPrec<P>> buildConfig(CFA.Loc errLoc)
BasicArgAbstractor.builder(argBuilder)
.waitlist(PriorityWaitlist.create(search.getComp(cfa, errLoc)))
.stopCriterion(refinement.getStopCriterion())
.logger(logger)
.build();
final ArgRefiner<CfaState<S>, CfaAction, CfaPrec<P>> refiner =
refinement.getRefiner(this);
final SafetyChecker<
ARG<CfaState<S>, CfaAction>, Trace<CfaState<S>, CfaAction>, CfaPrec<P>>
checker = ArgCegarChecker.create(abstractor, refiner, logger);
checker = ArgCegarChecker.create(abstractor, refiner);
return CfaConfig.create(checker, createInitPrec());
}

Expand Down
5 changes: 1 addition & 4 deletions ...ects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaPipelineChecker.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,6 @@ import hu.bme.mit.theta.analysis.expl.ExplState
import hu.bme.mit.theta.analysis.expr.ExprAction
import hu.bme.mit.theta.analysis.unit.UnitPrec
import hu.bme.mit.theta.cfa.CFA
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.common.logging.NullLogger

class CfaPipelineChecker<Pr : InvariantProof>
@JvmOverloads
Expand All @@ -39,9 +37,8 @@ constructor(
passes: MutableList<MonolithicExprPass<Pr>> = mutableListOf(),
validators: List<MonolithicExprPassValidator<in Pr>> =
MonolithicExprPassPipelineChecker.defaultValidators(),
logger: Logger = NullLogger.getInstance(),
) :
FormalismPipelineChecker<CFA, CfaState<ExplState>, CfaAction, Pr, InvariantProof>(
CfaToMonolithicAdapter(cfa),
MEPipelineCheckerConstructorArguments(checkerFactory, passes, validators, logger),
MEPipelineCheckerConstructorArguments(checkerFactory, passes, validators),
)
8 changes: 2 additions & 6 deletions ...s/cfa/cfa-analysis/src/test/java/hu/bme/mit/theta/cfa/analysis/CfaBoundedCheckerTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,7 @@
import hu.bme.mit.theta.cfa.CFA;
import hu.bme.mit.theta.cfa.dsl.CfaDslManager;
import hu.bme.mit.theta.common.OsHelper;
import hu.bme.mit.theta.common.logging.ConsoleLogger;
import hu.bme.mit.theta.common.logging.Logger;
import hu.bme.mit.theta.common.logging.NullLogger;
import hu.bme.mit.theta.solver.SolverFactory;
import hu.bme.mit.theta.solver.SolverManager;
import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
Expand Down Expand Up @@ -61,12 +59,11 @@ public static Collection<Object[]> data() {
@ParameterizedTest(name = "{index}: {0}, {1}")
public void test(String filePath, boolean isSafe) throws Exception {
initCfaBoundedCheckerTest(filePath, isSafe);
final Logger logger = new ConsoleLogger(Logger.Level.SUBSTEP);

SolverManager.registerSolverManager(Z3SolverManager.create());
if (OsHelper.getOs().equals(OsHelper.OperatingSystem.LINUX)) {
SolverManager.registerSolverManager(
SmtLibSolverManager.create(SmtLibSolverManager.HOME, NullLogger.getInstance()));
SmtLibSolverManager.create(SmtLibSolverManager.HOME));
}

final SolverFactory solverFactory;
Expand All @@ -88,8 +85,7 @@ public void test(String filePath, boolean isSafe) throws Exception {
BoundedCheckerBuilderKt.buildKIND(
monolithicExpr,
solverFactory.createSolver(),
solverFactory.createSolver(),
logger));
solverFactory.createSolver()));
status = checker.check(null);

Assertions.assertEquals(isSafe, status.isSafe());
Expand Down
Loading
Loading