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    }