Additional enhancements to compute mustremove and cantremove sets for

node elimination.

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index c472ffa185e4e015e5e47a7930866d46fc353100..44e085d77d9134f4fde113df0591c554a8cfe4eb 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -11,6 +11,10 @@ public class CastExpr extends Expr {
        return expr.freeVars();
     }
 
+    public Expr getExpr() {
+       return expr;
+    }
+
     public void findmatch(Descriptor d, Set s) {
        expr.findmatch(d,s);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index eefde7f2f733ad659d9665426cf6625899178330..8cb19f8e321761ebabc932a9c5e4c58cea6153e9 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -319,7 +319,14 @@ class ConcreteInterferes {
                    leftdescriptor=((VarExpr)lexpr2).getVar();
                else if (lexpr2 instanceof DotExpr) {
                    Expr e=lexpr2;
-                   for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+                   do {
+                       for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+                       if (e instanceof VarExpr)
+                           break;
+                       if (e instanceof CastExpr)
+                           e=((CastExpr)e).getExpr();
+                       else throw new Error("Bad Expr Type:"+e.name());
+                   } while (true);
                    leftdescriptor=((VarExpr)e).getVar();
                } else throw new Error("Bad Expr");
                

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 37abc39f3650f71fbe2df6f90b23aef6bf93f58a..7f44c18876a139d11304c7c500a4f8c93baf0cb1 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -1,5 +1,6 @@
 package MCC.IR;
 import java.util.*;
+import java.io.*;
 import MCC.State;
 
 public class GraphAnalysis {
@@ -49,7 +50,6 @@ public class GraphAnalysis {
            couldremove.addAll(optionalabstractrepair);
            couldremove.retainAll(cycles);
 
-
            /* Look for constraints which can only be satisfied one way */
            
            Vector constraints=termination.state.vConstraints;
@@ -68,7 +68,7 @@ public class GraphAnalysis {
            }
 
            /* Search through conjunction which must be satisfied, and attempt
-              to generate appropriate repair actions
+              to generate appropriate repair actions.
             */
            HashSet newset=new HashSet();
            for(Iterator cit=cantremove.iterator();cit.hasNext();) {
@@ -170,8 +170,41 @@ public class GraphAnalysis {
                if (termination.conjunctions.contains(gn))
                    return null; // Out of luck
            }
-           
-           
+
+           /* Search through abstract repair actions & correspond data structure updates */
+           for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode)it.next();
+               TermNode tn=(TermNode)gn.getOwner();
+
+               for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                   GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+                   GraphNode gn2=e.getTarget();
+                   TermNode tn2=(TermNode)gn2.getOwner();
+                   if (tn2.getType()!=TermNode.UPDATE)
+                       continue;
+
+                   boolean containsgn=cantremove.contains(gn);
+                   boolean containsgn2=cantremove.contains(gn2);
+
+                   cantremove.add(gn);
+                   cantremove.add(gn2);
+
+                   Set cycle=GraphNode.findcycles(cantremove);
+                   if (cycle.contains(gn2)) {
+                       if (!mustremove.contains(gn2)) {
+                           change=true;
+                           mustremove.add(gn2);
+                       }
+                   }
+
+                   if (!containsgn)
+                       cantremove.remove(gn);
+                   if (!containsgn2)
+                       cantremove.remove(gn2);
+               }
+           }
+
+           /* Searches individual conjunctions + abstract action +updates for cycles */
            for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
                GraphNode gn=(GraphNode)it.next();
                boolean foundnocycle=false;
@@ -189,8 +222,10 @@ public class GraphAnalysis {
                        if (tn3.getType()!=TermNode.UPDATE)
                            continue;
                        boolean containsgn=cantremove.contains(gn);
+                       boolean containsgn2=cantremove.contains(gn2);
                        boolean containsgn3=cantremove.contains(gn3);
                        cantremove.add(gn);
+                       cantremove.add(gn2);
                        cantremove.add(gn3);
                        Set cycle=GraphNode.findcycles(cantremove);
                        if (cycle.contains(gn3)) {
@@ -204,6 +239,8 @@ public class GraphAnalysis {
                        }
                        if (!containsgn)
                            cantremove.remove(gn);
+                       if (!containsgn2)
+                           cantremove.remove(gn2);
                        if (!containsgn3)
                            cantremove.remove(gn3);
                    }
@@ -215,6 +252,53 @@ public class GraphAnalysis {
                    }
                }
            }
+
+           /* Searches scope nodes + compensation nodes */
+           for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode)it.next();
+               boolean foundcompensation=false;
+               if (nodes.contains(gn)) {
+                   for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                       GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+                       GraphNode gn2=e.getTarget();
+                       TermNode tn2=(TermNode)gn2.getOwner();
+                       
+                       if (tn2.getType()!=TermNode.UPDATE)
+                           continue;
+                       /* We have a compensation node */
+                       boolean containsgn=cantremove.contains(gn);
+                       boolean containsgn2=cantremove.contains(gn2);
+                       cantremove.add(gn);
+                       cantremove.add(gn2);
+                       
+                       Set cycle=GraphNode.findcycles(cantremove);
+                       if (cycle.contains(gn2)) {
+                           if (!mustremove.contains(gn2)) {
+                               change=true;
+                               mustremove.add(gn2);
+                           }
+                       } else {
+                           if (!mustremove.contains(gn2))
+                               foundcompensation=true;
+                       }
+                       if (!containsgn)
+                           cantremove.remove(gn);
+                       if (!containsgn2)
+                           cantremove.remove(gn2);
+                   }
+               }
+               if (!foundcompensation) {
+                   for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+                       GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+                       GraphNode gn2=e.getTarget();
+                       TermNode tn2=(TermNode)gn2.getOwner();
+                       if (tn2.getType()==TermNode.UPDATE) {
+                           cantremove.add(gn2);
+                           break;
+                       }
+                   }
+               }
+           }
            couldremove.removeAll(mustremove);
            couldremove.removeAll(cantremove);
            
