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