diff --git a/src/classes/modules/java.logging/java/util/logging/Formatter.java b/src/classes/modules/java.logging/java/util/logging/Formatter.java new file mode 100644 index 000000000..77d7aee5b --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/Formatter.java @@ -0,0 +1,32 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +/** + * MJI model class for java.util.logging.Formatter + * + * Minimal stub to support Handler.setFormatter(Formatter). + */ +public abstract class Formatter { + + public abstract String format(LogRecord record); + + public String formatMessage(LogRecord record) { + return record.getMessage(); + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/Handler.java b/src/classes/modules/java.logging/java/util/logging/Handler.java new file mode 100644 index 000000000..6edb75be2 --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/Handler.java @@ -0,0 +1,41 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +/** + * MJI model class for java.util.logging.Handler + * + * Minimal stub to support Logger.addHandler() and FileHandler hierarchy + * without triggering JDK internal initialization. + */ +public abstract class Handler { + + public abstract void publish(LogRecord record); + + public abstract void flush(); + + public abstract void close(); + + public void setFormatter(Formatter fmt) { } + + public void setLevel(Level newLevel) { } + + public Level getLevel() { + return Level.ALL; + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/Level.java b/src/classes/modules/java.logging/java/util/logging/Level.java new file mode 100644 index 000000000..8d5c5e22f --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/Level.java @@ -0,0 +1,56 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +/** + * MJI model class for java.util.logging.Level + * + * Provides predefined logging levels to avoid triggering JDK's heavy + * Level initialization (which involves resource bundles and locale handling). + */ +public class Level { + private final String name; + private final int value; + + protected Level(String name, int value) { + this.name = name; + this.value = value; + } + + public String getName() { + return name; + } + + public final int intValue() { + return value; + } + + public static final Level OFF = new Level("OFF", Integer.MAX_VALUE); + public static final Level SEVERE = new Level("SEVERE", 1000); + public static final Level WARNING = new Level("WARNING", 900); + public static final Level INFO = new Level("INFO", 800); + public static final Level CONFIG = new Level("CONFIG", 700); + public static final Level FINE = new Level("FINE", 500); + public static final Level FINER = new Level("FINER", 400); + public static final Level FINEST = new Level("FINEST", 300); + public static final Level ALL = new Level("ALL", Integer.MIN_VALUE); + + public String toString() { + return name; + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/LogManager.java b/src/classes/modules/java.logging/java/util/logging/LogManager.java new file mode 100644 index 000000000..36496873c --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/LogManager.java @@ -0,0 +1,64 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +import java.util.HashMap; +import java.util.Map; + +/** + * MJI model class for java.util.logging.LogManager + * + * Provides a minimal LogManager that avoids JDK's heavy initialization + * (configuration file loading, file system access, security manager checks) + * which causes crashes in JPF. See issue #341. + */ +public class LogManager { + + private static final LogManager manager = new LogManager(); + private final Map loggers = new HashMap<>(); + + protected LogManager() { + } + + public static LogManager getLogManager() { + return manager; + } + + public synchronized Logger getLogger(String name) { + return loggers.get(name); + } + + public synchronized boolean addLogger(Logger logger) { + String name = logger.getName(); + if (loggers.containsKey(name)) { + return false; + } + loggers.put(name, logger); + return true; + } + + Logger demandLogger(String name, String resourceBundleName, Class caller) { + Logger result = getLogger(name); + if (result == null) { + Logger newLogger = new Logger(name, resourceBundleName); + addLogger(newLogger); + result = newLogger; + } + return result; + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/LogRecord.java b/src/classes/modules/java.logging/java/util/logging/LogRecord.java new file mode 100644 index 000000000..be9fe21d6 --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/LogRecord.java @@ -0,0 +1,45 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +/** + * MJI model class for java.util.logging.LogRecord + * + * Minimal stub to support Handler.publish(LogRecord). + */ +public class LogRecord { + private Level level; + private String message; + + public LogRecord(Level level, String msg) { + this.level = level; + this.message = msg; + } + + public Level getLevel() { + return level; + } + + public String getMessage() { + return message; + } + + public void setMessage(String message) { + this.message = message; + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/Logger.java b/src/classes/modules/java.logging/java/util/logging/Logger.java new file mode 100644 index 000000000..45b90e799 --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/Logger.java @@ -0,0 +1,114 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +/** + * MJI model class for java.util.logging.Logger + * + * Provides a lightweight Logger that bypasses JDK's heavy LogManager + * initialization (config file loading, file system access, security checks, + * Thread/AccessController calls) which cause crashes in JPF. + * See issue #341. + */ +public class Logger { + + private String name; + private String resourceBundleName; + + protected Logger(String name, String resourceBundleName) { + this.name = name; + this.resourceBundleName = resourceBundleName; + } + + public static Logger getLogger(String name) { + return getLogger(name, null); + } + + public static Logger getLogger(String name, String resourceBundleName) { + LogManager manager = LogManager.getLogManager(); + return manager.demandLogger(name, resourceBundleName, null); + } + + public static Logger getAnonymousLogger() { + return new Logger("", null); + } + + public static Logger getAnonymousLogger(String resourceBundleName) { + return new Logger("", resourceBundleName); + } + + public String getName() { + return name; + } + + public String getResourceBundleName() { + return resourceBundleName; + } + + public void setLevel(Level level) { } + + public Level getLevel() { + return Level.INFO; + } + + public void addHandler(Handler h) { } + + public void removeHandler(Handler h) { } + + public void setUseParentHandlers(boolean use) { } + + public boolean getUseParentHandlers() { + return true; + } + + public void info(String msg) { + log(Level.INFO, msg); + } + + public void warning(String msg) { + log(Level.WARNING, msg); + } + + public void severe(String msg) { + log(Level.SEVERE, msg); + } + + public void config(String msg) { + log(Level.CONFIG, msg); + } + + public void fine(String msg) { + log(Level.FINE, msg); + } + + public void finer(String msg) { + log(Level.FINER, msg); + } + + public void finest(String msg) { + log(Level.FINEST, msg); + } + + public void log(Level level, String msg) { + // no-op in verification mode to avoid state space expansion + } + + public boolean isLoggable(Level level) { + return false; + } +} diff --git a/src/classes/modules/java.logging/java/util/logging/StreamHandler.java b/src/classes/modules/java.logging/java/util/logging/StreamHandler.java new file mode 100644 index 000000000..2bd6a3ffe --- /dev/null +++ b/src/classes/modules/java.logging/java/util/logging/StreamHandler.java @@ -0,0 +1,51 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * 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. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package java.util.logging; + +import java.io.OutputStream; + +/** + * MJI model class for java.util.logging.StreamHandler + * + * Minimal stub to support FileHandler hierarchy. + */ +public class StreamHandler extends Handler { + + private OutputStream output; + + public StreamHandler() { } + + public StreamHandler(OutputStream out, Formatter formatter) { + this.output = out; + } + + protected synchronized void setOutputStream(OutputStream out) { + this.output = out; + } + + @Override + public void publish(LogRecord record) { } + + @Override + public void flush() { } + + @Override + public synchronized void close() { + flush(); + } +} diff --git a/src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java b/src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java new file mode 100644 index 000000000..8da7d3430 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/java/util/LoggerTest.java @@ -0,0 +1,65 @@ +package gov.nasa.jpf.test.java.util; + +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; +import java.util.logging.Logger; + +/** + * Regression test for issue #341: + * java.util.logging.Logger.getLogger crashes in JPF due to heavy + * JDK initialization (LogManager, Thread, AccessController, file system). + * + * With model classes for Logger, LogManager, and Level, these calls + * should work without property violations. + */ +public class LoggerTest extends TestJPF { + + @Test + public void testGetLogger() { + if (verifyNoPropertyViolation()) { + Logger log = Logger.getLogger("testLogger"); + assertNotNull(log); + assertEquals("testLogger", log.getName()); + } + } + + @Test + public void testGetLoggerWithResourceBundle() { + if (verifyNoPropertyViolation()) { + Logger log = Logger.getLogger("bundleLogger", "myBundle"); + assertNotNull(log); + assertEquals("bundleLogger", log.getName()); + } + } + + @Test + public void testLoggerMethods() { + if (verifyNoPropertyViolation()) { + Logger logger = Logger.getLogger("blah"); + logger.info("hello"); + logger.warning("warn"); + logger.severe("sev"); + logger.config("cfg"); + logger.fine("fine"); + logger.finer("finer"); + logger.finest("finest"); + } + } + + @Test + public void testGetAnonymousLogger() { + if (verifyNoPropertyViolation()) { + Logger log = Logger.getAnonymousLogger(); + assertNotNull(log); + } + } + + @Test + public void testSameLoggerReturned() { + if (verifyNoPropertyViolation()) { + Logger log1 = Logger.getLogger("shared"); + Logger log2 = Logger.getLogger("shared"); + assertTrue("Same logger should be returned for same name", log1 == log2); + } + } +}