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 }