Some embarrassing erros. The DNF conversion for negation wasn't

working quite right.  Printing negation a little more clearly.  Fixed
a problem with the termination analysis (it was too conservative).

diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 018df2fea7061c249748b6aaa86659cd8695ec05..55770f51614a349dcd7617fd2fe3712d1cbbe588 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -9,6 +9,11 @@ public class DNFConstraint {
        conjunctions.add(new Conjunction(new DNFPredicate(false,p)));
     }
 
+    public DNFConstraint(DNFPredicate dp) {
+       conjunctions=new Vector();
+       conjunctions.add(new Conjunction(dp));
+    }
+
     public DNFConstraint(Conjunction conj) {
        conjunctions=new Vector();
        conjunctions.add(conj);
@@ -17,7 +22,7 @@ public class DNFConstraint {
     public DNFConstraint(Vector conj) {
        conjunctions=conj;
     }
-    
+
     DNFConstraint() {
        conjunctions=new Vector();
     }
@@ -62,15 +67,23 @@ public class DNFConstraint {
 
     public DNFConstraint not() {
        DNFConstraint copy=copy();
+        DNFConstraint notconst=null;
        for (int i=0;i<size();i++) {
            Conjunction conj=copy.get(i);
+            DNFConstraint newconst=null;
            for (int j=0;j<conj.size();j++) {
                DNFPredicate dp=conj.get(j);
                dp.negatePred();
+                if (newconst==null)
+                   newconst=new DNFConstraint(dp);
+                else
+                   newconst=newconst.or(new DNFConstraint(dp));
            }
+            if (notconst==null)
+               notconst=newconst;
+            else
+               notconst=notconst.and(newconst);
        }
-       return copy;
+       return notconst;
    }
 }
-
-

diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
index 345a588e788378d77577b9e2158fd9754398312f..26fb1f8321bd7769d2bdbe78834377e5cf4e18c1 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFRule.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -9,6 +9,11 @@ public class DNFRule {
        ruleconjunctions.add(new RuleConjunction(new DNFExpr(false,e)));
     }
 
+    public DNFRule(DNFExpr de) {
+       ruleconjunctions=new Vector();
+       ruleconjunctions.add(new RuleConjunction(de));
+    }
+
     public DNFRule(RuleConjunction conj) {
        ruleconjunctions=new Vector();
        ruleconjunctions.add(conj);
@@ -17,7 +22,7 @@ public class DNFRule {
     public DNFRule(Vector conj) {
        ruleconjunctions=conj;
     }
-    
+
     DNFRule() {
        ruleconjunctions=new Vector();
     }
@@ -62,15 +67,23 @@ public class DNFRule {
 
     public DNFRule not() {
        DNFRule copy=copy();
+        DNFRule notrule=null;
        for (int i=0;i<size();i++) {
            RuleConjunction conj=copy.get(i);
+            DNFRule newrule=null;
            for (int j=0;j<conj.size();j++) {
                DNFExpr dp=conj.get(j);
                dp.negatePred();
+                if (newrule==null)
+                   newrule=new DNFRule(dp);
+                else
+                   newrule=newrule.or(new DNFRule(dp));
            }
+            if (notrule==null)
+               notrule=newrule;
+            else
+               notrule=notrule.and(newrule);
        }
-       return copy;
+       return notrule;
    }
 }
-
-

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 16a51f781861c0a263d3f88e263f629778309427..0d516d3d12d79fb41f0ded1bfe1a605f556ecb6e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -35,7 +35,7 @@ public class GraphAnalysis {
                         &&termination.conjunctions.contains(gn2))||
                        cantremovetrans.contains(gn2))
                        cantremovetrans.add(gn3);
-                   
+
                    if (termination.abstractrepair.contains(gn3)||
                        termination.conjunctions.contains(gn3)||
                        termination.updatenodes.contains(gn3)) {
@@ -55,7 +55,7 @@ public class GraphAnalysis {
                if (!goodoption) {
                    if (termination.scopenodes.contains(gn2))
                        return false;
-               }                   
+               }
            }
        }
        if (needcyclecheck) {
@@ -116,6 +116,8 @@ public class GraphAnalysis {
                GraphNode gn=(GraphNode) it.next();
                if (mustremove.contains(gn)||cantremove.contains(gn))
                    continue;
+               if (!safetransclosure(gn, mustremove,cantremove, cantremove))
+                    continue;
 
                boolean allgood=true;
                for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
@@ -124,7 +126,7 @@ public class GraphAnalysis {
                    assert tn2.getType()==TermNode.ABSTRACT;
                    boolean foundupdate=false;
                    for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
-                       GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();                 
+                       GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
                        if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
                            TermNode tn3=(TermNode)gn3.getOwner();
                            if (tn3.getType()==TermNode.UPDATE)
@@ -153,7 +155,7 @@ public class GraphAnalysis {
 
 
            /* Look for constraints which can only be satisfied one way */
-           
+
            Vector constraints=termination.state.vConstraints;
            for(int i=0;i<constraints.size();i++) {
                Constraint c=(Constraint)constraints.get(i);
@@ -226,7 +228,7 @@ public class GraphAnalysis {
                        change=true;
                }
            }
-           
+
            if (Compiler.AGGRESSIVESEARCH) {
                /* Aggressively remove compensation nodes */
                for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
@@ -321,7 +323,7 @@ public class GraphAnalysis {
                    AbstractRepair ar=tn2.getAbstract();
                    boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
                    int numadd=0;int numremove=0;
-                   
+
                    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                        GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
                        GraphNode gn3=e2.getTarget();
@@ -392,11 +394,11 @@ public class GraphAnalysis {
                        GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
                        GraphNode gn2=e.getTarget();
                        TermNode tn2=(TermNode)gn2.getOwner();
-                       
+
                        if ((tn2.getType()==TermNode.CONSEQUENCE)&&
                            !mustremove.contains(gn2))
                            count++;
-                           
+
 
                        if (tn2.getType()!=TermNode.UPDATE)
                            continue;
@@ -405,7 +407,7 @@ public class GraphAnalysis {
                        boolean containsgn2=cantremove.contains(gn2);
                        cantremove.add(gn);
                        cantremove.add(gn2);
-                       
+
                        Set cycle=GraphNode.findcycles(cantremove);
                        if (cycle.contains(gn2)) {
                            if (!mustremove.contains(gn2)) {
@@ -421,7 +423,7 @@ public class GraphAnalysis {
                        if (!containsgn2)
                            cantremove.remove(gn2);
                    }
-               
+
                    if (count==1) {
                        for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
                            GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
@@ -440,7 +442,7 @@ public class GraphAnalysis {
            }
            couldremove.removeAll(mustremove);
            couldremove.removeAll(cantremove);
-           
+
            Vector couldremovevector=new Vector();
            couldremovevector.addAll(couldremove);
            Vector combination=new Vector();
@@ -460,7 +462,7 @@ public class GraphAnalysis {
                e.printStackTrace();
                System.exit(-1);
            }
-           
+
            System.out.println("Searching set of "+couldremove.size()+" nodes.");
            System.out.println("Eliminated must "+mustremove.size()+" nodes");
            System.out.println("Eliminated cant "+cantremove.size()+" nodes");
@@ -479,22 +481,31 @@ public class GraphAnalysis {
                GraphNode gn=(GraphNode)it.next();
                System.out.println(gn.getTextLabel());
            }
-           
-           
+
+           System.out.println("==================================================");
            while(true) {
                if (illegal(combination,couldremovevector))
                    break;
                Set combinationset=buildset(combination,couldremovevector);
+                System.out.println("---------------------------");
+                for(Iterator it=combinationset.iterator();it.hasNext();) {
+                    System.out.println(((GraphNode)it.next()).getTextLabel());
+                }
+                System.out.println("---------------------------");
                checkmodify(combinationset);
                combinationset.addAll(mustremove);
                if (combinationset!=null) {
-                   System.out.println("Checkabstract="+checkAbstract(combinationset));
-                   System.out.println("Checkrepairs="+checkRepairs(combinationset));
-                   System.out.println("Checkall="+checkAll(combinationset));
-                   
-                   if (checkAbstract(combinationset)==0&&
-                       checkRepairs(combinationset)==0&&
-                       checkAll(combinationset)==0) {
+                    int checkabstract=checkAbstract(combinationset);
+                    int checkrep=checkRepairs(combinationset);
+                    int checkall=checkAll(combinationset);
+
+                   System.out.println("Checkabstract="+checkabstract);
+                   System.out.println("Checkrepairs="+checkrep);
+                   System.out.println("Checkall="+checkall);
+
+                   if (checkabstract==0&&
+                       checkrep==0&&
+                       checkall==0) {
                        return combinationset;
                    }
                }
@@ -522,7 +533,7 @@ public class GraphAnalysis {
                    if (!removednodes.contains(gn2)&&
                        tn2.getType()==TermNode.UPDATE) {
                        MultUpdateNode mun=tn2.getUpdate();
-                       
+
                        if (mun.getType()==MultUpdateNode.ADD)
                            numadd++;
                        if (mun.getType()==MultUpdateNode.REMOVE)
@@ -709,7 +720,7 @@ public class GraphAnalysis {
        tset.addAll(termination.consequencenodes);
        abstractnodes.retainAll(tset);
        Set cycles=GraphNode.findcycles(abstractnodes);
-       
+
        for(Iterator it=cycles.iterator();it.hasNext();) {
            GraphNode gn=(GraphNode)it.next();
            System.out.println("NODE: "+gn.getTextLabel());

diff --git a/Repair/RepairCompiler/MCC/IR/LogicStatement.java b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
index b750ffd83fe3fd53f85e5b1d84b07292dbc76f13..05691379d7c6c28b03b4ac2fe2378db145272de9 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/LogicStatement.java
+++ b/Repair/RepairCompiler/MCC/IR/LogicStatement.java
@@ -10,7 +10,7 @@ public class LogicStatement {
 
     public String name() {
        if (op==NOT)
-           return "!"+left.name();
+           return "!("+left.name()+")";
        String name=left.name();
        name+=" "+op.toString()+" ";
        if (right!=null)

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index c5f6b270e7b1dd86074e2efee592a7060c876af2..e9cde37d174b730ca782e0f1a07cc603ac505afc 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -191,8 +191,10 @@ public class OpExpr extends Expr {
        if (opcode==Opcode.RND)
            return "Round("+left.name()+")";
        String name=left.name()+opcode.toString();
-       if (right!=null)
+       if (right!=null) {
            name+=right.name();
+            name="("+name+")";
+        }
        return name;
     }
 
@@ -411,8 +413,9 @@ public class OpExpr extends Expr {
     public void prettyPrint(PrettyPrinter pp) {
         pp.output("(");
         if (opcode == Opcode.NOT) {
-           pp.output("!");
+           pp.output("!(");
             left.prettyPrint(pp);
+           pp.output(")");
        } else if (opcode == Opcode.NOP) {
             left.prettyPrint(pp);
        } else if (opcode == Opcode.RND) {

diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
index b7f34799f0f6de097fc0cb353cd49b859215a10c..108a88379b46e48f20e31bdcb3351b849073004a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
+++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java
@@ -381,6 +381,7 @@ public class SemanticChecker {
         if (!precheck(pn, "constraints")) {
             return false;
         }
+        //System.out.println(pn.PPrint(2,true));
 
         boolean ok = true;
         ParseNodeVector constraints = pn.getChildren();
@@ -594,7 +595,6 @@ public class SemanticChecker {
         } else if (pn.getChild("not") != null) {
             /* NOT body */
             LogicStatement left = parse_body(pn.getChild("not").getChild("body"));
-
             if (left == null) {
                 return null;
             }