Fixed some errors in the Repair Generator code.

[repair.git] / Repair / RepairCompiler / MCC / IR / GraphAnalysis.java

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3e44b831fd3fb6e4f788638cc90a2da0baf41633..16a51f781861c0a263d3f88e263f629778309427 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -19,6 +19,8 @@ public class GraphAnalysis {
     private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
        Stack workset=new Stack();
        HashSet closureset=new HashSet();
+       boolean needcyclecheck=false;
+       HashSet cantremovetrans=new HashSet();
        workset.push(gn);
        while(!workset.empty()) {
            GraphNode gn2=(GraphNode)workset.pop();
@@ -29,12 +31,24 @@ public class GraphAnalysis {
                    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
                    if (removed.contains(gn3))
                        continue;
+                   if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
+                        &&termination.conjunctions.contains(gn2))||
+                       cantremovetrans.contains(gn2))
+                       cantremovetrans.add(gn3);
+                   
                    if (termination.abstractrepair.contains(gn3)||
                        termination.conjunctions.contains(gn3)||
-                       termination.updatenodes.contains(gn3))
-                       return false;
-                   if (!removed.contains(gn3)&&
-                       ((!couldremove.contains(gn3))||cantremove.contains(gn3)))
+                       termination.updatenodes.contains(gn3)) {
+                       /**  Check for cycles if the graphnode can't
+                        * be removed (we know we aren't introducing
+                        * new things to repair). */
+                       if ((!termination.abstractrepair.contains(gn3)&&
+                            cantremove.contains(gn3))||
+                           cantremovetrans.contains(gn3)) {
+                           needcyclecheck=true;
+                       } else return false;
+                   }
+                   if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
                        goodoption=true;
                    workset.push(gn3);
                }
@@ -44,6 +58,16 @@ public class GraphAnalysis {
                }                   
            }
        }
+       if (needcyclecheck) {
+           Set cycles=GraphNode.findcycles(closureset);
+           for(Iterator it=cycles.iterator();it.hasNext();) {
+               GraphNode gn2=(GraphNode)it.next();
+               if (termination.abstractrepair.contains(gn2)||
+                   termination.conjunctions.contains(gn2)||
+                   termination.updatenodes.contains(gn2))
+                   return false;
+           }
+       }
        return true;
     }
 
@@ -86,6 +110,48 @@ public class GraphAnalysis {
                }
            }
 
+           /* Check for conjunction nodes which are fine */
+
+           for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode) it.next();
+               if (mustremove.contains(gn)||cantremove.contains(gn))
+                   continue;
+
+               boolean allgood=true;
+               for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                   GraphNode gn2=((GraphNode.Edge)edgeit.next()).getTarget();
+                   TermNode tn2=(TermNode)gn2.getOwner();
+                   assert tn2.getType()==TermNode.ABSTRACT;
+                   boolean foundupdate=false;
+                   for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+                       GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();                 
+                       if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
+                           TermNode tn3=(TermNode)gn3.getOwner();
+                           if (tn3.getType()==TermNode.UPDATE)
+                               foundupdate=true;
+                       }
+                   }
+                   if (!foundupdate)
+                       allgood=false;
+               }
+               if (allgood) {
+                   couldremove.remove(gn);
+                   if (Compiler.PRUNEQUANTIFIERS) {
+                       TermNode tn=(TermNode)gn.getOwner();
+                       Constraint constr=tn.getConstraint();
+                       for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
+                           GraphNode gn4=(GraphNode)consit.next();
+                           TermNode tn4=(TermNode)gn4.getOwner();
+                           if (tn4.getquantifiernode()) {
+                               mustremove.add(gn4); /* This node is history */
+                               System.out.println("Eliminating: "+gn4.getTextLabel());
+                           }
+                       }
+                   }
+               }
+           }
+
+
            /* Look for constraints which can only be satisfied one way */
            
            Vector constraints=termination.state.vConstraints;
@@ -195,6 +261,16 @@ public class GraphAnalysis {
                    }
 
                    System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
+                   System.out.println("CANTREMOVE");
+                   for(Iterator it2=cantremove.iterator();it2.hasNext();) {
+                       GraphNode gn2=(GraphNode)it2.next();
+                       System.out.println(gn2.getTextLabel());
+                   }
+                   System.out.println("MUSTREMOVE");
+                   for(Iterator it2=mustremove.iterator();it2.hasNext();) {
+                       GraphNode gn2=(GraphNode)it2.next();
+                       System.out.println(gn2.getTextLabel());
+                   }
                    return null; // Out of luck
                }
            }
@@ -283,7 +359,7 @@ public class GraphAnalysis {
                        if (!containsgn3)
                            cantremove.remove(gn3);
                    }
-                   if (ismodify&&((numadd==0)||(numremove==0))) {
+                   if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
                        for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                            GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
                            GraphNode gn3=e2.getTarget();
@@ -377,6 +453,13 @@ public class GraphAnalysis {
                e.printStackTrace();
                System.exit(-1);
            }
+
+           try {
+               GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
+           } catch (Exception e) {
+               e.printStackTrace();
+               System.exit(-1);
+           }
            
            System.out.println("Searching set of "+couldremove.size()+" nodes.");
            System.out.println("Eliminated must "+mustremove.size()+" nodes");
@@ -446,7 +529,7 @@ public class GraphAnalysis {
                            numremove++;
                    }
                }
-               if ((numadd==0)||(numremove==0)) {
+               if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
                    for(Iterator it2=gn.edges();it2.hasNext();) {
                        GraphNode.Edge edge=(GraphNode.Edge)it2.next();
                        GraphNode gn2=edge.getTarget();