From 78ba77e927e68b02e8530959c7d677d78b0843cf Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 25 Feb 2004 00:06:15 +0000 Subject: [PATCH] Updating files... --- Repair/RepairCompiler/MCC/IR/Cost.java | 8 + .../MCC/IR/RepairGenerator.java | 511 +++++++++++++++++- Repair/RepairCompiler/MCC/IR/Sources.java | 28 + Repair/RepairCompiler/MCC/IR/Termination.java | 5 +- Repair/RepairCompiler/MCC/SimpleHash.h | 3 + Repair/RepairCompiler/MCC/ex.cc | 10 + Repair/RepairCompiler/MCC/ex.constraints | 1 + Repair/RepairCompiler/MCC/ex.dependencies.dot | 15 + .../MCC/ex.dependencies.edgelabels.dot | 15 + Repair/RepairCompiler/MCC/ex.model | 5 + Repair/RepairCompiler/MCC/ex.space | 4 + Repair/RepairCompiler/MCC/ex.struct | 6 + 12 files changed, 588 insertions(+), 23 deletions(-) create mode 100755 Repair/RepairCompiler/MCC/IR/Cost.java create mode 100755 Repair/RepairCompiler/MCC/IR/Sources.java create mode 100755 Repair/RepairCompiler/MCC/ex.cc create mode 100755 Repair/RepairCompiler/MCC/ex.constraints create mode 100755 Repair/RepairCompiler/MCC/ex.dependencies.dot create mode 100755 Repair/RepairCompiler/MCC/ex.dependencies.edgelabels.dot create mode 100755 Repair/RepairCompiler/MCC/ex.model create mode 100755 Repair/RepairCompiler/MCC/ex.space create mode 100755 Repair/RepairCompiler/MCC/ex.struct diff --git a/Repair/RepairCompiler/MCC/IR/Cost.java b/Repair/RepairCompiler/MCC/IR/Cost.java new file mode 100755 index 0000000..7d0f40e --- /dev/null +++ b/Repair/RepairCompiler/MCC/IR/Cost.java @@ -0,0 +1,8 @@ +package MCC.IR; + +public class Cost { + Cost() {} + public int getCost(DNFPredicate dp) { + return 1; + } +}; diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index f1d66c0..5a29683 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -5,7 +5,6 @@ import java.util.*; import MCC.State; public class RepairGenerator { - State state; java.io.PrintWriter outputrepair = null; java.io.PrintWriter outputaux = null; @@ -22,6 +21,9 @@ public class RepairGenerator { HashSet usedupdates; Termination termination; Set removed; + static boolean DEBUG=false; + Cost cost; + Sources sources; public RepairGenerator(State state, Termination t) { this.state = state; @@ -29,6 +31,8 @@ public class RepairGenerator { usedupdates=new HashSet(); termination=t; removed=t.removedset; + cost=new Cost(); + sources=new Sources(state); Repair.repairgenerator=this; } @@ -47,9 +51,9 @@ public class RepairGenerator { } 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); + 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; name_updates(); @@ -58,9 +62,13 @@ public class RepairGenerator { generate_stateobject(); generate_call(); generate_worklist(); - generate_rules();/* + generate_rules(); generate_checks(); - generate_teardown();*/ + generate_teardown(); + CodeWriter crhead = new StandardCodeWriter(this.outputhead); + CodeWriter craux = new StandardCodeWriter(this.outputaux); + crhead.outputline("};"); + craux.outputline("};"); } @@ -116,6 +124,8 @@ public class RepairGenerator { CodeWriter craux = new StandardCodeWriter(outputaux); CodeWriter crhead = new StandardCodeWriter(outputhead); crhead.outputline("#include \"SimpleHash.h\""); + crhead.outputline("#include "); + crhead.outputline("#include "); crhead.outputline("class "+name+" {"); crhead.outputline("public:"); crhead.outputline(name+"();"); @@ -207,18 +217,26 @@ public class RepairGenerator { goodflag=VarDescriptor.makeNew("goodflag"); repairtable=VarDescriptor.makeNew("repairtable"); crhead.outputline("void doanalysis();"); - craux.outputline("void "+name +"_state::doanalysis() {"); + craux.outputline("void "+name +"_state::doanalysis()"); + craux.startblock(); craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;"); craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();"); craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;"); - craux.outputline("while (1) {"); + craux.outputline("while (1)"); + craux.startblock(); craux.outputline("int "+goodflag.getSafeSymbol()+"=1;"); craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();"); } private void generate_teardown() { CodeWriter cr = new StandardCodeWriter(outputaux); + cr.outputline("if ("+repairtable.getSafeSymbol()+")"); + cr.outputline("delete "+repairtable.getSafeSymbol()+";"); + cr.outputline("if ("+oldmodel.getSafeSymbol()+")"); + cr.outputline("delete "+oldmodel.getSafeSymbol()+";"); + cr.outputline("delete "+newmodel.getSafeSymbol()+";"); cr.outputline("delete "+worklist.getSafeSymbol()+";"); + cr.endblock(); } private void generate_rules() { @@ -258,7 +276,7 @@ public class RepairGenerator { CodeWriter cr = new StandardCodeWriter(outputaux) { public SymbolTable getSymbolTable() { return st; } }; - cr.outputline("// build " + rule.getLabel()); + cr.outputline("// build " +escape(rule.toString())); cr.startblock(); ListIterator quantifiers = rule.quantifiers(); while (quantifiers.hasNext()) { @@ -321,7 +339,7 @@ public class RepairGenerator { 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 " + rule.getLabel()); + cr.outputline("// build " +escape(rule.toString())); for (int j=0;j1) { + boolean first=true; + for(int j=0;jget("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");"); + } else { + expr.getLeftExpr().generate(cr,rightside); + expr.getRightExpr().generate(cr,newvalue); + cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";"); + cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");"); + } + if (negated) + if (opcode==Opcode.GT) { + opcode=Opcode.LE; + } else if (opcode==Opcode.GE) { + opcode=Opcode.LT; + } else if (opcode==Opcode.LT) { + opcode=Opcode.GE; + } else if (opcode==Opcode.LE) { + opcode=Opcode.GT; + } else if (opcode==Opcode.EQ) { + opcode=Opcode.NE; + } else if (opcode==Opcode.NE) { + opcode=Opcode.EQ; + } else { + throw new Error("Unrecognized Opcode"); + } + + if (opcode==Opcode.GT) { + cr.outputline(newvalue.getSafeSymbol()+"++;"); + } else if (opcode==Opcode.GE) { + /* Equal */ + } else if (opcode==Opcode.LT) { + cr.outputline(newvalue.getSafeSymbol()+"--;"); + } else if (opcode==Opcode.LE) { + /* Equal */ + } else if (opcode==Opcode.EQ) { + /* Equal */ + } else if (opcode==Opcode.NE) { + cr.outputline(newvalue.getSafeSymbol()+"++;"); + } else { + throw new Error("Unrecognized Opcode"); + } + /* Do abstract repairs */ + if (usageimage) { + cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");"); + if (!inverted) { + cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");"); + } else { + cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");"); + } + } + if (usageinvimage) { + cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");"); + if (!inverted) { + cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");"); + } else { + cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");"); + } + } + /* Do concrete repairs */ + /* Start with scheduling removal */ + for(int i=0;iaddrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");"); + } + } + } + } + /* Now do addition */ + UpdateNode un=munadd.getUpdate(0); + String name=(String)updatenames.get(un); + if (!inverted) { + cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");"); + } else { + cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");"); + } + } + + public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) { + ExprPredicate ep=(ExprPredicate)dpred.getPredicate(); + OpExpr expr=(OpExpr)ep.expr; + Opcode opcode=expr.getOpcode(); + { + boolean negated=dpred.isNegated(); + if (negated) + if (opcode==Opcode.GT) { + opcode=Opcode.LE; + } else if (opcode==Opcode.GE) { + opcode=Opcode.LT; + } else if (opcode==Opcode.LT) { + opcode=Opcode.GE; + } else if (opcode==Opcode.LE) { + opcode=Opcode.GT; + } else if (opcode==Opcode.EQ) { + opcode=Opcode.NE; + } else if (opcode==Opcode.NE) { + opcode=Opcode.EQ; + } else { + throw new Error("Unrecognized Opcode"); + } + } + MultUpdateNode munremove; + + MultUpdateNode munadd; + if (ep.getDescriptor() instanceof RelationDescriptor) { + munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION); + munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION); + } else { + munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET); + munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET); + } + int size=ep.leftsize(); + VarDescriptor sizevar=VarDescriptor.makeNew("size"); + ((OpExpr)expr).left.generate(cr, sizevar); + VarDescriptor change=VarDescriptor.makeNew("change"); + cr.outputline("int "+change.getSafeSymbol()+";"); + boolean generateadd=false; + boolean generateremove=false; + if (opcode==Opcode.GT) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=true; + generateremove=false; + } else if (opcode==Opcode.GE) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=true; + generateremove=false; + } else if (opcode==Opcode.LT) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=false; + generateremove=true; + } else if (opcode==Opcode.LE) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=false; + generateremove=true; + } else if (opcode==Opcode.EQ) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=true; + generateremove=true; + } else if (opcode==Opcode.NE) { + cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";"); + generateadd=true; + generateremove=false; + } else { + throw new Error("Unrecognized Opcode"); + } + Descriptor d=ep.getDescriptor(); + if (generateremove) { + cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)"); + cr.startblock(); + /* Find element to remove */ + VarDescriptor leftvar=VarDescriptor.makeNew("leftvar"); + VarDescriptor rightvar=VarDescriptor.makeNew("rightvar"); + if (d instanceof RelationDescriptor) { + if (ep.inverted()) { + rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar(); + cr.outputline("int "+leftvar.getSafeSymbol()+";"); + cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");"); + } else { + leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar(); + cr.outputline("int "+rightvar.getSafeSymbol()+";"); + cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");"); + } + } else { + cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();"); + } + /* Generate abstract remove instruction */ + if (d instanceof RelationDescriptor) { + RelationDescriptor rd=(RelationDescriptor) d; + boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE); + boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE); + if (usageimage) + cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");"); + if (usageinvimage) + cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");"); + } else { + cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");"); + } + /* Generate concrete remove instruction */ + for(int i=0;iaddrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");"); + } else { + cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");"); + } + } + } + } + } + cr.endblock(); + } + if (generateadd) { + cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)"); + cr.startblock(); + cr.endblock(); + } + } + + public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){ + InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate(); + boolean negated=dpred.isNegated(); + MultUpdateNode mun=getmultupdatenode(conj,dpred,-1); + VarDescriptor leftvar=VarDescriptor.makeNew("left"); + ip.expr.generate(cr, leftvar); + + if (negated) { + if (ip.setexpr instanceof ImageSetExpr) { + ImageSetExpr ise=(ImageSetExpr) ip.setexpr; + VarDescriptor rightvar=ise.getVar(); + boolean inverse=ise.inverted(); + RelationDescriptor rd=ise.getRelation(); + boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE); + boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE); + if (inverse) { + if (usageimage) + cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");"); + if (usageinvimage) + cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");"); + } else { + if (usageimage) + cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");"); + if (usageinvimage) + cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");"); + } + for(int i=0;iaddrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");"); + } else { + cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");"); + } + } + } + } + } + } else { + SetDescriptor sd=ip.setexpr.sd; + cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");"); + + for(int i=0;iaddset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");"); + } + } + } + } + } + } else { + /* Generate update */ + if (ip.setexpr instanceof ImageSetExpr) { + ImageSetExpr ise=(ImageSetExpr) ip.setexpr; + VarDescriptor rightvar=ise.getVar(); + boolean inverse=ise.inverted(); + RelationDescriptor rd=ise.getRelation(); + boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE); + boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE); + if (inverse) { + if (usageimage) + cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");"); + if (usageinvimage) + cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");"); + } else { + if (usageimage) + cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");"); + if (usageinvimage) + cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");"); + } + UpdateNode un=mun.getUpdate(0); + String name=(String)updatenames.get(un); + if (inverse) { + cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");"); + } else { + cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");"); + } + } else { + SetDescriptor sd=ip.setexpr.sd; + cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");"); + + UpdateNode un=mun.getUpdate(0); + /* Update for rule rule r */ + String name=(String)updatenames.get(un); + cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");"); + } + } + } @@ -710,7 +1180,6 @@ public class RepairGenerator { } cr.endblock(); } - } diff --git a/Repair/RepairCompiler/MCC/IR/Sources.java b/Repair/RepairCompiler/MCC/IR/Sources.java new file mode 100755 index 0000000..de6d4f3 --- /dev/null +++ b/Repair/RepairCompiler/MCC/IR/Sources.java @@ -0,0 +1,28 @@ +package MCC.IR; + +import MCC.State; + +public class Sources { + State state; + + public Sources(State s) { + this.state=s; + } + + public boolean setSource(SetDescriptor sd) { + return false; + } + public boolean allocSource(SetDescriptor sd) { + return true; + } + public SetDescriptor getSourceSet(SetDescriptor sd) { + return null; + } + public void generateSourceAlloc(CodeWriter cr,VarDescriptor vd, SetDescriptor sd) { + TypeDescriptor td=sd.getType(); + Expr e=td.getSizeExpr(); + VarDescriptor size=VarDescriptor.makeNew("size"); + e.generate(cr, size); + cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");"); + } +} diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 695699c..69f7613 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -17,7 +17,7 @@ public class Termination { Hashtable consequence; Hashtable abstractadd; Hashtable abstractremove; - + Hashtable conjtonodemap; Set removedset; State state; @@ -35,7 +35,7 @@ public class Termination { consequencenodes=new HashSet(); abstractadd=new Hashtable(); abstractremove=new Hashtable(); - + conjtonodemap=new Hashtable(); generateconjunctionnodes(); generatescopenodes(); @@ -90,6 +90,7 @@ public class Termination { if (!conjunctionmap.containsKey(c)) conjunctionmap.put(c,new HashSet()); ((Set)conjunctionmap.get(c)).add(gn); + conjtonodemap.put(dnf.get(j),gn); } } } diff --git a/Repair/RepairCompiler/MCC/SimpleHash.h b/Repair/RepairCompiler/MCC/SimpleHash.h index 5c2e271..182351c 100755 --- a/Repair/RepairCompiler/MCC/SimpleHash.h +++ b/Repair/RepairCompiler/MCC/SimpleHash.h @@ -123,6 +123,9 @@ public: int get(int key, int& data); int countdata(int data); void addParent(SimpleHash* parent); + inline int firstkey() { + return nodelist->key; + } inline SimpleIterator* iterator() { return new SimpleIterator(nodelist); } diff --git a/Repair/RepairCompiler/MCC/ex.cc b/Repair/RepairCompiler/MCC/ex.cc new file mode 100755 index 0000000..33c187e --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.cc @@ -0,0 +1,10 @@ + +// Token values + + + +foo_state * __repairstate0__=new foo_state(); +__repairstate0__->head=(int)head; +__repairstate0__->doanalysis(); +*((int*) &head)=__repairstate0__->head; +delete __repairstate0__; diff --git a/Repair/RepairCompiler/MCC/ex.constraints b/Repair/RepairCompiler/MCC/ex.constraints new file mode 100755 index 0000000..cde2dbc --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.constraints @@ -0,0 +1 @@ +[], sizeof(Nodes) >= literal(1); diff --git a/Repair/RepairCompiler/MCC/ex.dependencies.dot b/Repair/RepairCompiler/MCC/ex.dependencies.dot new file mode 100755 index 0000000..0c1cf61 --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.dependencies.dot @@ -0,0 +1,15 @@ +digraph dotvisitor { + rotate=90; + node [fontsize=10,height="0.1", width="0.1"]; + edge [fontsize=6]; + c1 [label="c1",shape=box]; + rule3 [label="rule3\nnextnodes"]; + rule2 [label="rule2\nNodes"]; + rule2 -> rule3 [label=""]; + rule2 -> c1 [label=""]; + rule1 [label="rule1\nNodes"]; + rule1 -> rule2 [label=""]; + rule1 -> rule3 [label=""]; + rule1 -> c1 [label=""]; +} + diff --git a/Repair/RepairCompiler/MCC/ex.dependencies.edgelabels.dot b/Repair/RepairCompiler/MCC/ex.dependencies.edgelabels.dot new file mode 100755 index 0000000..2752835 --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.dependencies.edgelabels.dot @@ -0,0 +1,15 @@ +digraph dotvisitor { + rotate=90; + node [fontsize=10,height="0.1", width="0.1"]; + edge [fontsize=6]; + c1 [label="c1",shape=box]; + rule3 [label="rule3\nnextnodes"]; + rule2 [label="rule2\nNodes"]; + rule2 -> rule3 [label="Nodes"]; + rule2 -> c1 [label="Nodes"]; + rule1 [label="rule1\nNodes"]; + rule1 -> rule2 [label="Nodes"]; + rule1 -> rule3 [label="Nodes"]; + rule1 -> c1 [label="Nodes"]; +} + diff --git a/Repair/RepairCompiler/MCC/ex.model b/Repair/RepairCompiler/MCC/ex.model new file mode 100755 index 0000000..fb4c2cf --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.model @@ -0,0 +1,5 @@ +[], !(head=literal(0)) => head in Nodes; +[forall node in Nodes], !(node.next=literal(0)) => node.next in Nodes; +[forall node in Nodes], !(node.next=literal(0)) => in nextnodes; + + diff --git a/Repair/RepairCompiler/MCC/ex.space b/Repair/RepairCompiler/MCC/ex.space new file mode 100755 index 0000000..ac17965 --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.space @@ -0,0 +1,4 @@ +set Nodes(Node); +nextnodes : Nodes -> Nodes (1->1); +prevnodes : Nodes -> Nodes (1->1); + diff --git a/Repair/RepairCompiler/MCC/ex.struct b/Repair/RepairCompiler/MCC/ex.struct new file mode 100755 index 0000000..f8782dc --- /dev/null +++ b/Repair/RepairCompiler/MCC/ex.struct @@ -0,0 +1,6 @@ +Node* head; +structure Node { + int data; + Node *next; + Node *prev; +} -- 2.34.1