4 public class ConcreteInterferes {
5 Termination termination;
7 public ConcreteInterferes(Termination t) {
12 static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
13 Descriptor updated_des=update.getDescriptor();
14 Inclusion inclusion=r.getInclusion();
15 if (inclusion instanceof RelationInclusion) {
16 RelationInclusion ri=(RelationInclusion)inclusion;
17 if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
19 if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
21 } else if (inclusion instanceof SetInclusion) {
22 SetInclusion si=(SetInclusion)inclusion;
23 if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
25 } else throw new Error();
29 static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
30 Descriptor updated_des=update.getDescriptor();
31 if (updated_des instanceof FieldDescriptor) {
32 /* Build variable correspondance */
33 HashSet set=new HashSet();
34 inclusionexpr.findmatch(updated_des,set);
36 for(Iterator matchit=set.iterator();matchit.hasNext();) {
37 DotExpr dotexpr=(DotExpr)matchit.next();
38 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
40 if (dotexpr.getField()!=updateexpr.getField())
42 Expr de=dotexpr.getExpr();
43 Expr ue=updateexpr.getExpr();
44 if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
46 updateexpr=(DotExpr)ue;
47 } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
48 VarDescriptor dvd=((VarExpr)de).getVar();
49 VarDescriptor uvd=((VarExpr)ue).getVar();
50 if (interferesinclusion(un,r,dvd,uvd))
58 } else if (updated_des instanceof VarDescriptor) {
59 /* We have a VarDescriptor - no correspondance necessary */
60 VarDescriptor vd=(VarDescriptor)updated_des;
61 if (interferesinclusion(un,r,vd,vd))
63 } else throw new Error();
67 static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
68 DNFRule negrule=r.getDNFNegGuardExpr();
69 HashMap remap=new HashMap();
72 for(int i=0;i<negrule.size();i++) {
73 RuleConjunction rconj=negrule.get(i);
75 for(int j=0;j<rconj.size();j++) {
76 DNFExpr dexpr=rconj.get(j);
77 if (dexpr.getExpr() instanceof OpExpr) {
78 OpExpr expr=(OpExpr)dexpr.getExpr();
79 Expr lexpr=expr.getLeftExpr();
80 Expr rexpr=expr.getRightExpr();
83 Set vars=rexpr.freeVars();
85 for(Iterator it=vars.iterator();it.hasNext();) {
86 VarDescriptor vd=(VarDescriptor) it.next();
88 /* VarDescriptor isn't a global */
101 Opcode op=expr.getOpcode();
102 op=Opcode.translateOpcode(dexpr.getNegation(),op);
105 for(int k=0;k<un.numUpdates();k++) {
106 Updates update=un.getUpdate(k);
107 if(update.isExpr()) {
108 Set uvars=update.getRightExpr().freeVars();
109 boolean freevarok=true;
111 for(Iterator it=uvars.iterator();it.hasNext();) {
112 VarDescriptor vd=(VarDescriptor) it.next();
113 if (!vd.isGlobal()) {
114 /* VarDescriptor isn't a global */
124 Opcode op2=update.getOpcode();
126 ((op2==Opcode.GT)&&(op==Opcode.GE))||
127 ((op2==Opcode.LT)&&(op==Opcode.LE))||
128 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
129 /* Operations match*/
130 if (lexpr.equals(remap,update.getLeftExpr())&&
131 rexpr.equals(remap,update.getRightExpr())) {
143 /* TODO: Check to see if there is an abstract repair */
145 break; /* try next conjunction */
154 /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
155 * the scope of the model definition rule r. */
157 public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
158 if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
160 for(int i=0;i<mun.numUpdates();i++) {
161 UpdateNode un=mun.getUpdate(i);
162 for (int j=0;j<un.numUpdates();j++) {
163 Updates update=un.getUpdate(j);
165 DNFRule drule=r.getDNFGuardExpr();
167 drule=r.getDNFNegGuardExpr();
170 if (!update.isAbstract()) {
171 Descriptor updated_des=update.getDescriptor();
172 assert updated_des!=null;
173 /* Update is local to this rule, and the effect is intentional */
174 /* If we're adding something, a side effect could be to falsify some other binding
175 If we're removing something, there is no similar side effect */
177 /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
178 if (r.getInclusion().usesDescriptor(updated_des)) {
180 if ((un.getRule()==r)&&
181 (((mun.op==MultUpdateNode.ADD)&&satisfy)
182 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
183 ||(mun.op==MultUpdateNode.MODIFY))) {
184 Inclusion inclusion=r.getInclusion();
185 if (inclusion instanceof RelationInclusion) {
186 RelationInclusion ri=(RelationInclusion)inclusion;
187 if ((!interferes(update,r,ri.getLeftExpr()))&&
188 (!interferes(update,r,ri.getRightExpr())))
190 } else if (inclusion instanceof SetInclusion) {
191 SetInclusion si=(SetInclusion)inclusion;
192 if (!interferes(update,r,si.getExpr()))
194 } else throw new Error();
198 if (interferesinclusion(un, update, r))
201 return true; /* Interferes with inclusion condition */
205 for(int k=0;k<drule.size();k++) {
206 RuleConjunction rconj=drule.get(k);
207 for(int l=0;l<rconj.size();l++) {
208 DNFExpr dexpr=rconj.get(l);
209 /* See if update interferes w/ dexpr */
210 if ((un.getRule()==r)&&
211 (((mun.op==MultUpdateNode.ADD)&&satisfy)
212 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
213 ||(mun.op==MultUpdateNode.MODIFY))) {
214 if (!interferes(update,r,dexpr.getExpr()))
215 continue; /* unique state - we're okay */
217 if (interferes(un,update, r,dexpr))
227 private boolean interferes(Updates u, Rule r, Expr e) {
228 Set exprs=e.useDescriptor(u.getDescriptor());
229 for(Iterator eit=exprs.iterator();eit.hasNext();) {
230 Expr e2=(Expr)eit.next();
231 if (mayinterfere(u,r,e2))
237 private boolean mayinterfere(Updates u, Rule r, Expr e) {
238 // Note: rule of u must be r
240 Expr update_e=u.getLeftExpr();
241 HashSet quantifierset=new HashSet();
243 if (termination.analyzeQuantifiers(r,quantifierset))
244 return false; /* Can't accidentally interfere with other bindings if there aren't any! */
246 boolean firstfield=true;
248 if (update_e instanceof CastExpr)
249 update_e=((CastExpr)update_e).getExpr();
250 else if (e instanceof CastExpr)
251 e=((CastExpr)e).getExpr();
252 else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
253 DotExpr de1=(DotExpr)update_e;
254 DotExpr de2=(DotExpr)e;
255 if (de1.isValue(null)&&!firstfield)
256 return true; /* Could have aliasing from this */
257 if (de1.getField()!=de2.getField())
258 return true; /* Different fields: not comparible */
261 Expr index1=de1.getIndex();
262 Expr index2=de2.getIndex();
265 if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
266 VarDescriptor vd1=((VarExpr)index1).getVar();
267 VarDescriptor vd2=((VarExpr)index2).getVar();
268 if ((vd1==vd2)&&!vd1.isGlobal()) {
269 quantifierset.add(getQuantifier(r,vd1));
270 if (termination.analyzeQuantifiers(r,quantifierset))
271 return false; /* State is disjoint from any other example */
275 update_e=de1.getExpr();
277 } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
278 VarDescriptor vd1=((VarExpr)update_e).getVar();
279 VarDescriptor vd2=((VarExpr)e).getVar();
280 if ((vd1==vd2)&&!vd1.isGlobal()) {
281 quantifierset.add(getQuantifier(r,vd1));
282 if (termination.analyzeQuantifiers(r,quantifierset))
283 return false; /* State is disjoint from any other example */
291 static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
292 for (int i=0;i<qs.numQuantifiers();i++) {
293 Quantifier q=qs.getQuantifier(i);
294 if (q instanceof SetQuantifier) {
295 SetQuantifier sq=(SetQuantifier)q;
298 } else if (q instanceof RelationQuantifier) {
299 RelationQuantifier rq=(RelationQuantifier)q;
300 if ((rq.x==vd)||(rq.y==vd))
302 } else if (q instanceof ForQuantifier) {
303 ForQuantifier fq=(ForQuantifier)q;
311 static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
312 AbstractRepair ar=mun.getRepair();
317 if (ar.getType()!=AbstractRepair.ADDTOSET)
319 // if (mun.op!=MultUpdateNode.ADD) (Redundant)
321 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
323 boolean negated=ar.getPredicate().isNegated();
324 Predicate p=ar.getPredicate().getPredicate();
325 if (!(p instanceof ExprPredicate))
327 ExprPredicate ep=(ExprPredicate)p;
328 if (ep.getType()!=ExprPredicate.SIZE)
330 if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
332 if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
335 if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
337 if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
342 if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
344 if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
347 if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
349 if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
357 static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
358 Descriptor descriptor=update.getDescriptor();
359 if (!dexpr.getExpr().usesDescriptor(descriptor))
362 /* We need to pair the variables */
363 if (update.isExpr()) {
364 Set vars=update.getRightExpr().freeVars();
365 Opcode op1=update.getOpcode();
366 Expr lexpr1=update.getLeftExpr();
367 Expr rexpr1=update.getRightExpr();
370 for(Iterator it=vars.iterator();it.hasNext();) {
371 VarDescriptor vd=(VarDescriptor) it.next();
372 if (!vd.isGlobal()) {
373 /* VarDescriptor isn't a global */
374 if (update.getVar()!=vd) {
380 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
381 OpExpr expr=(OpExpr)dexpr.getExpr();
382 Expr lexpr2=expr.getLeftExpr();
383 Expr rexpr2=expr.getRightExpr();
384 Opcode op2=expr.getOpcode();
385 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
388 vars=rexpr2.freeVars();
389 VarDescriptor leftdescriptor=null;
390 if (lexpr2 instanceof VarExpr)
391 leftdescriptor=((VarExpr)lexpr2).getVar();
392 else if (lexpr2 instanceof DotExpr) {
395 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
396 if (e instanceof VarExpr)
398 if (e instanceof CastExpr)
399 e=((CastExpr)e).getExpr();
400 else throw new Error("Bad Expr Type:"+e.name());
402 leftdescriptor=((VarExpr)e).getVar();
403 } else throw new Error("Bad Expr");
406 for(Iterator it=vars.iterator();it.hasNext();) {
407 VarDescriptor vd=(VarDescriptor) it.next();
408 if (!vd.isGlobal()) {
409 /* VarDescriptor isn't a global */
410 if (leftdescriptor!=vd) {
417 HashMap remap=new HashMap();
418 remap.put(update.getVar(),leftdescriptor);
420 lexpr1.equals(remap,lexpr2)&&
421 rexpr1.equals(remap,rexpr2))