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 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 }