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