From: bdemsky <bdemsky>
Date: Thu, 1 Apr 2004 16:23:06 +0000 (+0000)
Subject: Added Strongly Connected Component support into GraphNodes.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6460157f14fd4a96e59946c74267200a243c9951;p=repair.git

Added Strongly Connected Component support into GraphNodes.
---

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index aebb865..96a8645 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -118,16 +118,45 @@ public class GraphAnalysis {
 	    
 	    for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
-		if (!cantremove.contains(gn)) {
-		    cantremove.add(gn);
-		    Set cycle=GraphNode.findcycles(cantremove);
-		    if (cycle.contains(gn)) {
-			if (!mustremove.contains(gn)) {
-			    change=true;
-			    mustremove.add(gn);
+		boolean foundnocycle=false;
+
+		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.ABSTRACT)
+			continue;
+		    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+			GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
+			GraphNode gn3=e2.getTarget();
+			TermNode tn3=(TermNode)gn3.getOwner();
+			if (tn3.getType()!=TermNode.UPDATE)
+			    continue;
+			boolean containsgn=cantremove.contains(gn);
+			boolean containsgn3=cantremove.contains(gn3);
+			cantremove.add(gn);
+			cantremove.add(gn3);
+			Set cycle=GraphNode.findcycles(cantremove);
+			if (cycle.contains(gn3)) {
+			    if (!mustremove.contains(gn3)) {
+				change=true;
+				mustremove.add(gn3);
+			    }
 			}
+			if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
+			    foundnocycle=true;
+			}
+			if (!containsgn)
+			    cantremove.remove(gn);
+			if (!containsgn3)
+			    cantremove.remove(gn3);
+		    }
+		}
+		if(!foundnocycle) {
+		    if (!mustremove.contains(gn)) {
+			change=true;
+			mustremove.add(gn);
 		    }
-		    cantremove.remove(gn);
 		}
 	    }
 	    couldremove.removeAll(mustremove);
