001 package escjava.translate; 002 003 /** 004 * Responsible for converting GCExpr to formula Strings for input to Simplify. 005 * The GCExpr language is documented elsewhere, as is Simplifys input language. 006 */ 007 008 import java.io.*; 009 import java.util.Enumeration; 010 import java.util.Hashtable; 011 import java.util.Arrays; 012 import java.util.Vector; 013 import java.util.Iterator; 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 VcToStringPvs { 023 024 /* list of already declared variables in the pvs logic 025 like LS, null, Java.lang.Object etc... */ 026 static public Vector listOfDecl = new Vector(); 027 028 /* name of the variables that need to be declared 029 Before adding a variable to this set, we check if the variable isn't 030 already in this set or in listOfDecl */ 031 static public Vector listOfDeclAdd = new Vector(); 032 033 /* set containing the name of the new fonctions that need to be declared, 034 that are introduced during the creation of gc, but aren't explicitly redeclared 035 here normally (because Simplify seems to allow declarations 'on the fly' ??) 036 037 The second vector contains the number of parameters for functions 038 declared in the first one. 039 040 It means : 041 listOfDeclFun = < f, g> 042 listOfDeclFunNbParam = < 1, 2> 043 044 will be translated to : 045 f(a : S) : S 046 g(a, b :S) : S 047 */ 048 static public Vector listOfDeclFun = new Vector(); 049 static public Vector listOfDeclFunNbParam = new Vector(); 050 051 /** 052 * Resets any type-specific information that is accumulated through calls to 053 * <code>computeTypeSpecific</code>. 054 */ 055 public static void resetTypeSpecific() { 056 integralPrintNames = new Hashtable(); 057 //+@ set integralPrintNames.keyType = \type(Long); 058 //+@ set integralPrintNames.elementType = \type(String); 059 // add thresholds 060 integralPrintNames.put(minThreshold, String.valueOf(-MaxIntegral)); 061 integralPrintNames.put(maxThreshold, String.valueOf(MaxIntegral)); 062 } 063 064 /** 065 * Prints <code>e</code> as a simple-expression string to <code>to</code>. 066 * Any symbolic names created for integral literals in <code>e</code> are 067 * added to a static place (variable <code>integralPrintNames</code>) so 068 * that successive calls to <code>compute</code> can produce properties 069 * about these names. 070 */ 071 public static void computeTypeSpecific(/*@ non_null */Expr e, 072 /*@ non_null */PrintStream to) { 073 VcToString vts = new VcToString(); 074 vts.printFormula(to, e); 075 } 076 077 /** 078 * Prints <code>e</code> as a verification-condition string to 079 * <code>to</code>. Any symbolic names of integral literals stored by the 080 * most recent call to <code>computeTypeBackPred</code>, if any, will be 081 * considered when producing properties about such symbolic literals. 082 */ 083 public static void compute(/*@ non_null */Expr e, 084 /*@ non_null */PrintStream to) { 085 086 listOfDecl.add("elems"); 087 listOfDecl.add("alloc"); 088 listOfDecl.add("java_null"); 089 listOfDecl.add("T_double"); 090 listOfDecl.add("T_float"); 091 listOfDecl.add("T_long"); 092 listOfDecl.add("T_int"); 093 listOfDecl.add("T_short"); 094 listOfDecl.add("T_byte"); 095 listOfDecl.add("T_char"); 096 listOfDecl.add("T_boolean"); 097 listOfDecl.add("T_java_lang_Cloneable"); 098 listOfDecl.add("LS"); 099 100 Hashtable oldNames = integralPrintNames; 101 integralPrintNames = (Hashtable)oldNames.clone(); 102 103 // @review kiniry - Translation of Clement's French comment: 104 // If we are going to do something, always pretty-print! 105 //if (escjava.Main.options().prettyPrintVC) 106 to = new PrintStream(new escjava.prover.PPOutputStream(to)); 107 108 VcToStringPvs vts = new VcToStringPvs(); 109 vts.printDefpreds(to, vts.getDefpreds(e)); 110 //to.println("\n(EXPLIES "); 111 to.println("\n(EXPLIES("); 112 vts.printFormula(to, e); 113 //to.println(" (AND "); 114 to.println(",true))"); 115 116 // /* Remove the distinct clause at the end of the output 117 // it's replaced by declaring pvs variables 118 // */ 119 120 //vts.distinctSymbols(to); 121 vts.stringLiteralAssumptions(to); 122 123 to.print("Start of pvs declarations :\n "); 124 125 vts.integralPrintNameOrder(to); 126 127 //to.println("))"); 128 129 integralPrintNames = oldNames; 130 131 /* This piece of code declares all variables before leaving */ 132 Iterator i = null; 133 String tempString = null; // makes the compiler happy 134 Integer tempInteger = null; 135 136 to.println("ecReturn : S"); 137 to.println("ecThrow : S;"); 138 139 /* was in the simplify logic */ 140 to.println("distinctAxiom : AXIOM\nrefEQ(ecReturn, ecThrow) = bool_false\n"); 141 142 /* list of functions declarations 143 144 It means : 145 listOfDeclFun = < f, g> 146 listOfDeclFunNbParam = < 1, 2> 147 148 will be translated to : 149 f(a : S) : S 150 g(a, b :S) : S 151 152 */ 153 154 if(listOfDeclFun.size() != listOfDeclFunNbParam.size()) 155 System.out.println("Warning, inconsistency in declaration of new functions..."); 156 157 if(listOfDeclFun.size()!=0) { /* something to declare */ 158 i = listOfDeclFun.iterator(); 159 Iterator j = listOfDeclFunNbParam.iterator(); 160 161 while(i.hasNext() && j.hasNext()){ 162 163 try { 164 tempString = (String)i.next(); 165 tempInteger = (Integer)j.next(); 166 } 167 catch(Exception ex){ 168 System.out.println("VcToStringPvs::add2Decl *** error *** "+ex); 169 } 170 171 /* name of the function, for example : g */ 172 to.print(tempString+"("); 173 char c = 'a'; 174 175 /* declaring (a1, a2 :S) for g for example 176 note that if there is more than 24 parameters, it will stupidly fail 177 because c++ will come back to a, anyway it should not happen 178 */ 179 for( int k = 0; k < tempInteger.intValue(); k++, c++) { 180 to.print(c); 181 to.print(" : S"); 182 183 if(k < tempInteger.intValue() - 1) /* not the last */ 184 to.print(" ,"); 185 else /* finishing declaration, adding ) : S at the end */ 186 to.print(") : S\n"); 187 //to.print(") : S = "+c +"\n"); // experimental 188 } 189 } 190 191 to.print(";\n"); 192 } 193 194 /* theorem */ 195 i = listOfDeclAdd.iterator(); 196 197 to.println("testTheorem : THEOREM\nFORALL("); 198 while(i.hasNext()){ 199 200 try{ tempString = (String)i.next();} 201 catch(Exception ex){ 202 System.out.println("VcToStringPvs::add2Decl *** error *** "+ex); 203 } 204 205 to.print(tempString); 206 207 if(i.hasNext()) 208 to.print(" , "); 209 210 } 211 212 to.print(" : S ) :\n"); 213 214 } 215 216 public static void computePC(/*@ non_null */Expr e, 217 /*@ non_null */PrintStream to) { 218 Hashtable oldNames = integralPrintNames; 219 integralPrintNames = (Hashtable)oldNames.clone(); 220 221 VcToString vts = new VcToString(); 222 to.println("\n(AND "); 223 vts.printFormula(to, e); 224 vts.distinctSymbols(to); 225 vts.stringLiteralAssumptions(to); 226 vts.integralPrintNameOrder(to); 227 to.println(")"); 228 229 integralPrintNames = oldNames; 230 } 231 232 // holds set of symbols used 233 //@ spec_public 234 protected/*@ non_null */Set symbols = new Set(); 235 236 // string of initial assumptions 237 //@ spec_public 238 protected/*@ non_null */Set stringLiterals = new Set(); 239 240 //+@ invariant integralPrintNames.keyType == \type(Long); 241 //+@ invariant integralPrintNames.elementType == \type(String); 242 //@ spec_public 243 protected static/*@ non_null */Hashtable integralPrintNames; 244 245 protected VcToStringPvs() {} 246 247 protected String vc2Term(/*@ non_null */Expr e, Hashtable subst) { 248 Assert.notNull(e); 249 ByteArrayOutputStream baos = new ByteArrayOutputStream(); 250 PrintStream ps = new PrintStream(baos); 251 printTerm(ps, subst, e); 252 String s = baos.toString(); 253 ps.close(); 254 // System.out.println("vc2Term yields: "+s); 255 256 return s; 257 } 258 259 protected void printDefpreds(/*@ non_null */PrintStream to, DefPredVec preds) { 260 for (int i = 0; i < preds.size(); i++) { 261 DefPred dp = preds.elementAt(i); 262 to.print("(DEFPRED (" + dp.predId); 263 for (int j = 0; j < dp.args.size(); j++) { 264 to.print(" " + dp.args.elementAt(j).id); 265 } 266 to.print(") "); 267 printFormula(to, dp.body); 268 to.print(")\n"); 269 } 270 } 271 272 protected DefPredVec preds; 273 274 protected DefPredVec getDefpreds(/*@ non_null */Expr e) { 275 preds = DefPredVec.make(); 276 getDefpredsHelper(e); 277 return preds; 278 } 279 280 protected void getDefpredsHelper(/*@ non_null */Expr e) { 281 if (e instanceof DefPredLetExpr) { 282 DefPredLetExpr dple = (DefPredLetExpr)e; 283 preds.append(dple.preds); 284 } 285 for (int i = 0; i < e.childCount(); i++) { 286 Object c = e.childAt(i); 287 if (c instanceof Expr) { 288 getDefpredsHelper((Expr)c); 289 } 290 } 291 } 292 293 /* 294 the call to this fonction has been removed 295 as it's useless for the pvs logic 296 */ 297 protected void distinctSymbols(/*@ non_null */PrintStream to) { 298 299 to.print("(DISTINCT"); 300 Enumeration e = symbols.elements(); 301 302 while (e.hasMoreElements()) { 303 String s = (String)e.nextElement(); 304 to.print(" "); 305 306 } 307 to.print(")"); 308 } 309 310 protected void stringLiteralAssumptions(/*@ non_null */PrintStream to) { 311 Enumeration e = stringLiterals.elements(); 312 while (e.hasMoreElements()) { 313 String litname = (String)e.nextElement(); 314 315 to.print(" (NEQ "); 316 to.print(litname); 317 to.print(" null)"); 318 319 to.print(" (EQ (typeof "); 320 to.print(litname); 321 to.print(") |T_java.lang.String|)"); 322 323 // We could also assume "litname" to be allocated (but at this 324 // time we don't have the name of the initial value of "alloc"; 325 // probably it is "alloc", but it would be nice not to have to 326 // rely on that here). 327 } 328 } 329 330 // ====================================================================== 331 332 protected void printFormula(/*@ non_null */PrintStream out, 333 /*@ non_null */Expr e) { 334 // maps GenericVarDecls to Strings 335 // some complex invariant here 336 337 Hashtable subst = new Hashtable(); 338 printFormula(out, subst, e); 339 } 340 341 protected void printFormula(/*@ non_null */PrintStream out, Hashtable subst, 342 /*@ non_null */Expr e) { 343 Assert.notNull(e); 344 345 reallyPrintFormula(out, subst, e); 346 347 } 348 349 350 protected void reallyPrintFormula(/*@ non_null */PrintStream out, 351 Hashtable subst, 352 /*@ non_null */Expr e) { 353 354 //++ 355 // System.out.println("VcToStringPvs::reallyPrintFormula"); 356 //++ 357 358 switch (e.getTag()) { 359 360 case TagConstants.DEFPREDLETEXPR: { 361 DefPredLetExpr dple = (DefPredLetExpr)e; 362 printFormula(out, subst, dple.body); 363 break; 364 } 365 366 case TagConstants.SUBSTEXPR: { 367 SubstExpr se = (SubstExpr)e; 368 // perform current substitution on expression 369 String expr = vc2Term(se.val, subst); 370 // get old val, install new val 371 Object old = subst.put(se.var, expr); 372 //System.out.println("old="+old); 373 374 // print 375 printFormula(out, subst, se.target); 376 377 // restore old state 378 if (old == null) subst.remove(se.var); 379 else subst.put(se.var, old); 380 381 break; 382 } 383 384 case TagConstants.LABELEXPR: { 385 LabelExpr le = (LabelExpr)e; 386 // out.print("(" + (le.positive ? "LBLPOS" : "LBLNEG") + " |" + le.label 387 // + "| "); 388 // printFormula(out, subst, le.expr); 389 // out.print(")"); 390 out.println("%LBL"+(le.positive ? "POS" : "NEG")+replaceBadChar(le.label.toString())+"% "); 391 printFormula(out, subst, le.expr); 392 393 break; 394 } 395 396 case TagConstants.GUARDEXPR: { 397 if (!escjava.Main.options().guardedVC) { 398 Assert.fail("VcToString.reallyPrintFormula: unreachable"); 399 } else { 400 GuardExpr ge = (GuardExpr)e; 401 String var = escjava.Main.options().guardedVCPrefix 402 + UniqName.locToSuffix(ge.locPragmaDecl); 403 //out.print("(IMPLIES |" + var + "| "); 404 out.print("(IMPLIES " + replaceBadChar(var) + " "); 405 printFormula(out, subst, ge.expr); 406 out.print(")"); 407 escjava.Main.options().guardVars.add(var); 408 break; 409 } 410 } 411 412 case TagConstants.FORALL: 413 case TagConstants.EXISTS: { 414 QuantifiedExpr qe = (QuantifiedExpr)e; 415 if (qe.quantifier == TagConstants.FORALL) out.print("(FORALL ("); 416 else out.print("(EXISTS ("); 417 418 // System.out.println("qe.vars.size() "+qe.vars.size()); 419 420 String prefix = ""; 421 for (int i = 0; i < qe.vars.size(); i++) { 422 GenericVarDecl decl = qe.vars.elementAt(i); 423 Assert.notFalse(!subst.containsKey(decl), "Quantification over " 424 + "substituted variable"); 425 out.print(prefix); 426 427 // name of the variable 428 printVarDecl(out, decl); 429 430 // type 431 out.print(" : S"); 432 433 // // writing comma, fixme 434 if(i < qe.vars.size()-1) 435 out.print(","); 436 437 prefix = " "; 438 } 439 // out.print(") "); 440 441 // add the : after FORALL in pvs 442 out.print(") : \n"); 443 444 if (qe.nopats != null && qe.nopats.size() != 0) { 445 Assert.notFalse(!insideNoPats); 446 insideNoPats = true; 447 out.print("(NOPATS"); 448 for (int i = 0; i < qe.nopats.size(); i++) { 449 out.print(" "); 450 Expr nopat = qe.nopats.elementAt(i); 451 printTerm(out, subst, nopat); 452 } 453 out.print(") "); 454 insideNoPats = false; 455 } 456 if (qe.pats != null && qe.pats.size() != 0) { 457 Assert.notFalse(!insideNoPats); 458 insideNoPats = true; 459 if (qe.pats.size() == 1) out.print("(PATS"); 460 else out.print("(PATS (MPAT"); 461 for (int i = 0; i < qe.pats.size(); i++) { 462 out.print(" "); 463 Expr nopat = qe.pats.elementAt(i); 464 printTerm(out, subst, nopat); 465 } 466 if (qe.pats.size() == 1) out.print(") "); 467 else out.print("))"); 468 insideNoPats = false; 469 } 470 printFormula(out, subst, qe.expr); 471 /* for pvs, 472 useless since we added conversion between S and bool */ 473 out.print(" = bool_true "); 474 475 out.print(") "); 476 477 break; 478 } 479 480 // Operators on formulas 481 case TagConstants.BOOLIMPLIES: 482 case TagConstants.BOOLAND: 483 case TagConstants.BOOLANDX: 484 case TagConstants.BOOLOR: 485 case TagConstants.BOOLNOT: 486 case TagConstants.BOOLEQ: { 487 NaryExpr ne = (NaryExpr)e; 488 String op; 489 boolean normalCase = true; 490 String pvsOp = null; 491 492 switch (ne.getTag()) { 493 case TagConstants.BOOLIMPLIES: 494 //op = "IMPLIES"; 495 op = "boolImplies"; 496 break; 497 case TagConstants.BOOLAND: 498 case TagConstants.BOOLANDX: 499 //op = "AND"; 500 op = "boolAnd"; 501 normalCase = false; 502 pvsOp = "AND"; 503 break; 504 case TagConstants.BOOLOR: 505 //op = "OR"; 506 op = "boolOr"; 507 normalCase = false; 508 pvsOp = "OR"; 509 break; 510 case TagConstants.BOOLNOT: 511 //op = "NOT"; 512 op = "boolNot"; 513 break; 514 case TagConstants.BOOLEQ: 515 //op = "IFF"; 516 op = "boolEq"; 517 break; 518 default: 519 Assert.fail("Fall thru"); 520 op = null; // dummy assignment 521 } 522 523 /* (EQ a b c d) => 524 * boolAnd(EQ(a ,b), EQ(b,c)) AND boolAnd( EQ(b,c), EQ(c,d))) 525 */ 526 527 out.print(op+"("); 528 529 for (int i = 0; i < ne.exprs.size(); i++) { 530 out.print("("); 531 printFormula(out, subst, ne.exprs.elementAt(i)); 532 out.print(")"); 533 534 if((i < ne.exprs.size() - 1)){ /* not the last */ 535 536 if( isEven(i) ) 537 out.print(","); 538 else { 539 // this is the pvs operator for bool 540 if((i < ne.exprs.size() - 2)){ 541 out.print(")"+pvsOp+" "+op+"( "); 542 } 543 else /* before last */ 544 out.print(")"+pvsOp+" "+"( "); 545 } 546 } 547 548 } 549 out.print(")"); 550 551 // /* 552 // * Variant of the code for current_unsorted_logic_variante.pvs 553 // */ 554 555 // int nbBracket = 0; 556 // int j = 0; 557 558 // out.print(op+"("); 559 560 // if(normalCase){ 561 // for (int i = 0; i < ne.exprs.size(); i++) { 562 // printFormula(out, subst, ne.exprs.elementAt(i)); 563 564 // if( i != ne.exprs.size() -1) 565 // out.print(","); 566 // } 567 // } 568 // else { 569 570 // if(ne.exprs.size() == 2){ // no need for a list 571 // printFormula(out, subst, ne.exprs.elementAt(0)); 572 // out.print(","); 573 // printFormula(out, subst, ne.exprs.elementAt(1)); 574 575 // } 576 // else { 577 // for (int i = 0; i < ne.exprs.size(); i++) { 578 // out.print("cons("); 579 // printFormula(out, subst, ne.exprs.elementAt(i)); 580 // out.print(","); 581 582 // if(i == (ne.exprs.size() -1)) {// last 583 // out.print("null"); 584 // for( int j2 = 0; j2 <= i; j2++) 585 // out.print(")"); 586 // } 587 // } 588 // } 589 // } 590 591 // out.print(")"); 592 593 break; 594 } 595 596 case TagConstants.BOOLNE: { 597 NaryExpr ne = (NaryExpr)e; 598 out.print("(IFF "); 599 printFormula(out, subst, ne.exprs.elementAt(0)); 600 out.print(" (NOT "); 601 printFormula(out, subst, ne.exprs.elementAt(1)); 602 out.print("))"); 603 break; 604 } 605 606 case TagConstants.METHODCALL: { 607 NaryExpr ne = (NaryExpr)e; 608 609 /* 610 * useless to add EQ( true, call_to_fonction_returning_bool) 611 * in pvs 612 */ 613 614 //++ 615 // System.out.println("VcToStringPvs::reallyPrintFormula::MethodCall"); 616 //++ 617 618 //out.print("(EQ |@true| ( |"); 619 out.print(ne.methodName); 620 //out.print("| "); 621 int n = ne.exprs.size(); 622 for (int i = 0; i < n; i++) { 623 printTerm(out, subst, ne.exprs.elementAt(i)); 624 out.print(" "); 625 } 626 out.print("))"); 627 break; 628 } 629 630 // PredSyms 631 case TagConstants.ALLOCLT: 632 case TagConstants.ALLOCLE: 633 case TagConstants.ANYEQ: 634 case TagConstants.ANYNE: 635 case TagConstants.INTEGRALEQ: 636 case TagConstants.INTEGRALGE: 637 case TagConstants.INTEGRALGT: 638 case TagConstants.INTEGRALLE: 639 case TagConstants.INTEGRALLT: 640 case TagConstants.INTEGRALNE: 641 case TagConstants.LOCKLE: 642 case TagConstants.LOCKLT: 643 case TagConstants.REFEQ: 644 case TagConstants.REFNE: 645 case TagConstants.TYPEEQ: 646 case TagConstants.TYPENE: 647 case TagConstants.TYPELE: { 648 NaryExpr ne = (NaryExpr)e; 649 String op; 650 boolean possibleDeclarationOfStackTrace = false; 651 652 switch (ne.getTag()) { 653 case TagConstants.ALLOCLT: 654 op = "lockLT"; 655 break; 656 case TagConstants.ALLOCLE: 657 op = "lockLE"; 658 break; 659 case TagConstants.ANYEQ: 660 //op = "EQ"; 661 op = "refEQ"; 662 possibleDeclarationOfStackTrace = true; 663 // for elems, alloc 664 break; 665 case TagConstants.ANYNE: 666 //op = "NEQ"; 667 op = "refNE"; 668 break; 669 case TagConstants.INTEGRALEQ: 670 //op = "EQ"; 671 op = "integralEQ"; 672 break; 673 case TagConstants.INTEGRALGE: 674 op = "integralGE"; 675 break; 676 case TagConstants.INTEGRALGT: 677 op = "integralGT"; 678 break; 679 case TagConstants.INTEGRALLE: 680 op = "integralLE"; 681 break; 682 case TagConstants.INTEGRALLT: 683 op = "integralLT"; 684 break; 685 case TagConstants.INTEGRALNE: 686 //op = "NEQ"; 687 op = "integralNE"; 688 break; 689 case TagConstants.LOCKLE: 690 op = TagConstants.toVcString(TagConstants.LOCKLE); 691 break; 692 case TagConstants.LOCKLT: 693 op = TagConstants.toVcString(TagConstants.LOCKLT); 694 break; 695 case TagConstants.REFEQ: 696 //op = "EQ"; 697 op = "refEQ"; 698 break; 699 case TagConstants.REFNE: 700 //op = "NEQ"; 701 op = "refNE"; 702 break; 703 case TagConstants.TYPEEQ: 704 //op = "EQ"; 705 //op = "typeEQ"; 706 op = "="; 707 break; 708 case TagConstants.TYPENE: 709 //op = "NEQ"; 710 //op = "typeNE"; 711 op = "/="; 712 break; 713 case TagConstants.TYPELE: 714 //op = "<:"; 715 op = "<="; 716 break; 717 default: 718 Assert.fail("Fall thru"); 719 op = null; // dummy assignment 720 } 721 722 //out.print("(" + op); 723 out.print(op + "("); 724 for (int i = 0; i < ne.exprs.size(); i++) { 725 if( i>=1 ) out.print(", "); 726 //out.print(" "); 727 // makes it more 'readable' cough cough... 728 printTerm(out, subst, ne.exprs.elementAt(i)); 729 } 730 out.print(")"); 731 break; 732 } 733 734 default: { 735 if (e.getTag() == TagConstants.DTTFSA) { 736 NaryExpr ne = (NaryExpr)e; 737 TypeExpr te = (TypeExpr)ne.exprs.elementAt(0); 738 if (Types.isBooleanType(te.type)) { 739 // print this DTTFSA as a predicate 740 printDttfsa(out, subst, ne); 741 break; 742 } 743 } 744 // not a predicate, must be a term 745 746 // the two next lines are useless in pvs 747 748 //out.print("(EQ |@true| "); 749 printTerm(out, subst, e); 750 //out.print(")"); 751 break; 752 } 753 } 754 } 755 756 protected boolean isEven(int i){ 757 758 int j = i/2; 759 760 return ((j * 2) == i); 761 762 } 763 764 // ====================================================================== 765 766 /** 767 * <code>insideNoPats</code> is really a parameter to * 768 * <code>printTerm</code>. 769 */ 770 771 protected boolean insideNoPats = false; 772 773 protected void printTerm(/*@ non_null */PrintStream out, Hashtable subst, 774 /*@ non_null */Expr e) { 775 776 //++ 777 // System.out.println("VcToStringPvs::printTerm"); 778 //++ 779 780 int tag = e.getTag(); 781 boolean possibleNewPvsFunction = false; 782 783 switch (tag) { 784 785 case TagConstants.SUBSTEXPR: { 786 787 //++ 788 // System.out.println("printTerm::SUBSTEXPR"); 789 //++ 790 791 SubstExpr se = (SubstExpr)e; 792 // perform current substitution on expression 793 String expr = vc2Term(se.val, subst); 794 795 // get old val, install new val 796 Object old = subst.put(se.var, expr); 797 // print 798 printTerm(out, subst, se.target); 799 800 // restore old state 801 if (old == null) subst.remove(se.var); 802 else subst.put(se.var, old); 803 804 break; 805 } 806 807 case TagConstants.DEFPREDAPPLEXPR: { 808 809 //++ 810 // System.out.println("printTerm::DEFPREDAPPLEXPR"); 811 //++ 812 813 814 DefPredApplExpr dpae = (DefPredApplExpr)e; 815 out.print("(" + dpae.predId); 816 for (int i = 0; i < dpae.args.size(); i++) { 817 out.print(" "); 818 printTerm(out, subst, dpae.args.elementAt(i)); 819 } 820 out.print(")"); 821 break; 822 } 823 824 case TagConstants.TYPEEXPR: { 825 826 //++ 827 // System.out.println("printTerm::TYPEEXPR"); 828 //++ 829 830 TypeExpr te = (TypeExpr)e; 831 832 //System.out.println(BackPred.simplifyTypeName(te.type)); 833 834 // remove | around type name 835 836 out.print(replaceBadChar(BackPred.simplifyTypeName(te.type))); 837 break; 838 } 839 840 // Literals 841 842 // This handles case 8 of ESCJ 23b: 843 case TagConstants.STRINGLIT: { 844 845 //++ 846 // System.out.println("printTerm::STRINGLIT"); 847 //++ 848 849 LiteralExpr le = (LiteralExpr)e; 850 String s = "S_" + UniqName.locToSuffix(le.loc); 851 s = Atom.printableVersion(s); 852 stringLiterals.add(s); 853 out.print(s); 854 break; 855 } 856 857 case TagConstants.BOOLEANLIT: { 858 859 //++ 860 // System.out.println("printTerm::BOOLEANLIT"); 861 //++ 862 863 LiteralExpr le = (LiteralExpr)e; 864 // if (((Boolean)le.value).booleanValue()) out.print("|@true|"); 865 if (((Boolean)le.value).booleanValue()) out.print("bool_true "); 866 // else out.print("|bool$false|"); 867 else out.print("bool_false "); 868 break; 869 } 870 871 case TagConstants.CHARLIT: 872 case TagConstants.INTLIT: { 873 LiteralExpr le = (LiteralExpr)e; 874 //out.print(integralPrintName(((Integer)le.value).intValue())); 875 876 /* 877 * In case of special value, this fonction can print 878 * neg2147483648 or pos2147483647 (and normal int like 1 or 2). 879 * But in the latter case, we have to convert it to 880 * real_to_S(1) otherwise pvs will consider it as a real 881 */ 882 883 String s = integralPrintName(((Integer)le.value).intValue()); 884 885 /* lame way to determine if it's negXXXX or a 'normal int' */ 886 887 if( s.charAt(0)=='n' || s.charAt(0)=='p' ) 888 out.print(s); 889 else 890 out.print("real_to_S("+s+")"); 891 892 break; 893 } 894 895 case TagConstants.LONGLIT: { 896 LiteralExpr le = (LiteralExpr)e; 897 out.print(integralPrintName(((Long)le.value).longValue())); 898 break; 899 } 900 901 case TagConstants.FLOATLIT: { 902 LiteralExpr le = (LiteralExpr)e; 903 out.print("|F_" + ((Float)le.value).floatValue() + "|"); 904 break; 905 } 906 907 case TagConstants.DOUBLELIT: { 908 LiteralExpr le = (LiteralExpr)e; 909 out.print("|F_" + ((Double)le.value).doubleValue() + "|"); 910 break; 911 } 912 913 case TagConstants.NULLLIT: 914 //out.print("null"); 915 out.print("java_null"); 916 break; 917 918 case TagConstants.SYMBOLLIT: { 919 // Handles case 5 of ESCJ 23b: 920 LiteralExpr le = (LiteralExpr)e; 921 //String s = "|" + (String)le.value + "|"; 922 923 String s = (String)le.value; 924 symbols.add(s); 925 926 //System.out.println("TagConstants.SYMBOLLIT:"+s); 927 928 // name of different path to reach end of fonction 929 930 out.print(s); 931 break; 932 } 933 934 case TagConstants.VARIABLEACCESS: { 935 936 //++ 937 // System.out.println("VcToStringPvs::printTerm::VariableAccess"); 938 //++ 939 940 VariableAccess va = (VariableAccess)e; 941 String to = (String)subst.get(va.decl); 942 943 /* replace bad char in each case, because 944 * printVarDecl was modified too 945 */ 946 947 if (to != null) out.print(replaceBadChar(to)); 948 else printVarDecl(out, va.decl); 949 break; 950 } 951 952 // Nary functions 953 case TagConstants.ALLOCLT: 954 case TagConstants.ALLOCLE: 955 case TagConstants.ARRAYLENGTH: 956 case TagConstants.ARRAYFRESH: 957 case TagConstants.ARRAYMAKE: 958 case TagConstants.ARRAYSHAPEMORE: 959 case TagConstants.ARRAYSHAPEONE: 960 case TagConstants.ASELEMS: 961 case TagConstants.ASFIELD: 962 case TagConstants.ASLOCKSET: 963 case TagConstants.BOOLAND: 964 case TagConstants.BOOLANDX: 965 case TagConstants.BOOLEQ: 966 case TagConstants.BOOLIMPLIES: 967 case TagConstants.BOOLNE: 968 case TagConstants.BOOLNOT: 969 case TagConstants.BOOLOR: 970 case TagConstants.CLASSLITERALFUNC: 971 case TagConstants.CONDITIONAL: 972 case TagConstants.ELEMSNONNULL: 973 case TagConstants.ELEMTYPE: 974 case TagConstants.ECLOSEDTIME: 975 case TagConstants.FCLOSEDTIME: 976 977 case TagConstants.FLOATINGADD: 978 case TagConstants.FLOATINGDIV: 979 case TagConstants.FLOATINGEQ: 980 case TagConstants.FLOATINGGE: 981 case TagConstants.FLOATINGGT: 982 case TagConstants.FLOATINGLE: 983 case TagConstants.FLOATINGLT: 984 case TagConstants.FLOATINGMOD: 985 case TagConstants.FLOATINGMUL: 986 case TagConstants.FLOATINGNE: 987 case TagConstants.FLOATINGNEG: 988 case TagConstants.FLOATINGSUB: 989 990 case TagConstants.INTEGRALADD: 991 case TagConstants.INTEGRALAND: 992 case TagConstants.INTEGRALDIV: 993 case TagConstants.INTEGRALEQ: 994 case TagConstants.INTEGRALGE: 995 case TagConstants.INTEGRALGT: 996 case TagConstants.INTEGRALLE: 997 case TagConstants.INTEGRALLT: 998 case TagConstants.INTEGRALMOD: 999 case TagConstants.INTEGRALMUL: 1000 case TagConstants.INTEGRALNE: 1001 case TagConstants.INTEGRALNEG: 1002 case TagConstants.INTEGRALNOT: 1003 case TagConstants.INTEGRALOR: 1004 case TagConstants.INTSHIFTL: 1005 case TagConstants.LONGSHIFTL: 1006 case TagConstants.INTSHIFTR: 1007 case TagConstants.LONGSHIFTR: 1008 case TagConstants.INTSHIFTRU: 1009 case TagConstants.LONGSHIFTRU: 1010 case TagConstants.INTEGRALSUB: 1011 case TagConstants.INTEGRALXOR: 1012 1013 case TagConstants.INTERN: 1014 case TagConstants.INTERNED: 1015 case TagConstants.IS: 1016 case TagConstants.ISALLOCATED: 1017 case TagConstants.ISNEWARRAY: 1018 case TagConstants.LOCKLE: 1019 case TagConstants.LOCKLT: 1020 case TagConstants.MAX: 1021 case TagConstants.METHODCALL: 1022 case TagConstants.REFEQ: 1023 case TagConstants.REFNE: 1024 case TagConstants.SELECT: 1025 case TagConstants.STORE: 1026 case TagConstants.STRINGCAT: 1027 case TagConstants.STRINGCATP: 1028 case TagConstants.TYPEEQ: 1029 case TagConstants.TYPENE: 1030 case TagConstants.TYPELE: 1031 case TagConstants.TYPEOF: 1032 case TagConstants.UNSET: 1033 case TagConstants.VALLOCTIME: { 1034 NaryExpr ne = (NaryExpr)e; 1035 String op = null; //compiler happy \o/ 1036 switch (tag) { 1037 case TagConstants.INTEGRALADD: 1038 op = "+"; 1039 break; 1040 case TagConstants.INTEGRALMUL: 1041 op = "*"; 1042 break; 1043 case TagConstants.INTEGRALNEG: 1044 //op = "- 0"; 1045 op = "-"; 1046 break; 1047 case TagConstants.INTEGRALSUB: 1048 op = "-"; 1049 break; 1050 case TagConstants.TYPELE: 1051 op = "<:"; 1052 break; 1053 case TagConstants.METHODCALL: 1054 1055 /* 1056 * Here you catch the call to function like 1057 * java.lang.Throwable#_state 1058 */ 1059 1060 //op = "|" + ne.methodName.toString() + "|"; 1061 1062 op = ne.methodName.toString(); 1063 1064 op = replaceBadChar(op); 1065 1066 //++ 1067 // System.out.println("printTerm::METHODCALL "+op); 1068 //++ 1069 1070 /* in order to declare the fonction after */ 1071 possibleNewPvsFunction = true; 1072 1073 break; 1074 case TagConstants.INTEGRALNE: 1075 case TagConstants.REFNE: 1076 case TagConstants.TYPENE: 1077 case TagConstants.ANYNE: 1078 if (insideNoPats) { 1079 op = "NEQ"; 1080 break; 1081 } 1082 // fall thru 1083 default: 1084 1085 op = TagConstants.toVcString(tag); 1086 1087 //++ 1088 // System.out.println("printTerm::default "+op); 1089 //++ 1090 1091 } 1092 1093 // (typeof X) => typeOf( ) 1094 1095 //out.print("(" + op); 1096 out.print(op + "("); 1097 for (int i = 0; i < ne.exprs.size(); i++) { 1098 1099 /* makes it more readable */ 1100 if(i!=0) 1101 out.print(", "); 1102 1103 printTerm(out, subst, ne.exprs.elementAt(i)); 1104 } 1105 out.print(")"); 1106 1107 if(possibleNewPvsFunction) /* declaration of the function, by adding 1108 it to the appropriate set */ 1109 add2DeclFun(op,ne.exprs.size()); 1110 1111 break; 1112 } 1113 1114 case TagConstants.CAST: { 1115 1116 //++ 1117 // System.out.println("TagConstants.CAST"); 1118 //++ 1119 1120 NaryExpr ne = (NaryExpr)e; 1121 Assert.notFalse(ne.exprs.size() == 2); 1122 Expr x = ne.exprs.elementAt(0); 1123 TypeExpr t = (TypeExpr)ne.exprs.elementAt(1); 1124 1125 if (Types.isBooleanType(t.type)) { 1126 // Peephole optimization to remove casts to boolean, since 1127 // anything is a boolean in the underlying logic (it either 1128 // equals |@true| or it doesn't). The reason this peephole 1129 // optimization is performed here, rather than in trExpr 1130 // and trSpecExpr, is that then any expression cast to a 1131 // boolean will be printed as a term, not as a predicate. 1132 // This may sometimes be useful for boolean DTTFSA expression, 1133 // which are printed as predicate whenever they occur in 1134 // predicate positions. 1135 printTerm(out, subst, x); 1136 } else { 1137 out.print("("); 1138 out.print(TagConstants.toVcString(tag)); 1139 out.print(" "); 1140 printTerm(out, subst, x); 1141 out.print(" "); 1142 printTerm(out, subst, t); 1143 out.print(")"); 1144 } 1145 break; 1146 } 1147 1148 case TagConstants.DTTFSA: { 1149 NaryExpr ne = (NaryExpr)e; 1150 printDttfsa(out, subst, ne); 1151 break; 1152 } 1153 1154 default: 1155 Assert.fail("Bad tag in GCTerm: " + "(tag=" + tag + "," 1156 + TagConstants.toVcString(tag) + ") " + e); 1157 } 1158 } 1159 1160 //@ requires ne.op == TagConstants.DTTFSA; 1161 protected void printDttfsa(/*@ non_null */PrintStream out, Hashtable subst, 1162 /*@ non_null */NaryExpr ne) { 1163 LiteralExpr lit = (LiteralExpr)ne.exprs.elementAt(1); 1164 String op = (String)lit.value; 1165 if (ne.exprs.size() == 2) { 1166 out.print(op); 1167 } else if (op.equals("identity")) { 1168 Assert.notFalse(ne.exprs.size() == 3); 1169 Expr e2 = ne.exprs.elementAt(2); 1170 printTerm(out, subst, e2); 1171 } else { 1172 out.print("("); 1173 out.print(op); 1174 for (int i = 2; i < ne.exprs.size(); i++) { 1175 out.print(" "); 1176 Expr ei = ne.exprs.elementAt(i); 1177 printTerm(out, subst, ei); 1178 } 1179 out.print(")"); 1180 } 1181 } 1182 1183 // ====================================================================== 1184 1185 protected void printVarDecl(/*@ non_null */PrintStream out, GenericVarDecl decl) { 1186 // remove bacChar 1187 1188 //out.print(Atom.printableVersion(UniqName.variable(decl))); 1189 1190 out.print(replaceBadChar(Atom.printableVersion(UniqName.variable(decl)))); 1191 } 1192 1193 // ====================================================================== 1194 1195 protected static final long MaxIntegral = 1000000; 1196 1197 protected static final/*@ non_null */Long minThreshold = new Long(-MaxIntegral); 1198 1199 protected static final/*@ non_null */Long maxThreshold = new Long(MaxIntegral); 1200 1201 /** 1202 * * Convert an integral # into its printname according to the rules * of ESCJ 1203 * 23b, part 9. 1204 */ 1205 1206 protected/*@ non_null */String integralPrintName(long n) { 1207 if (-MaxIntegral <= n && n <= MaxIntegral) { 1208 return String.valueOf(n); 1209 } 1210 1211 Long l = new Long(n); 1212 String name = (String)integralPrintNames.get(l); 1213 if (name != null) { 1214 return name; 1215 } 1216 1217 if (n == -n) { 1218 // Need to handle minlong specially... 1219 name = "neg" + String.valueOf(n).substring(1); 1220 } else if (n < 0) { 1221 name = "neg" + String.valueOf(-n); 1222 } else { 1223 name = "pos" + String.valueOf(n); 1224 } 1225 1226 integralPrintNames.put(l, name); 1227 return name; 1228 } 1229 1230 /** Generates the inequalities that compare the integral literals 1231 * that were replaced in <code>integralPrintName</code> by symbolic 1232 * names. 1233 **/ 1234 1235 protected void integralPrintNameOrder(/*@ non_null */PrintStream ps) { 1236 int n = integralPrintNames.size(); 1237 Assert.notFalse(2 <= n); // should contain the two thresholds 1238 if (n == 0) { 1239 return; 1240 } 1241 1242 Long[] keys = new Long[n]; 1243 Enumeration e = integralPrintNames.keys(); 1244 for (int i = 0; e.hasMoreElements(); i++) { 1245 Long l = (Long)e.nextElement(); 1246 keys[i] = l; 1247 } 1248 Arrays.sort(keys); 1249 1250 /* added for pvs */ 1251 StringBuffer pvsDecl = new StringBuffer("\n"); 1252 StringBuffer pvsAxiom = new StringBuffer("\n"); 1253 boolean somethingToDeclare = false; 1254 1255 String valueI = (String)integralPrintNames.get(keys[0]); 1256 1257 /* loop invariant: valueI == integralPrintNames.get(keys[i]); */ 1258 for (int i = 0; i < n - 1; i++) { 1259 1260 /* This loop can be runned even if their is no declaration 1261 That's the need for somethingToDeclare raises */ 1262 1263 String valueNext = (String)integralPrintNames.get(keys[i + 1]); 1264 if (keys[i] == minThreshold) { 1265 Assert.notFalse(keys[i + 1] == maxThreshold); 1266 } else { 1267 1268 // Ugly hack to print it only the first time 1269 if(!somethingToDeclare) { 1270 pvsAxiom.append("integralAxiom : AXIOM("); 1271 somethingToDeclare = true; 1272 } 1273 1274 /* lame way to determine if it's negXXXX or 10000 1275 (as we must declare only negXXXX in this case) */ 1276 1277 pvsAxiom.append("("); 1278 1279 if( valueI.charAt(0)=='n' || valueI.charAt(0)=='p' ) 1280 /* valueI is the int declared */ 1281 pvsDecl.append(valueI+ " : S"); 1282 else 1283 pvsDecl.append(valueNext+ " : S"); 1284 1285 pvsAxiom.append(valueI + " < "+ valueNext); 1286 1287 pvsDecl.append("\n"); 1288 pvsAxiom.append(")"); 1289 1290 } 1291 1292 if( i < n - 2 && i != 0) /* another declaration after */ 1293 pvsAxiom.append("AND"); 1294 1295 valueI = valueNext; 1296 } 1297 1298 if(somethingToDeclare) 1299 pvsAxiom.append(")"); 1300 1301 ps.print(pvsDecl.toString()); 1302 ps.print(pvsAxiom.toString()); 1303 1304 } 1305 1306 static { 1307 resetTypeSpecific(); 1308 } 1309 1310 static private int add2Decl(String s){ 1311 1312 if( s.charAt(0) == '%') 1313 return 0; 1314 1315 Iterator i = listOfDecl.iterator(); 1316 String temp = null; // make the compiler happy 1317 1318 while(i.hasNext()){ 1319 1320 try{ temp = (String)i.next();} 1321 catch(Exception e){ 1322 System.out.println("VcToStringPvs::add2Decl *** error *** "+e); 1323 } 1324 1325 if( s.compareTo(temp) == 0) 1326 return 0; 1327 } 1328 1329 i = listOfDeclAdd.iterator(); 1330 1331 while(i.hasNext()){ 1332 1333 try{ temp = (String)i.next();} 1334 catch(Exception e){ 1335 System.out.println("VcToStringPvs::add2Decl *** error *** "+e); 1336 } 1337 1338 if( s.compareTo(temp) == 0) 1339 return 0; 1340 } 1341 1342 listOfDeclAdd.add(s); 1343 1344 //++ 1345 // System.out.println("Adding "+s+" to the listOfDecl"); 1346 //++ 1347 1348 return 1; 1349 } 1350 1351 static private int add2DeclFun(String s, int nbParameters){ 1352 1353 if( s.charAt(0) == '%') 1354 return 0; 1355 1356 Iterator i = listOfDeclFun.iterator(); 1357 String temp = null; // make the compiler happy 1358 1359 while(i.hasNext()){ 1360 1361 try{ temp = (String)i.next();} 1362 catch(Exception e){ 1363 System.out.println("VcToStringPvs::add2AdditionalDecl *** error *** "+e); 1364 } 1365 1366 if( s.compareTo(temp) == 0) 1367 return 0; 1368 } 1369 1370 listOfDeclFun.add(s); 1371 1372 /* this is so crappy, not to be able to push an int direclty */ 1373 listOfDeclFunNbParam.add(new Integer(nbParameters)); 1374 1375 //++ 1376 // if(listOfDeclFun.size() != listOfDeclFunNbParam.size()) 1377 // System.out.println("Warning, inconsistency in declaration of new functions..."); 1378 //++ 1379 1380 //++ 1381 // System.out.println("Adding "+s+", with arity "+nbParameters+" to listOfDeclFun"); 1382 //++ 1383 1384 return 1; 1385 } 1386 1387 public static String replaceBadChar(String s){ 1388 1389 // remove beginning and ending | 1390 if(s.charAt(0) == '|') 1391 s = s.substring(1,s.length()-1); 1392 1393 if(s.charAt(s.length()-1) == '|') 1394 s = s.substring(0,s.length()-2); 1395 1396 s = s.replace('@','_').replace('#','_').replace('|','_').replace('.','_').replace(':','_').replace('<','_').replace('>','_').replace('-','_').replace('^','_').replace(',','_').replace('[','_').replace(']','_').replace('!','_').replace('(','_').replace(')','_').replace(' ','_'); 1397 1398 if(s.compareTo("o") == 0) /* handle the case where a variable 1399 is named just 'o' which is a special 1400 variable in pvs */ 1401 s = "o_"; 1402 1403 /* delete _ at the beginning of variable names, coz it's forbidden in pvs */ 1404 while(s.charAt(0)=='_') 1405 s = s.substring(1,s.length()); 1406 1407 add2Decl(s); 1408 1409 return s; 1410 } 1411 1412 }