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 }