2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.annotation.MJI;
22 import gov.nasa.jpf.util.MethodInfoRegistry;
23 import gov.nasa.jpf.util.RunListener;
24 import gov.nasa.jpf.util.RunRegistry;
26 import java.lang.reflect.Modifier;
27 import java.util.ArrayList;
29 public class JPF_java_lang_reflect_Method extends NativePeer {
31 static MethodInfoRegistry registry;
33 // class init - this is called automatically from the NativePeer ctor
34 public static boolean init (Config conf) {
35 // this is an example of how to handle cross-initialization between
36 // native peers - this might also get explicitly called by the java.lang.Class
37 // peer, since it creates Method objects. Here we have to make sure
38 // we only reset between JPF runs
40 if (registry == null){
41 registry = new MethodInfoRegistry();
43 RunRegistry.getDefaultRegistry().addListener( new RunListener() {
45 public void reset (RunRegistry reg){
53 static int createMethodObject (MJIEnv env, ClassInfo ciMth, MethodInfo mi){
54 // note - it is the callers responsibility to ensure Method is properly initialized
55 int regIdx = registry.registerMethodInfo(mi);
56 int eidx = env.newObject( ciMth);
57 ElementInfo ei = env.getModifiableElementInfo(eidx);
59 ei.setIntField("regIdx", regIdx);
60 ei.setBooleanField("isAccessible", mi.isPublic());
65 // this is NOT an MJI method, but it is used outside this package, so
66 // we have to add 'final'
67 public static final MethodInfo getMethodInfo (MJIEnv env, int objRef){
68 return registry.getMethodInfo(env,objRef, "regIdx");
72 public int getName____Ljava_lang_String_2 (MJIEnv env, int objRef) {
73 MethodInfo mi = getMethodInfo(env, objRef);
75 int nameRef = env.getReferenceField( objRef, "name");
76 if (nameRef == MJIEnv.NULL) {
77 nameRef = env.newString(mi.getName());
78 env.setReferenceField(objRef, "name", nameRef);
85 public int getModifiers____I (MJIEnv env, int objRef){
86 MethodInfo mi = getMethodInfo(env, objRef);
87 return mi.getModifiers();
90 static int getParameterTypes( MJIEnv env, MethodInfo mi) {
91 ThreadInfo ti = env.getThreadInfo();
92 String[] argTypeNames = mi.getArgumentTypeNames();
93 int[] ar = new int[argTypeNames.length];
95 for (int i = 0; i < argTypeNames.length; i++) {
96 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
97 if (!ci.isRegistered()) {
101 ar[i] = ci.getClassObjectRef();
104 int aRef = env.newObjectArray("Ljava/lang/Class;", argTypeNames.length);
105 for (int i = 0; i < argTypeNames.length; i++) {
106 env.setReferenceArrayElement(aRef, i, ar[i]);
113 public int getParameterTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef){
114 return getParameterTypes(env, getMethodInfo(env, objRef));
117 // TODO: Fix for Groovy's model-checking
118 private static int getParameterizedTypeImplObj(String signature, MJIEnv env) {
120 ThreadInfo ti = env.getThreadInfo();
121 ClassLoaderInfo cli = env.getSystemClassLoaderInfo();
122 ClassInfo ci = cli.getResolvedClassInfo("sun.reflect.generics.reflectiveObjects.ParameterizedTypeImpl");
123 // Create a new object of type ParameterizedTypeImpl
124 int paramTypeRef = env.newObject(ci);
125 ElementInfo ei = env.getModifiableElementInfo(paramTypeRef);
126 // Get field information and fill out the fields
128 String className = Types.getGenericClassName(signature);
129 ClassInfo gci = cli.getResolvedClassInfo(className);
130 if (!gci.isRegistered()) {
131 gci.registerClass(ti);
133 ei.setReferenceField("rawType", gci.getClassObjectRef());
135 // actualTypeArguments
136 String[] parameterizedTypes = Types.getParameterizedTypesFromArgumentTypeNames(signature);
137 int[] types = new int[parameterizedTypes.length];
138 for(int j = 0; j < parameterizedTypes.length; j++) {
139 ClassInfo pci = cli.getResolvedClassInfo(parameterizedTypes[j]);
140 if (!pci.isRegistered()) {
141 pci.registerClass(ti);
143 types[j] = pci.getClassObjectRef();
145 int aRef = env.newObjectArray("Ljava/lang/reflect/Type;", parameterizedTypes.length);
146 // Set references for every array element
147 for (int j = 0; j < parameterizedTypes.length; j++) {
148 env.setReferenceArrayElement(aRef, j, types[j]);
150 ei.setReferenceField("actualTypeArguments", aRef);
153 String ownerType = Types.getOwnerClassName(signature);
154 if (ownerType != null) {
155 ClassInfo oci = ClassLoaderInfo.getCurrentResolvedClassInfo(ownerType);
156 if (!oci.isRegistered()) {
157 oci.registerClass(ti);
159 ei.setReferenceField("ownerType", oci.getClassObjectRef());
161 ei.setReferenceField("ownerType", MJIEnv.NULL);
167 static int getGenericParameterTypes( MJIEnv env, int objRef, MethodInfo mi) {
168 ThreadInfo ti = env.getThreadInfo();
169 String[] argTypeNames = mi.getArgumentGenericTypeNames();
170 int[] ar = new int[argTypeNames.length];
172 for (int i = 0; i < argTypeNames.length; i++) {
173 // Change this into just the generic class type if it is a generic class
174 if (Types.isGenericSignature(argTypeNames[i])) {
175 ar[i] = getParameterizedTypeImplObj(argTypeNames[i], env);
177 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
178 if (!ci.isRegistered()) {
179 ci.registerClass(ti);
181 ar[i] = ci.getClassObjectRef();
184 int aRef = env.newObjectArray("Ljava/lang/reflect/Type;", argTypeNames.length);
185 for (int i = 0; i < argTypeNames.length; i++) {
186 env.setReferenceArrayElement(aRef, i, ar[i]);
193 public int getGenericParameterTypes_____3Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
194 return getGenericParameterTypes(env, objRef, getMethodInfo(env, objRef));
198 public int getGenericReturnType____Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
199 MethodInfo mi = getMethodInfo(env, objRef);
200 ThreadInfo ti = env.getThreadInfo();
202 String returnTypeName = mi.getGenericReturnTypeName();
204 if (Types.isGenericSignature(returnTypeName)) {
205 retRef = getParameterizedTypeImplObj(returnTypeName, env);
207 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(returnTypeName);
208 if (!ci.isRegistered()) {
209 ci.registerClass(ti);
211 retRef = ci.getClassObjectRef();
216 // TODO: Fix for Groovy's model-checking
217 // TODO: We have been able to only register the generic class and not yet the parameterized types
219 int getExceptionTypes(MJIEnv env, MethodInfo mi) {
220 ThreadInfo ti = env.getThreadInfo();
221 String[] exceptionNames = mi.getThrownExceptionClassNames();
223 if (exceptionNames == null) {
224 exceptionNames = new String[0];
227 int[] ar = new int[exceptionNames.length];
229 for (int i = 0; i < exceptionNames.length; i++) {
230 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(exceptionNames[i]);
231 if (!ci.isRegistered()) {
232 ci.registerClass(ti);
235 ar[i] = ci.getClassObjectRef();
238 int aRef = env.newObjectArray("Ljava/lang/Class;", exceptionNames.length);
239 for (int i = 0; i < exceptionNames.length; i++) {
240 env.setReferenceArrayElement(aRef, i, ar[i]);
247 public int getExceptionTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef) {
248 return getExceptionTypes(env, getMethodInfo(env, objRef));
252 public int getDefaultValue____Ljava_lang_Object_2(MJIEnv env, int objRef) {
253 MethodInfo mi = getMethodInfo(env, objRef);
254 ClassInfo ci = mi.getClassInfo();
255 if(!ci.isInterface() || ci.getDirectInterfaceNames() == null || ci.getDirectInterfaceNames().length != 1 || !ci.getDirectInterfaceNames()[0].equals("java.lang.annotation.Annotation")) {
258 String annotationName = ci.getName();
259 AnnotationInfo ai = ci.getClassLoaderInfo().getResolvedAnnotationInfo(annotationName);
260 Object o = ai.getValue(mi.getName());
265 return env.liftNativeAnnotationValue(Types.getTypeName(mi.getReturnType()), o);
266 } catch(ClinitRequired e) {
267 env.handleClinitRequest(e.getRequiredClassInfo());
273 public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){
274 MethodInfo mi = getMethodInfo(env, objRef);
275 ThreadInfo ti = env.getThreadInfo();
277 ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
278 if (!ci.isRegistered()) {
279 ci.registerClass(ti);
282 return ci.getClassObjectRef();
286 public int getDeclaringClass____Ljava_lang_Class_2 (MJIEnv env, int objRef){
287 MethodInfo mi = getMethodInfo(env, objRef);
288 ClassInfo ci = mi.getClassInfo();
289 // it's got to be registered, otherwise we wouldn't be able to acquire the Method object
290 return ci.getClassObjectRef();
293 static int createBoxedReturnValueObject (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame) {
294 byte rt = mi.getReturnTypeCode();
295 int ret = MJIEnv.NULL;
299 if (rt == Types.T_DOUBLE) {
300 attr = frame.getLongResultAttr();
301 double v = frame.getDoubleResult();
302 ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"));
303 rei = env.getModifiableElementInfo(ret);
304 rei.setDoubleField("value", v);
305 } else if (rt == Types.T_FLOAT) {
306 attr = frame.getResultAttr();
307 float v = frame.getFloatResult();
308 ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"));
309 rei = env.getModifiableElementInfo(ret);
310 rei.setFloatField("value", v);
311 } else if (rt == Types.T_LONG) {
312 attr = frame.getLongResultAttr();
313 long v = frame.getLongResult();
314 ret = env.valueOfLong(v);
315 } else if (rt == Types.T_BYTE) {
316 attr = frame.getResultAttr();
317 int v = frame.getResult();
318 ret = env.valueOfByte((byte)v);
319 } else if (rt == Types.T_CHAR) {
320 attr = frame.getResultAttr();
321 int v = frame.getResult();
322 ret = env.valueOfCharacter((char)v);
323 } else if (rt == Types.T_SHORT) {
324 attr = frame.getResultAttr();
325 int v = frame.getResult();
326 ret = env.valueOfShort((short)v);
327 } else if (rt == Types.T_INT) {
328 attr = frame.getResultAttr();
329 int v = frame.getResult();
330 ret = env.valueOfInteger(v);
331 } else if (rt == Types.T_BOOLEAN) {
332 attr = frame.getResultAttr();
333 int v = frame.getResult();
334 ret = env.valueOfBoolean((v == 1)? true: false);
335 } else if (mi.isReferenceReturnType()){
336 attr = frame.getResultAttr();
337 ret = frame.getReferenceResult();
340 env.setReturnAttribute(attr);
344 static boolean pushUnboxedArguments (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame, int argIdx, int argsRef) {
346 ClassInfo sourceClass;
347 String destTypeNames[];
348 int nArgs, passedCount, sourceRef;
349 byte sourceType, destTypes[];
351 destTypes = mi.getArgumentTypes();
352 destTypeNames = mi.getArgumentTypeNames();
353 nArgs = destTypeNames.length;
355 // according to the API docs, passing null instead of an empty array is allowed for no args
356 passedCount = (argsRef != MJIEnv.NULL) ? env.getArrayLength(argsRef) : 0;
358 if (nArgs != passedCount) {
359 env.throwException(IllegalArgumentException.class.getName(), "Wrong number of arguments passed. Actual = " + passedCount + ". Expected = " + nArgs);
363 for (int i = 0; i < nArgs; i++) {
364 sourceRef = env.getReferenceArrayElement(argsRef, i);
366 // we have to handle null references explicitly
367 if (sourceRef == MJIEnv.NULL) {
368 if ((destTypes[i] != Types.T_REFERENCE) && (destTypes[i] != Types.T_ARRAY)) {
369 env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ". Actual = (null). Expected = " + destTypeNames[i]);
373 frame.pushRef(MJIEnv.NULL);
377 source = env.getElementInfo(sourceRef);
378 sourceClass = source.getClassInfo();
379 sourceType = getSourceType( sourceClass, destTypes[i], destTypeNames[i]);
381 Object attr = env.getElementInfo(argsRef).getFields().getFieldAttr(i);
382 if ((argIdx = pushArg( argIdx, frame, source, sourceType, destTypes[i], attr)) < 0 ){
383 env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ". Source Class = " + sourceClass.getName() + ". Dest Class = " + destTypeNames[i]);
391 // this returns the primitive type in case we have to unbox, and otherwise checks reference type compatibility
392 private static byte getSourceType (ClassInfo ciArgVal, byte destType, String destTypeName){
395 case Types.T_BOOLEAN:
403 return Types.getUnboxedType(ciArgVal.getName());
406 case Types.T_REFERENCE: // check if the source type is assignment compatible with the destType
407 if (ciArgVal.isInstanceOf(destTypeName)){
415 // do the proper type conversion - Java is pretty forgiving here and does
416 // not throw exceptions upon value truncation
417 private static int pushArg( int argIdx, DirectCallStackFrame frame, ElementInfo eiArg, byte srcType, byte destType, Object attr){
421 double v = eiArg.getDoubleField("value");
422 if (destType == Types.T_DOUBLE){
423 return frame.setDoubleArgument( argIdx, v, attr);
427 case Types.T_FLOAT: // covers float, double
429 float v = eiArg.getFloatField("value");
432 return frame.setFloatArgument( argIdx, v, attr);
434 return frame.setDoubleArgument( argIdx, v, attr);
440 long v = eiArg.getLongField("value");
443 return frame.setLongArgument(argIdx, v, attr);
445 return frame.setFloatArgument(argIdx, v, attr);
447 return frame.setDoubleArgument( argIdx, v, attr);
453 int v = eiArg.getIntField("value");
456 return frame.setArgument( argIdx, v, attr);
458 return frame.setLongArgument( argIdx, v, attr);
460 return frame.setFloatArgument(argIdx, v, attr);
462 return frame.setDoubleArgument( argIdx, v, attr);
468 int v = eiArg.getShortField("value");
472 return frame.setArgument( argIdx, v, attr);
474 return frame.setLongArgument( argIdx, v, attr);
476 return frame.setFloatArgument(argIdx, v, attr);
478 return frame.setDoubleArgument( argIdx, v, attr);
484 byte v = eiArg.getByteField("value");
489 return frame.setArgument( argIdx, v, attr);
491 return frame.setLongArgument( argIdx, v, attr);
493 return frame.setFloatArgument(argIdx, v, attr);
495 return frame.setDoubleArgument( argIdx, v, attr);
501 char v = eiArg.getCharField("value");
505 return frame.setArgument( argIdx, v, attr);
507 return frame.setLongArgument( argIdx, v, attr);
509 return frame.setFloatArgument(argIdx, v, attr);
511 return frame.setDoubleArgument( argIdx, v, attr);
515 case Types.T_BOOLEAN:
517 boolean v = eiArg.getBooleanField("value");
518 if (destType == Types.T_BOOLEAN){
519 return frame.setArgument( argIdx, v ? 1 : 0, attr);
525 int ref = eiArg.getObjectRef();
526 if (destType == Types.T_ARRAY){
527 return frame.setReferenceArgument( argIdx, ref, attr);
531 case Types.T_REFERENCE:
533 int ref = eiArg.getObjectRef();
534 if (destType == Types.T_REFERENCE){
535 return frame.setReferenceArgument( argIdx, ref, attr);
546 public int invoke__Ljava_lang_Object_2_3Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int mthRef, int objRef, int argsRef) {
547 ThreadInfo ti = env.getThreadInfo();
548 MethodInfo miCallee = getMethodInfo(env, mthRef);
549 ClassInfo calleeClass = miCallee.getClassInfo();
550 DirectCallStackFrame frame = ti.getReturnedDirectCall();
552 if (frame == null){ // first time
554 //--- check the instance we are calling on
555 if (!miCallee.isStatic()) {
556 if (objRef == MJIEnv.NULL){
557 env.throwException("java.lang.NullPointerException");
561 ElementInfo eiObj = ti.getElementInfo(objRef);
562 ClassInfo objClass = eiObj.getClassInfo();
564 if (!objClass.isInstanceOf(calleeClass)) {
565 env.throwException(IllegalArgumentException.class.getName(), "Object is not an instance of declaring class. Actual = " + objClass + ". Expected = " + calleeClass);
571 //--- check accessibility
572 ElementInfo eiMth = ti.getElementInfo(mthRef);
573 if (! (Boolean) eiMth.getFieldValueObject("isAccessible")) {
574 StackFrame caller = ti.getTopFrame().getPrevious();
575 ClassInfo callerClass = caller.getClassInfo();
577 if (callerClass != calleeClass) {
578 env.throwException(IllegalAccessException.class.getName(), "Class " + callerClass.getName() +
579 " can not access a member of class " + calleeClass.getName()
580 + " with modifiers \"" + Modifier.toString(miCallee.getModifiers()));
585 //--- push the direct call
586 frame = miCallee.createDirectCallStackFrame(ti, 0);
587 frame.setReflection();
590 if (!miCallee.isStatic()) {
591 frame.setReferenceArgument( argOffset++, objRef, null);
593 if (!pushUnboxedArguments( env, miCallee, frame, argOffset, argsRef)) {
594 // we've got a IllegalArgumentException
600 //--- check for and push required clinits
601 if (miCallee.isStatic()){
602 calleeClass.initializeClass(ti);
605 return MJIEnv.NULL; // reexecute
607 } else { // we have returned from the direct call
608 return createBoxedReturnValueObject( env, miCallee, frame);
613 // this one has to collect annotations upwards in the inheritance chain
614 static int getAnnotations (MJIEnv env, MethodInfo mi){
615 String mname = mi.getName();
616 String msig = mi.genericSignature;
617 ArrayList<AnnotationInfo> aiList = new ArrayList<AnnotationInfo>();
619 // our own annotations
620 ClassInfo ci = mi.getClassInfo();
621 for (AnnotationInfo ai : mi.getAnnotations()) {
625 // our superclass annotations
626 for (ci = ci.getSuperClass(); ci != null; ci = ci.getSuperClass()){
627 mi = ci.getMethod(mname, msig, false);
629 for (AnnotationInfo ai: mi.getAnnotations()){
636 return env.newAnnotationProxies(aiList.toArray(new AnnotationInfo[aiList.size()]));
637 } catch (ClinitRequired x){
638 env.handleClinitRequest(x.getRequiredClassInfo());
644 public int getAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
645 return getAnnotations( env, getMethodInfo(env,mthRef));
648 // the following ones consist of a package default implementation that is shared with
649 // the constructor peer, and a public model method
650 static int getAnnotation (MJIEnv env, MethodInfo mi, int annotationClsRef){
651 ClassInfo aci = env.getReferredClassInfo(annotationClsRef);
653 AnnotationInfo ai = mi.getAnnotation(aci.getName());
655 ClassInfo aciProxy = aci.getAnnotationProxy();
657 return env.newAnnotationProxy(aciProxy, ai);
658 } catch (ClinitRequired x){
659 env.handleClinitRequest(x.getRequiredClassInfo());
668 public int getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef, int annotationClsRef) {
669 return getAnnotation(env, getMethodInfo(env,mthRef), annotationClsRef);
672 static int getDeclaredAnnotations (MJIEnv env, MethodInfo mi){
673 AnnotationInfo[] ai = mi.getAnnotations();
676 return env.newAnnotationProxies(ai);
677 } catch (ClinitRequired x){
678 env.handleClinitRequest(x.getRequiredClassInfo());
684 public int getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
685 return getDeclaredAnnotations( env, getMethodInfo(env,mthRef));
688 static int getParameterAnnotations (MJIEnv env, MethodInfo mi){
689 AnnotationInfo[][] pa = mi.getParameterAnnotations();
690 // this should always return an array object, even if the method has no arguments
693 int paRef = env.newObjectArray("[Ljava/lang/annotation/Annotation;", pa.length);
695 for (int i=0; i<pa.length; i++){
696 int eRef = env.newAnnotationProxies(pa[i]);
697 env.setReferenceArrayElement(paRef, i, eRef);
702 } catch (ClinitRequired x){ // be prepared that we might have to initialize respective annotation classes
703 env.handleClinitRequest(x.getRequiredClassInfo());
709 public int getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
710 return getParameterAnnotations( env, getMethodInfo(env,mthRef));
714 public int toString____Ljava_lang_String_2 (MJIEnv env, int objRef){
715 StringBuilder sb = new StringBuilder();
717 MethodInfo mi = getMethodInfo(env, objRef);
719 sb.append(Modifier.toString(mi.getModifiers()));
722 sb.append(mi.getReturnTypeName());
725 sb.append(mi.getClassName());
728 sb.append(mi.getName());
732 String[] at = mi.getArgumentTypeNames();
733 for (int i=0; i<at.length; i++){
734 if (i>0) sb.append(',');
740 int sref = env.newString(sb.toString());
745 public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int mthRef){
746 ElementInfo ei = env.getElementInfo(mthRef);
747 ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo(JPF_java_lang_Class.METHOD_CLASSNAME);
749 if (ei.getClassInfo() == ci){
750 MethodInfo mi1 = getMethodInfo(env, objRef);
751 MethodInfo mi2 = getMethodInfo(env, mthRef);
752 if (mi1.getClassInfo() == mi2.getClassInfo()){
753 if (mi1.getName().equals(mi2.getName())){
754 if (mi1.getReturnType().equals(mi2.getReturnType())){
755 byte[] params1 = mi1.getArgumentTypes();
756 byte[] params2 = mi2.getArgumentTypes();
757 if (params1.length == params2.length){
758 for (int i = 0; i < params1.length; i++){
759 if (params1[i] != params2[i]){
773 public int hashCode____I (MJIEnv env, int objRef){
774 MethodInfo mi = getMethodInfo(env, objRef);
775 return mi.getClassName().hashCode() ^ mi.getName().hashCode();