001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava; 004 005 import java.util.Enumeration; 006 import java.util.Vector; 007 import java.io.*; 008 009 import javafe.ast.*; 010 import escjava.ast.*; 011 import javafe.tc.OutsideEnv; 012 import escjava.ast.EscPrettyPrint; 013 import escjava.ast.TagConstants; 014 import escjava.ast.Modifiers; 015 016 import escjava.backpred.FindContributors; 017 import escjava.gui.GUI; 018 import escjava.AnnotationHandler; 019 020 import javafe.reader.StandardTypeReader; 021 import escjava.reader.EscTypeReader; 022 023 import javafe.parser.PragmaParser; 024 025 import escjava.sp.*; 026 import escjava.translate.*; 027 import escjava.pa.*; 028 029 import javafe.tc.TypeSig; 030 import escjava.tc.TypeCheck; 031 032 import escjava.prover.*; 033 034 //import escjava.vcGeneration.VcGenerator; 035 036 import javafe.util.*; 037 038 /** 039 * Top level control module for ESC for Java. 040 * 041 * <p>This class (and its superclasses) handles parsing 042 * <code>escjava</code>'s command-line arguments and orchestrating the 043 * other pieces of the front end and escjava to perform the requested 044 * operations.<p> 045 * 046 * @see javafe.Tool 047 * @see javafe.SrcTool 048 */ 049 050 public class Main extends javafe.SrcTool 051 { 052 static public final String jarlocation; // can be null 053 054 static { 055 java.net.URL urlJar = GUI.class.getClassLoader().getResource( 056 "escjava/Main.class"); 057 String urlStr = urlJar.toString(); 058 int from = "jar:file:".length(); 059 int to = urlStr.indexOf("!/"); 060 if (to != -1) { 061 String j = urlStr.substring(from, to); 062 int k = j.lastIndexOf('/'); 063 if (k != -1) j = j.substring(0,k); 064 jarlocation = j; 065 } else { 066 jarlocation = null; 067 } 068 // This does not produce a good guess for the distribution 069 // root when running within the CVS distribution - just 070 // when running from a jar file. 071 //System.out.println("LOCATION " + urlStr + " " + jarlocation); 072 } 073 074 { 075 // Makes sure that the escjava.tc.Types factory instance is loaded 076 escjava.tc.Types.init(); 077 } 078 079 /** Our version number */ 080 //public final static String version = "(Nijmegen/Kodak) 1.3, 2003"; 081 public final static /*@ non_null @*/ String version = Version.VERSION; 082 083 084 private /*@ non_null @*/ AnnotationHandler annotationHandler = new AnnotationHandler(); 085 086 // Convenience copy of options().stages 087 public int stages; 088 089 /** 090 * Return the name of this tool. E.g., "ls" or "cp".<p> 091 * 092 * Used in usage and error messages.<p> 093 */ 094 public /*@ non_null @*/ String name() { return "escjava"; } 095 096 public /*@ non_null @*/ javafe.Options makeOptions() { return new Options(); } 097 098 // result can be null 099 public static /*@ pure */ Options options() { return (Options)options; } 100 101 // Front-end setup 102 103 /** 104 * Returns the Esc StandardTypeReader, EscTypeReader. 105 */ 106 // All three arguments can be null. 107 public /*@ non_null @*/ StandardTypeReader makeStandardTypeReader(String path, 108 String sourcePath, 109 PragmaParser P) { 110 return EscTypeReader.make(path, sourcePath, P, annotationHandler); 111 } 112 113 /** 114 * Returns the EscPragmaParser. 115 */ 116 public /*@ non_null @*/ javafe.parser.PragmaParser makePragmaParser() { 117 return new escjava.parser.EscPragmaParser(); 118 } 119 120 /** 121 * Returns the pretty printer to set 122 * <code>PrettyPrint.inst</code> to. 123 */ 124 public /*@ non_null @*/ PrettyPrint makePrettyPrint() { 125 DelegatingPrettyPrint p = new EscPrettyPrint(); 126 p.del = new StandardPrettyPrint(p); 127 return p; 128 } 129 130 /** 131 * Called to obtain an instance of the javafe.tc.TypeCheck class 132 * (or a subclass thereof). May not return <code>null</code>. By 133 * default, returns <code>javafe.tc.TypeCheck</code>. 134 */ 135 public /*@ non_null @*/ javafe.tc.TypeCheck makeTypeCheck() { 136 return new escjava.tc.TypeCheck(); 137 } 138 139 140 /** 141 * Override SrcTool.notify to ensure all lexicalPragmas get 142 * registered as they are loaded. 143 */ 144 //@ also 145 //@ requires justLoaded != null; 146 public void notify(CompilationUnit justLoaded) { 147 super.notify(justLoaded); 148 149 NoWarn.registerNowarns(justLoaded.lexicalPragmas); 150 151 if (options().printCompilationUnitsOnLoad) { 152 String pkgName = justLoaded.pkgName == null ? "" : justLoaded.pkgName.printName(); 153 String filename = Location.toFileName(justLoaded.loc); 154 System.out.println("LOADED: " + pkgName + " " + filename); 155 } 156 } 157 158 159 // Main processing code 160 161 /** 162 * Start up an instance of this tool using command-line arguments 163 * <code>args</code>. <p> 164 * 165 * This is the main entry point for the <code>escjava</code> 166 * command.<p> 167 */ 168 //@ requires \nonnullelements(args); 169 public static void main(/*@ non_null @*/ String[] args) { 170 int exitcode = compile(args); 171 if (exitcode != 0) System.exit(exitcode); 172 } 173 174 public Main() { 175 // resets any static variables left from a previous instantiation 176 clear(true); 177 } 178 179 boolean keepProver = false; 180 181 public void clear(boolean complete) { 182 // restore ordinary checking of assertions 183 super.clear(complete); 184 if (complete) NoWarn.init(); 185 gctranslator = new Translate(); 186 if (!keepProver) ProverManager.kill(); 187 // Disallow the -avoidSpec option: 188 javafe.SrcToolOptions.allowAvoidSpec = false; 189 } 190 191 /** 192 * An entry point for the tool useful for executing tests, 193 * since it returns the exit code. 194 * 195 * @param args The command-line arguments the program was invoked with 196 * @return The exit code for the program, indicating either a successful 197 * exit or an exit with errors or an exit because of an out of 198 * memory condition 199 * @see javafe.Tool#run(java.lang.String[]) 200 */ 201 //@ requires args != null; 202 /*@ ensures \result == okExitCode || \result == badUsageExitCode 203 @ || \result == errorExitCode || \result == outOfMemoryExitCode; 204 */ 205 206 public static int compile(String[] args) { 207 try { 208 Main t = new Main(); 209 int result = t.run(args); 210 return result; 211 } catch (OutOfMemoryError oom) { 212 Runtime rt = Runtime.getRuntime(); 213 long memUsedBytes = rt.totalMemory() - rt.freeMemory(); 214 System.out.println("java.lang.OutOfMemoryError (" + memUsedBytes + 215 " bytes used)"); 216 //oom.printStackTrace(System.out); 217 return outOfMemoryExitCode; 218 } 219 } 220 221 222 // SrcTool-instance specific processing 223 224 /** An instance of the GC->VC translator */ 225 public static Translate gctranslator = new Translate(); 226 227 /** 228 * Override setup so can issue version # as soon as possible (aka, 229 * just after decode options so know if -quiet or -testMode issued or not). 230 */ 231 public void setup() { 232 stages = options().stages; 233 if (options().simplify == null) setDefaultSimplify(); 234 if (options().simplify != null) System.setProperty("simplify",options().simplify); 235 super.setup(); 236 237 //$$ 238 ProverManager.useSimplify = options().useSimplify; 239 ProverManager.useSammy = options().useSammy; 240 ProverManager.useHarvey = options().useHarvey; 241 //$$ 242 243 if (!options().quiet) { 244 System.out.print("ESC/Java version " + 245 (options().testMode?"VERSION":version)); 246 247 System.out.print("\n"); 248 } 249 250 } 251 252 public void setDefaultSimplify() { 253 String os = System.getProperty("os.name"); 254 String root = null; 255 String name = "Simplify-1.5.4."; 256 if (os.startsWith("Windows")) { 257 root = name + "exe"; 258 } else if (os.startsWith("Mac")) { 259 root = name + "macosx"; 260 } else if (os.startsWith("Linux")) { 261 root = name + "linux"; 262 } else if (os.startsWith("Solaris")) { 263 root = name + "solaris"; 264 } else { 265 ErrorSet.warning("Unknown OS - could not find Simplify: " + os); 266 } 267 if (root == null) return; 268 269 270 File f; 271 if (jarlocation == null) f = new File(root); 272 else f = new File(jarlocation,root); 273 274 if (!f.exists()) { 275 ErrorSet.warning("Could not find a default SIMPLIFY executable - specify the path to SIMPLIFY for this operating system using the -simplify option[ " + os + " " + root + "]"); 276 return; 277 } 278 try { 279 options().simplify = f.getCanonicalPath(); 280 } catch (IOException e) { 281 ErrorSet.warning("Could not find a default SIMPLIFY executable - specify the path to SIMPLIFY for this operating system using the -simplify option[ " + os + " " + root + "]"); 282 return; 283 } 284 } 285 286 public void setupPaths() { 287 super.setupPaths(); 288 if (options().specspath == null) return; 289 if (compositeSourcePath == null) { 290 compositeClassPath = 291 options().specspath 292 + java.io.File.pathSeparator 293 + compositeClassPath; 294 } else { 295 compositeSourcePath = 296 options().specspath 297 + java.io.File.pathSeparator 298 + compositeSourcePath; 299 } 300 } 301 302 public void preload() { 303 // Check to see that we are using a legitimate Java VM version. 304 // ESC/Java2 does not support Java 1.5 at this time. 305 if (System.getProperty("java.version").indexOf("1.5") != -1) { 306 ErrorSet.fatal("Java 1.5 source, bytecode, and VMs are not supported at this time.\nPlease use a Java 1.4 VM and only process source code and bytecode from\nJava versions prior to 1.5."); 307 return; 308 } 309 super.preload(); 310 } 311 312 /** 313 * Hook for any work needed before <code>handleCU</code> is called 314 * on each <code>CompilationUnit</code> to process them. 315 */ 316 public void preprocess() { 317 318 if (ErrorSet.fatals > 0) { 319 ErrorSet.fatal(null); 320 } 321 322 // call our routines to run the constructor inlining experiment 323 if (options().inlineConstructors) 324 InlineConstructor.inlineConstructorsEverywhere(loaded); 325 326 327 //if (6 <= stages || options().predAbstract) { 328 //ProverManager.start(); 329 //} 330 331 } 332 333 /** 334 * A wrapper for opening output files for printing. 335 * 336 * dir can be null. 337 */ 338 //@ ensures \result != null; 339 private PrintStream fileToPrintStream(String dir, /*@ non_null @*/ String fname) { 340 File f = new File(dir, fname); 341 try { 342 return new PrintStream(new FileOutputStream(f)); 343 } catch (IOException e) { 344 javafe.util.ErrorSet.fatal(e.getMessage()); 345 return null; // unreachable 346 } 347 } 348 349 public void postload() { 350 super.postload(); 351 if (OutsideEnv.filesRead() == 0) { 352 ErrorSet.caution("No files read."); 353 } 354 } 355 356 /** 357 * Hook for any work needed after <code>handleCU</code> has been 358 * called on each <code>CompilationUnit</code> to process them. 359 */ 360 public void postprocess() { 361 362 // If we are in the Houdini context (guardedVC is true), output 363 // the association of file numbers to their names. 364 // Also, dump out a list of guard variable names. 365 if (options().guardedVC) { 366 PrintStream o = fileToPrintStream(options().guardedVCDir, options().guardedVCFileNumbers); 367 Vector v = LocationManagerCorrelatedReader.fileNumbersToNames(); 368 for(int i=0; i<v.size(); i++) o.println(i + " " + v.elementAt(i)); 369 o.close(); 370 371 o = fileToPrintStream(options().guardedVCDir, options().guardedVCGuardFile); 372 Enumeration e = options().guardVars.elements(); 373 while (e.hasMoreElements()) { 374 o.println((String)e.nextElement()); 375 } 376 o.close(); 377 } 378 379 if (!keepProver) ProverManager.kill(); 380 } 381 382 /** 383 * This method is called on each <code>CompilationUnit</code> that 384 * this tool processes. This method overrides the implementation 385 * given in the superclass, adding a couple of lines before the 386 * superclass implementation is called. 387 */ 388 public void handleCU(CompilationUnit cu) { 389 if (options().testRef) makePrettyPrint().print(System.out,cu); 390 391 NoWarn.setStartLine(options().startLine, cu); 392 393 UniqName.setDefaultSuffixFile(cu.getStartLoc()); 394 try { 395 super.handleCU(cu); 396 } catch (FatalError e) { 397 // Errors are already reported 398 //ErrorSet.report("Aborted processing " + cu.sourceFile().getHumanName() + " because of fatal errors"); 399 } 400 401 options().startLine = -1; // StartLine applies only to first CU 402 } 403 404 405 /** 406 * This method is called by SrcTool on the TypeDecl of each 407 * outside type that SrcTool is to process. 408 * 409 * <p> In addition, it calls itself recursively to handle types 410 * nested within outside types. 411 */ 412 //@ also 413 //@ requires td != null; 414 public void handleTD(TypeDecl td) { 415 long startTime = currentTime(); 416 TypeSig sig = TypeCheck.inst.getSig(td); 417 418 if (!options().quiet) 419 System.out.println("\n" + sig.toString() + " ..."); 420 421 /* If something is on the command-line, presume we want to check it 422 as thoroughly as possible. 423 if (sig.getTypeDecl().specOnly && 424 !options().checkSpecs) { // do not process specs 425 // No bodies to process 426 if (!options().quiet) System.out.println("Skipping " + 427 sig.toString() + " - specification only"); 428 return; 429 } 430 */ 431 432 if (Location.toLineNumber(td.getEndLoc()) < options().startLine) 433 return; 434 435 // Do actual work: 436 boolean aborted = processTD(td); 437 438 if (!options().quiet) 439 System.out.println(" [" + timeUsed(startTime) 440 + " total]" 441 + (aborted ? " (aborted)" : "") ); 442 443 /* 444 * Handled any nested types: [1.1] 445 */ 446 TypeDecl decl = sig.getTypeDecl(); 447 for (int i=0; i<decl.elems.size(); i++) { 448 if (decl.elems.elementAt(i) instanceof TypeDecl) 449 handleTD((TypeDecl)decl.elems.elementAt(i)); 450 } 451 } 452 453 /** 454 * Run all the requested stages on a given TypeDecl; return true 455 * if we had to abort. 456 * 457 */ 458 //@ requires td != null; 459 //@ requires (* td is not from a binary file. *); 460 private boolean processTD(TypeDecl td) { 461 try { 462 463 // ==== Start stage 1 ==== 464 465 /* 466 * Do Java type checking then print Java types if we've been 467 * asked to: 468 */ 469 long startTime = currentTime(); 470 int errorCount = ErrorSet.errors; 471 TypeSig sig = TypeCheck.inst.getSig(td); 472 sig.typecheck(); 473 NoWarn.typecheckRegisteredNowarns(); 474 475 476 if (options().pjt) { 477 // Create a pretty-printer that shows types 478 DelegatingPrettyPrint p = new javafe.tc.TypePrint(); 479 p.del = new EscPrettyPrint(p, new StandardPrettyPrint(p)); 480 481 System.out.println("\n**** Source code with types:"); 482 p.print(System.out, 0, td); 483 } 484 485 // Turn off extended static checking and abort if any errors 486 // occured while type checking *this* TypeDecl: 487 if (errorCount < ErrorSet.errors) { 488 if (stages>1) { 489 stages = 1; 490 ErrorSet.caution("Turning off extended static checking " + 491 "due to type error(s)"); 492 } 493 return true; 494 } 495 496 // ==== Start stage 2 ==== 497 if (stages<2) 498 return false; 499 500 501 // Generate the type-specific background predicate 502 errorCount = ErrorSet.errors; 503 if (Info.on) Info.out("[ Finding contributors for " + sig + "]"); 504 FindContributors scope = new FindContributors(sig); 505 VcToString.resetTypeSpecific(); 506 507 if (Info.on) Info.out("[ Found contributors for " + sig + "]"); 508 509 if (options().guardedVC) { 510 String locStr = UniqName.locToSuffix(td.locId); 511 String fn = locStr + ".class." + options().guardedVCFileExt; 512 File f = new File(options().guardedVCDir, fn); 513 PrintStream o = fileToPrintStream(options().guardedVCDir, fn); 514 o.println(options().ClassVCPrefix); 515 o.println(td.id + "@" + locStr); 516 o.print("\n(BG_PUSH "); 517 escjava.backpred.BackPred.genTypeBackPred(scope, o); 518 o.println(")"); 519 o.close(); 520 } 521 522 // Turn off extended static checking and abort if any type errors 523 // occured while generating the type-specific background predicate: 524 if (errorCount < ErrorSet.errors) { 525 stages = 1; 526 ErrorSet.caution("Turning off extended static checking " + 527 "due to type error(s)"); 528 return true; 529 } 530 531 if (options().testRef) makePrettyPrint().print(System.out,0,td); 532 533 // ==== Start stage 3 ==== 534 if (3 <= stages) { 535 536 if (6 <= stages || options().predAbstract) 537 ProverManager.push(scope); 538 539 LabelInfoToString.reset(); 540 InitialState initState = new InitialState(scope); 541 LabelInfoToString.mark(); 542 543 if (!options().quiet) 544 System.out.println(" [" + timeUsed(startTime) + "]"); 545 546 547 // Process the elements of "td"; stage 3 continues into stages 4 548 // and 5 inside processTypeDeclElem: 549 if (options().inlineConstructors && !Modifiers.isAbstract(td.modifiers)) { 550 // only process inlined versions of methods 551 for (int i = 0; i < td.elems.size(); i++) { 552 TypeDeclElem tde = td.elems.elementAt(i); 553 if (!InlineConstructor.isConstructorInlinable(tde) || 554 InlineConstructor.isConstructorInlinedMethod((MethodDecl) tde)) 555 processTypeDeclElem(tde, sig, initState); 556 } 557 } else { 558 for (int i = 0; i < td.elems.size(); i++) 559 processTypeDeclElem(td.elems.elementAt(i), sig, initState); 560 } 561 } 562 563 // ==== all done; clean up ==== 564 ProverManager.pop(); 565 566 } catch (FatalError e) { 567 // Error already reported 568 throw e; 569 } catch (Throwable e) { 570 System.out.println("Exception " + e + " thrown while processing " + TypeSig.getSig(td)); 571 e.printStackTrace(System.out); 572 return true; 573 } 574 return false; 575 } 576 577 578 /** 579 * Run stages 3+..6 as requested on a TypeDeclElem. 580 * 581 * requires te is not from a binary file, sig is the 582 * TypeSig for te's parent, and initState != null. 583 */ 584 //@ requires sig != null && initState != null; 585 private void processTypeDeclElem(TypeDeclElem te, TypeSig sig, 586 InitialState initState) { 587 // Only handle methods and constructors here: 588 if (!(te instanceof RoutineDecl)) 589 return; 590 RoutineDecl r = (RoutineDecl)te; 591 592 593 long startTime = java.lang.System.currentTimeMillis(); 594 if (!options().quiet) { 595 String name = TypeCheck.inst.getRoutineName(r) + 596 javafe.tc.TypeCheck.getSignature(r); 597 System.out.println("\n" + sig.toString() + ": " + 598 name + " ..."); 599 } 600 601 // Do the actual work, handling not implemented exceptions: 602 String status = "error"; 603 try { 604 status = processRoutineDecl(r, sig, initState); 605 } catch (javafe.util.NotImplementedException e) { 606 // continue - problem already reported 607 status = "not-implemented"; 608 } catch (FatalError e) { 609 // continue; 610 } 611 612 if (!options().quiet) 613 System.out.println(" [" + timeUsed(startTime) + "] " 614 + status); 615 616 /************************* 617 System.out.println("Lines " + 618 (Location.toLineNumber(r.getEndLoc()) 619 -Location.toLineNumber(r.getStartLoc())) 620 +" time "+timeUsed(startTime)); 621 *******************/ 622 623 624 } 625 626 /** 627 * Run stages 3+..6 as requested on a RoutineDeclElem; returns a 628 * short (~ 1 word) status message. 629 * 630 * requires - r is not from a binary file, sig is the TypeSig 631 * for r's parent, and initState != null. 632 */ 633 //@ ensures \result != null; 634 private String processRoutineDecl(/*@ non_null */ RoutineDecl r, 635 /*@ non_null */ TypeSig sig, 636 /*@ non_null */ InitialState initState) { 637 638 if (r.body == null) return "passed immediately"; 639 if (r.parent.specOnly) return "passed immediately"; 640 if ( Location.toLineNumber(r.getEndLoc()) < options().startLine ) 641 return "skipped"; 642 String simpleName = TypeCheck.inst.getRoutineName(r).intern(); 643 String fullName = sig.toString() + "." + simpleName + 644 javafe.tc.TypeCheck.getSignature(r); 645 fullName = removeSpaces(fullName).intern(); 646 if (options().routinesToSkip != null && 647 (options().routinesToSkip.contains(simpleName) || 648 options().routinesToSkip.contains(fullName))) { 649 return "skipped"; 650 } 651 if (options().routinesToCheck != null && 652 !options().routinesToCheck.contains(simpleName) && 653 !options().routinesToCheck.contains(fullName)) { 654 return "skipped"; 655 } 656 657 // ==== Stage 3 continues here ==== 658 /* 659 * Translate body into a GC: 660 */ 661 long startTime = java.lang.System.currentTimeMillis(); 662 long routineStartTime = startTime; 663 664 // don't check the body if we're checking some other inlining depth 665 Translate.globallyTurnOffChecks(gctranslator.inlineCheckDepth > 0); 666 667 LabelInfoToString.resetToMark(); 668 GuardedCmd gc = computeBody(r, initState); 669 /*-@ uninitialized @*/ /* readable_if stats; */ int origgcSize = 0; 670 if (options().statsTime || options().statsSpace) { 671 origgcSize = Util.size(gc); 672 } 673 674 String gcTime = timeUsed(startTime); 675 startTime = java.lang.System.currentTimeMillis(); 676 677 UniqName.resetUnique(); 678 679 if (gc==null) 680 return "passed immediately"; 681 if (options().pgc) { 682 System.out.println("\n**** Guarded Command:"); 683 ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, gc); 684 System.out.println(""); 685 } 686 687 Set directTargets = Targets.direct(gc); 688 GCSanity.check(gc); 689 690 691 // ==== Start stage 4 ==== 692 if (stages<4) 693 return "ok"; 694 695 // Convert GC to DSA: 696 697 String dsaTime = ""; 698 if (options().dsa) { // always true 699 /* 700 * From experiements from POPL01 (Cormac) 701 gc = passify ? Passify.compute(gc) : DSA.dsa(gc); 702 */ 703 gc = DSA.dsa(gc); 704 dsaTime = timeUsed(startTime); 705 startTime = java.lang.System.currentTimeMillis(); 706 707 if (options().pdsa) { 708 System.out.println("\n**** Dynamic Single Assignment:"); 709 ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, gc); 710 System.out.println(""); 711 } 712 } 713 714 // ==== Start stage 5 ==== 715 if (stages<5) 716 return "ok"; 717 718 // Generate the VC for GC: 719 Expr vcBody; 720 /* 721 * From experiements from POPL01 (Cormac) 722 if(wpnxw != 0 ) { 723 vcBody = WpName.compute( gc, wpnxw ); 724 } else 725 */ 726 if (options().spvc) { 727 /* 728 * From experiements from POPL01 (Cormac) 729 vcBody = wpp ? Wpp.compute(gc, GC.truelit, GC.truelit) : 730 SPVC.compute(gc); 731 */ 732 vcBody = SPVC.compute(gc); 733 } else { 734 vcBody = Ejp.compute(gc, GC.truelit, GC.truelit); 735 } 736 737 Expr vc = GC.implies(initState.getInitialState(), vcBody); 738 // Attach a label for use in the logfile generated (if any): 739 String label = "vc." + sig.toString() + "."; 740 if (r instanceof MethodDecl) 741 label += ((MethodDecl)r).id; 742 else 743 label += "<constructor>"; 744 label += "." + UniqName.locToSuffix(r.getStartLoc()); 745 vc = LabelExpr.make(r.getStartLoc(), r.getEndLoc(), 746 false, Identifier.intern(label), vc); 747 748 // Check for VC too big: 749 int usize = Util.size(vc, options().vclimit); 750 if (usize == -1) { 751 ErrorSet.caution("Unable to check " 752 + TypeCheck.inst.getName(r) 753 + " of type " + TypeSig.getSig(r.parent) 754 + " because its VC is too large"); 755 return "VC too big"; 756 } 757 758 if (options().printAssumers) { 759 System.out.print("ASSUMERS: "); 760 System.out.print(Location.toFileName(r.getStartLoc())); 761 System.out.print('|'); 762 System.out.print(fullName); 763 System.out.println(LabelInfoToString.get()); 764 } 765 766 String ejpTime = timeUsed(startTime); 767 startTime = java.lang.System.currentTimeMillis(); 768 // Translate VC to a string 769 Info.out("[converting VC to a string]"); 770 771 //$$ 772 /* Use the new vc generator (= nvcg) 773 * ifpvc stands for 'independant from prover' 774 */ 775 // if(options().nvcg){ 776 777 // StringBuffer sb = new StringBuffer(); 778 // StringBuffer dot = null; 779 780 // VcGenerator vcg = new VcGenerator((ASTNode)vc); 781 782 // if(options().nvcgpi) 783 // vcg.printInfo(); 784 785 // // write the proof generated by the new vcg to a file 786 // if(options().pSimplify){ 787 // try { 788 // String fn = UniqName.locToSuffix(r.locId); 789 // fn = fn + ".pSimplify"; 790 791 // FileWriter fw = new FileWriter(fn); 792 793 // fw.write(vcg.simplifyProof()); 794 795 // fw.close(); 796 797 // System.out.println("simplify proof using the new vcg has bee written to "+fn); 798 // } 799 // catch (Exception e) { 800 // System.out.println(e.getMessage()); 801 // } 802 // } 803 804 // // generate the dot file for the original vc tree 805 // if(options().vc2dot){ 806 // try { 807 // String fn = UniqName.locToSuffix(r.locId); 808 // fn = fn + ".vc.dot"; 809 810 // FileWriter fw = new FileWriter(fn); 811 812 // /* initialization of dot format */ 813 // fw.write("digraph G {\n"); 814 815 // fw.write(vcg.old2Dot()); 816 817 // /* end of dot file */ 818 // fw.write("\n}\n"); 819 // fw.close(); 820 821 // /* run the appropriate commad to generate the graph */ 822 // Runtime run = Runtime.getRuntime(); 823 824 // run.exec("dot -Tps "+fn+" -o "+fn+".ps"); 825 826 // System.out.println("graph of the original vc tree for method "+UniqName.locToSuffix(r.locId)+" have been written to "+fn+".ps"); 827 828 // } 829 // catch (Exception e) { 830 // System.out.println(e.getMessage()); 831 // } 832 // } 833 834 // /* generate the dot file for the translation of the tree. 835 // * ifpvc stands for independant from prover verification conditons 836 // */ 837 // if(options().ifpvc2dot){ 838 // try { 839 // String fn = UniqName.locToSuffix(r.locId); 840 // fn = fn + ".ifpvc.dot"; 841 842 // FileWriter fw = new FileWriter(fn); 843 844 // /* initialization of dot format */ 845 // fw.write("digraph G {\n"); 846 847 // /* generate the graph by visiting the tree */ 848 // fw.write(vcg.new2Dot()); 849 850 // /* end of dot file */ 851 // fw.write("\n}\n"); 852 // fw.close(); 853 854 // /* run the appropriate commad to generate the graph */ 855 // Runtime run = Runtime.getRuntime(); 856 857 // run.exec("dot -Tps "+fn+" -o "+fn+".ps"); 858 859 // System.out.println("graph of the independant from prover vc tree have been written to "+fn+".ps"); 860 861 // } 862 // catch (Exception e) { 863 // System.out.println(e.getMessage()); 864 // } 865 // } 866 // } 867 868 // if( options().pvsProof ) { 869 870 // String fn = UniqName.locToSuffix(r.locId)+".method."+"pvs"; 871 872 // PrintStream o = fileToPrintStream(".",fn); 873 // VcToStringPvs.compute(vc, o); 874 // o.close(); 875 876 // Runtime run = Runtime.getRuntime(); 877 878 // try{ 879 // run.exec("./rewrite-pvs-proof.py "+fn); 880 // } 881 // catch(Exception e) { 882 // System.out.println("Error when launching python script\n that reformats the proof for pvs, "+e); 883 // } 884 885 // System.out.println("Pvs translation of the proof has been written to $ESCTOOLS_ROOT/Escjava/"+fn); 886 // } 887 // //$$ 888 889 if (options().pvc || (Info.on && options().traceInfo > 0)) { 890 VcToString.compute(vc, System.out); 891 } 892 893 if (options().guardedVC) { 894 895 String fn = UniqName.locToSuffix(r.locId) + ".method." + 896 options().guardedVCFileExt; 897 PrintStream o = fileToPrintStream(options().guardedVCDir, fn); 898 o.println(options().MethodVCPrefix); 899 o.println(r.parent.id + "@" + UniqName.locToSuffix(r.parent.locId)); 900 VcToString.compute(vc, o); 901 o.close(); 902 return "guarded VC generation finished"; 903 } 904 905 String vcTime = timeUsed(startTime); 906 startTime = java.lang.System.currentTimeMillis(); 907 908 // ==== Start stage 6 ==== 909 if (stages<6) 910 return "ok"; 911 912 // Process Simplify's output 913 String status = "unexpectedly missing Simplify output"; 914 try { 915 916 int stat = doProving(vc,r,directTargets,null); 917 switch (stat) { 918 case Status.STATICCHECKED_OK: status = "passed"; break; 919 case Status.STATICCHECKED_ERROR: status = "failed"; break; 920 case Status.STATICCHECKED_TIMEOUT: status = "timed out"; break; 921 default: status = "unexpectedly missing Simplify output"; 922 } 923 924 } catch (escjava.prover.SubProcess.Died e) { 925 //System.out.println("DIED"); 926 ProverManager.died(); 927 } catch (FatalError e) { 928 //System.out.println("DIED"); 929 ProverManager.died(); 930 } 931 932 String proofTime = timeUsed(startTime); 933 if (options().statsTime) { 934 System.out.println(" [Time: "+timeUsed(routineStartTime) 935 +" GC: "+gcTime 936 +" DSA: "+dsaTime 937 +" Ejp: "+ejpTime 938 +" VC: "+vcTime 939 +" Proof(s): "+proofTime 940 +"]"); 941 } 942 if(options().statsSpace) { 943 System.out.println(" [Size: " 944 +" src: "+Util.size(r) 945 +" GC: "+origgcSize 946 +" DSA: "+Util.size(gc) 947 +" VC: "+Util.size(vc) 948 +"]"); 949 } 950 if(options().statsTermComplexity) 951 System.out.println(" [Number of terms: "+VcToString.termNumber+"]"); 952 if(options().statsVariableComplexity) 953 System.out.println(" [Number of variables: "+VcToString.variableNumber+"]"); 954 if(options().statsQuantifierComplexity) 955 System.out.println(" [Number of quantifiers: "+VcToString.quantifierNumber+"]"); 956 957 return status; 958 } 959 960 961 //@ requires vc != null; 962 // scope can be null 963 public int doProving(Expr vc, RoutineDecl r, Set directTargets, 964 FindContributors scope) { 965 try { 966 967 Enumeration results = ProverManager.prove(vc,scope); 968 969 //$$ 970 if( ProverManager.useSimplify ) { 971 //$$ 972 973 // Process Simplify's output 974 String status = "unexpectedly missing Simplify output"; 975 int stat = Status.STATICCHECKED_ERROR; 976 977 boolean nextWarningNeedsPrecedingLine = true; 978 if (results != null) while (results.hasMoreElements()) { 979 980 SimplifyOutput so = (SimplifyOutput)results.nextElement(); 981 switch (so.getKind()) { 982 case SimplifyOutput.VALID: 983 status = "passed"; 984 stat = Status.STATICCHECKED_OK; 985 break; 986 case SimplifyOutput.INVALID: 987 status = "failed"; 988 stat = Status.STATICCHECKED_ERROR; 989 break; 990 case SimplifyOutput.UNKNOWN: 991 status = "timed out"; 992 stat = Status.STATICCHECKED_TIMEOUT; 993 break; 994 case SimplifyOutput.COMMENT: { 995 SimplifyComment sc = (SimplifyComment)so; 996 System.out.println("SIMPLIFY: " + sc.getMsg()); 997 break; 998 } 999 case SimplifyOutput.COUNTEREXAMPLE: { 1000 if (nextWarningNeedsPrecedingLine) { 1001 escjava.translate.ErrorMsg.printSeparatorLine(System.out); 1002 nextWarningNeedsPrecedingLine = false; 1003 } 1004 SimplifyResult sr = (SimplifyResult)so; 1005 escjava.translate.ErrorMsg.print(TypeCheck.inst.getName(r), 1006 sr.getLabels(), sr.getContext(), 1007 r, directTargets, System.out); 1008 break; 1009 } 1010 case SimplifyOutput.EXCEEDED_PROVER_KILL_TIME: { 1011 SimplifyResult sr = (SimplifyResult)so; 1012 ErrorSet.caution("Unable to check " + 1013 TypeCheck.inst.getName(r) + 1014 " of type " + TypeSig.getSig(r.parent) + 1015 " completely because too much time required"); 1016 if (Info.on && sr.getLabels() != null) { 1017 Info.out("Current labels: " + sr.getLabels()); 1018 } 1019 nextWarningNeedsPrecedingLine = true; 1020 break; 1021 } 1022 case SimplifyOutput.EXCEEDED_PROVER_KILL_ITER: { 1023 SimplifyResult sr = (SimplifyResult)so; 1024 ErrorSet.caution("Unable to check " + 1025 TypeCheck.inst.getName(r) + 1026 " of type " + TypeSig.getSig(r.parent) + 1027 " completely because" + 1028 " too many iterations required"); 1029 if (Info.on && sr.getLabels() != null) { 1030 Info.out("Current labels: " + sr.getLabels()); 1031 } 1032 nextWarningNeedsPrecedingLine = true; 1033 break; 1034 } 1035 case SimplifyOutput.REACHED_CC_LIMIT: 1036 ErrorSet.caution("Not checking " + 1037 TypeCheck.inst.getName(r) + 1038 " of type " + TypeSig.getSig(r.parent) + 1039 " completely because" + 1040 " warning limit (PROVER_CC_LIMIT) reached"); 1041 break; 1042 case SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_TIME: { 1043 SimplifyResult sr = (SimplifyResult)so; 1044 ErrorSet.caution("Unable to check subgoal of " + 1045 TypeCheck.inst.getName(r) + 1046 " of type " + TypeSig.getSig(r.parent) + 1047 " completely because too much time required"); 1048 if (Info.on && sr.getLabels() != null) { 1049 Info.out("Current labels: " + sr.getLabels()); 1050 } 1051 nextWarningNeedsPrecedingLine = true; 1052 break; 1053 } 1054 case SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_ITER: { 1055 SimplifyResult sr = (SimplifyResult)so; 1056 ErrorSet.caution("Unable to check subgoal of " + 1057 TypeCheck.inst.getName(r) + 1058 " of type " + TypeSig.getSig(r.parent) + 1059 " completely because" + 1060 " too many iterations required"); 1061 if (Info.on && sr.getLabels() != null) { 1062 Info.out("Current labels: " + sr.getLabels()); 1063 } 1064 nextWarningNeedsPrecedingLine = true; 1065 break; 1066 } 1067 case SimplifyOutput.WARNING_TRIGGERLESS_QUANT: { 1068 TriggerlessQuantWarning tqw = (TriggerlessQuantWarning)so; 1069 int loc = tqw.getLocation(); 1070 /* Turn off this warning for now. FIXME 1071 Some generated axioms require using the Simplify heuristic to work correctly, 1072 while others generate this warning if there is no explict quantifier. 1073 String msg = "Unable to use quantification because " + 1074 "no trigger found: " + tqw.e1; 1075 if (loc != Location.NULL) { 1076 ErrorSet.caution(loc, msg); 1077 } else { 1078 ErrorSet.caution(msg); 1079 } 1080 if (Info.on && tqw.getLabels() != null) { 1081 Info.out("Current labels: " + tqw.getLabels()); 1082 } 1083 */ 1084 break; 1085 } 1086 default: 1087 Assert.fail("unexpected type of Simplify output"); 1088 break; 1089 } 1090 } 1091 1092 return stat; 1093 //$$ 1094 } 1095 //$$ 1096 return 0; 1097 // return stat; 1098 1099 } catch (escjava.prover.SubProcess.Died e) { 1100 //status = "died"; 1101 return Status.STATICCHECKED_ERROR; 1102 } 1103 1104 } 1105 1106 /** 1107 * This method computes the guarded command (including assuming 1108 * the precondition, the translated body, the checked 1109 * postcondition, and the modifies constraints) for the method or 1110 * constructor <code>r</code> in scope <code>scope</code>. 1111 * 1112 * @return <code>null</code> if <code>r</code> doesn't have a body. 1113 */ 1114 1115 //@ requires r != null; 1116 //@ requires initState != null; 1117 protected GuardedCmd computeBody(RoutineDecl r, InitialState initState) { 1118 if (r.getTag() == TagConstants.METHODDECL && 1119 ((MethodDecl)r).body == null) { 1120 // no body 1121 return null; 1122 } 1123 1124 // don't check the routine if it's a helper 1125 if (Helper.isHelper(r)) { 1126 return null; 1127 } 1128 1129 FindContributors scope = new FindContributors(r); 1130 TrAnExpr.initForRoutine(); 1131 1132 /* 1133 * Compute an upper bound for synTargs if -O7 given. 1134 * 1135 * For now, do this via the kludge of calling trBody... !!!! 1136 */ 1137 Set predictedSynTargs = null; 1138 if (!options().useAllInvPreBody) { 1139 long T = java.lang.System.currentTimeMillis(); 1140 /* 1141 * Compute translation assuming synTargs is empty: 1142 * (gives same set of targets faster than using null) 1143 */ 1144 GuardedCmd tmpBody = gctranslator.trBody(r, scope, 1145 initState.getPreMap(), 1146 /*predictedSynTargs*/new Set(), 1147 null, 1148 /* issueCautions */ false); 1149 if (options().noDirectTargetsOpt) 1150 predictedSynTargs = Targets.normal(tmpBody); 1151 else 1152 predictedSynTargs = Targets.direct(tmpBody); 1153 if (options().statsTime) 1154 System.out.println(" [prediction time: " + timeUsed(T) + "]"); 1155 } 1156 1157 1158 1159 /* 1160 * Translate the body: 1161 */ 1162 /* Note: initState.preMap is the same for all declarations. 1163 This may be overkill (FIXME). 1164 It might be better to use information from scope directly 1165 since it is generated from the routine decl. 1166 However, I don't know for sure what would go missing. DRCok 1167 */ 1168 1169 GuardedCmd body = gctranslator.trBody(r, scope, 1170 initState.getPreMap(), 1171 predictedSynTargs, null, 1172 /* issueCautions */ true); 1173 1174 1175 Set fullSynTargs = Targets.normal(body); 1176 Set synTargs; 1177 if (options().noDirectTargetsOpt) 1178 synTargs = fullSynTargs; 1179 else 1180 synTargs = Targets.direct(body); 1181 1182 1183 /* 1184 * Verify predictedSynTargs if present that 1185 * synTargs is a subset of predictedSynTargs. 1186 */ 1187 if (predictedSynTargs != null) { 1188 Enumeration e = synTargs.elements(); 1189 while (e.hasMoreElements()) { 1190 GenericVarDecl target = (GenericVarDecl)(e.nextElement()); 1191 Assert.notFalse(predictedSynTargs.contains(target)); 1192 } 1193 } 1194 1195 1196 TrAnExpr.translate = gctranslator; 1197 Spec spec = GetSpec.getSpecForBody(r, scope, synTargs, 1198 initState.getPreMap()); 1199 GetSpec.addAxioms(Translate.axsToAdd,spec.preAssumptions); 1200 gctranslator.addMoreLocations(spec.postconditionLocations); 1201 1202 // if the current RoutineDecl corresponds to one of our 1203 // constructor-inlined methods, then zero out its postconditions 1204 if (r instanceof MethodDecl && 1205 InlineConstructor.isConstructorInlinedMethod((MethodDecl) r)) 1206 spec.post = ConditionVec.make(); 1207 1208 GuardedCmd fullCmd = 1209 GetSpec.surroundBodyBySpec(body, spec, scope, fullSynTargs, 1210 initState.getPreMap(), 1211 r.getEndLoc()); 1212 1213 if (Main.options().loopTranslation == Options.LOOP_SAFE && 1214 Main.options().predAbstract) { 1215 long T = java.lang.System.currentTimeMillis(); 1216 Traverse.compute(fullCmd, initState, gctranslator); 1217 if (options().statsTime) { 1218 System.out.println(" [predicate abstraction time: " + 1219 timeUsed(T) + "]"); 1220 } 1221 } 1222 Translate.addTraceLabelSequenceNumbers(fullCmd); 1223 1224 return fullCmd; 1225 1226 } 1227 1228 1229 // Misc. Utility routines 1230 1231 private static String removeSpaces(/*@ non_null */ String s) { 1232 while (true) { 1233 int k = s.indexOf(' '); 1234 if (k == -1) { 1235 return s; 1236 } 1237 s = s.substring(0, k) + s.substring(k+1); 1238 } 1239 } 1240 } 1241