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