src/peers/gov/nasa/jpf/vm/JPF_java_io_RandomAccessFile.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.annotation.MJI;
  21
  22 import java.util.HashMap;
  23
  24 import gov.nasa.jpf.Config;
  25
  26 /**
  27  * MJI NativePeer class for java.io.RandomAccessFile library abstraction
  28  *
  29  * @author Owen O'Malley
  30  */
  31 public class JPF_java_io_RandomAccessFile extends NativePeer {
  32
  33         // need to see whether the file is already in use
  34         // if so, then we'll update the file data and length in the original file
  35         // we do update the length in the local object, but not the data
  36
  37         static HashMap<Integer, Integer> File2DataMap;
  38
  39   public static boolean init (Config conf) {
  40     File2DataMap = new HashMap<Integer, Integer>();
  41     return (File2DataMap != null);
  42   }
  43
  44         // get the mapped object if one exists
  45         private static int getMapping(MJIEnv env, int this_ptr) {
  46                 int fn_ptr = env.getReferenceField(this_ptr,"filename");
  47                 Object o = File2DataMap.get(new Integer(fn_ptr));
  48                 if (o == null)
  49                         return this_ptr;
  50                 return ((Integer)o).intValue();
  51         }
  52
  53         // set the mapping during the constructor call
  54   @MJI
  55         public void setDataMap____V (MJIEnv env, int this_ptr) {
  56                 int fn_ptr = env.getReferenceField(this_ptr,"filename");
  57                 if (!File2DataMap.containsKey(new Integer(fn_ptr)))
  58                         File2DataMap.put(new Integer(fn_ptr),new Integer(this_ptr));
  59         }
  60
  61   static ClassInfo getDataRepresentationClassInfo (MJIEnv env) {
  62     ThreadInfo ti = env.getThreadInfo();
  63     Instruction insn = ti.getPC();
  64
  65     ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo(DataRepresentation);
  66     if (ci.initializeClass(ti)){
  67       env.repeatInvocation();
  68       return null;
  69     }
  70
  71     return ci;
  72   }
  73
  74   @MJI
  75   public void writeByte__I__V (MJIEnv env, int this_ptr, int data) {
  76
  77
  78     long current_posn = env.getLongField(this_ptr, current_position);
  79     long current_len = env.getLongField(this_ptr, current_length);
  80     int chunk_size = env.getStaticIntField(RandomAccessFile, CHUNK_SIZE);
  81     int chunk = findDataChunk(env, this_ptr, current_posn,
  82                               chunk_size);
  83     setDataValue(env, chunk, current_posn, (byte) data, chunk_size);
  84     current_posn += 1;
  85     env.setLongField(this_ptr, current_position, current_posn);
  86     if (current_posn >= current_len) {
  87       env.setLongField(this_ptr, current_length, current_posn + 1);
  88       // update length in the mapped object if it exists
  89       env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
  90     }
  91   }
  92
  93   /**
  94    * This is a bit lame doing it this way, but it is easy.
  95    */
  96   @MJI
  97   public void write___3BII__V (MJIEnv env, int this_ptr, int data_array,
  98                            int start, int len) {
  99     byte[] data_values = env.getByteArrayObject(data_array);
 100     for(int i=start; i < len; ++i) {
 101       writeByte__I__V(env, this_ptr, data_values[i]);
 102     }
 103   }
 104
 105   @MJI
 106   public void setLength__J__V(MJIEnv env, int this_ptr, long len) {
 107     long current_posn = env.getLongField(this_ptr, current_position);
 108     long current_len = env.getLongField(this_ptr, current_length);
 109     if (current_posn >= len && len < current_len) {
 110       env.setLongField(this_ptr, current_position, len);
 111     }
 112     env.setLongField(this_ptr, current_length, len);
 113     // update length in the mapped object if it exists
 114     env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
 115   }
 116
 117   @MJI
 118   public int read___3BII__I (MJIEnv env, int this_ptr, int data_array,
 119                          int start, int len) {
 120     int i = 0;
 121     long current_posn = env.getLongField(this_ptr, current_position);
 122     long current_len = env.getLongField(this_ptr, current_length);
 123     while (i < len && current_posn < current_len) {
 124       env.setByteArrayElement(data_array, start + i, readByte____B(env, this_ptr));
 125       i += 1;
 126       current_posn += 1;
 127     }
 128     if (i == 0) {
 129       return -1;
 130     }
 131     return i;
 132   }
 133
 134   @MJI
 135   public byte readByte____B (MJIEnv env, int this_ptr) {
 136     long current_posn = env.getLongField(this_ptr, current_position);
 137     long current_len = env.getLongField(this_ptr, current_length);
 138     int chunk_size = env.getStaticIntField(RandomAccessFile, CHUNK_SIZE);
 139     if (current_posn >= current_len) {
 140       env.throwException(EOFException);
 141     }
 142     int chunk = findDataChunk(env, this_ptr, current_posn,
 143                               chunk_size);
 144     byte result = getDataValue(env, chunk, current_posn, chunk_size);
 145     env.setLongField(this_ptr, current_position, current_posn + 1);
 146     return result;
 147   }
 148
 149   private static final int INT_SIZE = 4;
 150   private static final String data_root = "data_root";
 151   private static final String current_position = "currentPosition";
 152   private static final String current_length = "currentLength";
 153   private static final String CHUNK_SIZE = "CHUNK_SIZE";
 154   private static final String chunk_index = "chunk_index";
 155   private static final String next = "next";
 156   private static final String data = "data";
 157   private static final String EOFException = "java.io.EOFException";
 158   private static final String RandomAccessFile = "java.io.RandomAccessFile";
 159   private static final String DataRepresentation =
 160     RandomAccessFile + "$DataRepresentation";
 161
 162   private static int findDataChunk(MJIEnv env, int this_ptr, long position,
 163                                    int chunk_size) {
 164
 165     ClassInfo dataRep = getDataRepresentationClassInfo(env);
 166     if (dataRep == null) {
 167       // will be reexecuted
 168       return 0;
 169     }
 170
 171         //check if the file data is mapped, use mapped this_ptr if it exists
 172         this_ptr = getMapping(env,this_ptr);
 173     int prev_obj = MJIEnv.NULL;
 174     int cur_obj = env.getReferenceField(this_ptr, data_root);
 175     long chunk_idx = position/chunk_size;
 176     while (cur_obj != MJIEnv.NULL &&
 177            env.getLongField(cur_obj, chunk_index) < chunk_idx) {
 178       prev_obj = cur_obj;
 179       cur_obj = env.getReferenceField(cur_obj, next);
 180     }
 181     if (cur_obj != MJIEnv.NULL &&
 182         env.getLongField(cur_obj, chunk_index) == chunk_idx) {
 183       return cur_obj;
 184     }
 185     int result = env.newObject(dataRep);
 186     int int_array = env.newIntArray(chunk_size/INT_SIZE);
 187     env.setReferenceField(result, data, int_array);
 188     env.setLongField(result, chunk_index, chunk_idx);
 189     env.setReferenceField(result, next, cur_obj);
 190     if (prev_obj == MJIEnv.NULL) {
 191       env.setReferenceField(this_ptr, data_root, result);
 192     } else {
 193       env.setReferenceField(prev_obj, next, result);
 194     }
 195     return result;
 196   }
 197
 198   private static void setDataValue(MJIEnv env, int chunk_obj, long position,
 199                                    byte data_value, int chunk_size) {
 200     int offset = (int) (position % chunk_size);
 201     int index = offset / INT_SIZE;
 202     int bit_shift = 8 * (offset % INT_SIZE);
 203     int int_array = env.getReferenceField(chunk_obj, data);
 204     int old_value = env.getIntArrayElement(int_array, index);
 205     env.setIntArrayElement(int_array, index,
 206                              (old_value & ~(0xff << bit_shift)) |
 207                              data_value << bit_shift);
 208   }
 209
 210   private static byte getDataValue(MJIEnv env, int chunk_obj, long position,
 211                                    int chunk_size) {
 212     int offset = (int) (position % chunk_size);
 213     int index = offset / INT_SIZE;
 214     int bit_shift = 8 * (offset % INT_SIZE);
 215     int int_array = env.getReferenceField(chunk_obj, data);
 216     return (byte) (env.getIntArrayElement(int_array, index) >> bit_shift);
 217
 218   }
 219 }
 220