Name typedefs
[repair.git] / Repair / RepairCompiler / MCC / IR / ConcreteInterferes.java
1 package MCC.IR;
2 import java.util.*;
3
4 public class ConcreteInterferes {
5     Termination termination;
6
7     public ConcreteInterferes(Termination t) {
8         this.termination=t;
9     }
10
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. */
14
15     public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
16         
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)) 
20             return false;
21
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()) 
28                     continue;
29
30                 DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
31                 Descriptor updated_des=update.getDescriptor();
32                 assert updated_des!=null;
33
34                 /* Test to see if the update only effects new
35                    objects and we're only testing for falsifying
36                    model definition rules. */
37                 
38                 if ((!satisfy)&&updateonlytonewobject(mun,un,update))
39                     continue;
40
41
42                 // See if the update interferes with the inclusion
43                 // condition for the rule
44                 if (r.getInclusion().usesDescriptor(updated_des)) {
45                     boolean ok=false;
46
47                     /* If the update is for this rule, and the effect
48                        is the intended effect, and the update only
49                        effects one binding, then the abstract repair
50                        node already models the action of this
51                        update. */
52
53                     if ((un.getRule()==r)&& 
54                         (((mun.op==MultUpdateNode.ADD)&&satisfy)
55                          ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
56                          ||(mun.op==MultUpdateNode.MODIFY))) {
57                         Inclusion inclusion=r.getInclusion();
58                         if (inclusion instanceof RelationInclusion) {
59                             RelationInclusion ri=(RelationInclusion)inclusion;
60                             if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
61                                 (!testdisjoint(update,r,ri.getRightExpr())))
62                                 ok=true;
63                         } else if (inclusion instanceof SetInclusion) {
64                             SetInclusion si=(SetInclusion)inclusion;
65                             if (!testdisjoint(update,r,si.getExpr()))
66                                 ok=true;
67                         } else throw new Error();
68                     }
69
70                     if ((un.getRule()==r)&&
71                         ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
72                         modifiesremoves(mun,un,r)) {
73                         Inclusion inclusion=r.getInclusion();
74                         if (inclusion instanceof RelationInclusion) {
75                             RelationInclusion ri=(RelationInclusion)inclusion;
76                             if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
77                                 (!testdisjoint(update,r,ri.getRightExpr())))
78                                 ok=true;         /* Update is specific to
79                                                     given binding of the rule,
80                                                     and adds are only performed
81                                                     if the removal is desired or
82                                                     the tuple doesn't exist.*/
83                         }
84                     }
85
86                     if (!ok) {
87                         if (satisfy) {
88                             /** Check to see if the update definitely falsifies r, thus
89                              * can't accidentally satisfy it r. */
90                             if (interferesinclusion(un, update, r)) 
91                                 return true;
92                         } else
93                             return true; /* Interferes with inclusion condition */
94                     }
95                 }
96                 
97                 for(int k=0;k<drule.size();k++) {
98                     RuleConjunction rconj=drule.get(k);
99                     for(int l=0;l<rconj.size();l++) {
100                         DNFExpr dexpr=rconj.get(l);
101                         /* See if update interferes w/ dexpr */
102                         if ((un.getRule()==r)&&
103                             (((mun.op==MultUpdateNode.ADD)&&satisfy)
104                              ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
105                              ||(mun.op==MultUpdateNode.MODIFY))) {
106                             if (!testdisjoint(update,r,dexpr.getExpr()))
107                                 continue; /* Update is specific to
108                                              given binding of the
109                                              rule, and effect is the
110                                              intended one, so we're
111                                              okay */
112                         }
113                         if ((un.getRule()==r)&&
114                             ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
115                             modifiesremoves(mun,un,r)) {
116                             if (!testdisjoint(update,r,dexpr.getExpr()))
117                                 continue; /* Update is specific to
118                                              given binding of the
119                                              rule, and adds are only
120                                              performed if the removal
121                                              is desired or the tuple
122                                              doesn't exist.*/
123                         }
124
125                         if (interferes(update,dexpr))
126                             return true;
127                     }
128                 }           
129             }
130         }
131         return false;
132     }
133
134
135     static private boolean modifiesremoves(MultUpdateNode mun,UpdateNode un, Rule r) {
136         AbstractRepair ar=mun.getRepair();
137         boolean inverted=ar.getPredicate().getPredicate().inverted();
138
139         if (ar.getType()!=AbstractRepair.MODIFYRELATION)
140             return false;
141         RelationInclusion ri=(RelationInclusion)r.getInclusion();
142         Expr e=inverted?ri.getRightExpr():ri.getLeftExpr();
143         while(e instanceof CastExpr) {
144             e=((CastExpr)e).getExpr();
145         }
146         if (!(e instanceof VarExpr))
147             return false;
148         VarExpr ve=(VarExpr)e;
149         if (ve.isValue())
150             return false;
151         return true;
152     }
153     
154     static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
155         AbstractRepair ar=mun.getRepair();
156         if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
157             for(int i=0;i<un.numUpdates();i++) {
158                 Updates u=un.getUpdate(i);
159                 if (u.getType()==Updates.POSITION&&
160                     ar.isNewObject(u.getRightPos()==0)) {
161                     Expr newleftexpr=u.getLeftExpr();
162                     Expr leftexpr=updates.getLeftExpr();
163                     boolean foundfield=false;
164                     while(true) {
165                         if (leftexpr.equals(null,newleftexpr)) {
166                             if (foundfield)
167                                 return true;
168                             else
169                                 break;
170                         } else if (leftexpr instanceof DotExpr) {
171                             if (!foundfield) {
172                                 foundfield=true;
173                             } else {
174                                 if (((DotExpr)leftexpr).isPtr())
175                                     break; //if its not a pointer, we're still in the structure
176                             }
177                             leftexpr=((DotExpr)leftexpr).getExpr();
178                         } else if (leftexpr instanceof CastExpr) {
179                             leftexpr=((CastExpr)leftexpr).getExpr();
180                         } else
181                             break;
182                     }
183                 }
184             }
185         
186         return false;
187     }
188
189     /** This method tries to show that if the Update update from the
190      *  UpdateNode un changes the value of the inclusion constraint
191      * that it falsifies the guard of model definition rule. */
192     
193     static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
194         Descriptor updated_des=update.getDescriptor();
195         Inclusion inclusion=r.getInclusion();
196         if (inclusion instanceof RelationInclusion) {
197             RelationInclusion ri=(RelationInclusion)inclusion;
198             if (ri.getLeftExpr().usesDescriptor(updated_des)
199                 &&searchinterfere(un,update,r,ri.getLeftExpr()))
200                 return true;
201             if (ri.getRightExpr().usesDescriptor(updated_des)
202                 &&searchinterfere(un,update,r,ri.getRightExpr()))
203                 return true;
204         } else if (inclusion instanceof SetInclusion) {
205             SetInclusion si=(SetInclusion)inclusion;
206             if (si.getExpr().usesDescriptor(updated_des)
207                 &&searchinterfere(un,update,r,si.getExpr()))
208                 return true;
209         } else throw new Error();
210         return false;
211     }
212
213     /** This method finds all instances of a field or global that an
214      * update may modify, and builds a variable correspondance */
215
216     static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
217         Descriptor updated_des=update.getDescriptor();
218         if (updated_des instanceof FieldDescriptor) {
219             /* Build variable correspondance */
220             HashSet set=new HashSet();
221             inclusionexpr.findmatch(updated_des,set);
222             
223             for(Iterator matchit=set.iterator();matchit.hasNext();) {
224                 DotExpr dotexpr=(DotExpr)matchit.next();
225                 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
226                 while(true) {
227                     if (dotexpr.getField()!=updateexpr.getField())
228                         return true;
229                     Expr de=dotexpr.getExpr();
230                     Expr ue=updateexpr.getExpr();
231                     if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
232                         dotexpr=(DotExpr)de;
233                         updateexpr=(DotExpr)ue;
234                     } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
235                         VarDescriptor dvd=((VarExpr)de).getVar();
236                         VarDescriptor uvd=((VarExpr)ue).getVar();
237                         if (interferesinclusion(un,r,dvd,uvd))
238                             return true;
239                         else
240                             break;
241                     } else
242                         return true;
243                 }
244             }
245         } else if (updated_des instanceof VarDescriptor) {
246             /* We have a VarDescriptor - no correspondance necessary */
247             VarDescriptor vd=(VarDescriptor)updated_des;
248             if (interferesinclusion(un,r,vd,vd))
249                 return true;
250         } else throw new Error();
251         return false;
252     }
253
254     /** This method tries to show that if dvd=uvd, then the update un
255      *  must falsify the rule r. */
256
257     static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
258         DNFRule negrule=r.getDNFNegGuardExpr();
259         HashMap remap=new HashMap();
260         remap.put(dvd,uvd);
261
262         for(int i=0;i<negrule.size();i++) {
263             RuleConjunction rconj=negrule.get(i);
264             boolean good=true;
265             for(int j=0;j<rconj.size();j++) {
266                 DNFExpr dexpr=rconj.get(j);
267                 if (dexpr.getExpr() instanceof OpExpr) {
268                     OpExpr expr=(OpExpr)dexpr.getExpr();
269                     Expr lexpr=expr.getLeftExpr();
270                     Expr rexpr=expr.getRightExpr();
271
272                     boolean varok=true;
273                     Set vars=rexpr.freeVars();
274                     if (vars!=null) 
275                         for(Iterator it=vars.iterator();it.hasNext();) {
276                             VarDescriptor vd=(VarDescriptor) it.next();
277                             if (!vd.isGlobal()) {
278                                 /* VarDescriptor isn't a global */
279                                 if (dvd!=vd) {
280                                     varok=false;
281                                     break;
282                                 }
283                             }
284                         }
285                     
286                     if (!varok)
287                         continue;
288
289                     Opcode op=expr.getOpcode();
290                     op=Opcode.translateOpcode(dexpr.getNegation(),op);
291
292                     boolean match=false;
293                     for(int k=0;k<un.numUpdates();k++) {
294                         Updates update=un.getUpdate(k);
295                         if(update.isExpr()) {
296                             Set uvars=update.getRightExpr().freeVars();
297                             boolean freevarok=true;
298                             if (uvars!=null)
299                             for(Iterator it=uvars.iterator();it.hasNext();) {
300                                 VarDescriptor vd=(VarDescriptor) it.next();
301                                 if (!vd.isGlobal()) {
302                                     /* VarDescriptor isn't a global */
303                                     if (uvd!=vd) {
304                                         freevarok=false;
305                                         break;
306                                     }
307                                 }
308                             }
309                             if (!freevarok)
310                                 continue;
311
312                             Opcode op2=update.getOpcode();
313                             if ((op2==op)||
314                                 ((op2==Opcode.GT)&&(op==Opcode.GE))||
315                                 ((op2==Opcode.LT)&&(op==Opcode.LE))||
316                                 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
317                                 /* Operations match*/
318                                 if (lexpr.equals(remap,update.getLeftExpr())&&
319                                     rexpr.equals(remap,update.getRightExpr())) {
320                                     match=true;
321                                     break;
322                                 }                                   
323                             }
324                         } 
325                     }
326                     if (!match) {
327                         good=false;
328                         break;
329                     }
330                 } else {
331                     /* TODO: Check to see if there is an abstract repair */
332                     good=false;
333                     break; /* try next conjunction */
334                 }
335             }
336             if (good)
337                 return false;
338         }
339         return true;
340     }
341
342     /** This method checks whether the update effects only the
343      *  intended binding for the model definition rule. */
344
345     private boolean testdisjoint(Updates u, Rule r, Expr e) {
346         // find all exprs that may be be effected by update
347         Set exprs=e.useDescriptor(u.getDescriptor());
348         for(Iterator eit=exprs.iterator();eit.hasNext();) {
349             Expr e2=(Expr)eit.next();
350             if (testdisjointness(u,r,e2))
351                 return true;
352         }
353         return false;
354     }
355
356     /** This method tries to show that the modification only effects
357      * one binding of the model definition rule, and thus has no
358      * unintended side effects. */
359
360     private boolean testdisjointness(Updates u, Rule r, Expr e) {
361         // Note: rule of u must be r
362
363         Expr update_e=u.getLeftExpr();
364         HashSet quantifierset=new HashSet();
365
366         if (termination.analyzeQuantifiers(r,quantifierset))
367             return false; /* Can't accidentally interfere with other bindings if there aren't any! */
368
369         boolean firstfield=true;
370         
371
372         while(true) {
373             if (update_e instanceof CastExpr)
374                 update_e=((CastExpr)update_e).getExpr();
375             else if (e instanceof CastExpr)
376                 e=((CastExpr)e).getExpr();
377             else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
378                 DotExpr de1=(DotExpr)update_e;
379                 DotExpr de2=(DotExpr)e;
380                 if (de1.isValue(null)&&!firstfield)
381                     return true; /* Could have aliasing from this */
382                 if (de1.getField()!=de2.getField())
383                     return true; /* Different fields: not comparible */
384                 firstfield=false;
385
386                 Expr index1=de1.getIndex();
387                 Expr index2=de2.getIndex();
388                 if (index1!=null) {
389                     assert index2!=null;
390                     if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
391                         VarDescriptor vd1=((VarExpr)index1).getVar();
392                         VarDescriptor vd2=((VarExpr)index2).getVar();
393                         if ((vd1==vd2)&&!vd1.isGlobal()) {
394                             quantifierset.add(getQuantifier(r,vd1));
395                             if (termination.analyzeQuantifiers(r,quantifierset))
396                                 return false; /* State is disjoint from any other example */
397                         }
398                     }
399                 }
400                 update_e=de1.getExpr();
401                 e=de2.getExpr();
402             } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
403                 VarDescriptor vd1=((VarExpr)update_e).getVar();
404                 VarDescriptor vd2=((VarExpr)e).getVar();
405                 if ((vd1==vd2)&&!vd1.isGlobal()) {
406                     quantifierset.add(getQuantifier(r,vd1));
407                     if (termination.analyzeQuantifiers(r,quantifierset))
408                         return false; /* State is disjoint from any other example */
409                 }
410                 return true;
411             } else return true;
412         }
413     }
414
415     /** This method returns the quantifier that defines the quantifier
416      * variable vd. */
417     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
418         for (int i=0;i<qs.numQuantifiers();i++) {
419             Quantifier q=qs.getQuantifier(i);
420             if (q instanceof SetQuantifier) {
421                 SetQuantifier sq=(SetQuantifier)q;
422                 if (sq.getVar()==vd)
423                     return sq;
424             } else if (q instanceof RelationQuantifier) {
425                 RelationQuantifier rq=(RelationQuantifier)q;
426                 if ((rq.x==vd)||(rq.y==vd))
427                     return rq;
428             } else if (q instanceof ForQuantifier) {
429                 ForQuantifier fq=(ForQuantifier)q;
430                 if (fq.getVar()==vd)
431                     return fq;
432             }
433         }
434         return null;
435     }
436     
437     /** This function checks to see if an update is only performed if
438      * a given set (or image set produced by a relation) is empty, and
439      * the algorithm is computing whether the update may falsify a
440      * rule that adds something to the set */
441
442     private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
443         AbstractRepair ar=mun.getRepair();
444         if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
445             if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
446                 return true;
447             boolean negated=ar.getPredicate().isNegated();
448             Predicate p=ar.getPredicate().getPredicate();
449             if (!(p instanceof ExprPredicate))
450                 return true;
451             ExprPredicate ep=(ExprPredicate)p;
452             if (ep.getType()!=ExprPredicate.SIZE)
453                 return true;
454             Opcode op=Opcode.translateOpcode(negated,ep.getOp());
455    
456             if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
457                 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
458                 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
459                 ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
460                 return false;
461         } else if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTORELATION)) {
462             /* This test is for image sets of relations. */
463             if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
464                 return true;
465             boolean negated=ar.getPredicate().isNegated();
466             Predicate p=ar.getPredicate().getPredicate();
467             if (!(p instanceof ExprPredicate))
468                 return true;
469             ExprPredicate ep=(ExprPredicate)p;
470             if (ep.getType()!=ExprPredicate.SIZE)
471                 return true;
472
473             Opcode op=Opcode.translateOpcode(negated,ep.getOp());
474             if (!(((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
475                 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
476                 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
477                 ((op==Opcode.GE)&&(ep.rightSize()==1)))) //(>=1)
478                 return true;
479
480             RelationInclusion ri=(RelationInclusion)r.getInclusion();
481             Expr tmpve=ep.inverted()?ri.getRightExpr():ri.getLeftExpr();
482             if (!(tmpve instanceof VarExpr))
483                 return true;
484             for(int i=0;i<mun.numUpdates();i++) {
485                 UpdateNode un=mun.getUpdate(i);
486                 for (int j=0;j<un.numUpdates();j++) {
487                     Updates update=un.getUpdate(j);
488                     //Abstract updates don't have concrete interference1
489                     if (update.isAbstract()) 
490                         continue;
491                     if (testdisjoint(update, r, r.getGuardExpr()))
492                         return true;
493                 }
494             }
495             return false;
496         }
497         return true;
498     }
499
500     static private boolean interferes(Updates update, DNFExpr dexpr) {
501         Descriptor descriptor=update.getDescriptor();
502         /* If the DNFExpr expr doesn't use the updated descriptor,
503            there is no interference. */
504         if (!dexpr.getExpr().usesDescriptor(descriptor))
505             return false;
506             
507         if (update.isExpr()) {
508             /* We need to pair the variables */
509             Set vars=update.getRightExpr().freeVars();
510             Opcode op1=update.getOpcode();
511             Expr lexpr1=update.getLeftExpr();
512             Expr rexpr1=update.getRightExpr();
513             boolean good=true;
514             if (vars!=null)
515                 for(Iterator it=vars.iterator();it.hasNext();) {
516                     VarDescriptor vd=(VarDescriptor) it.next();
517                     /* VarDescriptor isn't a global */
518                     if (!vd.isGlobal()) {
519                         if (update.getVar()!=vd) {
520                             good=false;
521                             break;
522                         }
523                     }
524                 }
525             if (good&&(dexpr.getExpr() instanceof OpExpr)) {
526                 OpExpr expr=(OpExpr)dexpr.getExpr();
527                 Expr lexpr2=expr.getLeftExpr();
528                 Expr rexpr2=expr.getRightExpr();
529                 Opcode op2=expr.getOpcode();
530                 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
531
532                 VarDescriptor leftdescriptor=null;
533                 {
534                     Expr e=lexpr2;
535                     while(!(e instanceof VarExpr)) {
536                         for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
537                         if (e instanceof VarExpr)
538                             break;
539                         if (e instanceof CastExpr)
540                             e=((CastExpr)e).getExpr();
541                         else throw new Error("Bad Expr Type:"+e.name());
542                     }
543                     leftdescriptor=((VarExpr)e).getVar();
544                 }
545
546                 vars=rexpr2.freeVars();
547                 if (vars!=null)
548                     for(Iterator it=vars.iterator();it.hasNext();) {
549                         VarDescriptor vd=(VarDescriptor) it.next();
550                         if (!vd.isGlobal()) {
551                             /* VarDescriptor isn't a global */
552                             if (leftdescriptor!=vd) {
553                                 good=false;
554                                 break;
555                             }
556                         }
557                     }
558
559
560                 if (good) {
561                     HashMap remap=new HashMap();
562                     remap.put(update.getVar(),leftdescriptor);
563                     if ((op1==op2)&&
564                         lexpr1.equals(remap,lexpr2)&&
565                         rexpr1.equals(remap,rexpr2))
566                         return false;
567                 }
568             }
569         }
570         return true;
571     }
572 }