Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java

   1 package MCC.IR;
   2 import java.util.*;
   3
   4 public class ConcreteInterferes {
   5     Termination termination;
   6
   7     public ConcreteInterferes(Termination t) {
   8         this.termination=t;
   9     }
  10
  11     /** Returns true if the data structure updates performed by mun
  12      * may increase (or decrease if satisfy=false) the scope of the
  13      * model definition rule r. */
  14
  15     public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
  16
  17         // A rule that adds something to a set can't be falsified by
  18         // an update that is only performed if the set is empty
  19         if (!initialinterferes(mun,r,satisfy))
  20             return false;
  21
  22         for(int i=0;i<mun.numUpdates();i++) {
  23             UpdateNode un=mun.getUpdate(i);
  24             for (int j=0;j<un.numUpdates();j++) {
  25                 Updates update=un.getUpdate(j);
  26                 //Abstract updates don't have concrete interference1
  27                 if (update.isAbstract())
  28                     continue;
  29
  30                 DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
  31                 Descriptor updated_des=update.getDescriptor();
  32                 assert updated_des!=null;
  33
  34                 /* Test to see if the update only effects new
  35                    objects and we're only testing for falsifying
  36                    model definition rules. */
  37
  38                 if ((!satisfy)&&updateonlytonewobject(mun,un,update))
  39                     continue;
  40
  41
  42                 // See if the update interferes with the inclusion
  43                 // condition for the rule
  44                 if (r.getInclusion().usesDescriptor(updated_des)) {
  45                     boolean ok=false;
  46
  47                     /* If the update is for this rule, and the effect
  48                        is the intended effect, and the update only
  49                        effects one binding, then the abstract repair
  50                        node already models the action of this
  51                        update. */
  52
  53                     if ((un.getRule()==r)&&
  54                         (((mun.op==MultUpdateNode.ADD)&&satisfy)
  55                          ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
  56                          ||(mun.op==MultUpdateNode.MODIFY))) {
  57                         Inclusion inclusion=r.getInclusion();
  58                         if (inclusion instanceof RelationInclusion) {
  59                             RelationInclusion ri=(RelationInclusion)inclusion;
  60                             if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
  61                                 (!testdisjoint(update,r,ri.getRightExpr())))
  62                                 ok=true;
  63                         } else if (inclusion instanceof SetInclusion) {
  64                             SetInclusion si=(SetInclusion)inclusion;
  65                             if (!testdisjoint(update,r,si.getExpr()))
  66                                 ok=true;
  67                         } else throw new Error();
  68                     }
  69
  70                     if ((un.getRule()==r)&&
  71                         ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
  72                         modifiesremoves(mun,un,r)) {
  73                         Inclusion inclusion=r.getInclusion();
  74                         if (inclusion instanceof RelationInclusion) {
  75                             RelationInclusion ri=(RelationInclusion)inclusion;
  76                             if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
  77                                 (!testdisjoint(update,r,ri.getRightExpr())))
  78                                 ok=true;         /* Update is specific to
  79                                                     given binding of the rule,
  80                                                     and adds are only performed
  81                                                     if the removal is desired or
  82                                                     the tuple doesn't exist.*/
  83                         }
  84                     }
  85
  86                     if (!ok) {
  87                         if (satisfy) {
  88                             /** Check to see if the update definitely falsifies r, thus
  89                              * can't accidentally satisfy it r. */
  90                             if (interferesinclusion(un, update, r))
  91                                 return true;
  92                         } else
  93                             return true; /* Interferes with inclusion condition */
  94                     }
  95                 }
  96
  97                 for(int k=0;k<drule.size();k++) {
  98                     RuleConjunction rconj=drule.get(k);
  99                     for(int l=0;l<rconj.size();l++) {
 100                         DNFExpr dexpr=rconj.get(l);
 101                         /* See if update interferes w/ dexpr */
 102                         if ((un.getRule()==r)&&
 103                             (((mun.op==MultUpdateNode.ADD)&&satisfy)
 104                              ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
 105                              ||(mun.op==MultUpdateNode.MODIFY))) {
 106                             if (!testdisjoint(update,r,dexpr.getExpr()))
 107                                 continue; /* Update is specific to
 108                                              given binding of the
 109                                              rule, and effect is the
 110                                              intended one, so we're
 111                                              okay */
 112                         }
 113                         if ((un.getRule()==r)&&
 114                             ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
 115                             modifiesremoves(mun,un,r)) {
 116                             if (!testdisjoint(update,r,dexpr.getExpr()))
 117                                 continue; /* Update is specific to
 118                                              given binding of the
 119                                              rule, and adds are only
 120                                              performed if the removal
 121                                              is desired or the tuple
 122                                              doesn't exist.*/
 123                         }
 124
 125                         if (interferes(update,dexpr))
 126                             return true;
 127                     }
 128                 }
 129             }
 130         }
 131         return false;
 132     }
 133
 134
 135     static private boolean modifiesremoves(MultUpdateNode mun,UpdateNode un, Rule r) {
 136         AbstractRepair ar=mun.getRepair();
 137         boolean inverted=ar.getPredicate().getPredicate().inverted();
 138
 139         if (ar.getType()!=AbstractRepair.MODIFYRELATION)
 140             return false;
 141         RelationInclusion ri=(RelationInclusion)r.getInclusion();
 142         Expr e=inverted?ri.getRightExpr():ri.getLeftExpr();
 143         while(e instanceof CastExpr) {
 144             e=((CastExpr)e).getExpr();
 145         }
 146         if (!(e instanceof VarExpr))
 147             return false;
 148         VarExpr ve=(VarExpr)e;
 149         if (ve.isValue())
 150             return false;
 151         return true;
 152     }
 153
 154     static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
 155         AbstractRepair ar=mun.getRepair();
 156         if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
 157             for(int i=0;i<un.numUpdates();i++) {
 158                 Updates u=un.getUpdate(i);
 159                 if (u.getType()==Updates.POSITION&&
 160                     ar.isNewObject(u.getRightPos()==0)) {
 161                     Expr newleftexpr=u.getLeftExpr();
 162                     Expr leftexpr=updates.getLeftExpr();
 163                     boolean foundfield=false;
 164                     while(true) {
 165                         if (leftexpr.equals(null,newleftexpr)) {
 166                             if (foundfield)
 167                                 return true;
 168                             else
 169                                 break;
 170                         } else if (leftexpr instanceof DotExpr) {
 171                             if (!foundfield) {
 172                                 foundfield=true;
 173                             } else {
 174                                 if (((DotExpr)leftexpr).isPtr())
 175                                     break; //if its not a pointer, we're still in the structure
 176                             }
 177                             leftexpr=((DotExpr)leftexpr).getExpr();
 178                         } else if (leftexpr instanceof CastExpr) {
 179                             leftexpr=((CastExpr)leftexpr).getExpr();
 180                         } else
 181                             break;
 182                     }
 183                 }
 184             }
 185
 186         return false;
 187     }
 188
 189     /** This method tries to show that if the Update update from the
 190      *  UpdateNode un changes the value of the inclusion constraint
 191      * that it falsifies the guard of model definition rule. */
 192
 193     static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
 194         Descriptor updated_des=update.getDescriptor();
 195         Inclusion inclusion=r.getInclusion();
 196         if (inclusion instanceof RelationInclusion) {
 197             RelationInclusion ri=(RelationInclusion)inclusion;
 198             if (ri.getLeftExpr().usesDescriptor(updated_des)
 199                 &&searchinterfere(un,update,r,ri.getLeftExpr()))
 200                 return true;
 201             if (ri.getRightExpr().usesDescriptor(updated_des)
 202                 &&searchinterfere(un,update,r,ri.getRightExpr()))
 203                 return true;
 204         } else if (inclusion instanceof SetInclusion) {
 205             SetInclusion si=(SetInclusion)inclusion;
 206             if (si.getExpr().usesDescriptor(updated_des)
 207                 &&searchinterfere(un,update,r,si.getExpr()))
 208                 return true;
 209         } else throw new Error();
 210         return false;
 211     }
 212
 213     /** This method finds all instances of a field or global that an
 214      * update may modify, and builds a variable correspondance */
 215
 216     static private boolean searchinterfere(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
 217         Descriptor updated_des=update.getDescriptor();
 218         if (updated_des instanceof FieldDescriptor) {
 219             /* Build variable correspondance */
 220             HashSet set=new HashSet();
 221             inclusionexpr.findmatch(updated_des,set);
 222
 223             for(Iterator matchit=set.iterator();matchit.hasNext();) {
 224                 DotExpr dotexpr=(DotExpr)matchit.next();
 225                 DotExpr updateexpr=(DotExpr)update.getLeftExpr();
 226                 while(true) {
 227                     if (dotexpr.getField()!=updateexpr.getField())
 228                         return true;
 229                     Expr de=dotexpr.getExpr();
 230                     Expr ue=updateexpr.getExpr();
 231                     if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
 232                         dotexpr=(DotExpr)de;
 233                         updateexpr=(DotExpr)ue;
 234                     } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
 235                         VarDescriptor dvd=((VarExpr)de).getVar();
 236                         VarDescriptor uvd=((VarExpr)ue).getVar();
 237                         if (interferesinclusion(un,r,dvd,uvd))
 238                             return true;
 239                         else
 240                             break;
 241                     } else
 242                         return true;
 243                 }
 244             }
 245         } else if (updated_des instanceof VarDescriptor) {
 246             /* We have a VarDescriptor - no correspondance necessary */
 247             VarDescriptor vd=(VarDescriptor)updated_des;
 248             if (interferesinclusion(un,r,vd,vd))
 249                 return true;
 250         } else throw new Error();
 251         return false;
 252     }
 253
 254     /** This method tries to show that if dvd=uvd, then the update un
 255      *  must falsify the rule r. */
 256
 257     static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
 258         DNFRule negrule=r.getDNFNegGuardExpr();
 259         HashMap remap=new HashMap();
 260         remap.put(dvd,uvd);
 261
 262         for(int i=0;i<negrule.size();i++) {
 263             RuleConjunction rconj=negrule.get(i);
 264             boolean good=true;
 265             for(int j=0;j<rconj.size();j++) {
 266                 DNFExpr dexpr=rconj.get(j);
 267                 if (dexpr.getExpr() instanceof OpExpr) {
 268                     OpExpr expr=(OpExpr)dexpr.getExpr();
 269                     Expr lexpr=expr.getLeftExpr();
 270                     Expr rexpr=expr.getRightExpr();
 271
 272                     boolean varok=true;
 273                     Set vars=rexpr.freeVars();
 274                     if (vars!=null)
 275                         for(Iterator it=vars.iterator();it.hasNext();) {
 276                             VarDescriptor vd=(VarDescriptor) it.next();
 277                             if (!vd.isGlobal()) {
 278                                 /* VarDescriptor isn't a global */
 279                                 if (dvd!=vd) {
 280                                     varok=false;
 281                                     break;
 282                                 }
 283                             }
 284                         }
 285
 286                     if (!varok)
 287                         continue;
 288
 289                     Opcode op=expr.getOpcode();
 290                     op=Opcode.translateOpcode(dexpr.getNegation(),op);
 291
 292                     boolean match=false;
 293                     for(int k=0;k<un.numUpdates();k++) {
 294                         Updates update=un.getUpdate(k);
 295                         if(update.isExpr()) {
 296                             Set uvars=update.getRightExpr().freeVars();
 297                             boolean freevarok=true;
 298                             if (uvars!=null)
 299                             for(Iterator it=uvars.iterator();it.hasNext();) {
 300                                 VarDescriptor vd=(VarDescriptor) it.next();
 301                                 if (!vd.isGlobal()) {
 302                                     /* VarDescriptor isn't a global */
 303                                     if (uvd!=vd) {
 304                                         freevarok=false;
 305                                         break;
 306                                     }
 307                                 }
 308                             }
 309                             if (!freevarok)
 310                                 continue;
 311
 312                             Opcode op2=update.getOpcode();
 313                             if ((op2==op)||
 314                                 ((op2==Opcode.GT)&&(op==Opcode.GE))||
 315                                 ((op2==Opcode.LT)&&(op==Opcode.LE))||
 316                                 ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
 317                                 /* Operations match*/
 318                                 if (lexpr.equals(remap,update.getLeftExpr())&&
 319                                     rexpr.equals(remap,update.getRightExpr())) {
 320                                     match=true;
 321                                     break;
 322                                 }
 323                             }
 324                         }
 325                     }
 326                     if (!match) {
 327                         good=false;
 328                         break;
 329                     }
 330                 } else {
 331                     /* TODO: Check to see if there is an abstract repair */
 332                     good=false;
 333                     break; /* try next conjunction */
 334                 }
 335             }
 336             if (good)
 337                 return false;
 338         }
 339         return true;
 340     }
 341
 342     /** This method checks whether the update effects only the
 343      *  intended binding for the model definition rule. */
 344
 345     private boolean testdisjoint(Updates u, Rule r, Expr e) {
 346         // find all exprs that may be be effected by update
 347         Set exprs=e.useDescriptor(u.getDescriptor());
 348         for(Iterator eit=exprs.iterator();eit.hasNext();) {
 349             Expr e2=(Expr)eit.next();
 350             if (testdisjointness(u,r,e2))
 351                 return true;
 352         }
 353         return false;
 354     }
 355
 356     /** This method tries to show that the modification only effects
 357      * one binding of the model definition rule, and thus has no
 358      * unintended side effects. */
 359
 360     private boolean testdisjointness(Updates u, Rule r, Expr e) {
 361         // Note: rule of u must be r
 362
 363         Expr update_e=u.getLeftExpr();
 364         HashSet quantifierset=new HashSet();
 365
 366         if (termination.analyzeQuantifiers(r,quantifierset))
 367             return false; /* Can't accidentally interfere with other bindings if there aren't any! */
 368
 369         boolean firstfield=true;
 370
 371
 372         while(true) {
 373             if (update_e instanceof CastExpr)
 374                 update_e=((CastExpr)update_e).getExpr();
 375             else if (e instanceof CastExpr)
 376                 e=((CastExpr)e).getExpr();
 377             else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
 378                 DotExpr de1=(DotExpr)update_e;
 379                 DotExpr de2=(DotExpr)e;
 380                 if (de1.isValue(null)&&!firstfield)
 381                     return true; /* Could have aliasing from this */
 382                 if (de1.getField()!=de2.getField())
 383                     return true; /* Different fields: not comparible */
 384                 firstfield=false;
 385
 386                 Expr index1=de1.getIndex();
 387                 Expr index2=de2.getIndex();
 388                 if (index1!=null) {
 389                     assert index2!=null;
 390                     if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
 391                         VarDescriptor vd1=((VarExpr)index1).getVar();
 392                         VarDescriptor vd2=((VarExpr)index2).getVar();
 393                         if ((vd1==vd2)&&!vd1.isGlobal()) {
 394                             quantifierset.add(getQuantifier(r,vd1));
 395                             if (termination.analyzeQuantifiers(r,quantifierset))
 396                                 return false; /* State is disjoint from any other example */
 397                         }
 398                     }
 399                 }
 400                 update_e=de1.getExpr();
 401                 e=de2.getExpr();
 402             } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
 403                 VarDescriptor vd1=((VarExpr)update_e).getVar();
 404                 VarDescriptor vd2=((VarExpr)e).getVar();
 405                 if ((vd1==vd2)&&!vd1.isGlobal()) {
 406                     quantifierset.add(getQuantifier(r,vd1));
 407                     if (termination.analyzeQuantifiers(r,quantifierset))
 408                         return false; /* State is disjoint from any other example */
 409                 }
 410                 return true;
 411             } else return true;
 412         }
 413     }
 414
 415     /** This method returns the quantifier that defines the quantifier
 416      * variable vd. */
 417     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
 418         for (int i=0;i<qs.numQuantifiers();i++) {
 419             Quantifier q=qs.getQuantifier(i);
 420             if (q instanceof SetQuantifier) {
 421                 SetQuantifier sq=(SetQuantifier)q;
 422                 if (sq.getVar()==vd)
 423                     return sq;
 424             } else if (q instanceof RelationQuantifier) {
 425                 RelationQuantifier rq=(RelationQuantifier)q;
 426                 if ((rq.x==vd)||(rq.y==vd))
 427                     return rq;
 428             } else if (q instanceof ForQuantifier) {
 429                 ForQuantifier fq=(ForQuantifier)q;
 430                 if (fq.getVar()==vd)
 431                     return fq;
 432             }
 433         }
 434         return null;
 435     }
 436
 437     /** This function checks to see if an update is only performed if
 438      * a given set (or image set produced by a relation) is empty, and
 439      * the algorithm is computing whether the update may falsify a
 440      * rule that adds something to the set */
 441
 442     private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 443         AbstractRepair ar=mun.getRepair();
 444         if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
 445             if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
 446                 return true;
 447             boolean negated=ar.getPredicate().isNegated();
 448             Predicate p=ar.getPredicate().getPredicate();
 449             if (!(p instanceof ExprPredicate))
 450                 return true;
 451             ExprPredicate ep=(ExprPredicate)p;
 452             if (ep.getType()!=ExprPredicate.SIZE)
 453                 return true;
 454             Opcode op=Opcode.translateOpcode(negated,ep.getOp());
 455
 456             if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
 457                 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
 458                 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
 459                 ((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
 460                 return false;
 461         } else if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTORELATION)) {
 462             /* This test is for image sets of relations. */
 463             if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
 464                 return true;
 465             boolean negated=ar.getPredicate().isNegated();
 466             Predicate p=ar.getPredicate().getPredicate();
 467             if (!(p instanceof ExprPredicate))
 468                 return true;
 469             ExprPredicate ep=(ExprPredicate)p;
 470             if (ep.getType()!=ExprPredicate.SIZE)
 471                 return true;
 472
 473             Opcode op=Opcode.translateOpcode(negated,ep.getOp());
 474             if (!(((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
 475                 ((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
 476                 ((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
 477                 ((op==Opcode.GE)&&(ep.rightSize()==1)))) //(>=1)
 478                 return true;
 479
 480             RelationInclusion ri=(RelationInclusion)r.getInclusion();
 481             Expr tmpve=ep.inverted()?ri.getRightExpr():ri.getLeftExpr();
 482             if (!(tmpve instanceof VarExpr))
 483                 return true;
 484             for(int i=0;i<mun.numUpdates();i++) {
 485                 UpdateNode un=mun.getUpdate(i);
 486                 for (int j=0;j<un.numUpdates();j++) {
 487                     Updates update=un.getUpdate(j);
 488                     //Abstract updates don't have concrete interference1
 489                     if (update.isAbstract())
 490                         continue;
 491                     if (testdisjoint(update, r, r.getGuardExpr()))
 492                         return true;
 493                 }
 494             }
 495             return false;
 496         }
 497         return true;
 498     }
 499
 500     static private boolean interferes(Updates update, DNFExpr dexpr) {
 501         Descriptor descriptor=update.getDescriptor();
 502         /* If the DNFExpr expr doesn't use the updated descriptor,
 503            there is no interference. */
 504         if (!dexpr.getExpr().usesDescriptor(descriptor))
 505             return false;
 506
 507         if (update.isExpr()) {
 508             /* We need to pair the variables */
 509             Set vars=update.getRightExpr().freeVars();
 510             Opcode op1=update.getOpcode();
 511             Expr lexpr1=update.getLeftExpr();
 512             Expr rexpr1=update.getRightExpr();
 513             boolean good=true;
 514             if (vars!=null)
 515                 for(Iterator it=vars.iterator();it.hasNext();) {
 516                     VarDescriptor vd=(VarDescriptor) it.next();
 517                     /* VarDescriptor isn't a global */
 518                     if (!vd.isGlobal()) {
 519                         if (update.getVar()!=vd) {
 520                             good=false;
 521                             break;
 522                         }
 523                     }
 524                 }
 525             if (good&&(dexpr.getExpr() instanceof OpExpr)) {
 526                 OpExpr expr=(OpExpr)dexpr.getExpr();
 527                 Expr lexpr2=expr.getLeftExpr();
 528                 Expr rexpr2=expr.getRightExpr();
 529                 Opcode op2=expr.getOpcode();
 530                 op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 531
 532                 VarDescriptor leftdescriptor=null;
 533                 {
 534                     Expr e=lexpr2;
 535                     while(!(e instanceof VarExpr)) {
 536                         for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
 537                         if (e instanceof VarExpr)
 538                             break;
 539                         if (e instanceof CastExpr)
 540                             e=((CastExpr)e).getExpr();
 541                         else throw new Error("Bad Expr Type:"+e.name());
 542                     }
 543                     leftdescriptor=((VarExpr)e).getVar();
 544                 }
 545
 546                 vars=rexpr2.freeVars();
 547                 if (vars!=null)
 548                     for(Iterator it=vars.iterator();it.hasNext();) {
 549                         VarDescriptor vd=(VarDescriptor) it.next();
 550                         if (!vd.isGlobal()) {
 551                             /* VarDescriptor isn't a global */
 552                             if (leftdescriptor!=vd) {
 553                                 good=false;
 554                                 break;
 555                             }
 556                         }
 557                     }
 558
 559
 560                 if (good) {
 561                     HashMap remap=new HashMap();
 562                     remap.put(update.getVar(),leftdescriptor);
 563                     if ((op1==op2)&&
 564                         lexpr1.equals(remap,lexpr2)&&
 565                         rexpr1.equals(remap,rexpr2))
 566                         return false;
 567                 }
 568             }
 569         }
 570         return true;
 571     }
 572 }