Started adding analysis for modifyrelation nodes.

Added check flag.

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index 96690778369cd69fb9216e4a1b9996f5f165005f..609455ac2bd4484b332908f3313035b0643a2c1a 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.1 2003/07/07 16:13:33 droy Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.2 2004/04/15 05:41:46 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -180,6 +180,8 @@ public class CLI {
            } else if (args[i].equals("-native")) {
                 context = 0;
                 fNative = true;
+           } else if (args[i].equals("-checkonly")) {
+                Compiler.REPAIR=false;
             } else if (args[i].equals("-vis")) {
                 context = 4;
                 fVis = true;

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 0395872829aaed67cb77ea53643fbdc6b86e716b..cc1f0de61a8a18e37997339710e098ac879ab23c 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -18,7 +18,7 @@ import MCC.IR.*;
 
 public class Compiler {
     /* Set this flag to false to turn repairs off */
-    public static boolean REPAIR=false;
+    public static boolean REPAIR=true;
     
     public static void main(String[] args) {
         State state = null;

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 96a86458a6a5656259894f5d32228b73063d670d..37abc39f3650f71fbe2df6f90b23aef6bf93f58a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -17,8 +17,23 @@ public class GraphAnalysis {
     public Set doAnalysis() {
        HashSet cantremove=new HashSet();
        HashSet mustremove=new HashSet();
+       HashSet optionalabstractrepair=new HashSet();
+
+       for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode)it.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           AbstractRepair ar=tn.getAbstract();
+           DNFPredicate dpred=ar.getPredicate();
+           Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
+           if ((repairnodes.size()>1)&&
+               containsmodify(repairnodes)) {
+               optionalabstractrepair.add(gn);
+           }
+       }
+
        cantremove.addAll(termination.scopenodes);
        cantremove.addAll(termination.abstractrepair);
+       cantremove.removeAll(optionalabstractrepair);
 
        while(true) {
            boolean change=false;
@@ -28,9 +43,10 @@ public class GraphAnalysis {
            GraphNode.computeclosure(nodes,mustremove);
            Set cycles=GraphNode.findcycles(nodes);
            Set couldremove=new HashSet();
-           couldremove.addAll(termination.conjunctions);
+           couldremove.addAll(termination.conjunctions);
            couldremove.addAll(termination.updatenodes);
            couldremove.addAll(termination.consequencenodes);
+           couldremove.addAll(optionalabstractrepair);
            couldremove.retainAll(cycles);
 
 
@@ -50,6 +66,10 @@ public class GraphAnalysis {
                        change=true;
                }
            }
+
+           /* Search through conjunction which must be satisfied, and attempt
+              to generate appropriate repair actions
+            */
            HashSet newset=new HashSet();
            for(Iterator cit=cantremove.iterator();cit.hasNext();) {
                GraphNode gn=(GraphNode)cit.next();
@@ -60,12 +80,9 @@ public class GraphAnalysis {
                        GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
                        GraphNode gn2=e.getTarget();
                        TermNode tn2=(TermNode)gn2.getOwner();
-                       if (tn2.getType()==TermNode.ABSTRACT) {
-                           AbstractRepair ar=tn2.getAbstract();
-                           if (ar.getType()==AbstractRepair.MODIFYRELATION) {
-                               nomodify=false;
-                               break;
-                           }
+                       if (nodes.contains(gn2)&&!mustremove.contains(gn2)&&
+                           tn2.getType()==TermNode.ABSTRACT) {
+
                            HashSet updateset=new HashSet();
                            for(Iterator upit=gn2.edges();upit.hasNext();) {
                                GraphNode.Edge e2=(GraphNode.Edge)upit.next();
@@ -75,13 +92,52 @@ public class GraphAnalysis {
                                    updateset.add(gn3);
                            }
                            updateset.removeAll(mustremove);
-                           if (updateset.size()==1)
+
+                           AbstractRepair ar=tn2.getAbstract();
+                           DNFPredicate dpred=ar.getPredicate();
+                           Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
+                           if (repairnodes.size()>1&&
+                               containsmodify(repairnodes)) {
+                               /* We are modifying a relation */
+                               HashSet retainednodes=new HashSet();
+                               retainednodes.addAll(repairnodes);
+                               retainednodes.retainAll(nodes);
+
+                               if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+                                   if (updateset.size()==0) {
+                                       if (retainednodes.size()>1) {
+                                           mustremove.add(gn);
+                                           change=true;
+                                       } else return null; /* Out of luck */
+                                   }
+                                   if (updateset.size()==1&&retainednodes.size()==1)
+                                       toremove.addAll(updateset); /* Required update */
+                               } else {
+                                   /* Addition or removal to relation */
+                                   assert (ar.getType()==AbstractRepair.ADDTORELATION)||(ar.getType()==AbstractRepair.REMOVEFROMRELATION);
+                                   if (updateset.size()==0) {
+                                       if (containsmodify(retainednodes)) {
+                                           /* Both ADD & REMOVE are no good */
+                                           for(Iterator it=retainednodes.iterator();it.hasNext();) {
+                                               GraphNode gnit=(GraphNode)it.next();
+                                               TermNode tnit=(TermNode)gnit.getOwner();
+                                               AbstractRepair arit=tnit.getAbstract();
+                                               if (arit.getType()!=AbstractRepair.MODIFYRELATION) {
+                                                   mustremove.add(gnit);
+                                                   change=true;
+                                               }
+                                           }
+                                       } else
+                                           return null; /* Out of luck */
+                                   }
+                                   if (updateset.size()==1&&retainednodes.size()==2)
+                                       toremove.addAll(updateset); /* Required update */
+                               }
+                           } else if (updateset.size()==1)
                                toremove.addAll(updateset);
                        }
                    }
-                   if (nomodify) {
-                       newset.addAll(toremove);
-                   }
+                   newset.addAll(toremove);
                }
            }
            {
@@ -182,6 +238,7 @@ public class GraphAnalysis {
                if (illegal(combination,couldremovevector))
                    break;
                Set combinationset=buildset(combination,couldremovevector);
+               checkmodify(combinationset);
                combinationset.addAll(mustremove);
                if (combinationset!=null) {
                    System.out.println("Checkabstract="+checkAbstract(combinationset));
@@ -200,6 +257,44 @@ public class GraphAnalysis {
        }
     }
 
+    private void checkmodify(Set removednodes) {
+       for (Iterator it=removednodes.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode)it.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           if (tn.getType()==TermNode.ABSTRACT) {
+               AbstractRepair ar=tn.getAbstract();
+               DNFPredicate dpred=ar.getPredicate();
+               Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
+               /* Has MODIFYRELATION */
+               if (containsmodify(repairnodes)&&
+                   (repairnodes.size()>1)&&
+                   (ar.getType()==AbstractRepair.REMOVEFROMRELATION||
+                    ar.getType()==AbstractRepair.ADDTORELATION)) {
+                   for(Iterator it2=repairnodes.iterator();it2.hasNext();) {
+                       GraphNode gn2=(GraphNode)it2.next();
+                       TermNode tn2=(TermNode)gn2.getOwner();
+                       AbstractRepair ar2=tn2.getAbstract();
+                       if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION||
+                           ar2.getType()==AbstractRepair.ADDTORELATION) {
+                           removednodes.add(gn2);
+                       }
+                   }
+               }
+           }
+       }
+    }
+
+    private static boolean containsmodify(Set repairnodes) {
+       for (Iterator it=repairnodes.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode) it.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           AbstractRepair ar=tn.getAbstract();
+           if (ar.getType()==AbstractRepair.MODIFYRELATION)
+               return true;
+       }
+       return false;
+    }
+
     private static Set buildset(Vector combination, Vector couldremove) {
        Set s=new HashSet();
        for(int i=0;i<combination.size();i++) {
@@ -342,6 +437,27 @@ public class GraphAnalysis {
                GraphNode gn=(GraphNode)it.next();
                if (!removed.contains(gn)) {
                    foundrepair=true;
+                   for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                       GraphNode.Edge edge=(GraphNode.Edge) edgeit.next();
+                       GraphNode gn2=edge.getTarget();
+                       TermNode tn2=(TermNode) gn2.getOwner();
+                       if (tn2.getType()==TermNode.ABSTRACT) {
+                           /* Abstract node */
+                           AbstractRepair ar=tn2.getAbstract();
+                           DNFPredicate dpred=ar.getPredicate();
+                           Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
+                           if (containsmodify(repairnodes)&&
+                               (repairnodes.size()>1)) {
+                               HashSet retainednodes=new HashSet();
+                               retainednodes.addAll(repairnodes);
+                               retainednodes.removeAll(removed);
+                               if (!containsmodify(retainednodes)&&
+                                   (retainednodes.size()<2))
+                                   return ERR_NOREPAIR;
+                           } else if (removed.contains(gn2))
+                               return ERR_NOREPAIR;
+                       }
+                   }
                }
            }
            if (!foundrepair)

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 1419a6856587d768d07a4674fb258ad901bdbe2c..53f424c85c9cdf295f64cb2175556052b3a280b0 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -646,9 +646,9 @@ public class RepairGenerator {
                 ListIterator quantifiers = constraint.quantifiers();
 
                 while (quantifiers.hasNext()) {
-                    Quantifier quantifier = (Quantifier) quantifiers.next();                   
+                    Quantifier quantifier = (Quantifier) quantifiers.next();
                     quantifier.generate_open(cr);
-                }            
+                }
 
                 cr.outputline("int maybe = 0;");
                         

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 8aa0370964d51c712852ef95bbb73ea657fca7d7..2dccba3de978c8fce64bba9c4ed774d08bda1169 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -19,6 +19,7 @@ public class Termination {
     Hashtable abstractadd;
     Hashtable abstractremove;
     Hashtable conjtonodemap;
+    Hashtable predtoabstractmap;
     Set removedset;
 
     State state;
@@ -37,6 +38,7 @@ public class Termination {
        abstractadd=new Hashtable();
        abstractremove=new Hashtable();
        conjtonodemap=new Hashtable();
+       predtoabstractmap=new Hashtable();
        if (!Compiler.REPAIR)
            return;
 
@@ -267,6 +269,9 @@ public class Termination {
                    GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
                    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
+                   if (!predtoabstractmap.containsKey(dp))
+                       predtoabstractmap.put(dp,new HashSet());
+                   ((Set)predtoabstractmap.get(dp)).add(gn2);
                    abstractrepair.add(gn2);
                }
            }
@@ -284,6 +289,9 @@ public class Termination {
            AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
            TermNode tn=new TermNode(ar);
            GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+           if (!predtoabstractmap.containsKey(tp))
+               predtoabstractmap.put(tp,new HashSet());
+           ((Set)predtoabstractmap.get(tp)).add(gn);
            abstractrepair.add(gn);
            abstractadd.put(sd,gn);
            
@@ -291,6 +299,9 @@ public class Termination {
            AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
            TermNode tn2=new TermNode(ar2);
            GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+           if (!predtoabstractmap.containsKey(tp2))
+               predtoabstractmap.put(tp2,new HashSet());
+           ((Set)predtoabstractmap.get(tp2)).add(gn2);
            abstractrepair.add(gn2);
            abstractremove.put(sd,gn2);
        }
@@ -309,6 +320,9 @@ public class Termination {
            AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
            TermNode tn=new TermNode(ar);
            GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+           if (!predtoabstractmap.containsKey(tp))
+               predtoabstractmap.put(tp,new HashSet());
+           ((Set)predtoabstractmap.get(tp)).add(gn);
            abstractrepair.add(gn);
            abstractadd.put(rd,gn);
            
@@ -316,6 +330,9 @@ public class Termination {
            AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
            TermNode tn2=new TermNode(ar2);
            GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+           if (!predtoabstractmap.containsKey(tp2))
+               predtoabstractmap.put(tp2,new HashSet());
+           ((Set)predtoabstractmap.get(tp2)).add(gn2);
            abstractrepair.add(gn2);
            abstractremove.put(rd,gn2);
        }