gov.nasa.jpf.jvm

Class JVMClassInfo

java.lang.Object

gov.nasa.jpf.vm.InfoObject

gov.nasa.jpf.vm.ClassInfo

gov.nasa.jpf.jvm.JVMClassInfo

All Implemented Interfaces:

GenericSignatureHolder, java.lang.Cloneable, java.lang.Iterable<MethodInfo>

public class JVMClassInfo
extends ClassInfo

a ClassInfo that was created from a Java classfile

Field Summary

Fields

Modifier and Type	Field and Description
protected static StringSetMatcher	excludeNestedInit
protected static StringSetMatcher	includeNestedInit
protected static boolean	nestedInit

Fields inherited from class gov.nasa.jpf.vm.ClassInfo

allInterfaces, autoloadAnnotations, autoloaded, bootstrapMethods, classFileUrl, classLoader, config, container, elementInfoAttrs, EMPTY_FIELDINFO_ARRAY, EMPTY_STRING_ARRAY, enableAssertions, enclosingClassName, enclosingMethodName, fieldsFactory, finalizer, genericSignature, id, ID_FIELD, iFields, INITIALIZED, innerClassNames, instanceDataOffset, instanceDataSize, interfaceNames, interfaces, isAbstract, isArray, isBuiltin, isClass, isEnum, isObjectClassInfo, isRefClassInfo, isReferenceArray, isStringClassInfo, isThreadClassInfo, isWeakReference, logger, methods, modifiers, name, nativePeer, nClassInfos, nInstanceFields, NO_INTERFACES, NO_METHODS, packageName, releaseActions, sFields, signature, source, sourceFileName, staticDataSize, superClass, superClassName, thisClassLoader, UNINITIALIZED, UNINITIALIZED_STRING, uniqueId

Fields inherited from class gov.nasa.jpf.vm.InfoObject

annotations, attr, typeAnnotations

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	JVMClassInfo(ClassInfo funcInterface, BootstrapMethodInfo bootstrapMethod, java.lang.String name, java.lang.String samUniqueName, java.lang.String[] fieldTypesName)
protected	JVMClassInfo(ClassInfo ciAnnotation, java.lang.String proxyName, ClassLoaderInfo cli, java.lang.String url)

Method Summary

Modifier and Type	Method and Description
protected void	addClassInit(ThreadInfo ti, JVMDirectCallStackFrame frame, JVMCodeBuilder cb)
protected ClassInfo	createAnnotationProxy(java.lang.String proxyName)
DirectCallStackFrame	createDirectCallStackFrame(ThreadInfo ti, MethodInfo miCallee, int nLocals)
protected ClassInfo	createFuncObjClassInfo(BootstrapMethodInfo bootstrapMethod, java.lang.String name, java.lang.String samUniqueName, java.lang.String[] fieldTypesName) This is called on the functional interface type.
DirectCallStackFrame	createRunStartStackFrame(ThreadInfo ti, MethodInfo miRun) while this is a normal DirectCallStackFrame, it has different code which has to be created here
StackFrame	createStackFrame(ThreadInfo ti, MethodInfo callee)
protected JVMCodeBuilder	getSystemCodeBuilder(ClassFile cf, MethodInfo mi)
protected static boolean	init(Config config)
boolean	initializeClass(ThreadInfo ti) perform initialization of this class and its not-yet-initialized superclasses (top down), which includes calling clinit() methods This is overridden here to model a questionable yet consequential behavior of hotspot, which is holding derived class locks when initializing base classes.
protected void	setAnnotationValueGetterCode(MethodInfo pmi, FieldInfo fi) to be called from super proxy ctor this needs to be in the VM specific ClassInfo because we need to create code
protected void	setDirectCallCode(MethodInfo miDirectCall, MethodInfo miCallee)
protected void	setLambdaDirectCallCode(MethodInfo miDirectCall, BootstrapMethodInfo bootstrapMethod) This method creates the body of the function object method that captures the lambda behavior.
protected void	setNativeCallCode(NativeMethodInfo miNative)
protected void	setRunStartCode(MethodInfo miStub, MethodInfo miRun)

Methods inherited from class gov.nasa.jpf.vm.ClassInfo

