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    }