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...

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index 626157cc152560c9e434a58ac74a37ea471ada29..88847f6759863eff7466c97016b7bc9f61bea129 100755 (executable)
--- 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 (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.7 2004/05/18 16:46:47 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.8 2004/05/31 14:19:10 bdemsky Exp $</tt>
  */
 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 f5dcfe15558f97eba1794f0957777708553b1a3e..5e184b42e043eb4b7e4546c66532a0db3435608f 100755 (executable)
--- 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 d36aabbd4496da5ce7288f31909f429801f282e8..c182a5dff656db18ef7166ec96683ee21d6bd64c 100755 (executable)
--- 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 59763b0e52420deccdd303f421b977a27ef878d3..9118096e2d3b57d52f897013202139acd8c11093 100755 (executable)
--- 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 62fbe050580f1094de3bead0d7e31366ba704ba8..f116cbfd4d235a22963a1906982f1e2de71c4c96 100755 (executable)
--- 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 766ae20ebd4e02b7b9e7d240eddc942a9ed2ff2a..aef0f28c02a8f62c9d973e9a8a94ee8c733fecc9 100755 (executable)
--- 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 dc66ecdc2f7eeb326c11961018175ea1fa81fa65..996083d21d8ebec5c8160a5b7b837e53a1ad3327 100755 (executable)
--- 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 f906386cc8598dbd2109cfdd8f595f031273cd8d..be4db265e6dca7c291888b1525f22dcb1c083907 100755 (executable)
--- 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 b9d09e1630fb540e0a176c9b695dc622b4e508b7..2a9e01af7b991fbf03d6ee3724fe5f271c4b6e85 100755 (executable)
--- 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 cb8f81eca87f58fa0e5d18b3200a70e70b5f8028..028c4b99ecf74715599ea290b58c1c8212df0260 100755 (executable)
--- 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;i<drule.size();i++) {
            RuleConjunction rconj=drule.get(i);
-           for(int j=0;j<rconj.size();j++){ 
+           for(int j=0;j<rconj.size();j++) { 
                DNFExpr dexpr=rconj.get(j);
                Expr e=dexpr.getExpr();
-               if (e.usesDescriptor(d)) {
+               Set descset=e.getRequiredDescriptors();
+               descset=SetDescriptor.expand(descset);
+               if (descset.contains(d)) {
                    boolean negated=dexpr.getNegation();
                    if (negated)
                        return NEGDEPENDENCY;

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 0dadae2701c75da28594875e956037c7c7950fb6..55aacfc30dc9ff1323f8ad2776facaba131504d6 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -36,12 +36,33 @@ public class OpExpr extends Expr {
        } else return llower;
     }
 
+
     public boolean isSafe() {
        if (right==null)
            return left.isSafe();
        return left.isSafe()&&right.isSafe();
     }
 
+    public boolean isInvariant(Set vars) {
+       return left.isInvariant(vars)&&((right==null)||right.isInvariant(vars));
+    }
+
+    public Set findInvariants(Set vars) {
+       if (isInt(this)) {
+           /* Don't hoist ints */
+           return new HashSet();
+       } else if (isInvariant(vars)) {
+           Set s=new HashSet();
+           s.add(this);
+           return s;
+       } else {
+           Set ls=left.findInvariants(vars);
+           if (right!=null)
+               ls.addAll(right.findInvariants(vars));
+           return ls;
+       }
+    }
+
     public Set getfunctions() {
        Set leftfunctions=left.getfunctions();
        Set rightfunctions=null;
@@ -327,7 +348,14 @@ public class OpExpr extends Expr {
 
     public void generate(CodeWriter writer, VarDescriptor dest) {
         VarDescriptor ld = VarDescriptor.makeNew("leftop");
-        left.generate(writer, ld);        
+       if (writer.getInvariantValue()!=null&&
+           writer.getInvariantValue().isInvariant(this)) {
+           writer.outputline("maybe="+writer.getInvariantValue().getMaybe(this).getSafeSymbol()+";");
+           writer.outputline("int "+dest.getSafeSymbol()+"="+writer.getInvariantValue().getValue(this).getSafeSymbol()+";");
+           return;
+       }
+
+        left.generate(writer, ld);
         VarDescriptor rd = null;
        VarDescriptor lm=VarDescriptor.makeNew("lm");
        VarDescriptor rm=VarDescriptor.makeNew("rm");
@@ -359,8 +387,7 @@ public class OpExpr extends Expr {
            writer.outputline("int "+rm.getSafeSymbol()+"=maybe;");
            writer.outputline("maybe = (!" + ld.getSafeSymbol() + " && " + rm.getSafeSymbol() + ") || (!" + rd.getSafeSymbol() +
                              " && " + lm.getSafeSymbol() + ") || (" + lm.getSafeSymbol() + " && " + rm.getSafeSymbol() + ");");
-           writer.outputline("int "+dest.getSafeSymbol() + " = " + ld.getSafeSymbol() + " || " + rd.getSafeSymbol() +
-                             ";");
+           writer.outputline("int "+dest.getSafeSymbol() + " = " + ld.getSafeSymbol() + " || " + rd.getSafeSymbol() + ";");
        } else if (opcode != Opcode.NOT) { /* two operands */
             assert rd != null;
             writer.outputline("int " + dest.getSafeSymbol() + " = " + 
@@ -401,23 +428,6 @@ public class OpExpr extends Expr {
 
         boolean ok = true;
 
-        // #ATTN#: if we want node.next != literal(0) to represent a null check than we need to allow ptr arithmetic
-        // either that or we use a isvalid clause to check for null
-
-        /*
-        if (lt != ReservedTypeDescriptor.INT) {
-            sa.getErrorReporter().report(null, "Left hand side of expression is of type '" + lt.getSymbol() + "' but must be type 'int'");
-            ok = false;
-        }
-
-        if (right != null) {
-            if (rt != ReservedTypeDescriptor.INT) {
-                sa.getErrorReporter().report(null, "Right hand side of expression is of type '" + rt.getSymbol() + "' but must be type 'int'");
-                ok = false;
-            }
-        }
-        */
-
         if (!ok) {
             return null;
         }

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index f0acb61f85864c7dd568b242b78fe09d40287de6..6074bbd504f07b78536f80471bdbacc67393d079 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -153,6 +153,9 @@ public class RepairGenerator {
                    }
                    craux.startblock();
                    craux.outputline("int maybe=0;");
+                   if (Compiler.GENERATEINSTRUMENT)
+                       craux.outputline("updatecount++;");
+
                    final SymbolTable st = un.getRule().getSymbolTable();                
                    CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
@@ -184,6 +187,8 @@ public class RepairGenerator {
                    craux.outputline(methodcall);
                    craux.startblock();
                    craux.outputline("int maybe=0;");
+                   if (Compiler.GENERATEINSTRUMENT)
+                       craux.outputline("updatecount++;");
                    final SymbolTable st2 = un.getRule().getSymbolTable();
                    CodeWriter cr2 = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st2; }
@@ -217,6 +222,8 @@ public class RepairGenerator {
                    craux.outputline(methodcall);
                    craux.startblock();
                    craux.outputline("int maybe=0;");
+                   if (Compiler.GENERATEINSTRUMENT)
+                       craux.outputline("updatecount++;");
                    final SymbolTable st2 = un.getRule().getSymbolTable();
                    CodeWriter cr2 = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st2; }
@@ -465,9 +472,21 @@ public class RepairGenerator {
        worklist=VarDescriptor.makeNew("worklist");
        goodflag=VarDescriptor.makeNew("goodflag");
        repairtable=VarDescriptor.makeNew("repairtable");
+
+       if (Compiler.GENERATEINSTRUMENT) {
+           craux.outputline("int updatecount;");
+           craux.outputline("int rebuildcount;");
+           craux.outputline("int abstractcount;");
+       }
+       
        crhead.outputline("void doanalysis();");
        craux.outputline("void "+name +"_state::doanalysis()");
        craux.startblock();
+       if (Compiler.GENERATEINSTRUMENT) {
+           craux.outputline("updatecount=0;");
+           craux.outputline("rebuildcount=0;");
+           craux.outputline("abstractcount=0;");
+       }
        craux.outputline("int highmark;");
        craux.outputline("initializestack(&highmark);");
        craux.outputline("typeobject *typeobject1=gettypeobject();");
@@ -480,11 +499,19 @@ public class RepairGenerator {
        craux.startblock();
        craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
        craux.outputline(worklist.getSafeSymbol()+"->reset();");
+       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<ruleset.size();i++) {
+                   Rule itrule=(Rule)ruleset.get(i);
                    
-                   String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
-                       repairtable.getSafeSymbol();
-                   for(int i=0;i<currentrule.numQuantifiers();i++) {
-                       Quantifier q=currentrule.getQuantifier(i);
-                       if (q instanceof SetQuantifier) {
-                           SetQuantifier sq=(SetQuantifier) q;
-                           methodcall+=","+sq.getVar().getSafeSymbol();
-                       } else if (q instanceof RelationQuantifier) {
-                           RelationQuantifier rq=(RelationQuantifier) q;
-                           methodcall+=","+rq.x.getSafeSymbol();
-                           methodcall+=","+rq.y.getSafeSymbol();
-                       } else if (q instanceof ForQuantifier) {
-                           ForQuantifier fq=(ForQuantifier) q;
-                           methodcall+=","+fq.getVar().getSafeSymbol();
+                   if (need_compensation(itrule)) {
+                       UpdateNode un=find_compensation(itrule);
+                       String name=(String)updatenames.get(un);
+                       usedupdates.add(un); /* Mark as used */
+                       
+                       String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
+                           repairtable.getSafeSymbol();
+                       for(int j=0;j<currentrule.numQuantifiers();j++) {
+                           Quantifier q=currentrule.getQuantifier(j);
+                           if (q instanceof SetQuantifier) {
+                               SetQuantifier sq=(SetQuantifier) q;
+                               methodcall+=","+sq.getVar().getSafeSymbol();
+                           } else if (q instanceof RelationQuantifier) {
+                               RelationQuantifier rq=(RelationQuantifier) q;
+                               methodcall+=","+rq.x.getSafeSymbol();
+                               methodcall+=","+rq.y.getSafeSymbol();
+                           } else if (q instanceof ForQuantifier) {
+                               ForQuantifier fq=(ForQuantifier) q;
+                               methodcall+=","+fq.getVar().getSafeSymbol();
+                           }
                        }
+                       methodcall+=");";
+                       if (currentrule!=itrule) {
+                           SetDescriptor sdrule=((SetInclusion)itrule.getInclusion()).getSet();
+                           cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
+                           cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+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 f60a00765c7dfa16d04614a07dfc70a1d417a6d7..ebe552e12a370326ea7fc666e6da66ecbb2d7d3c 100755 (executable)
--- 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 f7e19dcb49663b79c18bb89117044cc7232ada8a..347d1f9c7bba8a1483e8cb56659d0fcc38f671ef 100755 (executable)
--- 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 db9e44324bb1a23c81a680bd503bd62953d2f858..b25e5430780079719b2d6fbc662377bfe1a2381d 100755 (executable)
--- 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 c1579f22fe40dbe70ff1ef16943679dec9273624..77beed787a1e7cafc4aaaa02f4dd9eceabef518e 100755 (executable)
--- 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 19d18dcc84302bc917a9b20606d72bcdf543ac9d..a5299e396c7bf706747b6fbe609060658db317d4 100755 (executable)
--- 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 4832151c2566a48a5c49e3de6b42f97e0fb81785..b3a42b93b50523611504b3b90a88358f14293b38 100755 (executable)
--- 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<MAXFILES;i++)
       files[i].used=false;

diff --git a/Repair/RepairCompiler/MCC/State.java b/Repair/RepairCompiler/MCC/State.java
index 024aed37ec7aa0a555c5f001e983a23bf73e0a0b..a12d675903e15180b3f6ae79d7d0b0d06b3edd22 100755 (executable)
--- a/Repair/RepairCompiler/MCC/State.java
+++ b/Repair/RepairCompiler/MCC/State.java
@@ -34,6 +34,7 @@ public class State {
     public Hashtable rulenodes;
     public Hashtable constraintnodes;    
     public Hashtable implicitrule;
+    public Hashtable implicitruleinv;
     State() {
         vConstraints = null;
         vRules = null;
@@ -48,6 +49,7 @@ public class State {
         ptConstraints = null;
         ptSpace = null;
        implicitrule=new Hashtable();
+       implicitruleinv=new Hashtable();
     }
 
     void printall() {