@@ -140,7 +169,8 @@ public class GraphAnalysis {
 		continue; //recalculate
 
 	    System.out.println("Searching set of "+couldremove.size()+" nodes.");
-	    System.out.println("Eliminated "+mustremove.size()+" nodes");
+	    System.out.println("Eliminated must "+mustremove.size()+" nodes");
+	    System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 	    System.out.println("Searching following set:");
 	    for(Iterator it=couldremove.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index f5448e3..de8fe32 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -25,6 +25,7 @@ public class GraphNode {
         
         private String label;
         private GraphNode target;
+	private GraphNode source;
         private String dotnodeparams = new String();
 
         public Edge(String label, GraphNode target) {
@@ -36,6 +37,14 @@ public class GraphNode {
             return label;
         }
 
+	public void setSource(GraphNode s) {
+	    this.source=s;
+	}
+
+	public GraphNode getSource() {
+	    return source;
+	}
+
         public GraphNode getTarget() {
             return target;
         }
@@ -55,7 +64,10 @@ public class GraphNode {
 
     int discoverytime = -1;
     int finishingtime = -1; /* used for searches */
+    int scc = -1;
+
     Vector edges = new Vector();  
+    Vector inedges = new Vector();
     String nodelabel;
     String textlabel;
     NodeStatus status = UNVISITED;    
@@ -136,29 +148,51 @@ public class GraphNode {
         return edges.iterator();
     }
 
+    public Iterator inedges() {
+        return inedges.iterator();
+    }
+
     public void addEdge(Edge newedge) {
+	newedge.setSource(this);
         edges.addElement(newedge);
+	GraphNode tonode=newedge.getTarget();
+	tonode.inedges.addElement(newedge);
     }
 
-    public void reset() {
-        discoverytime = -1;
-        finishingtime = -1;
-        status = UNVISITED;
+    void reset() {
+	    discoverytime = -1;
+	    finishingtime = -1;
+	    status = UNVISITED;
     }
 
-    public void discover(int time) {
-        discoverytime = time;
-        status = PROCESSING;
+    void resetscc() {
+	status = UNVISITED;
+	scc = -1;
     }
 
-    public void finish(int time) {
+    public int getSCC() {
+	return scc;
+    }
+
+    void setSCC(int s) {
+	scc=s;
+    }
+
+    void discover(int time) {
+	discoverytime = time;
+	status = PROCESSING;
+    }
+
+    void finish(int time) {
         assert status == PROCESSING;
-        finishingtime = time;
+	finishingtime = time;
         status = FINISHED;
     }
 
+    /** Returns finishing time for dfs */
+
     public int getFinishingTime() {
-        return finishingtime;
+	return finishingtime;
     }
 
 
@@ -270,18 +304,98 @@ public class GraphNode {
 	    return true; /* found cycle */
     }
     
+    public static class SCC {
+	boolean hascycles;
+	HashMap map;
+	int numscc;
+	public SCC(boolean hascycles, HashMap map,int numscc) {
+	    this.hascycles=hascycles;
+	    this.map=map;
+	    this.numscc=numscc;
+	}
+
+	public boolean hasCycles() {
+	    return hascycles;
+	}
+
+	public int numSCC() {
+	    return numscc;
+	}
+
+	public Set getSCC(int i) {
+	    Integer scc=new Integer(i);
+	    return (Set)map.get(scc);
+	}
+
+	boolean hascycle(int i) {
+	    Integer scc=new Integer(i);
+	    Set s=(Set)map.get(scc);
+	    if (s.size()>1)
+		return true;
+	    Object [] array=s.toArray();
+	    GraphNode gn=(GraphNode)array[0];
+	    for(Iterator it=gn.edges();it.hasNext();) {
+		Edge e=(Edge)it.next();
+		if (e.getTarget()==gn)
+		    return true; /* Self Cycle */
+	    }
+	    return false;
+	}
+    }
+
     /**
      * DFS encapsulates the depth first search algorithm 
      */
     public static class DFS {
 
         int time = 0;
+	int sccindex = 0;
         Collection nodes;
+	Vector finishingorder=null;
+	HashMap sccmap;
 
         private DFS(Collection nodes) { 
             this.nodes = nodes;
         }
 
+	public static SCC computeSCC(Collection nodes) {
+	    if (nodes==null) {
+		throw new NullPointerException();
+	    }
+	    DFS dfs=new DFS(nodes);
+	    dfs.sccmap=new HashMap();
+	    dfs.finishingorder=new Vector();
+	    boolean hascycles=dfs.go();
+            for (Iterator it = nodes.iterator();it.hasNext();) {
+                GraphNode gn = (GraphNode) it.next();
+                gn.resetscc();
+            }
+	    for(int i=dfs.finishingorder.size()-1;i>=0;i--) {
+		GraphNode gn=(GraphNode)dfs.finishingorder.get(i);
+		if (gn.getStatus() == UNVISITED) {
+		    dfs.dfsprev(gn);
+		    dfs.sccindex++; /* Increment scc index */
+		}
+	    }
+	    return new SCC(hascycles,dfs.sccmap,dfs.sccindex);
+	}
+
+	void dfsprev(GraphNode gn) {
+	    if (gn.getStatus()==FINISHED||!nodes.contains(gn))
+		return;
+	    gn.setStatus(FINISHED);
+	    gn.setSCC(sccindex);
+	    Integer i=new Integer(sccindex);
+	    if (!sccmap.containsKey(i))
+		sccmap.put(i,new HashSet());
+	    ((Set)sccmap.get(i)).add(gn);
+	    for(Iterator edgeit=gn.inedges();edgeit.hasNext();) {
+		Edge e=(Edge)edgeit.next();
+		GraphNode gn2=e.getSource();
+		dfsprev(gn2);
+	    }
+	}
+
         public static boolean depthFirstSearch(Collection nodes) {
             if (nodes == null) {
                 throw new NullPointerException();
@@ -315,7 +429,7 @@ public class GraphNode {
 
         private boolean dfs(GraphNode gn) {
 	    boolean acyclic=true;
-            gn.discover(time++);            
+            gn.discover(time++);
             Iterator edges = gn.edges();
 
             while (edges.hasNext()) {
@@ -330,7 +444,8 @@ public class GraphNode {
 		    acyclic=false;
 		}
             }
-
+	    if (finishingorder!=null)
+		finishingorder.add(gn);
             gn.finish(time++);
 	    return acyclic;
         }
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index b00c06b..4e34613 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -27,6 +27,8 @@ public class ImplicitSchema {
     boolean needDR(RelationDescriptor rd,boolean isdomain) {
 	Vector rules=state.vRules;
 	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	if (sd instanceof ReservedSetDescriptor)
+	    return false;
 	for(int i=0;i<rules.size();i++) {
 	    Rule r=(Rule)rules.get(i);
 	    if ((r.numQuantifiers()==1)&&
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 48212d1..e8f5d74 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -512,8 +512,11 @@ public class Termination {
 	}
 	return true;
     }
+    /** This method generates data structure updates to implement the
+     * 	abstract atomic modification specified by ar. */
 
     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
+	
     }
 
 
diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 66aff55..ed6595b 100755
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -233,7 +233,7 @@ class UpdateNode {
 	    left=toe.left;
 	    right=toe.right;
 	    istuple=true;
-	} else if (abstractexpr instanceof TupleOfExpr) {
+	} else if (abstractexpr instanceof ElementOfExpr) {
 	    ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
 	    d=eoe.set;
 	    left=eoe.element;
@@ -279,7 +279,7 @@ class UpdateNode {
 		    Rule r=(Rule)state.vRules.get(i);
 		    if (r.getInclusion().getTargetDescriptors().contains(sd)) {
 			for(int j=0;j<mun.numUpdates();j++) {
-			    UpdateNode un=mun.getUpdate(i);
+			    UpdateNode un=mun.getUpdate(j);
 			    if (un.getRule()==r) {
 				/* Update for rule rule r */
 				String name=(String)rg.updatenames.get(un);
@@ -324,6 +324,7 @@ class UpdateNode {
 	    VarDescriptor right=VarDescriptor.makeNew("right");
 	    if (u.getType()==Updates.ABSTRACT) {
 		generate_abstract(cr, removal, slot0, slot1, u, rg);
+		return;
 	    }
 
 	    switch(u.getType()) {
diff --git a/Repair/RepairCompiler/MCC/Makefile b/Repair/RepairCompiler/MCC/Makefile
index 59652ed..77a20e0 100755
--- a/Repair/RepairCompiler/MCC/Makefile
+++ b/Repair/RepairCompiler/MCC/Makefile
@@ -18,31 +18,46 @@ COMPILER_CLASS = Compiler.class
 CLI_CLASS = CLI.class
 OTHER_CLASS = State.class LineCount.class Symbol.class
 
-IR_CLASS = IR/ParseNode.class IR/ParseNodeVector.class IR/ParseNodeDOTVisitor.class \
-IR/SemanticChecker.class IR/Expr.class IR/VarExpr.class IR/OpExpr.class IR/DotExpr.class \
-IR/LiteralExpr.class IR/IntegerLiteralExpr.class IR/BooleanLiteralExpr.class \
-IR/TokenLiteralExpr.class IR/Descriptor.class IR/TypeDescriptor.class IR/StructureTypeDescriptor.class \
-IR/MissingTypeDescriptor.class IR/ReservedTypeDescriptor.class IR/ArrayDescriptor.class \
-IR/FieldDescriptor.class IR/LabelDescriptor.class IR/ReservedFieldDescriptor.class \
-IR/SymbolTable.class IR/IRException.class IR/Opcode.class IR/SimpleIRErrorReporter.class \
-IR/IRErrorReporter.class IR/SetDescriptor.class IR/MissingSetDescriptor.class \
-IR/RelationDescriptor.class IR/ReservedSetDescriptor.class IR/TokenSetDescriptor.class \
-IR/Quantifier.class IR/SetQuantifier.class IR/ImageSetExpr.class \
-IR/CastExpr.class IR/SizeofExpr.class IR/SetExpr.class IR/VarDescriptor.class \
-IR/LogicStatement.class IR/Predicate.class IR/InclusionPredicate.class \
-IR/ExprPredicate.class IR/Constraint.class IR/RelationExpr.class \
-IR/RelationQuantifier.class IR/ForQuantifier.class IR/GraphNode.class \
-IR/DependencyBuilder.class IR/RelationInclusion.class IR/SetInclusion.class \
-IR/TupleOfExpr.class IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class \
-IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class \
-IR/StandardCodeWriter.class IR/WorklistGenerator.class IR/WorkList.class \
-IR/Optimizer.class IR/MetaInclusion.class IR/SizeofFunction.class \
-IR/RelationFunctionExpr.class
-
-#MODEL_CLASS = Field.class Literal.class Quantifier.class 		\
-#Set.class TypeElement.class						\
-#MDElementExpr.class Rule.class Guard.class Type.class 			\
-#ParseException.class ModelInclusionConstraint.class
+IR_CLASS = IR/ParseNode.class IR/ParseNodeVector.class			\
+IR/ParseNodeDOTVisitor.class IR/SemanticChecker.class IR/Expr.class	\
+IR/VarExpr.class IR/OpExpr.class IR/DotExpr.class IR/LiteralExpr.class	\
+IR/IntegerLiteralExpr.class IR/BooleanLiteralExpr.class			\
+IR/TokenLiteralExpr.class IR/Descriptor.class IR/TypeDescriptor.class	\
+IR/StructureTypeDescriptor.class IR/MissingTypeDescriptor.class		\
+IR/ReservedTypeDescriptor.class IR/ArrayDescriptor.class		\
+IR/FieldDescriptor.class IR/LabelDescriptor.class			\
+IR/ReservedFieldDescriptor.class IR/SymbolTable.class			\
+IR/IRException.class IR/Opcode.class IR/SimpleIRErrorReporter.class	\
+IR/IRErrorReporter.class IR/SetDescriptor.class				\
+IR/MissingSetDescriptor.class IR/RelationDescriptor.class		\
+IR/ReservedSetDescriptor.class IR/TokenSetDescriptor.class		\
+IR/Quantifier.class IR/SetQuantifier.class IR/ImageSetExpr.class	\
+IR/CastExpr.class IR/SizeofExpr.class IR/SetExpr.class			\
+IR/VarDescriptor.class IR/LogicStatement.class IR/Predicate.class	\
+IR/InclusionPredicate.class IR/ExprPredicate.class IR/Constraint.class	\
+IR/RelationExpr.class IR/RelationQuantifier.class			\
+IR/ForQuantifier.class IR/GraphNode.class IR/DependencyBuilder.class	\
+IR/RelationInclusion.class IR/SetInclusion.class IR/TupleOfExpr.class	\
+IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class			\
+IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class	\
+IR/StandardCodeWriter.class IR/WorklistGenerator.class			\
+IR/WorkList.class IR/Optimizer.class IR/MetaInclusion.class		\
+IR/SizeofFunction.class IR/RelationFunctionExpr.class			\
+IR/RepairGenerator.class IR/AbstractInterferes.class			\
+IR/PrettyPrinter.class IR/AbstractRepair.class IR/Quantifiers.class	\
+IR/Binding.class IR/ConcreteInterferes.class IR/Conjunction.class	\
+IR/Repair.class IR/ConsequenceNode.class IR/Cost.class			\
+IR/DNFConstraint.class IR/DNFExpr.class IR/DNFPredicate.class		\
+IR/RuleConjunction.class IR/DNFRule.class IR/ScopeNode.class		\
+IR/SemanticAnalyzer.class IR/GraphAnalysis.class IR/SetAnalysis.class	\
+IR/Sources.class IR/StructureGenerator.class IR/ImplicitSchema.class	\
+IR/Termination.class IR/LinedMessage.class IR/TermNode.class		\
+IR/UpdateNode.class IR/MultUpdateNode.class IR/Updates.class		\
+IR/Walkable.class
+
+#MODEL_CLASS = Field.class Literal.class Quantifier.class Set.class	\
+#TypeElement.class MDElementExpr.class Rule.class Guard.class		\
+#Type.class ParseException.class ModelInclusionConstraint.class
 
 ALL_CLASS = $(COMPILER_CLASS) $(CLI_CLASS) $(OTHER_CLASS) $(IR_CLASS)
 
@@ -92,5 +107,5 @@ $(SCANNER).java: $(SCANNER).lex.java
 	rm $(SCANNER).lex.java
 
 javadoc:
-	javadoc -package -d ../javadoc/ -windowtitle MCC $(ALLJAVA)
+	javadoc -source 1.4 -classpath ../ -package -d ../javadoc/ -windowtitle MCC $(ALLJAVA)