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 /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
163 * the scope of the model definition rule r. */
165 static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
166 if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
168 for(int i=0;i<mun.numUpdates();i++) {
169 UpdateNode un=mun.getUpdate(i);
170 for (int j=0;j<un.numUpdates();j++) {
171 Updates update=un.getUpdate(j);
173 DNFRule drule=r.getDNFGuardExpr();
175 drule=r.getDNFNegGuardExpr();
178 if (!update.isAbstract()) {
179 Descriptor updated_des=update.getDescriptor();
180 assert updated_des!=null;
181 /* Update is local to this rule, and the effect is intentional */
182 /* If we're adding something, a side effect could be to falsify some other binding
183 If we're removing something, there is no similar side effect */
185 /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
186 if ((un.getRule()==r)&&
187 (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
188 (r.numQuantifiers()==1)&&
189 (r.getQuantifier(0) instanceof SetQuantifier)&&
191 (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
192 ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
195 if ((un.getRule()==r)&&
196 (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
197 (r.numQuantifiers()==0))
201 if (r.getInclusion().usesDescriptor(updated_des)) {
203 if (interferesinclusion(un, update, r))
206 return true; /* Interferes with inclusion condition */
209 for(int k=0;k<drule.size();k++) {
210 RuleConjunction rconj=drule.get(k);
211 for(int l=0;l<rconj.size();l++) {
214 DNFExpr dexpr=rconj.get(l);
215 /* See if update interferes w/ dexpr */
216 if (interferes(un,update, r,dexpr))
226 static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
227 AbstractRepair ar=mun.getRepair();
232 if (ar.getType()!=AbstractRepair.ADDTOSET)
234 // if (mun.op!=MultUpdateNode.ADD) (Redundant)
236 if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
238 boolean negated=ar.getPredicate().isNegated();
239 Predicate p=ar.getPredicate().getPredicate();
240 if (!(p instanceof ExprPredicate))
242 ExprPredicate ep=(ExprPredicate)p;
243 if (ep.getType()!=ExprPredicate.SIZE)
245 if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
247 if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
250 if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
252 if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
257 if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
259 if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
262 if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
264 if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
272 static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
273 Descriptor descriptor=update.getDescriptor();
274 if (!dexpr.getExpr().usesDescriptor(descriptor))
277 /* We need to pair the variables */
278 if (update.isExpr()) {
279 Set vars=update.getRightExpr().freeVars();
280 Opcode op1=update.getOpcode();
281 Expr lexpr1=update.getLeftExpr();
282 Expr rexpr1=update.getRightExpr();
285 for(Iterator it=vars.iterator();it.hasNext();) {
286 VarDescriptor vd=(VarDescriptor) it.next();
287 if (!vd.isGlobal()) {
288 /* VarDescriptor isn't a global */
289 if (update.getVar()!=vd) {
295 if (good&&(dexpr.getExpr() instanceof OpExpr)) {
296 OpExpr expr=(OpExpr)dexpr.getExpr();
297 Expr lexpr2=expr.getLeftExpr();
298 Expr rexpr2=expr.getRightExpr();
299 Opcode op2=expr.getOpcode();
300 if (dexpr.getNegation()) {
301 /* remove negation through opcode translation */
304 else if (op2==Opcode.GE)
306 else if (op2==Opcode.EQ)
308 else if (op2==Opcode.NE)
310 else if (op2==Opcode.LT)
312 else if (op2==Opcode.LE)
316 vars=rexpr2.freeVars();
317 VarDescriptor leftdescriptor=null;
318 if (lexpr2 instanceof VarExpr)
319 leftdescriptor=((VarExpr)lexpr2).getVar();
320 else if (lexpr2 instanceof DotExpr) {
323 for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
324 if (e instanceof VarExpr)
326 if (e instanceof CastExpr)
327 e=((CastExpr)e).getExpr();
328 else throw new Error("Bad Expr Type:"+e.name());
330 leftdescriptor=((VarExpr)e).getVar();
331 } else throw new Error("Bad Expr");
334 for(Iterator it=vars.iterator();it.hasNext();) {
335 VarDescriptor vd=(VarDescriptor) it.next();
336 if (!vd.isGlobal()) {
337 /* VarDescriptor isn't a global */
338 if (leftdescriptor!=vd) {
345 HashMap remap=new HashMap();
346 remap.put(update.getVar(),leftdescriptor);
348 lexpr1.equals(remap,lexpr2)&&
349 rexpr1.equals(remap,rexpr2))