    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