X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FGraphAnalysis.java;h=3fdbe6e87a63ae9a6fb93443069b66bb979a1dd0;hp=6b6a7153c9a79ad12019b4ddcd1df321806febde;hb=87862c69c1cb47c83a858f0b6e52d9c0bc25913f;hpb=1865e2c81c6c387dcc48114a33921e26fc0211b1

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 6b6a715..3fdbe6e 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -20,52 +20,93 @@ public class GraphAnalysis {
 	Stack workset=new Stack();
 	HashSet closureset=new HashSet();
 	boolean needcyclecheck=false;
-	HashSet cantremovetrans=new HashSet();
+	HashSet dependent=new HashSet();
+
+	/* Compute dependent set */
+	workset.push(gn);
+	while(!workset.empty()) {
+	    GraphNode gn2=(GraphNode)workset.pop();
+	    for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+		GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+		if (removed.contains(gn3))
+		    continue;
+		if (!termination.conjunctions.contains(gn3)&&!dependent.contains(gn3)) {
+		    dependent.add(gn3);
+		    workset.push(gn3);
+		}
+	    }
+	}
+
+	/* Compute the closure set */
 	workset.push(gn);
 	while(!workset.empty()) {
 	    GraphNode gn2=(GraphNode)workset.pop();
 	    if (!closureset.contains(gn2)) {
 		closureset.add(gn2);
-		boolean goodoption=false;
 		for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
 		    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)) {
-			/**  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);
 		}
-		if (!goodoption) {
-		    if (termination.scopenodes.contains(gn2))
-			return false;
-		}		    
 	    }
 	}
-	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;
+
+	/* Check for harmful cycles through gn */
+	Set cycles=GraphNode.findcycles(closureset);
+	if (cycles.contains(gn))
+	    return false;
+
+	/* Check for harmful cycles being introduced in dependent nodes */
+	cycles=GraphNode.findcycles(dependent);
+	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;
+	}
+
+	/* Make sure all abstractrepairs/consequence nodes in the dependent nodes
+	   are well formed. */
+    outerloop:
+	for(Iterator it=dependent.iterator();it.hasNext();) {
+	    GraphNode gn2=(GraphNode)it.next();
+	    if (termination.abstractrepair.contains(gn2)||
+		termination.scopenodes.contains(gn2)) {
+		boolean ismodify=false;
+		int numadd=0;
+		int numremove=0;
+
+		if (termination.abstractrepair.contains(gn2)&&
+		    ((TermNode)gn2.getOwner()).getAbstract().getType()==AbstractRepair.MODIFYRELATION)
+		    ismodify=true;
+
+		innerloop:
+		for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+		    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+		    if (removed.contains(gn3))
+			continue innerloop;
+		    if (cantremove.contains(gn3)||
+			!couldremove.contains(gn3)) {
+			if (ismodify) {
+			    TermNode tn3=(TermNode)gn3.getOwner();
+			    MultUpdateNode mun=tn3.getUpdate();
+			    if (mun.getType()==MultUpdateNode.ADD)
+				numadd++;
+			    if (mun.getType()==MultUpdateNode.REMOVE)
+				numremove++;
+			    if (mun.getType()==MultUpdateNode.MODIFY)
+				continue outerloop;
+			    if ((numadd>0)&&(numremove>0||!((TermNode)gn2.getOwner()).getAbstract().needsRemoves(termination.state)))
+				continue outerloop;
+			} else
+			    if (termination.consequence.contains(gn3)||
+				termination.updatenodes.contains(gn3))
+				continue outerloop;
+		    }
+		}
+		return false;
 	    }
 	}
 	return true;
@@ -97,7 +138,7 @@ public class GraphAnalysis {
 	    for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode) it.next();
 		if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
-			    couldremove.remove(gn);
+		    couldremove.remove(gn);
 		}
 	    }
 
@@ -105,8 +146,8 @@ public class GraphAnalysis {
 
 	    for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode) it.next();
-		if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
-			couldremove.remove(gn);
+		if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
+		    couldremove.remove(gn);
 		}
 	    }
 
