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 }