addElementInfoAttr, addReleaseAction, areAssertionsEnabled, checkInheritedAnnotations, checkNoClinitInitialization, checkUnresolvedNativeMethods, cloneFor, computeSourceFileName, createInstanceFields, declaredMethodIterator, desiredAssertionStatus, equals, getAllInterfaceClassInfos, getAllInterfaces, getAnnotation, getAnnotationProxy, getAnnotations, getBootstrapMethodInfo, getClassFileUrl, getClassInfo, getClassLoaderInfo, getClassObject, getClassObjectRef, getClinit, getComponentClassInfo, getContainer, getDeclaredInstanceField, getDeclaredInstanceField, getDeclaredInstanceFields, getDeclaredMethodInfos, getDeclaredMethods, getDeclaredStaticField, getDeclaredStaticFields, getDefaultMethod, getDirectInterfaceNames, getElementInfoAttrs, getEnclosingClassInfo, getEnclosingClassName, getEnclosingMethodInfo, getEnclosingMethodName, getFieldAttrs, getFinalizer, getFinalizer0, getGenericSignature, getId, getInitializedClassInfo, getInitializedSystemClassInfo, getInnerClasses, getInnerClassInfos, getInstanceDataSize, getInstanceField, getInstanceField, getInstanceFields, getInterfaceAbstractMethod, getInterfaceClassInfos, getMatchingInstructions, getMatchingMethodInfos, getMethod, getMethod, getModifiableClassObject, getModifiableStaticElementInfo, getModifiers, getName, getNativePeer, getNumberOfDeclaredInstanceFields, getNumberOfInstanceFields, getNumberOfLoadedClasses, getNumberOfStaticFields, getNumberOfSuperClasses, getPackageName, getReflectionMethod, getResolvedAnnotationInfo, getSignature, getSimpleName, getSource, getSourceFileName, getStaticDataSize, getStaticElementInfo, getStaticField, getStaticField, getStaticFieldName, getStaticFieldValueObject, getStatics, getSuperClass, getSuperClass, getSuperClassName, getType, getUniqueId, hasAnnotations, hasCtors, hashCode, hasInnerClass, hasInstanceFieldInfoAttr, hasInstanceFields, hasReleaseAction, initializeClassAtomic, isAbstract, isArray, isBoxClass, isBuiltin, isBuiltinClass, isEnum, isEnum0, isInitialized, isInitializing, isInnerClassOf, isInstanceOf, isInstanceOf, isInterface, isObjectClassInfo, isObjectClassInfo, isObjectClassInfo0, isPrimitive, isRefClassInfo0, isReferenceArray, isReferenceClassInfo, isRegistered, isResolved, isStaticMethodAbstractionDeterministic, isStringClassInfo, isStringClassInfo, isStringClassInfo0, isSystemClass, isThreadClassInfo, isThreadClassInfo0, isWeakReference, isWeakReference0, iterator, linkFields, linkFields, loadAnnotationListeners, loadArrayInterfaces, loadBuiltinInterfaces, loadInterfaces, loadNativePeer, loadSource, loadSuperClass, makeModelClassPath, matchDeclaredMethods, matchMethods, needsInitialization, processJPFAnnotations, processJPFAttrAnnotation, processJPFConfigAnnotation, processNoJPFExecutionAnnotation, processReleaseActions, putDeclaredMethod, registerClass, resolveAndLink, resolveClass, resolveReferencedClass, setAnnotations, setAssertionStatus, setClass, setElementInfoAttrs, setEnclosingClass, setEnclosingMethod, setFields, setGenericSignature, setInitialized, setInitializing, setInnerClassNames, setInterfaceNames, setMethod, setMethods, setSourceFile, toString

Methods inherited from class gov.nasa.jpf.vm.InfoObject

addAnnotation, addAnnotations, addAttr, addTypeAnnotation, addTypeAnnotations, attrIterator, attrIterator, getAttr, getAttr, getDeclaredAnnotations, getNextAttr, getTargetTypeAnnotations, getTypeAnnotation, getTypeAnnotations, hasAnnotation, hasAttr, hasAttr, hasAttrValue, hasTypeAnnotation, hasTypeAnnotations, removeAttr, replaceAttr, setAttr, setTypeAnnotations

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

nestedInit

protected static boolean nestedInit

includeNestedInit

protected static StringSetMatcher includeNestedInit

