From 95271a46ce6573ff5532fda46561d2936cb25393 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 12 Aug 2004 21:41:40 +0000
Subject: [PATCH] Improved precision of computation of maximum set sizes.
 Removed generation of redundant rules by implicitschema.

---
 .../RepairCompiler/MCC/IR/ComputeMaxSize.java | 271 ++++++++++++++++--
 Repair/RepairCompiler/MCC/IR/Expr.java        |   7 +
 .../RepairCompiler/MCC/IR/ImplicitSchema.java | 101 ++++++-
 3 files changed, 359 insertions(+), 20 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
index 51221c3..a5a9d57 100755
--- a/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
+++ b/Repair/RepairCompiler/MCC/IR/ComputeMaxSize.java
@@ -7,12 +7,14 @@ import java.util.*;
 public class ComputeMaxSize {
     State state;
     Hashtable sizemap; /* -1 means infinity */
-
+    static int KBOUND=100;
 
     public ComputeMaxSize(State state) {
 	this.state=state;
 	sizemap=new Hashtable();
 	computesizes();
+	postprocess();
+	printsizes();
     }
     
     /** This method compute relation and set maximum sizes */
@@ -28,29 +30,42 @@ public class ComputeMaxSize {
 		Descriptor d=(Descriptor)dit.next();
 		if (d instanceof ReservedSetDescriptor)
 		    continue;
-		int totalsize=0;
+		int totalstarts=0;
+		int totalchains=0;
+		Rule chainrule=null;
 		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;
+			boolean start=true;
 			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();
+				    size=getsize(d2);
+				}
+				if (d==d2) {
+				    if (!start)
+					size=-1;
+				    else
+					size=1;
+				    start=false;
 				}
-				if ((size!=0)&&(d==d2))
-				    size=-1;
 			    } else if (q instanceof SetQuantifier) {
 				Descriptor d2=((SetQuantifier)q).getSet();
 				if (sizemap.containsKey(d2)) {
-				    size=((Integer)sizemap.get(d2)).intValue();
+				    size=getsize(d2);
+				}
+				if (d==d2) {
+				    if (!start)
+					size=-1;
+				    else
+					size=1;
+				    start=false;
 				}
-				if ((size!=0)&&(d==d2))
-				    size=-1;
 			    } else if (q instanceof ForQuantifier) {
 				ForQuantifier fq=(ForQuantifier)q;
 				boolean lowint=OpExpr.isInt(fq.lower);
@@ -60,30 +75,248 @@ public class ComputeMaxSize {
 				    if (size<=0) /* Catch sneaky bounds */
 					throw new Error("Funny bounds in: "+fq);
 				} else size=-1;
-			    } else {
-				size=-1;
-			    }
+			    } else 
+				throw new Error("Unrecognized Quantifier");
+			    
 			    if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
 				rulesize=-1;
 			    else
 				rulesize=rulesize*size;
 			}
 			
-			if ((rulesize==-1)||(totalsize==-1))
-			    totalsize=-1;
-			else
-			    totalsize+=rulesize;
+			if (start) {
+			    if ((rulesize==-1)||(totalstarts==-1))
+				totalstarts=-1;
+			    else
+				totalstarts+=rulesize;
+			} else {
+			    if (totalchains==0)
+				chainrule=r;
+			    else
+				chainrule=null;
+			    if ((rulesize==-1)||(totalchains==-1))
+				totalchains=-1;
+			    else
+				totalchains+=rulesize;
+			}
 		    }
 		}
-		if (!sizemap.containsKey(d)||((Integer)sizemap.get(d)).intValue()!=totalsize) {
+		if (totalstarts>=KBOUND)
+		    totalstarts=-1;
+		if (totalchains>=KBOUND)
+		    totalchains=-1;
+
+		if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
 		    change=true;
-		    sizemap.put(d,new Integer(totalsize));
+		    MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+		    sizemap.put(d,so);
 		}
 	    }
    	}
     }
