1) Instrumentation code to count model rebuilds, etc...
authorbdemsky <bdemsky>
Mon, 31 May 2004 14:19:40 +0000 (14:19 +0000)
committerbdemsky <bdemsky>
Mon, 31 May 2004 14:19:40 +0000 (14:19 +0000)
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...

19 files changed:
Repair/RepairCompiler/MCC/CLI.java
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/CastExpr.java
Repair/RepairCompiler/MCC/IR/CodeWriter.java
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java
Repair/RepairCompiler/MCC/IR/LiteralExpr.java
Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/StandardCodeWriter.java
Repair/RepairCompiler/MCC/IR/StructureTypeDescriptor.java
Repair/RepairCompiler/MCC/IR/VarExpr.java
Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc
Repair/RepairCompiler/MCC/Runtime/buildruntime
Repair/RepairCompiler/MCC/Runtime/danfile.cc
Repair/RepairCompiler/MCC/State.java

index 626157c..88847f6 100755 (executable)
@@ -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")) {
index f5dcfe1..5e184b4 100755 (executable)
@@ -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;
index d36aabb..c182a5d 100755 (executable)
@@ -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;
     }
-
 }
-
-
-
-
-
-
-
-
index 59763b0..9118096 100755 (executable)
@@ -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);
 }
index 62fbe05..f116cbf 100755 (executable)
@@ -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("");
index 766ae20..aef0f28 100755 (executable)
@@ -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();
+    }
 }
index dc66ecd..996083d 100755 (executable)
@@ -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);
                    }
            }
        }
index f906386..be4db26 100755 (executable)
@@ -46,5 +46,4 @@ public class IntegerLiteralExpr extends LiteralExpr {
         td = ReservedTypeDescriptor.INT;
         return td;
     }
-
 }
index b9d09e1..2a9e01a 100755 (executable)
@@ -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 */
+    }
 }
index cb8f81e..028c4b9 100755 (executable)
@@ -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;
index 0dadae2..55aacfc 100755 (executable)
@@ -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;
         }
index f0acb61..6074bbd 100755 (executable)
@@ -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++) {
index f60a007..ebe552e 100755 (executable)
@@ -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;
+    }
 }
index f7e19dc..347d1f9 100755 (executable)
@@ -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();
index db9e443..b25e543 100755 (executable)
@@ -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");
index c1579f2..77beed7 100755 (executable)
@@ -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) {
index 19d18dc..a5299e3 100755 (executable)
@@ -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
index 4832151..b3a42b9 100755 (executable)
@@ -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;
index 024aed3..a12d675 100755 (executable)
@@ -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() {