Add model classes for java.util.logging

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();
+  }
+}

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;
+  }
+}

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;
+  }
+}

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<String, Logger> 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;
+  }
+}

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;
+  }
+}

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;
+  }
+}