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