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