VM

java.lang.Object
- gov.nasa.jpf.vm.VM

Direct Known Subclasses:

MultiProcessVM, SingleProcessVM
```
public abstract class VM
extends java.lang.Object
```
This class represents the virtual machine. The virtual machine is able to move backward and forward one transition at a time.

Field Summary

Fields
Modifier and Type	Field and Description
`protected Predicate<ThreadInfo>`	`alivePredicate`
`protected Backtracker`	`backtracker` the structure responsible for storing and restoring backtrack info
`static boolean`	`CHECK_CONSISTENCY` this is a debugging aid to control compilation of expensive consistency checks (we don't control these with class-wise assertion enabling since we do use unconditional assertions for mandatory consistency checks)
`protected Config`	`config`
`protected static java.lang.String[]`	`EMPTY_ARGS`
`protected static int`	`error_id` The number of errors saved so far.
`protected FunctionObjectFactory`	`funcObjFactory`
`protected boolean`	`indentOutput`
`protected boolean`	`initialized`
`protected boolean`	`isBigEndian`
`protected boolean`	`isTraceReplay`
`protected JPF`	`jpf` our execution context
`protected Transition`	`lastTrailInfo` various caches for VMListener state acquisition.
`protected VMListener[]`	`listeners` potential execution listeners.
`protected static JPFLogger`	`log`
`protected int`	`newStateId` this was the last stateId - note this is also used for stateless model checking
`protected java.lang.StringBuilder`	`out` execution path to current state
`protected Path`	`path`
`protected boolean`	`pathOutput`
`protected java.util.ArrayList<java.lang.Runnable>`	`postGcActions`
`protected boolean`	`processFinalizers`
`protected StateRestorer<?>`	`restorer` optional serializer/restorer to support backtracker
`protected boolean`	`runGc`
`protected Scheduler`	`scheduler` ThreadChoiceGenerator management related to data races and shared objects
`protected StateSerializer`	`serializer` optional serializer to support stateSet
`protected SystemState`	`ss`
`protected StateSet`	`stateSet` the repository we use to find out if we already have seen a state
`protected Predicate<ThreadInfo>`	`timedoutRunnablePredicate`
`protected TimeModel`	`timeModel` how we model execution time
`protected boolean`	`transitionOccurred` did we get a new transition
`protected boolean`	`treeOutput`
`protected Predicate<ThreadInfo>`	`userliveNonDaemonPredicate`
`protected Predicate<ThreadInfo>`	`userTimedoutRunnablePredicate`
`protected static VM`	`vm` <2do> - this is a hack to be removed once there are no static references anymore

Constructor Summary

Constructors
Modifier	Constructor and Description
`protected`	`VM()` just here for unit test mockups, don't use as implicit base ctor in VM derived classes
	`VM(JPF jpf, Config conf)` be prepared this might throw JPFConfigExceptions

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`activateGC()`
`void`	`addListener(VMListener newListener)`
`void`	`addPostGcAction(java.lang.Runnable r)`
`boolean`	`backtrack()` Moves one step backward.
`void`	`breakTransition(java.lang.String reason)` imperatively break the transition to enable state matching
`void`	`checkConsistency(boolean isStateStore)` only for debugging, this is expensive If this is a store (forward) this is called before the state is stored.
`void`	`cleanUp()` called after the JPF run is finished.
`protected ThreadInfo`	`createFinalizerThreadInfo(int id, ApplicationContext appCtx)`
`protected ThreadInfo`	`createMainThreadInfo(int id, ApplicationContext appCtx)`
`protected SystemClassLoaderInfo`	`createSystemClassLoaderInfo(int appId)`
`protected void`	`createSystemClassLoaderObject(SystemClassLoaderInfo sysCl, ThreadInfo tiMain)`
`protected ThreadInfo`	`createThreadInfo(int objRef, int groupRef, int runnableRef, int nameRef)`
`long`	`currentTimeMillis()` <2do> this is where we will hook in a better time model
`void`	`dumpThreadStates()`
`boolean`	`finalizersEnabled()`
`void`	`forceState()`
`boolean`	`forward()` advance the program state forward() and backtrack() are the two primary interfaces towards the Search driver.
`Predicate<ThreadInfo>`	`getAlivePredicate()`
`abstract ApplicationContext`	`getApplicationContext(int objRef)`
`abstract ApplicationContext[]`	`getApplicationContexts()`
`abstract Predicate<ThreadInfo>`	`getAppTimedoutRunnablePredicate()`
`Backtracker`	`getBacktracker()`
`ChoiceGenerator<?>`	`getChoiceGenerator()` return the last registered SystemState's ChoiceGenerator object NOTE: there might be more than one ChoiceGenerator associated with the current transition (ChoiceGenerators can be cascaded)
`ChoiceGenerator<?>[]`	`getChoiceGenerators()` returns all ChoiceGenerators in current path
`<T extends ChoiceGenerator<?>> T[]`	`getChoiceGeneratorsOfType(java.lang.Class<T> cgType)`
`ClassInfo`	`getClassInfo(int objref)`
`protected ClassLoaderInfo`	`getClassLoader(int gid)` Returns the ClassLoader with the given globalId
`ClassLoaderList`	`getClassLoaderList()`
`Path`	`getClonedPath()` use that one if you have to store the path for subsequent use NOTE: without a prior call to updatePath(), this does NOT contain the ongoing transition.
`Config`	`getConfig()`
`abstract ApplicationContext`	`getCurrentApplicationContext()` given an object reference, it returns the ApplicationContext of the process to which this object belongs
`<T extends ChoiceGenerator<?>> T`	`getCurrentChoiceGenerator(java.lang.String id, java.lang.Class<T> cgType)` return the latest registered ChoiceGenerator used in this transition that matches the provided 'id' and is of 'cgType'.
`ThreadInfo`	`getCurrentThread()`
`Transition`	`getCurrentTransition()` this is the ongoing transition.
`abstract Predicate<ThreadInfo>`	`getDaemonRunnablePredicate()`
`ElementInfo`	`getElementInfo(int objref)`
`java.lang.Exception`	`getException()`
`FinalizerThreadInfo`	`getFinalizerThread()`
`FunctionObjectFactory`	`getFunctionObjectFacotry()`
`Heap`	`getHeap()`
`abstract java.util.Map<java.lang.Integer,IntTable<java.lang.String>>`	`getInitialInternStringsMap()`
`Instruction`	`getInstruction()`
`JPF`	`getJPF()`
`KernelState`	`getKernelState()`
`ChoiceGenerator<?>`	`getLastChoiceGeneratorInThread(ThreadInfo ti)`
`<T extends ChoiceGenerator<?>> T`	`getLastChoiceGeneratorOfType(java.lang.Class<T> cgType)`
`Step`	`getLastStep()`
`Transition`	`getLastTransition()`
`ThreadInfo[]`	`getLiveThreads()`
`protected ClassInfo`	`getMainClassInfo(SystemClassLoaderInfo sysCl, java.lang.String mainClassName, ThreadInfo tiMain, java.util.List<ClassInfo> list)` this adds the application main class and its supers to the list of startup classes
`protected MethodInfo`	`getMainEntryMethodInfo(java.lang.String mthName, ClassInfo ciMain)`
`ElementInfo`	`getModifiableElementInfo(int objref)`
`ChoiceGenerator<?>`	`getNextChoiceGenerator()`
`<T> T`	`getNextListenerOfType(java.lang.Class<T> type, T prev)`
`abstract int`	`getNumberOfApplications()`
`Path`	`getPath()` NOTE: only use this locally, since the path is getting modified by the VM The path only contains all states when queried from a stateAdvanced() notification.
`int`	`getPathLength()`
`ExceptionInfo`	`getPendingException()` note this is gone after backtracking or starting the next exception
`java.lang.String`	`getPendingOutput()` get the pending output (not yet stored in the path)
`protected boolean`	`getPlatformEndianness(Config config)`
`RestorableVMState`	`getRestorableState()` Bundles up the state of the system for export
`<T> StateRestorer<T>`	`getRestorer()`
`abstract Predicate<ThreadInfo>`	`getRunnablePredicate()`
`Scheduler`	`getScheduler()`
`Search`	`getSearch()` not ideal to have this here since it is kind of a backlink, but it's not any better if listeners have to dig this out from JPF Note - this isn't set during initialization, since the VM object is created first
`StateSerializer`	`getSerializer()`
`protected java.util.List<ClassInfo>`	`getStartupSystemClassInfos(SystemClassLoaderInfo sysCl, ThreadInfo tiMain)` return a list of ClassInfos for essential system types If system classes are not found, or are not valid JPF model classes, we throw a JPFConfigException and exit returned ClassInfos are not yet registered in Statics and don't have class objects
`protected java.util.List<java.lang.String>`	`getStartupSystemClassNames()` the minimal set of system classes we need for initialization
`int`	`getStateCount()`
`int`	`getStateId()` get the numeric id for the current state Note: this can be called several times (by the search and observers) for every forward()/backtrack(), so we want to cache things a bit
`StateSet`	`getStateSet()` Returns the stateSet if states are being matched.
`abstract java.lang.String`	`getSUTDescription()`
`abstract java.lang.String`	`getSUTName()`
`SystemState`	`getSystemState()` Gets the system state.
`ThreadList`	`getThreadList()`
`java.lang.String`	`getThreadName()`
`Predicate<ThreadInfo>`	`getTimedoutRunnablePredicate()`
`Predicate<ThreadInfo>`	`getUserLiveNonDaemonPredicate()`
`Predicate<ThreadInfo>`	`getUserTimedoutRunnablePredicate()`
`static VM`	`getVM()` <2do> this is a band aid to bundle all these legacy reference chains from JPFs past.
`Instruction`	`handleException(ThreadInfo ti, int xObjRef)` this is here so that we can intercept it in subclassed VMs
`boolean`	`hasListenerOfType(java.lang.Class<?> listenerCls)`
`boolean`	`hasNextChoiceGenerator()`
`boolean`	`hasPendingException()`
`boolean`	`hasToRecordPathOutput()`
`boolean`	`hasToRecordSteps()`
`void`	`ignoreState()`
`void`	`ignoreState(boolean cond)` override the state matching - ignore this state, no matter if we changed the heap or stacks.
`void`	`initFields(Config config)`
`abstract boolean`	`initialize()` this is the main initialization point that sets up startup objects threads and callstacks.
`protected void`	`initializeFinalizerThread(ApplicationContext appCtx, int tid)`
`protected ThreadInfo`	`initializeMainThread(ApplicationContext appCtx, int tid)` create and initialize the main thread for the given ApplicationContext.
`protected void`	`initSubsystems(Config config)`
`protected void`	`initSystemState(ThreadInfo mainThread)`
`protected void`	`initTimeModel(Config config)`
`boolean`	`isBigEndianPlatform()`
`boolean`	`isBoringState()`
`abstract boolean`	`isDeadlocked()`
`abstract boolean`	`isEndState()` We made this to be overriden by Single/MultiprcessesVM implementations, since for MultiprcessesVM one can decide when to terminate (after the the termination of all processes or only one process).
`boolean`	`isIgnoredState()`
`boolean`	`isInitialized()`
`boolean`	`isInterestingState()`
`boolean`	`isNewState()` answers if the current state already has been visited.
`boolean`	`isSingleProcess()`
`boolean`	`isTraceReplay()`
`boolean`	`isVisitedState()`
`void`	`kernelStateChanged()`
`long`	`nanoTime()` <2do> this is where we will hook in a better time model
`protected void`	`notifyChoiceGeneratorAdvanced(ChoiceGenerator<?> cg)`
`protected void`	`notifyChoiceGeneratorProcessed(ChoiceGenerator<?> cg)`
`protected void`	`notifyChoiceGeneratorRegistered(ChoiceGenerator<?> cg, ThreadInfo ti)`
`protected void`	`notifyChoiceGeneratorSet(ChoiceGenerator<?> cg)`
`protected void`	`notifyClassLoaded(ClassInfo ci)`
`protected void`	`notifyExceptionBailout(ThreadInfo ti)`
`protected void`	`notifyExceptionHandled(ThreadInfo ti)`
`protected void`	`notifyExceptionThrown(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyExecuteInstruction(ThreadInfo ti, Instruction insn)`
`protected void`	`notifyGCBegin()`
`protected void`	`notifyGCEnd()`
`protected void`	`notifyInstructionExecuted(ThreadInfo ti, Instruction insn, Instruction nextInsn)`
`protected void`	`notifyLoadClass(ClassFile cf)`
`protected void`	`notifyMethodEntered(ThreadInfo ti, MethodInfo mi)`
`protected void`	`notifyMethodExited(ThreadInfo ti, MethodInfo mi)`
`protected void`	`notifyObjectCreated(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectExposed(ThreadInfo ti, ElementInfo eiShared, ElementInfo eiExposed)`
`protected void`	`notifyObjectLocked(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectNotifies(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectNotifiesAll(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectReleased(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectShared(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectUnlocked(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyObjectWait(ThreadInfo ti, ElementInfo ei)`
`protected void`	`notifyThreadBlocked(ThreadInfo ti)`
`protected void`	`notifyThreadInterrupted(ThreadInfo ti)`
`protected void`	`notifyThreadNotified(ThreadInfo ti)`
`protected void`	`notifyThreadScheduled(ThreadInfo ti)`
`protected void`	`notifyThreadStarted(ThreadInfo ti)`
`protected void`	`notifyThreadTerminated(ThreadInfo ti)`
`protected void`	`notifyThreadWaiting(ThreadInfo ti)`
`protected void`	`notifyVMInitialized()`
`void`	`print(boolean b)`
`void`	`print(char c)`
`void`	`print(double d)`
`void`	`print(float f)`
`void`	`print(int i)`
`void`	`print(long l)`
`void`	`print(java.lang.String s)`
`void`	`printChoiceGeneratorStack()`
`void`	`printCurrentStackTrace()` Prints the current stack trace.
`void`	`printLiveThreadStatus(java.io.PrintWriter pw)` print call stacks of all live threads this is also used for debugging purposes, so we can't move it to the Reporter system (it's also using a bit too many internals for that)
`void`	`println()`
`void`	`println(java.lang.String s)`
`void`	`processFinalizers()`
`void`	`processPostGcActions()` to be called from the Heap after GC is completed (i.e.
`protected void`	`pushClinits(java.util.List<ClassInfo> startupClasses, ThreadInfo tiMain)`
`protected void`	`pushMainEntry(MethodInfo miMain, java.lang.String[] args, ThreadInfo tiMain)`
`protected void`	`pushMainEntryArgs(MethodInfo miMain, java.lang.String[] args, ThreadInfo tiMain, DirectCallStackFrame frame)`
`void`	`recordSteps(boolean cond)`
`void`	`registerClassLoader(ClassLoaderInfo cl)`
`int`	`registerThread(ThreadInfo ti)`
`protected void`	`registerThreadListCleanup(ClassInfo ciThread)`
`void`	`removeListener(VMListener removeListener)`
`void`	`resetNextCG()`
`void`	`restoreState(RestorableVMState state)`
`void`	`retainStateAttributes(boolean isRetained)`
`void`	`setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, java.lang.String failMsg)`
`boolean`	`setNextChoiceGenerator(ChoiceGenerator<?> cg)`
`protected void`	`setRootCG()` override this if the concrete VM needs a special root CG
`void`	`setSerializer(StateSerializer newSerializer)`
`void`	`setTraceReplay(boolean isReplay)`
`void`	`storePathOutput()`
`void`	`storeTrace(java.lang.String fileName, java.lang.String comment, boolean verbose)`
`abstract void`	`terminateProcess(ThreadInfo ti)`
`boolean`	`transitionOccurred()`
`void`	`updatePath()` store the current SystemState's Trail in our path, after updating it with whatever annotations the VM wants to add.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail
- CHECK_CONSISTENCY
```
public static final boolean CHECK_CONSISTENCY
```
  this is a debugging aid to control compilation of expensive consistency checks (we don't control these with class-wise assertion enabling since we do use unconditional assertions for mandatory consistency checks)
  
  See Also:
  
  Constant Field Values
- EMPTY_ARGS
```
protected static final java.lang.String[] EMPTY_ARGS
```
- log
```
protected static JPFLogger log
```
- jpf
```
protected JPF jpf
```
  our execution context
- error_id
```
protected static int error_id
```
  The number of errors saved so far. Used to generate the name of the error trail file.
- vm
```
protected static VM vm
```
  <2do> - this is a hack to be removed once there are no static references anymore
- ss
```
protected SystemState ss
```
- funcObjFactory
```
protected FunctionObjectFactory funcObjFactory
```
- path
```
protected Path path
```
- out
```
protected java.lang.StringBuilder out
```
  execution path to current state
- lastTrailInfo
```
protected Transition lastTrailInfo
```
  various caches for VMListener state acquisition. NOTE - these are only valid during notification <2do> get rid of the 'lasts' in favor of queries on the insn, the executing thread, and the VM. This is superfluous work to for every notification (even if there are no listeners using it) that can easily lead to inconsistencies
- isTraceReplay
```
protected boolean isTraceReplay
```
- stateSet
```
protected StateSet stateSet
```
  the repository we use to find out if we already have seen a state
- newStateId
```
protected int newStateId
```
  this was the last stateId - note this is also used for stateless model checking
- backtracker
```
protected Backtracker backtracker
```
  the structure responsible for storing and restoring backtrack info
- restorer
```
protected StateRestorer<?> restorer
```
  optional serializer/restorer to support backtracker
- serializer
```
protected StateSerializer serializer
```
  optional serializer to support stateSet
- listeners
```
protected VMListener[] listeners
```
  potential execution listeners. We keep them in a simple array to avoid creating objects on each notification
- transitionOccurred
```
protected boolean transitionOccurred
```
  did we get a new transition
- timeModel
```
protected TimeModel timeModel
```
  how we model execution time
- scheduler
```
protected Scheduler scheduler
```
  ThreadChoiceGenerator management related to data races and shared objects
- config
```
protected Config config
```
- runGc
```
protected boolean runGc
```
- treeOutput
```
protected boolean treeOutput
```
- pathOutput
```
protected boolean pathOutput
```
- indentOutput
```
protected boolean indentOutput
```
- processFinalizers
```
protected boolean processFinalizers
```
- isBigEndian
```
protected boolean isBigEndian
```
- initialized
```
protected boolean initialized
```
- userliveNonDaemonPredicate
```
protected Predicate<ThreadInfo> userliveNonDaemonPredicate
```
- timedoutRunnablePredicate
```
protected Predicate<ThreadInfo> timedoutRunnablePredicate
```
- alivePredicate
```
protected Predicate<ThreadInfo> alivePredicate
```
- userTimedoutRunnablePredicate
```
protected Predicate<ThreadInfo> userTimedoutRunnablePredicate
```
- postGcActions
```
protected java.util.ArrayList<java.lang.Runnable> postGcActions
```

Constructor Detail
- VM
```
public VM(JPF jpf,
          Config conf)
```
  be prepared this might throw JPFConfigExceptions
- VM
```
protected VM()
```
  just here for unit test mockups, don't use as implicit base ctor in VM derived classes

Method Detail

getJPF
```
public JPF getJPF()
```

initFields

public void initFields(Config config)

initSubsystems

protected void initSubsystems(Config config)

initTimeModel

protected void initTimeModel(Config config)

cleanUp
```
public void cleanUp()
```
called after the JPF run is finished. Shouldn't be public, but is called by JPF

getPlatformEndianness

protected boolean getPlatformEndianness(Config config)

isBigEndianPlatform
```
public boolean isBigEndianPlatform()
```

finalizersEnabled
```
public boolean finalizersEnabled()
```

isInitialized
```
public boolean isInitialized()
```

isSingleProcess
```
public boolean isSingleProcess()
```

createMainThreadInfo

protected ThreadInfo createMainThreadInfo(int id,
                                          ApplicationContext appCtx)

createThreadInfo

protected ThreadInfo createThreadInfo(int objRef,
                                      int groupRef,
                                      int runnableRef,
                                      int nameRef)

createFinalizerThreadInfo

protected ThreadInfo createFinalizerThreadInfo(int id,
                                               ApplicationContext appCtx)

getStartupSystemClassNames
```
protected java.util.List<java.lang.String> getStartupSystemClassNames()
```
the minimal set of system classes we need for initialization

getStartupSystemClassInfos
```
protected java.util.List<ClassInfo> getStartupSystemClassInfos(SystemClassLoaderInfo sysCl,
                                                               ThreadInfo tiMain)
```
return a list of ClassInfos for essential system types If system classes are not found, or are not valid JPF model classes, we throw a JPFConfigException and exit returned ClassInfos are not yet registered in Statics and don't have class objects

getMainClassInfo

protected ClassInfo getMainClassInfo(SystemClassLoaderInfo sysCl,
                                     java.lang.String mainClassName,
                                     ThreadInfo tiMain,
                                     java.util.List<ClassInfo> list)

this adds the application main class and its supers to the list of startup classes

createSystemClassLoaderInfo

protected SystemClassLoaderInfo createSystemClassLoaderInfo(int appId)

createSystemClassLoaderObject

protected void createSystemClassLoaderObject(SystemClassLoaderInfo sysCl,
                                             ThreadInfo tiMain)

pushMainEntryArgs

protected void pushMainEntryArgs(MethodInfo miMain,
                                 java.lang.String[] args,
                                 ThreadInfo tiMain,
                                 DirectCallStackFrame frame)

pushMainEntry

protected void pushMainEntry(MethodInfo miMain,
                             java.lang.String[] args,
                             ThreadInfo tiMain)

getMainEntryMethodInfo

protected MethodInfo getMainEntryMethodInfo(java.lang.String mthName,
                                            ClassInfo ciMain)

pushClinits

protected void pushClinits(java.util.List<ClassInfo> startupClasses,
                           ThreadInfo tiMain)

initialize
```
public abstract boolean initialize()
```
this is the main initialization point that sets up startup objects threads and callstacks. If this returns false VM initialization cannot proceed and JPF will terminate

initializeMainThread
```
protected ThreadInfo initializeMainThread(ApplicationContext appCtx,
                                          int tid)
```
create and initialize the main thread for the given ApplicationContext. This is called from VM.initialize() implementations, the caller has to handle exceptions that should be reported differently (JPFConfigException, ClassInfoException)

initializeFinalizerThread

protected void initializeFinalizerThread(ApplicationContext appCtx,
                                         int tid)

registerThreadListCleanup

protected void registerThreadListCleanup(ClassInfo ciThread)

setRootCG
```
protected void setRootCG()
```
override this if the concrete VM needs a special root CG

initSystemState

protected void initSystemState(ThreadInfo mainThread)

addPostGcAction

public void addPostGcAction(java.lang.Runnable r)

processPostGcActions
```
public void processPostGcActions()
```
to be called from the Heap after GC is completed (i.e. only live objects remain)

addListener

public void addListener(VMListener newListener)

hasListenerOfType

public boolean hasListenerOfType(java.lang.Class<?> listenerCls)

getNextListenerOfType

public <T> T getNextListenerOfType(java.lang.Class<T> type,
                                   T prev)

removeListener

public void removeListener(VMListener removeListener)

setTraceReplay

public void setTraceReplay(boolean isReplay)

isTraceReplay
```
public boolean isTraceReplay()
```

hasToRecordSteps
```
public boolean hasToRecordSteps()
```

recordSteps

public void recordSteps(boolean cond)

hasToRecordPathOutput

public boolean hasToRecordPathOutput()

notifyVMInitialized
```
protected void notifyVMInitialized()
```

notifyChoiceGeneratorRegistered

protected void notifyChoiceGeneratorRegistered(ChoiceGenerator<?> cg,
                                               ThreadInfo ti)

notifyChoiceGeneratorSet

protected void notifyChoiceGeneratorSet(ChoiceGenerator<?> cg)

notifyChoiceGeneratorAdvanced

protected void notifyChoiceGeneratorAdvanced(ChoiceGenerator<?> cg)

notifyChoiceGeneratorProcessed

protected void notifyChoiceGeneratorProcessed(ChoiceGenerator<?> cg)

notifyExecuteInstruction

protected void notifyExecuteInstruction(ThreadInfo ti,
                                        Instruction insn)

notifyInstructionExecuted

protected void notifyInstructionExecuted(ThreadInfo ti,
                                         Instruction insn,
                                         Instruction nextInsn)

notifyThreadStarted

protected void notifyThreadStarted(ThreadInfo ti)

notifyThreadBlocked

protected void notifyThreadBlocked(ThreadInfo ti)

notifyThreadWaiting

protected void notifyThreadWaiting(ThreadInfo ti)

notifyThreadNotified

protected void notifyThreadNotified(ThreadInfo ti)

notifyThreadInterrupted

protected void notifyThreadInterrupted(ThreadInfo ti)

notifyThreadTerminated

protected void notifyThreadTerminated(ThreadInfo ti)

notifyThreadScheduled

protected void notifyThreadScheduled(ThreadInfo ti)

notifyLoadClass

protected void notifyLoadClass(ClassFile cf)

notifyClassLoaded

protected void notifyClassLoaded(ClassInfo ci)

notifyObjectCreated

protected void notifyObjectCreated(ThreadInfo ti,
                                   ElementInfo ei)

notifyObjectReleased

protected void notifyObjectReleased(ThreadInfo ti,
                                    ElementInfo ei)

notifyObjectLocked

protected void notifyObjectLocked(ThreadInfo ti,
                                  ElementInfo ei)

notifyObjectUnlocked

protected void notifyObjectUnlocked(ThreadInfo ti,
                                    ElementInfo ei)

notifyObjectWait

protected void notifyObjectWait(ThreadInfo ti,
                                ElementInfo ei)

notifyObjectExposed

protected void notifyObjectExposed(ThreadInfo ti,
                                   ElementInfo eiShared,
                                   ElementInfo eiExposed)

notifyObjectShared

protected void notifyObjectShared(ThreadInfo ti,
                                  ElementInfo ei)

notifyObjectNotifies

protected void notifyObjectNotifies(ThreadInfo ti,
                                    ElementInfo ei)

notifyObjectNotifiesAll

protected void notifyObjectNotifiesAll(ThreadInfo ti,
                                       ElementInfo ei)

notifyGCBegin
```
protected void notifyGCBegin()
```

notifyGCEnd
```
protected void notifyGCEnd()
```

notifyExceptionThrown

protected void notifyExceptionThrown(ThreadInfo ti,
                                     ElementInfo ei)

notifyExceptionBailout

protected void notifyExceptionBailout(ThreadInfo ti)

notifyExceptionHandled

protected void notifyExceptionHandled(ThreadInfo ti)

notifyMethodEntered

protected void notifyMethodEntered(ThreadInfo ti,
                                   MethodInfo mi)

notifyMethodExited

protected void notifyMethodExited(ThreadInfo ti,
                                  MethodInfo mi)

getThreadName

public java.lang.String getThreadName()

getInstruction
```
public Instruction getInstruction()
```

getPendingException
```
public ExceptionInfo getPendingException()
```
note this is gone after backtracking or starting the next exception

getLastStep
```
public Step getLastStep()
```

getLastTransition
```
public Transition getLastTransition()
```

getClassInfo

public ClassInfo getClassInfo(int objref)

getPath
```
public Path getPath()
```
NOTE: only use this locally, since the path is getting modified by the VM The path only contains all states when queried from a stateAdvanced() notification. If this is called from an instructionExecuted() (or other VMListener), and you need the ongoing transition in it, you have to call updatePath() first

getCurrentTransition
```
public Transition getCurrentTransition()
```
this is the ongoing transition. Note that it is not yet stored in the path if this is called from a VMListener notification

getClonedPath
```
public Path getClonedPath()
```
use that one if you have to store the path for subsequent use NOTE: without a prior call to updatePath(), this does NOT contain the ongoing transition. See getPath() for usage from a VMListener

getPathLength
```
public int getPathLength()
```

getThreadList
```
public ThreadList getThreadList()
```

getClassLoaderList

public ClassLoaderList getClassLoaderList()

getRestorableState
```
public RestorableVMState getRestorableState()
```
Bundles up the state of the system for export

getSystemState
```
public SystemState getSystemState()
```
Gets the system state.

getKernelState
```
public KernelState getKernelState()
```

kernelStateChanged
```
public void kernelStateChanged()
```

getConfig
```
public Config getConfig()
```

getBacktracker
```
public Backtracker getBacktracker()
```

getRestorer

public <T> StateRestorer<T> getRestorer()

getSerializer

public StateSerializer getSerializer()

setSerializer

public void setSerializer(StateSerializer newSerializer)

getStateSet
```
public StateSet getStateSet()
```
Returns the stateSet if states are being matched.

getScheduler
```
public Scheduler getScheduler()
```

getFunctionObjectFacotry

public FunctionObjectFactory getFunctionObjectFacotry()

getChoiceGenerator
```
public ChoiceGenerator<?> getChoiceGenerator()
```
return the last registered SystemState's ChoiceGenerator object NOTE: there might be more than one ChoiceGenerator associated with the current transition (ChoiceGenerators can be cascaded)

getNextChoiceGenerator

public ChoiceGenerator<?> getNextChoiceGenerator()

hasNextChoiceGenerator

public boolean hasNextChoiceGenerator()

setNextChoiceGenerator

public boolean setNextChoiceGenerator(ChoiceGenerator<?> cg)

setMandatoryNextChoiceGenerator

public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg,
                                            java.lang.String failMsg)

getCurrentChoiceGenerator
```
public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator(java.lang.String id,
                                                                  java.lang.Class<T> cgType)
```
return the latest registered ChoiceGenerator used in this transition that matches the provided 'id' and is of 'cgType'. This should be the main getter for clients that are cascade aware

getChoiceGenerators
```
public ChoiceGenerator<?>[] getChoiceGenerators()
```
returns all ChoiceGenerators in current path

getChoiceGeneratorsOfType

public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType(java.lang.Class<T> cgType)

getLastChoiceGeneratorOfType

public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType(java.lang.Class<T> cgType)

getLastChoiceGeneratorInThread

public ChoiceGenerator<?> getLastChoiceGeneratorInThread(ThreadInfo ti)

print

public void print(java.lang.String s)

println

public void println(java.lang.String s)

print
```
public void print(boolean b)
```

print
```
public void print(char c)
```

print
```
public void print(int i)
```

print
```
public void print(long l)
```

print
```
public void print(double d)
```

print
```
public void print(float f)
```

println
```
public void println()
```

getPendingOutput
```
public java.lang.String getPendingOutput()
```
get the pending output (not yet stored in the path)

handleException

public Instruction handleException(ThreadInfo ti,
                                   int xObjRef)

this is here so that we can intercept it in subclassed VMs

storeTrace

public void storeTrace(java.lang.String fileName,
                       java.lang.String comment,
                       boolean verbose)

storePathOutput
```
public void storePathOutput()
```

printChoiceGeneratorStack

public void printChoiceGeneratorStack()

getLiveThreads
```
public ThreadInfo[] getLiveThreads()
```

printLiveThreadStatus
```
public void printLiveThreadStatus(java.io.PrintWriter pw)
```
print call stacks of all live threads this is also used for debugging purposes, so we can't move it to the Reporter system (it's also using a bit too many internals for that)

