Repair/RepairCompiler/MCC/IR/AbstractInterferes.java

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