Repair/RepairCompiler/MCC/IR/GraphAnalysis.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import MCC.State;
   4
   5 public class GraphAnalysis {
   6     Termination termination;
   7     static final int WORKS=0;
   8     static final int ERR_NOREPAIR=1;
   9     static final int ERR_CYCLE=2;
  10     static final int ERR_RULE=3;
  11     static final int ERR_ABSTRACT=4;
  12
  13     public GraphAnalysis(Termination t) {
  14         termination=t;
  15     }
  16
  17     public Set doAnalysis() {
  18         HashSet cantremove=new HashSet();
  19         HashSet mustremove=new HashSet();
  20         HashSet optionalabstractrepair=new HashSet();
  21
  22         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
  23             GraphNode gn=(GraphNode)it.next();
  24             TermNode tn=(TermNode)gn.getOwner();
  25             AbstractRepair ar=tn.getAbstract();
  26             DNFPredicate dpred=ar.getPredicate();
  27             Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
  28             if ((repairnodes.size()>1)&&
  29                 containsmodify(repairnodes)) {
  30                 optionalabstractrepair.add(gn);
  31             }
  32         }
  33
  34         cantremove.addAll(termination.scopenodes);
  35         cantremove.addAll(termination.abstractrepair);
  36         cantremove.removeAll(optionalabstractrepair);
  37
  38         while(true) {
  39             boolean change=false;
  40             HashSet nodes=new HashSet();
  41             nodes.addAll(termination.conjunctions);
  42             nodes.removeAll(mustremove);
  43             GraphNode.computeclosure(nodes,mustremove);
  44             Set cycles=GraphNode.findcycles(nodes);
  45             Set couldremove=new HashSet();
  46             couldremove.addAll(termination.conjunctions);
  47             couldremove.addAll(termination.updatenodes);
  48             couldremove.addAll(termination.consequencenodes);
  49             couldremove.addAll(optionalabstractrepair);
  50             couldremove.retainAll(cycles);
  51
  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
 175             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 176                 GraphNode gn=(GraphNode)it.next();
 177                 boolean foundnocycle=false;
 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.ABSTRACT)
 184                         continue;
 185                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 186                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 187                         GraphNode gn3=e2.getTarget();
 188                         TermNode tn3=(TermNode)gn3.getOwner();
 189                         if (tn3.getType()!=TermNode.UPDATE)
 190                             continue;
 191                         boolean containsgn=cantremove.contains(gn);
 192                         boolean containsgn3=cantremove.contains(gn3);
 193                         cantremove.add(gn);
 194                         cantremove.add(gn3);
 195                         Set cycle=GraphNode.findcycles(cantremove);
 196                         if (cycle.contains(gn3)) {
 197                             if (!mustremove.contains(gn3)) {
 198                                 change=true;
 199                                 mustremove.add(gn3);
 200                             }
 201                         }
 202                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 203                             foundnocycle=true;
 204                         }
 205                         if (!containsgn)
 206                             cantremove.remove(gn);
 207                         if (!containsgn3)
 208                             cantremove.remove(gn3);
 209                     }
 210                 }
 211                 if(!foundnocycle) {
 212                     if (!mustremove.contains(gn)) {
 213                         change=true;
 214                         mustremove.add(gn);
 215                     }
 216                 }
 217             }
 218             couldremove.removeAll(mustremove);
 219             couldremove.removeAll(cantremove);
 220
 221             Vector couldremovevector=new Vector();
 222             couldremovevector.addAll(couldremove);
 223             Vector combination=new Vector();
 224             if(change)
 225                 continue; //recalculate
 226
 227             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 228             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 229             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 230             System.out.println("Searching following set:");
 231             for(Iterator it=couldremove.iterator();it.hasNext();) {
 232                 GraphNode gn=(GraphNode)it.next();
 233                 System.out.println(gn.getTextLabel());
 234             }
 235
 236
 237             while(true) {
 238                 if (illegal(combination,couldremovevector))
 239                     break;
 240                 Set combinationset=buildset(combination,couldremovevector);
 241                 checkmodify(combinationset);
 242                 combinationset.addAll(mustremove);
 243                 if (combinationset!=null) {
 244                     System.out.println("Checkabstract="+checkAbstract(combinationset));
 245                     System.out.println("Checkrepairs="+checkRepairs(combinationset));
 246                     System.out.println("Checkall="+checkAll(combinationset));
 247
 248                     if (checkAbstract(combinationset)==0&&
 249                         checkRepairs(combinationset)==0&&
 250                         checkAll(combinationset)==0) {
 251                         return combinationset;
 252                     }
 253                 }
 254                 increment(combination,couldremovevector);
 255             }
 256             return null;
 257         }
 258     }
 259
 260     private void checkmodify(Set removednodes) {
 261         for (Iterator it=removednodes.iterator();it.hasNext();) {
 262             GraphNode gn=(GraphNode)it.next();
 263             TermNode tn=(TermNode)gn.getOwner();
 264             if (tn.getType()==TermNode.ABSTRACT) {
 265                 AbstractRepair ar=tn.getAbstract();
 266                 DNFPredicate dpred=ar.getPredicate();
 267                 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
 268                 /* Has MODIFYRELATION */
 269                 if (containsmodify(repairnodes)&&
 270                     (repairnodes.size()>1)&&
 271                     (ar.getType()==AbstractRepair.REMOVEFROMRELATION||
 272                      ar.getType()==AbstractRepair.ADDTORELATION)) {
 273                     for(Iterator it2=repairnodes.iterator();it2.hasNext();) {
 274                         GraphNode gn2=(GraphNode)it2.next();
 275                         TermNode tn2=(TermNode)gn2.getOwner();
 276                         AbstractRepair ar2=tn2.getAbstract();
 277                         if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION||
 278                             ar2.getType()==AbstractRepair.ADDTORELATION) {
 279                             removednodes.add(gn2);
 280                         }
 281                     }
 282                 }
 283             }
 284         }
 285     }
 286
 287     private static boolean containsmodify(Set repairnodes) {
 288         for (Iterator it=repairnodes.iterator();it.hasNext();) {
 289             GraphNode gn=(GraphNode) it.next();
 290             TermNode tn=(TermNode)gn.getOwner();
 291             AbstractRepair ar=tn.getAbstract();
 292             if (ar.getType()==AbstractRepair.MODIFYRELATION)
 293                 return true;
 294         }
 295         return false;
 296     }
 297
 298     private static Set buildset(Vector combination, Vector couldremove) {
 299         Set s=new HashSet();
 300         for(int i=0;i<combination.size();i++) {
 301             int index=((Integer)combination.get(i)).intValue();
 302             Object o=couldremove.get(index);
 303             if (s.contains(o))
 304                 return null;
 305             else
 306                 s.add(o);
 307         }
 308         return s;
 309     }
 310
 311     private static boolean illegal(Vector combination, Vector couldremove) {
 312         if (combination.size()>couldremove.size())
 313             return true;
 314         else return false;
 315     }
 316     private static void increment(Vector combination, Vector couldremove) {
 317         boolean incremented=false;
 318         boolean forcereset=false;
 319         for(int i=0;i<combination.size();i++) {
 320             int newindex=((Integer)combination.get(i)).intValue()+1;
 321             if (newindex==couldremove.size()||forcereset) {
 322                 forcereset=false;
 323                 if ((i+1)==combination.size()) {
 324                     newindex=1;
 325                 } else
 326                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 327                 for(int j=i;j>=0;j--) {
 328                     combination.set(j,new Integer(newindex));
 329                     newindex++;
 330                 }
 331                 if (newindex>couldremove.size())
 332                     forcereset=true;
 333             } else {
 334                 incremented=true;
 335                 combination.set(i,new Integer(newindex));
 336                 break;
 337             }
 338         }
 339         if (incremented==false) /* Increase length */ {
 340             combination.add(new Integer(0));
 341             System.out.println("Expanding to :"+combination.size());
 342         }
 343     }
 344
 345     /* This function checks the graph as a whole for bad cycles */
 346     public int checkAll(Collection removed) {
 347         Set nodes=new HashSet();
 348         nodes.addAll(termination.conjunctions);
 349         nodes.removeAll(removed);
 350         GraphNode.computeclosure(nodes,removed);
 351         Set cycles=GraphNode.findcycles(nodes);
 352         for(Iterator it=cycles.iterator();it.hasNext();) {
 353             GraphNode gn=(GraphNode)it.next();
 354             TermNode tn=(TermNode)gn.getOwner();
 355             switch(tn.getType()) {
 356             case TermNode.UPDATE:
 357             case TermNode.CONJUNCTION:
 358                 return ERR_CYCLE;
 359             case TermNode.ABSTRACT:
 360             case TermNode.RULESCOPE:
 361             case TermNode.CONSEQUENCE:
 362             default:
 363                 break;
 364             }
 365         }
 366         return WORKS;
 367     }
 368
 369     /* This function checks that
 370        1) All abstract repairs have a corresponding data structure update
 371           that isn't removed.
 372        2) All scope nodes have either a consequence node or a compensation
 373           node that isn't removed.
 374      */
 375     public int checkRepairs(Collection removed) {
 376         Set nodes=new HashSet();
 377         nodes.addAll(termination.conjunctions);
 378         nodes.removeAll(removed);
 379         GraphNode.computeclosure(nodes,removed);
 380         Set toretain=new HashSet();
 381         toretain.addAll(termination.abstractrepair);
 382         toretain.addAll(termination.scopenodes);
 383         nodes.retainAll(toretain);
 384         /* Nodes is now the reachable set of abstractrepairs */
 385         /* Check to see that each has an implementation */
 386         for(Iterator it=nodes.iterator();it.hasNext();) {
 387             GraphNode gn=(GraphNode)it.next();
 388             TermNode tn=(TermNode)gn.getOwner();
 389             if (tn.getType()==TermNode.RULESCOPE) {
 390                 boolean foundnode=false;
 391                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 392                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 393                     GraphNode gn2=edge.getTarget();
 394                     if (!removed.contains(gn2)) {
 395                         TermNode tn2=(TermNode)gn2.getOwner();
 396                         if ((tn2.getType()==TermNode.CONSEQUENCE)||
 397                             (tn2.getType()==TermNode.UPDATE)) {
 398                             foundnode=true;
 399                             break;
 400                         }
 401                     }
 402                 }
 403                 if (!foundnode) {
 404                     System.out.println(gn.getTextLabel());
 405                     return ERR_RULE;
 406                 }
 407             } else if (tn.getType()==TermNode.ABSTRACT) {
 408                 boolean foundnode=false;
 409                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 410                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 411                     GraphNode gn2=edge.getTarget();
 412                     if (!removed.contains(gn2)) {
 413                         TermNode tn2=(TermNode)gn2.getOwner();
 414                         if (tn2.getType()==TermNode.UPDATE) {
 415                             foundnode=true;
 416                             break;
 417                         }
 418                     }
 419                 }
 420                 if (!foundnode)
 421                     return ERR_ABSTRACT;
 422             } else throw new Error("Unanticipated Node");
 423         }
 424         return WORKS;
 425     }
 426     /* This method checks that all constraints have conjunction nodes
 427        and that there are no bad cycles in the abstract portion of the graph.
 428      */
 429     public int checkAbstract(Collection removed) {
 430         Vector constraints=termination.state.vConstraints;
 431         for(int i=0;i<constraints.size();i++) {
 432             Constraint c=(Constraint)constraints.get(i);
 433             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 434
 435             boolean foundrepair=false;
 436             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 437                 GraphNode gn=(GraphNode)it.next();
 438                 if (!removed.contains(gn)) {
 439                     foundrepair=true;
 440                     for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 441                         GraphNode.Edge edge=(GraphNode.Edge) edgeit.next();
 442                         GraphNode gn2=edge.getTarget();
 443                         TermNode tn2=(TermNode) gn2.getOwner();
 444                         if (tn2.getType()==TermNode.ABSTRACT) {
 445                             /* Abstract node */
 446                             AbstractRepair ar=tn2.getAbstract();
 447                             DNFPredicate dpred=ar.getPredicate();
 448                             Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
 449                             if (containsmodify(repairnodes)&&
 450                                 (repairnodes.size()>1)) {
 451                                 HashSet retainednodes=new HashSet();
 452                                 retainednodes.addAll(repairnodes);
 453                                 retainednodes.removeAll(removed);
 454                                 if (!containsmodify(retainednodes)&&
 455                                     (retainednodes.size()<2))
 456                                     return ERR_NOREPAIR;
 457                             } else if (removed.contains(gn2))
 458                                 return ERR_NOREPAIR;
 459                         }
 460                     }
 461                 }
 462             }
 463             if (!foundrepair)
 464                 return ERR_NOREPAIR;
 465         }
 466         Set abstractnodes=new HashSet();
 467         abstractnodes.addAll(termination.conjunctions);
 468         abstractnodes.removeAll(removed);
 469         GraphNode.computeclosure(abstractnodes,removed);
 470
 471         Set tset=new HashSet();
 472         tset.addAll(termination.conjunctions);
 473         tset.addAll(termination.abstractrepair);
 474         tset.addAll(termination.scopenodes);
 475         tset.addAll(termination.consequencenodes);
 476         abstractnodes.retainAll(tset);
 477         Set cycles=GraphNode.findcycles(abstractnodes);
 478
 479         for(Iterator it=cycles.iterator();it.hasNext();) {
 480             GraphNode gn=(GraphNode)it.next();
 481             System.out.println("NODE: "+gn.getTextLabel());
 482             TermNode tn=(TermNode)gn.getOwner();
 483             switch(tn.getType()) {
 484             case TermNode.CONJUNCTION:
 485             case TermNode.ABSTRACT:
 486                 return ERR_CYCLE;
 487             case TermNode.UPDATE:
 488                 throw new Error("No Update Nodes should be here");
 489             default:
 490             }
 491         }
 492         return WORKS;
 493     }
 494 }