dumpThreadStates
```
public void dumpThreadStates()
```

backtrack
```
public boolean backtrack()
```
Moves one step backward. This method and forward() are the main methods used by the search object. Note this is called with the state that caused the backtrack still being on the stack, so we have to remove that one first (i.e. popping two states and restoring the second one)

updatePath
```
public void updatePath()
```
store the current SystemState's Trail in our path, after updating it with whatever annotations the VM wants to add. This is supposed to be called after each transition we want to keep

forward
```
public boolean forward()
```
advance the program state forward() and backtrack() are the two primary interfaces towards the Search driver. note that the caller still has to check if there is a next state, and if the executed instruction sequence led into a new or already visited state

Returns:

'true' if there was an un-executed sequence out of the current state, 'false' if it was completely explored

printCurrentStackTrace
```
public void printCurrentStackTrace()
```
Prints the current stack trace. Just for debugging purposes

restoreState

public void restoreState(RestorableVMState state)

activateGC
```
public void activateGC()
```

retainStateAttributes

public void retainStateAttributes(boolean isRetained)

forceState
```
public void forceState()
```

ignoreState
```
public void ignoreState(boolean cond)
```
override the state matching - ignore this state, no matter if we changed the heap or stacks. use this with care, since it prunes whole search subtrees

ignoreState
```
public void ignoreState()
```

