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 (isInt1&&isInt2) {
 163                 if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 164                     ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 165                     size1==size2)
 166                     return false;
 167                 int size1a=size1;
 168                 int size2a=size2;
 169                 if (op1==Opcode.GT)
 170                     size1a++;
 171                 if (op1==Opcode.LT)
 172                     size1a--;
 173                 if (op1==Opcode.NE)
 174                     size1a++; /*FLAGNE this is current behavior for NE repairs */
 175
 176                 if (op2==Opcode.GT)
 177                     size2a++;
 178                 if (op2==Opcode.LT)
 179                     size2a--;
 180
 181                 if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 182                     ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 183                     (size1a<=size2a))
 184                     return false;
 185
 186                 if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 187                     ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 188                     (size1a>=size2a))
 189                     return false;
 190
 191                 if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 192                     (size1a==size2a))
 193                     return false;
 194
 195                 if ((op1==Opcode.EQ)&&
 196                     ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 197                     (size1a<=size2a))
 198                     return false;
 199
 200                 if ((op1==Opcode.EQ)&&
 201                     ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 202                     (size1a>=size2a))
 203                     return false;
 204
 205                 if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 206                     if (size1a!=size2)
 207                         return false;
 208
 209                 if ((op1==Opcode.NE)&&
 210                     (op2==Opcode.EQ)&&
 211                     (size1!=size2))
 212                     return false;
 213
 214                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 215                     ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 216                     (size1!=size2a))
 217                     return false;
 218
 219                 if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 220                     ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 221                     (size1!=size2a))
 222                     return false;
 223             }
 224         }
 225
 226         /* This handles all the c comparisons in the paper */
 227         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 228             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 229             (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
 230             (dp.getPredicate() instanceof ExprPredicate)&&
 231             (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 232             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 233             boolean neg1=ar.getPredicate().isNegated();
 234             Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 235             int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
 236             boolean neg2=dp.isNegated();
 237             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 238             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 239             /* Translate the opcodes */
 240             op1=Opcode.translateOpcode(neg1,op1);
 241             op2=Opcode.translateOpcode(neg2,op2);
 242
 243             if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
 244                 int size1a=0;
 245
 246                 if((op1==Opcode.EQ)||(op1==Opcode.LE))
 247                     size1a=size1;
 248                 if((op1==Opcode.LT)||(op1==Opcode.NE))
 249                     size1a=size1-1;
 250
 251                 if (((op2==Opcode.EQ)&&(size1a==size2))||
 252                     ((op2==Opcode.NE)&&(size1a!=size2))||
 253                     (op2==Opcode.LE)||
 254                     (op2==Opcode.LT)||
 255                     ((op2==Opcode.GE)&&(size1a>=size2))||
 256                     ((op2==Opcode.GT)&&(size1a>size2)))
 257                     return false;
 258             }
 259         }
 260
 261         if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 262             (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
 263             (dp.getPredicate() instanceof ExprPredicate)&&
 264             (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 265             boolean neg2=dp.isNegated();
 266             Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 267             int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 268             op2=Opcode.translateOpcode(neg2,op2);
 269
 270             if (((op2==Opcode.EQ)&&(size2==0))||
 271                 (op2==Opcode.LE)||
 272                 (op2==Opcode.LT))
 273                 return false;
 274
 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
 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 }