Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

   1 package MCC.IR;
   2 import java.util.*;
   3
   4 class AbstractInterferes {
   5     Termination termination;
   6
   7     public AbstractInterferes(Termination t) {
   8         termination=t;
   9     }
  10
  11     /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
  12      * Rule r */
  13     static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
  14         boolean mayadd=false;
  15         boolean mayremove=false;
  16         switch (ar.getType()) {
  17         case AbstractRepair.ADDTOSET:
  18         case AbstractRepair.ADDTORELATION:
  19             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  20                 return true;
  21             mayadd=true;
  22             break;
  23         case AbstractRepair.REMOVEFROMSET:
  24         case AbstractRepair.REMOVEFROMRELATION:
  25             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  26                 return true;
  27             mayremove=true;
  28             break;
  29         case AbstractRepair.MODIFYRELATION:
  30             if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
  31                 return true;
  32             if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
  33                 return true;
  34             mayadd=true;
  35             mayremove=true;
  36         break;
  37         default:
  38             throw new Error("Unrecognized Abstract Repair");
  39         }
  40         DNFRule drule=null;
  41         if (satisfy)
  42             drule=r.getDNFGuardExpr();
  43         else
  44             drule=r.getDNFNegGuardExpr();
  45
  46         for(int i=0;i<drule.size();i++) {
  47             RuleConjunction rconj=drule.get(i);
  48             for(int j=0;j<rconj.size();j++) {
  49                 DNFExpr dexpr=rconj.get(j);
  50                 Expr expr=dexpr.getExpr();
  51                 if (expr.usesDescriptor(ar.getDescriptor())) {
  52                     /* Need to check */
  53                     if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
  54                         return true;
  55                 }
  56             }
  57         }
  58         return false;
  59     }
  60
  61     /** Does performing the AbstractRepair ar falsify the predicate dp */
  62
  63     public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
  64         if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
  65             ((ar.getDescriptor() instanceof SetDescriptor)||
  66              !dp.getPredicate().usesDescriptor((RelationDescriptor)ar.getDescriptor())))
  67             return false;
  68
  69         /* This if handles all the c comparisons in the paper */
  70         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
  71             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
  72             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
  73             (dp.getPredicate() instanceof ExprPredicate)&&
  74             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
  75             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
  76             boolean neg1=ar.getPredicate().isNegated();
  77             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
  78             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
  79             boolean neg2=dp.isNegated();
  80             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
  81             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
  82             op1=Opcode.translateOpcode(neg1,op1);
  83             op2=Opcode.translateOpcode(neg2,op2);
  84
  85             if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
  86                 int size1a=0;
  87                 if((op1==Opcode.EQ)||(op1==Opcode.GE))
  88                     size1a=size1;
  89                 if((op1==Opcode.GT)||(op1==Opcode.NE))
  90                     size1a=size1+1;
  91
  92                 if (((op2==Opcode.EQ)&&(size1a==size2))||
  93                     ((op2==Opcode.NE)&&(size1a!=size2))||
  94                     (op2==Opcode.GE)||
  95                     (op2==Opcode.GT)||
  96                     ((op2==Opcode.LE)&&(size1a<=size2))||
  97                     ((op2==Opcode.LT)&&(size1a<size2)))
  98                     return false;
  99             }
 100         }
 101         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 102             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 103             (dp.getPredicate() instanceof ExprPredicate)&&
 104             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 105             boolean neg2=dp.isNegated();
 106             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 107             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 108
 109             op2=Opcode.translateOpcode(neg2,op2);
 110
 111             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 112
 113             if ((maxsize!=-1)&&
 114                 ((op2==Opcode.LT&&size2>maxsize)||
 115                  (op2==Opcode.LE&&size2>=maxsize)||
 116                  (op2==Opcode.EQ&&size2>=maxsize)))
 117                 return false;
 118
 119             if (((op2==Opcode.NE)&&(size2==0))||
 120                 (op2==Opcode.GE)||
 121                 (op2==Opcode.GT))
 122                 return false;
 123         }
 124         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 125             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 126             (dp.getPredicate() instanceof ExprPredicate)&&
 127             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 128             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 129
 130             boolean neg1=ar.getPredicate().isNegated();
 131             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 132             boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
 133             int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
 134             Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 135
 136
 137             boolean neg2=dp.isNegated();
 138             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 139             boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 140             int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 141             Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 142
 143             {
 144                 Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
 145                 Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
 146                 SetDescriptor sd1=lexpr1.getSet();
 147                 SetDescriptor sd2=lexpr2.getSet();
 148                 if (termination.mutuallyexclusive(sd1,sd2))
 149                     return false;
 150             }
 151
 152
 153
 154             /* Translate the opcodes */
 155             op1=Opcode.translateOpcode(neg1,op1);
 156             op2=Opcode.translateOpcode(neg2,op2);
 157
 158             /* Obvious cases which can't interfere */
 159             if (((op1==Opcode.GT)||
 160                 (op1==Opcode.GE))&&
 161                 ((op2==Opcode.GT)||
 162                  (op2==Opcode.GE)))
 163                 return false;
 164             if (((op1==Opcode.LT)||
 165                 (op1==Opcode.LE))&&
 166                 ((op2==Opcode.LT)||
 167                  (op2==Opcode.LE)))
 168                 return false;
 169             if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 170                 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 171                 expr1.equals(null,expr2)) {
 172                 return false;
 173             }
 174             if (isInt1&&isInt2) {
 175                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 176                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 177                     size1==size2)
 178                     return false;
 179                 int size1a=size1;
 180                 int size2a=size2;
 181                 if (op1==Opcode.GT)
 182                     size1a++;
 183                 if (op1==Opcode.LT)
 184                     size1a--;
 185                 if (op1==Opcode.NE)
 186                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 187
 188                 if (op2==Opcode.GT)
 189                     size2a++;
 190                 if (op2==Opcode.LT)
 191                     size2a--;
 192                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 193                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 194                     (size1a<=size2a))
 195                     return false;
 196                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 197                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 198                     (size1a>=size2a))
 199                     return false;
 200                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 201                     (size1a==size2a))
 202                     return false;
 203                 if ((op1==Opcode.EQ)&&
 204                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 205                     (size1a<=size2a))
 206                     return false;
 207                 if ((op1==Opcode.EQ)&&
 208                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 209                     (size1a>=size2a))
 210                     return false;
 211                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 212                     if (size1a!=size2)
 213                         return false;
 214                 if ((op1==Opcode.NE)&&
 215                     (op2==Opcode.EQ)&&
 216                     (size1!=size2))
 217                     return false;
 218                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 219                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 220                     (size1!=size2a))
 221                     return false;
 222                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 223                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 224                     (size1!=size2a))
 225                     return false;
 226             }
 227         }
 228         /* This handles all the c comparisons in the paper */
 229         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 230             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 231             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 232             (dp.getPredicate() instanceof ExprPredicate)&&
 233             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 234             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 235             boolean neg1=ar.getPredicate().isNegated();
 236             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 237             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 238             boolean neg2=dp.isNegated();
 239             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 240             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 241             /* Translate the opcodes */
 242             op1=Opcode.translateOpcode(neg1,op1);
 243             op2=Opcode.translateOpcode(neg2,op2);
 244
 245             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 246                 int size1a=0;
 247
 248                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 249                     size1a=size1;
 250                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 251                     size1a=size1-1;
 252
 253                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 254                     ((op2==Opcode.NE)&&(size1a!=size2))||
 255                     (op2==Opcode.LE)||
 256                     (op2==Opcode.LT)||
 257                     ((op2==Opcode.GE)&&(size1a>=size2))||
 258                     ((op2==Opcode.GT)&&(size1a>size2)))
 259                     return false;
 260             }
 261         }
 262
 263         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 264             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 265             (dp.getPredicate() instanceof ExprPredicate)&&
 266             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 267             boolean neg2=dp.isNegated();
 268             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 269             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 270             op2=Opcode.translateOpcode(neg2,op2);
 271
 272             if (((op2==Opcode.EQ)&&(size2==0))||
 273                 (op2==Opcode.LE)||
 274                 (op2==Opcode.LT))
 275                 return false;
 276         }
 277         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 278             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 279             (dp.getPredicate() instanceof InclusionPredicate)&&
 280             (dp.isNegated()==false))
 281             return false; /* Could only satisfy this predicate */
 282
 283         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 284             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 285             (dp.getPredicate() instanceof InclusionPredicate)&&
 286             (dp.isNegated()==true))
 287             return false; /* Could only satisfy this predicate */
 288         return true;
 289     }
 290
 291     /** Does the increase (or decrease) in scope of a model defintion rule represented by sn
 292      * falsify the predicate dp */
 293
 294     public boolean interferes(ScopeNode sn, DNFPredicate dp) {
 295         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 296             Rule r=sn.getRule();
 297             Set target=r.getInclusion().getTargetDescriptors();
 298             boolean match=false;
 299             for(int i=0;i<r.numQuantifiers();i++) {
 300                 Quantifier q=r.getQuantifier(i);
 301                 if (q instanceof SetQuantifier) {
 302                     SetQuantifier sq=(SetQuantifier) q;
 303                     if (target.contains(sq.getSet())) {
 304                         match=true;
 305                         break;
 306                     }
 307                 }
 308             }
 309             if (match&&
 310                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
 311                 (dp.getPredicate() instanceof ExprPredicate)&&
 312                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 313                 boolean neg=dp.isNegated();
 314                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 315                 int size=((ExprPredicate)dp.getPredicate()).rightSize();
 316                 op=Opcode.translateOpcode(neg,op);
 317
 318                 if ((op==Opcode.GE)&&
 319                     ((size==0)||(size==1)))
 320                     return false;
 321                 if ((op==Opcode.GT)&&
 322                     (size==0))
 323                     return false;
 324             }
 325         }
 326         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 327     }
 328
 329     /** Does increasing (or decreasing if satisfy=false) the size of the set or relation des
 330      * falsify the predicate dp */
 331
 332     public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 333         if ((des!=dp.getPredicate().getDescriptor()) &&
 334             ((des instanceof SetDescriptor)||
 335              !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
 336             return false;
 337
 338         /* This if handles all the c comparisons in the paper */
 339         if (des==dp.getPredicate().getDescriptor()&&
 340             (satisfy)&&
 341             (dp.getPredicate() instanceof ExprPredicate)&&
 342             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 343             boolean neg2=dp.isNegated();
 344             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 345             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 346             op2=Opcode.translateOpcode(neg2,op2);
 347
 348
 349             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 350             {
 351                 if ((maxsize!=-1)&&
 352                     ((op2==Opcode.LT&&size2>maxsize)||
 353                      (op2==Opcode.LE&&size2>=maxsize)||
 354                      (op2==Opcode.EQ&&size2>=maxsize)))
 355                     return false;
 356
 357                 if ((op2==Opcode.GE)||
 358                     (op2==Opcode.GT)||
 359                     (op2==Opcode.NE)&&(size2==0))
 360                     return false;
 361             }
 362         }
 363         /* This if handles all the c comparisons in the paper */
 364         if (des==dp.getPredicate().getDescriptor()&&
 365             (!satisfy)&&
 366             (dp.getPredicate() instanceof ExprPredicate)&&
 367             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 368             boolean neg2=dp.isNegated();
 369             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 370             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 371             op2=Opcode.translateOpcode(neg2,op2);
 372             {
 373                 if (((op2==Opcode.EQ)&&(size2==0))||
 374                     (op2==Opcode.LE)||
 375                     (op2==Opcode.LT))
 376                     return false;
 377             }
 378         }
 379         if ((des==dp.getPredicate().getDescriptor())&&
 380             satisfy&&
 381             (dp.getPredicate() instanceof InclusionPredicate)&&
 382             (dp.isNegated()==false))
 383             return false; /* Could only satisfy this predicate */
 384
 385         if ((des==dp.getPredicate().getDescriptor())&&
 386             (!satisfy)&&
 387             (dp.getPredicate() instanceof InclusionPredicate)&&
 388             (dp.isNegated()==true))
 389             return false; /* Could only satisfy this predicate */
 390
 391         return true;
 392     }
 393
 394     static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 395         for(int i=0;i<r.numQuantifiers();i++) {
 396             Quantifier q=r.getQuantifier(i);
 397             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 398                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 399                     return true;
 400             } else if (q instanceof ForQuantifier) {
 401                 if (q.getRequiredDescriptors().contains(des))
 402                     return true;
 403             } else throw new Error("Unrecognized Quantifier");
 404         }
 405         return false;
 406     }
 407
 408     static public boolean interferes(AbstractRepair ar, Quantifiers q) {
 409         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 410             return interferesquantifier(ar.getDescriptor(),true,q,true);
 411         return false;
 412     }
 413
 414     static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
 415         return interferesquantifier(des, satisfy, q,true);
 416     }
 417
 418     static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 419         if (interferesquantifier(des,satisfy,r,satisfyrule))
 420             return true;
 421         /* Scan DNF form */
 422         DNFRule drule=r.getDNFGuardExpr();
 423         for(int i=0;i<drule.size();i++) {
 424             RuleConjunction rconj=drule.get(i);
 425             for(int j=0;j<rconj.size();j++) {
 426                 DNFExpr dexpr=rconj.get(j);
 427                 Expr expr=dexpr.getExpr();
 428                 boolean negated=dexpr.getNegation();
 429                 /*
 430                   satisfy  negated
 431                   Yes      No             Yes
 432                   Yes      Yes            No
 433                   No       No             No
 434                   No       Yes            Yes
 435                 */
 436                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 437                 if (satisfiesrule==satisfyrule) {
 438                     /* Effect is the one being tested for */
 439                     /* Only expr's to be concerned with are TupleOfExpr and
 440                        ElementOfExpr */
 441                     if (expr.getRequiredDescriptors().contains(des)) {
 442                         if (((expr instanceof ElementOfExpr)||
 443                             (expr instanceof TupleOfExpr))&&
 444                             (expr.getRequiredDescriptors().size()==1))
 445                             return true;
 446                         else
 447                             throw new Error("Unrecognized EXPR");
 448                     }
 449                 }
 450             }
 451         }
 452         return false;
 453     }
 454 }