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    }