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 // See if the update interferes with the inclusion
35 // condition for the rule
36 if (r.getInclusion().usesDescriptor(updated_des)) {
39 /* If the update is for this rule, and the effect
40 is the intended effect, and the update only
41 effects one binding, then the abstract repair
42 node already models the action of this
45 if ((un.getRule()==r)&&
46 (((mun.op==MultUpdateNode.ADD)&&satisfy)
47 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
48 ||(mun.op==MultUpdateNode.MODIFY))) {
49 Inclusion inclusion=r.getInclusion();
50 if (inclusion instanceof RelationInclusion) {
51 RelationInclusion ri=(RelationInclusion)inclusion;
52 if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
53 (!testdisjoint(update,r,ri.getRightExpr())))
55 } else if (inclusion instanceof SetInclusion) {
56 SetInclusion si=(SetInclusion)inclusion;
57 if (!testdisjoint(update,r,si.getExpr()))
59 } else throw new Error();
65 /** Check to see if the update definitely falsifies r, thus
66 * can't accidentally satisfy it r. */
67 if (interferesinclusion(un, update, r))
70 return true; /* Interferes with inclusion condition */
74 for(int k=0;k<drule.size();k++) {
75 RuleConjunction rconj=drule.get(k);
76 for(int l=0;l<rconj.size();l++) {
77 DNFExpr dexpr=rconj.get(l);
78 /* See if update interferes w/ dexpr */
79 if ((un.getRule()==r)&&
80 (((mun.op==MultUpdateNode.ADD)&&satisfy)
81 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
82 ||(mun.op==MultUpdateNode.MODIFY))) {
83 if (!testdisjoint(update,r,dexpr.getExpr()))
84 continue; /* Update is specific to
86 rule, and effect is the
87 intended one, so we're
90 if (interferes(update,dexpr))
99 /** This method tries to show that if the Update update from the
100 * UpdateNode un changes the value of the inclusion constraint
101 * that it falsifies the guard of model definition rule. */
103 static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
104 Descriptor updated_des=update.getDescriptor();
105 Inclusion inclusion=r.getInclusion();
106 if (inclusion instanceof RelationInclusion) {
107 RelationInclusion ri=(RelationInclusion)inclusion;
108 if (ri.getLeftExpr().usesDescriptor(updated_des)
109 &&searchinterfere(un,update,r,ri.getLeftExpr()))
111 if (ri.getRightExpr().usesDescriptor(updated_des)
112 &&searchinterfere(un,update,r,ri.getRightExpr()))
114 } else if (inclusion instanceof SetInclusion) {
115 SetInclusion si=(SetInclusion)inclusion;
116 if (si.getExpr().usesDescriptor(updated_des)
117 &&searchinterfere(un,update,r,si.getExpr()))
119 } else throw new Error();
123 /** This method finds all instances of a field or global that an
124 * update may modify, and builds a variable correspondance */
126 static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
127 Descriptor updated_des=update.getDescriptor();
128 if (updated_des instanceof FieldDescriptor) {
129 /* Build variable correspondance */
130 HashSet set=new HashSet();
131 inclusionexpr.findmatch(updated_des,set);
133 for(Iterator matchit=set.iterator();matchit.hasNext();) {
134 DotExpr dotexpr=(DotExpr)matchit.next();
135 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
137 if (dotexpr.getField()!=updateexpr.getField())
139 Expr de=dotexpr.getExpr();
140 Expr ue=updateexpr.getExpr();
141 if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
143 updateexpr=(DotExpr)ue;
144 } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
145 VarDescriptor dvd=((VarExpr)de).getVar();
146 VarDescriptor uvd=((VarExpr)ue).getVar();
147 if (interferesinclusion(un,r,dvd,uvd))
155 } else if (updated_des instanceof VarDescriptor) {
156 /* We have a VarDescriptor - no correspondance necessary */
157 VarDescriptor vd=(VarDescriptor)updated_des;
158 if (interferesinclusion(un,r,vd,vd))
160 } else throw new Error();
164 /** This method tries to show that if dvd=uvd, then the update un
165 * must falsify the rule r. */
167 static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
168 DNFRule negrule=r.getDNFNegGuardExpr();
169 HashMap remap=new HashMap();
172 for(int i=0;i<negrule.size();i++) {
173 RuleConjunction rconj=negrule.get(i);
175 for(int j=0;j<rconj.size();j++) {
176 DNFExpr dexpr=rconj.get(j);
177 if (dexpr.getExpr() instanceof OpExpr) {
178 OpExpr expr=(OpExpr)dexpr.getExpr();
179 Expr lexpr=expr.getLeftExpr();
180 Expr rexpr=expr.getRightExpr();
183 Set vars=rexpr.freeVars();
185 for(Iterator it=vars.iterator();it.hasNext();) {
186 VarDescriptor vd=(VarDescriptor) it.next();
187 if (!vd.isGlobal()) {
188 /* VarDescriptor isn't a global */
199 Opcode op=expr.getOpcode();
200 op=Opcode.translateOpcode(dexpr.getNegation(),op);
203 for(int k=0;k<un.numUpdates();k++) {
204 Updates update=un.getUpdate(k);
205 if(update.isExpr()) {
206 Set uvars=update.getRightExpr().freeVars();
207 boolean freevarok=true;
209 for(Iterator it=uvars.iterator();it.hasNext();) {
210 VarDescriptor vd=(VarDescriptor) it.next();
211 if (!vd.isGlobal()) {
212 /* VarDescriptor isn't a global */
222 Opcode op2=update.getOpcode();
224 ((op2==Opcode.GT)&&(op==Opcode.GE))||
225 ((op2==Opcode.LT)&&(op==Opcode.LE))||
226 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
227 /* Operations match*/
228 if (lexpr.equals(remap,update.getLeftExpr())&&
229 rexpr.equals(remap,update.getRightExpr())) {
241 /* TODO: Check to see if there is an abstract repair */
243 break; /* try next conjunction */
252 /** This method checks whether the update effects only the
253 * intended binding for the model definition rule. */
255 private boolean testdisjoint(Updates u, Rule r, Expr e) {
256 // find all exprs that may be be effected by update
257 Set exprs=e.useDescriptor(u.getDescriptor());
258 for(Iterator eit=exprs.iterator();eit.hasNext();) {
259 Expr e2=(Expr)eit.next();
260 if (testdisjointness(u,r,e2))
266 /** This method tries to show that the modification only effects
267 * one binding of the model definition rule, and thus has no
268 * unintended side effects. */
270 private boolean testdisjointness(Updates u, Rule r, Expr e) {
271 // Note: rule of u must be r
273 Expr update_e=u.getLeftExpr();
274 HashSet quantifierset=new HashSet();
276 if (termination.analyzeQuantifiers(r,quantifierset))
277 return false; /* Can't accidentally interfere with other bindings if there aren't any! */
279 boolean firstfield=true;
283 if (update_e instanceof CastExpr)
284 update_e=((CastExpr)update_e).getExpr();
285 else if (e instanceof CastExpr)
286 e=((CastExpr)e).getExpr();
287 else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
288 DotExpr de1=(DotExpr)update_e;
289 DotExpr de2=(DotExpr)e;
290 if (de1.isValue(null)&&!firstfield)
291 return true; /* Could have aliasing from this */
292 if (de1.getField()!=de2.getField())
293 return true; /* Different fields: not comparible */
296 Expr index1=de1.getIndex();
297 Expr index2=de2.getIndex();
300 if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
301 VarDescriptor vd1=((VarExpr)index1).getVar();
302 VarDescriptor vd2=((VarExpr)index2).getVar();
303 if ((vd1==vd2)&&!vd1.isGlobal()) {
304 quantifierset.add(getQuantifier(r,vd1));
305 if (termination.analyzeQuantifiers(r,quantifierset))
306 return false; /* State is disjoint from any other example */
310 update_e=de1.getExpr();
312 } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
313 VarDescriptor vd1=((VarExpr)update_e).getVar();
314 VarDescriptor vd2=((VarExpr)e).getVar();
315 if ((vd1==vd2)&&!vd1.isGlobal()) {
316 quantifierset.add(getQuantifier(r,vd1));
317 if (termination.analyzeQuantifiers(r,quantifierset))
318 return false; /* State is disjoint from any other example */
325 /** This method returns the quantifier that defines the quantifier
327 static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
328 for (int i=0;i<qs.numQuantifiers();i++) {
329 Quantifier q=qs.getQuantifier(i);
330 if (q instanceof SetQuantifier) {
331 SetQuantifier sq=(SetQuantifier)q;
334 } else if (q instanceof RelationQuantifier) {
335 RelationQuantifier rq=(RelationQuantifier)q;
336 if ((rq.x==vd)||(rq.y==vd))
338 } else if (q instanceof ForQuantifier) {
339 ForQuantifier fq=(ForQuantifier)q;
348 /** This function checks to see if an update is only performed if
349 * a given set is empty, and the algorithm is computing whether
350 * the update may falsify a rule that adds something to the set */
352 static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
353 AbstractRepair ar=mun.getRepair();
354 if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
355 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
357 boolean negated=ar.getPredicate().isNegated();
358 Predicate p=ar.getPredicate().getPredicate();
359 if (!(p instanceof ExprPredicate))
361 ExprPredicate ep=(ExprPredicate)p;
362 if (ep.getType()!=ExprPredicate.SIZE)
364 Opcode op=Opcode.translateOpcode(negated,ep.getOp());
366 if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
367 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
368 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
369 ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
375 static private boolean interferes(Updates update, DNFExpr dexpr) {
376 Descriptor descriptor=update.getDescriptor();
377 /* If the DNFExpr expr doesn't use the updated descriptor,
378 there is no interference. */
379 if (!dexpr.getExpr().usesDescriptor(descriptor))
382 if (update.isExpr()) {
383 /* We need to pair the variables */
384 Set vars=update.getRightExpr().freeVars();
385 Opcode op1=update.getOpcode();
386 Expr lexpr1=update.getLeftExpr();
387 Expr rexpr1=update.getRightExpr();
390 for(Iterator it=vars.iterator();it.hasNext();) {
391 VarDescriptor vd=(VarDescriptor) it.next();
392 /* VarDescriptor isn't a global */
393 if (!vd.isGlobal()) {
394 if (update.getVar()!=vd) {
400 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
401 OpExpr expr=(OpExpr)dexpr.getExpr();
402 Expr lexpr2=expr.getLeftExpr();
403 Expr rexpr2=expr.getRightExpr();
404 Opcode op2=expr.getOpcode();
405 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
407 VarDescriptor leftdescriptor=null;
410 while(!(e instanceof VarExpr)) {
411 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
412 if (e instanceof VarExpr)
414 if (e instanceof CastExpr)
415 e=((CastExpr)e).getExpr();
416 else throw new Error("Bad Expr Type:"+e.name());
418 leftdescriptor=((VarExpr)e).getVar();
421 vars=rexpr2.freeVars();
423 for(Iterator it=vars.iterator();it.hasNext();) {
424 VarDescriptor vd=(VarDescriptor) it.next();
425 if (!vd.isGlobal()) {
426 /* VarDescriptor isn't a global */
427 if (leftdescriptor!=vd) {
436 HashMap remap=new HashMap();
437 remap.put(update.getVar(),leftdescriptor);
439 lexpr1.equals(remap,lexpr2)&&
440 rexpr1.equals(remap,rexpr2))