@@ -224,6 +308,13 @@ public class GraphAnalysis {
            if(change)
                continue; //recalculate
 
+           try {
+               GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
+           } catch (Exception e) {
+               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");

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 2dccba3de978c8fce64bba9c4ed774d08bda1169..55f49522eb3b8d4d0ab834ffe628749282435816 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -9,6 +9,8 @@ public class Termination {
     Hashtable conjunctionmap;
 
     HashSet abstractrepair;
+    HashSet abstractrepairadd;
+
     HashSet updatenodes;
     HashSet consequencenodes;
 
@@ -29,6 +31,7 @@ public class Termination {
        conjunctions=new HashSet();
        conjunctionmap=new Hashtable();
        abstractrepair=new HashSet();
+       abstractrepairadd=new HashSet();
        scopenodes=new HashSet();
        scopesatisfy=new Hashtable();
        scopefalsify=new Hashtable();
@@ -293,6 +296,7 @@ public class Termination {
                predtoabstractmap.put(tp,new HashSet());
            ((Set)predtoabstractmap.get(tp)).add(gn);
            abstractrepair.add(gn);
+           abstractrepairadd.add(gn);
            abstractadd.put(sd,gn);
            
            DNFPredicate tp2=new DNFPredicate(true,ip);
@@ -303,6 +307,7 @@ public class Termination {
                predtoabstractmap.put(tp2,new HashSet());
            ((Set)predtoabstractmap.get(tp2)).add(gn2);
            abstractrepair.add(gn2);
+           abstractrepairadd.add(gn2);
            abstractremove.put(sd,gn2);
        }
 
@@ -324,6 +329,7 @@ public class Termination {
                predtoabstractmap.put(tp,new HashSet());
            ((Set)predtoabstractmap.get(tp)).add(gn);
            abstractrepair.add(gn);
+           abstractrepairadd.add(gn);
            abstractadd.put(rd,gn);
            
            DNFPredicate tp2=new DNFPredicate(true,ip);
@@ -334,6 +340,7 @@ public class Termination {
                predtoabstractmap.put(tp2,new HashSet());
            ((Set)predtoabstractmap.get(tp2)).add(gn2);
            abstractrepair.add(gn2);
+           abstractrepairadd.add(gn2);
            abstractremove.put(rd,gn2);
        }
        
@@ -577,8 +584,11 @@ public class Termination {
                }
                RelationInclusion ri=(RelationInclusion)r.getInclusion();
                if (!(ri.getLeftExpr() instanceof VarExpr)) {
-                   Updates up=new Updates(ri.getLeftExpr(),leftindex);
-                   un.addUpdate(up);
+                   if (ri.getLeftExpr().isValue()) {
+                       Updates up=new Updates(ri.getLeftExpr(),leftindex);
+                       un.addUpdate(up);
+                   } else
+                       goodflag=false;
                } else {
                    VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
                    if (vd.isGlobal()) {
@@ -588,8 +598,11 @@ public class Termination {
                        goodflag=false;
                }
                if (!(ri.getRightExpr() instanceof VarExpr)) {
-                   Updates up=new Updates(ri.getRightExpr(),rightindex);
-                   un.addUpdate(up);
+                   if (ri.getRightExpr().isValue()) {
+                       Updates up=new Updates(ri.getRightExpr(),rightindex);
+                       un.addUpdate(up);
+                   } else
+                       goodflag=false;
                } else {
                    VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
                    if (vd.isGlobal()) {
@@ -741,11 +754,14 @@ public class Termination {
                    if(inc instanceof SetInclusion) {
                        SetInclusion si=(SetInclusion)inc;
                        if (!(si.elementexpr instanceof VarExpr)) {
-                           Updates up=new Updates(si.elementexpr,0);
-                           un.addUpdate(up);
+                           if (si.elementexpr.isValue()) {
+                               Updates up=new Updates(si.elementexpr,0);
+                               un.addUpdate(up);
+                           } else
+                               continue;
                        } else {
                            VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
-                           if (un.getBinding(vd)==null) {
+                           if (vd.isGlobal()) {
                                Updates up=new Updates(si.elementexpr,0);
                                un.addUpdate(up);
                            }
@@ -753,21 +769,27 @@ public class Termination {
                    } else if (inc instanceof RelationInclusion) {
                        RelationInclusion ri=(RelationInclusion)inc;
                        if (!(ri.getLeftExpr() instanceof VarExpr)) {
-                           Updates up=new Updates(ri.getLeftExpr(),0);
-                           un.addUpdate(up);
+                           if (ri.getLeftExpr().isValue()) {
+                               Updates up=new Updates(ri.getLeftExpr(),0);
+                               un.addUpdate(up);
+                           } else
+                               continue;
                        } else {
                            VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
-                           if (un.getBinding(vd)==null) {
+                           if (vd.isGlobal()) {
                                Updates up=new Updates(ri.getLeftExpr(),0);
                                un.addUpdate(up);
                            }
                        }
                        if (!(ri.getRightExpr() instanceof VarExpr)) {
-                           Updates up=new Updates(ri.getRightExpr(),1);
-                           un.addUpdate(up);
+                           if (ri.getRightExpr().isValue()) {
+                               Updates up=new Updates(ri.getRightExpr(),1);
+                               un.addUpdate(up);
+                           } else
+                               continue;
                        } else {
                            VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
-                           if (un.getBinding(vd)==null) {
+                           if (vd.isGlobal()) {
                                Updates up=new Updates(ri.getRightExpr(),1);
                                un.addUpdate(up);
                            }

diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
index a4e6d801654d56d2e54de76a00659671342909bc..f17d9564253cd9785be07832a5851518641708ff 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Updates.java
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -57,7 +57,14 @@ class Updates {
            return ((VarExpr)leftexpr).getVar();
        } else if (isField()) {
            Expr e=leftexpr;
-           for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+           do {
+               for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+               if (e instanceof VarExpr)
+                   break;
+               if (e instanceof CastExpr)
+                   e=((CastExpr)e).getExpr();
+               else throw new Error("Unrecognized Expr:"+e.name());
+           } while(true);
            return ((VarExpr)e).getVar();
        } else {
            System.out.println(toString());