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