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    }