From cdd4513e39de359245e55af313d8bdea2167a253 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 6 Apr 2004 02:48:30 +0000 Subject: [PATCH] Made flag work for checking only...Added support for modify relation updates. --- Repair/RepairCompiler/MCC/Compiler.java | 28 +-- .../MCC/IR/RepairGenerator.java | 167 +++++++++++++----- Repair/RepairCompiler/MCC/IR/Termination.java | 97 +++++++++- Repair/RepairCompiler/MCC/IR/UpdateNode.java | 10 +- Repair/RepairCompiler/MCC/Makefile | 6 +- .../RepairCompiler/MCC/Runtime/SimpleHash.cc | 30 +++- .../RepairCompiler/MCC/Runtime/SimpleHash.h | 5 +- 7 files changed, 263 insertions(+), 80 deletions(-) diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index 05c6033..013c5c6 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -17,6 +17,7 @@ import MCC.IR.*; */ public class Compiler { + /* Set this flag to false to turn repairs off */ public static boolean REPAIR=true; public static void main(String[] args) { @@ -56,11 +57,10 @@ public class Compiler { Termination termination=null; - if (REPAIR) { - /* Check partition constraints */ - (new ImplicitSchema(state)).update(); - termination=new Termination(state); - } + /* Check partition constraints */ + (new ImplicitSchema(state)).update(); + termination=new Termination(state); + state.printall(); (new DependencyBuilder(state)).calculate(); @@ -91,19 +91,19 @@ public class Compiler { //(new Optimizer(state)).optimize(); - if(REPAIR) { - FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc"); - FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h"); - RepairGenerator wg = new RepairGenerator(state,termination); - wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h"); - gcode2.close(); - gcode3.close(); - } else { + + FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc"); + FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h"); + RepairGenerator wg = new RepairGenerator(state,termination); + wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h"); + gcode2.close(); + gcode3.close(); + /* } else { WorklistGenerator ng = new WorklistGenerator(state); SetInclusion.worklist=true; RelationInclusion.worklist=true; ng.generate(gcode); - } + }*/ gcode.close(); } catch (Exception e) { e.printStackTrace(); diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index cce92d2..58b3b63 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -3,6 +3,7 @@ package MCC.IR; import java.io.*; import java.util.*; import MCC.State; +import MCC.Compiler; public class RepairGenerator { State state; @@ -35,7 +36,8 @@ public class RepairGenerator { removed=t.removedset; togenerate=new HashSet(); togenerate.addAll(termination.conjunctions); - togenerate.removeAll(removed); + if (Compiler.REPAIR) + togenerate.removeAll(removed); GraphNode.computeclosure(togenerate,removed); cost=new Cost(); sources=new Sources(state); @@ -108,6 +110,7 @@ public class RepairGenerator { String strepairtable="repairtable"; String stleft="left"; String stright="right"; + String stnew="newvalue"; private void generate_updates() { int count=0; @@ -146,11 +149,11 @@ public class RepairGenerator { CodeWriter cr = new StandardCodeWriter(outputaux) { public SymbolTable getSymbolTable() { return st; } }; - un.generate(cr, false, stleft,stright,this); + un.generate(cr, false, false, stleft,stright, null,this); craux.outputline("if (maybe) printf(\"REALLY BAD\");"); craux.endblock(); break; - case MultUpdateNode.REMOVE: + case MultUpdateNode.REMOVE: { Rule r=un.getRule(); String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable; for(int j=0;jaddrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");"); + if (munmodify!=null) { + for(int i=0;iaddrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+","+newvalue.getSafeSymbol()+");"); + } } } } - } - /* 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()+");"); + /* 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()+");"); + } } } @@ -1245,7 +1298,9 @@ public class RepairGenerator { cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))"); cr.startblock(); { /* Have update to call into */ - VarDescriptor funptr=VarDescriptor.makeNew("updateptr"); + VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr"); + cr.outputline("int "+mdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->getrelation2("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");"); + String parttype=""; for(int i=0;igetrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");"); + VarDescriptor funptr=VarDescriptor.makeNew("updateptr"); + VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr"); + String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol(); for(int i=0;igetrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");"); + cr.outputline("if ("+mdfyptr.getSafeSymbol()+")"); + { + cr.startblock(); + cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)) "+tmpptr.getSafeSymbol()); + cr.outputline(methodcall+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");"); + cr.endblock(); + } + cr.outputline("else "); + { + cr.startblock(); + cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol()); + cr.outputline(methodcall+");"); + cr.endblock(); + } cr.outputline("goto rebuild;"); } cr.endblock(); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index e8f5d74..8aa0370 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -2,6 +2,7 @@ package MCC.IR; import java.util.*; import java.io.*; import MCC.State; +import MCC.Compiler; public class Termination { HashSet conjunctions; @@ -36,6 +37,8 @@ public class Termination { abstractadd=new Hashtable(); abstractremove=new Hashtable(); conjtonodemap=new Hashtable(); + if (!Compiler.REPAIR) + return; generateconjunctionnodes(); generatescopenodes(); @@ -428,7 +431,7 @@ public class Termination { if (possiblerules.size()==0) return; int[] count=new int[possiblerules.size()]; - while(remains(count,possiblerules)) { + while(remains(count,possiblerules,true)) { MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE); TermNode tn=new TermNode(mun); GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn); @@ -490,33 +493,109 @@ public class Termination { gn.addEdge(e); updatenodes.add(gn2); } - increment(count,possiblerules); + increment(count,possiblerules,true); } } - static void increment(int count[], Vector rules) { + static void increment(int count[], Vector rules,boolean isremove) { count[0]++; for(int i=0;i<(rules.size()-1);i++) { - if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) { + int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size(); + if (count[i]>=num) { count[i+1]++; count[i]=0; } else break; } } - static boolean remains(int count[], Vector rules) { + static boolean remains(int count[], Vector rules, boolean isremove) { for(int i=0;i=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) { + int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size(); + if (count[i]>=num) { return false; } } return true; } + /** This method generates data structure updates to implement the * abstract atomic modification specified by ar. */ - + int modifycount=0; void generatemodifyrelation(GraphNode gn, AbstractRepair ar) { - + RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor(); + ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate(); + boolean inverted=exprPredicate.inverted(); + int leftindex=0; + int rightindex=1; + if (inverted) + leftindex=2; + else + rightindex=2; + + + Vector possiblerules=new Vector(); + for(int i=0;isetrelation = setrelation; this->lvalue=lvalue; this->rvalue=rvalue; this->data = data; + this->data2 = data2; this->next = 0; this->lnext=0; this->rule=rule; @@ -373,6 +374,10 @@ int RepairHash::addset(int setv, int rule, int value, int data) { } int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int data) { + return addrelation(relation,rule,lvalue,rvalue,data, 0); +} + +int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int data, int data2) { unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size; RepairHashNode **ptr = &bucket[hashkey]; @@ -384,13 +389,14 @@ int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int (*ptr)->rule==rule && (*ptr)->lvalue==lvalue && (*ptr)->rvalue==rvalue && - (*ptr)->data == data) { + (*ptr)->data == data && + (*ptr)->data2 == data2) { return 0; } ptr = &((*ptr)->next); } - *ptr = new RepairHashNode(relation,rule,lvalue,rvalue, data); + *ptr = new RepairHashNode(relation,rule,lvalue,rvalue, data,data2); (*ptr)->lnext=nodelist; nodelist=*ptr; numelements++; @@ -424,6 +430,24 @@ int RepairHash::getset(int setv, int rule, int value) { return getrelation(setv||SETFLAG, rule, value,0); } +int RepairHash::getrelation2(int relation, int rule, int lvalue,int rvalue) { + unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size; + + RepairHashNode **ptr = &bucket[hashkey]; + + /* check that this key/object pair isn't already here */ + // TBD can be optimized for set v. relation */ + while (*ptr) { + if ((*ptr)->setrelation == relation && + (*ptr)->rule==rule && + (*ptr)->lvalue==lvalue && + (*ptr)->rvalue==rvalue) { + return (*ptr)->data2; + } + ptr = &((*ptr)->next); + } + return 0; +} int RepairHash::getrelation(int relation, int rule, int lvalue,int rvalue) { unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size; diff --git a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h index c55c255..da21f2f 100755 --- a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h +++ b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h @@ -170,11 +170,12 @@ class RepairHashNode { RepairHashNode *next; RepairHashNode *lnext; int data; + int data2; int setrelation; int lvalue; int rvalue; int rule; - RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data); + RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data, int data2); }; class RepairHash { @@ -191,10 +192,12 @@ public: ~RepairHash(); int addset(int setv, int rule, int value, int data); int addrelation(int relation, int rule, int lvalue, int rvalue, int data); + int addrelation(int relation, int rule, int lvalue, int rvalue, int data, int data2); bool containsset(int setv, int rule, int value); bool containsrelation(int relation, int rule, int lvalue, int rvalue); int getset(int setv, int rule, int value); int getrelation(int relation, int rule, int lvalue, int rvalue); + int getrelation2(int relation, int rule, int lvalue, int rvalue); }; #endif -- 2.34.1