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    }