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