001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.ast;
004
005 import javafe.ast.ASTNode;
006 import javafe.ast.ASTDecoration;
007 import javafe.ast.ModifierPragma;
008 import javafe.ast.ModifierPragmaVec;
009 import javafe.ast.GenericVarDecl;
010 import javafe.ast.IdentifierNode;
011 import javafe.ast.ASTDecoration;
012 import javafe.ast.RoutineDecl;
013 import javafe.ast.MethodDecl;
014 import javafe.ast.ClassDecl;
015 import javafe.ast.TypeDecl;
016 import javafe.tc.TypeSig;
017 import javafe.ast.Type;
018 import javafe.ast.TypeName;
019 import javafe.ast.ArrayType;
020 import javafe.ast.PrimitiveType;
021 import javafe.ast.FormalParaDecl;
022 import javafe.ast.FormalParaDeclVec;
023 import javafe.ast.*;
024 import escjava.Main;
025
026 import javafe.util.*;
027 import java.util.Enumeration;
028
029
030 public final class Utils
031 {
032 /**
033 * Finds and returns the first modifier pragma of <code>vdecl</code>
034 * that has the tag <code>tag</code>, if any. If none, returns
035 * <code>null</code>.<p>
036 *
037 * Note, if you want to know whether a variable is
038 * <code>non_null</code> or <code>nullable</code> (outside of called
039 * within AnnotationHandler, of course), use method
040 * {@link escjava.AnnotationHandler.getNonNullAndNullable(javafe.ast.RoutineDecl)}
041 * instead, for it properly handles inheritance of
042 * <code>non_null</code> and <code>nullable</code> pragmas.
043 **/
044 static public ModifierPragma findModifierPragma(/*@ non_null */ GenericVarDecl vdecl,
045 int tag) {
046 return findModifierPragma(vdecl.pmodifiers,tag);
047 }
048
049 static public ModifierPragma findModifierPragma(ModifierPragmaVec mp,
050 int tag) {
051 if (mp != null) {
052 for (int j = 0; j < mp.size(); j++) {
053 ModifierPragma prag= mp.elementAt(j);
054 if (prag.getTag() == tag)
055 return prag;
056 }
057 }
058 return null; // not present
059 }
060
061 static public void removeModifierPragma(/*@ non_null */ GenericVarDecl vdecl, int tag) {
062 removeModifierPragma(vdecl.pmodifiers,tag);
063 }
064
065 static public void removeModifierPragma(ModifierPragmaVec p, int tag) {
066 if (p != null) {
067 for (int j = 0; j < p.size(); j++) {
068 ModifierPragma prag= p.elementAt(j);
069 if (prag.getTag() == tag) {
070 p.removeElementAt(j);
071 --j;
072 }
073 }
074 }
075 }
076
077 static public boolean isModel(javafe.ast.FieldDecl fd) {
078 return isModel(fd.pmodifiers);
079 }
080
081 static public boolean isModel(ModifierPragmaVec m) {
082 if (m == null) return false;
083 return findModifierPragma(m,TagConstants.MODEL) != null;
084 }
085
086 // Used for designator expressions, as in a modifies clause.
087 static public boolean isModel(Expr e) {
088 if (e instanceof VariableAccess) {
089 VariableAccess va = (VariableAccess)e;
090 if (va.decl instanceof FieldDecl) {
091 return isModel( (FieldDecl)va.decl );
092 }
093 //System.out.println("ISMODEL-VA " + va.decl.getClass());
094 } else if (e instanceof FieldAccess) {
095 return isModel( ((FieldAccess)e).decl );
096 } else if (e instanceof NothingExpr) {
097 return true;
098 } else if (e instanceof EverythingExpr) {
099 return false;
100 } else if (e instanceof ArrayRefExpr) {
101 return isModel( ((ArrayRefExpr)e).array );
102 } else if (e instanceof ArrayRangeRefExpr) {
103 return isModel( ((ArrayRangeRefExpr)e).array );
104 } else if (e instanceof WildRefExpr) {
105 return false;
106 } else if (e instanceof NaryExpr) {
107 // This can occur if \dttfsa is used in a modifies clause
108 return false;
109 } else {
110 //System.out.println(EscPrettyPrint.inst.toString(e));
111 //System.out.println("ISMODEL " + e.getClass());
112 //ErrorSet.dump(null);
113 }
114 return false; // default
115 }
116
117 static public abstract class BooleanDecoration extends ASTDecoration {
118 private static final Object decFALSE = new Object();
119 private static final Object decTRUE = new Object();
120 public BooleanDecoration(String s) {
121 super(s);
122 }
123 public void set(ASTNode o, boolean b) {
124 set(o, b?decTRUE:decFALSE);
125 }
126 public boolean isTrue(ASTNode o) {
127 Object res = get(o);
128 if (res == null) {
129 boolean b = calculate(o);
130 set(o,b);
131 return b;
132 }
133 return res == decTRUE;
134 }
135 public abstract boolean calculate(ASTNode o);
136 }
137
138 static private BooleanDecoration pureDecoration = new BooleanDecoration("pure") {
139 public boolean calculate(ASTNode o) {
140 RoutineDecl rd = (RoutineDecl)o;
141 return findPurePragma(rd) != null;
142 }
143 };
144 static public boolean isPure(RoutineDecl rd) {
145 return pureDecoration.isTrue(rd);
146 }
147 static public void setPure(RoutineDecl rd) {
148 pureDecoration.set(rd,true);
149 }
150 static public ModifierPragma findPurePragma(RoutineDecl rd) {
151 ModifierPragma m = null;
152 m = findModifierPragma(rd.pmodifiers,TagConstants.PURE);
153 if (m!=null) return m;
154 m = findModifierPragma(rd.parent.pmodifiers,TagConstants.PURE);
155 if (m != null) return m;
156 if (rd instanceof MethodDecl) {
157 MethodDecl md = (MethodDecl)rd;
158 Set direct = javafe.tc.PrepTypeDeclaration.getInst().getOverrides(md.parent, md);
159 Enumeration e = direct.elements();
160 while (e.hasMoreElements()) {
161 MethodDecl directMD = (MethodDecl)e.nextElement();
162 m = findPurePragma(directMD);
163 if (m != null) return m;
164 }
165 }
166 return null;
167 }
168 private static final BooleanDecoration immutableDecoration = new BooleanDecoration("immutable") {
169 public boolean calculate(ASTNode o) {
170 return findModifierPragma(((TypeDecl)o).pmodifiers, TagConstants.IMMUTABLE)
171 != null ;
172 //|| findModifierPragma(((TypeDecl)o).pmodifiers, TagConstants.PURE) != null;
173 }
174 };
175 public static boolean isImmutable(TypeDecl cd) {
176 return immutableDecoration.isTrue(cd);
177 }
178
179 public static final BooleanDecoration ensuresDecoration = new BooleanDecoration("ensuresFromException") {
180 public boolean calculate(ASTNode o) {
181 return false;
182 }
183 };
184
185 private static final BooleanDecoration allocatesDecoration = new BooleanDecoration("allocates") {
186 public boolean calculate(ASTNode o) {
187 if (!(o instanceof MethodDecl)) {
188 //System.out.println("CALLING ALLOCATES ON NOT METHOD " + Location.toString(o.getStartLoc()));
189 return true;
190 }
191 MethodDecl rd = (MethodDecl)o;
192 javafe.util.Set ov = escjava.tc.FlowInsensitiveChecks.getDirectOverrides((MethodDecl)rd);
193 Enumeration k = ov.elements();
194 while (k.hasMoreElements()) {
195 if (isAllocates( (MethodDecl)k.nextElement() )) {
196 //System.out.println("PARENT ALLOCATES " + rd.id() + " " + Location.toString(rd.getStartLoc()));
197 return true;
198 }
199 }
200 ModifierPragmaVec mpv = rd.pmodifiers;
201 for (int i=0; i<mpv.size(); ++i) {
202 ModifierPragma m = mpv.elementAt(i);
203 if (m instanceof ExprModifierPragma) {
204 if (checkForFresh( ((ExprModifierPragma)m).expr )) {
205 //System.out.println("ENSURES ALLOCATES " + rd.id() + " " + Location.toString(m.getStartLoc()));
206 return true;
207 }
208 } else if (m instanceof VarExprModifierPragma) {
209 if (checkForFresh( ((VarExprModifierPragma)m).expr )) {
210 //System.out.println("SIGNALS ALLOCATES " + rd.id() + " " + Location.toString(m.getStartLoc()));
211 return true;
212 }
213 }
214 }
215 return false;
216 }
217
218 private boolean checkForFresh(ExprVec ev) {
219 for (int i=0; i<ev.size(); ++i) {
220 if (checkForFresh(ev.elementAt(i))) return true;
221 }
222 return false;
223 }
224 private boolean checkForFresh(Expr e) {
225 if (e == null) return false;
226 else if (e instanceof BinaryExpr) {
227 BinaryExpr be = (BinaryExpr)e;
228 return checkForFresh(be.left) || checkForFresh(be.right);
229 } else if (e instanceof UnaryExpr) {
230 UnaryExpr ue = (UnaryExpr)e;
231 return checkForFresh(ue.expr);
232 } else if (e instanceof NaryExpr) {
233 NaryExpr ne = (NaryExpr)e;
234 if (ne.op == TagConstants.FRESH) return true;
235 return checkForFresh(ne.exprs);
236 } else if (e instanceof MethodInvocation) {
237 MethodInvocation mi = (MethodInvocation)e;
238 if (mi.od instanceof ExprObjectDesignator) {
239 if ( checkForFresh( ((ExprObjectDesignator)mi.od).expr )) return true;
240 }
241 return checkForFresh(mi.args);
242 } else if (e instanceof ArrayRefExpr) {
243 return checkForFresh( ((ArrayRefExpr)e).index) ||
244 checkForFresh( ((ArrayRefExpr)e).array) ;
245 } else if (e instanceof CondExpr) {
246 return checkForFresh( ((CondExpr)e).test ) ||
247 checkForFresh( ((CondExpr)e).thn ) ||
248 checkForFresh( ((CondExpr)e).els );
249 } else if (e instanceof CastExpr) {
250 return checkForFresh( ((CastExpr)e).expr );
251 } else if (e instanceof ParenExpr) {
252 return checkForFresh( ((ParenExpr)e).expr );
253 } else if (e instanceof LabelExpr) {
254 return checkForFresh( ((LabelExpr)e).expr );
255 } else if (e instanceof FieldAccess) {
256 FieldAccess fa = (FieldAccess)e;
257 if (fa.od instanceof ExprObjectDesignator) {
258 if ( checkForFresh( ((ExprObjectDesignator)fa.od).expr )) return true;
259 }
260 return false;
261 } else if (e instanceof NewArrayExpr) {
262 NewArrayExpr nae = (NewArrayExpr)e;
263 return checkForFresh( nae.dims );
264 // FIXME - what about array initializers?
265 } else if (e instanceof NewInstanceExpr) {
266 NewInstanceExpr nie = (NewInstanceExpr)e;
267 return checkForFresh( nie.args );
268 } else if (e instanceof SetCompExpr) {
269 return checkForFresh( ((SetCompExpr)e).expr );
270 } else if (e instanceof LiteralExpr) {
271 return false;
272 } else if (e instanceof VariableAccess) {
273 return false;
274 } else if (e instanceof ThisExpr) {
275 return false;
276 } else if (e instanceof ResExpr) {
277 return false;
278 } else if (e instanceof escjava.ast.TypeExpr) {
279 return false;
280 } else if (e instanceof LockSetExpr) {
281 return false;
282 } else if (e instanceof NotModifiedExpr) {
283 return false;
284 } else if (e instanceof InstanceOfExpr) {
285 return false;
286 } else if (e instanceof ClassLiteral) {
287 return false;
288 } else if (e instanceof QuantifiedExpr) {
289 return checkForFresh( ((QuantifiedExpr)e).expr) ||
290 checkForFresh( ((QuantifiedExpr)e).rangeExpr) ;
291 } else if (e instanceof GeneralizedQuantifiedExpr ) {
292 return checkForFresh( ((GeneralizedQuantifiedExpr)e).expr) ||
293 checkForFresh( ((GeneralizedQuantifiedExpr)e).rangeExpr) ;
294 } else if (e instanceof NumericalQuantifiedExpr) {
295 return checkForFresh( ((NumericalQuantifiedExpr)e).expr) ||
296 checkForFresh( ((NumericalQuantifiedExpr)e).rangeExpr) ;
297 } else {
298 System.out.println("CLASS " + e.getClass());
299 return true;
300 }
301 }
302 };
303 public static boolean isAllocates(RoutineDecl rd) {
304 return allocatesDecoration.isTrue(rd);
305 }
306
307 private static final BooleanDecoration functionDecoration = new BooleanDecoration("function") {
308 public boolean calculate(ASTNode o) {
309 RoutineDecl rd = (RoutineDecl)o;
310 if (findModifierPragma(rd.pmodifiers,TagConstants.FUNCTION)
311 != null) return true;
312 if (!isPure(rd)) return false;
313 // If non-static, the owning class must be immutable
314 // But it can't override non-function methods
315 // Constructors don't depend on the owning class
316 if (!Modifiers.isStatic(rd.modifiers) && (rd instanceof MethodDecl)) {
317 if ( ! isImmutable(rd.parent) ) return false;
318 if (isAllocates(rd)) return false;
319 javafe.util.Set ov = escjava.tc.FlowInsensitiveChecks.getAllOverrides((MethodDecl)rd);
320 Enumeration i = ov.elements();
321 while (i.hasMoreElements()) {
322 if (!isFunction( (MethodDecl)i.nextElement() )) return false;
323 }
324 }
325 // All argument types must be primitive or immutable
326 FormalParaDeclVec args = rd.args;
327 for (int i=0; i<args.size(); ++i) {
328 FormalParaDecl f = args.elementAt(i);
329 Type t = f.type;
330 if (t instanceof TypeName) t = TypeSig.getSig((TypeName)t);
331 if (t instanceof PrimitiveType) continue;
332 if (t instanceof ArrayType) return false;
333 if (t instanceof TypeSig) {
334 if (! isImmutable(((TypeSig)t).getTypeDecl())) return false;
335 }
336 }
337 return true;
338 }
339 };
340 public static boolean isFunction(RoutineDecl rd) {
341 return functionDecoration.isTrue(rd);
342 }
343
344
345 public static final ASTDecoration exceptionDecoration =
346 new ASTDecoration("originalExceptions");
347
348 public static final ASTDecoration axiomDecoration = new ASTDecoration("axioms");
349
350 public static final ASTDecoration representsDecoration =
351 new ASTDecoration("representsClauses");
352
353 public static final ASTDecoration owningDecl = new ASTDecoration("owningDecl");
354 public static final ASTDecoration allSpecs = new ASTDecoration("allSpecs");
355
356 static public ModifierPragmaVec getAllSpecs(RoutineDecl rd) {
357 Object o = allSpecs.get(rd);
358 if (o != null) return (ModifierPragmaVec)o;
359 ModifierPragmaVec result = ModifierPragmaVec.make();
360 allSpecs.set(rd,result);
361 result.append(rd.pmodifiers);
362 if (rd instanceof ConstructorDecl) return result;
363 MethodDecl rrd = (MethodDecl)rd;
364 Type[] argtypes = rd.argTypes();
365 TypeSig td = TypeSig.getSig(rd.parent);
366 java.util.Iterator i = td.superInterfaces().iterator();
367 td = td.superClass();
368 while (td != null) {
369 MethodDecl md = td.hasMethod(rrd.id, argtypes);
370 if (md != null) result.append(md.pmodifiers);
371 td = td.superClass();
372 }
373
374 while (i.hasNext()) {
375 td = (TypeSig)i.next();
376 MethodDecl md = td.hasMethod(rrd.id, argtypes);
377 if (md != null) result.append(md.pmodifiers);
378 }
379
380 return result;
381 }
382
383 public static final ASTDecoration inheritedSpecs = new ASTDecoration("inheritedSpecs");
384
385 static public ModifierPragmaVec getInheritedSpecs(RoutineDecl rd) {
386 IdentifierNode fullName = IdentifierNode.make(escjava.translate.TrAnExpr.fullName(rd,false));
387 Object o = inheritedSpecs.get(fullName);
388 if (o != null) return (ModifierPragmaVec)o;
389 ModifierPragmaVec result = ModifierPragmaVec.make();
390 inheritedSpecs.set(fullName,result);
391 return result;
392 }
393
394 static public ModifierPragmaVec addInheritedSpecs(RoutineDecl rd, ModifierPragmaVec mp) {
395 ModifierPragmaVec mpv = Utils.getInheritedSpecs(rd);
396 mpv.append(mp);
397 ExprModifierPragma req = null;
398 int index = 0;
399 for (int i=0; i<mpv.size(); ++i) {
400 ModifierPragma m = mpv.elementAt(i);
401 if (m.getTag() != TagConstants.REQUIRES) continue;
402 if (req == null) { req = (ExprModifierPragma)m; index = i; continue; }
403 req = escjava.AnnotationHandler.or(req,(ExprModifierPragma)m);
404 mpv.setElementAt(req,index);
405 mpv.removeElementAt(i);
406 --i;
407 }
408 return mpv;
409 }
410
411 }
412