    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    }