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