breakTransition
```
public void breakTransition(java.lang.String reason)
```
imperatively break the transition to enable state matching

transitionOccurred
```
public boolean transitionOccurred()
```

isNewState
```
public boolean isNewState()
```
answers if the current state already has been visited. This is mainly used by the searches (to control backtracking), but could also be useful for observers to build up search graphs (based on the state ids) this returns true if no state has been produced yet, and false if no transition occurred after a forward call

isEndState
```
public abstract boolean isEndState()
```
We made this to be overriden by Single/MultiprcessesVM implementations, since for MultiprcessesVM one can decide when to terminate (after the the termination of all processes or only one process). todo - that needs to be specified through the properties file

isVisitedState
```
public boolean isVisitedState()
```

isIgnoredState
```
public boolean isIgnoredState()
```

isInterestingState
```
public boolean isInterestingState()
```

isBoringState
```
public boolean isBoringState()
```

hasPendingException
```
public boolean hasPendingException()
```

isDeadlocked

public abstract boolean isDeadlocked()

getException

public java.lang.Exception getException()

getStateId
```
public int getStateId()
```
get the numeric id for the current state Note: this can be called several times (by the search and observers) for every forward()/backtrack(), so we want to cache things a bit

getStateCount
```
public int getStateCount()
```

getVM
```
public static VM getVM()
```
<2do> this is a band aid to bundle all these legacy reference chains from JPFs past. The goal is to replace them with proper accessors (normally through ThreadInfo, MJIEnv or VM, which all act as facades) wherever possible, and use VM.getVM() where there is no access to such a facade. Once this has been completed, we can start refactoring the users of VM.getVM() to get access to a suitable facade.

