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    }