Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java

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