Skip to content

Conversation

@HritikRaj2
Copy link
Contributor

@HritikRaj2 HritikRaj2 commented Dec 18, 2025

Problem

JPF crashes when code calls Logger.getLogger() because the real JDK implementation relies on native methods (e.g., jdk.internal.misc.VM.initializeFromArchive), unsupported Thread constructors, and complex security/filesystem APIs that are not supported in the Model Java Interface (MJI).

Solution

Implemented a set of model classes for the java.util.logging package. These models provide a simplified, pure-Java implementation compatible with JPF that supports basic logging operations, handler management, and stream output without relying on native JDK internals.

Changes

  • src/classes/modules/java.logging/java/util/logging/Logger.java: Updated to support adding/removing handlers and publishing log records.
  • src/classes/modules/java.logging/java/util/logging/LogManager.java: Minimal implementation to manage logger instances.
  • src/classes/modules/java.logging/java/util/logging/Level.java: Model class defining standard log levels.
  • src/classes/modules/java.logging/java/util/logging/Handler.java: Abstract base class for log handlers.
  • src/classes/modules/java.logging/java/util/logging/StreamHandler.java: Implements log publishing to an output stream (throws IOException correctly on flush).
  • src/classes/modules/java.logging/java/util/logging/LogRecord.java: Encapsulates log data.
  • src/classes/modules/java.logging/java/util/logging/Formatter.java: Abstract base for log formatting.
  • src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java: New test case verifying logger caching and output capturing via ByteArrayOutputStream (assertions only, no console printing).

Testing

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

Copy link
Member

@cyrille-artho cyrille-artho left a comment

Choose a reason for hiding this comment

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

Looks good!
Please add the copyright header (the first five lines of comments that is present in all files and also about half of the new files you have created) to the remaining files.

@HritikRaj2
Copy link
Contributor Author

@cyrille-artho
Thank you for the review!
I have added the standard copyright header to all the new files (Handler, StreamHandler, LogRecord, Formatter, LogManager) as requested.

@HritikRaj2
Copy link
Contributor Author

@cyrille-artho
When ever you get time please have a look on the changes
and also check #580 so i can do changes in it if required.

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