From: bdemsky Date: Tue, 11 May 2004 21:14:26 +0000 (+0000) Subject: Code to improve search by pruning certain types of repair.. X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=860ccbdf9cd6f96c6bba58641372b6776987a080 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 a8b2bce..11f479a 100755 --- 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 (6.035-staff@mit.edu) - * @version $Id: CLI.java,v 1.4 2004/05/10 21:54:40 bdemsky Exp $ + * @version $Id: CLI.java,v 1.5 2004/05/11 21:14:24 bdemsky Exp $ */ 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 df09791..9ecf6a6 100755 --- 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 b0a49a3..adc8721 100755 --- 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 6b6a715..a44f431 100755 --- 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 4fda86c..c99715d 100755 --- 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 c3d2c5d..c35feaf 100755 --- 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 337c569..bd46b6b 100755 --- 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 4698b51..7727567 100755 --- 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