Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

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