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