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 */