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    }