From 8098bc30c0b85814194cb8e53d62ffe5ffe318ef Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Sat, 17 Apr 2004 00:30:28 +0000
Subject: [PATCH] Added code to compute maximum sizes of sets.  So we can
 eliminate set removes when they aren't necessary.

---
 .../RepairCompiler/MCC/IR/ComputeMaxSize.java | 80 +++++++++++++++++++
 Repair/RepairCompiler/MCC/IR/Expr.java        |  2 +-
 .../RepairCompiler/MCC/IR/ExprPredicate.java  |  4 +-
 .../RepairCompiler/MCC/IR/GraphAnalysis.java  | 48 ++++++++---
 .../MCC/IR/InclusionPredicate.java            |  2 +-
 Repair/RepairCompiler/MCC/IR/OpExpr.java      | 26 ++++--
 Repair/RepairCompiler/MCC/IR/Predicate.java   |  2 +-
 .../MCC/IR/RepairGenerator.java               |  1 -
 Repair/RepairCompiler/MCC/IR/Termination.java | 12 ++-
 9 files changed, 153 insertions(+), 24 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java

diff --git a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
new file mode 100755
index 0000000..0dec8e0
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
@@ -0,0 +1,80 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+/** This class computes the maximum size of sets and relations */
+
+public class ComputeMaxSize {
+    State state;
+    Hashtable sizemap; /* -1 means infinity */
+
+
+    public ComputeMaxSize(State state) {
+	this.state=state;
+	sizemap=new Hashtable();
+	computesizes();
+    }
+    
+    /** This method compute relation and set maximum sizes */
+    private void computesizes() {
+	Vector rules=state.vRules;
+	boolean change=true;
+	Set descriptorset=new HashSet();
+	descriptorset.addAll(state.stSets.getAllDescriptors());
+	descriptorset.addAll(state.stRelations.getAllDescriptors());
+	while(change) {
+	    change=false;
+	    for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+		Descriptor d=(Descriptor)dit.next();
+		if (d instanceof ReservedSetDescriptor)
+		    continue;
+		int totalsize=0;
+		for(int i=0;i<rules.size();i++) {
+		    Rule r=(Rule)rules.get(i);
+		    if (r.getInclusion().getTargetDescriptors().contains(d)) {
+			/* This rule may add items to this set or relation */
+			int rulesize=1;
+			for(int j=0;j<r.numQuantifiers();j++) {
+			    Quantifier q=r.getQuantifier(j);
+			    int size=0;
+			    if (q instanceof RelationQuantifier) {
+				Descriptor d2=((RelationQuantifier)q).getRelation();
+				if (sizemap.containsKey(d2)) {
+				    size=((Integer)sizemap.get(d2)).intValue();
+				}
+				if ((size!=0)&&(d==d2))
+				    size=-1;
+			    } if (q instanceof SetQuantifier) {
+				Descriptor d2=((SetQuantifier)q).getSet();
+				if (sizemap.containsKey(d2)) {
+				    size=((Integer)sizemap.get(d2)).intValue();
+				}
+				if ((size!=0)&&(d==d2))
+				    size=-1;
+			    } else {
+				size=-1;
+			    }
+			    if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
+				rulesize=-1;
+			    else
+				rulesize=rulesize*size;
+			}
+			
+			if ((rulesize==-1)||(totalsize==-1))
+			    totalsize=-1;
+			else
+			    totalsize+=rulesize;
+		    }
+		}
+		if (!sizemap.containsKey(d)||((Integer)sizemap.get(d)).intValue()!=totalsize) {
+		    change=true;
+		    sizemap.put(d,new Integer(totalsize));
+		}
+	    }
+   	}
+    }
+    int getsize(Descriptor d) {
+	return ((Integer)sizemap.get(d)).intValue();
+    }
+}
+
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 1e13217..e98abc5 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -44,7 +44,7 @@ public abstract class Expr {
 	return false;
     }
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
 	System.out.println(this.getClass().getName());
 	throw new Error("Unrecognized EXPR");
     }
diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 4bed231..7626732 100755
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -45,8 +45,8 @@ public class ExprPredicate extends Predicate {
         return expr.getInversedRelations();
     }
 
-    public int[] getRepairs(boolean negated) {
-	return expr.getRepairs(negated);
+    public int[] getRepairs(boolean negated, Termination t) {
+	return expr.getRepairs(negated,t);
     }
 
     public Descriptor getDescriptor() {
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3bfefc0..e89898a 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -114,6 +114,13 @@ public class GraphAnalysis {
 	    for(Iterator it=cycles2.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
 		if (termination.conjunctions.contains(gn)) {
+		    try {
+			GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
+		    } catch (Exception e) {
+			e.printStackTrace();
+			System.exit(-1);
+		    }
+
 		    System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
 		    return null; // Out of luck
 		}
@@ -230,13 +237,18 @@ public class GraphAnalysis {
 	    /* Searches scope nodes + compensation nodes */
 	    for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
-		boolean foundcompensation=false;
+		int count=0;
 		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.CONSEQUENCE)&&
+			    !mustremove.contains(gn2))
+			    count++;
+			    
+
 			if (tn2.getType()!=TermNode.UPDATE)
 			    continue;
 			/* We have a compensation node */
@@ -253,22 +265,26 @@ public class GraphAnalysis {
 			    }
 			} else {
 			    if (!mustremove.contains(gn2))
-				foundcompensation=true;
+				count++;
 			}
 			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;
+		
+		    if (count==1) {
+			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||tn2.getType()==TermNode.CONSEQUENCE)&&
+				!mustremove.contains(gn2)) {
+				if (!cantremove.contains(gn2)) {
+				    cantremove.add(gn2);
+				    change=true;
+				}
+			    }
 			}
 		    }
 		}
@@ -297,6 +313,16 @@ public class GraphAnalysis {
 		GraphNode gn=(GraphNode)it.next();
 		System.out.println(gn.getTextLabel());
 	    }
