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