    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     */