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 }