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