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 \fresh(\result);
457 //@ signals_only \nothing;
458 private static String getLine(int loc) {
459 InputStream i = getFile(loc);
460 if (i==null)
461 return null;
462
463 // FIXME - why not use a buffered Reader here to read
464 // characters?
465 try {
466 /*
467 * skip to the start of the line in question:
468 */
469 long charsLeft = (Location.toOffset(loc)-1)
470 - Location.toColumn(loc);
471 // FIXME - wrong if offset is 0 - see if esc catches it
472 while ((charsLeft -= i.skip(charsLeft))>0) { // skip all but 1 byte
473 i.read(); // skip the last byte
474 charsLeft--;
475 }
476
477 // FIXME - this seems awfully inefficient
478 StringBuffer line = new StringBuffer(100);
479 for (int c=i.read(); c != '\r' && c != '\n' && c!= -1/*EOF*/; c=i.read())
480 line.append((char)c);
481
482 i.close();
483 return line.toString();
484 } catch (IOException e) {
485 return null;
486 }
487 }
488
489
490 /** See documentation for two-argument version of <code>displayColumn</code>.
491 * This version differs in that the default clip policy is applied.
492 */
493 //@ requires loc != Location.NULL;
494 //@ requires !Location.isWholeFileLoc(loc);
495 //@ modifies System.out.output;
496 //@ ensures true;
497 //@ signals_only \nothing;
498 public static void displayColumn(int loc) {
499 displayColumn(loc, null);
500 }
501
502 static private final int TABSTOP = 8;
503 /**
504 * Display (part of) the line that loc occurs on, then indicate via
505 * a caret (^) which column loc points to. <p>
506 *
507 * Tabs are expanded before the line is displayed using 8-character
508 * tab stops. 8 spaces is perhaps not what the user intended, but
509 * there will not be any other lines portrayed against which it must
510 * match, and the caret positioning will be consistent with the 8
511 * character spacing; at worst, the line will be spread out more than
512 * it would be with shorter tabs. <p>
513 *
514 * Precondition: <code>loc</code> is a regular location (e.g., not
515 * a whole-file location).<p>
516 *
517 * If an I/O error does occur, then the user is informed of the
518 * column number and that the line in question is not available; no
519 * error is reported.
520 *
521 * By using a non-null <code>policy</code> argument, a caller can fine-
522 * tune the policy used for introducing ellipses in the printed line.
523 */
524 //@ public normal_behavior
525 //@ requires loc != Location.NULL;
526 //@ requires !Location.isWholeFileLoc(loc);
527 //@ modifies System.out.output;
528 //@ ensures true;
529 public static void displayColumn(int loc, ClipPolicy policy) {
530 String line = getLine(loc);
531 int col = Location.toColumn(loc); // zero-based
532 //@ assume line != null ==> (col >= 0 && col < line.length()); // FIXME
533 if (line==null) {
534 System.out.println("(line text not available; see column "
535 + col + ")");
536 return;
537 }
538
539
540 /*
541 * Expand tabs in line, keeping col in sync:
542 */
543 StringBuffer adjusted = new StringBuffer(100);
544 int x = 0; // tab-adjusted location on line (0-based)
545 int acol = col;
546 for (int i=0; i<line.length(); i++) {
547 char c = line.charAt(i);
548 if (c != '\t') {
549 adjusted.append(c);
550 x++;
551 } else {
552 adjusted.append(' '); // Tab always non-zero skip
553 x++;
554 while (x%TABSTOP != 0) { // Skip to next tab stop
555 adjusted.append(' ');
556 x++;
557
558 if (i<col)
559 acol++;
560 }
561 }
562 }
563 line = adjusted.toString();
564 col = acol;
565
566
567 // Handle case where file has been modified since it was last read:
568 if (col>=line.length()) {
569 System.out.println("(line text no longer available; see column "
570 + col + ")");
571 return;
572 }
573
574
575 String noclipLine = line;
576 int noclipCol = col;
577 final int LINELENGTH = 80; // HACK? !!!!
578
579 /*
580 * Clip the start of line if column would otherwise be too far to
581 * the right:
582 */
583 if (col>LINELENGTH-15) {
584 int clip = col-(LINELENGTH/2 - 5);
585 //@ assert col - clip + 5 < LINELENGTH - 15;
586 col = col + 5 - clip; // This 5 is the length of " ... "
587 line = " ... " + line.substring(clip);
588 }
589
590 /*
591 * Clip the end of line if it would go past the edge of the screen:
592 */
593 if (line.length()>LINELENGTH-10) {
594 line = line.substring(0, LINELENGTH-10) + " ...";
595 } else if (policy != null &&
596 !policy.containsEndOfConstruct(noclipLine, noclipCol)) {
597 line += " ...";
598 }
599
600 System.out.println(line);
601
602 // Display a ^ where the col. # is:
603 for (int o=0; o<col; o++)
604 System.out.print(" ");
605 System.out.println("^");
606 }
607
608 /** Prints to System.out the given String (if not null)
609 and a current stack trace,
610 to be used for debugging with print statements.
611 */
612 //@ public normal_behavior
613 //@ modifies System.out.output;
614 //@ ensures true;
615 static public void dump(String s) {
616 if (s != null) System.out.println(s);
617 (new Exception()).printStackTrace();
618 }
619
620 public static interface Reporter {
621 /**
622 * Unified interface for reporting information - all messages to the
623 * user go through this method.
624 * @param severity - the severity of the condition: 0 for information
625 * 1 for warnings, 2 for errors
626 * @param loc - the location (as in @loc(javafe.util.Location))
627 * referred to by the message; Location.NULL if the message
628 * does not refer to any location in particular
629 * @param length - the length of the section of the line that should
630 * be high-lighted; -1 if the length is not known.
631 * @param message - the text message to be conveyed to the user
632 */
633 void report(int severity, int loc, int length, String message);
634
635 /** This method reports the location of an associated bit of
636 * information (e.g. the location of a referenced declaration)
637 * that goes with the most recent call of 'report'.
638 * @param loc The Location of theassociated information
639 */
640 void reportAssociatedInfo(int loc);
641 void reportAssociatedInfo2(int loc, ClipPolicy cp);
642 }
643
644 static private Reporter reporter = new StandardReporter();
645
646 /** Returns the current output reporter.
647 @return the current reporter
648 */
649 static public Reporter getReporter() {
650 return reporter;
651 }
652
653 /**
654 * Sets the reporter to be used to convey information to the user;
655 * returns the previous value of the reporter.
656 *
657 * @param r The new value of the single reporter object.
658 * @return The previous value of the reporter object.
659 */
660 public static Reporter setReporter(Reporter r) {
661 Reporter rr = reporter;
662 reporter = r;
663 return rr;
664 }
665
666 public static class StandardReporter implements Reporter {
667 public void report(int severity, int loc,
668 int length, String message) {
669 if (loc == Location.NULL) {
670 System.out.println(message);
671
672 } else {
673 System.out.print(Location.toFileName(loc) + ":");
674 if (!Location.isWholeFileLoc(loc))
675 System.out.print(Location.toLineNumber(loc) + ":");
676
677 // Display the type of the information & the information:
678 System.out.println(" " + message);
679
680 // Display which column # visually if available:
681 if (!Location.isWholeFileLoc(loc))
682 displayColumn(loc);
683 else if (message.length() == 0) {
684 System.out.println(" ( line not available )");
685 System.out.println("");
686 }
687 }
688 }
689
690 public void reportAssociatedInfo(int loc) {
691 if (loc != Location.NULL)
692 report(0, loc, -1, "Associated declaration: ");
693 }
694
695 // Alternate syntax for associated declarations - they
696 // should be unified, but that involves fixing all of the tests - FIXME
697 public void reportAssociatedInfo2(int loc, ClipPolicy cp) {
698 System.out.println("Associated declaration is "
699 + Location.toString(loc) + ":");
700 if (!Location.isWholeFileLoc(loc)) {
701 ErrorSet.displayColumn(loc, cp);
702 }
703 }
704
705
706 }
707 }