2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
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;
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;
43 * This class represents the virtual machine. The virtual machine is able to
44 * move backward and forward one transition at a time.
46 public abstract class VM {
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)
53 public static final boolean CHECK_CONSISTENCY = false;
55 protected static final String[] EMPTY_ARGS = new String[0];
57 protected static JPFLogger log = JPF.getLogger("vm");
60 * our execution context
65 * The number of errors saved so far.
66 * Used to generate the name of the error trail file.
68 protected static int error_id;
71 * <2do> - this is a hack to be removed once there are no static references
74 protected static VM vm;
80 protected SystemState ss;
82 protected FunctionObjectFactory funcObjFactory = new FunctionObjectFactory();
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
92 protected Path path; /** execution path to current state */
93 protected StringBuilder out; /** buffer to store output along path execution */
96 * various caches for VMListener state acquisition. NOTE - these are only
97 * valid during notification
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
103 protected Transition lastTrailInfo;
105 protected boolean isTraceReplay; // can be set by listeners to indicate this is a replay
107 /** the repository we use to find out if we already have seen a state */
108 protected StateSet stateSet;
110 /** this was the last stateId - note this is also used for stateless model checking */
111 protected int newStateId;
113 /** the structure responsible for storing and restoring backtrack info */
114 protected Backtracker backtracker;
116 /** optional serializer/restorer to support backtracker */
117 protected StateRestorer<?> restorer;
119 /** optional serializer to support stateSet */
120 protected StateSerializer serializer;
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];
126 /** did we get a new transition */
127 protected boolean transitionOccurred;
129 /** how we model execution time */
130 protected TimeModel timeModel;
132 /** ThreadChoiceGenerator management related to data races and shared objects */
133 protected Scheduler scheduler;
136 protected Config config; // that's for the options we use only once
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;
145 // <2do> there are probably many places where this should be used
146 protected boolean isBigEndian;
148 protected boolean initialized;
151 protected Predicate<ThreadInfo> userliveNonDaemonPredicate;
152 protected Predicate<ThreadInfo> timedoutRunnablePredicate;
153 protected Predicate<ThreadInfo> alivePredicate;
154 protected Predicate<ThreadInfo> userTimedoutRunnablePredicate;
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>();
163 * be prepared this might throw JPFConfigExceptions
165 public VM (JPF jpf, Config conf) {
166 this.jpf = jpf; // so that we know who instantiated us
168 // <2do> that's really a bad hack and should be removed once we
169 // have cleaned up the reference chains
174 runGc = config.getBoolean("vm.gc", true);
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);
180 processFinalizers = config.getBoolean("vm.process_finalizers", false);
182 isBigEndian = getPlatformEndianness(config);
185 initTimeModel(config);
187 initSubsystems(config);
190 // set predicates used to query from threadlist
191 userliveNonDaemonPredicate = new Predicate<ThreadInfo>() {
193 public boolean isTrue (ThreadInfo ti) {
194 return (!ti.isDaemon() && !ti.isTerminated() && !ti.isSystemThread());
198 timedoutRunnablePredicate = new Predicate<ThreadInfo>() {
200 public boolean isTrue (ThreadInfo ti) {
201 return (ti.isTimeoutRunnable());
205 userTimedoutRunnablePredicate = new Predicate<ThreadInfo>() {
207 public boolean isTrue (ThreadInfo ti) {
208 return (ti.isTimeoutRunnable() && !ti.isSystemThread());
212 alivePredicate = new Predicate<ThreadInfo>() {
214 public boolean isTrue (ThreadInfo ti) {
215 return (ti.isAlive());
221 * just here for unit test mockups, don't use as implicit base ctor in
226 public JPF getJPF() {
230 public void initFields (Config config) {
231 path = new Path("fix-this!");
234 ss = new SystemState(config, this);
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);
241 scheduler = config.getEssentialInstance("vm.scheduler.class", Scheduler.class);
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);
255 // peer classes get initialized upon NativePeer creation
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);
265 * called after the JPF run is finished. Shouldn't be public, but is called by JPF
267 public void cleanUp(){
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")) {
277 } else if (endianness.equalsIgnoreCase("little")) {
280 config.exception("illegal vm.endian value: " + endianness);
281 return false; // doesn't matter
285 public boolean isBigEndianPlatform(){
289 public boolean finalizersEnabled() {
290 return processFinalizers;
293 public boolean isInitialized() {
297 public boolean isSingleProcess() {
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')
308 static boolean checkSystemClassCompatibility (SystemClassLoaderInfo systemLoader) {
309 ClassInfo ci = systemLoader.getClassClassInfo();
310 return ci.checkIfValidClassClassInfo();
313 static boolean isValidClassName (String clsName) {
314 if ( !clsName.matches("[a-zA-Z_$][a-zA-Z_$0-9.]*")) {
318 // well, those two could be part of valid class names, but
319 // in all likeliness somebody specified a filename instead of
321 if (clsName.endsWith(".java")) {
324 if (clsName.endsWith(".class")) {
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);
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);
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);
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);
361 * the minimal set of system classes we need for initialization
363 protected List<String> getStartupSystemClassNames() {
364 ArrayList<String> startupClasses = new ArrayList<String>(64);
367 startupClasses.add("java.lang.Object");
368 startupClasses.add("java.lang.Class");
369 startupClasses.add("java.lang.ClassLoader");
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");
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");
400 // the cache for box types
401 startupClasses.add("gov.nasa.jpf.BoxObjectCaches");
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");
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);
427 // the main class has to be handled separately since it might be VM specific
429 return startupClasses;
433 * return a list of ClassInfos for essential system types
435 * If system classes are not found, or are not valid JPF model classes, we throw
436 * a JPFConfigException and exit
438 * returned ClassInfos are not yet registered in Statics and don't have class objects
440 protected List<ClassInfo> getStartupSystemClassInfos (SystemClassLoaderInfo sysCl, ThreadInfo tiMain){
441 LinkedList<ClassInfo> list = new LinkedList<ClassInfo>();
444 for (String clsName : getStartupSystemClassNames()) {
445 ClassInfo ci = sysCl.getResolvedClassInfo(clsName);
446 ci.registerStartupClass( tiMain, list); // takes care of superclasses and interfaces
448 } catch (ClassInfoException e){
450 throw new JPFConfigException("cannot load system class " + e.getFailedClass());
457 * this adds the application main class and its supers to the list of startup classes
459 protected ClassInfo getMainClassInfo (SystemClassLoaderInfo sysCl, String mainClassName, ThreadInfo tiMain, List<ClassInfo> list){
461 ClassInfo ciMain = sysCl.getResolvedClassInfo(mainClassName);
462 ciMain.registerStartupClass(tiMain, list); // this might add a couple more
466 } catch (ClassInfoException e){
467 throw new JPFConfigException("cannot load application class " + e.getFailedClass());
472 * these are called when creating ApplicationContexts and can be overridden by concrete VM types
474 protected SystemClassLoaderInfo createSystemClassLoaderInfo (int appId) {
475 Class<?>[] argTypes = { VM.class, int.class };
477 Object[] args = { this, Integer.valueOf(appId)};
478 SystemClassLoaderInfo sysCli = config.getEssentialInstance("vm.classloader.class", SystemClassLoaderInfo.class, argTypes, args);
482 protected void createSystemClassLoaderObject (SystemClassLoaderInfo sysCl, ThreadInfo tiMain) {
483 Heap heap = getHeap();
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());
492 sysCl.setClassLoaderObject(ei);
495 protected void pushMainEntryArgs (MethodInfo miMain, String[] args, ThreadInfo tiMain, DirectCallStackFrame frame){
496 String sig = miMain.getSignature();
497 Heap heap = getHeap();
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());
505 frame.setReferenceArgument( 0, eiArgs.getObjectRef(), null);
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);
512 frame.setReferenceArgument( 0, MJIEnv.NULL, null);
515 } else if (!sig.contains("()")){
516 throw new JPFException("unsupported main entry signature: " + miMain.getFullName());
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);
526 protected MethodInfo getMainEntryMethodInfo (String mthName, ClassInfo ciMain) {
527 MethodInfo miMain = ciMain.getMethod(mthName, true);
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);
537 protected void pushClinits (List<ClassInfo> startupClasses, ThreadInfo tiMain) {
538 for (ClassInfo ci : startupClasses){
539 MethodInfo mi = ci.getMethod("<clinit>()V", false);
541 DirectCallStackFrame frame = mi.createDirectCallStackFrame(tiMain, 0);
542 tiMain.pushFrame(frame);
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
553 public abstract boolean initialize ();
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)
560 protected ThreadInfo initializeMainThread (ApplicationContext appCtx, int tid){
561 SystemClassLoaderInfo sysCl = appCtx.sysCl;
563 ThreadInfo tiMain = createMainThreadInfo(tid, appCtx);
564 List<ClassInfo> startupClasses = getStartupSystemClassInfos(sysCl, tiMain);
565 ClassInfo ciMain = getMainClassInfo(sysCl, appCtx.mainClassName, tiMain, startupClasses);
567 if (!checkSystemClassCompatibility( sysCl)){
568 throw new JPFConfigException("non-JPF system classes, check classpath");
571 // create essential objects (we can't call ctors yet)
572 createSystemClassLoaderObject(sysCl, tiMain);
573 for (ClassInfo ci : startupClasses) {
574 ci.createAndLinkStartupClassObject(tiMain);
576 tiMain.createMainThreadObject(sysCl);
577 registerThread(tiMain);
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);
586 registerThreadListCleanup(sysCl.getThreadClassInfo());
591 protected void initializeFinalizerThread (ApplicationContext appCtx, int tid) {
592 if(processFinalizers) {
593 ApplicationContext app = getCurrentApplicationContext();
594 FinalizerThreadInfo finalizerTi = app.getFinalizerThread();
596 finalizerTi = (FinalizerThreadInfo) createFinalizerThreadInfo(tid, app);
597 finalizerTi.createFinalizerThreadObject(app.getSystemClassLoader());
599 appCtx.setFinalizerThread(finalizerTi);
603 protected void registerThreadListCleanup (ClassInfo ciThread){
604 assert ciThread != null : "java.lang.Thread not loaded yet";
606 ciThread.addReleaseAction( new ReleaseAction(){
608 public void release (ElementInfo ei) {
609 ThreadList tl = getThreadList();
610 int objRef = ei.getObjectRef();
611 ThreadInfo ti = tl.getThreadInfoForObjRef(objRef);
613 vm.getKernelState().changed();
621 * override this if the concrete VM needs a special root CG
623 protected void setRootCG(){
624 scheduler.setRootCG();
627 protected void initSystemState (ThreadInfo mainThread){
628 ss.setStartThread(mainThread);
630 ss.recordSteps(hasToRecordSteps());
632 if (!pathOutput) { // don't override if explicitly requested
633 pathOutput = hasToRecordPathOutput();
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);
641 transitionOccurred = true;
644 public void addPostGcAction (Runnable r){
645 postGcActions.add(r);
649 * to be called from the Heap after GC is completed (i.e. only live objects remain)
651 public void processPostGcActions(){
652 if (!postGcActions.isEmpty()){
653 for (Runnable r : postGcActions){
657 postGcActions.clear();
661 public void addListener (VMListener newListener) {
662 log.info("VMListener added: ", newListener);
663 listeners = Misc.appendElement(listeners, newListener);
666 public boolean hasListenerOfType (Class<?> listenerCls) {
667 return Misc.hasElementOfType(listeners, listenerCls);
670 public <T> T getNextListenerOfType(Class<T> type, T prev){
671 return Misc.getNextElementOfType(listeners, type, prev);
674 public void removeListener (VMListener removeListener) {
675 listeners = Misc.removeElement(listeners, removeListener);
678 public void setTraceReplay (boolean isReplay) {
679 isTraceReplay = isReplay;
682 public boolean isTraceReplay() {
683 return isTraceReplay;
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");
693 public void recordSteps( boolean cond) {
694 // <2do> not ideal - it might be already too late when this is called
696 config.setProperty("vm.store_steps", cond ? "true" : "false");
699 ss.recordSteps(cond);
703 public boolean hasToRecordPathOutput() {
704 if (config.getBoolean("vm.path_output")){ // explicitly requested
707 return jpf.getReporter().hasToReportOutput(); // implicilty required
711 //--- VM listener notifications
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)
720 protected void notifyVMInitialized () {
722 for (int i = 0; i < listeners.length; i++) {
723 listeners[i].vmInitialized(this);
725 } catch (UncaughtException x) {
727 } catch (JPF.ExitException x) {
729 } catch (Throwable t) {
730 throw new JPFListenerException("exception during vmInitialized() notification", t);
734 protected void notifyChoiceGeneratorRegistered (ChoiceGenerator<?>cg, ThreadInfo ti) {
736 for (int i = 0; i < listeners.length; i++) {
737 listeners[i].choiceGeneratorRegistered(this, cg, ti, ti.getPC());
739 } catch (UncaughtException x) {
741 } catch (JPF.ExitException x) {
743 } catch (Throwable t) {
744 throw new JPFListenerException("exception during choiceGeneratorRegistered() notification", t);
748 protected void notifyChoiceGeneratorSet (ChoiceGenerator<?>cg) {
750 for (int i = 0; i < listeners.length; i++) {
751 listeners[i].choiceGeneratorSet(this, cg);
753 } catch (UncaughtException x) {
755 } catch (JPF.ExitException x) {
757 } catch (Throwable t) {
758 throw new JPFListenerException("exception during choiceGeneratorSet() notification", t);
762 protected void notifyChoiceGeneratorAdvanced (ChoiceGenerator<?>cg) {
764 for (int i = 0; i < listeners.length; i++) {
765 listeners[i].choiceGeneratorAdvanced(this, cg);
767 } catch (UncaughtException x) {
769 } catch (JPF.ExitException x) {
771 } catch (Throwable t) {
772 throw new JPFListenerException("exception during choiceGeneratorAdvanced() notification", t);
776 protected void notifyChoiceGeneratorProcessed (ChoiceGenerator<?>cg) {
778 for (int i = 0; i < listeners.length; i++) {
779 listeners[i].choiceGeneratorProcessed(this, cg);
781 } catch (UncaughtException x) {
783 } catch (JPF.ExitException x) {
785 } catch (Throwable t) {
786 throw new JPFListenerException("exception during choiceGeneratorProcessed() notification", t);
790 protected void notifyExecuteInstruction (ThreadInfo ti, Instruction insn) {
792 for (int i = 0; i < listeners.length; i++) {
793 listeners[i].executeInstruction(this, ti, insn);
795 } catch (UncaughtException x) {
797 } catch (JPF.ExitException x) {
799 } catch (Throwable t) {
800 throw new JPFListenerException("exception during executeInstruction() notification", t);
804 protected void notifyInstructionExecuted (ThreadInfo ti, Instruction insn, Instruction nextInsn) {
806 //listener.instructionExecuted(this);
807 for (int i = 0; i < listeners.length; i++) {
808 listeners[i].instructionExecuted(this, ti, nextInsn, insn);
810 } catch (UncaughtException x) {
812 } catch (JPF.ExitException x) {
814 } catch (Throwable t) {
815 throw new JPFListenerException("exception during instructionExecuted() notification", t);
819 protected void notifyThreadStarted (ThreadInfo ti) {
821 for (int i = 0; i < listeners.length; i++) {
822 listeners[i].threadStarted(this, ti);
824 } catch (UncaughtException x) {
826 } catch (JPF.ExitException x) {
828 } catch (Throwable t) {
829 throw new JPFListenerException("exception during threadStarted() notification", t);
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) {
837 for (int i = 0; i < listeners.length; i++) {
838 listeners[i].threadBlocked(this, ti, ti.getLockObject());
840 } catch (UncaughtException x) {
842 } catch (JPF.ExitException x) {
844 } catch (Throwable t) {
845 throw new JPFListenerException("exception during threadBlocked() notification", t);
849 protected void notifyThreadWaiting (ThreadInfo ti) {
851 for (int i = 0; i < listeners.length; i++) {
852 listeners[i].threadWaiting(this, ti);
854 } catch (UncaughtException x) {
856 } catch (JPF.ExitException x) {
858 } catch (Throwable t) {
859 throw new JPFListenerException("exception during threadWaiting() notification", t);
863 protected void notifyThreadNotified (ThreadInfo ti) {
865 for (int i = 0; i < listeners.length; i++) {
866 listeners[i].threadNotified(this, ti);
868 } catch (UncaughtException x) {
870 } catch (JPF.ExitException x) {
872 } catch (Throwable t) {
873 throw new JPFListenerException("exception during threadNotified() notification", t);
877 protected void notifyThreadInterrupted (ThreadInfo ti) {
879 for (int i = 0; i < listeners.length; i++) {
880 listeners[i].threadInterrupted(this, ti);
882 } catch (UncaughtException x) {
884 } catch (JPF.ExitException x) {
886 } catch (Throwable t) {
887 throw new JPFListenerException("exception during threadInterrupted() notification", t);
891 protected void notifyThreadTerminated (ThreadInfo ti) {
893 for (int i = 0; i < listeners.length; i++) {
894 listeners[i].threadTerminated(this, ti);
896 } catch (UncaughtException x) {
898 } catch (JPF.ExitException x) {
900 } catch (Throwable t) {
901 throw new JPFListenerException("exception during threadTerminated() notification", t);
905 protected void notifyThreadScheduled (ThreadInfo ti) {
907 for (int i = 0; i < listeners.length; i++) {
908 listeners[i].threadScheduled(this, ti);
910 } catch (UncaughtException x) {
912 } catch (JPF.ExitException x) {
914 } catch (Throwable t) {
915 throw new JPFListenerException("exception during threadScheduled() notification", t);
919 protected void notifyLoadClass (ClassFile cf){
921 for (int i = 0; i < listeners.length; i++) {
922 listeners[i].loadClass(this, cf);
924 } catch (UncaughtException x) {
926 } catch (JPF.ExitException x) {
928 } catch (Throwable t) {
929 throw new JPFListenerException("exception during classLoaded() notification", t);
933 protected void notifyClassLoaded(ClassInfo ci) {
935 for (int i = 0; i < listeners.length; i++) {
936 listeners[i].classLoaded(this, ci);
938 } catch (UncaughtException x) {
940 } catch (JPF.ExitException x) {
942 } catch (Throwable t) {
943 throw new JPFListenerException("exception during classLoaded() notification", t);
947 protected void notifyObjectCreated(ThreadInfo ti, ElementInfo ei) {
949 for (int i = 0; i < listeners.length; i++) {
950 listeners[i].objectCreated(this, ti, ei);
952 } catch (UncaughtException x) {
954 } catch (JPF.ExitException x) {
956 } catch (Throwable t) {
957 throw new JPFListenerException("exception during objectCreated() notification", t);
961 protected void notifyObjectReleased(ThreadInfo ti, ElementInfo ei) {
963 for (int i = 0; i < listeners.length; i++) {
964 listeners[i].objectReleased(this, ti, ei);
966 } catch (UncaughtException x) {
968 } catch (JPF.ExitException x) {
970 } catch (Throwable t) {
971 throw new JPFListenerException("exception during objectReleased() notification", t);
975 protected void notifyObjectLocked(ThreadInfo ti, ElementInfo ei) {
977 for (int i = 0; i < listeners.length; i++) {
978 listeners[i].objectLocked(this, ti, ei);
980 } catch (UncaughtException x) {
982 } catch (JPF.ExitException x) {
984 } catch (Throwable t) {
985 throw new JPFListenerException("exception during objectLocked() notification", t);
989 protected void notifyObjectUnlocked(ThreadInfo ti, ElementInfo ei) {
991 for (int i = 0; i < listeners.length; i++) {
992 listeners[i].objectUnlocked(this, ti, ei);
994 } catch (UncaughtException x) {
996 } catch (JPF.ExitException x) {
998 } catch (Throwable t) {
999 throw new JPFListenerException("exception during objectUnlocked() notification", t);
1003 protected void notifyObjectWait(ThreadInfo ti, ElementInfo ei) {
1005 for (int i = 0; i < listeners.length; i++) {
1006 listeners[i].objectWait(this, ti, ei);
1008 } catch (UncaughtException x) {
1010 } catch (JPF.ExitException x) {
1012 } catch (Throwable t) {
1013 throw new JPFListenerException("exception during objectWait() notification", t);
1017 protected void notifyObjectExposed(ThreadInfo ti, ElementInfo eiShared, ElementInfo eiExposed) {
1019 for (int i = 0; i < listeners.length; i++) {
1020 listeners[i].objectExposed(this, ti, eiShared, eiExposed);
1022 } catch (UncaughtException x) {
1024 } catch (JPF.ExitException x) {
1026 } catch (Throwable t) {
1027 throw new JPFListenerException("exception during objectExposed() notification", t);
1031 protected void notifyObjectShared(ThreadInfo ti, ElementInfo ei) {
1033 for (int i = 0; i < listeners.length; i++) {
1034 listeners[i].objectShared(this, ti, ei);
1036 } catch (UncaughtException x) {
1038 } catch (JPF.ExitException x) {
1040 } catch (Throwable t) {
1041 throw new JPFListenerException("exception during objectShared() notification", t);
1045 protected void notifyObjectNotifies(ThreadInfo ti, ElementInfo ei) {
1047 for (int i = 0; i < listeners.length; i++) {
1048 listeners[i].objectNotify(this, ti, ei);
1050 } catch (UncaughtException x) {
1052 } catch (JPF.ExitException x) {
1054 } catch (Throwable t) {
1055 throw new JPFListenerException("exception during objectNotifies() notification", t);
1059 protected void notifyObjectNotifiesAll(ThreadInfo ti, ElementInfo ei) {
1061 for (int i = 0; i < listeners.length; i++) {
1062 listeners[i].objectNotifyAll(this, ti, ei);
1064 } catch (UncaughtException x) {
1066 } catch (JPF.ExitException x) {
1068 } catch (Throwable t) {
1069 throw new JPFListenerException("exception during objectNotifiesAll() notification", t);
1073 protected void notifyGCBegin() {
1075 for (int i = 0; i < listeners.length; i++) {
1076 listeners[i].gcBegin(this);
1078 } catch (UncaughtException x) {
1080 } catch (JPF.ExitException x) {
1082 } catch (Throwable t) {
1083 throw new JPFListenerException("exception during gcBegin() notification", t);
1087 protected void notifyGCEnd() {
1089 for (int i = 0; i < listeners.length; i++) {
1090 listeners[i].gcEnd(this);
1092 } catch (UncaughtException x) {
1094 } catch (JPF.ExitException x) {
1096 } catch (Throwable t) {
1097 throw new JPFListenerException("exception during gcEnd() notification", t);
1101 protected void notifyExceptionThrown(ThreadInfo ti, ElementInfo ei) {
1103 for (int i = 0; i < listeners.length; i++) {
1104 listeners[i].exceptionThrown(this, ti, ei);
1106 } catch (UncaughtException x) {
1108 } catch (JPF.ExitException x) {
1110 } catch (Throwable t) {
1111 throw new JPFListenerException("exception during exceptionThrown() notification", t);
1115 protected void notifyExceptionBailout(ThreadInfo ti) {
1117 for (int i = 0; i < listeners.length; i++) {
1118 listeners[i].exceptionBailout(this, ti);
1120 } catch (UncaughtException x) {
1122 } catch (JPF.ExitException x) {
1124 } catch (Throwable t) {
1125 throw new JPFListenerException("exception during exceptionBailout() notification", t);
1129 protected void notifyExceptionHandled(ThreadInfo ti) {
1131 for (int i = 0; i < listeners.length; i++) {
1132 listeners[i].exceptionHandled(this, ti);
1134 } catch (UncaughtException x) {
1136 } catch (JPF.ExitException x) {
1138 } catch (Throwable t) {
1139 throw new JPFListenerException("exception during exceptionHandled() notification", t);
1143 protected void notifyMethodEntered(ThreadInfo ti, MethodInfo mi) {
1145 for (int i = 0; i < listeners.length; i++) {
1146 listeners[i].methodEntered(this, ti, mi);
1148 } catch (UncaughtException x) {
1150 } catch (JPF.ExitException x) {
1152 } catch (Throwable t) {
1153 throw new JPFListenerException("exception during methodEntered() notification", t);
1157 protected void notifyMethodExited(ThreadInfo ti, MethodInfo mi) {
1159 for (int i = 0; i < listeners.length; i++) {
1160 listeners[i].methodExited(this, ti, mi);
1162 } catch (UncaughtException x) {
1164 } catch (JPF.ExitException x) {
1166 } catch (Throwable t) {
1167 throw new JPFListenerException("exception during methodExited() notification", t);
1171 // VMListener acquisition
1172 public String getThreadName () {
1173 ThreadInfo ti = ThreadInfo.getCurrentThread();
1175 return ti.getName();
1178 // VMListener acquisition
1179 public Instruction getInstruction () {
1180 ThreadInfo ti = ThreadInfo.getCurrentThread();
1185 * note this is gone after backtracking or starting the next exception
1187 public ExceptionInfo getPendingException () {
1188 ThreadInfo ti = ThreadInfo.getCurrentThread();
1191 return ti.getPendingException();
1197 public Step getLastStep () {
1198 Transition trail = ss.getTrail();
1199 if (trail != null) {
1200 return trail.getLastStep();
1206 public Transition getLastTransition () {
1207 if (path.size() == 0) {
1210 return path.get(path.size() - 1);
1213 public ClassInfo getClassInfo (int objref) {
1214 if (objref != MJIEnv.NULL) {
1215 return getElementInfo(objref).getClassInfo();
1222 * NOTE: only use this locally, since the path is getting modified by the VM
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
1228 public Path getPath () {
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
1236 public Transition getCurrentTransition() {
1237 return ss.getTrail();
1241 * use that one if you have to store the path for subsequent use
1243 * NOTE: without a prior call to updatePath(), this does NOT contain the
1244 * ongoing transition. See getPath() for usage from a VMListener
1246 public Path getClonedPath () {
1247 return path.clone();
1250 public int getPathLength () {
1254 public ThreadList getThreadList () {
1255 return getKernelState().getThreadList();
1258 public ClassLoaderList getClassLoaderList() {
1259 return getKernelState().getClassLoaderList();
1264 * Bundles up the state of the system for export
1266 public RestorableVMState getRestorableState () {
1267 return new RestorableVMState(this);
1271 * Gets the system state.
1273 public SystemState getSystemState () {
1277 public KernelState getKernelState () {
1278 return ss.getKernelState();
1281 public void kernelStateChanged(){
1282 ss.getKernelState().changed();
1285 public Config getConfig() {
1289 public Backtracker getBacktracker() {
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;
1301 // config read only if serializer is not also a restorer
1302 restorer = config.getInstance("vm.restorer.class", StateRestorer.class);
1304 restorer.attach(this);
1307 return (StateRestorer<T>) restorer;
1310 public StateSerializer getSerializer() {
1311 if (serializer == null) {
1312 serializer = config.getEssentialInstance("vm.serializer.class",
1313 StateSerializer.class);
1314 serializer.attach(this);
1319 public void setSerializer (StateSerializer newSerializer){
1320 serializer = newSerializer;
1321 serializer.attach(this);
1325 * Returns the stateSet if states are being matched.
1327 public StateSet getStateSet() {
1331 public Scheduler getScheduler(){
1335 public FunctionObjectFactory getFunctionObjectFacotry() {
1336 return funcObjFactory;
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)
1344 public ChoiceGenerator<?> getChoiceGenerator () {
1345 return ss.getChoiceGenerator();
1348 public ChoiceGenerator<?> getNextChoiceGenerator() {
1349 return ss.getNextChoiceGenerator();
1352 public boolean hasNextChoiceGenerator(){
1353 return (ss.getNextChoiceGenerator() != null);
1356 public boolean setNextChoiceGenerator (ChoiceGenerator<?> cg){
1357 return ss.setNextChoiceGenerator(cg);
1360 public void setMandatoryNextChoiceGenerator (ChoiceGenerator<?> cg, String failMsg){
1361 ss.setMandatoryNextChoiceGenerator(cg, failMsg);
1365 * return the latest registered ChoiceGenerator used in this transition
1366 * that matches the provided 'id' and is of 'cgType'.
1368 * This should be the main getter for clients that are cascade aware
1370 public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator (String id, Class<T> cgType) {
1371 return ss.getCurrentChoiceGenerator(id,cgType);
1375 * returns all ChoiceGenerators in current path
1377 public ChoiceGenerator<?>[] getChoiceGenerators() {
1378 return ss.getChoiceGenerators();
1381 public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType (Class<T> cgType) {
1382 return ss.getChoiceGeneratorsOfType(cgType);
1385 public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType (Class<T> cgType){
1386 return ss.getLastChoiceGeneratorOfType(cgType);
1389 public ChoiceGenerator<?> getLastChoiceGeneratorInThread (ThreadInfo ti){
1390 return ss.getLastChoiceGeneratorInThread(ti);
1393 public void print (String s) {
1395 System.out.print(s);
1403 public void println (String s) {
1406 StringBuilder indent = new StringBuilder();
1408 for (i = 0;i<=path.size();i++) {
1409 indent.append('|').append(i);
1411 indent.append("|").append(s);
1412 System.out.println(indent);
1415 System.out.println(s);
1425 public void print (boolean b) {
1427 System.out.print(b);
1431 appendOutput(Boolean.toString(b));
1435 public void print (char c) {
1437 System.out.print(c);
1445 public void print (int i) {
1447 System.out.print(i);
1451 appendOutput(Integer.toString(i));
1455 public void print (long l) {
1457 System.out.print(l);
1461 appendOutput(Long.toString(l));
1465 public void print (double d) {
1467 System.out.print(d);
1471 appendOutput(Double.toString(d));
1475 public void print (float f) {
1477 System.out.print(f);
1481 appendOutput(Float.toString(f));
1485 public void println () {
1487 System.out.println();
1496 void appendOutput (String s) {
1498 out = new StringBuilder();
1503 void appendOutput (char c) {
1505 out = new StringBuilder();
1511 * get the pending output (not yet stored in the path)
1513 public String getPendingOutput() {
1514 if (out != null && out.length() > 0){
1515 return out.toString();
1522 * this is here so that we can intercept it in subclassed VMs
1524 public Instruction handleException (ThreadInfo ti, int xObjRef){
1525 ti = null; // Get rid of IDE warning
1530 public void storeTrace (String fileName, String comment, boolean verbose) {
1531 ChoicePoint.storeTrace(fileName, getSUTName(), comment,
1532 ss.getChoiceGenerators(), verbose);
1535 public void storePathOutput () {
1539 private void printCG (ChoiceGenerator<?> cg, int n){
1540 ChoiceGenerator cgPrev = cg.getPreviousChoiceGenerator();
1541 if (cgPrev != null){
1542 printCG( cgPrev, --n);
1545 System.out.printf("[%d] ", n);
1546 System.out.println(cg);
1549 // for debugging purposes
1550 public void printChoiceGeneratorStack(){
1551 ChoiceGenerator<?> cg = getChoiceGenerator();
1553 int n = cg.getNumberOfParents();
1558 public ThreadInfo[] getLiveThreads () {
1559 return getThreadList().getThreads();
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)
1567 public void printLiveThreadStatus (PrintWriter pw) {
1568 int nThreads = ss.getThreadCount();
1569 ThreadInfo[] threads = getThreadList().getThreads();
1572 for (int i = 0; i < nThreads; i++) {
1573 ThreadInfo ti = threads[i];
1575 if (ti.getStackDepth() > 0){
1577 //pw.print("Thread: ");
1578 //pw.print(tiMain.getName());
1579 pw.println(ti.getStateDescription());
1581 List<ElementInfo> locks = ti.getLockedObjects();
1582 if (!locks.isEmpty()) {
1583 pw.print(" owned locks:");
1584 boolean first = true;
1585 for (ElementInfo e : locks) {
1596 ElementInfo ei = ti.getLockObject();
1598 if (ti.getState() == ThreadInfo.State.WAITING) {
1599 pw.print( " waiting on: ");
1601 pw.print( " blocked on: ");
1606 pw.println(" call stack:");
1607 for (StackFrame frame : ti){
1608 if (!frame.isDirectCallFrame()) {
1610 pw.println(frame.getStackTraceInfo());
1619 pw.println("no live threads");
1623 // just a debugging aid
1624 public void dumpThreadStates () {
1625 java.io.PrintWriter pw = new java.io.PrintWriter(System.out, true);
1626 printLiveThreadStatus(pw);
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)
1637 public boolean backtrack () {
1638 transitionOccurred = false;
1640 boolean success = backtracker.backtrack();
1642 if (CHECK_CONSISTENCY) checkConsistency(false);
1646 lastTrailInfo = path.getLast();
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
1660 public void updatePath () {
1661 Transition t = ss.getTrail();
1662 Transition tLast = path.getLast();
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
1668 // <2do> we should probably store the output directly in the TrailInfo,
1669 // but this might not be our only annotation in the future
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());
1682 * advance the program state
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
1688 * @return 'true' if there was an un-executed sequence out of the current state,
1689 * 'false' if it was completely explored
1692 public boolean forward () {
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
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.
1708 // actually, it hasn't occurred yet, but will
1709 transitionOccurred = ss.initializeNextTransition(this);
1711 if (transitionOccurred){
1712 if (CHECK_CONSISTENCY) {
1713 checkConsistency(true); // don't push an inconsistent state
1716 backtracker.pushKernelState();
1718 // cache this before we enter (and increment) the next insn(s)
1719 lastTrailInfo = path.getLast();
1722 ss.executeNextTransition(vm);
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
1729 backtracker.pushSystemState();
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
1737 if (runGc && !hasPendingException()) {
1738 if(ss.gcIfNeeded()) {
1739 processFinalizers();
1743 if (stateSet != null) {
1744 newStateId = stateSet.size();
1745 int id = stateSet.addCurrent();
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
1757 return false; // no transition occurred
1762 * Prints the current stack trace. Just for debugging purposes
1764 public void printCurrentStackTrace () {
1765 ThreadInfo th = ThreadInfo.getCurrentThread();
1768 th.printStackTrace();
1773 public void restoreState (RestorableVMState state) {
1774 if (state.path == null) {
1775 throw new JPFException("tried to restore partial VMState: " + state);
1777 backtracker.restoreState(state.getBkState());
1778 path = state.path.clone();
1781 public void activateGC () {
1786 //--- various state attribute getters and setters (mostly forwarding to SystemState)
1788 public void retainStateAttributes (boolean isRetained){
1789 ss.retainAttributes(isRetained);
1792 public void forceState () {
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
1801 public void ignoreState (boolean cond) {
1802 ss.setIgnored(cond);
1805 public void ignoreState(){
1810 * imperatively break the transition to enable state matching
1812 public void breakTransition (String reason) {
1813 ThreadInfo ti = ThreadInfo.getCurrentThread();
1814 ti.breakTransition(reason);
1817 public boolean transitionOccurred(){
1818 return transitionOccurred;
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)
1826 * this returns true if no state has been produced yet, and false if
1827 * no transition occurred after a forward call
1829 public boolean isNewState() {
1831 if (!transitionOccurred){
1835 if (stateSet != null) {
1838 } else if (ss.isIgnored()){
1841 return (newStateId == ss.getId());
1844 } else { // stateless model checking - each transition leads to a new state
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
1855 public abstract boolean isEndState ();
1857 public boolean isVisitedState(){
1858 return !isNewState();
1861 public boolean isIgnoredState(){
1862 return ss.isIgnored();
1865 public boolean isInterestingState () {
1866 return ss.isInteresting();
1869 public boolean isBoringState () {
1870 return ss.isBoring();
1873 public boolean hasPendingException () {
1874 return (getPendingException() != null);
1877 public abstract boolean isDeadlocked ();
1879 public Exception getException () {
1880 return ss.getUncaughtException();
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
1890 public int getStateId() {
1894 public int getStateCount() {
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.
1907 public static VM getVM () {
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
1916 public Search getSearch() {
1917 return jpf.getSearch();
1921 * pushClinit all our static fields. Called from <clinit> and reset
1923 static void initStaticFields () {
1928 * given an object reference, it returns the ApplicationContext of the process to which
1929 * this object belongs
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();
1937 public abstract int getNumberOfApplications();
1939 public Heap getHeap() {
1940 return ss.getHeap();
1943 public ElementInfo getElementInfo(int objref){
1944 return ss.getHeap().get(objref);
1947 public ElementInfo getModifiableElementInfo(int objref){
1948 return ss.getHeap().getModifiable(objref);
1952 public ThreadInfo getCurrentThread () {
1953 return ThreadInfo.currentThread;
1956 public void registerClassLoader(ClassLoaderInfo cl) {
1957 this.getKernelState().addClassLoader(cl);
1960 public int registerThread (ThreadInfo ti){
1961 getKernelState().changed();
1962 return getThreadList().add(ti);
1966 * Returns the ClassLoader with the given globalId
1968 protected ClassLoaderInfo getClassLoader(int gid) {
1969 return ss.ks.getClassLoader(gid);
1973 * <2do> this is where we will hook in a better time model
1975 public long currentTimeMillis () {
1976 return timeModel.currentTimeMillis();
1980 * <2do> this is where we will hook in a better time model
1982 public long nanoTime() {
1983 return timeModel.nanoTime();
1986 public void resetNextCG() {
1987 if (ss.nextCg != null) {
1993 * only for debugging, this is expensive
1995 * If this is a store (forward) this is called before the state is stored.
1997 * If this is a restore (visited forward or backtrack), this is called after
1998 * the state got restored
2000 public void checkConsistency(boolean isStateStore) {
2001 getThreadList().checkConsistency( isStateStore);
2002 getHeap().checkConsistency( isStateStore);
2005 public abstract void terminateProcess (ThreadInfo ti);
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();
2011 // ---------- Predicates used to query threads from ThreadList ---------- //
2013 public abstract Predicate<ThreadInfo> getRunnablePredicate();
2015 public abstract Predicate<ThreadInfo> getDaemonRunnablePredicate();
2017 public abstract Predicate<ThreadInfo> getAppTimedoutRunnablePredicate();
2019 public Predicate<ThreadInfo> getUserTimedoutRunnablePredicate () {
2020 return userTimedoutRunnablePredicate;
2023 public Predicate<ThreadInfo> getUserLiveNonDaemonPredicate() {
2024 return userliveNonDaemonPredicate;
2027 public Predicate<ThreadInfo> getTimedoutRunnablePredicate () {
2028 return timedoutRunnablePredicate;
2031 public Predicate<ThreadInfo> getAlivePredicate () {
2032 return alivePredicate;
2036 // ---------- Methods for handling finalizers ---------- //
2038 public FinalizerThreadInfo getFinalizerThread() {
2039 return getCurrentApplicationContext().getFinalizerThread();
2042 abstract void updateFinalizerQueues();
2044 public void processFinalizers() {
2045 if(processFinalizers) {
2046 updateFinalizerQueues();
2047 ChoiceGenerator<?> cg = getNextChoiceGenerator();
2048 if(cg==null || (cg.isSchedulingPoint() && !cg.isCascaded())) {
2049 getFinalizerThread().scheduleFinalizer();