Skip to content

Fix #341: Add model classes for java.util.logging#583

Closed
HritikRaj2 wants to merge 4 commits into
javapathfinder:masterfrom
HritikRaj2:fix-341-logger-support
Closed

Fix #341: Add model classes for java.util.logging#583
HritikRaj2 wants to merge 4 commits into
javapathfinder:masterfrom
HritikRaj2:fix-341-logger-support

Conversation

@HritikRaj2

Copy link
Copy Markdown
Contributor

Problem

JPF crashes when code calls Logger.getLogger() because the real JDK implementation uses:

  • Native methods (jdk.internal.misc.VM.initializeFromArchive)
  • Unsupported Thread constructors
  • Complex security and filesystem APIs

Solution

Created model classes for java.util.logging.Logger, LogManager, and Level that provide simplified, JPF-compatible implementations.

Changes

  • src/classes/modules/java.logging/java/util/logging/Logger.java - Model class for Logger
  • src/classes/modules/java.logging/java/util/logging/LogManager.java - Model class for LogManager
  • src/classes/modules/java.logging/java/util/logging/Level.java - Model class for Level
  • src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java - Test case

Testing

All existing tests pass + new test confirms Logger.getLogger() works without crashes.

- Created Logger, LogManager, and Level model classes
- Bypasses native method calls and complex JDK initialization
- Adds test case to verify Logger.getLogger() works in JPF
@HritikRaj2

Copy link
Copy Markdown
Contributor Author

Hi @cyrille-artho,
Please review when you have a chance!

@cyrille-artho cyrille-artho left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your contribution.
Please remove changes in whitespace in FileHandler, as there is no code change there.
Also, please try to add a minimal Handler for the log output so we can "write" the log to an array instead of to the terminal. This avoids cluttering the output during testing and lets us compare the output to the expected result.

* Apache License, Version 2.0 (the "License"); you may not use this file except
* in compliance with the License. You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please avoid changes in whitespace, as we subsequently want to merge changes to master to other branches (to support newer Java versions). Therefore, we want to keep only essential changes.

@Test
public void testGetLogger() {
if (verifyNoPropertyViolation()) {
System.out.println("--- calling getLogger");

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

remove println in unit tests

}

public void log(Level level, String msg) {
System.out.println("[" + level.getName() + "] " + name + ": " + msg);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We probably want to define the Handler in the logger, too, so we can redirect the log to an OutputStream. For testing, we can redirect to a ByteArrayOutputStream to compare the "written" messages to that stream with an expected result.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A very lightweight Handler will suffice for us; the only functionality that is essential is that the messages do not get written to the terminal during testing.

System.out.println("--- calling getLogger");
Logger log = Logger.getLogger("testLogger");
assertNotNull(log);
System.out.println("--- success: " + log.getName());

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Change this statement to an assertion (e.g., assertEquals(log.getName(), "testLogger") and add a few assertions to check other log settings.

if (verifyNoPropertyViolation()) {
System.out.println("--- calling getLogger");
Logger log = Logger.getLogger("testLogger");
assertNotNull(log);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can remove this line, as log is used below, so the test would fail if log were null.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the detailed review!

I will address all the points:

  1. Reverting the whitespace changes in FileHandler.java.
  2. Removing the System.out.println calls in the test.
  3. Implementing a minimal Handler and LogRecord model so we can redirect output to a stream.
  4. Updating the test to verify log content using assertions instead of visual inspection.

Working on the updates now!

@cyrille-artho

Copy link
Copy Markdown
Member

Thank you for your changes.
Your changes are currently on a commit on your repository but not on the right branch that is connected to your earlier PR.
You can try to update the branch you used for the PR or close your old PR and make a new one. That will allow me to review your changes.

@HritikRaj2

Copy link
Copy Markdown
Contributor Author

@cyrille-artho
Thank you for the guidance!

Following your advice, I have closed this Pull Request and opened a fresh one to ensure a clean commit history and to remove the unrelated files (like ClockTest and FileHandler) that were accidentally included here.
The new Pull Request is here: #584

@HritikRaj2 HritikRaj2 closed this Dec 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants