    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.pa;
    004
    005    import java.util.Hashtable;
    006    import java.util.Enumeration;
    007    import java.util.Vector;
    008    import java.io.*;
    009
    010    import javafe.ast.*;
    011    import javafe.util.Set;
    012    import javafe.util.Location;
    013    import javafe.util.Assert;
    014    import javafe.util.StackVector;
    015    import javafe.tc.Types;
    016
    017    import escjava.*;
    018    import escjava.ast.*;
    019    import escjava.ast.TagConstants;
    020    import escjava.ast.Modifiers;
    021    import escjava.translate.*;
    022    import escjava.sp.SPVC;
    023    import escjava.sp.*;
    024    import escjava.prover.*;
    025    import escjava.pa.generic.*;
    026
    027    import mocha.wrappers.jbdd.*;
    028
    029    public class PredicateAbstraction
    030    {
    031        public static /*@ non_null @*/ ASTDecoration paDecoration = new ASTDecoration("paDecoration");
    032
    033        static GuardedCmd abstractLoop(LoopCmd g, GuardedCmd context, Set env) {
    034            PredicateAbstraction pa = (PredicateAbstraction) paDecoration.get(g);
    035            if (pa == null) {
    036                pa = new PredicateAbstraction(g, env);
    037                paDecoration.set(g, pa);
    038            }
    039            return pa.abstractLoopHelper(context, env);
    040        }
    041
    042        private static boolean quantifyAssumptions =
    043            !Boolean.getBoolean("PAnoQuantifyAssumptions");
    044        ExprVec invariants = ExprVec.make();
    045        private /*@ non_null @*/ jbddManager bddManager;
    046        public  /*@ non_null @*/ Abstractor abstractor;
    047        private /*@ non_null @*/ LocalVarDeclVec skolemConstants;
    048        private /*@ non_null @*/ ExprVec loopPredicates;
    049        private GuardedCmd body;
    050        private /*@ non_null @*/ GuardedCmd bodyDesugared = GC.fail();
    051        private GuardedCmd havoc;
    052        private int startLoc;
    053        public int nQueries=0;
    054        long milliSecsUsed;
    055        GCProver perfCount;
    056
    057        private final /*@ non_null @*/ StackVector code = new StackVector();
    058        private final /*@ non_null @*/ GenericVarDeclVec temporaries = GenericVarDeclVec.make();
    059
    060        PredicateAbstraction(/*@ non_null @*/ LoopCmd g, Set env) {
    061
    062            body = GC.seq(g.guard, g.body);
    063            startLoc = g.getStartLoc();
    064
    065            Set vds = Targets.normal(body);
    066
    067            if( Main.options().inferPredicates ) {
    068                //System.out.println("Before inf: "+g.predicates);
    069                inferPredicates(g, env, vds);
    070                //System.out.println("After inf: "+g.predicates);
    071            }
    072
    073            this.skolemConstants = g.skolemConstants;
    074            this.loopPredicates = g.predicates;
    075            this.bddManager = new jbddManager( loopPredicates.size() );
    076
    077            if( System.getProperty("PABDT") != null ) {
    078                this.abstractor = new BinaryDecisionTreeAbstractor(bddManager);
    079            } else if( System.getProperty("PA3n") != null ) {
    080                this.abstractor = new EnumClausesAbstractor(bddManager);
    081            } else if( System.getProperty("PANK") != null ) {
    082                this.abstractor = new EnumNFindK(bddManager,
    083                                                 Integer.parseInt(System.getProperty("PANK")));
    084            } else {
    085                this.abstractor = new EnumMaxClausesFindMinAbstractor(bddManager);
    086            }
    087
    088            code.push();
    089
    090            Translate translate = (new Translate());
    091            GuardedCmd modifyGc = translate.modify(vds, g.locStart);
    092
    093            if( Main.options().preciseTargets ) {
    094                Set aTargets = ATarget.compute( VarInCmd.make(g.tempVars, g ));
    095                modifyGc = translate.modifyATargets( aTargets, g.getStartLoc());
    096            }
    097
    098            code.addElement(modifyGc);
    099
    100            for (Enumeration e = vds.elements(); e.hasMoreElements();) {
    101                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
    102
    103                if (!vd.id.toString().endsWith("@init")) {
    104                    code.addElement(GC.assume(TrAnExpr.targetTypeCorrect(vd, g.oldmap)));
    105                }
    106            }
    107
    108            for (int i = 0; i < g.invariants.size(); i++) {
    109                Condition cond = g.invariants.elementAt(i);
    110                code.addElement(GC.assume(cond.pred));
    111            }
    112
    113            havoc = GC.seq(GuardedCmdVec.popFromStackVector(code));
    114        }
    115
    116        private GuardedCmd abstractLoopHelper(GuardedCmd context, Set env) {
    117            int step = 0;
    118            milliSecsUsed -= java.lang.System.currentTimeMillis();
    119
    120            code.push();
    121            for(int j=0; j<skolemConstants.size();j++) {
    122                LocalVarDecl sc = skolemConstants.elementAt(j);
    123                code.addElement(GC.assume(TrAnExpr.typeAndNonNullCorrectAs(sc, sc.type, null, true, null)));
    124            }
    125            context = GC.seq( context,
    126                              GC.seq( GuardedCmdVec.popFromStackVector(code)));
    127
    128
    129            System.out.println("Step " + step + ": Computing for loop at "
    130                               +Location.toString( startLoc )
    131                               +" num preds = "+loopPredicates.size()
    132                               + "....");
    133
    134            perfCount = new GCProver(bddManager, loopPredicates, GC.skip(), null);
    135
    136            GCProver p = new GCProver(bddManager, loopPredicates, context, null);
    137            boolean atfixpoint = abstractor.union(p);
    138            p.done();
    139            perfCount.addPerfCounters(p);
    140
    141            System.out.println("  reachable size: "+p.size(abstractor.get()));
    142
    143            while (!atfixpoint) {
    144                ExprVec invs = p.concretize(abstractor.getClauses());
    145
    146                if( quantifyAssumptions ) {
    147                    invs = skolemQuantInvariants(skolemConstants, invs,
    148                                                 Location.NULL, Location.NULL);
    149                }
    150
    151                System.out.println("Step " + ++step + ": Computing....");
    152                GuardedCmd c = GC.seq( context, havoc,
    153                                       GC.assume(GC.and(invs)));
    154                // from shaz
    155                // c = GC.seq( context, havoc, GC.assume(e) );
    156                milliSecsUsed += java.lang.System.currentTimeMillis();
    157                bodyDesugared = Traverse.computeHelper(body, c, env);
    158                milliSecsUsed -= java.lang.System.currentTimeMillis();
    159
    160                if( Main.options().pgc ) {
    161                    System.out.println("\n**** Guarded Command c:");
    162                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, c);
    163                    System.out.println("");
    164                    System.out.println("\n**** Guarded Command body:");
    165                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, body);
    166                    System.out.println("");
    167                    System.out.println("\n**** Guarded Command bodyDesugared:");
    168                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, bodyDesugared);
    169                    System.out.println("");
    170                }
    171                p = new GCProver(bddManager, loopPredicates, GC.seq(c, bodyDesugared), p);
    172                atfixpoint = abstractor.union(p);
    173                p.done();
    174                perfCount.addPerfCounters(p);
    175
    176                System.out.println("  reachable size: "+p.size(abstractor.get()));
    177            }
    178
    179            invariants = skolemQuantInvariants(skolemConstants,
    180                                               p.concretize(abstractor.getClauses()),
    181                                               Location.NULL,
    182                                               Location.NULL);
    183
    184            milliSecsUsed += java.lang.System.currentTimeMillis();
    185            System.out.println("Finished loop at "
    186                               +Location.toString( startLoc ) );
    187            return VarInCmd.make(temporaries,
    188                                 GC.seq(havoc,
    189                                        GC.assume(GC.and(invariants)),
    190                                        bodyDesugared,
    191                                        GC.fail()));
    192        }
    193
    194        public static ExprVec skolemQuantInvariants(LocalVarDeclVec skolemConstants,
    195                                                    ExprVec invs,
    196                                                    int sloc, int eloc) {
    197
    198            // Now, assume the inferred invariants at the beginning of the loop,
    199            // universally quantified by the skolem constants
    200
    201            ExprVec r = ExprVec.make();
    202
    203            for(int i=0; i<invs.size(); i++) {
    204                Expr inv = invs.elementAt(i);
    205
    206                GenericVarDeclVec decls = GenericVarDeclVec.make();
    207                ExprVec ttc = ExprVec.make();
    208                for(int j=0; j<skolemConstants.size();j++) {
    209                    LocalVarDecl sc = skolemConstants.elementAt(j);
    210                    if( mentions( inv, sc ) ) {
    211                        decls.addElement(sc);
    212                        ttc.addElement( TrAnExpr.typeAndNonNullCorrectAs(sc, sc.type, null, true, null) );
    213                    }
    214                }
    215
    216                Expr f = GC.quantifiedExpr( sloc, eloc,
    217                                            TagConstants.FORALL,
    218                                            decls,
    219                                            GC.truelit,
    220                                            GC.implies( GC.and( ttc ),
    221                                                        inv ),
    222                                                null, null );
    223                r.addElement( f );
    224            }
    225
    226            return r;
    227        }
    228
    229        private static boolean mentions(/*@ non_null @*/ Expr e, GenericVarDecl d) {
    230            if( e instanceof VariableAccess ) {
    231                return ((VariableAccess)e).decl == d;
    232            } else {
    233                for(int i=0; i<e.childCount(); i++) {
    234                    Object c = e.childAt(i);
    235                    if( c instanceof Expr && mentions((Expr)c,d) ) {
    236                        return true;
    237                    }
    238                }
    239                return false;
    240            }
    241        }
    242
    243    /* Unused.
    244        private void inferPredicatesOld(LoopCmd g, Set env, Set targets) {
    245            Set t = new Set(targets.elements());
    246            t.intersect(env);
    247
    248            for (Enumeration e = t.elements(); e.hasMoreElements();) {
    249                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
    250                if( vd.type != null ) {
    251                    if( escjava.tc.Types.isIntegralType( vd.type ) ) {
    252                        // guess vd >= 0
    253                        ExprVec vec = ExprVec.make();
    254                        int loc = g.getStartLoc();
    255                        vec.addElement( VariableAccess.make(vd.id, loc, vd) );
    256                        vec.addElement( LiteralExpr.make( TagConstants.INTLIT,
    257                                                                       new Integer(0),
    258                                                                       loc ));
    259
    260                        Expr pred = NaryExpr.make( loc, loc, TagConstants.INTEGRALGE, null, vec );
    261                        g.predicates.addElement( pred );
    262                    }
    263
    264                    if ( escjava.tc.Types.isReferenceType( vd.type ) ) {
    265                        // guess vd != null
    266                        ExprVec vec = ExprVec.make();
    267                        int loc = g.getStartLoc();
    268                        vec.addElement( VariableAccess.make(vd.id, loc, vd) );
    269                        vec.addElement( LiteralExpr.make( TagConstants.NULLLIT,
    270                                                                       null,
    271                                                                       loc ));
    272
    273                        Expr pred = NaryExpr.make( loc, loc, TagConstants.REFNE, null, vec );
    274                        g.predicates.addElement( pred );
    275                    }
    276                }
    277            }
    278        }
    279    */
    280
    281        private void inferPredicates(/*@ non_null @*/ LoopCmd g,
    282                                     /*@ non_null @*/ Set env,
    283                                     Set targets)
    284        {
    285            int loc = g.getStartLoc();
    286
    287            LocalVarDecl sc = LocalVarDecl.make(Modifiers.NONE, null, Identifier.intern("sc"),
    288                                                Types.intType, loc, null, loc);
    289
    290            boolean useSC = false;
    291            ExprVec boundsSC = ExprVec.make();
    292            VariableAccess sca = VariableAccess.make(sc.id, loc, sc);
    293
    294            //System.out.println("Getting targets for : "+g);
    295            Set t = ATarget.compute(g);
    296            //System.out.println("Targets: "+t);
    297
    298
    299            // predicates based on environment
    300          outerLoop:
    301            for (Enumeration e = env.elements(); e.hasMoreElements();) {
    302                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
    303                if( vd.id.toString().indexOf('@') != -1 ) {
    304                    // not a user var
    305                    continue;
    306                }
    307                for (Enumeration e2 = t.elements(); e2.hasMoreElements();) {
    308                    ATarget at = (ATarget)e2.nextElement();
    309                    if( at.x == vd ) {
    310                        // a target; will deal with below
    311                        continue outerLoop;
    312                    }
    313                }
    314                if( vd.type != null ) {
    315                    if( escjava.tc.Types.isIntegralType( vd.type ) ) {
    316                        // guess sc < vd
    317                        boundsSC.addElement( GC.nary( loc, loc, TagConstants.INTEGRALLT,
    318                                                      sca,
    319                                                      VariableAccess.make(vd.id, loc, vd)));
    320                    }
    321                }
    322            }
    323
    324            for (Enumeration e = t.elements(); e.hasMoreElements();) {
    325                ATarget at = (ATarget)e.nextElement();
    326                VariableAccess va = VariableAccess.make( at.x.id, Location.NULL, at.x );
    327                Expr vaOld = (Expr)g.oldmap.get(at.x);
    328
    329                switch( at.indices.length ) {
    330                  case 0:
    331                    {
    332                        if( at.x.type != null ) {
    333                            guessPredicate( va, vaOld, at.x.type, g.predicates, loc, sca, boundsSC);
    334                        }
    335                    }
    336                    break;
    337
    338                  case 1:
    339                    {
    340                        if( at.x instanceof FieldDecl && at.x.type != null && at.indices[0] != null ) {
    341                            guessPredicate( GC.select( va, at.indices[0]),
    342                                            GC.select( vaOld, at.indices[0]),
    343                                            at.x.type, g.predicates, loc, sca, boundsSC);
    344                        }
    345                    }
    346                    break;
    347
    348                  case 2:
    349                    { // elems[..][..]
    350                        if( at.indices[0] != null ) {
    351                            Type type = null;
    352                            switch( at.indices[0].getTag() ) {
    353                                case TagConstants.VARIABLEACCESS:
    354                                    {
    355                                        GenericVarDecl vd = ((VariableAccess)at.indices[0]).decl;
    356                                        if( vd.type != null ) {
    357                                            Assert.notFalse( vd.type instanceof ArrayType );
    358                                            type = ((ArrayType)vd.type).elemType;
    359                                        }
    360                                    }
    361                                    break;
    362
    363                              case TagConstants.SELECT:
    364                                  {
    365                                      NaryExpr ne = (NaryExpr)at.indices[0];
    366                                      Expr arg0 = ne.exprs.elementAt(0);
    367                                      if( arg0 instanceof VariableAccess ) {
    368                                          GenericVarDecl vd = ((VariableAccess)arg0).decl;
    369                                          if( vd.type != null ) {
    370                                              Assert.notFalse( vd.type instanceof ArrayType );
    371                                              type = ((ArrayType)vd.type).elemType;
    372                                          }
    373                                      }
    374                                  }
    375                                  break;
    376                            }
    377
    378                            if( type != null ) {
    379                                Expr index;
    380                                if(at.indices[1] == null ) {
    381                                    index = sca;
    382                                    useSC = true;
    383                                } else {
    384                                    index = at.indices[1];
    385                                }
    386                                guessPredicate( GC.select( GC.select( va, at.indices[0]), index),
    387                                                null,
    388                                                type, g.predicates, loc, sca, boundsSC);
    389                            }
    390                        }
    391                    }
    392                    break;
    393                }
    394            }
    395
    396            if( useSC ) {
    397                    g.skolemConstants.addElement(sc);
    398                    // guess sc >= 0
    399                    g.predicates.addElement( GC.nary( loc, loc, TagConstants.INTEGRALGE, sca,
    400                                                      LiteralExpr.make(TagConstants.INTLIT, new Integer(0),
    401                                                                       loc) ) );
    402                    g.predicates.append(boundsSC);
    403            }
    404        }
    405
    406        private void guessPredicate( Expr e, Expr eOld, Type type,
    407                                     ExprVec predicates, int loc,
    408                                     Expr sca, ExprVec boundsSC ) {
    409
    410            if( type != null ) {
    411                Expr pred;
    412
    413                if( Types.isIntegralType( type ) ) {
    414                    if( eOld != null) {
    415                        // guess e >= eOld and e <= eOld
    416
    417                        pred = GC.nary( loc, loc, TagConstants.INTEGRALGE, e, eOld );
    418                        predicates.addElement( pred );
    419                        pred = GC.nary( loc, loc, TagConstants.INTEGRALLE, e, eOld );
    420                        predicates.addElement( pred );
    421                    } else {
    422                        // guess e >= 0
    423                        pred = GC.nary( loc, loc, TagConstants.INTEGRALGE, e,
    424                                        LiteralExpr.make( TagConstants.INTLIT,
    425                                                                       new Integer(0),
    426                                                                       loc ));
    427                        predicates.addElement( pred );
    428                    }
    429                    // guess sc < e
    430                    pred = GC.nary( loc, loc, TagConstants.INTEGRALLT, sca, e );
    431                    boundsSC.addElement( pred );
    432                }
    433
    434                if ( Types.isReferenceType( type ) ) {
    435                    // guess e != null
    436                    pred = GC.nary( loc, loc, TagConstants.REFNE, e,
    437                                    LiteralExpr.make( TagConstants.NULLLIT,
    438                                                      null, loc ) );
    439                    predicates.addElement( pred );
    440                }
    441            }
    442        }
    443
    444        /*
    445        private void computeMentionsSet(ASTNode n, Set s) {
    446            if( n instanceof VariableAccess ) {
    447                VariableAccess va = (VariableAccess)n;
    448                if( n.decl != null ) {
    449                    s.add(n.decl);
    450                }
    451            }
    452            for(int i=0; i<n.childCount(); i++) {
    453                Object c = n.childAt(i);
    454                computeMentionsSet(c,s);
    455            }
    456        }
    457        */
    458    }