+
+    void printsizes() {
+	Set descriptorset=new HashSet();
+	descriptorset.addAll(state.stSets.getAllDescriptors());
+	descriptorset.addAll(state.stRelations.getAllDescriptors());
+	for(Iterator dit=descriptorset.iterator();dit.hasNext();) {
+	    Descriptor d=(Descriptor)dit.next();
+	    if (d instanceof ReservedSetDescriptor)
+		continue;
+	    System.out.println("size("+d+")="+getsize(d));
+	}
+    }
+
+    private void postprocess() {
+	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 totalstarts=0;
+		int totalchains=0;
+		Rule chainrule=null;
+		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;
+			boolean start=true;
+			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=getsize(d2);
+				}
+				if (d==d2) {
+				    if (!start)
+					size=-1;
+				    else
+					size=1;
+				    start=false;
+				} else {
+				    if (getchainrule(d2)!=null) {
+					if (isMutuallyExclusive(r, getchainrule(d2)))
+					    size=getstarts(d2);
+				    }
+				}
+			    } else if (q instanceof SetQuantifier) {
+				Descriptor d2=((SetQuantifier)q).getSet();
+				if (sizemap.containsKey(d2)) {
+				    size=getsize(d2);
+				}
+				if (d==d2) {
+				    if (!start)
+					size=-1;
+				    else
+					size=1;
+				    start=false;
+				} else {
+				    if (getchainrule(d2)!=null) {
+					if (isMutuallyExclusive(r, getchainrule(d2)))
+					    size=getstarts(d2);
+				    }
+				}
+			    } else if (q instanceof ForQuantifier) {
+				ForQuantifier fq=(ForQuantifier)q;
+				boolean lowint=OpExpr.isInt(fq.lower);
+				boolean highint=OpExpr.isInt(fq.upper);
+				if (lowint&&highint) {
+				    size=1+OpExpr.getInt(fq.upper)-OpExpr.getInt(fq.lower);
+				    if (size<=0) /* Catch sneaky bounds */
+					throw new Error("Funny bounds in: "+fq);
+				} else size=-1;
+			    } else 
+				throw new Error("Unrecognized Quantifier");
+			    
+			    if ((rulesize!=0)&&((size==-1)||(rulesize==-1)))
+				rulesize=-1;
+			    else
+				rulesize=rulesize*size;
+			}
+			
+			if (start) {
+			    if ((rulesize==-1)||(totalstarts==-1))
+				totalstarts=-1;
+			    else
+				totalstarts+=rulesize;
+			} else {
+			    if (totalchains==0)
+				chainrule=r;
+			    else
+				chainrule=null;
+			    if ((rulesize==-1)||(totalchains==-1))
+				totalchains=-1;
+			    else
+				totalchains+=rulesize;
+			}
+		    }
+		}
+		if (totalstarts>=KBOUND)
+		    totalstarts=-1;
+		if (totalchains>=KBOUND)
+		    totalchains=-1;
+
+		if (!sizemap.containsKey(d)||getstarts(d)!=totalstarts||getchains(d)!=totalchains) {
+		    change=true;
+		    MaxSizeObject so=new MaxSizeObject(totalstarts,totalchains,chainrule);
+		    sizemap.put(d,so);
+		}
+	    }
+   	}
+
+    }
+
+    int getstarts(Descriptor d) {
+	MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+	return so.maxstarts;
+    }
+    int getchains(Descriptor d) {
+	MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+	return so.numberchains;
+    }
     int getsize(Descriptor d) {
-	return ((Integer)sizemap.get(d)).intValue();
+	MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+	if (so.maxstarts==0)
+	    return 0;
+	if (so.numberchains!=0)
+	    return -1;
+	return so.maxstarts;
     }
-}
 
