--- /dev/null
+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;
+ }
+}
static boolean DEBUG=false;
Cost cost;
Sources sources;
+ ModelRuleDependence mrd;
public RepairGenerator(State state, Termination t) {
this.state = state;
GraphNode.computeclosure(togenerate,removed);
cost=new Cost();
sources=new Sources(state);
+ mrd=ModelRuleDependence.doAnalysis(state);
Repair.repairgenerator=this;
}
generate_hashtables();
generate_stateobject();
generate_call();
- generate_worklist();
+ generate_start();
generate_rules();
generate_checks();
generate_teardown();
craux.outputline("}");
}
- private void generate_worklist() {
+ private void generate_start() {
CodeWriter crhead = new StandardCodeWriter(outputhead);
CodeWriter craux = new StandardCodeWriter(outputaux);
oldmodel=VarDescriptor.makeNew("oldmodel");
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+"();");
}
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) {
}
cr.outputline("}");
- cr.outputline(goodflag.getSafeSymbol()+"=0;");
cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
}
}
CodeWriter cr = new StandardCodeWriter(outputaux);
- cr.outputline("if ("+goodflag.getSafeSymbol()+")");
cr.startblock();
cr.outputline("if ("+repairtable.getSafeSymbol()+")");
cr.outputline("delete "+repairtable.getSafeSymbol()+";");
}
}
-
-
public static Vector getrulelist(Descriptor d) {
Vector dispatchrules = new Vector();
Vector rules = State.currentState.vRules;
}
methodcall+=");";
cr.outputline(methodcall);
- cr.outputline(goodflag.getSafeSymbol()+"=0;");
- cr.outputline("continue;");
+ cr.outputline("goto rebuild;");
}
cr.endblock();
/* Build standard compensation actions */
}
methodcall+=");";
cr.outputline(methodcall);
- cr.outputline(goodflag.getSafeSymbol()+"=0;");
- cr.outputline("continue;");
+ cr.outputline("goto rebuild;");
}
}
cr.endblock();
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)) {
}
}
cr.endblock();
+ cr.endblock();
}
}
methodcall+=");";
cr.outputline(methodcall);
- cr.outputline(goodflag.getSafeSymbol()+"=0;");
- cr.outputline("continue;");
+ cr.outputline("goto rebuild;");
}
cr.endblock();
/* Build standard compensation actions */
}
methodcall+=");";
cr.outputline(methodcall);
- cr.outputline(goodflag.getSafeSymbol()+"=0;");
- cr.outputline("continue;");
+ cr.outputline("goto rebuild;");
}
}
cr.endblock();
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)) {
}
}
}
+
+ cr.endblock();
cr.endblock();
}
}