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 }