getSearch
```
public Search getSearch()
```
not ideal to have this here since it is kind of a backlink, but it's not any better if listeners have to dig this out from JPF Note - this isn't set during initialization, since the VM object is created first

getCurrentApplicationContext
```
public abstract ApplicationContext getCurrentApplicationContext()
```
given an object reference, it returns the ApplicationContext of the process to which this object belongs

getApplicationContext

public abstract ApplicationContext getApplicationContext(int objRef)

getApplicationContexts

public abstract ApplicationContext[] getApplicationContexts()

getSUTName

public abstract java.lang.String getSUTName()

getSUTDescription

public abstract java.lang.String getSUTDescription()

getNumberOfApplications

public abstract int getNumberOfApplications()

getHeap
```
public Heap getHeap()
```

getElementInfo

public ElementInfo getElementInfo(int objref)

getModifiableElementInfo

public ElementInfo getModifiableElementInfo(int objref)

getCurrentThread
```
public ThreadInfo getCurrentThread()
```

registerClassLoader

public void registerClassLoader(ClassLoaderInfo cl)

registerThread

public int registerThread(ThreadInfo ti)

getClassLoader
```
protected ClassLoaderInfo getClassLoader(int gid)
```
Returns the ClassLoader with the given globalId

currentTimeMillis
```
public long currentTimeMillis()
```
<2do> this is where we will hook in a better time model