+    private Rule getchainrule(Descriptor d) {
+	MaxSizeObject so=(MaxSizeObject)sizemap.get(d);
+	return so.chainrule;
+    }
+
+    public static boolean isMutuallyExclusive(Rule r1,Rule r2) {
+	// Building a map between quantifier variables
+	if (r1.numQuantifiers()!=r2.numQuantifiers())
+	    return false;
+	Set usedDescriptors=new HashSet();
+	Hashtable varmap=new Hashtable();
+
+    outerloop:
+	for(int i=0;i<r1.numQuantifiers();i++) {
+	    Quantifier q1=r1.getQuantifier(i);
+	    if (!(q1 instanceof SetQuantifier))
+		return false;
+	    if (usedDescriptors.contains(((SetQuantifier)q1).getSet()))
+		return false;
+	    usedDescriptors.add(((SetQuantifier)q1).getSet());
+	    for(int j=0;j<r2.numQuantifiers();j++) {
+		Quantifier q2=r2.getQuantifier(j);
+		if (!(q2 instanceof SetQuantifier))
+		    return false;
+		if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
+		    varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+		    continue outerloop;
+		}
+	    }
+	    return false;
+	}
+	DNFRule dr1=r1.getDNFGuardExpr();
+	DNFRule dr2=r2.getDNFGuardExpr();
+	for(int i=0;i<dr1.size();i++) {
+	    for(int j=0;j<dr2.size();j++) {
+		RuleConjunction rc1=dr1.get(i);
+		RuleConjunction rc2=dr2.get(j);
+		if (!exclusive(varmap,rc1,rc2))
+		    return false;
+	    }
+	}
+	return true;
+    }
+    
+    private static boolean exclusive(Hashtable varmap, RuleConjunction rc1, RuleConjunction rc2) {
+	for (int i=0;i<rc1.size();i++) {
+	    for (int j=0;j<rc2.size();j++) {
+		DNFExpr de1=rc1.get(i);
+		DNFExpr de2=rc2.get(j);
+		if ((de1.getNegation()!=de2.getNegation())&&
+		    (de1.getExpr().equals(varmap,de2.getExpr())))
+		    return true;
+	    }
+	}
+	return false;
+    }
+}
+class MaxSizeObject {
+    int maxstarts;
+    int numberchains;
+    Rule chainrule;
+    
+    public MaxSizeObject(int start,int chain, Rule r) {
+	maxstarts=start;
+	numberchains=chain;
+	chainrule=r;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index d45280d..51ae613 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -82,6 +82,13 @@ public abstract class Expr {
 	return null; /* unknown value */
     }
 
+    public Expr stripCastExpr() {
+	Expr ptr=this;
+	while (ptr instanceof CastExpr)
+	    ptr=((CastExpr)ptr).getExpr();
+	return ptr;
+    }
+
     public boolean isSafe() {
 	return true;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 85bd076..f229334 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -338,6 +338,8 @@ public class ImplicitSchema {
     void updaterules() {
 	Vector oldrules=state.vRules;
 	Vector newrules=new Vector();
+	Vector allrules=new Vector();
+	allrules.addAll(oldrules);
 	for(int i=0;i<oldrules.size();i++) {
 	    Rule r=(Rule)oldrules.get(i);
 	    if (r.inclusion instanceof SetInclusion) {
@@ -366,7 +368,9 @@ public class ImplicitSchema {
 					     this set, as item is already
 					     in this set. */
 			}
-			
+			if (isRedundant(allrules,r,sd1))
+			    continue;
+
 			Rule nr=new Rule();
 			nr.setGuardExpr(r.getGuardExpr());
 			nr.quantifiers=r.quantifiers;
@@ -377,6 +381,7 @@ public class ImplicitSchema {
 			nr.setnogenerate();
 			nr.num=r.num;
 			newrules.add(nr);
+			allrules.add(nr);
 			state.implicitrule.put(nr,r);
 			if (!state.implicitruleinv.containsKey(r))
 			    state.implicitruleinv.put(r,new HashSet());
@@ -386,4 +391,98 @@ public class ImplicitSchema {
 	}
 	oldrules.addAll(newrules);
     }
+
+    private boolean isRedundant(Vector allrules,Rule r,SetDescriptor sd) {
+    outerloop:
+	for(int i=0;i<allrules.size();i++) {
+	    Rule r2=(Rule)allrules.get(i);
+	    if (!(r2.getInclusion() instanceof SetInclusion))
+		continue;
+	    //old rule to the same set as the new rule's inclusion condition
+	    if (sd!=((SetInclusion)r2.getInclusion()).getSet())
+		continue;
+	    //old rule quantifiers over superset of new rule's quantification
+	    Hashtable varmap=buildvarmap(state,r2,r,true);
+	    if (varmap==null)
+		continue;
+	    Expr ei1=((SetInclusion)r.getInclusion()).getExpr();
+	    Expr ei2=((SetInclusion)r2.getInclusion()).getExpr();
+	    if (!ei2.stripCastExpr().equals(varmap,ei1.stripCastExpr())) //adds same expression
+		continue;
+	    DNFRule dr1=r.getDNFGuardExpr();
+	    DNFRule dr2=r2.getDNFGuardExpr();
+
+	    //need to show that whenever the guard in r is satisfied, some guard in r2 is satisfied
+	innerloop1:
+	    for(int j=0;j<dr1.size();j++) {
+		RuleConjunction rc1=dr1.get(j);
+	    innerloop2:
+		for(int k=0;k<dr2.size();k++) {
+		    RuleConjunction rc2=dr2.get(k);
+		    //if rc1 being true implies rc2 being true continue to innerloop1
+		innerloop3:
+		    for(int l=0;l<rc2.size();l++) {
+			DNFExpr de2=rc2.get(l);
+			for(int m=0;m<rc1.size();m++) {
+			    DNFExpr de1=rc1.get(m);
+			    if (de1.getNegation()==de2.getNegation()&&
+				de2.getExpr().equals(varmap,de1.getExpr()))
+				continue innerloop3;
+			}
+			continue innerloop2; //see if we can satisfy some other conjunction
+		    }
+		    continue innerloop1; //all of the expr's in this conjunction are satisfied
+		}
+		continue outerloop;
+	    }
+	    return true;
+	}
+	return false;
+    }
+
+    public static Hashtable buildvarmap(State state,Rule r1,Rule r2,boolean subsetting) {
+	// Building a map between quantifier variables
+	Hashtable varmap=new Hashtable();
+	if (r1.numQuantifiers()!=r2.numQuantifiers())
+	    return null;
+	Set usedQuantifiers=new HashSet();
+    outerloop:
+	for(int i=0;i<r1.numQuantifiers();i++) {
+	    Quantifier q1=r1.getQuantifier(i);
+
+	    if (q1 instanceof SetQuantifier) {
+		for(int j=0;j<r2.numQuantifiers();j++) {
+		    Quantifier q2=r2.getQuantifier(j);
+		    if (!(q2 instanceof SetQuantifier))
+			continue;;
+		    if (usedQuantifiers.contains(q2))
+			continue;
+		    if (((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()||
+			(subsetting&&((SetQuantifier)q1).getSet().isSubset(((SetQuantifier)q2).getSet()))) {
+			varmap.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
+			usedQuantifiers.add(q2);
+			continue outerloop;
+		    }
+		}
+		return null;
+	    } else if (q1 instanceof RelationQuantifier) {
+		for(int j=0;j<r2.numQuantifiers();j++) {
+		    Quantifier q2=r2.getQuantifier(j);
+		    if (!(q2 instanceof RelationQuantifier))
+			continue;
+		    if (usedQuantifiers.contains(q2))
+			continue;
+		    if (((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
+			varmap.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
+			varmap.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
+			usedQuantifiers.add(q2);
+			continue outerloop;
+		    }
+		}
+		return null;
+	    }
+	}
+	return varmap;
+    }
+
 }
-- 
2.34.1