    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    }