001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.translate; 004 005 import java.util.Hashtable; 006 import java.util.Enumeration; 007 import java.util.LinkedList; 008 import java.util.ArrayList; 009 import java.util.ListIterator; 010 011 import javafe.ast.*; 012 import javafe.tc.*; 013 import javafe.util.Location; 014 import javafe.util.Assert; 015 import javafe.util.Info; 016 import javafe.util.Set; 017 import javafe.util.ErrorSet; 018 import escjava.ast.*; 019 import escjava.ast.TagConstants; 020 import escjava.ast.Modifiers; 021 import escjava.Main; 022 import escjava.tc.Types; 023 import escjava.parser.OldVarDecl; 024 025 import escjava.prover.Atom; 026 027 /** Translates Annotation Expressions to GCExpr. */ 028 029 public class TrAnExpr { 030 031 /** This hashtable keeps track of cautions issued, with respect to 032 * using variables in \old pragmas that were not mentioned in modifies 033 * pragmas. The purpose of this hashtable is to prevent issuing 034 * duplicate cautions. 035 **/ 036 037 // NOT USED private static Set issuedPRECautions = new Set(); 038 039 private static int newStringCount = 0; 040 041 public static Translate translate = null; 042 043 /** This is the abbreviated form of function <code>TrSpecExpr</code> 044 * described in ESCJ 16. It is a shorthand for the full form in which 045 * <code>sp</code> and <code>st</code> are passed in as empty maps. 046 **/ 047 048 public static Expr trSpecExpr(Expr e) { 049 return trSpecExpr(e, null, null); 050 } 051 052 public static Expr trSpecExpr(Expr e, Expr thisExpr) { 053 try { 054 specialThisExpr = thisExpr; 055 return trSpecExpr(e); 056 } finally { 057 specialThisExpr = null; 058 } 059 } 060 061 // inits if not already inited 062 public static void initForClause(boolean b) { 063 if (!extraSpecs) initForClause(); 064 } 065 public static void initForClause() { 066 extraSpecs = true; 067 trSpecExprAuxConditions = ExprVec.make(); 068 trSpecExprAuxAssumptions = ExprVec.make(); 069 trSpecAuxAxiomsNeeded = new java.util.HashSet(); 070 trSpecModelVarsUsed = new java.util.HashMap(); 071 boundStack.clear(); 072 } 073 074 public static void closeForClause() { 075 extraSpecs = false; 076 trSpecExprAuxConditions = null; 077 boundStack.clear(); 078 } 079 080 public static void initForRoutine() { 081 extraSpecs = false; 082 trSpecExprAuxConditions = null; 083 tempn = 100; 084 declStack = new LinkedList(); 085 currentAlloc = GC.allocvar; 086 currentState = GC.statevar; 087 boundStack = new LinkedList(); 088 maxLevel = Main.options().rewriteDepth; 089 } 090 091 public static boolean doRewrites() { 092 return extraSpecs; 093 } 094 095 public static int level = 0; 096 public static int maxLevel = 3; // FIXME if this is much bigger the JML specs file java.math.BigInteger.parse runs out of memory 097 public static boolean extraSpecs = false; 098 public static ExprVec trSpecExprAuxConditions = null; 099 public static ExprVec trSpecExprAuxAssumptions = null; 100 public static java.util.Map trSpecModelVarsUsed = null; 101 public static java.util.Set trSpecAuxAxiomsNeeded = null; 102 public static int tempn = 100; 103 public static LinkedList declStack = new LinkedList(); 104 public static VariableAccess currentAlloc = GC.allocvar; 105 public static VariableAccess currentState = GC.statevar; 106 public static LinkedList boundStack; 107 108 /** This is the full form of function <code>TrSpecExpr</code> 109 * described in ESCJ 16. Each of the parameters <code>sp</code> 110 * and <code>st</code> is allowed to be null, which is interpreted 111 * as the empty map. 112 **/ 113 114 protected static Expr specialResultExpr = null; 115 protected static Expr specialThisExpr = null; 116 117 protected static TrAnExpr inst = new TrAnExpr(); 118 119 public static Expr trSpecExpr(Expr e, Hashtable sp, Hashtable st, Expr thisExpr) { 120 try { 121 specialThisExpr = thisExpr; 122 return trSpecExpr(e,sp,st); 123 } finally { 124 specialThisExpr = null; 125 } 126 } 127 public static Expr trSpecExpr(Expr e, Hashtable sp, Hashtable st) { 128 return inst.trSpecExprI(e,sp,st); 129 } 130 131 public Expr trSpecExprI(Expr e, Hashtable sp, Hashtable st) { 132 int tag = e.getTag(); 133 switch (tag) { 134 case TagConstants.THISEXPR: { 135 ThisExpr t = (ThisExpr)e; 136 Expr a; 137 if (t.classPrefix != null) { 138 a = trSpecExprI(Inner.unfoldThis(t), sp, st); 139 } else if (specialThisExpr != null) { 140 a = specialThisExpr; 141 } else { 142 a = apply(sp, makeVarAccess(GC.thisvar.decl, e.getStartLoc())); 143 } 144 return a; 145 } 146 147 // Literals (which are already GCExpr's 148 case TagConstants.BOOLEANLIT: 149 case TagConstants.CHARLIT: 150 case TagConstants.DOUBLELIT: 151 case TagConstants.FLOATLIT: 152 case TagConstants.INTLIT: 153 case TagConstants.LONGLIT: 154 case TagConstants.NULLLIT: 155 return e; 156 157 case TagConstants.STRINGLIT: 158 { String s = ((LiteralExpr)e).value.toString(); 159 Expr ee = GC.nary(TagConstants.INTERN, 160 GC.symlit(Translate.Strings.intern(s).toString()), 161 GC.symlit(Integer.toString(s.length())) ); 162 return ee; 163 } 164 165 case TagConstants.RESEXPR: 166 if (specialResultExpr != null) return specialResultExpr; 167 return apply(sp, makeVarAccess(GC.resultvar.decl, e.getStartLoc())); 168 169 case TagConstants.LOCKSETEXPR: 170 return apply(sp, makeVarAccess(GC.LSvar.decl, e.getStartLoc())); 171 172 case TagConstants.VARIABLEACCESS: { 173 VariableAccess va = (VariableAccess)e; 174 if (va.decl instanceof OldVarDecl) { 175 // variable declared in an old pragma (not the \old fcn.) 176 VarInit vi = ((OldVarDecl)va.decl).init; 177 if (vi instanceof Expr) { 178 return trSpecExpr( (Expr)vi, sp, st); 179 } else { 180 ErrorSet.fatal(e.getStartLoc(), 181 "Have not implemented array initializers in old annotations"); 182 } 183 } else { 184 // local variable, parameter, or bound variable 185 return apply(sp, va); 186 } 187 } 188 189 case TagConstants.FIELDACCESS: { 190 FieldAccess fa = (FieldAccess)e; 191 VariableAccess va = makeVarAccess(fa.decl, fa.locId); 192 boolean treatLikeAField = false; 193 // va accesses the field 194 if (Utils.isModel(va.decl.pmodifiers)) { 195 // Treat a model variable like a field if (a) it has no 196 // represents clauses and (b) it is not modified. 197 198 ObjectDesignator od = fa.od; 199 TypeSig ts = null; 200 if (od == null) { 201 System.out.println("OD NULL"); // FIXME 202 // SHould use the TypeSIg of the class being translated 203 } else { 204 ts = (TypeSig)od.type(); 205 } 206 TypeDeclElemVec reps = ts == null ? null : // FIXME 207 GetSpec.getRepresentsClauses( 208 null /*ts.getTypeDecl()*/, fa.decl); 209 if (reps == null || reps.size() == 0) { 210 //boolean b = translate.frameHandler.isDefinitelyNotAssignable( 211 // (od instanceof ExprObjectDesignator) ? 212 // ((ExprObjectDesignator)od).expr : null ,fa.decl); 213 treatLikeAField = true; 214 } 215 //System.out.println("TREATLIKEAFIELD " + treatLikeAField + " " + doRewrites() + " " + fa + " " + Location.toString(fa.getStartLoc()) ); 216 //System.out.println("MODEL VAR " + fa.decl.id + " " + Location.toString(fa.locId)); 217 if (!treatLikeAField && doRewrites()) { 218 trSpecAuxAxiomsNeeded.add(new RepHelper(fa)); 219 Identifier id = representsMethodName(va); 220 if (Modifiers.isStatic(fa.decl.modifiers)) { 221 return GC.nary(id,stateVar(sp)); // FIXME or should this be a function of the class object 222 } 223 } else { // Treat like a field - only good if the model 224 // variable is not modified, since modifications 225 // to model vars are not by assignment. 226 227 /* 228 java.util.List reps = escjava.AnnotationHandler.findRepresents(fa.decl); 229 java.util.Iterator it = reps.iterator(); 230 while (it.hasNext()) { 231 Expr ex = (Expr)it.next(); 232 233 if (doRewrites() && !declStack.contains(fa.decl)) { 234 declStack.addFirst(fa.decl); 235 if (trSpecModelVarsUsed != null && 236 !trSpecModelVarsUsed.containsKey(fa.decl) ) trSpecModelVarsUsed.put(fa.decl,va); 237 238 Hashtable h = new Hashtable(); 239 if (fa.od instanceof ExprObjectDesignator) { 240 if (!(((ExprObjectDesignator)fa.od).expr instanceof ThisExpr)) { 241 h.put(Substitute.thisexpr, ((ExprObjectDesignator)fa.od).expr); 242 } 243 } else if (fa.od instanceof SuperObjectDesignator) { 244 // FIXME 245 System.out.println("NOT SUPPORTED-A " + fa.od.getClass()); 246 } // fall-through for TypeObjectDesignator 247 248 ex = Substitute.doSubst(h,ex); 249 Expr ee = trSpecExpr(ex,sp,st); 250 trSpecExprAuxConditions.addElement(ee); 251 declStack.removeFirst(); 252 } 253 } 254 */ 255 } 256 } 257 258 if (Modifiers.isStatic(fa.decl.modifiers)) { 259 //fa.od.getTag() == TagConstants.TYPEOBJECTDESIGNATOR) 260 VariableAccess nva = apply(sp, va); 261 return nva; 262 } else { 263 // select expression whose rhs is an instance variable 264 Expr lhs; 265 switch (fa.od.getTag()) { 266 case TagConstants.EXPROBJECTDESIGNATOR: { 267 ExprObjectDesignator eod = (ExprObjectDesignator)fa.od; 268 lhs = trSpecExpr(eod.expr, sp, st); 269 break; 270 } 271 272 case TagConstants.SUPEROBJECTDESIGNATOR: 273 lhs = apply(sp, makeVarAccess(GC.thisvar.decl, 274 fa.od.getStartLoc())); 275 break; 276 277 default: 278 //@ unreachable; 279 Assert.fail("Fall thru; tag = " 280 + escjava.ast.TagConstants.toString(fa.od.getTag())); 281 lhs = null; // dummy assignment 282 } 283 284 if (fa.decl == Types.lengthFieldDecl) { 285 return GC.nary(fa.getStartLoc(), fa.getEndLoc(), 286 TagConstants.ARRAYLENGTH, lhs); 287 } else if (Utils.isModel(va.decl.pmodifiers) && !treatLikeAField && doRewrites()) { 288 Identifier id = representsMethodName(va); 289 ExprVec arg = ExprVec.make(2); 290 arg.addElement(stateVar(sp)); 291 arg.addElement(lhs); 292 return GC.nary(id,arg); 293 } else { 294 return GC.nary(fa.getStartLoc(), fa.getEndLoc(), 295 TagConstants.SELECT, apply(sp, va), lhs); 296 } 297 } 298 } 299 300 case TagConstants.ARRAYREFEXPR: { 301 ArrayRefExpr r = (ArrayRefExpr)e; 302 303 if (TypeCheck.inst.getType(r.array).getTag() == TagConstants.LOCKSET) { 304 return GC.nary(r.array.getStartLoc(), r.locCloseBracket, 305 TagConstants.SELECT, 306 trSpecExpr(r.array, sp, st), 307 trSpecExpr(r.index, sp, st)); 308 } else { 309 VariableAccess elems = apply(sp, makeVarAccess(GC.elemsvar.decl, 310 e.getStartLoc())); 311 Expr e0 = trSpecExpr(r.array, sp, st); 312 Expr e1 = trSpecExpr(r.index, sp, st); 313 Expr a = GC.nary(TagConstants.SELECT, elems, e0); 314 return GC.nary(r.array.getStartLoc(), r.locCloseBracket, 315 TagConstants.SELECT, a, e1); 316 } 317 } 318 319 case TagConstants.ARRAYRANGEREFEXPR: 320 case TagConstants.WILDREFEXPR: 321 return null; 322 323 case TagConstants.PARENEXPR: { 324 // drop parens 325 ParenExpr pe = (ParenExpr)e; 326 return trSpecExpr(pe.expr, sp, st); 327 } 328 329 // Unary operator expressions 330 331 case TagConstants.UNARYSUB: 332 case TagConstants.NOT: 333 case TagConstants.BITNOT: { 334 UnaryExpr ue = (UnaryExpr)e; 335 int newtag = getGCTagForUnary(ue); 336 return GC.nary(ue.getStartLoc(), ue.getEndLoc(), newtag, 337 trSpecExpr(ue.expr, sp, st)); 338 } 339 340 case TagConstants.UNARYADD: { 341 // drop UnaryADD 342 UnaryExpr ue = (UnaryExpr)e; 343 return trSpecExpr(ue.expr, sp, st); 344 } 345 346 case TagConstants.TYPEOF: 347 case TagConstants.ELEMTYPE: 348 case TagConstants.MAX: 349 { 350 Assert.notFalse(((NaryExpr)e).exprs.size() == 1); 351 NaryExpr ne = (NaryExpr)e; 352 int n = ne.exprs.size(); 353 ExprVec exprs = ExprVec.make(n); 354 for (int i = 0; i < n; i++) { 355 exprs.addElement(trSpecExpr(ne.exprs.elementAt(i), sp, st)); 356 } 357 return GC.nary(ne.getStartLoc(), ne.getEndLoc(), ne.getTag(), exprs); 358 } 359 360 case TagConstants.DTTFSA: { 361 NaryExpr ne = (NaryExpr)e; 362 int n = ne.exprs.size(); 363 ExprVec exprs = ExprVec.make(n); 364 if (n>0) exprs.addElement(trSpecExpr(ne.exprs.elementAt(0), sp, st)); 365 if (n>1) exprs.addElement(ne.exprs.elementAt(1)); // This is a String - don't want to intern it 366 for (int i = 2; i < n; i++) { 367 exprs.addElement(trSpecExpr(ne.exprs.elementAt(i), sp, st)); 368 } 369 return GC.nary(ne.getStartLoc(), ne.getEndLoc(), ne.getTag(), exprs); 370 } 371 372 case TagConstants.ELEMSNONNULL: { 373 NaryExpr ne = (NaryExpr)e; 374 VariableAccess elems = apply(sp, makeVarAccess(GC.elemsvar.decl, 375 e.getStartLoc())); 376 377 return GC.nary(ne.getStartLoc(), ne.getEndLoc(), ne.getTag(), 378 trSpecExpr(ne.exprs.elementAt(0), sp, st), elems); 379 } 380 381 // Binary operator expressions 382 383 case TagConstants.OR: 384 case TagConstants.AND: 385 case TagConstants.IMPLIES: 386 case TagConstants.IFF: 387 case TagConstants.NIFF: 388 case TagConstants.BITOR: 389 case TagConstants.BITAND: 390 case TagConstants.BITXOR: 391 { 392 BinaryExpr be = (BinaryExpr)e; 393 int newtag = getGCTagForBinary(be); 394 return GC.nary(be.getStartLoc(), be.getEndLoc(), 395 newtag, 396 trSpecExpr(be.left, sp, st), 397 trSpecExpr(be.right, sp, st)); 398 } 399 400 case TagConstants.EQ: 401 case TagConstants.NE: 402 case TagConstants.LSHIFT: 403 case TagConstants.RSHIFT: 404 case TagConstants.URSHIFT: 405 { // FIXME - do these have any type matching to do? 406 BinaryExpr be = (BinaryExpr)e; 407 int newtag = getGCTagForBinary(be); 408 return GC.nary(be.getStartLoc(), be.getEndLoc(), 409 newtag, 410 trSpecExpr(be.left, sp, st), 411 trSpecExpr(be.right, sp, st)); 412 } 413 414 case TagConstants.GE: 415 case TagConstants.GT: 416 case TagConstants.LE: 417 case TagConstants.LT: 418 case TagConstants.ADD: 419 case TagConstants.SUB: 420 case TagConstants.DIV: 421 case TagConstants.MOD: 422 case TagConstants.STAR: 423 { 424 // Must do appropriate primitive type casting to make arguments the same type 425 // FIXME - what about + on strings? 426 BinaryExpr be = (BinaryExpr)e; 427 //EscPrettyPrint.inst.print(System.out,0,be); 428 int newtag = getGCTagForBinary(be); 429 Expr left = trSpecExpr(be.left, sp, st); 430 Expr right = trSpecExpr(be.right, sp, st); 431 /* 432 int leftType = ((PrimitiveType)TypeCheck.inst.getType(be.left)).getTag(); 433 int rightType = ((PrimitiveType)TypeCheck.inst.getType(be.right)).getTag(); 434 // FIXME - do we need to do any promotion ? 435 if (leftType != rightType && false) { 436 System.out.println("TYPES " + TagConstants.toString(newtag) + " " + TagConstants.toString(leftType) + " " + TagConstants.toString(rightType)); 437 } 438 */ 439 if (newtag == TagConstants.STRINGCAT) { 440 ExprVec ev = ExprVec.make(3); 441 ev.addElement(left); 442 ev.addElement(right); 443 ev.addElement(GC.nary(Identifier.intern("next"), 444 GC.allocvar, LiteralExpr.make(TagConstants.INTLIT,new Integer(++newStringCount),Location.NULL))); 445 return GC.nary(be.getStartLoc(), be.getEndLoc(), 446 newtag, ev); 447 } else { 448 return GC.nary(be.getStartLoc(), be.getEndLoc(), 449 newtag, left, right); 450 } 451 } 452 453 case TagConstants.NEWINSTANCEEXPR: { 454 NewInstanceExpr me = (NewInstanceExpr)e; 455 Type type = TypeCheck.inst.getType(me); 456 Expr v; 457 VariableAccess vv = tempName(e.getStartLoc(),"tempNewObject",type); 458 if (boundStack.size() == 0) { 459 v = vv; 460 } else { 461 ExprVec ev = ExprVec.make(); 462 java.util.Iterator ii = boundStack.iterator(); 463 while (ii.hasNext()) { 464 Object o = ((QuantifiedExpr)ii.next()).vars; 465 if (o instanceof GenericVarDecl) { 466 GenericVarDecl g = (GenericVarDecl)o; 467 ev.addElement( VariableAccess.make(g.id, g.getStartLoc(), g) ); 468 } else if (o instanceof GenericVarDeclVec) { 469 GenericVarDeclVec gi = (GenericVarDeclVec)o; 470 for (int kk = 0; kk<gi.size(); ++kk) { 471 GenericVarDecl g = gi.elementAt(kk); 472 ev.addElement( VariableAccess.make(g.id, g.getStartLoc(), g) ); 473 } 474 } else System.out.print("[[" + o.getClass() + "]]"); 475 } 476 v = GC.nary(vv.id,ev); 477 //v = MethodInvocation.make(ExprObjectDesignator.make(Location.NULL,ThisExpr.make(null,Location.NULL)),vv.id,null, Location.NULL, Location.NULL, ev); 478 } 479 boolean genSimpleVar = false; 480 boolean genFunctionCallAndAxioms = false; 481 boolean genVarAndConditions = false; 482 boolean isFunction = Utils.isFunction(me.decl); 483 if ((isFunction||true) && doRewrites()) { 484 genFunctionCallAndAxioms = true; 485 } else if ( !doRewrites() 486 || level > maxLevel 487 || declStack.contains(me.decl) 488 ) { 489 genSimpleVar = true; 490 } else { 491 genVarAndConditions = true; 492 } 493 494 if (genSimpleVar) { 495 return v; 496 } else if (genVarAndConditions) { 497 ++level; 498 declStack.addFirst(me.decl); 499 // v is the variable that is the result of the constructor call 500 // Adds v != null 501 Expr ee = GC.nary(TagConstants.REFNE, v, 502 LiteralExpr.make(TagConstants.NULLLIT, null, Location.NULL)); 503 trSpecExprAuxConditions.addElement(ee); 504 // Adds \typeof(v) == \type(...) 505 ee = GC.nary(TagConstants.TYPEEQ, 506 GC.nary(TagConstants.TYPEOF, v), 507 TypeExpr.make(Location.NULL, Location.NULL, type)); 508 trSpecExprAuxConditions.addElement(ee); 509 // Adds alloc < newalloc 510 VariableAccess newAlloc = 511 apply(sp,GC.makeVar(GC.allocvar.id,e.getStartLoc())); // alloc 512 trSpecExprAuxAssumptions.addElement( 513 GC.nary(TagConstants.ALLOCLT, currentAlloc, newAlloc)); 514 // Adds ! isAllocated(v, alloc) 515 trSpecExprAuxConditions.addElement( 516 GC.nary(TagConstants.BOOLNOT, 517 GC.nary(TagConstants.ISALLOCATED, v, currentAlloc))); 518 // Adds isAllocated(v, newalloc) 519 trSpecExprAuxConditions.addElement( 520 GC.nary(TagConstants.ISALLOCATED, v, newAlloc)); 521 currentAlloc = newAlloc; 522 // Go add all the specs generated by substituting v for \result 523 // in the specs of the constructor 524 getCalledSpecs(me.decl,null,me.args,v,sp,st); // adds to trSpecExprAuxConditions 525 //System.out.println("END-NEWINST " + Location.toString(me.decl.getStartLoc()) + " " + declStack.contains(me.decl)); 526 declStack.removeFirst(); 527 --level; 528 return v; 529 } else if (genFunctionCallAndAxioms) { 530 531 trSpecAuxAxiomsNeeded.add(new RepHelper(me.decl.parent,me.decl)); 532 Identifier constructorname = fullName(me.decl,false); 533 VariableAccess newAlloc = 534 apply(sp,GC.makeVar(GC.allocvar.id,e.getStartLoc())); // alloc 535 ExprVec ev = ExprVec.make(me.args.size()+4); 536 // FIXME - enclosingInstance ??? 537 if (!isFunction) { 538 ev.addElement( stateVar(sp) ); 539 } 540 ev.addElement(currentAlloc); 541 ev.addElement(newAlloc); 542 for (int i=0; i<me.args.size(); ++i) { 543 ev.addElement( trSpecExpr( me.args.elementAt(i), sp, st)); 544 } 545 Expr ne = GC.nary(me.getStartLoc(), me.getEndLoc(), 546 constructorname,ev); 547 // Adds alloc < newalloc 548 trSpecExprAuxAssumptions.addElement( 549 GC.nary(TagConstants.ALLOCLT, currentAlloc, newAlloc)); 550 currentAlloc = newAlloc; 551 return ne; 552 } 553 } 554 555 case TagConstants.METHODINVOCATION: { 556 /* We can handle a method invocation in a spec expression in two ways. 557 a) We can turn the method invocation into a function call within the target 558 logic. The we add axioms for that function call corresponding to the 559 postconditions of the method in the Java program. We add the implicit this 560 parameter as an argument of the function if the method is not static. 561 The difficulty is that not all methods are functions; functions have equal 562 results if their arguments are equal. Methods don't necessarily satisfy this 563 because their arguments have structure that might change without the object 564 identity changing. Having immutable objects helps. 565 b) Alternatively we define a new constant corresponding to the result of the 566 method invocation. [If the method invocation is within the scope of 567 quantifiers, then we have to define a new function with the appropriate 568 arguments.] Then we add an assumption that the constant satisfies the 569 postconditions of the method (with \result replaced by the new constant). 570 The difficulties are that we need a new constant for each method invocations 571 and that we have to limit the depth since method postconditions can contain 572 more method calls. 573 */ 574 575 MethodInvocation me = (MethodInvocation)e; 576 577 // FIXME - when is me.decl null ? When it is a built-in method like 578 // \reach().has() 579 580 boolean isFunction = me.decl == null ? true : Utils.isFunction(me.decl); 581 // The above result will be true if the method is declared to be a function 582 // or if it has only immutable arguments. 583 584 Expr v; 585 VariableAccess vv = tempName(e.getStartLoc(),"tempMethodReturn", 586 TypeCheck.inst.getType(me)); 587 if (boundStack.size() == 0) { 588 v = vv; 589 } else { 590 ExprVec ev = ExprVec.make(); 591 java.util.Iterator ii = boundStack.iterator(); 592 while (ii.hasNext()) { 593 Object o = ((QuantifiedExpr)ii.next()).vars; 594 if (o instanceof GenericVarDecl) { 595 GenericVarDecl g = (GenericVarDecl)o; 596 ev.addElement( VariableAccess.make(g.id, g.getStartLoc(), g) ); 597 } else if (o instanceof GenericVarDeclVec) { 598 GenericVarDeclVec gi = (GenericVarDeclVec)o; 599 for (int kk = 0; kk<gi.size(); ++kk) { 600 GenericVarDecl g = gi.elementAt(kk); 601 ev.addElement( VariableAccess.make(g.id, g.getStartLoc(), g) ); 602 } 603 } else System.out.print("[[" + o.getClass() + "]]"); // FIXME 604 } 605 v = GC.nary(vv.id,ev); 606 } 607 /* 608 System.out.print("METHOD " + me.decl.parent.id + " " + me.decl.id + " " ); 609 EscPrettyPrint.inst.print(System.out,0,me.od); 610 System.out.println(""); 611 */ 612 613 boolean genSimpleVar = false; 614 boolean genFunctionCallAndAxioms = false; 615 boolean genVarAndConditions = false; 616 if (isFunction || true) { 617 genFunctionCallAndAxioms = true; 618 } else if (!doRewrites() 619 || level > maxLevel 620 || declStack.contains(me.decl) 621 ) { 622 genSimpleVar = true; 623 } else { 624 genVarAndConditions = true; 625 } 626 627 if (genSimpleVar) { 628 // Just replace the method invocation with a simple new variable 629 // We won't be able to reason about it because it will be unique. 630 return v; 631 } else if (genVarAndConditions) { 632 ++level; 633 declStack.addFirst(me.decl); 634 ExprVec ev = ExprVec.make(me.args.size()); 635 if (!Modifiers.isStatic(me.decl.modifiers)) { 636 if (me.od instanceof ExprObjectDesignator) { 637 Expr ex = ((ExprObjectDesignator)me.od).expr; 638 ev.addElement( trSpecExpr( ex, sp, st)); 639 } else { 640 // FIXME 641 System.out.println("NOT SUPPORTED-B " + me.od.getClass()); 642 } 643 } 644 645 getCalledSpecs(me.decl,me.od,me.args,v,sp,st); // adds to trSpecExprAuxConditions 646 --level; 647 declStack.removeFirst(); 648 return v; 649 } else if (genFunctionCallAndAxioms) { 650 if (doRewrites()) { 651 trSpecAuxAxiomsNeeded.add(new RepHelper(me.decl.parent,me.decl)); 652 } 653 ExprVec ev = ExprVec.make(me.args.size()+1); 654 boolean useSuper = false; 655 if (!isFunction) { 656 ev.addElement( stateVar(sp) ); 657 } 658 if (!Modifiers.isStatic(me.decl.modifiers)) { 659 if (me.od instanceof ExprObjectDesignator) { 660 Expr ex = ((ExprObjectDesignator)me.od).expr; 661 ev.addElement( trSpecExpr( ex, sp, st)); 662 } else { 663 useSuper = true; 664 ev.addElement( trSpecExpr(javafe.ast.ThisExpr.make(null,me.od.getStartLoc()),sp,st)); 665 // FIXME 666 //System.out.println("NOT SUPPORTED-C " + me.od.getClass()); 667 } 668 } 669 for (int i=0; i<me.args.size(); ++i) { 670 ev.addElement( trSpecExpr( me.args.elementAt(i), sp, st)); 671 } 672 Expr ne = GC.nary(me.getStartLoc(), me.getEndLoc(), 673 TagConstants.METHODCALL,ev); 674 ((NaryExpr)ne).methodName = fullName(me.decl,useSuper); 675 return ne; 676 } 677 } 678 679 case TagConstants.NEWARRAYEXPR: { 680 NewArrayExpr nae = (NewArrayExpr)e; 681 if (doRewrites() ) { 682 ExprVec ev = ExprVec.make(5); 683 ev.addElement(apply(sp,currentAlloc) ); // current alloc 684 VariableAccess newAlloc = GC.makeVar(GC.allocvar.id,nae.getStartLoc()); 685 ev.addElement(apply(sp,newAlloc) ); // new alloc value 686 trSpecExprAuxAssumptions.addElement( 687 GC.nary(TagConstants.ALLOCLT, currentAlloc, newAlloc)); 688 currentAlloc = newAlloc; 689 Expr edims = GC.nary( TagConstants.ARRAYSHAPEONE, 690 trSpecExpr( nae.dims.elementAt(0), sp, st)); 691 for (int kk = 1; kk < nae.dims.size(); ++kk) { 692 edims = GC.nary( TagConstants.ARRAYSHAPEMORE, 693 trSpecExpr( nae.dims.elementAt(kk), sp, st), edims); 694 } 695 ev.addElement(edims ); // arrayShape 696 Type t = TypeCheck.inst.getType(nae); 697 ev.addElement( TypeExpr.make(Location.NULL, Location.NULL, t) ); 698 ev.addElement(Types.zeroEquivalent(Types.baseType(t))); // initial value 699 return GC.nary(TagConstants.ARRAYMAKE,ev); 700 } else { 701 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings, 702 e.getStartLoc(),"Not checking predicates containing new array expressions"); 703 return null; 704 } 705 } 706 707 case TagConstants.EXPLIES: { 708 // handle as implies, but with arguments reversed 709 BinaryExpr be = (BinaryExpr)e; 710 return GC.nary(be.getStartLoc(), be.getEndLoc(), 711 TagConstants.BOOLIMPLIES, 712 trSpecExpr(be.right, sp, st), 713 trSpecExpr(be.left, sp, st)); 714 } 715 716 case TagConstants.SUBTYPE: { 717 BinaryExpr be = (BinaryExpr)e; 718 return GC.nary(be.getStartLoc(), be.getEndLoc(), 719 TagConstants.TYPELE, 720 trSpecExpr(be.left, sp, st), 721 trSpecExpr(be.right, sp, st)); 722 } 723 724 // Other expressions 725 726 case TagConstants.CONDEXPR: { 727 CondExpr ce = (CondExpr)e; 728 return GC.nary(ce.test.getStartLoc(), ce.test.getEndLoc(), 729 TagConstants.CONDITIONAL, 730 trSpecExpr(ce.test, sp, st), 731 trSpecExpr(ce.thn, sp, st), 732 trSpecExpr(ce.els, sp, st)); 733 } 734 735 case TagConstants.INSTANCEOFEXPR: { 736 InstanceOfExpr ie = (InstanceOfExpr)e; 737 Expr isOfType = GC.nary(ie.getStartLoc(), ie.getEndLoc(), 738 TagConstants.IS, 739 trSpecExpr(ie.expr, sp, st), 740 trType(ie.type)); 741 Expr notNull = GC.nary(ie.getStartLoc(), ie.getEndLoc(), 742 TagConstants.REFNE, 743 trSpecExpr(ie.expr, sp, st), 744 GC.nulllit); 745 746 return GC.and(ie.getStartLoc(), ie.getEndLoc(), 747 isOfType, 748 notNull); 749 } 750 751 case TagConstants.CASTEXPR: { 752 CastExpr ce = (CastExpr)e; 753 return GC.nary(ce.getStartLoc(), ce.getEndLoc(), TagConstants.CAST, 754 trSpecExpr(ce.expr, sp, st), 755 trType(ce.type)); 756 } 757 758 case TagConstants.CLASSLITERAL: { 759 ClassLiteral cl = (ClassLiteral)e; 760 return GC.nary(cl.getStartLoc(), cl.getEndLoc(), 761 TagConstants.CLASSLITERALFUNC, 762 trType(cl.type)); 763 } 764 765 case TagConstants.TYPEEXPR: 766 return e; 767 768 case TagConstants.REACH: { 769 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings, 770 e.getStartLoc(),"Not checking predicates containing reach expressions"); 771 // FIXME - ignore these till we can figure out how to reason 772 return null; 773 } 774 775 case TagConstants.NUM_OF: 776 case TagConstants.SUM: 777 case TagConstants.PRODUCT: 778 { 779 //ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings, 780 //e.getStartLoc(),"Not checking predicates containing generalized quantifier expressions"); 781 // FIXME - ignore these till we can figure out how to reason 782 // Not sure this is the correct type ??? FIXME 783 Type t = TypeCheck.inst.getType(e); 784 VariableAccess va = tempName(e.getStartLoc(),"quantvalue",t); 785 return va; 786 } 787 788 case TagConstants.MIN: 789 case TagConstants.MAXQUANT: 790 { 791 Type t = TypeCheck.inst.getType(e); 792 VariableAccess va = tempName(e.getStartLoc(),"quantvalue",t); 793 ExprVec args = ExprVec.make(); 794 args.addElement(GC.statevar); 795 if (boundStack.size() > 0) { 796 ListIterator iter = boundStack.listIterator(boundStack.size()); 797 while (iter.hasPrevious()) { 798 QuantifiedExpr qqe = (QuantifiedExpr)iter.previous(); 799 Object o = qqe.vars; 800 if (o instanceof GenericVarDecl) { 801 GenericVarDecl g = (GenericVarDecl)o; 802 args.addElement(VariableAccess.make(g.id,Location.NULL,g)); 803 } else if (o instanceof GenericVarDeclVec) { 804 GenericVarDeclVec gi = (GenericVarDeclVec)o; 805 for (int i=0; i<gi.size(); ++i) { 806 GenericVarDecl g = gi.elementAt(i); 807 args.addElement(VariableAccess.make(g.id,Location.NULL,g)); 808 } 809 } 810 } 811 } 812 Expr vaf = GC.nary(va.id, args); 813 GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e; 814 Expr tex = trSpecExpr(qe.expr,sp,st); 815 Expr rex = trSpecExpr(qe.rangeExpr,sp,st); 816 GenericVarDeclVec dummyDecls = GenericVarDeclVec.make(); 817 Expr goodTypes = rex; 818 for (int k=0; k<qe.vars.size(); ++k) { 819 GenericVarDecl decl = qe.vars.elementAt(k); 820 Assert.notFalse(sp == null || ! sp.contains(decl)); 821 Assert.notFalse(st == null || ! st.contains(decl)); 822 dummyDecls.addElement(decl); 823 824 goodTypes = GC.and(goodTypes, quantTypeCorrect(decl, sp)); 825 } 826 Expr ne = GC.implies( 827 GC.quantifiedExpr(Location.NULL, Location.NULL, 828 TagConstants.EXISTS, qe.vars, null, GC.and(goodTypes, rex), null, null), 829 GC.quantifiedExpr(Location.NULL, Location.NULL, 830 TagConstants.EXISTS, qe.vars, null, 831 GC.and(goodTypes, GC.nary(TagConstants.INTEGRALEQ, vaf, tex)), 832 null, null)); 833 ExprVec pats = ExprVec.make(); 834 pats.addElement(vaf); 835 if (boundStack.size() > 0) { 836 // FIXME - the following only works for one level of bound variable 837 // because of the pats - need to combine them all or maybe just put 838 // the pats at the innermost level 839 ListIterator iter = boundStack.listIterator(boundStack.size()); 840 ExprVec ppats = pats; 841 while (iter.hasPrevious()) { 842 QuantifiedExpr qqe = (QuantifiedExpr)iter.previous(); 843 Expr rrex = qqe.rangeExpr == null ? GC.truelit : 844 trSpecExpr(qqe.rangeExpr, sp, st); 845 Object o = qqe.vars; 846 if (o instanceof GenericVarDecl) { 847 GenericVarDecl g = (GenericVarDecl)o; 848 ne = GC.forallwithpats(g,GC.implies(rrex,ne),ppats); 849 ppats = null; 850 } else if (o instanceof GenericVarDeclVec) { 851 GenericVarDeclVec gi = (GenericVarDeclVec)o; 852 int kk = gi.size(); 853 while (--kk >= 0) { 854 GenericVarDecl g = gi.elementAt(kk); 855 ne = GC.forallwithpats(g,GC.implies(rrex,ne),ppats); 856 ppats = null; 857 } 858 } else System.out.print("[[" + o.getClass() + "]]"); 859 } 860 } 861 trSpecExprAuxAssumptions.addElement(ne); 862 if (tag == TagConstants.MIN) { 863 // (\min vars; rangeexpr; expr) generates the axioms 864 // (\forall vars; rangeexpr ==> va <= expr) and 865 // (\exists vars; rangeexpr) ==> (\exists vars; rangeexpr && va == expr) 866 ne = QuantifiedExpr.make(Location.NULL, Location.NULL, 867 TagConstants.FORALL, qe.vars, null, 868 GC.implies(goodTypes, GC.nary(TagConstants.INTEGRALLE, vaf, tex)), 869 null,null); // Use pats? FIXME 870 } else { 871 // (\max vars; rangeexpr; expr) generates the axioms 872 // (\forall vars; rangeexpr ==> va >= expr) and 873 // (\exists vars; rangeexpr) ==> (\exists vars; rangeexpr && va == expr) 874 ne = QuantifiedExpr.make(Location.NULL, Location.NULL, 875 TagConstants.FORALL, qe.vars, null, 876 GC.implies(goodTypes, GC.nary(TagConstants.INTEGRALGE, vaf, tex)), 877 null, null); // FIXME Use Pats? 878 } 879 if (boundStack.size() > 0) { 880 ListIterator iter = boundStack.listIterator(boundStack.size()); 881 while (iter.hasPrevious()) { 882 QuantifiedExpr qqe = (QuantifiedExpr)iter.previous(); 883 Expr rrex = qqe.rangeExpr == null ? GC.truelit : 884 trSpecExpr(qqe.rangeExpr, sp, st); 885 Object o = qqe.vars; 886 if (o instanceof GenericVarDecl) { 887 GenericVarDecl g = (GenericVarDecl)o; 888 ne = GC.forall(g,rrex,GC.implies(rrex,ne)); 889 } else if (o instanceof GenericVarDeclVec) { 890 GenericVarDeclVec gi = (GenericVarDeclVec)o; 891 ne = GC.forall(gi,rrex,GC.implies(rrex,ne)); 892 /* 893 int kk = gi.size(); 894 while (--kk >= 0) { 895 GenericVarDecl g = gi.elementAt(kk); 896 ne = GC.forall(g,rrex,GC.implies(rrex,ne)); 897 } 898 */ 899 } else System.out.print("[[" + o.getClass() + "]]"); 900 } 901 } 902 trSpecExprAuxAssumptions.addElement(ne); 903 return vaf; 904 } 905 906 case TagConstants.FORALL: 907 case TagConstants.EXISTS: { 908 QuantifiedExpr qe = (QuantifiedExpr)e; 909 int op; 910 if (qe.getTag() == TagConstants.FORALL) 911 op = TagConstants.BOOLIMPLIES; 912 else 913 op = TagConstants.BOOLAND; 914 915 if (doRewrites()) boundStack.add(qe); 916 //if (doRewrites()) System.out.println("FORALL " + Location.toString(e.getStartLoc())); 917 //if (doRewrites()) ErrorSet.dump(null); 918 // FIXME - this needs to be integrated with the following two cases??? 919 if (qe.vars.size() != 1) { 920 int locStart = e.getStartLoc(); 921 int locEnd = e.getEndLoc(); 922 923 GenericVarDeclVec dummyDecls = GenericVarDeclVec.make(); 924 Expr goodTypes = GC.truelit; 925 for (int k=0; k<qe.vars.size(); ++k) { 926 GenericVarDecl decl = qe.vars.elementAt(k); 927 Assert.notFalse(sp == null || ! sp.contains(decl)); 928 Assert.notFalse(st == null || ! st.contains(decl)); 929 dummyDecls.addElement(decl); 930 931 goodTypes = GC.and(goodTypes, quantTypeCorrect(decl, sp)); 932 } 933 int pos = 0; 934 if (doRewrites()) pos = trSpecExprAuxConditions.size(); 935 Expr body = trSpecExpr(qe.expr, sp, st); 936 //if (doRewrites()) System.out.println("FORALL " + pos + " " + trSpecExprAuxConditions.size()); 937 if (doRewrites() && pos != trSpecExprAuxConditions.size() ) { 938 ExprVec ev; 939 if (pos == 0) { 940 ev = trSpecExprAuxConditions; 941 trSpecExprAuxConditions = ExprVec.make(); 942 } else { 943 int sz = trSpecExprAuxConditions.size(); 944 ev = ExprVec.make(sz - pos); 945 for (int i=pos; i < sz; ++i) { 946 ev.addElement(trSpecExprAuxConditions.elementAt(i)); 947 } 948 for (int i=pos; i<sz; ++i) { 949 trSpecExprAuxConditions.removeElementAt(sz+pos-i-1); 950 } 951 } 952 body = GC.andx( GC.nary(TagConstants.BOOLAND,ev), body); 953 } 954 if (doRewrites()) boundStack.removeLast(); 955 /* 956 if (doRewrites()) { 957 System.out.println("FORALL-ENDA " + Location.toString(e.getStartLoc())); 958 EscPrettyPrint.inst.print(System.out,0,body); 959 System.out.println(""); 960 } 961 */ 962 Expr qbody = GC.nary(locStart, locEnd, op, goodTypes, body); 963 // FIXME - here and nearby - the rangeExpr in the make call is not 964 // used later - is it ever not null coming into here? 965 return GC.quantifiedExpr(locStart, locEnd, tag, 966 qe.vars, 967 qe.rangeExpr == null ? goodTypes : 968 trSpecExpr(qe.rangeExpr, sp, st), 969 qbody, null, null); 970 } else if (Main.options().nestQuantifiers) { // default is false 971 GenericVarDecl decl = qe.vars.elementAt(0); 972 973 Assert.notFalse(sp == null || ! sp.contains(decl)); 974 Assert.notFalse(st == null || ! st.contains(decl)); 975 Assert.notFalse( qe.vars.size() == 1 ); 976 977 Expr body = GC.nary(qe.getStartLoc(), qe.getEndLoc(), op, 978 quantTypeCorrect(decl, sp), 979 trSpecExpr(qe.expr, sp, st)); 980 if (doRewrites()) boundStack.removeLast(); 981 //if (doRewrites()) System.out.println("FORALL-ENDB " + Location.toString(e.getStartLoc())); 982 return GC.quantifiedExpr(qe.getStartLoc(), qe.getEndLoc(), 983 qe.getTag(), 984 decl, 985 qe.rangeExpr == null ? null : 986 trSpecExpr(qe.rangeExpr, sp, st), 987 body, null, null); 988 } else { 989 // FIXME - need to handle AuxConditions in here 990 int locStart = e.getStartLoc(); 991 int locEnd = e.getEndLoc(); 992 993 GenericVarDeclVec dummyDecls = GenericVarDeclVec.make(); 994 Expr goodTypes = GC.truelit; 995 while (true) { 996 for (int k=0; k<qe.vars.size(); ++k) { 997 GenericVarDecl decl = qe.vars.elementAt(k); 998 Assert.notFalse(sp == null || ! sp.contains(decl)); 999 Assert.notFalse(st == null || ! st.contains(decl)); 1000 dummyDecls.addElement(decl); 1001 1002 goodTypes = GC.and(goodTypes, quantTypeCorrect(decl, sp)); 1003 } 1004 if (qe.expr.getTag() == tag) { 1005 qe = (QuantifiedExpr)qe.expr; 1006 } else { 1007 Expr body = trSpecExpr(qe.expr, sp, st); 1008 Expr qbody = GC.nary(locStart, locEnd, op, goodTypes, body); 1009 if (doRewrites()) boundStack.removeLast(); 1010 //if (doRewrites()) System.out.println("FORALL-ENDC " + Location.toString(e.getStartLoc())); 1011 return GC.quantifiedExpr(locStart, locEnd, tag, 1012 dummyDecls, 1013 qe.rangeExpr == null ? null : 1014 trSpecExpr(qe.rangeExpr, sp, st), 1015 qbody, null, null); 1016 } 1017 } 1018 } 1019 // unreachable; 1020 } 1021 1022 case TagConstants.SETCOMPEXPR: { 1023 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings, 1024 e.getStartLoc(),"Not checking predicates containing set comprehension expressions"); 1025 return null; 1026 } 1027 1028 case TagConstants.LABELEXPR: { 1029 LabelExpr le = (LabelExpr)e; 1030 return LabelExpr.make(le.getStartLoc(), le.getEndLoc(), 1031 le.positive, le.label, 1032 trSpecExpr(le.expr, sp, st)); 1033 } 1034 1035 case TagConstants.PRE: { 1036 // 1037 // Original code altered to generate a caution if the variables in 1038 // the PRE clause are not mentioned in an appropriate "modifies" 1039 // clause. Caroline Tice, 1/11/2000 1040 // Note: Current implementation assumes that if ANY substitution 1041 // takes place, then ALL appropriate substitutions took place. 1042 1043 NaryExpr ne = (NaryExpr)e; 1044 1045 /* Compare the number of substituted variables before and 1046 * after translating the PRE expression, using only the st 1047 * list (i.e. the "modifies" list) for the translations. If 1048 * no substitutions took place, generate a caution. 1049 * Then translate the expression previously generated, using 1050 * the union of sp and st. 1051 */ 1052 1053 /* FIXME - disable this for now. We use \old in AnnotationHandler when we 1054 are desugaring annotations, to wrap around a requires predicate when it is 1055 being combined with an ensures predicate. This error would have us only 1056 wrap those variables being modified and not everything. 1057 int cReplacementsBefore = getReplacementCount(); 1058 Expr tmpExpr = trSpecExpr(ne.exprs.elementAt(0), st, null); 1059 if (cReplacementsBefore == getReplacementCount()) { 1060 int loc = ne.getStartLoc(); 1061 String locStr = Location.toString(loc).intern(); 1062 if (!(issuedPRECautions.contains(locStr))) { 1063 ErrorSet.caution (loc, 1064 "Variables in \\old not mentioned in modifies pragma."); 1065 issuedPRECautions.add(locStr); 1066 } 1067 } 1068 //return trSpecExpr(ne.exprs.elementAt(0), union(sp, st), null); 1069 */ 1070 if (st != null) { 1071 return trSpecExpr(ne.exprs.elementAt(0), st, null); 1072 } else { 1073 return trSpecExpr(ne.exprs.elementAt(0), sp, st); 1074 } 1075 } 1076 1077 case TagConstants.FRESH: { 1078 NaryExpr ne = (NaryExpr)e; 1079 int sloc = ne.getStartLoc(); 1080 int eloc = ne.getEndLoc(); 1081 int n = ne.exprs.size(); 1082 ExprVec ev = ExprVec.make(n); 1083 for (int i=0; i<ne.exprs.size(); ++i) { 1084 Expr arg = trSpecExpr(ne.exprs.elementAt(i), sp, st); 1085 // arg != null 1086 Expr nonnull = GC.nary(sloc, eloc, 1087 TagConstants.REFNE, arg, GC.nulllit); 1088 // isAllocated(arg, alloc@pre) 1089 Expr isAlloced = GC.nary(sloc, eloc, TagConstants.ISALLOCATED, 1090 arg, apply(st, GC.allocvar)); 1091 // !isAllocated(arg, alloc@pre) 1092 Expr newlyallocated = GC.not(sloc, eloc, isAlloced); 1093 ev.addElement(GC.and(sloc, eloc, nonnull, newlyallocated)); 1094 } 1095 return GC.and(ev); 1096 } 1097 1098 case TagConstants.DOTDOT: 1099 BinaryExpr be = (BinaryExpr)e; 1100 // FIXME 1101 return be.left; 1102 1103 case TagConstants.NOWARN_OP: 1104 case TagConstants.WACK_NOWARN: 1105 case TagConstants.WARN_OP: 1106 case TagConstants.WARN: 1107 { 1108 // FIXME - set these as a pass through for now 1109 NaryExpr ne = (NaryExpr)e; 1110 return trSpecExpr(ne.exprs.elementAt(0), sp, st); 1111 } 1112 1113 case TagConstants.IS_INITIALIZED: 1114 case TagConstants.INVARIANT_FOR:{ 1115 // We return a fresh temporary variable, unused elsewhere, until 1116 // we know how to determine some conditions that these functions 1117 // satisfy. FIXME 1118 Identifier n = Identifier.intern("tempInit"+(++tempn)); 1119 VariableAccess v = VariableAccess.make(n, e.getStartLoc(), 1120 LocalVarDecl.make(Modifiers.NONE, null,n, 1121 Types.booleanType, 1122 UniqName.temporaryVariable, 1123 null, Location.NULL)); 1124 return v; 1125 } 1126 1127 case TagConstants.SPACE: 1128 case TagConstants.WACK_WORKING_SPACE: 1129 case TagConstants.WACK_DURATION: { 1130 // We return a fresh temporary variable, unused elsewhere, until 1131 // we know how to determine some conditions that these functions 1132 // satisfy. FIXME 1133 return tempName(e.getStartLoc(),"tempResources",Types.longType); 1134 } 1135 1136 case TagConstants.NOTHINGEXPR: 1137 case TagConstants.EVERYTHINGEXPR: 1138 return null; 1139 1140 case TagConstants.NOTMODIFIEDEXPR: { 1141 Expr ee = ((NotModifiedExpr)e).expr; 1142 Expr post = trSpecExpr(ee,sp,st); 1143 Expr pre; 1144 if (st == null) { 1145 pre = trSpecExpr(ee,sp,st); 1146 } else { 1147 pre = trSpecExpr(ee,st,null); 1148 } 1149 1150 Type t = TypeCheck.inst.getType(ee); 1151 int ftag = TagConstants.ANYEQ; 1152 if (Types.isBooleanType(t)) ftag = TagConstants.BOOLEQ; 1153 1154 return LabelExpr.make(ee.getStartLoc(),ee.getEndLoc(), 1155 false,GC.makeLabel("AdditionalInfo",ee.getStartLoc(),Location.NULL),GC.nary(ftag,post,pre)); 1156 } 1157 1158 default: 1159 Assert.fail("UnknownTag<"+e.getTag()+","+ 1160 TagConstants.toString(e.getTag())+"> on "+e+ " " + 1161 Location.toString(e.getStartLoc())); 1162 return null; // dummy return 1163 } 1164 } 1165 1166 static VariableAccess tempName(int loc, String prefix, Type type) { 1167 Identifier n = Identifier.intern(prefix + "#" + (++tempn)); 1168 VariableAccess v = VariableAccess.make(n, loc, 1169 LocalVarDecl.make(Modifiers.NONE, null,n, 1170 type, 1171 UniqName.temporaryVariable, 1172 null, Location.NULL)); 1173 return v; 1174 } 1175 1176 static public Hashtable union(Hashtable h0, Hashtable h1) { 1177 if (h0 == null) 1178 return h1; 1179 if (h1 == null) 1180 return h0; 1181 Hashtable h2 = new Hashtable(); 1182 for (Enumeration keys = h0.keys(); keys.hasMoreElements(); ) { 1183 Object key = keys.nextElement(); 1184 h2.put(key, h0.get(key)); 1185 } 1186 for (Enumeration keys = h1.keys(); keys.hasMoreElements(); ) { 1187 Object key = keys.nextElement(); 1188 h2.put(key, h1.get(key)); 1189 } 1190 return h2; 1191 } 1192 1193 /** This method implements the ESCJ 16 function 1194 * <code>TargetTypeCorrect</code>, 1195 * 1196 * except for the <code>init$</code> case! 1197 * 1198 **/ 1199 1200 /*@ requires vd == GC.allocvar.decl ==> wt != null; */ 1201 public static Expr targetTypeCorrect(/*@ non_null */ GenericVarDecl vd, 1202 Hashtable wt) { 1203 if (vd == GC.elemsvar.decl) { 1204 // ElemsTypeCorrect[[ vd ]] 1205 return elemsTypeCorrect(vd); 1206 } else if (vd == GC.allocvar.decl) { 1207 // wt[[ alloc ]] < alloc 1208 VariableAccess allocPre = (VariableAccess)wt.get(GC.allocvar.decl); 1209 return GC.nary(TagConstants.ALLOCLT, allocPre, GC.allocvar); 1210 } else if (vd instanceof FieldDecl && !Modifiers.isStatic(vd.modifiers)) { 1211 // FieldTypeCorrect[[ vd ]] 1212 return fieldTypeCorrect((FieldDecl)vd); 1213 } else { 1214 // TBW: If we ever implement safe loops, we need a case for 1215 // "init$" here, see ESCJ 16. 1216 1217 // TypeCorrect[[ vd ]] 1218 return typeCorrect(vd); 1219 } 1220 } 1221 1222 /** This method implements the ESCJ 16 function <code>TypeCorrect</code>. 1223 **/ 1224 1225 public static Expr typeCorrect(GenericVarDecl vd) { 1226 return typeAndNonNullCorrectAs(vd, vd.type, 1227 GetSpec.NonNullPragma(vd), false, 1228 null); 1229 } 1230 1231 public static Expr typeCorrect(GenericVarDecl vd, Hashtable sp) { 1232 return typeAndNonNullCorrectAs(vd, vd.type, 1233 GetSpec.NonNullPragma(vd), false, 1234 sp); 1235 } 1236 1237 // "vd" is a quantified variable 1238 public static Expr quantTypeCorrect(GenericVarDecl vd, Hashtable sp) { 1239 Assert.notFalse(GetSpec.NonNullPragma(vd) == null); 1240 if ((Types.isIntType(vd.type) || Types.isLongType(vd.type)) && 1241 !Main.options().useIntQuantAntecedents) { 1242 return GC.truelit; 1243 } else { 1244 return typeAndNonNullCorrectAs(vd, vd.type, null, true, sp); 1245 } 1246 } 1247 1248 public static Expr resultEqualsCall(GenericVarDecl vd, RoutineDecl rd, Hashtable sp) { 1249 VariableAccess v = makeVarAccess(vd, Location.NULL); 1250 boolean isConstructor = rd instanceof ConstructorDecl; 1251 1252 ExprVec ev = ExprVec.make( rd.args.size()+4 ); 1253 if (!Utils.isFunction(rd)) { 1254 ev.addElement( stateVar(sp) ); 1255 } 1256 1257 ArrayList bounds = new ArrayList(rd.args.size()+4); 1258 if (!Modifiers.isStatic(rd.modifiers)) { 1259 if (!isConstructor) { 1260 ev.addElement( apply(sp,GC.thisvar)); 1261 } 1262 } 1263 LocalVarDecl alloc1=null, alloc2=null; 1264 if (isConstructor) { 1265 // FIXME - do we need anything for constructors? is this right? 1266 alloc1 = UniqName.newBoundVariable("alloc_"); 1267 ev.addElement( makeVarAccess( (GenericVarDecl)alloc1, Location.NULL)); 1268 alloc2 = UniqName.newBoundVariable("allocNew_"); 1269 ev.addElement( makeVarAccess( (GenericVarDecl)alloc2, Location.NULL)); 1270 } 1271 1272 for (int k=0; k<rd.args.size(); ++k) { 1273 FormalParaDecl a = rd.args.elementAt(k); 1274 VariableAccess vn = makeVarAccess( a, Location.NULL); 1275 ev.addElement(vn); 1276 } 1277 Expr fcall = GC.nary(fullName(rd,false), ev); 1278 return GC.nary(TagConstants.ANYEQ, v, fcall); 1279 } 1280 1281 public static Expr typeCorrectAs(GenericVarDecl vd, Type type) { 1282 return typeAndNonNullCorrectAs(vd, type, null, false, null); 1283 } 1284 1285 public static Expr typeAndNonNullCorrectAs(GenericVarDecl vd, 1286 Type type, 1287 SimpleModifierPragma nonNullPragma, 1288 boolean forceNonNull, 1289 Hashtable sp) { 1290 return GC.and(typeAndNonNullAllocCorrectAs(vd, type, 1291 nonNullPragma, forceNonNull, 1292 sp, true)); 1293 } 1294 1295 /** Returns a vector of conjuncts. This vector is "virgin" and can be modified 1296 * by the caller. It contains at least 2 empty slots, allows clients to 1297 * append a couple of items without incurring another allocation. 1298 */ 1299 1300 public static ExprVec typeAndNonNullAllocCorrectAs(GenericVarDecl vd, 1301 Type type, 1302 SimpleModifierPragma nonNullPragma, 1303 boolean forceNonNull, 1304 Hashtable sp, 1305 boolean mentionAllocated) { 1306 VariableAccess v = makeVarAccess(vd, Location.NULL); 1307 ExprVec conjuncts = ExprVec.make(5); 1308 1309 // is(v, type) 1310 Expr e = GC.nary(TagConstants.IS, v, trType(type)); 1311 conjuncts.addElement(e); 1312 if (! Types.isReferenceType(type)) 1313 return conjuncts; 1314 1315 if (mentionAllocated) { 1316 // isAllocated(v, alloc) 1317 e = GC.nary(TagConstants.ISALLOCATED, 1318 v, 1319 apply(sp, GC.allocvar)); 1320 conjuncts.addElement(e); 1321 } 1322 1323 if (nonNullPragma != null || forceNonNull) { 1324 e = GC.nary(TagConstants.REFNE, v, GC.nulllit); 1325 if (nonNullPragma != null) { 1326 int locPragmaDecl = nonNullPragma.getStartLoc(); 1327 if (Main.options().guardedVC && locPragmaDecl != Location.NULL) { 1328 e = GuardExpr.make(e, locPragmaDecl); 1329 } 1330 LabelInfoToString.recordAnnotationAssumption(locPragmaDecl); 1331 } 1332 conjuncts.addElement(e); 1333 } 1334 1335 return conjuncts; 1336 } 1337 1338 public static Expr fieldTypeCorrect(FieldDecl fdecl) { 1339 VariableAccess f = makeVarAccess(fdecl, Location.NULL); 1340 1341 // f == asField(f, T) 1342 Expr asField = GC.nary(TagConstants.ANYEQ, 1343 f, 1344 GC.nary(TagConstants.ASFIELD, 1345 f, 1346 trType(fdecl.type))); 1347 if (! Types.isReferenceType(fdecl.type)) 1348 return asField; 1349 1350 ExprVec conjuncts = ExprVec.make(3); 1351 conjuncts.addElement(asField); 1352 1353 // fClosedTime(f) < alloc 1354 { 1355 Expr c0 = GC.nary(TagConstants.ALLOCLT, 1356 GC.nary(TagConstants.FCLOSEDTIME, f), 1357 GC.allocvar); 1358 conjuncts.addElement(c0); 1359 } 1360 1361 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(fdecl); 1362 if (nonNullPragma != null) { 1363 // (ALL s :: s != null ==> f[s] != null) 1364 LocalVarDecl sDecl = UniqName.newBoundVariable('s'); 1365 VariableAccess s = makeVarAccess(sDecl, Location.NULL); 1366 Expr c0 = GC.nary(TagConstants.REFNE, s, GC.nulllit); 1367 Expr c1 = GC.nary(TagConstants.REFNE, GC.select(f, s), GC.nulllit); 1368 Expr quant = GC.forall(sDecl, GC.implies(c0, c1)); 1369 int locPragmaDecl = nonNullPragma.getStartLoc(); 1370 LabelInfoToString.recordAnnotationAssumption(locPragmaDecl); 1371 if (Main.options().guardedVC && locPragmaDecl != Location.NULL) { 1372 quant = GuardExpr.make(quant, locPragmaDecl); 1373 } 1374 conjuncts.addElement(quant); 1375 } 1376 1377 return GC.and(conjuncts); 1378 } 1379 1380 public static Expr elemsTypeCorrect(GenericVarDecl edecl) { 1381 VariableAccess e = makeVarAccess(edecl, Location.NULL); 1382 // c0: e == asElems(e) 1383 Expr c0 = GC.nary(TagConstants.ANYEQ, e, GC.nary(TagConstants.ASELEMS, e)); 1384 // c1: eClosedTime(e) < alloc 1385 Expr c1 = GC.nary(TagConstants.ALLOCLT, 1386 GC.nary(TagConstants.ECLOSEDTIME, e), 1387 GC.allocvar); 1388 // c0 && c1 1389 return GC.and(c0, c1); 1390 } 1391 1392 /* getGCTagForBinary uses a 2-dim lookup table. Each entry is: 1393 1394 *<PRE> 1395 * { Binary tag, 1396 * nary-tag-for-bool, nary-tag-for-integral, nary-tag-for-long-integral, 1397 * nary-tag-for-floats, nary-tag-for-refs, nary-tag-for-typecode 1398 * }. 1399 * In the nary-tag-for-long-integral column, a -1 means unused. 1400 * In other columns, -1 means invalid combination. 1401 * </PRE> 1402 * */ 1403 1404 private static final int binary_table[][] 1405 = { { TagConstants.OR, 1406 TagConstants.BOOLOR, -1, -1, 1407 -1, -1, -1 }, 1408 { TagConstants.AND, 1409 TagConstants.BOOLAND, -1, -1, 1410 -1, -1, -1 }, 1411 { TagConstants.IMPLIES, 1412 TagConstants.BOOLIMPLIES, -1, -1, 1413 -1, -1, -1 }, 1414 { TagConstants.IFF, 1415 TagConstants.BOOLEQ, -1, -1, 1416 -1, -1, -1 }, 1417 { TagConstants.NIFF, 1418 TagConstants.BOOLNE, -1, -1, 1419 -1, -1, -1 }, 1420 { TagConstants.BITOR, 1421 TagConstants.BOOLOR, TagConstants.INTEGRALOR, -1, 1422 -1, -1, -1 }, 1423 { TagConstants.ASGBITOR, 1424 TagConstants.BOOLOR, TagConstants.INTEGRALOR, -1, 1425 -1, -1, -1 }, 1426 { TagConstants.BITAND, 1427 TagConstants.BOOLAND, TagConstants.INTEGRALAND, -1, 1428 -1, -1, -1 }, 1429 { TagConstants.ASGBITAND, 1430 TagConstants.BOOLAND, TagConstants.INTEGRALAND, -1, 1431 -1, -1, -1 }, 1432 { TagConstants.BITXOR, 1433 TagConstants.BOOLNE, TagConstants.INTEGRALXOR, -1, 1434 -1, -1, -1 }, 1435 { TagConstants.ASGBITXOR, 1436 TagConstants.BOOLNE, TagConstants.INTEGRALXOR, -1, 1437 -1, -1, -1 }, 1438 { TagConstants.EQ, 1439 TagConstants.BOOLEQ, TagConstants.INTEGRALEQ, -1, 1440 TagConstants.FLOATINGEQ, TagConstants.REFEQ, TagConstants.TYPEEQ }, 1441 { TagConstants.NE, 1442 TagConstants.BOOLNE, TagConstants.INTEGRALNE, -1, 1443 TagConstants.FLOATINGNE, TagConstants.REFNE, TagConstants.TYPENE }, 1444 { TagConstants.GE, 1445 -1, TagConstants.INTEGRALGE, -1, 1446 TagConstants.FLOATINGGE, -1, -1 }, 1447 { TagConstants.GT, 1448 -1, TagConstants.INTEGRALGT, -1, 1449 TagConstants.FLOATINGGT, -1, -1 }, 1450 { TagConstants.LE, 1451 -1, TagConstants.INTEGRALLE, -1, 1452 TagConstants.FLOATINGLE, TagConstants.LOCKLE, -1 }, 1453 { TagConstants.LT, 1454 -1, TagConstants.INTEGRALLT, -1, 1455 TagConstants.FLOATINGLT, TagConstants.LOCKLT, -1 }, 1456 { TagConstants.LSHIFT, 1457 -1, TagConstants.INTSHIFTL, TagConstants.LONGSHIFTL, 1458 -1, -1, -1 }, 1459 { TagConstants.ASGLSHIFT, 1460 -1, TagConstants.INTSHIFTL, TagConstants.LONGSHIFTL, 1461 -1, -1, -1 }, 1462 { TagConstants.RSHIFT, 1463 -1, TagConstants.INTSHIFTR, TagConstants.LONGSHIFTR, 1464 -1, -1, -1 }, 1465 { TagConstants.ASGRSHIFT, 1466 -1, TagConstants.INTSHIFTR, TagConstants.LONGSHIFTR, 1467 -1, -1, -1 }, 1468 { TagConstants.URSHIFT, 1469 -1, TagConstants.INTSHIFTRU, TagConstants.LONGSHIFTRU, 1470 -1, -1, -1 }, 1471 { TagConstants.ASGURSHIFT, 1472 -1, TagConstants.INTSHIFTRU, TagConstants.LONGSHIFTRU, 1473 -1, -1, -1 }, 1474 { TagConstants.ADD, 1475 -1, TagConstants.INTEGRALADD, -1, 1476 TagConstants.FLOATINGADD, -1, -1 }, // see below 1477 { TagConstants.ASGADD, 1478 -1, TagConstants.INTEGRALADD, -1, 1479 TagConstants.FLOATINGADD, -1, -1 }, 1480 { TagConstants.SUB, 1481 -1, TagConstants.INTEGRALSUB, -1, 1482 TagConstants.FLOATINGSUB, -1, -1 }, 1483 { TagConstants.ASGSUB, 1484 -1, TagConstants.INTEGRALSUB, -1, 1485 TagConstants.FLOATINGSUB, -1, -1 }, 1486 { TagConstants.DIV, 1487 -1, TagConstants.INTEGRALDIV, -1, 1488 TagConstants.FLOATINGDIV, -1, -1 }, 1489 { TagConstants.ASGDIV, 1490 -1, TagConstants.INTEGRALDIV, -1, 1491 TagConstants.FLOATINGDIV, -1, -1 }, 1492 { TagConstants.MOD, 1493 -1, TagConstants.INTEGRALMOD, -1, 1494 TagConstants.FLOATINGMOD, -1, -1 }, 1495 { TagConstants.ASGREM, 1496 -1, TagConstants.INTEGRALMOD, -1, 1497 TagConstants.FLOATINGMOD, -1, -1 }, 1498 { TagConstants.STAR, 1499 -1, TagConstants.INTEGRALMUL, -1, 1500 TagConstants.FLOATINGMUL, -1, -1 }, 1501 { TagConstants.ASGMUL, 1502 -1, TagConstants.INTEGRALMUL, -1, 1503 TagConstants.FLOATINGMUL, -1, -1 } }; 1504 1505 static { 1506 for (int i = 0; i < binary_table.length; i++) { 1507 if (binary_table[i].length != 7) 1508 Assert.fail("bad length, binary_table row " + i); 1509 } 1510 } 1511 1512 static public int getGCTagForBinary(BinaryExpr be) { 1513 1514 int tag = be.getTag(); 1515 1516 Type leftType = TypeCheck.inst.getType( be.left ); 1517 Type rightType = TypeCheck.inst.getType( be.right ); 1518 1519 // before consulting the table, handle "+" & "+=" on strings: 1520 if ((tag == TagConstants.ADD || tag == TagConstants.ASGADD) && 1521 (Types.isReferenceOrNullType(leftType) || 1522 Types.isReferenceOrNullType(rightType))) { 1523 // this "+" or "+=" denotes string concatenation 1524 return TagConstants.STRINGCAT; 1525 } 1526 1527 // find tag in table 1528 int i; 1529 1530 for( i=0; i<binary_table.length; i++ ) { 1531 if (binary_table[i][0] == tag) 1532 break; 1533 } 1534 if( i==binary_table.length ) 1535 Assert.fail("Bad tag "+TagConstants.toString(tag)); 1536 1537 // have index of correct line in i. 1538 int naryTag; 1539 if (Types.isBooleanType( leftType ) 1540 && Types.isBooleanType( rightType )) { 1541 naryTag = binary_table[i][1]; 1542 } else if (Types.isLongType( leftType ) 1543 && Types.isIntegralType( rightType )) { 1544 if (binary_table[i][3] != -1) { 1545 naryTag = binary_table[i][3]; 1546 } else { 1547 naryTag = binary_table[i][2]; 1548 } 1549 } else if (Types.isIntegralType( leftType ) 1550 && Types.isIntegralType( rightType )) { 1551 naryTag = binary_table[i][2]; 1552 } else if (Types.isNumericType( leftType ) 1553 && Types.isNumericType( rightType )) { 1554 // ## should convert integral args to floating point 1555 naryTag = binary_table[i][4]; 1556 } else if (Types.isReferenceOrNullType( leftType ) 1557 && Types.isReferenceOrNullType( rightType )) { 1558 naryTag = binary_table[i][5]; 1559 } else if (Types.isTypeType(leftType) 1560 && Types.isTypeType(rightType)) { 1561 naryTag = binary_table[i][6]; 1562 } else if (Types.isErrorType(leftType)) { 1563 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings,be.left.getStartLoc(), 1564 "Failed to translate some unimplemented construct"); 1565 naryTag = -1; // dummy assignment 1566 } else if (Types.isErrorType(rightType)) { 1567 if (be.right instanceof AmbiguousVariableAccess) 1568 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings,be.right.getStartLoc(), 1569 "Unknown variable"); 1570 else 1571 1572 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings,be.right.getStartLoc(), 1573 "Failed to translate some unimplemented construct"); 1574 naryTag = -1; // dummy assignment 1575 } else { 1576 System.out.println("LTYPE " + leftType); 1577 System.out.println("RTYPE " + rightType); 1578 Assert.fail("Bad types on tag "+TagConstants.toString(tag) ); 1579 naryTag = -1; // dummy assignment 1580 } 1581 1582 // have naryTag 1583 if( naryTag == -1 ) { 1584 Assert.fail("Bad tag/types combination at "+TagConstants.toString(tag) 1585 +" left type "+leftType 1586 +" right type "+rightType); 1587 } 1588 1589 return naryTag; 1590 } 1591 1592 /* getGCTagForUnary uses a 2-dim lookup table. Each entry is: 1593 1594 * <pre> 1595 * { Unary tag, 1596 * nary-tag-for-bool-args, 1597 * nary-tag-for-integral, 1598 * nary-tag-for-floats 1599 * }. 1600 * Use -1 if invalid combination. 1601 * </pre> 1602 */ 1603 1604 private static final int unary_table[][] 1605 = { { TagConstants.UNARYSUB, -1, TagConstants.INTEGRALNEG, 1606 TagConstants.FLOATINGNEG }, 1607 { TagConstants.NOT, TagConstants.BOOLNOT, -1, -1 }, 1608 { TagConstants.BITNOT, -1, TagConstants.INTEGRALNOT, -1 }, 1609 { TagConstants.INC, -1, TagConstants.INTEGRALADD, 1610 TagConstants.FLOATINGADD }, 1611 { TagConstants.POSTFIXINC, -1, TagConstants.INTEGRALADD, 1612 TagConstants.FLOATINGADD }, 1613 { TagConstants.DEC, -1, TagConstants.INTEGRALSUB, 1614 TagConstants.FLOATINGSUB }, 1615 { TagConstants.POSTFIXDEC, -1, TagConstants.INTEGRALSUB, 1616 TagConstants.FLOATINGSUB } }; 1617 1618 static { 1619 for (int i = 0; i < unary_table.length; i++) { 1620 if (unary_table[i].length != 4) 1621 Assert.fail("bad length, unary table row " + i); 1622 } 1623 } 1624 1625 /** TBW. Requires e.getTag() in { UNARYSUB, NOT, BITNOT, INC, 1626 POSTFIXINC, DEC, POSTFIXDEC } */ 1627 1628 static public int getGCTagForUnary(UnaryExpr e) { 1629 // find correct row in table 1630 int tag = e.getTag(); 1631 int row; 1632 for (row = 0; row < unary_table.length; row++) { 1633 if (unary_table[row][0] == tag) 1634 break; 1635 } 1636 Assert.notFalse(row < unary_table.length, "Bad tag"); 1637 1638 // find correct column in table 1639 /*-@ uninitialized */ int col = 0; 1640 Type argType = TypeCheck.inst.getType(e.expr); 1641 if (Types.isBooleanType(argType)) col = 1; 1642 else if (Types.isIntegralType(argType)) col = 2; 1643 else if (Types.isNumericType(argType)) col = 3; 1644 else if (Types.isErrorType(argType)) { 1645 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings, 1646 e.expr.getStartLoc(), 1647 "Failed to translate some unimplemented construct"); 1648 } else Assert.fail("Bad type"); 1649 1650 int result = unary_table[row][col]; 1651 Assert.notFalse(result != -1, "Bad type combination"); 1652 return result; 1653 } 1654 1655 public static VariableAccess makeVarAccess(GenericVarDecl decl, int loc) { 1656 return VariableAccess.make(decl.id, loc, decl); 1657 } 1658 1659 /** Returns the number of variable substitutions that calls to 1660 * <code>trSpecExpr</code> have caused. To find out how many times a 1661 * substitution was made, a caller can surround the call to 1662 * <code>trSpecExpr</code> by two calls to this method and compute the 1663 * difference. 1664 **/ 1665 1666 static public int getReplacementCount() { 1667 return cSubstReplacements; 1668 } 1669 1670 private static int cSubstReplacements = 0; 1671 1672 protected static VariableAccess apply(Hashtable map, VariableAccess va) { 1673 if (map == null) { 1674 return va; 1675 } 1676 VariableAccess v = (VariableAccess)map.get(va.decl); 1677 if (v != null) { 1678 if (va.decl == GC.thisvar.decl) cSubstReplacements++; 1679 return v; 1680 } else { 1681 return va; 1682 } 1683 } 1684 1685 public static TypeExpr trType(Type type) { 1686 // Other than unique-ification of type names, what distinguishes 1687 // Java types from the way they are represented in the verification 1688 // condition is that a Java array type "T[]" is represented as 1689 // "(array T)". The definition of "TrType" in ESCJ 16 spells out 1690 // the details of this conversion. However, unlike what ESCJ 16 1691 // says, the ESC/Java implementation represents types in 1692 // guarded-command expressions as "TypeExpr" nodes. The conversion 1693 // between "[]" and "array" is done when the "TypeExpr" is converted 1694 // to a verification condition string. 1695 return TypeExpr.make(type.getStartLoc(), type.getEndLoc(), type); 1696 } 1697 1698 public static void getCalledSpecs( 1699 RoutineDecl decl, 1700 ObjectDesignator od, ExprVec ev, 1701 Expr resultVar, 1702 Hashtable sp, Hashtable st) { 1703 //System.out.println("GCS " + decl.parent.id + " " + (decl instanceof MethodDecl ? (((MethodDecl)decl).id.toString()) : "" ) + " " + Location.toString(decl.getStartLoc()) + " " + (declStack.contains(decl)) ); 1704 ModifierPragmaVec md = decl.pmodifiers; 1705 if (md == null) return; 1706 for (int i=0; i<md.size(); ++i) { 1707 ModifierPragma m = md.elementAt(i); 1708 switch (m.getTag()) { 1709 case TagConstants.ENSURES: 1710 case TagConstants.POSTCONDITION: 1711 { 1712 if (Utils.ensuresDecoration.isTrue(m)) { 1713 //System.out.println("SKIPPING-A"); 1714 continue; 1715 } 1716 Expr e = ((ExprModifierPragma)m).expr; 1717 /* 1718 System.out.println("GCS-INSERTING FOR " + decl.parent.id + " " + (decl instanceof MethodDecl ? ((MethodDecl)decl).id.toString() : "") + " " + Location.toString(m.getStartLoc()) ); 1719 EscPrettyPrint.inst.print(System.out,0,m); 1720 System.out.println(""); 1721 */ 1722 //System.out.println("ENSURES " + e); 1723 Hashtable h = new Hashtable(); 1724 Expr oldResultExpr = specialResultExpr; 1725 specialResultExpr = resultVar; 1726 //h.put(Substitute.resexpr,resultVar); 1727 if (od instanceof ExprObjectDesignator) { 1728 if (!(((ExprObjectDesignator)od).expr instanceof ThisExpr)) { 1729 h.put(Substitute.thisexpr, ((ExprObjectDesignator)od).expr); 1730 } 1731 } else if (od instanceof SuperObjectDesignator) { 1732 // FIXME 1733 System.out.println("NOT SUPPORTED-D " + od.getClass()); 1734 } // fall-through for TypeObjectDesignator or null 1735 1736 FormalParaDeclVec args = decl.args; 1737 for (int j=0; j<args.size(); ++j) { 1738 h.put(args.elementAt(j), ev.elementAt(j)); 1739 } 1740 e = Substitute.doSimpleSubst(h,e); 1741 e = trSpecExpr(e,sp,st); 1742 trSpecExprAuxConditions.addElement(e); 1743 specialResultExpr = oldResultExpr; 1744 /* 1745 System.out.println("INSERTING-END " + Location.toString(m.getStartLoc()) ); 1746 EscPrettyPrint.inst.print(System.out,0,e); 1747 System.out.println(""); 1748 */ 1749 } 1750 1751 default: 1752 break; 1753 } 1754 } 1755 1756 // FIXME - What about constraint clauses 1757 /* 1758 1759 TypeDeclElemVec tdev = decl.parent.elems; 1760 for (int j=0; j<tdev.size(); ++j) { 1761 TypeDeclElem e = tdev.elementAt(j); 1762 if (!(e instanceof TypeDeclElemPragma)) continue; 1763 TypeDeclElemPragma p = (TypeDeclElemPragma)e; 1764 if (p.getTag() == TagConstants.INVARIANT) { 1765 Expr ee = ((ExprDeclPragma)p).expr; 1766 Hashtable h = new Hashtable(); 1767 h.put(Substitute.resexpr,resultVar); 1768 if (od instanceof ExprObjectDesignator) { 1769 if (!(((ExprObjectDesignator)od).expr instanceof ThisExpr)) { 1770 h.put(Substitute.thisexpr, ((ExprObjectDesignator)od).expr); 1771 } 1772 } else if (od instanceof SuperObjectDesignator) { 1773 // FIXME 1774 System.out.println("NOT SUPPORTED-E " + od.getClass()); 1775 } else if (od == null) { // Constructor case 1776 h.put(Substitute.thisexpr, resultVar); 1777 } // fall-through for TypeObjectDesignator 1778 ee = Substitute.doSimpleSubst(h,ee); 1779 ee = trSpecExpr(ee,sp,st); 1780 trSpecExprAuxConditions.addElement(ee); 1781 } 1782 } 1783 */ 1784 } 1785 1786 // This creates a unique name for a function call 1787 // The same name gets used for overriding methods 1788 static public Identifier fullName(RoutineDecl rd,boolean useSuper) { 1789 String fullname; 1790 if (Modifiers.isStatic(rd.getModifiers()) || rd instanceof ConstructorDecl) { 1791 int loc = rd.getStartLoc(); 1792 TypeSig sig = TypeSig.getSig(rd.parent); 1793 if (useSuper) sig = sig.superClass(); 1794 fullname = sig.getExternalName() + "." 1795 + rd.id().toString() + "." ; 1796 int line = Location.toLineNumber(loc); 1797 if (line == 1) { 1798 // If the reference is to a binary file, there is no unique 1799 // declaration location, so we append a hash code 1800 fullname = fullname + rd.hashCode(); 1801 } else { 1802 fullname = fullname + line + "." + Location.toColumn(loc); 1803 } 1804 } else { 1805 fullname = rd.id().toString() + "#"; 1806 if (!Utils.isFunction(rd)) fullname = fullname + "#state"; 1807 for (int i=0; i<rd.args.size(); ++i) { 1808 Type t = rd.args.elementAt(i).type; 1809 fullname = fullname + "#" + Types.printName(t); 1810 } 1811 } 1812 return Identifier.intern(fullname); 1813 } 1814 1815 1816 static public Expr getEquivalentAxioms(RepHelper o, Hashtable sp) { 1817 Expr ax = null; 1818 ASTNode astn = o.a; 1819 TypeDecl td = o.td; 1820 initForClause(); 1821 if (astn instanceof RoutineDecl) { 1822 boolean isConstructor = astn instanceof ConstructorDecl; 1823 RoutineDecl rd = (RoutineDecl)astn; 1824 GenericVarDecl newThis = UniqName.newBoundThis(); 1825 1826 1827 // NOTE: We wrap each postcondition in a separate forall quantification 1828 // because the variable names might be different. In addition, 1829 // Esc/java tacks on location information to make the names somewhat 1830 // unique, and these differ for different postconditions. The 1831 // postconditions themselves already have the variable usages within 1832 // them resolved to point to the original formal parameter declarations. 1833 // Thus it is easiest to simply use the formal parameters for the 1834 // quantification variables. Once could combine all the postconditions 1835 // that are associated with a single syntactic declaration; 1836 // constructors and static methods have just one relevant declaration; 1837 // but we haven't done this - in part because the output is more readable 1838 // with the conjunct broken up. 1839 1840 ModifierPragmaVec v = Utils.getAllSpecs(rd); 1841 ExprVec conjuncts = ExprVec.make(v.size()); 1842 1843 1844 // FIXME - what about ensures clauses with \old in them 1845 // Note - if there is an ensures clause with object fields, then it is 1846 // not a great candidate for a function call 1847 1848 // FIXME - need to guard this with signals and diverges 1849 // conditions as well 1850 // find ensures pragmas and translate them into axioms 1851 for (int i=0; i<v.size(); ++i) { 1852 ModifierPragma p = v.elementAt(i); 1853 if (p.getTag() != TagConstants.ENSURES && 1854 p.getTag() != TagConstants.POSTCONDITION) continue; 1855 if (Utils.ensuresDecoration.isTrue(p)) { 1856 //System.out.println("SKIPPING-B"); 1857 continue; 1858 } 1859 1860 RoutineDecl trd = (RoutineDecl) Utils.owningDecl.get(p); 1861 1862 ArrayList bounds = makeBounds(trd, newThis); 1863 1864 Expr fcall = createFunctionCall(trd,bounds,sp); 1865 1866 specialResultExpr = fcall; 1867 if (astn instanceof MethodDecl) { 1868 specialThisExpr = makeVarAccess( newThis, Location.NULL); 1869 } else { 1870 specialThisExpr = fcall; 1871 } 1872 1873 Expr translatedPostcondition = trSpecExpr( 1874 ((ExprModifierPragma)p).expr,null,null); // FIXME - no subst? 1875 1876 // Wrap the expression in a forall 1877 1878 Expr ee = createForall(translatedPostcondition,fcall,bounds); 1879 conjuncts.addElement(ee); 1880 } 1881 1882 specialResultExpr = null; 1883 specialThisExpr = null; 1884 1885 // There are a few more special axioms to create 1886 1887 ArrayList bounds = makeBounds(rd, newThis); 1888 Expr fcall = createFunctionCall(rd,bounds,sp); 1889 1890 Expr expr2; 1891 if (isConstructor) { 1892 ExprVec conjuncts2 = ExprVec.make(4); 1893 // If this is a constructor, then we are generating 1894 // axioms for a new instance expression. There are 1895 // a couple more implicit axioms 1896 1897 // result != null 1898 Expr ee = GC.nary(TagConstants.REFNE, fcall, GC.nulllit); 1899 conjuncts2.addElement(ee); 1900 1901 // Adds \typeof(v) == \type(...) 1902 Type type = TypeSig.getSig(rd.parent); 1903 ee = GC.nary(TagConstants.TYPEEQ, 1904 GC.nary(TagConstants.TYPEOF, fcall), 1905 trType(type)); 1906 //GC.nary(TagConstants.CLASSLITERALFUNC, trType(type))); 1907 conjuncts2.addElement(ee); 1908 // Adds ! isAllocated(v, alloc) 1909 ee = GC.nary(TagConstants.BOOLNOT, 1910 GC.nary(TagConstants.ISALLOCATED, fcall, 1911 makeVarAccess( (LocalVarDecl)bounds.get(0), Location.NULL))); 1912 conjuncts2.addElement(ee); 1913 // Adds isAllocated(v, newalloc) 1914 ee = GC.nary(TagConstants.ISALLOCATED, fcall, 1915 makeVarAccess( (LocalVarDecl)bounds.get(1), Location.NULL)); 1916 conjuncts2.addElement(ee); 1917 expr2 = GC.and(conjuncts2); 1918 } else { 1919 // add an axiom about the type of the method result 1920 Type type = ((MethodDecl)rd).returnType; 1921 // Is allows the result to be null for reference types 1922 // but is equivalent to \typeof() == . for primitive types 1923 expr2 = GC.nary(TagConstants.IS, 1924 fcall, 1925 trType(type)); 1926 } 1927 1928 1929 conjuncts.addElement(createForall(expr2,fcall,bounds)); 1930 1931 // create a composite AND of all the foralls 1932 ax = GC.and(conjuncts); 1933 1934 } else if (astn instanceof FieldDecl) { 1935 FieldDecl fd = (FieldDecl)astn; 1936 Expr ee = GC.and(getModelVarAxioms(td,fd,sp)); 1937 ax = ee; 1938 1939 } else { 1940 //System.out.println("NOTHING FOR TYPE YET"); 1941 // FIXME are these already included by virtue of the FindContributors mechanism 1942 ax = GC.truelit; 1943 } 1944 1945 closeForClause(); 1946 return ax; 1947 } 1948 1949 static private ArrayList makeBounds(RoutineDecl rd, GenericVarDecl newThis) { 1950 // Make the list of bound parameters 1951 ArrayList bounds = new ArrayList(rd.args.size()+4); 1952 Hashtable h = new Hashtable(); 1953 LocalVarDecl alloc1=null, alloc2=null; 1954 if (rd instanceof ConstructorDecl) { 1955 alloc1 = UniqName.newBoundVariable("alloc_"); 1956 bounds.add(alloc1); 1957 alloc2 = UniqName.newBoundVariable("allocNew_"); 1958 bounds.add(alloc2); 1959 } 1960 if (!Modifiers.isStatic(rd.modifiers)) { 1961 if (rd instanceof MethodDecl) bounds.add( newThis ); 1962 } 1963 for (int k=0; k<rd.args.size(); ++k) { 1964 FormalParaDecl a = rd.args.elementAt(k); 1965 //LocalVarDecl n = UniqName.newBoundVariable(a.id.toString()); 1966 VariableAccess vn = makeVarAccess( a, Location.NULL); 1967 bounds.add(a); 1968 h.put(a,vn); 1969 } 1970 return bounds; 1971 } 1972 1973 static private Expr createFunctionCall(RoutineDecl rd, ArrayList bounds, Hashtable sp) { 1974 1975 // create a function call 1976 ExprVec ev = ExprVec.make( bounds.size()+1 ); 1977 if (!Utils.isFunction(rd)) { 1978 ev.addElement( stateVar(sp) ); 1979 } 1980 for (int k=0; k<bounds.size(); ++k) { 1981 ev.addElement( makeVarAccess( (GenericVarDecl)bounds.get(k), Location.NULL)); 1982 } 1983 return GC.nary(fullName(rd,false), ev); 1984 1985 } 1986 1987 static private Expr createForall(Expr expr, Expr fcall, ArrayList bounds) { 1988 Expr ee = expr; 1989 Expr ee2 = ee; 1990 ExprVec pats = ExprVec.make(1); 1991 pats.addElement(fcall); 1992 for (int k=bounds.size()-1; k>=0; --k) { 1993 GenericVarDecl oo = (GenericVarDecl)bounds.get(k); 1994 ee = GC.forall(oo,ee); 1995 ee2 = GC.forallwithpats(oo,ee2,pats); 1996 } 1997 return GC.and(ee,ee2); 1998 } 1999 2000 /** Translates an individual represents clause into a class-level axiom. */ 2001 static public Expr getRepresentsAxiom(NamedExprDeclPragma p, Hashtable sp) { 2002 boolean isStatic; 2003 if (p.target instanceof FieldAccess) { 2004 isStatic = Modifiers.isStatic(((FieldAccess)p.target).decl.modifiers); 2005 } else { 2006 System.out.println("UNSUPPORTED OPTION-GRA " + p.target.getClass()); // FIXME - array access ?? 2007 isStatic = false; 2008 } 2009 GenericVarDecl newThis = UniqName.newBoundThis(); 2010 specialThisExpr = makeVarAccess( newThis, Location.NULL); 2011 ExprVec args = ExprVec.make(2); 2012 args.addElement(stateVar(sp)); 2013 if (!isStatic) args.addElement(specialThisExpr); 2014 ExprVec pats = ExprVec.make(2); 2015 Expr fcall = GC.nary(representsMethodName(p.target), args); 2016 pats.addElement(fcall); 2017 Expr e = TrAnExpr.trSpecExpr(p.expr, null, null); 2018 //e = GC.forallwithpats(newThis,e,pats); 2019 e = GC.forall(newThis,e); 2020 specialThisExpr = null; 2021 return e; 2022 } 2023 2024 static public Identifier representsMethodName(Object pt) { 2025 String id = "ZZZZZZZZZZZZZZ"; 2026 FieldDecl d; 2027 2028 if (pt instanceof FieldDecl) { 2029 d = (FieldDecl)pt; 2030 } else if (pt instanceof FieldAccess) { 2031 FieldAccess fa = (FieldAccess)pt; 2032 d = fa.decl; 2033 } else if (pt instanceof VariableAccess) { 2034 GenericVarDecl dd = ((VariableAccess)pt).decl; 2035 if (dd instanceof FieldDecl) d = (FieldDecl)dd; 2036 else { 2037 System.out.println("RMN " + dd.getClass() + " " + dd.toString() ); 2038 return Identifier.intern(id); 2039 } 2040 } else { 2041 System.out.println("RMN " + pt.getClass()); 2042 return Identifier.intern(id); 2043 } 2044 id = TypeSig.getSig(d.parent).getExternalName() + "#" + d.id.toString(); 2045 return Identifier.intern(id); 2046 } 2047 2048 public static ExprVec getModelVarAxioms(TypeDecl td, FieldDecl fd, Hashtable sp) { 2049 //TypeDeclElemVec tv = GetSpec.getRepresentsClauses(td,fd); 2050 TypeDeclElemVec tv = GetSpec.getRepresentsClauses(null,fd); 2051 2052 ExprVec ev = ExprVec.make(); 2053 if (tv != null) for (int i=0; i<tv.size(); ++i) { 2054 NamedExprDeclPragma p = (NamedExprDeclPragma)tv.elementAt(i); 2055 ev.addElement(getRepresentsAxiom(p,sp)); 2056 } 2057 return ev; 2058 } 2059 2060 public static VariableAccess stateVar(Hashtable sp) { 2061 if (sp == null) { // current context 2062 return currentState; 2063 } else { // possible old context 2064 return apply(sp,GC.statevar); 2065 } 2066 } 2067 }