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