Additional enhancements to compute mustremove and cantremove sets for

[repair.git] / Repair / RepairCompiler / MCC / IR / Termination.java

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 8aa0370964d51c712852ef95bbb73ea657fca7d7..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;
 
@@ -19,6 +21,7 @@ public class Termination {
     Hashtable abstractadd;
     Hashtable abstractremove;
     Hashtable conjtonodemap;
+    Hashtable predtoabstractmap;
     Set removedset;
 
     State state;
@@ -28,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();
@@ -37,6 +41,7 @@ public class Termination {
        abstractadd=new Hashtable();
        abstractremove=new Hashtable();
        conjtonodemap=new Hashtable();
+       predtoabstractmap=new Hashtable();
        if (!Compiler.REPAIR)
            return;
 
@@ -267,6 +272,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,14 +292,22 @@ 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);
+           abstractrepairadd.add(gn);
            abstractadd.put(sd,gn);
            
            DNFPredicate tp2=new DNFPredicate(true,ip);
            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);
+           abstractrepairadd.add(gn2);
            abstractremove.put(sd,gn2);
        }
 
@@ -309,14 +325,22 @@ 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);
+           abstractrepairadd.add(gn);
            abstractadd.put(rd,gn);
            
            DNFPredicate tp2=new DNFPredicate(true,ip);
            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);
+           abstractrepairadd.add(gn2);
            abstractremove.put(rd,gn2);
        }
        
@@ -560,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()) {
@@ -571,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()) {
@@ -724,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);
                            }
@@ -736,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);
                            }