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 gov.nasa.jpf.annotation.MJI;
  22
  23 /**
  24  * native peer for Annotation Proxies
  25  * (saves us some bytecode interpretation shoe leather)
  26  */
  27 public class JPF_gov_nasa_jpf_AnnotationProxyBase extends NativePeer {
  28
  29   @MJI
  30   public int annotationType____Ljava_lang_Class_2 (MJIEnv env, int objref) {
  31     ClassInfo ciProxy = env.getClassInfo(objref);  // this would be the proxy
  32
  33     // we could also pull it out from the interfaces, but we know the naming scheme
  34     String proxyName = ciProxy.getName();
  35     String annotation = proxyName.substring(0, proxyName.length() - 6); // "...$Proxy"
  36     ClassInfo ci = ClassLoaderInfo.getCurrentResolvedClassInfo(annotation);
  37
  38     return ci.getClassObjectRef();
  39   }
  40
  41   @MJI
  42   public int toString____Ljava_lang_String_2 (MJIEnv env, int objref){
  43     StringBuffer sb = new StringBuffer();
  44
  45     ClassInfo ci = env.getClassInfo(objref);
  46     String cname = ci.getName();
  47     int idx = cname.lastIndexOf('$');
  48
  49     sb.append('@');
  50     sb.append(cname.substring(0,idx));
  51
  52     FieldInfo[] fields = ci.getDeclaredInstanceFields();
  53     if (fields.length > 0){
  54       sb.append('(');
  55       for (int i=0; i<fields.length; i++){
  56         String fn = fields[i].getName();
  57         String ft = fields[i].getType();
  58
  59         if (i>0){
  60           sb.append(',');
  61         }
  62         sb.append(fn);
  63         sb.append('=');
  64
  65         if (ft.equals("int")){
  66           sb.append(env.getIntField(objref,fn));
  67
  68         } else if (ft.equals("long")){
  69           sb.append(env.getLongField(objref,fn));
  70
  71         } else if (ft.equals("double")){
  72           sb.append(env.getDoubleField(objref,fn));
  73
  74         } else if (ft.equals("boolean")){
  75           sb.append(env.getBooleanField(objref,fn));
  76
  77         } else if (ft.equals("java.lang.String")){
  78           sb.append(env.getStringObject(env.getReferenceField(objref, fn)));
  79
  80         } else if (ft.equals("java.lang.Class")){
  81           int cref = env.getReferenceField(objref, fn);
  82           if (cref != MJIEnv.NULL){
  83             int nref = env.getReferenceField(cref, "name");
  84             String cn = env.getStringObject(nref);
  85
  86             sb.append("class ");
  87             sb.append(cn);
  88           } else {
  89             sb.append("class ?");
  90           }
  91
  92         } else if (ft.endsWith("[]")){
  93           int ar = env.getReferenceField(objref, fn);
  94           int n = env.getArrayLength((ar));
  95
  96           sb.append('[');
  97
  98           if (ft.equals("java.lang.String[]")){
  99             for (int j=0; j<n; j++){
 100               if (j>0) sb.append(',');
 101               sb.append(env.getStringObject(env.getReferenceArrayElement(ar,j)));
 102             }
 103
 104           } else if (ft.equals("int[]")){
 105             for (int j=0; j<n; j++){
 106               if (j>0) sb.append(',');
 107               sb.append(env.getIntArrayElement(ar,j));
 108             }
 109
 110           } else if (ft.equals("long[]")){
 111             for (int j=0; j<n; j++){
 112               if (j>0) sb.append(',');
 113               sb.append(env.getLongArrayElement(ar,j));
 114             }
 115
 116           } else if (ft.equals("double[]")){
 117             for (int j=0; j<n; j++){
 118               if (j>0) sb.append(',');
 119               sb.append(env.getDoubleArrayElement(ar,j));
 120             }
 121
 122           } else if (ft.equals("boolean[]")){
 123             for (int j=0; j<n; j++){
 124               if (j>0) sb.append(',');
 125               sb.append(env.getBooleanArrayElement(ar,j));
 126             }
 127           } else if (ft.equals("java.lang.Class[]")){
 128             for (int j=0; j<n; j++){
 129               if (j>0) sb.append(',');
 130
 131               int cref = env.getReferenceArrayElement(ar,j);
 132               if (cref != MJIEnv.NULL){
 133                 int nref = env.getReferenceField(cref, "name");
 134                 String cn = env.getStringObject(nref);
 135
 136                 sb.append("class ");
 137                 sb.append(cn);
 138               } else {
 139                 sb.append("class ?");
 140               }
 141
 142             }
 143           }
 144
 145           sb.append(']');
 146
 147         } else { // arbitrary type name, must be a reference
 148           int eref = env.getReferenceField(objref, fn);
 149           if (eref != MJIEnv.NULL){
 150             ClassInfo eci = env.getClassInfo(eref);
 151             if (eci.isEnum()){
 152               int nref = env.getReferenceField(eref, "name");
 153               String en = env.getStringObject(nref);
 154
 155               sb.append(eci.getName());
 156               sb.append('.');
 157               sb.append(en);
 158             }
 159           }
 160         }
 161       }
 162       sb.append(')');
 163     }
 164
 165
 166     return env.newString(sb.toString());
 167   }
 168 }