001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.backpred;
004    
005    import java.util.*;
006    import java.io.*;
007    
008    import javafe.ast.*;
009    import javafe.tc.*;
010    import javafe.util.*;
011    
012    import escjava.Main;
013    import escjava.ast.TagConstants;
014    import escjava.ast.TypeExpr;
015    import escjava.prover.Atom;
016    import escjava.translate.*;
017    
018    /**
019     * Generates the background predicate for a given type.
020     *
021     * <p> The background predicate <I>for</I> a particular class or
022     * interface type T consists of the conjunction of the background
023     * predicates contributions of each contributor class. See
024     * <code>FindContributors</code> for the definition of the
025     * contributors of a class.
026    
027     * <p> A type must be typechecked in order to generate its background
028     * predicate.  A type need only be prepped in order to generate its
029     * background predicate contribution.
030     */
031    
032    public class BackPred
033    {
034        /**
035         * Returns the universal background predicate as a sequence of
036         * simplify commands. 
037         */
038    
039        public static void genUnivBackPred(/*@ non_null */ PrintStream proverStream) {
040            if (escjava.Main.options().univBackPredFile == null) {
041                proverStream.print(DefaultUnivBackPred.s);
042                return;
043            }
044            String filename = escjava.Main.options().univBackPredFile;
045            try {
046                FileInputStream fis = null;
047                try {
048                    fis = new FileInputStream(filename);
049                    int c;
050                    while( (c=fis.read()) != -1 ) proverStream.print((char)c);
051                } finally {
052                    if (fis != null) fis.close();
053                }
054            } catch( IOException e) {
055                ErrorSet.fatal("IOException: "+e);
056            }
057        }
058    
059    
060        /**
061         * Return the type-specific background predicate as a formula.
062         */
063        public static void genTypeBackPred(/*@ non_null */ FindContributors scope,
064                                           /*@ non_null */ PrintStream proverStream) {
065            // set up the background predicate buffer
066            proverStream.print("(AND ");
067    
068            // set up the distinct types axiom buffer
069            StringBuffer dta =
070                new StringBuffer("(DISTINCT arrayType |"
071                                 + UniqName.type(Types.booleanType) + "| |"
072                                 + UniqName.type(Types.charType) + "| |"
073                                 + UniqName.type(Types.byteType) + "| |"
074                                 + UniqName.type(Types.shortType) + "| |"
075                                 + UniqName.type(Types.intType) + "| |"
076                                 + UniqName.type(Types.longType) + "| |"
077                                 + UniqName.type(Types.floatType) + "| |"
078                                 + UniqName.type(Types.doubleType) + "| |"
079                                 + UniqName.type(escjava.tc.Types.typecodeType) + "|");
080    
081    
082            // Print them out, and add their contribution to the BP. 
083            Info.out("[TypeSig contributors for "
084                     +Types.printName(scope.originType)+":");
085            for( Enumeration typeSigs = scope.typeSigs();
086                 typeSigs.hasMoreElements(); )
087            {
088                TypeSig sig2 = (TypeSig)typeSigs.nextElement();
089                Info.out("    "+Types.printName( sig2 ));
090                addContribution( sig2.getTypeDecl(), proverStream );
091                dta.append(" "+simplifyTypeName( sig2 ) );
092            }
093            Info.out("]");
094    
095    
096            // Add the distinct types axiom
097            bg( dta.toString()+")", proverStream );
098    
099    
100            // Handle constant fields' contribution:
101            for( Enumeration fields = scope.fields();
102            fields.hasMoreElements(); ) {
103                FieldDecl fd = (FieldDecl)fields.nextElement();
104                if (!Modifiers.isFinal(fd.modifiers) || fd.init==null)
105                    continue;
106                
107                int loc = fd.init.getStartLoc();
108                VariableAccess f = VariableAccess.make(fd.id, loc, fd);
109                
110                if (Modifiers.isStatic(fd.modifiers)) {
111                    genFinalInitInfo(fd.init, null, null, f, fd.type, loc, 
112                            proverStream);
113                } else {
114                    LocalVarDecl sDecl = UniqName.newBoundVariable('s');
115                    VariableAccess s = TrAnExpr.makeVarAccess(sDecl, Location.NULL);
116                    genFinalInitInfo(fd.init, sDecl, s, GC.select(f, s), fd.type, 
117                            loc, proverStream);
118                }
119            }
120            
121            proverStream.print(")");
122        }
123    
124        //@ requires loc != Location.NULL;
125        //@ requires sDecl != null ==> s != null;
126        private static void genFinalInitInfo(/*@ non_null */ VarInit initExpr,
127                                             GenericVarDecl sDecl, Expr s,
128                                             /*@ non_null */ Expr x,
129                                             /*@ non_null */ Type type,
130                                             int loc,
131                                             /*@ non_null */ PrintStream proverStream) {
132            /* The dynamic type of the field is subtype of the static type of the
133             * initializing expression.
134             */
135            {
136                Type exprType = TypeCheck.inst.getType(initExpr);
137                Expr tExpr = TypeExpr.make(initExpr.getStartLoc(),
138                                           initExpr.getEndLoc(),
139                                           exprType);
140                produce(sDecl, s, GC.nary(TagConstants.IS, x, tExpr), proverStream);
141            }
142    
143            /* Generate primitive type constant info */
144            if (type instanceof PrimitiveType) {
145                if (initExpr instanceof Expr) {
146                    Expr constant = eval((Expr)initExpr, loc);
147                    if (constant != null) {
148                        produce(sDecl, s, eq(x, constant, type), proverStream);
149                    }
150                }
151                return;
152            }
153    
154            /* Peel off parentheses and casts. */
155            int tag;
156            while (true) {
157                tag = initExpr.getTag();
158    
159                if (tag == TagConstants.PARENEXPR) {
160                    initExpr = ((ParenExpr)initExpr).expr;
161                } else if (tag == TagConstants.CASTEXPR) {
162                    initExpr = ((CastExpr)initExpr).expr;
163                } else if (tag == TagConstants.NEWARRAYEXPR) {
164                    NewArrayExpr nae = (NewArrayExpr)initExpr;
165                    if (nae.init != null) {
166                        initExpr = nae.init;
167                        tag = initExpr.getTag();
168                    }
169                    break;
170                } else {
171                    break;
172                }
173            }
174    
175            /* Generate null related info */
176            if (isStaticallyNonNull(initExpr)) {
177                produce(sDecl, s, GC.nary(TagConstants.REFNE, x, GC.nulllit), 
178                        proverStream);
179            } else if (initExpr.getTag() == TagConstants.NULLLIT) {
180                produce(sDecl, s, GC.nary(TagConstants.REFEQ, x, GC.nulllit),
181                        proverStream);
182            }
183    
184            /* Generate new and array related info */
185            if (tag == TagConstants.ARRAYINIT) {
186                ArrayInit aInit = (ArrayInit)initExpr;
187          
188                // typeof(x) == array(T)
189                Expr typeofx = GC.nary(TagConstants.TYPEOF, x);
190                Expr arrayT = TypeExpr.make(aInit.getStartLoc(), aInit.getEndLoc(),
191                                            TypeCheck.inst.getType(aInit));
192                produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, arrayT),
193                        proverStream);
194                            
195                // arrayLength(x) == len
196                int len = aInit.elems.size();
197                produce(sDecl, s, GC.nary(TagConstants.INTEGRALEQ,
198                                          GC.nary(TagConstants.ARRAYLENGTH, x),
199                                          LiteralExpr.make(TagConstants.INTLIT,
200                                                           new Integer(len), loc)),
201                        proverStream);
202    
203            } else if (tag == TagConstants.NEWARRAYEXPR) {
204                NewArrayExpr nae = (NewArrayExpr)initExpr;
205                Assert.notFalse(nae.dims.size() > 0);  // arrayinit is handled above
206                // typeof(x) == array(...(array(T)))
207                Expr typeofx = GC.nary(TagConstants.TYPEOF, x);
208                Expr arrayT = TypeExpr.make(nae.getStartLoc(), nae.getEndLoc(),
209                                            TypeCheck.inst.getType(nae));
210                produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, arrayT),
211                        proverStream);
212    
213                LiteralExpr constant = eval(nae.dims.elementAt(0), loc);
214                if (constant != null) {
215                    Assert.notFalse(constant.getTag() == TagConstants.INTLIT);
216                    if (0 <= ((Integer)constant.value).intValue()) {
217                        // arrayLength(x) == constant
218                        produce(sDecl, s, GC.nary(TagConstants.INTEGRALEQ,
219                                                  GC.nary(TagConstants.ARRAYLENGTH, x),
220                                                  constant),
221                                proverStream);
222                    }
223                }
224    
225            } else if (tag == TagConstants.NEWINSTANCEEXPR) {
226                NewInstanceExpr ni = (NewInstanceExpr)initExpr;
227                // typeof(x) == T
228                Expr typeofx = GC.nary(TagConstants.TYPEOF, x);
229                Expr T = TypeExpr.make(ni.getStartLoc(), ni.getEndLoc(), ni.type);
230                produce(sDecl, s, GC.nary(TagConstants.TYPEEQ, typeofx, T),
231                        proverStream);
232            }
233        }
234    
235        //@ requires sDecl != null ==> s != null;
236        private static void produce(GenericVarDecl sDecl, Expr s,
237                                    /*@ non_null */ Expr e,
238                                    /*@ non_null */ PrintStream proverStream) {
239            if (sDecl != null) {
240                Expr ant = GC.nary(TagConstants.REFNE, s, GC.nulllit);
241                ExprVec nopats = ExprVec.make(1);
242                nopats.addElement(ant);
243                e = GC.forall(sDecl, GC.implies(ant, e), nopats);
244            }
245            proverStream.print("\n");
246            VcToString.computeTypeSpecific(e, proverStream);
247        }
248      
249        /**
250         * Add to b the contribution from a particular TypeDecl, which is
251         * a formula.
252         */
253    
254        static protected void addContribution(/*@ non_null */ TypeDecl d,
255                                    /*@ non_null */ PrintStream proverStream) {
256    
257            TypeSig sig = TypeCheck.inst.getSig(d);
258    
259            // === ESCJ 8: Section 1.1
260    
261            if( d instanceof ClassDecl ) {
262                ClassDecl cd = (ClassDecl)d;
263    
264                if( cd.superClass != null ) {
265                    saySubClass( sig, cd.superClass, proverStream );
266                }
267    
268                if( Modifiers.isFinal(cd.modifiers) )
269                    sayIsFinal( sig, proverStream );
270    
271            } else {
272                saySubType( sig, Types.javaLangObject(), proverStream );
273            }
274                                          
275            for( int i=0; i<d.superInterfaces.size(); i++ )
276                saySubType( sig, d.superInterfaces.elementAt(i), proverStream );
277    
278            saySuper(d, proverStream);
279        }
280    
281    
282        /** Record in the background predicate that x is a subclass of y. */
283    
284        private static void saySubClass( Type x, Type y,
285                                         /*@ non_null */ PrintStream proverStream ) {
286    
287            saySubType( x, y, proverStream );
288            bg("(EQ "+simplifyTypeName(x)+
289               " (asChild "+simplifyTypeName(x)+" "+simplifyTypeName(y)+"))",
290               proverStream);
291        }
292    
293        /** Record in the background predicate that x is a subtype of y. */
294    
295        private static void saySubType( Type x, Type y,
296                                        /*@ non_null */ PrintStream proverStream ) {
297    
298            bg( "(<: "+simplifyTypeName(x)+" "+simplifyTypeName(y)+")" , proverStream);
299    
300        }
301    
302        private static void saySuper(TypeDecl d, /*@ non_null*/ PrintStream proverStream) {
303            TypeSig sig = TypeCheck.inst.getSig(d);
304            String n = simplifyTypeName(sig);
305            StringBuffer b = new StringBuffer();
306            b.append( "(FORALL (t) (PATS (<: "+n+" t)) " +
307                       "(IFF (<: "+n+" t) (OR (EQ t "+n+") ");
308            if( d instanceof ClassDecl ) {
309                ClassDecl cd = (ClassDecl)d;
310    
311                if( cd.superClass != null ) {
312                    String sp = simplifyTypeName(cd.superClass);
313                    b.append("(<: "+sp+" t) ");
314                }
315            } else {
316                b.append( "(EQ t |T_java.lang.Object|) ");
317            }
318            for( int i=0; i<d.superInterfaces.size(); i++ ) {
319                String tt = simplifyTypeName(d.superInterfaces.elementAt(i));
320                b.append( "(<: " +tt+" t) ");
321            }
322            b.append(" )))");
323    
324            bg(b.toString(),proverStream);
325    
326        }
327    
328        /** Record in the background predicate that x is final. */
329    
330        private static void sayIsFinal( Type x,
331                                        /*@ non_null */ PrintStream proverStream ) {
332            String n = simplifyTypeName(x);
333            bg( "(FORALL (t) (PATS (<: t "+n+")) (IFF (<: t "+n+") (EQ t "+n+")))",
334                proverStream);
335        }
336    
337        public static String simplifyTypeName(/*@ non_null */ Type x) {
338            if (x instanceof ArrayType) {
339                ArrayType at = (ArrayType)x;
340                return "(|_array| " + simplifyTypeName(at.elemType) + ")";
341            } else {
342                return Atom.printableVersion(UniqName.type(x));
343            }
344        }
345    
346        /**
347         * Called with an S-expression that may contain a free variable
348         * "t".  Wraps "(FORALL (s) (IMPLIES (NEQ s null) " and "))"
349         * around this expression and adds it to the background predicate.
350         */
351    
352        protected static void bgi(/*@ non_null */ String s,
353                                /*@ non_null */ PrintStream proverStream) {
354            proverStream.print("\n(FORALL (s) (IMPLIES (NEQ s null) ");
355            proverStream.print(s);
356            proverStream.print("))");
357        }
358    
359        /**
360         * Called with a simplify command. Adds it to the background
361         * predicate. 
362         */
363    
364        protected static void bg(/*@ non_null */ String s,
365                               /*@ non_null */ PrintStream proverStream) {
366            proverStream.print('\n');
367            proverStream.print(s);
368        }
369    
370    
371        // ======================================================================
372    
373        /**
374         * Do we know statically that an expression always returns a
375         * non-null value?
376         */
377        protected static boolean isStaticallyNonNull(VarInit e) {
378            int tag = e.getTag();
379    
380            // New expressions are always non-null:
381            if (tag==TagConstants.NEWARRAYEXPR ||
382                tag==TagConstants.NEWINSTANCEEXPR)
383                return true;
384    
385            // Array initializers are always non-null:
386            if (tag==TagConstants.ARRAYINIT)
387                return true;
388    
389            // String constants can be non-null:
390            if (tag==TagConstants.STRINGLIT) {
391                LiteralExpr asLit = (LiteralExpr)e;
392                if (asLit.value != null)
393                    return true;
394            }
395    
396            if (tag == TagConstants.ADD || tag == TagConstants.ASGADD) {
397                BinaryExpr be = (BinaryExpr)e;
398                Type leftType = TypeCheck.inst.getType( be.left );
399                Type rightType = TypeCheck.inst.getType( be.right );
400                if (Types.isReferenceOrNullType(leftType) ||
401                    Types.isReferenceOrNullType(rightType)) {
402                    // The "+" or "+=" operator is String catenation, which always
403                    // returns a non-null value.
404                    return true;
405                }
406            }
407    
408            return false;
409        }
410    
411    
412        /**
413         * Like ConstantExpr.eval, but returns a LiteralExpr instead of an
414         * Integer/Long/etc.
415         *
416         * <p> Ignores String constants.  (Always returns null in that case.)
417         *
418         * <p> If returns a non-null LiteralExpr, sets its loc to
419         * <code>loc</code>.
420         */
421        //@ requires e!=null && loc!=Location.NULL;
422        protected static LiteralExpr eval(Expr e, int loc) {
423            Object val = ConstantExpr.eval(e);
424    
425            if (val instanceof Boolean)
426                return LiteralExpr.make(TagConstants.BOOLEANLIT, val, loc);
427    
428            // char, byte, short, int cases:
429            if (val instanceof Integer)
430                return LiteralExpr.make(TagConstants.INTLIT, val, loc);
431    
432            if (val instanceof Long)
433                return LiteralExpr.make(TagConstants.LONGLIT, val, loc);
434    
435            if (val instanceof Float)
436                return LiteralExpr.make(TagConstants.FLOATLIT, val, loc);
437            if (val instanceof Double)
438                return LiteralExpr.make(TagConstants.DOUBLELIT, val, loc);
439    
440            // Ignore String because don't have the right location
441    
442            return null;
443        }
444    
445    
446        /**
447         * Generate the appropriate GC equality e1 == e2 based on type t.
448         */
449        //@ requires e1 != null && e2!=null && t!=null;
450        //@ ensures \result != null;
451        protected static Expr eq(Expr e1, Expr e2, Type t) {
452            if (!(t instanceof PrimitiveType))
453                return GC.nary(TagConstants.REFEQ, e1, e2);
454    
455            switch (t.getTag()) {
456                case TagConstants.NULLTYPE:
457                    return GC.nary(TagConstants.REFEQ, e1, e2);
458    
459                case TagConstants.BOOLEANTYPE:
460                    return GC.nary(TagConstants.BOOLEQ, e1, e2);
461    
462                case TagConstants.CHARTYPE:
463                case TagConstants.BYTETYPE:
464                case TagConstants.SHORTTYPE:
465                case TagConstants.INTTYPE:
466                case TagConstants.LONGTYPE:
467                    return GC.nary(TagConstants.INTEGRALEQ, e1, e2);
468    
469                case TagConstants.FLOATTYPE:
470                case TagConstants.DOUBLETYPE:
471                    return GC.nary(TagConstants.FLOATINGEQ, e1, e2);
472    
473                case TagConstants.TYPECODE:
474                    return GC.nary(TagConstants.TYPEEQ, e1, e2);
475    
476                default:
477                    Assert.fail("Bad primitive type passed to BackPred.eq:"
478                                + TagConstants.toString(t.getTag()));
479                    return null;    // keep compiler happy...
480            }
481        }
482    }