src/main/gov/nasa/jpf/JPF.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf;
  19
  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;
  33
  34 import java.io.File;
  35 import java.util.ArrayList;
  36 import java.util.List;
  37 import java.util.logging.Logger;
  38
  39
  40 /**
  41  * main class of the JPF verification framework. This reads the configuration,
  42  * instantiates the Search and VM objects, and kicks off the Search
  43  */
  44 public class JPF implements Runnable {
  45
  46   public static String VERSION = "8.0"; // the major version number
  47
  48   static Logger logger     = null; // initially
  49
  50   public enum Status { NEW, RUNNING, DONE };
  51
  52   class ConfigListener implements ConfigChangeListener {
  53
  54     /**
  55      * check for new listeners that are dynamically configured
  56      */
  57     @Override
  58     public void propertyChanged(Config config, String key, String oldValue, String newValue) {
  59       if ("listener".equals(key)) {
  60         if (oldValue == null)
  61           oldValue = "";
  62
  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 };
  68
  69         if (newListeners != null) {
  70           for (String clsName : newListeners) {
  71             try {
  72               JPFListener newListener = config.getInstance("listener", clsName, JPFListener.class, argTypes, args);
  73               addListener(newListener);
  74               logger.info("config changed, added listener " + clsName);
  75
  76             } catch (JPFConfigException cfx) {
  77               logger.warning("listener change failed: " + cfx.getMessage());
  78             }
  79           }
  80         }
  81       }
  82     }
  83
  84     /**
  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
  88      */
  89     @Override
  90     public void jpfRunTerminated(Config config){
  91       config.removeChangeListener(this);
  92     }
  93   }
  94
  95   /** this is the backbone of all JPF configuration */
  96   Config config;
  97
  98   /** The search policy used to explore the state space */
  99   Search search;
 100
 101   /** Reference to the virtual machine used by the search */
 102   VM vm;
 103
 104   /** the report generator */
 105   Reporter reporter;
 106
 107   Status status = Status.NEW;
 108
 109   /** a list of listeners that get automatically added from VM, Search or Reporter initialization */
 110   List<VMListener> pendingVMListeners;
 111   List<SearchListener> pendingSearchListeners;
 112
 113
 114   /** we use this as safety margin, to be released upon OutOfMemoryErrors */
 115   byte[] memoryReserve;
 116
 117   private static Logger initLogging(Config conf) {
 118     LogManager.init(conf);
 119     return getLogger("gov.nasa.jpf");
 120   }
 121
 122   /**
 123    * use this one to get a Logger that is initialized via our Config mechanism. Note that
 124    * our own Loggers do NOT pass
 125    */
 126   public static JPFLogger getLogger (String name) {
 127     return LogManager.getLogger( name);
 128   }
 129
 130   public static void main(String[] args){
 131     int options = RunJPF.getOptions(args);
 132
 133     if (args.length == 0 || RunJPF.isOptionEnabled( RunJPF.HELP,options)) {
 134       RunJPF.showUsage();
 135       return;
 136     }
 137     if (RunJPF.isOptionEnabled( RunJPF.ADD_PROJECT,options)){
 138       RunJPF.addProject(args);
 139       return;
 140     }
 141
 142     if (RunJPF.isOptionEnabled( RunJPF.BUILD_INFO,options)){
 143       RunJPF.showBuild(RunJPF.class.getClassLoader());
 144     }
 145
 146     if (RunJPF.isOptionEnabled( RunJPF.LOG,options)){
 147       Config.enableLogging(true);
 148     }
 149
 150     Config conf = createConfig(args);
 151
 152     if (RunJPF.isOptionEnabled( RunJPF.SHOW, options)) {
 153       conf.printEntries();
 154     }
 155
 156     start(conf, args);
 157   }
 158
 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)
 162
 163     if (logger == null) {
 164       logger = initLogging(conf);
 165     }
 166
 167     if (!checkArgs(args)){
 168       return;
 169     }
 170
 171     setNativeClassPath(conf); // in case we have to find a shell
 172
 173     // check if there is a shell class specification, in which case we just delegate
 174     JPFShell shell = conf.getInstance("shell", JPFShell.class);
 175     if (shell != null) {
 176       shell.start(args); // responsible for exception handling itself
 177
 178     } else {
 179       // no shell, we start JPF directly
 180       LogManager.printStatus(logger);
 181       conf.printStatus(logger);
 182
 183       // this has to be done after we checked&consumed all "-.." arguments
 184       // this is NOT about checking properties!
 185       checkUnknownArgs(args);
 186
 187       try {
 188         JPF jpf = new JPF(conf);
 189         jpf.run();
 190
 191       } catch (ExitException x) {
 192         logger.severe( "JPF terminated");
 193
 194         // this is how we get most runtime config exceptions
 195         if (x.shouldReport()) {
 196           x.printStackTrace();
 197         }
 198
 199         /**
 200         Throwable cause = x.getCause();
 201         if ((cause != null) && conf.getBoolean("pass_exceptions", false)) {
 202           cause.fillInStackTrace();
 203           throw cause;
 204         }
 205         **/
 206
 207       } catch (JPFException jx) {
 208         logger.severe( "JPF exception, terminating: " + jx.getMessage());
 209         if (conf.getBoolean("jpf.print_exception_stack")) {
 210
 211           Throwable cause = jx.getCause();
 212           if (cause != null && cause != jx){
 213             cause.printStackTrace();
 214           } else {
 215             jx.printStackTrace();
 216           }
 217         }
 218         // pass this on, caller has to handle
 219         throw jx;
 220       }
 221     }
 222   }
 223
 224
 225   static void setNativeClassPath(Config config) {
 226     if (!config.hasSetClassLoader()) {
 227       config.initClassLoader( JPF.class.getClassLoader());
 228     }
 229   }
 230
 231
 232   protected JPF (){
 233     // just to support unit test mockups
 234   }
 235
 236   /**
 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(),
 240    * check for null
 241    */
 242   public JPF(Config conf) {
 243     config = conf;
 244
 245     setNativeClassPath(config); // before we do anything else
 246
 247     if (logger == null) { // maybe somebody created a JPF object explicitly
 248       logger = initLogging(config);
 249     }
 250
 251     initialize();
 252   }
 253
 254   /**
 255    * convenience method if caller doesn't care about Config
 256    */
 257   public JPF (String ... args) {
 258     this( createConfig(args));
 259   }
 260
 261   private void initialize() {
 262     VERSION = config.getString("jpf.version", VERSION);
 263     memoryReserve = new byte[config.getInt("jpf.memory_reserve", 64 * 1024)]; // in bytes
 264
 265     try {
 266
 267       Class<?>[] vmArgTypes = { JPF.class, Config.class };
 268       Object[] vmArgs = { this, config };
 269       vm = config.getEssentialInstance("vm.class", VM.class, vmArgTypes, vmArgs);
 270
 271       Class<?>[] searchArgTypes = { Config.class, VM.class };
 272       Object[] searchArgs = { config, vm };
 273       search = config.getEssentialInstance("search.class", Search.class,
 274                                                 searchArgTypes, searchArgs);
 275
 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);
 284       }
 285
 286       addListeners();
 287
 288       config.addChangeListener(new ConfigListener());
 289
 290     } catch (JPFConfigException cx) {
 291       logger.severe(cx.toString());
 292       //cx.getCause().printStackTrace();
 293       throw new ExitException(false, cx);
 294     }
 295   }
 296
 297
 298   public Status getStatus() {
 299     return status;
 300   }
 301
 302   public boolean isRunnable () {
 303     return ((vm != null) && (search != null));
 304   }
 305
 306   public void addPropertyListener (PropertyListenerAdapter pl) {
 307     if (vm != null) {
 308       vm.addListener( pl);
 309     }
 310     if (search != null) {
 311       search.addListener( pl);
 312       search.addProperty(pl);
 313     }
 314   }
 315
 316   public void addSearchListener (SearchListener l) {
 317     if (search != null) {
 318       search.addListener(l);
 319     }
 320   }
 321
 322   protected void addPendingVMListener (VMListener l){
 323     if (pendingVMListeners == null){
 324       pendingVMListeners = new ArrayList<VMListener>();
 325     }
 326     pendingVMListeners.add(l);
 327   }
 328
 329   protected void addPendingSearchListener (SearchListener l){
 330     if (pendingSearchListeners == null){
 331       pendingSearchListeners = new ArrayList<SearchListener>();
 332     }
 333     pendingSearchListeners.add(l);
 334   }
 335
 336   public void addListener (JPFListener l) {
 337     // the VM is instantiated first
 338     if (l instanceof VMListener) {
 339       if (vm != null) {
 340         vm.addListener( (VMListener) l);
 341
 342       } else { // no VM yet, we are in VM initialization
 343         addPendingVMListener((VMListener)l);
 344       }
 345     }
 346
 347     if (l instanceof SearchListener) {
 348       if (search != null) {
 349         search.addListener( (SearchListener) l);
 350
 351       } else { // no search yet, we are in Search initialization
 352         addPendingSearchListener((SearchListener)l);
 353       }
 354     }
 355   }
 356
 357   public <T> T getListenerOfType( Class<T> type){
 358     if (search != null){
 359       T listener = search.getNextListenerOfType(type, null);
 360       if (listener != null){
 361         return listener;
 362       }
 363     }
 364
 365     if (vm != null){
 366       T listener = vm.getNextListenerOfType(type, null);
 367       if (listener != null){
 368         return listener;
 369       }
 370     }
 371
 372     return null;
 373   }
 374
 375   public boolean addUniqueTypeListener (JPFListener l) {
 376     boolean addedListener = false;
 377     Class<?> cls = l.getClass();
 378
 379     if (l instanceof VMListener) {
 380       if (vm != null) {
 381         if (!vm.hasListenerOfType(cls)) {
 382           vm.addListener( (VMListener) l);
 383           addedListener = true;
 384         }
 385       }
 386     }
 387     if (l instanceof SearchListener) {
 388       if (search != null) {
 389         if (!search.hasListenerOfType(cls)) {
 390           search.addListener( (SearchListener) l);
 391           addedListener = true;
 392         }
 393       }
 394     }
 395
 396     return addedListener;
 397   }
 398
 399
 400   public void removeListener (JPFListener l){
 401     if (l instanceof VMListener) {
 402       if (vm != null) {
 403         vm.removeListener( (VMListener) l);
 404       }
 405     }
 406     if (l instanceof SearchListener) {
 407       if (search != null) {
 408         search.removeListener( (SearchListener) l);
 409       }
 410     }
 411   }
 412
 413   public void addVMListener (VMListener l) {
 414     if (vm != null) {
 415       vm.addListener(l);
 416     }
 417   }
 418
 419   public void addSearchProperty (Property p) {
 420     if (search != null) {
 421       search.addProperty(p);
 422     }
 423   }
 424
 425   /**
 426    * this is called after vm, search and reporter got instantiated
 427    */
 428   void addListeners () {
 429     Class<?>[] argTypes = { Config.class, JPF.class };
 430     Object[] args = { config, this };
 431
 432     // first listeners that were automatically added from VM, Search and Reporter initialization
 433     if (pendingVMListeners != null){
 434       for (VMListener l : pendingVMListeners) {
 435        vm.addListener(l);
 436       }
 437       pendingVMListeners = null;
 438     }
 439
 440     if (pendingSearchListeners != null){
 441       for (SearchListener l : pendingSearchListeners) {
 442        search.addListener(l);
 443       }
 444       pendingSearchListeners = null;
 445     }
 446
 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) {
 451         addListener(l);
 452       }
 453     }
 454   }
 455
 456   public Reporter getReporter () {
 457     return reporter;
 458   }
 459
 460   public <T extends Publisher> boolean addPublisherExtension (Class<T> pCls, PublisherExtension e) {
 461     if (reporter != null) {
 462       return reporter.addPublisherExtension(pCls, e);
 463     }
 464     return false;
 465   }
 466
 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);
 471     }
 472   }
 473
 474
 475   public Config getConfig() {
 476     return config;
 477   }
 478
 479   /**
 480    * return the search object. This can be null if the initialization has failed
 481    */
 482   public Search getSearch() {
 483     return search;
 484   }
 485
 486   /**
 487    * return the VM object. This can be null if the initialization has failed
 488    */
 489   public VM getVM() {
 490     return vm;
 491   }
 492
 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();
 497   }
 498
 499   public boolean foundErrors() {
 500     return !(search.getErrors().isEmpty());
 501   }
 502
 503   /**
 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
 506    * target class name
 507    */
 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]);
 513         }
 514         else {
 515           // this is supposed to be the target class name - everything that follows
 516           // is supposed to be processed by the program under test
 517           break;
 518         }
 519       }
 520     }
 521   }
 522
 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.");
 527   }
 528
 529
 530   /**
 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
 534    */
 535   static String getArg(String[] args, String pattern, String defValue, boolean consume) {
 536     String s = defValue;
 537
 538     if (args != null){
 539       for (int i = 0; i < args.length; i++) {
 540         String arg = args[i];
 541
 542         if (arg != null) {
 543           if (arg.matches(pattern)) {
 544             int idx=arg.indexOf('=');
 545             if (idx > 0) {
 546               s = arg.substring(idx+1);
 547               if (consume) {
 548                 args[i]=null;
 549               }
 550             } else if (i < args.length-1) {
 551               s = args[i+1];
 552               if (consume) {
 553                 args[i] = null;
 554                 args[i+1] = null;
 555               }
 556             }
 557             break;
 558           }
 559         }
 560       }
 561     }
 562
 563     return s;
 564   }
 565
 566   /**
 567    * what property file to look for
 568    */
 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('=');
 578           if (i > 0) {
 579             lastArg = lastArg.substring(i+1);
 580           }
 581         }
 582         args[idx] = null;
 583         return lastArg;
 584       }
 585     }
 586
 587     return getArg(args, "-c(onfig)?(=.+)?", "jpf.properties", true);
 588   }
 589
 590   /**
 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
 594    */
 595   public static Config createConfig (String[] args) {
 596     return new Config(args);
 597   }
 598
 599   /**
 600    * runs the verification.
 601    */
 602   @Override
 603   public void run() {
 604     Runtime rt = Runtime.getRuntime();
 605
 606     // this might be executed consecutively, so notify everybody
 607     RunRegistry.getDefaultRegistry().reset();
 608
 609     if (isRunnable()) {
 610       try {
 611         if (vm.initialize()) {
 612           status = Status.RUNNING;
 613           search.search();
 614         }
 615       } catch (OutOfMemoryError oom) {
 616
 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)
 619
 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)
 623
 624         memoryReserve = null; // release something
 625         long m0 = rt.freeMemory();
 626         long d = 10000;
 627
 628         // see if we can reclaim some memory before logging or printing statistics
 629         for (int i=0; i<10; i++) {
 630           rt.gc();
 631           long m1 = rt.freeMemory();
 632           if ((m1 <= m0) || ((m1 - m0) < d)) {
 633             break;
 634           }
 635           m0 = m1;
 636         }
 637
 638         logger.severe("JPF out of memory");
 639
 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
 643         try {
 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);
 649         }
 650
 651       // NOTE - this is not an exception firewall anymore
 652
 653       } finally {
 654         status = Status.DONE;
 655
 656         config.jpfRunTerminated();
 657         cleanUp();
 658       }
 659     }
 660   }
 661
 662   protected void cleanUp(){
 663     search.cleanUp();
 664     vm.cleanUp();
 665     reporter.cleanUp();
 666   }
 667
 668   public List<Error> getSearchErrors () {
 669     if (search != null) {
 670       return search.getErrors();
 671     }
 672
 673     return null;
 674   }
 675
 676   public Error getLastError () {
 677     if (search != null) {
 678       return search.getLastError();
 679     }
 680
 681     return null;
 682   }
 683
 684
 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);
 691         return false;
 692       }
 693     }
 694
 695     return true;
 696   }
 697
 698   public static void handleException(JPFException e) {
 699     logger.severe(e.getMessage());
 700     exit();
 701   }
 702
 703   /**
 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
 710    */
 711   @SuppressWarnings("serial")
 712   public static class ExitException extends RuntimeException {
 713     boolean report = true;
 714
 715     ExitException() {}
 716
 717     ExitException (boolean report, Throwable cause){
 718       super(cause);
 719
 720       this.report = report;
 721     }
 722
 723     ExitException(String msg) {
 724       super(msg);
 725     }
 726
 727     public boolean shouldReport() {
 728       return report;
 729     }
 730   }
 731 }