|
| |
|
| java.lang.Object
 gov.nasa.jpf.jvm.JVM
| JVM | | public class JVM implements VM(Code) | | This class represents the virtual machine. The virtual machine is able to
move backward and forward one transition at a time.
|
| Inner Class :class JVMState implements VMState | |
| Method Summary | |
| public void | addListener(VMListener newListener)
| | void | addListeners(Config config)
| | public void | addObservable(String observable)
| | void | appendOutput(String s)
| | void | appendOutput(char c)
| | public boolean | backtrack()
Moves one step backward. | | void | backtrackKernelState()
| | void | backtrackSystemState()
| | public boolean | checkFP()
| | static boolean | checkModelClassAccess()
do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
are tightly coupled with the JPF core (e.g. | | public boolean | checkNaN(double r)
| | public boolean | checkNaN(float r)
| | public boolean | checkNaNcompare(float r1, float r2)
| | public boolean | checkNaNcompare(double r1, double r2)
| | public BooleanChoiceGenerator | createBooleanChoiceGenerator()
| | public ChoiceGenerator | createChoiceGenerator(String id)
| | public IntChoiceGenerator | createIntChoiceGenerator(int min, int max)
| | protected ThreadInfo | createMainThread()
| | public ThreadInfo | createThread(int objRef)
| | boolean | finalizeObject(ElementInfo ei)
| | public boolean | forward()
| | public int | getAbstractionNonDeterministicThreadCount()
| | public int | getAliveThreadCount()
| | public String[] | getArgs()
| | public ChoiceGenerator | getChoiceGenerator()
| | public ClassInfo | getClassInfo()
| | public Reference | getClassReference(String name)
| | public DynamicArea | getDynamicArea()
| | public Exception | getException()
| | Instruction | getInstruction()
| | public KernelState | getKernelState()
| | public ClassInfo | getLastClassInfo()
| | public ElementInfo | getLastElementInfo()
| | public Instruction | getLastInstruction()
| | public Step | getLastStep()
| | public ThreadInfo | getLastThreadInfo()
| | public Transition | getLastTransition()
| | public String | getMainClassName()
| | public Instruction | getNextInstruction()
| | public Path | getPath()
| | public int | getPathLength()
| | public ExceptionInfo | getPendingException()
| | public Reference | getReference(String name)
| | public VMState | getRestorableForwardState()
| | public int | getRunnableThreadCount()
| | public VMState | getState()
| | public int | getStateId()
| | StaticArea | getStaticArea()
| | public SystemState | getSystemState()
Gets the system state. | | public String | getThreadName()
| | public int | getThreadNumber()
| | static JVM | getVM()
| | public boolean | hasPendingException()
| | public void | initFields(Config config)
| | static void | initStaticFields()
initialize all our static fields. | | void | initSubsystems(Config config)
| | public boolean | initialize()
load and initialize startup classes, return 'true' if successful.
This loads a bunch of core library classes, initializes the main thread,
and then all the required startup classes, but excludes the static init of
the main class. | | protected void | initializeStartupClasses()
| | public boolean | isBoringState()
| | public boolean | isDeadlocked()
| | public boolean | isEndState()
| | public boolean | isInterestingState()
| | public boolean | isNewState()
answers if the current state already has been visited. | | public boolean | isTerminated()
| | protected void | loadClass(ClassInfo ci)
| | public Path | loadPath(String fname)
| | protected void | loadStartupClasses()
| | void | notifyClassLoaded(ClassInfo ci)
| | void | notifyExceptionThrown(ThreadInfo ti, ElementInfo ei)
| | void | notifyGCBegin()
| | void | notifyGCEnd()
| | void | notifyInstructionExecuted(ThreadInfo ti, Instruction insn, Instruction nextInsn)
| | void | notifyObjectCreated(ThreadInfo ti, ElementInfo ei)
| | void | notifyObjectReleased(ElementInfo ei)
| | void | notifyThreadStarted(ThreadInfo ti)
| | void | notifyThreadTerminated(ThreadInfo ti)
| | public void | popKernelState()
| | void | prepareMain(Config config)
| | void | prepareMainClinit(Config config)
| | public void | print(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 | printCurrentStackTrace()
Prints the current stack trace. | | public void | printResults(PrintWriter pw)
| | public void | printStackTraces(PrintWriter pw)
| | public void | printStatus()
| | public void | println(String s)
| | public void | println()
| | public void | pushKernelState()
Saves the state of the system. | | public void | pushSystemState()
Saves the backtracking information. | | public void | removeListener(VMListener removeListener)
| | public void | restoreState(VMState st)
| | public void | rewind()
| | public void | savePath(Path path, Writer w)
| | public void | setIgnoreState(boolean b)
override the state matching - ignore this state, no matter if we changed
the heap or stacks. | | public void | setPath(Path p)
| | void | updatePath()
store the current SystemState's TrainInfo in our path, after updating it
with whatever annotations the JVM wants to add. |
| atomicLines | | boolean atomicLines(Code) | | |
| backtrackStack | | protected Stack backtrackStack(Code) | | and that adds the SystemState specifics (Scheduler)
|
| checkFPcompare | | boolean checkFPcompare(Code) | | |
| error_id | | protected static int error_id(Code) | | The number of errors saved so far.
Used to generate the name of the error trail file.
|
| indentOutput | | boolean indentOutput(Code) | | |
| jvm | | protected static JVM jvm(Code) | | <2do> - this is a hack to be removed once there are no static references
anymore
|
| lastTrailInfo | | TrailInfo lastTrailInfo(Code) | | various caches for VMListener state acqusition. NOTE - these are only
valid during notification
|
| observableInvokes | | public static HashSet observableInvokes(Code) | | Contains the list of invoke instructions which are observable.
|
| observableLabels | | public static HashSet observableLabels(Code) | | Contains the list of the labels which are observable.
|
| observablePositions | | public static HashSet observablePositions(Code) | | Contains the list of the positions which are observable.
|
| observableReturns | | public static HashSet observableReturns(Code) | | Contains the list of methods whose return instruction are observable.
|
| pathOutput | | boolean pathOutput(Code) | | |
| stateBacktrackStack | | protected Stack stateBacktrackStack(Code) | | that's mostly JPFs execution context (atomicity etc.)
|
| stateSet | | StateSet stateSet(Code) | | the repository we use to find out if we already have seen a state
|
| stateStoringStack | | protected Stack stateStoringStack(Code) | | where we keep the saved KernelState data
|
| treeOutput | | boolean treeOutput(Code) | | |
| JVM | | public JVM(Config conf) throws Config.Exception(Code) | | VM instances are another example of evil throw-up ctors, but this is
justified by the fact that they are only created via (configured)
reflection from within the safe confines of the JPF ctor - which
shields clients against blowups
|
| addObservable | | public void addObservable(String observable)(Code) | | |
| appendOutput | | void appendOutput(char c)(Code) | | |
| backtrack | | public boolean backtrack()(Code) | | 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)
|
| backtrackKernelState | | void backtrackKernelState()(Code) | | |
| backtrackSystemState | | void backtrackSystemState()(Code) | | |
| checkFP | | public boolean checkFP()(Code) | | |
| checkModelClassAccess | | static boolean checkModelClassAccess()(Code) | | do we see our model classes? Some of them cannot be used from the standard CLASSPATH, because they
are tightly coupled with the JPF core (e.g. java.lang.Class, java.lang.Thread,
java.lang.StackTraceElement etc.)
Our strategy here is kind of lame - we just look into java.lang.Class, if we find the 'int cref' field
(that's a true '42')
|
| checkNaN | | public boolean checkNaN(double r)(Code) | | |
| checkNaN | | public boolean checkNaN(float r)(Code) | | |
| checkNaNcompare | | public boolean checkNaNcompare(float r1, float r2)(Code) | | |
| checkNaNcompare | | public boolean checkNaNcompare(double r1, double r2)(Code) | | |
| createMainThread | | protected ThreadInfo createMainThread()(Code) | | be careful - everything that's executed from within here is not allowed
to depend on static class init having been done yet
|
| forward | | public boolean forward()(Code) | | try to advance the state
forward() and backtrack() are the two primary interfaces towards the Search
driver
return 'true' if there was an un-executed sequence out of the current state,
'false' if it was completely explored
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
|
| getAbstractionNonDeterministicThreadCount | | public int getAbstractionNonDeterministicThreadCount()(Code) | | |
| getAliveThreadCount | | public int getAliveThreadCount()(Code) | | |
| getChoiceGenerator | | public ChoiceGenerator getChoiceGenerator()(Code) | | return the current SystemState's ChoiceGenerator object
|
| getClassInfo | | public ClassInfo getClassInfo()(Code) | | answer the ClassInfo that was loaded most recently
part of the VMListener state acqusition
|
| getDynamicArea | | public DynamicArea getDynamicArea()(Code) | | return the 'heap' object, which is a global service
|
| getLastClassInfo | | public ClassInfo getLastClassInfo()(Code) | | answer the ClassInfo that was loaded most recently
part of the VMListener state acqusition (only valid from inside of
notification)
|
| getLastElementInfo | | public ElementInfo getLastElementInfo()(Code) | | answer the Object that was most recently created or collected
part of the VMListener state acqusition (only valid from inside of
notification)
|
| getLastInstruction | | public Instruction getLastInstruction()(Code) | | answer the last executed Instruction
part of the VMListener state acqusition (only valid from inside of
notification)
|
| getLastThreadInfo | | public ThreadInfo getLastThreadInfo()(Code) | | answer the ThreadInfo that was most recently started or finished
part of the VMListener state acqusition (only valid from inside of
notification)
|
| getNextInstruction | | public Instruction getNextInstruction()(Code) | | answer the next Instruction to execute in the current thread
part of the VMListener state acqusition (only valid from inside of
notification)
|
| getPathLength | | public int getPathLength()(Code) | | |
| getRestorableForwardState | | public VMState getRestorableForwardState()(Code) | | |
| getRunnableThreadCount | | public int getRunnableThreadCount()(Code) | | |
| getState | | public VMState getState()(Code) | | Bundles up the state of the system for export
|
| getStateId | | public int getStateId()(Code) | | 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
|
| getStaticArea | | StaticArea getStaticArea()(Code) | | same for "loaded classes", but be advised it will probably go away at some point
|
| getThreadNumber | | public int getThreadNumber()(Code) | | |
| hasPendingException | | public boolean hasPendingException()(Code) | | |
| initStaticFields | | static void initStaticFields()(Code) | | initialize all our static fields. Called from and reset
|
| initialize | | public boolean initialize()(Code) | | load and initialize startup classes, return 'true' if successful.
This loads a bunch of core library classes, initializes the main thread,
and then all the required startup classes, but excludes the static init of
the main class. Note that whatever gets executed in here should NOT contain
any non-determinism, since we are not backtrackable yet, i.e.
non-determinism in clinits should be constrained to the app class (and
classes used by it)
|
| initializeStartupClasses | | protected void initializeStartupClasses()(Code) | | |
| isBoringState | | public boolean isBoringState()(Code) | | |
| isDeadlocked | | public boolean isDeadlocked()(Code) | | |
| isEndState | | public boolean isEndState()(Code) | | |
| isInterestingState | | public boolean isInterestingState()(Code) | | |
| isNewState | | public boolean isNewState()(Code) | | 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)
|
| isTerminated | | public boolean isTerminated()(Code) | | |
| loadPath | | public Path loadPath(String fname)(Code) | | load a previously stored path from a file
<2do> should be simplified to use the JVMXMLTraceHandler (no use to
have different trace formats for the same VM)
|
| loadStartupClasses | | protected void loadStartupClasses()(Code) | | |
| notifyGCBegin | | void notifyGCBegin()(Code) | | |
| notifyGCEnd | | void notifyGCEnd()(Code) | | |
| popKernelState | | public void popKernelState()(Code) | | |
| prepareMainClinit | | void prepareMainClinit(Config config)(Code) | | |
| print | | public void print(boolean b)(Code) | | |
| print | | public void print(char c)(Code) | | |
| print | | public void print(int i)(Code) | | |
| print | | public void print(long l)(Code) | | |
| print | | public void print(double d)(Code) | | |
| print | | public void print(float f)(Code) | | |
| printCurrentStackTrace | | public void printCurrentStackTrace()(Code) | | Prints the current stack trace.
|
| printStatus | | public void printStatus()(Code) | | |
| println | | public void println()(Code) | | |
| pushKernelState | | public void pushKernelState()(Code) | | Saves the state of the system.
|
| pushSystemState | | public void pushSystemState()(Code) | | Saves the backtracking information.
|
| rewind | | public void rewind()(Code) | | |
| setIgnoreState | | public void setIgnoreState(boolean b)(Code) | | 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
|
| updatePath | | void updatePath()(Code) | | store the current SystemState's TrainInfo in our path, after updating it
with whatever annotations the JVM wants to add.
This is supposed to be called after each transition we want to keep
|
|
|
|