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