Added:
[repair.git] / Repair / RepairCompiler / MCC / IR / AbstractInterferes.java
1 package MCC.IR;
2 import java.util.*;
3
4 class AbstractInterferes {
5     static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
6         boolean mayadd=false;
7         boolean mayremove=false;
8         switch (ar.getType()) {
9         case AbstractRepair.ADDTOSET:
10         case AbstractRepair.ADDTORELATION:
11             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
12                 return true;
13             mayadd=true;
14             break;
15         case AbstractRepair.REMOVEFROMSET:
16         case AbstractRepair.REMOVEFROMRELATION:
17             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
18                 return true;
19             mayremove=true;
20             break;
21         case AbstractRepair.MODIFYRELATION:
22             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
23                 return true;
24             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
25                 return true;
26             mayadd=true;
27             mayremove=true;
28         break;
29         default:
30             throw new Error("Unrecognized Abstract Repair");
31         }
32         DNFRule drule=null;
33         if (satisfy)
34             drule=r.getDNFGuardExpr();
35         else
36             drule=r.getDNFNegGuardExpr();
37         
38         for(int i=0;i<drule.size();i++) {
39             RuleConjunction rconj=drule.get(i);
40             for(int j=0;j<rconj.size();j++) {
41                 DNFExpr dexpr=rconj.get(j);
42                 Expr expr=dexpr.getExpr();
43                 if (expr.usesDescriptor(ar.getDescriptor())) {
44                     /* Need to check */
45                     if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
46                         return true;
47                 }
48             }
49         }
50         return false;
51     }
52
53
54     static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
55         if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
56             ((ar.getDescriptor() instanceof SetDescriptor)||
57              !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
58             return false;
59
60         /* This if handles all the c comparisons in the paper */
61         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
62             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
63             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
64             (dp.getPredicate() instanceof ExprPredicate)&&
65             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
66             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
67             boolean neg1=ar.getPredicate().isNegated();
68             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
69             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
70             boolean neg2=dp.isNegated();
71             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
72             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
73             if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
74                 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
75                 int size1a=0;
76                 if (!neg1) {
77                     if((op1==Opcode.EQ)||(op1==Opcode.GE))
78                         size1a=size1;
79                     if((op1==Opcode.GT)||(op1==Opcode.NE))
80                         size1a=size1+1;
81                 }
82                 if (neg1) {
83                     if((op1==Opcode.EQ)||(op1==Opcode.LE))
84                         size1a=size1+1;
85                     if((op1==Opcode.LT)||(op1==Opcode.NE))
86                         size1a=size1;
87                 }
88                 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
89                     (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
90                     (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
91                     (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
92                     (!neg2&&(op2==Opcode.GE))||
93                     (!neg2&&(op2==Opcode.GT))||
94                     (neg2&&(op2==Opcode.LE))||
95                     (neg2&&(op2==Opcode.LT))||
96                     (neg2&&(op2==Opcode.GE)&&(size1a<size2))||
97                     (neg2&&(op2==Opcode.GT)&&(size1a<=size2))||
98                     (!neg2&&(op2==Opcode.LE)&&(size1a<=size2))||
99                     (!neg2&&(op2==Opcode.LT)&&(size1a<size2)))
100                     return false;
101             } 
102         }
103
104         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
105             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
106             (dp.getPredicate() instanceof ExprPredicate)&&
107             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
108             boolean neg2=dp.isNegated();
109             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
110             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
111             if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
112                 (neg2&&(op2==Opcode.NE)&&(size2==0))||
113                 (!neg2&&(op2==Opcode.GE))||
114                 (!neg2&&(op2==Opcode.GT))||
115                 (neg2&&(op2==Opcode.LE))||
116                 (neg2&&(op2==Opcode.LT)))
117                 return false;
118         }
119
120         /* This handles all the c comparisons in the paper */
121         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
122             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
123             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
124             (dp.getPredicate() instanceof ExprPredicate)&&
125             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
126             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
127             boolean neg1=ar.getPredicate().isNegated();
128             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
129             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
130             boolean neg2=dp.isNegated();
131             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
132             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
133             if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
134                 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
135                 int size1a=0;
136                 if (neg1) {
137                     if((op1==Opcode.EQ)||(op1==Opcode.GE))
138                         size1a=size1-1;
139                     if((op1==Opcode.GT)||(op1==Opcode.NE))
140                         size1a=size1;
141                 }
142                 if (!neg1) {
143                     if((op1==Opcode.EQ)||(op1==Opcode.LE))
144                         size1a=size1;
145                     if((op1==Opcode.LT)||(op1==Opcode.NE))
146                         size1a=size1-1;
147                 }
148                 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
149                     (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
150                     (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
151                     (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
152                     (neg2&&(op2==Opcode.GE))||
153                     (neg2&&(op2==Opcode.GT))||
154                     (!neg2&&(op2==Opcode.LE))||
155                     (!neg2&&(op2==Opcode.LT))||
156                     (!neg2&&(op2==Opcode.GE)&&(size1a>=size2))||
157                     (!neg2&&(op2==Opcode.GT)&&(size1a>size2))||
158                     (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
159                     (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
160                     return false;
161             }
162         }
163
164         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
165             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
166             (dp.getPredicate() instanceof ExprPredicate)&&
167             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
168             boolean neg2=dp.isNegated();
169             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
170             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
171             if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
172                 (neg2&&(op2==Opcode.NE)&&(size2==0))||
173                 (neg2&&(op2==Opcode.GE))||
174                 (neg2&&(op2==Opcode.GT))||
175                 (!neg2&&(op2==Opcode.LE))||
176                 (!neg2&&(op2==Opcode.LT)))
177                 return false;
178             
179         }
180         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
181             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
182             (dp.getPredicate() instanceof InclusionPredicate)&&
183             (dp.isNegated()==false))
184             return false; /* Could only satisfy this predicate */
185
186         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
187             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
188             (dp.getPredicate() instanceof InclusionPredicate)&&
189             (dp.isNegated()==true))
190             return false; /* Could only satisfy this predicate */
191           
192         return true;
193     }
194
195     static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
196         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
197             Rule r=sn.getRule();
198             Set target=r.getInclusion().getTargetDescriptors();
199             boolean match=false;
200             for(int i=0;i<r.numQuantifiers();i++) {
201                 Quantifier q=r.getQuantifier(i);
202                 if (q instanceof SetQuantifier) {
203                     SetQuantifier sq=(SetQuantifier) q;
204                     if (target.contains(sq.getSet())) {
205                         match=true;
206                         break;
207                     }
208                 }
209             }
210             if (match&&
211                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
212                 (dp.getPredicate() instanceof ExprPredicate)&&
213                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
214                 boolean neg=dp.isNegated();
215                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
216                 int size=((ExprPredicate)dp.getPredicate()).leftsize();
217                 if (neg) {
218                     /* remove negation through opcode translation */
219                     if (op==Opcode.GT)
220                         op=Opcode.LE;
221                     else if (op==Opcode.GE)
222                         op=Opcode.LT;
223                     else if (op==Opcode.EQ)
224                         op=Opcode.NE;
225                     else if (op==Opcode.NE)
226                         op=Opcode.EQ;
227                     else if (op==Opcode.LT)
228                         op=Opcode.GE;
229                     else if (op==Opcode.LE)
230                         op=Opcode.GT;
231                 }
232                 if ((op==Opcode.GE)&&
233                     ((size==0)||(size==1)))
234                     return false;
235                 if ((op==Opcode.GT)&&
236                     (size==0))
237                     return false;
238             }
239         }
240         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
241     }
242
243     static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
244         if ((des!=dp.getPredicate().getDescriptor()) &&
245             ((des instanceof SetDescriptor)||
246              !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
247             return false;
248
249         /* This if handles all the c comparisons in the paper */
250         if (des==dp.getPredicate().getDescriptor()&&
251             (satisfy)&&
252             (dp.getPredicate() instanceof ExprPredicate)&&
253             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
254             boolean neg2=dp.isNegated();
255             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
256             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
257             {
258                 if ((!neg2&&(op2==Opcode.GE))||
259                     (!neg2&&(op2==Opcode.GT))||
260                     (neg2&&(op2==Opcode.EQ)&&(size2==0))||
261                     (!neg2&&(op2==Opcode.NE)&&(size2==0))||
262                     (neg2&&(op2==Opcode.LE))||
263                     (neg2&&(op2==Opcode.LT)))
264                     return false;
265             }
266         }
267         /* This if handles all the c comparisons in the paper */
268         if (des==dp.getPredicate().getDescriptor()&&
269             (!satisfy)&&
270             (dp.getPredicate() instanceof ExprPredicate)&&
271             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
272             boolean neg2=dp.isNegated();
273             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
274             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
275             {
276                 if ((neg2&&(op2==Opcode.GE))||
277                     (neg2&&(op2==Opcode.GT))||
278                     (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
279                     (neg2&&(op2==Opcode.NE)&&(size2==0))||
280                     (!neg2&&(op2==Opcode.LE))||
281                     (!neg2&&(op2==Opcode.LT)))
282                     return false;
283             } 
284         }
285         if ((des==dp.getPredicate().getDescriptor())&&
286             satisfy&&
287             (dp.getPredicate() instanceof InclusionPredicate)&&
288             (dp.isNegated()==false))
289             return false; /* Could only satisfy this predicate */
290
291         if ((des==dp.getPredicate().getDescriptor())&&
292             (!satisfy)&&
293             (dp.getPredicate() instanceof InclusionPredicate)&&
294             (dp.isNegated()==true))
295             return false; /* Could only satisfy this predicate */
296
297         return true;
298     }
299
300     static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
301         for(int i=0;i<r.numQuantifiers();i++) {
302             Quantifier q=r.getQuantifier(i);
303             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
304                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
305                     return true;
306             } else if (q instanceof ForQuantifier) {
307                 if (q.getRequiredDescriptors().contains(des))
308                     return true;
309             } else throw new Error("Unrecognized Quantifier");
310         }
311         return false;
312     }
313
314     static public boolean interferes(AbstractRepair ar, Quantifiers q) {
315         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
316             return interferesquantifier(ar.getDescriptor(),true,q,true);
317         return false;
318     }
319
320     static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
321         return interferesquantifier(des, satisfy, q,true);
322     }
323
324     static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
325         if (interferesquantifier(des,satisfy,r,satisfyrule))
326             return true;
327         /* Scan DNF form */
328         DNFRule drule=r.getDNFGuardExpr();
329         for(int i=0;i<drule.size();i++) {
330             RuleConjunction rconj=drule.get(i);
331             for(int j=0;j<rconj.size();j++) {
332                 DNFExpr dexpr=rconj.get(j);
333                 Expr expr=dexpr.getExpr();
334                 boolean negated=dexpr.getNegation();
335                 /*
336                   satisfy  negated
337                   Yes      No             Yes
338                   Yes      Yes            No
339                   No       No             No
340                   No       Yes            Yes
341                 */
342                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
343                 if (satisfiesrule==satisfyrule) {
344                     /* Effect is the one being tested for */
345                     /* Only expr's to be concerned with are TupleOfExpr and
346                        ElementOfExpr */
347                     if (expr.getRequiredDescriptors().contains(des)) {
348                         if (((expr instanceof ElementOfExpr)||
349                             (expr instanceof TupleOfExpr))&&
350                             (expr.getRequiredDescriptors().size()==1))
351                             return true;
352                         else
353                             throw new Error("Unrecognized EXPR");
354                     }
355                 }
356             }
357         }
358         return false;
359     }
360 }