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 }