--- /dev/null
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0.
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package gov.nasa.jpf.vm;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.annotation.MJI;
+import gov.nasa.jpf.util.MethodInfoRegistry;
+import gov.nasa.jpf.util.RunListener;
+import gov.nasa.jpf.util.RunRegistry;
+
+import java.lang.reflect.Modifier;
+import java.util.ArrayList;
+
+public class JPF_java_lang_reflect_Method extends NativePeer {
+
+ static MethodInfoRegistry registry;
+
+ // class init - this is called automatically from the NativePeer ctor
+ public static boolean init (Config conf) {
+ // this is an example of how to handle cross-initialization between
+ // native peers - this might also get explicitly called by the java.lang.Class
+ // peer, since it creates Method objects. Here we have to make sure
+ // we only reset between JPF runs
+
+ if (registry == null){
+ registry = new MethodInfoRegistry();
+
+ RunRegistry.getDefaultRegistry().addListener( new RunListener() {
+ @Override
+ public void reset (RunRegistry reg){
+ registry = null;
+ }
+ });
+ }
+ return true;
+ }
+
+ static int createMethodObject (MJIEnv env, ClassInfo ciMth, MethodInfo mi){
+ // note - it is the callers responsibility to ensure Method is properly initialized
+ int regIdx = registry.registerMethodInfo(mi);
+ int eidx = env.newObject( ciMth);
+ ElementInfo ei = env.getModifiableElementInfo(eidx);
+
+ ei.setIntField("regIdx", regIdx);
+ ei.setBooleanField("isAccessible", mi.isPublic());
+
+ return eidx;
+ }
+
+ // this is NOT an MJI method, but it is used outside this package, so
+ // we have to add 'final'
+ public static final MethodInfo getMethodInfo (MJIEnv env, int objRef){
+ return registry.getMethodInfo(env,objRef, "regIdx");
+ }
+
+ @MJI
+ public int getName____Ljava_lang_String_2 (MJIEnv env, int objRef) {
+ MethodInfo mi = getMethodInfo(env, objRef);
+
+ int nameRef = env.getReferenceField( objRef, "name");
+ if (nameRef == MJIEnv.NULL) {
+ nameRef = env.newString(mi.getName());
+ env.setReferenceField(objRef, "name", nameRef);
+ }
+
+ return nameRef;
+ }
+
+ @MJI
+ public int getModifiers____I (MJIEnv env, int objRef){
+ MethodInfo mi = getMethodInfo(env, objRef);
+ return mi.getModifiers();
+ }
+
+ static int getParameterTypes( MJIEnv env, MethodInfo mi) {
+ ThreadInfo ti = env.getThreadInfo();
+ String[] argTypeNames = mi.getArgumentTypeNames();
+ int[] ar = new int[argTypeNames.length];
+
+ for (int i = 0; i < argTypeNames.length; i++) {
+ ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
+ if (!ci.isRegistered()) {
+ ci.registerClass(ti);
+ }
+
+ ar[i] = ci.getClassObjectRef();
+ }
+
+ int aRef = env.newObjectArray("Ljava/lang/Class;", argTypeNames.length);
+ for (int i = 0; i < argTypeNames.length; i++) {
+ env.setReferenceArrayElement(aRef, i, ar[i]);
+ }
+
+ return aRef;
+ }
+
+ @MJI
+ public int getParameterTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef){
+ return getParameterTypes(env, getMethodInfo(env, objRef));
+ }
+
+ int getExceptionTypes(MJIEnv env, MethodInfo mi) {
+ ThreadInfo ti = env.getThreadInfo();
+ String[] exceptionNames = mi.getThrownExceptionClassNames();
+
+ if (exceptionNames == null) {
+ exceptionNames = new String[0];
+ }
+
+ int[] ar = new int[exceptionNames.length];
+
+ for (int i = 0; i < exceptionNames.length; i++) {
+ ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(exceptionNames[i]);
+ if (!ci.isRegistered()) {
+ ci.registerClass(ti);
+ }
+
+ ar[i] = ci.getClassObjectRef();
+ }
+
+ int aRef = env.newObjectArray("Ljava/lang/Class;", exceptionNames.length);
+ for (int i = 0; i < exceptionNames.length; i++) {
+ env.setReferenceArrayElement(aRef, i, ar[i]);
+ }
+
+ return aRef;
+ }
+
+ @MJI
+ public int getExceptionTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef) {
+ return getExceptionTypes(env, getMethodInfo(env, objRef));
+ }
+
+ @MJI
+ public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){
+ MethodInfo mi = getMethodInfo(env, objRef);
+ ThreadInfo ti = env.getThreadInfo();
+
+ ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
+ if (!ci.isRegistered()) {
+ ci.registerClass(ti);
+ }
+
+ return ci.getClassObjectRef();
+ }
+
+ @MJI
+ public int getDeclaringClass____Ljava_lang_Class_2 (MJIEnv env, int objRef){
+ MethodInfo mi = getMethodInfo(env, objRef);
+ ClassInfo ci = mi.getClassInfo();
+ // it's got to be registered, otherwise we wouldn't be able to acquire the Method object
+ return ci.getClassObjectRef();
+ }
+
+ static int createBoxedReturnValueObject (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame) {
+ byte rt = mi.getReturnTypeCode();
+ int ret = MJIEnv.NULL;
+ ElementInfo rei;
+ Object attr = null;
+
+ if (rt == Types.T_DOUBLE) {
+ attr = frame.getLongResultAttr();
+ double v = frame.getDoubleResult();
+ ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"));
+ rei = env.getModifiableElementInfo(ret);
+ rei.setDoubleField("value", v);
+ } else if (rt == Types.T_FLOAT) {
+ attr = frame.getResultAttr();
+ float v = frame.getFloatResult();
+ ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"));
+ rei = env.getModifiableElementInfo(ret);
+ rei.setFloatField("value", v);
+ } else if (rt == Types.T_LONG) {
+ attr = frame.getLongResultAttr();
+ long v = frame.getLongResult();
+ ret = env.valueOfLong(v);
+ } else if (rt == Types.T_BYTE) {
+ attr = frame.getResultAttr();
+ int v = frame.getResult();
+ ret = env.valueOfByte((byte)v);
+ } else if (rt == Types.T_CHAR) {
+ attr = frame.getResultAttr();
+ int v = frame.getResult();
+ ret = env.valueOfCharacter((char)v);
+ } else if (rt == Types.T_SHORT) {
+ attr = frame.getResultAttr();
+ int v = frame.getResult();
+ ret = env.valueOfShort((short)v);
+ } else if (rt == Types.T_INT) {
+ attr = frame.getResultAttr();
+ int v = frame.getResult();
+ ret = env.valueOfInteger(v);
+ } else if (rt == Types.T_BOOLEAN) {
+ attr = frame.getResultAttr();
+ int v = frame.getResult();
+ ret = env.valueOfBoolean((v == 1)? true: false);
+ } else if (mi.isReferenceReturnType()){
+ attr = frame.getResultAttr();
+ ret = frame.getReferenceResult();
+ }
+
+ env.setReturnAttribute(attr);
+ return ret;
+ }
+
+ static boolean pushUnboxedArguments (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame, int argIdx, int argsRef) {
+ ElementInfo source;
+ ClassInfo sourceClass;
+ String destTypeNames[];
+ int nArgs, passedCount, sourceRef;
+ byte sourceType, destTypes[];
+
+ destTypes = mi.getArgumentTypes();
+ destTypeNames = mi.getArgumentTypeNames();
+ nArgs = destTypeNames.length;
+
+ // according to the API docs, passing null instead of an empty array is allowed for no args
+ passedCount = (argsRef != MJIEnv.NULL) ? env.getArrayLength(argsRef) : 0;
+
+ if (nArgs != passedCount) {
+ env.throwException(IllegalArgumentException.class.getName(), "Wrong number of arguments passed. Actual = " + passedCount + ". Expected = " + nArgs);
+ return false;
+ }
+
+ for (int i = 0; i < nArgs; i++) {
+ sourceRef = env.getReferenceArrayElement(argsRef, i);
+
+ // we have to handle null references explicitly
+ if (sourceRef == MJIEnv.NULL) {
+ if ((destTypes[i] != Types.T_REFERENCE) && (destTypes[i] != Types.T_ARRAY)) {
+ env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ". Actual = (null). Expected = " + destTypeNames[i]);
+ return false;
+ }
+
+ frame.pushRef(MJIEnv.NULL);
+ continue;
+ }
+
+ source = env.getElementInfo(sourceRef);
+ sourceClass = source.getClassInfo();
+ sourceType = getSourceType( sourceClass, destTypes[i], destTypeNames[i]);
+
+ Object attr = env.getElementInfo(argsRef).getFields().getFieldAttr(i);
+ if ((argIdx = pushArg( argIdx, frame, source, sourceType, destTypes[i], attr)) < 0 ){
+ env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ". Source Class = " + sourceClass.getName() + ". Dest Class = " + destTypeNames[i]);
+ return false;
+ }
+ }
+
+ return true;
+ }
+
+ // this returns the primitive type in case we have to unbox, and otherwise checks reference type compatibility
+ private static byte getSourceType (ClassInfo ciArgVal, byte destType, String destTypeName){
+ switch (destType){
+ // the primitives
+ case Types.T_BOOLEAN:
+ case Types.T_BYTE:
+ case Types.T_CHAR:
+ case Types.T_SHORT:
+ case Types.T_INT:
+ case Types.T_LONG:
+ case Types.T_FLOAT:
+ case Types.T_DOUBLE:
+ return Types.getUnboxedType(ciArgVal.getName());
+
+ case Types.T_ARRAY:
+ case Types.T_REFERENCE: // check if the source type is assignment compatible with the destType
+ if (ciArgVal.isInstanceOf(destTypeName)){
+ return destType;
+ }
+ }
+
+ return Types.T_NONE;
+ }
+
+ // do the proper type conversion - Java is pretty forgiving here and does
+ // not throw exceptions upon value truncation
+ private static int pushArg( int argIdx, DirectCallStackFrame frame, ElementInfo eiArg, byte srcType, byte destType, Object attr){
+ switch (srcType) {
+ case Types.T_DOUBLE:
+ {
+ double v = eiArg.getDoubleField("value");
+ if (destType == Types.T_DOUBLE){
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_FLOAT: // covers float, double
+ {
+ float v = eiArg.getFloatField("value");
+ switch (destType){
+ case Types.T_FLOAT:
+ return frame.setFloatArgument( argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_LONG:
+ {
+ long v = eiArg.getLongField("value");
+ switch (destType){
+ case Types.T_LONG:
+ return frame.setLongArgument(argIdx, v, attr);
+ case Types.T_FLOAT:
+ return frame.setFloatArgument(argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_INT:
+ {
+ int v = eiArg.getIntField("value");
+ switch (destType){
+ case Types.T_INT:
+ return frame.setArgument( argIdx, v, attr);
+ case Types.T_LONG:
+ return frame.setLongArgument( argIdx, v, attr);
+ case Types.T_FLOAT:
+ return frame.setFloatArgument(argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_SHORT:
+ {
+ int v = eiArg.getShortField("value");
+ switch (destType){
+ case Types.T_SHORT:
+ case Types.T_INT:
+ return frame.setArgument( argIdx, v, attr);
+ case Types.T_LONG:
+ return frame.setLongArgument( argIdx, v, attr);
+ case Types.T_FLOAT:
+ return frame.setFloatArgument(argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_BYTE:
+ {
+ byte v = eiArg.getByteField("value");
+ switch (destType){
+ case Types.T_BYTE:
+ case Types.T_SHORT:
+ case Types.T_INT:
+ return frame.setArgument( argIdx, v, attr);
+ case Types.T_LONG:
+ return frame.setLongArgument( argIdx, v, attr);
+ case Types.T_FLOAT:
+ return frame.setFloatArgument(argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_CHAR:
+ {
+ char v = eiArg.getCharField("value");
+ switch (destType){
+ case Types.T_CHAR:
+ case Types.T_INT:
+ return frame.setArgument( argIdx, v, attr);
+ case Types.T_LONG:
+ return frame.setLongArgument( argIdx, v, attr);
+ case Types.T_FLOAT:
+ return frame.setFloatArgument(argIdx, v, attr);
+ case Types.T_DOUBLE:
+ return frame.setDoubleArgument( argIdx, v, attr);
+ }
+ return -1;
+ }
+ case Types.T_BOOLEAN:
+ {
+ boolean v = eiArg.getBooleanField("value");
+ if (destType == Types.T_BOOLEAN){
+ return frame.setArgument( argIdx, v ? 1 : 0, attr);
+ }
+ return -1;
+ }
+ case Types.T_ARRAY:
+ {
+ int ref = eiArg.getObjectRef();
+ if (destType == Types.T_ARRAY){
+ return frame.setReferenceArgument( argIdx, ref, attr);
+ }
+ return -1;
+ }
+ case Types.T_REFERENCE:
+ {
+ int ref = eiArg.getObjectRef();
+ if (destType == Types.T_REFERENCE){
+ return frame.setReferenceArgument( argIdx, ref, attr);
+ }
+ return -1;
+ }
+ default:
+ // T_VOID, T_NONE
+ return -1;
+ }
+ }
+
+ @MJI
+ public int invoke__Ljava_lang_Object_2_3Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int mthRef, int objRef, int argsRef) {
+ ThreadInfo ti = env.getThreadInfo();
+ MethodInfo miCallee = getMethodInfo(env, mthRef);
+ ClassInfo calleeClass = miCallee.getClassInfo();
+ DirectCallStackFrame frame = ti.getReturnedDirectCall();
+
+ if (frame == null){ // first time
+
+ //--- check the instance we are calling on
+ if (!miCallee.isStatic()) {
+ if (objRef == MJIEnv.NULL){
+ env.throwException("java.lang.NullPointerException");
+ return MJIEnv.NULL;
+
+ } else {
+ ElementInfo eiObj = ti.getElementInfo(objRef);
+ ClassInfo objClass = eiObj.getClassInfo();
+
+ if (!objClass.isInstanceOf(calleeClass)) {
+ env.throwException(IllegalArgumentException.class.getName(), "Object is not an instance of declaring class. Actual = " + objClass + ". Expected = " + calleeClass);
+ return MJIEnv.NULL;
+ }
+ }
+ }
+
+ //--- check accessibility
+ ElementInfo eiMth = ti.getElementInfo(mthRef);
+ if (! (Boolean) eiMth.getFieldValueObject("isAccessible")) {
+ StackFrame caller = ti.getTopFrame().getPrevious();
+ ClassInfo callerClass = caller.getClassInfo();
+
+ if (callerClass != calleeClass) {
+ env.throwException(IllegalAccessException.class.getName(), "Class " + callerClass.getName() +
+ " can not access a member of class " + calleeClass.getName()
+ + " with modifiers \"" + Modifier.toString(miCallee.getModifiers()));
+ return MJIEnv.NULL;
+ }
+ }
+
+ //--- push the direct call
+ frame = miCallee.createDirectCallStackFrame(ti, 0);
+ frame.setReflection();
+
+ int argOffset = 0;
+ if (!miCallee.isStatic()) {
+ frame.setReferenceArgument( argOffset++, objRef, null);
+ }
+ if (!pushUnboxedArguments( env, miCallee, frame, argOffset, argsRef)) {
+ // we've got a IllegalArgumentException
+ return MJIEnv.NULL;
+ }
+ ti.pushFrame(frame);
+
+
+ //--- check for and push required clinits
+ if (miCallee.isStatic()){
+ calleeClass.initializeClass(ti);
+ }
+
+ return MJIEnv.NULL; // reexecute
+
+ } else { // we have returned from the direct call
+ return createBoxedReturnValueObject( env, miCallee, frame);
+ }
+ }
+
+
+ // this one has to collect annotations upwards in the inheritance chain
+ static int getAnnotations (MJIEnv env, MethodInfo mi){
+ String mname = mi.getName();
+ String msig = mi.genericSignature;
+ ArrayList<AnnotationInfo> aiList = new ArrayList<AnnotationInfo>();
+
+ // our own annotations
+ ClassInfo ci = mi.getClassInfo();
+ for (AnnotationInfo ai : mi.getAnnotations()) {
+ aiList.add(ai);
+ }
+
+ // our superclass annotations
+ for (ci = ci.getSuperClass(); ci != null; ci = ci.getSuperClass()){
+ mi = ci.getMethod(mname, msig, false);
+ if (mi != null){
+ for (AnnotationInfo ai: mi.getAnnotations()){
+ aiList.add(ai);
+ }
+ }
+ }
+
+ try {
+ return env.newAnnotationProxies(aiList.toArray(new AnnotationInfo[aiList.size()]));
+ } catch (ClinitRequired x){
+ env.handleClinitRequest(x.getRequiredClassInfo());
+ return MJIEnv.NULL;
+ }
+ }
+
+ @MJI
+ public int getAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
+ return getAnnotations( env, getMethodInfo(env,mthRef));
+ }
+
+ // the following ones consist of a package default implementation that is shared with
+ // the constructor peer, and a public model method
+ static int getAnnotation (MJIEnv env, MethodInfo mi, int annotationClsRef){
+ ClassInfo aci = env.getReferredClassInfo(annotationClsRef);
+
+ AnnotationInfo ai = mi.getAnnotation(aci.getName());
+ if (ai != null){
+ ClassInfo aciProxy = aci.getAnnotationProxy();
+ try {
+ return env.newAnnotationProxy(aciProxy, ai);
+ } catch (ClinitRequired x){
+ env.handleClinitRequest(x.getRequiredClassInfo());
+ return MJIEnv.NULL;
+ }
+ }
+
+ return MJIEnv.NULL;
+ }
+
+ @MJI
+ public int getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef, int annotationClsRef) {
+ return getAnnotation(env, getMethodInfo(env,mthRef), annotationClsRef);
+ }
+
+ static int getDeclaredAnnotations (MJIEnv env, MethodInfo mi){
+ AnnotationInfo[] ai = mi.getAnnotations();
+
+ try {
+ return env.newAnnotationProxies(ai);
+ } catch (ClinitRequired x){
+ env.handleClinitRequest(x.getRequiredClassInfo());
+ return MJIEnv.NULL;
+ }
+ }
+
+ @MJI
+ public int getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
+ return getDeclaredAnnotations( env, getMethodInfo(env,mthRef));
+ }
+
+ static int getParameterAnnotations (MJIEnv env, MethodInfo mi){
+ AnnotationInfo[][] pa = mi.getParameterAnnotations();
+ // this should always return an array object, even if the method has no arguments
+
+ try {
+ int paRef = env.newObjectArray("[Ljava/lang/annotation/Annotation;", pa.length);
+
+ for (int i=0; i<pa.length; i++){
+ int eRef = env.newAnnotationProxies(pa[i]);
+ env.setReferenceArrayElement(paRef, i, eRef);
+ }
+
+ return paRef;
+
+ } catch (ClinitRequired x){ // be prepared that we might have to initialize respective annotation classes
+ env.handleClinitRequest(x.getRequiredClassInfo());
+ return MJIEnv.NULL;
+ }
+ }
+
+ @MJI
+ public int getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
+ return getParameterAnnotations( env, getMethodInfo(env,mthRef));
+ }
+
+ @MJI
+ public int toString____Ljava_lang_String_2 (MJIEnv env, int objRef){
+ StringBuilder sb = new StringBuilder();
+
+ MethodInfo mi = getMethodInfo(env, objRef);
+
+ sb.append(Modifier.toString(mi.getModifiers()));
+ sb.append(' ');
+
+ sb.append(mi.getReturnTypeName());
+ sb.append(' ');
+
+ sb.append(mi.getClassName());
+ sb.append('.');
+
+ sb.append(mi.getName());
+
+ sb.append('(');
+
+ String[] at = mi.getArgumentTypeNames();
+ for (int i=0; i<at.length; i++){
+ if (i>0) sb.append(',');
+ sb.append(at[i]);
+ }
+
+ sb.append(')');
+
+ int sref = env.newString(sb.toString());
+ return sref;
+ }
+
+ @MJI
+ public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int mthRef){
+ ElementInfo ei = env.getElementInfo(mthRef);
+ ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo(JPF_java_lang_Class.METHOD_CLASSNAME);
+
+ if (ei.getClassInfo() == ci){
+ MethodInfo mi1 = getMethodInfo(env, objRef);
+ MethodInfo mi2 = getMethodInfo(env, mthRef);
+ if (mi1.getClassInfo() == mi2.getClassInfo()){
+ if (mi1.getName().equals(mi2.getName())){
+ if (mi1.getReturnType().equals(mi2.getReturnType())){
+ byte[] params1 = mi1.getArgumentTypes();
+ byte[] params2 = mi2.getArgumentTypes();
+ if (params1.length == params2.length){
+ for (int i = 0; i < params1.length; i++){
+ if (params1[i] != params2[i]){
+ return false;
+ }
+ }
+ return true;
+ }
+ }
+ }
+ }
+ }
+ return false;
+ }
+
+ @MJI
+ public int hashCode____I (MJIEnv env, int objRef){
+ MethodInfo mi = getMethodInfo(env, objRef);
+ return mi.getClassName().hashCode() ^ mi.getName().hashCode();
+ }
+}
projects / jpf-core.git / blobdiff