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(cycles);
  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                     System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
 118                     return null; // Out of luck
 119                 }
 120             }
 121
 122             /* Search through abstract repair actions & correspond data structure updates */
 123             for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
 124                 GraphNode gn=(GraphNode)it.next();
 125                 TermNode tn=(TermNode)gn.getOwner();
 126
 127                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 128                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 129                     GraphNode gn2=e.getTarget();
 130                     TermNode tn2=(TermNode)gn2.getOwner();
 131                     if (tn2.getType()!=TermNode.UPDATE)
 132                         continue;
 133
 134                     boolean containsgn=cantremove.contains(gn);
 135                     boolean containsgn2=cantremove.contains(gn2);
 136
 137                     cantremove.add(gn);
 138                     cantremove.add(gn2);
 139
 140                     Set cycle=GraphNode.findcycles(cantremove);
 141                     if (cycle.contains(gn2)) {
 142                         if (!mustremove.contains(gn2)) {
 143                             change=true;
 144                             mustremove.add(gn2);
 145                         }
 146                     }
 147                     if (!containsgn)
 148                         cantremove.remove(gn);
 149                     if (!containsgn2)
 150                         cantremove.remove(gn2);
 151                 }
 152             }
 153
 154             /* Searches individual conjunctions + abstract action +updates for cycles */
 155             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 156                 GraphNode gn=(GraphNode)it.next();
 157                 boolean foundnocycle=false;
 158
 159                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 160                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 161                     GraphNode gn2=e.getTarget();
 162                     TermNode tn2=(TermNode)gn2.getOwner();
 163                     if (tn2.getType()!=TermNode.ABSTRACT)
 164                         continue;
 165                     AbstractRepair ar=tn2.getAbstract();
 166                     boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 167                     int numadd=0;int numremove=0;
 168
 169                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 170                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 171                         GraphNode gn3=e2.getTarget();
 172                         TermNode tn3=(TermNode)gn3.getOwner();
 173                         if (tn3.getType()!=TermNode.UPDATE)
 174                             continue;
 175
 176                         boolean containsgn=cantremove.contains(gn);
 177                         boolean containsgn2=cantremove.contains(gn2);
 178                         boolean containsgn3=cantremove.contains(gn3);
 179                         cantremove.add(gn);
 180                         cantremove.add(gn2);
 181                         cantremove.add(gn3);
 182                         Set cycle=GraphNode.findcycles(cantremove);
 183                         if (cycle.contains(gn3)) {
 184                             if (!mustremove.contains(gn3)) {
 185                                 change=true;
 186                                 mustremove.add(gn3);
 187                             }
 188                         }
 189                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 190                             foundnocycle=true;
 191                             if (ismodify) {
 192                                 MultUpdateNode mun=tn3.getUpdate();
 193                                 if (mun.getType()==MultUpdateNode.ADD)
 194                                     numadd++;
 195                                 if (mun.getType()==MultUpdateNode.REMOVE)
 196                                     numremove++;
 197                             }
 198                         }
 199                         if (!containsgn)
 200                             cantremove.remove(gn);
 201                         if (!containsgn2)
 202                             cantremove.remove(gn2);
 203                         if (!containsgn3)
 204                             cantremove.remove(gn3);
 205                     }
 206                     if (ismodify&&((numadd==0)||(numremove==0))) {
 207                         for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 208                             GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 209                             GraphNode gn3=e2.getTarget();
 210                             TermNode tn3=(TermNode)gn3.getOwner();
 211                             if (tn3.getType()!=TermNode.UPDATE)
 212                                 continue;
 213                             MultUpdateNode mun=tn3.getUpdate();
 214                             if (((mun.getType()==MultUpdateNode.ADD)||
 215                                 (mun.getType()==MultUpdateNode.REMOVE))&&
 216                                 (!mustremove.contains(gn3)))
 217                                 mustremove.add(gn3);
 218                         }
 219                     }
 220                 }
 221
 222                 if(!foundnocycle) {
 223                     if (!mustremove.contains(gn)) {
 224                         change=true;
 225                         mustremove.add(gn);
 226                     }
 227                 }
 228             }
 229
 230             /* Searches scope nodes + compensation nodes */
 231             for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 232                 GraphNode gn=(GraphNode)it.next();
 233                 boolean foundcompensation=false;
 234                 if (nodes.contains(gn)) {
 235                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 236                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 237                         GraphNode gn2=e.getTarget();
 238                         TermNode tn2=(TermNode)gn2.getOwner();
 239
 240                         if (tn2.getType()!=TermNode.UPDATE)
 241                             continue;
 242                         /* We have a compensation node */
 243                         boolean containsgn=cantremove.contains(gn);
 244                         boolean containsgn2=cantremove.contains(gn2);
 245                         cantremove.add(gn);
 246                         cantremove.add(gn2);
 247
 248                         Set cycle=GraphNode.findcycles(cantremove);
 249                         if (cycle.contains(gn2)) {
 250                             if (!mustremove.contains(gn2)) {
 251                                 change=true;
 252                                 mustremove.add(gn2);
 253                             }
 254                         } else {
 255                             if (!mustremove.contains(gn2))
 256                                 foundcompensation=true;
 257                         }
 258                         if (!containsgn)
 259                             cantremove.remove(gn);
 260                         if (!containsgn2)
 261                             cantremove.remove(gn2);
 262                     }
 263                 }
 264                 if (!foundcompensation) {
 265                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 266                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 267                         GraphNode gn2=e.getTarget();
 268                         TermNode tn2=(TermNode)gn2.getOwner();
 269                         if (tn2.getType()==TermNode.UPDATE) {
 270                             cantremove.add(gn2);
 271                             break;
 272                         }
 273                     }
 274                 }
 275             }
 276             couldremove.removeAll(mustremove);
 277             couldremove.removeAll(cantremove);
 278
 279             Vector couldremovevector=new Vector();
 280             couldremovevector.addAll(couldremove);
 281             Vector combination=new Vector();
 282             if(change)
 283                 continue; //recalculate
 284
 285             try {
 286                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
 287             } catch (Exception e) {
 288                 e.printStackTrace();
 289                 System.exit(-1);
 290             }
 291
 292             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 293             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 294             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 295             System.out.println("Searching following set:");
 296             for(Iterator it=couldremove.iterator();it.hasNext();) {
 297                 GraphNode gn=(GraphNode)it.next();
 298                 System.out.println(gn.getTextLabel());
 299             }
 300
 301
 302             while(true) {
 303                 if (illegal(combination,couldremovevector))
 304                     break;
 305                 Set combinationset=buildset(combination,couldremovevector);
 306                 checkmodify(combinationset);
 307                 combinationset.addAll(mustremove);
 308                 if (combinationset!=null) {
 309                     System.out.println("Checkabstract="+checkAbstract(combinationset));
 310                     System.out.println("Checkrepairs="+checkRepairs(combinationset));
 311                     System.out.println("Checkall="+checkAll(combinationset));
 312
 313                     if (checkAbstract(combinationset)==0&&
 314                         checkRepairs(combinationset)==0&&
 315                         checkAll(combinationset)==0) {
 316                         return combinationset;
 317                     }
 318                 }
 319                 increment(combination,couldremovevector);
 320             }
 321             System.out.println("Search failed!");
 322             return null;
 323         }
 324     }
 325
 326     private void checkmodify(Set removednodes) {
 327         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
 328             GraphNode gn=(GraphNode)it.next();
 329             TermNode tn=(TermNode)gn.getOwner();
 330             AbstractRepair ar=tn.getAbstract();
 331
 332             /* Has MODIFYRELATION */
 333             if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 334                 int numadd=0;
 335                 int numremove=0;
 336                 for(Iterator it2=gn.edges();it2.hasNext();) {
 337                     GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 338                     GraphNode gn2=edge.getTarget();
 339                     TermNode tn2=(TermNode)gn2.getOwner();
 340                     if (!removednodes.contains(gn2)&&
 341                         tn2.getType()==TermNode.UPDATE) {
 342                         MultUpdateNode mun=tn2.getUpdate();
 343
 344                         if (mun.getType()==MultUpdateNode.ADD)
 345                             numadd++;
 346                         if (mun.getType()==MultUpdateNode.REMOVE)
 347                             numremove++;
 348                     }
 349                 }
 350                 if ((numadd==0)||(numremove==0)) {
 351                     for(Iterator it2=gn.edges();it2.hasNext();) {
 352                         GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 353                         GraphNode gn2=edge.getTarget();
 354                         TermNode tn2=(TermNode)gn2.getOwner();
 355                         if (!removednodes.contains(gn2)&&
 356                             tn2.getType()==TermNode.UPDATE) {
 357                             MultUpdateNode mun=tn2.getUpdate();
 358                             if ((mun.getType()==MultUpdateNode.ADD)
 359                                 ||(mun.getType()==MultUpdateNode.REMOVE)) {
 360                                 removednodes.add(gn2);
 361                             }
 362                         }
 363                     }
 364                 }
 365             }
 366         }
 367     }
 368
 369     private static Set buildset(Vector combination, Vector couldremove) {
 370         Set s=new HashSet();
 371         for(int i=0;i<combination.size();i++) {
 372             int index=((Integer)combination.get(i)).intValue();
 373             Object o=couldremove.get(index);
 374             if (s.contains(o))
 375                 return null;
 376             else
 377                 s.add(o);
 378         }
 379         return s;
 380     }
 381
 382     private static boolean illegal(Vector combination, Vector couldremove) {
 383         if (combination.size()>couldremove.size())
 384             return true;
 385         else return false;
 386     }
 387     private static void increment(Vector combination, Vector couldremove) {
 388         boolean incremented=false;
 389         boolean forcereset=false;
 390         for(int i=0;i<combination.size();i++) {
 391             int newindex=((Integer)combination.get(i)).intValue()+1;
 392             if (newindex==couldremove.size()||forcereset) {
 393                 forcereset=false;
 394                 if ((i+1)==combination.size()) {
 395                     newindex=1;
 396                 } else
 397                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 398                 for(int j=i;j>=0;j--) {
 399                     combination.set(j,new Integer(newindex));
 400                     newindex++;
 401                 }
 402                 if (newindex>couldremove.size())
 403                     forcereset=true;
 404             } else {
 405                 incremented=true;
 406                 combination.set(i,new Integer(newindex));
 407                 break;
 408             }
 409         }
 410         if (incremented==false) /* Increase length */ {
 411             combination.add(new Integer(0));
 412             System.out.println("Expanding to :"+combination.size());
 413         }
 414     }
 415
 416     /* This function checks the graph as a whole for bad cycles */
 417     public int checkAll(Collection removed) {
 418         Set nodes=new HashSet();
 419         nodes.addAll(termination.conjunctions);
 420         nodes.removeAll(removed);
 421         GraphNode.computeclosure(nodes,removed);
 422         Set cycles=GraphNode.findcycles(nodes);
 423         for(Iterator it=cycles.iterator();it.hasNext();) {
 424             GraphNode gn=(GraphNode)it.next();
 425             TermNode tn=(TermNode)gn.getOwner();
 426             switch(tn.getType()) {
 427             case TermNode.UPDATE:
 428             case TermNode.CONJUNCTION:
 429                 return ERR_CYCLE;
 430             case TermNode.ABSTRACT:
 431             case TermNode.RULESCOPE:
 432             case TermNode.CONSEQUENCE:
 433             default:
 434                 break;
 435             }
 436         }
 437         return WORKS;
 438     }
 439
 440     /* This function checks that
 441        1) All abstract repairs have a corresponding data structure update
 442           that isn't removed.
 443        2) All scope nodes have either a consequence node or a compensation
 444           node that isn't removed.
 445      */
 446     public int checkRepairs(Collection removed) {
 447         Set nodes=new HashSet();
 448         nodes.addAll(termination.conjunctions);
 449         nodes.removeAll(removed);
 450         GraphNode.computeclosure(nodes,removed);
 451         Set toretain=new HashSet();
 452         toretain.addAll(termination.abstractrepair);
 453         toretain.addAll(termination.scopenodes);
 454         nodes.retainAll(toretain);
 455         /* Nodes is now the reachable set of abstractrepairs */
 456         /* Check to see that each has an implementation */
 457         for(Iterator it=nodes.iterator();it.hasNext();) {
 458             GraphNode gn=(GraphNode)it.next();
 459             TermNode tn=(TermNode)gn.getOwner();
 460             if (tn.getType()==TermNode.RULESCOPE) {
 461                 boolean foundnode=false;
 462                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 463                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 464                     GraphNode gn2=edge.getTarget();
 465                     if (!removed.contains(gn2)) {
 466                         TermNode tn2=(TermNode)gn2.getOwner();
 467                         if ((tn2.getType()==TermNode.CONSEQUENCE)||
 468                             (tn2.getType()==TermNode.UPDATE)) {
 469                             foundnode=true;
 470                             break;
 471                         }
 472                     }
 473                 }
 474                 if (!foundnode) {
 475                     System.out.println(gn.getTextLabel());
 476                     return ERR_RULE;
 477                 }
 478             } else if (tn.getType()==TermNode.ABSTRACT) {
 479                 boolean foundnode=false;
 480                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 481                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 482                     GraphNode gn2=edge.getTarget();
 483                     if (!removed.contains(gn2)) {
 484                         TermNode tn2=(TermNode)gn2.getOwner();
 485                         if (tn2.getType()==TermNode.UPDATE) {
 486                             foundnode=true;
 487                             break;
 488                         }
 489                     }
 490                 }
 491                 if (!foundnode)
 492                     return ERR_ABSTRACT;
 493             } else throw new Error("Unanticipated Node");
 494         }
 495         return WORKS;
 496     }
 497     /* This method checks that all constraints have conjunction nodes
 498        and that there are no bad cycles in the abstract portion of the graph.
 499      */
 500     public int checkAbstract(Collection removed) {
 501         Vector constraints=termination.state.vConstraints;
 502         for(int i=0;i<constraints.size();i++) {
 503             Constraint c=(Constraint)constraints.get(i);
 504             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 505
 506             boolean foundrepair=false;
 507             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 508                 GraphNode gn=(GraphNode)it.next();
 509                 if (!removed.contains(gn)) {
 510                     foundrepair=true;
 511                 }
 512             }
 513             if (!foundrepair)
 514                 return ERR_NOREPAIR;
 515         }
 516
 517
 518         Set abstractnodes=new HashSet();
 519         abstractnodes.addAll(termination.conjunctions);
 520         abstractnodes.removeAll(removed);
 521         GraphNode.computeclosure(abstractnodes,removed);
 522
 523         Set tset=new HashSet();
 524         tset.addAll(termination.conjunctions);
 525         tset.addAll(termination.abstractrepair);
 526         tset.addAll(termination.scopenodes);
 527         tset.addAll(termination.consequencenodes);
 528         abstractnodes.retainAll(tset);
 529         Set cycles=GraphNode.findcycles(abstractnodes);
 530
 531         for(Iterator it=cycles.iterator();it.hasNext();) {
 532             GraphNode gn=(GraphNode)it.next();
 533             System.out.println("NODE: "+gn.getTextLabel());
 534             TermNode tn=(TermNode)gn.getOwner();
 535             switch(tn.getType()) {
 536             case TermNode.CONJUNCTION:
 537             case TermNode.ABSTRACT:
 538                 return ERR_CYCLE;
 539             case TermNode.UPDATE:
 540                 throw new Error("No Update Nodes should be here");
 541             default:
 542             }
 543         }
 544         return WORKS;
 545     }
 546 }