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