X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FAbstractInterferes.java;h=5b24327abbcf92503307e73c48a4b7ef20c0c97a;hp=569485c7fc1cbc73b587c10b57e4cd5040109672;hb=6e6caa157ea20e565ea92786ef266c952e6f39b3;hpb=cd8c06f13c3d628b15f745790e3eeac2891c5736

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 569485c..5b24327 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -1,6 +1,55 @@
 package MCC.IR;
 
 class AbstractInterferes {
+    static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
+	boolean mayadd=false;
+	boolean mayremove=false;
+	switch (ar.getType()) {
+	case AbstractRepair.ADDTOSET:
+	case AbstractRepair.ADDTORELATION:
+	    if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+		return true;
+	    mayadd=true;
+	    break;
+	case AbstractRepair.REMOVEFROMSET:
+	case AbstractRepair.REMOVEFROMRELATION:
+	    if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+		return true;
+	    mayremove=true;
+	    break;
+	case AbstractRepair.MODIFYRELATION:
+	    if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+		return true;
+	    if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+		return true;
+	    mayadd=true;
+	    mayremove=true;
+	break;
+	default:
+	    throw new Error("Unrecognized Abstract Repair");
+	}
+	DNFRule drule=null;
+	if (satisfy)
+	    drule=r.getDNFGuardExpr();
+	else
+	    drule=r.getDNFNegGuardExpr();
+	
+	for(int i=0;i<drule.size();i++) {
+	    RuleConjunction rconj=drule.get(i);
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		Expr expr=dexpr.getExpr();
+		if (expr.usesDescriptor(ar.getDescriptor())) {
+		    /* Need to check */
+		    if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
+			return true;
+		}
+	    }
+	}
+	return false;
+    }
+
+
     static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
 	if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
 	    ((ar.getDescriptor() instanceof SetDescriptor)||
@@ -50,7 +99,24 @@ class AbstractInterferes {
 		    return false;
 	    } 
 	}
-	/* This if handles all the c comparisons in the paper */
+
+	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		(neg2&&(op2==Opcode.NE)&&(size2==0))||
+		(!neg2&&(op2==Opcode.GE))||
+		(!neg2&&(op2==Opcode.GT))||
+		(neg2&&(op2==Opcode.LE))||
+		(neg2&&(op2==Opcode.LT)))
+		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)&&
 	    (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
@@ -63,8 +129,8 @@ class AbstractInterferes {
 	    boolean neg2=dp.isNegated();
 	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
-	    if ((neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
-		(!neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+	    if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
+		(neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
 		int size1a=0;
 		if (neg1) {
 		    if((op1==Opcode.EQ)||(op1==Opcode.GE))
@@ -91,8 +157,37 @@ class AbstractInterferes {
 		    (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
 		    (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
 		    return false;
-	    } 
+	    }
 	}
+
+	if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		(neg2&&(op2==Opcode.NE)&&(size2==0))||
+		(neg2&&(op2==Opcode.GE))||
+		(neg2&&(op2==Opcode.GT))||
+		(!neg2&&(op2==Opcode.LE))||
+		(!neg2&&(op2==Opcode.LT)))
+		return false;
+	    
+	}
+	if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+	    (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==false))
+	    return false; /* Could only satisfy this predicate */
+
+	if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
+	    (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==true))
+	    return false; /* Could only satisfy this predicate */
+	  
 	return true;
     }
 
@@ -113,6 +208,8 @@ class AbstractInterferes {
 	    {
 		if ((!neg2&&(op2==Opcode.GE))||
 		    (!neg2&&(op2==Opcode.GT))||
+		    (neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		    (!neg2&&(op2==Opcode.NE)&&(size2==0))||
 		    (neg2&&(op2==Opcode.LE))||
 		    (neg2&&(op2==Opcode.LT)))
 		    return false;
@@ -129,15 +226,29 @@ class AbstractInterferes {
 	    {
 		if ((neg2&&(op2==Opcode.GE))||
 		    (neg2&&(op2==Opcode.GT))||
+		    (!neg2&&(op2==Opcode.EQ)&&(size2==0))||
+		    (neg2&&(op2==Opcode.NE)&&(size2==0))||
 		    (!neg2&&(op2==Opcode.LE))||
 		    (!neg2&&(op2==Opcode.LT)))
 		    return false;
 	    } 
 	}
+	if ((des==dp.getPredicate().getDescriptor())&&
+	    satisfy&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==false))
+	    return false; /* Could only satisfy this predicate */
+
+	if ((des==dp.getPredicate().getDescriptor())&&
+	    (!satisfy)&&
+	    (dp.getPredicate() instanceof InclusionPredicate)&&
+	    (dp.isNegated()==true))
+	    return false; /* Could only satisfy this predicate */
+
 	return true;
     }
 
-    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+    static public boolean interferesquantifier(Descriptor des, boolean satisfy, Quantifiers r, boolean satisfyrule) {
 	for(int i=0;i<r.numQuantifiers();i++) {
 	    Quantifier q=r.getQuantifier(i);
 	    if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
@@ -148,6 +259,22 @@ class AbstractInterferes {
 		    return true;
 	    } else throw new Error("Unrecognized Quantifier");
 	}
+	return false;
+    }
+
+    static public boolean interferes(AbstractRepair ar, Quantifiers q) {
+	if (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)
+	    return interferesquantifier(ar.getDescriptor(),true,q,true);
+	return false;
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Quantifiers q) {
+	return interferesquantifier(des, satisfy, q,true);
+    }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+	if (interferesquantifier(des,satisfy,r,satisfyrule))
+	    return true;
 	/* Scan DNF form */
 	DNFRule drule=r.getDNFGuardExpr();
 	for(int i=0;i<drule.size();i++) {