@@ -116,6 +157,8 @@ public class GraphAnalysis {
 		GraphNode gn=(GraphNode) it.next();
 		if (mustremove.contains(gn)||cantremove.contains(gn))
 		    continue;
+		if (!safetransclosure(gn, mustremove,cantremove, couldremove))
+                    continue;
 
 		boolean allgood=true;
 		for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
@@ -124,7 +167,7 @@ public class GraphAnalysis {
 		    assert tn2.getType()==TermNode.ABSTRACT;
 		    boolean foundupdate=false;
 		    for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
-			GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();		    
+			GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
 			if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
 			    TermNode tn3=(TermNode)gn3.getOwner();
 			    if (tn3.getType()==TermNode.UPDATE)
@@ -134,13 +177,26 @@ public class GraphAnalysis {
 		    if (!foundupdate)
 			allgood=false;
 		}
-		if (allgood)
+		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;
 	    for(int i=0;i<constraints.size();i++) {
 		Constraint c=(Constraint)constraints.get(i);
@@ -157,9 +213,10 @@ public class GraphAnalysis {
 	    }
 
 
-	    /* Search through conjunction which must be satisfied, and attempt
-	       to generate appropriate repair actions.
-	     */
+	    /* Search through conjunction nodes which must be
+	       satisfied, and see if there are any data structure
+	       updates that must exist. */
+
 	    HashSet newset=new HashSet();
 	    for(Iterator cit=cantremove.iterator();cit.hasNext();) {
 		GraphNode gn=(GraphNode)cit.next();
@@ -213,7 +270,7 @@ public class GraphAnalysis {
 			change=true;
 		}
 	    }
-	    
+
 	    if (Compiler.AGGRESSIVESEARCH) {
 		/* Aggressively remove compensation nodes */
 		for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
@@ -248,6 +305,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
 		}
 	    }
@@ -287,9 +354,10 @@ public class GraphAnalysis {
 	    /* Searches individual conjunctions + abstract action +updates for cycles */
 	    for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
-		boolean foundnocycle=false;
 
 		for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                    boolean foundnocycle=false;
+
 		    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 		    GraphNode gn2=e.getTarget();
 		    TermNode tn2=(TermNode)gn2.getOwner();
@@ -298,7 +366,7 @@ public class GraphAnalysis {
 		    AbstractRepair ar=tn2.getAbstract();
 		    boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 		    int numadd=0;int numremove=0;
-		    
+
 		    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 			GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 			GraphNode gn3=e2.getTarget();
@@ -336,7 +404,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();
@@ -350,30 +418,25 @@ public class GraphAnalysis {
 				mustremove.add(gn3);
 			}
 		    }
-		}
 
-		if(!foundnocycle) {
-		    if (!mustremove.contains(gn)) {
-			change=true;
-			mustremove.add(gn);
-		    }
-		}
+
+                    if(!foundnocycle) {
+                        if (!mustremove.contains(gn)) {
+                            change=true;
+                            mustremove.add(gn);
+                        }
+                    }
+                }
 	    }
 
 	    /* Searches scope nodes + compensation nodes */
 	    for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
-		int count=0;
 		if (nodes.contains(gn)) {
     		    for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 			GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 			GraphNode gn2=e.getTarget();
 			TermNode tn2=(TermNode)gn2.getOwner();
-			
-			if ((tn2.getType()==TermNode.CONSEQUENCE)&&
-			    !mustremove.contains(gn2))
-			    count++;
-			    
 
 			if (tn2.getType()!=TermNode.UPDATE)
 			    continue;
@@ -382,42 +445,24 @@ public class GraphAnalysis {
 			boolean containsgn2=cantremove.contains(gn2);
 			cantremove.add(gn);
 			cantremove.add(gn2);
-			
+
 			Set cycle=GraphNode.findcycles(cantremove);
 			if (cycle.contains(gn2)) {
 			    if (!mustremove.contains(gn2)) {
 				change=true;
 				mustremove.add(gn2);
 			    }
-			} else {
-			    if (!mustremove.contains(gn2))
-				count++;
 			}
 			if (!containsgn)
 			    cantremove.remove(gn);
 			if (!containsgn2)
 			    cantremove.remove(gn2);
 		    }
-		
-		    if (count==1) {
-			for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
-			    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
-			    GraphNode gn2=e.getTarget();
-			    TermNode tn2=(TermNode)gn2.getOwner();
-			    if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
-				!mustremove.contains(gn2)) {
-				if (!cantremove.contains(gn2)) {
-				    cantremove.add(gn2);
-				    change=true;
-				}
-			    }
-			}
-		    }
 		}
 	    }
 	    couldremove.removeAll(mustremove);
 	    couldremove.removeAll(cantremove);
