    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002    // Modifications Copyright 2004, David Cok.
    003
    004    package javafe.util;
    005
    006    import java.io.*;
    007    import javafe.FrontEndTool;
    008
    009    /**
    010     * The <code>ErrorSet</code> class is responsible for displaying
    011     * cautions, warnings, ordinary errors, and fatal errors to the user.
    012     * It maintains counts of how many cautions, warnings, and errors have
    013     * been reported so far.
    014     *
    015     * <p> Currently, reporting is done via printing all messages to
    016     * <code>System.out</code>.  Messages are accompanied by an indication
    017     * of whether they are a caution, a warning, an ordinary error, or a
    018     * fatal error.
    019     *
    020     * <p> Messages are printed as soon as they are reported.  A future
    021     * version of <code>ErrorSet</code> may group together messages
    022     * concerning the same file to be printed in location sorted order
    023     * once the file has been processed fully.  (This will require adding
    024     * some kind of <code>end_of_file(F)</code> call.)
    025     *
    026     * <p> Rough rules for determining what class to report something as:
    027     * <dl>
    028     * <dt> Error: <dd> something that is definitely wrong and which
    029     *      prevents processing everything the tool was requested to work
    030     *      on.
    031     *
    032     * <dt> Fatal Error: <dd> similar except that it prevents any further
    033     *      processing at all.  (Tools may continue after ordinary errors
    034     *      by aborting processing of some, but not all, parts of the
    035     *      input program.)
    036     *
    037     * <dt> Caution: <dd>
    038     *      (1) something that is technically illegal according to the
    039     *      language spec(s), but the tool accepts anyways for
    040     *      compatibility with other tools.  (It must not force
    041     *      aborting.) <br>
    042     *      (2) something that is not technically illegal, but is likely
    043     *      to be misleading. (The user is encouraged to adjust the
    044     *      environment or the code to remove the caution.)
    045     *
    046     * <dt> Warning: <dd>something that the Tool believes, but is not
    047     *      sure, is a serious problem - used for static checking reports.
    048     * </dl>
    049     *
    050     * @see Location
    051     * @see FatalError
    052     */
    053
    054    public class ErrorSet
    055    {
    056      // The options field must be initialized before any calls here.
    057      //@ invariant FrontEndTool.options != null;
    058
    059      // Prevent javadoc from displaying a public constructor
    060      private ErrorSet() {};
    061
    062
    063      /***************************************************
    064       *                                                 *
    065       * Class Variables:                                  *
    066       *                                                 *
    067       **************************************************/
    068
    069      /**
    070       * The number of cautions reported so far.
    071       */
    072      public static int cautions = 0;
    073
    074
    075      /**
    076       * The number of warnings reported so far.
    077       */
    078      public static int warnings = 0;
    079
    080
    081      /**
    082       * The number of errors reported so far, including fatal errors.
    083       */
    084      public static int errors = 0;
    085
    086      /**
    087       * The number of fatal errors so far (some may have been caught and handled)
    088       */
    089      public static int fatals = 0;
    090
    091      /**
    092       * If <code>gag</code> is true, then no output is produced by
    093       * <code>ErrorSet</code> methods (useful for test harnesses).
    094       *
    095       * Defaults to false.<p>
    096       */
    097      public static boolean gag = false;
    098
    099      /** Resets all error and warning counts. */
    100      public static void clear() {
    101        fatals = 0;
    102        errors = 0;
    103        warnings = 0;
    104        cautions = 0;
    105        gag = false;
    106      }
    107
    108      private static int savedErrorsWarnings;
    109      private static int savedCautions;
    110
    111      public static void mark() {
    112        savedErrorsWarnings = errors + warnings;
    113        savedCautions = cautions;
    114      }
    115
    116      public static boolean errorsSinceMark() {
    117        return errors + warnings > savedErrorsWarnings;
    118      }
    119
    120      public static boolean cautionsSinceMark() {
    121        return cautions > savedCautions;
    122      }
    123
    124      /***************************************************
    125       *                                                 *
    126       * Reporting entry points:                           *
    127       *                                                 *
    128       **************************************************/
    129
    130      /**
    131       * Report a caution. <p>
    132       *
    133       * The message will be marked as a caution when it is displayed to
    134       * the user.  Increments <code>cautions</code> by one.<p>
    135       */
    136      //@ requires msg != null;
    137      //@ modifies cautions, System.out.output;
    138      //@ ensures gag ==> \not_modified(System.out.output);
    139      //@ ensures FrontEndTool.options.noCautions ==> \not_modified(System.out.output);
    140      public static void caution(String msg) {
    141        if (FrontEndTool.options.noCautions) {
    142
    143          return;
    144        }
    145        cautions++;
    146        report(CAUTION, msg);
    147      }
    148
    149      /**
    150       * Report a caution associated with a location. <p>
    151       *
    152       * Precondition: <code>loc</code> must be a regular location or a
    153       * whole file location.<p>
    154       *
    155       * The message will be marked as a caution when it is displayed to
    156       * the user.  Increments <code>cautions</code> by one.<p>
    157       */
    158      //@ requires loc != Location.NULL;
    159      //@ requires msg != null;
    160      //@ modifies cautions, System.out.output;
    161      public static void caution(int loc, String msg) {
    162        if (FrontEndTool.options.noCautions) {
    163          return;
    164        }
    165        cautions++;
    166        report(loc, CAUTION, msg);
    167      }
    168
    169      //@ requires loc != Location.NULL;
    170      //@ requires msg != null;
    171      //@ modifies cautions, System.out.output;
    172      public static void caution(int loc, String msg, int addLoc) {
    173        if (FrontEndTool.options.noCautions) {
    174          return;
    175        }
    176        cautions++;
    177        report(loc, CAUTION, msg);
    178        assocLoc(addLoc);
    179      }
    180
    181
    182      /**
    183       * Report a warning. <p>
    184       *
    185       * The message will be marked as a warning when it is displayed to
    186       * the user.  Increments <code>warnings</code> by one.<p>
    187       */
    188      //@ requires msg != null;
    189      //@ modifies warnings, System.out.output;
    190      public static void warning(String msg) {
    191        warnings++;
    192        report(WARNING, msg);
    193      }
    194
    195      /**
    196       * Report a warning associated with a location. <p>
    197       *
    198       * Precondition: <code>loc</code> must be a regular location or a
    199       * whole file location.<p>
    200       *
    201       * The message will be marked as a warning when it is displayed to
    202       * the user.  Increments <code>warnings</code> by one.<p>
    203       */
    204      //@ requires loc != Location.NULL;
    205      //@ requires msg != null;
    206      //@ modifies warnings, System.out.output;
    207      public static void warning(int loc, String msg) {
    208        warnings++;
    209        report(loc, WARNING, msg);
    210      }
    211
    212
    213      /**
    214       * Report an ordinary error. <p>
    215       *
    216       * The message will be marked as an error when it is displayed to
    217       * the user.  Increments <code>errors</code> by one.<p>
    218       */
    219      //@ requires msg != null;
    220      //@ modifies errors, System.out.output;
    221      public static void error(String msg) {
    222        errors++;
    223        report(ERROR, msg);
    224      }
    225
    226      /**
    227       * Report an ordinary error associated with a location. <p>
    228       *
    229       * Precondition: <code>loc</code> must be a regular location or a
    230       * whole file location.<p>
    231       *
    232       * The message will be marked as an error when it is displayed to
    233       * the user.  Increments <code>errors</code> by one. <p>
    234       */
    235      //@ requires loc != Location.NULL;
    236      //@ requires msg != null;
    237      //@ modifies errors, System.out.output;
    238      public static void error(int loc, String msg) {
    239        errors++;
    240        report(loc, ERROR, msg);
    241      }
    242
    243      //@ requires loc != Location.NULL;
    244      //@ requires msg != null;
    245      //@ modifies errors, System.out.output;
    246      public static void error(int loc, String msg, int addLoc) {
    247        errors++;
    248        report(loc, ERROR, msg);
    249        assocLoc(addLoc);
    250      }
    251
    252      //@ modifies System.out.output;
    253      public static void assocLoc(int loc) {
    254        if (loc != Location.NULL)
    255          reporter.reportAssociatedInfo(loc);
    256      }
    257
    258      /**
    259       * Report a fatal error.  Warning: This method does not
    260       * return normally!<p>
    261       *
    262       * The variable <code>errors</code> is incremented by one, the
    263       * error reported as a fatal error, and then an unchecked
    264       * <code>FatalError</code> exception is thrown.  The top level of a
    265       * <code>Tool</code> is responsible for catching the
    266       * <code>FatalError</code>, so that it can do whatever cleanup is
    267       * required before exiting.<p>
    268       */
    269      //@ requires msg != null;
    270      //@ modifies fatals, errors, System.out.output;
    271      //@ ensures false;
    272      //@ signals (Exception) fatals == \old(fatals)+1;
    273      //@ signals (Exception) errors == \old(errors)+1;
    274      //@ signals_only FatalError;
    275      public static void fatal(String msg) /*throws FatalError*/ {
    276        if (msg != null) {
    277          fatals++;
    278          errors++;
    279          report(FATALERROR, msg);
    280        }
    281        throw new FatalError();
    282      }                 //@ nowarn Exception;
    283
    284      /**
    285       * Report a fatal error associated with a location.  Warning: This
    286       * method does not return normally!<p>
    287       *
    288       * Precondition: <code>loc</code> must be a regular location or a
    289       * whole file location.<p>
    290       *
    291       * The variable <code>errors</code> is incremented by one, the
    292       * error reported as a fatal error, and then an unchecked
    293       * <code>FatalError</code> exception is thrown.  The top level of a
    294       * <code>Tool</code> is responsible for catching the
    295       * <code>FatalError</code>, so that it can do whatever cleanup is
    296       * required before exiting.<p>
    297       */
    298      //@ requires loc != Location.NULL;
    299      //@ requires msg != null;
    300      //@ modifies fatals, errors, System.out.output;
    301      //@ ensures false;
    302      //@ signals (Exception) fatals == \old(fatals)+1;
    303      //@ signals (Exception) errors == \old(errors)+1;
    304      //@ signals_only FatalError;
    305      public static void fatal(int loc, String msg) /*throws FatalError*/ {
    306        fatals++;
    307        errors++;
    308        report(loc, FATALERROR, msg);
    309        throw new FatalError();
    310      }                             //@ nowarn Exception;
    311
    312      /** Special call to report unimplemented features, so they can be caught
    313          and handled more easily.
    314      */
    315      // FIXME - do we need this?
    316      //@ requires msg != null;
    317      //@ requires loc != Location.NULL;
    318      //@ modifies System.out.output;
    319      //@ ensures false;
    320      //@ signals_only NotImplementedException;
    321      public static void notImplemented(boolean print, int loc, String msg) {
    322        if (print) report(loc, "Not implemented", msg);
    323        throw new NotImplementedException(msg);
    324      }                             //@ nowarn Exception;
    325
    326      /***************************************************
    327       *                                                 *
    328       * Common code for reporting:                *
    329       *                                                 *
    330       **************************************************/
    331
    332      // Constants for use as the type field of report:
    333
    334      private static /*@ non_null */ final String CAUTION           = "Caution";
    335      private static /*@ non_null */ final String WARNING           = "Warning";
    336      private static /*@ non_null */ final String ERROR             = "Error";
    337      private static /*@ non_null */ final String FATALERROR        = "Fatal error";
    338
    339
    340      /**
    341       * Report general information.
    342       *
    343       * <p> Type contains a non-null String describing the type of the
    344       * information (usually one of the above constants).  The
    345       * information itself is contained in the non-null String
    346       * msg.
    347       *
    348       * <p> This function is not responsible for incrementing counts or
    349       * other ErrorSet functionality.
    350       */
    351      //@ requires msg != null && type != null;
    352      //@ requires javafe.Tool.options != null;
    353      //@ modifies System.out.output;
    354      //@ ensures gag ==> \not_modified(System.out.output);
    355      private static void report(/*@ non_null */ String type, /*@ non_null */ String msg) {
    356        if (!gag)
    357          report(type + ": " + msg);
    358
    359        // Hack so we can see where error occurred, for debugging:
    360        if (javafe.Tool.options.showErrorLocation) dump(null); //@nowarn Modifies;
    361        // Ignore the modifications caused by the debugging line
    362
    363      } //@ nowarn Post; // dump does not satisfy the postcondition
    364
    365      /**
    366       *  Reports a general message, implemented here in order to
    367       *  have a single location through which error reporting happens.
    368       */
    369      //@ requires msg != null;
    370      //@ modifies System.out.output;
    371      public static void report(/*@ non_null @*/ String msg) {
    372        reporter.report(0,Location.NULL,-1,msg);
    373      }
    374
    375
    376      /**
    377       * Report information associated with a location. <p>
    378       *
    379       * Type contains a non-null String describing the type of the
    380       * information (usually one of the above constants).  The
    381       * information itself is contained in the non-null String
    382       * msg.<p>
    383       *
    384       * Precondition: <code>loc</code> must be a regular location or a
    385       * whole file location.<p>
    386       *
    387       * This function is not responsible for incrementing counts or
    388       * other ErrorSet functionality.<p>
    389       */
    390      //@ requires msg != null && type != null;
    391      //@ requires loc != Location.NULL;
    392      //@ modifies System.out.output;
    393      private static void report(int loc, String type, String msg) {
    394        if (gag)
    395          return;
    396
    397        // Hack so we can see where error occurred, for debugging:
    398        if (javafe.Tool.options.showErrorLocation) dump(null); //@ nowarn Modifies;
    399        // Ignore the modifications caused by the debugging line
    400
    401        if (loc==Location.NULL) {
    402          errors++;
    403          report("INTERNAL ERROR: ",
    404                 "NULL location erroneously passed to ErrorSet;"
    405                 + " Associated information is `" + type
    406                 + ": " + msg + "'");
    407        }
    408
    409        // Display the file human-readable name and line # if available:
    410
    411        reporter.report(0,loc,-1,type + ": " + msg);
    412
    413      }
    414
    415
    416      /***************************************************
    417       *                                                 *
    418       * Utility routines:                         *
    419       *                                                 *
    420       **************************************************/
    421
    422      /**
    423       * Return a new InputStream for the file that loc refers to or null
    424       * if an I/O error occurs while attempting to open the stream. <p>
    425       *
    426       * Precondition: <code>loc</code> must be a regular location or a
    427       * whole file location.<p>
    428       *
    429       * No error is reported if an I/O error occurs.
    430       */
    431      //@ requires loc != Location.NULL;
    432      //---@ modifies \nothing;
    433      //@ ensures \result != null ==> \result.isOpen;
    434      //@ ensures \fresh(\result); // FIXME - not sure about this
    435      //@ signals_only \nothing;
    436      private static InputStream getFile(int loc) {
    437        try {
    438          return Location.toFile(loc).getInputStream();
    439        } catch (IOException e) {
    440          return null;
    441        }
    442      }
    443
    444
    445      /**
    446       * Return the line loc refers to or null if an I/O error occurs
    447       * while attempting to read the line in. <p>
    448       *
    449       * Precondition: <code>loc</code> is a regular location (e.g., not
    450       * a whole-file location).<p>
    451       *
    452       * No error is reported if an I/O error occurs.
    453       */
    454      //@ requires loc != Location.NULL;
    455      //@ modifies \nothing;
    456      //@ ensures true;
    457      //@ ensures \fresh(\result);
    458      //@ signals_only \nothing;
    459      private static String getLine(int loc) {
    460        InputStream i = getFile(loc);
    461        if (i==null)
    462          return null;
    463
    464        // FIXME - why not use a buffered Reader here to read
    465        // characters?
    466        try {
    467          /*
    468           * skip to the start of the line in question:
    469           */
    470          long charsLeft = (Location.toOffset(loc)-1)
    471            - Location.toColumn(loc);
    472          // FIXME - wrong if offset is 0 - see if esc catches it
    473          while ((charsLeft -= i.skip(charsLeft))>0) { // skip all but 1 byte
    474            i.read();  // skip the last byte
    475            charsLeft--;
    476          }
    477
    478          // FIXME - this seems awfully inefficient
    479          StringBuffer line = new StringBuffer(100);
    480          for (int c=i.read(); c != 10/*newline*/ && c!= -1/*EOF*/; c=i.read())
    481            line.append((char)c);
    482
    483          i.close();
    484          return line.toString();
    485        } catch (IOException e) {
    486          return null;
    487        }
    488      }
    489
    490
    491      /** See documentation for two-argument version of <code>displayColumn</code>.
    492       * This version differs in that the default clip policy is applied.
    493       */
    494      //@ requires loc != Location.NULL;
    495      //@ requires !Location.isWholeFileLoc(loc);
    496      //@ modifies System.out.output;
    497      //@ ensures true;
    498      //@ signals_only \nothing;
    499      public static void displayColumn(int loc) {
    500        displayColumn(loc, null);
    501      }
    502
    503      static private final int TABSTOP = 8;
    504      /**
    505       * Display (part of) the line that loc occurs on, then indicate via
    506       * a caret (^) which column loc points to. <p>
    507       *
    508       * Tabs are expanded before the line is displayed using 8-character
    509       * tab stops.  8 spaces is perhaps not what the user intended, but
    510       * there will not be any other lines portrayed against which it must
    511       * match, and the caret positioning will be consistent with the 8
    512       * character spacing; at worst, the line will be spread out more than
    513       * it would be with shorter tabs. <p>
    514       *
    515       * Precondition: <code>loc</code> is a regular location (e.g., not
    516       * a whole-file location).<p>
    517       *
    518       * If an I/O error does occur, then the user is informed of the
    519       * column number and that the line in question is not available; no
    520       * error is reported.
    521       *
    522       * By using a non-null <code>policy</code> argument, a caller can fine-
    523       * tune the policy used for introducing ellipses in the printed line.
    524       */
    525      //@ public normal_behavior
    526      //@ requires loc != Location.NULL;
    527      //@ requires !Location.isWholeFileLoc(loc);
    528      //@ modifies System.out.output;
    529      //@ ensures true;
    530      public static void displayColumn(int loc, ClipPolicy policy) {
    531        String line = getLine(loc);
    532        int col = Location.toColumn(loc);     // zero-based
    533        //@ assume line != null ==> (col >= 0 && col < line.length());  // FIXME
    534        if (line==null) {
    535          System.out.println("(line text not available; see column "
    536                             + col + ")");
    537          return;
    538        }
    539
    540
    541        /*
    542         * Expand tabs in line, keeping col in sync:
    543         */
    544        StringBuffer adjusted = new StringBuffer(100);
    545        int x = 0;          // tab-adjusted location on line (0-based)
    546        int acol = col;
    547        for (int i=0; i<line.length(); i++) {
    548          char c = line.charAt(i);
    549          if (c != '\t') {
    550            adjusted.append(c);
    551            x++;
    552          } else {
    553            adjusted.append(' ');           // Tab always non-zero skip
    554            x++;
    555            while (x%TABSTOP != 0) {        // Skip to next tab stop
    556              adjusted.append(' ');
    557              x++;
    558
    559              if (i<col)
    560                acol++;
    561            }
    562          }
    563        }
    564        line = adjusted.toString();
    565        col = acol;
    566
    567
    568        // Handle case where file has been modified since it was last read:
    569        if (col>=line.length()) {
    570          System.out.println("(line text no longer available; see column "
    571                             + col + ")");
    572          return;
    573        }
    574
    575
    576        String noclipLine = line;
    577        int noclipCol = col;
    578        final int LINELENGTH = 80;  // HACK? !!!!
    579
    580        /*
    581         * Clip the start of line if column would otherwise be too far to
    582         * the right:
    583         */
    584        if (col>LINELENGTH-15) {
    585          int clip = col-(LINELENGTH/2 - 5);
    586          //@ assert col - clip + 5 < LINELENGTH - 15;
    587          col = col + 5 - clip; // This 5 is the length of " ... "
    588          line = " ... " + line.substring(clip);
    589        }
    590
    591        /*
    592         * Clip the end of line if it would go past the edge of the screen:
    593         */
    594        if (line.length()>LINELENGTH-10) {
    595          line = line.substring(0, LINELENGTH-10) + " ...";
    596        } else if (policy != null &&
    597                   !policy.containsEndOfConstruct(noclipLine, noclipCol)) {
    598          line += " ...";
    599        }
    600
    601        System.out.println(line);
    602
    603        // Display a ^ where the col. # is:
    604        for (int o=0; o<col; o++)
    605          System.out.print(" ");
    606        System.out.println("^");
    607      }
    608
    609      /** Prints to System.out the given String (if not null)
    610          and a current stack trace,
    611          to be used for debugging with print statements.
    612      */
    613      //@ public normal_behavior
    614      //@ modifies System.out.output;
    615      //@ ensures true;
    616      static public void dump(String s) {
    617        if (s != null) System.out.println(s);
    618        (new Exception()).printStackTrace();
    619      }
    620
    621      public static interface Reporter {
    622        /**
    623         * Unified interface for reporting information - all messages to the
    624         * user go through this method.
    625         * @param severity - the severity of the condition: 0 for information
    626         *  1 for warnings, 2 for errors
    627         * @param loc - the location (as in @loc(javafe.util.Location))
    628         *  referred to by the message; Location.NULL if the message
    629         *  does not refer to any location in particular
    630         * @param length - the length of the section of the line that should
    631         *  be high-lighted; -1 if the length is not known.
    632         * @param message - the text message to be conveyed to the user
    633         */
    634        void report(int severity, int loc, int length, String message);
    635
    636        /** This method reports the location of an associated bit of
    637         *  information (e.g. the location of a referenced declaration)
    638         *  that goes with the most recent call of 'report'.
    639         * @param loc The Location of theassociated information
    640         */
    641        void reportAssociatedInfo(int loc);
    642        void reportAssociatedInfo2(int loc, ClipPolicy cp);
    643      }
    644
    645      static private Reporter reporter = new StandardReporter();
    646
    647      /** Returns the current output reporter.
    648          @return the current reporter
    649      */
    650      static public Reporter getReporter() {
    651        return reporter;
    652      }
    653
    654      /**
    655       * Sets the reporter to be used to convey information to the user;
    656       * returns the previous value of the reporter.
    657       *
    658       * @param r The new value of the single reporter object.
    659       * @return  The previous value of the reporter object.
    660       */
    661      public static Reporter setReporter(Reporter r) {
    662        Reporter rr = reporter;
    663        reporter = r;
    664        return rr;
    665      }
    666
    667      public static class StandardReporter implements Reporter {
    668        public void report(int severity, int loc,
    669                           int length, String message) {
    670          if (loc == Location.NULL) {
    671            System.out.println(message);
    672
    673          } else {
    674            System.out.print(Location.toFileName(loc) + ":");
    675            if (!Location.isWholeFileLoc(loc))
    676              System.out.print(Location.toLineNumber(loc) + ":");
    677
    678            // Display the type of the information & the information:
    679            System.out.println(" " + message);
    680
    681            // Display which column # visually if available:
    682            if (!Location.isWholeFileLoc(loc))
    683              displayColumn(loc);
    684            else if (message.length() == 0) {
    685              System.out.println("                ( line not available )");
    686              System.out.println("");
    687            }
    688          }
    689        }
    690
    691        public void reportAssociatedInfo(int loc) {
    692          if (loc != Location.NULL)
    693            report(0, loc, -1, "Associated declaration: ");
    694        }
    695
    696        // Alternate syntax for associated declarations - they
    697        // should be unified, but that involves fixing all of the tests - FIXME
    698        public void reportAssociatedInfo2(int loc, ClipPolicy cp) {
    699          System.out.println("Associated declaration is "
    700                             + Location.toString(loc) + ":");
    701          if (!Location.isWholeFileLoc(loc)) {
    702            ErrorSet.displayColumn(loc, cp);
    703          }
    704        }
    705
    706
    707      }
    708    }