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