Repair/RepairCompiler/MCC/IR/GraphAnalysis.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5
   6 public class GraphAnalysis {
   7     Termination termination;
   8     static final int WORKS=0;
   9     static final int ERR_NOREPAIR=1;
  10     static final int ERR_CYCLE=2;
  11     static final int ERR_RULE=3;
  12     static final int ERR_ABSTRACT=4;
  13
  14     public GraphAnalysis(Termination t) {
  15         termination=t;
  16     }
  17
  18     public Set doAnalysis() {
  19         HashSet cantremove=new HashSet();
  20         HashSet mustremove=new HashSet();
  21         HashSet optionalabstractrepair=new HashSet();
  22
  23         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
  24             GraphNode gn=(GraphNode)it.next();
  25             TermNode tn=(TermNode)gn.getOwner();
  26             AbstractRepair ar=tn.getAbstract();
  27             DNFPredicate dpred=ar.getPredicate();
  28             Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
  29             if ((repairnodes.size()>1)&&
  30                 containsmodify(repairnodes)) {
  31                 optionalabstractrepair.add(gn);
  32             }
  33         }
  34
  35         cantremove.addAll(termination.scopenodes);
  36         cantremove.addAll(termination.abstractrepair);
  37         cantremove.removeAll(optionalabstractrepair);
  38
  39         while(true) {
  40             boolean change=false;
  41             HashSet nodes=new HashSet();
  42             nodes.addAll(termination.conjunctions);
  43             nodes.removeAll(mustremove);
  44             GraphNode.computeclosure(nodes,mustremove);
  45             Set cycles=GraphNode.findcycles(nodes);
  46             Set couldremove=new HashSet();
  47             couldremove.addAll(termination.conjunctions);
  48             couldremove.addAll(termination.updatenodes);
  49             couldremove.addAll(termination.consequencenodes);
  50             couldremove.addAll(optionalabstractrepair);
  51             couldremove.retainAll(cycles);
  52
  53             /* Look for constraints which can only be satisfied one way */
  54
  55             Vector constraints=termination.state.vConstraints;
  56             for(int i=0;i<constraints.size();i++) {
  57                 Constraint c=(Constraint)constraints.get(i);
  58                 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
  59                 HashSet tmpset=new HashSet();
  60                 tmpset.addAll(conjunctionset);
  61                 tmpset.removeAll(mustremove);
  62                 if (tmpset.size()==1) {
  63                     int oldsize=cantremove.size();
  64                     cantremove.addAll(tmpset);
  65                     if (cantremove.size()!=oldsize)
  66                         change=true;
  67                 }
  68             }
  69
  70             /* Search through conjunction which must be satisfied, and attempt
  71                to generate appropriate repair actions.
  72              */
  73             HashSet newset=new HashSet();
  74             for(Iterator cit=cantremove.iterator();cit.hasNext();) {
  75                 GraphNode gn=(GraphNode)cit.next();
  76                 boolean nomodify=true;
  77                 HashSet toremove=new HashSet();
  78                 if (termination.conjunctions.contains(gn)) {
  79                     for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
  80                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
  81                         GraphNode gn2=e.getTarget();
  82                         TermNode tn2=(TermNode)gn2.getOwner();
  83                         if (nodes.contains(gn2)&&!mustremove.contains(gn2)&&
  84                             tn2.getType()==TermNode.ABSTRACT) {
  85
  86                             HashSet updateset=new HashSet();
  87                             for(Iterator upit=gn2.edges();upit.hasNext();) {
  88                                 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
  89                                 GraphNode gn3=e2.getTarget();
  90                                 TermNode tn3=(TermNode)gn3.getOwner();
  91                                 if (tn3.getType()==TermNode.UPDATE)
  92                                     updateset.add(gn3);
  93                             }
  94                             updateset.removeAll(mustremove);
  95
  96                             AbstractRepair ar=tn2.getAbstract();
  97                             DNFPredicate dpred=ar.getPredicate();
  98                             Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
  99                             if (repairnodes.size()>1&&
 100                                 containsmodify(repairnodes)) {
 101                                 /* We are modifying a relation */
 102                                 HashSet retainednodes=new HashSet();
 103                                 retainednodes.addAll(repairnodes);
 104                                 retainednodes.retainAll(nodes);
 105
 106                                 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 107                                     if (updateset.size()==0) {
 108                                         if (retainednodes.size()>1) {
 109                                             mustremove.add(gn);
 110                                             change=true;
 111                                         } else return null; /* Out of luck */
 112                                     }
 113                                     if (updateset.size()==1&&retainednodes.size()==1)
 114                                         toremove.addAll(updateset); /* Required update */
 115                                 } else {
 116                                     /* Addition or removal to relation */
 117                                     assert (ar.getType()==AbstractRepair.ADDTORELATION)||(ar.getType()==AbstractRepair.REMOVEFROMRELATION);
 118                                     if (updateset.size()==0) {
 119                                         if (containsmodify(retainednodes)) {
 120                                             /* Both ADD & REMOVE are no good */
 121                                             for(Iterator it=retainednodes.iterator();it.hasNext();) {
 122                                                 GraphNode gnit=(GraphNode)it.next();
 123                                                 TermNode tnit=(TermNode)gnit.getOwner();
 124                                                 AbstractRepair arit=tnit.getAbstract();
 125                                                 if (arit.getType()!=AbstractRepair.MODIFYRELATION) {
 126                                                     mustremove.add(gnit);
 127                                                     change=true;
 128                                                 }
 129                                             }
 130                                         } else
 131                                             return null; /* Out of luck */
 132                                     }
 133                                     if (updateset.size()==1&&retainednodes.size()==2)
 134                                         toremove.addAll(updateset); /* Required update */
 135                                 }
 136                             } else if (updateset.size()==1)
 137                                 toremove.addAll(updateset);
 138                         }
 139                     }
 140                     newset.addAll(toremove);
 141                 }
 142             }
 143             {
 144                 int oldsize=cantremove.size();
 145                 cantremove.addAll(newset);
 146                 if (cantremove.size()!=oldsize)
 147                     change=true;
 148             }
 149
 150             /* Look for required actions for scope nodes */
 151             for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
 152                 GraphNode gn=(GraphNode)scopeit.next();
 153                 HashSet tmpset=new HashSet();
 154                 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 155                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 156                     tmpset.add(e.getTarget());
 157                 }
 158                 tmpset.removeAll(mustremove);
 159                 if (tmpset.size()==1) {
 160                     int oldsize=cantremove.size();
 161                     cantremove.addAll(tmpset);
 162                     if (cantremove.size()!=oldsize)
 163                         change=true;
 164                 }
 165             }
 166
 167             Set cycles2=GraphNode.findcycles(cantremove);
 168             for(Iterator it=cycles2.iterator();it.hasNext();) {
 169                 GraphNode gn=(GraphNode)it.next();
 170                 if (termination.conjunctions.contains(gn))
 171                     return null; // Out of luck
 172             }
 173
 174             /* Search through abstract repair actions & correspond data structure updates */
 175             for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
 176                 GraphNode gn=(GraphNode)it.next();
 177                 TermNode tn=(TermNode)gn.getOwner();
 178
 179                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 180                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 181                     GraphNode gn2=e.getTarget();
 182                     TermNode tn2=(TermNode)gn2.getOwner();
 183                     if (tn2.getType()!=TermNode.UPDATE)
 184                         continue;
 185
 186                     boolean containsgn=cantremove.contains(gn);
 187                     boolean containsgn2=cantremove.contains(gn2);
 188
 189                     cantremove.add(gn);
 190                     cantremove.add(gn2);
 191
 192                     Set cycle=GraphNode.findcycles(cantremove);
 193                     if (cycle.contains(gn2)) {
 194                         if (!mustremove.contains(gn2)) {
 195                             change=true;
 196                             mustremove.add(gn2);
 197                         }
 198                     }
 199
 200                     if (!containsgn)
 201                         cantremove.remove(gn);
 202                     if (!containsgn2)
 203                         cantremove.remove(gn2);
 204                 }
 205             }
 206
 207             /* Searches individual conjunctions + abstract action +updates for cycles */
 208             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 209                 GraphNode gn=(GraphNode)it.next();
 210                 boolean foundnocycle=false;
 211
 212                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 213                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 214                     GraphNode gn2=e.getTarget();
 215                     TermNode tn2=(TermNode)gn2.getOwner();
 216                     if (tn2.getType()!=TermNode.ABSTRACT)
 217                         continue;
 218                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 219                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 220                         GraphNode gn3=e2.getTarget();
 221                         TermNode tn3=(TermNode)gn3.getOwner();
 222                         if (tn3.getType()!=TermNode.UPDATE)
 223                             continue;
 224                         boolean containsgn=cantremove.contains(gn);
 225                         boolean containsgn2=cantremove.contains(gn2);
 226                         boolean containsgn3=cantremove.contains(gn3);
 227                         cantremove.add(gn);
 228                         cantremove.add(gn2);
 229                         cantremove.add(gn3);
 230                         Set cycle=GraphNode.findcycles(cantremove);
 231                         if (cycle.contains(gn3)) {
 232                             if (!mustremove.contains(gn3)) {
 233                                 change=true;
 234                                 mustremove.add(gn3);
 235                             }
 236                         }
 237                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 238                             foundnocycle=true;
 239                         }
 240                         if (!containsgn)
 241                             cantremove.remove(gn);
 242                         if (!containsgn2)
 243                             cantremove.remove(gn2);
 244                         if (!containsgn3)
 245                             cantremove.remove(gn3);
 246                     }
 247                 }
 248                 if(!foundnocycle) {
 249                     if (!mustremove.contains(gn)) {
 250                         change=true;
 251                         mustremove.add(gn);
 252                     }
 253                 }
 254             }
 255
 256             /* Searches scope nodes + compensation nodes */
 257             for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 258                 GraphNode gn=(GraphNode)it.next();
 259                 boolean foundcompensation=false;
 260                 if (nodes.contains(gn)) {
 261                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 262                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 263                         GraphNode gn2=e.getTarget();
 264                         TermNode tn2=(TermNode)gn2.getOwner();
 265
 266                         if (tn2.getType()!=TermNode.UPDATE)
 267                             continue;
 268                         /* We have a compensation node */
 269                         boolean containsgn=cantremove.contains(gn);
 270                         boolean containsgn2=cantremove.contains(gn2);
 271                         cantremove.add(gn);
 272                         cantremove.add(gn2);
 273
 274                         Set cycle=GraphNode.findcycles(cantremove);
 275                         if (cycle.contains(gn2)) {
 276                             if (!mustremove.contains(gn2)) {
 277                                 change=true;
 278                                 mustremove.add(gn2);
 279                             }
 280                         } else {
 281                             if (!mustremove.contains(gn2))
 282                                 foundcompensation=true;
 283                         }
 284                         if (!containsgn)
 285                             cantremove.remove(gn);
 286                         if (!containsgn2)
 287                             cantremove.remove(gn2);
 288                     }
 289                 }
 290                 if (!foundcompensation) {
 291                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 292                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 293                         GraphNode gn2=e.getTarget();
 294                         TermNode tn2=(TermNode)gn2.getOwner();
 295                         if (tn2.getType()==TermNode.UPDATE) {
 296                             cantremove.add(gn2);
 297                             break;
 298                         }
 299                     }
 300                 }
 301             }
 302             couldremove.removeAll(mustremove);
 303             couldremove.removeAll(cantremove);
 304
 305             Vector couldremovevector=new Vector();
 306             couldremovevector.addAll(couldremove);
 307             Vector combination=new Vector();
 308             if(change)
 309                 continue; //recalculate
 310
 311             try {
 312                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
 313             } catch (Exception e) {
 314                 e.printStackTrace();
 315                 System.exit(-1);
 316             }
 317
 318             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 319             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 320             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 321             System.out.println("Searching following set:");
 322             for(Iterator it=couldremove.iterator();it.hasNext();) {
 323                 GraphNode gn=(GraphNode)it.next();
 324                 System.out.println(gn.getTextLabel());
 325             }
 326
 327
 328             while(true) {
 329                 if (illegal(combination,couldremovevector))
 330                     break;
 331                 Set combinationset=buildset(combination,couldremovevector);
 332                 checkmodify(combinationset);
 333                 combinationset.addAll(mustremove);
 334                 if (combinationset!=null) {
 335                     System.out.println("Checkabstract="+checkAbstract(combinationset));
 336                     System.out.println("Checkrepairs="+checkRepairs(combinationset));
 337                     System.out.println("Checkall="+checkAll(combinationset));
 338
 339                     if (checkAbstract(combinationset)==0&&
 340                         checkRepairs(combinationset)==0&&
 341                         checkAll(combinationset)==0) {
 342                         return combinationset;
 343                     }
 344                 }
 345                 increment(combination,couldremovevector);
 346             }
 347             return null;
 348         }
 349     }
 350
 351     private void checkmodify(Set removednodes) {
 352         for (Iterator it=removednodes.iterator();it.hasNext();) {
 353             GraphNode gn=(GraphNode)it.next();
 354             TermNode tn=(TermNode)gn.getOwner();
 355             if (tn.getType()==TermNode.ABSTRACT) {
 356                 AbstractRepair ar=tn.getAbstract();
 357                 DNFPredicate dpred=ar.getPredicate();
 358                 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
 359                 /* Has MODIFYRELATION */
 360                 if (containsmodify(repairnodes)&&
 361                     (repairnodes.size()>1)&&
 362                     (ar.getType()==AbstractRepair.REMOVEFROMRELATION||
 363                      ar.getType()==AbstractRepair.ADDTORELATION)) {
 364                     for(Iterator it2=repairnodes.iterator();it2.hasNext();) {
 365                         GraphNode gn2=(GraphNode)it2.next();
 366                         TermNode tn2=(TermNode)gn2.getOwner();
 367                         AbstractRepair ar2=tn2.getAbstract();
 368                         if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION||
 369                             ar2.getType()==AbstractRepair.ADDTORELATION) {
 370                             removednodes.add(gn2);
 371                         }
 372                     }
 373                 }
 374             }
 375         }
 376     }
 377
 378     private static boolean containsmodify(Set repairnodes) {
 379         for (Iterator it=repairnodes.iterator();it.hasNext();) {
 380             GraphNode gn=(GraphNode) it.next();
 381             TermNode tn=(TermNode)gn.getOwner();
 382             AbstractRepair ar=tn.getAbstract();
 383             if (ar.getType()==AbstractRepair.MODIFYRELATION)
 384                 return true;
 385         }
 386         return false;
 387     }
 388
 389     private static Set buildset(Vector combination, Vector couldremove) {
 390         Set s=new HashSet();
 391         for(int i=0;i<combination.size();i++) {
 392             int index=((Integer)combination.get(i)).intValue();
 393             Object o=couldremove.get(index);
 394             if (s.contains(o))
 395                 return null;
 396             else
 397                 s.add(o);
 398         }
 399         return s;
 400     }
 401
 402     private static boolean illegal(Vector combination, Vector couldremove) {
 403         if (combination.size()>couldremove.size())
 404             return true;
 405         else return false;
 406     }
 407     private static void increment(Vector combination, Vector couldremove) {
 408         boolean incremented=false;
 409         boolean forcereset=false;
 410         for(int i=0;i<combination.size();i++) {
 411             int newindex=((Integer)combination.get(i)).intValue()+1;
 412             if (newindex==couldremove.size()||forcereset) {
 413                 forcereset=false;
 414                 if ((i+1)==combination.size()) {
 415                     newindex=1;
 416                 } else
 417                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 418                 for(int j=i;j>=0;j--) {
 419                     combination.set(j,new Integer(newindex));
 420                     newindex++;
 421                 }
 422                 if (newindex>couldremove.size())
 423                     forcereset=true;
 424             } else {
 425                 incremented=true;
 426                 combination.set(i,new Integer(newindex));
 427                 break;
 428             }
 429         }
 430         if (incremented==false) /* Increase length */ {
 431             combination.add(new Integer(0));
 432             System.out.println("Expanding to :"+combination.size());
 433         }
 434     }
 435
 436     /* This function checks the graph as a whole for bad cycles */
 437     public int checkAll(Collection removed) {
 438         Set nodes=new HashSet();
 439         nodes.addAll(termination.conjunctions);
 440         nodes.removeAll(removed);
 441         GraphNode.computeclosure(nodes,removed);
 442         Set cycles=GraphNode.findcycles(nodes);
 443         for(Iterator it=cycles.iterator();it.hasNext();) {
 444             GraphNode gn=(GraphNode)it.next();
 445             TermNode tn=(TermNode)gn.getOwner();
 446             switch(tn.getType()) {
 447             case TermNode.UPDATE:
 448             case TermNode.CONJUNCTION:
 449                 return ERR_CYCLE;
 450             case TermNode.ABSTRACT:
 451             case TermNode.RULESCOPE:
 452             case TermNode.CONSEQUENCE:
 453             default:
 454                 break;
 455             }
 456         }
 457         return WORKS;
 458     }
 459
 460     /* This function checks that
 461        1) All abstract repairs have a corresponding data structure update
 462           that isn't removed.
 463        2) All scope nodes have either a consequence node or a compensation
 464           node that isn't removed.
 465      */
 466     public int checkRepairs(Collection removed) {
 467         Set nodes=new HashSet();
 468         nodes.addAll(termination.conjunctions);
 469         nodes.removeAll(removed);
 470         GraphNode.computeclosure(nodes,removed);
 471         Set toretain=new HashSet();
 472         toretain.addAll(termination.abstractrepair);
 473         toretain.addAll(termination.scopenodes);
 474         nodes.retainAll(toretain);
 475         /* Nodes is now the reachable set of abstractrepairs */
 476         /* Check to see that each has an implementation */
 477         for(Iterator it=nodes.iterator();it.hasNext();) {
 478             GraphNode gn=(GraphNode)it.next();
 479             TermNode tn=(TermNode)gn.getOwner();
 480             if (tn.getType()==TermNode.RULESCOPE) {
 481                 boolean foundnode=false;
 482                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 483                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 484                     GraphNode gn2=edge.getTarget();
 485                     if (!removed.contains(gn2)) {
 486                         TermNode tn2=(TermNode)gn2.getOwner();
 487                         if ((tn2.getType()==TermNode.CONSEQUENCE)||
 488                             (tn2.getType()==TermNode.UPDATE)) {
 489                             foundnode=true;
 490                             break;
 491                         }
 492                     }
 493                 }
 494                 if (!foundnode) {
 495                     System.out.println(gn.getTextLabel());
 496                     return ERR_RULE;
 497                 }
 498             } else if (tn.getType()==TermNode.ABSTRACT) {
 499                 boolean foundnode=false;
 500                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 501                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 502                     GraphNode gn2=edge.getTarget();
 503                     if (!removed.contains(gn2)) {
 504                         TermNode tn2=(TermNode)gn2.getOwner();
 505                         if (tn2.getType()==TermNode.UPDATE) {
 506                             foundnode=true;
 507                             break;
 508                         }
 509                     }
 510                 }
 511                 if (!foundnode)
 512                     return ERR_ABSTRACT;
 513             } else throw new Error("Unanticipated Node");
 514         }
 515         return WORKS;
 516     }
 517     /* This method checks that all constraints have conjunction nodes
 518        and that there are no bad cycles in the abstract portion of the graph.
 519      */
 520     public int checkAbstract(Collection removed) {
 521         Vector constraints=termination.state.vConstraints;
 522         for(int i=0;i<constraints.size();i++) {
 523             Constraint c=(Constraint)constraints.get(i);
 524             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 525
 526             boolean foundrepair=false;
 527             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 528                 GraphNode gn=(GraphNode)it.next();
 529                 if (!removed.contains(gn)) {
 530                     foundrepair=true;
 531                     for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 532                         GraphNode.Edge edge=(GraphNode.Edge) edgeit.next();
 533                         GraphNode gn2=edge.getTarget();
 534                         TermNode tn2=(TermNode) gn2.getOwner();
 535                         if (tn2.getType()==TermNode.ABSTRACT) {
 536                             /* Abstract node */
 537                             AbstractRepair ar=tn2.getAbstract();
 538                             DNFPredicate dpred=ar.getPredicate();
 539                             Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
 540                             if (containsmodify(repairnodes)&&
 541                                 (repairnodes.size()>1)) {
 542                                 HashSet retainednodes=new HashSet();
 543                                 retainednodes.addAll(repairnodes);
 544                                 retainednodes.removeAll(removed);
 545                                 if (!containsmodify(retainednodes)&&
 546                                     (retainednodes.size()<2))
 547                                     return ERR_NOREPAIR;
 548                             } else if (removed.contains(gn2))
 549                                 return ERR_NOREPAIR;
 550                         }
 551                     }
 552                 }
 553             }
 554             if (!foundrepair)
 555                 return ERR_NOREPAIR;
 556         }
 557         Set abstractnodes=new HashSet();
 558         abstractnodes.addAll(termination.conjunctions);
 559         abstractnodes.removeAll(removed);
 560         GraphNode.computeclosure(abstractnodes,removed);
 561
 562         Set tset=new HashSet();
 563         tset.addAll(termination.conjunctions);
 564         tset.addAll(termination.abstractrepair);
 565         tset.addAll(termination.scopenodes);
 566         tset.addAll(termination.consequencenodes);
 567         abstractnodes.retainAll(tset);
 568         Set cycles=GraphNode.findcycles(abstractnodes);
 569
 570         for(Iterator it=cycles.iterator();it.hasNext();) {
 571             GraphNode gn=(GraphNode)it.next();
 572             System.out.println("NODE: "+gn.getTextLabel());
 573             TermNode tn=(TermNode)gn.getOwner();
 574             switch(tn.getType()) {
 575             case TermNode.CONJUNCTION:
 576             case TermNode.ABSTRACT:
 577                 return ERR_CYCLE;
 578             case TermNode.UPDATE:
 579                 throw new Error("No Update Nodes should be here");
 580             default:
 581             }
 582         }
 583         return WORKS;
 584     }
 585 }