[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/util LogHandler.java,NONE,1.1 LogManager.java,NONE,1.1

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/util
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/src/gov/nasa/jpf/util

Added Files:
	LogHandler.java LogManager.java 
Log Message:
this is the advent of the Debug replacement. We are using a conventional log scheme that actually piggybacks on java.util.logging, even though we don't really use logger hierarchies, we have our own initialization scheme, and we use our own log handler class. The reason for this is that we still want to maintain a single configuration scheme, and we want to be able to log to three different output destinations (hostname:port, file, out/err) without requiring to change class names in a logging.properties file. The handler is still very primitive in terms of output formatting, and the config consists of the following entries

# what is our default level for unspecified loggers
log.level=<defaultLevel>

# where to log to
log.output=<filename> | out | err | <hostname>:<port>

# logger specific levels
log.severe=<logger-pattern>{:<logger-pattern>
log.warning=..
log.info=..
log.config=..
log.fine=..
log.finer=..
log.finest=..

There is a new class gov.nasa.jpf.tools.LogConsole that can be used to display socket logging. This is now also meant to be used for the SearchMonitor. With this in place, Debug statements will now be replaced with the standard java.util.logging.Logger API, i.e.

static Logger log = JPF.getLogger("gov.nasa.jpf.<whatever>");
..
log.severe(msg); .. log.info(msg); ..

There is one caveat to notice: since Config results are reported by means of the logging facility, but the logging is configured via Config (single source), the Config initialization (ctor) is not allowed to produce logging output, but rather has to preserve all states, failures etc. for subsequent reporting (by JPF). This is less than optimal from a design point of view (cyclic dependency), but the user-friendly pinciple of a single config source overrides this.

Second caveat is that log output should be event based, not line-by-line, which means there is an increased tendency to see hidden StringBuffer use. If there is a good chance the log level will not be set, this should be wrapped for efficiency reasons in

if (logger.isLoggable(Level.<whatever>)) {
  logger.fine("Blah " + gna + '\n' + 
                    "another line");
}

The scheme could be extended to enable logger specific output (i.e. one console for vm, another one for a listener etc.) , and the console to allow multiple simultaneous connects, but we leave that for later (if it really makes sense). For now it is important that we can replace the Debug statements.

--- NEW FILE: LogManager.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//
package gov.nasa.jpf.util;

import gov.nasa.jpf.Config;
import java.util.HashMap;
import java.util.logging.Logger;
import java.util.logging.Level;
import java.util.logging.Formatter;
import java.util.logging.LogRecord;

/**
 * this class is responsible for returning properly JPF-configured
 * Loggers. It is not supposed to be used directly by clients, but rather
 * is a JPF delegatee.
 * 
 * While we could modify/replace the standard java.util.logging facility
 * at various levels (own LogManager, own initialization class etc.), we choose
 * the approach to piggyback on it, because these mechanisms either require
 * changing system properties, rely on only partly documented features, or
 * don't give us the full functionality we need. By having our own log
 * encapsulator, we could also replace the underlying mechanism if we really
 * want to
 */
public class LogManager {
  
  static class DefaultFormatter extends Formatter {
    // we might want to parameterize this
    public String format (LogRecord r) {
      String msg = "[JPF-" + r.getLevel().getName() + "]: " + r.getMessage() + '\n';
      
      return msg;
    }
  }
  
  static HashMap loggers = new HashMap(); // our own set
  
  static Level defaultLevel;
  static LogHandler handler;  // we have only one
  
  // I don't like these categories too much, but we want to act as a stand in
  static String[] activeSevere;
  static String[] activeWarning;
  static String[] activeInfo;
  static String[] activeConfig;
  static String[] activeFine;
  static String[] activeFiner;
  static String[] activeFinest;
  
  /**
   * note - this is not allowed to fail, since we couldn't log that. Hardcoded default
   * values have to do in this case (make sure we catch the proper Config exceptions)
   */
  public static void init (Config conf) {
    try {
      defaultLevel = Level.parse( conf.getString("log.level", "INFO").toUpperCase());
    } catch (Throwable x) {
      defaultLevel = Level.WARNING;
    }
    
    activeSevere = conf.getStringArray("log.severe");
    activeWarning = conf.getStringArray("log.warning");
    activeInfo = conf.getStringArray("log.info");
    activeConfig = conf.getStringArray("log.config");
    activeFine = conf.getStringArray("log.fine");
    activeFiner = conf.getStringArray("log.finer");
    activeFinest = conf.getStringArray("log.finest");
    
    handler = new LogHandler(conf);
  }
  
  static boolean checkInclusion (String[] actives, String name) {
    if (actives == null) {
      return false;
    }
    
    for (int i=0; i<actives.length; i++) {
      if (name.matches(actives[i])) {
        return true;
      }
    }
    
    return false;
  }
  
  static Level getLevel (String name) {
    if (checkInclusion(activeSevere, name)) return Level.SEVERE;
    if (checkInclusion(activeWarning, name)) return Level.WARNING;
    if (checkInclusion(activeInfo, name)) return Level.INFO;
    if (checkInclusion(activeConfig, name)) return Level.CONFIG;
    if (checkInclusion(activeFine, name)) return Level.FINE;
    if (checkInclusion(activeFiner, name)) return Level.FINER;
    if (checkInclusion(activeFinest, name)) return Level.FINEST;
    
    return defaultLevel;
  }
  
  public static Logger getLogger (String name) {
    // how often can you say 'Logger' in one method..
    Logger logger = (Logger) loggers.get(name);
    
    if (logger == null) {
      // we haven't had this one yet - create and init a new one from the host logging system
      logger = Logger.getLogger(name);
      logger.setLevel( getLevel(name));
      logger.addHandler(handler);
      logger.setUseParentHandlers(false); // we don't want to pass this up
      
      loggers.put(name, logger);
    }
    
    return logger;
  }
  
  public static void printStatus (Logger log) {
    handler.printStatus(log);
  }
}

--- NEW FILE: LogHandler.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//
package gov.nasa.jpf.util;

import gov.nasa.jpf.Config;

import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.OutputStream;
import java.io.FileOutputStream;
import java.net.ConnectException;
import java.net.Socket;
import java.net.UnknownHostException;
import java.util.logging.Handler;
import java.util.logging.LogRecord;
import java.util.logging.Logger;

/**
 * log handler class that deals with output selection and formatting. This is the
 * only handler we use for our own logging
 */
public class LogHandler extends Handler {

  public static final String LOG_HOST = "localhost";
  public static final int LOG_PORT = 20000;
  
  File file;
  Socket socket;
  OutputStream ostream;
  
  PrintWriter out;
  
  public LogHandler (Config conf) {
    String output = conf.getString("log.output", "out");
    
    if (output.matches("[a-zA-Z0-9.]*:[0-9]*")) { // we assume that's a hostname:port spec
      int idx = output.indexOf(':');
      String host = output.substring(0, idx);
      String port = output.substring(idx+1, output.length());
      ostream = connectSocket( host, port);
    } else if (output.equalsIgnoreCase("out") || output.equals("System.out")) {
      ostream = System.out;
    } else if (output.equalsIgnoreCase("err") || output.equals("System.err")) {
      ostream = System.err;
    } else {
      ostream = openFile(output);
    }
    
    if (ostream == null) {
      ostream = System.out;
    }
    
    out = new PrintWriter(ostream, true);
  }
  
  OutputStream connectSocket (String host, String portSpec) {
    int port = -1;
    
    if ((host == null) || (host.length() == 0)) {
      host = LOG_HOST;
    }
    
    if (portSpec != null) {
      try {
        port = Integer.parseInt(portSpec);
      } catch (NumberFormatException x) {
        // just catch it
      }
    }
    if (port == -1) {
      port = LOG_PORT;
    }
    
    
    try {
      socket = new Socket(host, port);
      return socket.getOutputStream();
    } catch (UnknownHostException uhx) {
      //System.err.println("unknown log host: " + host);
    } catch (ConnectException cex) {
      //System.err.println("no log host detected);
    } catch (IOException iox) {
      //System.err.println(iox);
    }

    return null;
  }
  
  OutputStream openFile (String fileName) {
    file = new File(fileName);
    
    try {
      if (file.exists()) {
        file.delete();
      }
      file.createNewFile();
      return new FileOutputStream(file);
    } catch (IOException iox) {
      // just catch it
    }
    
    return null;
  }
  
  public void close () throws SecurityException {
    if ((ostream != System.err) && (ostream != System.out)) {
      out.close();
    }
    
    if (socket != null) {
      try {
        socket.close();
      } catch (IOException iox) {
        // not much we can do
      }
    }
  }

  public void flush () {
    out.flush();
  }

  public void publish (LogRecord r) {
    out.println(r.getMessage());
  }

  public void printStatus (Logger log) {   
    if (socket != null) {
      log.config("logging to socket: " + socket);
    } else if (file != null) {
      log.config("logging to file: " + file.getAbsolutePath());
    } else if (ostream == System.err) {
      log.config("logging to System.err");
    } else if (ostream == System.out) {
      log.config("logging to System.out");
    } else {
      log.warning("unknown log destination");
    }
  }
}