X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FConcreteInterferes.java;h=ddc2e0d465df61fa70406d070a091b2ef50f4dde;hb=d080c822cf26b5a8d922966fa123466bc49831ba;hp=af193f7ec4dc7df0ab1d396633a7ef8249ff7e5f;hpb=f4d787b23a126c58eec51c860f2b3d3bf8de7569;p=repair.git

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index af193f7..ddc2e0d 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -1,5 +1,6 @@
 package MCC.IR;
 import java.util.*;
+import MCC.Compiler;
 
 public class ConcreteInterferes {
     Termination termination;
@@ -8,31 +9,229 @@ public class ConcreteInterferes {
 	this.termination=t;
     }
 
+    /** 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 interferesinclusion(UpdateNode un, Updates update, Rule r) {
+    public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+
+	// A rule that adds something to a set can't be falsified by
+	// an update that is only performed if the set is empty
+        if (!initialinterferes(mun,r,satisfy))
+	    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);
+		//Abstract updates don't have concrete interference1
+		if (update.isAbstract())
+		    continue;
+
+		DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
+		Descriptor updated_des=update.getDescriptor();
+		assert updated_des!=null;
+
+		/* Test to see if the update only effects new
+		   objects and we're only testing for falsifying
+		   model definition rules. */
+
+		if ((!satisfy)&&updateonlytonewobject(mun,un,update))
+		    continue;
+
+
+		// See if the update interferes with the inclusion
+		// condition for the rule
+		if (r.getInclusion().usesDescriptor(updated_des)) {
+		    boolean ok=false;
+
+		    /* If the update is for this rule, and the effect
+                       is the intended effect, and the update only
+                       effects one binding, then the abstract repair
+                       node already models the action of this
+                       update. */
+
+		    if ((un.getRule()==r)&&
+			(((mun.op==MultUpdateNode.ADD)&&satisfy)
+			 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+			 ||(mun.op==MultUpdateNode.MODIFY))) {
+			Inclusion inclusion=r.getInclusion();
+			if (inclusion instanceof RelationInclusion) {
+			    RelationInclusion ri=(RelationInclusion)inclusion;
+			    if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
+				(!testdisjoint(update,r,ri.getRightExpr())))
+				ok=true;
+			} else if (inclusion instanceof SetInclusion) {
+			    SetInclusion si=(SetInclusion)inclusion;
+			    if (!testdisjoint(update,r,si.getExpr()))
+				ok=true;
+			} else throw new Error();
+		    }
+
+		    if ((un.getRule()==r)&&
+			((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
+			modifiesremoves(mun,un,r)) {
+			Inclusion inclusion=r.getInclusion();
+			if (inclusion instanceof RelationInclusion) {
+			    RelationInclusion ri=(RelationInclusion)inclusion;
+			    if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
+				(!testdisjoint(update,r,ri.getRightExpr())))
+				ok=true;	 /* Update is specific to
+						    given binding of the rule,
+						    and adds are only performed
+						    if the removal is desired or
+						    the tuple doesn't exist.*/
+			}
+		    }
+
+		    if (!ok) {
+			if (satisfy) {
+			    /** Check to see if the update definitely falsifies r, thus
+			     * can't accidentally satisfy it r. */
+			    if (interferesinclusion(un, update, r)) {
+                                if (Compiler.DEBUGGRAPH)
+                                    System.out.println("CASE 1");
+				return true;
+                            }
+			} else {
+                            if (Compiler.DEBUGGRAPH)
+                                System.out.println("CASE 2");
+
+                            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 ((un.getRule()==r)&&
+			    (((mun.op==MultUpdateNode.ADD)&&satisfy)
+			     ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+			     ||(mun.op==MultUpdateNode.MODIFY))) {
+			    if (!testdisjoint(update,r,dexpr.getExpr()))
+				continue; /* Update is specific to
+                                             given binding of the
+                                             rule, and effect is the
+                                             intended one, so we're
+                                             okay */
+			}
+			if ((un.getRule()==r)&&
+			    ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
+			    modifiesremoves(mun,un,r)) {
+			    if (!testdisjoint(update,r,dexpr.getExpr()))
+				continue; /* Update is specific to
+                                             given binding of the
+                                             rule, and adds are only
+                                             performed if the removal
+                                             is desired or the tuple
+                                             doesn't exist.*/
+			}
+
+			if (interferes(update,dexpr)) {
+                            if (Compiler.DEBUGGRAPH)
+                                System.out.println("CASE 3");
+
+                            return true;
+                        }
+		    }
+		}
+	    }
+	}
+	return false;
+    }
+
+
+    static private boolean modifiesremoves(MultUpdateNode mun,UpdateNode un, Rule r) {
+	AbstractRepair ar=mun.getRepair();
+	boolean inverted=ar.getPredicate().getPredicate().inverted();
+
+	if (ar.getType()!=AbstractRepair.MODIFYRELATION)
+	    return false;
+	RelationInclusion ri=(RelationInclusion)r.getInclusion();
+	Expr e=inverted?ri.getRightExpr():ri.getLeftExpr();
+	while(e instanceof CastExpr) {
+	    e=((CastExpr)e).getExpr();
+	}
+	if (!(e instanceof VarExpr))
+	    return false;
+	VarExpr ve=(VarExpr)e;
+	if (ve.isValue())
+	    return false;
+	return true;
+    }
+
+    static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
+	AbstractRepair ar=mun.getRepair();
+	if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
+	    for(int i=0;i<un.numUpdates();i++) {
+		Updates u=un.getUpdate(i);
+		if (u.getType()==Updates.POSITION&&
+		    ar.isNewObject(u.getRightPos()==0)) {
+		    Expr newleftexpr=u.getLeftExpr();
+		    Expr leftexpr=updates.getLeftExpr();
+		    boolean foundfield=false;
+		    while(true) {
+			if (leftexpr.equals(null,newleftexpr)) {
+			    if (foundfield)
+				return true;
+			    else
+				break;
+			} else if (leftexpr instanceof DotExpr) {
+			    if (!foundfield) {
+				foundfield=true;
+			    } else {
+				if (((DotExpr)leftexpr).isPtr())
+				    break; //if its not a pointer, we're still in the structure
+			    }
+			    leftexpr=((DotExpr)leftexpr).getExpr();
+			} else if (leftexpr instanceof CastExpr) {
+			    leftexpr=((CastExpr)leftexpr).getExpr();
+			} else
+			    break;
+		    }
+		}
+	    }
+
+	return false;
+    }
+
+    /** This method tries to show that if the Update update from the
+     *  UpdateNode un changes the value of the inclusion constraint
+     * that it falsifies the guard of model definition rule. */
+
+    static private 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()))
+	    if (ri.getLeftExpr().usesDescriptor(updated_des)
+		&&searchinterfere(un,update,r,ri.getLeftExpr()))
 		return true;
