From ad9c0159edd8dd9eed39eb8f74635c5bffb95ed5 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 31 May 2004 14:19:40 +0000 Subject: [PATCH] 1) Instrumentation code to count model rebuilds, etc... 2) Don't generate code for model definition rules made to make set constraints explicit. 3) Loop invariant hoisting. We're not too aggressive here... 4) Mechanism to store precomputed values of exprs (for 3) 5) Improvements to Hash function - it now rehashes... --- Repair/RepairCompiler/MCC/CLI.java | 4 +- Repair/RepairCompiler/MCC/Compiler.java | 1 + Repair/RepairCompiler/MCC/IR/CastExpr.java | 18 +-- Repair/RepairCompiler/MCC/IR/CodeWriter.java | 3 +- Repair/RepairCompiler/MCC/IR/DotExpr.java | 42 ++++++ Repair/RepairCompiler/MCC/IR/Expr.java | 6 + .../RepairCompiler/MCC/IR/ImplicitSchema.java | 4 + .../MCC/IR/IntegerLiteralExpr.java | 1 - Repair/RepairCompiler/MCC/IR/LiteralExpr.java | 7 + .../MCC/IR/ModelRuleDependence.java | 6 +- Repair/RepairCompiler/MCC/IR/OpExpr.java | 50 ++++--- .../MCC/IR/RepairGenerator.java | 138 ++++++++++++++---- .../MCC/IR/StandardCodeWriter.java | 10 +- .../MCC/IR/StructureTypeDescriptor.java | 22 ++- Repair/RepairCompiler/MCC/IR/VarExpr.java | 22 ++- .../RepairCompiler/MCC/Runtime/SimpleHash.cc | 71 +++++---- .../RepairCompiler/MCC/Runtime/buildruntime | 13 +- Repair/RepairCompiler/MCC/Runtime/danfile.cc | 6 +- Repair/RepairCompiler/MCC/State.java | 2 + 19 files changed, 325 insertions(+), 101 deletions(-) diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java index 626157c..88847f6 100755 --- a/Repair/RepairCompiler/MCC/CLI.java +++ b/Repair/RepairCompiler/MCC/CLI.java @@ -11,7 +11,7 @@ import java.util.StringTokenizer; * files. * * @author le01, 6.035 Staff (6.035-staff@mit.edu) - * @version $Id: CLI.java,v 1.7 2004/05/18 16:46:47 bdemsky Exp $ + * @version $Id: CLI.java,v 1.8 2004/05/31 14:19:10 bdemsky Exp $ */ public class CLI { /** @@ -106,6 +106,8 @@ public class CLI { Compiler.REPAIR=false; } else if (args[i].equals("-debug")) { Compiler.GENERATEDEBUGHOOKS=true; + } else if (args[i].equals("-instrument")) { + Compiler.GENERATEINSTRUMENT=true; } else if (args[i].equals("-aggressivesearch")) { Compiler.AGGRESSIVESEARCH=true; } else if (args[i].equals("-prunequantifiernodes")) { diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index f5dcfe1..5e184b4 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -23,6 +23,7 @@ public class Compiler { public static boolean PRUNEQUANTIFIERS=false; public static boolean GENERATEDEBUGHOOKS=false; public static boolean GENERATEDEBUGPRINT=false; + public static boolean GENERATEINSTRUMENT=false; public static void main(String[] args) { State state = null; diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java index d36aabb..c182a5d 100755 --- a/Repair/RepairCompiler/MCC/IR/CastExpr.java +++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java @@ -15,6 +15,14 @@ public class CastExpr extends Expr { return expr; } + public boolean isInvariant(Set vars) { + return false; + } + + public Set findInvariants(Set vars) { + return expr.findInvariants(vars); + } + public void findmatch(Descriptor d, Set s) { expr.findmatch(d,s); } @@ -77,17 +85,7 @@ public class CastExpr extends Expr { sa.getErrorReporter().report(null, "Expression type '" + td.getSymbol() + "' is not a parent of the cast type '" + type.getSymbol() + "'"); return null; } - this.td = type; return type; } - } - - - - - - - - diff --git a/Repair/RepairCompiler/MCC/IR/CodeWriter.java b/Repair/RepairCompiler/MCC/IR/CodeWriter.java index 59763b0..9118096 100755 --- a/Repair/RepairCompiler/MCC/IR/CodeWriter.java +++ b/Repair/RepairCompiler/MCC/IR/CodeWriter.java @@ -11,5 +11,6 @@ public interface CodeWriter extends PrettyPrinter{ public void pushSymbolTable(SymbolTable st); public SymbolTable popSymbolTable(); public SymbolTable getSymbolTable(); - + public InvariantValue getInvariantValue(); + public void setInvariantValue(InvariantValue iv); } diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java index 62fbe05..f116cbf 100755 --- a/Repair/RepairCompiler/MCC/IR/DotExpr.java +++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java @@ -20,6 +20,40 @@ public class DotExpr extends Expr { this.index = index; } + public boolean isInvariant(Set vars) { + if (!left.isInvariant(vars)) + return false; + if (intindex!=null) + return intindex.isInvariant(vars); + else + return true; + } + + public Set findInvariants(Set vars) { + if (isInvariant(vars)) { + Set s=new HashSet(); + s.add(this); + return s; + } else { + Set ls=left.findInvariants(vars); + if (intindex!=null) { + ls.addAll(intindex.findInvariants(vars)); + Expr indexbound=((ArrayDescriptor)this.fd).getIndexBound(); + ls.addAll(indexbound.findInvariants(vars)); + if ((!(intindex instanceof IntegerLiteralExpr))|| + ((IntegerLiteralExpr) intindex).getValue() != 0) { + FieldDescriptor fd=this.fd; + if (fd instanceof ArrayDescriptor) + fd=((ArrayDescriptor)fd).getField(); + Expr basesize = fd.getBaseSizeExpr(); + ls.addAll(basesize.findInvariants(vars)); + } + } + return ls; + } + } + + public boolean isSafe() { if (!left.isSafe()) return false; @@ -131,6 +165,14 @@ public class DotExpr extends Expr { public void generate(CodeWriter writer, VarDescriptor dest) { VarDescriptor leftd = VarDescriptor.makeNew("left"); + if (writer.getInvariantValue()!=null&& + writer.getInvariantValue().isInvariant(this)) { + writer.outputline("maybe="+writer.getInvariantValue().getMaybe(this).getSafeSymbol()+";"); + writer.outputline(getType().getGenerateType().getSafeSymbol()+ + " "+dest.getSafeSymbol()+"="+writer.getInvariantValue().getValue(this).getSafeSymbol()+";"); + return; + } + writer.output("// " + leftd.getSafeSymbol() + " <-- "); left.prettyPrint(writer); writer.outputline(""); diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java index 766ae20..aef0f28 100755 --- a/Repair/RepairCompiler/MCC/IR/Expr.java +++ b/Repair/RepairCompiler/MCC/IR/Expr.java @@ -93,4 +93,10 @@ public abstract class Expr { public Expr getUpper() { return null; } + public boolean isInvariant(Set vars) { + return false; + } + public Set findInvariants(Set vars) { + return new HashSet(); + } } diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java index dc66ecd..996083d 100755 --- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java +++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java @@ -322,8 +322,12 @@ public class ImplicitSchema { nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1); nr.st=r.st; nr.setnogenerate(); + nr.num=r.num; newrules.add(nr); state.implicitrule.put(nr,r); + if (!state.implicitruleinv.containsKey(r)) + state.implicitruleinv.put(r,new HashSet()); + ((Set)state.implicitruleinv.get(r)).add(nr); } } } diff --git a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java index f906386..be4db26 100755 --- a/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java +++ b/Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java @@ -46,5 +46,4 @@ public class IntegerLiteralExpr extends LiteralExpr { td = ReservedTypeDescriptor.INT; return td; } - } diff --git a/Repair/RepairCompiler/MCC/IR/LiteralExpr.java b/Repair/RepairCompiler/MCC/IR/LiteralExpr.java index b9d09e1..2a9e01a 100755 --- a/Repair/RepairCompiler/MCC/IR/LiteralExpr.java +++ b/Repair/RepairCompiler/MCC/IR/LiteralExpr.java @@ -12,4 +12,11 @@ public abstract class LiteralExpr extends Expr { return new HashSet(); } + public boolean isInvariant(Set vars) { + return true; + } + + public Set findInvariants(Set vars) { + return new HashSet(); /* We won't lift literals...gcc can do this */ + } } diff --git a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java index cb8f81e..028c4b9 100755 --- a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java +++ b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java @@ -129,10 +129,12 @@ class ModelRuleDependence { boolean dependency=false; for(int i=0;ireset();"); + if (Compiler.GENERATEINSTRUMENT) + craux.outputline("rebuildcount++;"); } private void generate_teardown() { CodeWriter cr = new StandardCodeWriter(outputaux); cr.endblock(); + if (Compiler.GENERATEINSTRUMENT) { + cr.outputline("printf(\"updatecount=%d\\n\",updatecount);"); + cr.outputline("printf(\"rebuildcount=%d\\n\",rebuildcount);"); + cr.outputline("printf(\"abstractcount=%d\\n\",abstractcount);"); + } + } private void generate_print() { @@ -547,15 +574,54 @@ public class RepairGenerator { Iterator iterator_rs = ruleset.iterator(); while (iterator_rs.hasNext()) { Rule rule = (Rule) iterator_rs.next(); + if (rule.getnogenerate()) + continue; { final SymbolTable st = rule.getSymbolTable(); CodeWriter cr = new StandardCodeWriter(outputaux) { public SymbolTable getSymbolTable() { return st; } }; + InvariantValue ivalue=new InvariantValue(); + cr.setInvariantValue(ivalue); + cr.outputline("// build " +escape(rule.toString())); cr.startblock(); cr.outputline("int maybe=0;"); - ListIterator quantifiers = rule.quantifiers(); + + Expr ruleexpr=rule.getGuardExpr(); + HashSet invariantvars=new HashSet(); + Set invariants=ruleexpr.findInvariants(invariantvars); + + if ((ruleexpr instanceof BooleanLiteralExpr)&& + ((BooleanLiteralExpr)ruleexpr).getValue()) { + if (rule.getInclusion() instanceof SetInclusion) { + invariants.addAll(((SetInclusion)rule.getInclusion()).getExpr().findInvariants(invariantvars)); + } else if (rule.getInclusion() instanceof RelationInclusion) { + invariants.addAll(((RelationInclusion)rule.getInclusion()).getLeftExpr().findInvariants(invariantvars)); + invariants.addAll(((RelationInclusion)rule.getInclusion()).getRightExpr().findInvariants(invariantvars)); + } + } + ListIterator quantifiers = rule.quantifiers(); + while (quantifiers.hasNext()) { + Quantifier quantifier = (Quantifier) quantifiers.next(); + if (quantifier instanceof ForQuantifier) { + ForQuantifier fq=(ForQuantifier)quantifier; + invariants.addAll(fq.lower.findInvariants(invariantvars)); + invariants.addAll(fq.upper.findInvariants(invariantvars)); + } + } + + for(Iterator invit=invariants.iterator();invit.hasNext();) { + Expr invexpr=(Expr)invit.next(); + VarDescriptor tmpvd=VarDescriptor.makeNew("tmpvar"); + VarDescriptor maybevd=VarDescriptor.makeNew("maybevar"); + invexpr.generate(cr,tmpvd); + cr.outputline("int "+maybevd.getSafeSymbol()+"=maybe;"); + cr.outputline("maybe=0;"); + ivalue.assignPair(invexpr,tmpvd,maybevd); + } + + quantifiers = rule.quantifiers(); while (quantifiers.hasNext()) { Quantifier quantifier = (Quantifier) quantifiers.next(); quantifier.generate_open(cr); @@ -809,6 +875,8 @@ public class RepairGenerator { else cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")"); cr.startblock(); + if (Compiler.GENERATEINSTRUMENT) + cr.outputline("abstractcount++;"); if (p instanceof InclusionPredicate) generateinclusionrepair(conj,dpred, cr); else if (p instanceof ExprPredicate) { @@ -1524,14 +1592,13 @@ public class RepairGenerator { public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) { - - cr.outputline("// SET DISPATCH "); + cr.outputline("// SET DISPATCH "); if (Compiler.REPAIR) { cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&"); cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))"); cr.startblock(); { /* Adding new item */ - /* Perform safety checks */ + /* See if there is an outstanding update in the repairtable */ cr.outputline("if ("+repairtable.getSafeSymbol()+"&&"); cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))"); cr.startblock(); { @@ -1569,34 +1636,50 @@ public class RepairGenerator { } cr.endblock(); /* Build standard compensation actions */ - if (need_compensation(currentrule)) { - UpdateNode un=find_compensation(currentrule); - String name=(String)updatenames.get(un); - usedupdates.add(un); /* Mark as used */ + Vector ruleset=new Vector(); + ruleset.add(currentrule); + if (state.implicitruleinv.containsKey(currentrule)) + ruleset.addAll((Set)state.implicitruleinv.get(currentrule)); + for(int i=0;i"+sdrule.getJustSafeSymbol()+"_hash->contains("+setvar+"))"); + cr.startblock(); + } + cr.outputline(methodcall); + cr.outputline("delete "+newmodel.getSafeSymbol()+";"); + cr.outputline("goto rebuild;"); + cr.endblock(); } - methodcall+=");"; - cr.outputline(methodcall); - cr.outputline("delete "+newmodel.getSafeSymbol()+";"); - cr.outputline("goto rebuild;"); + if (currentrule==itrule) + cr.endblock(); } } - cr.endblock(); } String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol(); @@ -1622,6 +1705,7 @@ public class RepairGenerator { cr.endblock(); return; } + /* Add item to worklist if new */ cr.outputline("if ("+addeditem+")"); cr.startblock(); for(int i = 0; i < dispatchrules.size(); i++) { diff --git a/Repair/RepairCompiler/MCC/IR/StandardCodeWriter.java b/Repair/RepairCompiler/MCC/IR/StandardCodeWriter.java index f60a007..ebe552e 100755 --- a/Repair/RepairCompiler/MCC/IR/StandardCodeWriter.java +++ b/Repair/RepairCompiler/MCC/IR/StandardCodeWriter.java @@ -8,6 +8,7 @@ public class StandardCodeWriter implements CodeWriter { int indent = 0; java.io.PrintWriter output; Stack symboltables = new Stack(); + InvariantValue ivalue; public StandardCodeWriter(java.io.PrintWriter output) { this.output = output; } @@ -67,5 +68,12 @@ public class StandardCodeWriter implements CodeWriter { } return (SymbolTable) symboltables.peek(); } - + + public InvariantValue getInvariantValue() { + return ivalue; + } + + public void setInvariantValue(InvariantValue iv) { + ivalue=iv; + } } diff --git a/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java b/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java index f7e19dc..347d1f9 100755 --- a/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java +++ b/Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java @@ -28,13 +28,31 @@ public class StructureTypeDescriptor extends TypeDescriptor { public Enumeration getFieldKeys() { return fields.keys(); } - - public Expr getSizeExpr() { + public Expr getSizeExpr() { return getOffsetExpr(null); } + Expr sizeexpr=null; + Hashtable oexpr=new Hashtable(); + public Expr getOffsetExpr(FieldDescriptor field) { + if (field==null) { + if (sizeexpr==null) { + sizeexpr=internalgetOffsetExpr(field); + } + return sizeexpr; + } else if (oexpr.containsKey(field)) { + return (Expr)oexpr.get(field); + } else { + Expr tmp=internalgetOffsetExpr(field); + oexpr.put(field,tmp); + return tmp; + } + } + + + private Expr internalgetOffsetExpr(FieldDescriptor field) { /* Fix sizeof calculations */ if ((field==null)&&(subtype!=null)) return subtype.getSizeExpr(); diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java index db9e443..b25e543 100755 --- a/Repair/RepairCompiler/MCC/IR/VarExpr.java +++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java @@ -92,12 +92,32 @@ public class VarExpr extends Expr { return vd.isGlobal(); } - public void generate(CodeWriter writer, VarDescriptor dest) { + public boolean isInvariant(Set vars) { + return vd.isGlobal()||vars.contains(vd); + } + + public Set findInvariants(Set vars) { + if (isInvariant(vars)) { + Set s=new HashSet(); + s.add(this); + return s; + } else + return new HashSet(); + } + + public void generate(CodeWriter writer, VarDescriptor dest) { // #TBD#: bit of a hack, really should have been type checked properly assert vd != null; assert vd.getType() != null; this.td = vd.getType(); + if (writer.getInvariantValue()!=null&& + writer.getInvariantValue().isInvariant(this)) { + writer.outputline("maybe="+writer.getInvariantValue().getMaybe(this).getSafeSymbol()+";"); + writer.outputline(vd.getType().getGenerateType().getSafeSymbol()+ + " "+dest.getSafeSymbol()+"="+writer.getInvariantValue().getValue(this).getSafeSymbol()+";"); + return; + } writer.outputline(vd.getType().getGenerateType().getSafeSymbol() + " " + dest.getSafeSymbol() + " = (" + vd.getType().getGenerateType().getSafeSymbol() + ") " + vd.getSafeSymbol() + "; //varexpr"); diff --git a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc index c1579f2..77beed7 100755 --- a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc +++ b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc @@ -232,36 +232,53 @@ int SimpleHash::remove(int key, int data) { int SimpleHash::add(int key, int data) { - unsigned int hashkey = (unsigned int)key % size; - - struct SimpleNode **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)->key == key && (*ptr)->data == data) { - return 0; - } - ptr = &((*ptr)->next); - } - if (tailindex==ARRAYSIZE) { - listtail->nextarray=(struct ArraySimple *) calloc(sizeof(struct ArraySimple),1); - tailindex=0; - listtail=listtail->nextarray; + /* Rehash code */ + if (numelements>=size) { + int newsize=2*size+1; + struct SimpleNode ** newbucket = (struct SimpleNode **) calloc(sizeof(struct SimpleNode *)*newsize,1); + for(int i=size-1;i>=0;i--) { + for(struct SimpleNode *ptr=bucket[i];ptr!=NULL;) { + struct SimpleNode * nextptr=ptr->next; + unsigned int newhashkey=(unsigned int)ptr->key % newsize; + ptr->next=newbucket[newhashkey]; + newbucket[newhashkey]=ptr; + ptr=nextptr; + } } - - *ptr = &listtail->nodes[tailindex++]; - (*ptr)->key=key; - (*ptr)->data=data; - (*ptr)->inuse=1; + size=newsize; + free(bucket); + bucket=newbucket; + } - numelements++; - - for (int i = 0; i < numparents; i++) { - parents[i]->add(key, data); - } + unsigned int hashkey = (unsigned int)key % size; + struct SimpleNode **ptr = &bucket[hashkey]; + + /* check that this key/object pair isn't already here */ + /* TBD can be optimized for set v. relation */ - return 1; + while (*ptr) { + if ((*ptr)->key == key && (*ptr)->data == data) { + return 0; + } + ptr = &((*ptr)->next); + } + if (tailindex==ARRAYSIZE) { + listtail->nextarray=(struct ArraySimple *) calloc(sizeof(struct ArraySimple),1); + tailindex=0; + listtail=listtail->nextarray; + } + + *ptr = &listtail->nodes[tailindex++]; + (*ptr)->key=key; + (*ptr)->data=data; + (*ptr)->inuse=1; + + numelements++; + + for (int i = 0; i < numparents; i++) { + parents[i]->add(key, data); + } + return 1; } bool SimpleHash::contains(int key) { diff --git a/Repair/RepairCompiler/MCC/Runtime/buildruntime b/Repair/RepairCompiler/MCC/Runtime/buildruntime index 19d18dc..a5299e3 100755 --- a/Repair/RepairCompiler/MCC/Runtime/buildruntime +++ b/Repair/RepairCompiler/MCC/Runtime/buildruntime @@ -1,7 +1,8 @@ #!/bin/bash -g++ -g -c SimpleHash.cc -g++ -g -c tmap.cc -g++ -g -c instrument.cc -gcc -g -c libredblack/redblack.c -gcc -g -c stack.c -g++ -g -c size.cc +FLAG='-O9' +g++ $FLAG -c SimpleHash.cc +g++ $FLAG -c tmap.cc +g++ $FLAG -c instrument.cc +gcc $FLAG -c libredblack/redblack.c +gcc $FLAG -c stack.c +g++ $FLAG -c size.cc diff --git a/Repair/RepairCompiler/MCC/Runtime/danfile.cc b/Repair/RepairCompiler/MCC/Runtime/danfile.cc index 4832151..b3a42b9 100755 --- a/Repair/RepairCompiler/MCC/Runtime/danfile.cc +++ b/Repair/RepairCompiler/MCC/Runtime/danfile.cc @@ -440,7 +440,7 @@ int main(int argc, char **argv) time += selfcheck2(ptr); - printf("\ncompiled: %u us\n", (time/50)); + printf("\ncompiled: %u us\n", (time)); break; } @@ -529,6 +529,8 @@ int main(int argc, char **argv) case '8': { { struct block * ptr=chmountdisk("disk"); + int t=selfcheck2(ptr); + printf("\ncompiled: %u us\n", (t)); chunmountdisk(ptr); } struct block * ptr=mountdisk("disk"); @@ -569,7 +571,7 @@ int main(int argc, char **argv) } unmountdisk(ptr); } - + break; case '9': { for(int i=0;i