001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.translate;
004    
005    import java.io.ByteArrayOutputStream;
006    import java.util.ArrayList;
007    import java.util.Enumeration;
008    import java.util.HashMap;
009    import java.util.Hashtable;
010    import java.util.Iterator;
011    import java.util.LinkedList;
012    import java.util.Map;
013    import java.util.Vector;
014    
015    import javafe.Tool;
016    import javafe.ast.ASTDecoration;
017    import javafe.ast.ASTNode;
018    import javafe.ast.ArrayInit;
019    import javafe.ast.ArrayRefExpr;
020    import javafe.ast.ArrayType;
021    import javafe.ast.AssertStmt;
022    import javafe.ast.BinaryExpr;
023    import javafe.ast.BreakStmt;
024    import javafe.ast.CastExpr;
025    import javafe.ast.CatchClause;
026    import javafe.ast.ClassDecl;
027    import javafe.ast.ClassLiteral;
028    import javafe.ast.CondExpr;
029    import javafe.ast.ConstructorDecl;
030    import javafe.ast.ConstructorInvocation;
031    import javafe.ast.ContinueStmt;
032    import javafe.ast.DoStmt;
033    import javafe.ast.EvalStmt;
034    import javafe.ast.Expr;
035    import javafe.ast.ExprObjectDesignator;
036    import javafe.ast.ExprVec;
037    import javafe.ast.FieldAccess;
038    import javafe.ast.FieldDecl;
039    import javafe.ast.ForStmt;
040    import javafe.ast.FormalParaDecl;
041    import javafe.ast.GenericBlockStmt;
042    import javafe.ast.GenericVarDecl;
043    import javafe.ast.Identifier;
044    import javafe.ast.IfStmt;
045    import javafe.ast.InitBlock;
046    import javafe.ast.InstanceOfExpr;
047    import javafe.ast.LabelStmt;
048    import javafe.ast.LiteralExpr;
049    import javafe.ast.LocalVarDecl;
050    import javafe.ast.MethodDecl;
051    import javafe.ast.MethodInvocation;
052    import javafe.ast.ModifierPragma;
053    import javafe.ast.NewArrayExpr;
054    import javafe.ast.NewInstanceExpr;
055    import javafe.ast.ParenExpr;
056    import javafe.ast.PrettyPrint;
057    import javafe.ast.PrimitiveType;
058    import javafe.ast.ReturnStmt;
059    import javafe.ast.RoutineDecl;
060    import javafe.ast.Stmt;
061    import javafe.ast.SwitchLabel;
062    import javafe.ast.SwitchStmt;
063    import javafe.ast.SynchronizeStmt;
064    import javafe.ast.ThisExpr;
065    import javafe.ast.ThrowStmt;
066    import javafe.ast.TryCatchStmt;
067    import javafe.ast.TryFinallyStmt;
068    import javafe.ast.Type;
069    import javafe.ast.TypeDecl;
070    import javafe.ast.TypeDeclElem;
071    import javafe.ast.TypeName;
072    import javafe.ast.UnaryExpr;
073    import javafe.ast.VarDeclStmt;
074    import javafe.ast.VarInit;
075    import javafe.ast.VariableAccess;
076    import javafe.ast.WhileStmt;
077    import javafe.tc.TypeSig;
078    import javafe.util.Assert;
079    import javafe.util.ErrorSet;
080    import javafe.util.Info;
081    import javafe.util.Location;
082    import javafe.util.Set;
083    import javafe.util.StackVector;
084    import escjava.Main;
085    import escjava.Options;
086    import escjava.ast.ArrayRangeRefExpr;
087    import escjava.ast.Call;
088    import escjava.ast.CmdCmdCmd;
089    import escjava.ast.Condition;
090    import escjava.ast.ConditionVec;
091    import escjava.ast.DecreasesInfo;
092    import escjava.ast.DecreasesInfoVec;
093    import escjava.ast.DerivedMethodDecl;
094    import escjava.ast.DynInstCmd;
095    import escjava.ast.EscPrettyPrint;
096    import escjava.ast.EverythingExpr;
097    import escjava.ast.ExprCmd;
098    import escjava.ast.ExprModifierPragma;
099    import escjava.ast.ExprStmtPragma;
100    import escjava.ast.ExprStmtPragmaVec;
101    import escjava.ast.GenericVarDeclVec;
102    import escjava.ast.GetsCmd;
103    import escjava.ast.GhostDeclPragma;
104    import escjava.ast.GuardedCmd;
105    import escjava.ast.GuardedCmdVec;
106    import escjava.ast.LabelExpr;
107    import escjava.ast.LocalVarDeclVec;
108    import escjava.ast.LoopCmd;
109    import escjava.ast.ModelDeclPragma;
110    import escjava.ast.Modifiers;
111    import escjava.ast.ModifiesGroupPragma;
112    import escjava.ast.ModifiesGroupPragmaVec;
113    import escjava.ast.NaryExpr;
114    import escjava.ast.NothingExpr;
115    import escjava.ast.RestoreFromCmd;
116    import escjava.ast.SeqCmd;
117    import escjava.ast.SetStmtPragma;
118    import escjava.ast.SimpleModifierPragma;
119    import escjava.ast.SkolemConstantPragma;
120    import escjava.ast.Spec;
121    import escjava.ast.SubGetsCmd;
122    import escjava.ast.SubSubGetsCmd;
123    import escjava.ast.TagConstants;
124    import escjava.ast.TypeExpr;
125    import escjava.ast.Utils;
126    import escjava.ast.VarInCmd;
127    import escjava.ast.WildRefExpr;
128    import escjava.backpred.FindContributors;
129    import escjava.tc.FlowInsensitiveChecks;
130    import escjava.tc.TypeCheck;
131    import escjava.tc.Types;
132    
133    public final class Translate
134    {
135      Frame frameHandler = null;
136      
137      // This Set contains method declarations for which axioms derived from
138      // postconditions need to be added to the assumptions for verifying the body.
139      public static java.util.Set axsToAdd = new java.util.HashSet();
140    
141      private Hashtable premap;
142      private Hashtable premapWithArgs;
143    
144      /** The type containing the routine whose body is being translated. */
145      private TypeDecl typeDecl;
146    
147      /**
148       * Translates the body of a method or constructor, as described in ESCJ 16, section
149       * 8.
150       *
151       * @param predictedSynTargs for correct translation, this must contain an upper
152       * bound for the syntactic targets of the result of this call.  A value of null is
153       * taken to represent the set of all variables & is hence always a safe value.
154       *
155       * @note passing a value of <the empty set> for predictedSynTargs will give a
156       * translation missing assert statements for checking call preconditions, but
157       * otherwise correct.  The resulting computation runs faster than passing null,
158       * while still having the same set of targets.  escjava.Main is currently using
159       * this trick as a kludge to compute the syntactic targets upper bound.
160       */
161      //@ requires rd.body != null;
162      public GuardedCmd trBody(/*@ non_null */ RoutineDecl rd,
163                               /*@ non_null */ FindContributors scope,
164                               Hashtable premap,
165                               Set predictedSynTargs,
166                               Translate inlineParent,
167                               boolean issueCautions) {
168    
169        Hashtable paramMap = GetSpec.makeSubst(rd.args, "pre");
170        premapWithArgs = new Hashtable();
171        premapWithArgs.putAll(paramMap);
172        if (premap != null) premapWithArgs.putAll(premap);
173    
174        frameHandler = new Frame(this, issueCautions, rd, premapWithArgs);
175        TrAnExpr.translate = this;
176        this.typeDecl = rd.parent;
177        this.premap = premap;
178        axsToAdd = new java.util.HashSet();
179    
180        // Reset the state of the AuxInfo module if this is top-level call to trBody
181        if (inlineParent == null) {
182          AuxInfo.reset();
183        }
184    
185        // Reset the internal state of <code>this</code>
186        this.rdCurrent = rd;
187        this.scope = scope;
188        this.predictedSynTargs = predictedSynTargs;
189        this.inlineParent = inlineParent;
190        if (inlineParent == null) {
191          this.inConstructorContext = isStandaloneConstructor(rd);
192        } else {
193          this.inConstructorContext = inlineParent.inConstructorContext &&
194            rdCurrent.parent == inlineParent.rdCurrent.parent;
195        }
196        this.issueCautions = issueCautions;
197        this.modifyEverythingLocations = new ArrayList();
198    
199        if (Info.on) {
200          System.out.print("trBody: ");
201          for (Translate ttIR = inlineParent;
202               ttIR != null;
203               ttIR = ttIR.inlineParent) {
204            System.out.print("  ");
205          }
206          System.out.println(TypeCheck.inst.getSig(rd.parent).toString() + "." +
207                             TypeCheck.inst.getRoutineName(rd) +
208                             TypeCheck.getSignature(rd));
209          System.out.flush();
210        }
211    
212        code.clear(); code.push();  // this mark popped by "spill"
213        declaredLocals.clear();
214        temporaries.clear(); temporaries.push();  // this mark popped by "spill"
215        tmpcount = 0;
216    
217        GC.thisvar.decl.type = scope.originType;
218    
219        code.push();  // this mark popped below
220        
221        /*
222         * Translate body:
223         */
224        if (rd.getTag() == TagConstants.METHODDECL) {
225          if (! Modifiers.isSynchronized(rd.modifiers)) {
226            // non-synchronized method
227            trStmt(rd.body,rd.parent);
228          } else if (! Modifiers.isStatic(rd.modifiers)) {
229            // synchronized instance method
230            trSynchronizedBody(GC.thisvar, rd.body, rd.locOpenBrace, typeDecl);
231          } else {
232            // synchronized static method
233            trSynchronizedBody(GC.nary(TagConstants.CLASSLITERALFUNC,
234                                       getClassObject(rd.parent)),
235                               rd.body, rd.locOpenBrace, typeDecl);
236          }      
237        } else {
238          Assert.notFalse(rd.getTag() == TagConstants.CONSTRUCTORDECL);
239          trConstructorBody((ConstructorDecl)rd, premap);
240        }
241    
242    
243        // "code" now contains two marks followed by what ESCJ 16 calls "CS"
244        // (except for the "assume !isAllocated(objectToBeConstructed, alloc)",
245        // which has already been prepended to "code" here)
246        if (Main.options().traceInfo > 0 &&
247            (inlineParent != null || Main.options().traceInfo > 1)) {
248          // add a label to track the implicit return ("falling off the end
249          // of the routine")
250          int loc = rd.getEndLoc();
251          Assert.notFalse(loc != Location.NULL);
252          GuardedCmd g = traceInfoLabelCmd(loc, loc, "ImplicitReturn", loc);
253          code.addElement(g);
254        }
255        code.addElement(GC.gets(GC.ecvar, GC.ec_return));
256        code.addElement(GC.trycmd(GC.seq(GuardedCmdVec.popFromStackVector(code)),
257                                  GC.skip()));
258        if (rd.getTag() == TagConstants.CONSTRUCTORDECL) {
259          code.addElement(GC.gets(GC.resultvar, GC.thisvar));
260        }
261        GuardedCmd body = spill();
262        // "code" is now empty:
263        Assert.notFalse(code.vectors()==1 && code.size()==0);
264    
265        // Finally, if there are any formal parameters, wrap "body" in a
266        // statement that saves and restores the values of the formal parameters
267        GuardedCmd res;
268        if (rd.args.size() == 0) {
269          res = body;
270        }
271        else {
272            
273          declaredLocals.push();  // this mark popped by "popDeclBlock"
274          code.push();  // this mark popped by "popDeclBlock"
275            
276          VariableAccess[] ppp = new VariableAccess[rd.args.size() * 2];
277          for (int i = 0; i < rd.args.size(); i++) {
278            FormalParaDecl arg = rd.args.elementAt(i);
279            VariableAccess va = (VariableAccess)paramMap.get(arg);
280            declaredLocals.addElement(va.decl);
281            ppp[2*i] = TrAnExpr.makeVarAccess(arg, Location.NULL);
282            ppp[2*i+1] = va;
283          }
284          for (int i = 0; i < ppp.length; i += 2) {
285            code.addElement(GC.gets(ppp[i+1], ppp[i]));
286          }
287          code.addElement(body);
288          for (int i = 0; i < ppp.length; i += 2) {
289            code.addElement(GC.restoreFrom(ppp[i], ppp[i+1]));
290          }
291          res = popDeclBlock();
292        }
293        //TrAnExpr.translate = null;
294        // Don't turn the above off because at present helper methods
295        // are inlined in which case this method is called recursively.
296        return res;
297      }
298    
299      /**
300       * @return <code>true</code> when <code>rd</code> is a constructor that does not
301       * call a sibling constructor.
302       */
303      private boolean isStandaloneConstructor(/*@ non_null */ RoutineDecl rd) {
304        if (!(rd instanceof ConstructorDecl)) {
305          return false;
306        }
307        ConstructorDecl cd = (ConstructorDecl)rd;
308        // From here on, return "true" unless there is a call to a sibling
309        // constructor.
310    
311        if (cd.body == null || cd.body.getTag() != TagConstants.BLOCKSTMT) {
312          return true;
313        }
314        GenericBlockStmt body = (GenericBlockStmt)cd.body;
315    
316        if (body.stmts.size() == 0) {
317          return true;
318        }
319        Stmt s0 = body.stmts.elementAt(0);
320    
321        if (s0.getTag() != TagConstants.CONSTRUCTORINVOCATION) {
322          return true;
323        }
324        ConstructorInvocation ccall = (ConstructorInvocation)s0;
325    
326        return ccall.decl.parent != cd.parent;
327      }
328    
329      /**
330       * Auxiliary routine used by trBody to translate the body of a constructor, as
331       * described in ESCJ 16, section 8.
332       */
333      //@ requires cd.body != null;
334      private void trConstructorBody(/*@ non_null */ ConstructorDecl cd,
335                                     Hashtable premap) {
336        // assume !isAllocated(objectToBeConstructed, alloc);
337        {
338          Expr isAllocated = GC.nary(TagConstants.ISALLOCATED,
339                                     GC.objectTBCvar, GC.allocvar);
340          code.addElement(GC.assume(GC.not(isAllocated)));
341        }
342    
343    
344        if (cd.body == null) return; 
345        // FIXME - not entirely sure we should omit everything
346        // from here on if there is no body.
347        /*
348         * Find the call to the superclass or sibling constructor, if
349         * any.  In particular, set both "body" and "ccall" to
350         * non-"null" values if "cd.body" starts with a constructor
351         * call.  ("ccall" is non-"null" only if "body" is, too.)
352         */
353        GenericBlockStmt body = null;
354        ConstructorInvocation ccall = null;
355        if (cd.body.getTag() == TagConstants.BLOCKSTMT) {
356          body = (GenericBlockStmt)cd.body;
357          if (1 <= body.stmts.size()) {
358            Stmt s0 = body.stmts.elementAt(0);
359            if (s0.getTag() == TagConstants.CONSTRUCTORINVOCATION) {
360              ccall = (ConstructorInvocation)s0;
361            }
362          }
363        }
364    
365    
366        if (ccall==null) {
367          /*
368           * Here "cd" refers to a constructor of class "Object"
369           * that does not call any sibling constructor.
370           *
371           * The code that used to be here can be found in revision
372           * 1.87 of this file (Translate.java); it is probably
373           * somewhat "rotted", though.
374           */
375          Assert.notFalse(Types.isSameType(TypeSig.getSig(cd.parent),
376                                           Types.javaLangObject()));
377          Assert.notImplemented("Checking of Object constructor body");
378        }
379    
380    
381        TypeDecl tdecl = cd.parent;
382        TypeSig type = TypeSig.getSig(tdecl);
383        try {
384          if (!type.isTopLevelType())
385            Inner.firstThis0 = Inner.getEnclosingInstanceArg(cd);
386    
387          trConstructorCallStmt(ccall);
388        } finally {
389          Inner.firstThis0 = null;
390        }
391    
392    
393        // assume typeof(this) <: T
394        TypeExpr texpr = TypeExpr.make(tdecl.getStartLoc(),
395                                       tdecl.getEndLoc(),
396                                       type);
397        Expr goodType = GC.nary(TagConstants.TYPELE,
398                                GC.nary(TagConstants.TYPEOF, GC.thisvar),
399                                texpr);
400        code.addElement(GC.assume(goodType));
401            
402        // assume objectToBeConstructed == this;
403        code.addElement(GC.assume(GC.nary(TagConstants.REFEQ,
404                                          GC.objectTBCvar,
405                                          GC.thisvar)));
406    
407        /*
408         * Insert this.this$0 = this$0arg if we are an inner-class constructor:
409         */
410        {
411          TypeSig T = TypeSig.getSig(cd.parent);
412          if (!T.isTopLevelType()) {
413            FieldDecl this0 = Inner.getEnclosingInstanceField(T);
414            FormalParaDecl this0arg = Inner.getEnclosingInstanceArg(cd);
415                    
416            code.addElement(GC.subgets(
417                                       TrAnExpr.makeVarAccess(this0, Location.NULL),
418                                       GC.thisvar,
419                                       TrAnExpr.makeVarAccess(this0arg, Location.NULL)));
420          }
421        }
422    
423            
424        if (ccall.decl.parent != cd.parent) {
425          // superclass (not sibling) constructor call:
426          instanceInitializers(cd.parent);
427        }
428    
429        // call "trStmt" on the rest of the body:
430        declaredLocals.push();  // this mark popped by "wrapUpDeclBlock"
431        code.push();            // this mark popped by "wrapUpDeclBlock"
432        for (int i = 1; i < body.stmts.size(); i++) {
433          trStmt(body.stmts.elementAt(i),cd.parent);
434        }
435        wrapUpDeclBlock();
436      }
437    
438      private TypeExpr getClassObject(/*@ non_null */ TypeDecl tdClass) {
439        Type type = TypeSig.getSig(tdClass);
440        TypeExpr texpr = TypeExpr.make(tdClass.getStartLoc(), tdClass.getEndLoc(),
441                                       type);
442        return texpr;
443      }
444      
445    
446      /**
447       * This method implements "InstanceInitializers", as described in section 8.1 of
448       * ESCJ 16.
449       */  
450      private void instanceInitializers(/*@ non_null */ TypeDecl tdecl) {
451        // First, provide zero-equivalent values for fields in first-inherited
452        // interfaces
453        if (tdecl instanceof ClassDecl) {
454          Enumeration interfaces = GetSpec.getFirstInheritedInterfaces((ClassDecl)tdecl);
455          while (interfaces.hasMoreElements()) {
456            TypeDecl tdSuperInterface = (TypeDecl)interfaces.nextElement();
457            instanceInitializeZero(tdSuperInterface);
458          }
459        }
460        // Then, provide zero-equivalent values for fields in "tdecl"
461        instanceInitializeZero(tdecl);
462    
463        // Finally, compute the programmer-supplied initial values and assign
464        // the fields appropriately.  (Note, first-inherited interfaces don't
465        // have programmer-supplied initial values for instance fields, since
466        // the only instance fields in interfaces are ghost fields and they
467        // don't have initial values.)
468        for (int i = 0; i < tdecl.elems.size(); i++) {
469          TypeDeclElem tde = tdecl.elems.elementAt(i);
470          if (tde instanceof ModelDeclPragma) continue;
471          if (tde instanceof GhostDeclPragma)
472            tde = ((GhostDeclPragma)tde).decl;
473    
474          if (tde.getTag() == TagConstants.INITBLOCK) {
475            InitBlock ib = (InitBlock)tde;
476            if (!Modifiers.isStatic(ib.modifiers)) {
477              trStmt(ib.block,tdecl);
478            }
479          } else if (tde.getTag() == TagConstants.FIELDDECL) {
480            FieldDecl fd = (FieldDecl)tde;
481            if (!Modifiers.isStatic(fd.modifiers) && fd.init != null) {
482              Assert.notFalse(fd.locAssignOp != Location.NULL);
483              // e= Expr[[ fd.init ]]
484              Expr e = ptrExpr(fd.init);
485              // WriteCheck[[ f[this], e ]]
486              VariableAccess f = TrAnExpr.makeVarAccess(fd, Location.NULL);
487              Expr lhs = GC.select(f, GC.thisvar);
488              writeCheck(lhs, fd.init, e, fd.locAssignOp, true);
489              // f[this] = e
490              code.addElement(GC.subgets(f, GC.thisvar, e));
491            }
492          }
493        }
494      }
495    
496      /**
497       * Called by <code>instanceInitializers</code>.
498       */
499      private void instanceInitializeZero(/*@ non_null */ TypeDecl tdecl) {
500        for (int i = 0; i < tdecl.elems.size(); i++) {
501          TypeDeclElem tde = tdecl.elems.elementAt(i);
502          if (tde instanceof ModelDeclPragma) continue;
503          if (tde instanceof GhostDeclPragma)
504            tde = ((GhostDeclPragma)tde).decl;
505    
506          if (tde.getTag() == TagConstants.FIELDDECL) {
507            FieldDecl fd = (FieldDecl)tde;
508            if (!Modifiers.isStatic(fd.modifiers)) {
509              // f[this] = <default value>
510              VariableAccess fdref = TrAnExpr.makeVarAccess(fd, Location.NULL);
511              Expr defaultValue = null;
512              switch (fd.type.getTag()) {
513              case TagConstants.BOOLEANTYPE:
514                defaultValue = GC.falselit;
515                break;
516                  
517              case TagConstants.BIGINTTYPE:
518              case TagConstants.INTTYPE:
519              case TagConstants.LONGTYPE:
520              case TagConstants.CHARTYPE:
521              case TagConstants.BYTETYPE:
522              case TagConstants.SHORTTYPE:
523                defaultValue = GC.zerolit;
524                break;
525    
526              case TagConstants.ARRAYTYPE:
527              case TagConstants.TYPENAME:
528              case TagConstants.TYPESIG:
529                if (GetSpec.NonNullPragma(fd) != null) {
530                  defaultValue = temporary(fd.id.toString() + "@zero",
531                                           fd.getStartLoc());
532                } else {
533                  defaultValue = GC.nulllit;
534                }
535                break;
536    
537              case TagConstants.DOUBLETYPE:
538              case TagConstants.FLOATTYPE:
539                defaultValue = GC.nary(TagConstants.CAST, GC.zerolit,
540                                       GC.typeExpr(fd.type));
541                break;
542    
543              case TagConstants.TYPECODE:
544                // TYPE fields have no default value:
545                defaultValue = temporary(fd.id.toString() + "@zero",
546                                         fd.getStartLoc());
547                break;
548    
549              case TagConstants.NULLTYPE:
550              default:
551                /*@ unreachable ;*/
552                Assert.fail("Unexpected type tag " + TagConstants.toString(fd.type.getTag()));
553                break;
554              }
555              if (defaultValue != null)
556                code.addElement(GC.subgets(fdref, GC.thisvar, defaultValue));
557            }
558          }
559        }
560      }
561    
562      //// Instance variables
563    
564      /** References the routine currently being checked by trBody. */
565    
566      private RoutineDecl rdCurrent;
567    
568      /**
569       * Singly-linked list of the inline parents.  Is <code>null</code> if this
570       * translation is not being inlined.
571       */
572      private Translate inlineParent;
573    
574      /**
575       * Indicates whether to issue cautions.  Value is set from outer call to trBody
576       * and also used by nested/recursive calls.
577       */
578      private boolean issueCautions;
579    
580      /**
581       * Indicates whether or not the current routine is in a "constructor context",
582       * meaning that it is a constructor being checked or a method in the same class
583       * that's being inlined into the constructor.
584       */
585      private boolean inConstructorContext;
586    
587      /**
588       * Contains the guarded commands generated so far for the current method.  As the
589       * translation enters into Java blocks, <code>code</code> gets pushed.  As blocks
590       * are left, <code>code</code> is poped into a <code>GuardedCmdVec</code> which
591       * is wrapped inside a BLOCK guarded command that gets appended onto
592       * <code>code</code>.
593       */
594      /*@ spec_public */ private final StackVector code = new StackVector();
595    
596      /**
597       * List of loop invariant pragmas seen so far (and not yet used) within the
598       * current method.
599       */
600      private ExprStmtPragmaVec loopinvariants = ExprStmtPragmaVec.make();
601    
602      /**
603       * List of loop decreases pragmas seen so far (and not yet used) within the
604       * current method.
605       */
606    
607      private /*@ non_null */ ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make();
608    
609      private /*@ non_null */ ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make();
610      
611      protected /*@ non_null */ LocalVarDeclVec skolemConstants = LocalVarDeclVec.make();
612    
613      /**
614       * Contains the local Java variables declared in the current <em>block</em> so
615       * far for the current block and enclosing blocks of the current method.  This
616       * variable is maintained parallel to <code>code</code>: Each time a Java block
617       * is entered, <code>declaredLocals</code> gets pushed; when a block is left,
618       * <code>declaredLocals</code> is popped into a <code>GenericVarDeclVec</code>
619       * that gets wrapped inside a BLOCK guarded command.
620       */
621      private final /*@ non_null */ StackVector declaredLocals = new StackVector();
622    
623      /**
624       * Contains the temporaries that generated for the current method that haven't
625       * yet been declared in a VARINCMD.
626       */
627      private final /*@ non_null */ StackVector temporaries = new StackVector();
628    
629    
630      /** Describes the current scope. */
631    
632      private FindContributors scope;
633    
634      /**
635       * Describes the current predicted set of synTargs.
636       *
637       * <p> If non-null, then represents an <em>*upper*</em> bound on
638       * freeVars of the result of the current trBody(...) call.
639       */
640      private Set predictedSynTargs;
641    
642      /**
643       * Describes what aspects of an inlined call to check and what
644       * aspects to either assert or simply ignore.  A call
645       * (MethodInvocation, ConstructorInvocation, NewInstanceExpr) may
646       * map to an <code>InlineSettings</code> object in which the
647       * <code>nextInlineCheckDepth</code> and
648       * <code>nextInlineDepthPastCheck</code> fields are unused.
649       *
650       * <p> This variable is used only for some call-site specific
651       * inlining, in particular, currently only to handle the
652       * -inlineConstructors flag.  Other reasons for inlining are taken
653       * care of in method <code>computeInlineSettings</code>. </p>
654       */
655      public static final /*@ non_null */ ASTDecoration inlineDecoration =
656        new ASTDecoration("inlineDecoration");
657    
658    
659      //// Generation of variables to put into guarded commands
660    
661      /**
662       * Pops temporaries and code, and makes these into a VARINCMD command that is
663       * returned.  If there are no temporaries, only the code is returned.
664       */
665      private GuardedCmd spill() {
666        GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
667        GenericVarDeclVec temps = GenericVarDeclVec.popFromStackVector(temporaries);
668        return GC.block(temps, body);
669      }
670    
671    
672      /**
673       * Make a fresh version of a special variable to save it in.
674       *
675       * (This partially handles ESCJ 23b, case 4.)
676       */
677      //@ requires (* v accesses a special variable. *);
678      private VariableAccess adorn(VariableAccess v) {
679        Assert.precondition(v.decl.locId == UniqName.specialVariable);
680    
681        VariableAccess result= GC.makeVar(v.decl.id, v.decl.locId);
682        result.loc= v.getStartLoc();
683    
684        temporaries.addElement(result.decl);
685        return result;
686      }
687    
688    
689      /**
690       * Make a fresh "boolean" variable to hold the initialized status
691       * of a Java variable that is marked as "uninitialized".
692       *
693       * (This partially handles ESCJ 23b, case 13.)
694       */
695      //@ requires (* v accesses a normal Java variable. *);
696      private VariableAccess initadorn(/*@ non_null */ LocalVarDecl d) {
697        Identifier idn = Identifier.intern(d.id + "@init");
698    
699        VariableAccess result = GC.makeVar(idn, d.locId);
700        result.loc = Location.NULL;
701    
702        return result;
703      }
704    
705    
706      //// Statement translation
707    
708      // Utility routines
709    
710      private boolean isRecursiveInvocation(/*@ non_null */ RoutineDecl r) {
711        Translate t = this;
712        while (t != null) {
713          if (t.rdCurrent == r) {
714            return true;  // the routine has been visited before
715          }
716          t = t.inlineParent;
717        }
718        return false;
719      }
720    
721      /** Reduces number of stack marks by 1. */
722      
723      private GuardedCmd opBlockCmd(Expr label) {
724        GuardedCmd g= GC.seq(GuardedCmdVec.popFromStackVector(code));
725        GuardedCmd ifc= GC.ifcmd(GC.nary(TagConstants.ANYEQ, GC.ecvar, label),
726                                 GC.skip(), GC.raise());
727        return GC.trycmd(g, ifc);
728      }
729      
730      private Expr breakLabel(Stmt s) {return GC.symlit(s, "L_");}
731      private Expr continueLabel(Stmt s) {return GC.symlit(s, "C_");}
732    
733      /**
734       * Emits the commands <code>EC= label; raise</code> to <code>code</code>.
735       */
736      private void raise(Expr label) {
737        code.addElement(GC.gets(GC.ecvar, label));
738        code.addElement(GC.raise());
739      }
740    
741      /**
742       * Computes purity information for Java expression <code>e</code>, translates
743       * <code>e</code> (emitting any code needed to account for impurities or side
744       * effects in the expression), and emits code that performs a <code>RAISE
745       * label</code> command if the expression evaluates to <code>false</code>.  As
746       * usual, emitted code is appended to <code>code</code> and temporaries are
747       * appended to <code>temporaries</code>.
748       */
749      private void guard(Expr e, Expr label) {
750        Expr grd = ptrExpr(e);
751        code.push();  // popped off by boxPopFromStackVector
752        code.addElement(GC.assume(grd));
753        code.addElement(GC.skip());
754        code.push();  // popped off by boxPopFromStackVector
755        code.addElement(GC.assumeNegation(grd));
756        raise(label);
757        GuardedCmd ifc= GC.boxPopFromStackVector(code);
758        code.addElement(ifc);
759      }
760      
761      /**
762       * Appends to <code>code</code> commands that make up a loop with nominal body
763       * <code>guard;body</code>, where <code>label</code> is raised within
764       * <code>body</code> to terminate the loop.  The vector <code>J</code> contains
765       * the user-declared loop invariant pragmas.  The vector <code>decreases</code>
766       * contains the user-declared bound function pragmas.  The scope of the variables
767       * in <code>tempVars</code> is the nominal body; this method will wrap an
768       * appropriate <code>var .. in .. end</code> command around these.
769       */
770      private void makeLoop(int sLoop, int eLoop, int locHotspot,
771                            GenericVarDeclVec tempVars,
772                            GuardedCmd guard, 
773                            GuardedCmd body,
774                            /*@ non_null */ ExprStmtPragmaVec J, 
775                            ExprStmtPragmaVec decreases,
776                            LocalVarDeclVec skolemConsts, 
777                            /*@ non_null */ ExprStmtPragmaVec P,
778                            Expr label) {
779    
780        code.push();  // this mark popped by "opBlockCmd"
781    
782        // construct old variants of the variables that are targets of the loop.
783        code.push();
784        temporaries.push();
785        GuardedCmd S = GC.seq(guard, body);
786        Set normalTargets = Targets.normal(GC.block(tempVars, S));
787        Hashtable h = GetSpec.makeSubst(normalTargets.elements(), "loopold");
788    
789        for (Enumeration keys = h.keys(); keys.hasMoreElements(); ) {
790          GenericVarDecl vd = (GenericVarDecl) keys.nextElement();
791          VariableAccess va = (VariableAccess) h.get(vd);
792          temporaries.addElement(va.decl);
793          code.addElement(GC.assume(GC.nary(TagConstants.ANYEQ, 
794                                            VariableAccess.make(vd.id, sLoop, vd), va)));
795        }
796    
797    
798        ExprVec ev = ExprVec.make(10);
799    
800        ConditionVec invs = ConditionVec.make();
801        for (int i = 0; i < J.size(); i++) {
802          TrAnExpr.initForClause();
803          ExprStmtPragma loopinv = J.elementAt(i);
804          Expr pred = TrAnExpr.trSpecExpr(loopinv.expr, null, h);  // FIXME - what about formal params in old?
805          Condition cond = GC.condition(TagConstants.CHKLOOPINVARIANT,
806                                        pred,
807                                        loopinv.getStartLoc());
808          if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
809          invs.addElement(cond);      
810        }
811    
812        DecreasesInfoVec decs = DecreasesInfoVec.make();
813        for (int i = 0; i < decreases.size(); i++) {
814          ExprStmtPragma d = decreases.elementAt(i);
815          TrAnExpr.initForClause();
816          Expr de = TrAnExpr.trSpecExpr(d.expr);  // FIXME - what about old?
817          int loc = d.getStartLoc();
818          VariableAccess fOld = temporary("decreases", loc, loc);
819          DecreasesInfo di = new DecreasesInfo(loc, de, fOld);
820          if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
821          decs.addElement(di);
822        }
823    
824        ExprVec preds = ExprVec.make();
825        for (int i = 0; i < P.size(); i++) {
826          ExprStmtPragma looppred = P.elementAt(i);
827          Expr e = TrAnExpr.trSpecExpr(looppred.expr, null, h);  // FIXME - what about params?
828          if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow());
829          preds.addElement(e);
830        }
831    
832        // If we ever implement the "safe" (as opposed to "fast") version of
833        // loops, then "invs" should be extended with loop object invariant
834        // conditions, and "guard" should be prefixed by a sequence of
835        // TargetTypeCorrect assume commands, per ESCJ 16.
836    
837        LoopCmd loop = GC.loop(sLoop, eLoop, locHotspot, h,
838                               invs, decs, skolemConsts, preds,
839                               tempVars, guard, body);
840        switch (Main.options().loopTranslation) {
841        case Options.LOOP_FAST:
842        case Options.LOOP_FALL_THRU:
843          desugarLoopFast(loop,ev);
844          break;
845    
846        case Options.LOOP_SAFE:
847          desugarLoopSafe(loop,ev);
848          break;
849    
850        default:
851          Assert.fail("unexpected loop translation scheme: " + 
852                      Main.options().loopTranslation);
853        }
854    
855        code.addElement(loop);
856    
857        code.addElement(spill());
858    
859        code.addElement(opBlockCmd(label));
860      }
861    
862      /**
863       * Desugars <code>loop</code> according to the fast option.  In particular, sets
864       * <code>loop.desugared</code> to the desugaring.
865       */
866      private void desugarLoopFast(LoopCmd loop, ExprVec axs) {
867        // A fast-desugared loop has the shape:
868        //   var V in  J;B;S;J;B;S;J;..;fail  end
869        // where "V" is the list of temporary variables used within the
870        // loop, "J" is the command that checks loop invariants, "B" is
871        // the guard command, and "S" is the rest of the body of the
872        // loop.
873        //
874        // The number of repetitions of "J;B;S" is determined by
875        // "Main.loopUnrollCount".  After these repetitions is another
876        // "J", and if "Main.loopUnrollHalf" is "true", then there is
877        // then one more "B".  As shown above, the sequence ends with
878        // a "fail" command.
879        //
880        // If "Main.traceInfo" is positive, then each "J" is immediately
881        // preceded by a command of the form:
882        //   assume (lblpos trace.LoopIter^L#i true)
883        // where "L" is the source location of the loop and "i" is the
884        // iteration count.
885    
886        // Build a command that checks loop invariants
887        code.push();  // this mark popped below
888        checkLoopInvariants(loop,axs);
889        GuardedCmd J = GC.seq(GuardedCmdVec.popFromStackVector(code));
890    
891        code.push(); // this mark popped below after for loop
892    
893        String locString = UniqName.locToSuffix(loop.getStartLoc()) + "#";
894    
895        int numOfComponents = 3 * Main.options().loopUnrollCount +
896          (Main.options().loopUnrollHalf ? 2 : 1);
897        int iComp = 0;
898        int i = 0;
899        for ( ; true; i++) {
900          code.push();  // this mark popped below
901    
902          // -- J --
903          Assert.notFalse(iComp != numOfComponents);
904          if (Main.options().traceInfo > 0) {
905            String label = locString + i;
906            code.addElement(traceInfoLabelCmd(loop.getStartLoc(),
907                                              loop.getEndLoc(),
908                                              "LoopIter", label));
909          }
910          code.addElement(J);
911          iComp++;
912          if (iComp == numOfComponents) {
913            break;
914          }
915          // -- B --
916          addLoopDecreases(loop, 0);  // fOld = F;
917          GuardedCmd B = loop.guard;
918          if (Main.options().traceInfo > 0 && 0 < i) {
919            B = cloneGuardedCommand(B);
920          }
921          code.addElement(B);
922          iComp++;
923          if (iComp == numOfComponents) {
924            break;
925          }
926          // -- S --
927          GuardedCmd S = loop.body;
928          if (Main.options().traceInfo > 0 && 0 < i) {
929            S = cloneGuardedCommand(S);
930          }
931          code.addElement(S);
932          addNewAssumptionsNow(axs);
933          addLoopDecreases(loop, 1);  // check 0 <= fOld;
934          addLoopDecreases(loop, 2);  // check F < fOld;
935          iComp++;
936    
937          GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars);
938          code.addElement(iter);
939    
940          Assert.notFalse(iComp != numOfComponents);
941        }
942    
943        // pop once more to get J or J;B as the case might be
944        GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars);
945        code.addElement(iter);
946    
947        // Stop unrolling here
948        if (Main.options().loopTranslation != Options.LOOP_FALL_THRU) {
949          code.addElement(GC.fail());
950        }
951    
952        loop.desugared = GC.seq(GuardedCmdVec.popFromStackVector(code));
953      }
954    
955      //@ requires 0 <= iteration;
956      private GuardedCmd wrapUpUnrolledIteration(/*@ non_null */ String locString,
957                                                 int iteration,
958                                                 /*@ non_null */ GenericVarDeclVec tempVars) {
959        GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
960        body = GC.block(tempVars, body);
961        GuardedCmd iter = DynInstCmd.make(locString + iteration, body);
962        return iter;
963      }
964    
965      /**
966       * Adds to <code>code</code> the various pieces of the translation of the
967       * decreases pragma.  The pieces are:
968       * <ul>
969       * <li> 0. fOld = F;
970       * <li> 1. check 0 <= fOld;
971       * <li> 2. check F < fOld;
972       * </ul>
973       */
974      //@ requires 0 <= piece && piece < 3;
975      //@ modifies code.elementCount;
976      private void addLoopDecreases(/*@ non_null */ LoopCmd loop,
977                                    int piece) {
978        for (int i = 0; i < loop.decreases.size(); i++) {
979          DecreasesInfo di = loop.decreases.elementAt(i);
980          switch (piece) {
981          case 0: // fOld = F;
982            code.addElement(GC.gets(di.fOld, di.f));
983            break;
984          case 1: // check 0 <= fOld;
985            addCheck(loop.locHotspot, TagConstants.CHKDECREASES_BOUND,
986                     GC.nary(TagConstants.INTEGRALLE, GC.zerolit, di.fOld),
987                     di.loc);
988            break;
989          case 2: // check F < fOld;
990            addCheck(loop.locHotspot, TagConstants.CHKDECREASES_DECR,
991                     GC.nary(TagConstants.INTEGRALLT, di.f, di.fOld),
992                     di.loc);
993            break;
994          default:
995            //@ unreachable;
996            Assert.fail("addLoopDecreases: unexpected piece number");
997            break;
998          }
999        }
1000      }
1001    
1002    
1003      /**
1004       * targets is set of GenericVarDecls. aTargets is set of ATargets.
1005       */
1006      public GuardedCmd modifyATargets(/*@ non_null */ Set aTargets, int loc) {
1007        code.push();
1008        for (Enumeration e = aTargets.elements(); e.hasMoreElements();) {
1009          ATarget at = (ATarget)e.nextElement();
1010          VariableAccess va = VariableAccess.make(at.x.id, loc, at.x);
1011    
1012          if (at.indices.length == 0 || 
1013              (at.indices[0] == null && 
1014               (at.indices.length == 1 || at.indices[1] == null))) {
1015            // x, x[*], x[*][*]
1016            // System.out.println("x = " + at.x.id.toString() + 
1017            //                    ", at.indices.length = " + at.indices.length);
1018            code.addElement(modify(va, loc));
1019          } else if (at.indices.length == 1) {
1020            // x[e]
1021            VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1022            code.addElement(GC.subgets(va, at.indices[0], newVal));
1023          } else if (at.indices[0] == null) {
1024            // x[*][e]
1025            VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1026            VariableAccess var1 = GC.makeVar("i", loc);
1027            VariableAccess var2 = GC.makeVar("j", loc);
1028    
1029            Expr a = GC.implies(GC.nary(TagConstants.ANYNE, var2, at.indices[1]),
1030                                GC.nary(TagConstants.ANYEQ, 
1031                                        GC.select(GC.select(va, var1), var2), 
1032                                        GC.select(GC.select(newVal, var1), var2)));
1033            code.addElement(GC.assume(GC.forall(var1.decl,GC.forall(var2.decl, a ))));
1034            code.addElement(GC.gets(va, newVal));                     
1035          } else if (at.indices[1] == null) {
1036            // x[e][*]
1037            VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1038            VariableAccess var1 = GC.makeVar("i", loc);
1039            VariableAccess var2 = GC.makeVar("j", loc);
1040    
1041            Expr a = GC.implies(GC.and( GC.nary(TagConstants.ANYNE, var1, at.indices[0]),
1042                                        GC.nary(TagConstants.IS, var2, TrAnExpr.trType(Types.intType))),
1043                                GC.nary(TagConstants.ANYEQ, 
1044                                        GC.select(GC.select(va, var1), var2), 
1045                                        GC.select(GC.select(newVal, var1), var2)));
1046            code.addElement(GC.assume(GC.forall(var1.decl, GC.forall(var2.decl, a))));
1047            code.addElement(GC.gets(va, newVal));                     
1048          } else {
1049            // x[e][e]
1050            VariableAccess newVal = temporary(va.id.toString(), loc, loc);
1051            code.addElement(GC.subsubgets(va, at.indices[0], at.indices[1], newVal));
1052          }
1053        }
1054            
1055        return GC.seq(GuardedCmdVec.popFromStackVector(code));
1056      }
1057    
1058      public GuardedCmd modify(/*@ non_null */ Set simpleTargets, int loc) {
1059        code.push();
1060        for (Enumeration e = simpleTargets.elements(); e.hasMoreElements();) {
1061          GenericVarDecl at = (GenericVarDecl)e.nextElement();
1062          VariableAccess va = VariableAccess.make(at.id, loc, at);      
1063          code.addElement(modify(va, loc));
1064        }
1065            
1066        return GC.seq(GuardedCmdVec.popFromStackVector(code));
1067      }
1068    
1069      /**
1070       * Desugars <code>loop</code> according to the safe option.  In particular, sets
1071       * <code>loop.desugared</code> to the desugaring.
1072       */
1073      public void desugarLoopSafe(LoopCmd loop, ExprVec axs) {
1074        // Build a command that checks loop invariants safely
1075    
1076        code.push();  // this mark popped below
1077        checkLoopInvariants(loop,axs);
1078        code.addElement(GC.fail());
1079        GuardedCmd checkInvariantsInitially = 
1080          GC.seq(GuardedCmdVec.popFromStackVector(code));
1081    
1082        code.push();  // this mark popped shortly
1083        addLoopDecreases(loop, 0);  // fOld = F;
1084        code.addElement(loop.guard);
1085        code.addElement(loop.body);
1086        addNewAssumptionsNow(axs);
1087        addLoopDecreases(loop, 1);  // check 0 <= fOld;
1088        addLoopDecreases(loop, 2);  // check F < fOld;
1089        GuardedCmd S = GC.seq(GuardedCmdVec.popFromStackVector(code));
1090    
1091        Set vds = Targets.normal(GC.block(loop.tempVars, S));
1092        GuardedCmd modifyGc = modify(vds, loop.locStart);
1093    
1094        if( Main.options().preciseTargets ) {
1095          Set aTargets = ATarget.compute( GC.block(loop.tempVars, loop ));
1096          modifyGc = modifyATargets( aTargets, S.getStartLoc());
1097        }
1098    
1099        code.push();  // this mark popped below
1100        code.addElement(modifyGc);
1101    
1102        for (Enumeration e = vds.elements(); e.hasMoreElements();) {
1103          GenericVarDecl vd = (GenericVarDecl)e.nextElement();
1104            
1105          if (!vd.id.toString().endsWith("@init")) {
1106            code.addElement(GC.assume(TrAnExpr.targetTypeCorrect(vd, loop.oldmap)));
1107          }
1108        }
1109        addNewAssumptionsNow(axs);
1110        for (int i = 0; i < loop.invariants.size(); i++) {
1111          Condition cond = loop.invariants.elementAt(i);
1112          code.addElement(GC.assume(cond.pred));
1113        }
1114    
1115        if (Main.options().traceInfo > 0) {
1116          String label = UniqName.locToSuffix(loop.getStartLoc());
1117          code.addElement(traceInfoLabelCmd(loop, "LoopIter"));
1118        }
1119    
1120        code.addElement(DynInstCmd.make(UniqName.locToSuffix(loop.getStartLoc()), S));
1121    
1122        checkLoopInvariants(loop,axs);
1123        code.addElement(GC.fail());
1124        GuardedCmd checkInvariantsAfterIteration = 
1125          GC.seq(GuardedCmdVec.popFromStackVector(code));
1126    
1127        loop.desugared = GC.choosecmd(checkInvariantsInitially,
1128                                      checkInvariantsAfterIteration);
1129      }
1130    
1131      /**
1132       * Add to "code" checks for all loop invariants of "loop".
1133       */
1134      private void checkLoopInvariants(/*@ non_null */ LoopCmd loop, ExprVec axs) {
1135        addNewAssumptionsNow(axs);
1136        for (int i = 0; i < loop.invariants.size(); i++) {
1137          Condition cond = loop.invariants.elementAt(i);
1138          addCheck(loop.locHotspot, cond);
1139        }
1140      }
1141    
1142      //@ requires Main.options().traceInfo > 0;
1143      private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast,
1144                                           /*@ non_null */ String traceInfoTag) {
1145        int sloc = ast.getStartLoc();
1146        int eloc = ast.getEndLoc();
1147        return traceInfoLabelCmd(sloc, eloc, traceInfoTag, sloc);
1148      }
1149    
1150      //@ requires Main.options().traceInfo > 0;
1151      //@ requires loc != Location.NULL;
1152      private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast,
1153                                           /*@ non_null */ String traceInfoTag,
1154                                           int loc) {
1155        return traceInfoLabelCmd(ast.getStartLoc(), ast.getEndLoc(),
1156                                 traceInfoTag, loc);
1157      }
1158    
1159      //@ requires Main.options().traceInfo > 0;
1160      //@ requires loc != Location.NULL;
1161      private GuardedCmd traceInfoLabelCmd(int sloc, int eloc,
1162                                           /*@ non_null */ String traceInfoTag,
1163                                           int loc) {
1164        return traceInfoLabelCmd(sloc, eloc, traceInfoTag,
1165                                 UniqName.locToSuffix(loc));
1166      }
1167    
1168        
1169      private GuardedCmd traceInfoLabelCmd(int sloc, int eloc,
1170                                           /*@ non_null */ String traceInfoTag,
1171                                           String sortSeq) {
1172        Assert.notFalse(Main.options().traceInfo > 0);
1173    
1174        String str = "trace." + traceInfoTag + "^" + sortSeq;
1175        Identifier id = Identifier.intern(str);
1176        Expr l = LabelExpr.make(sloc, eloc, true, id, GC.truelit);
1177        return GC.assume(l);
1178      }
1179    
1180      /**
1181       * This method returns a guarded command <code>G</code> that is like
1182       * <code>gc</code> except that where <code>gc</code> contains a mutable command,
1183       * <code>G</code> contains a fresh copy of that command.  Thus, the resulting
1184       * command is as good as a fresh copy of <code>gc</code>, since all other guarded
1185       * commands are to be read-only after construction.<p>
1186       *
1187       * There is only one mutable command, namely an "assume" command
1188       * of the form:
1189       * <pre>
1190       *     assume (lblpos id true)
1191       * </pre>
1192       * where "id" is a trace label.  A fresh copy of this command consists of a fresh
1193       * assume command with a fresh labeled expression.  However, the "id" reference
1194       * may be shared in the fresh command.
1195       */
1196      private GuardedCmd cloneGuardedCommand(/*@ non_null */ GuardedCmd gc) {
1197        switch (gc.getTag()) {
1198        case TagConstants.SKIPCMD:
1199        case TagConstants.RAISECMD:
1200        case TagConstants.ASSERTCMD:
1201        case TagConstants.GETSCMD:
1202        case TagConstants.SUBGETSCMD:
1203        case TagConstants.SUBSUBGETSCMD:
1204        case TagConstants.RESTOREFROMCMD:
1205          return gc;
1206    
1207        case TagConstants.ASSUMECMD: {
1208          ExprCmd ec = (ExprCmd)gc;
1209          if (ec.pred.getTag() == TagConstants.LABELEXPR) {
1210            LabelExpr le = (LabelExpr)ec.pred;
1211            if (le.positive && le.expr == GC.truelit) {
1212              String str = le.label.toString();
1213              if (ErrorMsg.isTraceLabel(str)) {
1214                return GC.assume(LabelExpr.make(le.sloc, le.eloc, true,
1215                                                le.label, GC.truelit));
1216              }
1217            }
1218          }
1219          return gc;
1220        }
1221    
1222        case TagConstants.VARINCMD: {
1223          VarInCmd vc = (VarInCmd)gc;
1224          GuardedCmd body = cloneGuardedCommand(vc.g);
1225          if (body != vc.g) {
1226            return GC.block(vc.v, body);
1227          }
1228          return gc;
1229        }
1230    
1231        case TagConstants.DYNINSTCMD: {
1232          DynInstCmd dc = (DynInstCmd)gc;
1233          GuardedCmd body = cloneGuardedCommand(dc.g);
1234          if (body != dc.g) {
1235            return DynInstCmd.make(dc.s, body);
1236          }
1237          return gc;
1238        }
1239    
1240        case TagConstants.SEQCMD: {
1241          SeqCmd sc = (SeqCmd)gc;
1242          int len = sc.cmds.size();
1243          GuardedCmd[] cmds = null;  // allocate this array lazily
1244          for (int i = 0; i < len; i++) {
1245            GuardedCmd c = sc.cmds.elementAt(i);
1246            GuardedCmd g = cloneGuardedCommand(c);
1247            if (g != c) {
1248              if (cmds == null) {
1249                cmds = new GuardedCmd[len];
1250                // all elements up until now have been the same
1251                for (int j = 0; j < i; j++) {
1252                  cmds[j] = sc.cmds.elementAt(j);
1253                }
1254              }
1255              cmds[i] = g;
1256            } else if (cmds != null) {
1257              cmds[i] = g;
1258            }
1259          }
1260          if (cmds != null) {
1261            return GC.seq(GuardedCmdVec.make(cmds));
1262          }
1263          return gc;
1264        }
1265    
1266        case TagConstants.CALL: {
1267          Call call = (Call)gc;
1268          GuardedCmd desugared = cloneGuardedCommand(call.desugared);
1269          if (desugared != call.desugared) {
1270            Call newCall = Call.make(call.args, call.scall, call.ecall,
1271                                     call.inlined);
1272            newCall.rd = call.rd;
1273            newCall.spec = call.spec;
1274            newCall.desugared = desugared;
1275            return newCall;
1276          }
1277          return gc;
1278        }
1279    
1280        case TagConstants.TRYCMD: {
1281          CmdCmdCmd tc = (CmdCmdCmd)gc;
1282          GuardedCmd g1 = cloneGuardedCommand(tc.g1);
1283          GuardedCmd g2 = cloneGuardedCommand(tc.g2);
1284          if (g1 != tc.g1 || g2 != tc.g2) {
1285            return GC.trycmd(g1, g2);
1286          }
1287          return gc;
1288        }
1289    
1290        case TagConstants.LOOPCMD: {
1291          LoopCmd lp = (LoopCmd)gc;
1292          GuardedCmd guard = cloneGuardedCommand(lp.guard);
1293          GuardedCmd body = cloneGuardedCommand(lp.body);
1294          LoopCmd newLoop = GC.loop(lp.locStart, lp.locEnd, lp.locHotspot, lp.oldmap,
1295                                    lp.invariants, lp.decreases,
1296                                    lp.skolemConstants, lp.predicates, lp.tempVars,
1297                                    guard, body);
1298          newLoop.desugared = cloneGuardedCommand(lp.desugared);
1299          // A desugared loop contains trace info labels, and thus:
1300          Assert.notFalse(newLoop.desugared != lp.desugared);
1301          return newLoop;
1302        }
1303    
1304        case TagConstants.CHOOSECMD: {
1305          CmdCmdCmd cc = (CmdCmdCmd)gc;
1306          GuardedCmd g1 = cloneGuardedCommand(cc.g1);
1307          GuardedCmd g2 = cloneGuardedCommand(cc.g2);
1308          if (g1 != cc.g1 || g2 != cc.g2) {
1309            return GC.choosecmd(g1, g2);
1310          }
1311          return gc;
1312        }
1313    
1314        default:
1315          //@ unreachable;
1316          Assert.notFalse(false);
1317          return null;
1318        }
1319      }
1320    
1321      /**
1322       * Pops <code>declaredLocals</code> and <code>code</code> and then appends
1323       * <code>code</code> with a VARINCMD (if there were any new declared locals) or a
1324       * sequence of commands (otherwise).  The new code becomes the body of the
1325       * VARINCMD or the sequence of commands.
1326       */
1327      private void wrapUpDeclBlock() {
1328        if (code.size() == 0) {
1329          declaredLocals.pop();
1330          code.pop();
1331        } else {
1332          if (declaredLocals.size() == 0) {
1333            declaredLocals.pop();
1334            code.merge();
1335          } else {
1336            code.addElement(popDeclBlock());
1337          }
1338        }
1339      }
1340    
1341      /**
1342       * Pops the code and declared local variables, makes these into a command
1343       * (usually a VAR .. IN .. END command, but possibly a sequence command if there
1344       * are no declared local variables).  The command is then returned.
1345       */
1346      private GuardedCmd popDeclBlock() {
1347        GuardedCmd body= GC.seq(GuardedCmdVec.popFromStackVector(code));
1348        // The following "if" statement seems to be a bug, because it
1349        // fails to pop "declaredLocals".  Better would be not to even
1350        // check the "if", but to always pop from the stack vector, and
1351        // then let "GC.block" do the optimization.  --KRML, 29 Sep 1999
1352        // Actually, popDeclBlock is not called with declaredLocals.size()==0
1353        if (declaredLocals.size() == 0)
1354          return body;
1355        GenericVarDeclVec locals
1356          = GenericVarDeclVec.popFromStackVector(declaredLocals);
1357        return GC.block(locals, body);
1358      }
1359      
1360      /**
1361       * Translate <code>stmt</code> into a sequence of guarded commands
1362       * that are appended to <code>code</code>.
1363       *
1364       * <p> Temporaries generated for expressions in <code>stmt</code>
1365       * are added to <code>temporaries</code>, loop invariant pragmas are
1366       * added to <code>loopinvariants</code>, decreases pragmas are added
1367       * to <code>loopDecreases</code>, loop predicates are added to
1368       * <code>looppredicates<code>, and local skolemized variables are
1369       * added to <code>skolemConstants</code>. </p>
1370       *
1371       * @param stmt the statement that is to be translated.
1372       */
1373      //@ assignable loopinvariants, loopDecreases, skolemConstants, loopPredicates;
1374      private void trStmt(/*@ non_null */ Stmt stmt, TypeDecl decl) {
1375        int tag = stmt.getTag();
1376        switch (tag) {
1377          
1378        case TagConstants.RETURNSTMT: 
1379          {
1380            ReturnStmt r = (ReturnStmt)stmt;
1381            if (r.expr != null)
1382              code.addElement(GC.gets(GC.resultvar, ptrExpr(r.expr)));
1383            if (Main.options().traceInfo > 0) {
1384              // add a label to track the return
1385              GuardedCmd g = traceInfoLabelCmd(r, "Return", r.loc); 
1386              code.addElement(g);
1387            }
1388            raise(GC.ec_return);
1389            return;
1390          }
1391          
1392        case TagConstants.THROWSTMT: 
1393          {
1394            ThrowStmt t = (ThrowStmt)stmt;
1395            code.addElement(GC.gets(GC.xresultvar, ptrExpr(t.expr)));
1396            nullCheck(t.expr, GC.xresultvar, t.getStartLoc());
1397            if (Main.options().traceInfo > 0) {
1398              // add a label to track the throw
1399              GuardedCmd g = traceInfoLabelCmd(t, "Throw", t.loc);
1400              code.addElement(g);
1401            }
1402            raise(GC.ec_throw);
1403            return;
1404          }
1405          
1406        case TagConstants.SWITCHSTMT: 
1407          {
1408            SwitchStmt c = (SwitchStmt)stmt;
1409            VariableAccess e = fresh(c.expr, c.expr.getStartLoc(), "switch");
1410            code.addElement( GC.gets( e, ptrExpr( c.expr )));
1411    
1412            // we walk thru the switch body, building up the GC
1413            // at each case label, we wrap up the GC generated so far
1414            // on the lhs of a box, and put the new assume on the rhs.
1415            
1416            code.push();
1417            code.addElement(GC.assume(GC.falselit));
1418            
1419            for(int i=0; i<c.stmts.size(); i++) {
1420              Stmt s = c.stmts.elementAt(i);
1421    
1422              if( s.getTag() != TagConstants.SWITCHLABEL ) {
1423                // just a regular statement
1424                trStmt( s , decl);
1425              } else {
1426                
1427                SwitchLabel sl = (SwitchLabel)s;
1428                
1429                GuardedCmdVec vec = GuardedCmdVec.popFromStackVector(code);
1430                GuardedCmd boxLhs = GC.block(GenericVarDeclVec.make(),
1431                                             GC.seq(vec));
1432    
1433                Expr C;
1434                if( sl.expr != null ) {
1435    
1436                  C = GC.nary(s.getStartLoc(),s.getEndLoc(),
1437                              TagConstants.INTEGRALEQ,
1438                              e, TrAnExpr.trSpecExpr(sl.expr));  // FIXME -why a trSpecExpr?
1439                } else {
1440    
1441                  C = GC.truelit;
1442                  for(int j=0; j<c.stmts.size(); j++) {
1443    
1444                    Stmt s2 = c.stmts.elementAt(j);
1445                    if( s2.getTag() == TagConstants.SWITCHLABEL ) {
1446    
1447                      SwitchLabel sl2 = (SwitchLabel)s2;
1448    
1449                      if( sl2.expr != null )
1450                        C = GC.and(s.getStartLoc(),s.getEndLoc(),
1451                                   C,
1452                                   GC.nary(s.getStartLoc(),s.getEndLoc(),
1453                                           TagConstants.INTEGRALNE,
1454                                           e, TrAnExpr.trSpecExpr(sl2.expr)));  // FIXME - why a specExpr
1455                    }
1456                  }
1457                }
1458                
1459                GuardedCmd boxRhs = GC.assume(C);
1460                if (Main.options().traceInfo > 0) {
1461                  // add a label to track the switch branch taken
1462                  GuardedCmd g = traceInfoLabelCmd(s, "Switch");
1463                  boxRhs = GC.seq(g, boxRhs);
1464                }  
1465                GuardedCmd box = GC.choosecmd(boxLhs, boxRhs);
1466                
1467                code.push();
1468                code.addElement(box);
1469                
1470              }
1471            }
1472            
1473            GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
1474            GuardedCmd block = GC.blockL(c, body);
1475            code.addElement(block);
1476    
1477            return;
1478          }
1479          
1480        case TagConstants.BLOCKSTMT: 
1481          {
1482            GenericBlockStmt b = (GenericBlockStmt)stmt;
1483            declaredLocals.push();  // this mark popped by "wrapUpDeclBlock"
1484            code.push();            // this mark popped by "wrapUpDeclBlock"
1485    
1486            for (int i= 0; i < b.stmts.size(); i++)
1487              trStmt(b.stmts.elementAt(i),decl);
1488    
1489            wrapUpDeclBlock();
1490            return;
1491          }
1492    
1493        case TagConstants.WHILESTMT: 
1494          {
1495            WhileStmt w = (WhileStmt)stmt;
1496            Expr bLabel = breakLabel(w);
1497    
1498            temporaries.push();  // this mark popped below
1499    
1500            code.push();  // this mark popped below
1501            guard(w.expr, bLabel);
1502            GuardedCmd guardCmd =
1503              GC.seq(GuardedCmdVec.popFromStackVector(code));
1504    
1505            ExprStmtPragmaVec invariants = loopinvariants;
1506            loopinvariants = ExprStmtPragmaVec.make();
1507            ExprStmtPragmaVec decreases = loopDecreases;
1508            loopDecreases = ExprStmtPragmaVec.make();
1509            ExprStmtPragmaVec predicates = loopPredicates;
1510            loopPredicates = ExprStmtPragmaVec.make();
1511            LocalVarDeclVec skolemConsts = skolemConstants;
1512            skolemConstants = LocalVarDeclVec.make();
1513    
1514            code.push();  // this mark popped by "opBlockCmd"
1515            trStmt(w.stmt,decl);
1516            GuardedCmd bodyCmd = opBlockCmd(continueLabel(w));
1517    
1518            makeLoop(w.getStartLoc(), w.getEndLoc(), w.locGuardOpenParen,
1519                     GenericVarDeclVec.popFromStackVector(temporaries),
1520                     guardCmd, bodyCmd, invariants, decreases,
1521                     skolemConsts, predicates, bLabel);
1522              
1523            return;
1524          }
1525          
1526        case TagConstants.DOSTMT: 
1527          {
1528            DoStmt d = (DoStmt)stmt;
1529            Expr bLabel = breakLabel(d);
1530    
1531            // the following 3 marks are popped below
1532            temporaries.push();
1533            code.push();
1534    
1535            ExprStmtPragmaVec invariants = loopinvariants;
1536            loopinvariants = ExprStmtPragmaVec.make();
1537            ExprStmtPragmaVec decreases = loopDecreases;
1538            loopDecreases = ExprStmtPragmaVec.make();
1539            ExprStmtPragmaVec predicates = loopPredicates;
1540            loopPredicates = ExprStmtPragmaVec.make();
1541            LocalVarDeclVec skolemConsts = skolemConstants;
1542            skolemConstants = LocalVarDeclVec.make();
1543    
1544            code.push(); // this mark popped by "opBlockCmd"
1545            trStmt(d.stmt,decl);
1546            code.addElement(opBlockCmd(continueLabel(d)));
1547    
1548            guard(d.expr, bLabel);
1549    
1550            GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code));
1551    
1552            makeLoop(d.getStartLoc(), d.getEndLoc(), d.loc,
1553                     GenericVarDeclVec.popFromStackVector(temporaries),
1554                     GC.skip(), body, invariants, decreases,
1555                     skolemConsts, predicates, bLabel);
1556            return;
1557          }
1558          
1559        case TagConstants.FORSTMT: 
1560          {
1561            ForStmt x = (ForStmt)stmt;
1562    
1563            declaredLocals.push();  // this mark popped by "wrapUpDeclBlock"
1564            code.push();            // this mark popped by "wrapUpDeclBlock"
1565              
1566            // initializers
1567            for (int i= 0; i < x.forInit.size(); i++)
1568              trStmt(x.forInit.elementAt(i),decl);
1569    
1570            Expr bLabel = breakLabel(x);
1571    
1572            temporaries.push();  // this mark popped below
1573    
1574            ExprStmtPragmaVec invariants = loopinvariants;
1575            loopinvariants = ExprStmtPragmaVec.make();
1576            ExprStmtPragmaVec decreases = loopDecreases;
1577            loopDecreases = ExprStmtPragmaVec.make();
1578            ExprStmtPragmaVec predicates = loopPredicates;
1579            loopPredicates = ExprStmtPragmaVec.make();
1580            LocalVarDeclVec skolemConsts = skolemConstants;
1581            skolemConstants = LocalVarDeclVec.make();
1582    
1583            code.push();  // this mark popped below
1584            guard(x.test, bLabel);
1585            GuardedCmd guardCmd =
1586              GC.seq(GuardedCmdVec.popFromStackVector(code));
1587    
1588            code.push(); // this mark popped below
1589    
1590            code.push(); // this mark popped by "opBlockCmd"
1591            trStmt(x.body,decl);
1592            code.addElement(opBlockCmd(continueLabel(x)));
1593    
1594            for(int i=0; i < x.forUpdate.size(); i++)
1595              ptrExpr(x.forUpdate.elementAt(i));
1596    
1597            GuardedCmd bodyCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
1598    
1599            makeLoop(x.getStartLoc(), x.getEndLoc(), x.locFirstSemi,
1600                     GenericVarDeclVec.popFromStackVector(temporaries),
1601                     guardCmd, bodyCmd, invariants, decreases,
1602                     skolemConsts, predicates, bLabel);
1603    
1604            wrapUpDeclBlock();
1605            return;
1606          }
1607    
1608        case TagConstants.IFSTMT: 
1609          {
1610            IfStmt i = (IfStmt)stmt;
1611            trIfStmt(i.expr, i.thn, i.els, decl);
1612            return;
1613          }
1614          
1615        case TagConstants.BREAKSTMT: 
1616          {
1617            BreakStmt b = (BreakStmt)stmt;
1618            Stmt label = TypeCheck.inst.getBranchLabel(b);
1619            if (Main.options().traceInfo > 0) {
1620              // add a label to track the break
1621              GuardedCmd g = traceInfoLabelCmd(b, "Break", b.loc);
1622              code.addElement(g);
1623            }  
1624            raise(breakLabel(label));
1625            return;
1626          }
1627          
1628        case TagConstants.CONTINUESTMT: 
1629          { 
1630            ContinueStmt c = (ContinueStmt)stmt;
1631            Stmt label = TypeCheck.inst.getBranchLabel(c);
1632            if (Main.options().traceInfo > 0) {
1633              // add a label to track the continue
1634              GuardedCmd g = traceInfoLabelCmd(c, "Continue", c.loc);
1635              code.addElement(g);
1636            }  
1637            raise(continueLabel(label));
1638            return;
1639          }
1640          
1641        case TagConstants.SYNCHRONIZESTMT: 
1642          {
1643            SynchronizeStmt x = (SynchronizeStmt)stmt;
1644            int xStart = x.getStartLoc();
1645            int xEnd = x.getEndLoc();
1646            VariableAccess mu = fresh(x.expr, x.expr.getStartLoc(),
1647                                      "synchronized");
1648            Expr e = ptrExpr(x.expr);
1649            code.addElement(GC.gets(mu,e));
1650    
1651            nullCheck(x.expr, mu, x.locOpenParen);
1652    
1653            trSynchronizedBody(mu, x.stmt, x.locOpenParen, decl);
1654            return;
1655          }
1656    
1657          
1658        case TagConstants.EVALSTMT: 
1659          {
1660            EvalStmt x = (EvalStmt)stmt;
1661            ptrExpr(x.expr);
1662            return;
1663          }
1664          
1665        case TagConstants.LABELSTMT: 
1666          {
1667            LabelStmt x = (LabelStmt)stmt;
1668            code.push(); // this mark popped by "opBlockCmd"
1669            trStmt(x.stmt,decl);
1670            code.addElement(opBlockCmd(breakLabel(x.stmt)));
1671            return;
1672          }
1673          
1674        case TagConstants.SKIPSTMT: 
1675          return;
1676    
1677        case TagConstants.TRYFINALLYSTMT: 
1678          {
1679            TryFinallyStmt x = (TryFinallyStmt)stmt;
1680            int xStart = x.getStartLoc();
1681            int xEnd = x.getEndLoc();
1682            GuardedCmd temp;
1683    
1684            code.push();
1685            trStmt(x.tryClause,decl);
1686            GuardedCmd c0 = GC.seq(GuardedCmdVec.popFromStackVector(code));
1687    
1688            code.push();
1689            VariableAccess ecSave = adorn(GC.ecvar);
1690            VariableAccess resultSave = adorn(GC.resultvar);
1691            VariableAccess xresultSave = adorn(GC.xresultvar); 
1692    
1693            if (Main.options().traceInfo > 0) {
1694              // add a label to track that the finally clause is entered because
1695              // an exception was raised
1696              GuardedCmd g = traceInfoLabelCmd(x, "FinallyBegin", x.locFinally);
1697              code.addElement(g);
1698            }
1699            code.addElement(GC.assume(GC.nary(xStart,xEnd,
1700                                              TagConstants.ANYEQ,
1701                                              GC.ecvar, ecSave)));
1702            code.addElement(GC.assume(GC.nary(xStart,xEnd,
1703                                              TagConstants.REFEQ,
1704                                              GC.resultvar, resultSave)));
1705            code.addElement(GC.assume(GC.nary(xStart,xEnd,
1706                                              TagConstants.REFEQ,
1707                                              GC.xresultvar, xresultSave)));
1708    
1709            code.push();
1710            trStmt(x.finallyClause,decl);
1711            temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#n",
1712                                   GC.seq(GuardedCmdVec.popFromStackVector(code)));
1713            code.addElement(temp);
1714    
1715            code.addElement(GC.gets(GC.ecvar, ecSave));
1716            code.addElement(GC.gets(GC.resultvar, resultSave));
1717            code.addElement(GC.gets(GC.xresultvar, xresultSave));
1718            if (Main.options().traceInfo > 0) {
1719              // add a label to track that the finally clause is exited when it
1720              // was entered due to that an exception was raised
1721              GuardedCmd g = traceInfoLabelCmd(x, "FinallyEnd", x.getEndLoc());
1722              code.addElement(g);
1723            }
1724            code.addElement(GC.raise());
1725    
1726            GuardedCmd c1 = GC.seq(GuardedCmdVec.popFromStackVector(code));
1727    
1728            code.addElement(GC.trycmd(c0,c1));
1729    
1730            code.push();
1731            trStmt(x.finallyClause,decl);
1732            temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#x",
1733                                   GC.seq(GuardedCmdVec.popFromStackVector(code)));
1734            code.addElement(temp);
1735    
1736            return;
1737          }
1738          
1739        case TagConstants.TRYCATCHSTMT: 
1740          {
1741            TryCatchStmt x = (TryCatchStmt)stmt;
1742            int xStart = x.getStartLoc();
1743            int xEnd = x.getEndLoc();
1744    
1745            code.push();
1746            trStmt(x.tryClause,decl);
1747            GuardedCmd tryGC = GC.seq(GuardedCmdVec.popFromStackVector(code));
1748    
1749            GuardedCmd els = GC.raise();
1750    
1751            for(int i=x.catchClauses.size()-1; i>=0; i--) {
1752              CatchClause cc = (CatchClause)x.catchClauses.elementAt(i);
1753              int ccStart=cc.getStartLoc();
1754              int ccEnd=cc.getEndLoc();
1755    
1756              // tst is typeof(XRES) <: Ti
1757              Expr tst = GC.nary(ccStart,ccEnd,
1758                                 TagConstants.TYPELE,
1759                                 GC.nary(ccStart,ccEnd,
1760                                         TagConstants.TYPEOF,
1761                                         GC.xresultvar),
1762                                 TypeExpr.make(ccStart,ccEnd,
1763                                               cc.arg.type));
1764    
1765              if( i==0 ) {
1766                // extend tst with a disjunct XRES==null
1767                tst = GC.or(ccStart,ccEnd,
1768                            tst,
1769                            GC.nary(ccStart,ccEnd,
1770                                    TagConstants.REFEQ,
1771                                    GC.xresultvar,
1772                                    GC.nulllit));
1773              }
1774                                      
1775    
1776              code.push();
1777              declaredLocals.addElement(cc.arg);
1778              VariableAccess arg = VariableAccess.make( cc.arg.id, ccStart,
1779                                                        cc.arg );
1780              
1781              code.addElement(GC.assume(GC.nary(ccStart,ccEnd,
1782                                                TagConstants.ANYEQ,
1783                                                arg,
1784                                                GC.xresultvar)));
1785              trStmt(cc.body,decl);
1786              GuardedCmd thn = GC.seq(GuardedCmdVec.popFromStackVector(code));
1787    
1788              els = GC.ifcmd(tst, thn, els);
1789            }
1790    
1791            
1792            GuardedCmd handler =
1793              GC.ifcmd( GC.nary(xStart,xEnd,
1794                                TagConstants.ANYNE,
1795                                GC.ecvar,
1796                                GC.ec_throw),
1797                        GC.raise(),
1798                        els );
1799    
1800            code.addElement(GC.trycmd(tryGC,handler));
1801    
1802            return;
1803          }
1804          
1805        case TagConstants.VARDECLSTMT: 
1806          {
1807            LocalVarDecl vd = ((VarDeclStmt)stmt).decl;
1808            declaredLocals.addElement(vd);
1809            boolean isUninitialized = false;
1810            boolean isGhost = false;
1811            if (vd.pmodifiers != null) {
1812              isGhost = Utils.findModifierPragma(vd.pmodifiers,TagConstants.GHOST) != null;
1813              for (int i= 0; i < vd.pmodifiers.size(); i++) {
1814                ModifierPragma prag= vd.pmodifiers.elementAt(i);
1815                if (prag.getTag() == TagConstants.UNINITIALIZED) {
1816                  VariableAccess init = initadorn(vd);
1817                  declaredLocals.addElement(init.decl);
1818                  setInitVar(vd, init);
1819                  isUninitialized = true;
1820                  break;  // don't look for any further UNINITIALIZED modifiers
1821                }
1822              }
1823            }
1824    
1825            if (null != vd.init) {
1826              Assert.notFalse(vd.locAssignOp != Location.NULL);
1827              VariableAccess lhs = TrAnExpr.makeVarAccess(vd, vd.getStartLoc());
1828              TrAnExpr.initForClause();
1829              Expr rval = isGhost ? 
1830                TrAnExpr.trSpecExpr((Expr)vd.init,null,premapWithArgs) :
1831                ptrExpr(vd.init);
1832              if (TrAnExpr.extraSpecs) addNewAssumptions();
1833              if (! isUninitialized) {
1834                writeCheck(lhs, vd.init, rval, vd.locAssignOp, false);
1835              }
1836              code.addElement(GC.gets(lhs, rval));
1837            }
1838            return;
1839          }
1840          
1841        case TagConstants.CONSTRUCTORINVOCATION:
1842          //@ unreachable;
1843          // If the following assert breaks, there's something wrong in
1844          // "trBody" where the constructor call is split up from the rest of
1845          // the constructor body.
1846          Assert.fail("constructor invocation handled in TrConstructorCallStmt");
1847          return;
1848    
1849        case TagConstants.UNREACHABLE:
1850          addCheck(stmt, TagConstants.CHKCODEREACHABILITY, GC.falselit);
1851          return;
1852    
1853        case TagConstants.SETSTMTPRAGMA: {
1854          SetStmtPragma s = (SetStmtPragma)stmt;
1855    
1856          if (s.target instanceof FieldAccess) {
1857            FieldAccess fa = (FieldAccess)s.target;
1858            TrAnExpr.initForClause();
1859            Expr lhs= trFieldAccess(true, fa); // FIXME - premap?
1860            Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1861            if (TrAnExpr.extraSpecs) addNewAssumptions();
1862            // Add check that the lhs is allowed to be written (writable pragma)
1863            writeCheck(lhs, s.value, rval, s.locOp, false);
1864            // Add checks that the lhs is allowed to be assigned (assignable pragma)
1865            frameHandler.modifiesCheckField(lhs,fa.getStartLoc(),fa.decl);
1866            String name;
1867            if (lhs.getTag() == TagConstants.VARIABLEACCESS) {
1868              VariableAccess valhs = (VariableAccess)lhs;
1869              name = valhs.decl.id.toString();
1870              code.addElement(GC.gets(valhs, rval));
1871              if (Modifiers.isStatic(valhs.decl.modifiers)) {
1872                code.addElement(modify(GC.statevar,s.getStartLoc()));
1873              }
1874            } else {
1875              // Instance field
1876              NaryExpr target = (NaryExpr)lhs;
1877              VariableAccess field = (VariableAccess)target.exprs.elementAt(0);
1878              name = field.decl.id.toString();
1879              Expr obj = target.exprs.elementAt(1);
1880              code.addElement(GC.subgets(field, obj,rval));
1881              code.addElement(modify(GC.statevar,s.getStartLoc()));
1882            }
1883            return;
1884            /*
1885              This was originally here.  The if block just above was inserted to
1886              make the correspondence with assignment complete.
1887              Not sure if the protect expressions belong ??? FIXME
1888    
1889              VariableAccess field = VariableAccess.make(fa.id, fa.locId, fa.decl);
1890              if (Modifiers.isStatic(fa.decl.modifiers)) {
1891              code.addElement(GC.gets( field,
1892              TrAnExpr.trSpecExpr(s.value)));
1893              } else {
1894              Expr obj = ((ExprObjectDesignator)fa.od).expr;
1895              code.addElement(GC.subgets( field,
1896              TrAnExpr.trSpecExpr(obj),
1897              TrAnExpr.trSpecExpr(s.value) ));
1898              }
1899            */
1900    
1901          } else if (s.target instanceof VariableAccess) {
1902            // Assignments to local ghost variables end here
1903            VariableAccess lhs = (VariableAccess)s.target;
1904            TrAnExpr.initForClause();
1905            Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1906            if (TrAnExpr.extraSpecs) addNewAssumptions();
1907            writeCheck(lhs, s.value, rval, s.locOp, false);
1908            code.addElement(GC.gets(lhs,rval));
1909            // A local variable is not part of an assignable frame so there is no
1910            // assignable clause to check
1911            VariableAccess init = getInitVar(lhs.decl);
1912            if (init != null) 
1913              code.addElement(GC.gets(init, GC.truelit));
1914            return;
1915          } else if (s.target instanceof ArrayRefExpr) {
1916            ArrayRefExpr lhs= (ArrayRefExpr)s.target;
1917    
1918            TrAnExpr.initForClause();
1919            Expr array= TrAnExpr.trSpecExpr(lhs.array,null,premapWithArgs);
1920            Expr index= TrAnExpr.trSpecExpr(lhs.index,null,premapWithArgs);
1921            Expr rval= TrAnExpr.trSpecExpr(s.value,null,premapWithArgs);
1922            if (TrAnExpr.extraSpecs) addNewAssumptions();
1923            // Add a check that the value of the array index is in bounds
1924            arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
1925            // Add a check that the assignment to an array element is allowed
1926            // by the assignable clauses
1927            frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
1928            if (! isFinal(TypeCheck.inst.getType(lhs.array))) {
1929              addCheck(s.loc,
1930                       TagConstants.CHKARRAYSTORE,
1931                       GC.nary(TagConstants.IS, rval,
1932                               GC.nary(TagConstants.ELEMTYPE,
1933                                       GC.nary(TagConstants.TYPEOF, array))),
1934                       Location.NULL, lhs.array);
1935            }
1936    
1937            code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
1938            code.addElement(modify(GC.statevar,lhs.getStartLoc()));
1939            Expr a= GC.select(GC.elemsvar, array);
1940            return;
1941                
1942          } else {
1943    
1944            ErrorSet.fatal(s.getStartLoc(),
1945                           "Unknown construct to translate");
1946          }
1947          break;
1948        }
1949    
1950        case TagConstants.HENCE_BY:
1951          // FIXME - ignored - unclear semantics
1952          return;
1953    
1954        case TagConstants.ASSUME:
1955          {
1956            ExprStmtPragma x = (ExprStmtPragma)stmt;
1957            TrAnExpr.initForClause();
1958            Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs);
1959            if (TrAnExpr.extraSpecs) addNewAssumptionsNow();
1960            code.addElement(GC.assume(p));
1961            return;
1962          }
1963    
1964        case TagConstants.ASSERT: {
1965          ExprStmtPragma x = (ExprStmtPragma)stmt;
1966          TrAnExpr.initForClause();
1967          Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs);
1968          if (TrAnExpr.extraSpecs) addNewAssumptionsNow();
1969          code.addElement(GC.check(x.getStartLoc(), TagConstants.CHKASSERT,
1970                                   p, Location.NULL));
1971          return;
1972        }
1973    
1974        case TagConstants.LOOP_INVARIANT:
1975        case TagConstants.MAINTAINING:
1976          {
1977            ExprStmtPragma x = (ExprStmtPragma)stmt;
1978            loopinvariants.addElement(x);
1979            return;
1980          }
1981    
1982        case TagConstants.DECREASES:
1983        case TagConstants.DECREASING:
1984          {
1985            ExprStmtPragma x = (ExprStmtPragma)stmt;
1986            loopDecreases.addElement(x);
1987            return;
1988          }
1989    
1990        case TagConstants.LOOP_PREDICATE:
1991          {
1992            ExprStmtPragma x = (ExprStmtPragma)stmt;
1993            loopPredicates.addElement(x);
1994            return;
1995          }
1996    
1997        case TagConstants.SKOLEMCONSTANTPRAGMA:
1998          {
1999            SkolemConstantPragma p = (SkolemConstantPragma)stmt;
2000            skolemConstants.append(p.decls);
2001            break;
2002          }
2003    
2004        case TagConstants.CLASSDECLSTMT: 
2005          if (this.issueCautions && !escjava.Main.options().noNotCheckedWarnings) {
2006            ErrorSet.caution(stmt.getStartLoc(),
2007                             "Not checking block-level types");
2008          }   
2009          return;
2010    
2011        case TagConstants.ASSERTSTMT: {
2012          // Only process if we are supposed to be parsing Java
2013          // 1.4 or later and assertions are enabled.
2014          AssertStmt assertStmt = (AssertStmt)stmt;
2015          if (!Tool.options.assertIsKeyword || !Tool.options.assertionsEnabled) {
2016            // continue - simply skip the assertions
2017          } else if (Main.options().assertionMode ==
2018                     Options.JML_ASSERTIONS) {
2019            // Treat a Java assert as a JML assert
2020            // Since it is a Java statement, it can't contain JML constructs
2021            // FIXME - so should it be translated this way?
2022            Expr predicate = TrAnExpr.trSpecExpr(assertStmt.pred);
2023            code.addElement(GC.check(assertStmt.getStartLoc(), TagConstants.CHKASSERT,
2024                                     predicate, Location.NULL));
2025          } else if (Main.options().assertionMode ==
2026                     Options.JAVA_ASSERTIONS) {
2027            // Treat a Java assert as a (conditional) throw
2028            trIfStmt(assertStmt.ifStmt.expr, assertStmt.ifStmt.thn, assertStmt.ifStmt.els,decl);
2029          }
2030          return;
2031        }
2032        default:
2033          //@ unreachable;
2034          Assert.notFalse(false,"Unexpected tag " + TagConstants.toString(tag)
2035                          + " " + stmt + " " +
2036                          Location.toString(stmt.getStartLoc()));
2037          return;
2038        }
2039      }
2040    
2041      /**
2042       * Translate an "if" statement.
2043       *
2044       * @design This method was refactored out to handle Java's "assert" keyword as
2045       * well as normal "if" statements.
2046       */
2047      private void trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl) {
2048        Expr guardExpr = ptrExpr(guard);
2049            
2050        code.push();
2051        if (Main.options().traceInfo > 0) {
2052          // add a label to track the if branch taken
2053          GuardedCmd g = traceInfoLabelCmd(thenStmt, "Then");
2054          code.addElement(g);
2055        }  
2056        trStmt(thenStmt,decl);
2057        GuardedCmd thenGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
2058            
2059        code.push();          
2060        if (Main.options().traceInfo > 0) {
2061          // add a label to track the if branch taken
2062          GuardedCmd g = traceInfoLabelCmd(elseStmt, "Else");
2063          code.addElement(g);
2064        }  
2065        trStmt(elseStmt,decl);
2066        GuardedCmd elseGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code));
2067            
2068        code.addElement(GC.ifcmd(guardExpr, thenGuardedCmd, elseGuardedCmd));
2069        return;
2070      }
2071    
2072      //@ requires loc != Location.NULL;
2073      private void trSynchronizedBody(/*@ non_null */ Expr mu,
2074                                      /*@ non_null */ Stmt stmt, int loc, TypeDecl decl) {
2075        // check LockingOrderViolation: mutexLE(max(LS),mu) || LS[mu]
2076        addCheck(loc,
2077                 TagConstants.CHKLOCKINGORDER,
2078                 GC.or(GC.nary(TagConstants.LOCKLE,
2079                               GC.nary(TagConstants.MAX, GC.LSvar),
2080                               mu),
2081                       GC.nary(TagConstants.SELECT, GC.LSvar, mu)));
2082    
2083        VariableAccess newLS = adorn(GC.LSvar);
2084    
2085        // e1 is ( lockLE(max(LS),mu) && mu == max(newLS) )
2086        Expr e1 = GC.and(
2087                         // lockLE(max(LS),mu)
2088                         GC.nary(TagConstants.LOCKLE,
2089                                 GC.nary(TagConstants.MAX, GC.LSvar),
2090                                 mu),
2091                         // mu == max(newLS)
2092                         GC.nary(TagConstants.REFEQ,
2093                                 mu,
2094                                 GC.nary(TagConstants.MAX, newLS)));
2095    
2096        // e2 is ( LS[mu] && newLS == LS )
2097        Expr e2 = GC.and(
2098                         // LS[mu]
2099                         GC.select(GC.LSvar, mu ),
2100                         // newLS == LS
2101                         GC.nary(TagConstants.REFEQ, newLS, GC.LSvar));
2102    
2103        // assume (e1 || e2)
2104        code.addElement(GC.assume(GC.or(e1, e2)));
2105    
2106        // assume newLS == store(LS,mu,boolTrue)
2107        code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ?
2108                                          newLS,
2109                                          GC.nary(TagConstants.STORE,
2110                                                  GC.LSvar, mu, GC.truelit))));
2111    
2112        // assume newLS == asLockSet(newLS)
2113        code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ?
2114                                          newLS,
2115                                          GC.nary(TagConstants.ASLOCKSET,
2116                                                  newLS))));
2117    
2118        // Translate the body, using the new LS
2119        VariableAccess oldLS = GC.LSvar;
2120        GC.LSvar = newLS;
2121        trStmt(stmt,decl);
2122        GC.LSvar = oldLS;
2123      }
2124    
2125      /**
2126       * This method implements "TrConstructorCallStmt" as described in section 6 of
2127       * ESCJ 16.
2128       */
2129      private void trConstructorCallStmt(/*@ non_null */ ConstructorInvocation ci) {
2130        // Check if this is a constructor for an inner class; if so, we need to pass
2131        // an enclosing instance as the first argument.
2132        TypeSig resultType = TypeSig.getSig(ci.decl.parent);
2133        boolean inner = !resultType.isTopLevelType();
2134    
2135        // translate arguments
2136        int argsSize = ci.args.size() + (inner ? 1 : 0);
2137        ExprVec rawArgs = ci.args.copy();
2138        ExprVec args = ExprVec.make(argsSize);
2139    
2140        if (inner) {
2141          Expr rawExpr = ci.enclosingInstance;
2142          Assert.notNull(rawExpr);
2143          rawArgs.insertElementAt(rawExpr, 0);
2144    
2145          Purity.decorate(rawExpr);
2146          Expr arg = trExpr(true, rawExpr);
2147          args.addElement(arg);
2148    
2149          // do nullCheck here rather than non-null check in call(...):
2150          nullCheck(rawExpr, arg, ci.locDot);
2151        }
2152        for (int i = 0; i < ci.args.size(); i++) {
2153          Expr rawExpr = ci.args.elementAt(i);
2154          Purity.decorate(rawExpr);
2155          // protect all but the last argument
2156          Expr arg = trExpr(i != ci.args.size()-1, rawExpr);
2157          args.addElement(arg);
2158        }
2159    
2160        InlineSettings is = (InlineSettings)inlineDecoration.get(ci);
2161        code.addElement(call(ci.decl, rawArgs, args, scope,
2162                             ci.getStartLoc(), ci.getEndLoc(), 
2163                             ci.locOpenParen, true, is, null, false));  // FIXME - set the eod=null to the right value
2164        // this = RES
2165        code.addElement(GC.gets(GC.thisvar, GC.resultvar));
2166    
2167        // FIXME - this is for a 'this' or 'super' call within a constructor - need to put in modifies checks
2168      }
2169    
2170      //// Expression translation
2171    
2172      /**
2173       * Extends the code array with a command that evaluates e and returns an
2174       * expession which denotes this value in the poststate of that command. If
2175       * <code>protect</code> is true, then the expression returned will depend only on
2176       * values of temporary variables (that is, the expression returned will not be
2177       * affected by changes to program variables).<p> If <code>protect</code> is
2178       * <code>true</code>, then the value returned is certain to be of type
2179       * <code>VariableAccess</code>.
2180       */
2181      //@ ensures protect ==> \result instanceof VariableAccess;
2182      private Expr protect(boolean protect, Expr e, int loc) {
2183        if (protect) {
2184          VariableAccess result = fresh(e, loc);
2185          code.addElement(GC.gets(result, e));
2186          return result;
2187        } else return e;
2188      }
2189    
2190      //@ ensures protect ==> \result instanceof VariableAccess;
2191      private Expr protect(boolean protect, Expr e, int loc, String suffix) {
2192        if (protect) {
2193          VariableAccess result = fresh(e, loc, suffix);
2194          code.addElement(GC.gets(result, e));
2195          return result;
2196        } else return e;
2197      }
2198    
2199      /** Purify and translate expr without protection */
2200      private Expr ptrExpr(VarInit expr) {
2201        Purity.decorate(expr);
2202        return trExpr(false, expr);
2203      }
2204    
2205      /**
2206       * Translate <code>expr</code> into a sequence of guarded commands that are
2207       * appended to <code>code</code> and return an expression denoting the value of
2208       * the expression.  New temporaries may be generated; these are added to
2209       * <code>temporaries</code>.
2210       *
2211       * @param protect if true, then the expression return will depend only on values
2212       * of temporary variables (that is, the expression returned will not be affected
2213       * by changes in program variables).
2214       */
2215      private Expr trExpr(boolean protect, /*@ non_null */ VarInit expr) {
2216        int tag = expr.getTag();
2217    
2218        switch (tag) {
2219        case TagConstants.ARRAYINIT: 
2220          {
2221            ArrayInit x = (ArrayInit)expr;
2222            int xStart = x.getStartLoc();
2223            int xEnd = x.getEndLoc();
2224            
2225            int len = x.elems.size();
2226            boolean isPure[] = new boolean[len];
2227            Expr[] elems     = new Expr[len];
2228    
2229            // set isPure[i] to true if {E_{i+1},...,E_n} are all pure
2230            if( len != 0 ) isPure[len-1] = true;
2231            for(int i=len-2; i>=0; i-- ) {
2232              isPure[i] = isPure[i+1] && !Purity.impure(x.elems.elementAt(i+1));
2233            }
2234    
2235            for(int i=0; i<len; i++ )
2236              elems[i] = trExpr(isPure[i], x.elems.elementAt(i));
2237    
2238            // Construct variables
2239            VariableAccess a = fresh(x, xStart, "arrayinit");
2240            VariableAccess newallocvar = adorn(GC.allocvar);
2241    
2242            // assume !isAllocated(a, alloc);
2243            code.addElement(GC.assume(GC.not(xStart, xEnd,
2244                                             GC.nary(xStart, xEnd,
2245                                                     TagConstants.ISALLOCATED,
2246                                                     a, GC.allocvar))));
2247            // assume isAllocated(a, alloc');
2248            code.addElement(GC.assume(GC.nary(xStart, xEnd,
2249                                              TagConstants.ISALLOCATED,
2250                                              a,
2251                                              newallocvar )));
2252            // assume a != null;
2253            code.addElement(GC.assume(GC.nary(xStart, xEnd,
2254                                              TagConstants.REFNE,
2255                                              a,
2256                                              GC.nulllit )));
2257            // assume typeof(a) == array(T);
2258            Expr typeofa = GC.nary(xStart, xEnd,
2259                                   TagConstants.TYPEOF, a);
2260            Expr arrayT = TypeExpr.make(xStart, xEnd,
2261                                        TypeCheck.inst.getType(x));
2262    
2263            code.addElement(GC.assume(GC.nary(xStart, xEnd,
2264                                              TagConstants.TYPEEQ,
2265                                              typeofa, arrayT )));
2266    
2267            // assume arrayLength(a) == n
2268            code.addElement(GC.assume(GC.nary(xStart, xEnd,
2269                                              TagConstants.INTEGRALEQ,
2270                                              GC.nary(xStart, xEnd,
2271                                                      TagConstants.ARRAYLENGTH,
2272                                                      a),
2273                                              LiteralExpr.make(TagConstants.INTLIT,
2274                                                               new Integer(len),
2275                                                               xStart))));  
2276    
2277            // elems[a][i] = ei
2278            Expr elemsAta = GC.nary(xStart, xEnd,
2279                                    TagConstants.SELECT,
2280                                    GC.elemsvar, a);
2281            for(int i=0; i<len; i++ ) {
2282              Expr iLit =
2283                LiteralExpr.make(TagConstants.INTLIT, new Integer(i), xStart);
2284              Expr elemsAtaAti = GC.nary(xStart, xEnd,
2285                                         TagConstants.SELECT,
2286                                         elemsAta, iLit);
2287              code.addElement(GC.assume(GC.nary(xStart, xEnd,
2288                                                TagConstants.REFEQ,
2289                                                elemsAtaAti, elems[i] )));
2290            }
2291    
2292            // assume that everything allocated is an array
2293            code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar,
2294                                                           newallocvar)));
2295            // alloc = alloc'                                
2296            code.addElement(GC.gets(GC.allocvar, newallocvar));
2297    
2298            return a;
2299          }
2300                        
2301        case TagConstants.THISEXPR: {
2302          ThisExpr t = (ThisExpr)expr;
2303          if (t.classPrefix != null)
2304            return trExpr(protect, Inner.unfoldThis(t));
2305    
2306          // We ignore "protect" here, since "this" is (almost) never
2307          // assigned to.  (In the one case where "this" is assigned--
2308          // after the super-or-sibling constructor call in a
2309          // constructor--"protect" is not needed.
2310          return GC.thisvar;
2311        }
2312    
2313        case TagConstants.SETCOMPEXPR:
2314          ErrorSet.fatal(expr.getStartLoc(), "Set comprehension is not supported");
2315    
2316          // Literals
2317        case TagConstants.BOOLEANLIT: 
2318        case TagConstants.CHARLIT:
2319        case TagConstants.DOUBLELIT: 
2320        case TagConstants.FLOATLIT:
2321        case TagConstants.INTLIT:
2322        case TagConstants.LONGLIT:
2323        case TagConstants.NULLLIT:
2324          return (Expr)expr;
2325    
2326        case TagConstants.STRINGLIT:
2327          {
2328            String s = ((LiteralExpr)expr).value.toString();
2329            Expr result = GC.nary(
2330                                  TagConstants.INTERN,
2331                                  GC.symlit(Strings.intern(s).toString()),
2332                                  GC.symlit(Integer.toString(s.length())) );
2333    
2334            return result;
2335          }
2336    
2337        case TagConstants.ARRAYREFEXPR:
2338          {
2339            ArrayRefExpr x= (ArrayRefExpr)expr;
2340            Expr array= trExpr(Purity.impure(x.index), x.array);
2341            Expr index= trExpr(false, x.index);
2342    
2343            arrayAccessCheck(x.array, array, x.index, index, x.locOpenBracket);
2344    
2345            Expr a= GC.select(GC.elemsvar, array);
2346            return protect(protect, GC.select(a, index), x.locOpenBracket);
2347          }
2348    
2349        case TagConstants.NEWINSTANCEEXPR:
2350          { 
2351            NewInstanceExpr ni= (NewInstanceExpr)expr;
2352    
2353            ExprVec rawArgs = ni.args.copy();
2354            ExprVec args = ExprVec.make(ni.args.size());
2355    
2356            if (ni.anonDecl != null) {
2357              if (this.issueCautions && ! Main.options().noNotCheckedWarnings) {
2358                ErrorSet.caution(ni.anonDecl.loc,
2359                                 "Not checking body of anonymous class" +
2360                                 " (subclass of " +
2361                                 ni.type.name.printName() + ")");
2362              }
2363            }
2364    
2365            // translate enclosing instance argument if present:
2366            if (ni.enclosingInstance != null) {
2367              rawArgs.insertElementAt(ni.enclosingInstance, 0);
2368              Expr arg = trExpr(true, ni.enclosingInstance);
2369              args.addElement(arg);
2370    
2371              // do nullCheck here rather than non-null check in call(...):
2372              nullCheck(ni.enclosingInstance, arg, ni.locDot);
2373            }
2374    
2375            // translate normal arguments
2376            for (int i = 0; i < ni.args.size(); i++) {
2377              // protect all but the last argument
2378              Expr arg = trExpr(i != ni.args.size()-1, ni.args.elementAt(i));
2379              args.addElement(arg);
2380            }
2381    
2382            InlineSettings is = (InlineSettings)inlineDecoration.get(ni);
2383            code.addElement(call(ni.decl, rawArgs, args, scope,
2384                                 ni.loc, ni.getEndLoc(), ni.locOpenParen,
2385                                 false, is, temporary("RES", ni.loc, ni.loc),
2386                                 true));  
2387              
2388            {   Expr tType = TypeExpr.make(ni.loc, ni.getEndLoc(), ni.type);
2389            Expr resType = GC.nary(TagConstants.TYPEOF, GC.resultvar);
2390            if (ni.anonDecl != null) {
2391              //  assume typeof(RES) != T  (for anonymous new)
2392              code.addElement(GC.assume(GC.nary(TagConstants.TYPENE,
2393                                                resType,
2394                                                tType)));
2395            } else {
2396              // assume typeof(RES) == T  (for ordinary new)
2397              code.addElement(GC.assume(GC.nary(TagConstants.TYPEEQ,
2398                                                resType,
2399                                                tType)));
2400            }
2401            }
2402    
2403            ByteArrayOutputStream baos = new ByteArrayOutputStream();
2404            PrettyPrint.write(baos, "new!");
2405            PrettyPrint.inst.print(baos, ni.type);
2406            return protect(protect, GC.resultvar, ni.locOpenParen, baos.toString());
2407          }
2408    
2409        case TagConstants.NEWARRAYEXPR:
2410          {
2411            NewArrayExpr x= (NewArrayExpr)expr;
2412            int nd= x.dims.size();
2413    
2414            if (x.init != null) {
2415              return trExpr(true, x.init);
2416            }
2417    
2418            // Construct variables
2419            ByteArrayOutputStream baos = new ByteArrayOutputStream();
2420            PrettyPrint.write(baos, "new!");
2421            PrettyPrint.inst.print(baos, x.type);
2422            for (int i = 0; i < nd; i++) {
2423              PrettyPrint.write(baos, "[]");
2424            }
2425            VariableAccess result= fresh(x, x.loc, baos.toString());
2426            VariableAccess newallocvar= adorn(GC.allocvar);
2427    
2428            // Evaluate length in each dimension
2429            Expr[] dims= new Expr[nd];
2430            for (int i= 0; i < nd; i++) {
2431              boolean protectDim= false;
2432              for (int j= i+1; j < nd && ! protectDim; j++)
2433                protectDim= Purity.impure(x.dims.elementAt(j));
2434              dims[i]= trExpr(protectDim, x.dims.elementAt(i));
2435              // "nd" squared iterations, but nd should be small
2436            }
2437    
2438            // Check for negative array sizes
2439            for (int i= 0; i < nd; i++) {
2440              Expr nonneg= GC.nary(TagConstants.INTEGRALLE, GC.zerolit, dims[i]);
2441              Condition cond= GC.condition(TagConstants.CHKNEGATIVEARRAYSIZE,
2442                                           nonneg, Location.NULL);
2443              Expr je= x.dims.elementAt(i);
2444              code.addElement(GC.check(x.locOpenBrackets[i], cond,
2445                                       trim(x.dims.elementAt(i))));
2446            }
2447              
2448            // Construct call to arrayFresh
2449            Expr shape= GC.nary(TagConstants.ARRAYSHAPEONE, dims[nd-1]);
2450            Type type= ArrayType.make(x.type, Location.NULL);
2451            for (int i= nd-2; 0 <= i; i--) {
2452              shape= GC.nary(TagConstants.ARRAYSHAPEMORE, dims[i], shape);
2453              type= ArrayType.make(type, Location.NULL);
2454            }
2455            Expr[] arrayFreshArgs= {
2456              result, GC.allocvar, newallocvar, GC.elemsvar, shape,
2457              GC.typeExpr(type), GC.zeroequiv(x.type)
2458            };
2459            Expr arrayFresh= GC.nary(x.getStartLoc(), x.getEndLoc(),
2460                                     TagConstants.ARRAYFRESH,
2461                                     ExprVec.make(arrayFreshArgs));
2462    
2463            // Emit the Assume and a Gets commands
2464            code.addElement(GC.assume(arrayFresh));
2465            code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar,
2466                                                           newallocvar)));
2467            Expr ownerNull = predArrayOwnerNull(GC.allocvar, newallocvar, 
2468                                                result);
2469            if (ownerNull != null)
2470              code.addElement(GC.assume(ownerNull));
2471            code.addElement(GC.gets(GC.allocvar, newallocvar));
2472    
2473            // Return the variable containing the newly-allocated array
2474            return result;
2475          }
2476    
2477        case TagConstants.CONDEXPR:
2478          {
2479            CondExpr x= (CondExpr)expr;
2480            // ifCmd((tr(x.test), tr(x.thn), tr(x.els))
2481            Expr test= trExpr(false, x.test);
2482            VariableAccess result= fresh(x, x.locQuestion, "cond");
2483              
2484            code.push();
2485            if (Main.options().traceInfo > 0) {
2486              // add a label to track the if branch taken
2487              GuardedCmd g = traceInfoLabelCmd(x.thn, "Then");
2488              code.addElement(g);
2489            }  
2490            Expr thnP= trExpr(false, x.thn);
2491            code.addElement(GC.gets(result, thnP));
2492            GuardedCmd thenbody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2493              
2494            code.push();
2495            if (Main.options().traceInfo > 0) {
2496              // add a label to track the if branch taken
2497              GuardedCmd g = traceInfoLabelCmd(x.els, "Else");
2498              code.addElement(g);
2499            }  
2500            Expr elsP= trExpr(false, x.els);
2501            code.addElement(GC.gets(result, elsP));
2502            GuardedCmd elsebody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2503              
2504            code.addElement(GC.ifcmd(test, thenbody, elsebody));
2505            return result;
2506          }
2507    
2508        case TagConstants.INSTANCEOFEXPR:
2509          {
2510            InstanceOfExpr x= (InstanceOfExpr)expr;
2511            Expr obj = trExpr(protect, x.expr);
2512    
2513            Expr isOfType = GC.nary(x.getStartLoc(), x.getEndLoc(), 
2514                                    TagConstants.IS, obj,
2515                                    TypeExpr.make(x.type.getStartLoc(),
2516                                                  x.type.getEndLoc(),
2517                                                  x.type));
2518            Expr notNull = GC.nary(x.getStartLoc(), x.getEndLoc(), 
2519                                   TagConstants.REFNE, obj, GC.nulllit);
2520    
2521            return GC.and(x.getStartLoc(), x.getEndLoc(),
2522                          isOfType,
2523                          notNull);
2524          }
2525    
2526        case TagConstants.CASTEXPR:
2527          {
2528            CastExpr x= (CastExpr)expr;
2529            Expr result= trExpr(protect, x.expr);
2530            Expr te = GC.typeExpr(x.type);
2531            if (Types.isReferenceType(x.type)) {
2532              addCheck(expr,
2533                       TagConstants.CHKCLASSCAST,
2534                       GC.nary(TagConstants.IS, result, te));
2535            }
2536            result = GC.nary(TagConstants.CAST, result, te);
2537            return result;
2538          }
2539    
2540        case TagConstants.CLASSLITERAL:
2541          {
2542            ClassLiteral x= (ClassLiteral)expr;
2543            return GC.nary(x.getStartLoc(), x.getEndLoc(),
2544                           TagConstants.CLASSLITERALFUNC,
2545                           TypeExpr.make(x.type.getStartLoc(),
2546                                         x.type.getEndLoc(),
2547                                         x.type));
2548          }
2549    
2550          // Binary expressions
2551        case TagConstants.OR: case TagConstants.AND:
2552          {
2553            BinaryExpr x= (BinaryExpr)expr;
2554            VariableAccess result= fresh(x, x.locOp,
2555                                         (tag == TagConstants.OR ?
2556                                          "cor" : "cand"));
2557            Expr left= trExpr(false, x.left);
2558    
2559            // Create a chunk of code that evaluates the right expr and
2560            // saves its value in "result"
2561            code.push();
2562            Expr right= trExpr(false, x.right);
2563            code.addElement(GC.gets(result, right));
2564            GuardedCmd rightbody= GC.seq(GuardedCmdVec.popFromStackVector(code));
2565    
2566            GuardedCmd thn, els;
2567            if (tag == TagConstants.OR) {
2568              thn= GC.gets(result, GC.truelit);
2569              els= rightbody;
2570            } else {
2571              thn= rightbody;
2572              els= GC.gets(result, GC.falselit);
2573            }
2574            if (Main.options().traceInfo > 0) {
2575              // add labels to track which operands are evaluated
2576              GuardedCmd g = traceInfoLabelCmd(x, "FirstOpOnly", x.locOp);
2577              if (tag == TagConstants.OR) {
2578                thn = GC.seq(g, thn);
2579              }
2580              else {
2581                els = GC.seq(g, els);
2582              }
2583            }   
2584            code.addElement(GC.ifcmd(left, thn, els));
2585            return result;
2586          }
2587    
2588        case TagConstants.BITOR: case TagConstants.BITXOR:
2589        case TagConstants.BITAND: case TagConstants.NE:
2590        case TagConstants.EQ: case TagConstants.GE:
2591        case TagConstants.GT: case TagConstants.LE:
2592        case TagConstants.LT: case TagConstants.LSHIFT:
2593        case TagConstants.RSHIFT: case TagConstants.URSHIFT:
2594        case TagConstants.ADD: case TagConstants.SUB:
2595        case TagConstants.STAR:
2596        case TagConstants.DIV: case TagConstants.MOD:
2597          {
2598            BinaryExpr x= (BinaryExpr)expr;
2599            Expr left= trExpr(Purity.impure(x.right), x.left);
2600            Expr right= trExpr(false, x.right);
2601            if (tag == TagConstants.DIV || tag == TagConstants.MOD) {
2602              if (Types.isIntegralType(TypeCheck.inst.getType(x.right))) {
2603                addCheck(x.locOp, TagConstants.CHKARITHMETIC,
2604                         GC.nary(TagConstants.INTEGRALNE, right, GC.zerolit));
2605              }
2606            }
2607            int newtag= TrAnExpr.getGCTagForBinary(x);
2608            if (tag == TagConstants.GT || tag == TagConstants.GE ||
2609                tag == TagConstants.LT || tag == TagConstants.LE) {
2610              // Must be primitive types
2611              int leftTag = ((PrimitiveType)TypeCheck.inst.getType(x.left)).getTag();
2612              int rightTag = ((PrimitiveType)TypeCheck.inst.getType(x.right)).getTag();
2613              if (leftTag == rightTag) 
2614                ; // do nothing
2615              else if (leftTag == TagConstants.REALTYPE && rightTag != TagConstants.REALTYPE)
2616                right = GC.cast(right,Types.realType);
2617              else if (leftTag != TagConstants.REALTYPE && rightTag == TagConstants.REALTYPE)
2618                left = GC.cast(left,Types.realType);
2619              else if (leftTag == TagConstants.DOUBLETYPE && rightTag != TagConstants.DOUBLETYPE)
2620                right = GC.cast(right,Types.doubleType);
2621              else if (leftTag != TagConstants.DOUBLETYPE && rightTag == TagConstants.DOUBLETYPE)
2622                left = GC.cast(left,Types.doubleType);
2623              else if (leftTag == TagConstants.FLOATTYPE && rightTag != TagConstants.FLOATTYPE)
2624                right = GC.cast(right,Types.floatType);
2625              else if (leftTag != TagConstants.FLOATTYPE && rightTag == TagConstants.FLOATTYPE)
2626                left = GC.cast(left,Types.floatType);
2627                            
2628              // FIXME - other promotions ? Also in TrAnExpr.java
2629    
2630            }
2631            if (newtag == TagConstants.STRINGCAT) {
2632              return addNewString(x,left,right);
2633                    
2634            } else {
2635              return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(),
2636                                              newtag, left, right),
2637                             x.locOp);
2638            }
2639          }
2640    
2641        case TagConstants.ASSIGN:
2642          {
2643            BinaryExpr x= (BinaryExpr)expr;
2644            Expr right= x.right;
2645            Expr left= x.left;
2646    
2647            int ltag = left.getTag();
2648            if (ltag == TagConstants.VARIABLEACCESS) {
2649              VariableAccess lhs= (VariableAccess)left;
2650              Expr rval= trExpr(false, right);
2651              writeCheck(lhs, right, rval, x.locOp, false);
2652              code.addElement(GC.gets(lhs, rval));
2653              VariableAccess init= getInitVar(lhs.decl);
2654              if (init != null)
2655                code.addElement(GC.gets(init, GC.truelit));
2656              if (Modifiers.isStatic(lhs.decl.modifiers)) {
2657                code.addElement(modify(GC.statevar,x.getStartLoc()));
2658              }
2659              return protect(protect, left, x.locOp, lhs.decl.id.toString() + "=");
2660                
2661            } else if (ltag == TagConstants.FIELDACCESS) {
2662              Expr lhs= trFieldAccess(true, (FieldAccess)left);
2663              Expr rval= trExpr(false, right);
2664              String name;
2665              writeCheck(lhs, right, rval, x.locOp, false);
2666              // Add a check that the lhs field may be assigned (assignable clause)
2667              frameHandler.modifiesCheckField(lhs,lhs.getStartLoc(),
2668                                 ((FieldAccess)left).decl);
2669              if (lhs.getTag() == TagConstants.VARIABLEACCESS) {
2670                VariableAccess vaLhs = (VariableAccess)lhs;
2671                name = vaLhs.decl.id.toString();
2672                code.addElement(GC.gets(vaLhs, rval));
2673              } else {
2674                NaryExpr target= (NaryExpr)lhs;
2675                VariableAccess field= (VariableAccess)target.exprs.elementAt(0);
2676                name = field.decl.id.toString();
2677                Expr obj= target.exprs.elementAt(1);
2678                code.addElement(GC.subgets(field, obj, rval));
2679              }
2680              code.addElement(modify(GC.statevar,x.locOp));
2681              return protect(protect, lhs, x.locOp, name + "=");
2682                
2683            } else if (ltag == TagConstants.ARRAYREFEXPR) {
2684              ArrayRefExpr lhs= (ArrayRefExpr)left;
2685    
2686              Expr array= trExpr(true, lhs.array);
2687              Expr index= trExpr(true, lhs.index);
2688              Expr rval= trExpr(false, right);
2689    
2690              arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
2691              // Add a check that the array[index] on the lhs is assignable
2692              frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
2693              if (! isFinal(TypeCheck.inst.getType(lhs.array))) {
2694                addCheck(x.locOp,
2695                         TagConstants.CHKARRAYSTORE,
2696                         GC.nary(TagConstants.IS, rval,
2697                                 GC.nary(TagConstants.ELEMTYPE,
2698                                         GC.nary(TagConstants.TYPEOF, array))),
2699                         Location.NULL, lhs.array);
2700              }
2701    
2702              code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
2703              code.addElement(modify(GC.statevar,x.locOp));
2704              Expr a= GC.select(GC.elemsvar, array);
2705              return protect(protect, GC.select(a, index), x.locOp);
2706                
2707            } else {
2708              Assert.fail("Unexpected tag " + TagConstants.toString(ltag)
2709                          + " (" + ltag + ")");
2710            }
2711          }
2712    
2713        case TagConstants.INC: case TagConstants.DEC:
2714        case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
2715        case TagConstants.ASGMUL:
2716        case TagConstants.ASGADD: case TagConstants.ASGSUB:
2717        case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
2718        case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
2719        case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR:
2720        case TagConstants.ASGDIV: case TagConstants.ASGREM:
2721          {
2722            Expr right, left;
2723            int op;
2724            int locOp;
2725            Type rType;
2726            if (expr instanceof UnaryExpr) {
2727              UnaryExpr u= (UnaryExpr) expr;
2728              right= GC.onelit;
2729              rType = Types.intType;
2730              left= u.expr;
2731              op= TrAnExpr.getGCTagForUnary(u);
2732              locOp = u.locOp;
2733            } else {
2734              BinaryExpr x= (BinaryExpr)expr;
2735              right= x.right;
2736              rType = TypeCheck.inst.getType(right);
2737              left= x.left;
2738              op= TrAnExpr.getGCTagForBinary(x);
2739              locOp = x.locOp;
2740            }
2741            Type lType = TypeCheck.inst.getType(left);
2742            boolean returnold= (tag == TagConstants.POSTFIXINC
2743                                || tag == TagConstants.POSTFIXDEC);
2744    
2745            int ltag = left.getTag();
2746            if (ltag == TagConstants.VARIABLEACCESS) {
2747              VariableAccess lhs= (VariableAccess)left;
2748              readCheck(lhs, lhs.getStartLoc());
2749    
2750              Expr oldLval= protect(Purity.impure(right) || returnold, lhs,
2751                                    locOp, "old!" + lhs.decl.id.toString());
2752              Expr rval= trExpr(false, right);
2753    
2754              if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2755                Assert.notFalse(expr instanceof BinaryExpr);
2756                if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2757                  addCheck(locOp, TagConstants.CHKARITHMETIC,
2758                           GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2759                }
2760              }
2761    
2762              if (op == TagConstants.STRINGCAT) { 
2763                rval = addNewString(expr,left,rval);
2764                    
2765              } else {
2766                rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(), op, oldLval, rval);
2767                rval= addRelAsgCast(rval, lType, rType);
2768              }
2769                            
2770              writeCheck(lhs, null, rval, locOp, false);
2771              code.addElement(GC.gets(lhs, rval));
2772              if (returnold) {
2773                return oldLval;
2774              } else {
2775                return protect(protect, lhs, locOp, lhs.decl.id.toString() + "=");
2776              }
2777                
2778            } else if (ltag == TagConstants.FIELDACCESS) {
2779              FieldAccess lhs = (FieldAccess)left;
2780              Expr lval= trFieldAccess(true, lhs);
2781              readCheck(lval, lhs.locId);
2782              // Add a check that the lhs is assignable
2783              frameHandler.modifiesCheckField(lval,lhs.getStartLoc(),
2784                                 ((FieldAccess)left).decl);
2785    
2786              String name = lhs.decl.id.toString();
2787              Expr oldLval = protect(Purity.impure(right) || returnold, lval,
2788                                     locOp, "old!" + name);
2789              Expr rval= trExpr(false, right);
2790              if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2791                Assert.notFalse(expr instanceof BinaryExpr);
2792                if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2793                  addCheck(locOp, TagConstants.CHKARITHMETIC,
2794                           GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2795                }
2796              }
2797    
2798              if (op == TagConstants.STRINGCAT) { 
2799                rval = addNewString(expr,lval,rval);
2800                                
2801              } else {
2802                rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(),
2803                              op, oldLval, rval);
2804                rval= addRelAsgCast(rval, lType, rType);
2805              }
2806                            
2807              writeCheck(lval, null, rval, locOp, false);
2808              if (lval.getTag() == TagConstants.VARIABLEACCESS) {
2809                code.addElement(GC.gets((VariableAccess)lval, rval));
2810              } else {
2811                NaryExpr target= (NaryExpr)lval;
2812                VariableAccess field= (VariableAccess)target.exprs.elementAt(0);
2813                Expr obj= target.exprs.elementAt(1);
2814                code.addElement(GC.subgets(field, obj, rval));
2815              }
2816              code.addElement(modify(GC.statevar,locOp));
2817              if (returnold) {
2818                return oldLval;
2819              } else {
2820                return protect(protect, lval, locOp, name + "=");
2821              }
2822                
2823            } else if (ltag == TagConstants.ARRAYREFEXPR) {
2824              ArrayRefExpr lhs= (ArrayRefExpr)left;
2825    
2826              Expr array= trExpr(true, lhs.array);
2827              Expr index= trExpr(true, lhs.index);
2828              arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket);
2829              // Add a check that the lhs is assignable
2830              frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc());
2831              Expr oldLval = protect(Purity.impure(right) || returnold,
2832                                     GC.select(GC.select(GC.elemsvar, array),
2833                                               index),
2834                                     locOp, "old");
2835    
2836              Expr rval= trExpr(false, right);
2837              if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) {
2838                Assert.notFalse(expr instanceof BinaryExpr);
2839                if (Types.isIntegralType(TypeCheck.inst.getType(right))) {
2840                  addCheck(locOp, TagConstants.CHKARITHMETIC,
2841                           GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit));
2842                }
2843              }
2844    
2845              rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(),
2846                            op, oldLval, rval);
2847              rval= addRelAsgCast(rval, lType, rType);
2848        
2849              code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval));
2850              code.addElement(modify(GC.statevar,locOp));
2851              if (returnold) {
2852                return oldLval;
2853              } else {
2854                Expr a= GC.select(GC.elemsvar, array);
2855                return protect(protect, GC.select(a, index), locOp);
2856              }
2857                
2858            } else {
2859              Assert.fail("Unexpected tag " + TagConstants.toString(ltag)
2860                          + " (" + ltag + ")");
2861            }
2862          }
2863    
2864          // Unary expressions
2865        case TagConstants.UNARYADD:
2866          {
2867            // drop UnaryADD
2868            UnaryExpr x= (UnaryExpr)expr;
2869            return trExpr(protect, x.expr);
2870          }
2871            
2872        case TagConstants.UNARYSUB:
2873        case TagConstants.NOT: case TagConstants.BITNOT:
2874          {
2875            UnaryExpr x= (UnaryExpr)expr;
2876            Expr x2= trExpr(false, x.expr);
2877            int newtag= TrAnExpr.getGCTagForUnary(x);
2878            return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(),
2879                                            newtag, x2),
2880                           x.locOp);
2881          }
2882    
2883        case TagConstants.PARENEXPR:
2884          {
2885            ParenExpr x= (ParenExpr)expr;
2886            return trExpr(protect, x.expr);
2887          }
2888    
2889        case TagConstants.VARIABLEACCESS:
2890          {
2891            VariableAccess x= (VariableAccess)expr;
2892            readCheck(x, x.getStartLoc());
2893            return protect(protect, x, x.getStartLoc(), x.decl.id.toString());
2894          }
2895          
2896        case TagConstants.FIELDACCESS:
2897          {
2898            FieldAccess fa = (FieldAccess)expr;
2899            Expr result = trFieldAccess(false, fa);
2900            if (fa.decl != Types.lengthFieldDecl)
2901              readCheck(result, fa.locId);
2902            return protect(protect, result, fa.locId, fa.decl.id.toString());
2903          }
2904          
2905        case TagConstants.METHODINVOCATION:
2906          {
2907            return trMethodInvocation(protect, (MethodInvocation)expr);
2908          }
2909    
2910        default:
2911          //@ unreachable;
2912          Assert.fail("UnknownTag<" + TagConstants.toString(tag) + ">");
2913          return null;
2914        }
2915      }
2916    
2917      private static Expr addRelAsgCast(Expr rval, Type lType, Type rType) {
2918        if (!(lType instanceof PrimitiveType))
2919          return rval;
2920        
2921        switch (lType.getTag()) {
2922        case TagConstants.BYTETYPE:
2923        case TagConstants.SHORTTYPE:
2924        case TagConstants.CHARTYPE:
2925          break;  // cast needed
2926        case TagConstants.INTTYPE:
2927          if (Types.isLongType(rType) || Types.isFloatingPointType(rType)) {
2928            break;  // cast needed
2929          } else {
2930            return rval;
2931          }
2932        case TagConstants.LONGTYPE:
2933          if (Types.isFloatingPointType(rType)) {
2934            break;  // cast needed
2935          } else {
2936            return rval;
2937          }
2938        case TagConstants.FLOATTYPE:
2939        case TagConstants.DOUBLETYPE:
2940          return rval;
2941        default:
2942          return rval;
2943        }
2944        return GC.nary(TagConstants.CAST, rval, GC.typeExpr(lType));
2945      }
2946      
2947      /**
2948       * Returns the guarded-command expression:
2949       * <pre>
2950       * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
2951       *              ==> isNewArray(o))
2952       * </pre>
2953       */
2954      private static Expr predEvathangsAnArray(VariableAccess allocOld,
2955                                               VariableAccess allocNew) {
2956        LocalVarDecl odecl = UniqName.newBoundVariable('o');
2957        VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL);
2958    
2959        Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld));
2960        Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew);
2961        Expr e2 = GC.nary(TagConstants.ISNEWARRAY, o);
2962    
2963        Expr body = GC.implies(GC.and(e0, e1), e2);
2964                               
2965        // TBW:  "e2" should be the trigger of the following quantification
2966        return GC.forall(odecl, body);
2967      }
2968    
2969    
2970      /**
2971       * Returns the guarded-command expression:
2972       * <pre>
2973       * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew)
2974       *              ==> o.owner == null)
2975       * </pre>
2976       */  
2977      private static Expr predArrayOwnerNull(VariableAccess allocOld,
2978                                             VariableAccess allocNew,
2979                                             VariableAccess arr) {
2980        // get java.lang.Object
2981        TypeSig obj = Types.javaLangObject();
2982          
2983        FieldDecl owner = null; // make the compiler happy
2984        boolean notFound = false;
2985        try {
2986          owner = Types.lookupField(obj, Identifier.intern("owner"),
2987                                    obj);
2988        }
2989        catch (javafe.tc.LookupException e) {
2990          notFound = true;
2991        }
2992        // if we couldn't find the owner ghost field, there's nothing to do
2993        if (notFound)
2994          return null;
2995          
2996        VariableAccess ownerVA = TrAnExpr.makeVarAccess(owner, Location.NULL);
2997    
2998        LocalVarDecl odecl = UniqName.newBoundVariable('o');
2999        VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL);
3000    
3001        Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld));
3002        Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew);
3003        Expr e2 =  GC.nary(TagConstants.REFEQ, GC.select(ownerVA, arr),
3004                           GC.nulllit);
3005          
3006        
3007        Expr body = GC.implies(GC.and(e0, e1), e2);
3008          
3009        return GC.forall(odecl, body);
3010      }
3011    
3012      // @todo Should be moved type javafe.tc.Types
3013    
3014      /**
3015       * @return true if there can be no subtypes of <code>t</code>.
3016       * @design The definition of final used by this method is as follows.  Reference
3017       * types are "final" if they have the <code>final</code> modifier.  Array types
3018       * are "final" if their element types satisfy <code>isFinal</code>.  Primitive
3019       * types are "final".
3020       */
3021      public static boolean isFinal(/*@ non_null */ Type t) {
3022        int tag= t.getTag();
3023        switch (tag) {
3024        case TagConstants.BOOLEANTYPE:
3025        case TagConstants.INTTYPE:
3026        case TagConstants.LONGTYPE:
3027        case TagConstants.CHARTYPE:
3028        case TagConstants.FLOATTYPE:
3029        case TagConstants.DOUBLETYPE:
3030        case TagConstants.BYTETYPE:
3031        case TagConstants.SHORTTYPE:
3032          return true;
3033    
3034        case TagConstants.ARRAYTYPE:
3035          return isFinal(((ArrayType)t).elemType);
3036    
3037        case TagConstants.TYPENAME:
3038          t= TypeCheck.inst.getSig((TypeName)t);
3039        case TagConstants.TYPESIG:
3040          TypeSig ts= (TypeSig)t;
3041          return Modifiers.isFinal(ts.getTypeDecl().modifiers);
3042    
3043        default:
3044          //@ unreachable;
3045          Assert.fail("Unexpected tag " + TagConstants.toString(tag) + " ("
3046                      + tag + ")");
3047          return false;
3048        }
3049      }
3050    
3051      //// Factor processing of FieldAccess nodes
3052    
3053      /**
3054       * Returns either a <code>VariableAccess</code> if <code>fa</code> is a class
3055       * variable or a <code>SELECT</code> application if <code>fa</code> is an
3056       * instance variable access, or an <code>ARRAYLENGTH</code> application if
3057       * <code>fa</code> is the final array field <code>length</code>.  In the second
3058       * case, will emit code for computing the object designator and also a check to
3059       * ensure that object is not null.
3060       */
3061      private Expr trFieldAccess(boolean protectObject,
3062                                 /*@ non_null */ FieldAccess fa) {
3063        VariableAccess va;
3064        Iterator iter = modifyEverythingLocations.iterator();
3065        if (iter.hasNext()) {
3066          va = TrAnExpr.makeVarAccess(fa.decl, fa.locId);
3067          EverythingLoc s = (EverythingLoc)iter.next();
3068          s.add(va);
3069                    
3070        } else {
3071          va = TrAnExpr.makeVarAccess(fa.decl, fa.locId);
3072        }
3073    
3074        int tag= fa.od.getTag();
3075        if (Modifiers.isStatic(fa.decl.modifiers)) {
3076          // static field
3077          switch (tag) {
3078          case TagConstants.TYPEOBJECTDESIGNATOR:
3079          case TagConstants.SUPEROBJECTDESIGNATOR:
3080            break;
3081          case TagConstants.EXPROBJECTDESIGNATOR: {
3082            ExprObjectDesignator od= (ExprObjectDesignator)fa.od;
3083            Expr discardResult = trExpr(false, od.expr);
3084            break;
3085          }
3086          default:
3087            //@ unreachable;
3088            Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3089                        + " (" + tag + ")");
3090            break;
3091          }
3092          return va;
3093              
3094        } else {
3095          // instance variable
3096          Expr obj;
3097          switch (tag) {
3098          case TagConstants.EXPROBJECTDESIGNATOR: {
3099            ExprObjectDesignator od= (ExprObjectDesignator)fa.od;
3100            obj= trExpr(protectObject, od.expr);
3101            nullCheck(od.expr, obj, fa.od.locDot);
3102            break;
3103          }
3104          case TagConstants.SUPEROBJECTDESIGNATOR:
3105            obj= GC.thisvar;
3106            break;
3107          case TagConstants.TYPEOBJECTDESIGNATOR:
3108            // This case is not legal Java and should already have been
3109            // checked by the type checker
3110            //@ unreachable;
3111            Assert.fail("Unexpected tag");
3112            obj= null;  // dummy assignment
3113            break;
3114          default:
3115            //@ unreachable;
3116            Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3117                        + " (" + tag + ")");
3118            obj= null;  // dummy assignment
3119            break;
3120          }
3121    
3122          Expr res;
3123          if (fa.decl == Types.lengthFieldDecl) {
3124            return GC.nary(fa.getStartLoc(), fa.getEndLoc(),
3125                           TagConstants.ARRAYLENGTH, obj);
3126          } else {
3127            return GC.nary(fa.getStartLoc(), fa.getEndLoc(),
3128                           TagConstants.SELECT, va, obj);
3129          }
3130        }
3131      }
3132    
3133      /**
3134       * This translation of method invocation follows section 4.1 of ESCJ 16.
3135       */
3136      private Expr trMethodInvocation(boolean protect, 
3137                                      /*@ non_null */ MethodInvocation mi) {
3138        boolean isStatic = Modifiers.isStatic(mi.decl.modifiers);
3139    
3140        // for holding the translated arguments
3141        ExprVec args = ExprVec.make(mi.args.size() + 1);
3142        ExprVec argsRaw = ExprVec.make(mi.args.size() + 1);
3143        Expr nullcheckArg = null;  // Java expression
3144        /*-@ uninitialized */ int nullcheckLoc = Location.NULL;
3145        // FIXME /*@ readable nullcheckLoc if nullcheckArg != null; */
3146    
3147        Expr eod = null;
3148        int tag= mi.od.getTag();
3149        switch (tag) {
3150        case TagConstants.TYPEOBJECTDESIGNATOR: {
3151          Assert.notFalse(isStatic);  // non-static is not legal Java
3152          // the arguments are translated below
3153          break;
3154        }
3155        case TagConstants.EXPROBJECTDESIGNATOR: {
3156          ExprObjectDesignator od = (ExprObjectDesignator)mi.od;
3157          if (isStatic) {
3158            Expr discardResult = trExpr(false, od.expr);
3159          } else {
3160            // protect "self" if there are more arguments
3161            Expr self = trExpr(mi.args.size() != 0, od.expr);
3162            args.addElement(self);
3163            argsRaw.addElement(od.expr);
3164            nullcheckArg = od.expr;
3165            nullcheckLoc = od.locDot;
3166            eod = self;
3167          }
3168          // the (rest of) the arguments are translated below
3169          break;
3170        }
3171        case TagConstants.SUPEROBJECTDESIGNATOR: {
3172          if (! isStatic) {
3173            args.addElement(GC.thisvar);
3174            argsRaw.addElement(ThisExpr.make(null, mi.od.getStartLoc()));
3175            eod = GC.thisvar;
3176          }
3177          // the (rest of) the arguments are translated below
3178          break;
3179        }
3180        default:
3181          //@ unreachable;
3182          Assert.fail("Unexpected tag " + TagConstants.toString(tag)
3183                      + " (" + tag + ")");
3184          break;
3185        }
3186        
3187        // translate remaining arguments
3188        for (int i = 0; i < mi.args.size(); i++) {
3189          // protect all but the last argument
3190          Expr argRaw = mi.args.elementAt(i);
3191          Expr arg = trExpr(i != mi.args.size()-1, argRaw);
3192          args.addElement(arg);
3193          argsRaw.addElement(argRaw);
3194        }
3195    
3196        if (nullcheckArg != null) {
3197          nullCheck(nullcheckArg, args.elementAt(0), nullcheckLoc);
3198        }
3199    
3200        InlineSettings is = (InlineSettings)inlineDecoration.get(mi);
3201        code.addElement( call( mi.decl, argsRaw, args, scope, mi.locId, 
3202                               mi.getEndLoc(), mi.locOpenParen, false, is, eod, false));
3203        return protect(protect, GC.resultvar, mi.locOpenParen,
3204                       mi.decl.id.toString());
3205      }
3206    
3207      
3208      //// Helper methods for generating check assertions/assumptions
3209    
3210      /**
3211       * Emit a check at location <code>loc</code> that guarded command expression
3212       * <code>e</code>, which was translated from the Java expression <code>E</code>,
3213       * is not <code>null</code>.  If <code>E</code> denotes an expression that is
3214       * guaranteed not to be <code>null</code>, no check is emitted.
3215       */
3216      private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc) {
3217        nullCheck(E, e, loc, TagConstants.CHKNULLPOINTER, Location.NULL);
3218      }
3219    
3220      private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc,
3221                             int errorName, int locPragma) {
3222        // start by peeling off parentheses and casts
3223        E = trim(E);
3224    
3225        switch (E.getTag()) {
3226        case TagConstants.THISEXPR:
3227          return;
3228    
3229        case TagConstants.VARIABLEACCESS: {
3230          GenericVarDecl d = ((VariableAccess)E).decl;
3231          SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d);
3232          if (nonNullPragma != null && !Main.options().guardedVC) {
3233            LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc());
3234            return;
3235          }
3236          break;  // perform check
3237        }
3238    
3239        case TagConstants.FIELDACCESS: {
3240          FieldDecl fd = ((FieldAccess)E).decl;
3241          SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(fd);
3242          if (nonNullPragma != null && !Main.options().guardedVC) {
3243            if (Modifiers.isStatic(fd.modifiers) ||
3244                rdCurrent.getTag() != TagConstants.CONSTRUCTORDECL ||
3245                rdCurrent.parent != fd.parent) {
3246              LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc());
3247              return;
3248            }
3249          }
3250          break;  // perform check
3251        }
3252    
3253        default:
3254          break;  // perform check
3255        }
3256        
3257        Expr nullcheck = GC.nary(TagConstants.REFNE, e, GC.nulllit);
3258        addCheck(loc, errorName, nullcheck, locPragma, E);
3259      }
3260      
3261      /**
3262       * Peels off parentheses and casts from <code>E</code> and returns the result
3263       */
3264      private VarInit trim(/*@ non_null */ VarInit E) {
3265        while (true) {
3266          if (E.getTag() == TagConstants.PARENEXPR) {
3267            E = ((ParenExpr)E).expr;
3268          } else if (E.getTag() == TagConstants.CASTEXPR) {
3269            E = ((CastExpr)E).expr;
3270          } else {
3271            return E;
3272          }
3273        }
3274      }
3275      
3276      /**
3277       * Emit the checks that <code>array</code> is non-null and that
3278       * <code>index</code> is inbounds for <code>array</code>.  Implements the
3279       * ArrayAccessCheck function of ESCJ16.
3280       */
3281      private void arrayAccessCheck(/*@ non_null */ Expr Array, /*@ non_null */ Expr array,
3282                                    /*@ non_null */ Expr Index, /*@ non_null */ Expr index,
3283                                    int locOpenBracket) {
3284        nullCheck(Array, array, locOpenBracket);
3285    
3286        Expr length= GC.nary(TagConstants.ARRAYLENGTH, array);
3287        Expr indexNeg = GC.nary(TagConstants.INTEGRALLE, GC.zerolit, index);
3288        addCheck(locOpenBracket, TagConstants.CHKINDEXNEGATIVE, indexNeg,
3289                 Location.NULL, trim(Index));
3290        Expr indexTooBig = GC.nary(TagConstants.INTEGRALLT, index, length);
3291        addCheck(locOpenBracket, TagConstants.CHKINDEXTOOBIG, indexTooBig);
3292      }
3293    
3294      /**
3295       * Used by <code>readCheck</code> and <code>writeCheck</code> to accumulate the
3296       * list of mutexes protecting a shared variable.  Thus, these methods are not
3297       * thread re-entrant.
3298       */
3299      private /*@ non_null */ ExprVec mutexList = ExprVec.make(5);
3300      private /*@ non_null */ ArrayList locList = new ArrayList(5);
3301    
3302      /**
3303       * Insert checks done before reading variables.
3304       *
3305       * <p> This method implements ReadCheck as defined in ESCJ16.  Handles reads of
3306       * local, class, and instance variables (ESCJ16 splits these into two ReadCheck
3307       * functions). </p>
3308       *
3309       * @param va is the variable being read; it must be either a
3310       * <code>VariableAccess</code> (in the case of local variables and class fields)
3311       * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance
3312       * fields).
3313       * @param locId is the location of the variable or field being read.  It is used
3314       * to determine the location of the "wrong" part of the check's label.
3315       */
3316      private void readCheck(/*@ non_null */ Expr va, int locId) {
3317        Assert.notFalse(locId != Location.NULL);
3318        // "d" is the declaration of the variable being read
3319        GenericVarDecl d;
3320        Expr actualSelf = null;
3321        if (va.getTag() == TagConstants.SELECT) {
3322          NaryExpr sel= (NaryExpr)va;
3323          d= ((VariableAccess)sel.exprs.elementAt(0)).decl;
3324          actualSelf = sel.exprs.elementAt(1);
3325        } else {
3326          d= ((VariableAccess)va).decl;
3327        }
3328    
3329        if (d.pmodifiers == null) return;
3330    
3331        Hashtable map = null;
3332    
3333        mutexList.removeAllElements();
3334        locList.clear();
3335        ModifierPragma firstMonitoredPragma = null;
3336        for (int i= 0; i < d.pmodifiers.size(); i++) {
3337          ModifierPragma prag= d.pmodifiers.elementAt(i);
3338          int tag= prag.getTag();
3339          switch (tag) {
3340          case TagConstants.NON_NULL:
3341          case TagConstants.SPEC_PUBLIC:
3342          case TagConstants.SPEC_PROTECTED:
3343          case TagConstants.WRITABLE_IF:
3344            break;
3345              
3346          case TagConstants.UNINITIALIZED:
3347            // "uninitialized" can be used only with local variables
3348            Assert.notFalse(va.getTag() != TagConstants.SELECT);
3349            VariableAccess init= getInitVar((LocalVarDecl) d);
3350            addCheck(locId, TagConstants.CHKINITIALIZATION, init, prag);
3351            break;
3352    
3353          case TagConstants.READABLE_IF:
3354            map = initializeRWCheckSubstMap(map, actualSelf, locId);
3355            Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null);
3356            addCheck(locId, TagConstants.CHKDEFINEDNESS, dc, prag);
3357            break;
3358    
3359          case TagConstants.MONITORED_BY: {
3360            ExprModifierPragma emp = (ExprModifierPragma)prag;
3361            map = initializeRWCheckSubstMap(map, actualSelf, locId);
3362            mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null));
3363            locList.add(new Integer(emp.expr.getStartLoc()));
3364            if (firstMonitoredPragma == null)
3365              firstMonitoredPragma = prag;
3366            break;
3367          }
3368    
3369          case TagConstants.MONITORED:
3370            Assert.notFalse(d instanceof FieldDecl);
3371            if (Modifiers.isStatic(d.modifiers)) {
3372              mutexList.addElement(
3373                                   GC.nary(TagConstants.CLASSLITERALFUNC,
3374                                           getClassObject(((FieldDecl)d).parent)));
3375            } else {
3376              mutexList.addElement(actualSelf);
3377            }
3378            locList.add(new Integer(prag.getStartLoc()));
3379            if (firstMonitoredPragma == null)
3380              firstMonitoredPragma = prag;
3381            break;
3382    
3383          case TagConstants.INSTANCE:
3384          case TagConstants.IN:
3385          case TagConstants.MAPS:
3386          case TagConstants.GHOST:
3387          case TagConstants.MODEL:
3388            // ignore
3389            break;
3390    
3391          default:
3392            Assert.fail("Unexpected tag \"" + TagConstants.toString(tag)
3393                        + "\" (" + tag + ")");
3394          }
3395        }
3396    
3397        if (mutexList.size() != 0) {
3398          Expr onelocked= GC.falselit;
3399          for (int i= mutexList.size()-1; 0 <= i; i--) {
3400            Expr mu= mutexList.elementAt(i);
3401            onelocked= GC.or(GC.and(GC.nary(TagConstants.REFNE, mu, GC.nulllit),
3402                                    GC.nary(TagConstants.SELECT, GC.LSvar, mu)),
3403                             onelocked);
3404          }
3405          if (rdCurrent instanceof ConstructorDecl && actualSelf != null) {
3406            // In constructors, always allow access to the fields of the object
3407            // being constructed.
3408            // Note: The following could be optimized so that if "actualSelf"
3409            // is ``obviously'' "this", then the check could be omitted altogether.
3410            onelocked = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar),
3411                              onelocked);
3412          }
3413          // For a read race, we have a race condition if none of the 
3414          // monitors are locked.  Since we can't point to all of them
3415          // we point to the beginning of the first monitored declaration,
3416          // rather than to a specific expresssion - will likely be 
3417          // confusing to the user anyway.
3418          addCheck(locId, TagConstants.CHKSHARING, onelocked,
3419                   firstMonitoredPragma);
3420        }
3421        mutexList.removeAllElements(); // Help the garbage collector...
3422        locList.clear(); // Help the garbage collector...
3423      }
3424    
3425      /**
3426       * Insert checks done before writing variables, as prescribed by WriteCheck in
3427       * ESCJ 16.  Handles writes of local, class, and instance variables (ESCJ 16
3428       * splits these into two WriteCheck functions).
3429       *
3430       * @param va is the variable being written; it must be either a
3431       * <code>VariableAccess</code> (in the case of local variables and class fields)
3432       * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance
3433       * fields).
3434       * @param rval is the guarded command expression being written into
3435       * <code>va</code>.  The argument <code>Rval</code> is either the Java expression
3436       * from which <code>rval</code> was translated, or <code>null</code> if
3437       * <code>rval</code> was somehow synthesized.
3438       * @param locAssignOp is the location of the assignment operator that prescribes
3439       * the write.  It is used to determine the location of the "wrong" part of the
3440       * check's label.
3441       * @param inInitializerContext indicates whether or not the expression whose
3442       * write check is to be performed is the initializing expression of a field.
3443       */
3444      private void writeCheck(/*@ non_null */ Expr va, 
3445                              VarInit Rval, Expr rval, int locAssignOp,
3446                              boolean inInitializerContext) {
3447        Assert.notFalse(locAssignOp != Location.NULL);
3448        // "d" is the declaration of the variable being written
3449        GenericVarDecl d;
3450        Expr actualSelf = null;
3451        if (va.getTag() == TagConstants.SELECT) {
3452          NaryExpr sel= (NaryExpr)va;
3453          d= ((VariableAccess)sel.exprs.elementAt(0)).decl;
3454          actualSelf = sel.exprs.elementAt(1);
3455        } else {
3456          d= ((VariableAccess)va).decl;
3457        }
3458    
3459        // Handle non_null variables
3460        SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d);
3461        if (nonNullPragma != null) {
3462          if (Rval == null) {
3463            Expr nullcheck = GC.nary(TagConstants.REFNE, rval, GC.nulllit);
3464            addCheck(locAssignOp, TagConstants.CHKNONNULL, nullcheck,
3465                     nonNullPragma.getStartLoc());
3466          } else if (!Main.options().excuseNullInitializers || !inInitializerContext ||
3467                     trim(Rval).getTag() != TagConstants.NULLLIT) {
3468            nullCheck(Rval, rval, locAssignOp, TagConstants.CHKNONNULL,
3469                      nonNullPragma.getStartLoc());
3470          }
3471        }
3472    
3473        if (d.pmodifiers == null) return;
3474    
3475        Hashtable map = null;
3476    
3477        mutexList.removeAllElements();
3478        locList.clear();
3479        Expr onenotnull= GC.falselit;
3480        ModifierPragma firstMonitoredPragma = null;
3481        for (int i= 0; i < d.pmodifiers.size(); i++) {
3482          ModifierPragma prag= d.pmodifiers.elementAt(i);
3483          int tag= prag.getTag();
3484          switch (tag) {
3485          case TagConstants.IN:
3486          case TagConstants.MAPS:
3487          case TagConstants.INSTANCE:
3488          case TagConstants.UNINITIALIZED:
3489          case TagConstants.READABLE_IF:
3490          case TagConstants.SPEC_PUBLIC:
3491          case TagConstants.SPEC_PROTECTED:
3492          case TagConstants.GHOST:
3493          case TagConstants.NON_NULL:               // handled above
3494            break;
3495    
3496          case TagConstants.MODEL:
3497            ErrorSet.error(locAssignOp,"May not assign to a model variable");
3498            break;
3499    
3500          case TagConstants.WRITABLE_IF:
3501            map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp);
3502            Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null);
3503            addCheck(locAssignOp, TagConstants.CHKWRITABLE, dc, prag);
3504            break;
3505    
3506          case TagConstants.MONITORED_BY: {
3507            ExprModifierPragma emp = (ExprModifierPragma)prag;
3508            map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp);
3509            // We keep a list of locations in locList because the
3510            // translated expr (if it refers to this) may have a
3511            // dummy location and we want to be sure to have any
3512            // Race warning point to the actual object whose monitor
3513            // has not been acquired.
3514            mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null));
3515            locList.add(new Integer(emp.expr.getStartLoc()));
3516            if (firstMonitoredPragma == null)
3517              firstMonitoredPragma = prag;
3518            break;
3519          }
3520    
3521          case TagConstants.MONITORED:
3522            Assert.notFalse(d instanceof FieldDecl);
3523            if (Modifiers.isStatic(d.modifiers)) {
3524              mutexList.addElement(GC.nary(
3525                                           TagConstants.CLASSLITERALFUNC,
3526                                           getClassObject(((FieldDecl)d).parent)));
3527            } else {
3528              mutexList.addElement(actualSelf);
3529            }
3530            locList.add(new Integer(prag.getStartLoc()));
3531            onenotnull= GC.truelit;
3532            if (firstMonitoredPragma == null)
3533              firstMonitoredPragma = prag;
3534            break;
3535    
3536          default:
3537            Assert.fail("Unexpected tag \"" + TagConstants.toString(tag)
3538                        + "\" (" + tag + ")");
3539          }
3540        }
3541    
3542        if (mutexList.size() != 0) {
3543          Expr allnullorlocked= GC.truelit;
3544          boolean doConst = rdCurrent instanceof ConstructorDecl &&
3545            actualSelf != null;
3546          for (int i= mutexList.size()-1; 0 <= i; i--) {
3547            Expr mu= mutexList.elementAt(i);
3548            onenotnull= GC.or(GC.nary(TagConstants.REFNE, mu, GC.nulllit),
3549                              onenotnull);
3550            Expr nullOrLocked = 
3551              GC.or(GC.nary(TagConstants.REFEQ, mu, GC.nulllit),
3552                    GC.select(GC.LSvar, mu));
3553            if (!doConst) {
3554              int loc = mu.getStartLoc();
3555              if (loc == Location.NULL) loc = ((Integer)locList.get(i)).intValue();
3556              addCheck(locAssignOp, TagConstants.CHKSHARING,
3557                       nullOrLocked,loc); 
3558            }
3559            allnullorlocked=
3560              GC.and(nullOrLocked, allnullorlocked);
3561          }
3562          Expr p = GC.and(onenotnull, allnullorlocked);
3563          if (doConst) {
3564            // In constructors, always allow access to the fields of the object
3565            // being constructed.
3566            // Note: The following could be optimized so that if "actualSelf"
3567            // is ``obviously'' "this", then the check could be omitted altogether.
3568            p = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar), p);
3569            addCheck(locAssignOp, TagConstants.CHKSHARING, p, firstMonitoredPragma);
3570          } else {
3571            addCheck(locAssignOp, TagConstants.CHKSHARINGALLNULL, onenotnull, firstMonitoredPragma);
3572          }
3573        }
3574        mutexList.removeAllElements(); // Help the garbage collector...
3575        locList.clear(); // Help the garbage collector...
3576      }
3577    
3578      /**
3579       * The following method is used in readCheck and writeCheck to lazily construct a
3580       * substitution map (which may also create another temporary variable).
3581       */
3582      private Hashtable initializeRWCheckSubstMap(Hashtable prevMap,
3583                                                  Expr actualSelf,
3584                                                  int loc) {
3585        if (actualSelf == null) {
3586          // no map needed
3587          Assert.notFalse(prevMap == null);
3588          return null;
3589        } else if (prevMap != null) {
3590          return prevMap;
3591        } else {
3592          Hashtable map = new Hashtable();
3593          VariableAccess vaSelf;
3594          if (actualSelf instanceof VariableAccess) {
3595            vaSelf = (VariableAccess)actualSelf;
3596          } else {
3597            vaSelf = (VariableAccess)protect(true, actualSelf, loc, "od");
3598          }
3599          map.put(GC.thisvar.decl, vaSelf);
3600          return map;
3601        }
3602      }
3603      
3604      /**
3605       * Calls <code>GC.check</code> to create a check and appends the result to
3606       * <code>code</code>.
3607       */
3608      //@ modifies code.elementCount;
3609      private void addCheck(int locUse, Condition cond) {
3610        code.addElement(GC.check(locUse, cond));
3611      }
3612      
3613      /**
3614       * Calls <code>GC.check</code> to create a check and appends the result to
3615       * <code>code</code>.
3616       */
3617      //@ modifies code.elementCount;
3618      void addCheck(int locUse, int errorName, Expr pred) {
3619        addCheck(locUse, errorName, pred, Location.NULL);
3620      }
3621      
3622      /**
3623       * Calls <code>GC.check</code> to create a check and appends the result to
3624       * <code>code</code>.
3625       */
3626      //@ modifies code.elementCount;
3627      private void addCheck(/*@ non_null */ ASTNode use, int errorName, Expr pred) {
3628        code.addElement(GC.check(use.getStartLoc(),
3629                                 errorName, pred,
3630                                 Location.NULL));
3631      }
3632    
3633      /**
3634       * Calls <code>GC.check</code> to create a check and appends the result to
3635       * <code>code</code>.
3636       */
3637      //@ modifies code.elementCount;
3638      private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl) {
3639        code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl));
3640      }
3641      
3642      void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc) {
3643        code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, auxLoc, null));
3644      }
3645      
3646      /**
3647       * Calls <code>GC.check</code> to create a check and appends the result to
3648       * <code>code</code>.
3649       */
3650      //@ modifies code.elementCount;
3651      private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl,
3652                            Object aux) {
3653        code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, aux));
3654      }
3655      
3656      /** Calls <code>GC.check</code> to create a check and appends the
3657          result to <code>code</code>. */
3658    
3659      //@ modifies code.elementCount;
3660      private void addCheck(int locUse, int errorName, Expr pred,
3661                            /*@ non_null */ ASTNode prag) {
3662        code.addElement(GC.check(locUse, errorName, pred, prag.getStartLoc()));
3663      }
3664    
3665      private void addAssumption(Expr pred) {
3666        code.addElement(GC.assume(pred));
3667        //code.addElement(GC.check(pred.getStartLoc(),TagConstants.CHKCONSISTENT, pred,
3668        //          Location.NULL, null));
3669      }
3670    
3671      private void addAssumptions(ExprVec ev) {
3672        if (ev == null) return;
3673        for (int i=0; i<ev.size(); ++i) {
3674          addAssumption(ev.elementAt(i));
3675        }
3676      }
3677    
3678      private void addNewAssumptions() {
3679        addNewAssumptionsHelper();
3680        axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
3681        TrAnExpr.closeForClause();
3682      }
3683      ExprVec addNewAssumptionsNow() {
3684        addNewAssumptionsHelper();
3685        if (TrAnExpr.trSpecAuxAxiomsNeeded != null)
3686          axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded);
3687        ExprVec ev = ExprVec.make(10);
3688        GetSpec.addAxioms(axsToAdd,ev);
3689        addNewAssumptionsNow(ev);
3690        TrAnExpr.closeForClause();
3691        return ev;
3692      }
3693      private void addNewAssumptionsNow(ExprVec ev) {
3694        //addNewAssumptionsHelper();
3695        for (int i=0; i<ev.size(); ++i) {
3696          addAssumption(ev.elementAt(i));
3697        }
3698      }
3699      private void addNewAssumptionsHelper() {
3700        if (TrAnExpr.trSpecModelVarsUsed != null) {
3701          // These assignments with a null rhs are used to indicate
3702          // that the target has some unknown new value.
3703          Iterator ii = TrAnExpr.trSpecModelVarsUsed.values().iterator();
3704          while (ii.hasNext()) {
3705            VariableAccess d = (VariableAccess)ii.next();
3706            code.addElement(GC.gets(d,null));  // FIXME - what about array model vars, static model vars
3707          }
3708        }
3709        addAssumptions(TrAnExpr.trSpecExprAuxConditions);
3710        addAssumptions(TrAnExpr.trSpecExprAuxAssumptions);
3711      }
3712      /**
3713       * Return the <code>VariableAccesss</code> associated with <code>d</code> by a
3714       * call to <code>setInitVar</code>.  If none has been associated with
3715       * <code>d</code>, returns <code>null</code>.
3716       */
3717      private static VariableAccess getInitVar(GenericVarDecl d) {
3718        return (VariableAccess)Purity.translateDecoration.get(d);
3719      }
3720    
3721      /**
3722       * Associates <code>init</code> with <code>d</code>; will be returned by a call
3723       * to <code>getInitVar</code>. 
3724       */
3725      private static void setInitVar(GenericVarDecl d, VariableAccess init) {
3726        Purity.translateDecoration.set(d, init);
3727      }
3728    
3729      /** Modifies a GC designator. GC designator can include SubstExpr. */
3730      
3731      private GuardedCmd modify(/*@ non_null */ VariableAccess va, int loc) {
3732        VariableAccess newVal = temporary(va.id.toString(), loc, loc);
3733        return GC.gets(va, newVal);
3734      }
3735      
3736      private GuardedCmd modify(/*@ non_null */ Expr e, Hashtable pt, int loc) {
3737        VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(loc),
3738                                          e.getStartLoc(), e.getStartLoc());
3739    
3740        int etag = e.getTag();
3741        if (etag == TagConstants.VARIABLEACCESS) {
3742          // "e" is a single variable
3743          return GC.gets( (VariableAccess)e, newVal );
3744        }
3745    
3746        Assert.notFalse(etag == TagConstants.SELECT);
3747        NaryExpr nary = (NaryExpr)e;
3748        e = nary.exprs.elementAt(0);
3749        Expr index = nary.exprs.elementAt(1);
3750        if (pt != null) {
3751          index = GC.subst(Location.NULL, Location.NULL, pt, index);
3752        }
3753        etag = e.getTag();
3754        if (etag == TagConstants.VARIABLEACCESS) {
3755          // The given "e" had the form "f[index]"
3756          return GC.subgets((VariableAccess)e, index, newVal);
3757        }
3758    
3759        // The given "e" had the form "elems[array][index]"
3760        //Assert.notFalse(etag == TagConstants.SELECT);
3761        //nary = (NaryExpr)e;
3762        //VariableAccess elems = (VariableAccess)nary.exprs.elementAt(0);
3763        //Expr array = nary.exprs.elementAt(1);
3764        //if (pt != null) {
3765        //  array = GC.subst(Location.NULL, Location.NULL, pt, array);
3766        //}
3767        //return GC.subsubgets(elems, array, index, newVal);
3768        return null;
3769      }
3770    
3771    
3772      // the inlining depth at which to perform checking.
3773      public int inlineCheckDepth = 0;
3774      // the number of levels of inlining after the level that is checked.
3775      public int inlineDepthPastCheck = 0;
3776        
3777      /**
3778       * Creates and desugars a call node, extended to allow the possibility of
3779       * inlining a call.
3780       */
3781      private Call call(RoutineDecl rd, ExprVec argsRaw, ExprVec args,
3782                        FindContributors scope,
3783                        int scall, int ecall, int locOpenParen,
3784                        boolean superOrSiblingConstructorCall,
3785                        InlineSettings inline, Expr eod, boolean freshResult) {
3786        // save the current status of checking assertions
3787        boolean useGlobalStatus = NoWarn.useGlobalStatus;
3788    
3789        // obtain the appropriate inlining flags
3790        inline = computeInlineSettings(rd, argsRaw, inline, scall);
3791    
3792        // create call
3793        Call call = Call.make( args, scall, ecall, inline != null);
3794        call.rd = rd;
3795    
3796        // now figure out desugared part
3797        
3798        String description;
3799        Spec spec;
3800        if (inline != null) {
3801          if (inline.getSpecForInline) {
3802            //System.out.println("GETTING SPEC FOR INLINE");
3803            spec = GetSpec.getSpecForInline(call.rd, scope);
3804          } else {
3805            Set synTargs = predictedSynTargs;
3806            if (synTargs == null)
3807              synTargs = new Set();
3808            //System.out.println("GETTING SPEC FOR BODY");
3809            spec = GetSpec.getSpecForBody(call.rd, scope, synTargs, null);
3810          }
3811          description = "inlined call";
3812        }
3813        else {
3814          //System.out.println("GETTING SPEC FOR CALL " + Location.toString(call.rd.loc) );
3815          spec = GetSpec.getSpecForCall( call.rd, scope, predictedSynTargs );
3816          if (spec.modifiesEverything) {
3817            ErrorSet.caution(scall,
3818                             "A method that 'modifies everything' has been called; the verification of a body with such a call is not correct.");
3819          }
3820          description = "call";
3821        }
3822        call.spec = spec;
3823    
3824        Assert.notFalse( spec.dmd.args.size() == call.args.size(),
3825                         "formal args: " + spec.dmd.args.size()
3826                         + " actualargs: " + call.args.size() );
3827    
3828    
3829        // now start creating code and temporaries
3830        code.push();         // this mark popped by "spill"
3831        temporaries.push();  // this mark popped by "spill"
3832    
3833        // create pt = { p* -> p*@L, wt*@pre -> wt*@L }
3834        
3835        Vector ptDomain = new Vector();
3836        for(int i=0; i<spec.dmd.args.size(); i++)
3837          ptDomain.addElement( spec.dmd.args.elementAt(i) );
3838    
3839        // spec.preVarMap gives the set of locations that are in modifies clauses for the
3840        // called routine
3841        for(Enumeration e = spec.preVarMap.elements(); e.hasMoreElements(); )
3842          ptDomain.addElement( ((VariableAccess)e.nextElement()).decl );
3843        Hashtable pt = GetSpec.makeSubst( ptDomain.elements(),
3844                                          UniqName.locToSuffix(call.scall) );
3845        
3846        /* if the dontCheckPreconditions flag is set, turn off the following 
3847           checks for non_null parameters and preconditions */
3848        if (inline != null) {
3849          globallyTurnOffChecks(inline.dontCheckPreconditions);
3850        }
3851    
3852        // var p*@L = e* in
3853        Hashtable argsMap = new Hashtable();
3854        VariableAccess[] piLs = new VariableAccess[ call.args.size() ];
3855        for(int i=0; i<spec.dmd.args.size(); i++) {
3856          GenericVarDecl pi = spec.dmd.args.elementAt(i);
3857          piLs[i] = (VariableAccess)pt.get( pi );
3858          temporaries.addElement( piLs[i].decl );
3859          /* non_null pragmas are handled by desugaring now
3860             SimpleModifierPragma nonnull = null; // GetSpec.NonNullPragma(pi); 
3861             if (nonnull != null && !pi.id.toString().equals("this$0arg")) {
3862             Expr argRaw = argsRaw.elementAt(i);
3863             nullCheck(argRaw, call.args.elementAt(i),
3864             argRaw.getStartLoc(),
3865             TagConstants.CHKNONNULL, nonnull.getStartLoc());
3866             }
3867          */
3868          argsMap.put(pi,piLs[i]);
3869          code.addElement(GC.gets(piLs[i], call.args.elementAt(i)));
3870        }
3871    
3872        if (spec.dmd.isConstructor()) {
3873          code.addElement(GC.gets(GC.resultvar, eod));
3874        }
3875    
3876        for (int i=0; i<spec.preAssumptions.size(); ++i) {
3877          addAssumption(spec.preAssumptions.elementAt(i));
3878        }
3879    
3880        // check all preconditions
3881        for(int i=0; i<spec.pre.size(); i++) {
3882          Condition cond = spec.pre.elementAt(i);
3883          int label = cond.label;
3884          Expr p = cond.pred;
3885          if (cond.label == TagConstants.CHKPRECONDITION) {
3886            p = mapLocation(p,locOpenParen);
3887            label = TagConstants.CHKQUIET;
3888          }
3889          addCheck(locOpenParen,
3890                   label,
3891                   GC.subst( call.scall, call.ecall, pt, p ),
3892                   cond.locPragmaDecl);
3893        }
3894    
3895        // Add a check that all the locations that might be assigned by the callee
3896        // are allowed to be assigned by the caller
3897        DerivedMethodDecl calledSpecs = GetSpec.getCombinedMethodDecl(rd);
3898        frameHandler.modifiesCheckMethodI(calledSpecs.modifies,
3899                             eod, locOpenParen, pt,freshResult, rd.parent);
3900    
3901        if (inline != null && Main.options().traceInfo > 0) {
3902          // add a label to say that a routine is being called
3903          GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall,
3904                                           "Call", call.scall);
3905          code.addElement(g);
3906        }
3907    
3908    
3909        // var w*@L = w in
3910        for(Enumeration e = spec.preVarMap.keys(); e.hasMoreElements(); )
3911          {
3912            GenericVarDecl w = (GenericVarDecl)e.nextElement();
3913            VariableAccess wPre = (VariableAccess)spec.preVarMap.get(w);
3914            VariableAccess wL = (VariableAccess)pt.get( wPre.decl );
3915            Assert.notNull( wL );
3916            VariableAccess wAccess = VariableAccess.make( w.id, call.scall, w );
3917                
3918            temporaries.addElement( wL.decl );
3919            code.addElement( GC.gets( wL, wAccess ) );
3920          }
3921    
3922        // restore original checking of warnings
3923        NoWarn.useGlobalStatus = useGlobalStatus;
3924    
3925    
3926        if (inline != null) {
3927    
3928          // insert the translated body, with appropriate substitutions of
3929          // formals for the new names provided above
3930          Translate trInline = new Translate();
3931          trInline.inlineCheckDepth = inline.nextInlineCheckDepth;
3932          trInline.inlineDepthPastCheck = inline.nextInlineDepthPastCheck;
3933    
3934          // turn off body checks if the appropriate flag is set
3935          globallyTurnOffChecks(inline.dontCheckInlinedBody);
3936    
3937          GuardedCmd body = trInline.trBody(rd, scope, null, predictedSynTargs,
3938                                            this, this.issueCautions);
3939          body = substituteGC(pt, body);
3940          code.addElement(body);
3941    
3942          for (int i=0; i<spec.postAssumptions.size(); ++i) {
3943            addAssumption(spec.postAssumptions.elementAt(i));
3944          }
3945    
3946          // check all postconditions
3947          for(int i=0; i<spec.post.size(); i++) {
3948            Condition cond = spec.post.elementAt(i);
3949            if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) continue;
3950            addCheck(rd.getEndLoc(),
3951                     cond.label,
3952                     GC.subst( call.scall, call.ecall, pt, cond.pred),
3953                     cond.locPragmaDecl);
3954          }
3955          if (Main.options().traceInfo > 1) {
3956            // add a label to say that the inlined call has returned
3957            GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall,
3958                                             "CallReturn", call.scall);
3959            code.addElement(g);
3960          }
3961          // restore original checking of warnings
3962          NoWarn.useGlobalStatus = useGlobalStatus;
3963        }
3964    
3965        else {
3966          Type savedType = GC.thisvar.decl.type;
3967    
3968          // We need to evaluate all of the expressions in the
3969          // modifies clauses before we set the locations that are
3970          // in the modifies clauses to arbitrary values, since
3971          // some of the expressions might also be modified.
3972          // For example, a clause might be modifies i,a[i];
3973          // We don't try to see what expressions are modified;
3974          // we simply translate all of them, assigning the results
3975          // to some temporary variables.  Those temporary variables
3976          // are then used later.
3977          
3978          // For each item in the modifies clauses we add 0 or more
3979          // items to the translations and locations lists.  Later
3980          // we iterate over the modifies clauses again, in precisely
3981          // the same order - being sure to take off EXACTLY the same
3982          // items as we put on, for each kind of entry in the modifies 
3983          // clause.
3984    /*      System.out.println("ARGS " );
3985          { java.util.Iterator im = argsMap.keySet().iterator();
3986          while (im.hasNext()) {
3987            Object o = im.next();
3988            System.out.println("ITEM " + o + " ::: " + argsMap.get(o));
3989          }
3990          }*/
3991          Expr thisTrans = eod;
3992     /*     System.out.println("THISTRSANS");
3993          if (thisTrans != null) EscPrettyPrint.inst.print(System.out,0,thisTrans);
3994          System.out.println("");*/
3995          LinkedList translations = new LinkedList();
3996          LinkedList locations = new LinkedList();
3997          ModifiesGroupPragmaVec mgpv = calledSpecs.modifies;
3998          for (int i=0; i<mgpv.size(); ++i) {
3999            GC.thisvar.decl.type = TypeSig.getSig(calledSpecs.getContainingClass());
4000            ModifiesGroupPragma mgp = mgpv.elementAt(i);
4001            Expr precondition = mgp.precondition;
4002            precondition = TrAnExpr.trSpecExpr(precondition,argsMap,argsMap,eod);
4003            codevec = GuardedCmdVec.make();
4004            Frame.ModifiesIterator iter = new Frame.ModifiesIterator(
4005                                                  rd.parent,mgp.items,true,true);
4006            while (iter.hasNext()) {
4007              Object o = iter.next();
4008              if (o instanceof FieldAccess) {
4009                FieldAccess fa = (FieldAccess)o;
4010                //System.out.println("FIELD ACCESS " + fa + " " + Location.toString(fa.getStartLoc()) + " " + Location.toString(fa.decl.getStartLoc()));
4011                Expr b = TrAnExpr.trSpecExpr(fa,argsMap,argsMap,eod);
4012                if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.SELECT) {
4013                  // instance fields
4014                  NaryExpr n = (NaryExpr)b;
4015                  translations.add(n.exprs.elementAt(0));
4016                  translations.add(cacheValue(n.exprs.elementAt(1)));
4017                  locations.add(new Integer(fa.getStartLoc()));
4018                } else if (b instanceof VariableAccess) {
4019                  // static fields
4020                  translations.add(b);
4021                  translations.add(null);
4022                  locations.add(new Integer(fa.getStartLoc()));
4023                } else if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.METHODCALL) {
4024                  // model variable - skip
4025                  translations.add(null);
4026                } else {
4027                  translations.add(null);
4028                  // FIXME - turn into an internal error
4029                  System.out.println("UNSPPORTRED-EB " + b.getClass() + " " + TagConstants.toString(((NaryExpr)b).op));
4030                  escjava.ast.EscPrettyPrint.inst.print(System.out,0,b);
4031                  System.out.println("");
4032                }
4033              } else if (o instanceof ArrayRefExpr) {
4034                // array elements like a[i]
4035                ArrayRefExpr arr = (ArrayRefExpr)o;
4036                Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans);
4037                Expr index = arr.index == null ? GC.zerolit :
4038                  TrAnExpr.trSpecExpr(arr.index,argsMap,argsMap,thisTrans);
4039                translations.add(cacheValue(a));
4040                locations.add(new Integer(arr.getStartLoc()));
4041                translations.add(cacheValue(index));
4042              } else if (o instanceof ArrayRangeRefExpr){
4043                // array ranges like a[i..j] or a[*]
4044                ArrayRangeRefExpr arr = (ArrayRangeRefExpr)o;
4045                Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans);
4046                Expr low = arr.lowIndex == null ? GC.zerolit :
4047                  TrAnExpr.trSpecExpr(arr.lowIndex,argsMap,argsMap,thisTrans);
4048                Expr hi = arr.highIndex == null ? 
4049                    GC.nary(TagConstants.INTEGRALSUB,GC.nary(TagConstants.ARRAYLENGTH,a),GC.onelit) :
4050                      TrAnExpr.trSpecExpr(arr.highIndex,argsMap,argsMap,thisTrans);
4051                translations.add(cacheValue(a));
4052                translations.add(cacheValue(low));
4053                translations.add(cacheValue(hi));
4054              } else if (o instanceof NothingExpr) {
4055                // skip
4056              } else if (o instanceof EverythingExpr) {
4057                // skip
4058              } else if (o instanceof WildRefExpr) {
4059                // store refs like a.* or this.* or Type.* or super.*
4060                // skip - the wildref expression is expanded into
4061                // all of the fields by the iterator
4062              } else {
4063                // FIXME - turn into internal error
4064                System.out.println("UNSUPPORTED " + o.getClass());
4065              }
4066            }
4067            
4068            GC.thisvar.decl.type = savedType; // FIXME - put in finally clause?
4069            
4070            // An assignment generated for each modified target
4071            // of the form   i:7.19 = after@16.2:20.19
4072            
4073            // Here we handle special variables like alloc and state
4074            for (int ii=0; ii<spec.specialTargets.size(); ii++) {
4075              Expr target = spec.specialTargets.elementAt(ii);
4076              GuardedCmd gc = modify(target, pt, scall);
4077              
4078              if (gc != null) codevec.addElement(gc); 
4079            }
4080            
4081            // Here we set everything in the modifies clauses to
4082            // unspecified values.  For instance, for simple variables
4083            // we add the command: i:7.19 = after@16.2:20.19
4084            // There is nothing specified about the after variables.
4085            iter = new Frame.ModifiesIterator(rd.parent,mgp.items,true,true);
4086            while (iter.hasNext()) {
4087              Object o = iter.next();
4088              if (o instanceof FieldAccess) {
4089                VariableAccess a = (VariableAccess)translations.removeFirst();
4090                  if (a != null) {
4091                    Expr obj = (Expr)translations.removeFirst();
4092                    // if obj == null, the variable is static
4093                    int loc = ((Integer)(locations.removeFirst())).intValue();
4094                    VariableAccess newVal = 
4095                      temporary("after@" + UniqName.locToSuffix(scall),
4096                        loc, loc);
4097                    GuardedCmd g = obj != null ?
4098                        GC.subgets(a, obj, newVal ) :
4099                        GC.gets(a, newVal);
4100                    codevec.addElement(g);
4101                  }
4102              } else if (o instanceof ArrayRefExpr) {
4103                Expr a = (Expr)translations.removeFirst();
4104                Expr index = (Expr)translations.removeFirst();
4105                int loc = ((Integer)(locations.removeFirst())).intValue();
4106                VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(scall),
4107                    loc, loc);
4108                GuardedCmd g = GC.subsubgets(GC.elemsvar, a, index, newVal);
4109                codevec.addElement(g);
4110              } else if (o instanceof ArrayRangeRefExpr){
4111                // This one is slightly different.  The array a is
4112                // replaced by a new array unset(a,low,hi).
4113                // In the background predicate, unset(a,i,j) has the
4114                // same array elements as a, except for values between
4115                // i and j, inclusive.
4116                Expr a = (Expr)translations.removeFirst();
4117                Expr low = (Expr)translations.removeFirst();
4118                Expr hi = (Expr)translations.removeFirst();
4119                GuardedCmd g = GC.subgets(GC.elemsvar, a, GC.nary(TagConstants.UNSET, GC.select(GC.elemsvar,a), low, hi));
4120                codevec.addElement(g);
4121              } else if (o instanceof NothingExpr) {
4122                // skip
4123              } else if (o instanceof EverythingExpr) {
4124                // FIXME !!!
4125              } else if (o instanceof WildRefExpr) {
4126                // skip - the wildref expression is expanded into
4127                // all of the fields by the iterator
4128              } else {
4129                // FIXME - turn into an internal error
4130                System.out.println("UNSUPPORTED " + o.getClass());
4131              }
4132            }
4133            GuardedCmd seq = GC.seq(codevec);
4134            GuardedCmd ifcmd = GC.ifcmd(precondition,seq,GC.skip());
4135            code.addElement(ifcmd);
4136          }
4137    
4138          if (spec.modifiesEverything) {
4139            EverythingLoc el = new EverythingLoc(scall,pt);
4140            modifyEverythingLocations.add(el);
4141            el.completed.add(GC.ecvar);
4142            el.completed.add(GC.resultvar);
4143            el.completed.add(GC.xresultvar);
4144            code.addElement(el.gcseq);
4145            Iterator iter = spec.postconditionLocations.iterator();
4146            while (iter.hasNext()) {
4147              Object o = iter.next();
4148              if (o instanceof Expr) el.add((Expr)o);
4149              else System.out.println("WHAT? " + o.getClass() + " " + o);
4150              // FIXME
4151            }
4152                    
4153          }
4154    
4155          // modify EC, RES, XRES
4156          code.addElement(modify(GC.ecvar, scall));
4157          if (!spec.dmd.isConstructor()) {
4158            if (freshResult) code.addElement(GC.gets(GC.resultvar, eod));
4159            else {
4160              code.addElement(modify(GC.resultvar, scall));
4161            }
4162          }
4163          code.addElement(modify(GC.xresultvar, scall));
4164    
4165          // FIXME - we might be doing statevar twice - once
4166          // up above before the assignments of after values to
4167          // all the items in the modifies clause
4168          if (!Utils.isPure(rd))
4169            code.addElement(modify(GC.statevar, scall));
4170                                                     
4171          for (int i=0; i<spec.postAssumptions.size(); ++i) {
4172            addAssumption(spec.postAssumptions.elementAt(i));
4173          }
4174    
4175          // FIXME - do we need this - I think we already do it
4176          // FIXME - figure out why this needs Exception instead of Throwable
4177    
4178          addAssumption(
4179            GC.or(
4180              GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_return),
4181              GC.and(
4182                GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_throw),
4183                GC.nary(TagConstants.TYPELE,
4184                  GC.nary(TagConstants.TYPEOF,GC.xresultvar),
4185                  GC.typeExpr( 
4186                      Main.options().useThrowable ?
4187                         Types.javaLangThrowable() : Types.javaLangException() )
4188                )
4189              )
4190            )
4191          );
4192    
4193          // assume postconditions
4194          Condition exceptionCondition = null;
4195          for(int i=0; i<spec.post.size(); i++) {
4196            Condition cond = spec.post.elementAt(i);
4197            if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION) {
4198              continue;
4199            }
4200            if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) {
4201              exceptionCondition = cond;
4202              continue;
4203            }
4204            code.addElement(GC.assumeAnnotation(cond.locPragmaDecl,
4205                                                GC.subst(call.scall, call.ecall,
4206                                                         pt, cond.pred)));
4207          }
4208          if (exceptionCondition != null &&
4209                NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2) == 
4210                                                 TagConstants.CHK_AS_ASSERT) {
4211            Condition cond = exceptionCondition;
4212            int loc = rd.locThrowsKeyword;
4213            if (loc == Location.NULL) loc = rd.getStartLoc();
4214            addCheck(call.scall,
4215                     TagConstants.CHKUNEXPECTEDEXCEPTION2,
4216                     GC.subst( call.scall, call.ecall, pt, cond.pred),
4217                     loc);
4218          }
4219        }
4220        
4221        if( spec.dmd.throwsSet != null && spec.dmd.throwsSet.size() != 0 ) {        
4222          // #if (! superOrSiblingConstructorCall)
4223          //   assume EC == ec$return [] assume EC == ec$throw; raise
4224          // #else
4225          //   assume EC == ec$return []
4226          //   assume EC == ec$throw; assume !isAllocated(objectToBeConstructed, alloc); raise
4227          // #end
4228    
4229          code.push();
4230          code.addElement( GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return )));
4231            
4232          code.push();
4233          if (Main.options().traceInfo > 0) {
4234            // add a label to track whether the method invocation throws an
4235            // exception
4236            GuardedCmd g = traceInfoLabelCmd(scall, ecall,
4237                                             "RoutineException", scall);
4238            code.addElement(g);
4239          }  
4240          GuardedCmd cmd = GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw ));
4241          code.addElement( cmd );
4242            
4243          if (superOrSiblingConstructorCall) {
4244            Expr isAllocated = GC.nary(TagConstants.ISALLOCATED,
4245                                       GC.objectTBCvar, GC.allocvar);
4246            code.addElement(GC.assume(GC.not(isAllocated)));
4247          }
4248          code.addElement( GC.raise() );
4249            
4250          code.addElement( GC.boxPopFromStackVector(code) );
4251        }
4252        
4253        // extract code and temporaries created, and put into call.desugared
4254        
4255        call.desugared = DynInstCmd.make(UniqName.locToSuffix(call.scall), spill());
4256    
4257        // all done
4258        return call;
4259      }
4260    
4261      /**
4262       *  Computes the inlining settings for a given call.  A return value of
4263       * <code>null</code> means "don't inline".
4264       */
4265      private InlineSettings computeInlineSettings(/*@ non_null */ RoutineDecl rd,
4266                                                   /*@ non_null */ ExprVec argsRaw,
4267                                                   InlineSettings inline,
4268                                                   int scall) {
4269        // Try to use the given inline settings, but bag out if the routine
4270        // doesn't have a body
4271        if (inline != null) {
4272          if (rd.body == null) {
4273            // if we don't have the routine's body, we can't inline it
4274            // (does this ever happen? --jbs)
4275            if (this.issueCautions) {
4276              ErrorSet.caution(scall, "Couldn't inline call because the routine's body was not found");
4277            }
4278            return null;
4279          }
4280          // TBW:  should there be a check for isRecursiveInvocation here?
4281          return new InlineSettings(inline,
4282                                    inlineCheckDepth, inlineDepthPastCheck);
4283        }
4284    
4285        if (rd.body == null) {
4286          return null;
4287        }
4288    
4289        // Set the inlining bits appropriately, according to any given "helper"
4290        // pragma, but only if this is a non-recursive call.
4291        if (Helper.isHelper(rd) && !isRecursiveInvocation(rd)) {
4292          return new InlineSettings(false, false, true,
4293                                    inlineCheckDepth, inlineDepthPastCheck);
4294        }
4295    
4296        // Set the inlining bits appropriately, according to the
4297        // flag -inlineFromConstructors.
4298        if (Main.options().inlineFromConstructors && inConstructorContext &&
4299            !isRecursiveInvocation(rd)) {
4300          // inline if "rd" is an instance method in the same class as rdCurrent
4301          if (rd instanceof MethodDecl && !Modifiers.isStatic(rd.modifiers) &&
4302              rd.parent == rdCurrent.parent) {
4303            // ...and the method is not overridable
4304            if (!FlowInsensitiveChecks.isOverridable((MethodDecl)rd)) {
4305              // ...and the method is clearly being invoked on the "this" object
4306              Assert.notFalse(1 <= argsRaw.size());  // it's an instance method!
4307              VarInit e0 = argsRaw.elementAt(0);
4308              e0 = trim(e0);
4309              if (e0.getTag() == TagConstants.THISEXPR &&
4310                  ((ThisExpr)e0).classPrefix == null) {
4311                // inline it!
4312                return new InlineSettings(false, false, true,
4313                                          inlineCheckDepth, inlineDepthPastCheck);
4314              }
4315            }
4316          }
4317        }
4318    
4319        // Set the inlining bits appropriately, according to the two
4320        // inlining depth flags.
4321        // Also set the inlining depth flags for the next level appropriately.
4322        // We don't inline constructors because of problems with checking
4323        // the constructor for Object.
4324        if ((inlineCheckDepth > 0 || inlineDepthPastCheck > 0) &&
4325            rd instanceof MethodDecl && rd.body != null) {
4326    
4327          InlineSettings is = new InlineSettings(true, true, true,
4328                                                 inlineCheckDepth,
4329                                                 inlineDepthPastCheck);
4330          if (inlineCheckDepth > 1) {
4331            // don't check anything until we've reached the check depth
4332            is.nextInlineCheckDepth--;
4333          } else if (inlineCheckDepth == 1) {
4334            // check the body at the check depth
4335            is.dontCheckInlinedBody = false;
4336            is.getSpecForInline = false;
4337            is.nextInlineCheckDepth--;
4338          } else if (inlineCheckDepth == 0) {
4339            // check the preconditions of calls from the check depth
4340            is.dontCheckPreconditions = false;
4341            is.nextInlineCheckDepth--;
4342            is.nextInlineDepthPastCheck--;
4343          } else {
4344            // don't check anything lower than the check depth
4345            is.nextInlineDepthPastCheck--;
4346          }
4347    
4348          return is;
4349        }
4350    
4351        // don't inline
4352        return null;
4353      }
4354    
4355      /**
4356       * If the flag is true, set all assertion checks to assumes.  Otherwise, make
4357       * sure that regular checking of assertions is performed.
4358       */
4359      public static void globallyTurnOffChecks(boolean flag) {
4360        if (flag) {
4361          // turn precondition checks into assumes
4362          NoWarn.useGlobalStatus = true;
4363          NoWarn.globalStatus = TagConstants.CHK_AS_ASSUME;
4364        }
4365        else
4366          NoWarn.useGlobalStatus = false;
4367      }
4368    
4369      /**
4370       * When a call is inlined, we need to substitute the new names given to its
4371       * formal parameters for its original names in the inlined body. 
4372       */
4373      private static GuardedCmd substituteGC(/*@ non_null */ Hashtable pt, 
4374                                             /*@ non_null */ GuardedCmd gc) {
4375        int tag = gc.getTag();
4376        switch (tag) {
4377        case TagConstants.SKIPCMD:
4378        case TagConstants.RAISECMD:
4379          return gc;
4380        case TagConstants.ASSERTCMD:
4381        case TagConstants.ASSUMECMD:
4382          {
4383            ExprCmd exprcmd = (ExprCmd) gc;
4384            return ExprCmd.make(exprcmd.cmd,
4385                                Substitute.doSubst(pt, exprcmd.pred),
4386                                exprcmd.loc);
4387          }
4388        case TagConstants.GETSCMD:
4389          {
4390            GetsCmd getscmd = (GetsCmd) gc;
4391            return GetsCmd.make((VariableAccess) 
4392                                Substitute.doSubst(pt, getscmd.v),
4393                                Substitute.doSubst(pt, getscmd.rhs));
4394          }
4395        case TagConstants.SUBGETSCMD:
4396          {
4397            SubGetsCmd sgetscmd = (SubGetsCmd) gc;
4398            return SubGetsCmd.make((VariableAccess) 
4399                                   Substitute.doSubst(pt, sgetscmd.v),
4400                                   Substitute.doSubst(pt, sgetscmd.rhs),
4401                                   Substitute.doSubst(pt, sgetscmd.index));
4402          }
4403        case TagConstants.SUBSUBGETSCMD:
4404          {
4405            SubSubGetsCmd ssgetscmd = (SubSubGetsCmd) gc;
4406            return SubSubGetsCmd.make((VariableAccess)
4407                                      Substitute.doSubst(pt, ssgetscmd.v),
4408                                      Substitute.doSubst(pt, ssgetscmd.rhs),
4409                                      Substitute.doSubst(pt, ssgetscmd.index1),
4410                                      Substitute.doSubst(pt, ssgetscmd.index2));
4411          }
4412        case TagConstants.RESTOREFROMCMD:
4413          {
4414            RestoreFromCmd rfcmd = (RestoreFromCmd) gc;
4415            return RestoreFromCmd.make((VariableAccess)
4416                                       Substitute.doSubst(pt, rfcmd.v),
4417                                       Substitute.doSubst(pt, rfcmd.rhs));
4418          }
4419        case TagConstants.SEQCMD:
4420          {
4421            SeqCmd scmd = (SeqCmd) gc;
4422            int size = scmd.cmds.size();
4423            GuardedCmdVec vec = GuardedCmdVec.make(size);
4424            for (int i = 0; i < size; i++)
4425              vec.addElement(substituteGC(pt, scmd.cmds.elementAt(i)));
4426            return SeqCmd.make(vec);
4427          }
4428        case TagConstants.VARINCMD: 
4429          {
4430            VarInCmd vicmd = (VarInCmd) gc;
4431            return GC.block(vicmd.v, substituteGC(pt, vicmd.g));
4432          }
4433        case TagConstants.DYNINSTCMD: 
4434          {
4435            DynInstCmd dc = (DynInstCmd) gc;
4436            return DynInstCmd.make(dc.s, substituteGC(pt, dc.g));
4437          }
4438        case TagConstants.TRYCMD:
4439        case TagConstants.CHOOSECMD:
4440          {
4441            CmdCmdCmd cccmd = (CmdCmdCmd) gc;
4442            return CmdCmdCmd.make(cccmd.cmd,
4443                                  substituteGC(pt, cccmd.g1),
4444                                  substituteGC(pt, cccmd.g2));
4445          }
4446        case TagConstants.CALL: 
4447          {
4448            Call call = (Call) gc;
4449            int size = call.args.size();
4450            ExprVec vec = ExprVec.make(size);
4451            for (int i = 0; i < size; i++)
4452              vec.addElement(Substitute.doSubst(pt, 
4453                                                call.args.elementAt(i)));
4454            Call res = Call.make(vec, call.scall, call.ecall, 
4455                                 call.inlined);
4456            res.desugared = substituteGC(pt, call.desugared);
4457            res.rd = call.rd;
4458            res.spec = call.spec;
4459            return res;
4460          }
4461        case TagConstants.LOOPCMD: 
4462          {
4463            LoopCmd lcmd = (LoopCmd) gc;
4464            LoopCmd res = GC.loop(lcmd.locStart, lcmd.locEnd, lcmd.locHotspot, 
4465                                  lcmd.oldmap,
4466                                  lcmd.invariants, lcmd.decreases,
4467                                  lcmd.skolemConstants, lcmd.predicates, 
4468                                  lcmd.tempVars, lcmd.guard,
4469                                  lcmd.body);
4470            res.desugared = substituteGC(pt, lcmd.desugared);
4471            return res;
4472          }
4473        default:
4474          //@ unreachable;
4475          Assert.fail("Unknown kind of guarded command encountered");
4476          return null;
4477        }
4478      }
4479    
4480      /**
4481       * Destructively change the trace labels in <code>gc</code> to insert sequence
4482       * numbers that are used by the ErrorMsg class in printing trace labels in the
4483       * correct execution order.  This method requires that trace labels do not yet
4484       * contain sequence numbers.
4485       */
4486      public static void addTraceLabelSequenceNumbers(/*@ non_null */ GuardedCmd gc) {
4487        // order the body's trace labels by execution order
4488        if (Main.options().traceInfo > 0) {
4489          orderTraceLabels(gc, 0);
4490        }
4491      }
4492    
4493      /**
4494       * Walk through the guarded command translation of a method, adding unique number
4495       * to its location sequence, in order to sort trace labels in order of execution.
4496       * This is a destructive operation.
4497       */
4498      private static int orderTraceLabels(/*@ non_null */ GuardedCmd gc, int count) {
4499        int tag = gc.getTag();
4500        switch (tag) {
4501        case TagConstants.SKIPCMD:
4502        case TagConstants.RAISECMD:
4503        case TagConstants.ASSERTCMD:
4504        case TagConstants.GETSCMD:
4505        case TagConstants.SUBGETSCMD:
4506        case TagConstants.SUBSUBGETSCMD:
4507        case TagConstants.RESTOREFROMCMD:
4508          return count;
4509        case TagConstants.ASSUMECMD:
4510          {
4511            Expr pred = ((ExprCmd) gc).pred;
4512            if (pred.getTag() == TagConstants.LABELEXPR) {
4513              LabelExpr le = (LabelExpr) pred;
4514              count = orderTraceLabel(le, count);
4515            }
4516            return count;
4517          }
4518        case TagConstants.SEQCMD:
4519          {
4520            SeqCmd scmd = (SeqCmd) gc;
4521            int size = scmd.cmds.size();
4522            for (int i = 0; i < size; i++)
4523              count = orderTraceLabels(scmd.cmds.elementAt(i), count);
4524            return count;
4525          }
4526        case TagConstants.VARINCMD: 
4527          {
4528            VarInCmd vicmd = (VarInCmd) gc;
4529            return orderTraceLabels(vicmd.g, count);
4530          }
4531        case TagConstants.DYNINSTCMD: 
4532          {
4533            DynInstCmd dc = (DynInstCmd) gc;
4534            return orderTraceLabels(dc.g, count);
4535          }
4536        case TagConstants.TRYCMD:
4537        case TagConstants.CHOOSECMD:
4538          {
4539            CmdCmdCmd cccmd = (CmdCmdCmd) gc;
4540            count = orderTraceLabels(cccmd.g1, count);
4541            return orderTraceLabels(cccmd.g2, count);
4542          }
4543        case TagConstants.CALL: 
4544          {
4545            Call call = (Call) gc;
4546            return orderTraceLabels(call.desugared, count);
4547          }
4548        case TagConstants.LOOPCMD: 
4549          {
4550            LoopCmd lcmd = (LoopCmd) gc;
4551            return orderTraceLabels(lcmd.desugared, count);
4552          }
4553        default:
4554          //@ unreachable;
4555          Assert.fail("Unknown kind of guarded command encountered");
4556          return -1;
4557        }
4558      }
4559    
4560      /**
4561       * If the given label is a trace label, add the <code>count</code> number to the
4562       * given label expression's label name, so that trace labels will sort correctly.
4563       */
4564      private static int orderTraceLabel(/*@ non_null */ LabelExpr le, int count) {
4565        String name = le.label.toString();
4566        if (ErrorMsg.isTraceLabel(name)) {
4567          // check that we aren't touching a label that has already had a
4568          // number prefixed to it
4569          Assert.notFalse(name.indexOf(",") == -1);
4570          int k = name.indexOf("^");
4571          Assert.notFalse(k != -1);
4572          name = name.substring(0, k+1) + String.valueOf(count) + "," +
4573            name.substring(k+1);
4574          le.label = Identifier.intern(name);
4575          count++;
4576        }
4577            
4578        return count;
4579      }
4580    
4581    
4582      /***************************************************
4583       *                                                 *
4584       * Generating temporary variables:                   *
4585       *                                                 *
4586       ***************************************************/
4587    
4588      /**
4589       * Countains the number of temporaries generated for the method currently being
4590       * translated.
4591       *
4592       * <p> Reset to 0 on entry to {@link #trExpr(boolean, VarInit)}.
4593       */
4594      private int tmpcount;
4595    
4596      /**
4597       * Generate a temporary for the result of a given expression.
4598       *
4599       * <p> This partially implements ESCJ 23b, case 6.
4600       */
4601      private VariableAccess fresh(/*@ non_null */ VarInit e, int loc) {
4602        return fresh(e, loc, null);
4603      }
4604    
4605      private VariableAccess fresh(/*@ non_null */ VarInit e, int loc, String suffix) {
4606        String name = "tmp" + tmpcount++;
4607        if (suffix != null) {
4608          name += "!" + suffix;
4609        }
4610        return temporary(name, e.getStartLoc(), loc);
4611      }
4612    
4613      /**
4614       * Generate a temporary variable with prefix <code>s</code> and associated
4615       * expression location information <code>locAccess</code>.
4616       */
4617      private VariableAccess temporary(String s, int locAccess) {
4618        return temporary(s, locAccess, Location.NULL);
4619      }
4620    
4621      private VariableAccess temporary(String s, int locAccess, int locIdDecl) {
4622        // As per ESCJ 23b, case 6, we do not use locId:
4623        if (locIdDecl == Location.NULL) {
4624          locIdDecl = UniqName.temporaryVariable;
4625        }
4626    
4627        Identifier idn = Identifier.intern(s);
4628        VariableAccess result = GC.makeVar(idn, locIdDecl);
4629        temporaries.addElement(result.decl);
4630        result.loc = locAccess;
4631    
4632        return result;
4633      }
4634    
4635      public static Expr mapLocation(Expr e, int loc) {
4636        int tag = e.getTag();
4637        switch (tag) {
4638        case TagConstants.LABELEXPR:
4639          LabelExpr le = (LabelExpr)e;
4640          String s = le.label.toString();
4641          if (s.indexOf('@') != -1) return e;
4642          return LabelExpr.make(le.sloc,le.eloc,le.positive,
4643                                Identifier.intern(
4644                                                  s+"@"+UniqName.locToSuffix(loc)),
4645                                le.expr);
4646        case TagConstants.BOOLOR:
4647        case TagConstants.BOOLAND:
4648        case TagConstants.BOOLANDX:
4649          ExprVec ev = ExprVec.make();
4650          NaryExpr ne = (NaryExpr)e;
4651          ExprVec evo = ne.exprs;
4652          for (int k=0; k<evo.size(); ++k) {
4653            Expr ex = evo.elementAt(k);
4654            ex = mapLocation(ex,loc);
4655            ev.addElement(ex);
4656          }
4657          return NaryExpr.make(ne.sloc, ne.eloc, ne.op,
4658                               ne.methodName, ev);
4659        default:
4660          return e;
4661        }
4662      }
4663    
4664      public ArrayList modifyEverythingLocations = new ArrayList();
4665    
4666      public class EverythingLoc {
4667        public int loc;
4668        public Hashtable pt;
4669        public SeqCmd gcseq = SeqCmd.make(GuardedCmdVec.make());
4670        public Set completed = new Set();
4671        public EverythingLoc(int loc, Hashtable pt) {
4672          this.loc = loc;
4673          this.pt = pt;
4674        }
4675        public void add(Expr e) {
4676          if (e instanceof VariableAccess) {
4677            if (completed.contains( ((VariableAccess)e).decl )) return;
4678            completed.add( ((VariableAccess)e).decl );
4679          }
4680          GuardedCmd gc = modify(e, pt, loc);
4681          if (gc != null) gcseq.cmds.addElement(gc);
4682        }
4683      }
4684    
4685      public void addMoreLocations(java.util.Set s) {
4686        Iterator ii = modifyEverythingLocations.iterator();
4687        while (ii.hasNext()) {
4688          EverythingLoc ev = (EverythingLoc)ii.next();
4689          Iterator i = s.iterator();
4690          while (i.hasNext()) {
4691            Object o = i.next();
4692            ev.add((Expr)o);
4693          }
4694        }
4695      }
4696    
4697      // Changes all BOOLANDX operations to BOOLIMPLIES, in place
4698      static void setop(ASTNode e) {
4699        if (e instanceof NaryExpr) {
4700          NaryExpr ne = (NaryExpr)e;
4701          if (ne.getTag() == TagConstants.BOOLANDX) {
4702            ne.op = TagConstants.BOOLIMPLIES;
4703          }
4704        }
4705        int n = e.childCount();
4706        for (int i = 0; i<n; ++i) {
4707          Object o = e.childAt(i);
4708          if (o != null && o instanceof ASTNode) setop((ASTNode)o);
4709        }
4710      }
4711     
4712      public Expr addNewString(VarInit x, Expr left, Expr right) {
4713        // Construct variables
4714        VariableAccess result= fresh(x, x.getStartLoc(), "newString!");
4715        VariableAccess newallocvar= adorn(GC.allocvar);
4716            
4717        ExprVec ev = ExprVec.make(5);
4718        ev.addElement(result);
4719        ev.addElement(left);
4720        ev.addElement(right);
4721        ev.addElement(GC.allocvar); 
4722        ev.addElement(newallocvar);
4723            
4724        Expr newstring = GC.nary(x.getStartLoc(), x.getEndLoc(),
4725                                 TagConstants.STRINGCATP, ev);
4726            
4727        // Emit the Assume and a Gets commands
4728        code.addElement(GC.assume(newstring));
4729        code.addElement(GC.gets(GC.allocvar, newallocvar));
4730            
4731        return result;  // FIXME - we are omitting the protect, which I don't understand
4732      }
4733        
4734      public static class Strings {
4735        static Map map = new HashMap();
4736        static private int count = 0;
4737        static Integer intern(String s) {
4738          Object o = map.get(s);
4739          if (o != null) return ((Integer)o);
4740          Integer i = new Integer(++count);
4741          map.put(s,i);
4742          return i;
4743        }
4744      }
4745    
4746      private GuardedCmdVec codevec;
4747      private Identifier cacheVar = Identifier.intern("modCache");
4748    
4749      public VariableAccess cacheValue(Expr e) {
4750        VariableAccess va = GC.makeVar(cacheVar, e.getStartLoc());
4751        codevec.addElement(GC.gets(va, e));
4752        return va;
4753      }
4754    } // end of class Translate
4755    
4756    // FIXME - translation of model vars is handled for set, assume, assert, ghost decls
4757    // But still need to do so for other types of statement pragmas
4758    // Also need to do so for quantified expresssions.
4759    // What about for old expressions?
4760    
4761    /*
4762     * Local Variables:
4763     * Mode: Java
4764     * fill-column: 85
4765     * End:
4766     */