Starting our own version of JPF with support for generics.
[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.Modifier;
27 import java.util.ArrayList;
28
29 public class JPF_java_lang_reflect_Method extends NativePeer {
30
31   static MethodInfoRegistry registry;
32
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
39
40     if (registry == null){
41       registry = new MethodInfoRegistry();
42       
43       RunRegistry.getDefaultRegistry().addListener( new RunListener() {
44         @Override
45                 public void reset (RunRegistry reg){
46           registry = null;
47         }
48       });
49     }
50     return true;
51   }
52
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);
58     
59     ei.setIntField("regIdx", regIdx);
60     ei.setBooleanField("isAccessible", mi.isPublic());
61     
62     return eidx;
63   }
64   
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");
69   }
70   
71   @MJI
72   public int getName____Ljava_lang_String_2 (MJIEnv env, int objRef) {
73     MethodInfo mi = getMethodInfo(env, objRef);
74     
75     int nameRef = env.getReferenceField( objRef, "name");
76     if (nameRef == MJIEnv.NULL) {
77       nameRef = env.newString(mi.getName());
78       env.setReferenceField(objRef, "name", nameRef);
79     }
80    
81     return nameRef;
82   }
83
84   @MJI
85   public int getModifiers____I (MJIEnv env, int objRef){
86     MethodInfo mi = getMethodInfo(env, objRef);
87     return mi.getModifiers();
88   }
89
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];
94
95     for (int i = 0; i < argTypeNames.length; i++) {
96       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(argTypeNames[i]);
97       if (!ci.isRegistered()) {
98         ci.registerClass(ti);
99       }
100
101       ar[i] = ci.getClassObjectRef();
102     }
103
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]);
107     }
108
109     return aRef;
110   }
111
112   @MJI
113   public int getParameterTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef){
114     return getParameterTypes(env, getMethodInfo(env, objRef));
115   }
116
117   // TODO: DIRTY HACKS
118   @MJI
119   public int getGenericParameterTypes_____3Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
120     //return getGenericParameterTypes(env, getMethodInfo(env, objRef));
121     return getParameterTypes_____3Ljava_lang_Class_2 (env, objRef);
122   }
123
124   @MJI
125   public int getGenericReturnType____Ljava_lang_reflect_Type_2 (MJIEnv env, int objRef){
126     return getReturnType____Ljava_lang_Class_2(env, objRef);
127   }
128   // TODO: DIRTY HACKS
129   
130   int getExceptionTypes(MJIEnv env, MethodInfo mi) {
131     ThreadInfo ti = env.getThreadInfo();
132     String[] exceptionNames = mi.getThrownExceptionClassNames();
133      
134     if (exceptionNames == null) {
135       exceptionNames = new String[0];
136     }
137      
138     int[] ar = new int[exceptionNames.length];
139      
140     for (int i = 0; i < exceptionNames.length; i++) {
141       ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(exceptionNames[i]);
142       if (!ci.isRegistered()) {
143         ci.registerClass(ti);
144       }
145        
146       ar[i] = ci.getClassObjectRef();
147     }
148      
149     int aRef = env.newObjectArray("Ljava/lang/Class;", exceptionNames.length);
150     for (int i = 0; i < exceptionNames.length; i++) {
151       env.setReferenceArrayElement(aRef, i, ar[i]);
152     }
153      
154     return aRef;
155   }
156   
157   @MJI
158   public int getExceptionTypes_____3Ljava_lang_Class_2 (MJIEnv env, int objRef) {
159     return getExceptionTypes(env, getMethodInfo(env, objRef));
160   }
161   
162   @MJI
163   public int getDefaultValue____Ljava_lang_Object_2(MJIEnv env, int objRef) {
164     MethodInfo mi = getMethodInfo(env, objRef);
165     ClassInfo ci = mi.getClassInfo();
166     if(!ci.isInterface() || ci.getDirectInterfaceNames() == null || ci.getDirectInterfaceNames().length != 1 || !ci.getDirectInterfaceNames()[0].equals("java.lang.annotation.Annotation")) {
167       return MJIEnv.NULL;
168     }
169     String annotationName = ci.getName();
170     AnnotationInfo ai = ci.getClassLoaderInfo().getResolvedAnnotationInfo(annotationName);
171     Object o = ai.getValue(mi.getName());
172     if(o == null) {
173       return MJIEnv.NULL;
174     }
175     try {
176       return env.liftNativeAnnotationValue(Types.getTypeName(mi.getReturnType()), o);
177     } catch(ClinitRequired e) {
178       env.handleClinitRequest(e.getRequiredClassInfo());
179       return -1;
180     }
181   }
182   
183   @MJI
184   public int getReturnType____Ljava_lang_Class_2 (MJIEnv env, int objRef){
185     MethodInfo mi = getMethodInfo(env, objRef);
186     ThreadInfo ti = env.getThreadInfo();
187
188     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(mi.getReturnTypeName());
189     if (!ci.isRegistered()) {
190       ci.registerClass(ti);
191     }
192
193     return ci.getClassObjectRef();
194   }
195   
196   @MJI
197   public int getDeclaringClass____Ljava_lang_Class_2 (MJIEnv env, int objRef){
198     MethodInfo mi = getMethodInfo(env, objRef);    
199     ClassInfo ci = mi.getClassInfo();
200     // it's got to be registered, otherwise we wouldn't be able to acquire the Method object
201     return ci.getClassObjectRef();
202   }
203     
204   static int createBoxedReturnValueObject (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame) {
205     byte rt = mi.getReturnTypeCode();
206     int ret = MJIEnv.NULL;
207     ElementInfo rei;
208     Object attr = null;
209
210     if (rt == Types.T_DOUBLE) {
211       attr = frame.getLongResultAttr();
212       double v = frame.getDoubleResult();
213       ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Double"));
214       rei = env.getModifiableElementInfo(ret);
215       rei.setDoubleField("value", v);
216     } else if (rt == Types.T_FLOAT) {
217       attr = frame.getResultAttr();
218       float v = frame.getFloatResult();
219       ret = env.newObject(ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.Float"));
220       rei = env.getModifiableElementInfo(ret);
221       rei.setFloatField("value", v);
222     } else if (rt == Types.T_LONG) {
223       attr = frame.getLongResultAttr();
224       long v = frame.getLongResult();
225       ret = env.valueOfLong(v);
226     } else if (rt == Types.T_BYTE) {
227       attr = frame.getResultAttr();
228       int v = frame.getResult(); 
229       ret = env.valueOfByte((byte)v);
230     } else if (rt == Types.T_CHAR) {
231       attr = frame.getResultAttr();
232       int v = frame.getResult(); 
233       ret = env.valueOfCharacter((char)v);
234     } else if (rt == Types.T_SHORT) {
235       attr = frame.getResultAttr();
236       int v = frame.getResult(); 
237       ret = env.valueOfShort((short)v);
238     } else if (rt == Types.T_INT) {
239       attr = frame.getResultAttr();
240       int v = frame.getResult(); 
241       ret = env.valueOfInteger(v);
242     } else if (rt == Types.T_BOOLEAN) {
243       attr = frame.getResultAttr();
244       int v = frame.getResult();
245       ret = env.valueOfBoolean((v == 1)? true: false);
246     } else if (mi.isReferenceReturnType()){ 
247       attr = frame.getResultAttr();
248       ret = frame.getReferenceResult();
249     }
250
251     env.setReturnAttribute(attr);
252     return ret;
253   }
254
255   static boolean pushUnboxedArguments (MJIEnv env, MethodInfo mi, DirectCallStackFrame frame, int argIdx, int argsRef) {
256     ElementInfo source;
257     ClassInfo sourceClass;
258     String destTypeNames[];
259     int nArgs, passedCount, sourceRef;
260     byte sourceType, destTypes[];
261
262     destTypes     = mi.getArgumentTypes();
263     destTypeNames = mi.getArgumentTypeNames();
264     nArgs         = destTypeNames.length;
265     
266     // according to the API docs, passing null instead of an empty array is allowed for no args
267     passedCount   = (argsRef != MJIEnv.NULL) ? env.getArrayLength(argsRef) : 0;
268     
269     if (nArgs != passedCount) {
270       env.throwException(IllegalArgumentException.class.getName(), "Wrong number of arguments passed.  Actual = " + passedCount + ".  Expected = " + nArgs);
271       return false;
272     }
273     
274     for (int i = 0; i < nArgs; i++) {
275       sourceRef = env.getReferenceArrayElement(argsRef, i);
276
277       // we have to handle null references explicitly
278       if (sourceRef == MJIEnv.NULL) {
279         if ((destTypes[i] != Types.T_REFERENCE) && (destTypes[i] != Types.T_ARRAY)) {
280           env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ".  Actual = (null).  Expected = " + destTypeNames[i]);
281           return false;
282         } 
283          
284         frame.pushRef(MJIEnv.NULL);
285         continue;
286       }
287
288       source      = env.getElementInfo(sourceRef);
289       sourceClass = source.getClassInfo();   
290       sourceType = getSourceType( sourceClass, destTypes[i], destTypeNames[i]);
291
292       Object attr = env.getElementInfo(argsRef).getFields().getFieldAttr(i);
293       if ((argIdx = pushArg( argIdx, frame, source, sourceType, destTypes[i], attr)) < 0 ){
294         env.throwException(IllegalArgumentException.class.getName(), "Wrong argument type at index " + i + ".  Source Class = " + sourceClass.getName() + ".  Dest Class = " + destTypeNames[i]);
295         return false;        
296       }
297     }
298     
299     return true;
300   }
301
302   // this returns the primitive type in case we have to unbox, and otherwise checks reference type compatibility
303   private static byte getSourceType (ClassInfo ciArgVal, byte destType, String destTypeName){
304     switch (destType){
305     // the primitives
306     case Types.T_BOOLEAN:
307     case Types.T_BYTE:
308     case Types.T_CHAR:
309     case Types.T_SHORT:
310     case Types.T_INT:
311     case Types.T_LONG:
312     case Types.T_FLOAT:
313     case Types.T_DOUBLE:
314       return Types.getUnboxedType(ciArgVal.getName());
315       
316     case Types.T_ARRAY:
317     case Types.T_REFERENCE: // check if the source type is assignment compatible with the destType
318       if (ciArgVal.isInstanceOf(destTypeName)){
319         return destType;
320       }
321     }
322     
323     return Types.T_NONE;
324   }
325   
326   // do the proper type conversion - Java is pretty forgiving here and does
327   // not throw exceptions upon value truncation
328   private static int pushArg( int argIdx, DirectCallStackFrame frame, ElementInfo eiArg, byte srcType, byte destType, Object attr){    
329     switch (srcType) {
330     case Types.T_DOUBLE:
331     {
332       double v = eiArg.getDoubleField("value");
333       if (destType == Types.T_DOUBLE){
334         return frame.setDoubleArgument( argIdx, v, attr);
335       }
336       return -1;
337     }
338     case Types.T_FLOAT: // covers float, double
339     {
340       float v = eiArg.getFloatField("value");
341       switch (destType){
342       case Types.T_FLOAT:
343         return frame.setFloatArgument( argIdx, v, attr);
344       case Types.T_DOUBLE:
345         return frame.setDoubleArgument( argIdx, v, attr);
346       }
347       return -1;
348     }
349     case Types.T_LONG:
350     {
351       long v = eiArg.getLongField("value");
352       switch (destType){
353       case Types.T_LONG:
354         return frame.setLongArgument(argIdx, v, attr);
355       case Types.T_FLOAT:
356         return frame.setFloatArgument(argIdx, v, attr);
357       case Types.T_DOUBLE:
358         return frame.setDoubleArgument( argIdx, v, attr);
359       }
360       return -1;
361     }
362     case Types.T_INT:
363     { 
364       int v = eiArg.getIntField("value");
365       switch (destType){
366       case Types.T_INT:
367         return frame.setArgument( argIdx, v, attr);
368       case Types.T_LONG:
369         return frame.setLongArgument( argIdx, v, attr);
370       case Types.T_FLOAT:
371         return frame.setFloatArgument(argIdx, v, attr);
372       case Types.T_DOUBLE:
373         return frame.setDoubleArgument( argIdx, v, attr);
374       }
375       return -1;
376     }
377     case Types.T_SHORT:
378     { 
379       int v = eiArg.getShortField("value");
380       switch (destType){
381       case Types.T_SHORT:
382       case Types.T_INT:
383         return frame.setArgument( argIdx, v, attr);
384       case Types.T_LONG:
385         return frame.setLongArgument( argIdx, v, attr);
386       case Types.T_FLOAT:
387         return frame.setFloatArgument(argIdx, v, attr);
388       case Types.T_DOUBLE:
389         return frame.setDoubleArgument( argIdx, v, attr);
390       }
391       return -1;
392     }
393     case Types.T_BYTE:
394     { 
395       byte v = eiArg.getByteField("value");
396       switch (destType){
397       case Types.T_BYTE:
398       case Types.T_SHORT:
399       case Types.T_INT:
400         return frame.setArgument( argIdx, v, attr);
401       case Types.T_LONG:
402         return frame.setLongArgument( argIdx, v, attr);
403       case Types.T_FLOAT:
404         return frame.setFloatArgument(argIdx, v, attr);
405       case Types.T_DOUBLE:
406         return frame.setDoubleArgument( argIdx, v, attr);
407       }
408       return -1;
409     }
410     case Types.T_CHAR:
411     {
412       char v = eiArg.getCharField("value");
413       switch (destType){
414       case Types.T_CHAR:
415       case Types.T_INT:
416         return frame.setArgument( argIdx, v, attr);
417       case Types.T_LONG:
418         return frame.setLongArgument( argIdx, v, attr);
419       case Types.T_FLOAT:
420         return frame.setFloatArgument(argIdx, v, attr);
421       case Types.T_DOUBLE:
422         return frame.setDoubleArgument( argIdx, v, attr);
423       }
424       return -1;
425     }
426     case Types.T_BOOLEAN:
427     {
428       boolean v = eiArg.getBooleanField("value");
429       if (destType == Types.T_BOOLEAN){
430         return frame.setArgument( argIdx, v ? 1 : 0, attr);
431       }
432       return -1;
433     }
434     case Types.T_ARRAY:
435     {
436       int ref =  eiArg.getObjectRef();
437       if (destType == Types.T_ARRAY){
438         return frame.setReferenceArgument( argIdx, ref, attr);
439       }
440       return -1;
441     }
442     case Types.T_REFERENCE:
443     {
444       int ref =  eiArg.getObjectRef();
445       if (destType == Types.T_REFERENCE){
446         return frame.setReferenceArgument( argIdx, ref, attr);
447       }
448       return -1;
449     }
450     default:
451       // T_VOID, T_NONE
452       return -1;
453     }
454   }
455
456   @MJI
457   public int invoke__Ljava_lang_Object_2_3Ljava_lang_Object_2__Ljava_lang_Object_2 (MJIEnv env, int mthRef, int objRef, int argsRef) {
458     ThreadInfo ti = env.getThreadInfo();
459     MethodInfo miCallee = getMethodInfo(env, mthRef);
460     ClassInfo calleeClass = miCallee.getClassInfo();
461     DirectCallStackFrame frame = ti.getReturnedDirectCall();
462     
463     if (frame == null){ // first time
464
465       //--- check the instance we are calling on
466       if (!miCallee.isStatic()) {
467         if (objRef == MJIEnv.NULL){
468           env.throwException("java.lang.NullPointerException");
469           return MJIEnv.NULL;
470           
471         } else {
472           ElementInfo eiObj = ti.getElementInfo(objRef);
473           ClassInfo objClass = eiObj.getClassInfo();
474         
475           if (!objClass.isInstanceOf(calleeClass)) {
476             env.throwException(IllegalArgumentException.class.getName(), "Object is not an instance of declaring class.  Actual = " + objClass + ".  Expected = " + calleeClass);
477             return MJIEnv.NULL;
478           }
479         }
480       }
481
482       //--- check accessibility
483       ElementInfo eiMth = ti.getElementInfo(mthRef);
484       if (! (Boolean) eiMth.getFieldValueObject("isAccessible")) {
485         StackFrame caller = ti.getTopFrame().getPrevious();
486         ClassInfo callerClass = caller.getClassInfo();
487
488         if (callerClass != calleeClass) {
489           env.throwException(IllegalAccessException.class.getName(), "Class " + callerClass.getName() +
490                   " can not access a member of class " + calleeClass.getName()
491                   + " with modifiers \"" + Modifier.toString(miCallee.getModifiers()));
492           return MJIEnv.NULL;
493         }
494       }
495       
496       //--- push the direct call
497       frame = miCallee.createDirectCallStackFrame(ti, 0);
498       frame.setReflection();
499       
500       int argOffset = 0;
501       if (!miCallee.isStatic()) {
502         frame.setReferenceArgument( argOffset++, objRef, null);
503       }
504       if (!pushUnboxedArguments( env, miCallee, frame, argOffset, argsRef)) {
505         // we've got a IllegalArgumentException
506         return MJIEnv.NULL;  
507       }
508       ti.pushFrame(frame);
509       
510       
511       //--- check for and push required clinits
512       if (miCallee.isStatic()){
513         calleeClass.initializeClass(ti);
514       }
515       
516       return MJIEnv.NULL; // reexecute
517       
518     } else { // we have returned from the direct call
519       return createBoxedReturnValueObject( env, miCallee, frame);
520     }
521   }
522   
523
524   // this one has to collect annotations upwards in the inheritance chain
525   static int getAnnotations (MJIEnv env, MethodInfo mi){
526     String mname = mi.getName();
527     String msig = mi.genericSignature;
528     ArrayList<AnnotationInfo> aiList = new ArrayList<AnnotationInfo>();
529     
530     // our own annotations
531     ClassInfo ci = mi.getClassInfo();
532     for (AnnotationInfo ai : mi.getAnnotations()) {
533       aiList.add(ai);
534     }
535     
536     // our superclass annotations
537     for (ci = ci.getSuperClass(); ci != null; ci = ci.getSuperClass()){
538       mi = ci.getMethod(mname, msig, false);
539       if (mi != null){
540         for (AnnotationInfo ai: mi.getAnnotations()){
541           aiList.add(ai);
542         }        
543       }
544     }
545
546     try {
547       return env.newAnnotationProxies(aiList.toArray(new AnnotationInfo[aiList.size()]));
548     } catch (ClinitRequired x){
549       env.handleClinitRequest(x.getRequiredClassInfo());
550       return MJIEnv.NULL;
551     }    
552   }
553
554   @MJI
555   public int getAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
556     return getAnnotations( env, getMethodInfo(env,mthRef));
557   }
558   
559   // the following ones consist of a package default implementation that is shared with
560   // the constructor peer, and a public model method
561   static int getAnnotation (MJIEnv env, MethodInfo mi, int annotationClsRef){
562     ClassInfo aci = env.getReferredClassInfo(annotationClsRef);
563     
564     AnnotationInfo ai = mi.getAnnotation(aci.getName());
565     if (ai != null){
566       ClassInfo aciProxy = aci.getAnnotationProxy();
567       try {
568         return env.newAnnotationProxy(aciProxy, ai);
569       } catch (ClinitRequired x){
570         env.handleClinitRequest(x.getRequiredClassInfo());
571         return MJIEnv.NULL;
572       }
573     }
574     
575     return MJIEnv.NULL;
576   }  
577
578   @MJI
579   public int getAnnotation__Ljava_lang_Class_2__Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef, int annotationClsRef) {
580     return getAnnotation(env, getMethodInfo(env,mthRef), annotationClsRef);
581   }
582   
583   static int getDeclaredAnnotations (MJIEnv env, MethodInfo mi){
584     AnnotationInfo[] ai = mi.getAnnotations();
585
586     try {
587       return env.newAnnotationProxies(ai);
588     } catch (ClinitRequired x){
589       env.handleClinitRequest(x.getRequiredClassInfo());
590       return MJIEnv.NULL;
591     }    
592   }
593
594   @MJI
595   public int getDeclaredAnnotations_____3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
596     return getDeclaredAnnotations( env, getMethodInfo(env,mthRef));
597   }
598   
599   static int getParameterAnnotations (MJIEnv env, MethodInfo mi){
600     AnnotationInfo[][] pa = mi.getParameterAnnotations();
601     // this should always return an array object, even if the method has no arguments
602     
603     try {
604       int paRef = env.newObjectArray("[Ljava/lang/annotation/Annotation;", pa.length);
605       
606       for (int i=0; i<pa.length; i++){
607         int eRef = env.newAnnotationProxies(pa[i]);
608         env.setReferenceArrayElement(paRef, i, eRef);
609       }
610
611       return paRef;
612       
613     } catch (ClinitRequired x){ // be prepared that we might have to initialize respective annotation classes
614       env.handleClinitRequest(x.getRequiredClassInfo());
615       return MJIEnv.NULL;
616     }    
617   }
618
619   @MJI
620   public int getParameterAnnotations_____3_3Ljava_lang_annotation_Annotation_2 (MJIEnv env, int mthRef){
621     return getParameterAnnotations( env, getMethodInfo(env,mthRef));
622   }
623
624   @MJI
625   public int toString____Ljava_lang_String_2 (MJIEnv env, int objRef){
626     StringBuilder sb = new StringBuilder();
627     
628     MethodInfo mi = getMethodInfo(env, objRef);
629
630     sb.append(Modifier.toString(mi.getModifiers()));
631     sb.append(' ');
632
633     sb.append(mi.getReturnTypeName());
634     sb.append(' ');
635
636     sb.append(mi.getClassName());
637     sb.append('.');
638
639     sb.append(mi.getName());
640
641     sb.append('(');
642     
643     String[] at = mi.getArgumentTypeNames();
644     for (int i=0; i<at.length; i++){
645       if (i>0) sb.append(',');
646       sb.append(at[i]);
647     }
648     
649     sb.append(')');
650     
651     int sref = env.newString(sb.toString());
652     return sref;
653   }
654
655   @MJI
656   public boolean equals__Ljava_lang_Object_2__Z (MJIEnv env, int objRef, int mthRef){
657     ElementInfo ei = env.getElementInfo(mthRef);
658     ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo(JPF_java_lang_Class.METHOD_CLASSNAME);
659
660     if (ei.getClassInfo() == ci){
661       MethodInfo mi1 = getMethodInfo(env, objRef);
662       MethodInfo mi2 = getMethodInfo(env, mthRef);
663       if (mi1.getClassInfo() == mi2.getClassInfo()){
664         if (mi1.getName().equals(mi2.getName())){
665           if (mi1.getReturnType().equals(mi2.getReturnType())){
666             byte[] params1 = mi1.getArgumentTypes();
667             byte[] params2 = mi2.getArgumentTypes();
668             if (params1.length == params2.length){
669               for (int i = 0; i < params1.length; i++){
670                 if (params1[i] != params2[i]){
671                   return false;
672                 }
673               }
674               return true;
675             }
676           }
677         }
678       }
679     }
680     return false;
681   }
682
683   @MJI
684   public int hashCode____I (MJIEnv env, int objRef){
685     MethodInfo mi = getMethodInfo(env, objRef);
686     return mi.getClassName().hashCode() ^ mi.getName().hashCode();
687   }
688 }