Package gov.nasa.jpf.vm

Interface Summary

Interface	Description
AllocationContext	abstract type that captures the context (class, thread id and callstack) of an allocation Used for SGOID computation
AnnotationParser	a parser for annotation class files
Attributor	interface to configure various method and field attributes at class load time
Backtracker
Backtracker.RestorableState
ChoiceGenerator<T>	generic interface for configurable choice generators
ClosedMemento	this is a self-contained memento that remembers which object to restore, and where to restore it into (e.g.
DebugStateSerializer	debug extensions of StateSerializer interface
DoubleChoiceGenerator	Choice Generator that creates double values - this is only an interface so that we can type check implementors that use their own generic hierarchy
FieldLockInfoFactory	factory interface for creating concrete FieldLockInfo objects, which are configurable class sets (that might encapsulate heuristics)
FieldsFactory	abstract factory interface for creating Fields, i.e.
FloatChoiceGenerator	Choice Generator that creates float value - this is only an interface we can use for type checks of implementors that have their own generic hierarchy
GenericSignatureHolder	something that can have a GenericSignature classfile attribute
Heap	this is our implementation independent model of the heap
IncrementalChangeTracker	This should be implemented by classes that read & reset "hasChanged"-type information in the KernelState.
IntChoiceGenerator	Choice Generator that creates Integer values - this is just an interface so that we can type test for implementors that have their own generic hierarchy
KernelState.ChangeListener	interface for getting notified of changes to KernelState and everything "below" it.
LongChoiceGenerator	ChoiceGenerator for Long values - this is only an interface so that we can use it for type checks of implementors that use their own generic hierarchy
Memento<T>	generic interface for objects that are used to restore previous states from within a context that holds the references to the objects to restore (e.g.
MementoFactory	interface to create Memento objects for state storage/restore this follows some sort of a visitor pattern
MethodLocator	an interface to lookup methods
NativeStateHolder	interface for native state components that are not visible to the serializer, i.e.
ReferenceChoiceGenerator	that's a little bit counter-intuitive - references are just int values in JPF
ReferenceProcessor	a generic interface to process reference values
ReleaseAction	interface for actions to be taken when gc'ing objects that are no longer reachable.
Restorable<T>	generic interface of objects that can provide state storage/restore capabilities
Scheduler	a policy interface that is used for all system operations that might cause ThreadChoiceGenerators
SharednessPolicy	SharednessPolicy is a configured policy that is used to detect data races for objects that are accessible from concurrent threads.
StateRestorer<Saved>
StateSerializer
StateSet	interface to encapsulate an ADT (conceptually a set) used to answer if a state has been seen already
Statics	abstraction for the container of StaticElementInfos, which manages static fields.
Storable	Deprecated foo
SyncPolicy	a policy interface related to locking, blocking and thread lifetime events.
ThreadChoiceGenerator
ThreadInfoSet	interface to abstract the referencing set of threadinfos per object/class Used to detect shared objects/classes Instances are created through a configured factory (SharedObjectPolicy) We abstract the container so that the way we identify threads is not exposed to the client, and implementations can use either ThreadInfo references or global ids.
TimeModel	interface that encapsulates the mechanism to obtain values for System.getCurrentTimeMillis() System.nanoTime() calls.
VMListener	interface to register for callbacks by the VM Observer role in equally named pattern Note that we only have notifications for generic events, NOT for conditions that are property specific, and especially nothing that is just triggered from an extension.

Class Summary

Class	Description
AbstractRestorer<Saved>
AbstractSerializer
AbstractTypeAnnotationInfo	abstract AnnotationInfo base for Java 8 type annotations
Allocation	helper class for search global object id (SGOID) computation.
AllRunnablesSyncPolicy	a Scheduler implementation base class that allows filtering of runnable threads and implements SyncPolicy without backtracking or empty transitions, i.e.
AnnotationInfo	the JPF internal representation for Java Annotations AnnotationInfos represent a separate type system.
AnnotationInfo.AnnotationAttribute
AnnotationInfo.ClassValue
AnnotationInfo.Entry
AnnotationInfo.EnumValue
ApplicationContext	auxiliary class that captures the main entry and classloader context of applications
ArrayAccess	CG attribute to store array references of aload/astore operations
ArrayFields	a Field (data value) store for array objects
ArrayOffset	data encapsulation for backtracking.
AtomicData	helper object to store per thread information about atomic line execution <2do> check if we can't do this less expensive.
BooleanArrayFields	element values for boolean[] objects
BooleanChoiceGenerator	a pretty simple ChoiceGenerator that returns a boolean there is not much use in having a CG type interface (such as IntChoiceGenerator) since there is hardly a need for a generic type hierarchy of BooleanChoiceGenerator subtypes - what else can you do with true/false
BooleanFieldInfo	fieldinfo for slots holding booleans
BootstrapMethodInfo
BoxObjectCacheManager
ByteArrayFields	element values for byte[] objects
BytecodeAnnotationInfo	type annotation for type instructions such as instanceof, new, cast
BytecodeTypeParameterAnnotationInfo	type annotation for instructions that take type parameters, such as invoke insns for generic methods
ByteFieldInfo	fieldinfo for slots holding bytes
CharArrayFields	element values for char[] objects
CharFieldInfo	fieldinfo for slots holding chars
CheckExtendTransition	system attribute to dynamically mark ChoiceGenerators for transition extension checks
ChoiceGeneratorBase<T>	abstract root class for configurable choice generators
ChoicePoint	a little helper class that is used to replay previously stored traces (which are little more than just a list of ChoiceGenerator classnames and choiceIndex indexes stored in a previous run)
ClassFileContainer	abstract class that represents the source of a classfile, such as (root) directories and jars
ClassFileMatch	a lookup match for a given typename in a ClassFileContainer
ClassInfo	Describes the VM's view of a java class.
ClassLoaderInfo
ClassLoaderList	container for all ClassLoaderInfos that are in the current state.
ClassPath	this is a lookup mechanism for class files that is based on an ordered list of directory or jar entries
ConstInsnPathTime	time model that uses instruction count along current path to deduce the execution time.
DebugJenkinsStateSet	a JenkinsStateSet that stores program state information in a readable and diffable format.
DefaultBacktracker<KState>
DefaultFieldsFactory	our concrete Fields factory (representing the default JPF object model)
DefaultMementoRestorer	a MementoRestorer that uses the default mementos
DelegatingScheduler	a generic scheduler with configured SyncPolicy and SharednesPolicy objects it delegates to
DirectCallStackFrame	DirectCallStackFrames are only used for overlay calls (from native code), i.e.
DoubleArrayFields	element values for double[] objects
DoubleFieldInfo	type, name and attribute information for 'double' fields
DoubleSlotFieldInfo	a double or long field
DynamicElementInfo	A specialized version of ElementInfo that represents heap objects
ElementInfo	Describes an element of memory containing the field values of a class or an object.
ExceptionHandler	Stores the information about an exception handler.
ExceptionInfo	helper class to store context of an exception
ExceptionParameterAnnotationInfo	type annotation for catch arguments
FieldInfo	type, name and attribute information of a field.
FieldLockInfo	class encapsulating the lock protection status for field access instructions.
Fields	Represents the variable, hash-collapsed pooled data associated with an object that is related to the object values (as opposed to synchronization ->Monitor).
FinalizerThreadInfo
FloatArrayFields	element values for float[] objects
FloatFieldInfo	type, name, modifier info of float fields
FormalParameterAnnotationInfo	type annotation for formal parameters
FullStateSet	Implements a lossless StateSet
FunctionObjectFactory
GenericHeap	this is an abstract root for Heap implementations, providing a standard mark&sweep collector, change attribute management, and generic pinDownList, weakReference and internString handling The concrete Heap implementors have to provide the ElementInfo collection and associated getters, allocators and iterators
GenericSGOIDHeap	abstract Heap trait that implements SGOIDs by means of a search global Allocation map and a state managed allocCount map NOTE - a reference value of 0 represents null and therefore is not a valid SGOID
GenericSharednessPolicy	an abstract SharednessPolicy implementation that makes use of both shared field access CGs and exposure CGs.
GlobalSchedulingPoint	a SystemAttribute to mark global scheduling points.
GlobalSharednessPolicy	a SharedObjectPolicy that uses search global ThreadInfoSets and FieldLockInfos, i.e.
HandlerContext	utility wrapper for exception handlers that /would/ handle a given exception type <2do> This should be a class hierarchy to properly distinguish between ordinary catch handlers and UncaughtHandler objects, but so far this isn't worth it
HashedAllocationContext	an AllocationContext that uses a hash value for comparison.
InfoObject	common root for ClassInfo, MethodInfo, FieldInfo (and maybe more to follow) so far, it's used to factorize the annotation support, but we can also move the attributes up here Note this is used for both declaration- and type- annotations since there is a cross-over (type annotations of classes/interfaces are visible through the reflection API that is otherwise just reserved for declaration annotations) 2do - there are 3 annotation positions that are valid for both type and declaration annotations: class/interface, field and formal method parameters.
Instruction	common root of all JPF bytecode instruction classes
IntArrayFields	element values for int[] objects
IntegerFieldInfo	type, name, mod info about integer fields
JenkinsStateSet	Implements StateSet based on Jenkins hashes.
JPF_gov_nasa_jpf_vm_Verify	native peer class for programmatic JPF interface (that can be used inside of apps to verify - if you are aware of the danger that comes with it) this peer is a bit different in that it only uses static fields and methods because its use is supposed to be JPF global (without classloader namespaces)
JPFOutputStream	stream to write program state info in a readable and diff-able format.
KernelState	This class represents the SUT program state (statics, heap and threads)
LocalVarInfo
LockSetThresholdFli	a threshold FieldLockInfo with a set of lock candidates this is the destructive update version.
LongArrayFields	element values for long[] objects
LongFieldInfo
MementoRestorer	state storer/restorer that works solely on a snapshot basis
MethodInfo	information associated with a method.
MJIEnv	MJIEnv is the call environment for "native" methods, i.e.
Monitor	Represents the variable, hash-collapsed pooled data associated with an object that is not related to the object values (->Fields), but to the use of the object for synchronization purposes (locks and signals).
MultiProcessVM	A VM implementation that simulates running multiple applications within the same JPF process (centralized model checking of distributed applications).
NamedFields	value container for non-array classes
NativeMethodInfo	a MethodInfo for a native peer executed method
NativePeer	native peer classes are part of MJI and contain the code that is executed by the host VM (i.e.
NativeStackFrame	a stack frame for MJI methods This is a special Stackframe to execute NativeMethodInfos, which are just a wrapper around Java reflection calls.
NoJPFExec	InfoObject attr that flags a certain construct (field, method, class) is not supposed to be used under JPF.
NoOutOfMemoryErrorProperty	A property class so that gov.nasa.jpf.JPF can add an error to the gov.nasa.jpf.search.Search object when JPF catches an OutOfMemoryError.
NotDeadlockedProperty	property class to check for no-runnable-threads conditions
NoUncaughtExceptionsProperty	property class to check for uncaught exceptions
ObjRef	helper class to store object references in a context where Integer is used for boxed 'int' values
OVHeap	a heap that implements search global object ids (SGOIDs) and uses a simple ObjVector to store ElementInfos.
OVStatics	Statics implementation that uses a simple ObjVector as the underlying container.
Path	Path represents the data structure in which a execution trace is recorded.
PathSharednessPolicy	a SharednessPolicy implementation that only computes and keeps sharedness along the same path, i.e.
PersistentLockSetThresholdFli	persistent version of a FieldLockInfo with multiple locks
PersistentSingleLockThresholdFli	persistent SingleLockThresholdFli version
PersistentTidSet	set that stores threads via (search global) thread ids.
PreciseAllocationContext	class that captures execution context consisting of executing thread and pc's of ti's current StackFrames note that we pool (i.e.
PredicateMap
PriorityRunnablesSyncPolicy	a AllRunnablesSyncPolicy that only considers the runnables with the highest priority as choices 2do - it doesn't make much sense to compare priorities across process boundaries (unless we model distributed apps running on the same machine)
PSIMHeap	heap implementation that uses a PersistentStagingMsbIntMap as the underlying container This is intended for large state spaces, to minimize store/restore costs.
ReferenceArrayFields	element values for reference array objects (references are stored as int's)
ReferenceFieldInfo	field info for object fields
RestorableVMState	NOTE - making VMStates fully restorable is currently very expensive and should only be done on a selective basis
SerializingStateSet
ShortArrayFields	element values for short[] objects
ShortFieldInfo	fieldinfo for slots holding booleans
SingleLockThresholdFli	a threshold FieldLockInfo with a single lock candidate This is the base version that does destructive updates.
SingleProcessVM
SingleSlotFieldInfo	field type that requires a single slot (all but long and double)
StackFrame	Describes callerSlots stack frame.
StaticElementInfo	A specialized version of ElementInfo that is used for static fields.
StatisticFieldLockInfoFactory	a FieldLockInfo implementation with the following strategy: - at each check, store the intersection of the current threads lock set with the previous field lock set - if the access was checked less than CHECK_THRESHOLD times, report the field as unprotected - if the field lock set doesn't become empty after CHECK_THRESHOLD, report the field as protected - as an optimization, raise the check level above the threshold if we have a good probability that a current lock is a protection lock for this field - continue to check even after reaching the threshold, so that we can at least report a violated assumption NOTE there is a subtle problem: if we ever falsely assume lock protection in a path that subsequently recycles the shared object (e.g.
Step	this corresponds to an executed instruction.
SuperTypeAnnotationInfo	type annotation for super types (superclass and interfaces)
SystemClassLoaderInfo
SystemState	the class that encapsulates not only the current execution state of the VM (the KernelState), but also the part of it's history that is required by VM to backtrack, plus some potential annotations that can be used to control the search (i.e.
SystemTime	simple delegating TimeModel implementation that just returns System time.
ThreadData	this is the mutable Thread data we have to keep track of for storing/restoring states
ThreadInfo	Represents a thread.
ThreadList	Contains the list of all ThreadInfos for live java.lang.Thread objects We add a thread upon creation (within the ThreadInfo ctor), and remove it when the corresponding java.lang.Thread object gets recycled by JPF.
ThreadList.Count
ThresholdFieldLockInfo	a FieldLockInfo that assumes lock protection after n accesses with non-empty lock sets
ThrowsAnnotationInfo	type annotation for throws elements
TidSet	set that stores threads via (search global) thread ids.
Transition	concrete type to store execution paths.
TypeAnnotationInfo	type annotation for classes, enums and interfaces Note that we need a separate type than AbstractTypeAnnotationInfo since the type is used for queries (InfoObjects can have any number of type annotations with different targets)
TypeParameterAnnotationInfo	type annotation for type parameters
TypeParameterBoundAnnotationInfo	type annotation for type parameter bounds, such as note that boundIndex == 0 always has to be a class
Types	various type mangling/demangling routines This reflects the general type id mess in Java.
VariableAnnotationInfo	type annotation for local vars and resource vars
Verify	Verify is the programmatic interface of JPF that can be used from inside of applications.
VM	This class represents the virtual machine.

Enum Summary

Enum	Description
HandlerContext.UncaughtHandlerType
ThreadInfo.State

Exception Summary

Exception	Description
ArrayIndexOutOfBoundsExecutiveException
ClassChangeException	represents a IncompatibleClassChangeError that has to be thrown in the SUT
ClassInfoException
ClassParseException	an exception while parsing a ClassFile
ClinitRequired	this one is kind of a hack for situations where we detect deep from the stack that we need a clinit to be executed, but we can't flag this to the currently executed insn via a return value.
LoadOnJPFRequired
UncaughtException	represents the case of an unhandled exception detected by JPF This is a "controlflow exception", but I finally made my peace with it since UncaughtExceptions can be thrown from various places, including the VM (, finalizer) and we can't rely on that all these locations can check for pc == null.