001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package javafe.util;
004
005 import javafe.genericfile.GenericFile;
006
007 import java.util.Vector;
008 import java.io.IOException;
009
010 /**
011 * This <code>CorrelatedReader</code> class manages the allocation of
012 * location numbers.
013 */
014
015 public abstract class LocationManagerCorrelatedReader
016 extends BufferedCorrelatedReader
017 {
018 // Represents the internal state - changes to this should be
019 // benevolent side effects.
020 //@ public model JMLDataGroup internalState;
021
022 /* ************************************************
023 * *
024 * Class variables & constants: *
025 * *
026 * ************************************************/
027
028 /**
029 * The next location to be allocated to a LocationManagerCorrelatedReader
030 * instance. (The next instance's stream will have locations in a prefix of
031 * [freeLoc, freeLoc+MAXFILESIZE).) <p>
032 *
033 * We do not use ints below STARTFREELOC to denote locations. If
034 * freeLoc+MAXFILESIZE results in an overflow, then too many
035 * LocationManagerCorrelatedReader instances have been created and an
036 * assertion failure occurs.
037 */
038 //@ invariant STARTFREELOC <= freeLoc;
039
040 //@ spec_public
041 private static int freeLoc = STARTFREELOC;
042
043 /**
044 * A location is an integer that encodes file/line/column/offset
045 * information. When a LocationManagerCorrelatedReader is created,
046 * we allocate MAXFILESIZE locations for its stream. An assertion
047 * failure will occur if a location is requested for a character
048 * located at an offset greater than or equal to MAXFILESIZE.
049 */
050
051 static final int MAXFILESIZE = 30000000;
052
053 /**
054 * Each LocationManagerCorrelatedReader has a "new line offset
055 * array", or NLOA, that contains the offset of the beginning of
056 * each line. This array allows us to map an offset to line or
057 * column information. <p>
058 *
059 * NLOA is defined for indexes in [0..curLineNo). <p>
060 *
061 * If NLOA[i], i in [0..curLineNo), = j, then the characters at
062 * offset j and j-1 were on different lines. Furthermore, either
063 * (a) i=j=0, or
064 * (b) i>0, j>0, and the character at offset j-1 is a newline. <p>
065 *
066 * Note: this means a line ends just *after* a newline, not before. <p>
067 */
068 //@ invariant curLineNo <= NLOA.length;
069 /*@ invariant (\forall int i; 0 <= i && i < curLineNo ==> 0 <= NLOA[i]); */
070
071 /*@ spec_public */ private /*@ non_null */ int[] NLOA; //@ in internalState;
072
073 /** The default initial size to allocate an NLOA array */
074 //@ invariant NLOA_DEFAULT_SIZE <= NLOA.length;
075
076 private static final int NLOA_DEFAULT_SIZE = 200;
077
078 protected int streamid;
079
080 /**
081 * This constructor allocates a range of location for use by the
082 * CorrelatedReader.
083 */
084 //@ ensures curNdx == 0;
085 //@ ensures !marked;
086 //@ ensures !isWholeFile;
087 //@ ensures buf == null;
088 LocationManagerCorrelatedReader() {
089 // Allocate locations for us:
090 super(/*minLoc*/ freeLoc, /*beforeBufLoc*/ freeLoc-1,
091 /*maxLoc*/ freeLoc+MAXFILESIZE);
092 freeLoc += MAXFILESIZE;
093
094 if (freeLoc<0) {
095 long limit = (1L<<32 - STARTFREELOC) / MAXFILESIZE;
096 ErrorSet.fatal("javafe.util.LocationManagerCorrelatedReader "
097 + "maximum # of files limit (~"+limit+") exceeded");
098 }
099
100 this.NLOA = new int[NLOA_DEFAULT_SIZE];
101 this.NLOA[0] = 0;
102
103 streamid = allCorrStreams.size();
104 allCorrStreams.addElement(this);
105 }
106
107
108 /**
109 * Closes us. No other I/O operations may be called on us after
110 * we have been closed.
111 */
112
113 //@ also protected normal_behavior
114 //@ assignable maxLoc;
115 public void close() {
116 if (maxLoc == freeLoc) {
117 maxLoc = beforeBufLoc + curNdx + 1;
118 freeLoc = maxLoc;
119 }
120 super.close();
121 }
122
123 /** Records a newline at the current location.
124 */
125 //@ modifies NLOA;
126 //@ ensures curLineNo < NLOA.length;
127 //@ ensures 0 <= NLOA[curLineNo];
128
129 protected void recordNewLineLocation() {
130 if (curLineNo == NLOA.length) {
131 int[] new_NLOA = new int[ 2*NLOA.length ];
132 System.arraycopy( NLOA, 0, new_NLOA, 0, NLOA.length );
133 NLOA = new_NLOA;
134 }
135 //@ assert curLineNo < NLOA.length;
136 NLOA[ curLineNo ] = beforeBufLoc + curNdx + 1 - minLoc;
137 }
138
139 /**
140 * A static Vector containing all LocationManagerCorrelatedReader
141 * instances, in the order they were allocated, which is used to
142 * map a given location to a corresponding LocationManagerCorrelatedReader
143 * instance. <p>
144 *
145 * A location's streamId is its index in allCorrStreams. See
146 * locToStreamId(int) for the algorithm mapping locations to
147 * streamId's.
148 */
149 //@ invariant !allCorrStreams.containsNull;
150 //@ invariant allCorrStreams.elementType == \type(LocationManagerCorrelatedReader);
151
152 /*@spec_public*/ private static /*@ non_null @*/ Vector allCorrStreams = new Vector();
153
154 /**
155 * Creates and returns a vector that associates file numbers
156 * to file names.
157 */
158 //@ ensures \result != null;
159 //@ ensures \result.elementType == \type(String);
160 //@ ensures !\result.containsNull;
161
162 public static Vector fileNumbersToNames() {
163 Vector v = new Vector();
164 //@ set v.elementType = \type(String);
165 //@ set v.containsNull = false;
166 for(int i = 0; i < allCorrStreams.size(); i++) {
167 LocationManagerCorrelatedReader s = getCorrStreamAt(i);
168 v.addElement(s.getFile().getHumanName());
169 }
170 return v;
171 }
172
173 /* ************************************************
174 * *
175 * Inspecting Locations: *
176 * *
177 * *
178 * These methods are mostly package-protected. *
179 * The Location class provides access to these *
180 * methods. *
181 * *
182 * ************************************************/
183
184 /**
185 * Return the LocationManagerCorrelatedReader associated with
186 * streamId i. <p>
187 *
188 * If i is not a valid streamId (aka, i not in
189 * [0, allCorrStreams.size()) ), an assertion failure occurs. <p>
190 */
191 //@ requires 0 <= i && i < allCorrStreams.elementCount;
192 //@ modifies \nothing;
193 //@ ensures \result != null;
194
195 protected static LocationManagerCorrelatedReader getCorrStreamAt(int i) {
196 try {
197 LocationManagerCorrelatedReader c =
198 (LocationManagerCorrelatedReader)allCorrStreams.elementAt(i);
199
200 return c;
201 } catch (ArrayIndexOutOfBoundsException e) {
202 Assert.precondition("invalid streamId " + i);
203 return null; // dummy return
204 }
205 }
206
207 /**
208 * Attempt to return the valid regular location associated with a
209 * given streamId, line #, and col #. <p>
210 *
211 * If there is no such location currently in existence, an
212 * assertion failure will occur. <p>
213 *
214 * This method is intended mainly for debugging purposes. <p>
215 */
216 //@ requires 0 <= streamId && streamId < allCorrStreams.elementCount;
217 //@ requires 0 < line;
218 //@ requires 0 <= col;
219 //@ ensures \result != Location.NULL;
220
221 static int makeLocation(int streamId, int line, int col) {
222 LocationManagerCorrelatedReader s = getCorrStreamAt(streamId);
223
224 if (s.isWholeFile) {
225 return s.minLoc;
226 //Assert.fail("streamId denotes a whole file location");
227 }
228
229 if (line>s.curLineNo) {
230 System.out.println("INTERNAL ERROR: invalid request to form a location (out of range line number): " + streamId + " " + line + " " + col + " " + streamIdToFile(streamId).getHumanName());
231 line = 1; col = 0;
232 }
233
234 if ((line==s.curLineNo && col+1>s.curNdx) ||
235 (line != s.curLineNo && col+1>(s.NLOA[line]-s.NLOA[line-1]))) {
236 System.out.println("INTERNAL ERROR: invalid request to form a location (out of range column number): " + streamId + " " + line + " " + col + " " + streamIdToFile(streamId).getHumanName());
237 col = 0;
238 }
239
240 int loc;
241 if (line == 0) {
242 loc = s.minLoc + col;
243 } else {
244 loc = s.minLoc + s.NLOA[line-1] + col;
245 }
246
247 // Verify we got the right location:
248 if (locToStreamId(loc) != streamId ||
249 locToColumn(loc) != col ||
250 locToLineNumber(loc) != line) {
251 Assert.fail("bug found in makeLocation");
252 }
253
254 return loc;
255 }
256
257 /**
258 * Return the LocationManager CorrelatedReader instance associated
259 * with location loc. <p>
260 *
261 * Requires that loc be a valid location. <p>
262 */
263 //@ requires loc != Location.NULL;
264 //@ modifies \nothing;
265 //@ ensures \result != null;
266 //@ ensures \result.minLoc <= loc && loc <= \result.beforeBufLoc + \result.curNdx;
267
268 protected static LocationManagerCorrelatedReader locToStream(int loc) {
269 int i = locToStreamId(loc);
270 LocationManagerCorrelatedReader s = getCorrStreamAt(i);
271 Assert.notFalse(s.minLoc <= loc && loc <= s.beforeBufLoc + s.curNdx); //@ nowarn Pre;
272 return s;
273 }
274
275 /**
276 * Returns the internal stream ID used for the stream associated
277 * with location <code>loc</code>.
278 *
279 * Requires that loc be a valid location. <p>
280 */
281 //@ normal_behavior
282 //@ requires loc != Location.NULL;
283 //@ modifies \nothing;
284 //@ ensures 0 <= \result && \result < allCorrStreams.elementCount;
285 static int locToStreamId(int loc) {
286 // This is somewhat inefficient:
287 for(int i = 0; i < allCorrStreams.size(); i++) {
288 LocationManagerCorrelatedReader s = getCorrStreamAt(i);
289 if (s.minLoc <= loc && loc <= s.beforeBufLoc + s.curNdx) {
290 return i;
291 }
292 }
293
294 // Bad location:
295 Assert.precondition("Bad location "+loc);
296 return -1; // dummy return
297 }
298
299 /**
300 * Is a location a whole file location?
301 *
302 * Requires that loc be a valid location or NULL. <p>
303 */
304
305 //@ modifies \nothing;
306 static boolean isWholeFileLoc(int loc) {
307 if (loc == Location.NULL) {
308 return false;
309 }
310 return locToStream(loc).isWholeFile;
311 }
312
313 /**
314 * Returns the offset associated with location
315 * <code>loc</code>. <p>
316 *
317 * Requires that loc be a valid regular location (regular ==> not
318 * a whole-file location). <p>
319 *
320 * Note: offsets start with 1 (a la emacs). <p>
321 */
322 //@ requires loc != Location.NULL;
323
324 static int locToOffset(int loc) {
325 if (isWholeFileLoc(loc)) {
326 Assert.precondition("locToOffset passed a whole-file location");
327 }
328
329 LocationManagerCorrelatedReader s = locToStream(loc);
330 return loc - s.minLoc + 1;
331 }
332
333 /**
334 * Returns the line number associated with location
335 * <code>loc</code>. <p>
336 *
337 * Requires that loc be a valid regular location (regular ==> not
338 * a whole-file location). <p>
339 *
340 * Note: line numbers start with 1 (a la emacs). <p>
341 */
342 //@ requires loc != Location.NULL;
343 //@ ensures 1 <= \result;
344
345 static int locToLineNumber(int loc) {
346 return locToColOrLine(loc, false);
347 }
348
349 /**
350 * Returns the column number associated with location
351 * <code>loc</code>. <p>
352 *
353 * Requires that loc be a valid regular location (regular ==> not
354 * a whole-file location). <p>
355 *
356 * Note: column numbers start with 0. <p>
357 */
358 //@ requires loc != Location.NULL;
359 //@ ensures 0 <= \result;
360
361 static int locToColumn(int loc) {
362 return locToColOrLine(loc, true);
363 }
364
365 /**
366 * Returns the column number (if wantColumn) or line number (if
367 * !wantColumn) associated with location <code>loc</code>. <p>
368 *
369 * Requires that loc be a valid regular location (regular ==> not
370 * a whole-file location). <p>
371 *
372 * Note: line numbers start with 1 (a la emacs), while column
373 * numbers start with 0. <p>
374 */
375 //@ requires loc != Location.NULL;
376 //@ ensures 0 <= \result;
377 //@ ensures !wantColumn ==> 1 <= \result;
378
379 private static int locToColOrLine(int loc, boolean wantColumn) {
380 LocationManagerCorrelatedReader s = locToStream(loc);
381 int offset = loc - s.minLoc;
382
383 for (int i = s.curLineNo-1; /* Have sentinel s.NLOA[0]==0 */; i--) {
384 if( s.NLOA[i] <= offset ) {
385 // Line i+1 begins before offset
386 return wantColumn ? offset-s.NLOA[i] : i+1;
387 }
388 }
389 }
390
391 /**
392 * Returns the GenericFile associated with stream id
393 * <code>id</code>, where <code>id</code> has previously been
394 * returned by <code>locToStreamId</code>.
395 *
396 * Requires that id be a valid streamId.
397 */
398 //@ requires 0 <= id && id < allCorrStreams.elementCount;
399
400 static GenericFile streamIdToFile(int id) {
401 return getCorrStreamAt(id).getFile();
402 }
403
404 /**
405 * Returns the GenericFile associated with location
406 * <code>loc</code>. <p>
407 *
408 * Requires that id be a valid streamId of a FileCorrelatedReader. <p>
409 */
410 //@ requires loc != Location.NULL;
411 //@ ensures \result != null;
412
413 static GenericFile locToFile(int loc) {
414 return locToStream(loc).getFile();
415 }
416
417
418 /* ************************************************
419 * *
420 * Whole-file correlated readers: *
421 * *
422 * ************************************************/
423
424 /**
425 * Are all of our locations whole-file locations?
426 */
427 /*@spec_public*/ protected boolean isWholeFile = false;
428
429 //@ invariant isWholeFile ==> buf==null;
430
431
432 /* ************************************************
433 * *
434 * Stuff related to counting lines: *
435 * *
436 * ************************************************/
437
438 /**
439 * The total # of lines that have been read so far by all
440 * FileCorrelatedReaders. <p>
441 *
442 * This is not used internally, and is kept only for interested
443 * clients.
444 */
445
446 public static int totalLinesRead = 0;
447
448 /**
449 * The current line number; that is, the number of <newlines>
450 * we've read from our stream so far + 1. <p>
451 *
452 * (Line numbers are counted from 1 not 0.) <p>
453 */
454 //@ invariant 1 <= curLineNo;
455
456 protected int curLineNo = 1;
457
458 /**
459 * The value of curLineNo at the mark point (if marked is true). <p>
460 *
461 * The justification for why it's okay to place the following invariant
462 * in this class, even though <code>marked</code> is declared in the
463 * superclass, is that this class overrides the methods that set
464 * <code>marked</code> to <code>true</code>. (But there's no mechanical
465 * check that this justification is upheld, so it needs to be upheld
466 * manually.)
467 */
468 //@ invariant marked ==> 0 < markLineNo && markLineNo <= curLineNo;
469
470 //@ spec_public
471 private int markLineNo; /*@ readable markLineNo if marked; */
472
473 public void mark() {
474 markLineNo = curLineNo;
475 super.mark();
476 }
477
478 public void reset() throws IOException {
479 curLineNo = markLineNo;
480 super.reset();
481 }
482
483 /* ************************************************
484 * *
485 * Misc: *
486 * *
487 * ************************************************/
488
489 public /*@non_null*/String toString() {
490 StringBuffer r = new StringBuffer("LocationManagerCorrelatedReader: \"");
491 r.append(getFile().getHumanName());
492 r.append("\" ");
493
494 if (buf == null) {
495 r.append("closed");
496 } else {
497 r.append("buf[");
498 for(int i=curNdx; i<endBufNdx; i++ )
499 r.append( ""+(char)buf[i] );
500 r.append("] "+marked);
501 }
502
503 return r.toString();
504 }
505
506 static public void clear() {
507 freeLoc = STARTFREELOC;
508 totalLinesRead = 0;
509 allCorrStreams = new Vector();
510 }
511 }