|
1
20 package gov.nasa.jpf.jvm;
21
22 import java.util.HashMap  ;
23
24
29 public class JPF_java_io_RandomAccessFile {
30
31
35 static HashMap File2DataMap = new HashMap ();
36
37 private static int getMapping(MJIEnv env, int this_ptr) {
39 int fn_ptr = env.getReferenceField(this_ptr,"filename");
40 Object o = File2DataMap.get(new Integer (fn_ptr));
41 if (o == null)
42 return this_ptr;
43 return ((Integer )o).intValue();
44 }
45
46 public static void setDataMap(MJIEnv env, int this_ptr) {
48 int fn_ptr = env.getReferenceField(this_ptr,"filename");
49 if (!File2DataMap.containsKey(new Integer (fn_ptr)))
50 File2DataMap.put(new Integer (fn_ptr),new Integer (this_ptr));
51 }
52
53 public static void writeByte(MJIEnv env, int this_ptr, int data) {
54 long current_posn = env.getLongField(this_ptr, current_position);
55 long current_len = env.getLongField(this_ptr, current_length);
56 int chunk_size = env.getStaticIntField(RandomAccessFile, CHUNK_SIZE);
57 int chunk = findDataChunk(env, this_ptr, current_posn,
58 chunk_size);
59 setDataValue(env, chunk, current_posn, (byte) data, chunk_size);
60 current_posn += 1;
61 env.setLongField(this_ptr, current_position, current_posn);
62 if (current_posn >= current_len) {
63 env.setLongField(this_ptr, current_length, current_posn + 1);
64 env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
66 }
67 }
68
69
72 public static void write(MJIEnv env, int this_ptr, int data_array,
73 int start, int len) {
74 byte[] data_values = env.getByteArrayObject(data_array);
75 for(int i=start; i < len; ++i) {
76 writeByte(env, this_ptr, data_values[i]);
77 }
78 }
79
80 public static void setLength(MJIEnv env, int this_ptr, long len) {
81 long current_posn = env.getLongField(this_ptr, current_position);
82 long current_len = env.getLongField(this_ptr, current_length);
83 if (current_posn >= len && len < current_len) {
84 env.setLongField(this_ptr, current_position, len);
85 }
86 env.setLongField(this_ptr, current_length, len);
87 env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
89 }
90
91 public static int read(MJIEnv env, int this_ptr, int data_array,
92 int start, int len) {
93 int i = 0;
94 long current_posn = env.getLongField(this_ptr, current_position);
95 long current_len = env.getLongField(this_ptr, current_length);
96 while (i < len && current_posn < current_len) {
97 env.setByteArrayElement(data_array, start + i, readByte(env, this_ptr));
98 i += 1;
99 current_posn += 1;
100 }
101 if (i == 0) {
102 return -1;
103 }
104 return i;
105 }
106
107 public static byte readByte(MJIEnv env, int this_ptr) {
108 long current_posn = env.getLongField(this_ptr, current_position);
109 long current_len = env.getLongField(this_ptr, current_length);
110 int chunk_size = env.getStaticIntField(RandomAccessFile, CHUNK_SIZE);
111 if (current_posn >= current_len) {
112 env.throwException(EOFException);
113 }
114 int chunk = findDataChunk(env, this_ptr, current_posn,
115 chunk_size);
116 byte result = getDataValue(env, chunk, current_posn, chunk_size);
117 env.setLongField(this_ptr, current_position, current_posn + 1);
118 return result;
119 }
120
121 private static final int INT_SIZE = 4;
122 private static final String data_root = "data_root";
123 private static final String current_position = "currentPosition";
124 private static final String current_length = "currentLength";
125 private static final String CHUNK_SIZE = "CHUNK_SIZE";
126 private static final String chunk_index = "chunk_index";
127 private static final String next = "next";
128 private static final String data = "data";
129 private static final String EOFException = "java.io.EOFException";
130 private static final String RandomAccessFile = "java.io.RandomAccessFile";
131 private static final String DataRepresentation =
132 RandomAccessFile + "$DataRepresentation";
133
134 private static int findDataChunk(MJIEnv env, int this_ptr, long position,
135 int chunk_size) {
136
137 this_ptr = getMapping(env,this_ptr);
139 int prev_obj = MJIEnv.NULL;
140 int cur_obj = env.getReferenceField(this_ptr, data_root);
141 long chunk_idx = position/chunk_size;
142 while (cur_obj != MJIEnv.NULL &&
143 env.getLongField(cur_obj, chunk_index) < chunk_idx) {
144 prev_obj = cur_obj;
145 cur_obj = env.getReferenceField(cur_obj, next);
146 }
147 if (cur_obj != MJIEnv.NULL &&
148 env.getLongField(cur_obj, chunk_index) == chunk_idx) {
149 return cur_obj;
150 }
151 int result = env.newObject(DataRepresentation);
152 int int_array = env.newIntArray(chunk_size/INT_SIZE);
153 env.setReferenceField(result, data, int_array);
154 env.setLongField(result, chunk_index, chunk_idx);
155 env.setReferenceField(result, next, cur_obj);
156 if (prev_obj == MJIEnv.NULL) {
157 env.setReferenceField(this_ptr, data_root, result);
158 } else {
159 env.setReferenceField(prev_obj, next, result);
160 }
161 return result;
162 }
163
164 private static void setDataValue(MJIEnv env, int chunk_obj, long position,
165 byte data_value, int chunk_size) {
166 int offset = (int) (position % chunk_size);
167 int index = offset / INT_SIZE;
168 int bit_shift = 8 * (offset % INT_SIZE);
169 int int_array = env.getReferenceField(chunk_obj, data);
170 int old_value = env.getIntArrayElement(int_array, index);
171 env.setIntArrayElement(int_array, index,
172 (old_value & ~(0xff << bit_shift)) |
173 data_value << bit_shift);
174 }
175
176 private static byte getDataValue(MJIEnv env, int chunk_obj, long position,
177 int chunk_size) {
178 int offset = (int) (position % chunk_size);
179 int index = offset / INT_SIZE;
180 int bit_shift = 8 * (offset % INT_SIZE);
181 int int_array = env.getReferenceField(chunk_obj, data);
182 return (byte) (env.getIntArrayElement(int_array, index) >> bit_shift);
183
184 }
185 }
186
187 |
Popular Tags |
Java API By Example, From Geeks To Geeks.