    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003
    004    package escjava.translate;
    005
    006    import java.util.Hashtable;
    007    import java.util.Enumeration;
    008    import javafe.ast.*;
    009    import javafe.tc.*;
    010    import javafe.util.Location;
    011    import javafe.util.Assert;
    012    import javafe.util.Info;
    013    import javafe.util.StackVector;
    014    import escjava.ast.*;
    015    import escjava.ast.TagConstants;
    016    import escjava.tc.Types;
    017    import escjava.Main;
    018
    019    public final class GC {
    020
    021      //// Makers for guarded commands
    022
    023      //@ ensures \result != null;
    024      public static GuardedCmd block(/*@ non_null @*/ GenericVarDeclVec v,
    025                                     /*@ non_null @*/ GuardedCmd g)
    026      {
    027        if (v.size() == 0)
    028          return g;
    029        else
    030          return VarInCmd.make(v, g);
    031      }
    032
    033      //@ ensures \result != null;
    034      public static GuardedCmd blockL(Stmt label, GuardedCmd g) {
    035        return trycmd(g, ifcmd( nary(TagConstants.ANYEQ,
    036                                     ecvar,
    037                                     symlit(label, "L_")),
    038                                skip(),
    039                                raise()));
    040      }
    041
    042      /** Requires <code>0 < cmds.size()</code>. */
    043      public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
    044                                   /*@ non_null @*/ GuardedCmd g2)
    045        { GuardedCmd[] cvec= {g1,g2};
    046          return seq(GuardedCmdVec.make(cvec)); }
    047
    048      public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
    049                                   /*@ non_null @*/ GuardedCmd g2,
    050                                   /*@ non_null @*/ GuardedCmd g3 )
    051        { GuardedCmd[] cvec= {g1,g2,g3};
    052          return seq(GuardedCmdVec.make(cvec)); }
    053
    054      public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
    055                                   /*@ non_null @*/ GuardedCmd g2,
    056                                   /*@ non_null @*/ GuardedCmd g3,
    057                                   /*@ non_null @*/ GuardedCmd g4 )
    058        { GuardedCmd[] cvec= {g1,g2,g3,g4};
    059          return seq(GuardedCmdVec.make(cvec)); }
    060
    061      /** May mutilate contents of <code>cmds</code>.  The caller is expected
    062        * not to use <code>cmds</code> after this call.
    063        **/
    064
    065      //@ ensures \result != null;
    066      public static GuardedCmd seq(/*@ non_null */ GuardedCmdVec cmds) {
    067        int n;
    068        if (!Main.options().peepOptGC) {
    069          n = cmds.size();
    070        } else {
    071          n = 0;
    072          LOOP: for (int i = 0; i < cmds.size(); i++) {
    073            GuardedCmd g = cmds.elementAt(i);
    074            int tag = g.getTag();
    075            switch (tag) {
    076              case TagConstants.SKIPCMD:
    077                // don't keep (that is, don't copy and don't increment "n"
    078                break;
    079
    080              case TagConstants.RAISECMD:
    081                cmds.setElementAt(g, n);
    082                n++;
    083                // don't keep any further commands, since they won't
    084                // be reached anyway
    085                break LOOP;
    086
    087              case TagConstants.ASSERTCMD:
    088              case TagConstants.ASSUMECMD:
    089                {
    090                  cmds.setElementAt(g, n);
    091                  n++;
    092                  if ((tag != TagConstants.ASSERTCMD ||
    093                       !Main.options().noPeepOptGCAssertFalse) &&
    094                      isFalse(((ExprCmd)g).pred)) {
    095                    // don't keep any further commands, since they won't
    096                    // be reached anyway
    097                    break LOOP;
    098                  }
    099                  break;
    100                }
    101
    102              default:
    103                cmds.setElementAt(g, n);
    104                n++;
    105                break;
    106            }
    107          }
    108        }
    109        if (n == 0)
    110          return SimpleCmd.make(TagConstants.SKIPCMD, Location.NULL);
    111        if (n == 1)
    112          return cmds.elementAt(0);
    113        for (int elementsToBeRemoved = cmds.size() - n;
    114             elementsToBeRemoved != 0; elementsToBeRemoved--) {
    115          cmds.pop();
    116        }
    117        return SeqCmd.make(cmds);
    118      }
    119
    120      //@ ensures \result != null;
    121      public static GuardedCmd gets(/*@ non_null @*/ VariableAccess lhs,
    122                                    /*@ non_null @*/ Expr rhs) {
    123        return GetsCmd.make(lhs, rhs);
    124      }
    125
    126      //@ ensures \result != null;
    127      public static GuardedCmd subgets(/*@ non_null @*/ VariableAccess lhs,
    128                                       /*@ non_null @*/ Expr index,
    129                                       /*@ non_null @*/ Expr rhs) {
    130        return SubGetsCmd.make(lhs, rhs, index);
    131      }
    132
    133      //@ ensures \result != null;
    134      public static GuardedCmd subsubgets(/*@ non_null @*/ VariableAccess lhs,
    135                                          /*@ non_null @*/ Expr array,
    136                                          /*@ non_null @*/ Expr index,
    137                                          /*@ non_null @*/ Expr rhs) {
    138        return SubSubGetsCmd.make(lhs, rhs, array, index);
    139      }
    140
    141      //@ ensures \result != null;
    142      public static GuardedCmd restoreFrom(/*@ non_null @*/ VariableAccess lhs,
    143                                           /*@ non_null @*/ Expr rhs) {
    144        return RestoreFromCmd.make(lhs, rhs);
    145      }
    146
    147      //@ ensures \result != null;
    148      public static GuardedCmd raise() {
    149        return SimpleCmd.make(TagConstants.RAISECMD, Location.NULL);
    150      }
    151
    152      //@ ensures \result != null;
    153      public static GuardedCmd skip() {
    154        return SimpleCmd.make(TagConstants.SKIPCMD, Location.NULL);
    155      }
    156
    157      public static LoopCmd loop(int sLoop, int eLoop, int locHotspot,
    158                                 /*@ non_null @*/ Hashtable oldmap,
    159                                 /*@ non_null @*/ ConditionVec J,
    160                                 /*@ non_null @*/ DecreasesInfoVec decs,
    161                                 /*@ non_null @*/ LocalVarDeclVec skolemConsts,
    162                                 /*@ non_null @*/ ExprVec P,
    163                                 /*@ non_null @*/ GenericVarDeclVec tempVars,
    164                                 /*@ non_null @*/ GuardedCmd B,
    165                                 /*@ non_null @*/ GuardedCmd S) {
    166        return LoopCmd.make(sLoop, eLoop, locHotspot, oldmap, J, decs,
    167                            skolemConsts, P, tempVars, B, S);
    168      }
    169
    170      //@ ensures \result != null;
    171      public static GuardedCmd ifcmd(/*@ non_null @*/ Expr t,
    172                                     /*@ non_null @*/ GuardedCmd c,
    173                                     /*@ non_null @*/ GuardedCmd a)
    174      {
    175        GuardedCmd thn = GC.seq(GC.assume(t), c);
    176        GuardedCmd els = GC.seq(GC.assumeNegation(t), a);
    177        return choosecmd(thn, els);
    178      }
    179
    180      /** Pops two command sequences off <code>s</code>, call them <code>a</code>
    181          and <code>b</code>.  Then returns the box composition of these
    182          commands, that is, <code>a [] b</code>. */
    183
    184      //@ ensures \result != null;
    185      public static GuardedCmd boxPopFromStackVector(/*@ non_null @*/ StackVector s) {
    186        GuardedCmdVec b = GuardedCmdVec.popFromStackVector(s);
    187        GuardedCmdVec a = GuardedCmdVec.popFromStackVector(s);
    188        return choosecmd(GC.seq(a), GC.seq(b));
    189      }
    190
    191      //@ ensures \result != null;
    192      public static GuardedCmd choosecmd(/*@ non_null @*/ GuardedCmd a,
    193                                         /*@ non_null @*/ GuardedCmd b)
    194      {
    195        if (Main.options().peepOptGC) {
    196          if (a.getTag() == TagConstants.ASSUMECMD && isFalse(((ExprCmd)a).pred)) {
    197            return b;
    198          }
    199          if (b.getTag() == TagConstants.ASSUMECMD && isFalse(((ExprCmd)b).pred)) {
    200            return a;
    201          }
    202          if (a.getTag() == TagConstants.ASSERTCMD && isFalse(((ExprCmd)a).pred)) {
    203            return a;
    204          }
    205          if (b.getTag() == TagConstants.ASSERTCMD && isFalse(((ExprCmd)b).pred)) {
    206            return b;
    207          }
    208        }
    209        return CmdCmdCmd.make(TagConstants.CHOOSECMD, a, b);
    210      }
    211
    212      //@ ensures \result != null;
    213      public static GuardedCmd trycmd(/*@ non_null @*/ GuardedCmd c,
    214                                      /*@ non_null @*/ GuardedCmd a) {
    215        if (Main.options().peepOptGC) {
    216          if (a.getTag() == TagConstants.RAISECMD) {
    217            return c;
    218          }
    219          // It would be nice to do the following:
    220          //     if (!canRaise(c)) {
    221          //       return c;
    222          //     }
    223          // but we don't keep track of the possible outcomes of expressions,
    224          // and thus we'd end up spending quadratic time.  Instead, we do:
    225          switch (c.getTag()) {
    226            case TagConstants.SKIPCMD:
    227              return c;
    228
    229            case TagConstants.RAISECMD:
    230              return a;
    231
    232            case TagConstants.GETSCMD:
    233            case TagConstants.SUBGETSCMD:
    234            case TagConstants.SUBSUBGETSCMD:
    235            case TagConstants.RESTOREFROMCMD:
    236            case TagConstants.ASSERTCMD:
    237            case TagConstants.ASSUMECMD:
    238              return c;
    239
    240            default:
    241              break;
    242          }
    243        }
    244        return CmdCmdCmd.make(TagConstants.TRYCMD, c, a);
    245      }
    246
    247      /** Returns <code>true</code> when <code>e</code> is a boolean
    248        * literal expression whose value is <code>b</code>.
    249        **/
    250      public static boolean isBooleanLiteral(/*@ non_null */ Expr e, boolean b) {
    251        if (e.getTag() == TagConstants.BOOLEANLIT) {
    252          LiteralExpr le = (LiteralExpr)e;
    253          if (le.value != null) {
    254            Boolean bb = (Boolean)le.value;
    255            return bb.booleanValue() == b;
    256          }
    257        } else if( e.getTag() == TagConstants.BOOLNOT) {
    258            return isBooleanLiteral( ((NaryExpr)e).exprs.elementAt(0), !b );
    259        }
    260        return false;
    261      }
    262
    263      /** Returns <code>true</code> only if <code>e</code> represents an
    264        * expression equivalent to <code>false</code>.  This method may
    265        * return <code>false</code> under any circumstance, but tries to
    266        * use cheap methods to figure out whether <code>e</code> is equivalent
    267        * to <code>false</code>, in which case <code>true</code> is returned.
    268        **/
    269
    270      public static boolean isFalse(/*@ non_null @*/ Expr e) {
    271        // first strip off any Simplify label
    272        while (e.getTag() == TagConstants.LABELEXPR) {
    273          LabelExpr le = (LabelExpr)e;
    274          e = le.expr;
    275        }
    276
    277        return isBooleanLiteral(e, false);
    278      }
    279
    280     /** Creates an assert, assume, or skip command, depending on
    281         the kind of given error name and locations, and depending on what
    282         checks are enabled where.  There are two versions of the
    283         <code>check</code> method.
    284
    285         In the first version, <code>errorName</code> is the error name
    286         (that is, the tag constant of the type of check), <code>pred</code>
    287         evaluates to <code>false</code> if the check goes wrong,
    288         <code>locUse</code> is the source location of the command or
    289         expression that can go wrong, and <code>locPragmaDecl</code> is
    290         the location of the associated pragma, if any (or <code>Location.NULL</code>
    291         if not applicable).
    292
    293         In the second version, <code>errorName</code>, <code>pred</code>,
    294         and <code>locPragmaDecl</code> are taken from the components of the
    295         given condition <code>cond</code>.  */
    296
    297      //@ ensures \result != null;
    298      public static GuardedCmd check(int locUse,
    299                                     int errorName,
    300                                     /*@ non_null @*/ Expr pred,
    301                                     int locPragmaDecl) {
    302        return check(locUse, errorName, pred, locPragmaDecl, null);
    303      }
    304
    305      //@ ensures \result != null;
    306      public static GuardedCmd check(int locUse,
    307                                     int errorName,
    308                                     /*@ non_null @*/ Expr pred,
    309                                     int locPragmaDecl,
    310                                     /*@ non_null @*/ Object aux) {
    311            return check(locUse,errorName, pred, locPragmaDecl, Location.NULL,aux);
    312      }
    313
    314      //@ ensures \result != null;
    315      public static GuardedCmd check(int locUse,
    316                                     int errorName,
    317                                     /*@ non_null @*/ Expr pred,
    318                                     int locPragmaDecl,
    319                                     int auxLoc,
    320                                     /*@ non_null @*/ Object aux) {
    321        //Assert.notFalse(locUse != Location.NULL);
    322        if (Main.options().guardedVC && locPragmaDecl != Location.NULL) {
    323          pred = GuardExpr.make(pred, locPragmaDecl);
    324        }
    325        switch( NoWarn.getChkStatus( errorName, locUse, locPragmaDecl) ) {
    326        case TagConstants.CHK_AS_ASSUME:
    327          LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
    328          return assume(pred);
    329        case TagConstants.CHK_AS_ASSERT:
    330          LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
    331          return assertPredicate(locUse, errorName, pred, locPragmaDecl, auxLoc, aux);
    332        case TagConstants.CHK_AS_SKIP:
    333          return skip();
    334        default:
    335          Assert.fail("unreachable");
    336          return null; // dummy return
    337        }
    338
    339      }
    340
    341
    342      /** See description of <code>check</code> above. */
    343
    344      //@ ensures \result != null;
    345      public static GuardedCmd check(int locUse, /*@ non_null @*/ Condition cond) {
    346        Assert.notFalse(locUse != Location.NULL);
    347        return check(locUse, cond.label, cond.pred, cond.locPragmaDecl, null);
    348      }
    349
    350      /** See description of <code>check</code> above. */
    351
    352      //@ ensures \result != null;
    353      public static GuardedCmd check(int locUse,
    354                                     /*@ non_null @*/ Condition cond,
    355                                     /*@ non_null @*/ Object aux)
    356      {
    357        Assert.notFalse(locUse != Location.NULL);
    358        return check(locUse, cond.label, cond.pred, cond.locPragmaDecl, aux);
    359      }
    360
    361      //@ requires label != TagConstants.CHKFREE;
    362      //@ ensures \result != null;
    363      public static Condition condition(int label,
    364                                        /*@ non_null @*/ Expr pred,
    365                                        int locPragmaDecl) {
    366        Assert.notFalse(label != TagConstants.CHKFREE);
    367        return Condition.make(label, pred, locPragmaDecl);
    368      }
    369
    370      //@ ensures \result != null;
    371      public static Condition freeCondition(/*@ non_null @*/ Expr pred, int locPragmaDecl) {
    372        return Condition.make(TagConstants.CHKFREE, pred, locPragmaDecl);
    373      }
    374
    375      //@ ensures \result != null;
    376      public static Condition assumeCondition(/*@ non_null @*/ Expr pred, int locPragmaDecl) {
    377        return Condition.make(TagConstants.CHKASSUME, pred, locPragmaDecl);
    378      }
    379
    380      //@ requires locPragmaDecl != Location.NULL;
    381      //@ ensures \result != null;
    382      public static GuardedCmd assumeAnnotation(int locPragmaDecl,
    383                                                /*@ non_null */ Expr p) {
    384        if (Main.options().guardedVC && locPragmaDecl != Location.NULL) {
    385          p = GuardExpr.make(p, locPragmaDecl);
    386        }
    387        LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
    388        return assume(p);
    389      }
    390
    391      //@ ensures \result != null;
    392      public static GuardedCmd assume(/*@ non_null @*/ Expr p)
    393      {
    394        if (Main.options().peepOptGC && isBooleanLiteral(p, true)) {
    395          return skip();
    396        }
    397        if (p.getTag() == TagConstants.BOOLAND && (p instanceof NaryExpr)
    398               && ((NaryExpr)p).exprs.size() > 1) {
    399           // An optimization that makes ASSUME commands simpler - unpacks an AND
    400           // into multiple ASSUMEs to make reading easier.
    401            NaryExpr ne = (NaryExpr)p;
    402            GuardedCmdVec gcv = GuardedCmdVec.make(ne.exprs.size());
    403            for (int i=0; i<ne.exprs.size(); ++i) {
    404              Expr e = ne.exprs.elementAt(i);
    405              ExprCmd a = ExprCmd.make(TagConstants.ASSUMECMD, e, Location.NULL);
    406              gcv.addElement(a);
    407            }
    408            return GC.seq(gcv);
    409        }
    410        if (p.getTag() == TagConstants.FORALL && (p instanceof QuantifiedExpr)) {
    411          // This is an optimization that changes a Forall of a boolean and into
    412          // a sequence of foralls of the conjuncts.
    413          QuantifiedExpr qe = (QuantifiedExpr)p;
    414          if (qe.expr.getTag() == TagConstants.BOOLAND) {
    415            ExprVec ev = ((NaryExpr)qe.expr).exprs;
    416            if (ev.size() > 1) {
    417              GuardedCmdVec gcv = GuardedCmdVec.make(ev.size());
    418              for (int i=0; i<ev.size(); ++i) {
    419                Expr e =  QuantifiedExpr.make(qe.sloc,qe.eloc,qe.quantifier,
    420                             qe.vars,qe.rangeExpr,ev.elementAt(i),qe.nopats,qe.pats);
    421                ExprCmd a = ExprCmd.make(TagConstants.ASSUMECMD, e, Location.NULL);
    422                gcv.addElement(a);
    423              }
    424              return GC.seq(gcv);
    425            }
    426          }
    427        }
    428        return ExprCmd.make(TagConstants.ASSUMECMD, p, Location.NULL);
    429      }
    430
    431      //@ ensures \result != null;
    432      public static GuardedCmd assumeNegation(/*@ non_null @*/ Expr p) {
    433        Expr non_p = not(p.getStartLoc(), p.getEndLoc(), p);
    434        return assume(non_p);
    435      }
    436
    437      //@ ensures \result != null;
    438      public static GuardedCmd fail() {
    439        return assume(falselit);
    440      }
    441
    442      private static int assertContinueCounter = 0;
    443
    444    //  //@ requires locUse != Location.NULL;
    445    //  private static GuardedCmd assertPredicate(int locUse,
    446    //                                            int errorName, Expr pred,
    447    //                                            int locPragmaDecl,
    448    //                                            Object aux) {
    449    //      return assertPredicate(locUse, errorName, pred, locPragmaDecl,
    450    //              Location.NULL, aux);
    451    //  }
    452
    453      //@ ensures \result != null;
    454      private static GuardedCmd assertPredicate(int locUse,
    455                                                int errorName,
    456                                                /*@ non_null @*/ Expr pred,
    457                                                int locPragmaDecl,
    458                                                int auxLoc,
    459                                                /*@ non_null @*/ Object aux) {
    460        if (Main.options().assertContinue) {
    461          Identifier idn = Identifier.intern("assertContinue" +
    462                                             assertContinueCounter);
    463          assertContinueCounter++;
    464          VariableAccess acVar = makeVar(idn, locUse);
    465          acVar.loc = Location.NULL;
    466          pred = or(pred, acVar);
    467        }
    468        if (errorName != TagConstants.CHKQUIET) {
    469            String name = TagConstants.toString(errorName);
    470            if (aux != null && Main.options().suggest) {
    471              int n = AuxInfo.put(aux);
    472              name += "/" + n;
    473            }
    474            Identifier en = makeLabel(name,locPragmaDecl,auxLoc,locUse);
    475            pred = LabelExpr.make(locUse, locUse, false, en, pred);
    476        }
    477        return ExprCmd.make(TagConstants.ASSERTCMD, pred, locUse);
    478      }
    479
    480      //@ ensures \result != null;
    481      public static Identifier makeLabel(/*@ non_null @*/ String name,
    482                                         int locPragmaDecl, int auxLoc, int locUse) {
    483            String lab = name;
    484            if (locPragmaDecl != Location.NULL) {
    485                lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl);
    486            }
    487            if (auxLoc != Location.NULL) {
    488                lab = lab + ":" + UniqName.locToSuffix(auxLoc);
    489            }
    490            if (locUse != Location.NULL)
    491                lab += "@" + UniqName.locToSuffix(locUse);
    492            return Identifier.intern(lab);
    493      }
    494
    495      //@ ensures \result != null;
    496      public static Identifier makeLabel(/*@ non_null @*/ String name,
    497                                         int locPragmaDecl, int locUse) {
    498            String lab = name;
    499            if (locPragmaDecl != Location.NULL) {
    500                lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl);
    501            }
    502            if (locUse != Location.NULL)
    503                lab += "@" + UniqName.locToSuffix(locUse);
    504            return Identifier.intern(lab);
    505      }
    506
    507      //@ ensures \result != null;
    508      public static Identifier makeFullLabel(/*@ non_null @*/ String name,
    509                                             int locPragmaDecl, int locUse)
    510      {
    511            String lab = name;
    512            if (locPragmaDecl != Location.NULL) {
    513                lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl,false);
    514            }
    515            if (locUse != Location.NULL)
    516                lab += "@" + UniqName.locToSuffix(locUse,false);
    517            return Identifier.intern(lab);
    518      }
    519
    520      //@ requires subst != null && target != null ;
    521      //+@ requires subst.keyType == \type(GenericVarDecl) ;
    522      //+@ requires subst.elementType <: \type(Expr) ;
    523      public static Expr subst(int sloc, int eloc, Hashtable subst, Expr target)
    524        {
    525          if ( !Main.options().lazySubst ) {
    526            // perform substitution eagerly
    527
    528            return Substitute.doSubst( subst, target );
    529
    530          } else {
    531            // create lazy substitutions
    532
    533            for(Enumeration e = subst.keys(); e.hasMoreElements(); )
    534              {
    535                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
    536                Expr to = (Expr)subst.get( vd );
    537                target = subst(sloc, eloc, vd, to, target);
    538              }
    539            return target;
    540          }
    541        }
    542
    543      //@ requires target != null ;
    544      //@ requires var!=null && val!=null;
    545      public static Expr subst(int sloc, int eloc,
    546                               GenericVarDecl var, Expr val, Expr target) {
    547        if ( !Main.options().lazySubst ) {
    548          // perform substitution eagerly
    549          Hashtable t = new Hashtable();
    550          t.put( var, val );
    551          return subst( sloc, eloc, t, target );
    552        } else {
    553          return SubstExpr.make( sloc, eloc, var, val, target );
    554        }
    555      }
    556
    557      //@ requires target != null ;
    558      //@ requires var != null && val!=null;
    559      public static Expr subst(GenericVarDecl var, Expr val, Expr target) {
    560        return subst( Location.NULL, Location.NULL, var, val, target );
    561      }
    562
    563
    564      //// Makers for literals
    565
    566      public static final /*@ non_null @*/ Expr nulllit =
    567        LiteralExpr.make(TagConstants.NULLLIT, null, Location.NULL);
    568
    569      public static final /*@ non_null @*/ Expr zerolit =
    570        LiteralExpr.make(TagConstants.INTLIT, new Integer(0), Location.NULL);
    571
    572      public static final /*@ non_null @*/ Expr onelit =
    573        LiteralExpr.make(TagConstants.INTLIT, new Integer(1), Location.NULL);
    574
    575      public static final /*@ non_null @*/ Expr truelit =
    576        LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.TRUE,Location.NULL);
    577
    578      public static final /*@ non_null @*/ Expr falselit =
    579        LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.FALSE,Location.NULL);
    580
    581      public static final /*@ non_null @*/ Expr dzerolit =
    582        LiteralExpr.make(TagConstants.DOUBLELIT, new Double(0.0), Location.NULL);
    583
    584      //@ ensures \result != null;
    585      public static Expr symlit(/*null*/ String s) {
    586        return LiteralExpr.make(TagConstants.SYMBOLLIT, s, Location.NULL);
    587      }
    588
    589      //@ ensures \result != null;
    590      public static Expr symlit(/*@ non_null @*/ Stmt s, /*@ non_null @*/ String prefix) {
    591        return symlit(prefix + UniqName.locToSuffix(s.getStartLoc()));
    592      }
    593
    594      //@ ensures \result != null;
    595      public static Expr zeroequiv(/*@ non_null @*/ Type t) {
    596        switch (t.getTag()) {
    597        case TagConstants.ARRAYTYPE:
    598        case TagConstants.NULLTYPE:
    599        case TagConstants.TYPENAME:
    600        case TagConstants.TYPESIG:
    601          return nulllit;
    602
    603        case TagConstants.BOOLEANTYPE:
    604          return falselit;
    605
    606        case TagConstants.INTTYPE:
    607        case TagConstants.LONGTYPE:
    608        case TagConstants.CHARTYPE:
    609        case TagConstants.BYTETYPE:
    610        case TagConstants.SHORTTYPE:
    611          return zerolit;
    612
    613        case TagConstants.DOUBLETYPE:
    614        case TagConstants.FLOATTYPE:
    615          return dzerolit;
    616        }
    617        /*@ unreachable; */
    618        Assert.fail("Bad tag");
    619        return null;
    620      }
    621
    622
    623      //// Makers for variables
    624
    625      //@ ensures \result != null;
    626      public static VariableAccess makeVar(/*@ non_null @*/ Identifier name, int locId) {
    627        LocalVarDecl v
    628          = LocalVarDecl.make(0, null, name, Types.anyType, locId,
    629                              null, Location.NULL);
    630        return VariableAccess.make(name, Location.NULL, v);
    631      }
    632
    633      //@ ensures \result != null;
    634      public static VariableAccess makeVar(/*@ non_null @*/ String name, int locId) {
    635        return makeVar(Identifier.intern(name), locId);
    636      }
    637
    638      //@ ensures \result != null;
    639      public static VariableAccess makeFormalPara(/*@ non_null @*/ String name,
    640                                                  /*@ non_null @*/ Type type,
    641                                                  int locId) {
    642        Identifier nameId = Identifier.intern(name);
    643        FormalParaDecl v
    644          = FormalParaDecl.make(0, null, nameId, type, locId);
    645        return VariableAccess.make( Identifier.intern(name), Location.NULL, v);
    646      }
    647
    648
    649      //@ ensures \result != null;
    650      public static VariableAccess makeVar(/*@ non_null @*/ String name) {
    651        return makeVar(name, Location.NULL);
    652      }
    653
    654      //@ ensures \result != null;
    655      public static VariableAccess makeVar(/*@ non_null @*/ Identifier name) {
    656        return makeVar(name, Location.NULL);
    657      }
    658
    659      //@ ensures \result != null;
    660      public static VariableAccess makeFormalPara(/*@ non_null @*/ String name,
    661                                                  /*@ non_null @*/ Type type) {
    662        return makeFormalPara(name, type, Location.NULL);
    663      }
    664
    665      //@ ensures \result != null;
    666      public static VariableAccess makeFormalPara(/*@ non_null @*/ String name) {
    667        return makeFormalPara(name, Types.anyType);
    668      }
    669
    670
    671      public static final /*@ non_null @*/ VariableAccess allocvar = makeVar("alloc",
    672                                                      UniqName.specialVariable);
    673      public static final /*@ non_null @*/ VariableAccess ecvar = makeVar("EC",
    674                                                   UniqName.specialVariable);
    675      public static final /*@ non_null @*/ VariableAccess elemsvar = makeVar("elems",
    676                                                      UniqName.specialVariable);
    677      public static final /*@ non_null @*/ VariableAccess resultvar = makeVar("RES",
    678                                               UniqName.specialVariable);
    679      public static final /*@ non_null @*/ VariableAccess xresultvar = makeVar("XRES",
    680                                                        UniqName.specialVariable);
    681      public static final /*@ non_null @*/ VariableAccess objectTBCvar = makeVar("objectToBeConstructed",
    682                                                                UniqName.specialVariable);
    683      public static final /*@ non_null @*/ VariableAccess statevar = makeVar("state",
    684                                                      UniqName.specialVariable);
    685
    686      // LSvar is not final because it is temporarily updated at
    687      // synchronized expressions. See trExpr
    688         public static VariableAccess LSvar = makeVar("LS",
    689                                   UniqName.specialVariable);
    690
    691
    692      /*
    693       * The type of thisvar (thisvar.decl.type) is set by
    694       * Translate.trBody.  It is also temporarily changed by
    695       * GetSpec.trMethodDecl.
    696       */
    697      //@ invariant thisvar.decl.type instanceof TypeSig;
    698      public static final /*@ non_null @*/ VariableAccess thisvar =
    699          makeFormalPara("this", javafe.tc.Types.javaLangObject(),
    700                         UniqName.specialVariable);
    701
    702
    703      /*
    704       * These handle case 5 of ESCJ 23b:
    705       */
    706      public static final /*@ non_null @*/ Expr ec_throw = symlit("ecThrow");
    707      public static final /*@ non_null @*/ Expr ec_return = symlit("ecReturn");
    708
    709      //// Makers for expressions
    710
    711      //@ ensures \result != null;
    712      public static Expr typeExpr(/*@ non_null @*/ Type t)
    713        { return TypeExpr.make(Location.NULL, Location.NULL, t); }
    714
    715      public static Expr cast(/*@ non_null @*/ Expr e,
    716                              /*@ non_null @*/ Type t)
    717      {
    718            if (e instanceof LiteralExpr)
    719                    return LiteralExpr.cast((LiteralExpr)e,
    720                            t == Types.doubleType ? TagConstants.DOUBLELIT :
    721                            t == Types.floatType ? TagConstants.FLOATLIT :
    722                            t == Types.longType ? TagConstants.LONGLIT :
    723                                    TagConstants.INTLIT);
    724            return nary(TagConstants.CAST, e, typeExpr(t));
    725      }
    726
    727      // Various forms of nary()
    728
    729      //@ ensures \result != null;
    730      public static Expr nary(int tag, /*@ non_null */ Expr e) {
    731        return nary(Location.NULL, Location.NULL, tag, e);
    732      }
    733
    734      //@ ensures \result != null;
    735      public static Expr nary(int sloc, int eloc, int tag,
    736                              /*@ non_null */ Expr e) {
    737        Expr[] args = { e };
    738        return nary( sloc, eloc, tag, ExprVec.make(args));
    739      }
    740
    741      //@ ensures \result != null;
    742      public static Expr nary(int tag,
    743                              /*@ non_null */ Expr e1, /*@ non_null */ Expr e2) {
    744        return nary(Location.NULL, Location.NULL, tag, e1, e2);
    745      }
    746
    747      //@ ensures \result != null;
    748      public static Expr nary(int sloc, int eloc, int tag,
    749                              /*@ non_null */ Expr e1, /*@ non_null */ Expr e2) {
    750        Expr[] args = { e1, e2 };
    751        return nary(sloc,eloc,tag, ExprVec.make(args));
    752      }
    753
    754      //@ ensures \result != null;
    755      public static Expr nary(int tag, /*@ non_null */ Expr e1,
    756                              /*@ non_null */ Expr e2, /*@ non_null */ Expr e3) {
    757        return nary(Location.NULL, Location.NULL, tag, e1, e2, e3);
    758      }
    759
    760      //@ ensures \result != null;
    761      public static Expr nary(int sloc, int eloc, int tag,
    762                              /*@ non_null */ Expr e1, /*@ non_null */ Expr e2,
    763                              /*@ non_null */ Expr e3) {
    764        Expr[] args = { e1, e2, e3 };
    765        return nary(sloc,eloc,tag, ExprVec.make(args));
    766      }
    767
    768      //@ ensures \result != null;
    769      public static Expr nary(int tag, /*@ non_null @*/ ExprVec ev) {
    770            return nary(Location.NULL, Location.NULL, tag, ev);
    771      }
    772
    773      //@ ensures \result != null;
    774      public static Expr nary(/*@ non_null @*/ Identifier id, /*@ non_null @*/ ExprVec ev) {
    775            Expr e = nary(Location.NULL, Location.NULL, TagConstants.METHODCALL, ev);
    776            ((NaryExpr)e).methodName = id;
    777            return e;
    778      }
    779
    780      //@ ensures \result != null;
    781      public static Expr nary(/*@ non_null @*/ Identifier id, /*@ non_null @*/ Expr e) {
    782            ExprVec ev = ExprVec.make(1);
    783            ev.addElement(e);
    784            return nary(id,ev);
    785    }
    786
    787      //@ ensures \result != null;
    788      public static Expr nary(/*@ non_null @*/ Identifier id,
    789                              /*@ non_null @*/ Expr e1,
    790                              /*@ non_null @*/ Expr e2)
    791      {
    792            ExprVec ev = ExprVec.make(2);
    793            ev.addElement(e1);
    794            ev.addElement(e2);
    795            return nary(id,ev);
    796      }
    797
    798      //@ ensures \result != null;
    799      public static Expr nary(int sloc, int eloc,
    800                              /*@ non_null @*/ Identifier id,
    801                              /*@ non_null @*/ ExprVec ev)
    802      {
    803            Expr e = nary(sloc, eloc, TagConstants.METHODCALL, ev);
    804            ((NaryExpr)e).methodName = id;
    805            return e;
    806      }
    807
    808      //@ ensures \result != null;
    809      public static Expr nary(int sloc, int eloc, int tag,
    810                              /*@ non_null @*/ ExprVec ev)
    811      {
    812        if( Main.options().peepOptE ) {
    813          // Do some optimizations ...
    814
    815          switch( tag ) {
    816            case TagConstants.BOOLAND:
    817            case TagConstants.BOOLANDX:
    818              {
    819                ExprVec w = ExprVec.make( ev.size() );
    820                if( selectiveAdd( w, ev, truelit, falselit,
    821                                  tag ) )
    822                  {
    823                    return falselit;
    824                  }
    825
    826                if( w.size() == 0 )
    827                  return truelit;
    828                else if( w.size() == 1 )
    829                  return w.elementAt(0);
    830                else
    831                  return NaryExpr.make( sloc, eloc, tag, null, w);
    832              }
    833
    834            case TagConstants.BOOLOR:
    835              {
    836                ExprVec w = ExprVec.make( ev.size() );
    837                if( selectiveAdd( w, ev, falselit, truelit,
    838                                  TagConstants.BOOLOR ) )
    839                  {
    840                    return truelit;
    841                  }
    842
    843                if( w.size() == 0 )
    844                  return falselit;
    845                else if( w.size() == 1 )
    846                  return w.elementAt(0);
    847                else
    848                  return NaryExpr.make( sloc, eloc, TagConstants.BOOLOR, null, w);
    849              }
    850
    851            case TagConstants.BOOLIMPLIES:
    852              {
    853                Expr c0 = ev.elementAt(0);
    854                Expr c1 = ev.elementAt(1);
    855
    856                if( Main.options().bubbleNotDown ) {
    857                  return or( sloc, eloc,
    858                             not( sloc, eloc, c0 ),
    859                             c1 );
    860                } else {
    861                    // Change a ==> (b ==> c) to (a ^ b) ==> c
    862                    if(c1.getTag() == TagConstants.BOOLIMPLIES ) {
    863                        NaryExpr ne = (NaryExpr)c1;
    864                        return implies( sloc, eloc,
    865                                        and( sloc, eloc, c0, ne.exprs.elementAt(0) ),
    866                                        ne.exprs.elementAt(1) );
    867                    } else if (isBooleanLiteral(c0, false)) {
    868                    // false ==> X --> true
    869                    return GC.truelit;
    870                  } else if (isBooleanLiteral(c1, true)) {
    871                    // X ==> true --> true
    872                    return GC.truelit;
    873                  } else if (isBooleanLiteral(c0, true)) {
    874                    // true ==> X --> X
    875                    return c1;
    876                  } else if (isBooleanLiteral(c1, false)) {
    877                    // X ==> false --> !X
    878                    return nary(sloc, eloc, TagConstants.BOOLNOT, c0);
    879                  } else {
    880                    break; // go to default case
    881                  }
    882                }
    883              }
    884
    885            case TagConstants.BOOLNOT:
    886              // Change (not (and a b)) -> (or (not a) (not b)), etc
    887              // Also (not (not a)) -> a
    888              {
    889                Expr c0 = ev.elementAt(0);
    890                if (isBooleanLiteral(c0, false)) {
    891                  return truelit;
    892                } else if (isBooleanLiteral(c0, true)) {
    893                  return falselit;
    894                } else if ( c0.getTag() == TagConstants.BOOLNOT ) {
    895                    return ((NaryExpr)c0).exprs.elementAt(0);
    896                } else if( Main.options().bubbleNotDown ) {
    897                  switch( c0.getTag() ) {
    898                  case TagConstants.BOOLOR:
    899                  case TagConstants.BOOLAND:
    900                  case TagConstants.BOOLANDX:
    901                    {
    902                      ExprVec w = ((NaryExpr)c0).exprs;
    903                      ExprVec r = ExprVec.make();
    904                      for(int i=0; i<w.size(); i++) {
    905                        r.addElement( not( sloc, eloc, w.elementAt(i)));
    906                      }
    907                      return nary( sloc, eloc,
    908                                   c0.getTag() == TagConstants.BOOLOR ?
    909                                     TagConstants.BOOLAND : TagConstants.BOOLOR,
    910                                   r );
    911                    }
    912                  }
    913                }
    914
    915                break; // go to default case
    916              }
    917
    918            case TagConstants.ANYEQ:
    919              // Change (ANYEQ a a) -> true
    920              {
    921                  if( ev.size() == 2 &&
    922                      ev.elementAt(0) instanceof VariableAccess &&
    923                      ev.elementAt(1) instanceof VariableAccess &&
    924                      ((VariableAccess)ev.elementAt(0)).decl ==
    925                      ((VariableAccess)ev.elementAt(1)).decl ) {
    926                      return GC.truelit;
    927                  }
    928
    929                  if( ev.size() == 2 &&
    930                      ev.elementAt(0) instanceof LiteralExpr &&
    931                      ev.elementAt(1) instanceof LiteralExpr &&
    932                      ((LiteralExpr)ev.elementAt(0)).value.equals(
    933                             ((LiteralExpr)ev.elementAt(1)).value )) {
    934                      return GC.truelit;
    935                  }
    936
    937                break; // go to default case
    938              }
    939
    940          }
    941        }
    942
    943        // No special case, so do default
    944        return NaryExpr.make(sloc,eloc,tag, null, ev);
    945      }
    946
    947
    948      //// Makers for other GCExpr nodes
    949
    950      //@ ensures \result != null;
    951      public static Expr select(/*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
    952        return nary(TagConstants.SELECT, c0, c1);
    953      }
    954
    955      //@ ensures \result != null;
    956      public static Expr not(/*@ non_null @*/ Expr c) {
    957        return not(Location.NULL, Location.NULL, c);
    958      }
    959
    960      //@ ensures \result != null;
    961      public static Expr not(int sloc, int eloc, /*@ non_null @*/ Expr c) {
    962        return nary(sloc, eloc, TagConstants.BOOLNOT, c);
    963      }
    964
    965      //@ ensures \result != null;
    966      public static Expr and(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
    967        return and(Location.NULL, Location.NULL, c1, c2);
    968      }
    969
    970      //@ ensures \result != null;
    971      public static Expr andx(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
    972        ExprVec es = ExprVec.make(2);
    973        es.addElement(c1);
    974        es.addElement(c2);
    975        return nary(Location.NULL, Location.NULL, TagConstants.BOOLANDX, es);
    976      }
    977
    978      //@ ensures \result != null;
    979      public static Expr and(int sloc, int eloc, /*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
    980        Expr[] es = {c1, c2};
    981        return and( sloc, eloc, ExprVec.make(es) );
    982      }
    983
    984      //@ ensures \result != null;
    985      public static Expr and(/*@ non_null @*/ ExprVec v) {
    986        return and(Location.NULL, Location.NULL, v);
    987      }
    988
    989      //@ ensures \result != null;
    990      public static Expr and(int sloc, int eloc, /*@ non_null @*/ ExprVec v) {
    991        return nary( sloc, eloc, TagConstants.BOOLAND, v );
    992      }
    993
    994      //@ ensures \result != null;
    995      public static Expr or(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
    996        return or(Location.NULL, Location.NULL, c1, c2);
    997      }
    998
    999      //@ ensures \result != null;
    1000      public static Expr or(int sloc, int eloc,
    1001                            /*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
    1002        Expr[] es = {c1, c2};
    1003        return or( sloc, eloc, ExprVec.make(es) );
    1004      }
    1005
    1006      //@ ensures \result != null;
    1007      public static Expr or(/*@ non_null @*/ ExprVec v) {
    1008        return or(Location.NULL, Location.NULL, v);
    1009      }
    1010
    1011      //@ ensures \result != null;
    1012      public static Expr or(int sloc, int eloc, /*@ non_null @*/ ExprVec v) {
    1013        return nary( sloc, eloc, TagConstants.BOOLOR, v );
    1014      }
    1015
    1016      //@ ensures \result != null;
    1017      public static Expr implies(/*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
    1018        return implies( Location.NULL, Location.NULL, c0, c1 );
    1019      }
    1020
    1021      //@ ensures \result != null;
    1022      public static Expr implies(int sloc, int eloc, /*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
    1023        return nary( sloc, eloc, TagConstants.BOOLIMPLIES, c0, c1);
    1024      }
    1025
    1026      //@ ensures \result != null;
    1027      public static Expr forall(/*@ non_null @*/ GenericVarDecl v, /*@ non_null @*/ Expr e) {
    1028        return forall( Location.NULL, Location.NULL, v, GC.truelit, e, null );
    1029      }
    1030
    1031      //@ ensures \result != null;
    1032      public static Expr forall(/*@ non_null @*/ GenericVarDecl v, Expr range, /*@ non_null @*/ Expr e) {
    1033        return forall( Location.NULL, Location.NULL, v, range, e, null );
    1034      }
    1035
    1036      //@ ensures \result != null;
    1037      public static Expr forall(/*@ non_null @*/ GenericVarDeclVec v,
    1038                                /*null?*/ Expr range,
    1039                                /*@ non_null @*/ Expr e)
    1040      {
    1041        return quantifiedExpr( Location.NULL, Location.NULL,
    1042                    TagConstants.FORALL, v, range, e, null, null );
    1043      }
    1044
    1045      //@ ensures \result != null;
    1046      public static Expr forall(/*@ non_null @*/ GenericVarDecl v,
    1047                                /*@ non_null @*/ Expr e,
    1048                                ExprVec nopats)
    1049      {
    1050        return forall( Location.NULL, Location.NULL, v, GC.truelit, e, nopats );
    1051      }
    1052
    1053      //@ ensures \result != null;
    1054      public static Expr forallwithpats(/*@ non_null @*/ GenericVarDecl v,
    1055                                        /*@ non_null @*/ Expr e,
    1056                                        /*@ non_null @*/ ExprVec pats) {
    1057        return quantifiedExpr( Location.NULL, Location.NULL,
    1058                    TagConstants.FORALL, v, GC.truelit, e, null, pats );
    1059      }
    1060
    1061      //@ ensures \result != null;
    1062      public static Expr forall(int sloc, int eloc, /*@ non_null @*/ GenericVarDecl v,
    1063                                Expr range, /*@ non_null @*/ Expr e) {
    1064        return forall(sloc, eloc, v, range, e, null);
    1065      }
    1066
    1067      //@ ensures \result != null;
    1068      public static Expr forall(int sloc, int eloc,
    1069                                /*@ non_null @*/ GenericVarDecl v,
    1070                                Expr range,
    1071                                /*@ non_null @*/ Expr e,
    1072                                ExprVec nopats) {
    1073        Assert.notNull(v);
    1074        Assert.notNull(e);
    1075
    1076        if( Main.options().peepOptE ) {
    1077
    1078          // Change forall (a) ((a==b) ==> e) -> e[b/a] if b a variable
    1079
    1080          if( e.getTag() == TagConstants.BOOLIMPLIES ) {
    1081
    1082            NaryExpr nary = (NaryExpr)e;
    1083            Expr impliesLhs = nary.exprs.elementAt(0);
    1084            Expr impliesRhs = nary.exprs.elementAt(1);
    1085            switch( impliesLhs.getTag() ) {
    1086              case TagConstants.ANYEQ:
    1087              case TagConstants.BOOLEQ:
    1088              case TagConstants.INTEGRALEQ:
    1089              case TagConstants.REFEQ:
    1090              case TagConstants.TYPEEQ:
    1091
    1092                NaryExpr lhsNary = (NaryExpr)impliesLhs;
    1093                Expr eqLhs = lhsNary.exprs.elementAt(0);
    1094                Expr eqRhs = lhsNary.exprs.elementAt(1);
    1095                if( eqLhs.getTag() == TagConstants.VARIABLEACCESS
    1096                    && ((VariableAccess)eqLhs).decl == v
    1097                    && isSimple( eqRhs ))
    1098                  {
    1099                    // Can replace the forall with a substitution
    1100                    return subst( v, eqRhs, impliesRhs );
    1101                  }
    1102            }
    1103          }
    1104        }
    1105
    1106        // could not do the substitution
    1107        return quantifiedExpr(sloc, eloc, TagConstants.FORALL, v, range, e, nopats, null);
    1108      }
    1109
    1110      //@ ensures \result != null;
    1111      public static Expr quantifiedExpr(int sloc, int eloc, int tag,
    1112                                        /*@ non_null @*/ GenericVarDecl v,
    1113                                        Expr range,
    1114                                        /*@ non_null @*/ Expr e,
    1115                                        ExprVec nopats,
    1116                                        ExprVec pats)
    1117        {
    1118          GenericVarDeclVec vs = GenericVarDeclVec.make();
    1119          vs.addElement(v);
    1120          return quantifiedExpr(sloc, eloc, tag, vs, range, e, nopats, pats );
    1121        }
    1122
    1123      //@ ensures \result != null;
    1124      public static Expr quantifiedExpr(int sloc, int eloc, int tag,
    1125                                        /*@ non_null @*/ GenericVarDeclVec vs,
    1126                                        /*null?*/   Expr range,
    1127                                        /*@ non_null @*/ Expr e,
    1128                                        /*null?*/   ExprVec nopats,
    1129                                        /*null?*/   ExprVec pats)
    1130        {
    1131          Assert.notFalse( tag == TagConstants.FORALL
    1132                           || tag == TagConstants.EXISTS );
    1133
    1134          if( tag == TagConstants.FORALL && vs.size() == 0 ) {
    1135              // empty forall
    1136              return e;
    1137          }
    1138
    1139          if( Main.options().peepOptE ) {
    1140
    1141            // change Q(a)Q(b)e -> Q(a b) e, where Q is a quantifier
    1142
    1143            if( e.getTag() == tag ) {
    1144              QuantifiedExpr qe = (QuantifiedExpr)e;
    1145              GenericVarDeclVec copy = vs.copy();
    1146              copy.append( qe.vars );
    1147              if (qe.nopats != null) {
    1148                if (nopats == null) {
    1149                  nopats = qe.nopats;
    1150                } else {
    1151                  nopats = nopats.copy();
    1152                  nopats.append(qe.nopats);
    1153                }
    1154              }
    1155              if (range == null) range = qe.rangeExpr;
    1156              else if (qe.rangeExpr != null) range = GC.and(range,qe.rangeExpr);
    1157              return QuantifiedExpr.make( sloc, eloc, tag, copy,
    1158                                          range, qe.expr,
    1159                                          nopats, qe.pats );
    1160            }
    1161          }
    1162
    1163          // No optimization done
    1164          return QuantifiedExpr.make( sloc, eloc, tag, vs, range, e, nopats, pats );
    1165        }
    1166
    1167      public static boolean isSimple(/*@ non_null @*/ Expr e) {
    1168        switch( e.getTag() ) {
    1169          case TagConstants.VARIABLEACCESS:
    1170          case TagConstants.TYPEEXPR:
    1171          case TagConstants.BOOLEANLIT:
    1172          case TagConstants.CHARLIT:
    1173          case TagConstants.DOUBLELIT:
    1174          case TagConstants.FLOATLIT:
    1175          case TagConstants.INTLIT:
    1176          case TagConstants.LONGLIT:
    1177          case TagConstants.NULLLIT:
    1178          case TagConstants.STRINGLIT:
    1179          case TagConstants.SYMBOLLIT:
    1180            return true;
    1181
    1182          default:
    1183            return false;
    1184        }
    1185      }
    1186
    1187      /**
    1188       * Adds elements to <code>to</code> from <code>from</code>.
    1189       * Elements equal to bot are dropped. If an element equal to top is
    1190       * encountered, true is returned and to is undefined. If top is
    1191       * never encountered, false is returned. If from contains an
    1192       * NaryExpr with tag naryTagMerge, the components of that NaryExpr
    1193       * are treated in a similar manner.
    1194       */
    1195      private static boolean selectiveAdd(/*@ non_null @*/ ExprVec to,
    1196                                          /*@ non_null @*/ ExprVec from,
    1197                                          Expr bot, Expr top, int naryTagMerge)
    1198        {
    1199          for(int i=0; i<from.size(); i++) {
    1200            Expr e = from.elementAt(i);
    1201            if( e == bot ) {
    1202              // drop e
    1203            } else if( e == top ) {
    1204              return true;
    1205            } else if( e.getTag() == naryTagMerge ) {
    1206              ExprVec exprs = ((NaryExpr)e).exprs;
    1207              if( selectiveAdd( to, exprs, bot, top, naryTagMerge ) )
    1208                return true;
    1209            } else {
    1210              // nothing special
    1211              to.addElement(e);
    1212            }
    1213          }
    1214          return false;
    1215        }
    1216
    1217    }