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