001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.ast; 004 005 import java.io.OutputStream; 006 import java.util.Enumeration; 007 import javafe.ast.*; 008 import javafe.util.Assert; 009 import escjava.parser.EscPragmaParser; 010 import escjava.ast.TagConstants; 011 import escjava.ParsedRoutineSpecs; 012 013 public class EscPrettyPrint extends DelegatingPrettyPrint 014 { 015 public EscPrettyPrint() { } 016 017 //@ requires self != null; 018 //@ requires del != null; 019 public EscPrettyPrint(PrettyPrint self, PrettyPrint del) { 020 super(self, del); 021 } 022 023 //@ also 024 //@ requires o != null; 025 //@ requires lp != null; 026 public void print(OutputStream o, LexicalPragma lp) { 027 if (lp.getTag() == TagConstants.NOWARNPRAGMA) { 028 write(o, "//@ "); 029 write(o, TagConstants.toString(TagConstants.NOWARN)); 030 NowarnPragma nwp = (NowarnPragma)lp; 031 for (int i = 0; i < nwp.checks.size(); i++) { 032 if (i == 0) write(o, ' '); 033 else write(o, ", "); 034 write(o, nwp.checks.elementAt(i).toString()); 035 } 036 write(o, "\n"); 037 } else writeln(o, "// Unknown LexicalPragma (tag = " + lp.getTag() + 038 " " + TagConstants.toString(lp.getTag()) + ')'); 039 } 040 041 //@ requires o != null; // note that d can be null 042 public void exsuresPrintDecl(OutputStream o, GenericVarDecl d) { 043 if (d == null) 044 write(o, "<null GenericVarDecl>"); 045 else { 046 self.print(o, d.type); 047 if (!(d.id.equals(TagConstants.ExsuresIdnName))) { 048 write (o, ' '); 049 write(o, d.id.toString()); 050 } 051 } 052 } 053 054 //@ also 055 //@ requires o != null; 056 //@ requires tp != null; 057 public void print(OutputStream o, int ind, TypeDeclElemPragma tp) { 058 int tag = tp.getTag(); 059 int otag = tag; if (tp.isRedundant()) otag = TagConstants.makeRedundant(tag); 060 switch (tag) { 061 case TagConstants.AXIOM: 062 case TagConstants.INVARIANT: 063 case TagConstants.REPRESENTS: 064 case TagConstants.CONSTRAINT: { 065 Expr e = tag == TagConstants.REPRESENTS ? 066 ((NamedExprDeclPragma)tp).expr : 067 ((ExprDeclPragma)tp).expr; 068 write(o, "/*@ "); 069 write(o, TagConstants.toString(otag)); 070 write(o, ' '); 071 self.print(o, ind, e); 072 write(o, "; */"); 073 break; 074 } 075 076 case TagConstants.MODELTYPEPRAGMA: { 077 ModelTypePragma mtp = (ModelTypePragma)tp; 078 write(o, "/*@ model "); 079 self.print(o, ind, mtp.decl); 080 write(o, "@*/"); 081 082 break; 083 } 084 085 case TagConstants.MODELDECLPRAGMA: { 086 FieldDecl d = ((ModelDeclPragma)tp).decl; 087 /* 088 * Below is a "//@" to prevent illegal nested /* ... comments 089 * that otherwise might result from any attached modifier pragmas. 090 * 091 * We rely on the fact that no ESC modifier can generate newlines 092 * when pretty printed. !!!! 093 */ 094 write(o, "//@ model "); 095 self.print(o, ind, d, true); 096 // write(o, " */\n"); 097 write(o, "\n"); 098 break; 099 } 100 101 case TagConstants.GHOSTDECLPRAGMA: { 102 FieldDecl d = ((GhostDeclPragma)tp).decl; 103 /* 104 * Below is a "//@" to prevent illegal nested /* ... comments 105 * that otherwise might result from any attached modifier pragmas. 106 * 107 * We rely on the fact that no ESC modifier can generate newlines 108 * when pretty printed. !!!! 109 */ 110 write(o, "//@ ghost "); 111 self.print(o, ind, d, true); 112 // write(o, " */\n"); 113 write(o, "\n"); 114 break; 115 } 116 case TagConstants.STILLDEFERREDDECLPRAGMA: { 117 Identifier v = ((StillDeferredDeclPragma)tp).var; 118 write(o, "/*@ "); 119 write(o, TagConstants.toString(TagConstants.STILL_DEFERRED)); 120 write(o, " "); 121 write(o,v.toString()); 122 write(o, "; */"); 123 break; 124 } 125 default: 126 write(o, "/* Unknown TypeDeclElemPragma (tag = " + TagConstants.toString(tag) + ") */"); 127 break; 128 } 129 } 130 131 //@ requires o != null; 132 //@ requires v != null; 133 public void print(OutputStream o, int ind, ModifierPragmaVec v) { 134 int n = v.size(); 135 for (int i=0; i<n; ++i) { 136 print(o,ind,v.elementAt(i)); 137 } 138 } 139 140 //@ also 141 //@ requires o != null; 142 //@ requires mp != null; 143 public void print(OutputStream o, int ind, ModifierPragma mp) { 144 int tag = mp.getTag(); 145 switch (tag) { 146 case TagConstants.ALSO: 147 write(o, "/*@ "); 148 write(o, TagConstants.toString(mp.originalTag())); 149 write(o, " */"); 150 break; 151 152 case TagConstants.OPENPRAGMA: 153 writeln(o, "{|"); 154 ++ind; 155 break; 156 157 case TagConstants.CLOSEPRAGMA: 158 --ind; 159 writeln(o, "|}"); 160 break; 161 162 case TagConstants.MODEL_PROGRAM: 163 write(o, "/*@ "); 164 write(o, TagConstants.toString(tag)); 165 write(o, "{...} */"); // FIXME - do all of model program 166 break; 167 168 case TagConstants.ALSO_REFINE: 169 case TagConstants.CODE_BIGINT_MATH: 170 case TagConstants.CODE_CONTRACT: 171 case TagConstants.CODE_JAVA_MATH: 172 case TagConstants.CODE_SAFE_MATH: 173 case TagConstants.END: 174 case TagConstants.EXAMPLE: 175 case TagConstants.EXCEPTIONAL_EXAMPLE: 176 case TagConstants.FOR_EXAMPLE: 177 case TagConstants.HELPER: 178 case TagConstants.IMMUTABLE: 179 case TagConstants.IMPLIES_THAT: 180 case TagConstants.INSTANCE: 181 case TagConstants.MAY_BE_NULL: // Chalin-Kiniry experiements 182 case TagConstants.MONITORED: 183 case TagConstants.NON_NULL: 184 case TagConstants.NON_NULL_REF_BY_DEFAULT: // Chalin-Kiniry experiements 185 case TagConstants.NORMAL_EXAMPLE: 186 case TagConstants.NULL_REF_BY_DEFAULT: // Chalin-Kiniry experiements 187 case TagConstants.OBS_PURE: // Chalin-Kiniry experiements 188 case TagConstants.PEER: // Universe type annotation 189 case TagConstants.PURE: 190 case TagConstants.READONLY: // Universe type annotation 191 case TagConstants.REP: // Universe type annotation 192 case TagConstants.SPEC_BIGINT_MATH: 193 case TagConstants.SPEC_JAVA_MATH: 194 case TagConstants.SPEC_PROTECTED: // SC HPT AAST 3 195 case TagConstants.SPEC_PUBLIC: 196 case TagConstants.SPEC_SAFE_MATH: 197 case TagConstants.UNINITIALIZED: 198 case TagConstants.WRITABLE_DEFERRED: 199 write(o, "/*@ "); 200 write(o, TagConstants.toString(tag)); 201 write(o, " */"); 202 break; 203 204 case TagConstants.GHOST: 205 case TagConstants.MODEL: 206 break; 207 208 case TagConstants.NO_WACK_FORALL: 209 case TagConstants.OLD: 210 write(o, "/*@ "); 211 write(o, TagConstants.toString(tag)); 212 write(o, " */"); 213 LocalVarDecl d = ((VarDeclModifierPragma)mp).decl; 214 self.print(o, ind, d, true); 215 write(o, "; */"); 216 break; 217 218 case TagConstants.ALSO_ENSURES: 219 case TagConstants.ALSO_REQUIRES: 220 case TagConstants.ENSURES: 221 case TagConstants.DIVERGES: 222 case TagConstants.POSTCONDITION: 223 case TagConstants.PRECONDITION: 224 case TagConstants.WHEN: 225 case TagConstants.MONITORED_BY: // from EscPragmaParser.continuePragma(Token) 226 case TagConstants.READABLE_IF: 227 case TagConstants.REQUIRES: 228 case TagConstants.WRITABLE_IF: { 229 write(o, "/*@ "); 230 if (mp.isRedundant()) 231 write(o, TagConstants.toString(TagConstants.makeRedundant(tag))); 232 else 233 write(o, TagConstants.toString(tag)); 234 write(o, ' '); 235 if (!(mp instanceof ExprModifierPragma)) System.out.print("{{{{ " + mp + "}}}}"); 236 Expr e = ((ExprModifierPragma)mp).expr; 237 self.print(o, ind, e); 238 write(o, "; */"); 239 break; 240 } 241 242 // All redundant tokens should not exist in the AST 243 // anymore; they are represented with redundant fields in 244 // the AST nodes. 245 case TagConstants.ASSERT_REDUNDANTLY: 246 case TagConstants.ASSIGNABLE_REDUNDANTLY: 247 case TagConstants.ASSUME_REDUNDANTLY: 248 case TagConstants.CONSTRAINT_REDUNDANTLY: 249 case TagConstants.DECREASES_REDUNDANTLY: 250 case TagConstants.DECREASING_REDUNDANTLY: 251 case TagConstants.DIVERGES_REDUNDANTLY: 252 case TagConstants.DURATION_REDUNDANTLY: 253 case TagConstants.ENSURES_REDUNDANTLY: 254 case TagConstants.EXSURES_REDUNDANTLY: 255 case TagConstants.HENCE_BY_REDUNDANTLY: 256 case TagConstants.INVARIANT_REDUNDANTLY: 257 case TagConstants.LOOP_INVARIANT_REDUNDANTLY: 258 case TagConstants.MAINTAINING_REDUNDANTLY: 259 case TagConstants.MEASURED_BY_REDUNDANTLY: 260 case TagConstants.MODIFIABLE_REDUNDANTLY: 261 case TagConstants.MODIFIES_REDUNDANTLY: 262 case TagConstants.POSTCONDITION_REDUNDANTLY: 263 case TagConstants.PRECONDITION_REDUNDANTLY: 264 case TagConstants.REPRESENTS_REDUNDANTLY: 265 case TagConstants.REQUIRES_REDUNDANTLY: 266 case TagConstants.SIGNALS_REDUNDANTLY: 267 case TagConstants.WHEN_REDUNDANTLY: 268 case TagConstants.WORKING_SPACE_REDUNDANTLY: 269 Assert.fail("Redundant keywords should not be in AST!: " 270 + TagConstants.toString(tag)); 271 break; 272 273 case TagConstants.MODIFIESGROUPPRAGMA: { 274 ModifiesGroupPragma mm = (ModifiesGroupPragma)mp; 275 write(o, "/*@ modifies "); 276 if (mm.precondition != null) { 277 self.print(o,ind,mm.precondition); 278 write(o, " ==> ("); 279 } 280 for (int i=0; i<mm.items.size(); ++i) { 281 if (i != 0) write(o, ", "); 282 CondExprModifierPragma ce = mm.items.elementAt(i); 283 self.print(o, ind, ce.expr); 284 if (ce.cond != null) { 285 write(o, " if "); 286 self.print(o, ind, ce.cond); 287 } 288 } 289 if (mm.precondition != null) write(o, ")"); 290 291 write(o, "; @*/"); 292 break; 293 } 294 295 case TagConstants.DURATION: 296 case TagConstants.WORKING_SPACE: 297 case TagConstants.ALSO_MODIFIES: 298 case TagConstants.ASSIGNABLE: 299 case TagConstants.MEASURED_BY: 300 case TagConstants.MODIFIABLE: 301 case TagConstants.MODIFIES: { 302 Expr e = ((CondExprModifierPragma)mp).expr; 303 Expr p = ((CondExprModifierPragma)mp).cond; 304 write(o, "/*@ "); 305 if (mp.isRedundant()) 306 write(o, TagConstants.toString(TagConstants.makeRedundant(tag))); 307 else 308 write(o, TagConstants.toString(tag)); 309 write(o, ' '); 310 self.print(o, ind, e); 311 if (p != null) { 312 write(o, " if "); 313 self.print(o, ind, p); 314 } 315 write(o, "; */"); 316 break; 317 } 318 319 case TagConstants.ALSO_EXSURES: 320 case TagConstants.EXSURES: 321 case TagConstants.SIGNALS: { 322 VarExprModifierPragma vemp = (VarExprModifierPragma)mp; 323 write(o, "/*@ "); 324 write(o, TagConstants.toString(mp.originalTag())); 325 write(o, " ("); 326 //self.print(o, vemp.arg); 327 exsuresPrintDecl(o, vemp.arg); 328 write(o, ") "); 329 self.print(o, ind, vemp.expr); 330 write(o, "; */"); 331 break; 332 } 333 334 case TagConstants.BEHAVIOR: 335 case TagConstants.EXCEPTIONAL_BEHAVIOR: 336 case TagConstants.NORMAL_BEHAVIOR: 337 write(o, "/*@ "); 338 write(o, TagConstants.toString(tag)); 339 write(o, " */"); 340 break; 341 342 case TagConstants.PARSEDSPECS: { 343 ParsedRoutineSpecs s = ((ParsedSpecs)mp).specs; 344 writeln(o,"/*@"); 345 if (s.initialAlso != null) self.print(o,ind,s.initialAlso); 346 java.util.Iterator i = s.specs.iterator(); 347 int k = 0; 348 while (i.hasNext()) { 349 Object oo = i.next(); 350 if (oo == mp || oo == s) break; 351 print(o,ind,(ModifierPragmaVec)oo); 352 } 353 if (s.impliesThat.size() > 0) writeln(o, "implies_that"); 354 i = s.impliesThat.iterator(); 355 while (i.hasNext()) { 356 print(o,ind,(ModifierPragmaVec)i.next()); 357 } 358 if (s.examples.size() > 0) writeln(o, "for_example"); 359 i = s.examples.iterator(); 360 while (i.hasNext()) { 361 print(o,ind,(ModifierPragmaVec)i.next()); 362 } 363 for (int j=0; j<s.modifiers.size(); ++j) { 364 //print(o,ind,s.modifiers.elementAt(j)); 365 } 366 writeln(o,"@*/"); 367 break; 368 } 369 370 default: 371 write(o, "/* Unknown ModifierPragma (tag = " + TagConstants.toString(tag) + ") */"); 372 break; 373 } 374 } 375 376 //@ also 377 //@ requires o != null; 378 //@ requires sp != null; 379 public void print(OutputStream o, int ind, StmtPragma sp) { 380 int tag = sp.getTag(); 381 int otag = sp.originalTag(); 382 switch (tag) { 383 case TagConstants.UNREACHABLE: 384 write(o, "/*@ "); 385 write(o, TagConstants.toString(otag)); 386 write(o, " */"); 387 break; 388 389 case TagConstants.ASSERT: { 390 Expr e = ((ExprStmtPragma)sp).expr; 391 Expr l = ((ExprStmtPragma)sp).label; 392 write(o, "/*@ "); 393 write(o, TagConstants.toString(otag)); 394 write(o, " "); 395 self.print(o, ind, e); 396 if (l != null) { 397 write(o, " : "); 398 self.print(o, ind, l); 399 } 400 write(o, "; */"); 401 break; 402 } 403 404 case TagConstants.HENCE_BY: 405 case TagConstants.ASSUME: 406 case TagConstants.DECREASES: 407 case TagConstants.DECREASING: 408 case TagConstants.MAINTAINING: 409 case TagConstants.LOOP_INVARIANT: 410 case TagConstants.LOOP_PREDICATE: { 411 Expr e = ((ExprStmtPragma)sp).expr; 412 write(o, "/*@ "); 413 write(o, TagConstants.toString(otag)); 414 write(o, ' '); 415 self.print(o, ind, e); 416 write(o, "; */"); 417 break; 418 } 419 420 case TagConstants.SETSTMTPRAGMA: { 421 SetStmtPragma s = (SetStmtPragma)sp; 422 write(o, "/*@ "); 423 write(o, TagConstants.toString(TagConstants.SET)); 424 write(o, " "); 425 self.print(o, ind, s.target); 426 write(o, " = "); 427 self.print(o, ind, s.value); 428 write(o, "; */"); 429 break; 430 } 431 432 default: 433 write(o, "/* Unknown StmtPragma (tag = " + TagConstants.toString(otag) + ") */"); 434 break; 435 } 436 } 437 438 // g can be null 439 public static void print(GuardedCmd g) { 440 ((EscPrettyPrint)inst).print(System.out,0,g); 441 } 442 443 /** Print a guarded command. Assumes that <code>g</code> should be 444 printed starting at the current position of <code>o</code>. It 445 does <em>not</em> print a new-line at the end of the statement. 446 However, if the statement needs to span multiple lines (for 447 example, because it has embedded statements), then these lines are 448 indented by <code>ind</code> spaces. */ 449 450 //@ requires o != null; 451 // g can be null 452 public void print(OutputStream o, int ind, GuardedCmd g) { 453 if (g == null) { 454 writeln(o, "<null Stmt>"); 455 return; 456 } 457 458 int tag = g.getTag(); 459 switch (tag) { 460 case TagConstants.SKIPCMD: 461 write(o, "SKIP"); 462 return; 463 464 case TagConstants.RAISECMD: 465 write(o, "RAISE"); 466 return; 467 468 case TagConstants.ASSERTCMD: 469 write(o, "ASSERT "); 470 print(o, ind, ((ExprCmd)g).pred); 471 return; 472 473 case TagConstants.ASSUMECMD: 474 write(o, "ASSUME "); 475 print(o, ind, ((ExprCmd)g).pred); 476 return; 477 478 case TagConstants.GETSCMD: { 479 GetsCmd gc = (GetsCmd)g; 480 if (escjava.Main.options().nvu) 481 write(o, gc.v.decl.id.toString()); 482 else 483 write(o, escjava.translate.UniqName.variable(gc.v.decl)); 484 write(o, " = "); 485 if (gc.rhs != null) print(o, ind, gc.rhs); 486 return; 487 } 488 489 case TagConstants.SUBGETSCMD: { 490 SubGetsCmd sgc = (SubGetsCmd)g; 491 if (escjava.Main.options().nvu) 492 write(o, sgc.v.decl.id.toString()); 493 else 494 write(o, escjava.translate.UniqName.variable(sgc.v.decl)); 495 write(o, "["); 496 print(o, ind, sgc.index); 497 write(o, "] = "); 498 if (sgc.rhs != null) print(o, ind, sgc.rhs); 499 return; 500 } 501 502 case TagConstants.SUBSUBGETSCMD: { 503 SubSubGetsCmd ssgc = (SubSubGetsCmd)g; 504 if (escjava.Main.options().nvu) 505 write(o, ssgc.v.decl.id.toString()); 506 else 507 write(o, escjava.translate.UniqName.variable(ssgc.v.decl)); 508 write(o, "["); 509 print(o, ind, ssgc.index1); 510 write(o, "]["); 511 print(o, ind, ssgc.index2); 512 write(o, "] = "); 513 if (ssgc.rhs != null) print(o, ind, ssgc.rhs); 514 return; 515 } 516 517 case TagConstants.RESTOREFROMCMD: { 518 RestoreFromCmd gc = (RestoreFromCmd)g; 519 write(o, "RESTORE "); 520 if (escjava.Main.options().nvu) 521 write(o, gc.v.decl.id.toString()); 522 else 523 write(o, escjava.translate.UniqName.variable(gc.v.decl)); 524 write(o, " FROM "); 525 print(o, ind, gc.rhs); 526 return; 527 } 528 529 case TagConstants.VARINCMD: { 530 VarInCmd vc = (VarInCmd)g; 531 write(o, "VAR"); 532 printVarVec(o, vc.v); 533 writeln(o, " IN"); 534 spaces(o, ind+INDENT); 535 print(o, ind+INDENT, vc.g); 536 writeln(o); 537 spaces(o, ind); 538 write(o, "END"); 539 return; 540 } 541 542 case TagConstants.DYNINSTCMD: { 543 DynInstCmd dc = (DynInstCmd)g; 544 writeln(o, "DynamicInstanceCmd \"" + dc.s + "\" IN"); 545 spaces(o, ind+INDENT); 546 print(o, ind+INDENT, dc.g); 547 writeln(o); 548 spaces(o, ind); 549 write(o, "END"); 550 return; 551 } 552 553 case TagConstants.SEQCMD: { 554 SeqCmd sc = (SeqCmd)g; 555 int len = sc.cmds.size(); 556 if (len == 0) write(o, "SKIP"); 557 else if (len == 1) print(o, ind, sc.cmds.elementAt(0)); 558 else { 559 for (int i = 0; i < len; i++) { 560 if (i != 0) { 561 writeln(o, ";"); 562 spaces(o, ind); 563 } 564 print(o, ind, sc.cmds.elementAt(i)); 565 } 566 } 567 return; 568 } 569 570 case TagConstants.CALL: { 571 Call call = (Call)g; 572 if (call.inlined) { 573 write(o, "INLINED "); 574 } 575 write(o, "CALL "+ call.spec.dmd.getId()); 576 print(o, ind, call.args ); 577 if (escjava.Main.options().showCallDetails) { 578 writeln(o, " {"); 579 spaces(o, ind+INDENT); 580 printSpec(o, ind+INDENT, call.spec ); 581 writeln(o); 582 spaces(o, ind); 583 writeln(o, "DESUGARED:"); 584 spaces(o, ind+INDENT); 585 print(o, ind+INDENT, call.desugared); 586 writeln(o); 587 spaces(o, ind); 588 write(o, "}"); 589 } 590 return; 591 } 592 593 case TagConstants.TRYCMD: { 594 CmdCmdCmd tc = (CmdCmdCmd)g; 595 write(o, "{"); 596 spaces(o, INDENT-1 ); 597 print(o, ind+INDENT, tc.g1); 598 599 writeln(o); 600 spaces(o, ind); 601 write(o, "!"); 602 spaces(o, INDENT-1 ); 603 print(o, ind+INDENT, tc.g2); 604 writeln(o); 605 606 spaces(o, ind); 607 write(o, "}"); 608 return; 609 } 610 611 case TagConstants.LOOPCMD: { 612 LoopCmd lp = (LoopCmd)g; 613 writeln(o, "LOOP"); 614 printCondVec(o, ind+INDENT, lp.invariants, 615 TagConstants.toString(TagConstants.LOOP_INVARIANT)); 616 printDecrInfoVec(o, ind+INDENT, lp.decreases, 617 TagConstants.toString(TagConstants.DECREASES)); 618 619 int nextInd = ind+INDENT; 620 if (lp.tempVars.size() != 0) { 621 spaces(o, nextInd); 622 write(o, "VAR"); 623 printVarVec(o, lp.tempVars); 624 writeln(o, " IN"); 625 nextInd += INDENT; 626 } 627 628 spaces(o, nextInd); 629 print(o, nextInd, lp.guard); 630 // let a double-semicolon denote the break between the "guard" and "body" 631 writeln(o, ";;"); 632 spaces(o, nextInd); 633 print(o, nextInd, lp.body); 634 writeln(o); 635 636 if (lp.tempVars.size() != 0) { 637 spaces(o, ind+INDENT); 638 writeln(o, "END"); 639 } 640 641 if (escjava.Main.options().showLoopDetails) { 642 spaces(o, ind); 643 writeln(o, "PREDICATES:"); 644 for (int i = 0; i < lp.predicates.size(); i++) { 645 spaces(o, ind+INDENT); 646 print(o, ind+INDENT, lp.predicates.elementAt(i)); 647 writeln(o); 648 } 649 650 /* 651 spaces(o, ind); 652 writeln(o, "INVARIANTS:"); 653 for (int i = 1; i < lp.invariants.size(); i++) { 654 spaces(o, ind+INDENT); 655 print(o, ind+INDENT, lp.invariants.elementAt(i).pred); 656 writeln(o); 657 } 658 */ 659 660 spaces(o, ind); 661 writeln(o, "DESUGARED:"); 662 spaces(o, ind+INDENT); 663 print(o, ind+INDENT, lp.desugared); 664 writeln(o); 665 } 666 667 spaces(o, ind); 668 write(o, "END"); 669 return; 670 } 671 672 case TagConstants.CHOOSECMD: { 673 CmdCmdCmd cc = (CmdCmdCmd)g; 674 write(o, "{"); 675 spaces(o, INDENT-1 ); 676 print(o, ind+INDENT, cc.g1); 677 678 writeln(o); 679 spaces(o, ind); 680 writeln(o, "[]"); 681 682 spaces(o, ind+INDENT); 683 print(o, ind+INDENT, cc.g2); 684 writeln(o); 685 686 spaces(o, ind); 687 write(o, "}"); 688 return; 689 } 690 691 default: 692 write(o, "UnknownTag<" + tag + ":"); 693 write(o, TagConstants.toString(tag) + ">"); 694 return; 695 } 696 } 697 698 //@ requires o != null; 699 //@ requires vars != null; 700 private void printVarVec(OutputStream o, GenericVarDeclVec vars) { 701 for (int i = 0; i < vars.size(); i++) { 702 GenericVarDecl vd = vars.elementAt(i); 703 write(o, ' '); 704 if (false) { 705 // Someday we may have special variables for map types 706 write(o, "Map["); 707 // write(o, ((FieldDecl)vd).parent.id.toString()); 708 write(o, " -> "); 709 print(o, vd.type); 710 write(o, "]"); 711 } else print(o, vd.type); 712 write(o, ' '); 713 if (escjava.Main.options().nvu) 714 write(o, vd.id.toString()); 715 else 716 write(o, escjava.translate.UniqName.variable(vd)); 717 if (i != vars.size()-1) { 718 write(o, ';'); 719 } 720 } 721 } 722 723 //@ requires o != null; 724 //@ requires spec != null; 725 public void printSpec(OutputStream o, int ind, Spec spec) { 726 write(o, "SPEC "); 727 728 ModifierPragmaVec local = spec.dmd.original.pmodifiers; 729 ModifierPragmaVec combined = ModifierPragmaVec.make(); 730 731 for (int i=0; i<spec.dmd.requires.size(); i++) 732 combined.addElement(spec.dmd.requires.elementAt(i)); 733 for (int i=0; i<spec.dmd.modifies.size(); i++) 734 combined.addElement(spec.dmd.modifies.elementAt(i)); 735 for (int i=0; i<spec.dmd.ensures.size(); i++) 736 combined.addElement(spec.dmd.ensures.elementAt(i)); 737 for (int i=0; i<spec.dmd.exsures.size(); i++) 738 combined.addElement(spec.dmd.exsures.elementAt(i)); 739 740 spec.dmd.original.pmodifiers = combined; 741 print(o, ind+INDENT, spec.dmd.original, 742 spec.dmd.getContainingClass().id, 743 false); 744 spec.dmd.original.pmodifiers = local; 745 746 747 spaces(o, ind); 748 write(o, "targets "); 749 print(o, ind, spec.targets); 750 writeln(o, ";"); 751 752 spaces(o, ind); 753 write(o, "prevarmap { "); 754 boolean first=true; 755 for(Enumeration e = spec.preVarMap.keys(); e.hasMoreElements(); ) 756 { 757 if( !first ) 758 write(o, ", "); 759 else 760 first = false; 761 762 GenericVarDecl vd = (GenericVarDecl)e.nextElement(); 763 VariableAccess va = (VariableAccess)spec.preVarMap.get(vd); 764 print( o, vd ); 765 write(o, "->" ); 766 print( o, ind, va ); 767 } 768 writeln(o, " };"); 769 770 printCondVec(o, ind, spec.pre, "pre"); 771 printCondVec(o, ind, spec.post, "post"); 772 return; 773 } 774 775 //@ requires o != null; 776 //@ requires cv != null; 777 //@ requires name != null; 778 public void printCondVec(OutputStream o, int ind, ConditionVec cv, 779 String name) { 780 for(int i=0; i<cv.size(); i++) 781 { 782 spaces(o, ind); 783 write(o, name+" "); 784 printCond(o, ind, cv.elementAt(i)); 785 writeln(o, ";"); 786 } 787 } 788 789 //@ requires o != null; 790 //@ requires div != null; 791 //@ requires name != null; 792 public void printDecrInfoVec(OutputStream o, int ind, 793 DecreasesInfoVec div, String name) { 794 for (int i = 0; i < div.size(); i++) { 795 spaces(o, ind); 796 write(o, name+" "); 797 print(o, ind, div.elementAt(i).f); 798 writeln(o, ";"); 799 } 800 } 801 802 //@ requires o != null; 803 //@ requires cond != null; 804 public void printCond(OutputStream o, int ind, Condition cond) { 805 write(o, TagConstants.toString(cond.label)+": "); 806 print(o, ind, cond.pred ); 807 } 808 809 //@ also 810 //@ requires o != null; 811 //@ requires e != null; 812 public void print(OutputStream o, int ind, VarInit e) { 813 int tag = e.getTag(); 814 switch (tag) { 815 816 case TagConstants.VARIABLEACCESS: { 817 VariableAccess lva = (VariableAccess)e; 818 if (escjava.Main.options().nvu) 819 write(o, lva.decl.id.toString()); 820 else 821 write(o, escjava.translate.UniqName.variable(lva.decl)); 822 break; 823 } 824 825 case TagConstants.IMPLIES: 826 case TagConstants.EXPLIES: 827 case TagConstants.IFF: 828 case TagConstants.NIFF: 829 case TagConstants.SUBTYPE: { 830 BinaryExpr be = (BinaryExpr)e; 831 self.print(o, ind, be.left); 832 write(o, ' '); write(o, TagConstants.toString(be.op)); write(o, ' '); 833 self.print(o, ind, be.right); 834 break; 835 } 836 837 case TagConstants.SYMBOLLIT: 838 write(o, (String) (((LiteralExpr)e).value)); 839 break; 840 841 case TagConstants.LABELEXPR: { 842 LabelExpr le = (LabelExpr)e; 843 write(o, "("); 844 write(o, (le.positive ? TagConstants.toString(TagConstants.LBLPOS) : 845 TagConstants.toString(TagConstants.LBLNEG))); 846 write(o, " "); 847 write(o, le.label.toString()); 848 write(o, ' '); 849 self.print(o, ind, le.expr); 850 write(o, ")"); 851 break; 852 } 853 854 case TagConstants.LOCKSETEXPR: 855 write(o, TagConstants.toString(TagConstants.LS)); 856 break; 857 858 case TagConstants.ELEMSNONNULL: 859 case TagConstants.ELEMTYPE: 860 case TagConstants.FRESH: 861 case TagConstants.MAX: 862 case TagConstants.NOWARN_OP: 863 case TagConstants.PRE: 864 case TagConstants.SPACE: 865 case TagConstants.TYPEOF: 866 case TagConstants.WACK_BIGINT_MATH: 867 case TagConstants.WACK_DURATION: 868 case TagConstants.WACK_JAVA_MATH: 869 case TagConstants.WACK_NOWARN: 870 case TagConstants.WACK_SAFE_MATH: 871 case TagConstants.WACK_WORKING_SPACE: 872 case TagConstants.WARN: 873 case TagConstants.WARN_OP: { 874 write(o, TagConstants.toString(tag)); 875 self.print(o, ind, ((NaryExpr)e).exprs); 876 break; 877 } 878 879 case TagConstants.NOT_MODIFIED: 880 write(o, TagConstants.toString(tag)); 881 write(o, '('); 882 self.print(o, ind, ((NotModifiedExpr)e).expr); 883 write(o, ')'); 884 break; 885 886 case TagConstants.DTTFSA: { 887 ExprVec es = ((NaryExpr)e).exprs; 888 write(o, TagConstants.toString(tag)); 889 write(o, '('); 890 self.print(o, ((TypeExpr)es.elementAt(0)).type); 891 for (int i = 1; i < es.size(); i++) { 892 write(o, ", "); 893 self.print(o, ind, es.elementAt(i)); 894 } 895 write(o, ')'); 896 break; 897 } 898 899 case TagConstants.NUM_OF:{ 900 NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e; 901 write(o, "("); 902 write(o, TagConstants.toString(tag)); 903 write(o, " "); 904 String prefix = ""; 905 for( int i=0; i<qe.vars.size(); i++) { 906 GenericVarDecl decl = qe.vars.elementAt(i); 907 write(o, prefix ); 908 if (i == 0) self.print(o, decl.type); 909 write(o, ' '); 910 if (escjava.Main.options().nvu) 911 write(o, decl.id.toString()); 912 else 913 write(o, escjava.translate.UniqName.variable(decl)); 914 prefix = ", "; 915 } 916 write(o, "; "); 917 self.print(o, ind, qe.expr); 918 write(o, ')'); 919 break; 920 } 921 922 case TagConstants.SUM: 923 case TagConstants.PRODUCT: 924 case TagConstants.MIN: 925 case TagConstants.MAXQUANT:{ 926 GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e; 927 write(o, "("); 928 write(o, TagConstants.toString(tag)); 929 write(o, " "); 930 String prefix = ""; 931 for( int i=0; i<qe.vars.size(); i++) { 932 GenericVarDecl decl = qe.vars.elementAt(i); 933 write(o, prefix ); 934 if (i == 0) self.print(o, decl.type); 935 write(o, ' '); 936 if (escjava.Main.options().nvu) 937 write(o, decl.id.toString()); 938 else 939 write(o, escjava.translate.UniqName.variable(decl)); 940 prefix = ", "; 941 } 942 write(o, "; "); 943 self.print(o, ind, qe.expr); 944 write(o, "; "); 945 self.print(o, ind, qe.rangeExpr); 946 write(o, ')'); 947 break; 948 } 949 case TagConstants.FORALL: 950 case TagConstants.EXISTS: { 951 QuantifiedExpr qe = (QuantifiedExpr)e; 952 write(o, "("); 953 write(o, TagConstants.toString(tag)); 954 write(o, " "); 955 String prefix = ""; 956 for( int i=0; i<qe.vars.size(); i++) { 957 GenericVarDecl decl = qe.vars.elementAt(i); 958 write(o, prefix ); 959 if (i == 0) self.print(o, decl.type); 960 write(o, ' '); 961 if (escjava.Main.options().nvu) 962 write(o, decl.id.toString()); 963 else 964 write(o, escjava.translate.UniqName.variable(decl)); 965 prefix = ", "; 966 } 967 write(o, "; "); 968 self.print(o, ind, qe.expr); 969 write(o, ')'); 970 break; 971 } 972 973 case TagConstants.RESEXPR: 974 write(o, TagConstants.toString(TagConstants.RES)); 975 break; 976 977 case TagConstants.BOOLEANLIT: { 978 String comment = (String)EscPragmaParser.informalPredicateDecoration.get(e); 979 if (comment != null) { 980 LiteralExpr le = (LiteralExpr)e; 981 Boolean b = (Boolean)le.value; 982 Assert.notFalse(b.booleanValue() == true); 983 984 write(o, "(*"); 985 write(o, comment); 986 write(o, "*)"); 987 } else { 988 super.print(o, ind, e); 989 } 990 break; 991 } 992 993 case TagConstants.SUBSTEXPR: { 994 SubstExpr subst = (SubstExpr)e; 995 write(o, "[subst "); 996 self.print(o, ind, subst.val); 997 write(o, " for "); 998 if (escjava.Main.options().nvu) 999 write(o, subst.var.id.toString()); 1000 else 1001 write(o, escjava.translate.UniqName.variable(subst.var)); 1002 write(o, " in "); 1003 self.print(o, ind, subst.target); 1004 write(o, "]"); 1005 break; 1006 } 1007 1008 case TagConstants.TYPEEXPR: 1009 write(o, TagConstants.toString(TagConstants.TYPE)); 1010 write(o, "("); 1011 self.print(o, ((TypeExpr)e).type); 1012 write(o, ")"); 1013 break; 1014 1015 case TagConstants.ARRAYRANGEREFEXPR: { 1016 ArrayRangeRefExpr we = (ArrayRangeRefExpr)e; 1017 print( o, ind, we.array ); 1018 write(o, "["); 1019 if (we.lowIndex == null && we.highIndex == null) { 1020 write(o, "*"); 1021 } else { 1022 print(o, ind, we.lowIndex); 1023 write(o,".."); 1024 print(o, ind, we.highIndex); 1025 } 1026 write(o, "]"); 1027 break; 1028 } 1029 1030 case TagConstants.WILDREFEXPR: { 1031 WildRefExpr we = (WildRefExpr)e; 1032 print( o, ind, we.od ); 1033 // The ObjectDesignator prints the '.' 1034 write(o, "*"); 1035 break; 1036 } 1037 1038 case TagConstants.GUARDEXPR: { 1039 GuardExpr ge = (GuardExpr)e; 1040 write ( o, "(GUARD "); 1041 write ( o, escjava.translate.UniqName.locToSuffix(ge.locPragmaDecl) + " "); 1042 print( o, ind, ge.expr ); 1043 write(o, ")"); 1044 break; 1045 } 1046 1047 case TagConstants.ALLOCLT: 1048 case TagConstants.ALLOCLE: 1049 case TagConstants.ANYEQ: 1050 case TagConstants.ANYNE: 1051 case TagConstants.ARRAYLENGTH: 1052 case TagConstants.ARRAYFRESH: 1053 case TagConstants.ARRAYMAKE: 1054 case TagConstants.ARRAYSHAPEMORE: 1055 case TagConstants.ARRAYSHAPEONE: 1056 case TagConstants.ASELEMS: 1057 case TagConstants.ASFIELD: 1058 case TagConstants.ASLOCKSET: 1059 case TagConstants.BOOLAND: 1060 case TagConstants.BOOLANDX: 1061 case TagConstants.BOOLEQ: 1062 case TagConstants.BOOLIMPLIES: 1063 case TagConstants.BOOLNE: 1064 case TagConstants.BOOLNOT: 1065 case TagConstants.BOOLOR: 1066 case TagConstants.CAST: 1067 case TagConstants.CLASSLITERALFUNC: 1068 case TagConstants.CONDITIONAL: 1069 case TagConstants.ECLOSEDTIME: 1070 case TagConstants.FCLOSEDTIME: 1071 case TagConstants.FLOATINGADD: 1072 case TagConstants.FLOATINGDIV: 1073 case TagConstants.FLOATINGEQ: 1074 case TagConstants.FLOATINGGE: 1075 case TagConstants.FLOATINGGT: 1076 case TagConstants.FLOATINGLE: 1077 case TagConstants.FLOATINGLT: 1078 case TagConstants.FLOATINGMOD: 1079 case TagConstants.FLOATINGMUL: 1080 case TagConstants.FLOATINGNE: 1081 case TagConstants.FLOATINGNEG: 1082 case TagConstants.FLOATINGSUB: 1083 case TagConstants.INTEGRALADD: 1084 case TagConstants.INTEGRALAND: 1085 case TagConstants.INTEGRALDIV: 1086 case TagConstants.INTEGRALEQ: 1087 case TagConstants.INTEGRALGE: 1088 case TagConstants.INTEGRALGT: 1089 case TagConstants.INTEGRALLE: 1090 case TagConstants.INTEGRALLT: 1091 case TagConstants.INTEGRALMOD: 1092 case TagConstants.INTEGRALMUL: 1093 case TagConstants.INTEGRALNE: 1094 case TagConstants.INTEGRALNEG: 1095 case TagConstants.INTEGRALNOT: 1096 case TagConstants.INTEGRALOR: 1097 case TagConstants.INTSHIFTL: 1098 case TagConstants.LONGSHIFTL: 1099 case TagConstants.INTSHIFTR: 1100 case TagConstants.LONGSHIFTR: 1101 case TagConstants.INTSHIFTRU: 1102 case TagConstants.LONGSHIFTRU: 1103 case TagConstants.INTEGRALSUB: 1104 case TagConstants.INTEGRALXOR: 1105 case TagConstants.INTERN: 1106 case TagConstants.INTERNED: 1107 case TagConstants.IS: 1108 case TagConstants.ISALLOCATED: 1109 case TagConstants.ISNEWARRAY: 1110 case TagConstants.LOCKLE: 1111 case TagConstants.LOCKLT: 1112 case TagConstants.REFEQ: 1113 case TagConstants.REFNE: 1114 case TagConstants.SELECT: 1115 case TagConstants.STORE: 1116 case TagConstants.STRINGCAT: 1117 case TagConstants.STRINGCATP: 1118 case TagConstants.TYPEEQ: 1119 case TagConstants.TYPENE: 1120 case TagConstants.TYPELE: 1121 case TagConstants.UNSET: 1122 case TagConstants.VALLOCTIME: 1123 write(o, TagConstants.toString(tag)); 1124 self.print(o, ind, ((NaryExpr)e).exprs); 1125 break; 1126 1127 case TagConstants.METHODCALL: 1128 write(o, ((NaryExpr)e).methodName.toString()); 1129 self.print(o, ind, ((NaryExpr)e).exprs); 1130 break; 1131 1132 case TagConstants.NOTMODIFIEDEXPR: 1133 write(o, TagConstants.toString(TagConstants.NOT_MODIFIED)); 1134 write(o, "("); 1135 self.print(o, ind, ((NotModifiedExpr)e).expr); 1136 write(o, ")"); 1137 break; 1138 1139 case TagConstants.EVERYTHINGEXPR: 1140 write(o, TagConstants.toString(TagConstants.EVERYTHING)); 1141 break; 1142 case TagConstants.NOTHINGEXPR: 1143 write(o, TagConstants.toString(TagConstants.NOTHING)); 1144 break; 1145 case TagConstants.NOTSPECIFIEDEXPR: 1146 write(o, TagConstants.toString(TagConstants.NOT_SPECIFIED)); 1147 break; 1148 1149 default: 1150 Assert.notFalse(tag<=javafe.tc.TagConstants.LAST_TAG, 1151 "illegal attempt to pass tag #" + tag + " (" + 1152 TagConstants.toString(tag) + ") to javafe"); 1153 super.print(o, ind, e); 1154 break; 1155 } 1156 } 1157 1158 //@ also 1159 //@ requires o != null; 1160 //@ requires t != null; 1161 public void print(OutputStream o, Type t) { 1162 1163 switch ( t.getTag()) { 1164 case TagConstants.ANY: 1165 write(o, "anytype" ); 1166 break; 1167 1168 case TagConstants.TYPECODE: 1169 case TagConstants.LOCKSET: 1170 case TagConstants.OBJECTSET: 1171 write(o, TagConstants.toString(t.getTag()) ); 1172 break; 1173 1174 case TagConstants.BIGINTTYPE: 1175 write(o, "bigint"); 1176 break; 1177 1178 case TagConstants.REALTYPE: 1179 write(o, "real"); 1180 break; 1181 1182 default: 1183 super.print( o, t ); 1184 } 1185 } 1186 1187 /* (non-Javadoc) 1188 * @see javafe.ast.PrettyPrint#toString(int) 1189 */ 1190 public /*@ non_null @*/ String toString(int tag) { 1191 // Best version available in the back end: 1192 return escjava.ast.TagConstants.toString(tag); 1193 } 1194 1195 }