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
  12     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
  13         Descriptor updated_des=update.getDescriptor();
  14         Inclusion inclusion=r.getInclusion();
  15         if (inclusion instanceof RelationInclusion) {
  16             RelationInclusion ri=(RelationInclusion)inclusion;
  17             if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
  18                 return true;
  19             if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
  20                 return true;
  21         } else if (inclusion instanceof SetInclusion) {
  22             SetInclusion si=(SetInclusion)inclusion;
  23             if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
  24                 return true;
  25         } else throw new Error();
  26         return false;
  27     }
  28
  29     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
  30         Descriptor updated_des=update.getDescriptor();
  31         if (updated_des instanceof FieldDescriptor) {
  32             /* Build variable correspondance */
  33             HashSet set=new HashSet();
  34             inclusionexpr.findmatch(updated_des,set);
  35
  36             for(Iterator matchit=set.iterator();matchit.hasNext();) {
  37                 DotExpr dotexpr=(DotExpr)matchit.next();
  38                 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
  39                 while(true) {
  40                     if (dotexpr.getField()!=updateexpr.getField())
  41                         return true;
  42                     Expr de=dotexpr.getExpr();
  43                     Expr ue=updateexpr.getExpr();
  44                     if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
  45                         dotexpr=(DotExpr)de;
  46                         updateexpr=(DotExpr)ue;
  47                     } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
  48                         VarDescriptor dvd=((VarExpr)de).getVar();
  49                         VarDescriptor uvd=((VarExpr)ue).getVar();
  50                         if (interferesinclusion(un,r,dvd,uvd))
  51                             return true;
  52                         else
  53                             break;
  54                     } else
  55                         return true;
  56                 }
  57             }
  58         } else if (updated_des instanceof VarDescriptor) {
  59             /* We have a VarDescriptor - no correspondance necessary */
  60             VarDescriptor vd=(VarDescriptor)updated_des;
  61             if (interferesinclusion(un,r,vd,vd))
  62                 return true;
  63         } else throw new Error();
  64         return false;
  65     }
  66
  67     static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
  68         DNFRule negrule=r.getDNFNegGuardExpr();
  69         HashMap remap=new HashMap();
  70         remap.put(dvd,uvd);
  71
  72         for(int i=0;i<negrule.size();i++) {
  73             RuleConjunction rconj=negrule.get(i);
  74             boolean good=true;
  75             for(int j=0;j<rconj.size();j++) {
  76                 DNFExpr dexpr=rconj.get(j);
  77                 if (dexpr.getExpr() instanceof OpExpr) {
  78                     OpExpr expr=(OpExpr)dexpr.getExpr();
  79                     Expr lexpr=expr.getLeftExpr();
  80                     Expr rexpr=expr.getRightExpr();
  81
  82                     boolean varok=true;
  83                     Set vars=rexpr.freeVars();
  84                     if (vars!=null)
  85                         for(Iterator it=vars.iterator();it.hasNext();) {
  86                             VarDescriptor vd=(VarDescriptor) it.next();
  87                             if (!vd.isGlobal()) {
  88                                 /* VarDescriptor isn't a global */
  89                                 if (dvd!=vd) {
  90                                     varok=false;
  91                                     break;
  92                                 }
  93                             }
  94                         }
  95
  96                     if (!varok)
  97                         continue;
  98
  99
 100
 101                     Opcode op=expr.getOpcode();
 102                     op=Opcode.translateOpcode(dexpr.getNegation(),op);
 103
 104                     boolean match=false;
 105                     for(int k=0;k<un.numUpdates();k++) {
 106                         Updates update=un.getUpdate(k);
 107                         if(update.isExpr()) {
 108                             Set uvars=update.getRightExpr().freeVars();
 109                             boolean freevarok=true;
 110                             if (uvars!=null)
 111                             for(Iterator it=uvars.iterator();it.hasNext();) {
 112                                 VarDescriptor vd=(VarDescriptor) it.next();
 113                                 if (!vd.isGlobal()) {
 114                                     /* VarDescriptor isn't a global */
 115                                     if (uvd!=vd) {
 116                                         freevarok=false;
 117                                         break;
 118                                     }
 119                                 }
 120                             }
 121                             if (!freevarok)
 122                                 continue;
 123
 124                             Opcode op2=update.getOpcode();
 125                             if ((op2==op)||
 126                                 ((op2==Opcode.GT)&&(op==Opcode.GE))||
 127                                 ((op2==Opcode.LT)&&(op==Opcode.LE))||
 128                                 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
 129                                 /* Operations match*/
 130                                 if (lexpr.equals(remap,update.getLeftExpr())&&
 131                                     rexpr.equals(remap,update.getRightExpr())) {
 132                                     match=true;
 133                                     break;
 134                                 }
 135                             }
 136                         }
 137                     }
 138                     if (!match) {
 139                         good=false;
 140                         break;
 141                     }
 142                 } else {
 143                     /* TODO: Check to see if there is an abstract repair */
 144                     good=false;
 145                     break; /* try next conjunction */
 146                 }
 147             }
 148             if (good)
 149                 return false;
 150         }
 151         return true;
 152     }
 153
 154     /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
 155      * the scope of the model definition rule r. */
 156
 157     public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 158         if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
 159             return false;
 160         for(int i=0;i<mun.numUpdates();i++) {
 161             UpdateNode un=mun.getUpdate(i);
 162             for (int j=0;j<un.numUpdates();j++) {
 163                 Updates update=un.getUpdate(j);
 164
 165                 DNFRule drule=r.getDNFGuardExpr();
 166                 if (satisfy)
 167                     drule=r.getDNFNegGuardExpr();
 168
 169
 170                 if (!update.isAbstract()) {
 171                     Descriptor updated_des=update.getDescriptor();
 172                     assert updated_des!=null;
 173                     /* Update is local to this rule, and the effect is intentional */
 174                     /* If we're adding something, a side effect could be to falsify some other binding
 175                        If we're removing something, there is no similar side effect */
 176
 177                     /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
 178                     if (r.getInclusion().usesDescriptor(updated_des)) {
 179                         boolean ok=false;
 180                         if ((un.getRule()==r)&&
 181                             (((mun.op==MultUpdateNode.ADD)&&satisfy)
 182                              ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
 183                              ||(mun.op==MultUpdateNode.MODIFY))) {
 184                             Inclusion inclusion=r.getInclusion();
 185                             if (inclusion instanceof RelationInclusion) {
 186                                 RelationInclusion ri=(RelationInclusion)inclusion;
 187                                 if ((!interferes(update,r,ri.getLeftExpr()))&&
 188                                     (!interferes(update,r,ri.getRightExpr())))
 189                                     ok=true;
 190                             } else if (inclusion instanceof SetInclusion) {
 191                                 SetInclusion si=(SetInclusion)inclusion;
 192                                 if (!interferes(update,r,si.getExpr()))
 193                                     ok=true;
 194                             } else throw new Error();
 195                         }
 196                         if (!ok) {
 197                             if (satisfy) {
 198                                 if (interferesinclusion(un, update, r))
 199                                     return true;
 200                             } else
 201                                 return true; /* Interferes with inclusion condition */
 202                         }
 203                     }
 204
 205                     for(int k=0;k<drule.size();k++) {
 206                         RuleConjunction rconj=drule.get(k);
 207                         for(int l=0;l<rconj.size();l++) {
 208                             DNFExpr dexpr=rconj.get(l);
 209                             /* See if update interferes w/ dexpr */
 210                             if ((un.getRule()==r)&&
 211                                 (((mun.op==MultUpdateNode.ADD)&&satisfy)
 212                                  ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
 213                                  ||(mun.op==MultUpdateNode.MODIFY))) {
 214                                 if (!interferes(update,r,dexpr.getExpr()))
 215                                     continue; /* unique state - we're okay */
 216                             }
 217                             if (interferes(un,update, r,dexpr))
 218                                 return true;
 219                         }
 220                     }
 221                 }
 222             }
 223         }
 224         return false;
 225     }
 226
 227     private boolean interferes(Updates u, Rule r, Expr e) {
 228         Set exprs=e.useDescriptor(u.getDescriptor());
 229         for(Iterator eit=exprs.iterator();eit.hasNext();) {
 230             Expr e2=(Expr)eit.next();
 231             if (mayinterfere(u,r,e2))
 232                 return true;
 233         }
 234         return false;
 235     }
 236
 237     private boolean mayinterfere(Updates u, Rule r, Expr e) {
 238         // Note: rule of u must be r
 239
 240         Expr update_e=u.getLeftExpr();
 241         HashSet quantifierset=new HashSet();
 242
 243         if (termination.analyzeQuantifiers(r,quantifierset))
 244             return false; /* Can't accidentally interfere with other bindings if there aren't any! */
 245
 246         boolean firstfield=true;
 247         while(true) {
 248             if (update_e instanceof CastExpr)
 249                 update_e=((CastExpr)update_e).getExpr();
 250             else if (e instanceof CastExpr)
 251                 e=((CastExpr)e).getExpr();
 252             else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
 253                 DotExpr de1=(DotExpr)update_e;
 254                 DotExpr de2=(DotExpr)e;
 255                 if (de1.isValue(null)&&!firstfield)
 256                     return true; /* Could have aliasing from this */
 257                 if (de1.getField()!=de2.getField())
 258                     return true; /* Different fields: not comparible */
 259                 firstfield=false;
 260
 261                 Expr index1=de1.getIndex();
 262                 Expr index2=de2.getIndex();
 263                 if (index1!=null) {
 264                     assert index2!=null;
 265                     if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
 266                         VarDescriptor vd1=((VarExpr)index1).getVar();
 267                         VarDescriptor vd2=((VarExpr)index2).getVar();
 268                         if ((vd1==vd2)&&!vd1.isGlobal()) {
 269                             quantifierset.add(getQuantifier(r,vd1));
 270                             if (termination.analyzeQuantifiers(r,quantifierset))
 271                                 return false; /* State is disjoint from any other example */
 272                         }
 273                     }
 274                 }
 275                 update_e=de1.getExpr();
 276                 e=de2.getExpr();
 277             } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
 278                 VarDescriptor vd1=((VarExpr)update_e).getVar();
 279                 VarDescriptor vd2=((VarExpr)e).getVar();
 280                 if ((vd1==vd2)&&!vd1.isGlobal()) {
 281                     quantifierset.add(getQuantifier(r,vd1));
 282                     if (termination.analyzeQuantifiers(r,quantifierset))
 283                         return false; /* State is disjoint from any other example */
 284                 }
 285                 return true;
 286             } else return true;
 287         }
 288
 289     }
 290
 291     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
 292         for (int i=0;i<qs.numQuantifiers();i++) {
 293             Quantifier q=qs.getQuantifier(i);
 294             if (q instanceof SetQuantifier) {
 295                 SetQuantifier sq=(SetQuantifier)q;
 296                 if (sq.getVar()==vd)
 297                     return sq;
 298             } else if (q instanceof RelationQuantifier) {
 299                 RelationQuantifier rq=(RelationQuantifier)q;
 300                 if ((rq.x==vd)||(rq.y==vd))
 301                     return rq;
 302             } else if (q instanceof ForQuantifier) {
 303                 ForQuantifier fq=(ForQuantifier)q;
 304                 if (fq.getVar()==vd)
 305                     return fq;
 306             }
 307         }
 308         return null;
 309     }
 310
 311     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 312         AbstractRepair ar=mun.getRepair();
 313         if (satisfy)
 314             return true;
 315         if (ar==null)
 316             return true;
 317         if (ar.getType()!=AbstractRepair.ADDTOSET)
 318             return true;
 319         //      if (mun.op!=MultUpdateNode.ADD)  (Redundant)
 320         //    return true;
 321         if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
 322             return true;
 323         boolean negated=ar.getPredicate().isNegated();
 324         Predicate p=ar.getPredicate().getPredicate();
 325         if (!(p instanceof ExprPredicate))
 326             return true;
 327         ExprPredicate ep=(ExprPredicate)p;
 328         if (ep.getType()!=ExprPredicate.SIZE)
 329             return true;
 330         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
 331             return false;
 332         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
 333             return false;
 334
 335         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
 336             return false;
 337         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
 338             return false;
 339
 340
 341
 342         if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
 343             return false;
 344         if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
 345             return false;
 346
 347         if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
 348             return false;
 349         if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
 350             return false;
 351
 352         return true;
 353
 354
 355     }
 356
 357     static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
 358         Descriptor descriptor=update.getDescriptor();
 359         if (!dexpr.getExpr().usesDescriptor(descriptor))
 360             return false;
 361
 362         /* We need to pair the variables */
 363         if (update.isExpr()) {
 364             Set vars=update.getRightExpr().freeVars();
 365             Opcode op1=update.getOpcode();
 366             Expr lexpr1=update.getLeftExpr();
 367             Expr rexpr1=update.getRightExpr();
 368             boolean good=true;
 369             if (vars!=null)
 370                 for(Iterator it=vars.iterator();it.hasNext();) {
 371                     VarDescriptor vd=(VarDescriptor) it.next();
 372                     if (!vd.isGlobal()) {
 373                         /* VarDescriptor isn't a global */
 374                         if (update.getVar()!=vd) {
 375                             good=false;
 376                             break;
 377                         }
 378                     }
 379                 }
 380             if (good&&(dexpr.getExpr() instanceof OpExpr)) {
 381                 OpExpr expr=(OpExpr)dexpr.getExpr();
 382                 Expr lexpr2=expr.getLeftExpr();
 383                 Expr rexpr2=expr.getRightExpr();
 384                 Opcode op2=expr.getOpcode();
 385                 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 386
 387                 good=true;
 388                 vars=rexpr2.freeVars();
 389                 VarDescriptor leftdescriptor=null;
 390                 if (lexpr2 instanceof VarExpr)
 391                     leftdescriptor=((VarExpr)lexpr2).getVar();
 392                 else if (lexpr2 instanceof DotExpr) {
 393                     Expr e=lexpr2;
 394                     do {
 395                         for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
 396                         if (e instanceof VarExpr)
 397                             break;
 398                         if (e instanceof CastExpr)
 399                             e=((CastExpr)e).getExpr();
 400                         else throw new Error("Bad Expr Type:"+e.name());
 401                     } while (true);
 402                     leftdescriptor=((VarExpr)e).getVar();
 403                 } else throw new Error("Bad Expr");
 404
 405                 if (vars!=null)
 406                     for(Iterator it=vars.iterator();it.hasNext();) {
 407                         VarDescriptor vd=(VarDescriptor) it.next();
 408                         if (!vd.isGlobal()) {
 409                             /* VarDescriptor isn't a global */
 410                             if (leftdescriptor!=vd) {
 411                                 good=false;
 412                                 break;
 413                             }
 414                         }
 415                     }
 416                 if (good) {
 417                     HashMap remap=new HashMap();
 418                     remap.put(update.getVar(),leftdescriptor);
 419                     if ((op1==op2)&&
 420                         lexpr1.equals(remap,lexpr2)&&
 421                         rexpr1.equals(remap,rexpr2))
 422                         return false;
 423                 }
 424             }
 425         }
 426         return true;
 427     }
 428 }