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                     op=Opcode.translateOpcode(dexpr.getNegation(),op);
  97
  98                     boolean match=false;
  99                     for(int k=0;k<un.numUpdates();k++) {
 100                         Updates update=un.getUpdate(k);
 101                         if(update.isExpr()) {
 102                             Set uvars=update.getRightExpr().freeVars();
 103                             boolean freevarok=true;
 104                             if (uvars!=null)
 105                             for(Iterator it=uvars.iterator();it.hasNext();) {
 106                                 VarDescriptor vd=(VarDescriptor) it.next();
 107                                 if (!vd.isGlobal()) {
 108                                     /* VarDescriptor isn't a global */
 109                                     if (uvd!=vd) {
 110                                         freevarok=false;
 111                                         break;
 112                                     }
 113                                 }
 114                             }
 115                             if (!freevarok)
 116                                 continue;
 117
 118                             Opcode op2=update.getOpcode();
 119                             if ((op2==op)||
 120                                 ((op2==Opcode.GT)&&(op==Opcode.GE))||
 121                                 ((op2==Opcode.LT)&&(op==Opcode.LE))||
 122                                 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
 123                                 /* Operations match*/
 124                                 if (lexpr.equals(remap,update.getLeftExpr())&&
 125                                     rexpr.equals(remap,update.getRightExpr())) {
 126                                     match=true;
 127                                     break;
 128                                 }
 129                             }
 130                         }
 131                     }
 132                     if (!match) {
 133                         good=false;
 134                         break;
 135                     }
 136                 } else {
 137                     /* TODO: Check to see if there is an abstract repair */
 138                     good=false;
 139                     break; /* try next conjunction */
 140                 }
 141             }
 142             if (good)
 143                 return false;
 144         }
 145         return true;
 146     }
 147
 148     /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
 149      * the scope of the model definition rule r. */
 150
 151     static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 152         if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
 153             return false;
 154         for(int i=0;i<mun.numUpdates();i++) {
 155             UpdateNode un=mun.getUpdate(i);
 156             for (int j=0;j<un.numUpdates();j++) {
 157                 Updates update=un.getUpdate(j);
 158
 159                 DNFRule drule=r.getDNFGuardExpr();
 160                 if (satisfy)
 161                     drule=r.getDNFNegGuardExpr();
 162
 163
 164                 if (!update.isAbstract()) {
 165                     Descriptor updated_des=update.getDescriptor();
 166                     assert updated_des!=null;
 167                     /* Update is local to this rule, and the effect is intentional */
 168                     /* If we're adding something, a side effect could be to falsify some other binding
 169                        If we're removing something, there is no similar side effect */
 170
 171                     /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
 172                     if ((un.getRule()==r)&&
 173                         (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
 174                         (r.numQuantifiers()==1)&&
 175                         (r.getQuantifier(0) instanceof SetQuantifier)&&
 176                         update.isField()&&
 177                         (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
 178                         ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
 179                         continue;
 180
 181                     if ((un.getRule()==r)&&
 182                         (((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
 183                         (r.numQuantifiers()==0))
 184                         continue;
 185
 186
 187                     if (r.getInclusion().usesDescriptor(updated_des)) {
 188                         if (satisfy) {
 189                             if (interferesinclusion(un, update, r))
 190                             return true;
 191                         } else
 192                             return true; /* Interferes with inclusion condition */
 193                     }
 194
 195                     for(int k=0;k<drule.size();k++) {
 196                         RuleConjunction rconj=drule.get(k);
 197                         for(int l=0;l<rconj.size();l++) {
 198
 199
 200                             DNFExpr dexpr=rconj.get(l);
 201                             /* See if update interferes w/ dexpr */
 202                             if (interferes(un,update, r,dexpr))
 203                                 return true;
 204                         }
 205                     }
 206                 }
 207             }
 208         }
 209         return false;
 210     }
 211
 212     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 213         AbstractRepair ar=mun.getRepair();
 214         if (satisfy)
 215             return true;
 216         if (ar==null)
 217             return true;
 218         if (ar.getType()!=AbstractRepair.ADDTOSET)
 219             return true;
 220         //      if (mun.op!=MultUpdateNode.ADD)  (Redundant)
 221         //    return true;
 222         if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
 223             return true;
 224         boolean negated=ar.getPredicate().isNegated();
 225         Predicate p=ar.getPredicate().getPredicate();
 226         if (!(p instanceof ExprPredicate))
 227             return true;
 228         ExprPredicate ep=(ExprPredicate)p;
 229         if (ep.getType()!=ExprPredicate.SIZE)
 230             return true;
 231         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
 232             return false;
 233         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
 234             return false;
 235
 236         if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
 237             return false;
 238         if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
 239             return false;
 240
 241
 242
 243         if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
 244             return false;
 245         if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
 246             return false;
 247
 248         if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
 249             return false;
 250         if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
 251             return false;
 252
 253         return true;
 254
 255
 256     }
 257
 258     static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
 259         Descriptor descriptor=update.getDescriptor();
 260         if (!dexpr.getExpr().usesDescriptor(descriptor))
 261             return false;
 262
 263         /* We need to pair the variables */
 264         if (update.isExpr()) {
 265             Set vars=update.getRightExpr().freeVars();
 266             Opcode op1=update.getOpcode();
 267             Expr lexpr1=update.getLeftExpr();
 268             Expr rexpr1=update.getRightExpr();
 269             boolean good=true;
 270             if (vars!=null)
 271                 for(Iterator it=vars.iterator();it.hasNext();) {
 272                     VarDescriptor vd=(VarDescriptor) it.next();
 273                     if (!vd.isGlobal()) {
 274                         /* VarDescriptor isn't a global */
 275                         if (update.getVar()!=vd) {
 276                             good=false;
 277                             break;
 278                         }
 279                     }
 280                 }
 281             if (good&&(dexpr.getExpr() instanceof OpExpr)) {
 282                 OpExpr expr=(OpExpr)dexpr.getExpr();
 283                 Expr lexpr2=expr.getLeftExpr();
 284                 Expr rexpr2=expr.getRightExpr();
 285                 Opcode op2=expr.getOpcode();
 286                 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 287
 288                 good=true;
 289                 vars=rexpr2.freeVars();
 290                 VarDescriptor leftdescriptor=null;
 291                 if (lexpr2 instanceof VarExpr)
 292                     leftdescriptor=((VarExpr)lexpr2).getVar();
 293                 else if (lexpr2 instanceof DotExpr) {
 294                     Expr e=lexpr2;
 295                     do {
 296                         for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
 297                         if (e instanceof VarExpr)
 298                             break;
 299                         if (e instanceof CastExpr)
 300                             e=((CastExpr)e).getExpr();
 301                         else throw new Error("Bad Expr Type:"+e.name());
 302                     } while (true);
 303                     leftdescriptor=((VarExpr)e).getVar();
 304                 } else throw new Error("Bad Expr");
 305
 306                 if (vars!=null)
 307                     for(Iterator it=vars.iterator();it.hasNext();) {
 308                         VarDescriptor vd=(VarDescriptor) it.next();
 309                         if (!vd.isGlobal()) {
 310                             /* VarDescriptor isn't a global */
 311                             if (leftdescriptor!=vd) {
 312                                 good=false;
 313                                 break;
 314                             }
 315                         }
 316                     }
 317                 if (good) {
 318                     HashMap remap=new HashMap();
 319                     remap.put(update.getVar(),leftdescriptor);
 320                     if ((op1==op2)&&
 321                         lexpr1.equals(remap,lexpr2)&&
 322                         rexpr1.equals(remap,rexpr2))
 323                         return false;
 324                 }
 325             }
 326         }
 327         return true;
 328     }
 329 }