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