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 }