excludeNestedInit

protected static StringSetMatcher excludeNestedInit

Constructor Detail

JVMClassInfo

protected JVMClassInfo(ClassInfo ciAnnotation,
                       java.lang.String proxyName,
                       ClassLoaderInfo cli,
                       java.lang.String url)

JVMClassInfo

protected JVMClassInfo(ClassInfo funcInterface,
                       BootstrapMethodInfo bootstrapMethod,
                       java.lang.String name,
                       java.lang.String samUniqueName,
                       java.lang.String[] fieldTypesName)

Method Detail

init

protected static boolean init(Config config)

createAnnotationProxy

protected ClassInfo createAnnotationProxy(java.lang.String proxyName)

Overrides:

createAnnotationProxy in class ClassInfo

createFuncObjClassInfo

protected ClassInfo createFuncObjClassInfo(BootstrapMethodInfo bootstrapMethod,
                                           java.lang.String name,
                                           java.lang.String samUniqueName,
                                           java.lang.String[] fieldTypesName)

This is called on the functional interface type. It creates a synthetic type which implements the functional interface and contains a method capturing the behavior of the lambda expression.

Overrides:

createFuncObjClassInfo in class ClassInfo

initializeClass

public boolean initializeClass(ThreadInfo ti)

perform initialization of this class and its not-yet-initialized superclasses (top down), which includes calling clinit() methods This is overridden here to model a questionable yet consequential behavior of hotspot, which is holding derived class locks when initializing base classes. The generic implementation in ClassInfo uses non-nested locks (i.e. A.clinit() only synchronizes on A.class) and hence cannot produce the same static init deadlocks as hotspot. In order to catch such defects we implement nested locking here. The main difference is that the generic implementation only pushes DCSFs for required clinits and otherwise doesn't lock anything. Here, we create one static init specific DCSF which wraps all clinits in nested monitorenter/exits. We create this even if there is no clinit so that we mimic hotspot locking. Note this scheme also enables us to get rid of the automatic clinit sync (they don't have a 0x20 sync modifier in classfiles)

Overrides:

initializeClass in class ClassInfo

Returns:

true if client needs to re-execute because we pushed DirectCallStackFrames

addClassInit

protected void addClassInit(ThreadInfo ti,
                            JVMDirectCallStackFrame frame,
                            JVMCodeBuilder cb)

getSystemCodeBuilder

protected JVMCodeBuilder getSystemCodeBuilder(ClassFile cf,
                                              MethodInfo mi)

setAnnotationValueGetterCode

protected void setAnnotationValueGetterCode(MethodInfo pmi,
                                            FieldInfo fi)

to be called from super proxy ctor this needs to be in the VM specific ClassInfo because we need to create code

Overrides:

setAnnotationValueGetterCode in class ClassInfo

setDirectCallCode

protected void setDirectCallCode(MethodInfo miDirectCall,
                                 MethodInfo miCallee)

Overrides:

setDirectCallCode in class ClassInfo

setNativeCallCode

protected void setNativeCallCode(NativeMethodInfo miNative)

Overrides:

setNativeCallCode in class ClassInfo

setRunStartCode

protected void setRunStartCode(MethodInfo miStub,
                               MethodInfo miRun)

Overrides:

setRunStartCode in class ClassInfo

setLambdaDirectCallCode

protected void setLambdaDirectCallCode(MethodInfo miDirectCall,
                                       BootstrapMethodInfo bootstrapMethod)

This method creates the body of the function object method that captures the lambda behavior.

Overrides:

setLambdaDirectCallCode in class ClassInfo

createStackFrame

public StackFrame createStackFrame(ThreadInfo ti,
                                   MethodInfo callee)

Overrides:

createStackFrame in class ClassInfo

createDirectCallStackFrame

public DirectCallStackFrame createDirectCallStackFrame(ThreadInfo ti,
                                                       MethodInfo miCallee,
                                                       int nLocals)

Overrides:

createDirectCallStackFrame in class ClassInfo

createRunStartStackFrame

public DirectCallStackFrame createRunStartStackFrame(ThreadInfo ti,
                                                     MethodInfo miRun)

while this is a normal DirectCallStackFrame, it has different code which has to be created here

Overrides:

createRunStartStackFrame in class ClassInfo