src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_AnnotationProxyBase.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
  19 package gov.nasa.jpf.vm;
  20
  21 import java.util.Arrays;
  22 import java.util.Objects;
  23 import java.util.function.IntFunction;
  24
  25 import gov.nasa.jpf.annotation.MJI;
  26
  27 /**
  28  * native peer for Annotation Proxies
  29  * (saves us some bytecode interpretation shoe leather)
  30  */
  31 public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer {
  32
  33   @MJI
  34   public int annotationType____Ljava_lang_Class_2 (MJIEnv env, int objref) {
  35     ClassInfo ciProxy = env.getClassInfo(objref);  // this would be the proxy
  36
  37     // we could also pull it out from the interfaces, but we know the naming scheme
  38     String proxyName = ciProxy.getName();
  39     String annotation = proxyName.substring(0, proxyName.length() - 6); // "...$Proxy"
  40     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(annotation);
  41
  42     return ci.getClassObjectRef();
  43   }
  44
  45   @MJI
  46   public boolean equals__Ljava_lang_Object_2__Z(MJIEnv env, int objRef, int otherObj) {
  47     if(otherObj == MJIEnv.NULL) {
  48       return false;
  49     }
  50     ClassInfo thisProxy = env.getClassInfo(objRef);
  51     ClassInfo otherProxy = env.getClassInfo(otherObj);
  52     if(!thisProxy.equals(otherProxy)) {
  53       if(!otherProxy.getAllInterfaceClassInfos().containsAll(thisProxy.getAllInterfaces())) {
  54         return false;
  55       }
  56       // oof, someone implemented an annotation in user code. Delegate to their equals and let them deal with it
  57       MethodInfo mi = otherProxy.getMethod("equals(Ljava/lang/Object;)Z", true);
  58       assert mi != null;
  59       ThreadInfo ti = env.getThreadInfo();
  60       DirectCallStackFrame frame = ti.getReturnedDirectCall();
  61       if(frame == null) {
  62         frame = mi.createDirectCallStackFrame(ti, 0);
  63         frame.setReferenceArgument(0, otherObj, env.getObjectAttr(otherObj));
  64         frame.setReferenceArgument(1, objRef, env.getObjectAttr(objRef));
  65         ti.pushFrame(frame);
  66         return false;
  67       } else {
  68         Object attr = frame.getResultAttr();
  69         int ret = frame.getResult();
  70         env.setReturnAttribute(attr);
  71         return ret == 1;
  72       }
  73     }
  74     return annotationsEqual(env, objRef, otherObj);
  75   }
  76
  77   public static boolean annotationsEqual(MJIEnv env, int aObj, int bObj) {
  78     if((aObj == MJIEnv.NULL) != (bObj == MJIEnv.NULL)) {
  79       return false;
  80     }
  81     ClassInfo thisProxy = env.getClassInfo(aObj);
  82     ClassInfo otherProxy = env.getClassInfo(bObj);
  83     if(!thisProxy.equals(otherProxy)) {
  84       return false;
  85     }
  86     FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
  87     ElementInfo aE = env.getElementInfo(aObj);
  88     ElementInfo bE = env.getElementInfo(bObj);
  89     for (int i=0; i<fields.length; i++){
  90       FieldInfo fi = fields[i];
  91       String fn = fi.getName();
  92       String ft = fi.getType();
  93       if(!fi.isReference()) {
  94         if(fi.is1SlotField()) {
  95           if(aE.get1SlotField(fi) != bE.get1SlotField(fi)) {
  96             return false;
  97           }
  98         } else {
  99           if(aE.get2SlotField(fi) != bE.get2SlotField(fi)) {
 100             return false;
 101           }
 102         }
 103       } else if(ft.equals("java.lang.Class")) {
 104         if(env.getReferenceField(aObj, fi) != env.getReferenceField(bObj, fi)) {
 105           return false;
 106         }
 107       } else if(ft.equals("java.lang.String")) {
 108         String aStr = env.getStringField(aObj, fn);
 109         String bStr = env.getStringField(bObj, fn);
 110         if(!Objects.equals(aStr, bStr)) {
 111           return false;
 112         }
 113       } else if(ft.endsWith("[]")) {
 114         String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
 115         int aArrayRef = env.getReferenceField(aObj, fi);
 116         int bArrayRef = env.getReferenceField(bObj, fi);
 117         if((aArrayRef == MJIEnv.NULL) != (bArrayRef == MJIEnv.NULL)) {
 118           return false;
 119         }
 120         ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
 121         ElementInfo bArrayContents = env.getElementInfo(bArrayRef);
 122         assert aArrayContents.isArray() && bArrayContents.isArray();
 123         if(Types.isBasicType(elemType) || elemType.equals("java.lang.Class")) {
 124           Object rawArray1 = aArrayContents.getArrayFields().getValues();
 125           Object rawArray2 = bArrayContents.getArrayFields().getValues();
 126           if(!Objects.deepEquals(rawArray1, rawArray2)) {
 127             return false;
 128           }
 129         // string array
 130         } else if(elemType.equals("java.lang.String")) {
 131           if(!Arrays.equals(env.getStringArrayObject(aArrayRef), env.getStringArrayObject(bArrayRef))) {
 132             return false;
 133           }
 134         // either annotation or enum
 135         } else {
 136           int arrayLength1 = env.getArrayLength(aArrayRef);
 137           int arrayLength2 = env.getArrayLength(bArrayRef);
 138           if(arrayLength2 != arrayLength1) {
 139             return false;
 140           }
 141           for(int j = 0; j < arrayLength1; j++) {
 142             int elem1Ref = env.getReferenceArrayElement(aArrayRef, j);
 143             int elem2Ref = env.getReferenceArrayElement(bArrayRef, j);
 144             assert elem1Ref != MJIEnv.NULL && elem2Ref != MJIEnv.NULL;
 145             if(!referenceTypesEqual(env, elem1Ref, elem2Ref)) {
 146               return false;
 147             }
 148           }
 149         }
 150       } else {
 151         if(!referenceTypesEqual(env, env.getReferenceField(aObj, fi), env.getReferenceField(bObj, fi))) {
 152           return false;
 153         }
 154       }
 155     }
 156     return true;
 157   }
 158
 159   private static boolean referenceTypesEqual(MJIEnv env, int elem1Ref, int elem2Ref) {
 160     ClassInfo aci = env.getClassInfo(elem1Ref);
 161     ClassInfo bci = env.getClassInfo(elem2Ref);
 162     assert aci != null && bci != null;
 163     if(!aci.equals(bci)) {
 164       return false;
 165     }
 166     if(aci.isEnum()) {
 167       return elem1Ref == elem2Ref;
 168     } else {
 169       return annotationsEqual(env, elem1Ref, elem2Ref);
 170     }
 171   }
 172
 173   @MJI
 174   public int toString____Ljava_lang_String_2 (MJIEnv env, int objref){
 175     StringBuilder sb = new StringBuilder();
 176     annotationReferenceToString(env, objref, sb);
 177     return env.newString(sb.toString());
 178   }
 179
 180   private int annotationHashCode(MJIEnv env, int objRef) {
 181     ClassInfo thisProxy = env.getClassInfo(objRef);
 182     FieldInfo[] fields = thisProxy.getDeclaredInstanceFields();
 183     int hashCode = 0;
 184     for (int i=0; i<fields.length; i++){
 185       FieldInfo fi = fields[i];
 186       int fieldHash = computeFieldHash(env, objRef, fi);
 187       hashCode += (127 * getStringHash(env, env.newString(fi.getName()))) ^ fieldHash;
 188     }
 189     return hashCode;
 190   }
 191
 192   private int computeFieldHash(MJIEnv env, int objRef, FieldInfo fi) {
 193     String fn = fi.getName();
 194     String ft = fi.getType();
 195     if(!fi.isReference()) {
 196       switch(ft) {
 197       case "byte":
 198         return Byte.valueOf(env.getByteField(objRef, fn)).hashCode();
 199       case "boolean":
 200         return Boolean.valueOf(env.getBooleanField(objRef, fn)).hashCode();
 201       case "char":
 202         return Character.valueOf(env.getCharField(objRef, fn)).hashCode();
 203       case "short":
 204         return Short.valueOf(env.getShortField(objRef, fn)).hashCode();
 205       case "int":
 206         return Integer.valueOf(env.getIntField(objRef, fn)).hashCode();
 207       case "long":
 208         return Long.valueOf(env.getLongField(objRef, fn)).hashCode();
 209       case "float":
 210         return Float.valueOf(env.getFloatField(objRef, fn)).hashCode();
 211       case "double":
 212         return Double.valueOf(env.getDoubleField(objRef, fn)).hashCode();
 213       default:
 214         throw new UnsupportedOperationException();
 215       }
 216     } else if(ft.equals("java.lang.Class")) {
 217       return getObjectHash(env.getReferenceField(objRef, fi));
 218     } else if(ft.equals("java.lang.String")) {
 219       return getStringHash(env, env.getReferenceField(objRef, fi));
 220     } else if(ft.endsWith("[]")) {
 221       int aArrayRef = env.getReferenceField(objRef, fi);
 222       ElementInfo aArrayContents = env.getElementInfo(aArrayRef);
 223       String elemType = Types.getTypeName(Types.getArrayElementType(fi.getSignature()));
 224       if(Types.isBasicType(elemType)) {
 225         Object rawArray1 = aArrayContents.getArrayFields().getValues();
 226         if(rawArray1 instanceof boolean[]) {
 227           return Arrays.hashCode((boolean[])rawArray1);
 228         } else if(rawArray1 instanceof byte[]) {
 229           return Arrays.hashCode((byte[])rawArray1);
 230         } else if(rawArray1 instanceof char[]) {
 231           return Arrays.hashCode((char[])rawArray1);
 232         } else if(rawArray1 instanceof short[]) {
 233           return Arrays.hashCode((short[])rawArray1);
 234         } else if(rawArray1 instanceof int[]) {
 235           return Arrays.hashCode((int[])rawArray1);
 236         } else if(rawArray1 instanceof long[]) {
 237           return Arrays.hashCode((long[])rawArray1);
 238         } else if(rawArray1 instanceof float[]) {
 239           return Arrays.hashCode((float[])rawArray1);
 240         } else if(rawArray1 instanceof double[]) {
 241           return Arrays.hashCode((double[])rawArray1);
 242         } else {
 243           throw new RuntimeException();
 244         }
 245       } else if(elemType.equals("java.lang.Class")) {
 246         return computeObjectArrayHash(env, aArrayRef, this::getObjectHash);
 247       // string array
 248       } else if(elemType.equals("java.lang.String")) {
 249         return computeObjectArrayHash(env, aArrayRef, (ref) -> getStringHash(env, ref));
 250       } else {
 251         return computeObjectArrayHash(env, aArrayRef, (ref) -> hashReferenceValue(env, ref));
 252       }
 253     } else {
 254       return hashReferenceValue(env, env.getReferenceField(objRef, fi));
 255     }
 256   }
 257
 258   /*
 259    * THIS WILL BREAK if the JDK uses a different hashcode from the one here
 260    */
 261   private int computeObjectArrayHash(MJIEnv env, int arrayRef, IntFunction<Integer> refHasher) {
 262     int arrayLength1 = env.getArrayLength(arrayRef);
 263     int hash = 1;
 264     for(int j = 0; j < arrayLength1; j++) {
 265       int elem1Ref = env.getReferenceArrayElement(arrayRef, j);
 266       hash = 31 * hash + refHasher.apply(elem1Ref);
 267     }
 268     return hash;
 269   }
 270
 271   private int getStringHash(MJIEnv env, int strObjRef) {
 272     return JPF_java_lang_String.computeStringHashCode(env, strObjRef);
 273   }
 274
 275   private int getObjectHash(int ref) {
 276     return ref ^ 0xABCD;
 277   }
 278
 279   private int hashReferenceValue(MJIEnv env, int elem1Ref) {
 280     ClassInfo aci = env.getClassInfo(elem1Ref);
 281     if(aci.isEnum()) {
 282       return getObjectHash(elem1Ref);
 283     } else {
 284       return annotationHashCode(env, elem1Ref);
 285     }
 286   }
 287
 288   @MJI
 289   public int hashCode____I(MJIEnv env, int objRef) {
 290     return annotationHashCode(env, objRef);
 291   }
 292
 293   private void annotationReferenceToString(MJIEnv env, int objref, StringBuilder sb) {
 294     ClassInfo ci = env.getClassInfo(objref);
 295     String cname = ci.getName();
 296     int idx = cname.lastIndexOf('$');
 297
 298     sb.append('@');
 299     sb.append(cname.substring(0,idx));
 300
 301     FieldInfo[] fields = ci.getDeclaredInstanceFields();
 302     if (fields.length > 0){
 303       sb.append('(');
 304       for (int i=0; i<fields.length; i++){
 305         String fn = fields[i].getName();
 306         String ft = fields[i].getType();
 307
 308         if (i>0){
 309           sb.append(',');
 310         }
 311         sb.append(fn);
 312         sb.append('=');
 313
 314         if(ft.equals("int")) {
 315           sb.append(env.getIntField(objref,fn));
 316
 317         } else if(ft.equals("byte")) {
 318           sb.append(env.getByteField(objref,fn));
 319
 320         } else if(ft.equals("boolean")) {
 321           sb.append(env.getBooleanField(objref,fn));
 322
 323         } else if(ft.equals("short")) {
 324           sb.append(env.getShortField(objref, fn));
 325
 326         } else if(ft.equals("char")) {
 327           sb.append(env.getCharField(objref, fn));
 328
 329         } else if(ft.equals("float")) {
 330           sb.append(env.getFloatField(objref, fn));
 331
 332         } else if(ft.equals("long")) {
 333           sb.append(env.getLongField(objref, fn));
 334
 335         } else if(ft.equals("double")) {
 336           sb.append(env.getDoubleField(objref,fn));
 337
 338         } else if(ft.equals("java.lang.String")) {
 339           sb.append(env.getStringObject(env.getReferenceField(objref, fn)));
 340
 341         } else if(ft.equals("java.lang.Class")) {
 342           int cref = env.getReferenceField(objref, fn);
 343           if (cref != MJIEnv.NULL){
 344             int nref = env.getReferenceField(cref, "name");
 345             String cn = env.getStringObject(nref);
 346
 347             sb.append("class ");
 348             sb.append(cn);
 349           } else {
 350             sb.append("class ?");
 351           }
 352
 353         } else if(ft.endsWith("[]")) {
 354           int ar = env.getReferenceField(objref, fn);
 355           int n = env.getArrayLength((ar));
 356
 357           sb.append('[');
 358
 359           if(ft.equals("int[]")) {
 360             for (int j=0; j<n; j++){
 361               if (j>0) sb.append(',');
 362               sb.append(env.getIntArrayElement(ar,j));
 363             }
 364
 365           } else if(ft.equals("byte[]")) {
 366             for (int j=0; j<n; j++){
 367               if (j>0) sb.append(',');
 368               sb.append(env.getByteArrayElement(ar,j));
 369             }
 370
 371           } else if(ft.equals("boolean[]")) {
 372             for (int j=0; j<n; j++){
 373               if (j>0) sb.append(',');
 374               sb.append(env.getBooleanArrayElement(ar,j));
 375             }
 376
 377           } else if(ft.equals("short[]")) {
 378             for (int j=0; j<n; j++){
 379               if (j>0) sb.append(',');
 380               sb.append(env.getShortArrayElement(ar,j));
 381             }
 382
 383           } else if(ft.equals("char[]")) {
 384             for (int j=0; j<n; j++){
 385               if (j>0) sb.append(',');
 386               sb.append(env.getCharArrayElement(ar,j));
 387             }
 388
 389           } else if(ft.equals("float[]")) {
 390             for (int j=0; j<n; j++){
 391               if (j>0) sb.append(',');
 392               sb.append(env.getFloatArrayElement(ar,j));
 393             }
 394
 395           } else if(ft.equals("long[]")) {
 396             for (int j=0; j<n; j++){
 397               if (j>0) sb.append(',');
 398               sb.append(env.getLongArrayElement(ar,j));
 399             }
 400
 401           } else if(ft.equals("double[]")) {
 402             for (int j=0; j<n; j++){
 403               if (j>0) sb.append(',');
 404               sb.append(env.getDoubleArrayElement(ar,j));
 405             }
 406
 407           } else if(ft.equals("java.lang.String[]")) {
 408             for (int j=0; j<n; j++){
 409               if (j>0) sb.append(',');
 410               sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j)));
 411             }
 412
 413           } else if(ft.equals("java.lang.Class[]")) {
 414             for (int j=0; j<n; j++){
 415               if (j>0) sb.append(',');
 416
 417               int cref = env.getReferenceArrayElement(ar,j);
 418               if (cref != MJIEnv.NULL){
 419                 int nref = env.getReferenceField(cref, "name");
 420                 String cn = env.getStringObject(nref);
 421
 422                 sb.append("class ");
 423                 sb.append(cn);
 424               } else {
 425                 sb.append("class ?");
 426               }
 427
 428             }
 429           } else {
 430             for(int j=0; j < n; j++) {
 431               if (j>0) sb.append(',');
 432
 433               int cref = env.getReferenceArrayElement(ar,j);
 434               if (cref != MJIEnv.NULL){
 435                 referenceToString(env, sb, cref);
 436               } else {
 437                 sb.append("null");
 438               }
 439             }
 440           }
 441
 442           sb.append("]");
 443         } else {
 444           int eref = env.getReferenceField(objref, fn);
 445           if (eref != MJIEnv.NULL){
 446             referenceToString(env, sb, eref);
 447           }
 448         }
 449       }
 450       sb.append(')');
 451     }
 452   }
 453
 454   private void referenceToString(MJIEnv env, StringBuilder sb, int eref) {
 455     ClassInfo eci = env.getClassInfo(eref);
 456     if (eci.isEnum()){
 457       int nref = env.getReferenceField(eref, "name");
 458       String en = env.getStringObject(nref);
 459
 460       sb.append(eci.getName());
 461       sb.append('.');
 462       sb.append(en);
 463     } else {
 464       annotationReferenceToString(env, eref, sb);
 465     }
 466   }
 467 }