+	    System.out.println("Must remove set:");
+	    for(Iterator it=mustremove.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		System.out.println(gn.getTextLabel());
+	    }
+	    System.out.println("Cant remove set:");
+	    for(Iterator it=cantremove.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		System.out.println(gn.getTextLabel());
+	    }
 	    
 	    
 	    while(true) {
diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index c27bb44..8c4e6d1 100755
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -56,7 +56,7 @@ public class InclusionPredicate extends Predicate {
 	    return setexpr.sd;
     }
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
 	if (setexpr instanceof ImageSetExpr) {
 	    if (negated)
 		return new int[] {AbstractRepair.REMOVEFROMRELATION};
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index c7cdd0d..4714735 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -178,7 +178,7 @@ public class OpExpr extends Expr {
     }
     
 
-    public int[] getRepairs(boolean negated) {
+    public int[] getRepairs(boolean negated, Termination t) {
 	if (left instanceof RelationExpr)
 	    return new int[] {AbstractRepair.MODIFYRELATION};
 	if (left instanceof SizeofExpr) {
@@ -199,35 +199,51 @@ public class OpExpr extends Expr {
 		    op=Opcode.GT;
 	    }
 
+	    int maxsize=t.maxsize.getsize(getDescriptor());
+	    int size=getInt(right);
 
 
 	    boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
 	    if (isRelation) {
 		if (op==Opcode.EQ) {
-		    if (((IntegerLiteralExpr)right).getValue()==0)
+		    if (size==0)
 			return new int[] {AbstractRepair.REMOVEFROMRELATION};
-		    else
+		    else {
+			if ((maxsize!=-1)&&maxsize<=size)
+			    return new int[] {AbstractRepair.ADDTORELATION};
 			return new int[] {AbstractRepair.ADDTORELATION,
 					  AbstractRepair.REMOVEFROMRELATION};
+		    }
 		} else if (op==Opcode.GE||op==Opcode.GT) {
 		    return new int[]{AbstractRepair.ADDTORELATION}; 
 		} else if (op==Opcode.LE||op==Opcode.LT) {
+		    if ((op==Opcode.LT&&maxsize!=-1&&maxsize<size)||(op==Opcode.LE&&maxsize!=-1&&maxsize<=size))
+			return new int[0];
 		    return new int[]{AbstractRepair.REMOVEFROMRELATION};
 		} else if (op==Opcode.NE) {
+		    if (maxsize<size&&maxsize!=-1)
+			return new int[0];
 		    return new int[]{AbstractRepair.ADDTORELATION};
 		} else throw new Error();
 	    } else {
 		if (op==Opcode.EQ) {
-		    if (((IntegerLiteralExpr)right).getValue()==0)
+		    if (size==0)
 			return new int[] {AbstractRepair.REMOVEFROMSET};			
-		    else
+		    else {
+			if (maxsize<=size&&maxsize!=-1)
+			    return new int[] {AbstractRepair.ADDTOSET};
 			return new int[] {AbstractRepair.ADDTOSET,
 					      AbstractRepair.REMOVEFROMSET};
+		    }
 		} else if (op==Opcode.GE||op==Opcode.GT) {
 		    return new int[] {AbstractRepair.ADDTOSET}; 
 		} else if (op==Opcode.LE||op==Opcode.LT) {
+		    if ((op==Opcode.LT&&maxsize<size&&maxsize!=-1)||(op==Opcode.LE&&maxsize<=size&&maxsize!=-1))
+			return new int[0];
 		    return new int[] {AbstractRepair.REMOVEFROMSET};
 		} else if (op==Opcode.NE) {
+		    if (maxsize<size&&maxsize!=-1)
+			return new int[0];
 		    return new int[] {AbstractRepair.ADDTOSET};
 		} else throw new Error();
 	    }
diff --git a/Repair/RepairCompiler/MCC/IR/Predicate.java b/Repair/RepairCompiler/MCC/IR/Predicate.java
index cb9aa39..be84d66 100755
--- a/Repair/RepairCompiler/MCC/IR/Predicate.java
+++ b/Repair/RepairCompiler/MCC/IR/Predicate.java
@@ -7,7 +7,7 @@ public abstract class Predicate extends LogicStatement {
     public DNFConstraint constructDNF() {
 	return new DNFConstraint(this);
     }
-    abstract public int[] getRepairs(boolean negated);
+    abstract public int[] getRepairs(boolean negated, Termination t);
     abstract public Descriptor getDescriptor();
     abstract public boolean inverted();
     public boolean usesDescriptor(RelationDescriptor rd) {
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index fe034f2..9d236e8 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -1547,7 +1547,6 @@ public class RepairGenerator {
 		}
 	    }
 	}
-
 	cr.endblock();
 	cr.endblock();
     }
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 55f4952..73c89f1 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -23,7 +23,7 @@ public class Termination {
     Hashtable conjtonodemap;
     Hashtable predtoabstractmap;
     Set removedset;
-
+    ComputeMaxSize maxsize;
     State state;
 
     public Termination(State state) {
@@ -45,6 +45,14 @@ public class Termination {
 	if (!Compiler.REPAIR)
 	    return;
 
+	for(int i=0;i<state.vRules.size();i++)
+	    System.out.println(state.vRules.get(i));
+	for(int i=0;i<state.vConstraints.size();i++)
+	    System.out.println(state.vConstraints.get(i));
+
+
+	maxsize=new ComputeMaxSize(state);
+
 	generateconjunctionnodes();
 	generatescopenodes();
 	generaterepairnodes();
@@ -264,7 +272,7 @@ public class Termination {
 	    Conjunction conj=tn.getConjunction();
 	    for(int i=0;i<conj.size();i++) {
 		DNFPredicate dp=conj.get(i);
-		int[] array=dp.getPredicate().getRepairs(dp.isNegated());
+		int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
 		Descriptor d=dp.getPredicate().getDescriptor();
 		for(int j=0;j<array.length;j++) {
 		    AbstractRepair ar=new AbstractRepair(dp,array[j],d);
-- 
2.34.1