001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019:
020: package gov.nasa.jpf.jvm;
021:
022: import java.util.HashMap;
023:
024: /**
025: * MJI NativePeer class for java.io.RandomAccessFile library abstraction
026: *
027: * @author Owen O'Malley
028: */
029: public class JPF_java_io_RandomAccessFile {
030:
031: // need to see whether the file is already in use
032: // if so, then we'll update the file data and length in the original file
033: // we do update the length in the local object, but not the data
034:
035: static HashMap File2DataMap = new HashMap();
036:
037: // get the mapped object if one exists
038: private static int getMapping(MJIEnv env, int this _ptr) {
039: int fn_ptr = env.getReferenceField(this _ptr, "filename");
040: Object o = File2DataMap.get(new Integer(fn_ptr));
041: if (o == null)
042: return this _ptr;
043: return ((Integer) o).intValue();
044: }
045:
046: // set the mapping during the constructor call
047: public static void setDataMap(MJIEnv env, int this _ptr) {
048: int fn_ptr = env.getReferenceField(this _ptr, "filename");
049: if (!File2DataMap.containsKey(new Integer(fn_ptr)))
050: File2DataMap
051: .put(new Integer(fn_ptr), new Integer(this _ptr));
052: }
053:
054: public static void writeByte(MJIEnv env, int this _ptr, int data) {
055: long current_posn = env
056: .getLongField(this _ptr, current_position);
057: long current_len = env.getLongField(this _ptr, current_length);
058: int chunk_size = env.getStaticIntField(RandomAccessFile,
059: CHUNK_SIZE);
060: int chunk = findDataChunk(env, this _ptr, current_posn,
061: chunk_size);
062: setDataValue(env, chunk, current_posn, (byte) data, chunk_size);
063: current_posn += 1;
064: env.setLongField(this _ptr, current_position, current_posn);
065: if (current_posn >= current_len) {
066: env
067: .setLongField(this _ptr, current_length,
068: current_posn + 1);
069: // update length in the mapped object if it exists
070: env.setLongField(getMapping(env, this _ptr), current_length,
071: current_posn + 1);
072: }
073: }
074:
075: /**
076: * This is a bit lame doing it this way, but it is easy.
077: */
078: public static void write(MJIEnv env, int this _ptr, int data_array,
079: int start, int len) {
080: byte[] data_values = env.getByteArrayObject(data_array);
081: for (int i = start; i < len; ++i) {
082: writeByte(env, this _ptr, data_values[i]);
083: }
084: }
085:
086: public static void setLength(MJIEnv env, int this _ptr, long len) {
087: long current_posn = env
088: .getLongField(this _ptr, current_position);
089: long current_len = env.getLongField(this _ptr, current_length);
090: if (current_posn >= len && len < current_len) {
091: env.setLongField(this _ptr, current_position, len);
092: }
093: env.setLongField(this _ptr, current_length, len);
094: // update length in the mapped object if it exists
095: env.setLongField(getMapping(env, this _ptr), current_length,
096: current_posn + 1);
097: }
098:
099: public static int read(MJIEnv env, int this _ptr, int data_array,
100: int start, int len) {
101: int i = 0;
102: long current_posn = env
103: .getLongField(this _ptr, current_position);
104: long current_len = env.getLongField(this _ptr, current_length);
105: while (i < len && current_posn < current_len) {
106: env.setByteArrayElement(data_array, start + i, readByte(
107: env, this _ptr));
108: i += 1;
109: current_posn += 1;
110: }
111: if (i == 0) {
112: return -1;
113: }
114: return i;
115: }
116:
117: public static byte readByte(MJIEnv env, int this _ptr) {
118: long current_posn = env
119: .getLongField(this _ptr, current_position);
120: long current_len = env.getLongField(this _ptr, current_length);
121: int chunk_size = env.getStaticIntField(RandomAccessFile,
122: CHUNK_SIZE);
123: if (current_posn >= current_len) {
124: env.throwException(EOFException);
125: }
126: int chunk = findDataChunk(env, this _ptr, current_posn,
127: chunk_size);
128: byte result = getDataValue(env, chunk, current_posn, chunk_size);
129: env.setLongField(this _ptr, current_position, current_posn + 1);
130: return result;
131: }
132:
133: private static final int INT_SIZE = 4;
134: private static final String data_root = "data_root";
135: private static final String current_position = "currentPosition";
136: private static final String current_length = "currentLength";
137: private static final String CHUNK_SIZE = "CHUNK_SIZE";
138: private static final String chunk_index = "chunk_index";
139: private static final String next = "next";
140: private static final String data = "data";
141: private static final String EOFException = "java.io.EOFException";
142: private static final String RandomAccessFile = "java.io.RandomAccessFile";
143: private static final String DataRepresentation = RandomAccessFile
144: + "$DataRepresentation";
145:
146: private static int findDataChunk(MJIEnv env, int this _ptr,
147: long position, int chunk_size) {
148:
149: //check if the file data is mapped, use mapped this_ptr if it exists
150: this _ptr = getMapping(env, this _ptr);
151: int prev_obj = MJIEnv.NULL;
152: int cur_obj = env.getReferenceField(this _ptr, data_root);
153: long chunk_idx = position / chunk_size;
154: while (cur_obj != MJIEnv.NULL
155: && env.getLongField(cur_obj, chunk_index) < chunk_idx) {
156: prev_obj = cur_obj;
157: cur_obj = env.getReferenceField(cur_obj, next);
158: }
159: if (cur_obj != MJIEnv.NULL
160: && env.getLongField(cur_obj, chunk_index) == chunk_idx) {
161: return cur_obj;
162: }
163: int result = env.newObject(DataRepresentation);
164: int int_array = env.newIntArray(chunk_size / INT_SIZE);
165: env.setReferenceField(result, data, int_array);
166: env.setLongField(result, chunk_index, chunk_idx);
167: env.setReferenceField(result, next, cur_obj);
168: if (prev_obj == MJIEnv.NULL) {
169: env.setReferenceField(this _ptr, data_root, result);
170: } else {
171: env.setReferenceField(prev_obj, next, result);
172: }
173: return result;
174: }
175:
176: private static void setDataValue(MJIEnv env, int chunk_obj,
177: long position, byte data_value, 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: int old_value = env.getIntArrayElement(int_array, index);
183: env.setIntArrayElement(int_array, index,
184: (old_value & ~(0xff << bit_shift))
185: | data_value << bit_shift);
186: }
187:
188: private static byte getDataValue(MJIEnv env, int chunk_obj,
189: long position, int chunk_size) {
190: int offset = (int) (position % chunk_size);
191: int index = offset / INT_SIZE;
192: int bit_shift = 8 * (offset % INT_SIZE);
193: int int_array = env.getReferenceField(chunk_obj, data);
194: return (byte) (env.getIntArrayElement(int_array, index) >> bit_shift);
195:
196: }
197: }
|