Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java

   1 package MCC.IR;
   2 import java.util.*;
   3
   4 class ConcreteInterferes {
   5
   6     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
   7         Descriptor updated_des=update.getDescriptor();
   8         Inclusion inclusion=r.getInclusion();
   9         if (inclusion instanceof RelationInclusion) {
  10             RelationInclusion ri=(RelationInclusion)inclusion;
  11             if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
  12                 return true;
  13             if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
  14                 return true;
  15         } else if (inclusion instanceof SetInclusion) {
  16             SetInclusion si=(SetInclusion)inclusion;
  17             if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
  18                 return true;
  19         } else throw new Error();
  20         return false;
  21     }
  22
  23     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
  24         Descriptor updated_des=update.getDescriptor();
  25         if (updated_des instanceof FieldDescriptor) {
  26             /* Build variable correspondance */
  27             HashSet set=new HashSet();
  28             inclusionexpr.findmatch(updated_des,set);
  29
  30             for(Iterator matchit=set.iterator();matchit.hasNext();) {
  31                 DotExpr dotexpr=(DotExpr)matchit.next();
  32                 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
  33                 while(true) {
  34                     if (dotexpr.getField()!=updateexpr.getField())
  35                         return true;
  36                     Expr de=dotexpr.getExpr();
  37                     Expr ue=updateexpr.getExpr();
  38                     if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
  39                         dotexpr=(DotExpr)de;
  40                         updateexpr=(DotExpr)ue;
  41                     } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
  42                         VarDescriptor dvd=((VarExpr)de).getVar();
  43                         VarDescriptor uvd=((VarExpr)ue).getVar();
  44                         if (interferesinclusion(un,r,dvd,uvd))
  45                             return true;
  46                         else
  47                             break;
  48                     } else
  49                         return true;
  50                 }
  51             }
  52         } else if (updated_des instanceof VarDescriptor) {
  53             /* We have a VarDescriptor - no correspondance necessary */
  54             VarDescriptor vd=(VarDescriptor)updated_des;
  55             if (interferesinclusion(un,r,vd,vd))
  56                 return true;
  57         } else throw new Error();
  58         return false;
  59     }
  60
  61     static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
  62         DNFRule negrule=r.getDNFNegGuardExpr();
  63         HashMap remap=new HashMap();
  64         remap.put(dvd,uvd);
  65
  66         for(int i=0;i<negrule.size();i++) {
  67             RuleConjunction rconj=negrule.get(i);
  68             boolean good=true;
  69             for(int j=0;j<rconj.size();j++) {
  70                 DNFExpr dexpr=rconj.get(j);
  71                 if (dexpr.getExpr() instanceof OpExpr) {
  72                     OpExpr expr=(OpExpr)dexpr.getExpr();
  73                     Expr lexpr=expr.getLeftExpr();
  74                     Expr rexpr=expr.getRightExpr();
  75
  76                     boolean varok=true;
  77                     Set vars=rexpr.freeVars();
  78                     if (vars!=null)
  79                         for(Iterator it=vars.iterator();it.hasNext();) {
  80                             VarDescriptor vd=(VarDescriptor) it.next();
  81                             if (!vd.isGlobal()) {
  82                                 /* VarDescriptor isn't a global */
  83                                 if (dvd!=vd) {
  84                                     varok=false;
  85                                     break;
  86                                 }
  87                             }
  88                         }
  89
  90                     if (!varok)
  91                         continue;
  92
  93
  94
  95                     Opcode op=expr.getOpcode();
  96
  97                     if (dexpr.getNegation()) {
  98                         /* remove negation through opcode translation */
  99                         if (op==Opcode.GT)
 100                             op=Opcode.LE;
 101                         else if (op==Opcode.GE)
 102                             op=Opcode.LT;
 103                         else if (op==Opcode.EQ)
 104                             op=Opcode.NE;
 105                         else if (op==Opcode.NE)
 106                             op=Opcode.EQ;
 107                         else if (op==Opcode.LT)
 108                             op=Opcode.GE;
 109                         else if (op==Opcode.LE)
 110                             op=Opcode.GT;
 111                     }
 112                     boolean match=false;
 113                     for(int k=0;k<un.numUpdates();k++) {
 114                         Updates update=un.getUpdate(k);
 115                         if(update.isExpr()) {
 116                             Set uvars=update.getRightExpr().freeVars();
 117                             boolean freevarok=true;
 118                             if (uvars!=null)
 119                             for(Iterator it=uvars.iterator();it.hasNext();) {
 120                                 VarDescriptor vd=(VarDescriptor) it.next();
 121                                 if (!vd.isGlobal()) {
 122                                     /* VarDescriptor isn't a global */
 123                                     if (uvd!=vd) {
 124                                         freevarok=false;
 125                                         break;
 126                                     }
 127                                 }
 128                             }
 129                             if (!freevarok)
 130                                 continue;
 131
 132                             Opcode op2=update.getOpcode();
 133                             if ((op2==op)||
 134                                 ((op2==Opcode.GT)&&(op==Opcode.GE))||
 135                                 ((op2==Opcode.LT)&&(op==Opcode.LE))||
 136                                 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
 137                                 /* Operations match*/
 138                                 if (lexpr.equals(remap,update.getLeftExpr())&&
 139                                     rexpr.equals(remap,update.getRightExpr())) {
 140                                     match=true;
 141                                     break;
 142                                 }
 143                             }
 144                         }
 145                     }
 146                     if (!match) {
 147                         good=false;
 148                         break;
 149                     }
 150                 } else {
 151                     /* TODO: Check to see if there is an abstract repair */
 152                     good=false;
 153                     break; /* try next conjunction */
 154                 }
 155             }
 156             if (good)
 157                 return false;
 158         }
 159         return true;
 160     }
 161
 162     /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
 163      * the scope of the model definition rule r. */
 164
 165     static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 166         if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
 167             return false;
 168         for(int i=0;i<mun.numUpdates();i++) {
 169             UpdateNode un=mun.getUpdate(i);
 170             for (int j=0;j<un.numUpdates();j++) {
 171                 Updates update=un.getUpdate(j);
 172
 173                 DNFRule drule=r.getDNFGuardExpr();
 174                 if (satisfy)
 175                     drule=r.getDNFNegGuardExpr();
 176
 177
 178                 if (!update.isAbstract()) {
 179                     Descriptor updated_des=update.getDescriptor();
 180                     assert updated_des!=null;
 181                     /* Update is local to this rule, and the effect is intentional */
 182                     /* If we're adding something, a side effect could be to falsify some other binding
 183                        If we're removing something, there is no similar side effect */
 184
 185                     /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
 186                     if ((un.getRule()==r)&&
 187                         (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
 188                         (r.numQuantifiers()==1)&&
 189                         (r.getQuantifier(0) instanceof SetQuantifier)&&
 190                         update.isField()&&
 191                         (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
 192                         ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
 193                         continue;
 194
 195                     if ((un.getRule()==r)&&
 196                         (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
 197                         (r.numQuantifiers()==0))
 198                         continue;
 199
 200
 201                     if (r.getInclusion().usesDescriptor(updated_des)) {
 202                         if (satisfy) {
 203                             if (interferesinclusion(un, update, r))
 204                             return true;
 205                         } else
 206                             return true; /* Interferes with inclusion condition */
 207                     }
 208
 209                     for(int k=0;k<drule.size();k++) {
 210                         RuleConjunction rconj=drule.get(k);
 211                         for(int l=0;l<rconj.size();l++) {
 212
 213
 214                             DNFExpr dexpr=rconj.get(l);
 215                             /* See if update interferes w/ dexpr */
 216                             if (interferes(un,update, r,dexpr))
 217                                 return true;
 218                         }
 219                     }
 220                 }
 221             }
 222         }
 223         return false;
 224     }
 225
 226     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 227         AbstractRepair ar=mun.getRepair();
 228         if (satisfy)
 229             return true;
 230         if (ar==null)
 231             return true;
 232         if (ar.getType()!=AbstractRepair.ADDTOSET)
 233             return true;
 234         //      if (mun.op!=MultUpdateNode.ADD)  (Redundant)
 235         //    return true;
 236         if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
 237             return true;
 238         boolean negated=ar.getPredicate().isNegated();
 239         Predicate p=ar.getPredicate().getPredicate();
 240         if (!(p instanceof ExprPredicate))
 241             return true;
 242         ExprPredicate ep=(ExprPredicate)p;
 243         if (ep.getType()!=ExprPredicate.SIZE)
 244             return true;
 245         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
 246             return false;
 247         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
 248             return false;
 249
 250         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
 251             return false;
 252         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
 253             return false;
 254
 255
 256
 257         if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
 258             return false;
 259         if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
 260             return false;
 261
 262         if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
 263             return false;
 264         if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
 265             return false;
 266
 267         return true;
 268
 269
 270     }
 271
 272     static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
 273         Descriptor descriptor=update.getDescriptor();
 274         if (!dexpr.getExpr().usesDescriptor(descriptor))
 275             return false;
 276
 277         /* We need to pair the variables */
 278         if (update.isExpr()) {
 279             Set vars=update.getRightExpr().freeVars();
 280             Opcode op1=update.getOpcode();
 281             Expr lexpr1=update.getLeftExpr();
 282             Expr rexpr1=update.getRightExpr();
 283             boolean good=true;
 284             if (vars!=null)
 285                 for(Iterator it=vars.iterator();it.hasNext();) {
 286                     VarDescriptor vd=(VarDescriptor) it.next();
 287                     if (!vd.isGlobal()) {
 288                         /* VarDescriptor isn't a global */
 289                         if (update.getVar()!=vd) {
 290                             good=false;
 291                             break;
 292                         }
 293                     }
 294                 }
 295             if (good&&(dexpr.getExpr() instanceof OpExpr)) {
 296                 OpExpr expr=(OpExpr)dexpr.getExpr();
 297                 Expr lexpr2=expr.getLeftExpr();
 298                 Expr rexpr2=expr.getRightExpr();
 299                 Opcode op2=expr.getOpcode();
 300                 if (dexpr.getNegation()) {
 301                     /* remove negation through opcode translation */
 302                     if (op2==Opcode.GT)
 303                         op2=Opcode.LE;
 304                     else if (op2==Opcode.GE)
 305                         op2=Opcode.LT;
 306                     else if (op2==Opcode.EQ)
 307                         op2=Opcode.NE;
 308                     else if (op2==Opcode.NE)
 309                         op2=Opcode.EQ;
 310                     else if (op2==Opcode.LT)
 311                         op2=Opcode.GE;
 312                     else if (op2==Opcode.LE)
 313                         op2=Opcode.GT;
 314                 }
 315                 good=true;
 316                 vars=rexpr2.freeVars();
 317                 VarDescriptor leftdescriptor=null;
 318                 if (lexpr2 instanceof VarExpr)
 319                     leftdescriptor=((VarExpr)lexpr2).getVar();
 320                 else if (lexpr2 instanceof DotExpr) {
 321                     Expr e=lexpr2;
 322                     for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
 323                     leftdescriptor=((VarExpr)e).getVar();
 324                 } else throw new Error("Bad Expr");
 325
 326                 if (vars!=null)
 327                     for(Iterator it=vars.iterator();it.hasNext();) {
 328                         VarDescriptor vd=(VarDescriptor) it.next();
 329                         if (!vd.isGlobal()) {
 330                             /* VarDescriptor isn't a global */
 331                             if (leftdescriptor!=vd) {
 332                                 good=false;
 333                                 break;
 334                             }
 335                         }
 336                     }
 337                 if (good) {
 338                     HashMap remap=new HashMap();
 339                     remap.put(update.getVar(),leftdescriptor);
 340                     if ((op1==op2)&&
 341                         lexpr1.equals(remap,lexpr2)&&
 342                         rexpr1.equals(remap,rexpr2))
 343                         return false;
 344                 }
 345             }
 346         }
 347         return true;
 348     }
 349 }