X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=55f49522eb3b8d4d0ab834ffe628749282435816;hb=aba31a4e9a0ea1e1cf30a6f4eb66baca2ae52c5d;hp=8aa0370964d51c712852ef95bbb73ea657fca7d7;hpb=cdd4513e39de359245e55af313d8bdea2167a253;p=repair.git

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 8aa0370..55f4952 100755
--- 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);
 			    }