001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.translate;
004    
005    
006    import java.util.Hashtable;
007    import java.util.Enumeration;
008    import java.util.Vector;
009    
010    import javafe.ast.*;
011    import escjava.ast.*;
012    import escjava.ast.TagConstants;
013    
014    import javafe.util.*;
015    
016    
017    /**
018     ** Responsible for performing substitutions in expressions.
019     **/
020    
021    
022    public class Substitute {
023    
024      private static class SetRef {  // used by method "doSubst"
025        Set s;
026      }
027    
028      /**
029       ** Does substitution on GCExprs union (resolved) SpecExprs. <p>
030       **
031       ** No SubstExpr's may be contained in e.<p>
032       **/
033    
034      //@ ensures e != null ==> \result != null;
035      public static Expr doSubst(/*@ non_null */ Hashtable subst, Expr e) {
036        if (e == null) {
037            return null;
038        }
039        return doSubst(subst, e, new SetRef());
040      }
041    
042      //@ ensures e != null ==> \result != null;
043      public static Expr doSimpleSubst(/*@ non_null */ Hashtable subst, Expr e) {
044        if (e == null) {
045            return null;
046        }
047        return doSubst(subst, e, null);
048      }
049    
050    
051    
052      /**
053       ** Does substitution on GCExprs union (resolved) SpecExprs. <p>
054       **
055       ** No SubstExpr's may be contained in e.<p>
056       **
057       ** <code>rhsVars</code> refers to a pointer to a Set.  This pointer
058       ** is either null or the set of variables (GenericVarDecl's) occurring
059       ** in right-hand sides of <code>subst</code>.
060       **/
061    
062      //@ modifies rhsVars.s;
063      //@ ensures rhsVars != null ==> \old(rhsVars.s) != null ==> rhsVars.s == \old(rhsVars.s);
064      //@ ensures \result != null;
065      private static Expr doSubst(/*@ non_null */ Hashtable subst, Expr e,
066                                  /*@ non_null */ SetRef rhsVars) {
067        Expr result = null;
068        boolean newInstance = true;
069        switch( e.getTag() ) {
070            
071        /*************************************************************
072         * Cases needed only for SpecExprs:
073         */
074    
075        case TagConstants.WILDREFEXPR: {
076            WildRefExpr w = (WildRefExpr)e;
077            ObjectDesignator newOd = w.od;
078            if (newOd != null &&
079                newOd.getTag() == TagConstants.EXPROBJECTDESIGNATOR) {
080                ExprObjectDesignator eod = (ExprObjectDesignator)newOd;
081                newOd = ExprObjectDesignator.make(eod.locDot,
082                                                  doSubst(subst, eod.expr,rhsVars));
083                ((ExprObjectDesignator)newOd).type = eod.type;
084            }
085    
086            result = WildRefExpr.make(
087                            w.var == null ? null : doSubst(subst,w.var,rhsVars),
088                            newOd);
089            break;
090        }
091    
092        case TagConstants.ARRAYRANGEREFEXPR: {
093            ArrayRangeRefExpr ar = (ArrayRangeRefExpr)e;
094            result = ArrayRangeRefExpr.make(
095                    ar.locOpenBracket,
096                    doSubst(subst,ar.array,rhsVars),
097                    ar.lowIndex == null ? null : doSubst(subst,ar.lowIndex,rhsVars),
098                    ar.highIndex == null ? null : doSubst(subst,ar.highIndex,rhsVars));
099            break;
100        }
101    
102        case TagConstants.ARRAYREFEXPR:
103          {
104            ArrayRefExpr ae = (ArrayRefExpr)e;
105            result = ArrayRefExpr.make(doSubst(subst,ae.array,rhsVars),
106                                       doSubst(subst,ae.index,rhsVars),
107                                       ae.locOpenBracket,
108                                       ae.locCloseBracket);
109            break;
110          }
111    
112        // Code for BinaryExpr is in default case below.
113    
114        case TagConstants.CASTEXPR:
115          {
116            CastExpr ce = (CastExpr)e;
117            result = CastExpr.make(doSubst(subst,ce.expr,rhsVars), ce.type,
118                                   ce.locOpenParen, ce.locCloseParen);
119            break;
120          }
121    
122        case TagConstants.CONDEXPR:
123          {
124            CondExpr ce = (CondExpr)e;
125            result = CondExpr.make(doSubst(subst,ce.test,rhsVars),
126                                   doSubst(subst,ce.thn,rhsVars),
127                                   doSubst(subst,ce.els,rhsVars), ce.locQuestion,
128                                   ce.locColon);
129            break;
130          }
131    
132        case TagConstants.FIELDACCESS:
133          {
134            FieldAccess fa = (FieldAccess)e;
135    
136            ObjectDesignator newOd = fa.od;
137            if (newOd.getTag() == TagConstants.EXPROBJECTDESIGNATOR) {
138                ExprObjectDesignator eod = (ExprObjectDesignator)newOd;
139                newOd = ExprObjectDesignator.make(eod.locDot,
140                                                  doSubst(subst, eod.expr,rhsVars));
141                ((ExprObjectDesignator)newOd).type = eod.type;
142            }
143    
144            FieldAccess newFa = FieldAccess.make(newOd, fa.id, fa.locId);
145            newFa.decl = fa.decl;
146    
147            result = newFa;
148            break;
149          }
150    
151        case TagConstants.INSTANCEOFEXPR:
152          {
153            InstanceOfExpr ioe = (InstanceOfExpr)e;
154            result = InstanceOfExpr.make(doSubst(subst,ioe.expr,rhsVars),
155                                         ioe.type, ioe.loc);
156            break;
157          }
158    
159        case TagConstants.PARENEXPR:
160          {
161            ParenExpr pe = (ParenExpr)e;
162            result = ParenExpr.make(doSubst(subst,pe.expr,rhsVars),
163                                    pe.locOpenParen, pe.locCloseParen);
164            break;
165          }
166    
167        // UnaryExpr cases:
168        case TagConstants.UNARYADD:
169        case TagConstants.UNARYSUB:
170        case TagConstants.NOT:
171        case TagConstants.BITNOT:
172        case TagConstants.INC:
173        case TagConstants.DEC:
174          {
175            UnaryExpr ue = (UnaryExpr)e;
176            result = UnaryExpr.make( ue.op, doSubst(subst,ue.expr,rhsVars), ue.locOp);
177            break;
178          }
179    
180    
181    
182        /*************************************************************
183         * Cases needed for GCExpr's:
184         */
185    
186        case TagConstants.LABELEXPR:
187          {
188            LabelExpr le = (LabelExpr)e;
189            result = LabelExpr.make( le.sloc, le.eloc, le.positive,
190                                     le.label, doSubst(subst,le.expr,rhsVars));
191            break;
192          }
193    
194        case TagConstants.GUARDEXPR:
195          {
196            GuardExpr ge = (GuardExpr)e;
197            result = GuardExpr.make( doSubst( subst, ge.expr, rhsVars ), ge.locPragmaDecl );
198            break;
199          }
200    
201        case TagConstants.NUM_OF:
202          {
203            NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e;
204    
205            // this routine requires that the bound variables of the quantified
206            // expression not occur as left-hand sides of the substitution,
207            // so here's a run-time check of this condition
208            for(int i=0; i<qe.vars.size(); i++) {
209              Assert.notFalse( !subst.contains( qe.vars.elementAt(i) ));
210            }
211    
212            // the routine also requires that the variables in the right-hand
213            // sides of the substitution are not captured by the quantified
214            // expression, so here's a check for that
215            if (rhsVars != null) {
216                if (rhsVars.s == null) {
217                  rhsVars.s = new Set();
218                  for (Enumeration variables = subst.elements(); variables.hasMoreElements(); ) {
219                    Expr ee = (Expr)variables.nextElement();
220                    rhsVars.s.union(freeVars(ee));
221                  }
222                }
223                for (int i = 0; i < qe.vars.size(); i++) {
224                  Assert.notFalse(!rhsVars.s.contains(qe.vars.elementAt(i)));
225                }
226            }
227    
228            ExprVec newNopats;
229            if (qe.nopats == null) {
230              newNopats = null;
231            } else {
232              newNopats = ExprVec.make(qe.nopats.size());
233              for (int i = 0; i < qe.nopats.size(); i++) {
234                newNopats.addElement(doSubst(subst, qe.nopats.elementAt(i), rhsVars));
235              }
236            }
237            result = NumericalQuantifiedExpr.make( qe.sloc, qe.eloc, qe.quantifier,
238                                          qe.vars, 
239                                          qe.rangeExpr == null ? null :
240                                            doSubst(subst,qe.rangeExpr,rhsVars),
241                                          doSubst(subst,qe.expr,rhsVars),
242                                          newNopats);
243            break;
244          }
245        case TagConstants.MAXQUANT:
246        case TagConstants.MIN:
247        case TagConstants.SUM:
248        case TagConstants.PRODUCT:
249          {
250            GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e;
251    
252            // this routine requires that the bound variables of the quantified
253            // expression not occur as left-hand sides of the substitution,
254            // so here's a run-time check of this condition
255            for(int i=0; i<qe.vars.size(); i++) {
256              Assert.notFalse( !subst.contains( qe.vars.elementAt(i) ));
257            }
258    
259            // the routine also requires that the variables in the right-hand
260            // sides of the substitution are not captured by the quantified
261            // expression, so here's a check for that
262            if (rhsVars.s == null) {
263              rhsVars.s = new Set();
264              for (Enumeration variables = subst.elements(); variables.hasMoreElements(); ) {
265                Expr ee = (Expr)variables.nextElement();
266                rhsVars.s.union(freeVars(ee));
267              }
268            }
269            for (int i = 0; i < qe.vars.size(); i++) {
270              Assert.notFalse(!rhsVars.s.contains(qe.vars.elementAt(i)));
271            }
272    
273            ExprVec newNopats;
274            if (qe.nopats == null) {
275              newNopats = null;
276            } else {
277              newNopats = ExprVec.make(qe.nopats.size());
278              for (int i = 0; i < qe.nopats.size(); i++) {
279                newNopats.addElement(doSubst(subst, qe.nopats.elementAt(i), rhsVars));
280              }
281            }
282            result = GeneralizedQuantifiedExpr.make( qe.sloc, qe.eloc, qe.quantifier,
283                              qe.vars, doSubst(subst,qe.expr,rhsVars),
284                                doSubst(subst, qe.rangeExpr,rhsVars),
285                              newNopats);
286            break;
287          }
288        case TagConstants.FORALL:
289        case TagConstants.EXISTS:
290          {
291            QuantifiedExpr qe = (QuantifiedExpr)e;
292    
293            // this routine requires that the bound variables of the quantified
294            // expression not occur as left-hand sides of the substitution,
295            // so here's a run-time check of this condition
296            for(int i=0; i<qe.vars.size(); i++) {
297              Assert.notFalse( !subst.contains( qe.vars.elementAt(i) ));
298            }
299    
300            // the routine also requires that the variables in the right-hand
301            // sides of the substitution are not captured by the quantified
302            // expression, so here's a check for that
303            if (rhsVars != null) {
304                if (rhsVars.s == null) {
305                  rhsVars.s = new Set();
306                  for (Enumeration variables = subst.elements(); variables.hasMoreElements(); ) {
307                    Expr ee = (Expr)variables.nextElement();
308                    rhsVars.s.union(freeVars(ee));
309                  }
310                }
311                for (int i = 0; i < qe.vars.size(); i++) {
312                  Assert.notFalse(!rhsVars.s.contains(qe.vars.elementAt(i)));
313                }
314            }
315    
316            ExprVec newNopats;
317            if (qe.nopats == null) {
318              newNopats = null;
319            } else {
320              newNopats = ExprVec.make(qe.nopats.size());
321              for (int i = 0; i < qe.nopats.size(); i++) {
322                newNopats.addElement(doSubst(subst, qe.nopats.elementAt(i), rhsVars));
323              }
324            }
325    
326            ExprVec newPats;
327            if (qe.pats == null) {
328              newPats = null;
329            } else {
330              newPats = ExprVec.make(qe.pats.size());
331              for (int i = 0; i < qe.pats.size(); i++) {
332                newPats.addElement(doSubst(subst, qe.pats.elementAt(i), rhsVars));
333              }
334            }
335    
336            result = QuantifiedExpr.make( qe.sloc, qe.eloc, qe.quantifier,
337                                          qe.vars, 
338                                          qe.rangeExpr == null ? null :
339                                            doSubst(subst,qe.rangeExpr,rhsVars),
340                                          doSubst(subst,qe.expr,rhsVars),
341                                          newNopats, newPats);
342            break;
343          }
344              
345        case TagConstants.RESEXPR:
346          {
347            newInstance = false;
348            Expr to = (Expr)subst.get( resexpr );
349            result = (to==null ? e : to);
350            break;
351          }
352        case TagConstants.THISEXPR:
353          {
354            newInstance = false;
355            Expr to = (Expr)subst.get( thisexpr );
356            result = (to==null ? e : to);
357            break;
358          }
359        case TagConstants.TYPEEXPR:
360        case TagConstants.LOCKSETEXPR:
361        case TagConstants.CLASSLITERAL:
362    
363        case TagConstants.BOOLEANLIT: 
364        case TagConstants.CHARLIT:
365        case TagConstants.DOUBLELIT: 
366        case TagConstants.FLOATLIT:
367        case TagConstants.INTLIT:
368        case TagConstants.LONGLIT:
369        case TagConstants.NULLLIT:
370        case TagConstants.STRINGLIT:
371        case TagConstants.SYMBOLLIT:
372        case TagConstants.EVERYTHINGEXPR:
373        case TagConstants.NOTHINGEXPR:
374          {
375            newInstance = false;
376            result = e;
377            break;
378          }
379              
380        case TagConstants.NOTMODIFIEDEXPR:
381          {
382            NotModifiedExpr nme = (NotModifiedExpr)e;
383            result = NotModifiedExpr.make(nme.loc, 
384                doSubst(subst, nme.expr, rhsVars));
385            break;
386          }
387    
388        case TagConstants.VARIABLEACCESS:
389          {
390            //newInstance = false;
391            VariableAccess va = (VariableAccess)e;
392            Expr to = (Expr)subst.get( va.decl );
393    
394            if( to != null ) {
395              // System.out.println("Doing subst on "+va.decl.id);
396              result =  to;
397            } else {
398              // System.out.println("Not doing subst on "+va.decl.id + " " + va.decl);
399              result = e;
400              if (va.id == Identifier.intern("RES")) {
401                    to = (Expr)subst.get(resexpr);
402                    if (to != null) result = to;
403              }
404            }
405            break;
406          }
407    
408        default:
409          {
410            if (e instanceof NaryExpr) {
411    
412              NaryExpr ne = (NaryExpr)e;
413              ExprVec nu = ExprVec.make( ne.exprs.size() );
414              for( int i=0; i<ne.exprs.size(); i++ ) {
415                nu.addElement( doSubst( subst, ne.exprs.elementAt(i), rhsVars ) );
416              }
417              result =  NaryExpr.make(ne.sloc, ne.eloc, ne.op, ne.methodName, nu);
418            } else if (e instanceof BinaryExpr) {
419    
420              BinaryExpr be = (BinaryExpr)e;
421              result = BinaryExpr.make(be.op, doSubst(subst,be.left,rhsVars),
422                                       doSubst(subst,be.right,rhsVars), be.locOp);
423            } else if (e instanceof SetCompExpr) {
424              SetCompExpr se = (SetCompExpr)e;
425              // FIXME - how do bound vars affect substitution?
426              return e;
427            } else if (e instanceof MethodInvocation) {
428              MethodInvocation me = (MethodInvocation)e;
429              ExprVec args = ExprVec.make(me.args.size());
430              for (int i = 0; i< me.args.size(); ++i) {
431                    Expr ee = me.args.elementAt(i);
432                    args.addElement( doSubst(subst, ee, rhsVars));
433              }
434              MethodInvocation r = MethodInvocation.make(me.od, me.id, me.tmodifiers, me.locId, 
435                            me.locOpenParen, args);
436              r.decl = me.decl;
437              result = r;
438            } else if (e instanceof NewArrayExpr) {
439              NewArrayExpr me = (NewArrayExpr)e;
440              ArrayInit init = me.init;
441              // FIXME - need substitution
442              //Expr init = doSubst(subst, me.init, rhsVars);
443              result = NewArrayExpr.make(me.type,me.dims,init,
444                            me.loc,me.locOpenBrackets);
445            } else if (e instanceof NewInstanceExpr) {
446              NewInstanceExpr me = (NewInstanceExpr)e;
447              ExprVec args = ExprVec.make(me.args.size());
448              for (int i = 0; i< me.args.size(); ++i) {
449                    Expr ee = me.args.elementAt(i);
450                    args.addElement( doSubst(subst, ee, rhsVars));
451              }
452              Expr ee = me.enclosingInstance;
453              if (ee != null) ee = doSubst(subst, ee, rhsVars);
454              NewInstanceExpr r = NewInstanceExpr.make(ee,
455                            me.locDot, me.type, args, me.anonDecl,
456                            me.loc, me.locOpenParen);
457              r.decl = me.decl;
458              result = r;
459            } else if (e instanceof AmbiguousVariableAccess) {
460              // This will happen if there has been an undefined variable in
461              // another compilation unit.  We ignore it here, rather than
462              // throwing the Assertion failure, in order to continue as 
463              // gracefully as possible.
464              result = e;
465            } else {
466    
467                Assert.fail("Bad expr in Substitute.doSubst: "+e+ " " 
468                                    + Location.toString(e.getStartLoc()));
469                return null; // dummy return
470            }
471          }
472        }
473    
474        if (newInstance) escjava.tc.FlowInsensitiveChecks.copyType(e, result);
475        return result;
476      }
477    
478      final static public Expr resexpr = ResExpr.make(Location.NULL);
479      final static public Expr thisexpr = ThisExpr.make(null,Location.NULL);
480    
481      /**
482       ** Calculate the free variables of an expression or a GuardedCmd. <p>
483       **
484       ** Precondition; e must be resolved, e may not contain FieldAccess as
485       **               a subnode. <p>
486       **
487       ** [mdl: I have checked that this code works with invariants
488       **  translated to Exprs.  I am unsure if it works correctly on
489       **  anything else.]
490       **
491       ** Note: length is not a free variable of translated code.  (It turns
492       ** into applications of the built-in function arrayLength.)
493       **/
494      //@ ensures \result != null;
495      public static Set freeVars(ASTNode e) {
496    
497        CalcFreeVars t = new CalcFreeVars();
498        t.traverse(e);
499        return t.getFreeVars();
500      }
501    
502    
503        public static boolean mentionsFresh(Expr e) {
504            if( e.getTag() == TagConstants.FRESH )
505                return true;
506    
507            for( int i=0; i<e.childCount(); i++ ) {
508                Object o = e.childAt(i);
509                if( o instanceof Expr ) {
510                    if( mentionsFresh( (Expr)o ) )
511                        return true;
512                }
513            }
514    
515            return false;
516        }
517    }
518    
519    
520    class CalcFreeVars {
521      
522      private Set freeVars = new Set();
523      private Vector quantifiedVars = new Vector();  // need a bag
524    
525      Set getFreeVars() {
526        return freeVars;
527      }
528    
529      void traverse(ASTNode e) {
530    
531        GenericVarDeclVec bindings = null;
532        
533        switch( e.getTag() ) {
534    
535          /*
536           * Local/parameter/field variable references:
537           */
538          case TagConstants.AMBIGUOUSVARIABLEACCESS:
539            {
540              Assert.precondition("Unresolved ASTNode passed to freeVars");
541              return;
542            }
543          case TagConstants.VARIABLEACCESS:
544            {
545              VariableAccess va = (VariableAccess)e;
546    
547              if( !quantifiedVars.contains(va.decl) ) {
548                freeVars.add( va.decl );
549              }
550              return;
551            }
552          case TagConstants.FIELDACCESS:
553            {
554    System.out.println("FA " + Location.toString(e.getStartLoc()) + " " + e);
555              Assert.precondition
556                  ("ASTNode with FieldAccess subnode passed to freeVars");
557              break;
558            }
559    
560    
561          /*
562           * Variable binding operators:
563           */
564          case TagConstants.SUBSTEXPR:
565            {
566              GenericVarDecl var = ((SubstExpr)e).var;
567              bindings = GenericVarDeclVec.make();
568              bindings.addElement(var);
569              break;
570            }
571          case TagConstants.FORALL:
572          case TagConstants.EXISTS:
573            {
574              QuantifiedExpr qe = (QuantifiedExpr)e;
575              bindings = qe.vars;
576              break;
577            }
578          case TagConstants.VARINCMD:
579            {
580              VarInCmd c = (VarInCmd)e;
581              bindings = c.v;
582              break;
583            }
584    
585          /*
586           * Need to handle Call's specially:
587           */
588          case TagConstants.CALL:
589            {
590              Call call = (Call)e;
591              // want to include vars in call.desugared
592              // desugared is not considered a child,
593              // so do traversal explicitly
594              traverse( call.desugared );
595              return; // do not look at children
596            }
597        }
598    
599        // Record bound variables
600    
601        if( bindings != null ) {
602          for(int i=0; i<bindings.size(); i++ ) {
603            GenericVarDecl decl = bindings.elementAt(i);
604            quantifiedVars.addElement(  decl );
605          }
606        }
607    
608        // Visit all children
609        
610        for( int i=0; i<e.childCount(); i++ ) {
611          Object o = e.childAt(i);
612          if( o instanceof ASTNode )
613            traverse( (ASTNode)o );
614        }
615    
616        // Remove bound variables from env
617        if( bindings != null ) {
618          for(int i=0; i<bindings.size(); i++ ) {
619            // The following line appears not to be used [KRML, 12 Apr 1999]
620            GenericVarDecl decl = bindings.elementAt(i);
621            quantifiedVars.removeElementAt( quantifiedVars.size()-1 );
622          }
623        }
624        
625        return;
626      }
627    
628    }
629