nanoTime
```
public long nanoTime()
```
<2do> this is where we will hook in a better time model

resetNextCG
```
public void resetNextCG()
```

checkConsistency
```
public void checkConsistency(boolean isStateStore)
```
only for debugging, this is expensive If this is a store (forward) this is called before the state is stored. If this is a restore (visited forward or backtrack), this is called after the state got restored

terminateProcess

public abstract void terminateProcess(ThreadInfo ti)

getInitialInternStringsMap

public abstract java.util.Map<java.lang.Integer,IntTable<java.lang.String>> getInitialInternStringsMap()

getRunnablePredicate

public abstract Predicate<ThreadInfo> getRunnablePredicate()

getDaemonRunnablePredicate

public abstract Predicate<ThreadInfo> getDaemonRunnablePredicate()

getAppTimedoutRunnablePredicate

public abstract Predicate<ThreadInfo> getAppTimedoutRunnablePredicate()

getUserTimedoutRunnablePredicate

public Predicate<ThreadInfo> getUserTimedoutRunnablePredicate()

getUserLiveNonDaemonPredicate

public Predicate<ThreadInfo> getUserLiveNonDaemonPredicate()

getTimedoutRunnablePredicate

public Predicate<ThreadInfo> getTimedoutRunnablePredicate()

getAlivePredicate

