X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FImplicitSchema.java;h=f229334e87696c791017656abd7e88e21d4ff65a;hp=1be006833b5a50bd199929d0175afd9f8a17e376;hb=fcb08dbb9564da3732dd8b0cbf0088d0f9826541;hpb=0ddd66cf596f161886dc67214f3fb2e19f6f7168

diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 1be0068..f229334 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -1,5 +1,7 @@
 package MCC.IR;
 import MCC.State;
+import MCC.Compiler;
+
 import java.util.*;
 
 public class ImplicitSchema {
@@ -7,11 +9,13 @@ public class ImplicitSchema {
     SetAnalysis setanalysis;
     public ImplicitSchema(State state) {
 	this.state=state;
-	this.setanalysis=new SetAnalysis(state);
+	this.setanalysis=state.setanalysis;
     }
 
     public void update() {
-	//	updaterules();
+	if (Compiler.REPAIR) {
+	    updaterules();
+	}
 	updateconstraints();
 	updaterelationconstraints();
     }
@@ -23,6 +27,11 @@ public class ImplicitSchema {
     boolean needDR(RelationDescriptor rd,boolean isdomain) {
 	Vector rules=state.vRules;
 	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	if (sd instanceof ReservedSetDescriptor)
+	    return false;
+
+	/* See if there is a rule that adds the corresponding range or domain
+	   of the relation to the correct set */
 	for(int i=0;i<rules.size();i++) {
 	    Rule r=(Rule)rules.get(i);
 	    if ((r.numQuantifiers()==1)&&
@@ -39,8 +48,6 @@ public class ImplicitSchema {
 		    return false;
 	    }
 	}
-
-
 	for(int i=0;i<rules.size();i++) {
 	    Rule r=(Rule)rules.get(i);
 	    Inclusion inc=r.getInclusion();
@@ -49,9 +56,11 @@ public class ImplicitSchema {
 		boolean good=false;
 		RelationInclusion rinc=(RelationInclusion)inc;
 		Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+		/* Check for varexpr's and quantification over */
 		if (expr instanceof VarExpr) {
 		    VarDescriptor vd=((VarExpr)expr).getVar();
 		    assert vd!=null;
+		    /* See if the var is from an appropriate quantifier */
 		    for (int j=0;j<r.numQuantifiers();j++) {
 			Quantifier q=r.getQuantifier(j);
 			if ((q instanceof SetQuantifier)&&
@@ -71,15 +80,15 @@ public class ImplicitSchema {
 			    good=true;
 			    break;
 			}
-			
 		    }
 		    if (good)
-			continue; /* Proved for this case */
+			continue; /* Checked for this case */
 		}
+		if (checkguard(r,isdomain))
+		    continue;
 		for(int j=0;j<rules.size();j++) {
 		    Rule r2=(Rule)rules.get(j);
 		    Inclusion inc2=r2.getInclusion();
-		    
 		    if (checkimplication(r,r2,isdomain)) {
 			good=true;
 			break;
@@ -88,12 +97,41 @@ public class ImplicitSchema {
 		if (good)
 		    continue;
 
-		return true; /* Couldn't prove we didn't need */
+		return true; /* Couldn't verify we didn't need */
 	    }
 	}
 	return false;
     }
 
+    boolean checkguard(Rule r,boolean isdomain) {
+	RelationInclusion inc=(RelationInclusion) r.getInclusion();
+	RelationDescriptor rd=inc.getRelation();
+	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	Expr expr=isdomain?inc.getLeftExpr():inc.getRightExpr();
+	DNFRule dnfGuard=r.getDNFGuardExpr();
+	for(int i=0;i<dnfGuard.size();i++) {
+	    RuleConjunction rconj=dnfGuard.get(i);
+	    boolean foundcheck=false;
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		if (!dexpr.getNegation()&&
+		    dexpr.getExpr() instanceof ElementOfExpr) {
+		    ElementOfExpr eoe=(ElementOfExpr)dexpr.getExpr();
+		    
+		    if (eoe.set==sd&&
+			eoe.element.equals(null,expr)) {
+			foundcheck=true;
+			break;
+		    }
+		}
+	    }
+	    if (!foundcheck) {
+		return false;
+	    }
+	}
+	return true;
+    }
+
     boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
 	/* r1 is the relation */
 	/* See if this rule guarantees relation */
@@ -101,26 +139,23 @@ public class ImplicitSchema {
 	   1. match up quantifiers
 	   2. check inclusion condition
 	   3. see if guard expr of set rule is more general */
-
 	RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
 	RelationDescriptor rd=inc1.getRelation();
 	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
 	Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
-
+	
 	Inclusion inc2=r2.getInclusion();
 	if (!(inc2 instanceof SetInclusion))
 	    return false;
 	SetInclusion sinc2=(SetInclusion)inc2;
 	if (sinc2.getSet()!=sd)
 	    return false;
-	if (r1.numQuantifiers()!=r2.numQuantifiers())
-	    return false; 
+
 	/* Construct a mapping between quantifiers */
 	int[] mapping=new int[r2.numQuantifiers()];
 	HashMap map=new HashMap();
 	for(int i=0;i<r1.numQuantifiers();i++) {
 	    Quantifier q1=r1.getQuantifier(i);
-	    boolean foundmapping=false;
 	    for (int j=0;j<r2.numQuantifiers();j++) {
 		if (mapping[j]==1)
 		    continue; /* Its already used */
@@ -129,7 +164,6 @@ public class ImplicitSchema {
 		    ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
 		    mapping[j]=1;
 		    map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
-		    foundmapping=true;
 		    break;
 		}
 		if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
@@ -137,17 +171,28 @@ public class ImplicitSchema {
 		    mapping[j]=1;
 		    map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
 		    map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
-		    foundmapping=true;
 		    break;
 		}
+		if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
+		    ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
+		    ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
+		    mapping[j]=1;
+		    map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
+		}
 	    }
-	    if (!foundmapping)
+	}
+
+	/* Make sure all bindings in the set rule are bound */
+	for (int i=0;i<r2.numQuantifiers();i++) {
+	    if (mapping[i]!=1)
 		return false;
 	}
+
 	/* Built mapping */
 	Expr sexpr=sinc2.getExpr();
 	if (!expr.equals(map,sexpr))
 	    return false;  /* This rule doesn't add the right thing */
+
 	DNFRule drule1=r1.getDNFGuardExpr();
 	DNFRule drule2=r2.getDNFGuardExpr();
 	for (int i=0;i<drule1.size();i++) {
@@ -156,7 +201,7 @@ public class ImplicitSchema {
 	    for (int j=0;j<drule2.size();j++) {
 		RuleConjunction rconj2=drule2.get(j);
 		/* Need to show than rconj2 is true if rconj1 is true */
-		if (implication(map,rconj1,rconj2)) {
+		if (implication(map,rconj1,rconj2,sinc2)) {
 		    foundmatch=true;
 		    break;
 		}
@@ -167,10 +212,18 @@ public class ImplicitSchema {
 	return true;
     }
 
-    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2) {
+    boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
 	for(int i=0;i<rc2.size();i++) {
 	    /* Check that rc1 has all predicates that rc2 has */
 	    DNFExpr de2=rc2.get(i);
+	    /* Predicates for objects that aren't in set */
+	    if (de2.getNegation()&&
+		(de2.getExpr() instanceof ElementOfExpr)) {
+		ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
+		if (si.getSet().isSubset(eoe.set)&&
+		    si.getExpr().equals(null,eoe.element))
+		    continue; /* This predicate isn't a problem */
+	    }
 	    boolean havematch=false;
 	    for(int j=0;j<rc1.size();j++) {
 		DNFExpr de1=rc1.get(i);
@@ -285,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) {
@@ -293,17 +348,141 @@ public class ImplicitSchema {
 		if (supersets!=null)
 		    for(Iterator superit=supersets.iterator();superit.hasNext();) {
 			SetDescriptor sd1=(SetDescriptor)superit.next();
+			Expr e=((SetInclusion)r.inclusion).getExpr();
+			while(e instanceof CastExpr) {
+			    e=((CastExpr)e).getExpr();
+			}
+			if (e instanceof VarExpr) {
+			    VarDescriptor vde=((VarExpr)e).getVar();
+			    boolean ok=false;
+			    for (int j=0;j<r.numQuantifiers();j++) {
+				Quantifier tmp=r.getQuantifier(j);
+				if (tmp instanceof SetQuantifier&&
+				    ((SetQuantifier)tmp).getVar()==vde)
+				    ok=true; /* Need to make sure we don't have a relation quantifier. */
+			    }
+
+			    SetDescriptor currentset=e.getSet();
+			    if (ok&&currentset!=null&&currentset.isSubset(sd1))
+				continue; /* This rule doesn't add item to
+					     this set, as item is already
+					     in this set. */
+			}
+			if (isRedundant(allrules,r,sd1))
+			    continue;
+
 			Rule nr=new Rule();
-			nr.guard=r.guard;
+			nr.setGuardExpr(r.getGuardExpr());
 			nr.quantifiers=r.quantifiers;
 			nr.isstatic=r.isstatic;
 			nr.isdelay=r.isdelay;
 			nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
 			nr.st=r.st;
+			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());
+			((Set)state.implicitruleinv.get(r)).add(nr);
 		    }
 	    }
 	}
 	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;
+    }
+
 }