    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
    016    import escjava.*;
    017    import escjava.ast.*;
    018    import escjava.ast.TagConstants;
    019    import escjava.translate.*;
    020    import escjava.sp.SPVC;
    021    import escjava.sp.*;
    022    import escjava.pa.generic.*;
    023    import escjava.prover.*;
    024
    025    import mocha.wrappers.jbdd.*;
    026
    027    public class GCProver implements Prover
    028    {
    029        private jbddManager bddManager;
    030        private ExprVec loopPredicates;
    031
    032        private boolean noisy = Boolean.getBoolean("PANOISY");
    033
    034        public jbdd valid;
    035        public Vector validClauses = new Vector();
    036        private Vector allInvalidClauses = new Vector();
    037        private jbdd oldValid;
    038
    039        private PrintStream ps = ProverManager.prover().subProcessToStream();
    040        private VarMap subst;
    041        int queriesConsidered=0, queriesTried=0, queriesValid=0;
    042        long milliSecsUsed;
    043
    044        public GCProver(jbddManager bddManager,
    045                        ExprVec loopPredicates,
    046                        GuardedCmd g,
    047                        GCProver oldProver) {
    048            GCSanity.check(g);
    049
    050            this.bddManager = bddManager;
    051            this.loopPredicates = loopPredicates;
    052            valid = bddManager.jbdd_one();
    053
    054            oldValid =  oldProver == null ? bddManager.jbdd_zero() : oldProver.valid;
    055
    056            VarMapPair out = new VarMapPair();
    057            GuardedCmd gc = DSA.dsa(g,out);
    058            Expr vc = SPVC.computeN(gc);
    059            subst = out.n;
    060            ProverManager.push(vc);
    061    /*
    062            ps.print("\n(BG_PUSH ");
    063            VcToString.computePC(vc, ps);
    064            ps.println(")");
    065            Main.prover.sendCommands("");
    066    */
    067
    068        }
    069
    070        public boolean check(jbdd query) {
    071
    072            if( noisy ) say("query = "+printClause( query ));
    073
    074            queriesConsidered++;
    075
    076            switch( quickCheck( query )) {
    077              case VALID:
    078                return true;
    079
    080              case INVALID:
    081                return false;
    082
    083              case UNKNOWN:
    084                // query is possible invariant, call simplify
    085                milliSecsUsed -= java.lang.System.currentTimeMillis();
    086                ProverManager.prover().startProve();
    087                VcToString.compute( subst.apply(concretize( query )),
    088                                    ps);
    089                Enumeration results = ProverManager.prover().streamProve();
    090                boolean queryvalid = processSimplifyOutput(results);
    091                if( noisy ) say( "SIMPLIFY: "+(queryvalid ? "valid" : "invalid"));
    092                queriesTried++;
    093                milliSecsUsed += java.lang.System.currentTimeMillis();
    094
    095                if( queryvalid ) {
    096                    queriesValid++;
    097
    098                    validClauses.add( query );
    099                    jbdd t = jbdd.jbdd_and( valid, query, true, true );
    100                    // valid.jbdd_free();
    101                    valid = t;
    102                    return true;
    103                } else {
    104                    // query not tautology or contradictory
    105                    // maybe some extension is an invariant
    106                    allInvalidClauses.add( query );
    107                    return false;
    108                }
    109
    110              default:
    111                Assert.fail("");
    112                return false;
    113            }
    114        }
    115
    116        public int quickCheck(jbdd query) {
    117
    118            // check if query not implied by oldValid
    119            if( !oldValid.jbdd_leq( query, true, true ) ) {
    120                say("not implied by oldValid");
    121                return INVALID;
    122            };
    123
    124            // check if query redundant
    125            if( valid.jbdd_leq( query, true, true ) ) {
    126                say("redundant");
    127                return VALID;
    128            }
    129
    130            // check if query contradictory
    131            if( valid.jbdd_leq( query, true, false ) ) {
    132                say("contradictory");
    133                return INVALID;
    134            };
    135
    136            // Chk if query an extension of something in validClauses
    137
    138            boolean queryMaybeValid = true;
    139
    140            // query is possible invariant,
    141            // see if there exists d in allInvalidClauses such that
    142            // valid => (query => d)
    143            // if so, query is not valid
    144            // Optimized check is (valid /\ query) => d
    145
    146            jbdd validAndQuery = jbdd.jbdd_and(valid, query, true, true);
    147
    148            for(Enumeration e2 = allInvalidClauses.elements();
    149                e2.hasMoreElements() && queryMaybeValid; ) {
    150                jbdd clause = (jbdd)e2.nextElement();
    151                if( validAndQuery.jbdd_leq( clause, true, true ) ) {
    152                    // query not a tautology
    153                    say("invalid by earlier test");
    154                    return INVALID;
    155                }
    156            }
    157
    158            // validAndQuery.jbdd_free();
    159
    160            return UNKNOWN;
    161        }
    162
    163        public String report() {
    164            return("Considered "+ queriesConsidered
    165                   +" tried "+queriesTried
    166                   +" valid "+queriesValid +
    167                   " simplify-time "+milliSecsUsed+"ms");
    168        }
    169
    170        public void addPerfCounters(GCProver p) {
    171            queriesConsidered += p.queriesConsidered;
    172            queriesTried += p.queriesTried;
    173            queriesValid += p.queriesValid;
    174            milliSecsUsed += p.milliSecsUsed;
    175        }
    176
    177        public void done() {
    178            ProverManager.pop();
    179        }
    180
    181        public String printClause(jbdd b) {
    182            if (b.jbdd_is_tautology(true)) {
    183                return "TRUE";
    184            }
    185            else if (b.jbdd_is_tautology(false)) {
    186                return "";
    187            }
    188            else {
    189                int n = b.jbdd_top_var_id();
    190                if( b.jbdd_then().jbdd_is_tautology(true)) {
    191                    // n is positive
    192                    return "p"+n+"-1 "+ printClause( b.jbdd_else());
    193                } else {
    194                    // n is negative
    195                    return "p"+n+"-0 "+ printClause( b.jbdd_then());
    196                }
    197            }
    198        }
    199
    200        private void say(String s) {
    201            if( noisy ) {
    202                System.out.println(s);
    203            }
    204        }
    205
    206        boolean processSimplifyOutput(Enumeration results) {
    207            boolean valid = false;
    208            while (results.hasMoreElements()) {
    209                SimplifyOutput so = (SimplifyOutput)results.nextElement();
    210                switch (so.getKind()) {
    211                case SimplifyOutput.VALID: {
    212                    valid = true;
    213                    Assert.notFalse(!results.hasMoreElements());
    214                    break;
    215                }
    216
    217                case SimplifyOutput.INVALID:
    218                case SimplifyOutput.UNKNOWN:
    219                case SimplifyOutput.COMMENT:
    220                case SimplifyOutput.COUNTEREXAMPLE:
    221                case SimplifyOutput.EXCEEDED_PROVER_KILL_TIME:
    222                case SimplifyOutput.EXCEEDED_PROVER_KILL_ITER:
    223                case SimplifyOutput.REACHED_CC_LIMIT:
    224                case SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_TIME:
    225                case SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_ITER:
    226                case SimplifyOutput.WARNING_TRIGGERLESS_QUANT:
    227                    break;
    228
    229                default:
    230                  Assert.fail("unexpected type of Simplify output");
    231                  break;
    232                }
    233            }
    234            return valid;
    235        }
    236
    237        ExprVec concretize(Vector clauses) {
    238            ExprVec r = ExprVec.make( clauses.size() );
    239            for(int i=0; i<clauses.size(); i++) {
    240                r.addElement( concretize( (jbdd)clauses.elementAt(i) ));
    241            }
    242            return r;
    243        }
    244
    245        Expr concretize(jbdd b) {
    246            if (b.jbdd_is_tautology(true)) {
    247                return GC.truelit;
    248            }
    249            else if (b.jbdd_is_tautology(false)) {
    250                return GC.falselit;
    251            }
    252            else {
    253                Expr e = loopPredicates.elementAt(b.jbdd_top_var_id());
    254                jbdd thn = b.jbdd_then();
    255                jbdd els = b.jbdd_else();
    256
    257                if( thn.jbdd_is_tautology(true)) {
    258                    return GC.or( e, concretize( els ));
    259                } else if( els.jbdd_is_tautology(true)) {
    260                    return GC.or( GC.not(e), concretize( thn ));
    261                } else {
    262                    return GC.or( GC.and(e, concretize( thn )),
    263                                  GC.and(GC.not(e), concretize( els )));
    264                }
    265            }
    266        }
    267
    268        public int size(jbdd b) {
    269            return size(b, bddManager.jbdd_num_vars());
    270        }
    271
    272        public int size(jbdd b, int nbitsFree) {
    273            if( b.jbdd_is_tautology(false) ) {
    274                return 0;
    275            }
    276            if( b.jbdd_is_tautology(true) ) {
    277                int r=1;
    278                while( nbitsFree-- >0 ) r = 2*r;
    279                return r;
    280            }
    281            return size( b.jbdd_then(), nbitsFree-1 )
    282                +  size( b.jbdd_else(), nbitsFree-1 );
    283        }
    284    }