001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package javafe.util;
004
005 import java.io.IOException;
006
007 /**
008 * Instances of this <code>CorrelatedReader</code> contain a buffer.
009 */
010
011 public abstract class BufferedCorrelatedReader extends CorrelatedReader
012 {
013 /**
014 * All locations are allocated at or above a medium-large int
015 * STARTFREELOC to make it less likely that other program ints can
016 * be interpreted as locations.
017 */
018
019 /*@ spec_public */ static final int STARTFREELOC = 1000000;
020
021 /**
022 * The allocated location range for this CorrelatedReader instance
023 * is [minLoc, maxLoc). <p>
024 *
025 * Note that in practice only a prefix,
026 * [minLoc, min(beforeBufLoc + curNdx, maxLoc-1)],
027 * of the range representing the characters read so far are actually valid
028 * locations at any given time.
029 */
030 //@ invariant STARTFREELOC <= minLoc;
031 //@ invariant minLoc <= maxLoc;
032
033 protected int minLoc;
034 protected int maxLoc;
035
036 /**
037 * While open, we buffer input in the buffer <code>buf</code>, which
038 * grows on demand.
039 *
040 * We are closed iff <code>buf</code> is non-null.
041 */
042
043 /*@spec_public*/ protected byte[] buf;
044
045 /**
046 * The location of the first character in the buffer, minus 1. <p>
047 *
048 * The locations of later valid characters are obtained by adding
049 * their index to this loc. <p>
050 */
051 //@ invariant minLoc-1 <= beforeBufLoc;
052
053 protected int beforeBufLoc;
054
055 /**
056 * The first unused entry in the buffer. Aka,
057 * buf[0]...buf[endBufNdx-1] contains valid data (if buf != null).
058 */
059 //@ invariant buf != null ==> endBufNdx <= buf.length;
060
061 protected int endBufNdx;
062
063 /**
064 * The index of the next character to be read from the buffer. If
065 * equal to endBufNdx, then we need to read more from the stream.
066 */
067 //@ invariant 0 <= curNdx;
068 //@ invariant curNdx <= endBufNdx;
069
070 protected int curNdx = 0;
071
072 /**
073 * The value of curNdx for the last character read, or, if no
074 * characters have been read yet, the value of curNdx.
075 *
076 * Note that because of unicode conversion, this may not be just
077 * curNdx-1. This exists because mark() marks from just before
078 * the last character read, not the current position.
079 */
080 //@ invariant 0 <= lastCharNdx;
081 //@ invariant lastCharNdx <= curNdx;
082
083 protected int lastCharNdx = curNdx;
084
085 /**
086 * For unicode conversion, we need to know if we have just seen
087 * an even or odd number of backslashes. Accordingly, we record
088 * the location of the last odd backslash read (Location.NULL if one
089 * has not been seen yet).
090 */
091
092 protected int oddSlashLoc = Location.NULL;
093
094
095 /**
096 * This constructor leaves <code>buf</code> as null.
097 */
098 //@ requires STARTFREELOC <= minLoc;
099 //@ requires minLoc <= maxLoc;
100 //@ requires minLoc-1 <= beforeBufLoc;
101 //@ ensures curNdx == 0;
102 //@ ensures !marked;
103 //@ ensures buf == null;
104 BufferedCorrelatedReader(int minLoc, int beforeBufLoc, int maxLoc) {
105 this.minLoc = minLoc;
106 this.beforeBufLoc = beforeBufLoc;
107 this.maxLoc = maxLoc;
108 }
109
110
111 /**
112 * Closes us. No other I/O operations may be called on us after
113 * we have been closed.
114 */
115 //@ also modifies buf;
116 //@ ensures buf == null;
117
118 public void close() {
119 buf = null;
120 super.close();
121 }
122
123 /**
124 * Returns the location of the last character read. If no
125 * character has been read yet, returns a whole-file location for
126 * this file.
127 */
128
129 public int getLocation() {
130 int loc = beforeBufLoc + curNdx;
131
132 if (loc<minLoc) { // no characters read yet
133 return FileCorrelatedReader.createWholeFileLoc(getFile());
134 }
135
136 if (loc>maxLoc) {
137 ErrorSet.fatal("Input file `" + getFile().getHumanName() +
138 "' is too large (maximum file size is " +
139 LocationManagerCorrelatedReader.MAXFILESIZE + " bytes).");
140 }
141
142 return loc;
143 }
144
145 /**
146 * Refills the buffer. <p>
147 *
148 * In doing so, may reallocate the buffer. <p>
149 *
150 * Returns true iff not end-of-file, and at least one character
151 * was read from the file. Throws an IOException if no
152 * characters could be read from the stream.<p>
153 *
154 * Requires we are open.<p>
155 */
156 //@ requires buf != null;
157 //@ requires curNdx == endBufNdx;
158 //@ ensures \result ==> curNdx < endBufNdx;
159
160 protected abstract boolean refillBuf() throws IOException;
161
162 /**
163 * Peeks the next character from this input stream.
164 * Does no unicode conversion. <p>
165 *
166 * Requires we are open.<p>
167 */
168 //@ requires buf != null;
169 //@ ensures 0 <= \result ==> curNdx < endBufNdx;
170
171 protected int peek() throws IOException {
172 if (curNdx == endBufNdx) {
173 // Refill buffer:
174 if (!refillBuf()) {
175 // EOF
176 return -1;
177 }
178 }
179
180 return buf[curNdx];
181 }
182
183 /**
184 * Reads the next character from this input stream.
185 * Does no unicode conversion. <p>
186 *
187 * Requires we are open.<p>
188 */
189 //@ requires buf != null;
190
191 protected int readRaw() throws IOException {
192 if (curNdx == endBufNdx) {
193 // Refill buffer:
194 if (!refillBuf()) {
195 // EOF
196 return -1;
197 }
198 }
199
200 return buf[curNdx++];
201 }
202
203 /* ************************************************
204 * *
205 * Marks: *
206 * *
207 * ************************************************/
208
209 /**
210 * The value of curNdx at the mark point (if marked is true).
211 */
212 //@ invariant marked ==> 0 <= markNdx && markNdx <= curNdx;
213
214 protected int markNdx; /*@ readable markNdx if marked; */
215
216 /**
217 * Marks the position of the current character in this input
218 * stream. A subsequent call to the <code>reset</code> method
219 * repositions this stream at the last marked position.
220 *
221 * This method differs from
222 * <code>java.io.InputStream.readlimit</code> in that it does not
223 * take a <code>readlimit</code> argument. <p>
224 *
225 * @see javafe.util.BufferedCorrelatedReader#reset()
226 * @see javafe.util.BufferedCorrelatedReader#clearMark()
227 * @see javafe.util.BufferedCorrelatedReader#createReaderFromMark
228 */
229
230 public void mark() {
231 markNdx = curNdx;
232 marked = true;
233 }
234
235 /**
236 * Removes the mark (if any) from the input stream.
237 *
238 * @see javafe.util.BufferedCorrelatedReader#mark()
239 */
240 public void clearMark() {
241 marked = false;
242 }
243
244 /**
245 * Repositions this stream to the position at the time the
246 * <code>mark</code> method was last called on this input stream. <p>
247 *
248 * Requires that the input stream had been previously marked
249 * via the <code>mark()</code> method. <p>
250 *
251 * If mark() is called before read(), then the mark will be
252 * restored to its previous value (and not the preceeding
253 * character().<p>
254 *
255 * @exception IOException if this stream is not marked.
256 * @see javafe.util.BufferedCorrelatedReader#mark()
257 */
258
259 public void reset() throws IOException {
260 if (!marked) {
261 throw new IOException("mark: CorrelatedReader not marked");
262 }
263
264 curNdx = markNdx;
265 lastCharNdx = curNdx;
266
267 // System.out.println("Reset to "+(beforeBufLoc + curNdx)+" - "
268 // +getLocation());
269
270 marked = false;
271 }
272
273 /** Returns the location of the character before the mark.
274 */
275 //@ requires marked;
276 //@ ensures STARTFREELOC-1 <= \result;
277
278 public int getBeforeMarkLocation() {
279 Assert.notFalse(marked);
280
281 return beforeBufLoc + markNdx;
282 }
283
284 /** Returns a new buffer containing the contents of this BufferedCorrelatedReader's
285 * buffer, from the marked position to the current position less
286 * <code>discard</code> bytes (not characters).
287 *
288 * Clears the mark as a side-effect. <p>
289 *
290 * @exception IndexOutOfBoundsException if <code>discard</code> is negative or exceeds the number of marked characters
291 */
292 //@ requires 0 <= discard;
293 //@ requires marked;
294 //@ modifies marked;
295 //@ ensures !marked;
296 //@ ensures \result != null;
297
298 public byte[] getBufferFromMark(int discard)
299 throws IndexOutOfBoundsException {
300
301 if (buf == null) {
302 Assert.precondition("getBufferFromMark called on a closed CorrelatedReader");
303 }
304 if (!marked) {
305 Assert.precondition("getBufferFromMark called on a " +
306 "CorrelatedReader that has not been marked");
307 }
308 if (discard < 0 || curNdx-markNdx < discard) {
309 throw new IndexOutOfBoundsException();
310 }
311
312 int start = markNdx;
313 int len = curNdx-markNdx - discard;
314
315 byte[] newBuffer = new byte[len];
316 System.arraycopy(buf, start, newBuffer, 0, len);
317
318 marked = false;
319
320 return newBuffer;
321 }
322
323 /**
324 * Creates a <code>CorrelatedReader</code> object for the input
325 * text from the marked position, to the current position. <p>
326 *
327 * Calls to <code>getLocation()</code> for characters from the
328 * new <code>CorrelatedReader</code> yield the same locations as
329 * calls to <code>getLocation()</code> for the same characters on
330 * this <code>CorrelatedReader</code>. <p>
331 *
332 * The <code>discard</code> argument specifies the number of
333 * characters to discard from the end of the
334 * sub-<code>CorrelatedReader</code>. <p>
335 *
336 * Clears the mark as a side-effect. <p>
337 *
338 * Requires that the input stream had been previously marked via
339 * the <code>mark()</code> method and that we have not been
340 * closed. <p>
341 *
342 * @exception IndexOutOfBoundsException if <code>discard</code> is negative or exceeds the number of marked characters
343 *
344 * @see javafe.util.BufferedCorrelatedReader#mark()
345 */
346
347 public CorrelatedReader createReaderFromMark(int discard)
348 throws IndexOutOfBoundsException {
349 int b4markLoc = getBeforeMarkLocation();
350 byte[] subBuffer = getBufferFromMark(discard);
351 return new SubCorrelatedReader(getFile(), subBuffer, b4markLoc);
352 }
353 }