4 public class ConcreteInterferes {
5 Termination termination;
7 public ConcreteInterferes(Termination t) {
11 /** Returns true if the data structure updates performed by mun
12 * may increase (or decrease if satisfy=false) the scope of the
13 * model definition rule r. */
15 public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
17 // A rule that adds something to a set can't be falsified by
18 // an update that is only performed if the set is empty
19 if (!initialinterferes(mun,r,satisfy))
22 for(int i=0;i<mun.numUpdates();i++) {
23 UpdateNode un=mun.getUpdate(i);
24 for (int j=0;j<un.numUpdates();j++) {
25 Updates update=un.getUpdate(j);
26 //Abstract updates don't have concrete interference1
27 if (update.isAbstract())
30 DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
31 Descriptor updated_des=update.getDescriptor();
32 assert updated_des!=null;
34 /* Test to see if the update only effects new
35 objects and we're only testing for falsifying
36 model definition rules. */
38 if ((!satisfy)&&updateonlytonewobject(mun,un,update))
42 // See if the update interferes with the inclusion
43 // condition for the rule
44 if (r.getInclusion().usesDescriptor(updated_des)) {
47 /* If the update is for this rule, and the effect
48 is the intended effect, and the update only
49 effects one binding, then the abstract repair
50 node already models the action of this
53 if ((un.getRule()==r)&&
54 (((mun.op==MultUpdateNode.ADD)&&satisfy)
55 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
56 ||(mun.op==MultUpdateNode.MODIFY))) {
57 Inclusion inclusion=r.getInclusion();
58 if (inclusion instanceof RelationInclusion) {
59 RelationInclusion ri=(RelationInclusion)inclusion;
60 if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
61 (!testdisjoint(update,r,ri.getRightExpr())))
63 } else if (inclusion instanceof SetInclusion) {
64 SetInclusion si=(SetInclusion)inclusion;
65 if (!testdisjoint(update,r,si.getExpr()))
67 } else throw new Error();
70 if ((un.getRule()==r)&&
71 ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
72 modifiesremoves(mun,un,r)) {
73 Inclusion inclusion=r.getInclusion();
74 if (inclusion instanceof RelationInclusion) {
75 RelationInclusion ri=(RelationInclusion)inclusion;
76 if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
77 (!testdisjoint(update,r,ri.getRightExpr())))
78 ok=true; /* Update is specific to
79 given binding of the rule,
80 and adds are only performed
81 if the removal is desired or
82 the tuple doesn't exist.*/
88 /** Check to see if the update definitely falsifies r, thus
89 * can't accidentally satisfy it r. */
90 if (interferesinclusion(un, update, r))
93 return true; /* Interferes with inclusion condition */
97 for(int k=0;k<drule.size();k++) {
98 RuleConjunction rconj=drule.get(k);
99 for(int l=0;l<rconj.size();l++) {
100 DNFExpr dexpr=rconj.get(l);
101 /* See if update interferes w/ dexpr */
102 if ((un.getRule()==r)&&
103 (((mun.op==MultUpdateNode.ADD)&&satisfy)
104 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
105 ||(mun.op==MultUpdateNode.MODIFY))) {
106 if (!testdisjoint(update,r,dexpr.getExpr()))
107 continue; /* Update is specific to
109 rule, and effect is the
110 intended one, so we're
113 if ((un.getRule()==r)&&
114 ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
115 modifiesremoves(mun,un,r)) {
116 if (!testdisjoint(update,r,dexpr.getExpr()))
117 continue; /* Update is specific to
119 rule, and adds are only
120 performed if the removal
121 is desired or the tuple
125 if (interferes(update,dexpr))
135 static private boolean modifiesremoves(MultUpdateNode mun,UpdateNode un, Rule r) {
136 AbstractRepair ar=mun.getRepair();
137 boolean inverted=ar.getPredicate().getPredicate().inverted();
139 if (ar.getType()!=AbstractRepair.MODIFYRELATION)
141 RelationInclusion ri=(RelationInclusion)r.getInclusion();
142 Expr e=inverted?ri.getRightExpr():ri.getLeftExpr();
143 while(e instanceof CastExpr) {
144 e=((CastExpr)e).getExpr();
146 if (!(e instanceof VarExpr))
148 VarExpr ve=(VarExpr)e;
154 static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
155 AbstractRepair ar=mun.getRepair();
156 if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
157 for(int i=0;i<un.numUpdates();i++) {
158 Updates u=un.getUpdate(i);
159 if (u.getType()==Updates.POSITION&&
160 ar.isNewObject(u.getRightPos()==0)) {
161 Expr newleftexpr=u.getLeftExpr();
162 Expr leftexpr=updates.getLeftExpr();
163 boolean foundfield=false;
165 if (leftexpr.equals(null,newleftexpr)) {
170 } else if (leftexpr instanceof DotExpr) {
174 if (((DotExpr)leftexpr).isPtr())
175 break; //if its not a pointer, we're still in the structure
177 leftexpr=((DotExpr)leftexpr).getExpr();
178 } else if (leftexpr instanceof CastExpr) {
179 leftexpr=((CastExpr)leftexpr).getExpr();
189 /** This method tries to show that if the Update update from the
190 * UpdateNode un changes the value of the inclusion constraint
191 * that it falsifies the guard of model definition rule. */
193 static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
194 Descriptor updated_des=update.getDescriptor();
195 Inclusion inclusion=r.getInclusion();
196 if (inclusion instanceof RelationInclusion) {
197 RelationInclusion ri=(RelationInclusion)inclusion;
198 if (ri.getLeftExpr().usesDescriptor(updated_des)
199 &&searchinterfere(un,update,r,ri.getLeftExpr()))
201 if (ri.getRightExpr().usesDescriptor(updated_des)
202 &&searchinterfere(un,update,r,ri.getRightExpr()))
204 } else if (inclusion instanceof SetInclusion) {
205 SetInclusion si=(SetInclusion)inclusion;
206 if (si.getExpr().usesDescriptor(updated_des)
207 &&searchinterfere(un,update,r,si.getExpr()))
209 } else throw new Error();
213 /** This method finds all instances of a field or global that an
214 * update may modify, and builds a variable correspondance */
216 static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
217 Descriptor updated_des=update.getDescriptor();
218 if (updated_des instanceof FieldDescriptor) {
219 /* Build variable correspondance */
220 HashSet set=new HashSet();
221 inclusionexpr.findmatch(updated_des,set);
223 for(Iterator matchit=set.iterator();matchit.hasNext();) {
224 DotExpr dotexpr=(DotExpr)matchit.next();
225 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
227 if (dotexpr.getField()!=updateexpr.getField())
229 Expr de=dotexpr.getExpr();
230 Expr ue=updateexpr.getExpr();
231 if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
233 updateexpr=(DotExpr)ue;
234 } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
235 VarDescriptor dvd=((VarExpr)de).getVar();
236 VarDescriptor uvd=((VarExpr)ue).getVar();
237 if (interferesinclusion(un,r,dvd,uvd))
245 } else if (updated_des instanceof VarDescriptor) {
246 /* We have a VarDescriptor - no correspondance necessary */
247 VarDescriptor vd=(VarDescriptor)updated_des;
248 if (interferesinclusion(un,r,vd,vd))
250 } else throw new Error();
254 /** This method tries to show that if dvd=uvd, then the update un
255 * must falsify the rule r. */
257 static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
258 DNFRule negrule=r.getDNFNegGuardExpr();
259 HashMap remap=new HashMap();
262 for(int i=0;i<negrule.size();i++) {
263 RuleConjunction rconj=negrule.get(i);
265 for(int j=0;j<rconj.size();j++) {
266 DNFExpr dexpr=rconj.get(j);
267 if (dexpr.getExpr() instanceof OpExpr) {
268 OpExpr expr=(OpExpr)dexpr.getExpr();
269 Expr lexpr=expr.getLeftExpr();
270 Expr rexpr=expr.getRightExpr();
273 Set vars=rexpr.freeVars();
275 for(Iterator it=vars.iterator();it.hasNext();) {
276 VarDescriptor vd=(VarDescriptor) it.next();
277 if (!vd.isGlobal()) {
278 /* VarDescriptor isn't a global */
289 Opcode op=expr.getOpcode();
290 op=Opcode.translateOpcode(dexpr.getNegation(),op);
293 for(int k=0;k<un.numUpdates();k++) {
294 Updates update=un.getUpdate(k);
295 if(update.isExpr()) {
296 Set uvars=update.getRightExpr().freeVars();
297 boolean freevarok=true;
299 for(Iterator it=uvars.iterator();it.hasNext();) {
300 VarDescriptor vd=(VarDescriptor) it.next();
301 if (!vd.isGlobal()) {
302 /* VarDescriptor isn't a global */
312 Opcode op2=update.getOpcode();
314 ((op2==Opcode.GT)&&(op==Opcode.GE))||
315 ((op2==Opcode.LT)&&(op==Opcode.LE))||
316 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
317 /* Operations match*/
318 if (lexpr.equals(remap,update.getLeftExpr())&&
319 rexpr.equals(remap,update.getRightExpr())) {
331 /* TODO: Check to see if there is an abstract repair */
333 break; /* try next conjunction */
342 /** This method checks whether the update effects only the
343 * intended binding for the model definition rule. */
345 private boolean testdisjoint(Updates u, Rule r, Expr e) {
346 // find all exprs that may be be effected by update
347 Set exprs=e.useDescriptor(u.getDescriptor());
348 for(Iterator eit=exprs.iterator();eit.hasNext();) {
349 Expr e2=(Expr)eit.next();
350 if (testdisjointness(u,r,e2))
356 /** This method tries to show that the modification only effects
357 * one binding of the model definition rule, and thus has no
358 * unintended side effects. */
360 private boolean testdisjointness(Updates u, Rule r, Expr e) {
361 // Note: rule of u must be r
363 Expr update_e=u.getLeftExpr();
364 HashSet quantifierset=new HashSet();
366 if (termination.analyzeQuantifiers(r,quantifierset))
367 return false; /* Can't accidentally interfere with other bindings if there aren't any! */
369 boolean firstfield=true;
373 if (update_e instanceof CastExpr)
374 update_e=((CastExpr)update_e).getExpr();
375 else if (e instanceof CastExpr)
376 e=((CastExpr)e).getExpr();
377 else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
378 DotExpr de1=(DotExpr)update_e;
379 DotExpr de2=(DotExpr)e;
380 if (de1.isValue(null)&&!firstfield)
381 return true; /* Could have aliasing from this */
382 if (de1.getField()!=de2.getField())
383 return true; /* Different fields: not comparible */
386 Expr index1=de1.getIndex();
387 Expr index2=de2.getIndex();
390 if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
391 VarDescriptor vd1=((VarExpr)index1).getVar();
392 VarDescriptor vd2=((VarExpr)index2).getVar();
393 if ((vd1==vd2)&&!vd1.isGlobal()) {
394 quantifierset.add(getQuantifier(r,vd1));
395 if (termination.analyzeQuantifiers(r,quantifierset))
396 return false; /* State is disjoint from any other example */
400 update_e=de1.getExpr();
402 } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
403 VarDescriptor vd1=((VarExpr)update_e).getVar();
404 VarDescriptor vd2=((VarExpr)e).getVar();
405 if ((vd1==vd2)&&!vd1.isGlobal()) {
406 quantifierset.add(getQuantifier(r,vd1));
407 if (termination.analyzeQuantifiers(r,quantifierset))
408 return false; /* State is disjoint from any other example */
415 /** This method returns the quantifier that defines the quantifier
417 static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
418 for (int i=0;i<qs.numQuantifiers();i++) {
419 Quantifier q=qs.getQuantifier(i);
420 if (q instanceof SetQuantifier) {
421 SetQuantifier sq=(SetQuantifier)q;
424 } else if (q instanceof RelationQuantifier) {
425 RelationQuantifier rq=(RelationQuantifier)q;
426 if ((rq.x==vd)||(rq.y==vd))
428 } else if (q instanceof ForQuantifier) {
429 ForQuantifier fq=(ForQuantifier)q;
437 /** This function checks to see if an update is only performed if
438 * a given set (or image set produced by a relation) is empty, and
439 * the algorithm is computing whether the update may falsify a
440 * rule that adds something to the set */
442 private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
443 AbstractRepair ar=mun.getRepair();
444 if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
445 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
447 boolean negated=ar.getPredicate().isNegated();
448 Predicate p=ar.getPredicate().getPredicate();
449 if (!(p instanceof ExprPredicate))
451 ExprPredicate ep=(ExprPredicate)p;
452 if (ep.getType()!=ExprPredicate.SIZE)
454 Opcode op=Opcode.translateOpcode(negated,ep.getOp());
456 if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
457 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
458 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
459 ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
461 } else if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTORELATION)) {
462 /* This test is for image sets of relations. */
463 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
465 boolean negated=ar.getPredicate().isNegated();
466 Predicate p=ar.getPredicate().getPredicate();
467 if (!(p instanceof ExprPredicate))
469 ExprPredicate ep=(ExprPredicate)p;
470 if (ep.getType()!=ExprPredicate.SIZE)
473 Opcode op=Opcode.translateOpcode(negated,ep.getOp());
474 if (!(((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
475 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
476 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
477 ((op==Opcode.GE)&&(ep.rightSize()==1)))) //(>=1)
480 RelationInclusion ri=(RelationInclusion)r.getInclusion();
481 Expr tmpve=ep.inverted()?ri.getRightExpr():ri.getLeftExpr();
482 if (!(tmpve instanceof VarExpr))
484 for(int i=0;i<mun.numUpdates();i++) {
485 UpdateNode un=mun.getUpdate(i);
486 for (int j=0;j<un.numUpdates();j++) {
487 Updates update=un.getUpdate(j);
488 //Abstract updates don't have concrete interference1
489 if (update.isAbstract())
491 if (testdisjoint(update, r, r.getGuardExpr()))
500 static private boolean interferes(Updates update, DNFExpr dexpr) {
501 Descriptor descriptor=update.getDescriptor();
502 /* If the DNFExpr expr doesn't use the updated descriptor,
503 there is no interference. */
504 if (!dexpr.getExpr().usesDescriptor(descriptor))
507 if (update.isExpr()) {
508 /* We need to pair the variables */
509 Set vars=update.getRightExpr().freeVars();
510 Opcode op1=update.getOpcode();
511 Expr lexpr1=update.getLeftExpr();
512 Expr rexpr1=update.getRightExpr();
515 for(Iterator it=vars.iterator();it.hasNext();) {
516 VarDescriptor vd=(VarDescriptor) it.next();
517 /* VarDescriptor isn't a global */
518 if (!vd.isGlobal()) {
519 if (update.getVar()!=vd) {
525 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
526 OpExpr expr=(OpExpr)dexpr.getExpr();
527 Expr lexpr2=expr.getLeftExpr();
528 Expr rexpr2=expr.getRightExpr();
529 Opcode op2=expr.getOpcode();
530 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
532 VarDescriptor leftdescriptor=null;
535 while(!(e instanceof VarExpr)) {
536 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
537 if (e instanceof VarExpr)
539 if (e instanceof CastExpr)
540 e=((CastExpr)e).getExpr();
541 else throw new Error("Bad Expr Type:"+e.name());
543 leftdescriptor=((VarExpr)e).getVar();
546 vars=rexpr2.freeVars();
548 for(Iterator it=vars.iterator();it.hasNext();) {
549 VarDescriptor vd=(VarDescriptor) it.next();
550 if (!vd.isGlobal()) {
551 /* VarDescriptor isn't a global */
552 if (leftdescriptor!=vd) {
561 HashMap remap=new HashMap();
562 remap.put(update.getVar(),leftdescriptor);
564 lexpr1.equals(remap,lexpr2)&&
565 rexpr1.equals(remap,rexpr2))