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