From: bdemsky <bdemsky>
Date: Thu, 2 Jun 2005 20:26:27 +0000 (+0000)
Subject: Rewrote safetransclosure method so its obvious it is correct.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=1f785a8dec4eee153efa32c710e46e7917dd4742

Rewrote safetransclosure method so its obvious it is correct.
---

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 875baa2..06ab42c 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -15,72 +15,98 @@ public class GraphAnalysis {
     public GraphAnalysis(Termination t) {
 	termination=t;
     }
-    /**  This method returns true if leaving node gn in the repair
-     *  dependence graph will not result in cycles.
-     gn = updatenode, conjunctionnode, consequence node
-    */
+
     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);
+	HashSet dependent=new HashSet();
 
-	/* Iterating over everything reachable from gn */
+	/* 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);
+		}
+	    }
+	}
 
-	    /* Closureset is everything we've already iterated over */
+	/* 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;
-
-		    /* Consider only the nodes in the graph */
-
-		    
-		    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 (cantremove.contains(gn3)||
-			    cantremovetrans.contains(gn3)) {
-			    needcyclecheck=true;
-			} else if (termination.updatenodes.contains(gn3)&&
-				   !couldremove.contains(gn3)) {
-			    needcyclecheck=true;
-			} else return false;
-		    }
-		    if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
-			goodoption=true;
 		    workset.push(gn3);
 		}
-		if (!goodoption&&!cantremovetrans.contains(gn2)) {
-		    if (termination.scopenodes.contains(gn2))
-			return false;
-		    if (termination.abstractrepair.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;