From: bdemsky <bdemsky>
Date: Wed, 19 May 2004 19:06:18 +0000 (+0000)
Subject: Fixed inteferes bug, improved precision of other analysis to allow
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=39c49d28308d7d4c977de6ca15048bcdcbb3d881;ds=sidebyside

Fixed inteferes bug, improved precision of other analysis to allow
specs to still work.
---

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 5ae9aaa..2fe4aef 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -98,7 +98,6 @@ class AbstractInterferes {
 		    return false;
 	    }
 	}
-
 	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
 	    (dp.getPredicate() instanceof ExprPredicate)&&
@@ -122,13 +121,12 @@ class AbstractInterferes {
 		(op2==Opcode.GT))
 		return false;
 	}
-
 	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 	    (ar.getType()==AbstractRepair.MODIFYRELATION)&&
 	    (dp.getPredicate() instanceof ExprPredicate)&&
 	    (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
-
+	    
 	    boolean neg1=ar.getPredicate().isNegated();
 	    Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 	    boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
@@ -140,7 +138,18 @@ class AbstractInterferes {
 	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 	    boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
 	    int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
-	    Expr expr2=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
+	    Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+
+	    {
+		Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
+		Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
+		SetDescriptor sd1=lexpr1.getSet();
+		SetDescriptor sd2=lexpr2.getSet();
+		if (termination.mutuallyexclusive(sd1,sd2))
+		    return false;
+	    }
+
+
 
 	    /* Translate the opcodes */
 	    op1=Opcode.translateOpcode(neg1,op1);
@@ -152,19 +161,16 @@ class AbstractInterferes {
 		((op2==Opcode.GT)||
 		 (op2==Opcode.GE)))
 		return false;
-
 	    if (((op1==Opcode.LT)||
 		(op1==Opcode.LE))&&
 		((op2==Opcode.LT)||
 		 (op2==Opcode.LE)))
 		return false;
-		
 	    if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 		((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 		expr1.equals(null,expr2)) {
 		return false;
 	    }
-
 	    if (isInt1&&isInt2) {
 		if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 		    ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
@@ -183,52 +189,42 @@ class AbstractInterferes {
 		    size2a++;
 		if (op2==Opcode.LT)
 		    size2a--;
-
 		if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
 		    ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
 		    (size1a<=size2a))
 		    return false;
-
 		if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
 		    ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
 		    (size1a>=size2a))
 		    return false;
-		
 		if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
 		    (size1a==size2a))
 		    return false;
-
 		if ((op1==Opcode.EQ)&&
 		    ((op2==Opcode.LE)||(op2==Opcode.LT))&&
 		    (size1a<=size2a))
 		    return false;
-
 		if ((op1==Opcode.EQ)&&
 		    ((op2==Opcode.GE)||(op2==Opcode.GT))&&
 		    (size1a>=size2a))
 		    return false;
-
 		if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
 		    if (size1a!=size2)
 			return false;
-
 		if ((op1==Opcode.NE)&&
 		    (op2==Opcode.EQ)&&
 		    (size1!=size2))
 		    return false;
-
 		if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 		    ((op2==Opcode.GT)||(op2==Opcode.GE))&&
 		    (size1!=size2a))
 		    return false;
-
 		if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
 		    ((op2==Opcode.LT)||(op2==Opcode.LE))&&
 		    (size1!=size2a))
 		    return false;
 	    }
 	}
-
 	/* This handles all the c comparisons in the paper */
 	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
 	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
@@ -277,7 +273,6 @@ class AbstractInterferes {
 		(op2==Opcode.LE)||
 		(op2==Opcode.LT))
 		return false;
-	    
 	}
 	if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
 	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
@@ -290,7 +285,6 @@ class AbstractInterferes {
 	    (dp.getPredicate() instanceof InclusionPredicate)&&
 	    (dp.isNegated()==true))
 	    return false; /* Could only satisfy this predicate */
-	  
 	return true;
     }
 
