From cc8dc64af87942be304d8d599dd3779002a2c645 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 12 Feb 2004 06:53:39 +0000 Subject: [PATCH] Adding code to generate repair algorithms. Its not complete yet... This checkin sets defaults to repair... --- Repair/RepairCompiler/MCC/Compiler.java | 10 +- Repair/RepairCompiler/MCC/IR/DotExpr.java | 2 +- .../RepairCompiler/MCC/IR/GraphAnalysis.java | 126 +++++- Repair/RepairCompiler/MCC/IR/GraphNode.java | 4 +- .../RepairCompiler/MCC/IR/ImplicitSchema.java | 2 + .../MCC/IR/RelationInclusion.java | 11 +- Repair/RepairCompiler/MCC/IR/Repair.java | 86 ++++ .../MCC/IR/RepairGenerator.java | 401 ++++++++++++++++++ Repair/RepairCompiler/MCC/IR/Rule.java | 11 +- .../RepairCompiler/MCC/IR/SetDescriptor.java | 2 +- .../RepairCompiler/MCC/IR/SetInclusion.java | 16 +- .../MCC/IR/StructureTypeDescriptor.java | 2 +- Repair/RepairCompiler/MCC/IR/Termination.java | 6 + Repair/RepairCompiler/MCC/State.java | 3 +- 14 files changed, 654 insertions(+), 28 deletions(-) create mode 100755 Repair/RepairCompiler/MCC/IR/Repair.java create mode 100755 Repair/RepairCompiler/MCC/IR/RepairGenerator.java diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index 7773d7f..ebda670 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -85,14 +85,16 @@ public class Compiler { try { FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc"); + FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc"); + FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h"); // do model optimizations //(new Optimizer(state)).optimize(); - NaiveGenerator ng = new NaiveGenerator(state); - ng.generate(gcode); - //WorklistGenerator wg = new WorklistGenerator(state); - //wg.generate(gcode); + //NaiveGenerator ng = new NaiveGenerator(state); + //ng.generate(gcode); + RepairGenerator wg = new RepairGenerator(state); + wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h"); gcode.close(); } catch (Exception e) { e.printStackTrace(); diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java index 93beabc..8253991 100755 --- a/Repair/RepairCompiler/MCC/IR/DotExpr.java +++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java @@ -115,7 +115,7 @@ public class DotExpr extends Expr { // descriptor not the underlying field descriptor /* we calculate the offset in bits */ - offsetbits = struct.getOffsetExpr(fd); + offsetbits = struct.getOffsetExpr(fd); if (fd instanceof ArrayDescriptor) { fd = ((ArrayDescriptor) fd).getField(); diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java index fd32767..3488a66 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java +++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java @@ -13,13 +13,118 @@ public class GraphAnalysis { public GraphAnalysis(Termination t) { termination=t; } + + public Set doAnalysis() { + HashSet nodes=new HashSet(); + nodes.addAll(termination.conjunctions); + GraphNode.computeclosure(nodes,null); + Set cycles=GraphNode.findcycles(nodes); + Set couldremove=new HashSet(); + couldremove.addAll(termination.conjunctions); + couldremove.addAll(termination.updatenodes); + couldremove.addAll(termination.consequencenodes); + couldremove.retainAll(cycles); + Vector constraints=termination.state.vConstraints; + for(int i=0;iadd("+rule.getNum()+",-1,0,0);"); + } else { + for (int j=0;jadd("+rule.getNum()+","+j+","+leftvar+","+rightvar+");"); + } + } + } + } + } + + + public static void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) { + + cr.outputline("// SET DISPATCH "); + + Vector dispatchrules = getrulelist(sd); + + if (dispatchrules.size() == 0) { + cr.outputline("// nothing to dispatch"); + return; + } + + for(int i = 0; i < dispatchrules.size(); i++) { + Rule rule = (Rule) dispatchrules.elementAt(i); + if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) { + /* Guard depends on this relation, so we recomput everything */ + cr.outputline("WORKLIST->add("+rule.getNum()+",-1,0,0);"); + } else { + for (int j=0;jadd("+rule.getNum()+","+j+","+setvar+",0);"); + } + } + } + } + } +} diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java new file mode 100755 index 0000000..b20ae6f --- /dev/null +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -0,0 +1,401 @@ +package MCC.IR; + +import java.io.*; +import java.util.*; +import MCC.State; + +public class RepairGenerator { + + State state; + java.io.PrintWriter outputrepair = null; + java.io.PrintWriter outputaux = null; + java.io.PrintWriter outputhead = null; + String name="foo"; + String headername; + public RepairGenerator(State state) { + this.state = state; + } + + public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) { + this.outputrepair = new java.io.PrintWriter(outputrepair, true); + this.outputaux = new java.io.PrintWriter(outputaux, true); + this.outputhead = new java.io.PrintWriter(outputhead, true); + headername=st; + + generate_tokentable(); + generate_hashtables(); + generate_stateobject(); + generate_call(); + /* generate_worklist(); + generate_rules(); + generate_checks(); + generate_teardown();*/ + + } + + private void generate_call() { + CodeWriter cr = new StandardCodeWriter(outputrepair); + VarDescriptor vdstate=VarDescriptor.makeNew("repairstate"); + cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();"); + + + Iterator globals=state.stGlobals.descriptors(); + while (globals.hasNext()) { + VarDescriptor vd=(VarDescriptor) globals.next(); + cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";"); + } + /* Insert repair here */ + + globals=state.stGlobals.descriptors(); + while (globals.hasNext()) { + VarDescriptor vd=(VarDescriptor) globals.next(); + cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";"); + } + + cr.outputline("delete ("+vdstate.getSafeSymbol()+");"); + } + private void generate_tokentable() { + + CodeWriter cr = new StandardCodeWriter(outputrepair); + Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator(); + + cr.outputline(""); + cr.outputline("// Token values"); + cr.outputline(""); + + while (tokens.hasNext()) { + Object token = tokens.next(); + cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString()); + } + + cr.outputline(""); + cr.outputline(""); + } + + private void generate_stateobject() { + CodeWriter crhead = new StandardCodeWriter(outputhead); + crhead.outputline("class "+name+"_state {"); + crhead.outputline("public:"); + Iterator globals=state.stGlobals.descriptors(); + while (globals.hasNext()) { + VarDescriptor vd=(VarDescriptor) globals.next(); + crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";"); + } + } + + private void generate_hashtables() { + CodeWriter craux = new StandardCodeWriter(outputaux); + CodeWriter crhead = new StandardCodeWriter(outputhead); + crhead.outputline("#include \"SimpleHash.h\""); + crhead.outputline("class "+name+" {"); + crhead.outputline("public:"); + crhead.outputline(name+"();"); + crhead.outputline("~"+name+"();"); + craux.outputline("#include \""+headername+"\""); + + craux.outputline(name+"::"+name+"() {"); + craux.outputline("// creating hashtables "); + + /* build sets */ + Iterator sets = state.stSets.descriptors(); + + /* first pass create all the hash tables */ + while (sets.hasNext()) { + SetDescriptor set = (SetDescriptor) sets.next(); + crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;"); + craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();"); + } + + /* second pass build relationships between hashtables */ + sets = state.stSets.descriptors(); + + while (sets.hasNext()) { + SetDescriptor set = (SetDescriptor) sets.next(); + Iterator subsets = set.subsets(); + + while (subsets.hasNext()) { + SetDescriptor subset = (SetDescriptor) subsets.next(); + craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);"); + } + } + + /* build relations */ + Iterator relations = state.stRelations.descriptors(); + + /* first pass create all the hash tables */ + while (relations.hasNext()) { + RelationDescriptor relation = (RelationDescriptor) relations.next(); + + if (relation.testUsage(RelationDescriptor.IMAGE)) { + crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;"); + craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();"); + } + + if (relation.testUsage(RelationDescriptor.INVIMAGE)) { + crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;"); + craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();"); + } + } + + craux.outputline("}"); + crhead.outputline("};"); + craux.outputline(name+"::~"+name+"() {"); + craux.outputline("// deleting hashtables"); + + /* build destructor */ + sets = state.stSets.descriptors(); + + /* first pass create all the hash tables */ + while (sets.hasNext()) { + SetDescriptor set = (SetDescriptor) sets.next(); + craux.outputline("delete("+set.getSafeSymbol() + "_hash);"); + } + + /* destroy relations */ + relations = state.stRelations.descriptors(); + + /* first pass create all the hash tables */ + while (relations.hasNext()) { + RelationDescriptor relation = (RelationDescriptor) relations.next(); + + if (relation.testUsage(RelationDescriptor.IMAGE)) { + craux.outputline("delete("+relation.getSafeSymbol() + "_hash);"); + } + + if (relation.testUsage(RelationDescriptor.INVIMAGE)) { + craux.outputline("delete(" + relation.getSafeSymbol() + ");"); + } + } + craux.outputline("}"); + } + + private void generate_worklist() { + CodeWriter cr = new StandardCodeWriter(outputrepair); + cr.outputline("WORKLIST = new WorkList();"); + } + + private void generate_teardown() { + CodeWriter cr = new StandardCodeWriter(outputrepair); + cr.outputline("delete WORKLIST;"); + } + + 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 + + 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(outputrepair) { + public SymbolTable getSymbolTable() { return st; } + }; + + cr.outputline("// build " + rule.getLabel()); + cr.startblock(); + + 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 */ + 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(outputrepair); + + cr2.outputline("WORKLIST->reset();"); + cr2.outputline("while (WORKLIST->hasMoreElements())"); + cr2.startblock(); + cr2.outputline("WORKITEM *wi = (WORKITEM *) WORKLIST->nextElement();"); + + 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(outputrepair) { + public SymbolTable getSymbolTable() { return st; } + }; + + cr.indent(); + cr.outputline(elseladder + " (wi->id == " + dispatchid + ")"); + cr.startblock(); + + cr.outputline("// build " + rule.getLabel()); + + ListIterator quantifiers = rule.quantifiers(); + + int count = 0; + while (quantifiers.hasNext()) { + Quantifier quantifier = (Quantifier) quantifiers.next(); + count = quantifier.generate_worklistload(cr, count ); + } + + /* 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 */ + rule.getInclusion().generate(cr); + cr.endblock(); + + // close startblocks generated by DotExpr memory checks + //DotExpr.generate_memory_endblocks(cr); + + 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.endblock(); + + } + + private void generate_checks() { + + /* do constraint checks */ + Vector constraints = state.vConstraints; + + for (int i = 0; i < constraints.size(); i++) { + + Constraint constraint = (Constraint) constraints.elementAt(i); + + { + + final SymbolTable st = constraint.getSymbolTable(); + + CodeWriter cr = new StandardCodeWriter(outputrepair) { + public SymbolTable getSymbolTable() { return st; } + }; + + cr.outputline("// checking " + constraint.getLabel()); + cr.startblock(); + + ListIterator quantifiers = constraint.quantifiers(); + + while (quantifiers.hasNext()) { + Quantifier quantifier = (Quantifier) quantifiers.next(); + quantifier.generate_open(cr); + } + + cr.outputline("int maybe = 0;"); + + /* now we have to generate the guard test */ + + VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean"); + constraint.getLogicStatement().generate(cr, constraintboolean); + + cr.outputline("if (maybe)"); + cr.startblock(); + cr.outputline("__Success = 0;"); + cr.outputline("printf(\"maybe fail " + (i+1) + ". \");"); + cr.outputline("exit(1);"); + cr.endblock(); + + cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")"); + cr.startblock(); + + cr.outputline("__Success = 0;"); + cr.outputline("printf(\"fail " + (i+1) + ". \");"); + cr.outputline("exit(1);"); + cr.endblock(); + + while (quantifiers.hasPrevious()) { + Quantifier quantifier = (Quantifier) quantifiers.previous(); + cr.endblock(); + } + + cr.endblock(); + cr.outputline(""); + cr.outputline(""); + } + + } + + outputrepair.println("// if (__Success) { printf(\"all tests passed\"); }"); + } + +} + + + diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java index 806b3f8..4cfa2a8 100755 --- a/Repair/RepairCompiler/MCC/IR/Rule.java +++ b/Repair/RepairCompiler/MCC/IR/Rule.java @@ -13,7 +13,7 @@ public class Rule implements Quantifiers { Inclusion inclusion = null; SymbolTable st = new SymbolTable(); DNFRule dnfguard=null,dnfnegguard=null; - + boolean nogenerate=false; String label; int num; @@ -23,6 +23,14 @@ public class Rule implements Quantifiers { label = new String("rule" + count++); } + public void setnogenerate() { + nogenerate=true; + } + + public boolean getnogenerate() { + return nogenerate; + } + public String toString() { String name=""; for(int i=0;iadd((int)" + vd.getSafeSymbol() + writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() + ", (int)" + vd.getSafeSymbol() + ");"); - + if (SetInclusion.worklist) { writer.outputline("if (" + addeditem + ")"); writer.startblock(); { @@ -75,7 +74,14 @@ public class SetInclusion extends Inclusion { } writer.endblock(); } - + if (Compiler.REPAIR) { + writer.outputline("if (" + addeditem + ")"); + writer.startblock(); { + Repair.generate_dispatch(writer, set, vd.getSafeSymbol()); + } + writer.endblock(); + } + } } diff --git a/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java b/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java index a9fd29c..7296606 100755 --- a/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java +++ b/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java @@ -88,7 +88,7 @@ public class StructureTypeDescriptor extends TypeDescriptor { size = new OpExpr(Opcode.ADD, fieldsize, size); } - return size; + return size; } public Iterator getFields() { diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index b788acc..ff5985f 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -66,6 +66,12 @@ public class Termination { System.out.println(mun.toString()); } GraphAnalysis ga=new GraphAnalysis(this); + Set toremove=ga.doAnalysis(); + System.out.println("Removing:"); + for(Iterator it=toremove.iterator();it.hasNext();) { + GraphNode gn=(GraphNode)it.next(); + System.out.println(gn.getTextLabel()); + } } void generateconjunctionnodes() { diff --git a/Repair/RepairCompiler/MCC/State.java b/Repair/RepairCompiler/MCC/State.java index 9f907a9..024aed3 100755 --- a/Repair/RepairCompiler/MCC/State.java +++ b/Repair/RepairCompiler/MCC/State.java @@ -33,7 +33,7 @@ public class State { public Hashtable rulenodes; public Hashtable constraintnodes; - + public Hashtable implicitrule; State() { vConstraints = null; vRules = null; @@ -47,6 +47,7 @@ public class State { ptModel = null; ptConstraints = null; ptSpace = null; + implicitrule=new Hashtable(); } void printall() { -- 2.34.1