48aff581d0190cdbb6152425a8013b8fb2252d1d
[jpf-core.git] / src / peers / gov / nasa / jpf / vm / JPF_java_lang_reflect_Method.java
1 /*
2  * Copyright (C) 2014, United States Government, as represented by the
3  * Administrator of the National Aeronautics and Space Administration.
4  * All rights reserved.
5  *
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
9  * 
10  *        http://www.apache.org/licenses/LICENSE-2.0. 
11  *
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.
17  */
18 package gov.nasa.jpf.vm;
19
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;
25
26 import java.lang.reflect.Method;
27 import java.lang.reflect.Modifier;
28 import java.util.ArrayList;
29
30 public class JPF_java_lang_reflect_Method extends NativePeer {
31
32   static MethodInfoRegistry registry;
33
34   // class init - this is called automatically from the NativePeer ctor
35   public static boolean init (Config conf) {
36     // this is an example of how to handle cross-initialization between
37     // native peers - this might also get explicitly called by the java.lang.Class
38     // peer, since it creates Method objects. Here we have to make sure
39     // we only reset between JPF runs
40
41     if (registry == null){
42       registry = new MethodInfoRegistry();
43       
44       RunRegistry.getDefaultRegistry().addListener( new RunListener() {
45         @Override
46                 public void reset (RunRegistry reg){
47           registry = null;
48         }
49       });
50     }
51     return true;
52   }
53
54   static int createMethodObject (MJIEnv env, ClassInfo ciMth, MethodInfo mi){
55     // note - it is the callers responsibility to ensure Method is properly initialized    
56     int regIdx = registry.registerMethodInfo(mi);
57     int eidx = env.newObject( ciMth);
58     ElementInfo ei = env.getModifiableElementInfo(eidx);
59     
60     ei.setIntField("regIdx", regIdx);
61     ei.setBooleanField("isAccessible", mi.isPublic());
62     
63     return eidx;
64   }
65   
66   // this is NOT an MJI method, but it is used outside this package, so
67   // we have to add 'final'
68   public static final MethodInfo getMethodInfo (MJIEnv env, int objRef){
69     return registry.getMethodInfo(env,objRef, "regIdx");
70   }
71   
72   @MJI
73   public int getName____Ljava_lang_String_2 (MJIEnv env, int objRef) {
74     MethodInfo mi = getMethodInfo(env, objRef);
75     
76     int nameRef = env.getReferenceField( objRef, "name");
77     if (nameRef == MJIEnv.NULL) {
78       nameRef = env.newString(mi.getName());
79       env.setReferenceField(objRef, "name", nameRef);
80     }
81    
82     return nameRef;
83   }
84
85   @MJI
86   public int getModifiers____I (MJIEnv env, int objRef){
87     MethodInfo mi = getMethodInfo(env, objRef);
88     return mi.getModifiers();
89   }
90
91   static int getParameterTypes( MJIEnv env, MethodInfo mi) {
92     ThreadInfo ti = env.getThreadInfo();
93     String[] argTypeNames = mi.getArgumentTypeNames();
94     int[] ar = new int[argTypeNames.length];
95
96     for (int i = 0; i < argTypeNames.length; i++) {
97       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
98       if (!ci.isRegistered()) {
99         ci.registerClass(ti);
100       }
101
102       ar[i] = ci.getClassObjectRef();
103     }
104
105     int aRef = env.newObjectArray("Ljava/lang/Class;", argTypeNames.length);
106     for (int i = 0; i < argTypeNames.length; i++) {
107       env.setReferenceArrayElement(aRef, i, ar[i]);
108     }
109
110     return aRef;
111   }
112
113   @MJI
114   public int getParameterTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef){
115     return getParameterTypes(env, getMethodInfo(env, objRef));
116   }
117
118   // TODO: Fix for Groovy's model-checking
119   private static int getParameterizedTypeImplObj(String signature, MJIEnv env, int objRef, MethodInfo mi) {
120
121     ThreadInfo ti = env.getThreadInfo();
122     ClassLoaderInfo cli = env.getSystemClassLoaderInfo();
123     ClassInfo ci = cli.getResolvedClassInfo("sun.reflect.generics.reflectiveObjects.ParameterizedTypeImpl");
124     // Create a new object of type ParameterizedTypeImpl
125     int paramTypeRef = env.newObject(ci);
126     ElementInfo ei = env.getModifiableElementInfo(paramTypeRef);
127     // Get field information and fill out the fields
128     // rawType field
129     String className = Types.getGenericClassName(signature);
130     ClassInfo gci = cli.getResolvedClassInfo(className);
131     if (!gci.isRegistered()) {
132         gci.registerClass(ti);
133     }
134     ei.setReferenceField("rawType", gci.getClassObjectRef());
135
136     // actualTypeArguments
137     String[] parameterizedTypes = Types.getParameterizedTypes(signature);
138     int[] types = new int[parameterizedTypes.length];
139     String classGenericSig = mi.getClassInfo().getGenericSignature();
140     String methodGenericSig = mi.getGenericSignature();
141     for(int j = 0; j < parameterizedTypes.length; j++) {
142       if (Types.isTypeParameter(parameterizedTypes[j], methodGenericSig) ||
143           Types.isTypeParameter(parameterizedTypes[j], classGenericSig)) {
144         types[j] = getTypeVariableImplObject(env, objRef, mi, parameterizedTypes[j]);
145       } else {
146         ClassInfo pci = cli.getResolvedClassInfo(parameterizedTypes[j]);
147         if (!pci.isRegistered()) {
148           pci.registerClass(ti);
149         }
150         types[j] = pci.getClassObjectRef();
151       }
152     }
153     int aRef = env.newObjectArray("Ljava/lang/reflect/Type;", parameterizedTypes.length);
154     // Set references for every array element
155     for (int j = 0; j < parameterizedTypes.length; j++) {
156       env.setReferenceArrayElement(aRef, j, types[j]);
157     }
158     ei.setReferenceField("actualTypeArguments", aRef);
159
160     // ownerType
161     String ownerType = Types.getOwnerClassName(signature);
162     if (ownerType != null) {
163       ClassInfo oci = ClassLoaderInfo.getCurrentResolvedClassInfo(ownerType);
164       if (!oci.isRegistered()) {
165         oci.registerClass(ti);
166       }
167       ei.setReferenceField("ownerType", oci.getClassObjectRef());
168     } else {
169       ei.setReferenceField("ownerType", MJIEnv.NULL);
170     }
171
172     return paramTypeRef;
173   }
174
175   private static int getTypeVariableImplObject(MJIEnv env, int objRef, MethodInfo mi, String parameterizedType) {
176
177     ClassLoaderInfo cli = env.getSystemClassLoaderInfo();
178     ClassInfo ci = cli.getResolvedClassInfo("sun.reflect.generics.reflectiveObjects.TypeVariableImpl");
179
180     int typeVarRef = env.newObject(ci);
181     ElementInfo ei = env.getModifiableElementInfo(typeVarRef);
182     // genericDeclaration contains this java.lang.reflect.Method object
183     ei.setReferenceField("genericDeclaration", objRef);
184     ei.setReferenceField("name", env.newString(parameterizedType));
185
186     return typeVarRef;
187   }
188
189   static int getGenericParameterTypes( MJIEnv env, int objRef, MethodInfo mi) {
190     ThreadInfo ti = env.getThreadInfo();
191     String[] argTypeNames = mi.getArgumentGenericTypeNames();
192     int[] ar = new int[argTypeNames.length];
193
194     for (int i = 0; i < argTypeNames.length; i++) {
195       // Change this into just the generic class type if it is a generic class
196       if (Types.isGenericSignature(argTypeNames[i])) {
197         ar[i] = getParameterizedTypeImplObj(argTypeNames[i], env, objRef, mi);
198       } else {
199         ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
200         if (!ci.isRegistered()) {
201           ci.registerClass(ti);
202         }
203         ar[i] = ci.getClassObjectRef();
204       }
205     }
206     int aRef = env.newObjectArray("Ljava/lang/reflect/Type;", argTypeNames.length);
207     for (int i = 0; i < argTypeNames.length; i++) {
208       env.setReferenceArrayElement(aRef, i, ar[i]);
209     }
210
211     return aRef;
212   }
213
214   @MJI
215   public int getGenericParameterTypes_____3Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
216     return getGenericParameterTypes(env, objRef, getMethodInfo(env, objRef));
217   }
218
219   @MJI
220   public int getGenericReturnType____Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
221     MethodInfo mi = getMethodInfo(env, objRef);
222     ThreadInfo ti = env.getThreadInfo();
223
224     int retRef;
225     if (Types.isGenericSignature(mi.getGenericReturnTypeName())) {
226       retRef = getParameterizedTypeImplObj(mi.getGenericReturnTypeName(), env, objRef, mi);
227     } else {
228       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
229       if (!ci.isRegistered()) {
230         ci.registerClass(ti);
231       }
232       retRef = ci.getClassObjectRef();
233     }
234
235     return retRef;
236   }
237   // TODO: Fix for Groovy's model-checking
238   // TODO: We have been able to only register the generic class and not yet the parameterized types
239
240   int getExceptionTypes(MJIEnv env, MethodInfo mi) {
241     ThreadInfo ti = env.getThreadInfo();
242     String[] exceptionNames = mi.getThrownExceptionClassNames();
243      
244     if (exceptionNames == null) {
245       exceptionNames = new String[0];
246     }
247      
248     int[] ar = new int[exceptionNames.length];
249      
250     for (int i = 0; i < exceptionNames.length; i++) {
251       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(exceptionNames[i]);
252       if (!ci.isRegistered()) {
253         ci.registerClass(ti);
254       }
255        
256       ar[i] = ci.getClassObjectRef();
257     }
258      
259     int aRef = env.newObjectArray("Ljava/lang/Class;", exceptionNames.length);
260     for (int i = 0; i < exceptionNames.length; i++) {
261       env.setReferenceArrayElement(aRef, i, ar[i]);
262     }
263      
264     return aRef;
265   }
266   
267   @MJI
268   public int getExceptionTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef) {
269     return getExceptionTypes(env, getMethodInfo(env, objRef));
270   }
271   
272   @MJI
273   public int getDefaultValue____Ljava_lang_Object_2(MJIEnv env, int objRef) {
274     MethodInfo mi = getMethodInfo(env, objRef);
275     ClassInfo ci = mi.getClassInfo();
276     if(!ci.isInterface() || ci.getDirectInterfaceNames() == null || ci.getDirectInterfaceNames().length != 1 || !ci.getDirectInterfaceNames()[0].equals("java.lang.annotation.Annotation")) {
277       return MJIEnv.NULL;
278     }
279     String annotationName = ci.getName();
280     AnnotationInfo ai = ci.getClassLoaderInfo().getResolvedAnnotationInfo(annotationName);
281     Object o = ai.getValue(mi.getName());
282     if(o == null) {
283       return MJIEnv.NULL;
284     }
285     try {
286       return env.liftNativeAnnotationValue(Types.getTypeName(mi.getReturnType()), o);
287     } catch(ClinitRequired e) {
288       env.handleClinitRequest(e.getRequiredClassInfo());
289       return -1;
290     }
291   }
292   
293   @MJI
294   public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){
295     MethodInfo mi = getMethodInfo(env, objRef);
296     ThreadInfo ti = env.getThreadInfo();
297
298     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
299     if (!ci.isRegistered()) {
300       ci.registerClass(ti);
301     }
302
303     return ci.getClassObjectRef();
304   }
305   
306   @MJI
307   public int getDeclaringClass____Ljava_lang_Class_2 (MJIEnv env, int objRef){
308     MethodInfo mi = getMethodInfo(env, objRef);    
309     ClassInfo ci = mi.getClassInfo();
310     // it's got to be registered, otherwise we wouldn't be able to acquire the Method object
311     return ci.getClassObjectRef();
312   }
313     
314   static int createBoxedReturnValueObject (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame) {
315     byte rt = mi.getReturnTypeCode();
316     int ret = MJIEnv.NULL;
317     ElementInfo rei;
318     Object attr = null;
319
320     if (rt == Types.T_DOUBLE) {
321       attr = frame.getLongResultAttr();
322       double v = frame.getDoubleResult();
323       ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"));
324       rei = env.getModifiableElementInfo(ret);
325       rei.setDoubleField("value", v);
326     } else if (rt == Types.T_FLOAT) {
327       attr = frame.getResultAttr();
328       float v = frame.getFloatResult();
329       ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"));
330       rei = env.getModifiableElementInfo(ret);
331       rei.setFloatField("value", v);
332     } else if (rt == Types.T_LONG) {
333       attr = frame.getLongResultAttr();
334       long v = frame.getLongResult();
335       ret = env.valueOfLong(v);
336     } else if (rt == Types.T_BYTE) {
337       attr = frame.getResultAttr();
338       int v = frame.getResult(); 
339       ret = env.valueOfByte((byte)v);
340     } else if (rt == Types.T_CHAR) {
341       attr = frame.getResultAttr();
342       int v = frame.getResult(); 
343       ret = env.valueOfCharacter((char)v);
344     } else if (rt == Types.T_SHORT) {
345       attr = frame.getResultAttr();
346       int v = frame.getResult(); 
347       ret = env.valueOfShort((short)v);
348     } else if (rt == Types.T_INT) {
349       attr = frame.getResultAttr();
350       int v = frame.getResult(); 
351       ret = env.valueOfInteger(v);
352     } else if (rt == Types.T_BOOLEAN) {
353       attr = frame.getResultAttr();
354       int v = frame.getResult();
355       ret = env.valueOfBoolean((v == 1)? true: false);
356     } else if (mi.isReferenceReturnType()){ 
357       attr = frame.getResultAttr();
358       ret = frame.getReferenceResult();
359     }
360
361     env.setReturnAttribute(attr);
362     return ret;
363   }
364
365   static boolean pushUnboxedArguments (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame, int argIdx, int argsRef) {
366     ElementInfo source;
367     ClassInfo sourceClass;
368     String destTypeNames[];
369     int nArgs, passedCount, sourceRef;
370     byte sourceType, destTypes[];
371
372     destTypes     = mi.getArgumentTypes();
373     destTypeNames = mi.getArgumentTypeNames();
374     nArgs         = destTypeNames.length;
375     
376     // according to the API docs, passing null instead of an empty array is allowed for no args
377     passedCount   = (argsRef != MJIEnv.NULL) ? env.getArrayLength(argsRef) : 0;
378     
379     if (nArgs != passedCount) {
380       env.throwException(IllegalArgumentException.class.getName(), "Wrong number of arguments passed.  Actual = " + passedCount + ".  Expected = " + nArgs);
381       return false;
382     }
383     
384     for (int i = 0; i < nArgs; i++) {
385       sourceRef = env.getReferenceArrayElement(argsRef, i);
386
387       // we have to handle null references explicitly
388       if (sourceRef == MJIEnv.NULL) {
389         if ((destTypes[i] != Types.T_REFERENCE) && (destTypes[i] != Types.T_ARRAY)) {
390           env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ".  Actual = (null).  Expected = " + destTypeNames[i]);
391           return false;
392         } 
393          
394         frame.pushRef(MJIEnv.NULL);
395         continue;
396       }
397
398       source      = env.getElementInfo(sourceRef);
399       sourceClass = source.getClassInfo();   
400       sourceType = getSourceType( sourceClass, destTypes[i], destTypeNames[i]);
401
402       Object attr = env.getElementInfo(argsRef).getFields().getFieldAttr(i);
403       if ((argIdx = pushArg( argIdx, frame, source, sourceType, destTypes[i], attr)) < 0 ){
404         env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ".  Source Class = " + sourceClass.getName() + ".  Dest Class = " + destTypeNames[i]);
405         return false;        
406       }
407     }
408     
409     return true;
410   }
411
412   // this returns the primitive type in case we have to unbox, and otherwise checks reference type compatibility
413   private static byte getSourceType (ClassInfo ciArgVal, byte destType, String destTypeName){
414     switch (destType){
415     // the primitives
416     case Types.T_BOOLEAN:
417     case Types.T_BYTE:
418     case Types.T_CHAR:
419     case Types.T_SHORT:
420     case Types.T_INT:
421     case Types.T_LONG:
422     case Types.T_FLOAT:
423     case Types.T_DOUBLE:
424       return Types.getUnboxedType(ciArgVal.getName());
425       
426     case Types.T_ARRAY:
427     case Types.T_REFERENCE: // check if the source type is assignment compatible with the destType
428       if (ciArgVal.isInstanceOf(destTypeName)){
429         return destType;
430       }
431     }
432     
433     return Types.T_NONE;
434   }
435   
436   // do the proper type conversion - Java is pretty forgiving here and does
437   // not throw exceptions upon value truncation
438   private static int pushArg( int argIdx, DirectCallStackFrame frame, ElementInfo eiArg, byte srcType, byte destType, Object attr){    
439     switch (srcType) {
440     case Types.T_DOUBLE:
441     {
442       double v = eiArg.getDoubleField("value");
443       if (destType == Types.T_DOUBLE){
444         return frame.setDoubleArgument( argIdx, v, attr);
445       }
446       return -1;
447     }
448     case Types.T_FLOAT: // covers float, double
449     {
450       float v = eiArg.getFloatField("value");
451       switch (destType){
452       case Types.T_FLOAT:
453         return frame.setFloatArgument( argIdx, v, attr);
454       case Types.T_DOUBLE:
455         return frame.setDoubleArgument( argIdx, v, attr);
456       }
457       return -1;
458     }
459     case Types.T_LONG:
460     {
461       long v = eiArg.getLongField("value");
462       switch (destType){
463       case Types.T_LONG:
464         return frame.setLongArgument(argIdx, v, attr);
465       case Types.T_FLOAT:
466         return frame.setFloatArgument(argIdx, v, attr);
467       case Types.T_DOUBLE:
468         return frame.setDoubleArgument( argIdx, v, attr);
469       }
470       return -1;
471     }
472     case Types.T_INT:
473     { 
474       int v = eiArg.getIntField("value");
475       switch (destType){
476       case Types.T_INT:
477         return frame.setArgument( argIdx, v, attr);
478       case Types.T_LONG:
479         return frame.setLongArgument( argIdx, v, attr);
480       case Types.T_FLOAT:
481         return frame.setFloatArgument(argIdx, v, attr);
482       case Types.T_DOUBLE:
483         return frame.setDoubleArgument( argIdx, v, attr);
484       }
485       return -1;
486     }
487     case Types.T_SHORT:
488     { 
489       int v = eiArg.getShortField("value");
490       switch (destType){
491       case Types.T_SHORT:
492       case Types.T_INT:
493         return frame.setArgument( argIdx, v, attr);
494       case Types.T_LONG:
495         return frame.setLongArgument( argIdx, v, attr);
496       case Types.T_FLOAT:
497         return frame.setFloatArgument(argIdx, v, attr);
498       case Types.T_DOUBLE:
499         return frame.setDoubleArgument( argIdx, v, attr);
500       }
501       return -1;
502     }
503     case Types.T_BYTE:
504     { 
505       byte v = eiArg.getByteField("value");
506       switch (destType){
507       case Types.T_BYTE:
508       case Types.T_SHORT:
509       case Types.T_INT:
510         return frame.setArgument( argIdx, v, attr);
511       case Types.T_LONG:
512         return frame.setLongArgument( argIdx, v, attr);
513       case Types.T_FLOAT:
514         return frame.setFloatArgument(argIdx, v, attr);
515       case Types.T_DOUBLE:
516         return frame.setDoubleArgument( argIdx, v, attr);
517       }
518       return -1;
519     }
520     case Types.T_CHAR:
521     {
522       char v = eiArg.getCharField("value");
523       switch (destType){
524       case Types.T_CHAR:
525       case Types.T_INT:
526         return frame.setArgument( argIdx, v, attr);
527       case Types.T_LONG:
528         return frame.setLongArgument( argIdx, v, attr);
529       case Types.T_FLOAT:
530         return frame.setFloatArgument(argIdx, v, attr);
531       case Types.T_DOUBLE:
532         return frame.setDoubleArgument( argIdx, v, attr);
533       }
534       return -1;
535     }
536     case Types.T_BOOLEAN:
537     {
538       boolean v = eiArg.getBooleanField("value");
539       if (destType == Types.T_BOOLEAN){
540         return frame.setArgument( argIdx, v ? 1 : 0, attr);
541       }
542       return -1;
543     }
544     case Types.T_ARRAY:
545     {
546       int ref =  eiArg.getObjectRef();
547       if (destType == Types.T_ARRAY){
548         return frame.setReferenceArgument( argIdx, ref, attr);
549       }
550       return -1;
551     }
552     case Types.T_REFERENCE:
553     {
554       int ref =  eiArg.getObjectRef();
555       if (destType == Types.T_REFERENCE){
556         return frame.setReferenceArgument( argIdx, ref, attr);
557       }
558       return -1;
559     }
560     default:
561       // T_VOID, T_NONE
562       return -1;
563     }
564   }
565
566   @MJI
567   public int invoke__Ljava_lang_Object_2_3Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int mthRef, int objRef, int argsRef) {
568     ThreadInfo ti = env.getThreadInfo();
569     MethodInfo miCallee = getMethodInfo(env, mthRef);
570     ClassInfo calleeClass = miCallee.getClassInfo();
571     DirectCallStackFrame frame = ti.getReturnedDirectCall();
572     
573     if (frame == null){ // first time
574
575       //--- check the instance we are calling on
576       if (!miCallee.isStatic()) {
577         if (objRef == MJIEnv.NULL){
578           env.throwException("java.lang.NullPointerException");
579           return MJIEnv.NULL;
580           
581         } else {
582           ElementInfo eiObj = ti.getElementInfo(objRef);
583           ClassInfo objClass = eiObj.getClassInfo();
584         
585           if (!objClass.isInstanceOf(calleeClass)) {
586             env.throwException(IllegalArgumentException.class.getName(), "Object is not an instance of declaring class.  Actual = " + objClass + ".  Expected = " + calleeClass);
587             return MJIEnv.NULL;
588           }
589         }
590       }
591
592       //--- check accessibility
593       ElementInfo eiMth = ti.getElementInfo(mthRef);
594       if (! (Boolean) eiMth.getFieldValueObject("isAccessible")) {
595         StackFrame caller = ti.getTopFrame().getPrevious();
596         ClassInfo callerClass = caller.getClassInfo();
597
598         if (callerClass != calleeClass) {
599           env.throwException(IllegalAccessException.class.getName(), "Class " + callerClass.getName() +
600                   " can not access a member of class " + calleeClass.getName()
601                   + " with modifiers \"" + Modifier.toString(miCallee.getModifiers()));
602           return MJIEnv.NULL;
603         }
604       }
605       
606       //--- push the direct call
607       frame = miCallee.createDirectCallStackFrame(ti, 0);
608       frame.setReflection();
609       
610       int argOffset = 0;
611       if (!miCallee.isStatic()) {
612         frame.setReferenceArgument( argOffset++, objRef, null);
613       }
614       if (!pushUnboxedArguments( env, miCallee, frame, argOffset, argsRef)) {
615         // we've got a IllegalArgumentException
616         return MJIEnv.NULL;  
617       }
618       ti.pushFrame(frame);
619       
620       
621       //--- check for and push required clinits
622       if (miCallee.isStatic()){
623         calleeClass.initializeClass(ti);
624       }
625       
626       return MJIEnv.NULL; // reexecute
627       
628     } else { // we have returned from the direct call
629       return createBoxedReturnValueObject( env, miCallee, frame);
630     }
631   }
632   
633
634   // this one has to collect annotations upwards in the inheritance chain
635   static int getAnnotations (MJIEnv env, MethodInfo mi){
636     String mname = mi.getName();
637     String msig = mi.genericSignature;
638     ArrayList<AnnotationInfo> aiList = new ArrayList<AnnotationInfo>();
639     
640     // our own annotations
641     ClassInfo ci = mi.getClassInfo();
642     for (AnnotationInfo ai : mi.getAnnotations()) {
643       aiList.add(ai);
644     }
645     
646     // our superclass annotations
647     for (ci = ci.getSuperClass(); ci != null; ci = ci.getSuperClass()){
648       mi = ci.getMethod(mname, msig, false);
649       if (mi != null){
650         for (AnnotationInfo ai: mi.getAnnotations()){
651           aiList.add(ai);
652         }        
653       }
654     }
655
656     try {
657       return env.newAnnotationProxies(aiList.toArray(new AnnotationInfo[aiList.size()]));
658     } catch (ClinitRequired x){
659       env.handleClinitRequest(x.getRequiredClassInfo());
660       return MJIEnv.NULL;
661     }    
662   }
663
664   @MJI
665   public int getAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
666     return getAnnotations( env, getMethodInfo(env,mthRef));
667   }
668   
669   // the following ones consist of a package default implementation that is shared with
670   // the constructor peer, and a public model method
671   static int getAnnotation (MJIEnv env, MethodInfo mi, int annotationClsRef){
672     ClassInfo aci = env.getReferredClassInfo(annotationClsRef);
673     
674     AnnotationInfo ai = mi.getAnnotation(aci.getName());
675     if (ai != null){
676       ClassInfo aciProxy = aci.getAnnotationProxy();
677       try {
678         return env.newAnnotationProxy(aciProxy, ai);
679       } catch (ClinitRequired x){
680         env.handleClinitRequest(x.getRequiredClassInfo());
681         return MJIEnv.NULL;
682       }
683     }
684     
685     return MJIEnv.NULL;
686   }  
687
688   @MJI
689   public int getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef, int annotationClsRef) {
690     return getAnnotation(env, getMethodInfo(env,mthRef), annotationClsRef);
691   }
692   
693   static int getDeclaredAnnotations (MJIEnv env, MethodInfo mi){
694     AnnotationInfo[] ai = mi.getAnnotations();
695
696     try {
697       return env.newAnnotationProxies(ai);
698     } catch (ClinitRequired x){
699       env.handleClinitRequest(x.getRequiredClassInfo());
700       return MJIEnv.NULL;
701     }    
702   }
703
704   @MJI
705   public int getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
706     return getDeclaredAnnotations( env, getMethodInfo(env,mthRef));
707   }
708   
709   static int getParameterAnnotations (MJIEnv env, MethodInfo mi){
710     AnnotationInfo[][] pa = mi.getParameterAnnotations();
711     // this should always return an array object, even if the method has no arguments
712     
713     try {
714       int paRef = env.newObjectArray("[Ljava/lang/annotation/Annotation;", pa.length);
715       
716       for (int i=0; i<pa.length; i++){
717         int eRef = env.newAnnotationProxies(pa[i]);
718         env.setReferenceArrayElement(paRef, i, eRef);
719       }
720
721       return paRef;
722       
723     } catch (ClinitRequired x){ // be prepared that we might have to initialize respective annotation classes
724       env.handleClinitRequest(x.getRequiredClassInfo());
725       return MJIEnv.NULL;
726     }    
727   }
728
729   @MJI
730   public int getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
731     return getParameterAnnotations( env, getMethodInfo(env,mthRef));
732   }
733
734   @MJI
735   public int toString____Ljava_lang_String_2 (MJIEnv env, int objRef){
736     StringBuilder sb = new StringBuilder();
737     
738     MethodInfo mi = getMethodInfo(env, objRef);
739
740     sb.append(Modifier.toString(mi.getModifiers()));
741     sb.append(' ');
742
743     sb.append(mi.getReturnTypeName());
744     sb.append(' ');
745
746     sb.append(mi.getClassName());
747     sb.append('.');
748
749     sb.append(mi.getName());
750
751     sb.append('(');
752     
753     String[] at = mi.getArgumentTypeNames();
754     for (int i=0; i<at.length; i++){
755       if (i>0) sb.append(',');
756       sb.append(at[i]);
757     }
758     
759     sb.append(')');
760     
761     int sref = env.newString(sb.toString());
762     return sref;
763   }
764
765   @MJI
766   public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int mthRef){
767     ElementInfo ei = env.getElementInfo(mthRef);
768     ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo(JPF_java_lang_Class.METHOD_CLASSNAME);
769
770     if (ei.getClassInfo() == ci){
771       MethodInfo mi1 = getMethodInfo(env, objRef);
772       MethodInfo mi2 = getMethodInfo(env, mthRef);
773       if (mi1.getClassInfo() == mi2.getClassInfo()){
774         if (mi1.getName().equals(mi2.getName())){
775           if (mi1.getReturnType().equals(mi2.getReturnType())){
776             byte[] params1 = mi1.getArgumentTypes();
777             byte[] params2 = mi2.getArgumentTypes();
778             if (params1.length == params2.length){
779               for (int i = 0; i < params1.length; i++){
780                 if (params1[i] != params2[i]){
781                   return false;
782                 }
783               }
784               return true;
785             }
786           }
787         }
788       }
789     }
790     return false;
791   }
792
793   @MJI
794   public int hashCode____I (MJIEnv env, int objRef){
795     MethodInfo mi = getMethodInfo(env, objRef);
796     return mi.getClassName().hashCode() ^ mi.getName().hashCode();
797   }
798 }