001 /* $Id: GetSpec.java,v 1.70 2006/08/10 22:24:22 g_karab Exp $
002 * Copyright 2000, 2001, Compaq Computer Corporation
003 */
004
005 package escjava.translate;
006
007 import escjava.Main;
008 import escjava.ast.*;
009 import escjava.ast.Modifiers;
010 import escjava.ast.TagConstants;
011 import escjava.backpred.FindContributors;
012 import escjava.tc.TypeCheck;
013 import escjava.tc.Types;
014 import java.util.ArrayList;
015 import java.util.Enumeration;
016 import java.util.HashSet;
017 import java.util.Hashtable;
018 import java.util.Iterator;
019 import javafe.ast.*;
020 import javafe.tc.TypeSig;
021
022 import javafe.util.*;
023
024 /**
025 * Responsible for getting Spec for calls. Includes ... from ESCJ16c.
026 */
027
028 public final class GetSpec {
029
030 public static Spec getSpecForCall(/*@ non_null */RoutineDecl rd,
031 /*@ non_null */FindContributors scope, Set predictedSynTargs) {
032 Spec spec = getCommonSpec(rd, scope, null);
033 return extendSpecForCall(spec, scope, predictedSynTargs);
034 }
035
036 /* used for calls that are inlined */
037 public static Spec getSpecForInline(/*@ non_null */RoutineDecl rd,
038 /*@ non_null */FindContributors scope) {
039 return getCommonSpec(rd, scope, null);
040 // TBW: Should also add NonNullInit checks somewhere!
041 }
042
043 public static Spec getSpecForBody(/*@ non_null */RoutineDecl rd,
044 /*@ non_null */FindContributors scope,
045 /*@ non_null */Set synTargs, Hashtable premap) {
046 Spec spec = getCommonSpec(rd, scope, premap);
047 if (rd.body==null && Main.options().idc)
048 {
049 return(spec);
050 }
051 else
052 {
053 return extendSpecForBody(spec, scope, synTargs);
054 }
055 }
056
057 private static /*@ non_null @*/ Spec getCommonSpec(
058 /*@ non_null */RoutineDecl rd,
059 /*@ non_null */FindContributors scope, Hashtable premap) {
060 /*
061 * Need to typecheck TypeDecl containing callee so that
062 * requires/ensures/modifies clauses etc are resolved.
063 */
064
065 TypeSig T = TypeSig.getSig(rd.parent);
066 T.typecheck();
067
068 DerivedMethodDecl combined = getCombinedMethodDecl(rd);
069 DerivedMethodDecl filtered = filterMethodDecl(combined, scope);
070
071 /*
072 * If we are translating the spec for an inner-class constructor, then we
073 * need to substitute this$0arg for this.this$0 everywhere:
074 */
075 Spec spec = null;
076 try {
077 if (filtered.isConstructor() && !T.isTopLevelType()) {
078 Inner.firstThis0 = Inner
079 .getEnclosingInstanceArg((ConstructorDecl)filtered.original);
080 }
081
082 spec = trMethodDecl(filtered, premap);
083 } finally {
084 Inner.firstThis0 = null;
085 }
086
087 return spec;
088 }
089
090 static private /*@ non_null @*/ ASTDecoration dmdDecoration = new ASTDecoration("dmd");
091
092 /**
093 * * Implement GetCombinedMethodDecl from ESCJ 16c section 7:
094 * <p>* * Precondition: the type declaring rd has been typechecked.
095 * <p>* * Note: this routine may typecheck the supertypes of the type that *
096 * declares rd.
097 */
098 //@ ensures \result != null;
099 public static DerivedMethodDecl getCombinedMethodDecl(
100 /*@ non_null */RoutineDecl rd)
101 {
102 DerivedMethodDecl dmd = (DerivedMethodDecl)dmdDecoration.get(rd);
103 if (dmd != null) return dmd;
104
105 dmd = new DerivedMethodDecl(rd);
106 dmdDecoration.set(rd, dmd);
107
108 dmd.throwsSet = rd.raises;
109 dmd.requires = ExprModifierPragmaVec.make();
110 dmd.modifies = ModifiesGroupPragmaVec.make();
111 dmd.ensures = ExprModifierPragmaVec.make();
112 dmd.exsures = VarExprModifierPragmaVec.make();
113
114 if (rd instanceof ConstructorDecl) {
115 // Handle constructor case:
116 dmd.args = rd.args;
117 TypeSig thisType = TypeSig.getSig(rd.parent);
118 if (!thisType.isTopLevelType()) {
119 // An Inner class; add this$0 argument:
120 dmd.args = rd.args.copy();
121 FormalParaDecl this0arg = Inner
122 .getEnclosingInstanceArg((ConstructorDecl)rd);
123 dmd.args.insertElementAt(this0arg, 0);
124 }
125
126 dmd.returnType = thisType;
127 addModifiersToDMD(dmd, rd);
128
129 } else {
130 // Handle method case:
131 //@ assume rd instanceof MethodDecl;
132
133 MethodDecl md = (MethodDecl)rd;
134 dmd.returnType = md.returnType;
135
136 if (Modifiers.isStatic(rd.modifiers)) {
137 // static method
138 dmd.args = rd.args;
139 } else {
140 // instance method
141 dmd.args = md.args.copy();
142 dmd.args.insertElementAt((FormalParaDecl)GC.thisvar.decl, 0);
143 }
144
145 /*
146 * Add modifiers from this method as well as all methods it overrides;
147 * also handle non_null:
148 */
149 addModifiersToDMD(dmd, md);
150 Set overrides = escjava.tc.FlowInsensitiveChecks.getAllOverrides(md);
151 Enumeration overridden_methods = overrides.elements();
152 while (overridden_methods.hasMoreElements()) {
153 MethodDecl smd = (MethodDecl)overridden_methods.nextElement();
154 TypeSig.getSig(smd.parent).typecheck();
155
156 addModifiersToDMD(dmd, smd);
157 }
158 }
159
160 dmd.computeFreshUsage();
161
162 return dmd;
163 }
164
165 /**
166 * * Add the modifiers of rd to dmd, making any necessary substitions * of
167 * parameter names. Also propagates non_null's.
168 * <p>* * Precondition: rd has been typechecked.
169 * <p>
170 */
171 private static void addModifiersToDMD(/*@ non_null */DerivedMethodDecl dmd,
172 /*@ non_null */RoutineDecl rd) {
173 /*
174 * Compute the substitution on parameter names to change a spec for an
175 * overridden method to refer to our method's parameter names instead of
176 * its; propagate non_nulls:
177 */
178 Hashtable subst = new Hashtable();
179 if (rd != dmd.original) {
180 for (int i = 0; i < rd.args.size(); i++) {
181 GenericVarDecl newDecl = dmd.original.args.elementAt(i);
182 GenericVarDecl oldDecl = rd.args.elementAt(i);
183
184 // This may no longer be necessary, but it doesn't hurt
185 SimpleModifierPragma nonnull = NonNullPragma(oldDecl);
186 if (nonnull != null) setNonNullPragma(newDecl, nonnull);
187
188 VariableAccess va = VariableAccess.make(newDecl.id, Location.NULL,
189 newDecl);
190
191 subst.put(oldDecl, va);
192 }
193 }
194
195 if (rd.pmodifiers == null) return;
196
197 for (int i = 0; i < rd.pmodifiers.size(); i++) {
198 // We omit pragmas that have something notimplemented, but carry on
199 // with the rest
200 try {
201 ModifierPragma mp = rd.pmodifiers.elementAt(i);
202 switch (mp.getTag()) {
203 case TagConstants.REQUIRES:
204 case TagConstants.ALSO_REQUIRES:
205 case TagConstants.PRECONDITION: {
206 ExprModifierPragma emp = (ExprModifierPragma)mp;
207 emp = doSubst(subst, emp);
208 dmd.requires.addElement(emp);
209 break;
210 }
211 case TagConstants.MODIFIESGROUPPRAGMA: {
212 ModifiesGroupPragma em = (ModifiesGroupPragma)mp;
213 for (int ii = 0; ii < em.items.size(); ++ii) {
214 CondExprModifierPragma emp = em.items.elementAt(ii);
215 if (emp.expr == null) {
216 em.items.removeElementAt(i);
217 --ii;
218 continue;
219 }
220 int t = emp.expr.getTag();
221 // FIXME - no contribution to spec for these keywords
222 if (t == TagConstants.EVERYTHINGEXPR) {
223 dmd.modifiesEverything = true;
224 } else if (t == TagConstants.NOTSPECIFIEDEXPR) {
225 dmd.modifiesEverything = true;
226 emp.expr = EverythingExpr.make(emp.expr.getStartLoc());
227 //} else if (t == TagConstants.NOTHINGEXPR ) {
228 // no action
229 }
230 emp = doSubst(subst, emp);
231 em.items.setElementAt(emp, ii);
232 }
233 dmd.modifies.addElement(em);
234 break;
235 }
236 /*
237 * case TagConstants.MODIFIES: case TagConstants.ALSO_MODIFIES: case
238 * TagConstants.MODIFIABLE: case TagConstants.ASSIGNABLE: {
239 * CondExprModifierPragma emp = (CondExprModifierPragma)mp; if
240 * (emp.expr == null) break; // ignore - informal int t =
241 * emp.expr.getTag(); // FIXME - no contribution to spec for these
242 * keywords if (t == TagConstants.EVERYTHINGEXPR) {
243 * dmd.modifiesEverything = true; } else if (t ==
244 * TagConstants.NOTSPECIFIEDEXPR) { dmd.modifiesEverything = true;
245 * //emp = doSubst(subst, // EverythingExpr.make(emp.getStartLoc()) );
246 * break; // FIXME } else if (t == TagConstants.NOTHINGEXPR ) { // no
247 * action } else { } emp = doSubst(subst, emp);
248 * dmd.modifies.addElement(emp); break; }
249 */
250 case TagConstants.ENSURES:
251 case TagConstants.ALSO_ENSURES:
252 case TagConstants.POSTCONDITION: {
253 ExprModifierPragma emp = (ExprModifierPragma)mp;
254 int t = emp.errorTag;
255 emp = doSubst(subst, emp);
256 emp.errorTag = t;
257 dmd.ensures.addElement(emp);
258 break;
259 }
260 case TagConstants.NON_NULL:
261 /*
262 * if (dmd.nonnull == null) { dmd.nonnull =
263 * (SimpleModifierPragma)mp; }
264 */
265 break;
266 case TagConstants.EXSURES:
267 case TagConstants.ALSO_EXSURES:
268 case TagConstants.SIGNALS: {
269 VarExprModifierPragma vemp = (VarExprModifierPragma)mp;
270 vemp = doSubst(subst, vemp);
271 dmd.exsures.addElement(vemp);
272 break;
273 }
274 default:
275 break;
276 }
277 } catch (NotImplementedException e) {
278 // Error message already printed
279 }
280 }
281 }
282
283 /** Perform a substitution on an ExprModifierPragma * */
284 private static ExprModifierPragma doSubst(Hashtable subst,
285 /*@ non_null @*/ ExprModifierPragma emp) {
286 return ExprModifierPragma.make(emp.tag,
287 Substitute.doSubst(subst, emp.expr), emp.loc);
288 }
289
290 /** Perform a substitution on a CondExprModifierPragma * */
291 private static CondExprModifierPragma doSubst(Hashtable subst,
292 /*@ non_null @*/ CondExprModifierPragma emp)
293 {
294 return CondExprModifierPragma.make(emp.tag, Substitute.doSubst(subst,
295 emp.expr), emp.loc, emp.cond == null ? null : Substitute.doSubst(subst,
296 emp.cond));
297 }
298
299 /** Perform a substitution on a VarExprModifierPragma * */
300 //@ ensures \result != null;
301 private static VarExprModifierPragma doSubst(Hashtable subst,
302 /*@ non_null @*/ VarExprModifierPragma vemp)
303 {
304 VarExprModifierPragma v =
305 VarExprModifierPragma.make(vemp.tag, vemp.arg, Substitute.doSubst(
306 subst, vemp.expr), vemp.loc);
307 v.setOriginalTag(vemp.originalTag());
308 return v;
309 }
310
311 //@ ensures \result != null;
312 public static DerivedMethodDecl filterMethodDecl(
313 /*@ non_null */DerivedMethodDecl dmd,
314 /*@ non_null */FindContributors scope) {
315 if (!Main.options().filterMethodSpecs) { return dmd; }
316
317 DerivedMethodDecl dmdFiltered = new DerivedMethodDecl(dmd.original);
318 dmdFiltered.args = dmd.args;
319 dmdFiltered.returnType = dmd.returnType;
320 dmdFiltered.throwsSet = dmd.throwsSet;
321
322 dmdFiltered.requires = dmd.requires;
323 dmdFiltered.modifies = filterModifies(dmd.modifies, scope);
324 dmdFiltered.ensures = filterExprModPragmas(dmd.ensures, scope);
325 dmdFiltered.exsures = filterVarExprModPragmas(dmd.exsures, scope);
326
327 dmdFiltered.computeFreshUsage();
328
329 return dmdFiltered;
330 }
331
332 //@ ensures \result != null;
333 private static ExprModifierPragmaVec filterExprModPragmas(
334 /*@ non_null */ExprModifierPragmaVec vec,
335 /*@ non_null */FindContributors scope) {
336 int n = vec.size();
337 ExprModifierPragmaVec vecNew = null; // lazily allocated
338 for (int i = 0; i < n; i++) {
339 ExprModifierPragma emp = vec.elementAt(i);
340 if (exprIsVisible(scope.originType, emp.expr)) {
341 // keep this pragma
342 if (vecNew != null) {
343 vecNew.addElement(emp);
344 }
345 } else {
346 // filter out this pragma
347 if (vecNew == null) {
348 vecNew = ExprModifierPragmaVec.make(n - 1);
349 for (int j = 0; j < i; j++) {
350 vecNew.addElement(vec.elementAt(j));
351 }
352 }
353 }
354 }
355 if (vecNew == null) {
356 return vec;
357 } else {
358 return vecNew;
359 }
360 }
361
362 //@ ensures \result != null;
363 private static ModifiesGroupPragmaVec filterModifies(
364 /*@ non_null */ModifiesGroupPragmaVec mvec,
365 /*@ non_null */FindContributors scope) {
366 ModifiesGroupPragmaVec result = ModifiesGroupPragmaVec.make();
367 int mn = mvec.size();
368 for (int j = 0; j < mn; ++j) {
369 ModifiesGroupPragma mv = mvec.elementAt(j);
370 CondExprModifierPragmaVec vec = mv.items;
371 CondExprModifierPragmaVec vecNew = null; // lazily allocated
372 int n = vec.size();
373 for (int i = 0; i < n; i++) {
374 CondExprModifierPragma vemp = vec.elementAt(i);
375 if (exprIsVisible(scope.originType, vemp.expr)
376 && exprIsVisible(scope.originType, vemp.cond)) {
377 // keep this pragma
378 if (vecNew != null) {
379 vecNew.addElement(vemp);
380 }
381 } else {
382 // filter out this pragma
383 if (vecNew == null) {
384 vecNew = CondExprModifierPragmaVec.make(n - 1);
385 for (int k = 0; k < i; k++) {
386 vecNew.addElement(vec.elementAt(k));
387 }
388 }
389 }
390 }
391 result.addElement(ModifiesGroupPragma.make(mv.tag, mv.clauseLoc).append(
392 vecNew == null ? vec : vecNew));
393 }
394 return result;
395 }
396
397 //@ ensures \result != null;
398 private static VarExprModifierPragmaVec filterVarExprModPragmas(
399 /*@ non_null */VarExprModifierPragmaVec vec,
400 /*@ non_null */FindContributors scope) {
401 int n = vec.size();
402 VarExprModifierPragmaVec vecNew = null; // lazily allocated
403 for (int i = 0; i < n; i++) {
404 VarExprModifierPragma vemp = vec.elementAt(i);
405 if (exprIsVisible(scope.originType, vemp.expr)) {
406 // keep this pragma
407 if (vecNew != null) {
408 vecNew.addElement(vemp);
409 }
410 } else {
411 // filter out this pragma
412 if (vecNew == null) {
413 vecNew = VarExprModifierPragmaVec.make(n - 1);
414 for (int j = 0; j < i; j++) {
415 vecNew.addElement(vec.elementAt(j));
416 }
417 }
418 }
419 }
420 if (vecNew == null) {
421 return vec;
422 } else {
423 return vecNew;
424 }
425 }
426
427 //-------------------------------------------------------------------------
428 //-------------------------------------------------------------------------
429 //-------------------------------------------------------------------------
430
431 /** Translates a MethodDecl to a Spec. */
432
433 //@ ensures \result != null;
434 private static Spec trMethodDecl(/*@ non_null */DerivedMethodDecl dmd,
435 Hashtable premap) {
436 Assert.notNull(dmd);
437
438 /*
439 * Unlike any body we may be translating, for these translations this's type
440 * is that of the type that contains the method or constructor dmd.original.
441 */
442 TypeSig T = TypeSig.getSig(dmd.getContainingClass());
443 Type savedType = GC.thisvar.decl.type;
444 GC.thisvar.decl.type = T;
445
446 // (we restore GC.thisvar.decl.type just before returning)
447
448 ExprVec preAssumptions = ExprVec.make();
449 ConditionVec pre = trMethodDeclPreconditions(dmd, preAssumptions);
450
451 ExprVec targets = ExprVec.make();
452 ExprVec specialTargets = ExprVec.make();
453
454 if (!Utils.isPure(dmd.original)) {
455 targets.addElement(GC.statevar);
456 specialTargets.addElement(GC.statevar);
457 }
458 if (dmd.usesFresh) targets.addElement(GC.allocvar);
459 if (dmd.usesFresh) specialTargets.addElement(GC.allocvar);
460
461 // translates modifies list
462
463 for (int k = 0; k < dmd.modifies.size(); ++k) {
464 Frame.ModifiesIterator ii = new Frame.ModifiesIterator(
465 dmd.getContainingClass(),dmd.modifies.elementAt(k).items, true, true);
466 while (ii.hasNext()) {
467 Expr designator = (Expr)ii.next();
468 //if (Utils.isModel(designator)) continue;
469 Expr gcDesignator = TrAnExpr.trSpecExpr(designator);
470 // Returns null for modifies \nothing, \everything FIXME?
471 // array-range, wild-ref expressions FIXME!!
472 if (gcDesignator != null) {
473 targets.addElement(gcDesignator);
474 } else if (designator instanceof ArrayRangeRefExpr) {
475 targets.addElement(GC.elemsvar);
476 } else if (designator instanceof EverythingExpr) {
477 targets.addElement(GC.elemsvar);
478 }
479 }
480 }
481
482 // handle targets stuff, and create preVarMap
483
484 Set roots = new Set(); // set of GenericVarDecls
485
486 for (int i = 0; i < targets.size(); i++) {
487 Expr gcDesignator = targets.elementAt(i);
488 VariableAccess shaved = shave(gcDesignator);
489 roots.add(shaved.decl);
490 }
491
492 Hashtable preVarMap = premap;
493 if (premap == null) preVarMap = makeSubst(roots.elements(), "pre");
494 //else
495 // preVarMap = restrict( premap, roots.elements() );
496
497 /*
498 * Re the change above: premap is a map from variables with a @pre suffix to
499 * their declarations; preVarMap is the relevant piece of this for the
500 * currnet method. However, that was determined by the set of locations
501 * specified in modifies clauses. That leads to erroneous behavior if the
502 * modifies clause is incorrect.
503 *
504 * The change is to use the premap without restriction. That allows the
505 * verification of a body of a method to proceed without dependence on the
506 * accuracy of the modifies clause. However it also adds a lot of conjuncts
507 * into the verification condition - and the premap is accumulated from the
508 * entire class declaration. An improvement would be to simply use the
509 * premap generated from the uses of \old in the body of the method + the
510 * spec of the method + the spec of the class.
511 */
512 // Now create the postconditions
513 ExprVec postAssumptions = ExprVec.make();
514 ConditionVec post = trMethodDeclPostcondition(dmd, preVarMap,
515 postAssumptions);
516
517 java.util.Set postlocs = new java.util.HashSet();
518 int size = post.size();
519 for (int ic = 0; ic < size; ++ic) {
520 collectFields(post.elementAt(ic).pred, postlocs);
521 }
522
523 Spec spec = Spec.make(dmd, targets, specialTargets, preVarMap,
524 preAssumptions, pre, postAssumptions, post,
525 false && dmd.modifiesEverything, postlocs); // FIXME - turning off
526 // modifies everything for
527 // now
528
529 GC.thisvar.decl.type = savedType;
530
531 return spec;
532 }
533
534 /** Computes the preconditions, according to section 7.2.0 of ESCJ 16. */
535
536 //@ ensures \result != null;
537 private static ConditionVec trMethodDeclPreconditions(
538 /*@ non_null */DerivedMethodDecl dmd, ExprVec preAssumptions) {
539 ConditionVec pre = ConditionVec.make();
540
541 // Account for properties about parameters
542 for (int i = 0; i < dmd.args.size(); i++) {
543 FormalParaDecl arg = dmd.args.elementAt(i);
544
545 if (i == 0 && arg == GC.thisvar.decl) {
546 // the special parameter "this"
547 addFreeTypeCorrectAs(arg, TypeSig.getSig(dmd.getContainingClass()), pre);
548 VariableAccess argAccess = TrAnExpr.makeVarAccess(arg, Location.NULL);
549 Expr nonnull = GC.nary(TagConstants.REFNE, argAccess, GC.nulllit);
550 Condition cond = GC.freeCondition(nonnull, Location.NULL);
551 pre.addElement(cond);
552
553 } else {
554 // regular parameters
555 addFreeTypeCorrectAs(arg, arg.type, pre);
556 /*
557 * non_null is handled in the desugaring SimpleModifierPragma
558 * nonNullPragma = NonNullPragma(arg); if (nonNullPragma != null) {
559 * VariableAccess argAccess = TrAnExpr.makeVarAccess(arg,
560 * Location.NULL); Expr nonnull = GC.nary(TagConstants.REFNE, argAccess,
561 * GC.nulllit); Condition cond = GC.freeCondition(nonnull,
562 * nonNullPragma.getStartLoc()); pre.addElement(cond); }
563 */
564 }
565 }
566
567 if (dmd.isConstructor()) {
568 // Free: RES != null && !isAllocated(RES, wt[[alloc]])
569 Expr nonnull = GC.nary(TagConstants.REFNE, GC.resultvar, GC.nulllit);
570 Expr allocated = GC.nary(TagConstants.ISALLOCATED, GC.resultvar,
571 GC.allocvar);
572 //(VariableAccess)wt.get(GC.allocvar.decl));
573 Expr notAllocated = GC.not(allocated);
574 preAssumptions.addElement(nonnull);
575 preAssumptions.addElement(notAllocated);
576 }
577 // Add the declared preconditions
578
579 // Make the disjunction of all of the preconditions
580
581 java.util.Set axsToAdd = new java.util.HashSet();
582 if (dmd.requires.size() != 0) {
583 Expr expr = dmd.requires.elementAt(0).expr;
584 int loc = dmd.requires.elementAt(0).getStartLoc();
585 for (int i = 1; i < dmd.requires.size(); ++i) {
586 ExprModifierPragma e = dmd.requires.elementAt(i);
587 if (loc == Location.NULL) loc = e.getStartLoc();
588 expr = BinaryExpr.make(TagConstants.OR, expr, e.expr, loc);
589 javafe.tc.FlowInsensitiveChecks.setType(expr, Types.booleanType);
590 }
591 TrAnExpr.initForClause();
592
593 Hashtable map = null;
594 if (dmd.isConstructor()) {
595 map = new Hashtable();
596 map.put(GC.thisvar.decl, GC.resultvar);
597 //map.put(GC.thisvar.decl, temporary(GC.resultvar.id.toString(), scall,
598 // scall)
599 }
600 Expr pred = TrAnExpr.trSpecExpr(expr, map, null);
601
602 //Expr pred = TrAnExpr.trSpecExpr(expr);
603 if (TrAnExpr.extraSpecs) {
604 preAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions);
605 preAssumptions.append(TrAnExpr.trSpecExprAuxConditions);
606 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
607 TrAnExpr.closeForClause();
608 }
609
610 // [GKS]
611 if(Main.options().idc) { // add is-defined conditions
612 //Expr e = expr2IsDefExpr(expr);
613 if(!escjava.AnnotationHandler.isTrue(expr)) {
614 if (false // DISABLE THIS FOR NOW
615 && expr instanceof LabelExpr && ((LabelExpr)expr).expr instanceof InstanceOfExpr)
616 {
617 // [FIXME] This is a temporary solution.
618 // Filter out LabelExpr nodes with their first node being InstanceOfExpr because
619 // those are the precondition of client methods that we do not want to handle.
620 }
621 else
622 {
623 // Note: the expression argument to the CHECK-DEFINEDNESS
624 // command is the requires clause assertion expression
625 // untranslated -- i.e. not translated into the equivalent
626 // GC expression form. The translation is not later when
627 // the CHECK-DEFINEDNESS command is desugared.
628 if(DefGCmd.debug)
629 System.err.println("GK-Trace-IDC: " + expr);
630 Condition cond = GC.condition(TagConstants.CHKEXPRDEFINEDNESS,
631 expr,//TrAnExpr.trSpecExpr(e, map, null),
632 expr.getStartLoc());
633 pre.addElement(cond);
634 }
635 }
636 }
637 Condition cond = GC.condition(TagConstants.CHKPRECONDITION, pred, loc);
638
639 pre.addElement(cond);
640 }
641
642 addAxioms(axsToAdd, preAssumptions);
643
644 return pre;
645 }
646
647 /** Returns a boolean Expr that characterizes when <code>expr</code> is
648 * defined. E.g. when called on an expression like "x/y" it would yield
649 * the Expr (label Zero:n.m y != 0).
650 */
651 private static /*@ non_null */ Expr expr2IsDefExpr(Expr expr) {
652 // System.err.println("\texpr2IsDefExpr(" + expr + ")");
653 Expr result = null;
654 if(expr instanceof LabelExpr) {
655 LabelExpr labelExpr =(LabelExpr)expr;
656 result = expr2IsDefExpr(labelExpr.expr);
657 /*
658 result = LabelExpr.make(labelExpr.getStartLoc(),
659 labelExpr.getEndLoc(),
660 labelExpr.positive,
661 labelExpr.label,
662 result);
663 */
664 } else if(expr instanceof ParenExpr){
665 ParenExpr parenExpr=(ParenExpr)expr;
666 result = expr2IsDefExpr(parenExpr.expr);
667 } else if(expr instanceof LiteralExpr ||
668 expr instanceof VariableAccess ||
669 expr instanceof ThisExpr
670 ) {
671 result = escjava.AnnotationHandler.T;
672 } else if(expr instanceof InstanceOfExpr) {
673 InstanceOfExpr e = (InstanceOfExpr)expr;
674 result = expr2IsDefExpr(e);
675 } else if(expr instanceof BinaryExpr) {
676 BinaryExpr bExpr = (BinaryExpr)expr;
677 Expr leftIsDefExpr = expr2IsDefExpr(bExpr.left);
678 Expr rightIsDefExpr = expr2IsDefExpr(bExpr.right);
679 Type t = javafe.tc.FlowInsensitiveChecks.getType(bExpr);
680
681 switch(expr.getTag()) {
682 case TagConstants.DIV:
683 LiteralExpr zero = (LiteralExpr)escjava.tc.FlowInsensitiveChecks
684 .setType(LiteralExpr.make(TagConstants.INTLIT,
685 new Integer(0),
686 bExpr.getStartLoc()),
687 t); // Types.intType);
688 Expr ne = BinaryExpr.make(TagConstants.NE,
689 bExpr.right,
690 zero,
691 bExpr.getStartLoc());
692 javafe.tc.FlowInsensitiveChecks.setType(ne, Types.booleanType);
693 result = LabelExpr.make(bExpr.locOp,
694 bExpr.getEndLoc(),
695 false,
696 escjava.translate.
697 GC.makeFullLabel("Zero",
698 bExpr.locOp,
699 Location.NULL),
700 ne);
701 javafe.tc.FlowInsensitiveChecks.setType(result, Types.booleanType);
702 break;
703
704 case TagConstants.AND:
705 Expr impPart = escjava.AnnotationHandler.implies(bExpr.left,
706 rightIsDefExpr);
707 result = escjava.AnnotationHandler.and(leftIsDefExpr, impPart);
708 break;
709
710 case TagConstants.OR:
711 Expr notLeft = escjava.AnnotationHandler.not(bExpr.left);
712 result = escjava.AnnotationHandler.implies(notLeft,rightIsDefExpr);
713 break;
714
715 default:
716 result = escjava.AnnotationHandler.and(leftIsDefExpr, rightIsDefExpr);
717 break;
718 }
719 } else if(expr instanceof CondExpr) {
720 CondExpr cExpr = (CondExpr)expr;
721 Expr testIsDefExpr = expr2IsDefExpr(cExpr.test);
722 Expr thnIsDefExpr = expr2IsDefExpr(cExpr.thn);
723 Expr elsIsDefExpr = expr2IsDefExpr(cExpr.els);
724
725 Expr impThen = escjava.AnnotationHandler.implies(cExpr.test,
726 thnIsDefExpr);
727 Expr notTest = escjava.AnnotationHandler.not(cExpr.test);
728 javafe.tc.FlowInsensitiveChecks.setType(notTest, Types.booleanType);
729 Expr impElse = escjava.AnnotationHandler.implies(notTest,
730 elsIsDefExpr);
731 result = escjava.AnnotationHandler.
732 and(testIsDefExpr,
733 escjava.AnnotationHandler.and(impThen, impElse));
734 } else {
735 if(true) throw new NullPointerException(expr.toString());
736 switch(expr.getTag()) {
737 default:
738 if(true) throw new NullPointerException(expr.toString());
739 break;
740 }
741 }
742 // System.err.println("\texpr2IsDefExpr =" + result);
743 return result == null ? escjava.AnnotationHandler.T : result;
744 }
745
746 /** Computes the postconditions, according to section 7.2.2 of ESCJ 16. */
747 //@ ensures \result != null;
748 private static ConditionVec trMethodDeclPostcondition(
749 /*@ non_null */DerivedMethodDecl dmd,
750 /*@ non_null */Hashtable wt,
751 /*@ non_null */ExprVec postAssumptions) {
752 ConditionVec post = ConditionVec.make();
753
754 // type correctness of targets (including "alloc", if "alloc" is a target)
755 Enumeration wtEnum = wt.keys();
756 while (wtEnum.hasMoreElements()) {
757 GenericVarDecl vd = (GenericVarDecl)wtEnum.nextElement();
758 Expr e = TrAnExpr.targetTypeCorrect(vd, wt);
759 Condition cond = GC.freeCondition(e, Location.NULL);
760 post.addElement(cond);
761 }
762
763 if (dmd.isConstructor()) {
764 // Free: RES != null && !isAllocated(RES, wt[[alloc]])
765 Expr nonnull = GC.nary(TagConstants.REFNE, GC.resultvar, GC.nulllit);
766 Expr allocated = GC.nary(TagConstants.ISALLOCATED, GC.resultvar,
767 (VariableAccess)wt.get(GC.allocvar.decl));
768 Expr notAllocated = GC.not(allocated);
769 Condition cond = GC.freeCondition(GC.and(nonnull, notAllocated),
770 Location.NULL);
771 post.addElement(cond);
772 }
773
774 if (!Types.isVoidType(dmd.returnType)) {
775 // Free: TypeCorrectAs[[ RES, T ]]
776 addFreeTypeCorrectAs(GC.resultvar.decl, dmd.returnType, post);
777
778 if (Utils.isPure(dmd.original) && (
779 dmd.original instanceof ConstructorDecl ||
780 !Utils.isAllocates(dmd.original))) {
781 Expr e = TrAnExpr.resultEqualsCall(GC.resultvar.decl, dmd.original, wt);
782 Condition cond = GC.freeCondition(e, Location.NULL);
783 post.addElement(cond);
784 }
785 }
786
787 TypeSig T = TypeSig.getSig(dmd.getContainingClass());
788 if (dmd.isConstructor() && !T.isTopLevelType()) {
789 // Free: RES.this$0 == this$0arg
790 Expr this0 = TrAnExpr.makeVarAccess(Inner.getEnclosingInstanceField(T),
791 Location.NULL);
792 FormalParaDecl this0arg = Inner
793 .getEnclosingInstanceArg((ConstructorDecl)dmd.original);
794 Expr thisSet = GC.nary(TagConstants.REFEQ,
795 GC.select(this0, GC.resultvar), TrAnExpr.makeVarAccess(this0arg,
796 Location.NULL));
797 Condition cond = GC.freeCondition(thisSet, Location.NULL);
798 post.addElement(cond);
799 }
800
801 if (dmd.throwsSet.size() == 0) {
802 // UnexpectedException: EC == ecReturn
803 Expr pred = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return);
804 Condition cond = GC.condition(TagConstants.CHKUNEXPECTEDEXCEPTION, pred,
805 Location.NULL);
806 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION)
807 == TagConstants.CHK_AS_ASSERT) post.addElement(cond);
808 cond = GC.condition(TagConstants.CHKUNEXPECTEDEXCEPTION2, pred,
809 Location.NULL);
810 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2)
811 == TagConstants.CHK_AS_ASSERT) post.addElement(cond);
812 } else {
813 // Free: EC == ecThrow ==>
814 // XRES != null && typeof(XRES) <: Throwable &&
815 // isAllocated(XRES, alloc)
816 Expr antecedent = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw);
817 ExprVec ev = ExprVec.make();
818 // XRES != null
819 Expr p = GC.nary(TagConstants.REFNE, GC.xresultvar, GC.nulllit);
820 ev.addElement(p);
821 // typeof(XRES) <: Throwable
822 p = GC.nary(TagConstants.TYPELE, GC.nary(TagConstants.TYPEOF,
823 GC.xresultvar), GC.typeExpr(Types.javaLangThrowable()));
824 ev.addElement(p);
825 // isAllocated(XRES, alloc)
826 p = GC.nary(TagConstants.ISALLOCATED, GC.xresultvar, GC.allocvar);
827 ev.addElement(p);
828 // conjoin and add free postcondition
829 Expr consequence = GC.and(ev);
830 Condition cond = GC.freeCondition(GC.implies(antecedent, consequence),
831 Location.NULL);
832 post.addElement(cond);
833
834 // UnexpectedException:
835 // EC == ecReturn ||
836 // (EC == ecThrow &&
837 // (typeof(XRES) <: X1 && ... &&& typeof(XRES) <: Xx))
838 Expr normal = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return);
839 Expr except = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw);
840 Expr typeofXRES = GC.nary(TagConstants.TYPEOF, GC.xresultvar);
841 ev.removeAllElements();
842 int num = dmd.throwsSet.size();
843 Object originalnum = Utils.exceptionDecoration.get(dmd.original);
844 if (originalnum != null) num = ((Integer)originalnum).intValue();
845 for (int i = 0; i < num; i++) {
846 TypeName x = dmd.throwsSet.elementAt(i);
847 p = GC.nary(TagConstants.TYPELE, typeofXRES, GC.typeExpr(x));
848 ev.addElement(p);
849 }
850 Expr pp = GC.or(normal, GC.and(except, GC.or(ev)));
851
852 if (!Main.options().strictExceptions) {
853 for (int i = num; i < dmd.throwsSet.size(); i++) {
854 TypeName x = dmd.throwsSet.elementAt(i);
855 p = GC.nary(TagConstants.TYPELE, typeofXRES, GC.typeExpr(x));
856 ev.addElement(p);
857 }
858 }
859
860 Expr eOutcomes;
861 eOutcomes = GC.or(ev);
862
863 p = GC.or(normal, GC.and(except, eOutcomes));
864
865 // Note: This is commented out because we sometimes fabricate a
866 // throws clause where there was none before. - DRCok
867 //Assert.notFalse(dmd.original.locThrowsKeyword != Location.NULL);
868 cond = GC
869 .condition(TagConstants.CHKUNEXPECTEDEXCEPTION, p, Location.NULL);
870 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION)
871 == TagConstants.CHK_AS_ASSERT) post.addElement(cond);
872 cond = GC
873 .condition(TagConstants.CHKUNEXPECTEDEXCEPTION2, pp, Location.NULL);
874 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2)
875 == TagConstants.CHK_AS_ASSERT) post.addElement(cond);
876 }
877
878 // constructors ensure that the new object's owner field is null
879 if (dmd.isConstructor()) {
880 // get java.lang.Object
881 TypeSig obj = Types.javaLangObject();
882
883 FieldDecl owner = null; // make the compiler happy
884 boolean found = true;
885 boolean save = escjava.tc.FlowInsensitiveChecks.inAnnotation;
886 try {
887 escjava.tc.FlowInsensitiveChecks.inAnnotation = true;
888 owner = Types.lookupField(obj, Identifier.intern("owner"), obj);
889 } catch (javafe.tc.LookupException e) {
890 found = false;
891 } finally {
892 escjava.tc.FlowInsensitiveChecks.inAnnotation = save;
893 }
894 // if we couldn't find the owner ghost field, there's nothing to do
895 if (found) {
896 VariableAccess ownerVA = TrAnExpr.makeVarAccess(owner, Location.NULL);
897 Expr everything;
898 Expr ownerNull = GC.nary(TagConstants.REFEQ, GC.select(ownerVA,
899 GC.resultvar), GC.nulllit);
900 // if there are no exceptions thrown, it is sufficient to do
901 // RES.owner == null
902 if (dmd.throwsSet.size() == 0)
903 everything = ownerNull;
904 // else we need to do (EC == ECReturn) ==> (RES.owner == null)
905 else {
906 Expr ret = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return);
907 everything = GC.implies(ret, ownerNull);
908 }
909 Condition cond = GC.condition(TagConstants.CHKOWNERNULL, everything,
910 Location.NULL);
911 post.addElement(cond);
912 }
913 }
914
915 // Finally, add declared postconditions
916 // First normal postconditions
917 try {
918 // EC == ecReturn
919 Expr ante = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return);
920
921 Hashtable map;
922 if (dmd.isConstructor()) {
923 map = new Hashtable();
924 map.put(GC.thisvar.decl, GC.resultvar);
925 } else {
926 map = null;
927 }
928 java.util.Set axsToAdd = new java.util.HashSet();
929 ArrayList conds = new ArrayList();
930 for (int i = 0; i < dmd.ensures.size(); i++) {
931 try {
932 ExprModifierPragma prag = dmd.ensures.elementAt(i);
933 //[GKS]
934 if (Main.options().idc)
935 {
936 if (Main.options().debug)
937 {
938 System.err.println("GK-Trace-PRAG: " + prag);
939 System.out.println("GK-Trace-PPRN: " +
940 EscPrettyPrint.inst.toString(prag.expr));
941 }
942 Expr expr=prag.expr;
943 Condition cond=GC.condition(TagConstants.CHKEXPRDEFINEDNESS,
944 expr,expr.getStartLoc());
945 // Disable this for now so that I can test routines and constructors
946 // with no bodies.
947 //conds.add(cond);
948 }
949 //[GKE]
950 TrAnExpr.initForClause();
951 Expr pred = TrAnExpr.trSpecExpr(prag.expr, map, wt);
952 if (TrAnExpr.extraSpecs) {
953 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions);
954 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions);
955 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
956 TrAnExpr.closeForClause();
957 }
958 pred = GC.implies(ante, pred);
959 int tag = prag.errorTag == 0 ? TagConstants.CHKPOSTCONDITION
960 : prag.errorTag;
961 Condition cond = GC.condition(tag, pred, prag.getStartLoc());
962 conds.add(cond);
963 } catch (NotImplementedException e) {
964 TrAnExpr.closeForClause();
965 // If something not implemented occurs, a message has already
966 // been issued (unless turned off by an option). We catch it
967 // at this point and go on to the next ensures clause, only
968 // skipping the clause containing the construct that is not
969 // implemented.
970 }
971 }
972 addAxioms(axsToAdd, postAssumptions);
973 Iterator jj = conds.iterator();
974 while (jj.hasNext()) {
975 post.addElement((Condition)jj.next());
976 }
977 } finally {
978 TrAnExpr.closeForClause();
979 }
980 /*
981 * System.out.println("WT"); Enumeration ee = wt.keys(); while
982 * (ee.hasMoreElements()) { Object o = ee.nextElement();
983 * System.out.println("MAP: " + o + " -->> " + wt.get(o)); }
984 */
985 // Then exceptional postconditions
986 {
987 // EC == ecThrow
988 Expr ante0 = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw);
989 // typeof(XRES)
990 Expr typeofXRES = GC.nary(TagConstants.TYPEOF, GC.xresultvar);
991
992 java.util.Set axsToAdd = new java.util.HashSet();
993 ArrayList conds = new ArrayList();
994 for (int i = 0; i < dmd.exsures.size(); i++) {
995 try {
996 // Pragma has the form: exsures (T v) E
997 VarExprModifierPragma prag = dmd.exsures.elementAt(i);
998 TrAnExpr.initForClause();
999 // TrSpecExpr[[ E, {v-->XRES}, wt ]]
1000 Hashtable map = new Hashtable();
1001 Expr pred;
1002 if (prag.arg != null) {
1003 map.put(prag.arg, GC.xresultvar);
1004 pred = TrAnExpr.trSpecExpr(prag.expr, map, wt);
1005 // typeof(XRES) <: T
1006 Expr ante1 = GC.nary(TagConstants.TYPELE, typeofXRES, GC
1007 .typeExpr(prag.arg.type));
1008 // EC == ecThrow && typeof(XRES) <: T
1009 // ==> TrSpecExpr[[ E, {v-->XRES}, wt ]]
1010 pred = GC.implies(GC.and(ante0, ante1), pred);
1011 } else {
1012 pred = TrAnExpr.trSpecExpr(prag.expr, map, wt);
1013 pred = GC.implies(ante0, pred);
1014 }
1015 if (TrAnExpr.extraSpecs) {
1016 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions);
1017 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions);
1018 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1019 TrAnExpr.closeForClause();
1020 }
1021 //int tag = prag.errorTag == 0 ? TagConstants.CHKPOSTCONDITION :
1022 // prag.errorTag;
1023 int tag = TagConstants.CHKPOSTCONDITION;
1024 Condition cond = GC.condition(tag, pred, prag.getStartLoc());
1025 conds.add(cond);
1026 } catch (NotImplementedException e) {
1027 TrAnExpr.closeForClause();
1028 }
1029 }
1030 addAxioms(axsToAdd, postAssumptions);
1031 Iterator jj = conds.iterator();
1032 while (jj.hasNext()) {
1033 post.addElement((Condition)jj.next());
1034 }
1035 }
1036
1037 // Then any initially clauses (for constructors, if not a helper)
1038
1039 boolean isHelper = Utils.findModifierPragma(dmd.original.pmodifiers,
1040 TagConstants.HELPER) != null;
1041
1042 if (dmd.isConstructor() && !isHelper) {
1043 Hashtable map = new Hashtable();
1044 map.put(GC.thisvar.decl, GC.resultvar);
1045 TypeDeclElemVec pmods = dmd.getContainingClass().elems;
1046 java.util.Set axsToAdd = new java.util.HashSet();
1047 for (int i = 0; i < pmods.size(); ++i) {
1048 TypeDeclElem p = pmods.elementAt(i);
1049 if (!(p instanceof TypeDeclElemPragma)) continue;
1050 if (((TypeDeclElemPragma)p).getTag() != TagConstants.INITIALLY)
1051 continue;
1052 ExprDeclPragma prag = (ExprDeclPragma)p;
1053 try {
1054 TrAnExpr.initForClause();
1055 Expr pred = TrAnExpr.trSpecExpr(prag.expr, map, wt);
1056 if (TrAnExpr.extraSpecs) {
1057 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions);
1058 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions);
1059 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1060 TrAnExpr.closeForClause();
1061 }
1062 int tag = TagConstants.CHKINITIALLY;
1063 Condition cond = GC.condition(tag, pred, prag.getStartLoc());
1064 post.addElement(cond);
1065 } catch (NotImplementedException e) {
1066 TrAnExpr.closeForClause();
1067 }
1068 }
1069 addAxioms(axsToAdd, postAssumptions);
1070 }
1071
1072 if (dmd.isConstructor() || isHelper) return post;
1073 // Then any constraint clauses (for methods)
1074
1075 TypeDecl tdecl = dmd.getContainingClass();
1076 Set s = new javafe.util.Set();
1077 if (tdecl instanceof InterfaceDecl)
1078 s.add(tdecl);
1079 else {
1080 ClassDecl cdecl = (ClassDecl)tdecl;
1081 while (true) {
1082 post = addConstraintClauses(post, cdecl, wt, postAssumptions);
1083 addSuperInterfaces(cdecl, s);
1084 if (cdecl.superClass == null) break;
1085 cdecl = (ClassDecl)TypeSig.getSig(cdecl.superClass).getTypeDecl();
1086 }
1087 }
1088 Enumeration en = s.elements();
1089 while (en.hasMoreElements()) {
1090 InterfaceDecl ifd = (InterfaceDecl)en.nextElement();
1091 post = addConstraintClauses(post, ifd, wt, postAssumptions);
1092 }
1093 return post;
1094 }
1095
1096 /**
1097 * axsToAdd holds a Set of RepHelper - we need to add to the assumptions any
1098 * axioms pertinent to the RepHelper.
1099 */
1100 static public void addAxioms(/*@ non_null @*/ java.util.Set axsToAdd, ExprVec assumptions) {
1101 java.util.Set axsDone = new java.util.HashSet();
1102 while (!axsToAdd.isEmpty()) {
1103 RepHelper o = (RepHelper)axsToAdd.iterator().next();
1104 axsToAdd.remove(o);
1105 if (!axsDone.add(o)) continue;
1106 Expr e = TrAnExpr.getEquivalentAxioms(o, null);
1107 assumptions.addElement(e);
1108 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1109 TrAnExpr.trSpecAuxAxiomsNeeded.clear();
1110 }
1111 }
1112
1113 // FIXME - need to include inherited constraint clauses
1114 static public ConditionVec addConstraintClauses(ConditionVec post,
1115 /*@ non_null @*/ TypeDecl decl,
1116 Hashtable wt,
1117 ExprVec postAssumptions) {
1118 TypeDeclElemVec pmods = decl.elems;
1119 java.util.Set axsToAdd = new java.util.HashSet();
1120 for (int i = 0; i < pmods.size(); ++i) {
1121 TypeDeclElem p = pmods.elementAt(i);
1122 if (!(p instanceof TypeDeclElemPragma)) continue;
1123 if (((TypeDeclElemPragma)p).getTag() != TagConstants.CONSTRAINT)
1124 continue;
1125 ExprDeclPragma prag = (ExprDeclPragma)p;
1126 try {
1127 TrAnExpr.initForClause();
1128 Expr pred = TrAnExpr.trSpecExpr(prag.expr, null, wt);
1129 if (TrAnExpr.extraSpecs) {
1130 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions);
1131 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions);
1132 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1133 TrAnExpr.closeForClause();
1134 }
1135 int tag = TagConstants.CHKCONSTRAINT;
1136 Condition cond = GC.condition(tag, pred, prag.getStartLoc());
1137 post.addElement(cond);
1138 } catch (NotImplementedException e) {
1139 TrAnExpr.closeForClause();
1140 }
1141 }
1142
1143 addAxioms(axsToAdd, postAssumptions);
1144 return post;
1145 }
1146
1147 //-------------------------------------------------------------------------
1148 //-------------------------------------------------------------------------
1149 //-------------------------------------------------------------------------
1150
1151 /** Implements ExtendSpecForCall, section 7.3 of ESCJ 16. */
1152
1153 //@ ensures \result != null;
1154 private static Spec extendSpecForCall(/*@ non_null */Spec spec,
1155 /*@ non_null */FindContributors scope,
1156 Set predictedSynTargs)
1157 {
1158 // FIXME - I'm not sure that \old variables not in the modifies list get
1159 // translated here
1160 // I think those translations are in scope but not in spec.
1161 // spec.preVarMap contains the modified variables for the current routine
1162 // but it is the preVarMap in the initialState generated from scope that has
1163 // the
1164 // relevant mappings of variables mentioned in \old expressions
1165
1166 // The set of variables modified by *this* GC call:
1167 Set modifiedVars = new Set(spec.preVarMap.keys());
1168
1169 ParamAndGlobalVarInfo vars = null;
1170
1171 boolean isConstructor = spec.dmd.isConstructor();
1172 InvariantInfo ii = mergeInvariants(collectInvariants(scope, spec.preVarMap));
1173 // FIXME - Possibly causes bloated VCs -- I haven't found an example
1174 // yet that needs this, but it seems it ought.
1175 //HashSet axs = collectInvariantsAxsToAdd;
1176 //ExprVec assumptions = addNewAxs(axs,null);
1177 //spec.preAssumptions.append(assumptions);
1178 //spec.postAssumptions.append(assumptions);
1179
1180 for (; ii != null; ii = ii.next) {
1181
1182 int tag = ii.prag.getTag();
1183 boolean includeInPre = true;
1184 boolean includeInPost = tag != TagConstants.AXIOM;
1185
1186 /*
1187 * Does ii mention a variable that this GC call will modify?
1188 */
1189 Set invFV = Substitute.freeVars(ii.J);
1190 boolean mentionsModifiedVars = Main.options().useAllInvPostCall
1191 || invFV.containsAny(modifiedVars) || spec.modifiesEverything;
1192
1193 /*
1194 * Does ii mention a variable that the body that is making the GC call
1195 * ever modifies?
1196 */
1197 boolean falsifiable = true;
1198 if (predictedSynTargs != null || spec.modifiesEverything) {
1199 Assert.notFalse(!Main.options().useAllInvPreBody);
1200 falsifiable = invFV.containsAny(predictedSynTargs);
1201 }
1202
1203 if (ii.isStatic) {
1204 // static invariant
1205
1206 // PRECONDITION for static invariant
1207 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, ii.J,
1208 ii.prag.getStartLoc());
1209 if (falsifiable && includeInPre) spec.pre.addElement(cond);
1210
1211 // POSTCONDITION for static invariant
1212
1213 if (mentionsModifiedVars) {
1214 // The free variables of "J" overlap with "synTargs", so add "J"
1215 cond = GC.freeCondition(ii.J, ii.prag.getStartLoc());
1216 if (includeInPost) spec.post.addElement(cond);
1217 }
1218
1219 } else {
1220 // instance invariant
1221 Assert.notNull(ii.sdecl);
1222 Assert.notNull(ii.s);
1223
1224 if (falsifiable) {
1225 // PRECONDITION for instance invariant
1226
1227 // Gather parameters and static fields, unless already cached
1228 if (vars == null) {
1229 vars = collectParamsAndGlobals(spec, scope);
1230 }
1231
1232 /*
1233 * Without any optimizations, we would generate one precondition here,
1234 *
1235 * p == null || !is(p, trType[[ U ]]) || TrSpecExpr[[ J, {this-->p}, {} ]]
1236 *
1237 * for each parameter or static field "p", where U is the type of this
1238 * in invariant J.
1239 *
1240 *
1241 * Optimizations:
1242 * - First, generate no preconditions for any p such that we can
1243 * prove statically that p cannot have type U at runtime.
1244 * - Second, combine all the remaining preconditions into 1
1245 * universally quantified precondition:
1246 *
1247 * (FORALL s :: (s == p0 || s == p1 || ...) ==> s == null || !is(s,
1248 * trType[[ U ]] || TrSpecExpr[[ J, {this-->p}, {} ]] )
1249 *
1250 * where "p0", "p1", ... are the parameters and static fields. If the
1251 * list "p0", "p1", ... is empty, don't generate a precondition.
1252 * - Third, if all of the p_i's are "non_null", drop the disjunct "s ==
1253 * null".
1254 * - Fourth, if all of the p_i's can be proved to be statically of
1255 * type U, drop the disjunct "!is(s, trType[[ U ]]".
1256 */
1257
1258 // Build equalities & collect info on which disjuncts to include:
1259 boolean allAreNonnull = true;
1260 boolean allAreOfTypeU = true;
1261 ExprVec alternatives = ExprVec.make();
1262
1263 for (ParamAndGlobalVarInfo info = vars; info != null; info = info.next) {
1264 if (!Types.isSubclassOf(info.U, ii.U)) {
1265 // p may not always/never hold an object of type U (ii.U)
1266 if (!Types.isSubclassOf(ii.U, info.U))
1267 // p can never hold an object of type U (ii.U)
1268 continue;
1269 allAreOfTypeU = false;
1270 }
1271
1272 Expr eq = GC.nary(TagConstants.REFEQ, ii.s, TrAnExpr.makeVarAccess(
1273 info.vdecl, Location.NULL));
1274 alternatives.addElement(eq);
1275 //if (! info.isNonnull) // FIXME
1276 allAreNonnull = false;
1277 }
1278
1279 /*
1280 * -noOutCalls changes this to check *in addition* all non-null
1281 * allocated objects of dynamic type U *except* objectToBeConstructed:
1282 */
1283 if (Main.options().noOutCalls) {
1284 // isAllocated(ii.s, alloc [in pre-state])
1285 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED, ii.s,
1286 GC.allocvar);
1287 Expr notEq = GC.nary(TagConstants.REFNE, ii.s, GC.objectTBCvar);
1288
1289 alternatives.addElement(GC.and(isAllocated, notEq));
1290 allAreNonnull = false;
1291 allAreOfTypeU = false;
1292 }
1293
1294 // build precondition if any alternatives:
1295 if (alternatives.size() != 0) {
1296 Expr ante = GC.or(alternatives);
1297 Expr cons = ii.J;
1298
1299 ExprVec disjuncts = ExprVec.make();
1300 if (!allAreNonnull)
1301 disjuncts.addElement(GC.nary(TagConstants.REFEQ, ii.s,
1302 GC.nulllit));
1303 if (!allAreOfTypeU)
1304 disjuncts.addElement(GC.not(GC.nary(TagConstants.IS, ii.s,
1305 TrAnExpr.trType(ii.U))));
1306 if (disjuncts.size() != 0) {
1307 disjuncts.addElement(cons);
1308 cons = GC.or(disjuncts);
1309 }
1310
1311 Expr quant = GC.forall(ii.sdecl, GC.implies(ante, cons));
1312 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT,
1313 quant, ii.prag.getStartLoc());
1314 if (includeInPre) spec.pre.addElement(cond);
1315 }
1316 }
1317
1318 // POSTCONDITION for instance invariant
1319
1320 if (mentionsModifiedVars && includeInPost) {
1321 // TypeCorrectNoallocAs[[ s, U ]] && s != null
1322 ExprVec ev = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U,
1323 null, true, null, false);
1324 ExprVec nopats = ev.copy();
1325
1326 Expr p = TrAnExpr.trSpecExpr(ii.prag.expr, TrAnExpr.union(
1327 spec.preVarMap, ii.map), null);
1328 if (spec.modifiesEverything)
1329 collectFields(p, spec.postconditionLocations);
1330 if (includeInPre) ev.addElement(p);
1331
1332 Expr ante = GC.and(ev);
1333 Expr impl = GC.implies(ante, ii.J);
1334
1335 spec.post.addElement(GC.freeCondition(GC.forall(ii.sdecl, impl,
1336 nopats), ii.prag.getStartLoc()));
1337 }
1338 }
1339 }
1340
1341 return spec;
1342 }
1343
1344 /** Implements ExtendSpecForBody, section 7.4 of ESCJ 16. */
1345
1346 //@ ensures \result != null;
1347 private static Spec extendSpecForBody(/*@ non_null */Spec spec,
1348 /*@ non_null */FindContributors scope,
1349 /*@ non_null */Set synTargs)
1350 {
1351
1352 TypeDecl td = spec.dmd.getContainingClass();
1353 boolean isConstructor = spec.dmd.isConstructor();
1354
1355 // Add NonNullInit checks
1356 if (isConstructor && !spec.dmd.isConstructorThatCallsSibling()) {
1357 // first check fields in first-inherited interfaces
1358 ClassDecl cd = (ClassDecl)td;
1359 Enumeration inheritedInterfaces = getFirstInheritedInterfaces(cd);
1360 while (inheritedInterfaces.hasMoreElements()) {
1361 TypeDecl tdSuperInterface = (TypeDecl)inheritedInterfaces.nextElement();
1362 nonNullInitChecks(tdSuperInterface, spec.post);
1363 }
1364 // then check fields in the current class
1365 nonNullInitChecks(td, spec.post);
1366 }
1367
1368 InvariantInfo ii = mergeInvariants(collectInvariants(scope, spec.preVarMap));
1369 // FIXME - Possibly causing bloated VCs
1370 HashSet axsToAdd = collectInvariantsAxsToAdd;
1371 ExprVec assumptions = addNewAxs(axsToAdd, null);
1372 spec.preAssumptions.append(assumptions);
1373 spec.postAssumptions.append(assumptions);
1374
1375 for (; ii != null; ii = ii.next) {
1376 int tag = ii.prag.getTag();
1377 addInvariantBody(ii, spec, synTargs);
1378 }
1379
1380 ExprVec axioms = collectAxioms(scope);
1381
1382 for (int i = 0; i < axioms.size(); i++) {
1383 spec.pre.addElement(GC.freeCondition(axioms.elementAt(i), Location.NULL));
1384 }
1385
1386 // FIXME - possibly causing bloated VCs
1387 for (int i = 0; i < axioms.size(); i++) {
1388 spec.postAssumptions.addElement(axioms.elementAt(i));
1389 }
1390
1391 return spec;
1392 }
1393
1394 /**
1395 * Add to <code>post</code> all NonNullInit checks for non_null instance
1396 * fields and instance ghost fields declared in <code>td</code>.
1397 */
1398 private static void nonNullInitChecks(/*@ non_null */TypeDecl td,
1399 /*@ non_null */ConditionVec post) {
1400 TypeDeclElemVec tdes = td.elems;
1401
1402 // check that non_null instance fields have been initialized
1403 for (int i = 0; i < tdes.size(); i++) {
1404 TypeDeclElem tde = tdes.elementAt(i);
1405 FieldDecl fd;
1406 if (tde.getTag() == TagConstants.FIELDDECL) {
1407 fd = (FieldDecl)tde;
1408 } else if (tde.getTag() == TagConstants.GHOSTDECLPRAGMA) {
1409 fd = ((GhostDeclPragma)tde).decl;
1410 } else {
1411 continue;
1412 }
1413
1414 if (!Modifiers.isStatic(fd.modifiers)) {
1415 SimpleModifierPragma smp = NonNullPragma(fd);
1416 if (smp != null) {
1417 // NonNullInit: EC==ecReturn ==> f[RES] != null
1418
1419 Expr left = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return);
1420
1421 VariableAccess f = TrAnExpr.makeVarAccess(fd, Location.NULL);
1422 Expr right = GC.nary(TagConstants.REFNE, GC.select(f, GC.resultvar),
1423 GC.nulllit);
1424 Expr pred = GC.implies(left, right);
1425 Condition cond = GC.condition(TagConstants.CHKNONNULLINIT, pred, smp
1426 .getStartLoc());
1427 post.addElement(cond);
1428 }
1429 }
1430 }
1431 }
1432
1433 //@ ensures \result != null && \result.elementType == \type(InterfaceDecl);
1434 static public Enumeration getFirstInheritedInterfaces(
1435 /*@non_null */ClassDecl cd) {
1436 Set interfaces = new Set();
1437 addSuperInterfaces(cd, interfaces);
1438 if (interfaces.size() != 0 && cd.superClass != null) {
1439 TypeDecl tdSuper = TypeSig.getSig(cd.superClass).getTypeDecl();
1440 Set superClassInterfaces = new Set();
1441 addSuperInterfaces(tdSuper, superClassInterfaces);
1442 Enumeration superClassesInterfaces = superClassInterfaces.elements();
1443 while (superClassesInterfaces.hasMoreElements()) {
1444 interfaces.remove(superClassesInterfaces.nextElement());
1445 }
1446 }
1447 return interfaces.elements();
1448 }
1449
1450 //@ requires set.elementType == \type(InterfaceDecl);
1451 private static void addSuperInterfaces(/*@ non_null */TypeDecl td,
1452 /*@ non_null */Set set) {
1453 if (td instanceof InterfaceDecl) {
1454 set.add(td);
1455 }
1456 // add superinterfaces of "td"
1457 TypeNameVec si = td.superInterfaces;
1458 for (int i = 0; i < si.size(); i++) {
1459 TypeName superName = si.elementAt(i);
1460 TypeDecl superDecl = TypeSig.getSig(superName).getTypeDecl();
1461 addSuperInterfaces(superDecl, set);
1462 }
1463 }
1464
1465 /**
1466 * Extend <code>spec</code>, in a way appropriate for checking the body of
1467 * a method or constructor, to account for invariant <code>ii.J</code>
1468 * declared in class <code>ii.U</code>. The body to be checked has
1469 * syntactic targets <code>synTargs</code>.
1470 */
1471
1472 private static void addInvariantBody(/*@ non_null */InvariantInfo ii,
1473 /*@ non_null */Spec spec,
1474 /*@ non_null */Set synTargs) {
1475
1476 Set invFV = Substitute.freeVars(ii.J);
1477
1478 /*
1479 * Include invariant in post only if intersection of vars of invariant and
1480 * vars modified in the method body is nonempty.
1481 */
1482 // Also include it if we are dealing with a constructor, since then
1483 // the invariant might never have been established.
1484 boolean isConstructor = spec.dmd.isConstructor();
1485 boolean includeInPre = true;
1486 boolean includeInPostOrig = true;
1487 boolean includeInPost = includeInPostOrig
1488 && (Main.options().useAllInvPostBody || invFV.containsAny(synTargs));
1489
1490 if (ii.isStatic) {
1491 // static invariant
1492
1493 Condition cond = GC.freeCondition(ii.J, ii.prag.getStartLoc());
1494
1495 if (includeInPre) spec.pre.addElement(cond);
1496
1497 if (includeInPost) {
1498 cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, ii.J, ii.prag
1499 .getStartLoc());
1500 spec.post.addElement(cond);
1501 }
1502
1503 } else {
1504 // instance invariant
1505
1506 // Do the precondition
1507 {
1508 // Method, or constructor not declared below:
1509 // (FORALL s :: TypeCorrectNoallocAs[[ s, U ]] && s != null ==> J)
1510 //
1511 // Constructor of a class T, where either
1512 // * U is a subtype of T, and
1513 // either U is not T or the constructor does not call a sibling
1514 // or
1515 // * U is an interface, and
1516 // + m calls sibling constructor and U is not a
1517 // superinterface of T
1518 // or
1519 // + m does not call sibling constructor and U is not a
1520 // superinterface of a proper superclass of T
1521 // (FORALL s :: TypeCorrectNoallocAs[[ s, U ]] && s != null &&
1522 // s != objectToBeConstructed
1523 // ==> J)
1524 //
1525 // In either case, NOPATS is the same as the antecedent.
1526 ExprVec ante = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U,
1527 null, true, null, false);
1528 if (spec.dmd.isConstructor()) {
1529 TypeSig tU = ii.U;
1530 TypeSig tT = TypeSig.getSig(spec.dmd.getContainingClass());
1531 boolean includeAntecedent = false;
1532 if (Types.isSubclassOf(tU, tT)) {
1533 if (!Types.isSameType(tU, tT)
1534 || !spec.dmd.isConstructorThatCallsSibling()) {
1535 includeAntecedent = true;
1536 }
1537 } else if (ii.prag.parent instanceof InterfaceDecl) {
1538 if (spec.dmd.isConstructorThatCallsSibling()) {
1539 if (!Types.isSubclassOf(tT, tU)) {
1540 includeAntecedent = true;
1541 }
1542 } else {
1543 ClassDecl cd = (ClassDecl)spec.dmd.getContainingClass();
1544 if (!Types.isSubclassOf(TypeSig.getSig(cd.superClass), tU)) {
1545 includeAntecedent = true;
1546 }
1547 }
1548 }
1549 if (includeAntecedent) {
1550 Expr p = GC.nary(TagConstants.REFNE, ii.s, GC.objectTBCvar);
1551 ante.addElement(p);
1552 }
1553 }
1554 Expr body = GC.implies(GC.and(ante), ii.J);
1555 Expr quant = GC.forall(ii.sdecl, body, ante);
1556 Condition cond = GC.freeCondition(quant, ii.prag.getStartLoc());
1557 if (includeInPre) spec.pre.addElement(cond);
1558 }
1559
1560 // Do the postcondition
1561
1562 // Include the invariant as a checked postcondition if its free variables
1563 // overlap with the syntactic targets of the body (as indicated by the
1564 // current value of "includeInPost"), or if the routine is a constructor
1565 // (that does not call a sibling) of some class "T" and the invariant is
1566 // declared in "T" or in one of "T"'s first-inherited interfaces.
1567 if (!includeInPost && spec.dmd.isConstructor()
1568 && !spec.dmd.isConstructorThatCallsSibling()) {
1569 TypeSig tU = ii.U;
1570 ClassDecl cd = (ClassDecl)spec.dmd.getContainingClass();
1571 TypeSig tT = TypeSig.getSig(cd);
1572 if (Types.isSubclassOf(tT, tU)
1573 && (cd.superClass == null || !Types.isSubclassOf(TypeSig
1574 .getSig(cd.superClass), tU))) {
1575 // "U" is "T" or a first-inherited interface of "T"
1576 includeInPost = true;
1577 }
1578 }
1579
1580 if (includeInPost && includeInPostOrig) {
1581 // TypeCorrectAs[[ s, U ]] && s != null
1582 ExprVec ante = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U,
1583 null, true, null, true);
1584
1585 if (spec.dmd.isConstructor()) {
1586 TypeSig tU = ii.U;
1587 TypeSig tT = TypeSig.getSig(spec.dmd.getContainingClass());
1588 if (!Types.isSubclassOf(tT, tU)) {
1589 // "m" is a constructor, and "U" is not a superclass or
1590 // superinterface of "T"
1591 // Add to antecedent the conjunct: s != this
1592 ante.addElement(GC.nary(TagConstants.REFNE, ii.s, GC.thisvar));
1593 } else if (Types.isSameType(tU, tT) && spec.dmd.throwsSet.size() != 0) {
1594 // "m" is a constructor, and "U" is "T", and throws set is nonempty
1595 // Add to antecedent the conjunct: (EC == ecReturn || s != this)
1596 ante.addElement(GC.or(GC.nary(TagConstants.ANYEQ, GC.ecvar,
1597 GC.ec_return), GC.nary(TagConstants.REFNE, ii.s, GC.thisvar)));
1598 }
1599 }
1600 Expr body = GC.implies(GC.and(ante), ii.J);
1601 Expr quant = GC.forall(ii.sdecl, body);
1602 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, quant,
1603 ii.prag.getStartLoc());
1604 spec.post.addElement(cond);
1605 if (Info.on) {
1606 Info.out("[addInvariantBody: Including body-post-invariant at "
1607 + Location.toString(ii.prag.getStartLoc()) + "]");
1608 }
1609 } else {
1610 if (Info.on) {
1611 Info.out("[addInvariantBody: Skipping body-post-invariant at "
1612 + Location.toString(ii.prag.getStartLoc()) + "]");
1613 }
1614 }
1615 }
1616 }
1617
1618 /** Collects the axioms in <code>scope</code>. */
1619
1620 //@ ensures \result != null;
1621 private static ExprVec collectAxioms(/*@ non_null */FindContributors scope) {
1622
1623 ExprVec r = ExprVec.make();
1624
1625 TrAnExpr.initForClause();
1626 for (Enumeration typeSigs = scope.typeSigs(); typeSigs.hasMoreElements();) {
1627
1628 TypeDecl td = ((javafe.tc.TypeSig)typeSigs.nextElement()).getTypeDecl();
1629
1630 for (int i = 0; i < td.elems.size(); i++) {
1631 TypeDeclElem tde = td.elems.elementAt(i);
1632 if (tde.getTag() == TagConstants.AXIOM) {
1633 ExprDeclPragma axiom = (ExprDeclPragma)tde;
1634 if (!Main.options().filterInvariants
1635 || exprIsVisible(scope.originType, axiom.expr)) {
1636 r.addElement(TrAnExpr.trSpecExpr(axiom.expr, null, null));
1637 }
1638 }
1639 }
1640
1641 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(td);
1642 for (int i = 0; i < tv.size(); ++i) {
1643 TypeDeclElem tde = tv.elementAt(i);
1644 NamedExprDeclPragma p = (NamedExprDeclPragma)tde;
1645 FieldDecl fd = ((FieldAccess)p.target).decl;
1646 Expr e = TrAnExpr.getRepresentsAxiom(p, null);
1647 r.addElement(e);
1648 }
1649 }
1650
1651 TrAnExpr.closeForClause();
1652 return r;
1653 }
1654
1655 /**
1656 * Gets the represents clauses for a model field fd as seen from a type
1657 * declaration td; fd may be declared in td or in a supertype of td.
1658 * If td is null, then all represents clauses are returned, in any loaded class.
1659 */
1660 static public TypeDeclElemVec getRepresentsClauses(TypeDecl td, FieldDecl fd) {
1661 if (td == null) return (TypeDeclElemVec)Utils.representsDecoration.get(fd);
1662 TypeDeclElemVec mpv = (TypeDeclElemVec)Utils.representsDecoration.get(td);
1663 TypeDeclElemVec n = TypeDeclElemVec.make(mpv.size());
1664 for (int i = 0; i < mpv.size(); ++i) {
1665 TypeDeclElem m = mpv.elementAt(i);
1666 if (!(m instanceof NamedExprDeclPragma)) continue;
1667 NamedExprDeclPragma nem = (NamedExprDeclPragma)m;
1668 if (((FieldAccess)nem.target).decl == fd) n.addElement(m);
1669 }
1670 return n;
1671 }
1672
1673 /** Collects the invariants in <code>scope</code>. */
1674
1675 private static HashSet collectInvariantsAxsToAdd;
1676
1677 private static InvariantInfo collectInvariants(
1678 /*@ non_null */FindContributors scope, Hashtable premap) {
1679 collectInvariantsAxsToAdd = null;
1680 InvariantInfo ii = null;
1681 InvariantInfo iiPrev = null;
1682
1683 Enumeration invariants = scope.invariants();
1684 try {
1685 TrAnExpr.initForClause();
1686 while (invariants.hasMoreElements()) {
1687 ExprDeclPragma ep = (ExprDeclPragma)invariants.nextElement();
1688 Expr J = ep.expr;
1689
1690 boolean Jvisible = !Main.options().filterInvariants
1691 || exprIsVisible(scope.originType, J);
1692
1693 // System.out.print( (Jvisible?"Visible":"Invisible")+": ");
1694 // javafe.ast.PrettyPrint.inst.print(System.out, 0, J );
1695 // System.out.println();
1696
1697 if (Jvisible) {
1698 //System.out.println("COLLECTING INVARIANT " +
1699 // Location.toString(ep.getStartLoc()));
1700
1701 // Add a new node at the end of "ii"
1702 InvariantInfo invinfo = new InvariantInfo();
1703 invinfo.prag = ep;
1704 invinfo.U = TypeSig.getSig(ep.parent);
1705 if (iiPrev == null)
1706 ii = invinfo;
1707 else
1708 iiPrev.next = invinfo;
1709 iiPrev = invinfo;
1710
1711 // The following determines whether or not an invariant is a
1712 // static invariant by, in essence, checking for occurrence
1713 // of "this" in the guarded-command translation of "J", not
1714 // in "J" itself. (These yield different results in the
1715 // unusual case that "J" mentioned "this" in a subexpression
1716 // "E.g", where "g" is a static field.)
1717 // First, build the map "{this-->s}" for a new "s".
1718
1719 LocalVarDecl sdecl = UniqName.newBoundThis();
1720 VariableAccess s = TrAnExpr.makeVarAccess(sdecl, Location.NULL);
1721 Hashtable map = new Hashtable();
1722 map.put(GC.thisvar.decl, s);
1723
1724 int cReplacementsBefore = TrAnExpr.getReplacementCount();
1725
1726 /*
1727 * Unlike any body we may be translating, for these translations
1728 * this's type is that of the type that contains the invariant J.
1729 */
1730 Type savedType = GC.thisvar.decl.type;
1731 GC.thisvar.decl.type = TypeSig.getSig(ep.getParent());
1732
1733 invinfo.J = TrAnExpr.trSpecExpr(J, map, null);
1734 if (TrAnExpr.trSpecExprAuxConditions.size() != 0) {
1735 // Use andx here, because the op needs to be and in preconditions
1736 // and
1737 // implies in postconditions
1738 invinfo.J = GC.andx(GC.nary(TagConstants.BOOLAND,
1739 TrAnExpr.trSpecExprAuxConditions), invinfo.J);
1740 TrAnExpr.trSpecExprAuxConditions = ExprVec.make();
1741 }
1742 GC.thisvar.decl.type = savedType;
1743
1744 if (cReplacementsBefore == TrAnExpr.getReplacementCount()) {
1745 // static invariant
1746 invinfo.isStatic = true;
1747 invinfo.sdecl = null;
1748 invinfo.s = null;
1749 invinfo.map = null;
1750 } else {
1751 invinfo.isStatic = false;
1752 invinfo.sdecl = sdecl;
1753 invinfo.s = s;
1754 invinfo.map = map;
1755 }
1756 //System.out.println("COLLECTING INVARIANT-END " +
1757 // Location.toString(ep.getStartLoc()));
1758 }
1759 }
1760 // FIXME - Possibly causing bloated VCs
1761 collectInvariantsAxsToAdd = new java.util.HashSet();
1762 collectInvariantsAxsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1763 java.util.Set axsToAdd = new java.util.HashSet();
1764 //axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1765 java.util.Set axsDone = new java.util.HashSet();
1766 /*
1767 * while (false && ! axsToAdd.isEmpty()) { // FIXME - keep this off ???
1768 * RepHelper o = (RepHelper)axsToAdd.iterator().next();
1769 * axsToAdd.remove(o); if (!axsDone.add(o)) continue; Expr e =
1770 * TrAnExpr.getEquivalentAxioms(o,null); //axsToAdd.addAll(
1771 * TrAnExpr.trSpecAuxAxiomsNeeded); // Add a new node at the end of "ii"
1772 * InvariantInfo invinfo = new InvariantInfo(); invinfo.J = e;
1773 * invinfo.prag = ExprDeclPragma.make(TagConstants.AXIOM, e, 0,
1774 * Location.NULL); // FIXME invinfo.U = TypeSig.getSig(ep.parent); if
1775 * (iiPrev == null) ii = invinfo; else iiPrev.next = invinfo; iiPrev =
1776 * invinfo; if (true ) { //|| cReplacementsBefore ==
1777 * TrAnExpr.getReplacementCount()) // FIXME // static invariant
1778 * invinfo.isStatic = true; invinfo.sdecl = null; invinfo.s = null;
1779 * invinfo.map = null; } else { invinfo.isStatic = false; // FIXME
1780 * invinfo.sdecl = sdecl; // FIXME invinfo.s = s; // FIXME invinfo.map =
1781 * map; } }
1782 */
1783 } finally {
1784 TrAnExpr.closeForClause();
1785 }
1786
1787 return ii;
1788 }
1789
1790 /**
1791 * Collects the parameters of <code>spec.args</code> and the static fields
1792 * in <code>scope</code>, whose types are class types.
1793 */
1794
1795 private static ParamAndGlobalVarInfo collectParamsAndGlobals(
1796 /*@ non_null */Spec spec,
1797 /*@ non_null */FindContributors scope) {
1798 ParamAndGlobalVarInfo vars = null;
1799 ParamAndGlobalVarInfo varPrev = null;
1800
1801 // Add the parameters
1802 for (int i = 0; i < spec.dmd.args.size(); i++) {
1803 FormalParaDecl arg = spec.dmd.args.elementAt(i);
1804 TypeSig classSig;
1805 boolean isNonnull;
1806 if (i == 0 && arg == GC.thisvar.decl) {
1807 classSig = TypeSig.getSig(spec.dmd.getContainingClass());
1808 isNonnull = true;
1809 } else {
1810 classSig = Types.toClassTypeSig(arg.type);
1811 isNonnull = NonNullPragma(arg) != null;
1812 isNonnull = false; // FIXME
1813 }
1814
1815 if (classSig != null) {
1816 // The parameter is of a class type
1817 ParamAndGlobalVarInfo info = new ParamAndGlobalVarInfo();
1818 if (varPrev == null)
1819 vars = info;
1820 else
1821 varPrev.next = info;
1822 varPrev = info;
1823
1824 info.vdecl = arg;
1825 info.U = classSig;
1826 info.isNonnull = isNonnull;
1827 }
1828 }
1829
1830 // Add the static fields
1831 Enumeration fields = scope.fields();
1832 while (fields.hasMoreElements()) {
1833 FieldDecl fd = (FieldDecl)fields.nextElement();
1834
1835 TypeSig classSig = Types.toClassTypeSig(fd.type);
1836
1837 if (classSig != null && Modifiers.isStatic(fd.modifiers)) {
1838 // the field is a static field of a class type
1839 ParamAndGlobalVarInfo info = new ParamAndGlobalVarInfo();
1840 if (varPrev == null)
1841 vars = info;
1842 else
1843 varPrev.next = info;
1844 varPrev = info;
1845
1846 info.vdecl = fd;
1847 info.U = classSig;
1848 info.isNonnull = NonNullPragma(fd) != null;
1849 }
1850 }
1851
1852 return vars;
1853 }
1854
1855 //@ ensures \result != null;
1856 private static ExprVec addNewAxs(/*@ non_null @*/ HashSet axsToAdd, ExprVec assumptions) {
1857 if (assumptions == null) assumptions = ExprVec.make();
1858 java.util.Set axsDone = new java.util.HashSet();
1859 while (!axsToAdd.isEmpty()) {
1860 RepHelper o = (RepHelper)axsToAdd.iterator().next();
1861 axsToAdd.remove(o);
1862 if (!axsDone.add(o)) continue;
1863 Expr e = TrAnExpr.getEquivalentAxioms(o, null);
1864 assumptions.addElement(e);
1865 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
1866 TrAnExpr.trSpecAuxAxiomsNeeded.clear();
1867 }
1868 return assumptions;
1869
1870 }
1871
1872 /** Shaves a GC designator. */
1873
1874 private static VariableAccess shave(/*@ non_null */Expr e) {
1875 switch (e.getTag()) {
1876 case TagConstants.VARIABLEACCESS:
1877 return (VariableAccess)e;
1878
1879 case TagConstants.SELECT:
1880 return shave(((NaryExpr)e).exprs.elementAt(0));
1881
1882 default:
1883 Assert.fail("Unexpected case: " + " "
1884 + TagConstants.toString(e.getTag()) + " " + e + " "
1885 + Location.toString(e.getStartLoc()));
1886 return null;
1887 }
1888 }
1889
1890 /**
1891 * Creates and returns a new map that is <code>map</code> restricted to the
1892 * domain <code>e</code>. Assumes that every element in <code>e</code> is
1893 * in the domain of <code>map</code>.
1894 */
1895
1896 //+@ requires map.keyType == \type(GenericVarDecl);
1897 //+@ requires map.elementType == \type(VariableAccess);
1898 //+@ requires e.elementType == \type(GenericVarDecl);
1899 //@ ensures \result != null;
1900 static Hashtable restrict(/*@ non_null @*/ Hashtable map,
1901 /*@ non_null @*/ Enumeration e) {
1902 Hashtable r = new Hashtable();
1903 while (e.hasMoreElements()) {
1904 GenericVarDecl vd = (GenericVarDecl)e.nextElement();
1905 VariableAccess variant = (VariableAccess)map.get(vd);
1906 Assert.notNull(variant);
1907 r.put(vd, variant);
1908 }
1909 return r;
1910 }
1911
1912 /**
1913 * Converts a GenericVarDecl enumeration to a mapping from those variables to
1914 * new Variableaccesses.
1915 */
1916
1917 //@ requires e.elementType == \type(GenericVarDecl);
1918 //@ ensures \result != null;
1919 static Hashtable makeSubst(/*@ non_null */Enumeration e,
1920 /*@ non_null */String postfix) {
1921 Hashtable r = new Hashtable();
1922 while (e.hasMoreElements()) {
1923 GenericVarDecl vd = (GenericVarDecl)e.nextElement();
1924 VariableAccess variant = createVarVariant(vd, postfix);
1925 r.put(vd, variant);
1926 }
1927 return r;
1928 }
1929
1930 //@ ensures \result != null;
1931 static Hashtable makeSubst(/*@ non_null */FormalParaDeclVec args,
1932 /*@ non_null */String postfix) {
1933 Hashtable r = new Hashtable();
1934 for (int i = 0; i < args.size(); i++) {
1935 GenericVarDecl vd = args.elementAt(i);
1936 VariableAccess variant = createVarVariant(vd, postfix);
1937 r.put(vd, variant);
1938 }
1939 return r;
1940 }
1941
1942 /**
1943 * * Given a GenericVarDecl named "x@old", returns a VariableAccess to a *
1944 * fresh LocalVarDecl named "x@ <postfix>". * * This handles ESCJ 23b case 13.
1945 */
1946 //@ ensures \result != null;
1947 static VariableAccess createVarVariant(/*@ non_null */GenericVarDecl vd,
1948 /*@ non_null */String postfix)
1949 {
1950 String name = vd.id.toString();
1951 if (name.indexOf('@') != -1) name = name.substring(0, name.indexOf('@'));
1952
1953 Identifier id = Identifier.intern(name + "@" + postfix);
1954 LocalVarDecl ld = LocalVarDecl.make(vd.modifiers, vd.pmodifiers, id,
1955 vd.type, vd.locId, null, Location.NULL);
1956 VariableAccess va = VariableAccess.make(id, vd.locId, ld);
1957
1958 return va;
1959 }
1960
1961 /**
1962 * Adds to <code>cv</code> a condition stating that <code>vd</code> has
1963 * type <code>type</code>.
1964 */
1965
1966 private static void addFreeTypeCorrectAs(GenericVarDecl vd, Type type,
1967 /*@ non_null @*/ ConditionVec cv) {
1968 Expr e = TrAnExpr.typeCorrectAs(vd, type);
1969 Condition cond = GC.freeCondition(e, Location.NULL);
1970 cv.addElement(cond);
1971 }
1972
1973 /**
1974 * Returns a command that first does an <code>assume</code> for each
1975 * precondition in <code>spec</code>, then does <code>body</code>, then
1976 * checks the postconditions of <code>spec</code>, and finally checks the
1977 * modifies constraints implied by <code>spec</code>.
1978 */
1979
1980 public static GuardedCmd surroundBodyBySpec(GuardedCmd body,
1981 /*@ non_null @*/ Spec spec,
1982 FindContributors scope,
1983 Set syntargets,
1984 Hashtable premap,
1985 int locEndCurlyBrace)
1986 {
1987 StackVector code = new StackVector();
1988 code.push();
1989 addAssumptions(spec.preAssumptions, code);
1990 assumeConditions(spec.pre, code);
1991 code.addElement(body);
1992 addAssumptions(spec.postAssumptions, code);
1993 checkConditions(spec.post, locEndCurlyBrace, code);
1994 checkModifiesConstraints(spec, scope, syntargets, premap, locEndCurlyBrace,
1995 code);
1996
1997 return GC.seq(GuardedCmdVec.popFromStackVector(code));
1998 }
1999
2000 /**
2001 * Appends <code>code</code> with an <code>assume C</code> command for
2002 * every condition <code>C</code> in <code>cv</code>.
2003 */
2004
2005 private static void addAssumptions(/*@ non_null @*/ ExprVec ev,
2006 /*@ non_null @*/ StackVector code)
2007 {
2008 for (int i = 0; i < ev.size(); i++) {
2009 Expr e = ev.elementAt(i);
2010 code.addElement(GC.assume(e));
2011 //code.addElement(GC.check(e.getStartLoc(),TagConstants.CHKCONSISTENT,e,e.getStartLoc(),null));
2012 }
2013 }
2014
2015 private static void assumeConditions(/*@ non_null @*/ ConditionVec cv,
2016 /*@ non_null @*/ StackVector code)
2017 {
2018 for (int i = 0; i < cv.size(); i++) {
2019 Condition cond = cv.elementAt(i);
2020 //[GKS]
2021 if(Main.options().idc && cond.label == TagConstants.CHKEXPRDEFINEDNESS)
2022 {
2023 if(DefGCmd.debug)
2024 System.err.println("GK-Trace-DEF: "+ cond);
2025
2026 DefGCmd oDefGCs = new DefGCmd();
2027 if(DefGCmd.debug) {
2028 System.err.println("\tAbout to trAndGen:" +
2029 EscPrettyPrint.inst.toString(cond.pred));
2030 System.err.println("\tI.e.:" + cond.pred);
2031 }
2032 oDefGCs.trAndGen(cond.pred);
2033 GuardedCmd gc=oDefGCs.popFromCode();
2034 //GuardedCmd gc = GC.check(cond.locPragmaDecl, cond);
2035 code.addElement(gc);
2036 //[GKE]
2037 } else {
2038 code.addElement(GC.assumeAnnotation(cond.locPragmaDecl, cond.pred));
2039 }
2040 }
2041 }
2042
2043 /**
2044 * Appends <code>code</code> with an <code>check loc: C</code> command for
2045 * every condition <code>C</code> in <code>cv</code>.
2046 */
2047
2048 private static void checkConditions(/*@ non_null @*/ ConditionVec cv,
2049 int loc,
2050 StackVector code)
2051 {
2052 for (int i = 0; i < cv.size(); i++) {
2053 Condition cond = cv.elementAt(i);
2054 if (cond.label == TagConstants.CHKEXPRDEFINEDNESS)
2055 {
2056 if(Main.options().debug)
2057 {
2058 System.err.println("GK-Trace-POST: in GetSpec.checkConditions()");
2059 System.err.println("\tAbout to trAndGen:" +
2060 EscPrettyPrint.inst.toString(cond.pred));
2061 System.err.println("\tI.e.:" + cond.pred);
2062 }
2063 DefGCmd oDefGCs = new DefGCmd();
2064 oDefGCs.trAndGen(cond.pred);
2065 GuardedCmd gc=oDefGCs.popFromCode();
2066 code.addElement(gc);
2067 continue;
2068 }
2069 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) continue;
2070 Translate.setop(cond.pred);
2071 // if the condition is an object invariant, send its guarded command
2072 // translation as auxiliary info to GC.check
2073 if (cond.label == TagConstants.CHKOBJECTINVARIANT)
2074 code.addElement(GC.check(loc, cond, cond.pred));
2075 else
2076 code.addElement(GC.check(loc, cond));
2077 }
2078 }
2079
2080 private static void checkModifiesConstraints(Spec spec,
2081 FindContributors scope, Set syntargets, Hashtable premap, int loc,
2082 StackVector code) {
2083 // TBW
2084 }
2085
2086 private static InvariantInfo mergeInvariants(InvariantInfo ii) {
2087 if (!Main.options().mergeInv) return ii;
2088
2089 // Combined static/dynamic invariants, indexed by TypeSIg
2090 Hashtable staticInvs = new Hashtable();
2091 Hashtable dynInvs = new Hashtable();
2092
2093 while (ii != null) {
2094
2095 Hashtable table = ii.isStatic ? staticInvs : dynInvs;
2096
2097 InvariantInfo old = (InvariantInfo)table.get(ii.U);
2098
2099 if (old == null) {
2100
2101 table.put(ii.U, ii);
2102
2103 } else {
2104
2105 // Add ii to old
2106 old.J = GC.and(old.J, ii.isStatic ? ii.J : GC.subst(ii.sdecl, old.s,
2107 ii.J));
2108 }
2109
2110 ii = ii.next;
2111 }
2112
2113 // Now pull out merged invariants from tables
2114 Hashtable[] tables = {staticInvs, dynInvs};
2115 ii = null;
2116
2117 for (int i = 0; i < 2; i++) {
2118 Hashtable table = tables[i];
2119
2120 for (Enumeration e = table.elements(); e.hasMoreElements();) {
2121 InvariantInfo t = (InvariantInfo)e.nextElement();
2122 t.next = ii;
2123 ii = t;
2124 }
2125 }
2126
2127 return ii;
2128 }
2129
2130 private static boolean exprIsVisible(TypeSig originType,
2131 /*@ non_null @*/ Expr e) {
2132
2133 switch (e.getTag()) {
2134
2135 case TagConstants.FIELDACCESS: {
2136 FieldAccess fa = (FieldAccess)e;
2137 FieldDecl decl = fa.decl;
2138
2139 if (fa.od instanceof ExprObjectDesignator
2140 && !exprIsVisible(originType, ((ExprObjectDesignator)fa.od).expr))
2141 return false;
2142
2143 if (decl.parent == null) {
2144 // for array.length "field", there is no parent
2145 return true;
2146 } else if (Utils.findModifierPragma(decl, TagConstants.SPEC_PUBLIC) != null) {
2147 return true;
2148 } else {
2149 TypeSig sigDecl = TypeSig.getSig(decl.parent);
2150 return TypeCheck.inst.canAccess(originType, sigDecl, decl.modifiers,
2151 decl.pmodifiers);
2152 }
2153 }
2154
2155 default: {
2156 // Recurse over all children
2157 for (int i = 0; i < e.childCount(); i++) {
2158 Object o = e.childAt(i);
2159 if (o instanceof Expr) {
2160 if (!exprIsVisible(originType, (Expr)o)) return false;
2161 }
2162 }
2163
2164 return true;
2165 }
2166 }
2167 }
2168
2169 static public void collectFields(/*@ non_null @*/ Expr e, java.util.Set s) {
2170 // FIXME - have to avoid collecting bound variables of quantifiers
2171 switch (e.getTag()) {
2172 case TagConstants.PRE:
2173 return;
2174 case TagConstants.VARIABLEACCESS:
2175 VariableAccess va = (VariableAccess)e;
2176 if (va.decl instanceof FormalParaDecl) {
2177 //System.out.println("PARA " + ((VariableAccess)e).decl );
2178 return;
2179 }
2180 if (va.id.toString().endsWith("@pre")) return;
2181 //System.out.println("COLLECTED-VA " + e);
2182 s.add(e);
2183 break;
2184 default:
2185 }
2186
2187 // Recurse over all children
2188 for (int i = 0; i < e.childCount(); i++) {
2189 Object o = e.childAt(i);
2190 if (o instanceof Expr) collectFields((Expr)o, s);
2191 }
2192
2193 }
2194
2195 /*****************************************************************************
2196 * * Handling NON_NULL: * *
2197 ****************************************************************************/
2198
2199 /**
2200 * * Decorates <code>GenericVarDecl</code>'s to point to * NonNullPragmas
2201 * (SimpleModifierPragma's).
2202 */
2203 //@ invariant nonnullDecoration != null;
2204 // FIXME @ invariant nonnullDecoration.decorationType ==
2205 // FIXME @ \type(SimpleModifierPragma);
2206 /*@ spec_public */
2207 private static ASTDecoration nonnullDecoration = new ASTDecoration(
2208 "nonnullDecoration");
2209
2210 /**
2211 * * Mark v as non_null because of non_null pragma nonnull. * * Precondition:
2212 * nonnull is a NON_NULL pragma. * * (Used to implement inheritence of
2213 * non_null's.)
2214 */
2215 private static void setNonNullPragma(GenericVarDecl v,
2216 SimpleModifierPragma nonnull) {
2217 nonnullDecoration.set(v, nonnull);
2218 }
2219
2220 /**
2221 * * Has a particular declaration been declared non_null? If so, * return the
2222 * non_null pragma responsible. Otherwise, return null.
2223 * <p>* * Precondition: if the declaration is a formal parameter, then the *
2224 * spec of it's routine has already been computed.
2225 * <p>* * * WARNING: this is the only authorized way to determine this *
2226 * information. Do *not* attempt to search for NON_NULL modifiers * directly.
2227 * (This is needed to handle inherited NON_NULL's * properly.)
2228 */
2229 public static SimpleModifierPragma NonNullPragma(GenericVarDecl v) {
2230 // First check for a mark:
2231 /*
2232 * In JML, non_null pragmas do not inherit! SimpleModifierPragma mark =
2233 * (SimpleModifierPragma) nonnullDecoration.get(v); if (mark != null) return
2234 * mark;
2235 */
2236
2237 // Else fall back on a direct search of local modifiers:
2238 return (SimpleModifierPragma)Utils.findModifierPragma(v,
2239 TagConstants.NON_NULL);
2240 }
2241
2242 /**
2243 * Returns non-null if the formal parameter is declared non-null in some
2244 * overridden declaration of the method.
2245 */
2246 public static SimpleModifierPragma superNonNullPragma(GenericVarDecl v) {
2247 // First check for a mark:
2248 SimpleModifierPragma mark = (SimpleModifierPragma)nonnullDecoration.get(v);
2249 return mark;
2250 }
2251
2252 }
2253
2254 /**
2255 * * This class is used by <code>collectInvariants</code> and its callers, *
2256 * <code>extendSpecForCall</code> and <code>extendSpecForBody</code>.
2257 */
2258
2259 class InvariantInfo {
2260
2261 ExprDeclPragma prag;
2262
2263 TypeSig U; // "TypeSig" of class or interface that contains "prag"
2264
2265 boolean isStatic; // "true" if pragma declares a static invariant
2266
2267 LocalVarDecl sdecl; // "null" if "isStatic"; otherwise, a dummy variable
2268
2269 VariableAccess s; // "null" if "isStatic"; otherwise, a variable access
2270
2271 // of "sdecl"
2272 Hashtable map; // "{this-->s}"
2273
2274 Expr J; // translated expression, with substitution
2275
2276 // "{this-->s}" if not "isStatic"
2277 InvariantInfo next; // for linking "InvariantInfo" nodes
2278 }
2279
2280 /**
2281 * This class is used by <code>collectParamsAndGlobalVars</code> and its *
2282 * caller, <code>extendSpecForCall</code>.
2283 */
2284
2285 class ParamAndGlobalVarInfo {
2286
2287 GenericVarDecl vdecl;
2288
2289 TypeSig U;
2290
2291 boolean isNonnull;
2292
2293 ParamAndGlobalVarInfo next;
2294 }
2295