Code to improve search by pruning certain types of repair..

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index a8b2bce0e245eb0b243593eb945052ab87d476f4..11f479a8a47382afd1346d35d0a4af1e69164a64 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.4 2004/05/10 21:54:40 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.5 2004/05/11 21:14:24 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -106,6 +106,8 @@ public class CLI {
                 Compiler.REPAIR=false;
            } else if (args[i].equals("-aggressivesearch")) {
                 Compiler.AGGRESSIVESEARCH=true;
+           } else if (args[i].equals("-prunequantifiernodes")) {
+                Compiler.PRUNEQUANTIFIERS=true;
             } else if (args[i].equals("-verbose") || args[i].equals("-v")) {
                 context = 0;
                 verbose++;

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index df0979133640e4a735dc3b5342cbc21fbd902291..9ecf6a653a6e40209b1e04f5cc0ed30b898fbe6a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -20,6 +20,7 @@ public class Compiler {
     /* Set this flag to false to turn repairs off */
     public static boolean REPAIR=true;
     public static boolean AGGRESSIVESEARCH=false;
+    public static boolean PRUNEQUANTIFIERS=false;
 
     public static void main(String[] args) {
         State state = null;

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index b0a49a3e8953dce5d42a1ccc7589da81b13995fb..adc872120c5e865d2d8bcf36c71c512863bb19df 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -9,7 +9,7 @@ public class DotExpr extends Expr {
     String field;
     Expr index;
     
-    static boolean DOMEMCHECKS=true;
+    static boolean DOMEMCHECKS=false;
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;
 

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 6b6a7153c9a79ad12019b4ddcd1df321806febde..a44f431ff60c72d5c186440a92ec715e4381e98e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -134,8 +134,21 @@ public class GraphAnalysis {
                    if (!foundupdate)
                        allgood=false;
                }
-               if (allgood)
+               if (allgood) {
                    couldremove.remove(gn);
+                   if (Compiler.PRUNEQUANTIFIERS) {
+                       TermNode tn=(TermNode)gn.getOwner();
+                       Constraint constr=tn.getConstraint();
+                       for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
+                           GraphNode gn4=(GraphNode)consit.next();
+                           TermNode tn4=(TermNode)gn4.getOwner();
+                           if (tn4.getquantifiernode()) {
+                               mustremove.add(gn4); /* This node is history */
+                               System.out.println("Eliminating: "+gn4.getTextLabel());
+                           }
+                       }
+                   }
+               }
            }
 
 

diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index 4fda86c2b3ce6647b07cfbce24c463f06feee6a3..c99715d335a716f1dee7e0cf32621dc35f2433e2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -10,9 +10,17 @@ public class InclusionPredicate extends Predicate {
     public TypeDescriptor typecheck(SemanticAnalyzer sa) {
        TypeDescriptor t=expr.typecheck(sa);
        TypeDescriptor ts=setexpr.typecheck(sa);
-       if (t!=ts)
+       if (t instanceof StructureTypeDescriptor) {
+           while(((StructureTypeDescriptor)t).getSuperType()!=null)
+               t=((StructureTypeDescriptor)t).getSuperType();
+       }
+       if (ts instanceof StructureTypeDescriptor) {
+           while(((StructureTypeDescriptor)ts).getSuperType()!=null)
+               ts=((StructureTypeDescriptor)ts).getSuperType();
+       }
+       if (t!=ts) {
            return null;
-       
+       }
        return ReservedTypeDescriptor.INT;
     }
 

diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index c3d2c5dd081a50cafee8c003dcd88a29062736af..c35feaf168cd07e13dc7ea3de39ef14469a4f307 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -404,6 +404,7 @@ public class SemanticChecker {
             TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
 
             if (constype == null) {
+               System.out.println("Failed attempting to type constraint");
                 ok = false;
             } else if (constype != ReservedTypeDescriptor.INT) {
                 er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
@@ -439,6 +440,7 @@ public class SemanticChecker {
                 assert qn.getLabel().equals("quantifier");
                 Quantifier quantifier = parse_quantifier(qn);
                 if (quantifier == null) {
+                   System.out.println("Failed parsing quantifier");
                     ok = false;
                 } else {
                     constraint.addQuantifier(quantifier);
@@ -450,6 +452,7 @@ public class SemanticChecker {
         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 
         if (logicexpr == null) {
+           System.out.println("Failed parsing logical expression");
             ok = false;
         } else {
             constraint.setLogicStatement(logicexpr);

diff --git a/Repair/RepairCompiler/MCC/IR/TermNode.java b/Repair/RepairCompiler/MCC/IR/TermNode.java
index 337c5697d963bf2f93f6143df67653143bd96709..bd46b6bec1f04fb2581b916de213ce675bf92727 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/TermNode.java
+++ b/Repair/RepairCompiler/MCC/IR/TermNode.java
@@ -14,6 +14,16 @@ class TermNode {
     AbstractRepair repair;
     ScopeNode scope;
     MultUpdateNode update;
+    boolean quantifiernode=false;
+
+    public void setquantifiernode() {
+       quantifiernode=true;
+    }
+    
+    public boolean getquantifiernode() {
+       return quantifiernode;
+    }
+
 
     public int getType() {
        return type;

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 4698b51702b1b0f119a98f7130f0e482c8843c71..772756717c6de06a60066396f317efa2461bfc34 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -143,8 +143,6 @@ public class Termination {
                    conjunctionmap.put(c,new HashSet());
                ((Set)conjunctionmap.get(c)).add(gn);
                conjtonodemap.put(dnf.get(j),gn);
-
-
            }
            // Construct quantifier "conjunction" nodes
            for(int j=0;j<c.numQuantifiers();j++) {
@@ -156,6 +154,7 @@ public class Termination {
                    DNFConstraint dconst=new DNFConstraint(ip);
                    dconst=dconst.not();
                    TermNode tn=new TermNode(c,dconst.get(0));
+                   tn.setquantifiernode();
                    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
                                               "Conj ("+i+","+j+") "+dconst.get(0).name()
                                               ,tn);
@@ -172,6 +171,7 @@ public class Termination {
                    DNFConstraint dconst=new DNFConstraint(ip);
                    dconst=dconst.not();
                    TermNode tn=new TermNode(c,dconst.get(0));
+                   tn.setquantifiernode();
                    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
                                               "Conj ("+i+","+j+") "+dconst.get(0).name()
                                               ,tn);

diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index 2e5973331f07341f76380e7c4f9530bbb2acb757..db9e44324bb1a23c81a680bd503bd62953d2f858 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -3,7 +3,7 @@ package MCC.IR;
 import java.util.*;
 
 public class VarExpr extends Expr {
-    static boolean DOMEMCHECKS=true;
+    static boolean DOMEMCHECKS=false;
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;