Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

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