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   @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: Fix for Groovy's model-checking
 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 }