Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

   1 package MCC.IR;
   2
   3 class AbstractInterferes {
   4     static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
   5         boolean mayadd=false;
   6         boolean mayremove=false;
   7         switch (ar.getType()) {
   8         case AbstractRepair.ADDTOSET:
   9         case AbstractRepair.ADDTORELATION:
  10             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  11                 return true;
  12             mayadd=true;
  13             break;
  14         case AbstractRepair.REMOVEFROMSET:
  15         case AbstractRepair.REMOVEFROMRELATION:
  16             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  17                 return true;
  18             mayremove=true;
  19             break;
  20         case AbstractRepair.MODIFYRELATION:
  21             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  22                 return true;
  23             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  24                 return true;
  25             mayadd=true;
  26             mayremove=true;
  27         break;
  28         default:
  29             throw new Error("Unrecognized Abstract Repair");
  30         }
  31         DNFRule drule=null;
  32         if (satisfy)
  33             drule=r.getDNFGuardExpr();
  34         else
  35             drule=r.getDNFNegGuardExpr();
  36
  37         for(int i=0;i<drule.size();i++) {
  38             RuleConjunction rconj=drule.get(i);
  39             for(int j=0;j<rconj.size();j++) {
  40                 DNFExpr dexpr=rconj.get(j);
  41                 Expr expr=dexpr.getExpr();
  42                 if (expr.usesDescriptor(ar.getDescriptor())) {
  43                     /* Need to check */
  44                     if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
  45                         return true;
  46                 }
  47             }
  48         }
  49         return false;
  50     }
  51
  52
  53     static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
  54         if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
  55             ((ar.getDescriptor() instanceof SetDescriptor)||
  56              !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
  57             return false;
  58
  59         /* This if handles all the c comparisons in the paper */
  60         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
  61             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
  62             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
  63             (dp.getPredicate() instanceof ExprPredicate)&&
  64             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
  65             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
  66             boolean neg1=ar.getPredicate().isNegated();
  67             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
  68             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
  69             boolean neg2=dp.isNegated();
  70             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
  71             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
  72             if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
  73                 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
  74                 int size1a=0;
  75                 if (!neg1) {
  76                     if((op1==Opcode.EQ)||(op1==Opcode.GE))
  77                         size1a=size1;
  78                     if((op1==Opcode.GT)||(op1==Opcode.NE))
  79                         size1a=size1+1;
  80                 }
  81                 if (neg1) {
  82                     if((op1==Opcode.EQ)||(op1==Opcode.LE))
  83                         size1a=size1+1;
  84                     if((op1==Opcode.LT)||(op1==Opcode.NE))
  85                         size1a=size1;
  86                 }
  87                 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
  88                     (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
  89                     (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
  90                     (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
  91                     (!neg2&&(op2==Opcode.GE))||
  92                     (!neg2&&(op2==Opcode.GT))||
  93                     (neg2&&(op2==Opcode.LE))||
  94                     (neg2&&(op2==Opcode.LT))||
  95                     (neg2&&(op2==Opcode.GE)&&(size1a<size2))||
  96                     (neg2&&(op2==Opcode.GT)&&(size1a<=size2))||
  97                     (!neg2&&(op2==Opcode.LE)&&(size1a<=size2))||
  98                     (!neg2&&(op2==Opcode.LT)&&(size1a<size2)))
  99                     return false;
 100             }
 101         }
 102
 103         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 104             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 105             (dp.getPredicate() instanceof ExprPredicate)&&
 106             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 107             boolean neg2=dp.isNegated();
 108             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 109             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
 110             if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
 111                 (neg2&&(op2==Opcode.NE)&&(size2==0))||
 112                 (!neg2&&(op2==Opcode.GE))||
 113                 (!neg2&&(op2==Opcode.GT))||
 114                 (neg2&&(op2==Opcode.LE))||
 115                 (neg2&&(op2==Opcode.LT)))
 116                 return false;
 117         }
 118
 119         /* This handles all the c comparisons in the paper */
 120         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 121             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 122             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 123             (dp.getPredicate() instanceof ExprPredicate)&&
 124             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 125             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 126             boolean neg1=ar.getPredicate().isNegated();
 127             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 128             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
 129             boolean neg2=dp.isNegated();
 130             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 131             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
 132             if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
 133                 (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
 134                 int size1a=0;
 135                 if (neg1) {
 136                     if((op1==Opcode.EQ)||(op1==Opcode.GE))
 137                         size1a=size1-1;
 138                     if((op1==Opcode.GT)||(op1==Opcode.NE))
 139                         size1a=size1;
 140                 }
 141                 if (!neg1) {
 142                     if((op1==Opcode.EQ)||(op1==Opcode.LE))
 143                         size1a=size1;
 144                     if((op1==Opcode.LT)||(op1==Opcode.NE))
 145                         size1a=size1-1;
 146                 }
 147                 if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
 148                     (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
 149                     (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
 150                     (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
 151                     (neg2&&(op2==Opcode.GE))||
 152                     (neg2&&(op2==Opcode.GT))||
 153                     (!neg2&&(op2==Opcode.LE))||
 154                     (!neg2&&(op2==Opcode.LT))||
 155                     (!neg2&&(op2==Opcode.GE)&&(size1a>=size2))||
 156                     (!neg2&&(op2==Opcode.GT)&&(size1a>size2))||
 157                     (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
 158                     (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
 159                     return false;
 160             }
 161         }
 162
 163         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 164             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 165             (dp.getPredicate() instanceof ExprPredicate)&&
 166             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 167             boolean neg2=dp.isNegated();
 168             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 169             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
 170             if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
 171                 (neg2&&(op2==Opcode.NE)&&(size2==0))||
 172                 (neg2&&(op2==Opcode.GE))||
 173                 (neg2&&(op2==Opcode.GT))||
 174                 (!neg2&&(op2==Opcode.LE))||
 175                 (!neg2&&(op2==Opcode.LT)))
 176                 return false;
 177
 178         }
 179         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 180             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 181             (dp.getPredicate() instanceof InclusionPredicate)&&
 182             (dp.isNegated()==false))
 183             return false; /* Could only satisfy this predicate */
 184
 185         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 186             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 187             (dp.getPredicate() instanceof InclusionPredicate)&&
 188             (dp.isNegated()==true))
 189             return false; /* Could only satisfy this predicate */
 190
 191         return true;
 192     }
 193
 194     static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 195         if ((des!=dp.getPredicate().getDescriptor()) &&
 196             ((des instanceof SetDescriptor)||
 197              !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
 198             return false;
 199
 200         /* This if handles all the c comparisons in the paper */
 201         if (des==dp.getPredicate().getDescriptor()&&
 202             (satisfy)&&
 203             (dp.getPredicate() instanceof ExprPredicate)&&
 204             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 205             boolean neg2=dp.isNegated();
 206             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 207             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
 208             {
 209                 if ((!neg2&&(op2==Opcode.GE))||
 210                     (!neg2&&(op2==Opcode.GT))||
 211                     (neg2&&(op2==Opcode.EQ)&&(size2==0))||
 212                     (!neg2&&(op2==Opcode.NE)&&(size2==0))||
 213                     (neg2&&(op2==Opcode.LE))||
 214                     (neg2&&(op2==Opcode.LT)))
 215                     return false;
 216             }
 217         }
 218         /* This if handles all the c comparisons in the paper */
 219         if (des==dp.getPredicate().getDescriptor()&&
 220             (!satisfy)&&
 221             (dp.getPredicate() instanceof ExprPredicate)&&
 222             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 223             boolean neg2=dp.isNegated();
 224             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 225             int size2=((ExprPredicate)dp.getPredicate()).leftsize();
 226             {
 227                 if ((neg2&&(op2==Opcode.GE))||
 228                     (neg2&&(op2==Opcode.GT))||
 229                     (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
 230                     (neg2&&(op2==Opcode.NE)&&(size2==0))||
 231                     (!neg2&&(op2==Opcode.LE))||
 232                     (!neg2&&(op2==Opcode.LT)))
 233                     return false;
 234             }
 235         }
 236         if ((des==dp.getPredicate().getDescriptor())&&
 237             satisfy&&
 238             (dp.getPredicate() instanceof InclusionPredicate)&&
 239             (dp.isNegated()==false))
 240             return false; /* Could only satisfy this predicate */
 241
 242         if ((des==dp.getPredicate().getDescriptor())&&
 243             (!satisfy)&&
 244             (dp.getPredicate() instanceof InclusionPredicate)&&
 245             (dp.isNegated()==true))
 246             return false; /* Could only satisfy this predicate */
 247
 248         return true;
 249     }
 250
 251     static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 252         for(int i=0;i<r.numQuantifiers();i++) {
 253             Quantifier q=r.getQuantifier(i);
 254             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 255                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 256                     return true;
 257             } else if (q instanceof ForQuantifier) {
 258                 if (q.getRequiredDescriptors().contains(des))
 259                     return true;
 260             } else throw new Error("Unrecognized Quantifier");
 261         }
 262         return false;
 263     }
 264
 265     static public boolean interferes(AbstractRepair ar, Quantifiers q) {
 266         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 267             return interferesquantifier(ar.getDescriptor(),true,q,true);
 268         return false;
 269     }
 270
 271     static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
 272         return interferesquantifier(des, satisfy, q,true);
 273     }
 274
 275     static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 276         if (interferesquantifier(des,satisfy,r,satisfyrule))
 277             return true;
 278         /* Scan DNF form */
 279         DNFRule drule=r.getDNFGuardExpr();
 280         for(int i=0;i<drule.size();i++) {
 281             RuleConjunction rconj=drule.get(i);
 282             for(int j=0;j<rconj.size();j++) {
 283                 DNFExpr dexpr=rconj.get(j);
 284                 Expr expr=dexpr.getExpr();
 285                 boolean negated=dexpr.getNegation();
 286                 /*
 287                   satisfy  negated
 288                   Yes      No             Yes
 289                   Yes      Yes            No
 290                   No       No             No
 291                   No       Yes            Yes
 292                 */
 293                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 294                 if (satisfiesrule==satisfyrule) {
 295                     /* Effect is the one being tested for */
 296                     /* Only expr's to be concerned with are TupleOfExpr and
 297                        ElementOfExpr */
 298                     if (expr.getRequiredDescriptors().contains(des)) {
 299                         if (((expr instanceof ElementOfExpr)||
 300                             (expr instanceof TupleOfExpr))&&
 301                             (expr.getRequiredDescriptors().size()==1))
 302                             return true;
 303                         else
 304                             throw new Error("Unrecognized EXPR");
 305                     }
 306                 }
 307             }
 308         }
 309         return false;
 310     }
 311 }