    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