    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