4 class ConcreteInterferes {
6 static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
7 Descriptor updated_des=update.getDescriptor();
8 Inclusion inclusion=r.getInclusion();
9 if (inclusion instanceof RelationInclusion) {
10 RelationInclusion ri=(RelationInclusion)inclusion;
11 if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
13 if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
15 } else if (inclusion instanceof SetInclusion) {
16 SetInclusion si=(SetInclusion)inclusion;
17 if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
19 } else throw new Error();
23 static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
24 Descriptor updated_des=update.getDescriptor();
25 if (updated_des instanceof FieldDescriptor) {
26 /* Build variable correspondance */
27 HashSet set=new HashSet();
28 inclusionexpr.findmatch(updated_des,set);
30 for(Iterator matchit=set.iterator();matchit.hasNext();) {
31 DotExpr dotexpr=(DotExpr)matchit.next();
32 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
34 if (dotexpr.getField()!=updateexpr.getField())
36 Expr de=dotexpr.getExpr();
37 Expr ue=updateexpr.getExpr();
38 if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
40 updateexpr=(DotExpr)ue;
41 } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
42 VarDescriptor dvd=((VarExpr)de).getVar();
43 VarDescriptor uvd=((VarExpr)ue).getVar();
44 if (interferesinclusion(un,r,dvd,uvd))
52 } else if (updated_des instanceof VarDescriptor) {
53 /* We have a VarDescriptor - no correspondance necessary */
54 VarDescriptor vd=(VarDescriptor)updated_des;
55 if (interferesinclusion(un,r,vd,vd))
57 } else throw new Error();
61 static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
62 DNFRule negrule=r.getDNFNegGuardExpr();
63 HashMap remap=new HashMap();
66 for(int i=0;i<negrule.size();i++) {
67 RuleConjunction rconj=negrule.get(i);
69 for(int j=0;j<rconj.size();j++) {
70 DNFExpr dexpr=rconj.get(j);
71 if (dexpr.getExpr() instanceof OpExpr) {
72 OpExpr expr=(OpExpr)dexpr.getExpr();
73 Expr lexpr=expr.getLeftExpr();
74 Expr rexpr=expr.getRightExpr();
77 Set vars=rexpr.freeVars();
79 for(Iterator it=vars.iterator();it.hasNext();) {
80 VarDescriptor vd=(VarDescriptor) it.next();
82 /* VarDescriptor isn't a global */
95 Opcode op=expr.getOpcode();
97 if (dexpr.getNegation()) {
98 /* remove negation through opcode translation */
101 else if (op==Opcode.GE)
103 else if (op==Opcode.EQ)
105 else if (op==Opcode.NE)
107 else if (op==Opcode.LT)
109 else if (op==Opcode.LE)
113 for(int k=0;k<un.numUpdates();k++) {
114 Updates update=un.getUpdate(k);
115 if(update.isExpr()) {
116 Set uvars=update.getRightExpr().freeVars();
117 boolean freevarok=true;
119 for(Iterator it=uvars.iterator();it.hasNext();) {
120 VarDescriptor vd=(VarDescriptor) it.next();
121 if (!vd.isGlobal()) {
122 /* VarDescriptor isn't a global */
132 Opcode op2=update.getOpcode();
134 ((op2==Opcode.GT)&&(op==Opcode.GE))||
135 ((op2==Opcode.LT)&&(op==Opcode.LE))||
136 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
137 /* Operations match*/
138 if (lexpr.equals(remap,update.getLeftExpr())&&
139 rexpr.equals(remap,update.getRightExpr())) {
151 /* TODO: Check to see if there is an abstract repair */
153 break; /* try next conjunction */
162 static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
163 if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
165 for(int i=0;i<mun.numUpdates();i++) {
166 UpdateNode un=mun.getUpdate(i);
167 for (int j=0;j<un.numUpdates();j++) {
168 Updates update=un.getUpdate(j);
170 DNFRule drule=r.getDNFGuardExpr();
172 drule=r.getDNFNegGuardExpr();
175 if (!update.isAbstract()) {
176 Descriptor updated_des=update.getDescriptor();
177 assert updated_des!=null;
178 /* Update is local to this rule, and the effect is intentional */
179 /* If we're adding something, a side effect could be to falsify some other binding
180 If we're removing something, there is no similar side effect */
181 if ((un.getRule()==r)&&
182 (((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
183 (r.numQuantifiers()==1)&&
184 (r.getQuantifier(0) instanceof SetQuantifier)&&
186 (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
187 ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
189 if ((un.getRule()==r)&&
190 (((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
191 (r.numQuantifiers()==0))
195 if (r.getInclusion().usesDescriptor(updated_des)) {
197 if (interferesinclusion(un, update, r))
200 return true; /* Interferes with inclusion condition */
203 for(int k=0;k<drule.size();k++) {
204 RuleConjunction rconj=drule.get(k);
205 for(int l=0;l<rconj.size();l++) {
208 DNFExpr dexpr=rconj.get(l);
209 /* See if update interferes w/ dexpr */
210 if (interferes(un,update, r,dexpr))
220 static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
221 AbstractRepair ar=mun.getRepair();
226 if (ar.getType()!=AbstractRepair.ADDTOSET)
228 // if (mun.op!=MultUpdateNode.ADD) (Redundant)
230 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
232 boolean negated=ar.getPredicate().isNegated();
233 Predicate p=ar.getPredicate().getPredicate();
234 if (!(p instanceof ExprPredicate))
236 ExprPredicate ep=(ExprPredicate)p;
237 if (ep.getType()!=ExprPredicate.SIZE)
239 if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==1)&&!negated)
241 if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==1)&&negated)
244 if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==0)&&!negated)
246 if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==0)&&negated)
251 if ((ep.getOp()==Opcode.GT)&&(ep.leftsize()==0)&&!negated)
253 if ((ep.getOp()==Opcode.LE)&&(ep.leftsize()==0)&&negated)
256 if ((ep.getOp()==Opcode.GE)&&(ep.leftsize()==1)&&!negated)
258 if ((ep.getOp()==Opcode.LT)&&(ep.leftsize()==1)&&negated)
266 static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
267 Descriptor descriptor=update.getDescriptor();
268 if (!dexpr.getExpr().usesDescriptor(descriptor))
271 /* We need to pair the variables */
272 if (update.isExpr()) {
273 Set vars=update.getRightExpr().freeVars();
274 Opcode op1=update.getOpcode();
275 Expr lexpr1=update.getLeftExpr();
276 Expr rexpr1=update.getRightExpr();
279 for(Iterator it=vars.iterator();it.hasNext();) {
280 VarDescriptor vd=(VarDescriptor) it.next();
281 if (!vd.isGlobal()) {
282 /* VarDescriptor isn't a global */
283 if (update.getVar()!=vd) {
289 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
290 OpExpr expr=(OpExpr)dexpr.getExpr();
291 Expr lexpr2=expr.getLeftExpr();
292 Expr rexpr2=expr.getRightExpr();
293 Opcode op2=expr.getOpcode();
294 if (dexpr.getNegation()) {
295 /* remove negation through opcode translation */
298 else if (op2==Opcode.GE)
300 else if (op2==Opcode.EQ)
302 else if (op2==Opcode.NE)
304 else if (op2==Opcode.LT)
306 else if (op2==Opcode.LE)
310 vars=rexpr2.freeVars();
311 VarDescriptor leftdescriptor=null;
312 if (lexpr2 instanceof VarExpr)
313 leftdescriptor=((VarExpr)lexpr2).getVar();
314 else if (lexpr2 instanceof DotExpr) {
316 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
317 leftdescriptor=((VarExpr)e).getVar();
318 } else throw new Error("Bad Expr");
321 for(Iterator it=vars.iterator();it.hasNext();) {
322 VarDescriptor vd=(VarDescriptor) it.next();
323 if (!vd.isGlobal()) {
324 /* VarDescriptor isn't a global */
325 if (leftdescriptor!=vd) {
332 HashMap remap=new HashMap();
333 remap.put(update.getVar(),leftdescriptor);
335 lexpr1.equals(remap,lexpr2)&&
336 rexpr1.equals(remap,rexpr2))