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