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