2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
20 import gov.nasa.jpf.report.Publisher;
21 import gov.nasa.jpf.report.PublisherExtension;
22 import gov.nasa.jpf.report.Reporter;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.search.SearchListener;
25 import gov.nasa.jpf.tool.RunJPF;
26 import gov.nasa.jpf.util.JPFLogger;
27 import gov.nasa.jpf.util.LogManager;
28 import gov.nasa.jpf.util.Misc;
29 import gov.nasa.jpf.util.RunRegistry;
30 import gov.nasa.jpf.vm.VM;
31 import gov.nasa.jpf.vm.NoOutOfMemoryErrorProperty;
32 import gov.nasa.jpf.vm.VMListener;
35 import java.util.ArrayList;
36 import java.util.List;
37 import java.util.logging.Logger;
41 * main class of the JPF verification framework. This reads the configuration,
42 * instantiates the Search and VM objects, and kicks off the Search
44 public class JPF implements Runnable {
46 public static String VERSION = "8.0"; // the major version number
48 static Logger logger = null; // initially
50 public enum Status { NEW, RUNNING, DONE };
52 class ConfigListener implements ConfigChangeListener {
55 * check for new listeners that are dynamically configured
58 public void propertyChanged(Config config, String key, String oldValue, String newValue) {
59 if ("listener".equals(key)) {
63 String[] nv = config.asStringArray(newValue);
64 String[] ov = config.asStringArray(oldValue);
65 String[] newListeners = Misc.getAddedElements(ov, nv);
66 Class<?>[] argTypes = { Config.class, JPF.class }; // Many listeners have 2 parameter constructors
67 Object[] args = {config, JPF.this };
69 if (newListeners != null) {
70 for (String clsName : newListeners) {
72 JPFListener newListener = config.getInstance("listener", clsName, JPFListener.class, argTypes, args);
73 addListener(newListener);
74 logger.info("config changed, added listener " + clsName);
76 } catch (JPFConfigException cfx) {
77 logger.warning("listener change failed: " + cfx.getMessage());
85 * clean up to avoid a sublte but serious memory leak when using the
86 * same config for multiple JPF objects/runs - this listener is an inner
87 * class object that keeps its encapsulating JPF instance alive
90 public void jpfRunTerminated(Config config){
91 config.removeChangeListener(this);
95 /** this is the backbone of all JPF configuration */
98 /** The search policy used to explore the state space */
101 /** Reference to the virtual machine used by the search */
104 /** the report generator */
107 Status status = Status.NEW;
109 /** a list of listeners that get automatically added from VM, Search or Reporter initialization */
110 List<VMListener> pendingVMListeners;
111 List<SearchListener> pendingSearchListeners;
114 /** we use this as safety margin, to be released upon OutOfMemoryErrors */
115 byte[] memoryReserve;
117 private static Logger initLogging(Config conf) {
118 LogManager.init(conf);
119 return getLogger("gov.nasa.jpf");
123 * use this one to get a Logger that is initialized via our Config mechanism. Note that
124 * our own Loggers do NOT pass
126 public static JPFLogger getLogger (String name) {
127 return LogManager.getLogger( name);
130 public static void main(String[] args){
131 int options = RunJPF.getOptions(args);
133 if (args.length == 0 || RunJPF.isOptionEnabled( RunJPF.HELP,options)) {
137 if (RunJPF.isOptionEnabled( RunJPF.ADD_PROJECT,options)){
138 RunJPF.addProject(args);
142 if (RunJPF.isOptionEnabled( RunJPF.BUILD_INFO,options)){
143 RunJPF.showBuild(RunJPF.class.getClassLoader());
146 if (RunJPF.isOptionEnabled( RunJPF.LOG,options)){
147 Config.enableLogging(true);
150 Config conf = createConfig(args);
152 if (RunJPF.isOptionEnabled( RunJPF.SHOW, options)) {
159 public static void start(Config conf, String[] args){
160 // this is redundant to jpf.report.<publisher>.start=..config..
161 // but nobody can remember this (it's only used to produce complete reports)
163 if (logger == null) {
164 logger = initLogging(conf);
167 if (!checkArgs(args)){
171 setNativeClassPath(conf); // in case we have to find a shell
173 // check if there is a shell class specification, in which case we just delegate
174 JPFShell shell = conf.getInstance("shell", JPFShell.class);
176 shell.start(args); // responsible for exception handling itself
179 // no shell, we start JPF directly
180 LogManager.printStatus(logger);
181 conf.printStatus(logger);
183 // this has to be done after we checked&consumed all "-.." arguments
184 // this is NOT about checking properties!
185 checkUnknownArgs(args);
188 JPF jpf = new JPF(conf);
191 } catch (ExitException x) {
192 logger.severe( "JPF terminated");
194 // this is how we get most runtime config exceptions
195 if (x.shouldReport()) {
200 Throwable cause = x.getCause();
201 if ((cause != null) && conf.getBoolean("pass_exceptions", false)) {
202 cause.fillInStackTrace();
207 } catch (JPFException jx) {
208 logger.severe( "JPF exception, terminating: " + jx.getMessage());
209 if (conf.getBoolean("jpf.print_exception_stack")) {
211 Throwable cause = jx.getCause();
212 if (cause != null && cause != jx){
213 cause.printStackTrace();
215 jx.printStackTrace();
218 // pass this on, caller has to handle
225 static void setNativeClassPath(Config config) {
226 if (!config.hasSetClassLoader()) {
227 config.initClassLoader( JPF.class.getClassLoader());
233 // just to support unit test mockups
237 * create new JPF object. Note this is always guaranteed to return, but the
238 * Search and/or VM object instantiation might have failed (i.e. the JPF
239 * object might not be really usable). If you directly use getSearch() / getVM(),
242 public JPF(Config conf) {
245 setNativeClassPath(config); // before we do anything else
247 if (logger == null) { // maybe somebody created a JPF object explicitly
248 logger = initLogging(config);
255 * convenience method if caller doesn't care about Config
257 public JPF (String ... args) {
258 this( createConfig(args));
261 private void initialize() {
262 VERSION = config.getString("jpf.version", VERSION);
263 memoryReserve = new byte[config.getInt("jpf.memory_reserve", 64 * 1024)]; // in bytes
267 Class<?>[] vmArgTypes = { JPF.class, Config.class };
268 Object[] vmArgs = { this, config };
269 vm = config.getEssentialInstance("vm.class", VM.class, vmArgTypes, vmArgs);
271 Class<?>[] searchArgTypes = { Config.class, VM.class };
272 Object[] searchArgs = { config, vm };
273 search = config.getEssentialInstance("search.class", Search.class,
274 searchArgTypes, searchArgs);
276 // although the Reporter will always be notified last, this has to be set
277 // first so that it can register utility listeners like Statistics that
278 // can be used by configured listeners
279 Class<?>[] reporterArgTypes = { Config.class, JPF.class };
280 Object[] reporterArgs = { config, this };
281 reporter = config.getInstance("report.class", Reporter.class, reporterArgTypes, reporterArgs);
282 if (reporter != null){
283 search.setReporter(reporter);
288 config.addChangeListener(new ConfigListener());
290 } catch (JPFConfigException cx) {
291 logger.severe(cx.toString());
292 //cx.getCause().printStackTrace();
293 throw new ExitException(false, cx);
298 public Status getStatus() {
302 public boolean isRunnable () {
303 return ((vm != null) && (search != null));
306 public void addPropertyListener (PropertyListenerAdapter pl) {
310 if (search != null) {
311 search.addListener( pl);
312 search.addProperty(pl);
316 public void addSearchListener (SearchListener l) {
317 if (search != null) {
318 search.addListener(l);
322 protected void addPendingVMListener (VMListener l){
323 if (pendingVMListeners == null){
324 pendingVMListeners = new ArrayList<VMListener>();
326 pendingVMListeners.add(l);
329 protected void addPendingSearchListener (SearchListener l){
330 if (pendingSearchListeners == null){
331 pendingSearchListeners = new ArrayList<SearchListener>();
333 pendingSearchListeners.add(l);
336 public void addListener (JPFListener l) {
337 // the VM is instantiated first
338 if (l instanceof VMListener) {
340 vm.addListener( (VMListener) l);
342 } else { // no VM yet, we are in VM initialization
343 addPendingVMListener((VMListener)l);
347 if (l instanceof SearchListener) {
348 if (search != null) {
349 search.addListener( (SearchListener) l);
351 } else { // no search yet, we are in Search initialization
352 addPendingSearchListener((SearchListener)l);
357 public <T> T getListenerOfType( Class<T> type){
359 T listener = search.getNextListenerOfType(type, null);
360 if (listener != null){
366 T listener = vm.getNextListenerOfType(type, null);
367 if (listener != null){
375 public boolean addUniqueTypeListener (JPFListener l) {
376 boolean addedListener = false;
377 Class<?> cls = l.getClass();
379 if (l instanceof VMListener) {
381 if (!vm.hasListenerOfType(cls)) {
382 vm.addListener( (VMListener) l);
383 addedListener = true;
387 if (l instanceof SearchListener) {
388 if (search != null) {
389 if (!search.hasListenerOfType(cls)) {
390 search.addListener( (SearchListener) l);
391 addedListener = true;
396 return addedListener;
400 public void removeListener (JPFListener l){
401 if (l instanceof VMListener) {
403 vm.removeListener( (VMListener) l);
406 if (l instanceof SearchListener) {
407 if (search != null) {
408 search.removeListener( (SearchListener) l);
413 public void addVMListener (VMListener l) {
419 public void addSearchProperty (Property p) {
420 if (search != null) {
421 search.addProperty(p);
426 * this is called after vm, search and reporter got instantiated
428 void addListeners () {
429 Class<?>[] argTypes = { Config.class, JPF.class };
430 Object[] args = { config, this };
432 // first listeners that were automatically added from VM, Search and Reporter initialization
433 if (pendingVMListeners != null){
434 for (VMListener l : pendingVMListeners) {
437 pendingVMListeners = null;
440 if (pendingSearchListeners != null){
441 for (SearchListener l : pendingSearchListeners) {
442 search.addListener(l);
444 pendingSearchListeners = null;
447 // and finally everything that's user configured
448 List<JPFListener> listeners = config.getInstances("listener", JPFListener.class, argTypes, args);
449 if (listeners != null) {
450 for (JPFListener l : listeners) {
456 public Reporter getReporter () {
460 public <T extends Publisher> boolean addPublisherExtension (Class<T> pCls, PublisherExtension e) {
461 if (reporter != null) {
462 return reporter.addPublisherExtension(pCls, e);
467 public <T extends Publisher> void setPublisherItems (Class<T> pCls,
468 int category, String[] topics) {
469 if (reporter != null) {
470 reporter.setPublisherItems(pCls, category, topics);
475 public Config getConfig() {
480 * return the search object. This can be null if the initialization has failed
482 public Search getSearch() {
487 * return the VM object. This can be null if the initialization has failed
493 public static void exit() {
494 // Hmm, exception as non local return. But we might be called from a
495 // context we don't want to kill
496 throw new ExitException();
499 public boolean foundErrors() {
500 return !(search.getErrors().isEmpty());
504 * this assumes that we have checked and 'consumed' (nullified) all known
505 * options, so we just have to check for any '-' option prior to the
508 static void checkUnknownArgs (String[] args) {
509 for ( int i=0; i<args.length; i++) {
510 if (args[i] != null) {
511 if (args[i].charAt(0) == '-') {
512 logger.warning("unknown command line option: " + args[i]);
515 // this is supposed to be the target class name - everything that follows
516 // is supposed to be processed by the program under test
523 public static void printBanner (Config config) {
524 System.out.println("Java Pathfinder core system v" +
525 config.getString("jpf.version", VERSION) +
526 " - (C) 2005-2014 United States Government. All rights reserved.");
531 * find the value of an arg that is either specific as
532 * "-key=value" or as "-key value". If not found, the supplied
533 * defValue is returned
535 static String getArg(String[] args, String pattern, String defValue, boolean consume) {
539 for (int i = 0; i < args.length; i++) {
540 String arg = args[i];
543 if (arg.matches(pattern)) {
544 int idx=arg.indexOf('=');
546 s = arg.substring(idx+1);
550 } else if (i < args.length-1) {
567 * what property file to look for
569 static String getConfigFileName (String[] args) {
570 if (args.length > 0) {
571 // check if the last arg is a mode property file
572 // if yes, it has to include a 'target' spec
573 int idx = args.length-1;
574 String lastArg = args[idx];
575 if (lastArg.endsWith(".jpf") || lastArg.endsWith(".properties")) {
576 if (lastArg.startsWith("-c")) {
577 int i = lastArg.indexOf('=');
579 lastArg = lastArg.substring(i+1);
587 return getArg(args, "-c(onfig)?(=.+)?", "jpf.properties", true);
591 * return a Config object that holds the JPF options. This first
592 * loads the properties from a (potentially configured) properties file, and
593 * then overlays all command line arguments that are key/value pairs
595 public static Config createConfig (String[] args) {
596 return new Config(args);
600 * runs the verification.
604 Runtime rt = Runtime.getRuntime();
606 // this might be executed consecutively, so notify everybody
607 RunRegistry.getDefaultRegistry().reset();
611 if (vm.initialize()) {
612 status = Status.RUNNING;
615 } catch (OutOfMemoryError oom) {
617 // try to get memory back before we do anything that makes it worse
618 // (note that we even try to avoid calls here, we are on thin ice)
620 // NOTE - we don't try to recover at this point (that is what we do
621 // if we fall below search.min_free within search()), we only want to
622 // terminate gracefully (incl. report)
624 memoryReserve = null; // release something
625 long m0 = rt.freeMemory();
628 // see if we can reclaim some memory before logging or printing statistics
629 for (int i=0; i<10; i++) {
631 long m1 = rt.freeMemory();
632 if ((m1 <= m0) || ((m1 - m0) < d)) {
638 logger.severe("JPF out of memory");
640 // that's questionable, but we might want to see statistics / coverage
641 // to know how far we got. We don't inform any other listeners though
642 // if it throws an exception we bail - we can't handle it w/o memory
644 search.notifySearchConstraintHit("JPF out of memory");
645 search.error(new NoOutOfMemoryErrorProperty()); // JUnit tests will succeed if OOM isn't flagged.
646 reporter.searchFinished(search);
647 } catch (Throwable t){
648 throw new JPFListenerException("exception during out-of-memory termination", t);
651 // NOTE - this is not an exception firewall anymore
654 status = Status.DONE;
656 config.jpfRunTerminated();
662 protected void cleanUp(){
668 public List<Error> getSearchErrors () {
669 if (search != null) {
670 return search.getErrors();
676 public Error getLastError () {
677 if (search != null) {
678 return search.getLastError();
685 // some minimal sanity checks
686 static boolean checkArgs (String[] args){
687 String lastArg = args[args.length-1];
688 if (lastArg != null && lastArg.endsWith(".jpf")){
689 if (!new File(lastArg).isFile()){
690 logger.severe("application property file not found: " + lastArg);
698 public static void handleException(JPFException e) {
699 logger.severe(e.getMessage());
704 * private helper class for local termination of JPF (without killing the
705 * whole Java process via System.exit).
706 * While this is basically a bad non-local goto exception, it seems to be the
707 * least of evils given the current JPF structure, and the need to terminate
708 * w/o exiting the whole Java process. If we just do a System.exit(), we couldn't
709 * use JPF in an embedded context
711 @SuppressWarnings("serial")
712 public static class ExitException extends RuntimeException {
713 boolean report = true;
717 ExitException (boolean report, Throwable cause){
720 this.report = report;
723 ExitException(String msg) {
727 public boolean shouldReport() {