public abstract class VM extends Object
Modifier and Type | Field and Description |
---|---|
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 String[] |
EMPTY_ARGS |
protected static int |
error_id
The number of errors saved so far.
|
protected boolean |
indentOutput |
protected boolean |
initialized |
protected boolean |
isBigEndian |
protected boolean |
isTraceReplay |
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 StringBuilder |
out
execution path to current state
|
protected Path |
path |
protected boolean |
pathOutput |
protected ArrayList<Runnable> |
postGcActions |
protected StateRestorer<?> |
restorer
optional serializer/restorer to support backtracker
|
protected boolean |
runGc |
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 TimeModel |
timeModel
how we model execution time
|
protected boolean |
transitionOccurred
did we get a new transition
|
protected boolean |
treeOutput |
protected static VM |
vm
<2do> - this is a hack to be removed once there are no static references
anymore
|
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
|
Modifier and Type | Method and Description |
---|---|
void |
activateGC() |
void |
addListener(VMListener newListener) |
void |
addPostGcAction(Runnable r) |
boolean |
backtrack()
Moves one step backward.
|
void |
breakTransition()
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 int |
createMainThreadGroup(SystemClassLoaderInfo sysCl,
ThreadInfo tiMain,
int mainThreadRef)
we need to initialize the ThreadGroup object explicitly because the main thread is not yet runnable
|
protected ThreadInfo |
createMainThreadInfo(int id,
ApplicationContext appCtx) |
protected void |
createMainThreadObject(SystemClassLoaderInfo sysCl,
ThreadInfo tiMain)
we need to initialize the Thread object explicitly because the main thread is not yet runnable
|
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() |
void |
forceState() |
boolean |
forward()
advance the program state
forward() and backtrack() are the two primary interfaces towards the Search
driver.
|
int |
getAliveThreadCount() |
abstract ApplicationContext |
getApplicationContext(int objRef)
given an object reference, it returns the ApplicationContext of the process to which
this object belongs
|
abstract ApplicationContext[] |
getApplicationContexts() |
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<?>> |
getChoiceGeneratorsOfType(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() |
<T extends ChoiceGenerator<?>> |
getCurrentChoiceGenerator(String id,
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.
|
ElementInfo |
getElementInfo(int objref) |
Exception |
getException() |
Heap |
getHeap() |
Instruction |
getInstruction() |
JPF |
getJPF() |
KernelState |
getKernelState() |
<T extends ChoiceGenerator<?>> |
getLastChoiceGeneratorOfType(Class<T> cgType) |
Step |
getLastStep() |
Transition |
getLastTransition() |
ThreadInfo[] |
getLiveThreads() |
protected ClassInfo |
getMainClassInfo(SystemClassLoaderInfo sysCl,
String mainClassName,
ThreadInfo tiMain,
List<ClassInfo> list)
this adds the application main class and its supers to the list of startup classes
|
protected MethodInfo |
getMainEntryMethodInfo(String mthName,
ClassInfo ciMain) |
ElementInfo |
getModifiableElementInfo(int objref) |
ChoiceGenerator<?> |
getNextChoiceGenerator() |
<T> T |
getNextListenerOfType(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() |
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() |
int |
getRunnableThreadCount() |
SchedulerFactory |
getSchedulerFactory() |
StateSerializer |
getSerializer() |
protected 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 List<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 String |
getSUTDescription() |
abstract String |
getSUTName() |
SystemState |
getSystemState()
Gets the system state.
|
ThreadList |
getThreadList() |
String |
getThreadName() |
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(Class<?> listenerCls) |
abstract boolean |
hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti) |
boolean |
hasOtherNonDaemonRunnablesThan(ThreadInfo ti) |
boolean |
hasOtherRunnablesThan(ThreadInfo ti) |
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 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 |
isAtomic() |
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 |
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 |
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(String s) |
void |
printCurrentStackTrace()
Prints the current stack trace.
|
void |
printLiveThreadStatus(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(String s) |
void |
processPostGcActions()
to be called from the Heap after GC is completed (i.e.
|
protected void |
pushClinits(List<ClassInfo> startupClasses,
ThreadInfo tiMain) |
protected void |
pushMainEntry(MethodInfo miMain,
String[] args,
ThreadInfo tiMain) |
protected void |
pushMainEntryArgs(MethodInfo miMain,
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,
String failMsg) |
boolean |
setNextChoiceGenerator(ChoiceGenerator<?> cg) |
void |
setSerializer(StateSerializer newSerializer) |
void |
setTraceReplay(boolean isReplay) |
void |
storePathOutput() |
void |
storeTrace(String fileName,
String comment,
boolean verbose) |
boolean |
transitionOccurred() |
void |
updatePath()
store the current SystemState's Trail in our path, after updating it
with whatever annotations the VM wants to add.
|
public static final boolean CHECK_CONSISTENCY
protected static final String[] EMPTY_ARGS
protected static JPFLogger log
protected static int error_id
protected static VM vm
protected SystemState ss
protected Path path
protected StringBuilder out
protected Transition lastTrailInfo
protected boolean isTraceReplay
protected StateSet stateSet
protected int newStateId
protected Backtracker backtracker
protected StateRestorer<?> restorer
protected StateSerializer serializer
protected VMListener[] listeners
protected boolean transitionOccurred
protected TimeModel timeModel
protected Config config
protected boolean runGc
protected boolean treeOutput
protected boolean pathOutput
protected boolean indentOutput
protected boolean isBigEndian
protected boolean initialized
protected VM()
public JPF getJPF()
public void initFields(Config config)
protected void initSubsystems(Config config)
protected void initTimeModel(Config config)
public void cleanUp()
protected boolean getPlatformEndianness(Config config)
public boolean isBigEndianPlatform()
public boolean isInitialized()
public boolean isSingleProcess()
protected ThreadInfo createMainThreadInfo(int id, ApplicationContext appCtx)
protected ThreadInfo createThreadInfo(int objRef, int groupRef, int runnableRef, int nameRef)
protected List<String> getStartupSystemClassNames()
protected List<ClassInfo> getStartupSystemClassInfos(SystemClassLoaderInfo sysCl, ThreadInfo tiMain)
protected ClassInfo getMainClassInfo(SystemClassLoaderInfo sysCl, String mainClassName, ThreadInfo tiMain, List<ClassInfo> list)
protected SystemClassLoaderInfo createSystemClassLoaderInfo(int appId)
protected void createSystemClassLoaderObject(SystemClassLoaderInfo sysCl, ThreadInfo tiMain)
protected int createMainThreadGroup(SystemClassLoaderInfo sysCl, ThreadInfo tiMain, int mainThreadRef)
protected void createMainThreadObject(SystemClassLoaderInfo sysCl, ThreadInfo tiMain)
protected void pushMainEntryArgs(MethodInfo miMain, String[] args, ThreadInfo tiMain, DirectCallStackFrame frame)
protected void pushMainEntry(MethodInfo miMain, String[] args, ThreadInfo tiMain)
protected MethodInfo getMainEntryMethodInfo(String mthName, ClassInfo ciMain)
protected void pushClinits(List<ClassInfo> startupClasses, ThreadInfo tiMain)
public abstract boolean initialize()
protected ThreadInfo initializeMainThread(ApplicationContext appCtx, int tid)
protected void registerThreadListCleanup(ClassInfo ciThread)
protected void initSystemState(ThreadInfo mainThread)
public void addPostGcAction(Runnable r)
public void processPostGcActions()
public void addListener(VMListener newListener)
public boolean hasListenerOfType(Class<?> listenerCls)
public <T> T getNextListenerOfType(Class<T> type, T prev)
public void removeListener(VMListener removeListener)
public void setTraceReplay(boolean isReplay)
public boolean isTraceReplay()
public boolean hasToRecordSteps()
public void recordSteps(boolean cond)
public boolean hasToRecordPathOutput()
protected void notifyVMInitialized()
protected void notifyChoiceGeneratorRegistered(ChoiceGenerator<?> cg, ThreadInfo ti)
protected void notifyChoiceGeneratorSet(ChoiceGenerator<?> cg)
protected void notifyChoiceGeneratorAdvanced(ChoiceGenerator<?> cg)
protected void notifyChoiceGeneratorProcessed(ChoiceGenerator<?> cg)
protected void notifyExecuteInstruction(ThreadInfo ti, Instruction insn)
protected void notifyInstructionExecuted(ThreadInfo ti, Instruction insn, Instruction nextInsn)
protected void notifyThreadStarted(ThreadInfo ti)
protected void notifyThreadBlocked(ThreadInfo ti)
protected void notifyThreadWaiting(ThreadInfo ti)
protected void notifyThreadNotified(ThreadInfo ti)
protected void notifyThreadInterrupted(ThreadInfo ti)
protected void notifyThreadTerminated(ThreadInfo ti)
protected void notifyThreadScheduled(ThreadInfo ti)
protected void notifyLoadClass(ClassFile cf)
protected void notifyClassLoaded(ClassInfo ci)
protected void notifyObjectCreated(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectReleased(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectLocked(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectUnlocked(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectWait(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectNotifies(ThreadInfo ti, ElementInfo ei)
protected void notifyObjectNotifiesAll(ThreadInfo ti, ElementInfo ei)
protected void notifyGCBegin()
protected void notifyGCEnd()
protected void notifyExceptionThrown(ThreadInfo ti, ElementInfo ei)
protected void notifyExceptionBailout(ThreadInfo ti)
protected void notifyExceptionHandled(ThreadInfo ti)
protected void notifyMethodEntered(ThreadInfo ti, MethodInfo mi)
protected void notifyMethodExited(ThreadInfo ti, MethodInfo mi)
public String getThreadName()
public Instruction getInstruction()
public int getAliveThreadCount()
public ExceptionInfo getPendingException()
public Step getLastStep()
public Transition getLastTransition()
public ClassInfo getClassInfo(int objref)
public Path getPath()
public Transition getCurrentTransition()
public Path getClonedPath()
public int getPathLength()
public int getRunnableThreadCount()
public ThreadList getThreadList()
public ClassLoaderList getClassLoaderList()
public RestorableVMState getRestorableState()
public SystemState getSystemState()
public KernelState getKernelState()
public void kernelStateChanged()
public Config getConfig()
public SchedulerFactory getSchedulerFactory()
public Backtracker getBacktracker()
public <T> StateRestorer<T> getRestorer()
public StateSerializer getSerializer()
public void setSerializer(StateSerializer newSerializer)
public StateSet getStateSet()
public ChoiceGenerator<?> getChoiceGenerator()
public ChoiceGenerator<?> getNextChoiceGenerator()
public boolean setNextChoiceGenerator(ChoiceGenerator<?> cg)
public void setMandatoryNextChoiceGenerator(ChoiceGenerator<?> cg, String failMsg)
public <T extends ChoiceGenerator<?>> T getCurrentChoiceGenerator(String id, Class<T> cgType)
public ChoiceGenerator<?>[] getChoiceGenerators()
public <T extends ChoiceGenerator<?>> T[] getChoiceGeneratorsOfType(Class<T> cgType)
public <T extends ChoiceGenerator<?>> T getLastChoiceGeneratorOfType(Class<T> cgType)
public void print(String s)
public void println(String s)
public void print(boolean b)
public void print(char c)
public void print(int i)
public void print(long l)
public void print(double d)
public void print(float f)
public void println()
public String getPendingOutput()
public Instruction handleException(ThreadInfo ti, int xObjRef)
public void storePathOutput()
public ThreadInfo[] getLiveThreads()
public void printLiveThreadStatus(PrintWriter pw)
public void dumpThreadStates()
public boolean backtrack()
public void updatePath()
public boolean forward()
public void printCurrentStackTrace()
public void restoreState(RestorableVMState state)
public void activateGC()
public void retainStateAttributes(boolean isRetained)
public void forceState()
public void ignoreState(boolean cond)
public void ignoreState()
public void breakTransition()
public boolean transitionOccurred()
public boolean isNewState()
public abstract boolean isEndState()
public boolean isVisitedState()
public boolean isIgnoredState()
public boolean isInterestingState()
public boolean isBoringState()
public boolean hasPendingException()
public abstract boolean isDeadlocked()
public Exception getException()
public int getStateId()
public int getStateCount()
public static VM getVM()
public abstract ApplicationContext getApplicationContext(int objRef)
public abstract ApplicationContext[] getApplicationContexts()
public abstract String getSUTName()
public abstract String getSUTDescription()
public abstract int getNumberOfApplications()
public Heap getHeap()
public ElementInfo getElementInfo(int objref)
public ElementInfo getModifiableElementInfo(int objref)
public ThreadInfo getCurrentThread()
public boolean hasOtherRunnablesThan(ThreadInfo ti)
public boolean hasOtherNonDaemonRunnablesThan(ThreadInfo ti)
public abstract boolean hasOnlyDaemonRunnablesOtherThan(ThreadInfo ti)
public void registerClassLoader(ClassLoaderInfo cl)
public int registerThread(ThreadInfo ti)
public boolean isAtomic()
protected ClassLoaderInfo getClassLoader(int gid)
public long currentTimeMillis()
public long nanoTime()
public void resetNextCG()
public void checkConsistency(boolean isStateStore)