From 5f2028babc95ce9837fd60cc7e330d6c0d1ba13f Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Fri, 2 Apr 2004 19:31:11 +0000
Subject: [PATCH] Compute strongly connected components of model rules, and do
 computations the correct way...

---
 .../MCC/IR/ModelRuleDependence.java           | 149 +++++++++
 .../MCC/IR/RepairGenerator.java               | 313 +++++++++---------
 2 files changed, 307 insertions(+), 155 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java

diff --git a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
new file mode 100755
index 0000000..dfdcfb8
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
@@ -0,0 +1,149 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+class ModelRuleDependence {
+    State state;
+    HashSet nodes;
+    HashMap ruletonode, nodetorule;
+    // Stores references to negated edges
+    HashSet negatededges;
+    GraphNode.SCC scc;
+    HashMap sccCache;
+
+    private final int NODEPENDENCY=0;
+    private final int NORMDEPENDENCY=1;
+    private final int NEGDEPENDENCY=2;
+    
+    private ModelRuleDependence(State state) {
+	this.state=state;
+	this.nodes=new HashSet();
+	this.ruletonode=new HashMap();
+	this.nodetorule=new HashMap();
+	this.negatededges=new HashSet();
+	this.sccCache=new HashMap();
+    }
+    
+    public static ModelRuleDependence doAnalysis(State state) {
+	ModelRuleDependence mrd=new ModelRuleDependence(state);
+	mrd.generateNodes();
+	mrd.generateEdges();
+	mrd.scc=GraphNode.DFS.computeSCC(mrd.nodes);
+	if (mrd.checkForNegatedDependences())
+	    throw new Error("Negated Dependence");
+	return mrd;
+    }
+
+    public int numSCC() {
+	return scc.numSCC();
+    }
+
+    /** Gives strongly connected components in reverse topological
+     * order */
+    public Set getSCC(int i) {
+	Integer in=new Integer(i);
+	if (sccCache.containsKey(in))
+	    return (Set) sccCache.get(in);
+	Set nodescc=scc.getSCC(i);
+	HashSet rulescc=new HashSet();
+	for (Iterator nodeit=nodescc.iterator();nodeit.hasNext();) {
+	    GraphNode gn=(GraphNode) nodeit.next();
+	    Rule r=(Rule)nodetorule.get(gn);
+	    rulescc.add(r);
+	}
+	sccCache.put(in,rulescc);
+	return rulescc;
+    }
+
+    public boolean hasCycle(Rule r) {
+	return hasCycle(getComponent(r));
+    }
+
+    public boolean hasCycle(int i) {
+	return scc.hasCycle(i);
+    }
+
+    public int getComponent(Rule r) {
+	return scc.getComponent((GraphNode)ruletonode.get(r));
+    }
+
+    /** Returns true if there are any negated dependence cycles, false
+     * otherwise. */
+    private boolean checkForNegatedDependences() {
+	for(Iterator it=negatededges.iterator();it.hasNext();) {
+	    GraphNode.Edge e=(GraphNode.Edge)it.next();
+	    int scc1=scc.getComponent(e.getSource());
+	    int scc2=scc.getComponent(e.getTarget());
+	    if (scc1==scc2)
+		return true;
+	}
+	return false;
+    }
+
+    /** Build mapping between nodes and rules */
+    private void generateNodes() {
+	for(int i=0;i<state.vRules.size();i++) {
+	    GraphNode gn=new GraphNode("Rule"+i);
+	    ruletonode.put(state.vRules.get(i),gn);
+	    nodetorule.put(gn,state.vRules.get(i));
+	    nodes.add(gn);
+	}
+    }
+    
+    /** Generate edges between rule nodes */
+    private void generateEdges() {
+	for(int i=0;i<state.vRules.size();i++) {
+	    for(int j=0;j<state.vRules.size();j++) {
+		Rule r1=(Rule)state.vRules.get(i);
+		Rule r2=(Rule)state.vRules.get(j);
+		generateEdge(r1,r2);
+	    }
+	}
+    }
+
+    private void generateEdge(Rule r1,Rule r2) {
+	Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
+	int dep=checkBody(d,r2.getDNFGuardExpr());
+	if (dep==NODEPENDENCY)
+	    dep=checkQuantifiers(d,r2);
+	if (dep==NODEPENDENCY)
+	    return;
+	GraphNode gn1=(GraphNode) ruletonode.get(r1);
+	GraphNode gn2=(GraphNode) ruletonode.get(r2);
+	GraphNode.Edge edge=new GraphNode.Edge("dependency",gn2);
+	gn1.addEdge(edge);
+	if (dep==NEGDEPENDENCY)
+	    negatededges.add(edge);
+    }
+
+    private int checkBody(Descriptor d, DNFRule drule) {
+	boolean dependency=false;
+	for(int i=0;i<drule.size();i++) {
+	    RuleConjunction rconj=drule.get(i);
+	    for(int j=0;j<rconj.size();j++){ 
+		DNFExpr dexpr=rconj.get(j);
+		Expr e=dexpr.getExpr();
+		if (e.usesDescriptor(d)) {
+		    boolean negated=dexpr.getNegation();
+		    if (negated)
+			return NEGDEPENDENCY;
+		    else
+			dependency=true;
+		}
+	    }
+	}
+	if (dependency)
+	    return NORMDEPENDENCY;
+	else 
+	    return NODEPENDENCY;
+    }
+
+    private int checkQuantifiers(Descriptor d, Quantifiers qs) {
+	for (int i=0;i<qs.numQuantifiers();i++) {
+	    Quantifier q=qs.getQuantifier(i);
+	    if (q.getRequiredDescriptors().contains(d))
+		return NORMDEPENDENCY;
+	}
+	return NODEPENDENCY;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 79677d1..cce92d2 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -25,6 +25,7 @@ public class RepairGenerator {
     static boolean DEBUG=false;
     Cost cost;
     Sources sources;
+    ModelRuleDependence mrd;
 
     public RepairGenerator(State state, Termination t) {
         this.state = state;
@@ -38,6 +39,7 @@ public class RepairGenerator {
         GraphNode.computeclosure(togenerate,removed);
 	cost=new Cost();
 	sources=new Sources(state);
+	mrd=ModelRuleDependence.doAnalysis(state);
 	Repair.repairgenerator=this;
     }
 
@@ -82,7 +84,7 @@ public class RepairGenerator {
         generate_hashtables();
 	generate_stateobject();
 	generate_call();
-	generate_worklist();
+	generate_start();
         generate_rules();
         generate_checks();
         generate_teardown();
@@ -399,7 +401,7 @@ public class RepairGenerator {
         craux.outputline("}");
     }
 
-    private void generate_worklist() {
+    private void generate_start() {
         CodeWriter crhead = new StandardCodeWriter(outputhead);
         CodeWriter craux = new StandardCodeWriter(outputaux);
 	oldmodel=VarDescriptor.makeNew("oldmodel");
@@ -420,7 +422,6 @@ public class RepairGenerator {
 	craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 	craux.outputline("while (1)");
 	craux.startblock();
-	craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
 	craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
     }
     
@@ -429,156 +430,145 @@ public class RepairGenerator {
 	cr.endblock();
     }
 
+    Set ruleset=null;
     private void generate_rules() {
 	/* first we must sort the rules */
-        Iterator allrules = state.vRules.iterator();
-        Vector emptyrules = new Vector(); // rules with no quantifiers
-        Vector worklistrules = new Vector(); // the rest of the rules
 	RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 	SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
-
-        while (allrules.hasNext()) {
-            Rule rule = (Rule) allrules.next();
-            ListIterator quantifiers = rule.quantifiers();
-            boolean noquantifiers = true;
-            while (quantifiers.hasNext()) {
-                Quantifier quantifier = (Quantifier) quantifiers.next();
-                if (quantifier instanceof ForQuantifier) {
-                    // ok, because integers exist already!
-                } else {
-                    // real quantifier
-                    noquantifiers = false;
-                    break;
-                }
-            }
-            if (noquantifiers) {
-                emptyrules.add(rule);
-            } else {
-                worklistrules.add(rule);
-            }
-        }
-       
-        Iterator iterator_er = emptyrules.iterator();
-        while (iterator_er.hasNext()) {
-            Rule rule = (Rule) iterator_er.next();
-            {
-                final SymbolTable st = rule.getSymbolTable();                
-                CodeWriter cr = new StandardCodeWriter(outputaux) {
-                        public SymbolTable getSymbolTable() { return st; }
-                    };
-		cr.outputline("// build " +escape(rule.toString()));
-                cr.startblock();
-		cr.outputline("int maybe=0;");
-                ListIterator quantifiers = rule.quantifiers();
-                while (quantifiers.hasNext()) {
-                    Quantifier quantifier = (Quantifier) quantifiers.next();
-                    quantifier.generate_open(cr);
-                }
-
-                /* pretty print! */
-                cr.output("//");
-                rule.getGuardExpr().prettyPrint(cr);
-                cr.outputline("");
-
-                /* now we have to generate the guard test */
-		VarDescriptor guardval = VarDescriptor.makeNew();
-                rule.getGuardExpr().generate(cr, guardval);
-		cr.outputline("if (" + guardval.getSafeSymbol() + ")");
-                cr.startblock();
-
-                /* now we have to generate the inclusion code */
-		currentrule=rule;
-                rule.getInclusion().generate(cr);
-                cr.endblock();
-                while (quantifiers.hasPrevious()) {
-                    Quantifier quantifier = (Quantifier) quantifiers.previous();
-                    cr.endblock();
-                }
-                cr.endblock();
-                cr.outputline("");
-                cr.outputline("");
-            }
-        }
-
-        CodeWriter cr2 = new StandardCodeWriter(outputaux);        
-
-        cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
-        cr2.startblock();
-	VarDescriptor idvar=VarDescriptor.makeNew("id");
-        cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
-        
-        String elseladder = "if";
-
-        Iterator iterator_rules = worklistrules.iterator();
-        while (iterator_rules.hasNext()) {
-
-            Rule rule = (Rule) iterator_rules.next();
-            int dispatchid = rule.getNum();
-
-            {
-                final SymbolTable st = rule.getSymbolTable();
-                CodeWriter cr = new StandardCodeWriter(outputaux) {
-                        public SymbolTable getSymbolTable() { return st; }
-                    };
-
-                cr.indent();
-                cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
-                cr.startblock();
-		cr.outputline("int maybe=0;");
-		VarDescriptor typevar=VarDescriptor.makeNew("type");
-		VarDescriptor leftvar=VarDescriptor.makeNew("left");
-		VarDescriptor rightvar=VarDescriptor.makeNew("right");
-		cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
-		cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
-		cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
-		cr.outputline("// build " +escape(rule.toString()));
-
-
-		for (int j=0;j<rule.numQuantifiers();j++) {
-		    Quantifier quantifier = rule.getQuantifier(j);
-		    quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
+	System.out.println("SCC="+(mrd.numSCC()-1));
+	for(int sccindex=0;sccindex<mrd.numSCC();sccindex++) {
+	    ruleset=mrd.getSCC(sccindex);
+	    boolean needworklist=mrd.hasCycle(sccindex);
+	    
+	    if (!needworklist) {
+		Iterator iterator_rs = ruleset.iterator();
+		while (iterator_rs.hasNext()) {
+		    Rule rule = (Rule) iterator_rs.next();
+		    {
+			final SymbolTable st = rule.getSymbolTable();
+			CodeWriter cr = new StandardCodeWriter(outputaux) {
+				public SymbolTable getSymbolTable() { return st; }
+			    };
+			cr.outputline("// build " +escape(rule.toString()));
+			cr.startblock();
+			cr.outputline("int maybe=0;");
+			ListIterator quantifiers = rule.quantifiers();
+			while (quantifiers.hasNext()) {
+			    Quantifier quantifier = (Quantifier) quantifiers.next();
+			    quantifier.generate_open(cr);
+			}
+			
+			/* pretty print! */
+			cr.output("//");
+			rule.getGuardExpr().prettyPrint(cr);
+			cr.outputline("");
+			
+			/* now we have to generate the guard test */
+			VarDescriptor guardval = VarDescriptor.makeNew();
+			rule.getGuardExpr().generate(cr, guardval);
+			cr.outputline("if (" + guardval.getSafeSymbol() + ")");
+			cr.startblock();
+			
+			/* now we have to generate the inclusion code */
+			currentrule=rule;
+			rule.getInclusion().generate(cr);
+			cr.endblock();
+			while (quantifiers.hasPrevious()) {
+			    Quantifier quantifier = (Quantifier) quantifiers.previous();
+			    cr.endblock();
+			}
+			cr.endblock();
+			cr.outputline("");
+			cr.outputline("");
+		    }
+		}
+	    } else {
+		CodeWriter cr2 = new StandardCodeWriter(outputaux);
+		
+		for(Iterator initialworklist=ruleset.iterator();initialworklist.hasNext();) {
+		    /** Construct initial worklist set */
+		    Rule rule=(Rule)initialworklist.next();
+		    cr2.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
 		}
 
-                /* pretty print! */
-                cr.output("//");
-
-                rule.getGuardExpr().prettyPrint(cr);
-                cr.outputline("");
+		cr2.outputline("while ("+worklist.getSafeSymbol()+"->hasMoreElements())");
+		cr2.startblock();
+		VarDescriptor idvar=VarDescriptor.makeNew("id");
+		cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
+		
+		String elseladder = "if";
+		
+		Iterator iterator_rules = ruleset.iterator();
+		while (iterator_rules.hasNext()) {
+		    
+		    Rule rule = (Rule) iterator_rules.next();
+		    int dispatchid = rule.getNum();
+		    
+		    {
+			final SymbolTable st = rule.getSymbolTable();
+			CodeWriter cr = new StandardCodeWriter(outputaux) {
+				public SymbolTable getSymbolTable() { return st; }
+			    };
+			
+			cr.indent();
+			cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
+			cr.startblock();
+			cr.outputline("int maybe=0;");
+			VarDescriptor typevar=VarDescriptor.makeNew("type");
+			VarDescriptor leftvar=VarDescriptor.makeNew("left");
+			VarDescriptor rightvar=VarDescriptor.makeNew("right");
+			cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
+			cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
+			cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
+			cr.outputline("// build " +escape(rule.toString()));
+			
+			
+			for (int j=0;j<rule.numQuantifiers();j++) {
+			    Quantifier quantifier = rule.getQuantifier(j);
+			    quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
+			}
+			
+			/* pretty print! */
+			cr.output("//");
+			
+			rule.getGuardExpr().prettyPrint(cr);
+			cr.outputline("");
 
-                /* now we have to generate the guard test */
+			/* now we have to generate the guard test */
         
-                VarDescriptor guardval = VarDescriptor.makeNew();
-                rule.getGuardExpr().generate(cr, guardval);
-                
-                cr.outputline("if (" + guardval.getSafeSymbol() + ")");
-                cr.startblock();
-
-                /* now we have to generate the inclusion code */
-		currentrule=rule;
-                rule.getInclusion().generate(cr);
-                cr.endblock();
-
-		for (int j=0;j<rule.numQuantifiers();j++) {
-		    cr.endblock();
-		}
-
-                // close startblocks generated by DotExpr memory checks
-                //DotExpr.generate_memory_endblocks(cr);
+			VarDescriptor guardval = VarDescriptor.makeNew();
+			rule.getGuardExpr().generate(cr, guardval);
+			
+			cr.outputline("if (" + guardval.getSafeSymbol() + ")");
+			cr.startblock();
 
-                cr.endblock(); // end else-if WORKLIST ladder
+			/* now we have to generate the inclusion code */
+			currentrule=rule;
+			rule.getInclusion().generate(cr);
+			cr.endblock();
+			
+			for (int j=0;j<rule.numQuantifiers();j++) {
+			    cr.endblock();
+			}
 
-                elseladder = "else if";
-            }
-        }
+			// close startblocks generated by DotExpr memory checks
+			//DotExpr.generate_memory_endblocks(cr);
 
-        cr2.outputline("else");
-        cr2.startblock();
-        cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
-        cr2.outputline("exit(1);");
-        cr2.endblock();
-        // end block created for worklist
-	cr2.outputline(worklist.getSafeSymbol()+"->pop();");
-        cr2.endblock();
+			cr.endblock(); // end else-if WORKLIST ladder
+			
+			elseladder = "else if";
+		    }
+		}
+		cr2.outputline("else");
+		cr2.startblock();
+		cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
+		cr2.outputline("exit(1);");
+		cr2.endblock();
+		// end block created for worklist
+		cr2.outputline(worklist.getSafeSymbol()+"->pop();");
+		cr2.endblock();
+	    }
+	}
     }
 
     public static String escape(String s) {
@@ -727,7 +717,6 @@ public class RepairGenerator {
 		}
 		cr.outputline("}");
 
-		cr.outputline(goodflag.getSafeSymbol()+"=0;");
 		cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 		cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 		cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
@@ -745,7 +734,6 @@ public class RepairGenerator {
             }
         }
 	CodeWriter cr = new StandardCodeWriter(outputaux);
-	cr.outputline("if ("+goodflag.getSafeSymbol()+")");
 	cr.startblock();
 	cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 	cr.outputline("delete "+repairtable.getSafeSymbol()+";");
@@ -1184,8 +1172,6 @@ public class RepairGenerator {
 	}
     }
 
-
-
     public static Vector getrulelist(Descriptor d) {
         Vector dispatchrules = new Vector();
         Vector rules = State.currentState.vRules;
@@ -1286,8 +1272,7 @@ public class RepairGenerator {
 		}
 		methodcall+=");";
 		cr.outputline(methodcall);
-		cr.outputline(goodflag.getSafeSymbol()+"=0;");
-		cr.outputline("continue;");
+		cr.outputline("goto rebuild;");
 	    }
 	    cr.endblock();
 	    /* Build standard compensation actions */
@@ -1312,8 +1297,7 @@ public class RepairGenerator {
 		}
 		methodcall+=");";
 		cr.outputline(methodcall);
-		cr.outputline(goodflag.getSafeSymbol()+"=0;");
-		cr.outputline("continue;");
+		cr.outputline("goto rebuild;");
 	    }
 	}
 	cr.endblock();
@@ -1333,12 +1317,21 @@ public class RepairGenerator {
 
         Vector dispatchrules = getrulelist(rd);
         
+	Set toremove=new HashSet();
+	for(int i=0;i<dispatchrules.size();i++) {
+	    Rule r=(Rule)dispatchrules.get(i);
+	    if (!ruleset.contains(r))
+		toremove.add(r);
+	}
+	dispatchrules.removeAll(toremove);
         if (dispatchrules.size() == 0) {
             cr.outputline("// nothing to dispatch");
 	    cr.endblock();
             return;
         }
        
+	cr.outputline("if ("+addeditem+")");
+	cr.startblock();
         for(int i = 0; i < dispatchrules.size(); i++) {
             Rule rule = (Rule) dispatchrules.elementAt(i);
 	    if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
@@ -1355,6 +1348,7 @@ public class RepairGenerator {
 	    }
         }
 	cr.endblock();
+	cr.endblock();
     }
 
 
@@ -1399,8 +1393,7 @@ public class RepairGenerator {
 		}
 		methodcall+=");";
 		cr.outputline(methodcall);
-		cr.outputline(goodflag.getSafeSymbol()+"=0;");
-		cr.outputline("continue;");
+		cr.outputline("goto rebuild;");
 	    }
 	    cr.endblock();
 	    /* Build standard compensation actions */
@@ -1427,8 +1420,7 @@ public class RepairGenerator {
 		}
 		methodcall+=");";
 		cr.outputline(methodcall);
-		cr.outputline(goodflag.getSafeSymbol()+"=0;");
-		cr.outputline("continue;");
+		cr.outputline("goto rebuild;");
 	    }
 	}
 	cr.endblock();
@@ -1439,12 +1431,21 @@ public class RepairGenerator {
 	cr.startblock();
         Vector dispatchrules = getrulelist(sd);
 
+	Set toremove=new HashSet();
+	for(int i=0;i<dispatchrules.size();i++) {
+	    Rule r=(Rule)dispatchrules.get(i);
+	    if (!ruleset.contains(r))
+		toremove.add(r);
+	}
+	dispatchrules.removeAll(toremove);
+
         if (dispatchrules.size() == 0) {
             cr.outputline("// nothing to dispatch");
 	    cr.endblock();
             return;
         }
-
+	cr.outputline("if ("+addeditem+")");
+	cr.startblock();
         for(int i = 0; i < dispatchrules.size(); i++) {
             Rule rule = (Rule) dispatchrules.elementAt(i);
 	    if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
@@ -1460,6 +1461,8 @@ public class RepairGenerator {
 		}
 	    }
 	}
+
+	cr.endblock();
 	cr.endblock();
     }
 }
-- 
2.34.1