KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > JPF


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // directory tree for the complete NOSA document.
10 //
11 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18 //
19 package gov.nasa.jpf;
20
21 import gov.nasa.jpf.util.CoverageManager;
22 import gov.nasa.jpf.util.Debug;
23 import gov.nasa.jpf.util.LogManager;
24
25 import java.io.PrintWriter JavaDoc;
26 import java.util.logging.Level JavaDoc;
27 import java.util.logging.Logger JavaDoc;
28
29
30 /**
31  * main class of the JPF verification framework. This reads the configuration,
32  * instantiates the Search and VM objects, and kicks off the Search
33  */
34 public class JPF implements Runnable JavaDoc {
35
36   /** JPF version, we read this inlater from default.properties */
37   static String JavaDoc VERSION = "3.?";
38
39   static Logger JavaDoc logger;
40   
41   public Config config;
42
43   /**
44    * the singleton driver object, so that we can override FactoryMethods
45    */
46   static JPF jpf;
47
48   /**
49    * Reference to the virtual machine used by the model checker.
50    */
51   public VM vm;
52
53   /**
54    * The search engine used to visit the state space.
55    */
56   public Search search;
57
58   /**
59    * this is a pre-recorded path, NOT one freshly produced by a property
60    * violation
61    */
62   Path path;
63
64
65   /**
66    * use this one to get a Logger that is initialized via our Config mechanism. Note that
67    * our own Loggers do NOT pass
68    */
69   public static Logger JavaDoc getLogger (String JavaDoc name) {
70     return LogManager.getLogger( name);
71   }
72   
73   /**
74    * create new JPF object. Note this is always guaranteed to return, but the
75    * Search and/or VM object instantiation might have failed (i.e. the JPF
76    * object might not be really usable). If you directly use getSearch() / getVM(),
77    * check for null
78    */
79   public JPF(Config conf) {
80     config = conf;
81
82     try {
83       vm = (VM) config.getEssentialInstance("vm.class", VM.class);
84       
85       Class JavaDoc[] argTypes = { Config.class, VM.class };
86       Object JavaDoc[] args = { config, vm };
87       search = (Search) config.getEssentialInstance("search.class", Search.class, argTypes, args);
88       
89       addCombinedListeners();
90     } catch (Config.Exception cx) {
91       Debug.println(Debug.ERROR, cx);
92     }
93   }
94
95   public boolean isRunnable () {
96     return ((vm != null) && (search != null));
97   }
98   
99   public void addSearchListener (SearchListener l) {
100     if (search != null) {
101       search.addListener(l);
102     }
103   }
104   
105   public void addVMListener (VMListener l) {
106     if (vm != null) {
107       vm.addListener(l);
108     }
109   }
110
111   public void addSearchProperty (Property p) {
112     if (search != null) {
113       search.addProperty(p);
114     }
115   }
116   
117   // add all combined listeners
118 void addCombinedListeners () throws Config.Exception {
119     Object JavaDoc[] listeners = config.getInstances("jpf.listener", 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.addListener( (SearchListener) listeners[i]);
130           }
131         }
132       }
133     }
134   }
135   
136   /**
137    * return the search object. This can be null if the initialization has failed
138    */
139   public Search getSearch() {
140     return search;
141   }
142
143   /**
144    * return the VM object. This can be null if the initialization has failed
145    */
146   public VM getVM() {
147     return vm;
148   }
149   
150   public static void exit() {
151     // Hmm, exception as non local return. But we might be called from a
152 // context we don't want to kill
153 throw new ExitException();
154   }
155
156   public boolean foundErrors() {
157     return !(search.getErrors().isEmpty());
158   }
159
160
161   static boolean isHelpRequest (String JavaDoc[] args) {
162     if (args == null) return true;
163     if (args.length == 0) return true;
164     
165     for (int i=0; i<args.length; i++) {
166       if ("-help".equals(args[i])) {
167         args[i] = null;
168         return true;
169       }
170     }
171     
172     return false;
173   }
174   
175   static boolean isPrintConfigRequest(String JavaDoc[] args) {
176     if (args == null) return false;
177     
178     for (int i=0; i<args.length; i++) {
179       if ("-show".equals(args[i])) {
180         args[i] = null;
181         return true;
182       }
183     }
184     return false;
185   }
186     
187   /**
188    * this assumes that we have checked and 'consumed' (nullified) all known
189    * options, so we just have to check for any '-' option prior to the
190    * target class name
191    */
192   static void checkUnknownArgs (String JavaDoc[] args) {
193     for ( int i=0; i<args.length; i++) {
194       if (args[i] != null) {
195         if (args[i].charAt(0) == '-') {
196           logger.warning("unknown command line option: " + args[i]);
197         }
198         else {
199           // this is supposed to be the target class name - everything that follows
200 // is supposed to be processed by the program under test
201 break;
202         }
203       }
204     }
205   }
206   
207   public static void printBanner (Config config) {
208     if (logger.isLoggable(Level.INFO)) {
209       logger.info("Java Pathfinder Model Checker v" +
210                   config.getString("jpf.version", "3.1x") +
211                   " - (C) 1999-2005 RIACS/NASA Ames Research Center");
212     }
213   }
214   
215   
216   public static void main(String JavaDoc[] args) {
217     Config conf = createConfig(args);
218     LogManager.init(conf);
219     logger = getLogger("gov.nasa.jpf");
220
221     printBanner(conf);
222     
223     LogManager.printStatus(logger);
224     conf.printStatus(logger);
225     
226     if (isHelpRequest(args)) {
227       showUsage();
228     }
229     
230     if (isPrintConfigRequest(args)) {
231       conf.print(new PrintWriter JavaDoc(System.out));
232     }
233     
234     if (conf.getTargetArg() != null) {
235       checkUnknownArgs(args);
236       
237       JPF jpf = new JPF(conf);
238       jpf.run();
239     }
240   }
241
242   /**
243    * find the value of an arg that is either specific as
244    * "-key=value" or as "-key value". If not found, the supplied
245    * defValue is returned
246    */
247   static String JavaDoc getArg(String JavaDoc[] args, String JavaDoc pattern, String JavaDoc defValue, boolean consume) {
248     String JavaDoc s = defValue;
249
250     for (int i = 0; i < args.length; i++) {
251       String JavaDoc arg = args[i];
252
253       if (arg != null) {
254         if (arg.matches(pattern)) {
255           int idx=arg.indexOf('=');
256           if (idx > 0) {
257             s = arg.substring(idx+1);
258             if (consume) {
259               args[i]=null;
260             }
261           } else if (i < args.length-1) {
262             s = args[i+1];
263             if (consume) {
264               args[i] = null;
265               args[i+1] = null;
266             }
267           }
268           break;
269         }
270       }
271     }
272     return s;
273   }
274   
275   /**
276    * what property file to look for
277    */
278   static String JavaDoc getConfigFileName (String JavaDoc[] args) {
279     return getArg(args, "-c(onfig)?(=.+)?", "jpf.properties", true);
280   }
281   
282   /**
283    * where to look for the file (if it's not in the current dir)
284    */
285   static String JavaDoc getRootDirName (String JavaDoc[] args) {
286     return getArg(args, "[+]jpf[.]basedir(=.+)?", null, false); // stupid compiler complaining about escape seq
287 }
288   
289   /**
290    * return a Config object that holds the JPF options. This first
291    * loads the properties from a (potentially configured) properties file, and
292    * then overlays all command line arguments that are key/value pairs
293    */
294   public static Config createConfig (String JavaDoc[] args) {
295     String JavaDoc pf = getConfigFileName(args);
296     String JavaDoc rd = getRootDirName(args);
297
298     return new Config(args, pf, rd, JPF.class);
299   }
300   
301   /**
302    * runs the verification.
303    */
304   public void run() {
305     if (isRunnable()) {
306       try {
307         if (vm.initialize()) {
308           search.search();
309           printResults();
310         }
311       } catch (ExitException ex) {
312         Debug.println(Debug.WARNING, "JPF terminated");
313       } catch (JPFException jx) {
314         Debug.println(Debug.ERROR, "JPF exception, terminating: " + jx.getMessage());
315         if (config.getBoolean("jpf.print_exception_stack")) {
316           Debug.println(Debug.ERROR);
317           jx.printStackTrace();
318         }
319         // bail here
320 } catch (Throwable JavaDoc t) {
321         // the last line of defense
322 t.printStackTrace();
323       }
324     }
325   }
326
327   public ErrorList getSearchErrors () {
328     if (search != null) {
329       return search.getErrors();
330     }
331     
332     return null;
333   }
334   
335   static void showUsage() {
336     System.out
337         .println("Usage: \"java [<vm-option>..] gov.nasa.jpf.JPF [<jpf-option>..] [<app> [<app-arg>..]]");
338     System.out.println(" <jpf-option> : -c <config-file> : name of config properties file (default \"jpf.properties\")");
339     System.out.println(" | -help : print usage information");
340     System.out.println(" | -show : print configuration dictionary contents");
341     System.out.println(" | +<key>=<value> : add or override key/value pair to config dictionary");
342     System.out.println(" <app> : application class or *.xml error trace file");
343     System.out.println(" <app-arg> : arguments passed into main(String[]) if application class");
344   }
345
346   /**
347    * Prints the results of the verification.
348    *
349    * <2do>pcm - we have to unify the result output, Debug is the wrong place
350    * for this
351    */
352   private void printResults() {
353     ErrorList errors = search.getErrors();
354
355     // let the VM report whatever it has to (and we don't know about
356 vm.printResults(new PrintWriter JavaDoc(System.out, true));
357
358     Debug.println(Debug.ERROR);
359     Debug.println(Debug.ERROR);
360     Debug.println(Debug.ERROR, "===================================");
361
362     int nerrors = errors.size();
363
364     if (nerrors == 0) {
365       Debug.println(Debug.ERROR, " No Errors Found");
366     } else if (nerrors == 1) {
367       Debug.println(Debug.ERROR, " 1 Error Found: "
368           + errors.getError(0).getMessage());
369     } else {
370       Debug.println(Debug.ERROR, " " + nerrors + " Errors Found");
371     }
372
373     Debug.println(Debug.ERROR, "===================================");
374     Debug.println(Debug.ERROR);
375
376     // <2do> how do we get the statistics here, now that they are just
377 // observers?
378
379     CoverageManager.printResults();
380   }
381
382   public static void handleException(JPFException e) {
383     Debug.println(Debug.ERROR, "jpf: " + e.getMessage());
384
385     if (e instanceof JPFException) {
386       Debug.println(Debug.ERROR);
387       e.printStackTrace();
388     }
389
390     exit();
391   }
392
393   /**
394    * private helper class for local termination of JPF (without killing the
395    * whole Java process via System.exit).
396    * While this is basically a bad non-local goto exception, it seems to be the
397    * least of evils given the current JPF structure, and the need to terminate
398    * w/o exiting the whole Java process. If we just do a System.exit(), we couldn't
399    * use JPF in an embedded context
400    */
401   static class ExitException extends RuntimeException JavaDoc {
402     ExitException() {
403     }
404
405     ExitException(String JavaDoc msg) {
406       super(msg);
407     }
408   }
409 }
Popular Tags