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