X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FConcreteInterferes.java;h=eefde7f2f733ad659d9665426cf6625899178330;hp=e6718a69eefbf4f6b975b9cd1780709ff38a9328;hb=5206adad89e8c25fe06bf649840920337f1c2ad1;hpb=ce993d16a8b0057b8d5881be15aed42926e54783

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index e6718a6..eefde7f 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -1,23 +1,349 @@
 package MCC.IR;
+import java.util.*;
 
 class ConcreteInterferes {
+
+    static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
+	Descriptor updated_des=update.getDescriptor();
+	Inclusion inclusion=r.getInclusion();
+	if (inclusion instanceof RelationInclusion) {
+	    RelationInclusion ri=(RelationInclusion)inclusion;
+	    if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
+		return true;
+	    if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
+		return true;
+	} else if (inclusion instanceof SetInclusion) {
+	    SetInclusion si=(SetInclusion)inclusion;
+	    if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
+		return true;
+	} else throw new Error();
+	return false;
+    }
+
+    static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
+	Descriptor updated_des=update.getDescriptor();
+	if (updated_des instanceof FieldDescriptor) {
+	    /* Build variable correspondance */
+	    HashSet set=new HashSet();
+	    inclusionexpr.findmatch(updated_des,set);
+	    
+	    for(Iterator matchit=set.iterator();matchit.hasNext();) {
+		DotExpr dotexpr=(DotExpr)matchit.next();
+		DotExpr updateexpr=(DotExpr)update.getLeftExpr();
+		while(true) {
+		    if (dotexpr.getField()!=updateexpr.getField())
+			return true;
+		    Expr de=dotexpr.getExpr();
+		    Expr ue=updateexpr.getExpr();
+		    if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
+			dotexpr=(DotExpr)de;
+			updateexpr=(DotExpr)ue;
+		    } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
+			VarDescriptor dvd=((VarExpr)de).getVar();
+			VarDescriptor uvd=((VarExpr)ue).getVar();
+			if (interferesinclusion(un,r,dvd,uvd))
+			    return true;
+			else
+			    break;
+		    } else
+			return true;
+		}
+	    }
+	} else if (updated_des instanceof VarDescriptor) {
+	    /* We have a VarDescriptor - no correspondance necessary */
+	    VarDescriptor vd=(VarDescriptor)updated_des;
+	    if (interferesinclusion(un,r,vd,vd))
+		return true;
+	} else throw new Error();
+	return false;
+    }
+
+    static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
+	DNFRule negrule=r.getDNFNegGuardExpr();
+	HashMap remap=new HashMap();
+	remap.put(dvd,uvd);
+
+	for(int i=0;i<negrule.size();i++) {
+	    RuleConjunction rconj=negrule.get(i);
+	    boolean good=true;
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		if (dexpr.getExpr() instanceof OpExpr) {
+		    OpExpr expr=(OpExpr)dexpr.getExpr();
+		    Expr lexpr=expr.getLeftExpr();
+		    Expr rexpr=expr.getRightExpr();
+
+		    boolean varok=true;
+		    Set vars=rexpr.freeVars();
+		    if (vars!=null) 
+			for(Iterator it=vars.iterator();it.hasNext();) {
+			    VarDescriptor vd=(VarDescriptor) it.next();
+			    if (!vd.isGlobal()) {
+				/* VarDescriptor isn't a global */
+				if (dvd!=vd) {
+				    varok=false;
+				    break;
+				}
+			    }
+			}
+		    
+		    if (!varok)
+			continue;
+
+
+
+		    Opcode op=expr.getOpcode();
+
+		    if (dexpr.getNegation()) {
+			/* remove negation through opcode translation */
+			if (op==Opcode.GT)
+			    op=Opcode.LE;
+			else if (op==Opcode.GE)
+			    op=Opcode.LT;
+			else if (op==Opcode.EQ)
+			    op=Opcode.NE;
+			else if (op==Opcode.NE)
+			    op=Opcode.EQ;
+			else if (op==Opcode.LT)
+			    op=Opcode.GE;
+			else if (op==Opcode.LE)
+			    op=Opcode.GT;
+		    }
+		    boolean match=false;
+		    for(int k=0;k<un.numUpdates();k++) {
+			Updates update=un.getUpdate(k);
+			if(update.isExpr()) {
+			    Set uvars=update.getRightExpr().freeVars();
+			    boolean freevarok=true;
+			    if (uvars!=null)
+			    for(Iterator it=uvars.iterator();it.hasNext();) {
+				VarDescriptor vd=(VarDescriptor) it.next();
+				if (!vd.isGlobal()) {
+				    /* VarDescriptor isn't a global */
+				    if (uvd!=vd) {
+					freevarok=false;
+					break;
+				    }
+				}
+			    }
+			    if (!freevarok)
+				continue;
+
+			    Opcode op2=update.getOpcode();
+			    if ((op2==op)||
+				((op2==Opcode.GT)&&(op==Opcode.GE))||
+				((op2==Opcode.LT)&&(op==Opcode.LE))||
+				((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
+				/* Operations match*/
+				if (lexpr.equals(remap,update.getLeftExpr())&&
+				    rexpr.equals(remap,update.getRightExpr())) {
+				    match=true;
+				    break;
+				}				    
+			    }
+			} 
+		    }
+		    if (!match) {
+			good=false;
+			break;
+		    }
+		} else {
+		    /* TODO: Check to see if there is an abstract repair */
+		    good=false;
+		    break; /* try next conjunction */
+		}
+	    }
+	    if (good)
+		return false;
+	}
+	return true;
+    }
+
+    /** Returns true if the data structure updates performed by mun may increase (or decrease if satisfy=false)
+     * the scope of the model definition rule r. */
+
     static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
