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    }