    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.reader;
    004
    005    import javafe.ast.CompilationUnit;
    006    import javafe.ast.LexicalPragmaVec;
    007    import javafe.ast.Modifiers;
    008    import javafe.ast.Identifier;
    009    import javafe.ast.Name;
    010    import javafe.ast.*;
    011    import javafe.ast.TypeDecl;
    012    import javafe.ast.TypeDeclVec;
    013    import javafe.tc.TypeSig;
    014    import javafe.ast.PrettyPrint;                  // Debugging methods only
    015    import javafe.ast.StandardPrettyPrint;          // Debugging methods only
    016    import javafe.ast.DelegatingPrettyPrint;        // Debugging methods only
    017    import escjava.ast.EscPrettyPrint;              // Debugging methods only
    018    import javafe.util.Location;
    019    import escjava.ast.RefinePragma;
    020    import escjava.ast.*;
    021    import escjava.ast.TagConstants; // Resolves ambiguity
    022    import escjava.RefinementSequence;
    023
    024    import escjava.AnnotationHandler;
    025    import javafe.genericfile.*;
    026    import javafe.parser.PragmaParser;
    027    import javafe.filespace.Tree;
    028    import javafe.filespace.Query;
    029
    030    import javafe.util.Assert;
    031    import javafe.util.ErrorSet;
    032
    033    import javafe.reader.*;
    034    import javafe.tc.OutsideEnv;
    035
    036    import java.util.ArrayList;
    037    import java.util.Enumeration;
    038    import java.util.Iterator;
    039    import java.io.File;
    040    import java.io.FilenameFilter;
    041
    042    /**
    043     * An <code>EscTypeReader</code> is a <code>StandardTypeReader</code>
    044     * extended to understand ".spec" files.
    045     */
    046
    047    public class EscTypeReader extends StandardTypeReader
    048    {
    049        // Private creation
    050
    051        /**
    052         * Create an <code>ESCTypeReader</code> from a query engine, a
    053         * source reader, and a binary reader.  All arguments must be
    054         * non-null.
    055         */
    056        protected EscTypeReader(/*@ non_null @*/ Query engine,
    057                                /*@ non_null @*/ Query srcEngine,
    058                                /*@ non_null @*/ CachedReader srcReader,
    059                                /*@ non_null @*/ CachedReader binReader) {
    060            super(engine, srcEngine, srcReader, binReader);
    061        }
    062
    063
    064        // Public creation
    065
    066        /**
    067         * Create a <code>EscTypeReader</code> from a query engine, a
    068         * source reader, and a binary reader.  All arguments must be
    069         * non-null.
    070         */
    071        //@ ensures \result != null;
    072        public static StandardTypeReader make(/*@ non_null @*/ Query engine,
    073                                              /*@ non_null @*/ Query srcEngine,
    074                                              /*@ non_null @*/ CachedReader srcReader,
    075                                              /*@ non_null @*/ CachedReader binReader) {
    076            return new EscTypeReader(engine, srcEngine, srcReader, binReader);
    077        }
    078
    079        /**
    080         * Create a <code>EscTypeReader</code> from a non-null query
    081         * engine and a pragma parser.  The pragma parser may be null.
    082         */
    083        //@ requires Q != null;
    084        //    pragmaP can be null && ah doesn't appear to be used.
    085        //@ ensures \result != null;
    086        public static StandardTypeReader make(Query Q, Query sourceQ,
    087                            PragmaParser pragmaP, AnnotationHandler ah) {
    088            Assert.precondition(Q != null);
    089
    090            return make(Q, sourceQ, new RefinementCachedReader(
    091                                            new SrcReader(pragmaP)),
    092                                    new CachedReader(new BinReader()));
    093        }
    094
    095        /**
    096         * Create a <code>EscTypeReader</code> using a given Java
    097         * classpath for our underlying Java file space and a given pragma
    098         * parser.  If the given path is null, the default Java classpath
    099         * is used.
    100         *
    101         * <p> A fatal error will be reported via <code>ErrorSet</code> if
    102         * an I/O error occurs while initially scanning the filesystem.
    103         */
    104        //@ ensures \result != null;
    105        public static StandardTypeReader make(String path, String srcPath,
    106                                PragmaParser pragmaP, AnnotationHandler ah) {
    107            if (path==null)
    108                path = javafe.filespace.ClassPath.current();
    109            Query q = StandardTypeReader.queryFromClasspath(path);
    110
    111            Query srcq = srcPath == null ? q :
    112                            StandardTypeReader.queryFromClasspath(srcPath);
    113
    114            return make(q, srcq, pragmaP, ah);
    115        }
    116
    117        /**
    118         * Create a <code>EscTypeReader</code> using a the default Java
    119         * classpath for our underlying Java file space and a given pragma
    120         * parser.
    121         *
    122         * <p> A fatal error will be reported via <code>ErrorSet</code> if
    123         * an I/O error occurs while initially scanning the filesystem.
    124         */
    125        //@ ensures \result != null;
    126        public static StandardTypeReader make(PragmaParser pragmaP) {
    127            return make((String)null, (String)null, pragmaP);
    128        }
    129
    130        /**
    131         * Create a <code>EscTypeReader</code> using the default Java
    132         * classpath for our underlying Java file space and no pragma
    133         * parser.
    134         *
    135         * <p> A fatal error will be reported via <code>ErrorSet</code> if
    136         * an I/O error occurs while initially scanning the filesystem.
    137         */
    138        //@ ensures \result != null;
    139        public static StandardTypeReader make() {
    140            return make((PragmaParser) null);
    141        }
    142
    143
    144        // Existance/Accessibility
    145
    146        /**
    147         * Return true iff the fully-qualified outside type P.T exists.
    148         */
    149        public boolean exists(/*@ non_null @*/ String[] P,
    150                              /*@ non_null @*/ String T) {
    151            if ( super.exists(P, T)) return true;
    152            for (int i=0; i<activeSuffixes.length; ++i) {
    153                if (javaSrcFileSpace.findFile(P, T, activeSuffixes[i]) != null) {
    154                    return true;
    155                }
    156            }
    157            return false;
    158        }
    159
    160        //@ requires P != null;
    161        //@ requires T != null;
    162        // can return null
    163        public GenericFile findFirst(String[] P, String T) {
    164            return javaSrcFileSpace.findFile(P,T,activeSuffixes);
    165        }
    166
    167        //@ requires P != null;
    168        //@ requires filename != null;
    169        // can return null
    170        public GenericFile findSrcFile(String[] P, String filename) {
    171            return javaSrcFileSpace.findFile(P,filename);
    172        }
    173
    174        //@ requires P != null;
    175        //@ requires filename != null;
    176        // can return null
    177        public GenericFile findBinFile(String[] P, String filename) {
    178            return javaFileSpace.findFile(P,filename);
    179        }
    180
    181        public GenericFile findType(/*@ non_null @*/ String[] P,
    182                                    /*@ non_null @*/ String T) {
    183            GenericFile gf = javaSrcFileSpace.findFile(P,T,activeSuffixes);
    184            if (gf == null) gf = javaFileSpace.findFile(P, T, "class");
    185            return gf;
    186        }
    187
    188
    189
    190        public /*@ non_null @*/ FilenameFilter filter() {
    191            return new FilenameFilter() {
    192                public boolean accept(File f, String n) {
    193                    int p = n.indexOf('.');
    194                    if (p == -1) return false;
    195                    n = n.substring(p+1);
    196                    for (int i=0; i<activeSuffixes.length; ++i) {
    197                        if (n.equals(activeSuffixes[i])) {
    198                            return true;
    199                        }
    200                    }
    201                    return false;
    202                }
    203            };
    204        }
    205
    206        /*@ non_null @*/ String[] activeSuffixes = { "refines-java", "refines-spec", "refines-jml",
    207                              "java", "spec", "jml" };
    208
    209        /*@ non_null @*/ String[] nonJavaSuffixes = { "refines-java", "refines-spec", "refines-jml",
    210                              "spec", "jml",
    211                              "java-refined", "spec-refined", "jml-refined" };
    212
    213        // Reading
    214
    215        public CompilationUnit read(/*@ non_null @*/ GenericFile f,
    216                                    boolean avoidSpec) {
    217          return super.read(f,avoidSpec);
    218        }
    219
    220        /**
    221         * Override {@link StandardTypeReader#read(String[], String, boolean)}
    222         * method to include ".spec" files.
    223         */
    224        public CompilationUnit read(/*@ non_null @*/ String[] P,
    225                                    /*@ non_null @*/ String T,
    226                                    boolean avoidSpec) {
    227            // If a source exists and we wish to avoid specs, use it:
    228            if (avoidSpec) {
    229                GenericFile src = locateSource(P, T, true);
    230                if (src != null) {
    231                    return super.read(src, true);
    232                }
    233            }
    234
    235            // If not, use spec file if available:
    236            for (int i=0; i<activeSuffixes.length; ++i) {
    237                GenericFile spec = javaSrcFileSpace.findFile(P, T, activeSuffixes[i]);
    238                if (spec != null) {
    239                    return read(spec, false);
    240                }
    241            }
    242
    243            // Lastly, try source in spec mode then the binary:
    244            GenericFile source = locateSource(P, T, true);
    245            if (source != null)
    246                return super.read(source, false);
    247            return super.read(P, T, avoidSpec);     // only a binary exists...
    248        }
    249
    250        /**
    251         * Does a CompilationUnit contain a specOnly TypeDecl?
    252         */
    253        //@ requires cu != null;
    254        boolean containsSpecOnly(CompilationUnit cu) {
    255            for (int i=0; i<cu.elems.size(); i++) {
    256                TypeDecl d = cu.elems.elementAt(i);
    257                //@ assume d != null;
    258
    259                if (d.specOnly)
    260                    return true;
    261            }
    262
    263            return false;
    264        }
    265
    266
    267        // Test methods
    268
    269        //@ requires args != null;
    270        //@ requires \nonnullelements(args);
    271        public static void main(String[] args)
    272                throws java.io.IOException {
    273            if (args.length<2 || args.length>3
    274                || (args.length==3 && !args[2].equals("avoidSpec"))) {
    275                System.err.println("EscTypeReader: <package> <simple name>"
    276                                   + " [avoidSpec]");
    277                System.exit(1);
    278            }
    279
    280            javafe.util.Info.on = true;
    281
    282            String[] P = javafe.filespace.StringUtil.parseList(args[0], '.');
    283            StandardTypeReader R = make(new escjava.parser.EscPragmaParser());
    284
    285            DelegatingPrettyPrint p = new EscPrettyPrint();
    286            p.del = new StandardPrettyPrint(p);
    287            PrettyPrint.inst = p;
    288
    289
    290            CompilationUnit cu = R.read(P, args[1], args.length==3);
    291            if (cu==null) {
    292                System.out.println("Unable to load that type.");
    293                System.exit(1);
    294            }
    295
    296            PrettyPrint.inst.print( System.out, cu );
    297        }
    298    }