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
 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
 126         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 127             (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 128             (dp.getPredicate() instanceof ExprPredicate)&&
 129             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 130             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 131
 132             boolean neg1=ar.getPredicate().isNegated();
 133             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 134             boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
 135             int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
 136             Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 137
 138
 139             boolean neg2=dp.isNegated();
 140             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 141             boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 142             int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 143             Expr expr2=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
 144
 145             /* Translate the opcodes */
 146             op1=Opcode.translateOpcode(neg1,op1);
 147             op2=Opcode.translateOpcode(neg2,op2);
 148
 149             /* Obvious cases which can't interfere */
 150             if (((op1==Opcode.GT)||
 151                 (op1==Opcode.GE))&&
 152                 ((op2==Opcode.GT)||
 153                  (op2==Opcode.GE)))
 154                 return false;
 155
 156             if (((op1==Opcode.LT)||
 157                 (op1==Opcode.LE))&&
 158                 ((op2==Opcode.LT)||
 159                  (op2==Opcode.LE)))
 160                 return false;
 161
 162             if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 163                 ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 164                 expr1.equals(null,expr2)) {
 165                 return false;
 166             }
 167
 168             if (isInt1&&isInt2) {
 169                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 170                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 171                     size1==size2)
 172                     return false;
 173                 int size1a=size1;
 174                 int size2a=size2;
 175                 if (op1==Opcode.GT)
 176                     size1a++;
 177                 if (op1==Opcode.LT)
 178                     size1a--;
 179                 if (op1==Opcode.NE)
 180                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 181
 182                 if (op2==Opcode.GT)
 183                     size2a++;
 184                 if (op2==Opcode.LT)
 185                     size2a--;
 186
 187                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 188                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 189                     (size1a<=size2a))
 190                     return false;
 191
 192                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 193                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 194                     (size1a>=size2a))
 195                     return false;
 196
 197                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 198                     (size1a==size2a))
 199                     return false;
 200
 201                 if ((op1==Opcode.EQ)&&
 202                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 203                     (size1a<=size2a))
 204                     return false;
 205
 206                 if ((op1==Opcode.EQ)&&
 207                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 208                     (size1a>=size2a))
 209                     return false;
 210
 211                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 212                     if (size1a!=size2)
 213                         return false;
 214
 215                 if ((op1==Opcode.NE)&&
 216                     (op2==Opcode.EQ)&&
 217                     (size1!=size2))
 218                     return false;
 219
 220                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 221                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 222                     (size1!=size2a))
 223                     return false;
 224
 225                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 226                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 227                     (size1!=size2a))
 228                     return false;
 229             }
 230         }
 231
 232         /* This handles all the c comparisons in the paper */
 233         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 234             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 235             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 236             (dp.getPredicate() instanceof ExprPredicate)&&
 237             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 238             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 239             boolean neg1=ar.getPredicate().isNegated();
 240             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 241             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 242             boolean neg2=dp.isNegated();
 243             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 244             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 245             /* Translate the opcodes */
 246             op1=Opcode.translateOpcode(neg1,op1);
 247             op2=Opcode.translateOpcode(neg2,op2);
 248
 249             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 250                 int size1a=0;
 251
 252                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 253                     size1a=size1;
 254                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 255                     size1a=size1-1;
 256
 257                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 258                     ((op2==Opcode.NE)&&(size1a!=size2))||
 259                     (op2==Opcode.LE)||
 260                     (op2==Opcode.LT)||
 261                     ((op2==Opcode.GE)&&(size1a>=size2))||
 262                     ((op2==Opcode.GT)&&(size1a>size2)))
 263                     return false;
 264             }
 265         }
 266
 267         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 268             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 269             (dp.getPredicate() instanceof ExprPredicate)&&
 270             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 271             boolean neg2=dp.isNegated();
 272             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 273             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 274             op2=Opcode.translateOpcode(neg2,op2);
 275
 276             if (((op2==Opcode.EQ)&&(size2==0))||
 277                 (op2==Opcode.LE)||
 278                 (op2==Opcode.LT))
 279                 return false;
 280
 281         }
 282         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 283             (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 284             (dp.getPredicate() instanceof InclusionPredicate)&&
 285             (dp.isNegated()==false))
 286             return false; /* Could only satisfy this predicate */
 287
 288         if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 289             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 290             (dp.getPredicate() instanceof InclusionPredicate)&&
 291             (dp.isNegated()==true))
 292             return false; /* Could only satisfy this predicate */
 293
 294         return true;
 295     }
 296
 297     /** Does the increase (or decrease) in scope of a model defintion rule represented by sn
 298      * falsify the predicate dp */
 299
 300     public boolean interferes(ScopeNode sn, DNFPredicate dp) {
 301         if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
 302             Rule r=sn.getRule();
 303             Set target=r.getInclusion().getTargetDescriptors();
 304             boolean match=false;
 305             for(int i=0;i<r.numQuantifiers();i++) {
 306                 Quantifier q=r.getQuantifier(i);
 307                 if (q instanceof SetQuantifier) {
 308                     SetQuantifier sq=(SetQuantifier) q;
 309                     if (target.contains(sq.getSet())) {
 310                         match=true;
 311                         break;
 312                     }
 313                 }
 314             }
 315             if (match&&
 316                 sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
 317                 (dp.getPredicate() instanceof ExprPredicate)&&
 318                 (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 319                 boolean neg=dp.isNegated();
 320                 Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 321                 int size=((ExprPredicate)dp.getPredicate()).rightSize();
 322                 op=Opcode.translateOpcode(neg,op);
 323
 324                 if ((op==Opcode.GE)&&
 325                     ((size==0)||(size==1)))
 326                     return false;
 327                 if ((op==Opcode.GT)&&
 328                     (size==0))
 329                     return false;
 330             }
 331         }
 332         return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
 333     }
 334
 335     /** Does increasing (or decreasing if satisfy=false) the size of the set or relation des
 336      * falsify the predicate dp */
 337
 338     public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 339         if ((des!=dp.getPredicate().getDescriptor()) &&
 340             ((des instanceof SetDescriptor)||
 341              !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
 342             return false;
 343
 344         /* This if handles all the c comparisons in the paper */
 345         if (des==dp.getPredicate().getDescriptor()&&
 346             (satisfy)&&
 347             (dp.getPredicate() instanceof ExprPredicate)&&
 348             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 349             boolean neg2=dp.isNegated();
 350             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 351             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 352             op2=Opcode.translateOpcode(neg2,op2);
 353
 354
 355             int maxsize=termination.maxsize.getsize(dp.getPredicate().getDescriptor());
 356             {
 357                 if ((maxsize!=-1)&&
 358                     ((op2==Opcode.LT&&size2>maxsize)||
 359                      (op2==Opcode.LE&&size2>=maxsize)||
 360                      (op2==Opcode.EQ&&size2>=maxsize)))
 361                     return false;
 362
 363                 if ((op2==Opcode.GE)||
 364                     (op2==Opcode.GT)||
 365                     (op2==Opcode.NE)&&(size2==0))
 366                     return false;
 367             }
 368         }
 369         /* This if handles all the c comparisons in the paper */
 370         if (des==dp.getPredicate().getDescriptor()&&
 371             (!satisfy)&&
 372             (dp.getPredicate() instanceof ExprPredicate)&&
 373             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 374             boolean neg2=dp.isNegated();
 375             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 376             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 377             op2=Opcode.translateOpcode(neg2,op2);
 378             {
 379                 if (((op2==Opcode.EQ)&&(size2==0))||
 380                     (op2==Opcode.LE)||
 381                     (op2==Opcode.LT))
 382                     return false;
 383             }
 384         }
 385         if ((des==dp.getPredicate().getDescriptor())&&
 386             satisfy&&
 387             (dp.getPredicate() instanceof InclusionPredicate)&&
 388             (dp.isNegated()==false))
 389             return false; /* Could only satisfy this predicate */
 390
 391         if ((des==dp.getPredicate().getDescriptor())&&
 392             (!satisfy)&&
 393             (dp.getPredicate() instanceof InclusionPredicate)&&
 394             (dp.isNegated()==true))
 395             return false; /* Could only satisfy this predicate */
 396
 397         return true;
 398     }
 399
 400     static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 401         for(int i=0;i<r.numQuantifiers();i++) {
 402             Quantifier q=r.getQuantifier(i);
 403             if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
 404                 if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
 405                     return true;
 406             } else if (q instanceof ForQuantifier) {
 407                 if (q.getRequiredDescriptors().contains(des))
 408                     return true;
 409             } else throw new Error("Unrecognized Quantifier");
 410         }
 411         return false;
 412     }
 413
 414     static public boolean interferes(AbstractRepair ar, Quantifiers q) {
 415         if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
 416             return interferesquantifier(ar.getDescriptor(),true,q,true);
 417         return false;
 418     }
 419
 420     static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
 421         return interferesquantifier(des, satisfy, q,true);
 422     }
 423
 424     static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
 425         if (interferesquantifier(des,satisfy,r,satisfyrule))
 426             return true;
 427         /* Scan DNF form */
 428         DNFRule drule=r.getDNFGuardExpr();
 429         for(int i=0;i<drule.size();i++) {
 430             RuleConjunction rconj=drule.get(i);
 431             for(int j=0;j<rconj.size();j++) {
 432                 DNFExpr dexpr=rconj.get(j);
 433                 Expr expr=dexpr.getExpr();
 434                 boolean negated=dexpr.getNegation();
 435                 /*
 436                   satisfy  negated
 437                   Yes      No             Yes
 438                   Yes      Yes            No
 439                   No       No             No
 440                   No       Yes            Yes
 441                 */
 442                 boolean satisfiesrule=(satisfy^negated);/*XOR of these */
 443                 if (satisfiesrule==satisfyrule) {
 444                     /* Effect is the one being tested for */
 445                     /* Only expr's to be concerned with are TupleOfExpr and
 446                        ElementOfExpr */
 447                     if (expr.getRequiredDescriptors().contains(des)) {
 448                         if (((expr instanceof ElementOfExpr)||
 449                             (expr instanceof TupleOfExpr))&&
 450                             (expr.getRequiredDescriptors().size()==1))
 451                             return true;
 452                         else
 453                             throw new Error("Unrecognized EXPR");
 454                     }
 455                 }
 456             }
 457         }
 458         return false;
 459     }
 460 }