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 }