Class and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ClassInfo
Describes the VM's view of a java class.
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
Instruction
common root of all JPF bytecode instruction classes
|
MethodInfo
information associated with a method.
|
Path
Path represents the data structure in which a execution trace is recorded.
|
RestorableVMState
NOTE - making VMStates fully restorable is currently very
expensive and should only be done on a selective basis
|
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.
|
VM
This class represents the virtual machine.
|
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 and Description |
---|
AnnotationInfo
the JPF internal representation for Java Annotations
AnnotationInfos represent a separate type system.
|
AnnotationParser
a parser for annotation class files
|
ClassFactory
interface for factory class to create ClassFileContainers
|
ClassFileContainer
abstract class that represents the source of a classfile, such
as (root) directories and jars
|
ClassInfo
Describes the VM's view of a java class.
|
ClassLoaderInfo |
ClassParseException
an exception while parsing a ClassFile
|
ClassParser
the abstract type that initializes ClassInfos from external data such as *.class files
|
DirectCallStackFrame
DirectCallStackFrames are only used for overlay calls (from native code), i.e.
|
FieldInfo
type, name and attribute information of a field.
|
GenericSignatureHolder
something that can have a GenericSignature classfile attribute
|
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
|
Instruction
common root of all JPF bytecode instruction classes
|
LookupSwitchInstruction
interface to insulate us from any specific Instruction hierarchy
|
MethodInfo
information associated with a method.
|
NativeMethodInfo
a MethodInfo for a native peer executed method
|
NativeStackFrame
a stack frame for MJI methods
This is a special Stackframe to execute NativeMethodInfos, which are just a wrapper around Java reflection
calls.
|
StackFrame
Describes callerSlots stack frame.
|
TableSwitchInstruction
interface to insulate us from any specific Instruction hierarchy
|
ThreadInfo
Represents a thread.
|
Class and Description |
---|
AllocInstruction
an empty (tag) interface to identify allocating instructions
|
ArrayIndexOutOfBoundsExecutiveException |
ClassInfo
Describes the VM's view of a java class.
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
FieldInfo
type, name and attribute information of a field.
|
Heap
this is our implementation independent model of the heap
|
Instruction
common root of all JPF bytecode instruction classes
|
KernelState
This class represents the SUT program state (statics, heap and threads)
|
LocalVarInfo |
LookupSwitchInstruction
interface to insulate us from any specific Instruction hierarchy
|
MethodInfo
information associated with a method.
|
NativeMethodInfo
a MethodInfo for a native peer executed method
|
ReturnInstruction
an empty (tag) interface to identify return instructions
since .jvm so far does not use any specific feature of ReturnInstructions,
we just need an empty type to make .jvm independent of a specific
Instruction set
|
StackFrame
Describes callerSlots stack frame.
|
StaticElementInfo
A specialized version of ElementInfo that is used for static fields.
|
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.
|
TableSwitchInstruction
interface to insulate us from any specific Instruction hierarchy
|
ThreadInfo
Represents a thread.
|
Class and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ClassInfo
Describes the VM's view of a java class.
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
FieldInfo
type, name and attribute information of a field.
|
Instruction
common root of all JPF bytecode instruction classes
|
MethodInfo
information associated with a method.
|
StackFrame
Describes callerSlots stack frame.
|
ThreadInfo
Represents a thread.
|
VM
This class represents the virtual machine.
|
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 and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
MethodInfo
information associated with a method.
|
StackFrame
Describes callerSlots stack frame.
|
Class and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
Instruction
common root of all JPF bytecode instruction classes
|
Path
Path represents the data structure in which a execution trace is recorded.
|
ThreadInfo
Represents a thread.
|
VM
This class represents the virtual machine.
|
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 and Description |
---|
Path
Path represents the data structure in which a execution trace is recorded.
|
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.
|
Transition
concrete type to store execution paths.
|
VM
This class represents the virtual machine.
|
Class and Description |
---|
RestorableVMState
NOTE - making VMStates fully restorable is currently very
expensive and should only be done on a selective basis
|
VM
This class represents the virtual machine.
|
Class and Description |
---|
ClassInfo
Describes the VM's view of a java class.
|
ClosedMemento
this is a self-contained memento that remembers which object to restore,
and where to restore it into (e.g.
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
FieldInfo
type, name and attribute information of a field.
|
LocalVarInfo |
MethodInfo
information associated with a method.
|
MJIEnv
MJIEnv is the call environment for "native" methods, i.e.
|
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 and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ClassInfo
Describes the VM's view of a java class.
|
MJIEnv
MJIEnv is the call environment for "native" methods, i.e.
|
ThreadInfo
Represents a thread.
|
Class and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ChoiceGeneratorBase
abstract root class for configurable choice generators
|
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 and Description |
---|
MJIEnv
MJIEnv is the call environment for "native" methods, i.e.
|
NativePeer
native peer classes are part of MJI and contain the code that is
executed by the host VM (i.e.
|
Class and Description |
---|
AbstractRestorer |
Allocation
helper class for search global object id (SGOID) computation.
|
AllocationContext
abstract type that captures the context (class, thread id and callstack)
of an allocation
Used for SGOID computation
|
AnnotationInfo
the JPF internal representation for Java Annotations
AnnotationInfos represent a separate type system.
|
AnnotationInfo.Entry |
AnnotationParser
a parser for annotation class files
|
ApplicationContext
auxiliary class that captures the main entry and classloader context
of applications
|
ArrayFields
a Field (data value) store for array objects
|
ArrayIndexOutOfBoundsExecutiveException |
ArrayOffset
data encapsulation for backtracking.
|
AtomicFieldUpdater
base class for atomic field updaters
NOTE - since all native methods are static, we have to be too
|
Attributor
interface to configure various method and field attributes at class
load time
|
Backtracker |
Backtracker.RestorableState |
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
|
ByteArrayFields
element values for byte[] objects
|
CharArrayFields
element values for char[] objects
|
ChoiceGenerator
generic interface for configurable choice generators
|
ChoiceGeneratorBase
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
choice indexes stored in a previous run)
|
ClassFactory
interface for factory class to create ClassFileContainers
|
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.
|
ClassInfoException |
ClassLoaderInfo |
ClassLoaderList
container for all ClassLoaderInfos that are in the current state.
|
ClassParseException
an exception while parsing a ClassFile
|
ClassParser
the abstract type that initializes ClassInfos from external data such as *.class files
|
ClassPath
this is a lookup mechanism for class files that is based on an ordered
list of directory or jar entries
|
ClosedMemento
this is a self-contained memento that remembers which object to restore,
and where to restore it into (e.g.
|
DefaultAttributor
default Attributor implementation to set method and fiel attributes
at class load time.
|
DefaultSchedulerFactory
the general policy is that we only create Thread CGs here (based on their
status), but we don't change any thread or lock status.
|
DirectCallStackFrame
DirectCallStackFrames are only used for overlay calls (from native code), i.e.
|
DoubleArrayFields
element values for double[] objects
|
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
|
FieldInfo
type, name and attribute information of a field.
|
FieldLockInfo
class encapsulating the lock protection status for field access
instructions.
|
FieldLockInfoFactory
factory interface for creating concrete FieldLockInfo objects, which
are configurable class sets (that might encapsulate heuristics)
|
Fields
Represents the variable, hash-collapsed pooled data associated with an object
that is related to the object values (as opposed to synchronization ->Monitor).
|
FieldsFactory
abstract factory interface for creating Fields, i.e.
|
FloatArrayFields
element values for float[] objects
|
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
|
GenericHeap.ElementInfoMarker |
GenericSGOIDHeap
abstract Heap trait that implements SGOIDs by means of a search global
Allocation map and a state managed allocCount map
|
GenericSignatureHolder
something that can have a GenericSignature classfile attribute
|
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
|
HandlerContext.UncaughtHandlerType |
Heap
this is our implementation independent model of the heap
|
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
|
Instruction
common root of all JPF bytecode instruction classes
|
IntArrayFields
element values for int[] objects
|
JenkinsStateSet
Implements StateSet based on Jenkins hashes.
|
JPF_java_lang_ClassLoader |
KernelState
This class represents the SUT program state (statics, heap and threads)
|
KernelState.ChangeListener
interface for getting notified of changes to KernelState and everything
"below" it.
|
LocalVarInfo |
LongArrayFields
element values for long[] objects
|
Memento
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
|
MementoRestorer
state storer/restorer that works solely on a snapshot basis
|
MethodInfo
information associated with a method.
|
MethodLocator
an interface to lookup methods
|
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).
|
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.
|
ObjRef
helper class to store object references in a context where Integer is used for boxed 'int' values
|
Path
Path represents the data structure in which a execution trace is recorded.
|
PreciseAllocationContext
class that captures execution context consisting of executing thread and
pc's of ti's current StackFrames
note that we pool (i.e.
|
ReferenceArrayFields
element values for reference array objects
(references are stored as int's)
|
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
generic interface of objects that can provide state storage/restore capabilities
|
RestorableVMState
NOTE - making VMStates fully restorable is currently very
expensive and should only be done on a selective basis
|
SchedulerFactory
interface of factory object that creates all ChoiceGenerators required
to implement scheduling strategies
|
SerializingStateSet |
SharedObjectPolicy
abstraction for configured policy object that is responsible for detecting shared objects and classes
The interface has to support both
tracking (actual access) based policies
("what is shared")
conservative reachability based policies
("what could be shared")
The interface is intentionally kept generic to support both policies since tracking - while being
far more efficient in terms of states and speed - can either miss some paths or cause state spaces
to depend on search history, thus leading to different search graphs for randomized searches.
|
ShortArrayFields
element values for short[] objects
|
SingleSlotFieldInfo
field type that requires a single slot (all but long and double)
|
StackFrame
Describes callerSlots stack frame.
|
StateRestorer |
StateSerializer |
StateSet
interface to encapsulate an ADT (conceptually a set) used to answer if
a state has been seen already
|
StaticElementInfo
A specialized version of ElementInfo that is used for static fields.
|
Statics
abstraction for the container of StaticElementInfos, which manages static fields.
|
Step
this corresponds to an executed instruction.
|
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.
|
ThreadChoiceGenerator |
ThreadData
this is the mutable Thread data we have to keep track of for storing/restoring states
|
ThreadInfo
Represents a thread.
|
ThreadInfo.StackIterator |
ThreadInfo.State |
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.
|
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 |
TimeModel
interface that encapsulates the mechanism to obtain values for
System.getCurrentTimeMillis()
System.nanoTime()
calls.
|
Transition
concrete type to store execution paths.
|
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 (
|
VM
This class represents the virtual machine.
|
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 and Description |
---|
ChoiceGenerator
generic interface for configurable choice generators
|
ChoiceGeneratorBase
abstract root class for configurable choice generators
|
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
|
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
|
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
|
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
|
ReferenceChoiceGenerator
that's a little bit counter-intuitive - references are just int values in JPF
|
StackFrame
Describes callerSlots stack frame.
|
ThreadChoiceGenerator |
ThreadInfo
Represents a thread.
|
Class and Description |
---|
AbstractSerializer |
ArrayFields
a Field (data value) store for array objects
|
ClassInfo
Describes the VM's view of a java class.
|
DebugStateSerializer
debug extensions of StateSerializer interface
|
ElementInfo
Describes an element of memory containing the field values of a class or an
object.
|
FieldInfo
type, name and attribute information of a field.
|
Fields
Represents the variable, hash-collapsed pooled data associated with an object
that is related to the object values (as opposed to synchronization ->Monitor).
|
KernelState.ChangeListener
interface for getting notified of changes to KernelState and everything
"below" it.
|
MethodInfo
information associated with a method.
|
ReferenceArrayFields
element values for reference array objects
(references are stored as int's)
|
ReferenceProcessor
a generic interface to process reference values
|
StackFrame
Describes callerSlots stack frame.
|
StateSerializer |
StaticElementInfo
A specialized version of ElementInfo that is used for static fields.
|
Statics
abstraction for the container of StaticElementInfos, which manages static fields.
|
ThreadInfo
Represents a thread.
|
VM
This class represents the virtual machine.
|
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.
|