-	    
+
 	    Vector couldremovevector=new Vector();
 	    couldremovevector.addAll(couldremove);
 	    Vector combination=new Vector();
@@ -437,7 +482,7 @@ public class GraphAnalysis {
 		e.printStackTrace();
 		System.exit(-1);
 	    }
-	    
+
 	    System.out.println("Searching set of "+couldremove.size()+" nodes.");
 	    System.out.println("Eliminated must "+mustremove.size()+" nodes");
 	    System.out.println("Eliminated cant "+cantremove.size()+" nodes");
@@ -456,22 +501,31 @@ public class GraphAnalysis {
 		GraphNode gn=(GraphNode)it.next();
 		System.out.println(gn.getTextLabel());
 	    }
-	    
-	    
+
+	    System.out.println("==================================================");
 	    while(true) {
 		if (illegal(combination,couldremovevector))
 		    break;
 		Set combinationset=buildset(combination,couldremovevector);
+                System.out.println("---------------------------");
+                for(Iterator it=combinationset.iterator();it.hasNext();) {
+                    System.out.println(((GraphNode)it.next()).getTextLabel());
+                }
+                System.out.println("---------------------------");
 		checkmodify(combinationset);
 		combinationset.addAll(mustremove);
 		if (combinationset!=null) {
-		    System.out.println("Checkabstract="+checkAbstract(combinationset));
-		    System.out.println("Checkrepairs="+checkRepairs(combinationset));
-		    System.out.println("Checkall="+checkAll(combinationset));
-		    
-		    if (checkAbstract(combinationset)==0&&
-			checkRepairs(combinationset)==0&&
-			checkAll(combinationset)==0) {
+                    int checkabstract=checkAbstract(combinationset);
+                    int checkrep=checkRepairs(combinationset);
+                    int checkall=checkAll(combinationset);
+
+		    System.out.println("Checkabstract="+checkabstract);
+		    System.out.println("Checkrepairs="+checkrep);
+		    System.out.println("Checkall="+checkall);
+
+		    if (checkabstract==0&&
+			checkrep==0&&
+			checkall==0) {
 			return combinationset;
 		    }
 		}
@@ -499,14 +553,14 @@ public class GraphAnalysis {
 		    if (!removednodes.contains(gn2)&&
 			tn2.getType()==TermNode.UPDATE) {
 			MultUpdateNode mun=tn2.getUpdate();
-			
+
 			if (mun.getType()==MultUpdateNode.ADD)
 			    numadd++;
 			if (mun.getType()==MultUpdateNode.REMOVE)
 			    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();
@@ -669,8 +723,9 @@ public class GraphAnalysis {
 		    foundrepair=true;
 		}
    	    }
-	    if (!foundrepair)
+	    if (!foundrepair) {
 		return ERR_NOREPAIR;
+            }
 	}
 
 
@@ -686,7 +741,7 @@ public class GraphAnalysis {
 	tset.addAll(termination.consequencenodes);
 	abstractnodes.retainAll(tset);
 	Set cycles=GraphNode.findcycles(abstractnodes);
-	
+
 	for(Iterator it=cycles.iterator();it.hasNext();) {
 	    GraphNode gn=(GraphNode)it.next();
 	    System.out.println("NODE: "+gn.getTextLabel());