optimized works

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 7ea9362de66b9d1660172afdc5f46c6ccf59e3a2..bca936ca67a94183ab71d8abf11176aef767c2b2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -76,8 +76,14 @@ public class Compiler {
             
             try {
                 FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
+
+                // do model optimizations
+                (new Optimizer(state)).optimize();
+
                 NaiveGenerator ng = new NaiveGenerator(state);
                 ng.generate(gcode);
+                //WorklistGenerator wg = new WorklistGenerator(state);
+                //wg.generate(gcode);
                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();

diff --git a/Repair/RepairCompiler/MCC/IR/CodeWriter.java b/Repair/RepairCompiler/MCC/IR/CodeWriter.java
index f2fcd2c5e7ab5caaeef359e417a84bc2272cace2..59763b0e52420deccdd303f421b977a27ef878d3 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CodeWriter.java
+++ b/Repair/RepairCompiler/MCC/IR/CodeWriter.java
@@ -8,6 +8,8 @@ public interface CodeWriter extends PrettyPrinter{
     public void startblock();
     public void endblock();
 
+    public void pushSymbolTable(SymbolTable st);
+    public SymbolTable popSymbolTable();
     public SymbolTable getSymbolTable();
     
 }

diff --git a/Repair/RepairCompiler/MCC/IR/Constraint.java b/Repair/RepairCompiler/MCC/IR/Constraint.java
index 61f9b90a25376478fd2b8de1d10bfaa97c1a4416..852313a87d9b169ece1c110c9df229d92d2bcb08 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Constraint.java
+++ b/Repair/RepairCompiler/MCC/IR/Constraint.java
@@ -12,10 +12,17 @@ public class Constraint {
     Vector quantifiers = new Vector(); 
     LogicStatement logicstatement = null;
 
+    int num;
+
     public Constraint() {
+        num = count;
         label = new String("c" + count++);
     }
 
+    public int getNum() {
+        return num;
+    }
+
     public String getLabel() {
         return label;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index b5d0243630c93e7d88eb3eae0ee3e492361f14ce..5336065a8855a3f4e34e7b93cb70e087ba09764c 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -36,6 +36,10 @@ public class DotExpr extends Expr {
         return v;
     }
 
+    public Expr getExpr() {
+        return left;
+    }
+
     public void generate(CodeWriter writer, VarDescriptor dest) {
         VarDescriptor leftd = VarDescriptor.makeNew("left");
 

diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index b5481c3d2a96bc056a01b6636aead86e4cd16a6b..1e7fd14eb6182b35f621895dcbd855734b11d2b8 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -21,4 +21,8 @@ public abstract class Expr {
 
     public abstract void prettyPrint(PrettyPrinter pp);
 
+    public Set getInversedRelations() {
+        throw new IRException("unsupported");
+    }
+
 }

diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index 52adc76758950df0f38d163073abde502d450384..c7f507965e822624f2a97430e90ce28c3d10b787 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
@@ -22,6 +22,22 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = inverse;
     }
 
+    public VarDescriptor getVar() {
+        return vd;
+    }
+
+    public RelationDescriptor getRelation() {
+        return rd;
+    }
+
+    public Set getInversedRelations() {
+        HashSet set = new HashSet();
+        if (inverse) {
+            set.add(rd);
+        }
+        return set;
+    }
+
     public Set getRequiredDescriptors() {
         HashSet v = new HashSet();
         v.add(rd);
@@ -46,7 +62,12 @@ public class ImageSetExpr extends SetExpr {
     }
 
     public void prettyPrint(PrettyPrinter pp) {
-        throw new IRException("not supported");
+        pp.output(vd.toString());
+        pp.output(".");
+        if (inverse) {
+            pp.output("~");
+        }
+        pp.output(rd.toString());
     }
 
     public TypeDescriptor typecheck(SemanticAnalyzer sa) {

diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index cbe703772393f9a38382b1e0024e61884e5ed62e..fd4d8ff9e6d869f987bbb5391c9a964f832dfb97 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -31,6 +31,15 @@ public class InclusionPredicate extends Predicate {
         expr.generate(writer, var);
         setexpr.generate_inclusion(writer, dest, var);
     }
+
+    public Set getInversedRelations() {
+
+        throw new IRException("unsupported");
+
+        //Set set = setexpr.getInversedRelations();
+        //set.addAll(expr.getInversedRelations());
+        //return set;
+    }
             
 }
     

diff --git a/Repair/RepairCompiler/MCC/IR/LiteralExpr.java b/Repair/RepairCompiler/MCC/IR/LiteralExpr.java
index df14ed1877dda3179beb9e5668d023fecd96f9f8..b9d09e1630fb540e0a176c9b695dc622b4e508b7 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/LiteralExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/LiteralExpr.java
@@ -8,4 +8,8 @@ public abstract class LiteralExpr extends Expr {
         return new HashSet();
     }
 
+    public Set getInversedRelations() {
+        return new HashSet();
+    }
+
 }

diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index 43fb985118580afedc3db675b03fbfe9a9f287b0..9c3a1ed335e7a46e4796fb4449bfcd77b6da8877 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -7,6 +7,18 @@ public class LogicStatement {
     public static final Operation AND = new Operation("AND");
     public static final Operation OR = new Operation("OR");
     public static final Operation NOT = new Operation("NOT");
+
+    public Set getInversedRelations() {
+        if (left == null) {
+            throw new IRException();
+        }
+
+        Set set = left.getInversedRelations();
+        if (right != null) {
+            set.addAll(right.getInversedRelations());
+        }
+        return set;
+    }
     
     public static class Operation {
         private final String name;

diff --git a/Repair/RepairCompiler/MCC/IR/NaiveGenerator.java b/Repair/RepairCompiler/MCC/IR/NaiveGenerator.java
index dd460118b2f8ae66f14e7f8b732f0736f242f20e..08ed84d6325ddd44a83d3a90faed431f3d758cf5 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/NaiveGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/NaiveGenerator.java
@@ -117,12 +117,15 @@ public class NaiveGenerator {
             GraphNode rulenode = (GraphNode) rules.next();
             Rule rule = (Rule) rulenode.getOwner();            
 
+            if (!state.vRules.contains(rule)) {
+                // this is no longer a top-level rule
+                continue;
+            }
+
             {
 
-                final SymbolTable st = rule.getSymbolTable();                
-                CodeWriter cr = new StandardCodeWriter(output) {
-                        public SymbolTable getSymbolTable() { return st; }
-                    };
+                CodeWriter cr = new StandardCodeWriter(output);
+                cr.pushSymbolTable(rule.getSymbolTable()); 
                 
                 cr.outputline("// build " + rule.getLabel());
                 cr.startblock();
@@ -187,11 +190,8 @@ public class NaiveGenerator {
 
             {
 
-                final SymbolTable st = constraint.getSymbolTable();
-                
-                CodeWriter cr = new StandardCodeWriter(output) {
-                        public SymbolTable getSymbolTable() { return st; }
-                    };
+                CodeWriter cr = new StandardCodeWriter(output);
+                cr.pushSymbolTable(constraint.getSymbolTable());
                 
                 cr.outputline("// checking " + constraint.getLabel());
                 cr.startblock();
@@ -213,14 +213,16 @@ public class NaiveGenerator {
                 cr.outputline("if (maybe)");
                 cr.startblock();
                 cr.outputline("__Success = 0;");
-                cr.outputline("printf(\"maybe fail " + (i+1) + ". \");");
+                cr.outputline("printf(\"maybe fail " + constraint.getNum() + ". \");");
+                cr.outputline("exit(1);");
                 cr.endblock();
 
                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
                 cr.startblock();
 
                 cr.outputline("__Success = 0;");
-                cr.outputline("printf(\"fail " + (i+1) + ". \");");
+                cr.outputline("printf(\"fail " + constraint.getNum() + ". \");");
+                cr.outputline("exit(1);");
                 cr.endblock();
 
                 while (quantifiers.hasPrevious()) {
@@ -235,7 +237,7 @@ public class NaiveGenerator {
             
         }
 
-        output.println("if (__Success) { printf(\"all tests passed\"); }");
+        output.println("//if (__Success) { printf(\"all tests passed\"); }");
     }    
 
 }

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index b484055663067987c64ce53cd5a6cceb5b75cf3d..315c9fadfd1528337b09471905f7479438aa2503 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -16,6 +16,14 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public Set getInversedRelations() {
+        Set set = left.getInversedRelations();
+        if (right != null) {
+            set.addAll(right.getInversedRelations());
+        }
+        return set;
+    }
+
     public Set getRequiredDescriptors() {
         Set v = left.getRequiredDescriptors();
      

diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index 9f795e281c34971a6e6f765e73d5faba0bbff38c..5a541f5cba3bbcb5d22923ea70869c858d38f612 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -14,6 +14,22 @@ public class RelationExpr extends Expr {
         this.inverse = inverse;
     }
 
+    public Expr getExpr() {
+        return expr;
+    }
+    
+    public RelationDescriptor getRelation() {
+        return relation;
+    }
+
+    public Set getInversedRelations() {
+        Set set = expr.getInversedRelations();
+        if (inverse) {
+            set.add(relation);
+        }
+        return set;
+    }
+
     public Set getRequiredDescriptors() {
         Set v = expr.getRequiredDescriptors();        
         v.add(relation);

diff --git a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
index 840a43aba754c5b3c88f616b833d1d4c12bfce03..ab6a8d40540a0bda5c369063bd198e63aa72e5e0 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationInclusion.java
@@ -9,7 +9,7 @@ public class RelationInclusion extends Inclusion {
 
     // #TBD#: this flag needs to be set by some static analysis
     boolean typesafe = true;
-    static boolean worklist = true;
+    static boolean worklist = false;
 
     public RelationInclusion(Expr leftelementexpr, Expr rightelementexpr, RelationDescriptor relation) {
         this.leftelementexpr = leftelementexpr;
@@ -17,6 +17,18 @@ public class RelationInclusion extends Inclusion {
         this.relation = relation;
     }
 
+    public Expr getLeftExpr() {
+        return leftelementexpr;
+    }
+    
+    public Expr getRightExpr() {
+        return rightelementexpr;
+    }
+
+    public RelationDescriptor getRelation() {
+        return relation;
+    }
+
     public Set getTargetDescriptors() {
         HashSet v = new HashSet();
         v.add(relation);

diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java
index a482c08c7f99a372e6e1e0d30851399592d9eda3..69e8d0d45ec7da2fec4eb47080b4fafa0cacb826 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Rule.java
+++ b/Repair/RepairCompiler/MCC/IR/Rule.java
@@ -66,6 +66,19 @@ public class Rule {
         return st;
     }
 
+    public Set getQuantifierDescriptors() {
+
+        HashSet topdescriptors = new HashSet();
+
+        for (int i = 0; i < quantifiers.size(); i++) {            
+            Quantifier q = (Quantifier) quantifiers.elementAt(i);
+            topdescriptors.addAll(q.getRequiredDescriptors());                
+        }
+        
+        return SetDescriptor.expand(topdescriptors);
+    }
+
+
     public Set getRequiredDescriptors() {
 
         HashSet topdescriptors = new HashSet();

diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java
index 083ebaf341d40f03a90869c0f401fb9f738a7d43..b2a37cf1a41cefc20071012049c6e797de73b312 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java
@@ -14,6 +14,10 @@ public class SetExpr extends Expr {
         this.sd = null;
     }
 
+    public Set getInversedRelations() {
+        return new HashSet();
+    }
+
     public Set getRequiredDescriptors() {
         HashSet v = new HashSet();
         v.add(sd);

diff --git a/Repair/RepairCompiler/MCC/IR/SetInclusion.java b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
index 22ceb1d0a6e9333c306c474d35f0d92b3d5f7e78..a9450d623a70f504ec25e0ef36b6f91e82046e24 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SetInclusion.java
+++ b/Repair/RepairCompiler/MCC/IR/SetInclusion.java
@@ -7,13 +7,21 @@ public class SetInclusion extends Inclusion {
     Expr elementexpr;
     SetDescriptor set;
 
-    static boolean worklist = true;
+    public String generatedresult = null;
+    public String generatedaddeditem = null;
+
+    static boolean worklist = false;
+    public boolean dostore = true;
 
     public SetInclusion(Expr elementexpr, SetDescriptor set) {
         this.elementexpr = elementexpr;
         this.set = set;
     }
 
+    public SetDescriptor getSet() {
+        return set;
+    }
+
     public Set getTargetDescriptors() {
         HashSet v = new HashSet();
         v.add(set);
@@ -28,18 +36,29 @@ public class SetInclusion extends Inclusion {
         VarDescriptor vd = VarDescriptor.makeNew("element");
         elementexpr.generate(writer, vd);
 
+        // allows access to the value of this set addition later
+        generatedresult = vd.getSafeSymbol();
+
         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
-        writer.outputline("int " + addeditem + ";");
+        generatedaddeditem = addeditem; // allows access to the result of the set addition later.
+
+        // we set equal to one so that if dostore == false the guard in teh 
+        // metainclusion generation for the subrules and sub quantifiers will go on        
+        writer.outputline("int " + addeditem + " = 1;");
+
+        if (dostore) {
         
-        writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
-                          +  ", (int)" + vd.getSafeSymbol() + ");");
+            writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
+                              +  ", (int)" + vd.getSafeSymbol() + ");");
 
-        if (SetInclusion.worklist) {
-            writer.outputline("if (" + addeditem + ")");
-            writer.startblock(); {                
-                WorkList.generate_dispatch(writer, set, vd.getSafeSymbol());
+            if (SetInclusion.worklist) {
+                writer.outputline("if (" + addeditem + ")");
+                writer.startblock(); {                
+                    WorkList.generate_dispatch(writer, set, vd.getSafeSymbol());
+                }
+                writer.endblock();
             }
-            writer.endblock();
+
         }
         
     }

diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
index 506db005e77079c2c3736026bbd7254c6034dac0..09d37e40aec7faec46d74b40f4081a2613795e39 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
@@ -14,6 +14,10 @@ public class SizeofExpr extends Expr {
         this.setexpr = setexpr;
     }
 
+    public SetExpr getSetExpr() {
+        return setexpr;
+    }
+
     public Set getRequiredDescriptors() {
         return setexpr.getRequiredDescriptors();
     }
@@ -33,5 +37,8 @@ public class SizeofExpr extends Expr {
         return this.td;        
     }
 
+    public Set getInversedRelations() {
+        return setexpr.getInversedRelations();
+    }
         
 }

diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index e62335ed3aa1bbd2c1eab8ea5b075d6fa757cde6..a697a5fa9a0eb5ba885db9f71ac83eebc3c19063 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -12,9 +12,17 @@ public class VarExpr extends Expr {
         this.varname = varname; 
     }
 
+    public Set getInversedRelations() {
+        return new HashSet();
+    }
+
     public Set getRequiredDescriptors() {
         return new HashSet();
     }
+    
+    public VarDescriptor getVar() {
+        return vd;
+    }
 
     public void generate(CodeWriter writer, VarDescriptor dest) {        
 

diff --git a/Repair/RepairCompiler/MCC/Makefile b/Repair/RepairCompiler/MCC/Makefile
index bf746074be2ad9055a1de41960e338c9cf9c034c..b1d5648285f7d9c239557cd376f715d9ea043ff0 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Makefile
+++ b/Repair/RepairCompiler/MCC/Makefile
@@ -35,7 +35,9 @@ IR/RelationQuantifier.class IR/ForQuantifier.class IR/GraphNode.class \
 IR/DependencyBuilder.class IR/RelationInclusion.class IR/SetInclusion.class \
 IR/TupleOfExpr.class IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class \
 IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class \
-IR/StandardCodeWriter.class
+IR/StandardCodeWriter.class IR/WorklistGenerator.class IR/WorkList.class \
+IR/Optimizer.class IR/MetaInclusion.class IR/SizeofFunction.class \
+IR/RelationFunctionExpr.class
 
 #MODEL_CLASS = Field.class Literal.class Quantifier.class              \
 #Set.class TypeElement.class                                           \