From 7b490abd701dbb555dea07567a8daeaf3d36df9d Mon Sep 17 00:00:00 2001
From: droy <droy>
Date: Sat, 20 Sep 2003 20:49:15 +0000
Subject: [PATCH] optimized works

---
 Repair/RepairCompiler/MCC/Compiler.java       |  6 +++
 Repair/RepairCompiler/MCC/IR/CodeWriter.java  |  2 +
 Repair/RepairCompiler/MCC/IR/Constraint.java  |  7 ++++
 Repair/RepairCompiler/MCC/IR/DotExpr.java     |  4 ++
 Repair/RepairCompiler/MCC/IR/Expr.java        |  4 ++
 .../RepairCompiler/MCC/IR/ImageSetExpr.java   | 23 +++++++++++-
 .../MCC/IR/InclusionPredicate.java            |  9 +++++
 Repair/RepairCompiler/MCC/IR/LiteralExpr.java |  4 ++
 .../RepairCompiler/MCC/IR/LogicStatement.java | 12 ++++++
 .../RepairCompiler/MCC/IR/NaiveGenerator.java | 26 +++++++------
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  8 ++++
 .../RepairCompiler/MCC/IR/RelationExpr.java   | 16 ++++++++
 .../MCC/IR/RelationInclusion.java             | 14 ++++++-
 Repair/RepairCompiler/MCC/IR/Rule.java        | 13 +++++++
 Repair/RepairCompiler/MCC/IR/SetExpr.java     |  4 ++
 .../RepairCompiler/MCC/IR/SetInclusion.java   | 37 ++++++++++++++-----
 Repair/RepairCompiler/MCC/IR/SizeofExpr.java  |  7 ++++
 Repair/RepairCompiler/MCC/IR/VarExpr.java     |  8 ++++
 Repair/RepairCompiler/MCC/Makefile            |  4 +-
 19 files changed, 184 insertions(+), 24 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 7ea9362..bca936c 100755
--- 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 f2fcd2c..59763b0 100755
--- 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 61f9b90..852313a 100755
--- 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 b5d0243..5336065 100755
--- 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 b5481c3..1e7fd14 100755
--- 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 52adc76..c7f5079 100755
--- 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 cbe7037..fd4d8ff 100755
--- 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 df14ed1..b9d09e1 100755
--- 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 43fb985..9c3a1ed 100755
--- 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 dd46011..08ed84d 100755
--- 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 b484055..315c9fa 100755
--- 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 9f795e2..5a541f5 100755
--- 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 840a43a..ab6a8d4 100755
--- 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 a482c08..69e8d0d 100755
--- 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 083ebaf..b2a37cf 100755
--- 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 22ceb1d..a9450d6 100755
--- 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 506db00..09d37e4 100755
--- 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 e62335e..a697a5f 100755
--- 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 bf74607..b1d5648 100755
--- 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						\
-- 
2.34.1