diff --git a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
index dfdcfb8..cb8f81e 100755
--- a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
@@ -104,8 +104,17 @@ class ModelRuleDependence {
     private void generateEdge(Rule r1,Rule r2) {
 	Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
 	int dep=checkBody(d,r2.getDNFGuardExpr());
-	if (dep==NODEPENDENCY)
-	    dep=checkQuantifiers(d,r2);
+	if (dep==NODEPENDENCY) {
+	    SetDescriptor bsd=null;
+	    if (d instanceof SetDescriptor) {
+		SetInclusion si=(SetInclusion)r1.getInclusion();
+		if (si.getExpr() instanceof VarExpr) {
+		    VarDescriptor vd=((VarExpr)si.getExpr()).getVar();
+		    bsd=vd.getSet();
+		}
+	    }
+	    dep=checkQuantifiers(bsd,d,r2);
+	}
 	if (dep==NODEPENDENCY)
 	    return;
 	GraphNode gn1=(GraphNode) ruletonode.get(r1);
@@ -138,10 +147,17 @@ class ModelRuleDependence {
 	    return NODEPENDENCY;
     }
 
-    private int checkQuantifiers(Descriptor d, Quantifiers qs) {
+    private int checkQuantifiers(SetDescriptor bsd, Descriptor d, Quantifiers qs) {
 	for (int i=0;i<qs.numQuantifiers();i++) {
 	    Quantifier q=qs.getQuantifier(i);
-	    if (q.getRequiredDescriptors().contains(d))
+	    if (q instanceof SetQuantifier&&
+		d instanceof SetDescriptor) {
+		SetQuantifier sq=(SetQuantifier)q;
+		SetDescriptor sd=(SetDescriptor)d;
+		if (sq.getSet().isSubset(sd)&&
+		    ((bsd==null)||!bsd.isSubset(sq.getSet())))
+		    return NORMDEPENDENCY;
+	    } else if (q.getRequiredDescriptors().contains(d))
 		return NORMDEPENDENCY;
 	}
 	return NODEPENDENCY;
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 2364436..0dadae2 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -44,7 +44,8 @@ public class OpExpr extends Expr {
 
     public Set getfunctions() {
 	Set leftfunctions=left.getfunctions();
-	Set rightfunctions=right.getfunctions();
+	Set rightfunctions=null;
+	if (right!=null) rightfunctions=right.getfunctions();
 	if (leftfunctions!=null&&rightfunctions!=null) {
 	    HashSet functions=new HashSet();
 	    functions.addAll(leftfunctions);
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 7727567..32b4a1b 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -256,6 +256,7 @@ public class Termination {
 
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
+		    System.out.println("Checking "+gn.getTextLabel()+" --> "+gn2.getTextLabel());
 		    if (AbstractInterferes.interferes(ar,cons)||
 			abstractinterferes.interferes(ar,dp)) {
 			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
@@ -1114,4 +1115,42 @@ public class Termination {
 	}
 	return true;
     }
+
+    public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+	if (mutualexclusive(sd1,sd2)||
+	    mutualexclusive(sd2,sd1))
+	    return true;
+	else
+	    return false;
+    }
+
+    private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+	Vector rules=state.vRules;
+	for(int i=0;i<rules.size();i++) {
+	    Rule r=(Rule)rules.get(i);
+	    if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
+		/* Rule may add items to sd1 */
+		SetInclusion si=(SetInclusion)r.getInclusion();
+		Expr ve=si.getExpr();
+		DNFRule drule=r.getDNFGuardExpr();
+		for(int j=0;j<drule.size();j++) {
+		    RuleConjunction rconj=drule.get(j);
+		    boolean containsexclusion=false;
+		    for (int k=0;k<rconj.size();k++) {
+			DNFExpr dexpr=rconj.get(k);
+			if (dexpr.getNegation()&&
+			    dexpr.getExpr() instanceof ElementOfExpr&&
+			    ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
+			    SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
+			    if (sd.isSubset(sd2))
+				containsexclusion=true;
+			}
+		    }
+		    if (!containsexclusion)
+			return false;
+		}
+	    }
+	}
+	return true;
+    }
 }