+	    return false;
 	for(int i=0;i<mun.numUpdates();i++) {
 	    UpdateNode un=mun.getUpdate(i);
 	    for (int j=0;j<un.numUpdates();j++) {
 		Updates update=un.getUpdate(j);
+		
 		DNFRule drule=r.getDNFGuardExpr();
-		for(int k=0;k<drule.size();k++) {
-		    RuleConjunction rconj=drule.get(k);
-		    for(int l=0;l<rconj.size();l++) {
-			DNFExpr dexpr=rconj.get(l);
-			/* See if update interfers w/ dexpr */
-			Descriptor updatedes=update.getDescriptor();
-			
+		if (satisfy)
+		    drule=r.getDNFNegGuardExpr();
+
+
+		if (!update.isAbstract()) {
+		    Descriptor updated_des=update.getDescriptor();
+		    assert updated_des!=null;
+		    /* Update is local to this rule, and the effect is intentional */
+		    /* If we're adding something, a side effect could be to falsify some other binding
+		       If we're removing something, there is no similar side effect */
+
+		    /* ISSUE: Rules need to be updated if we allow concrete expression of the form x.f.g */
+		    if ((un.getRule()==r)&&
+			(((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
+			(r.numQuantifiers()==1)&&
+			(r.getQuantifier(0) instanceof SetQuantifier)&&
+			update.isField()&&
+			(((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
+			((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
+			continue;
+
+    		    if ((un.getRule()==r)&&
+			(((mun.op==MultUpdateNode.ADD)&&satisfy)||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)||(mun.op==MultUpdateNode.MODIFY))&&
+			(r.numQuantifiers()==0))
+			continue;
+		    
+
+		    if (r.getInclusion().usesDescriptor(updated_des)) {
+			if (satisfy) {
+			    if (interferesinclusion(un, update, r))
+			    return true;
+			} else
+			    return true; /* Interferes with inclusion condition */
+		    }
+		    
+		    for(int k=0;k<drule.size();k++) {
+			RuleConjunction rconj=drule.get(k);
+			for(int l=0;l<rconj.size();l++) {
+
+
+			    DNFExpr dexpr=rconj.get(l);
+			    /* See if update interferes w/ dexpr */
+			    if (interferes(un,update, r,dexpr))
+				return true;
+			}
 		    }
 		}
 	    }
 	}
 	return false;
     }
+
+    static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	AbstractRepair ar=mun.getRepair();
+	if (satisfy)
+	    return true;
+	if (ar==null)
+	    return true;
+	if (ar.getType()!=AbstractRepair.ADDTOSET)
+	    return true;
+	//	if (mun.op!=MultUpdateNode.ADD)  (Redundant)
+	//    return true;
+	if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
+	    return true;
+	boolean negated=ar.getPredicate().isNegated();
+	Predicate p=ar.getPredicate().getPredicate();
+	if (!(p instanceof ExprPredicate))
+	    return true;
+	ExprPredicate ep=(ExprPredicate)p;
+	if (ep.getType()!=ExprPredicate.SIZE)
+	    return true;
+	if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
+	    return false;
+
+	if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
+	    return false;
+
+
+
+	if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
+	    return false;
+
+	if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
+	    return false;
+	if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
+	    return false;
+	
+	return true;
+
+	
+    }
+
+    static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
+	Descriptor descriptor=update.getDescriptor();
+	if (!dexpr.getExpr().usesDescriptor(descriptor))
+	    return false;
+	    
+	/* We need to pair the variables */
+	if (update.isExpr()) {
+	    Set vars=update.getRightExpr().freeVars();
+	    Opcode op1=update.getOpcode();
+	    Expr lexpr1=update.getLeftExpr();
+	    Expr rexpr1=update.getRightExpr();
+	    boolean good=true;
+	    if (vars!=null)
+		for(Iterator it=vars.iterator();it.hasNext();) {
+		    VarDescriptor vd=(VarDescriptor) it.next();
+		    if (!vd.isGlobal()) {
+			/* VarDescriptor isn't a global */
+			if (update.getVar()!=vd) {
+			    good=false;
+			    break;
+			}
+		    }
+		}
+	    if (good&&(dexpr.getExpr() instanceof OpExpr)) {
+		OpExpr expr=(OpExpr)dexpr.getExpr();
+		Expr lexpr2=expr.getLeftExpr();
+		Expr rexpr2=expr.getRightExpr();
+		Opcode op2=expr.getOpcode();
+		if (dexpr.getNegation()) {
+		    /* remove negation through opcode translation */
+		    if (op2==Opcode.GT)
+			op2=Opcode.LE;
+		    else if (op2==Opcode.GE)
+			op2=Opcode.LT;
+		    else if (op2==Opcode.EQ)
+			op2=Opcode.NE;
+		    else if (op2==Opcode.NE)
+			op2=Opcode.EQ;
+		    else if (op2==Opcode.LT)
+			op2=Opcode.GE;
+		    else if (op2==Opcode.LE)
+			op2=Opcode.GT;
+		}
+		good=true;
+		vars=rexpr2.freeVars();
+		VarDescriptor leftdescriptor=null;
+		if (lexpr2 instanceof VarExpr)
+		    leftdescriptor=((VarExpr)lexpr2).getVar();
+		else if (lexpr2 instanceof DotExpr) {
+		    Expr e=lexpr2;
+		    for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+		    leftdescriptor=((VarExpr)e).getVar();
+		} else throw new Error("Bad Expr");
+		
+		if (vars!=null)
+		    for(Iterator it=vars.iterator();it.hasNext();) {
+			VarDescriptor vd=(VarDescriptor) it.next();
+			if (!vd.isGlobal()) {
+			    /* VarDescriptor isn't a global */
+			    if (leftdescriptor!=vd) {
+				good=false;
+				break;
+			    }
+			}
+		    }
+		if (good) {
+		    HashMap remap=new HashMap();
+		    remap.put(update.getVar(),leftdescriptor);
+		    if ((op1==op2)&&
+			lexpr1.equals(remap,lexpr2)&&
+			rexpr1.equals(remap,rexpr2))
+			return false;
+		}
+	    }
+	}
+	return true;
+    }
 }