src/main/gov/nasa/jpf/vm/VM.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.vm;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.JPFConfigException;
  23 import gov.nasa.jpf.JPFException;
  24 import gov.nasa.jpf.JPFListenerException;
  25 import gov.nasa.jpf.jvm.ClassFile;
  26 import gov.nasa.jpf.vm.FinalizerThreadInfo;
  27 import gov.nasa.jpf.search.Search;
  28 import gov.nasa.jpf.util.IntTable;
  29 import gov.nasa.jpf.util.JPFLogger;
  30 import gov.nasa.jpf.util.Misc;
  31 import gov.nasa.jpf.util.Predicate;
  32
  33 import java.io.PrintWriter;
  34 import java.nio.ByteOrder;
  35 import java.util.ArrayList;
  36 import java.util.Collections;
  37 import java.util.LinkedList;
  38 import java.util.List;
  39 import java.util.Map;
  40
  41
  42 /**
  43  * This class represents the virtual machine. The virtual machine is able to
  44  * move backward and forward one transition at a time.
  45  */
  46 public abstract class VM {
  47
  48   /**
  49    * this is a debugging aid to control compilation of expensive consistency checks
  50    * (we don't control these with class-wise assertion enabling since we do use
  51    * unconditional assertions for mandatory consistency checks)
  52    */
  53   public static final boolean CHECK_CONSISTENCY = false;
  54
  55   protected static final String[] EMPTY_ARGS = new String[0];
  56
  57   protected static JPFLogger log = JPF.getLogger("vm");
  58
  59   /**
  60    * our execution context
  61    */
  62   protected JPF jpf;
  63
  64   /**
  65    * The number of errors saved so far.
  66    * Used to generate the name of the error trail file.
  67    */
  68   protected static int error_id;
  69
  70   /**
  71    * <2do> - this is a hack to be removed once there are no static references
  72    * anymore
  73    */
  74   protected static VM vm;
  75
  76   static {
  77     initStaticFields();
  78   }
  79
  80   protected SystemState ss;
  81
  82   protected FunctionObjectFactory funcObjFactory = new FunctionObjectFactory();
  83
  84   // <2do> - if you are confused about the various pieces of state and its
  85   // storage/backtrack structures, I'm with you. It's mainly an attempt to
  86   // separate non-policy VM state (objects), policy VM state (Scheduler)
  87   // and general JPF execution state, with special support for stack oriented
  88   // state restoration (backtracking).
  89   // this needs to be cleaned up and the principle reinstated
  90
  91
  92   protected Path path;  /** execution path to current state */
  93   protected StringBuilder out;  /** buffer to store output along path execution */
  94
  95   /**
  96    * various caches for VMListener state acquisition. NOTE - these are only
  97    * valid during notification
  98    *
  99    * <2do> get rid of the 'lasts' in favor of queries on the insn, the executing
 100    * thread, and the VM. This is superfluous work to for every notification
 101    * (even if there are no listeners using it) that can easily lead to inconsistencies
 102    */
 103   protected Transition      lastTrailInfo;
 104
 105   protected boolean isTraceReplay; // can be set by listeners to indicate this is a replay
 106
 107   /** the repository we use to find out if we already have seen a state */
 108   protected StateSet stateSet;
 109
 110   /** this was the last stateId - note this is also used for stateless model checking */
 111   protected int newStateId;
 112
 113   /** the structure responsible for storing and restoring backtrack info */
 114   protected Backtracker backtracker;
 115
 116   /** optional serializer/restorer to support backtracker */
 117   protected StateRestorer<?> restorer;
 118
 119   /** optional serializer to support stateSet */
 120   protected StateSerializer serializer;
 121
 122   /** potential execution listeners. We keep them in a simple array to avoid
 123    creating objects on each notification */
 124   protected VMListener[] listeners = new VMListener[0];
 125
 126   /** did we get a new transition */
 127   protected boolean transitionOccurred;
 128
 129   /** how we model execution time */
 130   protected TimeModel timeModel;
 131
 132   /** ThreadChoiceGenerator management related to data races and shared objects */
 133   protected Scheduler scheduler;
 134
 135
 136   protected Config config; // that's for the options we use only once
 137
 138   // VM options we use frequently
 139   protected boolean runGc;
 140   protected boolean treeOutput;
 141   protected boolean pathOutput;
 142   protected boolean indentOutput;
 143   protected boolean processFinalizers;
 144
 145   // <2do> there are probably many places where this should be used
 146   protected boolean isBigEndian;
 147
 148   protected boolean initialized;
 149
 150   //thread filters
 151   protected Predicate<ThreadInfo> userliveNonDaemonPredicate;
 152   protected Predicate<ThreadInfo> timedoutRunnablePredicate;
 153   protected Predicate<ThreadInfo> alivePredicate;
 154   protected Predicate<ThreadInfo> userTimedoutRunnablePredicate;
 155
 156   // a list of actions to be run post GC. This is a bit redundant to VMListener,
 157   // but in addition to avoid the per-instruction execution overhead of a VMListener
 158   // we want a (internal) mechanism that is on-demand only, i.e. processed
 159   // actions are removed from the list
 160   protected ArrayList<Runnable> postGcActions = new ArrayList<Runnable>();
 161
 162   /**
 163    * be prepared this might throw JPFConfigExceptions
 164    */
 165   public VM (JPF jpf, Config conf) {
 166     this.jpf = jpf; // so that we know who instantiated us
 167
 168     // <2do> that's really a bad hack and should be removed once we
 169     // have cleaned up the reference chains
 170     vm = this;
 171
 172     config = conf;
 173
 174     runGc = config.getBoolean("vm.gc", true);
 175
 176     treeOutput = config.getBoolean("vm.tree_output", true);
 177     // we have to defer setting pathOutput until we have a reporter registered
 178     indentOutput = config.getBoolean("vm.indent_output",false);
 179
 180     processFinalizers = config.getBoolean("vm.process_finalizers", false);
 181
 182     isBigEndian = getPlatformEndianness(config);
 183     initialized = false;
 184
 185     initTimeModel(config);
 186
 187     initSubsystems(config);
 188     initFields(config);
 189
 190     // set predicates used to query from threadlist
 191     userliveNonDaemonPredicate = new Predicate<ThreadInfo>() {
 192       @Override
 193         public boolean isTrue (ThreadInfo ti) {
 194         return (!ti.isDaemon() && !ti.isTerminated() && !ti.isSystemThread());
 195       }
 196     };
 197
 198     timedoutRunnablePredicate = new Predicate<ThreadInfo>() {
 199       @Override
 200         public boolean isTrue (ThreadInfo ti) {
 201         return (ti.isTimeoutRunnable());
 202       }
 203     };
 204
 205     userTimedoutRunnablePredicate = new Predicate<ThreadInfo>() {
 206       @Override
 207         public boolean isTrue (ThreadInfo ti) {
 208         return (ti.isTimeoutRunnable() && !ti.isSystemThread());
 209       }
 210     };
 211
 212     alivePredicate = new Predicate<ThreadInfo>() {
 213       @Override
 214         public boolean isTrue (ThreadInfo ti) {
 215         return (ti.isAlive());
 216       }
 217     };
 218   }
 219
 220   /**
 221    * just here for unit test mockups, don't use as implicit base ctor in
 222    * VM derived classes
 223    */
 224   protected VM (){}
 225
 226   public JPF getJPF() {
 227     return jpf;
 228   }
 229
 230   public void initFields (Config config) {
 231     path = new Path("fix-this!");
 232     out = null;
 233
 234     ss = new SystemState(config, this);
 235
 236     stateSet = config.getInstance("vm.storage.class", StateSet.class);
 237     if (stateSet != null) stateSet.attach(this);
 238     backtracker = config.getEssentialInstance("vm.backtracker.class", Backtracker.class);
 239     backtracker.attach(this);
 240
 241     scheduler = config.getEssentialInstance("vm.scheduler.class", Scheduler.class);
 242
 243     newStateId = -1;
 244   }
 245
 246   protected void initSubsystems (Config config) {
 247     ClassLoaderInfo.init(config);
 248     ClassInfo.init(config);
 249     ThreadInfo.init(config);
 250     ElementInfo.init(config);
 251     MethodInfo.init(config);
 252     NativePeer.init(config);
 253     ChoiceGeneratorBase.init(config);
 254
 255     // peer classes get initialized upon NativePeer creation
 256   }
 257
 258   protected void initTimeModel (Config config){
 259     Class<?>[] argTypes = { VM.class, Config.class };
 260     Object[] args = { this, config };
 261     timeModel = config.getEssentialInstance("vm.time.class", TimeModel.class, argTypes, args);
 262   }
 263
 264   /**
 265    * called after the JPF run is finished. Shouldn't be public, but is called by JPF
 266    */
 267   public void cleanUp(){
 268     // nothing yet
 269   }
 270
 271   protected boolean getPlatformEndianness (Config config){
 272     String endianness = config.getString("vm.endian");
 273     if (endianness == null) {
 274       return ByteOrder.nativeOrder() == ByteOrder.BIG_ENDIAN;
 275     } else if (endianness.equalsIgnoreCase("big")) {
 276       return true;
 277     } else if (endianness.equalsIgnoreCase("little")) {
 278       return false;
 279     } else {
 280       config.exception("illegal vm.endian value: " + endianness);
 281       return false; // doesn't matter
 282     }
 283   }
 284
 285   public boolean isBigEndianPlatform(){
 286     return isBigEndian;
 287   }
 288
 289   public boolean finalizersEnabled() {
 290     return processFinalizers;
 291   }
 292
 293   public boolean isInitialized() {
 294     return initialized;
 295   }
 296
 297   public boolean isSingleProcess() {
 298     return true;
 299   }
 300
 301   /**
 302    * do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
 303    * are tightly coupled with the JPF core (e.g. java.lang.Class, java.lang.Thread,
 304    * java.lang.StackTraceElement etc.)
 305    * Our strategy here is kind of lame - we just look into java.lang.Class if we find the 'uniqueId' field
 306    * (that's a true '42')
 307    */
 308   static boolean checkSystemClassCompatibility (SystemClassLoaderInfo systemLoader) {
 309     ClassInfo ci = systemLoader.getClassClassInfo();
 310     return ci.checkIfValidClassClassInfo();
 311   }
 312
 313   static boolean isValidClassName (String clsName) {
 314     if ( !clsName.matches("[a-zA-Z_$][a-zA-Z_$0-9.]*")) {
 315       return false;
 316     }
 317
 318     // well, those two could be part of valid class names, but
 319     // in all likeliness somebody specified a filename instead of
 320     // a classname
 321     if (clsName.endsWith(".java")) {
 322       return false;
 323     }
 324     if (clsName.endsWith(".class")) {
 325       return false;
 326     }
 327
 328     return true;
 329   }
 330
 331   //--- ThreadInfo factory methods
 332   protected ThreadInfo createMainThreadInfo (int id, ApplicationContext appCtx){
 333     ThreadInfo tiMain = new ThreadInfo( this, id, appCtx);
 334     ThreadInfo.currentThread = tiMain; // we still need this for listeners that process startup class loading events
 335     registerThread(tiMain);
 336
 337     return tiMain;
 338   }
 339
 340   protected ThreadInfo createThreadInfo (int objRef, int groupRef, int runnableRef, int nameRef){
 341     ThreadInfo tiCurrent = ThreadInfo.getCurrentThread();
 342     ThreadInfo tiNew = new ThreadInfo( this, objRef, groupRef, runnableRef, nameRef, tiCurrent);
 343
 344     // note that we have to register here so that subsequent native peer calls can use the objRef
 345     // to lookup the ThreadInfo. This is a bit premature since the thread is not runnable yet,
 346     // but chances are it will be started soon, so we don't waste another data structure to do the mapping
 347     registerThread( tiNew);
 348
 349     return tiNew;
 350   }
 351
 352   // created if the option "vm.process_finalizers" is set to true
 353   protected ThreadInfo createFinalizerThreadInfo (int id, ApplicationContext appCtx){
 354     FinalizerThreadInfo finalizerTi = new FinalizerThreadInfo( this, appCtx, id);
 355     registerThread(finalizerTi);
 356
 357     return finalizerTi;
 358   }
 359
 360   /**
 361    * the minimal set of system classes we need for initialization
 362    */
 363   protected List<String> getStartupSystemClassNames() {
 364     ArrayList<String> startupClasses = new ArrayList<String>(64);
 365
 366     // bare essentials
 367     startupClasses.add("java.lang.Object");
 368     startupClasses.add("java.lang.Class");
 369     startupClasses.add("java.lang.ClassLoader");
 370
 371     // the builtin types (and their arrays)
 372     startupClasses.add("boolean");
 373     startupClasses.add("[Z");
 374     startupClasses.add("byte");
 375     startupClasses.add("[B");
 376     startupClasses.add("char");
 377     startupClasses.add("[C");
 378     startupClasses.add("short");
 379     startupClasses.add("[S");
 380     startupClasses.add("int");
 381     startupClasses.add("[I");
 382     startupClasses.add("long");
 383     startupClasses.add("[J");
 384     startupClasses.add("float");
 385     startupClasses.add("[F");
 386     startupClasses.add("double");
 387     startupClasses.add("[D");
 388     startupClasses.add("void");
 389
 390     // the box types
 391     startupClasses.add("java.lang.Boolean");
 392     startupClasses.add("java.lang.Character");
 393     startupClasses.add("java.lang.Short");
 394     startupClasses.add("java.lang.Integer");
 395     startupClasses.add("java.lang.Long");
 396     startupClasses.add("java.lang.Float");
 397     startupClasses.add("java.lang.Double");
 398     startupClasses.add("java.lang.Byte");
 399
 400     // the cache for box types
 401     startupClasses.add("gov.nasa.jpf.BoxObjectCaches");
 402
 403     // standard system classes
 404     startupClasses.add("java.lang.String");
 405     startupClasses.add("java.lang.Thread");
 406     startupClasses.add("java.lang.ThreadGroup");
 407     startupClasses.add("java.lang.Thread$State");
 408     startupClasses.add("java.lang.Thread$Permit");
 409     startupClasses.add("java.io.PrintStream");
 410     startupClasses.add("java.io.InputStream");
 411     startupClasses.add("java.lang.System");
 412     startupClasses.add("java.lang.ref.Reference");
 413     startupClasses.add("java.lang.ref.WeakReference");
 414     startupClasses.add("java.lang.Enum");
 415     startupClasses.add("gov.nasa.jpf.FinalizerThread");
 416
 417     // we could be more fancy and use wildcard patterns and the current classpath
 418     // to specify extra classes, but this could be VERY expensive. Projected use
 419     // is mostly to avoid static init of single classes during the search
 420     String[] extraStartupClasses = config.getStringArray("vm.extra_startup_classes");
 421     if (extraStartupClasses != null) {
 422       for (String extraCls : extraStartupClasses) {
 423         startupClasses.add(extraCls);
 424       }
 425     }
 426
 427     // the main class has to be handled separately since it might be VM specific
 428
 429     return startupClasses;
 430   }
 431
 432   /**
 433    * return a list of ClassInfos for essential system types
 434    *
 435    * If system classes are not found, or are not valid JPF model classes, we throw
 436    * a JPFConfigException and exit
 437    *
 438    * returned ClassInfos are not yet registered in Statics and don't have class objects
 439    */
 440   protected List<ClassInfo> getStartupSystemClassInfos (SystemClassLoaderInfo sysCl, ThreadInfo tiMain){
 441     LinkedList<ClassInfo> list = new LinkedList<ClassInfo>();
 442
 443     try {
 444       for (String clsName : getStartupSystemClassNames()) {
 445         ClassInfo ci = sysCl.getResolvedClassInfo(clsName);
 446         ci.registerStartupClass( tiMain, list); // takes care of superclasses and interfaces
 447       }
 448     } catch (ClassInfoException e){
 449       e.printStackTrace();
 450       throw new JPFConfigException("cannot load system class " + e.getFailedClass());
 451     }
 452
 453     return list;
 454   }
 455
 456   /**
 457    * this adds the application main class and its supers to the list of startup classes
 458    */
 459   protected ClassInfo getMainClassInfo (SystemClassLoaderInfo sysCl, String mainClassName, ThreadInfo tiMain, List<ClassInfo> list){
 460     try {
 461       ClassInfo ciMain = sysCl.getResolvedClassInfo(mainClassName);
 462       ciMain.registerStartupClass(tiMain, list); // this might add a couple more
 463
 464       return ciMain;
 465
 466     } catch (ClassInfoException e){
 467       throw new JPFConfigException("cannot load application class " + e.getFailedClass());
 468     }
 469   }
 470
 471   /*
 472    * these are called when creating ApplicationContexts and can be overridden by concrete VM types
 473    */
 474   protected SystemClassLoaderInfo createSystemClassLoaderInfo (int appId) {
 475     Class<?>[] argTypes = { VM.class, int.class };
 476
 477     Object[] args = { this, Integer.valueOf(appId)};
 478     SystemClassLoaderInfo sysCli = config.getEssentialInstance("vm.classloader.class", SystemClassLoaderInfo.class, argTypes, args);
 479     return sysCli;
 480   }
 481
 482   protected void createSystemClassLoaderObject (SystemClassLoaderInfo sysCl, ThreadInfo tiMain) {
 483     Heap heap = getHeap();
 484
 485     // create ClassLoader object for the ClassLoader type defined by this SystemClassLoaderInfo
 486     // NOTE - this requires the SystemClassLoaderInfo cache to be initialized
 487     ClassInfo ciCl = sysCl.getClassLoaderClassInfo();
 488     ElementInfo ei = heap.newObject( ciCl, tiMain);
 489     //ei.setReferenceField("parent", MJIEnv.NULL);
 490     heap.registerPinDown(ei.getObjectRef());
 491
 492     sysCl.setClassLoaderObject(ei);
 493   }
 494
 495   protected void pushMainEntryArgs (MethodInfo miMain, String[] args, ThreadInfo tiMain, DirectCallStackFrame frame){
 496     String sig = miMain.getSignature();
 497     Heap heap = getHeap();
 498
 499     if (sig.contains("([Ljava/lang/String;)")){
 500       ElementInfo eiArgs = heap.newArray("Ljava/lang/String;", args.length, tiMain);
 501       for (int i = 0; i < args.length; i++) {
 502         ElementInfo eiArg = heap.newString(args[i], tiMain);
 503         eiArgs.setReferenceElement(i, eiArg.getObjectRef());
 504       }
 505       frame.setReferenceArgument( 0, eiArgs.getObjectRef(), null);
 506
 507     } else if (sig.contains("(Ljava/lang/String;)")){
 508       if (args.length > 1){
 509         ElementInfo eiArg = heap.newString(args[0], tiMain);
 510         frame.setReferenceArgument( 0, eiArg.getObjectRef(), null);
 511       } else {
 512         frame.setReferenceArgument( 0, MJIEnv.NULL, null);
 513       }
 514
 515     } else if (!sig.contains("()")){
 516       throw new JPFException("unsupported main entry signature: " + miMain.getFullName());
 517     }
 518   }
 519
 520   protected void pushMainEntry (MethodInfo miMain, String[] args, ThreadInfo tiMain) {
 521     DirectCallStackFrame frame = miMain.createDirectCallStackFrame(tiMain, 0);
 522     pushMainEntryArgs( miMain, args, tiMain, frame);
 523     tiMain.pushFrame(frame);
 524   }
 525
 526   protected MethodInfo getMainEntryMethodInfo (String mthName, ClassInfo ciMain) {
 527     MethodInfo miMain = ciMain.getMethod(mthName, true);
 528
 529     //--- do some sanity checks if this is a valid entry method
 530     if (miMain == null || !miMain.isStatic()) {
 531       throw new JPFConfigException("no static entry method: " + ciMain.getName() + '.' + mthName);
 532     }
 533
 534     return miMain;
 535   }
 536
 537   protected void pushClinits (List<ClassInfo> startupClasses, ThreadInfo tiMain) {
 538     for (ClassInfo ci : startupClasses){
 539       MethodInfo mi = ci.getMethod("<clinit>()V", false);
 540       if (mi != null) {
 541         DirectCallStackFrame frame = mi.createDirectCallStackFrame(tiMain, 0);
 542         tiMain.pushFrame(frame);
 543       } else {
 544         ci.setInitialized();
 545       }
 546     }
 547   }
 548
 549   /**
 550    * this is the main initialization point that sets up startup objects threads and callstacks.
 551    * If this returns false VM initialization cannot proceed and JPF will terminate
 552    */
 553   public abstract boolean initialize ();
 554
 555   /**
 556    * create and initialize the main thread for the given ApplicationContext.
 557    * This is called from VM.initialize() implementations, the caller has to handle exceptions that should be reported
 558    * differently (JPFConfigException, ClassInfoException)
 559    */
 560   protected ThreadInfo initializeMainThread (ApplicationContext appCtx, int tid){
 561     SystemClassLoaderInfo sysCl = appCtx.sysCl;
 562
 563     ThreadInfo tiMain = createMainThreadInfo(tid, appCtx);
 564     List<ClassInfo> startupClasses = getStartupSystemClassInfos(sysCl, tiMain);
 565     ClassInfo ciMain = getMainClassInfo(sysCl, appCtx.mainClassName, tiMain, startupClasses);
 566
 567     if (!checkSystemClassCompatibility( sysCl)){
 568       throw new JPFConfigException("non-JPF system classes, check classpath");
 569     }
 570
 571     // create essential objects (we can't call ctors yet)
 572     createSystemClassLoaderObject(sysCl, tiMain);
 573     for (ClassInfo ci : startupClasses) {
 574       ci.createAndLinkStartupClassObject(tiMain);
 575     }
 576     tiMain.createMainThreadObject(sysCl);
 577     registerThread(tiMain);
 578
 579     // note that StackFrames have to be pushed in reverse order
 580     MethodInfo miMain = getMainEntryMethodInfo(appCtx.mainEntry, ciMain);
 581     appCtx.setEntryMethod(miMain);
 582     pushMainEntry(miMain, appCtx.args, tiMain);
 583     Collections.reverse(startupClasses);
 584     pushClinits(startupClasses, tiMain);
 585
 586     registerThreadListCleanup(sysCl.getThreadClassInfo());
 587
 588     return tiMain;
 589   }
 590
 591   protected void initializeFinalizerThread (ApplicationContext appCtx, int tid) {
 592     if(processFinalizers) {
 593       ApplicationContext app = getCurrentApplicationContext();
 594       FinalizerThreadInfo finalizerTi = app.getFinalizerThread();
 595
 596       finalizerTi = (FinalizerThreadInfo) createFinalizerThreadInfo(tid, app);
 597       finalizerTi.createFinalizerThreadObject(app.getSystemClassLoader());
 598
 599       appCtx.setFinalizerThread(finalizerTi);
 600     }
 601   }
 602
 603   protected void registerThreadListCleanup (ClassInfo ciThread){
 604     assert ciThread != null : "java.lang.Thread not loaded yet";
 605
 606     ciThread.addReleaseAction( new ReleaseAction(){
 607       @Override
 608         public void release (ElementInfo ei) {
 609         ThreadList tl = getThreadList();
 610         int objRef = ei.getObjectRef();
 611         ThreadInfo ti = tl.getThreadInfoForObjRef(objRef);
 612         if (tl.remove(ti)){
 613           vm.getKernelState().changed();
 614         }
 615       }
 616     });
 617   }
 618
 619
 620   /**
 621    * override this if the concrete VM needs a special root CG
 622    */
 623   protected void setRootCG(){
 624     scheduler.setRootCG();
 625   }
 626
 627   protected void initSystemState (ThreadInfo mainThread){
 628     ss.setStartThread(mainThread);
 629
 630     ss.recordSteps(hasToRecordSteps());
 631
 632     if (!pathOutput) { // don't override if explicitly requested
 633       pathOutput = hasToRecordPathOutput();
 634     }
 635
 636     setRootCG(); // this has to be guaranteed to register a CG
 637     if (!hasNextChoiceGenerator()){
 638       throw new JPFException("scheduler failed to set ROOT choice generator: " + scheduler);
 639     }
 640
 641     transitionOccurred = true;
 642   }
 643
 644   public void addPostGcAction (Runnable r){
 645     postGcActions.add(r);
 646   }
 647
 648   /**
 649    * to be called from the Heap after GC is completed (i.e. only live objects remain)
 650    */
 651   public void processPostGcActions(){
 652     if (!postGcActions.isEmpty()){
 653       for (Runnable r : postGcActions){
 654         r.run();
 655       }
 656
 657       postGcActions.clear();
 658     }
 659   }
 660
 661   public void addListener (VMListener newListener) {
 662     log.info("VMListener added: ", newListener);
 663     listeners = Misc.appendElement(listeners, newListener);
 664   }
 665
 666   public boolean hasListenerOfType (Class<?> listenerCls) {
 667     return Misc.hasElementOfType(listeners, listenerCls);
 668   }
 669
 670   public <T> T getNextListenerOfType(Class<T> type, T prev){
 671     return Misc.getNextElementOfType(listeners, type, prev);
 672   }
 673
 674   public void removeListener (VMListener removeListener) {
 675     listeners = Misc.removeElement(listeners, removeListener);
 676   }
 677
 678   public void setTraceReplay (boolean isReplay) {
 679     isTraceReplay = isReplay;
 680   }
 681
 682   public boolean isTraceReplay() {
 683     return isTraceReplay;
 684   }
 685
 686   public boolean hasToRecordSteps() {
 687     // we have to record if there either is a reporter that has
 688     // a 'trace' topic, or there is an explicit request
 689     return jpf.getReporter().hasToReportTrace()
 690              || config.getBoolean("vm.store_steps");
 691   }
 692
 693   public void recordSteps( boolean cond) {
 694     // <2do> not ideal - it might be already too late when this is called
 695
 696     config.setProperty("vm.store_steps", cond ? "true" : "false");
 697
 698     if (ss != null){
 699       ss.recordSteps(cond);
 700     }
 701   }
 702
 703   public boolean hasToRecordPathOutput() {
 704     if (config.getBoolean("vm.path_output")){ // explicitly requested
 705       return true;
 706     } else {
 707       return jpf.getReporter().hasToReportOutput(); // implicilty required
 708     }
 709   }
 710
 711   //--- VM listener notifications
 712
 713   /*
 714    * while some of these can be called from various places, the calls that happen from within Instruction.execute() should
 715    * happen right before return since listeners might do things such as ThreadInfo.createAndThrowException(..), i.e. cause
 716    * side effects that would violate consistency requirements of successive operations (e.g. by assuming we are still executing
 717    * in the same StackFrame - after throwing an exception)
 718    */
 719
 720   protected void notifyVMInitialized () {
 721     try {
 722       for (int i = 0; i < listeners.length; i++) {
 723         listeners[i].vmInitialized(this);
 724       }
 725     } catch (UncaughtException x) {
 726       throw x;
 727     } catch (JPF.ExitException x) {
 728       throw x;
 729     } catch (Throwable t) {
 730       throw new JPFListenerException("exception during vmInitialized() notification", t);
 731     }
 732   }
 733
 734   protected void notifyChoiceGeneratorRegistered (ChoiceGenerator<?>cg, ThreadInfo ti) {
 735     try {
 736       for (int i = 0; i < listeners.length; i++) {
 737         listeners[i].choiceGeneratorRegistered(this, cg, ti, ti.getPC());
 738       }
 739     } catch (UncaughtException x) {
 740       throw x;
 741     } catch (JPF.ExitException x) {
 742       throw x;
 743     } catch (Throwable t) {
 744       throw new JPFListenerException("exception during choiceGeneratorRegistered() notification", t);
 745     }
 746   }
 747
 748   protected void notifyChoiceGeneratorSet (ChoiceGenerator<?>cg) {
 749     try {
 750       for (int i = 0; i < listeners.length; i++) {
 751         listeners[i].choiceGeneratorSet(this, cg);
 752       }
 753     } catch (UncaughtException x) {
 754       throw x;
 755     } catch (JPF.ExitException x) {
 756       throw x;
 757     } catch (Throwable t) {
 758       throw new JPFListenerException("exception during choiceGeneratorSet() notification", t);
 759     }
 760   }
 761
 762   protected void notifyChoiceGeneratorAdvanced (ChoiceGenerator<?>cg) {
 763     try {
 764       for (int i = 0; i < listeners.length; i++) {
 765         listeners[i].choiceGeneratorAdvanced(this, cg);
 766       }
 767     } catch (UncaughtException x) {
 768       throw x;
 769     } catch (JPF.ExitException x) {
 770       throw x;
 771     } catch (Throwable t) {
 772       throw new JPFListenerException("exception during choiceGeneratorAdvanced() notification", t);
 773     }
 774   }
 775
 776   protected void notifyChoiceGeneratorProcessed (ChoiceGenerator<?>cg) {
 777     try {
 778       for (int i = 0; i < listeners.length; i++) {
 779         listeners[i].choiceGeneratorProcessed(this, cg);
 780       }
 781     } catch (UncaughtException x) {
 782       throw x;
 783     } catch (JPF.ExitException x) {
 784       throw x;
 785     } catch (Throwable t) {
 786       throw new JPFListenerException("exception during choiceGeneratorProcessed() notification", t);
 787     }
 788   }
 789
 790   protected void notifyExecuteInstruction (ThreadInfo ti, Instruction insn) {
 791     try {
 792       for (int i = 0; i < listeners.length; i++) {
 793         listeners[i].executeInstruction(this, ti, insn);
 794       }
 795     } catch (UncaughtException x) {
 796       throw x;
 797     } catch (JPF.ExitException x) {
 798       throw x;
 799     } catch (Throwable t) {
 800       throw new JPFListenerException("exception during executeInstruction() notification", t);
 801     }
 802   }
 803
 804   protected void notifyInstructionExecuted (ThreadInfo ti, Instruction insn, Instruction nextInsn) {
 805     try {
 806       //listener.instructionExecuted(this);
 807       for (int i = 0; i < listeners.length; i++) {
 808         listeners[i].instructionExecuted(this, ti, nextInsn, insn);
 809       }
 810     } catch (UncaughtException x) {
 811       throw x;
 812     } catch (JPF.ExitException x) {
 813       throw x;
 814     } catch (Throwable t) {
 815       throw new JPFListenerException("exception during instructionExecuted() notification", t);
 816     }
 817   }
 818
 819   protected void notifyThreadStarted (ThreadInfo ti) {
 820     try {
 821       for (int i = 0; i < listeners.length; i++) {
 822         listeners[i].threadStarted(this, ti);
 823       }
 824     } catch (UncaughtException x) {
 825       throw x;
 826     } catch (JPF.ExitException x) {
 827       throw x;
 828     } catch (Throwable t) {
 829       throw new JPFListenerException("exception during threadStarted() notification", t);
 830     }
 831   }
 832
 833   // NOTE: the supplied ThreadInfo does NOT have to be the running thread, as this
 834   // notification can occur as a result of a lock operation in the current thread
 835   protected void notifyThreadBlocked (ThreadInfo ti) {
 836     try {
 837       for (int i = 0; i < listeners.length; i++) {
 838         listeners[i].threadBlocked(this, ti, ti.getLockObject());
 839       }
 840     } catch (UncaughtException x) {
 841       throw x;
 842     } catch (JPF.ExitException x) {
 843       throw x;
 844     } catch (Throwable t) {
 845       throw new JPFListenerException("exception during threadBlocked() notification", t);
 846     }
 847   }
 848
 849   protected void notifyThreadWaiting (ThreadInfo ti) {
 850     try {
 851       for (int i = 0; i < listeners.length; i++) {
 852         listeners[i].threadWaiting(this, ti);
 853       }
 854     } catch (UncaughtException x) {
 855       throw x;
 856     } catch (JPF.ExitException x) {
 857       throw x;
 858     } catch (Throwable t) {
 859       throw new JPFListenerException("exception during threadWaiting() notification", t);
 860     }
 861   }
 862
 863   protected void notifyThreadNotified (ThreadInfo ti) {
 864     try {
 865       for (int i = 0; i < listeners.length; i++) {
 866         listeners[i].threadNotified(this, ti);
 867       }
 868     } catch (UncaughtException x) {
 869       throw x;
 870     } catch (JPF.ExitException x) {
 871       throw x;
 872     } catch (Throwable t) {
 873       throw new JPFListenerException("exception during threadNotified() notification", t);
 874     }
 875   }
 876
 877   protected void notifyThreadInterrupted (ThreadInfo ti) {
 878     try {
 879       for (int i = 0; i < listeners.length; i++) {
 880         listeners[i].threadInterrupted(this, ti);
 881       }
 882     } catch (UncaughtException x) {
 883       throw x;
 884     } catch (JPF.ExitException x) {
 885       throw x;
 886     } catch (Throwable t) {
 887       throw new JPFListenerException("exception during threadInterrupted() notification", t);
 888     }
 889   }
 890
 891   protected void notifyThreadTerminated (ThreadInfo ti) {
 892     try {
 893       for (int i = 0; i < listeners.length; i++) {
 894         listeners[i].threadTerminated(this, ti);
 895       }
 896     } catch (UncaughtException x) {
 897       throw x;
 898     } catch (JPF.ExitException x) {
 899       throw x;
 900     } catch (Throwable t) {
 901       throw new JPFListenerException("exception during threadTerminated() notification", t);
 902     }
 903   }
 904
 905   protected void notifyThreadScheduled (ThreadInfo ti) {
 906     try {
 907       for (int i = 0; i < listeners.length; i++) {
 908         listeners[i].threadScheduled(this, ti);
 909       }
 910     } catch (UncaughtException x) {
 911       throw x;
 912     } catch (JPF.ExitException x) {
 913       throw x;
 914     } catch (Throwable t) {
 915       throw new JPFListenerException("exception during threadScheduled() notification", t);
 916     }
 917   }
 918
 919   protected void notifyLoadClass (ClassFile cf){
 920     try {
 921       for (int i = 0; i < listeners.length; i++) {
 922         listeners[i].loadClass(this, cf);
 923       }
 924     } catch (UncaughtException x) {
 925       throw x;
 926     } catch (JPF.ExitException x) {
 927       throw x;
 928     } catch (Throwable t) {
 929       throw new JPFListenerException("exception during classLoaded() notification", t);
 930     }
 931   }
 932
 933   protected void notifyClassLoaded(ClassInfo ci) {
 934     try {
 935       for (int i = 0; i < listeners.length; i++) {
 936         listeners[i].classLoaded(this, ci);
 937       }
 938     } catch (UncaughtException x) {
 939       throw x;
 940     } catch (JPF.ExitException x) {
 941       throw x;
 942     } catch (Throwable t) {
 943       throw new JPFListenerException("exception during classLoaded() notification", t);
 944     }
 945   }
 946
 947   protected void notifyObjectCreated(ThreadInfo ti, ElementInfo ei) {
 948     try {
 949       for (int i = 0; i < listeners.length; i++) {
 950         listeners[i].objectCreated(this, ti, ei);
 951       }
 952     } catch (UncaughtException x) {
 953       throw x;
 954     } catch (JPF.ExitException x) {
 955       throw x;
 956     } catch (Throwable t) {
 957       throw new JPFListenerException("exception during objectCreated() notification", t);
 958     }
 959   }
 960
 961   protected void notifyObjectReleased(ThreadInfo ti, ElementInfo ei) {
 962     try {
 963       for (int i = 0; i < listeners.length; i++) {
 964         listeners[i].objectReleased(this, ti, ei);
 965       }
 966     } catch (UncaughtException x) {
 967       throw x;
 968     } catch (JPF.ExitException x) {
 969       throw x;
 970     } catch (Throwable t) {
 971       throw new JPFListenerException("exception during objectReleased() notification", t);
 972     }
 973   }
 974
 975   protected void notifyObjectLocked(ThreadInfo ti, ElementInfo ei) {
 976     try {
 977       for (int i = 0; i < listeners.length; i++) {
 978         listeners[i].objectLocked(this, ti, ei);
 979       }
 980     } catch (UncaughtException x) {
 981       throw x;
 982     } catch (JPF.ExitException x) {
 983       throw x;
 984     } catch (Throwable t) {
 985       throw new JPFListenerException("exception during objectLocked() notification", t);
 986     }
 987   }
 988
 989   protected void notifyObjectUnlocked(ThreadInfo ti, ElementInfo ei) {
 990     try {
 991       for (int i = 0; i < listeners.length; i++) {
 992         listeners[i].objectUnlocked(this, ti, ei);
 993       }
 994     } catch (UncaughtException x) {
 995       throw x;
 996     } catch (JPF.ExitException x) {
 997       throw x;
 998     } catch (Throwable t) {
 999       throw new JPFListenerException("exception during objectUnlocked() notification", t);
1000     }
1001   }
1002
1003   protected void notifyObjectWait(ThreadInfo ti, ElementInfo ei) {
1004     try {
1005       for (int i = 0; i < listeners.length; i++) {
1006         listeners[i].objectWait(this, ti, ei);
1007       }
1008     } catch (UncaughtException x) {
1009       throw x;
1010     } catch (JPF.ExitException x) {
1011       throw x;
1012     } catch (Throwable t) {
1013       throw new JPFListenerException("exception during objectWait() notification", t);
1014     }
1015   }
1016
1017    protected void notifyObjectExposed(ThreadInfo ti, ElementInfo eiShared, ElementInfo eiExposed) {
1018     try {
1019       for (int i = 0; i < listeners.length; i++) {
1020         listeners[i].objectExposed(this, ti, eiShared, eiExposed);
1021       }
1022     } catch (UncaughtException x) {
1023       throw x;
1024     } catch (JPF.ExitException x) {
1025       throw x;
1026     } catch (Throwable t) {
1027       throw new JPFListenerException("exception during objectExposed() notification", t);
1028     }
1029   }
1030
1031    protected void notifyObjectShared(ThreadInfo ti, ElementInfo ei) {
1032     try {
1033       for (int i = 0; i < listeners.length; i++) {
1034         listeners[i].objectShared(this, ti, ei);
1035       }
1036     } catch (UncaughtException x) {
1037       throw x;
1038     } catch (JPF.ExitException x) {
1039       throw x;
1040     } catch (Throwable t) {
1041       throw new JPFListenerException("exception during objectShared() notification", t);
1042     }
1043   }
1044
1045   protected void notifyObjectNotifies(ThreadInfo ti, ElementInfo ei) {
1046     try {
1047       for (int i = 0; i < listeners.length; i++) {
1048         listeners[i].objectNotify(this, ti, ei);
1049       }
1050     } catch (UncaughtException x) {
1051       throw x;
1052     } catch (JPF.ExitException x) {
1053       throw x;
1054     } catch (Throwable t) {
1055       throw new JPFListenerException("exception during objectNotifies() notification", t);
1056     }
1057   }
1058
1059   protected void notifyObjectNotifiesAll(ThreadInfo ti, ElementInfo ei) {
1060     try {
1061       for (int i = 0; i < listeners.length; i++) {
1062         listeners[i].objectNotifyAll(this, ti, ei);
1063       }
1064     } catch (UncaughtException x) {
1065       throw x;
1066     } catch (JPF.ExitException x) {
1067       throw x;
1068     } catch (Throwable t) {
1069       throw new JPFListenerException("exception during objectNotifiesAll() notification", t);
1070     }
1071   }
1072
1073   protected void notifyGCBegin() {
1074     try {
1075       for (int i = 0; i < listeners.length; i++) {
1076         listeners[i].gcBegin(this);
1077       }
1078     } catch (UncaughtException x) {
1079       throw x;
1080     } catch (JPF.ExitException x) {
1081       throw x;
1082     } catch (Throwable t) {
1083       throw new JPFListenerException("exception during gcBegin() notification", t);
1084     }
1085   }
1086
1087   protected void notifyGCEnd() {
1088     try {
1089       for (int i = 0; i < listeners.length; i++) {
1090         listeners[i].gcEnd(this);
1091       }
1092     } catch (UncaughtException x) {
1093       throw x;
1094     } catch (JPF.ExitException x) {
1095       throw x;
1096     } catch (Throwable t) {
1097       throw new JPFListenerException("exception during gcEnd() notification", t);
1098     }
1099   }
1100
1101   protected void notifyExceptionThrown(ThreadInfo ti, ElementInfo ei) {
1102     try {
1103       for (int i = 0; i < listeners.length; i++) {
1104         listeners[i].exceptionThrown(this, ti, ei);
1105       }
1106     } catch (UncaughtException x) {
1107       throw x;
1108     } catch (JPF.ExitException x) {
1109       throw x;
1110     } catch (Throwable t) {
1111       throw new JPFListenerException("exception during exceptionThrown() notification", t);
1112     }
1113   }
1114
1115   protected void notifyExceptionBailout(ThreadInfo ti) {
1116     try {
1117       for (int i = 0; i < listeners.length; i++) {
1118         listeners[i].exceptionBailout(this, ti);
1119       }
1120     } catch (UncaughtException x) {
1121       throw x;
1122     } catch (JPF.ExitException x) {
1123       throw x;
1124     } catch (Throwable t) {
1125       throw new JPFListenerException("exception during exceptionBailout() notification", t);
1126     }
1127   }
1128
1129   protected void notifyExceptionHandled(ThreadInfo ti) {
1130     try {
1131       for (int i = 0; i < listeners.length; i++) {
1132         listeners[i].exceptionHandled(this, ti);
1133       }
1134     } catch (UncaughtException x) {
1135       throw x;
1136     } catch (JPF.ExitException x) {
1137       throw x;
1138     } catch (Throwable t) {
1139       throw new JPFListenerException("exception during exceptionHandled() notification", t);
1140     }
1141   }
1142
1143   protected void notifyMethodEntered(ThreadInfo ti, MethodInfo mi) {
1144     try {
1145       for (int i = 0; i < listeners.length; i++) {
1146         listeners[i].methodEntered(this, ti, mi);
1147       }
1148     } catch (UncaughtException x) {
1149       throw x;
1150     } catch (JPF.ExitException x) {
1151       throw x;
1152     } catch (Throwable t) {
1153       throw new JPFListenerException("exception during methodEntered() notification", t);
1154     }
1155   }
1156
1157   protected void notifyMethodExited(ThreadInfo ti, MethodInfo mi) {
1158     try {
1159       for (int i = 0; i < listeners.length; i++) {
1160         listeners[i].methodExited(this, ti, mi);
1161       }
1162     } catch (UncaughtException x) {
1163       throw x;
1164     } catch (JPF.ExitException x) {
1165       throw x;
1166     } catch (Throwable t) {
1167       throw new JPFListenerException("exception during methodExited() notification", t);
1168     }
1169   }
1170
1171   // VMListener acquisition
1172   public String getThreadName () {
1173     ThreadInfo ti = ThreadInfo.getCurrentThread();
1174
1175     return ti.getName();
1176   }
1177
1178   // VMListener acquisition
1179   public Instruction getInstruction () {
1180     ThreadInfo ti = ThreadInfo.getCurrentThread();
1181     return ti.getPC();
1182   }
1183
1184   /**
1185    * note this is gone after backtracking or starting the next exception
1186    */
1187   public ExceptionInfo getPendingException () {
1188     ThreadInfo ti = ThreadInfo.getCurrentThread();
1189
1190     if (ti != null){
1191       return ti.getPendingException();
1192     } else {
1193       return null;
1194     }
1195   }
1196
1197   public Step getLastStep () {
1198     Transition trail = ss.getTrail();
1199     if (trail != null) {
1200       return trail.getLastStep();
1201     }
1202
1203     return null;
1204   }
1205
1206   public Transition getLastTransition () {
1207     if (path.size() == 0) {
1208       return null;
1209     }
1210     return path.get(path.size() - 1);
1211   }
1212
1213   public ClassInfo getClassInfo (int objref) {
1214     if (objref != MJIEnv.NULL) {
1215       return getElementInfo(objref).getClassInfo();
1216     } else {
1217       return null;
1218     }
1219   }
1220
1221   /**
1222    * NOTE: only use this locally, since the path is getting modified by the VM
1223    *
1224    * The path only contains all states when queried from a stateAdvanced() notification.
1225    * If this is called from an instructionExecuted() (or other VMListener), and you need
1226    * the ongoing transition in it, you have to call updatePath() first
1227    */
1228   public Path getPath () {
1229     return path;
1230   }
1231
1232   /**
1233    * this is the ongoing transition. Note that it is not yet stored in the path
1234    * if this is called from a VMListener notification
1235    */
1236   public Transition getCurrentTransition() {
1237     return ss.getTrail();
1238   }
1239
1240   /**
1241    * use that one if you have to store the path for subsequent use
1242    *
1243    * NOTE: without a prior call to updatePath(), this does NOT contain the
1244    * ongoing transition. See getPath() for usage from a VMListener
1245    */
1246   public Path getClonedPath () {
1247     return path.clone();
1248   }
1249
1250   public int getPathLength () {
1251     return path.size();
1252   }
1253
1254   public ThreadList getThreadList () {
1255     return getKernelState().getThreadList();
1256   }
1257
1258   public ClassLoaderList getClassLoaderList() {
1259     return getKernelState().getClassLoaderList();
1260   }
1261
1262
1263   /**
1264    * Bundles up the state of the system for export
1265    */
1266   public RestorableVMState getRestorableState () {
1267     return new RestorableVMState(this);
1268   }
1269
1270   /**
1271    * Gets the system state.
1272    */
1273   public SystemState getSystemState () {
1274     return ss;
1275   }
1276
1277   public KernelState getKernelState () {
1278     return ss.getKernelState();
1279   }
1280
1281   public void kernelStateChanged(){
1282     ss.getKernelState().changed();
1283   }
1284
1285   public Config getConfig() {
1286     return config;
1287   }
1288
1289   public Backtracker getBacktracker() {
1290     return backtracker;
1291   }
1292
1293   @SuppressWarnings("unchecked")
1294   public <T> StateRestorer<T> getRestorer() {
1295     if (restorer == null) {
1296       if (serializer instanceof StateRestorer) {
1297         restorer = (StateRestorer<?>) serializer;
1298       } else if (stateSet instanceof StateRestorer) {
1299         restorer = (StateRestorer<?>) stateSet;
1300       } else {
1301         // config read only if serializer is not also a restorer
1302         restorer = config.getInstance("vm.restorer.class", StateRestorer.class);
1303       }
1304       restorer.attach(this);
1305     }
1306
1307     return (StateRestorer<T>) restorer;
1308   }
1309
1310   public StateSerializer getSerializer() {
1311     if (serializer == null) {
1312       serializer = config.getEssentialInstance("vm.serializer.class",
1313                                       StateSerializer.class);
1314       serializer.attach(this);
1315     }
1316     return serializer;
1317   }
1318
1319   public void setSerializer (StateSerializer newSerializer){
1320     serializer = newSerializer;
1321     serializer.attach(this);
1322   }
1323
1324   /**
1325    * Returns the stateSet if states are being matched.
1326    */
1327   public StateSet getStateSet() {
1328     return stateSet;
1329   }
1330
1331   public Scheduler getScheduler(){
1332     return scheduler;
1333   }
1334
1335   public FunctionObjectFactory getFunctionObjectFacotry() {
1336     return funcObjFactory;
1337   }
1338
1339   /**
1340    * return the last registered SystemState's ChoiceGenerator object
1341    * NOTE: there might be more than one ChoiceGenerator associated with the
1342    * current transition (ChoiceGenerators can be cascaded)
1343    */
1344   public ChoiceGenerator<?> getChoiceGenerator () {
1345     return ss.getChoiceGenerator();
1346   }
1347
1348   public ChoiceGenerator<?> getNextChoiceGenerator() {
1349     return ss.getNextChoiceGenerator();
1350   }
1351
1352   public boolean hasNextChoiceGenerator(){
1353     return (ss.getNextChoiceGenerator() != null);
1354   }
1355
1356   public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg){
1357     return ss.setNextChoiceGenerator(cg);
1358   }
1359
1360   public void setMandatoryNextChoiceGenerator (ChoiceGenerator<?> cg, String failMsg){
1361     ss.setMandatoryNextChoiceGenerator(cg, failMsg);
1362   }
1363
1364   /**
1365    * return the latest registered ChoiceGenerator used in this transition
1366    * that matches the provided 'id' and is of 'cgType'.
1367    *
1368    * This should be the main getter for clients that are cascade aware
1369    */
1370   public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator (String id, Class<T> cgType) {
1371     return ss.getCurrentChoiceGenerator(id,cgType);
1372   }
1373
1374   /**
1375    * returns all ChoiceGenerators in current path
1376    */
1377   public ChoiceGenerator<?>[] getChoiceGenerators() {
1378     return ss.getChoiceGenerators();
1379   }
1380
1381   public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType (Class<T> cgType) {
1382     return ss.getChoiceGeneratorsOfType(cgType);
1383   }
1384
1385   public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType (Class<T> cgType){
1386     return ss.getLastChoiceGeneratorOfType(cgType);
1387   }
1388
1389   public ChoiceGenerator<?> getLastChoiceGeneratorInThread (ThreadInfo ti){
1390     return ss.getLastChoiceGeneratorInThread(ti);
1391   }
1392
1393   public void print (String s) {
1394     if (treeOutput) {
1395       System.out.print(s);
1396     }
1397
1398     if (pathOutput) {
1399       appendOutput(s);
1400     }
1401   }
1402
1403   public void println (String s) {
1404     if (treeOutput) {
1405       if (indentOutput){
1406         StringBuilder indent = new StringBuilder();
1407         int i;
1408         for (i = 0;i<=path.size();i++) {
1409           indent.append('|').append(i);
1410         }
1411         indent.append("|").append(s);
1412         System.out.println(indent);
1413       }
1414       else {
1415         System.out.println(s);
1416       }
1417     }
1418
1419     if (pathOutput) {
1420       appendOutput(s);
1421       appendOutput('\n');
1422     }
1423   }
1424
1425   public void print (boolean b) {
1426     if (treeOutput) {
1427       System.out.print(b);
1428     }
1429
1430     if (pathOutput) {
1431       appendOutput(Boolean.toString(b));
1432     }
1433   }
1434
1435   public void print (char c) {
1436     if (treeOutput) {
1437       System.out.print(c);
1438     }
1439
1440     if (pathOutput) {
1441       appendOutput(c);
1442     }
1443   }
1444
1445   public void print (int i) {
1446     if (treeOutput) {
1447       System.out.print(i);
1448     }
1449
1450     if (pathOutput) {
1451       appendOutput(Integer.toString(i));
1452     }
1453   }
1454
1455   public void print (long l) {
1456     if (treeOutput) {
1457       System.out.print(l);
1458     }
1459
1460     if (pathOutput) {
1461       appendOutput(Long.toString(l));
1462     }
1463   }
1464
1465   public void print (double d) {
1466     if (treeOutput) {
1467       System.out.print(d);
1468     }
1469
1470     if (pathOutput) {
1471       appendOutput(Double.toString(d));
1472     }
1473   }
1474
1475   public void print (float f) {
1476     if (treeOutput) {
1477       System.out.print(f);
1478     }
1479
1480     if (pathOutput) {
1481       appendOutput(Float.toString(f));
1482     }
1483   }
1484
1485   public void println () {
1486     if (treeOutput) {
1487       System.out.println();
1488     }
1489
1490     if (pathOutput) {
1491       appendOutput('\n');
1492     }
1493   }
1494
1495
1496   void appendOutput (String s) {
1497     if (out == null) {
1498       out = new StringBuilder();
1499     }
1500     out.append(s);
1501   }
1502
1503   void appendOutput (char c) {
1504     if (out == null) {
1505       out = new StringBuilder();
1506     }
1507     out.append(c);
1508   }
1509
1510   /**
1511    * get the pending output (not yet stored in the path)
1512    */
1513   public String getPendingOutput() {
1514     if (out != null && out.length() > 0){
1515       return out.toString();
1516     } else {
1517       return null;
1518     }
1519   }
1520
1521   /**
1522    * this is here so that we can intercept it in subclassed VMs
1523    */
1524   public Instruction handleException (ThreadInfo ti, int xObjRef){
1525     ti = null;        // Get rid of IDE warning
1526     xObjRef = 0;
1527     return null;
1528   }
1529
1530   public void storeTrace (String fileName, String comment, boolean verbose) {
1531     ChoicePoint.storeTrace(fileName, getSUTName(), comment,
1532                            ss.getChoiceGenerators(), verbose);
1533   }
1534
1535   public void storePathOutput () {
1536     pathOutput = true;
1537   }
1538
1539   private void printCG (ChoiceGenerator<?> cg, int n){
1540     ChoiceGenerator cgPrev = cg.getPreviousChoiceGenerator();
1541     if (cgPrev != null){
1542       printCG( cgPrev, --n);
1543     }
1544
1545     System.out.printf("[%d] ", n);
1546     System.out.println(cg);
1547   }
1548
1549   // for debugging purposes
1550   public void printChoiceGeneratorStack(){
1551     ChoiceGenerator<?> cg = getChoiceGenerator();
1552     if (cg != null){
1553       int n = cg.getNumberOfParents();
1554       printCG(cg, n);
1555     }
1556   }
1557
1558   public ThreadInfo[] getLiveThreads () {
1559     return getThreadList().getThreads();
1560   }
1561
1562   /**
1563    * print call stacks of all live threads
1564    * this is also used for debugging purposes, so we can't move it to the Reporter system
1565    * (it's also using a bit too many internals for that)
1566    */
1567   public void printLiveThreadStatus (PrintWriter pw) {
1568     int nThreads = ss.getThreadCount();
1569     ThreadInfo[] threads = getThreadList().getThreads();
1570     int n=0;
1571
1572     for (int i = 0; i < nThreads; i++) {
1573       ThreadInfo ti = threads[i];
1574
1575       if (ti.getStackDepth() > 0){
1576         n++;
1577         //pw.print("Thread: ");
1578         //pw.print(tiMain.getName());
1579         pw.println(ti.getStateDescription());
1580
1581         List<ElementInfo> locks = ti.getLockedObjects();
1582         if (!locks.isEmpty()) {
1583           pw.print("  owned locks:");
1584           boolean first = true;
1585           for (ElementInfo e : locks) {
1586             if (first) {
1587               first = false;
1588             } else {
1589               pw.print(",");
1590             }
1591             pw.print(e);
1592           }
1593           pw.println();
1594         }
1595
1596         ElementInfo ei = ti.getLockObject();
1597         if (ei != null) {
1598           if (ti.getState() == ThreadInfo.State.WAITING) {
1599             pw.print( "  waiting on: ");
1600           } else {
1601             pw.print( "  blocked on: ");
1602           }
1603           pw.println(ei);
1604         }
1605
1606         pw.println("  call stack:");
1607         for (StackFrame frame : ti){
1608           if (!frame.isDirectCallFrame()) {
1609             pw.print("\tat ");
1610             pw.println(frame.getStackTraceInfo());
1611           }
1612         }
1613
1614         pw.println();
1615       }
1616     }
1617
1618     if (n==0) {
1619       pw.println("no live threads");
1620     }
1621   }
1622
1623   // just a debugging aid
1624   public void dumpThreadStates () {
1625     java.io.PrintWriter pw = new java.io.PrintWriter(System.out, true);
1626     printLiveThreadStatus(pw);
1627     pw.flush();
1628   }
1629
1630   /**
1631    * Moves one step backward. This method and forward() are the main methods
1632    * used by the search object.
1633    * Note this is called with the state that caused the backtrack still being on
1634    * the stack, so we have to remove that one first (i.e. popping two states
1635    * and restoring the second one)
1636    */
1637   public boolean backtrack () {
1638     transitionOccurred = false;
1639
1640     boolean success = backtracker.backtrack();
1641     if (success) {
1642       if (CHECK_CONSISTENCY) checkConsistency(false);
1643
1644       // restore the path
1645       path.removeLast();
1646       lastTrailInfo = path.getLast();
1647
1648       return true;
1649
1650     } else {
1651       return false;
1652     }
1653   }
1654
1655   /**
1656    * store the current SystemState's Trail in our path, after updating it
1657    * with whatever annotations the VM wants to add.
1658    * This is supposed to be called after each transition we want to keep
1659    */
1660   public void updatePath () {
1661     Transition t = ss.getTrail();
1662     Transition tLast = path.getLast();
1663
1664     // NOTE: don't add the transition twice, this is public and might get called
1665     // from listeners, so the transition object might get changed
1666
1667     if (tLast != t) {
1668       // <2do> we should probably store the output directly in the TrailInfo,
1669       // but this might not be our only annotation in the future
1670
1671       // did we have output during the last transition? If yes, add it
1672       if ((out != null) && (out.length() > 0)) {
1673         t.setOutput( out.toString());
1674         out.setLength(0);
1675       }
1676
1677       path.add(t);
1678     }
1679   }
1680
1681   /**
1682    * advance the program state
1683    *
1684    * forward() and backtrack() are the two primary interfaces towards the Search
1685    * driver. note that the caller still has to check if there is a next state,
1686    * and if the executed instruction sequence led into a new or already visited state
1687    *
1688    * @return 'true' if there was an un-executed sequence out of the current state,
1689    * 'false' if it was completely explored
1690    *
1691    */
1692   public boolean forward () {
1693
1694     // the reason we split up CG initialization and transition execution
1695     // is that program state storage is not required if the CG initialization
1696     // does not produce a new choice since we have to backtrack in that case
1697     // anyways. This can be caused by complete enumeration of CGs and/or by
1698     // CG listener intervention (i.e. not just after backtracking). For a large
1699     // number of matched or end states and ignored transitions this can be a
1700     // huge saving.
1701     // The downside is that CG notifications are NOT allowed anymore to change the
1702     // KernelState (modify fields or thread states) since those changes would
1703     // happen before storing the KernelState, and hence would make backtracking
1704     // inconsistent. This is advisable anyways since all program state changes
1705     // should take place during transitions, but the real snag is that this
1706     // cannot be easily enforced.
1707
1708     // actually, it hasn't occurred yet, but will
1709     transitionOccurred = ss.initializeNextTransition(this);
1710
1711     if (transitionOccurred){
1712       if (CHECK_CONSISTENCY) {
1713         checkConsistency(true); // don't push an inconsistent state
1714       }
1715
1716       backtracker.pushKernelState();
1717
1718       // cache this before we enter (and increment) the next insn(s)
1719       lastTrailInfo = path.getLast();
1720
1721       try {
1722         ss.executeNextTransition(vm);
1723
1724       } catch (UncaughtException e) {
1725         // we don't pass this up since it means there were insns executed and we are
1726         // in a consistent state
1727       } // every other exception goes upwards
1728
1729       backtracker.pushSystemState();
1730       updatePath();
1731
1732       if (!isIgnoredState()) {
1733         // if this is ignored we are going to backtrack anyways
1734         // matching states out of ignored transitions is also not a good idea
1735         // because this transition is usually incomplete
1736
1737         if (runGc && !hasPendingException()) {
1738           if(ss.gcIfNeeded()) {
1739             processFinalizers();
1740           }
1741         }
1742
1743         if (stateSet != null) {
1744           newStateId = stateSet.size();
1745           int id = stateSet.addCurrent();
1746           ss.setId(id);
1747
1748         } else { // this is 'state-less' model checking, i.e. we don't match states
1749           ss.setId(++newStateId); // but we still should have states numbered in case listeners use the id
1750         }
1751       }
1752
1753       return true;
1754
1755     } else {
1756
1757       return false;  // no transition occurred
1758     }
1759   }
1760
1761   /**
1762    * Prints the current stack trace. Just for debugging purposes
1763    */
1764   public void printCurrentStackTrace () {
1765     ThreadInfo th = ThreadInfo.getCurrentThread();
1766
1767     if (th != null) {
1768       th.printStackTrace();
1769     }
1770   }
1771
1772
1773   public void restoreState (RestorableVMState state) {
1774     if (state.path == null) {
1775       throw new JPFException("tried to restore partial VMState: " + state);
1776     }
1777     backtracker.restoreState(state.getBkState());
1778     path = state.path.clone();
1779   }
1780
1781   public void activateGC () {
1782     ss.activateGC();
1783   }
1784
1785
1786   //--- various state attribute getters and setters (mostly forwarding to SystemState)
1787
1788   public void retainStateAttributes (boolean isRetained){
1789     ss.retainAttributes(isRetained);
1790   }
1791
1792   public void forceState () {
1793     ss.setForced(true);
1794   }
1795
1796   /**
1797    * override the state matching - ignore this state, no matter if we changed
1798    * the heap or stacks.
1799    * use this with care, since it prunes whole search subtrees
1800    */
1801   public void ignoreState (boolean cond) {
1802     ss.setIgnored(cond);
1803   }
1804
1805   public void ignoreState(){
1806     ignoreState(true);
1807   }
1808
1809   /**
1810    * imperatively break the transition to enable state matching
1811    */
1812   public void breakTransition (String reason) {
1813     ThreadInfo ti = ThreadInfo.getCurrentThread();
1814     ti.breakTransition(reason);
1815   }
1816
1817   public boolean transitionOccurred(){
1818     return transitionOccurred;
1819   }
1820
1821   /**
1822    * answers if the current state already has been visited. This is mainly
1823    * used by the searches (to control backtracking), but could also be useful
1824    * for observers to build up search graphs (based on the state ids)
1825    *
1826    * this returns true if no state has been produced yet, and false if
1827    * no transition occurred after a forward call
1828    */
1829   public boolean isNewState() {
1830
1831     if (!transitionOccurred){
1832       return false;
1833     }
1834
1835     if (stateSet != null) {
1836       if (ss.isForced()){
1837         return true;
1838       } else if (ss.isIgnored()){
1839         return false;
1840       } else {
1841         return (newStateId == ss.getId());
1842       }
1843
1844     } else { // stateless model checking - each transition leads to a new state
1845       return true;
1846     }
1847   }
1848
1849   /**
1850    * We made this to be overriden by Single/MultiprcessesVM implementations,
1851    * since for MultiprcessesVM one can decide when to terminate (after the
1852    * the termination of all processes or only one process).
1853    * todo - that needs to be specified through the properties file
1854    */
1855   public abstract boolean isEndState ();
1856
1857   public boolean isVisitedState(){
1858     return !isNewState();
1859   }
1860
1861   public boolean isIgnoredState(){
1862     return ss.isIgnored();
1863   }
1864
1865   public boolean isInterestingState () {
1866     return ss.isInteresting();
1867   }
1868
1869   public boolean isBoringState () {
1870     return ss.isBoring();
1871   }
1872
1873   public boolean hasPendingException () {
1874     return (getPendingException() != null);
1875   }
1876
1877   public abstract boolean isDeadlocked ();
1878
1879   public Exception getException () {
1880     return ss.getUncaughtException();
1881   }
1882
1883
1884
1885   /**
1886    * get the numeric id for the current state
1887    * Note: this can be called several times (by the search and observers) for
1888    * every forward()/backtrack(), so we want to cache things a bit
1889    */
1890   public int getStateId() {
1891     return ss.getId();
1892   }
1893
1894   public int getStateCount() {
1895     return newStateId;
1896   }
1897
1898
1899   /**
1900    * <2do> this is a band aid to bundle all these legacy reference chains
1901    * from JPFs past. The goal is to replace them with proper accessors (normally
1902    * through ThreadInfo, MJIEnv or VM, which all act as facades) wherever possible,
1903    * and use VM.getVM() where there is no access to such a facade. Once this
1904    * has been completed, we can start refactoring the users of VM.getVM() to
1905    * get access to a suitable facade.
1906    */
1907   public static VM getVM () {
1908     return vm;
1909   }
1910
1911   /**
1912    * not ideal to have this here since it is kind of a backlink, but it's not
1913    * any better if listeners have to dig this out from JPF
1914    * Note - this isn't set during initialization, since the VM object is created first
1915    */
1916   public Search getSearch() {
1917     return jpf.getSearch();
1918   }
1919
1920   /**
1921    * pushClinit all our static fields. Called from <clinit> and reset
1922    */
1923   static void initStaticFields () {
1924     error_id = 0;
1925   }
1926
1927   /**
1928    *  given an object reference, it returns the ApplicationContext of the process to which
1929    *  this object belongs
1930    */
1931   public abstract ApplicationContext getCurrentApplicationContext();
1932   public abstract ApplicationContext getApplicationContext(int objRef);
1933   public abstract ApplicationContext[] getApplicationContexts();
1934   public abstract String getSUTName();
1935   public abstract String getSUTDescription();
1936
1937   public abstract int getNumberOfApplications();
1938
1939   public Heap getHeap() {
1940     return ss.getHeap();
1941   }
1942
1943   public ElementInfo getElementInfo(int objref){
1944     return ss.getHeap().get(objref);
1945   }
1946
1947   public ElementInfo getModifiableElementInfo(int objref){
1948     return ss.getHeap().getModifiable(objref);
1949   }
1950
1951
1952   public ThreadInfo getCurrentThread () {
1953     return ThreadInfo.currentThread;
1954   }
1955
1956   public void registerClassLoader(ClassLoaderInfo cl) {
1957     this.getKernelState().addClassLoader(cl);
1958   }
1959
1960   public int registerThread (ThreadInfo ti){
1961     getKernelState().changed();
1962     return getThreadList().add(ti);
1963   }
1964
1965   /**
1966    * Returns the ClassLoader with the given globalId
1967    */
1968   protected ClassLoaderInfo getClassLoader(int gid) {
1969     return ss.ks.getClassLoader(gid);
1970   }
1971
1972   /**
1973    * <2do> this is where we will hook in a better time model
1974    */
1975   public long currentTimeMillis () {
1976     return timeModel.currentTimeMillis();
1977   }
1978
1979   /**
1980    * <2do> this is where we will hook in a better time model
1981    */
1982   public long nanoTime() {
1983     return timeModel.nanoTime();
1984   }
1985
1986   public void resetNextCG() {
1987     if (ss.nextCg != null) {
1988       ss.nextCg.reset();
1989     }
1990   }
1991
1992   /**
1993    * only for debugging, this is expensive
1994    *
1995    * If this is a store (forward) this is called before the state is stored.
1996    *
1997    * If this is a restore (visited forward or backtrack), this is called after
1998    * the state got restored
1999    */
2000   public void checkConsistency(boolean isStateStore) {
2001     getThreadList().checkConsistency( isStateStore);
2002     getHeap().checkConsistency( isStateStore);
2003   }
2004
2005   public abstract void terminateProcess (ThreadInfo ti);
2006
2007   // this is invoked by the heap (see GenericHeap.newInternString()) upon creating
2008   // the very first intern string
2009   public abstract Map<Integer,IntTable<String>> getInitialInternStringsMap();
2010
2011   // ---------- Predicates used to query threads from ThreadList ---------- //
2012
2013   public abstract Predicate<ThreadInfo> getRunnablePredicate();
2014
2015   public abstract Predicate<ThreadInfo> getDaemonRunnablePredicate();
2016
2017   public abstract Predicate<ThreadInfo> getAppTimedoutRunnablePredicate();
2018
2019   public Predicate<ThreadInfo> getUserTimedoutRunnablePredicate () {
2020     return userTimedoutRunnablePredicate;
2021   }
2022
2023   public Predicate<ThreadInfo> getUserLiveNonDaemonPredicate() {
2024     return userliveNonDaemonPredicate;
2025   }
2026
2027   public Predicate<ThreadInfo> getTimedoutRunnablePredicate () {
2028     return timedoutRunnablePredicate;
2029   }
2030
2031   public Predicate<ThreadInfo> getAlivePredicate () {
2032     return alivePredicate;
2033   }
2034
2035
2036   // ---------- Methods for handling finalizers ---------- //
2037
2038   public FinalizerThreadInfo getFinalizerThread() {
2039     return getCurrentApplicationContext().getFinalizerThread();
2040   }
2041
2042   abstract void updateFinalizerQueues();
2043
2044   public void processFinalizers() {
2045     if(processFinalizers) {
2046       updateFinalizerQueues();
2047       ChoiceGenerator<?> cg = getNextChoiceGenerator();
2048       if(cg==null || (cg.isSchedulingPoint() && !cg.isCascaded())) {
2049         getFinalizerThread().scheduleFinalizer();
2050       }
2051     }
2052   }
2053 }