001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf;
020:
021: import gov.nasa.jpf.util.CoverageManager;
022: import gov.nasa.jpf.util.Debug;
023: import gov.nasa.jpf.util.LogManager;
024:
025: import java.io.PrintWriter;
026: import java.util.logging.Level;
027: import java.util.logging.Logger;
028:
029: /**
030: * main class of the JPF verification framework. This reads the configuration,
031: * instantiates the Search and VM objects, and kicks off the Search
032: */
033: public class JPF implements Runnable {
034:
035: /** JPF version, we read this inlater from default.properties */
036: static String VERSION = "3.?";
037:
038: static Logger logger;
039:
040: public Config config;
041:
042: /**
043: * the singleton driver object, so that we can override FactoryMethods
044: */
045: static JPF jpf;
046:
047: /**
048: * Reference to the virtual machine used by the model checker.
049: */
050: public VM vm;
051:
052: /**
053: * The search engine used to visit the state space.
054: */
055: public Search search;
056:
057: /**
058: * this is a pre-recorded path, NOT one freshly produced by a property
059: * violation
060: */
061: Path path;
062:
063: /**
064: * use this one to get a Logger that is initialized via our Config mechanism. Note that
065: * our own Loggers do NOT pass
066: */
067: public static Logger getLogger(String name) {
068: return LogManager.getLogger(name);
069: }
070:
071: /**
072: * create new JPF object. Note this is always guaranteed to return, but the
073: * Search and/or VM object instantiation might have failed (i.e. the JPF
074: * object might not be really usable). If you directly use getSearch() / getVM(),
075: * check for null
076: */
077: public JPF(Config conf) {
078: config = conf;
079:
080: try {
081: vm = (VM) config.getEssentialInstance("vm.class", VM.class);
082:
083: Class[] argTypes = { Config.class, VM.class };
084: Object[] args = { config, vm };
085: search = (Search) config.getEssentialInstance(
086: "search.class", Search.class, argTypes, args);
087:
088: addCombinedListeners();
089: } catch (Config.Exception cx) {
090: Debug.println(Debug.ERROR, cx);
091: }
092: }
093:
094: public boolean isRunnable() {
095: return ((vm != null) && (search != null));
096: }
097:
098: public void addSearchListener(SearchListener l) {
099: if (search != null) {
100: search.addListener(l);
101: }
102: }
103:
104: public void addVMListener(VMListener l) {
105: if (vm != null) {
106: vm.addListener(l);
107: }
108: }
109:
110: public void addSearchProperty(Property p) {
111: if (search != null) {
112: search.addProperty(p);
113: }
114: }
115:
116: // add all combined listeners
117: void addCombinedListeners() throws Config.Exception {
118: Object[] listeners = config.getInstances("jpf.listener",
119: JPFListener.class);
120: if (listeners != null) {
121: for (int i = 0; i < listeners.length; i++) {
122: if (listeners[i] instanceof VMListener) {
123: if (vm != null) {
124: vm.addListener((VMListener) listeners[i]);
125: }
126: }
127: if (listeners[i] instanceof SearchListener) {
128: if (search != null) {
129: search
130: .addListener((SearchListener) listeners[i]);
131: }
132: }
133: }
134: }
135: }
136:
137: /**
138: * return the search object. This can be null if the initialization has failed
139: */
140: public Search getSearch() {
141: return search;
142: }
143:
144: /**
145: * return the VM object. This can be null if the initialization has failed
146: */
147: public VM getVM() {
148: return vm;
149: }
150:
151: public static void exit() {
152: // Hmm, exception as non local return. But we might be called from a
153: // context we don't want to kill
154: throw new ExitException();
155: }
156:
157: public boolean foundErrors() {
158: return !(search.getErrors().isEmpty());
159: }
160:
161: static boolean isHelpRequest(String[] args) {
162: if (args == null)
163: return true;
164: if (args.length == 0)
165: return true;
166:
167: for (int i = 0; i < args.length; i++) {
168: if ("-help".equals(args[i])) {
169: args[i] = null;
170: return true;
171: }
172: }
173:
174: return false;
175: }
176:
177: static boolean isPrintConfigRequest(String[] args) {
178: if (args == null)
179: return false;
180:
181: for (int i = 0; i < args.length; i++) {
182: if ("-show".equals(args[i])) {
183: args[i] = null;
184: return true;
185: }
186: }
187: return false;
188: }
189:
190: /**
191: * this assumes that we have checked and 'consumed' (nullified) all known
192: * options, so we just have to check for any '-' option prior to the
193: * target class name
194: */
195: static void checkUnknownArgs(String[] args) {
196: for (int i = 0; i < args.length; i++) {
197: if (args[i] != null) {
198: if (args[i].charAt(0) == '-') {
199: logger.warning("unknown command line option: "
200: + args[i]);
201: } else {
202: // this is supposed to be the target class name - everything that follows
203: // is supposed to be processed by the program under test
204: break;
205: }
206: }
207: }
208: }
209:
210: public static void printBanner(Config config) {
211: if (logger.isLoggable(Level.INFO)) {
212: logger
213: .info("Java Pathfinder Model Checker v"
214: + config.getString("jpf.version", "3.1x")
215: + " - (C) 1999-2005 RIACS/NASA Ames Research Center");
216: }
217: }
218:
219: public static void main(String[] args) {
220: Config conf = createConfig(args);
221: LogManager.init(conf);
222: logger = getLogger("gov.nasa.jpf");
223:
224: printBanner(conf);
225:
226: LogManager.printStatus(logger);
227: conf.printStatus(logger);
228:
229: if (isHelpRequest(args)) {
230: showUsage();
231: }
232:
233: if (isPrintConfigRequest(args)) {
234: conf.print(new PrintWriter(System.out));
235: }
236:
237: if (conf.getTargetArg() != null) {
238: checkUnknownArgs(args);
239:
240: JPF jpf = new JPF(conf);
241: jpf.run();
242: }
243: }
244:
245: /**
246: * find the value of an arg that is either specific as
247: * "-key=value" or as "-key value". If not found, the supplied
248: * defValue is returned
249: */
250: static String getArg(String[] args, String pattern,
251: String defValue, boolean consume) {
252: String s = defValue;
253:
254: for (int i = 0; i < args.length; i++) {
255: String arg = args[i];
256:
257: if (arg != null) {
258: if (arg.matches(pattern)) {
259: int idx = arg.indexOf('=');
260: if (idx > 0) {
261: s = arg.substring(idx + 1);
262: if (consume) {
263: args[i] = null;
264: }
265: } else if (i < args.length - 1) {
266: s = args[i + 1];
267: if (consume) {
268: args[i] = null;
269: args[i + 1] = null;
270: }
271: }
272: break;
273: }
274: }
275: }
276: return s;
277: }
278:
279: /**
280: * what property file to look for
281: */
282: static String getConfigFileName(String[] args) {
283: return getArg(args, "-c(onfig)?(=.+)?", "jpf.properties", true);
284: }
285:
286: /**
287: * where to look for the file (if it's not in the current dir)
288: */
289: static String getRootDirName(String[] args) {
290: return getArg(args, "[+]jpf[.]basedir(=.+)?", null, false); // stupid compiler complaining about escape seq
291: }
292:
293: /**
294: * return a Config object that holds the JPF options. This first
295: * loads the properties from a (potentially configured) properties file, and
296: * then overlays all command line arguments that are key/value pairs
297: */
298: public static Config createConfig(String[] args) {
299: String pf = getConfigFileName(args);
300: String rd = getRootDirName(args);
301:
302: return new Config(args, pf, rd, JPF.class);
303: }
304:
305: /**
306: * runs the verification.
307: */
308: public void run() {
309: if (isRunnable()) {
310: try {
311: if (vm.initialize()) {
312: search.search();
313: printResults();
314: }
315: } catch (ExitException ex) {
316: Debug.println(Debug.WARNING, "JPF terminated");
317: } catch (JPFException jx) {
318: Debug.println(Debug.ERROR,
319: "JPF exception, terminating: "
320: + jx.getMessage());
321: if (config.getBoolean("jpf.print_exception_stack")) {
322: Debug.println(Debug.ERROR);
323: jx.printStackTrace();
324: }
325: // bail here
326: } catch (Throwable t) {
327: // the last line of defense
328: t.printStackTrace();
329: }
330: }
331: }
332:
333: public ErrorList getSearchErrors() {
334: if (search != null) {
335: return search.getErrors();
336: }
337:
338: return null;
339: }
340:
341: static void showUsage() {
342: System.out
343: .println("Usage: \"java [<vm-option>..] gov.nasa.jpf.JPF [<jpf-option>..] [<app> [<app-arg>..]]");
344: System.out
345: .println(" <jpf-option> : -c <config-file> : name of config properties file (default \"jpf.properties\")");
346: System.out
347: .println(" | -help : print usage information");
348: System.out
349: .println(" | -show : print configuration dictionary contents");
350: System.out
351: .println(" | +<key>=<value> : add or override key/value pair to config dictionary");
352: System.out
353: .println(" <app> : application class or *.xml error trace file");
354: System.out
355: .println(" <app-arg> : arguments passed into main(String[]) if application class");
356: }
357:
358: /**
359: * Prints the results of the verification.
360: *
361: * <2do>pcm - we have to unify the result output, Debug is the wrong place
362: * for this
363: */
364: private void printResults() {
365: ErrorList errors = search.getErrors();
366:
367: // let the VM report whatever it has to (and we don't know about
368: vm.printResults(new PrintWriter(System.out, true));
369:
370: Debug.println(Debug.ERROR);
371: Debug.println(Debug.ERROR);
372: Debug.println(Debug.ERROR,
373: "===================================");
374:
375: int nerrors = errors.size();
376:
377: if (nerrors == 0) {
378: Debug.println(Debug.ERROR, " No Errors Found");
379: } else if (nerrors == 1) {
380: Debug.println(Debug.ERROR, " 1 Error Found: "
381: + errors.getError(0).getMessage());
382: } else {
383: Debug
384: .println(Debug.ERROR, " " + nerrors
385: + " Errors Found");
386: }
387:
388: Debug.println(Debug.ERROR,
389: "===================================");
390: Debug.println(Debug.ERROR);
391:
392: // <2do> how do we get the statistics here, now that they are just
393: // observers?
394:
395: CoverageManager.printResults();
396: }
397:
398: public static void handleException(JPFException e) {
399: Debug.println(Debug.ERROR, "jpf: " + e.getMessage());
400:
401: if (e instanceof JPFException) {
402: Debug.println(Debug.ERROR);
403: e.printStackTrace();
404: }
405:
406: exit();
407: }
408:
409: /**
410: * private helper class for local termination of JPF (without killing the
411: * whole Java process via System.exit).
412: * While this is basically a bad non-local goto exception, it seems to be the
413: * least of evils given the current JPF structure, and the need to terminate
414: * w/o exiting the whole Java process. If we just do a System.exit(), we couldn't
415: * use JPF in an embedded context
416: */
417: static class ExitException extends RuntimeException {
418: ExitException() {
419: }
420:
421: ExitException(String msg) {
422: super(msg);
423: }
424: }
425: }
|