src/main/gov/nasa/jpf/util/ObjectConverter.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.util;
  20
  21 import gov.nasa.jpf.JPFException;
  22 import gov.nasa.jpf.vm.ClassInfo;
  23 import gov.nasa.jpf.vm.ClinitRequired;
  24 import gov.nasa.jpf.vm.ElementInfo;
  25 import gov.nasa.jpf.vm.FieldInfo;
  26 import gov.nasa.jpf.vm.Fields;
  27 import gov.nasa.jpf.vm.MJIEnv;
  28
  29 import java.lang.reflect.Array;
  30 import java.lang.reflect.Field;
  31
  32 /**
  33  * Object transformer from Java objects to JPF objects
  34  * @author Ivan Mushketik
  35  */
  36 public class ObjectConverter {
  37   /**
  38    * Create JPF object from Java object
  39    * @param env - MJI environment
  40    * @param javaObject - java object that is used to created JPF object from
  41    * @return reference to new JPF object
  42    */
  43   public static int JPFObjectFromJavaObject(MJIEnv env, Object javaObject) throws ClinitRequired {
  44       Class<?> javaClass = javaObject.getClass();
  45       String typeName = javaClass.getName();
  46       int newObjRef = env.newObject(typeName);
  47       ElementInfo newObjEI = env.getModifiableElementInfo(newObjRef);
  48
  49       ClassInfo ci = env.getClassInfo(newObjRef);
  50
  51       while (ci != null) {
  52         for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
  53           if (!fi.isReference()) {
  54             setJPFPrimitive(newObjEI, fi, javaObject);
  55           }
  56           else {
  57             try {
  58               Field arrField = getField(fi.getName(), javaClass);
  59               arrField.setAccessible(true);
  60               Object fieldJavaObj = arrField.get(javaObject);
  61
  62               int fieldJPFObjRef;
  63               if (isArrayField(fi)) {
  64                 fieldJPFObjRef = getJPFArrayRef(env, fieldJavaObj);
  65               } else {
  66                 fieldJPFObjRef = JPFObjectFromJavaObject(env, fieldJavaObj);
  67               }
  68
  69               newObjEI.setReferenceField(fi, fieldJPFObjRef);
  70
  71             } catch (NoSuchFieldException nsfx){
  72               throw new JPFException("JPF object creation failed, no such field: " + fi.getFullName(), nsfx);
  73             } catch (IllegalAccessException iax){
  74               throw new JPFException("JPF object creation failed, illegal access: " + fi.getFullName(), iax);
  75             }
  76           }
  77         }
  78
  79         ci = ci.getSuperClass();
  80       }
  81
  82       return newObjRef;
  83   }
  84
  85   private Object createObject(String className) {
  86     return null;
  87   }
  88
  89   private static void setJPFPrimitive(ElementInfo newObjEI, FieldInfo fi, Object javaObject) {
  90     try {
  91
  92       String jpfTypeName = fi.getType();
  93       Class javaClass = javaObject.getClass();
  94       Field javaField = getField(fi.getName(), javaClass);
  95       javaField.setAccessible(true);
  96
  97       if (jpfTypeName.equals("char")) {
  98         newObjEI.setCharField(fi, javaField.getChar(javaObject));
  99       }
 100       else if (jpfTypeName.equals("byte")) {
 101         newObjEI.setByteField(fi, javaField.getByte(javaObject));
 102       }
 103       else if (jpfTypeName.equals("short")) {
 104         newObjEI.setShortField(fi, javaField.getShort(javaObject));
 105       }
 106       else if (jpfTypeName.equals("int")) {
 107         newObjEI.setIntField(fi, javaField.getInt(javaObject));
 108       }
 109       else if (jpfTypeName.equals("long")) {
 110         newObjEI.setLongField(fi, javaField.getLong(javaObject));
 111       }
 112       else if (jpfTypeName.equals("float")) {
 113         newObjEI.setFloatField(fi, javaField.getFloat(javaObject));
 114       }
 115       else if (jpfTypeName.equals("double")) {
 116         newObjEI.setDoubleField(fi, javaField.getDouble(javaObject));
 117       }
 118     }
 119     catch (Exception ex) {
 120       throw new JPFException(ex);
 121     }
 122   }
 123
 124   private static Field getField(String fieldName, Class javaClass) throws NoSuchFieldException {
 125     while (true) {
 126       try {
 127         Field field = javaClass.getDeclaredField(fieldName);
 128         return field;
 129       } catch (NoSuchFieldException ex) {
 130         // Try to search this field in a super class
 131         javaClass = javaClass.getSuperclass();
 132
 133         // No more super class. Wrong field
 134         if (javaClass == null) {
 135           throw ex;
 136         }
 137       }
 138     }
 139
 140   }
 141
 142   private static int getJPFArrayRef(MJIEnv env, Object javaArr) throws NoSuchFieldException, IllegalAccessException {
 143
 144     Class arrayElementClass = javaArr.getClass().getComponentType();
 145
 146     int javaArrLength = Array.getLength(javaArr);
 147     int arrRef;
 148
 149     if (arrayElementClass == Character.TYPE) {
 150       arrRef = env.newCharArray(javaArrLength);
 151       ElementInfo charArrRef = env.getModifiableElementInfo(arrRef);
 152       char[] charArr = charArrRef.asCharArray();
 153
 154       for (int i = 0; i < javaArrLength; i++) {
 155         charArr[i] = Array.getChar(javaArr, i);
 156       }
 157     }
 158     else if (arrayElementClass == Byte.TYPE) {
 159       arrRef = env.newByteArray(javaArrLength);
 160       ElementInfo byteArrRef = env.getModifiableElementInfo(arrRef);
 161       byte[] byteArr = byteArrRef.asByteArray();
 162
 163       for (int i = 0; i < javaArrLength; i++) {
 164         byteArr[i] = Array.getByte(javaArr, i);
 165       }
 166     }
 167     else if (arrayElementClass == Short.TYPE) {
 168       arrRef = env.newShortArray(javaArrLength);
 169       ElementInfo shortArrRef = env.getModifiableElementInfo(arrRef);
 170       short[] shortArr = shortArrRef.asShortArray();
 171
 172       for (int i = 0; i < javaArrLength; i++) {
 173         shortArr[i] = Array.getShort(javaArr, i);
 174       }
 175     }
 176     else if (arrayElementClass == Integer.TYPE) {
 177       arrRef = env.newIntArray(javaArrLength);
 178       ElementInfo intArrRef = env.getModifiableElementInfo(arrRef);
 179       int[] intArr = intArrRef.asIntArray();
 180
 181       for (int i = 0; i < javaArrLength; i++) {
 182         intArr[i] = Array.getInt(javaArr, i);
 183       }
 184     }
 185     else if (arrayElementClass == Long.TYPE) {
 186       arrRef = env.newLongArray(javaArrLength);
 187       ElementInfo longArrRef = env.getModifiableElementInfo(arrRef);
 188       long[] longArr = longArrRef.asLongArray();
 189
 190       for (int i = 0; i < javaArrLength; i++) {
 191         longArr[i] = Array.getLong(javaArr, i);
 192       }
 193     }
 194     else if (arrayElementClass == Float.TYPE) {
 195       arrRef = env.newFloatArray(javaArrLength);
 196       ElementInfo floatArrRef = env.getModifiableElementInfo(arrRef);
 197       float[] floatArr = floatArrRef.asFloatArray();
 198
 199       for (int i = 0; i < javaArrLength; i++) {
 200         floatArr[i] = Array.getFloat(javaArr, i);
 201       }
 202     }
 203     else if (arrayElementClass == Double.TYPE) {
 204       arrRef = env.newDoubleArray(javaArrLength);
 205       ElementInfo floatArrRef = env.getModifiableElementInfo(arrRef);
 206       double[] doubleArr = floatArrRef.asDoubleArray();
 207
 208       for (int i = 0; i < javaArrLength; i++) {
 209         doubleArr[i] = Array.getDouble(javaArr, i);
 210       }
 211     }
 212     else {
 213       arrRef = env.newObjectArray(arrayElementClass.getCanonicalName(), javaArrLength);
 214       ElementInfo arrayEI = env.getModifiableElementInfo(arrRef);
 215
 216       Fields fields = arrayEI.getFields();
 217
 218       for (int i = 0; i < javaArrLength; i++) {
 219         int newArrElRef;
 220         Object javaArrEl = Array.get(javaArr, i);
 221
 222         if (javaArrEl != null) {
 223           if (javaArrEl.getClass().isArray()) {
 224             newArrElRef = getJPFArrayRef(env, javaArrEl);
 225           }
 226           else {
 227             newArrElRef = JPFObjectFromJavaObject(env, javaArrEl);
 228           }
 229         }
 230         else {
 231           newArrElRef = MJIEnv.NULL;
 232         }
 233
 234         fields.setReferenceValue(i, newArrElRef);
 235       }
 236     }
 237
 238     return arrRef;
 239   }
 240
 241   // Do we need this??
 242   public static Object javaObjectFromJPFObject(ElementInfo ei) {
 243     try {
 244       String typeName = ei.getType();
 245       Class clazz = ClassLoader.getSystemClassLoader().loadClass(typeName);
 246
 247       Object javaObject = clazz.newInstance();
 248       ClassInfo ci = ei.getClassInfo();
 249       while (ci != null) {
 250
 251         for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
 252           if (!fi.isReference()) {
 253             setJavaPrimitive(javaObject, ei, fi);
 254           }
 255         }
 256
 257         ci = ci.getSuperClass();
 258       }
 259
 260       return javaObject;
 261     } catch (Exception ex) {
 262       throw new JPFException(ex);
 263     }
 264   }
 265
 266   private static void setJavaPrimitive(Object javaObject, ElementInfo ei, FieldInfo fi) throws NoSuchFieldException, IllegalAccessException {
 267     String primitiveType = fi.getName();
 268     String fieldName = fi.getName();
 269
 270     Class javaClass = javaObject.getClass();
 271     Field javaField = javaClass.getDeclaredField(fieldName);
 272     javaField.setAccessible(true);
 273
 274     if (primitiveType.equals("char")) {
 275       javaField.setChar(javaObject, ei.getCharField(fi));
 276     }
 277     else if (primitiveType.equals("byte")) {
 278       javaField.setByte(javaObject, ei.getByteField(fi));
 279     }
 280     else if (primitiveType.equals("short")) {
 281       javaField.setShort(javaObject, ei.getShortField(fi));
 282     }
 283     else if (primitiveType.equals("int")) {
 284       javaField.setInt(javaObject, ei.getIntField(fi));
 285     }
 286     else if (primitiveType.equals("long")) {
 287       javaField.setLong(javaObject, ei.getLongField(fi));
 288     }
 289     else if (primitiveType.equals("float")) {
 290       javaField.setFloat(javaObject, ei.getFloatField(fi));
 291     }
 292     else if (primitiveType.equals("double")) {
 293       javaField.setDouble(javaObject, ei.getDoubleField(fi));
 294     }
 295     else {
 296       throw new JPFException("Can't convert " + primitiveType + " to " +
 297               javaField.getClass().getCanonicalName());
 298     }
 299   }
 300
 301   private static boolean isArrayField(FieldInfo fi) {
 302     return fi.getType().lastIndexOf('[') >= 0;
 303   }
 304
 305
 306 }