001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.translate; 004 005 /** 006 * Responsible for converting GCExpr to formula Strings for input to Simplify. 007 * The GCExpr language is documented elsewhere, as is Simplifys input language. 008 */ 009 010 import java.io.*; 011 import java.util.Enumeration; 012 import java.util.Hashtable; 013 import java.util.Arrays; 014 import javafe.ast.*; 015 import javafe.tc.Types; 016 import javafe.util.*; 017 import escjava.ast.*; 018 import escjava.ast.TagConstants; 019 import escjava.backpred.BackPred; 020 import escjava.prover.Atom; 021 022 public class VcToString { 023 024 /* 025 * Counter for additional informations when passing -Stats flag 026 */ 027 static public int quantifierNumber = 0; 028 static public int termNumber = 0; 029 static public int variableNumber = 0; 030 031 /** 032 * Resets any type-specific information that is accumulated through calls to 033 * <code>computeTypeSpecific</code>. 034 */ 035 public static void resetTypeSpecific() { 036 integralPrintNames = new Hashtable(); 037 //+@ set integralPrintNames.keyType = \type(Long); 038 //+@ set integralPrintNames.elementType = \type(String); 039 // add thresholds 040 integralPrintNames.put(minThreshold, String.valueOf(-MaxIntegral)); 041 integralPrintNames.put(maxThreshold, String.valueOf(MaxIntegral)); 042 } 043 044 /** 045 * Prints <code>e</code> as a simple-expression string to <code>to</code>. 046 * Any symbolic names created for integral literals in <code>e</code> are 047 * added to a static place (variable <code>integralPrintNames</code>) so 048 * that successive calls to <code>compute</code> can produce properties 049 * about these names. 050 */ 051 public static void computeTypeSpecific(/*@ non_null */Expr e, 052 /*@ non_null */PrintStream to) { 053 VcToString vts = new VcToString(); 054 vts.printFormula(to, e); 055 } 056 057 /** 058 * Prints <code>e</code> as a verification-condition string to 059 * <code>to</code>. Any symbolic names of integral literals stored by the 060 * most recent call to <code>computeTypeBackPred</code>, if any, will be 061 * considered when producing properties about such symbolic literals. 062 */ 063 public static void compute(/*@ non_null */Expr e, 064 /*@ non_null */PrintStream to) { 065 Hashtable oldNames = integralPrintNames; 066 integralPrintNames = (Hashtable)oldNames.clone(); 067 068 if (escjava.Main.options().prettyPrintVC) 069 to = new PrintStream(new escjava.prover.PPOutputStream(to)); 070 071 /* 072 * reset counters; 073 */ 074 quantifierNumber = 0; 075 termNumber = 0; 076 variableNumber = 0; 077 078 VcToString vts = new VcToString(); 079 080 vts.printDefpreds(to, vts.getDefpreds(e)); 081 to.println("\n(EXPLIES "); 082 vts.printFormula(to, e); 083 to.println(" (AND "); 084 vts.distinctSymbols(to); 085 vts.stringLiteralAssumptions(to); 086 vts.integralPrintNameOrder(to); 087 to.println("))"); 088 089 integralPrintNames = oldNames; 090 } 091 092 public static void computePC(/*@ non_null */Expr e, 093 /*@ non_null */PrintStream to) { 094 Hashtable oldNames = integralPrintNames; 095 integralPrintNames = (Hashtable)oldNames.clone(); 096 097 VcToString vts = new VcToString(); 098 to.println("\n(AND "); 099 vts.printFormula(to, e); 100 vts.distinctSymbols(to); 101 vts.stringLiteralAssumptions(to); 102 vts.integralPrintNameOrder(to); 103 to.println(")"); 104 105 integralPrintNames = oldNames; 106 } 107 108 // holds set of symbols used 109 //@ spec_public 110 protected/*@ non_null */Set symbols = new Set(); 111 112 // string of initial assumptions 113 //@ spec_public 114 protected /*@ non_null */ Set stringLiterals = new Set(); 115 116 //+@ invariant integralPrintNames.keyType == \type(Long); 117 //+@ invariant integralPrintNames.elementType == \type(String); 118 //@ spec_public 119 protected static/*@ non_null */Hashtable integralPrintNames; 120 121 protected VcToString() {} 122 123 protected String vc2Term(/*@ non_null */Expr e, Hashtable subst) { 124 Assert.notNull(e); 125 ByteArrayOutputStream baos = new ByteArrayOutputStream(); 126 PrintStream ps = new PrintStream(baos); 127 printTerm(ps, subst, e); 128 String s = baos.toString(); 129 ps.close(); 130 // System.out.println("vc2Term yields: "+s); 131 return s; 132 } 133 134 protected void printDefpreds(/*@ non_null */PrintStream to, DefPredVec preds) { 135 for (int i = 0; i < preds.size(); i++) { 136 DefPred dp = preds.elementAt(i); 137 to.print("(DEFPRED (" + dp.predId); 138 for (int j = 0; j < dp.args.size(); j++) { 139 to.print(" " + dp.args.elementAt(j).id); 140 } 141 to.print(") "); 142 printFormula(to, dp.body); 143 to.print(")\n"); 144 } 145 } 146 147 protected DefPredVec preds; 148 149 protected DefPredVec getDefpreds(/*@ non_null */Expr e) { 150 preds = DefPredVec.make(); 151 getDefpredsHelper(e); 152 return preds; 153 } 154 155 protected void getDefpredsHelper(/*@ non_null */Expr e) { 156 if (e instanceof DefPredLetExpr) { 157 DefPredLetExpr dple = (DefPredLetExpr)e; 158 preds.append(dple.preds); 159 } 160 for (int i = 0; i < e.childCount(); i++) { 161 Object c = e.childAt(i); 162 if (c instanceof Expr) { 163 getDefpredsHelper((Expr)c); 164 } 165 } 166 } 167 168 protected void distinctSymbols(/*@ non_null */PrintStream to) { 169 to.print("(DISTINCT"); 170 Enumeration e = symbols.elements(); 171 while (e.hasMoreElements()) { 172 String s = (String)e.nextElement(); 173 to.print(" "); 174 to.print(s); 175 } 176 to.print(")"); 177 } 178 179 protected void stringLiteralAssumptions(/*@ non_null */PrintStream to) { 180 Enumeration e = stringLiterals.elements(); 181 while (e.hasMoreElements()) { 182 String litname = (String)e.nextElement(); 183 184 to.print(" (NEQ "); 185 to.print(litname); 186 to.print(" null)"); 187 188 to.print(" (EQ (typeof "); 189 to.print(litname); 190 to.print(") |T_java.lang.String|)"); 191 192 // We could also assume "litname" to be allocated (but at this 193 // time we don't have the name of the initial value of "alloc"; 194 // probably it is "alloc", but it would be nice not to have to 195 // rely on that here). 196 } 197 } 198 199 // ====================================================================== 200 201 protected void printFormula(/*@ non_null */PrintStream out, 202 /*@ non_null */Expr e) { 203 // maps GenericVarDecls to Strings 204 // some complex invariant here 205 206 Hashtable subst = new Hashtable(); 207 printFormula(out, subst, e); 208 } 209 210 protected void printFormula(/*@ non_null */PrintStream out, Hashtable subst, 211 /*@ non_null */Expr e) { 212 Assert.notNull(e); 213 214 reallyPrintFormula(out, subst, e); 215 } 216 217 protected void reallyPrintFormula(/*@ non_null */PrintStream out, 218 Hashtable subst, 219 /*@ non_null */Expr e) { 220 221 // System.out.print("printFormula: "); 222 // PrettyPrint.inst.print(System.out, e); 223 // System.out.println("\nsubst="+subst); 224 225 switch (e.getTag()) { 226 227 case TagConstants.DEFPREDLETEXPR: { 228 DefPredLetExpr dple = (DefPredLetExpr)e; 229 printFormula(out, subst, dple.body); 230 break; 231 } 232 233 case TagConstants.SUBSTEXPR: { 234 235 System.out.println("SubstExpr"); 236 237 SubstExpr se = (SubstExpr)e; 238 // perform current substitution on expression 239 String expr = vc2Term(se.val, subst); 240 // get old val, install new val 241 Object old = subst.put(se.var, expr); 242 //System.out.println("old="+old); 243 244 // print 245 printFormula(out, subst, se.target); 246 247 // restore old state 248 if (old == null) subst.remove(se.var); 249 else subst.put(se.var, old); 250 251 break; 252 } 253 254 case TagConstants.LABELEXPR: { 255 LabelExpr le = (LabelExpr)e; 256 out.print("(" + (le.positive ? "LBLPOS" : "LBLNEG") + " |" + le.label 257 + "| "); 258 printFormula(out, subst, le.expr); 259 out.print(")"); 260 break; 261 } 262 263 case TagConstants.GUARDEXPR: { 264 if (!escjava.Main.options().guardedVC) { 265 Assert.fail("VcToString.reallyPrintFormula: unreachable"); 266 } else { 267 GuardExpr ge = (GuardExpr)e; 268 String var = escjava.Main.options().guardedVCPrefix 269 + UniqName.locToSuffix(ge.locPragmaDecl); 270 out.print("(IMPLIES |" + var + "| "); 271 printFormula(out, subst, ge.expr); 272 out.print(")"); 273 escjava.Main.options().guardVars.add(var); 274 break; 275 } 276 } 277 278 case TagConstants.FORALL: 279 case TagConstants.EXISTS: { 280 quantifierNumber++; 281 282 QuantifiedExpr qe = (QuantifiedExpr)e; 283 if (qe.quantifier == TagConstants.FORALL) out.print("(FORALL ("); 284 else out.print("(EXISTS ("); 285 286 String prefix = ""; 287 for (int i = 0; i < qe.vars.size(); i++) { 288 GenericVarDecl decl = qe.vars.elementAt(i); 289 Assert.notFalse(!subst.containsKey(decl), "Quantification over " 290 + "substituted variable"); 291 out.print(prefix); 292 printVarDecl(out, decl); 293 prefix = " "; 294 } 295 out.print(") "); 296 if (qe.nopats != null && qe.nopats.size() != 0) { 297 Assert.notFalse(!insideNoPats); 298 insideNoPats = true; 299 out.print("(NOPATS"); 300 for (int i = 0; i < qe.nopats.size(); i++) { 301 out.print(" "); 302 Expr nopat = qe.nopats.elementAt(i); 303 printTerm(out, subst, nopat); 304 } 305 out.print(") "); 306 insideNoPats = false; 307 } 308 if (qe.pats != null && qe.pats.size() != 0) { 309 Assert.notFalse(!insideNoPats); 310 insideNoPats = true; 311 if (qe.pats.size() == 1) out.print("(PATS"); 312 else out.print("(PATS (MPAT"); 313 for (int i = 0; i < qe.pats.size(); i++) { 314 out.print(" "); 315 Expr nopat = qe.pats.elementAt(i); 316 printTerm(out, subst, nopat); 317 } 318 if (qe.pats.size() == 1) out.print(") "); 319 else out.print("))"); 320 insideNoPats = false; 321 } 322 printFormula(out, subst, qe.expr); 323 out.print(")"); 324 break; 325 } 326 327 // Operators on formulas 328 case TagConstants.BOOLIMPLIES: 329 case TagConstants.BOOLAND: 330 case TagConstants.BOOLANDX: 331 case TagConstants.BOOLOR: 332 case TagConstants.BOOLNOT: 333 case TagConstants.BOOLEQ: { 334 NaryExpr ne = (NaryExpr)e; 335 String op; 336 337 switch (ne.getTag()) { 338 case TagConstants.BOOLIMPLIES: 339 op = "IMPLIES"; 340 break; 341 case TagConstants.BOOLAND: 342 case TagConstants.BOOLANDX: 343 op = "AND"; 344 break; 345 case TagConstants.BOOLOR: 346 op = "OR"; 347 break; 348 case TagConstants.BOOLNOT: 349 op = "NOT"; 350 break; 351 case TagConstants.BOOLEQ: 352 op = "IFF"; 353 break; 354 default: 355 Assert.fail("Fall thru"); 356 op = null; // dummy assignment 357 } 358 359 out.print("(" + op); 360 for (int i = 0; i < ne.exprs.size(); i++) { 361 out.print(" "); 362 printFormula(out, subst, ne.exprs.elementAt(i)); 363 } 364 out.print(")"); 365 break; 366 } 367 368 case TagConstants.BOOLNE: { 369 NaryExpr ne = (NaryExpr)e; 370 out.print("(IFF "); 371 printFormula(out, subst, ne.exprs.elementAt(0)); 372 out.print(" (NOT "); 373 printFormula(out, subst, ne.exprs.elementAt(1)); 374 out.print("))"); 375 break; 376 } 377 378 case TagConstants.METHODCALL: { 379 NaryExpr ne = (NaryExpr)e; 380 out.print("(EQ |@true| ( |"); 381 out.print(ne.methodName); 382 out.print("| "); 383 int n = ne.exprs.size(); 384 for (int i = 0; i < n; i++) { 385 printTerm(out, subst, ne.exprs.elementAt(i)); 386 out.print(" "); 387 } 388 out.print("))"); 389 break; 390 } 391 392 // PredSyms 393 case TagConstants.ALLOCLT: 394 case TagConstants.ALLOCLE: 395 case TagConstants.ANYEQ: 396 case TagConstants.ANYNE: 397 case TagConstants.INTEGRALEQ: 398 case TagConstants.INTEGRALGE: 399 case TagConstants.INTEGRALGT: 400 case TagConstants.INTEGRALLE: 401 case TagConstants.INTEGRALLT: 402 case TagConstants.INTEGRALNE: 403 case TagConstants.LOCKLE: 404 case TagConstants.LOCKLT: 405 case TagConstants.REFEQ: 406 case TagConstants.REFNE: 407 case TagConstants.TYPEEQ: 408 case TagConstants.TYPENE: 409 case TagConstants.TYPELE: { 410 NaryExpr ne = (NaryExpr)e; 411 String op; 412 413 switch (ne.getTag()) { 414 case TagConstants.ALLOCLT: 415 op = "<"; 416 break; 417 case TagConstants.ALLOCLE: 418 op = "<="; 419 break; 420 case TagConstants.ANYEQ: 421 op = "EQ"; 422 break; 423 case TagConstants.ANYNE: 424 op = "NEQ"; 425 break; 426 case TagConstants.INTEGRALEQ: 427 op = "EQ"; 428 break; 429 case TagConstants.INTEGRALGE: 430 op = ">="; 431 break; 432 case TagConstants.INTEGRALGT: 433 op = ">"; 434 break; 435 case TagConstants.INTEGRALLE: 436 op = "<="; 437 break; 438 case TagConstants.INTEGRALLT: 439 op = "<"; 440 break; 441 case TagConstants.INTEGRALNE: 442 op = "NEQ"; 443 break; 444 case TagConstants.LOCKLE: 445 op = TagConstants.toVcString(TagConstants.LOCKLE); 446 break; 447 case TagConstants.LOCKLT: 448 op = TagConstants.toVcString(TagConstants.LOCKLT); 449 break; 450 case TagConstants.REFEQ: 451 op = "EQ"; 452 break; 453 case TagConstants.REFNE: 454 op = "NEQ"; 455 break; 456 case TagConstants.TYPEEQ: 457 op = "EQ"; 458 break; 459 case TagConstants.TYPENE: 460 op = "NEQ"; 461 break; 462 case TagConstants.TYPELE: 463 op = "<:"; 464 break; 465 default: 466 Assert.fail("Fall thru"); 467 op = null; // dummy assignment 468 } 469 470 out.print("(" + op); 471 for (int i = 0; i < ne.exprs.size(); i++) { 472 out.print(" "); 473 printTerm(out, subst, ne.exprs.elementAt(i)); 474 } 475 out.print(")"); 476 break; 477 } 478 479 default: { 480 if (e.getTag() == TagConstants.DTTFSA) { 481 NaryExpr ne = (NaryExpr)e; 482 TypeExpr te = (TypeExpr)ne.exprs.elementAt(0); 483 if (Types.isBooleanType(te.type)) { 484 // print this DTTFSA as a predicate 485 printDttfsa(out, subst, ne); 486 break; 487 } 488 } 489 // not a predicate, must be a term 490 out.print("(EQ |@true| "); 491 printTerm(out, subst, e); 492 out.print(")"); 493 break; 494 } 495 } 496 } 497 498 // ====================================================================== 499 500 /** 501 * <code>insideNoPats</code> is really a parameter to * 502 * <code>printTerm</code>. 503 */ 504 505 protected boolean insideNoPats = false; 506 507 protected void printTerm(/*@ non_null */PrintStream out, Hashtable subst, 508 /*@ non_null */Expr e) { 509 510 termNumber++; 511 512 int tag = e.getTag(); 513 switch (tag) { 514 515 case TagConstants.SUBSTEXPR: { 516 SubstExpr se = (SubstExpr)e; 517 // perform current substitution on expression 518 String expr = vc2Term(se.val, subst); 519 // get old val, install new val 520 Object old = subst.put(se.var, expr); 521 // print 522 printTerm(out, subst, se.target); 523 524 // restore old state 525 if (old == null) subst.remove(se.var); 526 else subst.put(se.var, old); 527 528 break; 529 } 530 531 case TagConstants.DEFPREDAPPLEXPR: { 532 DefPredApplExpr dpae = (DefPredApplExpr)e; 533 out.print("(" + dpae.predId); 534 for (int i = 0; i < dpae.args.size(); i++) { 535 out.print(" "); 536 printTerm(out, subst, dpae.args.elementAt(i)); 537 } 538 out.print(")"); 539 break; 540 } 541 542 case TagConstants.TYPEEXPR: { 543 TypeExpr te = (TypeExpr)e; 544 out.print(BackPred.simplifyTypeName(te.type)); 545 break; 546 } 547 548 // Literals 549 550 // This handles case 8 of ESCJ 23b: 551 case TagConstants.STRINGLIT: { 552 LiteralExpr le = (LiteralExpr)e; 553 String s = "S_" + UniqName.locToSuffix(le.loc); 554 s = Atom.printableVersion(s); 555 stringLiterals.add(s); 556 out.print(s); 557 break; 558 } 559 560 case TagConstants.BOOLEANLIT: { 561 LiteralExpr le = (LiteralExpr)e; 562 if (((Boolean)le.value).booleanValue()) out.print("|@true|"); 563 else out.print("|bool$false|"); 564 break; 565 } 566 567 case TagConstants.CHARLIT: 568 case TagConstants.INTLIT: { 569 LiteralExpr le = (LiteralExpr)e; 570 out.print(integralPrintName(((Integer)le.value).intValue())); 571 break; 572 } 573 574 case TagConstants.LONGLIT: { 575 LiteralExpr le = (LiteralExpr)e; 576 out.print(integralPrintName(((Long)le.value).longValue())); 577 break; 578 } 579 580 case TagConstants.FLOATLIT: { 581 LiteralExpr le = (LiteralExpr)e; 582 out.print("|F_" + ((Float)le.value).floatValue() + "|"); 583 break; 584 } 585 586 case TagConstants.DOUBLELIT: { 587 LiteralExpr le = (LiteralExpr)e; 588 out.print("|F_" + ((Double)le.value).doubleValue() + "|"); 589 break; 590 } 591 592 case TagConstants.NULLLIT: 593 out.print("null"); 594 break; 595 596 case TagConstants.SYMBOLLIT: { 597 // Handles case 5 of ESCJ 23b: 598 LiteralExpr le = (LiteralExpr)e; 599 String s = "|" + (String)le.value + "|"; 600 symbols.add(s); 601 out.print(s); 602 break; 603 } 604 605 case TagConstants.VARIABLEACCESS: { 606 variableNumber++; 607 608 VariableAccess va = (VariableAccess)e; 609 String to = (String)subst.get(va.decl); 610 611 if (to != null) out.print(to); 612 else printVarDecl(out, va.decl); 613 break; 614 } 615 616 // Nary functions 617 case TagConstants.ALLOCLT: //++ 618 case TagConstants.ALLOCLE: //++ 619 case TagConstants.ARRAYLENGTH: //++ 620 case TagConstants.ARRAYFRESH: //++ 621 case TagConstants.ARRAYMAKE: //++ 622 case TagConstants.ARRAYSHAPEMORE: //++ 623 case TagConstants.ARRAYSHAPEONE: //++ 624 case TagConstants.ASELEMS: //++ 625 case TagConstants.ASFIELD: //++ 626 case TagConstants.ASLOCKSET: //++ 627 case TagConstants.BOOLAND: //++ 628 case TagConstants.BOOLANDX: //++ 629 case TagConstants.BOOLEQ: //++ 630 case TagConstants.BOOLIMPLIES: //++ 631 case TagConstants.BOOLNE: //++ 632 case TagConstants.BOOLNOT: //++ 633 case TagConstants.BOOLOR: //++ 634 case TagConstants.CLASSLITERALFUNC: 635 case TagConstants.CONDITIONAL: 636 case TagConstants.ELEMSNONNULL: 637 case TagConstants.ELEMTYPE: 638 case TagConstants.ECLOSEDTIME: //++ 639 case TagConstants.FCLOSEDTIME: //++ 640 641 case TagConstants.FLOATINGADD: //++ 642 case TagConstants.FLOATINGDIV: //++ 643 case TagConstants.FLOATINGEQ: //++ 644 case TagConstants.FLOATINGGE: //++ 645 case TagConstants.FLOATINGGT: //++ 646 case TagConstants.FLOATINGLE: //++ 647 case TagConstants.FLOATINGLT: //++ 648 case TagConstants.FLOATINGMOD: //++ 649 case TagConstants.FLOATINGMUL: //++ 650 case TagConstants.FLOATINGNE: //++ 651 case TagConstants.FLOATINGNEG: 652 case TagConstants.FLOATINGSUB: 653 654 case TagConstants.INTEGRALADD: //++ 655 case TagConstants.INTEGRALAND: 656 case TagConstants.INTEGRALDIV: //++ 657 case TagConstants.INTEGRALEQ: //++ 658 case TagConstants.INTEGRALGE: //++ 659 case TagConstants.INTEGRALGT: //++ 660 case TagConstants.INTEGRALLE: //++ 661 case TagConstants.INTEGRALLT: //++ 662 case TagConstants.INTEGRALMOD: //++ 663 case TagConstants.INTEGRALMUL: //++ 664 case TagConstants.INTEGRALNE: //++ 665 case TagConstants.INTEGRALNEG: 666 case TagConstants.INTEGRALNOT: 667 case TagConstants.INTEGRALOR: 668 case TagConstants.INTSHIFTL: 669 case TagConstants.LONGSHIFTL: 670 case TagConstants.INTSHIFTR: 671 case TagConstants.LONGSHIFTR: 672 case TagConstants.INTSHIFTRU: 673 case TagConstants.LONGSHIFTRU: 674 case TagConstants.INTEGRALSUB: 675 case TagConstants.INTEGRALXOR: 676 677 case TagConstants.INTERN: 678 case TagConstants.INTERNED: 679 case TagConstants.IS: //++ 680 case TagConstants.ISALLOCATED: //++ 681 case TagConstants.ISNEWARRAY: //++ 682 case TagConstants.LOCKLE: //++ 683 case TagConstants.LOCKLT: //++ 684 case TagConstants.MAX: 685 case TagConstants.METHODCALL: 686 case TagConstants.REFEQ: //++ 687 case TagConstants.REFNE: //++ 688 case TagConstants.SELECT: //++ 689 case TagConstants.STORE: //++ 690 case TagConstants.STRINGCAT: 691 case TagConstants.STRINGCATP: 692 case TagConstants.TYPEEQ: //++ 693 case TagConstants.TYPENE: //++ 694 case TagConstants.TYPELE: //++ 695 case TagConstants.TYPEOF: //++ 696 case TagConstants.UNSET: 697 case TagConstants.VALLOCTIME: { 698 NaryExpr ne = (NaryExpr)e; 699 String op; 700 switch (tag) { 701 case TagConstants.INTEGRALADD: 702 op = "+"; 703 break; 704 case TagConstants.INTEGRALMUL: 705 op = "*"; 706 break; 707 case TagConstants.INTEGRALNEG: 708 op = "- 0"; 709 break; 710 case TagConstants.INTEGRALSUB: 711 op = "-"; 712 break; 713 case TagConstants.TYPELE: 714 op = "<:"; 715 break; 716 case TagConstants.METHODCALL: 717 op = "|" + ne.methodName.toString() + "|"; 718 break; 719 case TagConstants.INTEGRALNE: 720 case TagConstants.REFNE: 721 case TagConstants.TYPENE: 722 case TagConstants.ANYNE: 723 if (insideNoPats) { 724 op = "NEQ"; 725 break; 726 } 727 // fall thru 728 default: 729 op = TagConstants.toVcString(tag); 730 } 731 out.print("(" + op); 732 for (int i = 0; i < ne.exprs.size(); i++) { 733 out.print(" "); 734 printTerm(out, subst, ne.exprs.elementAt(i)); 735 } 736 out.print(")"); 737 break; 738 } 739 740 case TagConstants.CAST: { 741 NaryExpr ne = (NaryExpr)e; 742 Assert.notFalse(ne.exprs.size() == 2); 743 Expr x = ne.exprs.elementAt(0); 744 TypeExpr t = (TypeExpr)ne.exprs.elementAt(1); 745 746 if (Types.isBooleanType(t.type)) { 747 // Peephole optimization to remove casts to boolean, since 748 // anything is a boolean in the underlying logic (it either 749 // equals |@true| or it doesn't). The reason this peephole 750 // optimization is performed here, rather than in trExpr 751 // and trSpecExpr, is that then any expression cast to a 752 // boolean will be printed as a term, not as a predicate. 753 // This may sometimes be useful for boolean DTTFSA expression, 754 // which are printed as predicate whenever they occur in 755 // predicate positions. 756 printTerm(out, subst, x); 757 } else { 758 out.print("("); 759 out.print(TagConstants.toVcString(tag)); 760 out.print(" "); 761 printTerm(out, subst, x); 762 out.print(" "); 763 printTerm(out, subst, t); 764 out.print(")"); 765 } 766 break; 767 } 768 769 case TagConstants.DTTFSA: { 770 NaryExpr ne = (NaryExpr)e; 771 printDttfsa(out, subst, ne); 772 break; 773 } 774 775 default: 776 Assert.fail("Bad tag in GCTerm: " + "(tag=" + tag + "," 777 + TagConstants.toVcString(tag) + ") " + e); 778 } 779 } 780 781 //@ requires ne.op == TagConstants.DTTFSA; 782 protected void printDttfsa(/*@ non_null */PrintStream out, Hashtable subst, 783 /*@ non_null */NaryExpr ne) { 784 LiteralExpr lit = (LiteralExpr)ne.exprs.elementAt(1); 785 String op = (String)lit.value; 786 if (ne.exprs.size() == 2) { 787 out.print(op); 788 } else if (op.equals("identity")) { 789 Assert.notFalse(ne.exprs.size() == 3); 790 Expr e2 = ne.exprs.elementAt(2); 791 printTerm(out, subst, e2); 792 } else { 793 out.print("("); 794 out.print(op); 795 for (int i = 2; i < ne.exprs.size(); i++) { 796 out.print(" "); 797 Expr ei = ne.exprs.elementAt(i); 798 printTerm(out, subst, ei); 799 } 800 out.print(")"); 801 } 802 } 803 804 // ====================================================================== 805 806 protected void printVarDecl(/*@ non_null */PrintStream out, GenericVarDecl decl) { 807 out.print(Atom.printableVersion(UniqName.variable(decl))); 808 } 809 810 // ====================================================================== 811 812 protected static final long MaxIntegral = 1000000; 813 814 protected static final/*@ non_null */Long minThreshold = new Long(-MaxIntegral); 815 816 protected static final/*@ non_null */Long maxThreshold = new Long(MaxIntegral); 817 818 /** 819 * * Convert an integral # into its printname according to the rules * of ESCJ 820 * 23b, part 9. 821 */ 822 823 protected/*@ non_null */String integralPrintName(long n) { 824 if (-MaxIntegral <= n && n <= MaxIntegral) { 825 return String.valueOf(n); 826 } 827 828 Long l = new Long(n); 829 String name = (String)integralPrintNames.get(l); 830 if (name != null) { 831 return name; 832 } 833 834 if (n == -n) { 835 // Need to handle minlong specially... 836 name = "neg" + String.valueOf(n).substring(1); 837 } else if (n < 0) { 838 name = "neg" + String.valueOf(-n); 839 } else { 840 name = "pos" + String.valueOf(n); 841 } 842 843 integralPrintNames.put(l, name); 844 return name; 845 } 846 847 /** Generates the inequalities that compare the integral literals 848 * that were replaced in <code>integralPrintName</code> by symbolic 849 * names. 850 **/ 851 852 protected void integralPrintNameOrder(/*@ non_null */PrintStream ps) { 853 int n = integralPrintNames.size(); 854 Assert.notFalse(2 <= n); // should contain the two thresholds 855 if (n == 0) { 856 return; 857 } 858 859 Long[] keys = new Long[n]; 860 Enumeration e = integralPrintNames.keys(); 861 for (int i = 0; e.hasMoreElements(); i++) { 862 Long l = (Long)e.nextElement(); 863 keys[i] = l; 864 } 865 Arrays.sort(keys); 866 867 String valueI = (String)integralPrintNames.get(keys[0]); 868 /* loop invariant: valueI == integralPrintNames.get(keys[i]); */ 869 for (int i = 0; i < n - 1; i++) { 870 String valueNext = (String)integralPrintNames.get(keys[i + 1]); 871 if (keys[i] == minThreshold) { 872 Assert.notFalse(keys[i + 1] == maxThreshold); 873 } else { 874 ps.print(" (< "); 875 ps.print(valueI); 876 ps.print(" "); 877 ps.print(valueNext); 878 ps.print(")"); 879 } 880 valueI = valueNext; 881 } 882 } 883 884 static { 885 resetTypeSpecific(); 886 } 887 888 } 889 890 /* 891 * Local Variables: 892 * Mode: Java 893 * fill-column: 85 894 * End: 895 */