Menu
▾
▴
javapathfinder-devel — development related topics (your place if you work with the sources)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
(38) |
Jun
(13) |
Jul
(3) |
Aug
(14) |
Sep
(25) |
Oct
(44) |
Nov
(6) |
Dec
(2) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(4) |
Feb
(14) |
Mar
(16) |
Apr
(2) |
May
(1) |
Jun
(2) |
Jul
(2) |
Aug
(1) |
Sep
(1) |
Oct
|
Nov
(3) |
Dec
(1) |
| 2007 |
Jan
(3) |
Feb
(39) |
Mar
(30) |
Apr
(31) |
May
(20) |
Jun
(72) |
Jul
(41) |
Aug
(78) |
Sep
(48) |
Oct
(59) |
Nov
(31) |
Dec
(47) |
| 2008 |
Jan
(18) |
Feb
(37) |
Mar
(45) |
Apr
(78) |
May
(16) |
Jun
|
Jul
(8) |
Aug
(10) |
Sep
(23) |
Oct
(10) |
Nov
(12) |
Dec
(1) |
| 2009 |
Jan
(4) |
Feb
|
Mar
(3) |
Apr
(1) |
May
(1) |
Jun
(1) |
Jul
|
Aug
|
Sep
(1) |
Oct
(3) |
Nov
(2) |
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2013 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(2) |
Oct
|
Nov
|
Dec
|
|
From: pcm <pcm...@us...> - 2005-06-09 19:55:10
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv14410/src/gov/nasa/jpf/jvm Modified Files: Step.java Log Message: trying a bit harder in case we don't have sources. It now prints out at least what sources are missing. Note that there is still the vm.report.show_missing_lines, which goes beyond that by printing executed insns (too many options, <sigh>) Index: Step.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Step.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- Step.java 26 Apr 2005 19:44:05 -0000 1.1.1.1 +++ Step.java 9 Jun 2005 19:54:54 -0000 1.2 @@ -88,24 +88,27 @@ public String getComment () { return comment; } - + public void printStepOn (PrintWriter pw, SourceRef lastPrinted, String prefix) { Source source = Source.getSource(fileName); boolean isLineMissing = source.isLineMissing(line); if (!this.equals(lastPrinted)) { if (!isLineMissing) { - lastPrinted.set(this); - - if (prefix != null) { - pw.print( prefix); - } else { - pw.print(" "); - } + pw.print( (prefix != null) ? prefix : " "); pw.print(Left.format(fileName + ":" + line, 20)); pw.print(' '); - pw.println(source.getLine(line)); + pw.println(source.getLine(line)); + } else { + if (!fileName.equals(lastPrinted.getFileName()) && !showMissingLines) { + pw.print( (prefix != null) ? prefix : " "); + pw.print("[no source for: "); + pw.print(fileName); + pw.println(']'); + } } + + lastPrinted.set(this); } if (showBytecode || (showMissingLines && isLineMissing) ) { @@ -117,11 +120,11 @@ pw.println(insn); } } - + if (comment != null) { pw.print(" // "); pw.println(comment); - } + } } public void toXML (PrintWriter pw) { |
|
From: pcm <pcm...@us...> - 2005-06-09 19:55:10
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv14410/src/gov/nasa/jpf Modified Files: Path.java Error.java Log Message: trying a bit harder in case we don't have sources. It now prints out at least what sources are missing. Note that there is still the vm.report.show_missing_lines, which goes beyond that by printing executed insns (too many options, <sigh>) Index: Path.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Path.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- Path.java 9 Jun 2005 16:29:23 -0000 1.2 +++ Path.java 9 Jun 2005 19:54:54 -0000 1.3 @@ -110,7 +110,7 @@ Object entry; for (int index = 0; index < length; index++) { - pw.print("Step #"); + pw.print("Transition #"); pw.print(index); if ((entry = list.get(index)) != null) { Index: Error.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Error.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- Error.java 26 Apr 2005 19:43:55 -0000 1.1.1.1 +++ Error.java 9 Jun 2005 19:54:54 -0000 1.2 @@ -58,9 +58,9 @@ property.printOn( ps); ps.println(); - ps.print("----------------------------------- path to error ("); + ps.print("----------------------------------- path to error (length: "); ps.print(path.length()); - ps.println(" steps):"); + ps.println(')'); path.printOn(ps); ps.println("------------------------------------ end error path"); |
|
From: pcm <pcm...@us...> - 2005-06-09 16:29:31
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31198/src/gov/nasa/jpf/jvm Modified Files: TrailInfo.java JVM.java UncaughtException.java Log Message: the path was not updated on UncaughtException exit, causing the last Transition not to appear in the error report. We probably should print out something even if the sourcepath is not set, so Step.printStepOn() still needs some work Index: TrailInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/TrailInfo.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- TrailInfo.java 26 Apr 2005 19:44:08 -0000 1.1.1.1 +++ TrailInfo.java 9 Jun 2005 16:29:23 -0000 1.2 @@ -120,7 +120,8 @@ void addStep (Step step) { if (first == null) { - first = last = step; + first = step; + last = step; } else { last.next = step; last = step; @@ -138,7 +139,6 @@ pw.print(" Random #"); pw.print(random); } - pw.println(); if (showSteps) { Index: JVM.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v retrieving revision 1.5 retrieving revision 1.6 diff -u -d -r1.5 -r1.6 --- JVM.java 9 Jun 2005 06:46:44 -0000 1.5 +++ JVM.java 9 Jun 2005 16:29:23 -0000 1.6 @@ -898,6 +898,25 @@ return forward(); } + /** + * store the current SystemState's TrainInfo in our path, after updating it + * with whatever annotations the JVM wants to add. + * This is supposed to be called after each transition we want to keep + */ + void updatePath () { + Transition t = ss.trail(); + + // <2do> we should probably store the output directly in the TrailInfo, + // but this might not be our only annotation in the future + + // did we have output during the last transition? If yes, add it + if ((out != null) && (out.length() > 0)) { + t.setOutput( out.toString()); + out.setLength(0); + } + + path.add(t); + } /** * try to advance the state @@ -945,12 +964,7 @@ // by the subsequent operations (before we return from forward) pushSystemState(); - Transition t = ss.trail(); - if ((out != null) && (out.length() > 0)) { - t.setOutput( out.toString()); - out.setLength(0); - } - path.add(t); + updatePath(); // get ready for the next round (resets Scheduler) ss.prepareNext(this); @@ -967,7 +981,8 @@ // } catch (JPFException e) { // throw e; } catch (UncaughtException e) { - // something blew up, so we definitely executed something + updatePath(); // or we loose the last transition + // something blew up, so we definitely executed something (hence return true) return true; } catch (RuntimeException e) { throw new JPFException(e); Index: UncaughtException.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/UncaughtException.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- UncaughtException.java 26 Apr 2005 19:44:08 -0000 1.1.1.1 +++ UncaughtException.java 9 Jun 2005 16:29:23 -0000 1.2 @@ -78,5 +78,6 @@ pw.print(" : "); thread.printStackTrace(pw, xObjRef); + pw.flush(); } } |
|
From: pcm <pcm...@us...> - 2005-06-09 16:29:31
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31198/src/gov/nasa/jpf Modified Files: Path.java Log Message: the path was not updated on UncaughtException exit, causing the last Transition not to appear in the error report. We probably should print out something even if the sourcepath is not set, so Step.printStepOn() still needs some work Index: Path.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Path.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- Path.java 26 Apr 2005 19:43:55 -0000 1.1.1.1 +++ Path.java 9 Jun 2005 16:29:23 -0000 1.2 @@ -112,7 +112,7 @@ for (int index = 0; index < length; index++) { pw.print("Step #"); pw.print(index); - + if ((entry = list.get(index)) != null) { pw.print(' '); |
|
From: John P. <joh...@us...> - 2005-06-09 06:46:53
|
Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv18132/src/gov/nasa/jpf/jvm Modified Files: JVM.java Log Message: added an option to indent printlns by the number of non-deterministic choices that have been made on a path to make the application output more sensible under backtracking. option enabled by vm.indent_output = true. Index: JVM.java =================================================================== RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- JVM.java 7 May 2005 00:40:01 -0000 1.4 +++ JVM.java 9 Jun 2005 06:46:44 -0000 1.5 @@ -154,6 +154,7 @@ boolean atomicLines; boolean treeOutput; boolean pathOutput; + boolean indentOutput; /** * VM instances are another example of evil throw-up ctors, but this is @@ -174,6 +175,7 @@ atomicLines = config.getBoolean("vm.por.atomic_lines", true); treeOutput = config.getBoolean("vm.tree_output", true); pathOutput = config.getBoolean("vm.path_output", false); + indentOutput = config.getBoolean("vm.indent_output",false); initSubsystems(config); initFields(config); @@ -709,7 +711,17 @@ public void println (String s) { if (treeOutput) { - System.out.println(s); + if (indentOutput){ + StringBuffer indent = new StringBuffer(); + int i; + for (i = 0;i<=path.length();i++) { + indent.append("|" + i); + } + System.out.println(indent + "|" +s); + } + else { + System.out.println(s); + } } if (pathOutput) { |
|
From: pcm <pcm...@us...> - 2005-06-08 23:47:11
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23004/src/gov/nasa/jpf Modified Files: Config.java JPF.java Log Message: changed the config dump back to using a provided PrintWriter, so that debuging the config doesn't rely on it's proper functioning (since logging is controlled by config). This also takes care of missing output because of insufficient log level (-show always prints) Index: JPF.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/JPF.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- JPF.java 18 May 2005 06:41:44 -0000 1.4 +++ JPF.java 8 Jun 2005 23:47:02 -0000 1.5 @@ -228,7 +228,7 @@ } if (isPrintConfigRequest(args)) { - conf.print(logger); + conf.print(new PrintWriter(System.out)); } if (conf.getTargetArg() != null) { Index: Config.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- Config.java 18 May 2005 06:41:44 -0000 1.4 +++ Config.java 8 Jun 2005 23:47:02 -0000 1.5 @@ -703,34 +703,30 @@ return -1; } - public void print(Logger log) { - if (log.isLoggable(Level.CONFIG)) { - StringWriter sw = new StringWriter(1024); - PrintWriter pw = new PrintWriter(sw, true); - pw.println("----------- dictionary contents"); - - // just how much do you have to do to get a sorted printout :( - TreeSet kset = new TreeSet(); - for (Enumeration e = propertyNames(); e.hasMoreElements();) { - kset.add(e.nextElement()); - } - for (Iterator it = kset.iterator(); it.hasNext();) { - String key = (String) it.next(); - Object val = getProperty(key); - pw.print(key); - pw.print(" = "); - pw.println(val); - } - - if ((freeArgs != null) && (freeArgs.length > 0)) { - pw.println("----------- free arguments"); - for (int i = 0; i < freeArgs.length; i++) { - pw.println(freeArgs[i]); - } + public void print (PrintWriter pw) { + pw.println("----------- dictionary contents"); + + // just how much do you have to do to get a sorted printout :( + TreeSet kset = new TreeSet(); + for (Enumeration e = propertyNames(); e.hasMoreElements();) { + kset.add(e.nextElement()); + } + for (Iterator it = kset.iterator(); it.hasNext();) { + String key = (String) it.next(); + String val = getExpandedString(key); + pw.print(key); + pw.print(" = "); + pw.println(val); + } + + if ((freeArgs != null) && (freeArgs.length > 0)) { + pw.println("----------- free arguments"); + for (int i = 0; i < freeArgs.length; i++) { + pw.println(freeArgs[i]); } - - log.config(sw.toString()); } + + pw.flush(); } public void printStatus(Logger log) { |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:58
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/src/gov/nasa/jpf/tools Modified Files: SearchMonitor.java Added Files: LogConsole.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: LogConsole.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.tools; import java.io.BufferedReader; import java.io.IOException; import java.io.InputStreamReader; import java.net.ServerSocket; import java.net.Socket; /** * simple logging facility that listens on a socket (e.g. for log output display) */ public class LogConsole { static int DEF_PORT = 20000; // keep this in sync with the gov.nasa.jpf.util.LogHandler class ShutdownHook implements Runnable { public void run () { if (running) { // not very threadsafe, but worst thing that can happen is we close twice killed = true; System.out.println("\nLogConsole killed, shutting down"); } try { cs.close(); ss.close(); } catch (Throwable t) { // not much we can do here anyway } } } boolean running; int port; boolean autoclose; boolean killed; ServerSocket ss; Socket cs; public void run () { running = true; Runtime.getRuntime().addShutdownHook(new Thread(new ShutdownHook())); if (port == 0) { port = DEF_PORT; } try { ss = new ServerSocket(port); try { do { System.out.println("LogConsole listening on port: " + port); cs = ss.accept(); BufferedReader in = new BufferedReader( new InputStreamReader(cs.getInputStream())); String msg; System.out.println("LogConsole connected"); System.out.println("--------------------------------------------------------------------------------"); try { while ((msg = in.readLine()) != null) { System.out.println(msg); } System.out.println("--------------------------------------------------------------------------------"); System.out.println("LogConsole disconnected"); } catch (IOException iox) { System.err.println(iox); } in.close(); cs.close(); } while (!autoclose); System.out.println("LogConsole closing"); } catch (IOException iox) { if (!killed) { System.err.println("Error: LogConsole accept failed on port: " + port); } } } catch (IOException iox) { System.err.println("Error: LogConsole cannot listen on port: " + port); } running = false; } public void showUsage () { System.out.println("LogConsole: socket based console logger"); System.out.println(" usage: java gov.nasa.jpf.tools.LogConsole {flags} [<port>]"); System.out.println(" args: -help show this message"); System.out.println(" -autoclose close the application upon disconnect"); System.out.println(" <port> optional port number, default: " + DEF_PORT); } boolean processArgs (String[] args) { for (int i=0; i<args.length; i++) { if (args[i].charAt(0) == '-') { if (args[i].equals("-autoclose")) { args[i] = null; autoclose = true; } else if (args[i].equals("-help")) { showUsage(); return false; } else { System.err.println("Warning: unknown argument (see -help for usage): " + args[i]); } } else { if (args[i].matches("[0-9]+")) { if (port != 0) { System.err.println("Error: only one port parameter allowed (see -help for usage): " + args[i]); return false; } try { port = Integer.parseInt(args[i]); } catch (NumberFormatException nfx) { System.err.println("Error: illegal port spec: " + args[i]); return false; } } else { System.out.println("Error: unknown argument: " + args[i]); return false; } } } return true; } public static void main (String[] args) { LogConsole console = new LogConsole(); if (console.processArgs(args)) { console.run(); } } } Index: SearchMonitor.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/SearchMonitor.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- SearchMonitor.java 26 Apr 2005 19:44:22 -0000 1.1.1.1 +++ SearchMonitor.java 18 May 2005 06:41:45 -0000 1.2 @@ -41,17 +41,19 @@ */ public class SearchMonitor implements SearchListener { - boolean logger; // true if this is just listening & reporting on an externally running JPF - boolean autoclose = false; - String host = "localhost"; - int port = 5556; + static final String DEF_HOSTNAME = "localhost"; + static final int DEF_PORT = 20000; + static final int DEF_INTERVAL = 1000; // min duration in ms between reports + + String hostName = DEF_HOSTNAME; + int port = DEF_PORT; Socket sock; PrintWriter out; int reportNumber; - int interval = 1000; // min duration in ms between reports + int interval = DEF_INTERVAL; long time; long lastTime; long startTime; @@ -247,36 +249,60 @@ out.println(); } + int consumeIntArg (String[] args, int i, String varName, int def) { + int ret = def; + + args[i] = null; + if (i < args.length-1){ + i++; + try { + ret = Integer.parseInt(args[i]); + args[i] = null; + } catch (NumberFormatException nfx) { + System.err.print("Warning: illegal " + varName + " specification: " + args[i] + + " using default " + ret); + } + } + + return ret; + } + void filterArgs (String[] args) { for (int i=0; i<args.length; i++) { - if (args[i].equals("-logger")) { - args[i] = null; - logger = true; - } else if (args[i].equals("-autoclose")) { + if (args[i].equals("-port")) { + port = consumeIntArg(args, i++, "port", DEF_PORT); + } else if (args[i].equals("-interval")) { + interval = consumeIntArg(args, i++, "interval", DEF_INTERVAL); + } else if (args[i].equals("-hostname")) { args[i] = null; - autoclose = true; + if (i < args.length-1){ + i++; + hostName = args[i]; + args[i] = null; + } } } } static void printUsage () { System.out.println("SearchMonitor - a JPF listener tool to monitor JPF searches"); - System.out.println("usage: java gov.nasa.jpf.tools.SearchMonitor <jpf-options> <monitor-options> <class>"); + System.out.println("usage: java gov.nasa.jpf.tools.SearchMonitor <jpf-options> <monitor-options> <class>"); System.out.println("<monitor-options>:"); - System.out.println(" -logger : run as a logger (don't run JPF)"); - System.out.println(" -autoclose : terminate logger after disconnect"); + System.out.println(" -hostname <name> : connect to host <name>, default: " + DEF_HOSTNAME); + System.out.println(" -port <num> : connect to port <num>, default: " + DEF_PORT); + System.out.println(" -interval <num> : report every <num> msec, default: " + DEF_INTERVAL); } void connect () { try { - sock = new Socket(host, port); + sock = new Socket(hostName, port); out = new PrintWriter(sock.getOutputStream(), true); } catch (UnknownHostException uhx) { - System.err.println("unknown log host: " + host + ", using System.out"); + System.err.println("Warning: unknown log host: " + hostName + ", using System.out"); } catch (ConnectException cex) { - System.err.println("no log host detected, using System.out"); + System.err.println("Warning: no log host detected, using System.out"); } catch (IOException iox) { System.err.println(iox); } @@ -286,60 +312,11 @@ } } - void log () { - try { - ServerSocket ss = new ServerSocket(port); - - try { - do { - System.out.println("logger listening on port: " + port); - - Socket cs = ss.accept(); - BufferedReader in = new BufferedReader( new InputStreamReader(cs.getInputStream())); - String msg; - - System.out.println("logger connected"); - System.out.println("------------------------------"); - try { - - while ((msg = in.readLine()) != null) { - System.out.println(msg); - } - - System.out.println("------------------------------"); - System.out.println("logger disconnected"); - } catch (IOException iox) { - System.err.println(iox); - } finally { - try { - in.close(); - cs.close(); - } catch (IOException iox) { - } - } - - } while (!autoclose); - - } catch (IOException iox) { - System.err.println("error: accept failed on port: " + port); - } finally { - ss.close(); - } - } catch (IOException iox) { - System.err.println("error: cannot listen on port: " + port); - } - } - public void run (Config conf) { - if (logger) { - log(); - - } else { - JPF jpf = new JPF(conf); - jpf.addSearchListener(this); + JPF jpf = new JPF(conf); + jpf.addSearchListener(this); - jpf.run(); - } + jpf.run(); } public static void main (String[] args) { @@ -348,29 +325,16 @@ return; } - SearchMonitor listener = new SearchMonitor(); - listener.filterArgs(args); - Config conf = JPF.createConfig(args); - listener.initFromConfig(conf); - + SearchMonitor listener = new SearchMonitor(conf); + + listener.filterArgs(args); listener.run(conf); } - void initFromConfig (Config config) { - host = config.getString("monitor.log_hostname", host); - port = config.getInt("monitor.log_port", port); - interval = config.getInt("monitor.interval", port); - } - - public SearchMonitor () { - // nothing to do here - } - - /** - * that is our JPF instantiation ctor - */ public SearchMonitor (Config config) { - initFromConfig(config); - } + hostName = config.getString("monitor.hostname", DEF_HOSTNAME); + port = config.getInt("monitor.port", DEF_PORT); + interval = config.getInt("monitor.interval", DEF_INTERVAL); + } } |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:58
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/src/gov/nasa/jpf Modified Files: JPF.java Config.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. Index: JPF.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/JPF.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- JPF.java 12 May 2005 06:25:32 -0000 1.3 +++ JPF.java 18 May 2005 06:41:44 -0000 1.4 @@ -20,8 +20,11 @@ import gov.nasa.jpf.util.CoverageManager; import gov.nasa.jpf.util.Debug; +import gov.nasa.jpf.util.LogManager; import java.io.PrintWriter; +import java.util.logging.Level; +import java.util.logging.Logger; /** @@ -33,7 +36,9 @@ /** JPF version, we read this inlater from default.properties */ static String VERSION = "3.?"; - public Config config; + static Logger logger; + + public Config config; /** * the singleton driver object, so that we can override FactoryMethods @@ -56,6 +61,15 @@ */ Path path; + + /** + * use this one to get a Logger that is initialized via our Config mechanism. Note that + * our own Loggers do NOT pass + */ + public static Logger getLogger (String name) { + return LogManager.getLogger( name); + } + /** * create new JPF object. Note this is always guaranteed to return, but the * Search and/or VM object instantiation might have failed (i.e. the JPF @@ -179,7 +193,7 @@ for ( int i=0; i<args.length; i++) { if (args[i] != null) { if (args[i].charAt(0) == '-') { - Debug.println(Debug.ERROR, "! Warning - unknown command line option: " + args[i]); + logger.warning("unknown command line option: " + args[i]); } else { // this is supposed to be the target class name - everything that follows @@ -191,26 +205,30 @@ } public static void printBanner (Config config) { - System.out.print("Java Pathfinder Model Checker v"); - System.out.print(config.getString("jpf.version", "3.1x")); - System.out.println(" - (C) 1999-2005 RIACS/NASA Ames Research Center"); + if (logger.isLoggable(Level.INFO)) { + logger.info("Java Pathfinder Model Checker v" + + config.getString("jpf.version", "3.1x") + + " - (C) 1999-2005 RIACS/NASA Ames Research Center"); + } } + public static void main(String[] args) { Config conf = createConfig(args); + LogManager.init(conf); + logger = getLogger("gov.nasa.jpf"); printBanner(conf); + LogManager.printStatus(logger); + conf.printStatus(logger); + if (isHelpRequest(args)) { showUsage(); } if (isPrintConfigRequest(args)) { - conf.print(); - } - - if (!conf.gotDefaultProperties()) { - Debug.println(Debug.ERROR, "no default properties found (hardcoded defaults might not work)"); + conf.print(logger); } if (conf.getTargetArg() != null) { Index: Config.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- Config.java 12 May 2005 06:25:32 -0000 1.3 +++ Config.java 18 May 2005 06:41:44 -0000 1.4 @@ -18,131 +18,171 @@ // package gov.nasa.jpf; -import gov.nasa.jpf.util.Debug; - import java.io.File; import java.io.FileInputStream; import java.io.IOException; import java.io.InputStream; import java.io.PrintWriter; +import java.io.StringWriter; import java.lang.reflect.Constructor; import java.lang.reflect.InvocationTargetException; +import java.net.URL; import java.util.ArrayList; import java.util.Enumeration; import java.util.Iterator; import java.util.Properties; import java.util.TreeSet; +import java.util.logging.Level; +import java.util.logging.Logger; /** - * class that encapsulates property-based JPF configuration. This is mainly - * an associative array with various typed accessors, and a structured - * initialization process. - * This implementation has the design constraint that it does not promote - * symbolic information to concrete types, which means that frequently - * accessed data should be promoted and cached in client classes. This in - * turn means we assume the data is not going to change at runtime. - * Major motivation for this mechanism is to avoid 'Option' classes that - * have concrete type fields, and hence are structural bottlenecks, i.e. - * every parameterized user extension (Heuristics, Scheduler etc.) require - * to update this single class. - * Note that Config is also not thread safe with respect to retrieving - * exceptions that occurrred during instantiation + * class that encapsulates property-based JPF configuration. This is mainly an + * associative array with various typed accessors, and a structured + * initialization process. This implementation has the design constraint that it + * does not promote symbolic information to concrete types, which means that + * frequently accessed data should be promoted and cached in client classes. + * This in turn means we assume the data is not going to change at runtime. + * Major motivation for this mechanism is to avoid 'Option' classes that have + * concrete type fields, and hence are structural bottlenecks, i.e. every + * parameterized user extension (Heuristics, Scheduler etc.) require to update + * this single class. Note that Config is also not thread safe with respect to + * retrieving exceptions that occurrred during instantiation + * + * Another important caveat for both implementation and usage of Config is that + * it is supposed to be our master configuration mechanism, i.e. it is also used + * to configure other core services like logging. This means that Config + * initialization should not depend on these services. Initialization has to + * return at all times, recording potential problems for later handling. This is + * why we have to keep the Config data model and initialization fairly simple + * and robust. */ public class Config extends Properties { - - static final String TARGET_KEY="target"; - static final String TARGET_ARGS_KEY="target_args"; - + + static final String TARGET_KEY = "target"; + + static final String TARGET_ARGS_KEY = "target_args"; + /** - * this class wraps the various exceptions we might encounter esp. - * during reflection instantiation + * this class wraps the various exceptions we might encounter esp. during + * reflection instantiation */ public class Exception extends java.lang.Exception { - public Exception (String msg) { + public Exception(String msg) { super(msg); } - - public Exception (String msg, Throwable cause) { + + public Exception(String msg, Throwable cause) { super(msg, cause); } - - public Exception (String key, Class cls, String failure) { - super( "error instantiating class " + cls.getName() + " for entry \"" + - key + "\":" + failure); + + public Exception(String key, Class cls, String failure) { + super("error instantiating class " + cls.getName() + " for entry \"" + + key + "\":" + failure); } - - public Exception (String key, Class cls, String failure, Throwable cause) { - this(key,cls,failure); + + public Exception(String key, Class cls, String failure, Throwable cause) { + this(key, cls, failure); initCause(cause); } - - public String toString () { - StringBuffer sb = new StringBuffer(); + + public String toString() { + StringBuffer sb = new StringBuffer(); sb.append("JPF configuration error: "); sb.append(getMessage()); - + return sb.toString(); } } - + String fileName; - boolean gotProperties; + + Object source; + + boolean gotProperties; /** - * all arguments that are not <key>=<value> pairs + * all arguments that are not <key>= <value>pairs */ String[] freeArgs; - + /** - * this is our internal defaults ctor + * this is our internal defaults ctor */ - private Config (String alternatePath, Class codeBase) { + private Config(String alternatePath, Class codeBase) { gotProperties = loadFile("default.properties", alternatePath, codeBase); } - - public Config (String[] args, String fileName, String alternatePath, Class codeBase) { - super(new Config( alternatePath, (codeBase == null) ? codeBase = getCallerClass(1) : codeBase)); - + + public Config(String[] args, String fileName, String alternatePath, + Class codeBase) { + super(new Config(alternatePath, + (codeBase == null) ? codeBase = getCallerClass(1) : codeBase)); + this.fileName = fileName; gotProperties = loadFile(fileName, alternatePath, codeBase); - + processArgs(args); normalizeValues(); } - - public boolean gotDefaultProperties () { + + public boolean gotDefaultProperties() { if (defaults != null && defaults instanceof Config) { - return ((Config)defaults).gotProperties(); + return ((Config) defaults).gotProperties(); } return false; } - - public boolean gotProperties () { + + public boolean gotProperties() { return gotProperties; } - - public String getFileName () { + + public String getFileName() { return fileName; } - - public String[] getArgs () { + + public String getSourceName() { + if (source == null) { + return null; + } else if (source instanceof File) { + return ((File) source).getAbsolutePath(); + } else if (source instanceof URL) { + return source.toString(); + } else { + return source.toString(); + } + } + + public String getDefaultsSourceName() { + if ((defaults != null) && (defaults instanceof Config)) { + return ((Config) defaults).getSourceName(); + } else { + return null; + } + } + + public Object getSource() { + return source; + } + + public String[] getArgs() { return freeArgs; } - - public void throwException (String msg) throws Exception { + + public void throwException(String msg) throws Exception { throw new Exception(msg); } - + /** * find callers class - * @param up - levels upwards from our caller (NOT counting ourselves) + * + * @param up - + * levels upwards from our caller (NOT counting ourselves) * @return caller class, null if illegal 'up' value */ - public static Class getCallerClass (int up) { - int idx = up+1; // don't count ourselves - + public static Class getCallerClass(int up) { + int idx = up + 1; // don't count ourselves + StackTraceElement[] st = (new Throwable()).getStackTrace(); - if ((up <0) || (idx >= st.length)) { + if ((up < 0) || (idx >= st.length)) { return null; } else { try { @@ -152,7 +192,7 @@ } } } - + boolean loadFile(String fileName, String alternatePath, Class codeBase) { InputStream is = null; @@ -162,23 +202,23 @@ if (!f.exists()) { // Ok, try alternatePath, if fileName wasn't absolute if (!f.isAbsolute() && (alternatePath != null)) { - f = new File(alternatePath, fileName); + f = new File(alternatePath, fileName); } } - + if (f.exists()) { + source = f; is = new FileInputStream(f); - Debug.println(Debug.MESSAGE, "reading config from file: " + f.getAbsolutePath()); - } else { + } else { // if there is no file, try to load as a resource (jar) Class clazz = (codeBase != null) ? codeBase : Config.class; is = clazz.getResourceAsStream(fileName); if (is != null) { - Debug.println(Debug.MESSAGE, "reading config from resource: " + fileName); + source = clazz.getResource(fileName); // a URL } } - if (is != null){ + if (is != null) { load(is); return true; } @@ -190,23 +230,25 @@ } /** - * extract all "+<key>=<val>" parameters, store/overwrite them in our + * extract all "+ <key>= <val>" parameters, store/overwrite them in our * dictionary, collect all other parameters in a String array - * @param args - array of String parameters to process + * + * @param args - + * array of String parameters to process */ void processArgs(String[] args) { int i; String arg; ArrayList list = new ArrayList(); - for (i=0; i<args.length; i++) { + for (i = 0; i < args.length; i++) { String a = args[i]; if (a != null) { if (a.charAt(0) == '+') { int idx = a.indexOf("="); if (idx > 0) { - setProperty( a.substring(1, idx), a.substring(idx + 1)); - } else { + setProperty(a.substring(1, idx), a.substring(idx + 1)); + } else { setProperty(a.substring(1), ""); } } else { @@ -217,18 +259,20 @@ int n = list.size(); freeArgs = new String[n]; - for (i=0; i<n; i++) { + for (i = 0; i < n; i++) { freeArgs[i] = (String) list.get(i); } } /** - * return the index of the first free argument that does not start with an hyphen + * return the index of the first free argument that does not start with an + * hyphen */ - public int getNonOptionArgIndex () { - if ((freeArgs == null) || (freeArgs.length == 0)) return -1; - - for (int i=0; i<freeArgs.length; i++) { + public int getNonOptionArgIndex() { + if ((freeArgs == null) || (freeArgs.length == 0)) + return -1; + + for (int i = 0; i < freeArgs.length; i++) { String a = freeArgs[i]; if (a != null) { char c = a.charAt(0); @@ -237,15 +281,15 @@ } } } - + return -1; } - + /** - * return the first non-option freeArg, or 'null' if there is none - * (usually denotes the application to start) + * return the first non-option freeArg, or 'null' if there is none (usually + * denotes the application to start) */ - public String getTargetArg () { + public String getTargetArg() { int i = getNonOptionArgIndex(); if (i < 0) { return getString(TARGET_KEY); @@ -253,14 +297,14 @@ return freeArgs[i]; } } - + /** - * return all args that follow the first non-option freeArgs - * (usually denotes the parametsr to pass to the application to start) + * return all args that follow the first non-option freeArgs (usually denotes + * the parametsr to pass to the application to start) */ - public String[] getTargetArgParameters () { + public String[] getTargetArgParameters() { int i = getNonOptionArgIndex(); - if (i >= freeArgs.length-1) { + if (i >= freeArgs.length - 1) { String[] a = getStringArray(TARGET_ARGS_KEY); if (a != null) { return a; @@ -268,70 +312,48 @@ return new String[0]; } } else { - int n = freeArgs.length - (i+1); + int n = freeArgs.length - (i + 1); String[] a = new String[n]; - System.arraycopy(freeArgs, i+1, a, 0, n); + System.arraycopy(freeArgs, i + 1, a, 0, n); return a; } } - - public String getArg (int i) { - if (freeArgs == null) return null; - if (freeArgs.length-1 < i) return null; - if (i < 0) return null; - + + public String getArg(int i) { + if (freeArgs == null) + return null; + if (freeArgs.length - 1 < i) + return null; + if (i < 0) + return null; + return freeArgs[i]; } - - public void print () { - PrintWriter pw = new PrintWriter(System.out, true); - pw.println("----------- dictionary contents"); - - // just how much do you have to do to get a sorted printout :( - TreeSet kset = new TreeSet(); - for (Enumeration e=propertyNames(); e.hasMoreElements();) { - kset.add(e.nextElement()); - } - for (Iterator it = kset.iterator(); it.hasNext(); ) { - String key = (String)it.next(); - Object val = getProperty(key); - pw.print(key); - pw.print(" = "); - pw.println(val); - } - if ((freeArgs != null) && (freeArgs.length > 0)) { - pw.println("----------- free arguments"); - for (int i=0; i<freeArgs.length; i++) { - pw.println(freeArgs[i]); - } - } - } - /** * turn standard type values (boolean etc.) into common formats - * ("true"/"false" for booleans) + * ("true"/"false" for booleans) */ - void normalizeValues () { - for (Enumeration keys = keys(); keys.hasMoreElements(); ){ + void normalizeValues() { + for (Enumeration keys = keys(); keys.hasMoreElements();) { String k = (String) keys.nextElement(); String v = getProperty(k); - if ("true".equalsIgnoreCase(v) || "t".equalsIgnoreCase(v) || - "yes".equalsIgnoreCase(v) || "y".equalsIgnoreCase(v)){ + if ("true".equalsIgnoreCase(v) || "t".equalsIgnoreCase(v) + || "yes".equalsIgnoreCase(v) || "y".equalsIgnoreCase(v)) { put(k, "true"); - } else if ("false".equalsIgnoreCase(v) || "f".equalsIgnoreCase(v) || - "no".equalsIgnoreCase(v) || "n".equalsIgnoreCase(v)) { + } else if ("false".equalsIgnoreCase(v) || "f".equalsIgnoreCase(v) + || "no".equalsIgnoreCase(v) || "n".equalsIgnoreCase(v)) { put(k, "false"); } } } - - public boolean getBoolean (String key) { + + public boolean getBoolean(String key) { String v = getProperty(key); return (v != null) && ("true".equals(v)); } - - public boolean getBoolean (String key, boolean def) { + + public boolean getBoolean(String key, boolean def) { String v = getProperty(key); if (v != null) { return ("true".equals(v)); @@ -339,12 +361,12 @@ return def; } } - - public int getInt (String key) { + + public int getInt(String key) { return getInt(key, 0); } - public int getInt (String key, int defValue) { + public int getInt(String key, int defValue) { String v = getProperty(key); if (v != null) { try { @@ -353,15 +375,15 @@ return defValue; } } - - return defValue; + + return defValue; } - - public long getLong (String key) { + + public long getLong(String key) { return getLong(key, 0L); } - - public long getLong (String key, long defValue) { + + public long getLong(String key, long defValue) { String v = getProperty(key); if (v != null) { try { @@ -370,15 +392,15 @@ return defValue; } } - - return defValue; + + return defValue; } - public String getString (String key) { - return getProperty(key); + public String getString(String key) { + return getProperty(key); } - - public String getString (String key, String defValue) { + + public String getString(String key, String defValue) { String s = getProperty(key); if (s != null) { return s; @@ -386,48 +408,50 @@ return defValue; } } - + /** - * same as getString(), except of that we look for '${<key>}' patterns, and replace them - * with values if we find corresponding keys. Expansion is not done recursively (but could be) + * same as getString(), except of that we look for '${ <key>}' patterns, and + * replace them with values if we find corresponding keys. Expansion is not + * done recursively (but could be) */ - public String getExpandedString (String key) { + public String getExpandedString(String key) { int i, j = 0; String s = getString(key); if (s == null || s.length() == 0) { return s; } - + while ((i = s.indexOf("${", j)) >= 0) { if ((j = s.indexOf('}', i)) > 0) { - String k = s.substring(i+2, j); + String k = s.substring(i + 2, j); String v = getString(k, ""); if (v != null) { - s = s.substring(0, i) + v + s.substring(j+1, s.length()); + s = s.substring(0, i) + v + s.substring(j + 1, s.length()); j = i + v.length(); } else { - s = s.substring(0, i) + s.substring(j+1, s.length()); - j = i; + s = s.substring(0, i) + s.substring(j + 1, s.length()); + j = i; } } } return s; } - + /** - * return memory size in bytes, or 'defValue' if not in dictionary. Encoding can have a 'M' or 'k' postfix, - * values have to be positive integers (decimal notation) + * return memory size in bytes, or 'defValue' if not in dictionary. Encoding + * can have a 'M' or 'k' postfix, values have to be positive integers (decimal + * notation) */ - public long getMemorySize (String key, long defValue) { + public long getMemorySize(String key, long defValue) { String v = getProperty(key); - long sz = defValue; - + long sz = defValue; + if (v != null) { - int n = v.length()-1; + int n = v.length() - 1; try { char c = v.charAt(n); - + if ((c == 'M') || (c == 'm')) { sz = Long.parseLong(v.substring(0, n)) << 20; } else if ((c == 'K') || (c == 'k')) { @@ -435,134 +459,135 @@ } else { sz = Long.parseLong(v); } - + } catch (NumberFormatException nfx) { return defValue; } } - + return sz; } - - public String[] getStringArray (String key) { + + public String[] getStringArray(String key) { String v = getProperty(key); if (v != null) { - return v.split("[:;, ]"); + return v.split("[:;, ]+"); } - + return null; } - - public Class getClass (String key) throws Exception { + + public Class getClass(String key) throws Exception { String v = getProperty(key); - if ((v != null) && (v.length() >0)) { + if ((v != null) && (v.length() > 0)) { try { return Class.forName(v); } catch (ClassNotFoundException cfx) { - throw new Exception( "class not found " + v); + throw new Exception("class not found " + v); } catch (ExceptionInInitializerError ix) { - throw new Exception("class initialization of " + v + " failed: " + ix, ix); + throw new Exception("class initialization of " + v + " failed: " + ix, + ix); } } - + return null; } - - public Class getEssentialClass (String key) throws Exception { + + public Class getEssentialClass(String key) throws Exception { Class cls = getClass(key); if (cls == null) { throw new Exception("no classname entry for: \"" + key + "\""); } - + return cls; } - - public Class[] getClasses (String key) throws Exception { + + public Class[] getClasses(String key) throws Exception { String[] v = getStringArray(key); if (v != null) { int n = v.length; Class[] a = new Class[n]; - for (int i=0; i<n; i++) { + for (int i = 0; i < n; i++) { try { a[i] = Class.forName(v[i]); } catch (ClassNotFoundException cnfx) { - throw new Exception( "class not found " + v[i]); + throw new Exception("class not found " + v[i]); } catch (ExceptionInInitializerError ix) { - throw new Exception("class initialization of " + v[i] + " failed: " + ix, ix); + throw new Exception("class initialization of " + v[i] + " failed: " + + ix, ix); } } - + return a; } - + return null; } - - public Object[] getInstances (String key, Class type) throws Exception { + + public Object[] getInstances(String key, Class type) throws Exception { Class[] c = getClasses(key); if (c != null) { Class[] argTypes = { Config.class }; Object[] args = { this }; Object[] a = new Object[c.length]; - - for (int i=0; i<c.length; i++) { + + for (int i = 0; i < c.length; i++) { a[i] = getInstance(key, c[i], type, argTypes, args); } - + return a; } - + return null; } - - public Object getInstance (String key, Class type) throws Exception { + + public Object getInstance(String key, Class type) throws Exception { Class[] argTypes = { Config.class }; Object[] args = { this }; - - return getInstance( key, type, argTypes, args); + + return getInstance(key, type, argTypes, args); } - - public Object getInstance (String key, Class type, Class[] argTypes, Object[] args) throws Exception { + + public Object getInstance(String key, Class type, Class[] argTypes, + Object[] args) throws Exception { Class cls = getClass(key); if (cls != null) { - return getInstance( key, cls, type, argTypes, args); + return getInstance(key, cls, type, argTypes, args); } else { return null; } } - public Object getEssentialInstance (String key, Class type) throws Exception { + public Object getEssentialInstance(String key, Class type) throws Exception { Class[] argTypes = { Config.class }; Object[] args = { this }; - return getEssentialInstance( key, type, argTypes, args); + return getEssentialInstance(key, type, argTypes, args); } - public Object getEssentialInstance (String key, Class type, Class[] argTypes, Object[] args) throws Exception { + public Object getEssentialInstance(String key, Class type, Class[] argTypes, + Object[] args) throws Exception { Class cls = getEssentialClass(key); - return getInstance(key,cls,type,argTypes,args); + return getInstance(key, cls, type, argTypes, args); } - + /** - * this is our private instantiation workhorse - * try to instantiate an object of class 'cls' by using the following ordered set of ctors - * 1. <cls> (<argTypes>) - * 2. <cls> (Config) - * 3. <cls> () - * if all of that fails, or there was a 'type' provided the instantiated object does not - * comply with, return null + * this is our private instantiation workhorse try to instantiate an object of + * class 'cls' by using the following ordered set of ctors 1. <cls>( + * <argTypes>) 2. <cls>(Config) 3. <cls>() if all of that fails, or there was + * a 'type' provided the instantiated object does not comply with, return null */ - Object getInstance (String key, Class cls, Class type, - Class[] argTypes, Object[] args) throws Exception { + Object getInstance(String key, Class cls, Class type, Class[] argTypes, + Object[] args) throws Exception { Object o = null; Constructor ctor = null; - + if (cls == null) { return null; } - + do { try { - ctor = cls.getConstructor(argTypes); + ctor = cls.getConstructor(argTypes); o = ctor.newInstance(args); } catch (NoSuchMethodException nmx) { if (argTypes.length >= 1) { @@ -571,55 +596,56 @@ argTypes = new Class[1]; argTypes[0] = Config.class; args = new Object[1]; - args[0] = this; + args[0] = this; } else { // fallback 2: try the default ctor argTypes = new Class[0]; - args = new Object[0]; + args = new Object[0]; } } else { // Ok, there is no suitable ctor, bail out throw new Exception(key, cls, "no suitable ctor found"); } } catch (IllegalAccessException iacc) { - throw new Exception( key, cls, "\n> ctor not accessible: " + - getMethodSignature(ctor)); + throw new Exception(key, cls, "\n> ctor not accessible: " + + getMethodSignature(ctor)); } catch (IllegalArgumentException iarg) { - throw new Exception( key, cls, "\n> illegal constructor arguments: " + - getMethodSignature(ctor)); + throw new Exception(key, cls, "\n> illegal constructor arguments: " + + getMethodSignature(ctor)); } catch (InvocationTargetException ix) { Throwable tx = ix.getTargetException(); if (tx instanceof Config.Exception) { - throw new Exception( tx.getMessage() + - "\n> used within \"" + key + "\" instantiation of " - + cls); + throw new Exception(tx.getMessage() + "\n> used within \"" + key + + "\" instantiation of " + cls); } else { - throw new Exception( key, cls, "\n> exception in " + - getMethodSignature(ctor) + ":\n>> " + tx, tx); + throw new Exception(key, cls, "\n> exception in " + + getMethodSignature(ctor) + ":\n>> " + tx, tx); } } catch (InstantiationException ivt) { - throw new Exception( key, cls, "\n> abstract class cannot be instantiated"); + throw new Exception(key, cls, + "\n> abstract class cannot be instantiated"); } catch (ExceptionInInitializerError eie) { - throw new Exception( key, cls, "\n> static initialization failed:\n>> " + eie.getException(), - eie.getException()); + throw new Exception(key, cls, "\n> static initialization failed:\n>> " + + eie.getException(), eie.getException()); } } while (o == null); - + // check type if ((type != null) && !type.isInstance(o)) { - throw new Exception( key, cls, "\n> instance not of type: " + type.getName()); + throw new Exception(key, cls, "\n> instance not of type: " + + type.getName()); } - + return o; } - String getMethodSignature (Constructor ctor) { + String getMethodSignature(Constructor ctor) { StringBuffer sb = new StringBuffer(); sb.append(ctor.getName()); sb.append('('); Class[] argTypes = ctor.getParameterTypes(); - for (int i=0; i<argTypes.length; i++) { - if (i >0) { + for (int i = 0; i < argTypes.length; i++) { + if (i > 0) { sb.append(','); } sb.append(argTypes[i].getName()); @@ -627,66 +653,95 @@ sb.append(')'); return sb.toString(); } - + /** * check if any of the freeArgs matches a regular expression - * @param regex - regular expression to check for + * + * @param regex - + * regular expression to check for * @return true if found, false if not found or no freeArgs */ - public boolean hasArg (String regex) { - if (freeArgs == null) { - return false; - } - - for (int i=0; i<freeArgs.length; i++) { - if (freeArgs[i].matches(regex)) { - return true; - } - } - - return false; + public boolean hasArg(String regex) { + if (freeArgs == null) { + return false; + } + + for (int i = 0; i < freeArgs.length; i++) { + if (freeArgs[i].matches(regex)) { + return true; + } + } + + return false; } - public boolean hasValue (String key) { + public boolean hasValue(String key) { String v = getProperty(key); return ((v != null) && (v.length() > 0)); } - - public boolean hasValueIgnoreCase (String key, String value) { + + public boolean hasValueIgnoreCase(String key, String value) { String v = getProperty(key); if (v != null) { return v.equalsIgnoreCase(value); } - + return false; } - - public int getChoiceIndexIgnoreCase (String key, String[] choices) { + + public int getChoiceIndexIgnoreCase(String key, String[] choices) { String v = getProperty(key); - + if ((v != null) && (choices != null)) { - for (int i=0; i<choices.length; i++) { + for (int i = 0; i < choices.length; i++) { if (v.equalsIgnoreCase(choices[i])) { return i; } } } - + return -1; } - - public void printContents (PrintWriter ps) { - ps.println("----- config options -----"); - list(ps); - ps.println("----- free arguments -----"); - if (freeArgs == null) { - ps.println("<null>"); - } else { - for (int i=0; i<freeArgs.length; i++) { - ps.print(freeArgs[i]); - ps.print(' '); - } - ps.println(); - } + + public void print(Logger log) { + if (log.isLoggable(Level.CONFIG)) { + StringWriter sw = new StringWriter(1024); + PrintWriter pw = new PrintWriter(sw, true); + pw.println("----------- dictionary contents"); + + // just how much do you have to do to get a sorted printout :( + TreeSet kset = new TreeSet(); + for (Enumeration e = propertyNames(); e.hasMoreElements();) { + kset.add(e.nextElement()); + } + for (Iterator it = kset.iterator(); it.hasNext();) { + String key = (String) it.next(); + Object val = getProperty(key); + pw.print(key); + pw.print(" = "); + pw.println(val); + } + + if ((freeArgs != null) && (freeArgs.length > 0)) { + pw.println("----------- free arguments"); + for (int i = 0; i < freeArgs.length; i++) { + pw.println(freeArgs[i]); + } + } + + log.config(sw.toString()); + } + } + + public void printStatus(Logger log) { + log.config("configuration initialized from: " + getSourceName()); + + Config def = (Config) defaults; + if (def.source == null) { + log.warning("no defaults.properties found"); + } else { + log.config("default configuration initialized from: " + + def.getSourceName()); + } } } |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:57
|
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"); } } } |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:57
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jpf/java/lang In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/env/jpf/java/lang Modified Files: Class.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. Index: Class.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jpf/java/lang/Class.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- Class.java 5 May 2005 01:03:54 -0000 1.2 +++ Class.java 18 May 2005 06:41:46 -0000 1.3 @@ -24,6 +24,7 @@ import java.lang.reflect.Field; import java.lang.reflect.Method; import java.lang.reflect.Constructor; +import java.net.URL; /** * MJI model class for java.lang.Class library abstraction @@ -73,6 +74,10 @@ throw new JPFException("Class.getResourceAsStream() not yet supported"); } + public URL getResource (String name) { + throw new JPFException("Class.getResource() not yet supported"); + } + public Constructor getDeclaredConstructor (Class[] paramTypes) throws NoSuchMethodException, SecurityException { // <2do> |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:57
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jpf/java/io In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/env/jpf/java/io Modified Files: File.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. Index: File.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jpf/java/io/File.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- File.java 12 May 2005 06:25:31 -0000 1.2 +++ File.java 18 May 2005 06:41:46 -0000 1.3 @@ -22,6 +22,10 @@ /** * MJI model class for java.io.File * + * NOTE - a number of methods are only stubbed out here to make Eclipse compile + * JPF code that uses java.io.File (there is no way to tell Eclipse to exclude the + * model classes from ths build-path) + * * @author Owen O'Malley */ public class File @@ -49,8 +53,16 @@ return false; } - public void delete() {} + public boolean delete() { + // not yet + return true; + } + public boolean createNewFile () { + // not yet + return true; + } + public String getName() { return filename; } |
|
From: pcm <pcm...@us...> - 2005-05-18 06:41:56
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30521/src/gov/nasa/jpf/jvm Modified Files: RandomOrderScheduler.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. Index: RandomOrderScheduler.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/RandomOrderScheduler.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- RandomOrderScheduler.java 26 Apr 2005 19:44:04 -0000 1.1.1.1 +++ RandomOrderScheduler.java 18 May 2005 06:41:45 -0000 1.2 @@ -27,6 +27,9 @@ /** * scheduler that picks runnable threads in random order + * + * <2do> make this thing more efficient by using primitive types instead of + * BitSet */ public class RandomOrderScheduler extends Scheduler implements Cloneable { private static Random rand; |
|
From: Todd W. <tod...@us...> - 2005-05-17 14:03:04
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv22510/env/jvm/gov/nasa/jpf/jvm Modified Files: JPF_java_lang_Math.java Log Message: Added new MJI methods for java.lang.Math including asin, acos, atan, atan2, ceil, cos, floor, log, rint, sin, and tan. Only rudimentary testing was done but should work fine since they are just "pass-through" methods to the real Java library calls. Index: JPF_java_lang_Math.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- JPF_java_lang_Math.java 16 May 2005 18:33:14 -0000 1.3 +++ JPF_java_lang_Math.java 17 May 2005 14:02:55 -0000 1.4 @@ -85,4 +85,48 @@ public static double exp__D (MJIEnv env, int clsObjRef, double a) { return Math.exp(a); } + + public static double asin__D (MJIEnv env, int clsObjRef, double a) { + return Math.asin(a); + } + + public static double acos__D (MJIEnv env, int clsObjRef, double a) { + return Math.acos(a); + } + + public static double atan__D (MJIEnv env, int clsObjRef, double a) { + return Math.atan(a); + } + + public static double atan2__DD (MJIEnv env, int clsObjRef, double a, double b) { + return Math.atan2(a,b); + } + + public static double ceil__D (MJIEnv env, int clsObjRef, double a) { + return Math.ceil(a); + } + + public static double cos__D (MJIEnv env, int clsObjRef, double a) { + return Math.cos(a); + } + + public static double floor__D (MJIEnv env, int clsObjRef, double a) { + return Math.floor(a); + } + + public static double log__D (MJIEnv env, int clsObjRef, double a) { + return Math.log(a); + } + + public static double rint__D (MJIEnv env, int clsObjRef, double a) { + return Math.rint(a); + } + + public static double sin__D (MJIEnv env, int clsObjRef, double a) { + return Math.sin(a); + } + + public static double tan__D (MJIEnv env, int clsObjRef, double a) { + return Math.tan(a); + } } \ No newline at end of file |
|
From: Willem V. <wv...@us...> - 2005-05-17 03:11:23
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30968/env/jvm/gov/nasa/jpf/jvm Modified Files: JPF_java_lang_Math.java Log Message: * added Random to Math * so that our beloved dining Philosophers don't throw a fit :-) Index: JPF_java_lang_Math.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- JPF_java_lang_Math.java 26 Apr 2005 19:43:26 -0000 1.1.1.1 +++ JPF_java_lang_Math.java 16 May 2005 18:16:10 -0000 1.2 @@ -77,4 +77,8 @@ public static double sqrt__D (MJIEnv env, int clsObjRef, double a) { return Math.sqrt(a); } + + public static double random__ (MJIEnv env, int clsObjRef) { + return Math.random(); + } } \ No newline at end of file |
|
From: Willem V. <wv...@us...> - 2005-05-17 02:06:34
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3966/env/jvm/gov/nasa/jpf/jvm Modified Files: JPF_java_lang_Math.java Log Message: * added exp method per problem listed in the Forums Index: JPF_java_lang_Math.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- JPF_java_lang_Math.java 16 May 2005 18:16:10 -0000 1.2 +++ JPF_java_lang_Math.java 16 May 2005 18:33:14 -0000 1.3 @@ -81,4 +81,8 @@ public static double random__ (MJIEnv env, int clsObjRef) { return Math.random(); } + + public static double exp__D (MJIEnv env, int clsObjRef, double a) { + return Math.exp(a); + } } \ No newline at end of file |
|
From: John P. <joh...@us...> - 2005-05-16 21:26:23
|
Update of /cvsroot/javapathfinder//javapathfinder/bin In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30860/bin Modified Files: jpf.bat Log Message: small fix Index: jpf.bat =================================================================== RCS file: /cvsroot/javapathfinder//javapathfinder/bin/jpf.bat,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- jpf.bat 12 May 2005 06:25:31 -0000 1.3 +++ jpf.bat 16 May 2005 18:15:47 -0000 1.4 @@ -18,7 +18,7 @@ set CP=%CP%;%JPF_HOME%\build\test REM Otherwise, we look for the jar (binary distributions) -set %CP%;%JPF_HOME%\lib\jpf.jar +set CP=%CP%;%JPF_HOME%\lib\jpf.jar REM And these are the external libs we use at runtime REM (include the CLASSPATH first, in case somebody wants to use specific versions) |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:40
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219/src/gov/nasa/jpf Modified Files: Config.java JPF.java Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: JPF.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/JPF.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- JPF.java 11 May 2005 18:05:34 -0000 1.2 +++ JPF.java 12 May 2005 06:25:32 -0000 1.3 @@ -220,36 +220,54 @@ jpf.run(); } } - + /** - * answer the filename of the JPF properties file to use. If it's not - * specified via '-config', the default "jpf.properties" is used. + * find the value of an arg that is either specific as + * "-key=value" or as "-key value". If not found, the supplied + * defValue is returned */ - static String getConfigFileName(String[] args) { - String pf = "jpf.properties"; + static String getArg(String[] args, String pattern, String defValue, boolean consume) { + String s = defValue; for (int i = 0; i < args.length; i++) { String arg = args[i]; if (arg != null) { - - if (arg.matches("-c(onfig)?(=.+)?")) { + if (arg.matches(pattern)) { int idx=arg.indexOf('='); if (idx > 0) { - pf = arg.substring(idx+1); - args[i]=null; + s = arg.substring(idx+1); + if (consume) { + args[i]=null; + } } else if (i < args.length-1) { - pf = args[i+1]; - args[i] = null; - args[i+1] = null; + s = args[i+1]; + if (consume) { + args[i] = null; + args[i+1] = null; + } } break; } } } - return pf; + return s; } - + + /** + * what property file to look for + */ + static String getConfigFileName (String[] args) { + return getArg(args, "-c(onfig)?(=.+)?", "jpf.properties", true); + } + + /** + * where to look for the file (if it's not in the current dir) + */ + static String getRootDirName (String[] args) { + return getArg(args, "[+]jpf[.]basedir(=.+)?", null, false); // stupid compiler complaining about escape seq + } + /** * return a Config object that holds the JPF options. This first * loads the properties from a (potentially configured) properties file, and @@ -257,8 +275,9 @@ */ public static Config createConfig (String[] args) { String pf = getConfigFileName(args); + String rd = getRootDirName(args); - return new Config(args, pf, JPF.class); + return new Config(args, pf, rd, JPF.class); } /** Index: Config.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- Config.java 3 May 2005 03:31:59 -0000 1.2 +++ Config.java 12 May 2005 06:25:32 -0000 1.3 @@ -96,15 +96,15 @@ /** * this is our internal defaults ctor */ - private Config (Class codeBase) { - gotProperties = loadFile("default.properties", codeBase); + private Config (String alternatePath, Class codeBase) { + gotProperties = loadFile("default.properties", alternatePath, codeBase); } - public Config (String[] args, String fileName, Class codeBase) { - super( new Config(codeBase == null ? codeBase = getCallerClass(1) : codeBase)); + public Config (String[] args, String fileName, String alternatePath, Class codeBase) { + super(new Config( alternatePath, (codeBase == null) ? codeBase = getCallerClass(1) : codeBase)); this.fileName = fileName; - gotProperties = loadFile(fileName, codeBase); + gotProperties = loadFile(fileName, alternatePath, codeBase); processArgs(args); normalizeValues(); @@ -153,21 +153,28 @@ } } - boolean loadFile(String fileName, Class codeBase) { + boolean loadFile(String fileName, String alternatePath, Class codeBase) { InputStream is = null; try { // first, try to load from a file File f = new File(fileName); + if (!f.exists()) { + // Ok, try alternatePath, if fileName wasn't absolute + if (!f.isAbsolute() && (alternatePath != null)) { + f = new File(alternatePath, fileName); + } + } + if (f.exists()) { is = new FileInputStream(f); - Debug.println(Debug.MESSAGE, "reading config from file: " + fileName); - } else { + Debug.println(Debug.MESSAGE, "reading config from file: " + f.getAbsolutePath()); + } else { // if there is no file, try to load as a resource (jar) Class clazz = (codeBase != null) ? codeBase : Config.class; is = clazz.getResourceAsStream(fileName); if (is != null) { - Debug.println(Debug.MESSAGE, "reading config from resource: " + fileName); + Debug.println(Debug.MESSAGE, "reading config from resource: " + fileName); } } |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:40
|
Update of /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/mc In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219/test/gov/nasa/jpf/mc Modified Files: TestOldClassicJPF.java Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: TestOldClassicJPF.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/mc/TestOldClassicJPF.java,v retrieving revision 1.1 retrieving revision 1.2 diff -u -d -r1.1 -r1.2 --- TestOldClassicJPF.java 11 May 2005 21:43:21 -0000 1.1 +++ TestOldClassicJPF.java 12 May 2005 06:25:32 -0000 1.2 @@ -52,7 +52,7 @@ public void testCrossingNoHeuristic () { String[] args = { testClass }; - runJPFassertionError(args); + runJPFDeadlock(args); } /** @@ -63,7 +63,7 @@ String[] args = { "+search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch", "+search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic", testClass }; - runJPFassertionError(args); + runJPFDeadlock(args); } } |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:40
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219/src/gov/nasa/jpf/jvm Modified Files: ThreadInfo.java Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: ThreadInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadInfo.java,v retrieving revision 1.9 retrieving revision 1.10 diff -u -d -r1.9 -r1.10 --- ThreadInfo.java 10 May 2005 06:46:55 -0000 1.9 +++ ThreadInfo.java 12 May 2005 06:25:32 -0000 1.10 @@ -282,6 +282,8 @@ data = new int[0]; hasChanged = new BitSet(); + vm = JVM.getVM(); // <2do> cut this + env = new MJIEnv(this); // <2do> what about the other fields? |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:40
|
Update of /cvsroot/javapathfinder/javapathfinder/bin In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219/bin Modified Files: jpf jpf-dot jpf-dot.bat jpf.bat Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: jpf-dot.bat =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf-dot.bat,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- jpf-dot.bat 11 May 2005 18:05:34 -0000 1.2 +++ jpf-dot.bat 12 May 2005 06:25:31 -0000 1.3 @@ -46,4 +46,4 @@ REM StateSpaceDot tool options set SSDO=-show-source -transition-numbers -java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.tools.StateSpaceDot %SSDO% %1 %2 %3 %4 %5 %6 %7 %8 %9 +java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.tools.StateSpaceDot +jpf.basedir="%JPF_HOME%" %SSDO% %1 %2 %3 %4 %5 %6 %7 %8 %9 Index: jpf.bat =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf.bat,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- jpf.bat 11 May 2005 18:05:34 -0000 1.2 +++ jpf.bat 12 May 2005 06:25:31 -0000 1.3 @@ -42,4 +42,4 @@ set JVM_FLAGS=-Xmx1536m -java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.JPF %1 %2 %3 %4 %5 %6 %7 %8 %9 +java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.JPF +jpf.basedir="%JPF_HOME%" %1 %2 %3 %4 %5 %6 %7 %8 %9 Index: jpf-dot =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf-dot,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- jpf-dot 11 May 2005 18:05:34 -0000 1.4 +++ jpf-dot 12 May 2005 06:25:31 -0000 1.5 @@ -63,4 +63,4 @@ SSDOT_FLAGS="-show-source -transition-numbers" fi -java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.tools.StateSpaceDot $SSDOT_FLAGS $@ +java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.tools.StateSpaceDot +jpf.basedir="$JPF_HOME" $SSDOT_FLAGS $@ Index: jpf =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf,v retrieving revision 1.6 retrieving revision 1.7 diff -u -d -r1.6 -r1.7 --- jpf 11 May 2005 18:05:34 -0000 1.6 +++ jpf 12 May 2005 06:25:31 -0000 1.7 @@ -55,4 +55,4 @@ JVM_FLAGS="-Xmx1024m" fi -java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF $@ +java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF +jpf.basedir="$JPF_HOME" $@ |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:40
|
Update of /cvsroot/javapathfinder/javapathfinder/env/jpf/java/io In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219/env/jpf/java/io Modified Files: File.java Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: File.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/env/jpf/java/io/File.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- File.java 26 Apr 2005 19:43:25 -0000 1.1.1.1 +++ File.java 12 May 2005 06:25:31 -0000 1.2 @@ -55,6 +55,16 @@ return filename; } + public String getAbsolutePath () { + // not yet implemented + return null; + } + + public boolean isAbsolute() { + // not yet implemented + return false; + } + private String filename; } |
|
From: pcm <pcm...@us...> - 2005-05-12 06:25:39
|
Update of /cvsroot/javapathfinder/javapathfinder In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9219 Modified Files: default.properties Log Message: * added Config support for an alternate lookup dir, which should be used when JPF doesn't find a property file in the current dir, and before it tries to load the properties from resources. The dir is initialized from the +jpf.basedir=<dir> option, which is in turn now automatically set when using the bin/jpf script. This should make it easier to run JPF from within Eclipse, but outside its root dir (e.g. from where the application code resides) * hot fixed the BFSearch MJIEnv problem (ThreadInfo(ThreadData) ctor). THIS IS NOT YET THE REAL SOLUTION, since we want to get away from static references, but it buys us time to do the proper refactoring. Index: default.properties =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/default.properties,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- default.properties 7 May 2005 00:40:01 -0000 1.2 +++ default.properties 12 May 2005 06:25:31 -0000 1.3 @@ -98,7 +98,7 @@ vm.classpath = build/examples # where do we look for sources (defaults assume we start in the JPF root dir) -# vm.sourcepath = src:examples:test +vm.sourcepath = ${jpf.basedir}/src:${jpf.basedir}/examples:${jpf.basedir}/test # where to get atomicity and other code execution attributes from vm.attributor.class = gov.nasa.jpf.jvm.DefaultAttributor |
|
From: John P. <joh...@us...> - 2005-05-11 23:00:16
|
Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv14313/src/gov/nasa/jpf Removed Files: default.properties Log Message: get this thing out of here!!!! somehow ant is finding this and putting it into the build path! --- default.properties DELETED --- |
|
From: Willem V. <wv...@us...> - 2005-05-11 21:43:35
|
Update of /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/mc In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6731/test/gov/nasa/jpf/mc Added Files: oldclassic.java TestOldClassicJPF.java Log Message: * test for oldclassic in BFS --- NEW FILE: TestOldClassicJPF.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.mc; import gov.nasa.jpf.jvm.TestJPF; import junit.framework.TestSuite; import junit.textui.TestRunner; /** * JPF driver for breadth first search test */ public class TestOldClassicJPF extends TestJPF { static String testClass = "gov.nasa.jpf.mc.oldclassic"; public TestOldClassicJPF (String name) { super(name); } public static void main (String[] args) { TestRunner.run(suite()); } public static TestSuite suite () { return new TestSuite(TestOldClassicJPF.class); } /**************************** tests **********************************/ /** * Tests running the Crossing example with no heuristics, i.e., with the * default DFS. */ public void testCrossingNoHeuristic () { String[] args = { testClass }; runJPFassertionError(args); } /** * Tests running the Crossing example with BFS heuristic. */ public void testCrossingBFSHeuristic () { String[] args = { "+search.class=gov.nasa.jpf.search.heuristic.HeuristicSearch", "+search.heuristic.class=gov.nasa.jpf.search.heuristic.BFSHeuristic", testClass }; runJPFassertionError(args); } } --- NEW FILE: oldclassic.java --- package gov.nasa.jpf.mc; // // 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. // /** * This example shows a deadlock which occurs as a result of a missed signal. * It also contains an assertion check that shows the race violation that is the * cause for the missed signal (and ultimate deadlock) * @author wvisser */ public class oldclassic { public static void main (String[] args) { Event new_event1 = new Event(); Event new_event2 = new Event(); FirstTask task1 = new FirstTask(new_event1, new_event2); SecondTask task2 = new SecondTask(new_event1, new_event2); task1.start(); task2.start(); } } /** * DOCUMENT ME! */ class Event { int count = 0; public synchronized void signal_event () { count = (count + 1) % 3; notifyAll(); } public synchronized void wait_for_event () { try { wait(); } catch (InterruptedException e) { } ; } } /** * DOCUMENT ME! */ class FirstTask extends java.lang.Thread { Event event1; Event event2; int count = 0; public FirstTask (Event e1, Event e2) { this.event1 = e1; this.event2 = e2; } public void run () { count = event1.count; while (true) { if (count == event1.count) { assert (count == event1.count); event1.wait_for_event(); } count = event1.count; event2.signal_event(); } } } /** * DOCUMENT ME! */ class SecondTask extends java.lang.Thread { Event event1; Event event2; int count = 0; public SecondTask (Event e1, Event e2) { this.event1 = e1; this.event2 = e2; } public void run () { count = event2.count; while (true) { event1.signal_event(); if (count == event2.count) { assert (count == event2.count); event2.wait_for_event(); } count = event2.count; } } } |
|
From: Willem V. <wv...@us...> - 2005-05-11 21:43:12
|
Update of /cvsroot/javapathfinder/javapathfinder In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6487 Modified Files: build.xml Log Message: * added new run-test for BFS Index: build.xml =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/build.xml,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- build.xml 28 Apr 2005 21:08:02 -0000 1.3 +++ build.xml 11 May 2005 21:42:35 -0000 1.4 @@ -322,6 +322,7 @@ <include name="**/mc/TestVMDeadlockJPF.class"/> <include name="**/mc/TestRandomJPF.class"/> <include name="**/mc/TestCrossingJPF.class"/> + <include name="**/mc/TestOldClassicJPF.class"/> </fileset> </batchtest> </junit> |
