Interface | Description |
---|---|
AllocationContext |
abstract type that captures the context (class, thread id and callstack)
of an allocation
Used for SGOID computation
|
AllocInstruction |
an empty (tag) interface to identify allocating instructions
|
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
|
ClassFactory |
interface for factory class to create ClassFileContainers
|
ClassParser |
the abstract type that initializes ClassInfos from external data such as *.class files
|
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
|
LookupSwitchInstruction |
interface to insulate us from any specific Instruction 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
|
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
|
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
|
SchedulerFactory |
interface of factory object that creates all ChoiceGenerators required
to implement scheduling strategies
|
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
|
TableSwitchInstruction |
interface to insulate us from any specific Instruction hierarchy
|
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 | Description |
---|---|
AbstractRestorer<Saved> | |
AbstractSerializer | |
Allocation |
helper class for search global object id (SGOID) computation.
|
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.
|
AtomicFieldUpdater |
base class for atomic field updaters
NOTE - since all native methods are static, we have to be too
|
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
|
BoxObjectCacheManager | |
ByteArrayFields |
element values for byte[] objects
|
ByteFieldInfo |
fieldinfo for slots holding bytes
|
CharArrayFields |
element values for char[] objects
|
CharFieldInfo |
fieldinfo for slots holding chars
|
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
choice 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
|
ConfigAttributor |
A configuration file-driven attributor so that we can tailor JPF's
attributor based on the application under test.
|
ConstInsnPathTime |
time model that uses instruction count along current path to deduce
the execution time.
|
ContextBoundingSchedulerFactory |
SchedulerFactory that limits the search by imposing a maximum number of
thread preemptions (i.e., preempting context switches) that can occur per execution
path.
|
DebugJenkinsStateSet |
a JenkinsStateSet that stores program state information in a readable
and diffable format.
|
DefaultAttributor |
default Attributor implementation to set method and fiel attributes
at class load time.
|
DefaultBacktracker<KState> | |
DefaultFieldsFactory |
our concrete Fields factory (representing the default JPF object model)
|
DefaultMementoRestorer |
a MementoRestorer that uses the default mementos
|
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.
|
DistributedSchedulerFactory | |
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
|
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).
|
FloatArrayFields |
element values for float[] objects
|
FloatFieldInfo |
type, name, modifier info of float fields
|
FullStateSet |
Implements a lossless StateSet
|
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
|
GlobalTrackingPolicy |
a SharedObjectPolicy that uses search global ThreadInfoSets, 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
|
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_AnnotationProxyBase |
native peer for Annotation Proxies
(saves us some bytecode interpretation shoe leather)
|
JPF_gov_nasa_jpf_CachedROHttpConnection |
very simple URLConnection model that can be used for reading static URL contents
The data can be stored in/read from the file system, and is cached
to avoid DOS by means of model checking
|
JPF_gov_nasa_jpf_ConsoleOutputStream |
MJI NativePeer class to intercept all System.out and System.err
printing.
|
JPF_gov_nasa_jpf_DelegatingTimeZone |
native peer for JPFs concrete TimeZone class, which is just delegating to the
host VM so that we are independent of Java versions
|
JPF_gov_nasa_jpf_SerializationConstructor | |
JPF_gov_nasa_jpf_test_MemoryGoal |
native peer for MemoryGoal tests
|
JPF_gov_nasa_jpf_tools_MethodTester |
native peer for the MethodTester tool
|
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)
|
JPF_java_io_File |
intercept and forward some of the filesystem access methods.
|
JPF_java_io_FileDescriptor |
native peer for file descriptors, which are our basic interface to
access file contents.
|
JPF_java_io_InputStreamReader | |
JPF_java_io_ObjectInputStream | |
JPF_java_io_ObjectOutputStream | |
JPF_java_io_ObjectStreamClass | |
JPF_java_io_OutputStreamWriter |
native peer for OutputStreamWriter, to avoid that we have the
char-to-byte conversion in JPF
<2do> this needs to be de-staticed (see model class)
|
JPF_java_io_RandomAccessFile |
MJI NativePeer class for java.io.RandomAccessFile library abstraction
|
JPF_java_lang_Boolean | |
JPF_java_lang_Byte | |
JPF_java_lang_Character |
MJI NativePeer class for java.lang.Character library abstraction
Whoever is using this seriously is definitely screwed, performance-wise
|
JPF_java_lang_Class |
MJI NativePeer class for java.lang.Class library abstraction
|
JPF_java_lang_ClassLoader | |
JPF_java_lang_Double |
MJI NativePeer class for java.lang.Double library abstraction
|
JPF_java_lang_Float |
MJI NativePeer class for java.lang.Float library abstraction
|
JPF_java_lang_Integer |
MJI NativePeer class for java.lang.Integer library abstraction
|
JPF_java_lang_Long |
MJI NativePeer class for java.lang.Long library abstraction
|
JPF_java_lang_Math |
MJI NativePeer class for java.lang.Math library abstraction
|
JPF_java_lang_Object |
MJI NativePeer class for java.lang.Object library abstraction
|
JPF_java_lang_reflect_Array |
MJI NativePeer class for java.lang.reflect.Array library abstraction
|
JPF_java_lang_reflect_Constructor |
native peer for rudimentary constructor reflection.
|
JPF_java_lang_reflect_Field | |
JPF_java_lang_reflect_Method | |
JPF_java_lang_reflect_Proxy | |
JPF_java_lang_Runtime |
just a dummy for now, to avoid UnsatisfiedLinkErrors
|
JPF_java_lang_Short |
MJI NativePeer class for java.lang.Short library abstraction
|
JPF_java_lang_String |
MJI NativePeer class for java.lang.String library abstraction
|
JPF_java_lang_StringBuffer |
MJI NativePeer class for java.lang.StringBuffer library abstraction
|
JPF_java_lang_StringBuilder | |
JPF_java_lang_StringCoding |
we are not really interested in model checking this, so we intercept
and ignore
<2do> at some point we should probably do proper decoding/encoding,
but the java.lang.StringCoding class is unfortunately not public,
and it would be a pain to work around the access restrictions
|
JPF_java_lang_System |
MJI NativePeer class for java.lang.System library abstraction
|
JPF_java_lang_Thread |
MJI NativePeer class for java.lang.Thread library abstraction
NOTE - this implementation depends on all live thread objects being
in ThreadList
|
JPF_java_lang_Throwable |
MJI NativePeer class for java.lang.Throwable library abstraction
|
JPF_java_net_URLClassLoader | |
JPF_java_net_URLDecoder |
native peer for java.net.URLDecoder forwarding
|
JPF_java_net_URLEncoder |
native peer for java.net.URLEncoder forwarding
|
JPF_java_security_MessageDigest | |
JPF_java_text_Bidi | |
JPF_java_text_DateFormat |
this is just the minimal support for DateFormat.parse(String)
|
JPF_java_text_DateFormatSymbols | |
JPF_java_text_DecimalFormat | |
JPF_java_text_DecimalFormatSymbols |
MJI NativePeer class for java.text.DecimalFormatSymbols library abstraction
we need to intercept the initialization because it is requires
file io (properties) based on the Locale
|
JPF_java_text_Format |
native peer for java.text.Format delegation.
|
JPF_java_text_SimpleDateFormat |
(incomplete) native peer for SimpleDateFormat.
|
JPF_java_util_Calendar | |
JPF_java_util_concurrent_atomic_AtomicInteger |
native peer for java.util.concurrent.atomic.AtomicInteger
this implementation just cuts off native methods
|
JPF_java_util_concurrent_atomic_AtomicIntegerArray |
native peer for java.util.concurrent.atomic.AtomicIntegerArray
|
JPF_java_util_concurrent_atomic_AtomicIntegerFieldUpdater |
a full peer for the AtomicIntegerFieldUpdater
|
JPF_java_util_concurrent_atomic_AtomicLong |
native peer for java.util.concurrent.atomic.AtomicLong
this implementation just cuts off native methods
|
JPF_java_util_concurrent_atomic_AtomicLongArray |
native peer for java.util.concurrent.atomic.AtomicLongArray
|
JPF_java_util_concurrent_atomic_AtomicLongFieldUpdater |
a full peer for the AtomicLongFieldUpdater
|
JPF_java_util_concurrent_atomic_AtomicReferenceArray |
native peer for java.util.concurrent.atomic.AtomicReferenceArray
|
JPF_java_util_concurrent_atomic_AtomicReferenceFieldUpdater |
a full peer for the AtomicReferenceFieldUpdater
|
JPF_java_util_Date | |
JPF_java_util_Locale | |
JPF_java_util_logging_Level |
this is only a skeleton to make basic logging work under JPF
|
JPF_java_util_Random |
MJI NativePeer class for java.util.Random library abstraction
model - peer delegation is done via restoring a singleton, which unfortunately
has to resort to the rather nasty Unsafe mechanism because the required
random internals are private.
|
JPF_java_util_regex_Matcher |
native peer for a regex Matcher
this is just a delegatee peer
|
JPF_java_util_regex_Pattern | |
JPF_java_util_ResourceBundle |
native peer for ResourceBundle
|
JPF_java_util_TimeZone |
native peer for java.util.TimeZone
this is a (mostly) delegating implementation that became necessary because TimeZone has been
considerably changed in Java 1.7 (OpenJDK) and we need a version that is compatible with
pre and post 1.7 releases
|
JPF_sun_misc_Hashing |
simple forwarding sun.misc.Hashing peer to speed up execution and shorten traces
|
JPF_sun_misc_Unsafe |
we don't want this class! This is a hodgepodge of stuff that shouldn't be in Java, but
is handy for some hacks.
|
JPF_sun_misc_VM |
this is just a placeholder for now, we don't support its functionality
|
JPF_sun_net_www_protocol_http_Handler |
native peer to configure concrete URLConnection classes for specific URLs
We use model class configuration in case somebody wants to implement logic
in there that requires backtracking, and doesn't want to do this on the
native peer level
example config:
http.connection= http://*.dtd => gov.nasa.jpf.CachedROHttpConnection, http://foo.com/* -- x.y.MyHttpConnection
|
JPF_sun_reflect_Reflection | |
JPF_sun_reflect_ReflectionFactory |
<2do> hack around a hack - we need to override this as long as we don't
replace ObjectStreamClass
|
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 | |
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.
|
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
|
OverlappingContenderPolicy |
a thread tracking policy that uses ThreadInfoSets which are
search global from the point of object creation.
|
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.
|
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 | |
PrioritySchedulerFactory |
a scheduler policy which always runs one of the threads that
have equal top priority
|
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 | |
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
|
ShortFieldInfo |
fieldinfo for slots holding booleans
|
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.
|
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 | |
TidSet |
set that stores threads via (search global) thread ids.
|
Transition |
concrete type to store execution paths.
|
Types |
various type mangling/demangling routines
This reflects the general type id mess in Java.
|
Verify |
Verify is the programmatic interface of JPF that can be used from inside of
applications.
|
VM |
This class represents the virtual machine.
|
Enum | Description |
---|---|
HandlerContext.UncaughtHandlerType | |
ThreadInfo.State |
Exception | Description |
---|---|
ArrayIndexOutOfBoundsExecutiveException | |
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 (
|