-	    if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
+	    if (ri.getRightExpr().usesDescriptor(updated_des)
+		&&searchinterfere(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()))
+	    if (si.getExpr().usesDescriptor(updated_des)
+		&&searchinterfere(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) {
+    /** This method finds all instances of a field or global that an
+     * update may modify, and builds a variable correspondance */
+
+    static private boolean searchinterfere(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();
@@ -64,7 +263,10 @@ public class ConcreteInterferes {
 	return false;
     }
 
-    static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
+    /** This method tries to show that if dvd=uvd, then the update un
+     *  must falsify the rule r. */
+
+    static private boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
 	DNFRule negrule=r.getDNFNegGuardExpr();
 	HashMap remap=new HashMap();
 	remap.put(dvd,uvd);
@@ -81,7 +283,7 @@ public class ConcreteInterferes {
 
 		    boolean varok=true;
 		    Set vars=rexpr.freeVars();
-		    if (vars!=null) 
+		    if (vars!=null)
 			for(Iterator it=vars.iterator();it.hasNext();) {
 			    VarDescriptor vd=(VarDescriptor) it.next();
 			    if (!vd.isGlobal()) {
@@ -92,12 +294,10 @@ public class ConcreteInterferes {
 				}
 			    }
 			}
-		    
+
 		    if (!varok)
 			continue;
 
-
-
 		    Opcode op=expr.getOpcode();
 		    op=Opcode.translateOpcode(dexpr.getNegation(),op);
 
@@ -131,9 +331,9 @@ public class ConcreteInterferes {
 				    rexpr.equals(remap,update.getRightExpr())) {
 				    match=true;
 				    break;
-				}				    
+				}
 			    }
-			} 
+			}
 		    }
 		    if (!match) {
 			good=false;
@@ -151,90 +351,25 @@ public class ConcreteInterferes {
 	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. */
+    /** This method checks whether the update effects only the
+     *  intended binding for the model definition rule. */
 
-    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();
-		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 (r.getInclusion().usesDescriptor(updated_des)) {
-			boolean ok=false;
-			if ((un.getRule()==r)&&
-			    (((mun.op==MultUpdateNode.ADD)&&satisfy)
-			     ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
-			     ||(mun.op==MultUpdateNode.MODIFY))) {
-			    Inclusion inclusion=r.getInclusion();
-			    if (inclusion instanceof RelationInclusion) {
-				RelationInclusion ri=(RelationInclusion)inclusion;
-				if ((!interferes(update,r,ri.getLeftExpr()))&&
-				    (!interferes(update,r,ri.getRightExpr())))
-				    ok=true;
-			    } else if (inclusion instanceof SetInclusion) {
-				SetInclusion si=(SetInclusion)inclusion;
-				if (!interferes(update,r,si.getExpr()))
-				    ok=true;
-			    } else throw new Error();
-			}
-			if (!ok) {
-			    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 ((un.getRule()==r)&&
-				(((mun.op==MultUpdateNode.ADD)&&satisfy)
-				 ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
-				 ||(mun.op==MultUpdateNode.MODIFY))) {
-				if (!interferes(update,r,dexpr.getExpr()))
-				    continue; /* unique state - we're okay */
-			    }
-			    if (interferes(un,update, r,dexpr))
-				return true;
-			}
-		    }
-		}
-	    }
-	}
-	return false;
-    }
-
-    private boolean interferes(Updates u, Rule r, Expr e) {
+    private boolean testdisjoint(Updates u, Rule r, Expr e) {
+	// find all exprs that may be be effected by update
 	Set exprs=e.useDescriptor(u.getDescriptor());
 	for(Iterator eit=exprs.iterator();eit.hasNext();) {
 	    Expr e2=(Expr)eit.next();
-	    if (mayinterfere(u,r,e2))
+	    if (testdisjointness(u,r,e2))
 		return true;
 	}
 	return false;
     }
 
-    private boolean mayinterfere(Updates u, Rule r, Expr e) {
+    /** This method tries to show that the modification only effects
+     * one binding of the model definition rule, and thus has no
+     * unintended side effects. */
+
+    private boolean testdisjointness(Updates u, Rule r, Expr e) {
 	// Note: rule of u must be r
 
 	Expr update_e=u.getLeftExpr();
@@ -244,6 +379,8 @@ public class ConcreteInterferes {
 	    return false; /* Can't accidentally interfere with other bindings if there aren't any! */
 
 	boolean firstfield=true;
+
+
 	while(true) {
 	    if (update_e instanceof CastExpr)
 		update_e=((CastExpr)update_e).getExpr();
@@ -252,7 +389,7 @@ public class ConcreteInterferes {
 	    else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
 		DotExpr de1=(DotExpr)update_e;
 		DotExpr de2=(DotExpr)e;
-		if (de1.isValue()&&!firstfield)
+		if (de1.isValue(null)&&!firstfield)
 		    return true; /* Could have aliasing from this */
 		if (de1.getField()!=de2.getField())
 		    return true; /* Different fields: not comparible */
@@ -285,9 +422,10 @@ public class ConcreteInterferes {
 		return true;
 	    } else return true;
 	}
-
     }
 
+    /** This method returns the quantifier that defines the quantifier
+     * variable vd. */
     static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
 	for (int i=0;i<qs.numQuantifiers();i++) {
 	    Quantifier q=qs.getQuantifier(i);
@@ -307,60 +445,79 @@ public class ConcreteInterferes {
 	}
 	return null;
     }
-    
-    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;
+    /** This function checks to see if an update is only performed if
+     * a given set (or image set produced by a relation) is empty, and
+     * the algorithm is computing whether the update may falsify a
+     * rule that adds something to the set */
 
+    private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	AbstractRepair ar=mun.getRepair();
+	if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET)) {
+	    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;
+	    Opcode op=Opcode.translateOpcode(negated,ep.getOp());
 
+	    if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
+		((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
+		((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
+		((op==Opcode.GE)&&(ep.rightSize()==1))) //(>=1)
+		return false;
+	} else if ((!satisfy)&&(ar!=null)&&(ar.getType()==AbstractRepair.ADDTORELATION)) {
+	    /* This test is for image sets of relations. */
+	    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.GT)&&(ep.rightSize()==0)&&!negated)
-	    return false;
-	if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
-	    return false;
+	    Opcode op=Opcode.translateOpcode(negated,ep.getOp());
+ 	    if (!(((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
+		((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
+		((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
+		((op==Opcode.GE)&&(ep.rightSize()==1)))) //(>=1)
+		return true;
 
-	if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
-	    return false;
-	if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
+	    RelationInclusion ri=(RelationInclusion)r.getInclusion();
+	    Expr tmpve=ep.inverted()?ri.getRightExpr():ri.getLeftExpr();
+	    if (!(tmpve instanceof VarExpr))
+		return true;
+	    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);
+		    //Abstract updates don't have concrete interference1
+		    if (update.isAbstract())
+			continue;
+		    if (testdisjoint(update, r, r.getGuardExpr()))
+			return true;
+		}
+	    }
 	    return false;
-	
+   	}
 	return true;
-
-	
     }
 
-    static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
+    static private boolean interferes(Updates update, DNFExpr dexpr) {
 	Descriptor descriptor=update.getDescriptor();
+	/* If the DNFExpr expr doesn't use the updated descriptor,
+	   there is no interference. */
 	if (!dexpr.getExpr().usesDescriptor(descriptor))
 	    return false;
-	    
-	/* We need to pair the variables */
+
 	if (update.isExpr()) {
+	    /* We need to pair the variables */
 	    Set vars=update.getRightExpr().freeVars();
 	    Opcode op1=update.getOpcode();
 	    Expr lexpr1=update.getLeftExpr();
@@ -369,8 +526,8 @@ public class ConcreteInterferes {
 	    if (vars!=null)
 		for(Iterator it=vars.iterator();it.hasNext();) {
 		    VarDescriptor vd=(VarDescriptor) it.next();
+		    /* VarDescriptor isn't a global */
 		    if (!vd.isGlobal()) {
-			/* VarDescriptor isn't a global */
 			if (update.getVar()!=vd) {
 			    good=false;
 			    break;
@@ -384,24 +541,21 @@ public class ConcreteInterferes {
 		Opcode op2=expr.getOpcode();
 		op2=Opcode.translateOpcode(dexpr.getNegation(),op2);
 
-		good=true;
-		vars=rexpr2.freeVars();
 		VarDescriptor leftdescriptor=null;
-		if (lexpr2 instanceof VarExpr)
-		    leftdescriptor=((VarExpr)lexpr2).getVar();
-		else if (lexpr2 instanceof DotExpr) {
+		{
 		    Expr e=lexpr2;
-		    do {
+		    while(!(e instanceof VarExpr)) {
 			for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
 			if (e instanceof VarExpr)
 			    break;
 			if (e instanceof CastExpr)
 			    e=((CastExpr)e).getExpr();
 			else throw new Error("Bad Expr Type:"+e.name());
-		    } while (true);
+		    }
 		    leftdescriptor=((VarExpr)e).getVar();
-		} else throw new Error("Bad Expr");
-		
+		}
+
+		vars=rexpr2.freeVars();
 		if (vars!=null)
 		    for(Iterator it=vars.iterator();it.hasNext();) {
 			VarDescriptor vd=(VarDescriptor) it.next();
@@ -413,6 +567,8 @@ public class ConcreteInterferes {
 			    }
 			}
 		    }
+
+
 		if (good) {
 		    HashMap remap=new HashMap();
 		    remap.put(update.getVar(),leftdescriptor);