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