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))
43 // See if the update interferes with the inclusion
44 // condition for the rule
45 if (r.getInclusion().usesDescriptor(updated_des)) {
48 /* If the update is for this rule, and the effect
49 is the intended effect, and the update only
50 effects one binding, then the abstract repair
51 node already models the action of this
54 if ((un.getRule()==r)&&
55 (((mun.op==MultUpdateNode.ADD)&&satisfy)
56 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
57 ||(mun.op==MultUpdateNode.MODIFY))) {
58 Inclusion inclusion=r.getInclusion();
59 if (inclusion instanceof RelationInclusion) {
60 RelationInclusion ri=(RelationInclusion)inclusion;
61 if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
62 (!testdisjoint(update,r,ri.getRightExpr())))
64 } else if (inclusion instanceof SetInclusion) {
65 SetInclusion si=(SetInclusion)inclusion;
66 if (!testdisjoint(update,r,si.getExpr()))
68 } else throw new Error();
73 /** Check to see if the update definitely falsifies r, thus
74 * can't accidentally satisfy it r. */
75 if (interferesinclusion(un, update, r))
78 return true; /* Interferes with inclusion condition */
82 for(int k=0;k<drule.size();k++) {
83 RuleConjunction rconj=drule.get(k);
84 for(int l=0;l<rconj.size();l++) {
85 DNFExpr dexpr=rconj.get(l);
86 /* See if update interferes w/ dexpr */
87 if ((un.getRule()==r)&&
88 (((mun.op==MultUpdateNode.ADD)&&satisfy)
89 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
90 ||(mun.op==MultUpdateNode.MODIFY))) {
91 if (!testdisjoint(update,r,dexpr.getExpr()))
92 continue; /* Update is specific to
94 rule, and effect is the
95 intended one, so we're
98 if (interferes(update,dexpr))
107 static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
108 AbstractRepair ar=mun.getRepair();
109 if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
110 for(int i=0;i<un.numUpdates();i++) {
111 Updates u=un.getUpdate(i);
112 if (u.getType()==Updates.POSITION&&
113 ar.isNewObject(u.getRightPos()==0)) {
114 Expr newleftexpr=u.getLeftExpr();
115 Expr leftexpr=updates.getLeftExpr();
116 boolean foundfield=false;
118 if (leftexpr.equals(null,newleftexpr)) {
123 } else if (leftexpr instanceof DotExpr) {
127 if (((DotExpr)leftexpr).isPtr())
128 break; //if its not a pointer, we're still in the structure
130 leftexpr=((DotExpr)leftexpr).getExpr();
131 } else if (leftexpr instanceof CastExpr) {
132 leftexpr=((CastExpr)leftexpr).getExpr();
142 /** This method tries to show that if the Update update from the
143 * UpdateNode un changes the value of the inclusion constraint
144 * that it falsifies the guard of model definition rule. */
146 static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
147 Descriptor updated_des=update.getDescriptor();
148 Inclusion inclusion=r.getInclusion();
149 if (inclusion instanceof RelationInclusion) {
150 RelationInclusion ri=(RelationInclusion)inclusion;
151 if (ri.getLeftExpr().usesDescriptor(updated_des)
152 &&searchinterfere(un,update,r,ri.getLeftExpr()))
154 if (ri.getRightExpr().usesDescriptor(updated_des)
155 &&searchinterfere(un,update,r,ri.getRightExpr()))
157 } else if (inclusion instanceof SetInclusion) {
158 SetInclusion si=(SetInclusion)inclusion;
159 if (si.getExpr().usesDescriptor(updated_des)
160 &&searchinterfere(un,update,r,si.getExpr()))
162 } else throw new Error();
166 /** This method finds all instances of a field or global that an
167 * update may modify, and builds a variable correspondance */
169 static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
170 Descriptor updated_des=update.getDescriptor();
171 if (updated_des instanceof FieldDescriptor) {
172 /* Build variable correspondance */
173 HashSet set=new HashSet();
174 inclusionexpr.findmatch(updated_des,set);
176 for(Iterator matchit=set.iterator();matchit.hasNext();) {
177 DotExpr dotexpr=(DotExpr)matchit.next();
178 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
180 if (dotexpr.getField()!=updateexpr.getField())
182 Expr de=dotexpr.getExpr();
183 Expr ue=updateexpr.getExpr();
184 if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
186 updateexpr=(DotExpr)ue;
187 } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
188 VarDescriptor dvd=((VarExpr)de).getVar();
189 VarDescriptor uvd=((VarExpr)ue).getVar();
190 if (interferesinclusion(un,r,dvd,uvd))
198 } else if (updated_des instanceof VarDescriptor) {
199 /* We have a VarDescriptor - no correspondance necessary */
200 VarDescriptor vd=(VarDescriptor)updated_des;
201 if (interferesinclusion(un,r,vd,vd))
203 } else throw new Error();
207 /** This method tries to show that if dvd=uvd, then the update un
208 * must falsify the rule r. */
210 static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
211 DNFRule negrule=r.getDNFNegGuardExpr();
212 HashMap remap=new HashMap();
215 for(int i=0;i<negrule.size();i++) {
216 RuleConjunction rconj=negrule.get(i);
218 for(int j=0;j<rconj.size();j++) {
219 DNFExpr dexpr=rconj.get(j);
220 if (dexpr.getExpr() instanceof OpExpr) {
221 OpExpr expr=(OpExpr)dexpr.getExpr();
222 Expr lexpr=expr.getLeftExpr();
223 Expr rexpr=expr.getRightExpr();
226 Set vars=rexpr.freeVars();
228 for(Iterator it=vars.iterator();it.hasNext();) {
229 VarDescriptor vd=(VarDescriptor) it.next();
230 if (!vd.isGlobal()) {
231 /* VarDescriptor isn't a global */
242 Opcode op=expr.getOpcode();
243 op=Opcode.translateOpcode(dexpr.getNegation(),op);
246 for(int k=0;k<un.numUpdates();k++) {
247 Updates update=un.getUpdate(k);
248 if(update.isExpr()) {
249 Set uvars=update.getRightExpr().freeVars();
250 boolean freevarok=true;
252 for(Iterator it=uvars.iterator();it.hasNext();) {
253 VarDescriptor vd=(VarDescriptor) it.next();
254 if (!vd.isGlobal()) {
255 /* VarDescriptor isn't a global */
265 Opcode op2=update.getOpcode();
267 ((op2==Opcode.GT)&&(op==Opcode.GE))||
268 ((op2==Opcode.LT)&&(op==Opcode.LE))||
269 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
270 /* Operations match*/
271 if (lexpr.equals(remap,update.getLeftExpr())&&
272 rexpr.equals(remap,update.getRightExpr())) {
284 /* TODO: Check to see if there is an abstract repair */
286 break; /* try next conjunction */
295 /** This method checks whether the update effects only the
296 * intended binding for the model definition rule. */
298 private boolean testdisjoint(Updates u, Rule r, Expr e) {
299 // find all exprs that may be be effected by update
300 Set exprs=e.useDescriptor(u.getDescriptor());
301 for(Iterator eit=exprs.iterator();eit.hasNext();) {
302 Expr e2=(Expr)eit.next();
303 if (testdisjointness(u,r,e2))
309 /** This method tries to show that the modification only effects
310 * one binding of the model definition rule, and thus has no
311 * unintended side effects. */
313 private boolean testdisjointness(Updates u, Rule r, Expr e) {
314 // Note: rule of u must be r
316 Expr update_e=u.getLeftExpr();
317 HashSet quantifierset=new HashSet();
319 if (termination.analyzeQuantifiers(r,quantifierset))
320 return false; /* Can't accidentally interfere with other bindings if there aren't any! */
322 boolean firstfield=true;
326 if (update_e instanceof CastExpr)
327 update_e=((CastExpr)update_e).getExpr();
328 else if (e instanceof CastExpr)
329 e=((CastExpr)e).getExpr();
330 else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
331 DotExpr de1=(DotExpr)update_e;
332 DotExpr de2=(DotExpr)e;
333 if (de1.isValue(null)&&!firstfield)
334 return true; /* Could have aliasing from this */
335 if (de1.getField()!=de2.getField())
336 return true; /* Different fields: not comparible */
339 Expr index1=de1.getIndex();
340 Expr index2=de2.getIndex();
343 if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
344 VarDescriptor vd1=((VarExpr)index1).getVar();
345 VarDescriptor vd2=((VarExpr)index2).getVar();
346 if ((vd1==vd2)&&!vd1.isGlobal()) {
347 quantifierset.add(getQuantifier(r,vd1));
348 if (termination.analyzeQuantifiers(r,quantifierset))
349 return false; /* State is disjoint from any other example */
353 update_e=de1.getExpr();
355 } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
356 VarDescriptor vd1=((VarExpr)update_e).getVar();
357 VarDescriptor vd2=((VarExpr)e).getVar();
358 if ((vd1==vd2)&&!vd1.isGlobal()) {
359 quantifierset.add(getQuantifier(r,vd1));
360 if (termination.analyzeQuantifiers(r,quantifierset))
361 return false; /* State is disjoint from any other example */
368 /** This method returns the quantifier that defines the quantifier
370 static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
371 for (int i=0;i<qs.numQuantifiers();i++) {
372 Quantifier q=qs.getQuantifier(i);
373 if (q instanceof SetQuantifier) {
374 SetQuantifier sq=(SetQuantifier)q;
377 } else if (q instanceof RelationQuantifier) {
378 RelationQuantifier rq=(RelationQuantifier)q;
379 if ((rq.x==vd)||(rq.y==vd))
381 } else if (q instanceof ForQuantifier) {
382 ForQuantifier fq=(ForQuantifier)q;
390 /** This function checks to see if an update is only performed if
391 * a given set (or image set produced by a relation) is empty, and
392 * the algorithm is computing whether the update may falsify a
393 * rule that adds something to the set */
395 private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
396 AbstractRepair ar=mun.getRepair();
397 if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
398 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
400 boolean negated=ar.getPredicate().isNegated();
401 Predicate p=ar.getPredicate().getPredicate();
402 if (!(p instanceof ExprPredicate))
404 ExprPredicate ep=(ExprPredicate)p;
405 if (ep.getType()!=ExprPredicate.SIZE)
407 Opcode op=Opcode.translateOpcode(negated,ep.getOp());
409 if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
410 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
411 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
412 ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
414 } else if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTORELATION)) {
415 /* This test is for image sets of relations. */
416 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
418 boolean negated=ar.getPredicate().isNegated();
419 Predicate p=ar.getPredicate().getPredicate();
420 if (!(p instanceof ExprPredicate))
422 ExprPredicate ep=(ExprPredicate)p;
423 if (ep.getType()!=ExprPredicate.SIZE)
426 Opcode op=Opcode.translateOpcode(negated,ep.getOp());
427 if (!(((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
428 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
429 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
430 ((op==Opcode.GE)&&(ep.rightSize()==1)))) //(>=1)
433 RelationInclusion ri=(RelationInclusion)r.getInclusion();
434 Expr tmpve=ep.inverted()?ri.getRightExpr():ri.getLeftExpr();
435 if (!(tmpve instanceof VarExpr))
437 for(int i=0;i<mun.numUpdates();i++) {
438 UpdateNode un=mun.getUpdate(i);
439 for (int j=0;j<un.numUpdates();j++) {
440 Updates update=un.getUpdate(j);
441 //Abstract updates don't have concrete interference1
442 if (update.isAbstract())
444 if (testdisjoint(update, r, r.getGuardExpr()))
453 static private boolean interferes(Updates update, DNFExpr dexpr) {
454 Descriptor descriptor=update.getDescriptor();
455 /* If the DNFExpr expr doesn't use the updated descriptor,
456 there is no interference. */
457 if (!dexpr.getExpr().usesDescriptor(descriptor))
460 if (update.isExpr()) {
461 /* We need to pair the variables */
462 Set vars=update.getRightExpr().freeVars();
463 Opcode op1=update.getOpcode();
464 Expr lexpr1=update.getLeftExpr();
465 Expr rexpr1=update.getRightExpr();
468 for(Iterator it=vars.iterator();it.hasNext();) {
469 VarDescriptor vd=(VarDescriptor) it.next();
470 /* VarDescriptor isn't a global */
471 if (!vd.isGlobal()) {
472 if (update.getVar()!=vd) {
478 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
479 OpExpr expr=(OpExpr)dexpr.getExpr();
480 Expr lexpr2=expr.getLeftExpr();
481 Expr rexpr2=expr.getRightExpr();
482 Opcode op2=expr.getOpcode();
483 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
485 VarDescriptor leftdescriptor=null;
488 while(!(e instanceof VarExpr)) {
489 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
490 if (e instanceof VarExpr)
492 if (e instanceof CastExpr)
493 e=((CastExpr)e).getExpr();
494 else throw new Error("Bad Expr Type:"+e.name());
496 leftdescriptor=((VarExpr)e).getVar();
499 vars=rexpr2.freeVars();
501 for(Iterator it=vars.iterator();it.hasNext();) {
502 VarDescriptor vd=(VarDescriptor) it.next();
503 if (!vd.isGlobal()) {
504 /* VarDescriptor isn't a global */
505 if (leftdescriptor!=vd) {
514 HashMap remap=new HashMap();
515 remap.put(update.getVar(),leftdescriptor);
517 lexpr1.equals(remap,lexpr2)&&
518 rexpr1.equals(remap,rexpr2))