    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    }