public Predicate<ThreadInfo> getAlivePredicate()

getFinalizerThread

public FinalizerThreadInfo getFinalizerThread()

processFinalizers
```
public void processFinalizers()
```

Class VM

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

CHECK_CONSISTENCY

EMPTY_ARGS

log

jpf

error_id

vm

ss

funcObjFactory

path

out

lastTrailInfo

isTraceReplay

stateSet

newStateId

backtracker

restorer

serializer

listeners

transitionOccurred

timeModel

scheduler

config

runGc

treeOutput

pathOutput

indentOutput

processFinalizers

isBigEndian

initialized

userliveNonDaemonPredicate

timedoutRunnablePredicate

alivePredicate

userTimedoutRunnablePredicate

postGcActions

Constructor Detail

VM

VM

Method Detail

getJPF

initFields

initSubsystems

initTimeModel

cleanUp

getPlatformEndianness

isBigEndianPlatform

finalizersEnabled

isInitialized

isSingleProcess

createMainThreadInfo

createThreadInfo

createFinalizerThreadInfo

getStartupSystemClassNames

getStartupSystemClassInfos

getMainClassInfo

createSystemClassLoaderInfo

createSystemClassLoaderObject

pushMainEntryArgs

pushMainEntry

getMainEntryMethodInfo

pushClinits

initialize

initializeMainThread

initializeFinalizerThread

registerThreadListCleanup

setRootCG

initSystemState

addPostGcAction

processPostGcActions

addListener

hasListenerOfType

getNextListenerOfType

removeListener

setTraceReplay

isTraceReplay