From 9918f5482edda50339844652d2a75e563af54ea9 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 10 Mar 2004 06:15:03 +0000
Subject: [PATCH] Added: Concrete Interference rule that falsify a rule that
 quantifies over a set can't remove the last element of the set.

Concrete Interference rule that updates that definitely falsify a rule can't modify
the inclusion condition causing a possible addition.

Intelligence in the GraphAnalysis package that computes must & cant remove sets.
Search through only unique combinations.
---
 .../MCC/IR/AbstractInterferes.java            |  49 +++++
 Repair/RepairCompiler/MCC/IR/CastExpr.java    |   4 +
 .../MCC/IR/ConcreteInterferes.java            | 200 +++++++++++++++--
 Repair/RepairCompiler/MCC/IR/DotExpr.java     |   8 +
 Repair/RepairCompiler/MCC/IR/Expr.java        |   3 +
 .../RepairCompiler/MCC/IR/GraphAnalysis.java  | 203 ++++++++++++++----
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  58 +++--
 .../MCC/IR/RepairGenerator.java               |  11 +-
 Repair/RepairCompiler/MCC/IR/Termination.java |  56 ++++-
 Repair/RepairCompiler/MCC/Runtime/redblack.c  |  17 +-
 10 files changed, 525 insertions(+), 84 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 5b24327..592b9d4 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -1,4 +1,5 @@
 package MCC.IR;
+import java.util.*;
 
 class AbstractInterferes {
     static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
@@ -191,6 +192,54 @@ class AbstractInterferes {
 	return true;
     }
 
+    static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
+	if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
+	    Rule r=sn.getRule();
+	    Set target=r.getInclusion().getTargetDescriptors();
+	    boolean match=false;
+	    for(int i=0;i<r.numQuantifiers();i++) {
+		Quantifier q=r.getQuantifier(i);
+		if (q instanceof SetQuantifier) {
+		    SetQuantifier sq=(SetQuantifier) q;
+		    if (target.contains(sq.getSet())) {
+			match=true;
+			break;
+		    }
+		}
+	    }
+	    if (match&&
+		sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
+		(dp.getPredicate() instanceof ExprPredicate)&&
+		(((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+		boolean neg=dp.isNegated();
+		Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
+		int size=((ExprPredicate)dp.getPredicate()).leftsize();
+		if (neg) {
+		    /* 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;
+		}
+		if ((op==Opcode.GE)&&
+		    ((size==0)||(size==1)))
+		    return false;
+		if ((op==Opcode.GT)&&
+		    (size==0))
+		    return false;
+	    }
+	}
+	return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
+    }
+
     static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
 	if ((des!=dp.getPredicate().getDescriptor()) &&
 	    ((des instanceof SetDescriptor)||
diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 88fde6d..c472ffa 100755
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -11,6 +11,10 @@ public class CastExpr extends Expr {
 	return expr.freeVars();
     }
 
+    public void findmatch(Descriptor d, Set s) {
+	expr.findmatch(d,s);
+    }
+
     public CastExpr(TypeDescriptor type, Expr expr) {
         this.type = type;
         this.expr = expr;
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index c711d82..2c7d59e 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -2,6 +2,163 @@ 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;
+    }
+
     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;
@@ -35,8 +192,13 @@ class ConcreteInterferes {
 			continue;
 
 
-		    if (r.getInclusion().usesDescriptor(updated_des))
-			return true; /* Interferes with inclusion condition */
+		    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);
@@ -113,16 +275,17 @@ class ConcreteInterferes {
 	    Expr lexpr1=update.getLeftExpr();
 	    Expr rexpr1=update.getRightExpr();
 	    boolean good=true;
-	    for(Iterator it=vars.iterator();it.hasNext();) {
-		VarDescriptor vd=(VarDescriptor) it.next();
-		if (un.getBinding(vd)!=null) {
-		    /* VarDescriptor isn't a global */
-		    if (update.getVar()!=vd) {
-			good=false;
-			break;
+	    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();
@@ -154,16 +317,17 @@ class ConcreteInterferes {
 		    leftdescriptor=((VarExpr)e).getVar();
 		} else throw new Error("Bad Expr");
 		
-		for(Iterator it=vars.iterator();it.hasNext();) {
-		    VarDescriptor vd=(VarDescriptor) it.next();
-		    if (un.getBinding(vd)!=null) {
-			/* VarDescriptor isn't a global */
-			if (leftdescriptor!=vd) {
-			    good=false;
-			    break;
+		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);
diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 38ee61a..08a5618 100755
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -12,6 +12,14 @@ public class DotExpr extends Expr {
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;
 
+    public void findmatch(Descriptor d, Set s) {
+	if (d==fd)
+	    s.add(this);
+	left.findmatch(d,s);
+	if (index!=null)
+	    index.findmatch(d,s);
+    }
+
     public Set freeVars() {
 	Set lset=left.freeVars();
 	Set iset=null;
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index ab7cbee..596c125 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -62,4 +62,7 @@ public abstract class Expr {
     public Set freeVars() {
 	return null;
     }
+
+    public void findmatch(Descriptor d, Set s) {
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3488a66..aebb865 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -15,46 +15,159 @@ public class GraphAnalysis {
     }
 
     public Set doAnalysis() {
-	HashSet nodes=new HashSet();
-	nodes.addAll(termination.conjunctions);
-	GraphNode.computeclosure(nodes,null);
-	Set cycles=GraphNode.findcycles(nodes);
-	Set couldremove=new HashSet();
-	couldremove.addAll(termination.conjunctions);
-	couldremove.addAll(termination.updatenodes);
-	couldremove.addAll(termination.consequencenodes);
-	couldremove.retainAll(cycles);
-	Vector constraints=termination.state.vConstraints;
-	for(int i=0;i<constraints.size();i++) {
-	    Constraint c=(Constraint)constraints.get(i);
-	    Set conjunctionset=(Set)termination.conjunctionmap.get(c);
-	    if (conjunctionset.size()==1)
-		couldremove.removeAll(conjunctionset);
-	}
+	HashSet cantremove=new HashSet();
+	HashSet mustremove=new HashSet();
+	cantremove.addAll(termination.scopenodes);
+	cantremove.addAll(termination.abstractrepair);
 
+	while(true) {
+	    boolean change=false;
+	    HashSet nodes=new HashSet();
+	    nodes.addAll(termination.conjunctions);
+	    nodes.removeAll(mustremove);
+	    GraphNode.computeclosure(nodes,mustremove);
+	    Set cycles=GraphNode.findcycles(nodes);
+	    Set couldremove=new HashSet();
+	    couldremove.addAll(termination.conjunctions);
+	    couldremove.addAll(termination.updatenodes);
+	    couldremove.addAll(termination.consequencenodes);
+	    couldremove.retainAll(cycles);
 
-	Vector couldremovevector=new Vector();
-	couldremovevector.addAll(couldremove);
-	Vector combination=new Vector();
 
-	while(true) {
-	    if (illegal(combination,couldremovevector))
-		break;
-	    Set combinationset=buildset(combination,couldremovevector);
-	    if (combinationset!=null) {
-		System.out.println("Checkabstract="+checkAbstract(combinationset));
-		System.out.println("Checkrepairs="+checkRepairs(combinationset));
-		System.out.println("Checkall="+checkAll(combinationset));
-		
-		if (checkAbstract(combinationset)==0&&
-		    checkRepairs(combinationset)==0&&
-		    checkAll(combinationset)==0) {
-		    return combinationset;
+	    /* Look for constraints which can only be satisfied one way */
+	    
+	    Vector constraints=termination.state.vConstraints;
+	    for(int i=0;i<constraints.size();i++) {
+		Constraint c=(Constraint)constraints.get(i);
+		Set conjunctionset=(Set)termination.conjunctionmap.get(c);
+		HashSet tmpset=new HashSet();
+		tmpset.addAll(conjunctionset);
+		tmpset.removeAll(mustremove);
+		if (tmpset.size()==1) {
+		    int oldsize=cantremove.size();
+		    cantremove.addAll(tmpset);
+		    if (cantremove.size()!=oldsize)
+			change=true;
 		}
 	    }
-	    increment(combination,couldremovevector);
+	    HashSet newset=new HashSet();
+	    for(Iterator cit=cantremove.iterator();cit.hasNext();) {
+		GraphNode gn=(GraphNode)cit.next();
+		boolean nomodify=true;
+		HashSet toremove=new HashSet();
+		if (termination.conjunctions.contains(gn)) {
+		    for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+			GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+			GraphNode gn2=e.getTarget();
+			TermNode tn2=(TermNode)gn2.getOwner();
+			if (tn2.getType()==TermNode.ABSTRACT) {
+			    AbstractRepair ar=tn2.getAbstract();
+			    if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+				nomodify=false;
+				break;
+			    }
+			    HashSet updateset=new HashSet();
+			    for(Iterator upit=gn2.edges();upit.hasNext();) {
+				GraphNode.Edge e2=(GraphNode.Edge)upit.next();
+				GraphNode gn3=e2.getTarget();
+				TermNode tn3=(TermNode)gn3.getOwner();
+				if (tn3.getType()==TermNode.UPDATE)
+				    updateset.add(gn3);
+			    }
+			    updateset.removeAll(mustremove);
+			    if (updateset.size()==1)
+				toremove.addAll(updateset);
+			}
+		    }
+		    if (nomodify) {
+			newset.addAll(toremove);
+		    }
+		}
+	    }
+	    {
+		int oldsize=cantremove.size();
+		cantremove.addAll(newset);
+		if (cantremove.size()!=oldsize)
+		    change=true;
+	    }
+
+	    /* Look for required actions for scope nodes */
+	    for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
+		GraphNode gn=(GraphNode)scopeit.next();
+		HashSet tmpset=new HashSet();
+		for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+		    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+		    tmpset.add(e.getTarget());
+		}
+		tmpset.removeAll(mustremove);
+		if (tmpset.size()==1) {
+		    int oldsize=cantremove.size();
+		    cantremove.addAll(tmpset);
+		    if (cantremove.size()!=oldsize)
+			change=true;
+		}
+	    }
+	    
+	    Set cycles2=GraphNode.findcycles(cantremove);
+	    for(Iterator it=cycles2.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		if (termination.conjunctions.contains(gn))
+		    return null; // Out of luck
+	    }
+	    
+	    
+	    for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		if (!cantremove.contains(gn)) {
+		    cantremove.add(gn);
+		    Set cycle=GraphNode.findcycles(cantremove);
+		    if (cycle.contains(gn)) {
+			if (!mustremove.contains(gn)) {
+			    change=true;
+			    mustremove.add(gn);
+			}
+		    }
+		    cantremove.remove(gn);
+		}
+	    }
+	    couldremove.removeAll(mustremove);
+	    couldremove.removeAll(cantremove);
+	    
+	    Vector couldremovevector=new Vector();
+	    couldremovevector.addAll(couldremove);
+	    Vector combination=new Vector();
+	    if(change)
+		continue; //recalculate
+
+	    System.out.println("Searching set of "+couldremove.size()+" nodes.");
+	    System.out.println("Eliminated "+mustremove.size()+" nodes");
+	    System.out.println("Searching following set:");
+	    for(Iterator it=couldremove.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		System.out.println(gn.getTextLabel());
+	    }
+	    
+	    
+	    while(true) {
+		if (illegal(combination,couldremovevector))
+		    break;
+		Set combinationset=buildset(combination,couldremovevector);
+		combinationset.addAll(mustremove);
+		if (combinationset!=null) {
+		    System.out.println("Checkabstract="+checkAbstract(combinationset));
+		    System.out.println("Checkrepairs="+checkRepairs(combinationset));
+		    System.out.println("Checkall="+checkAll(combinationset));
+		    
+		    if (checkAbstract(combinationset)==0&&
+			checkRepairs(combinationset)==0&&
+			checkAll(combinationset)==0) {
+			return combinationset;
+		    }
+		}
+		increment(combination,couldremovevector);
+	    }
+	    return null;
 	}
-	return null;
     }
 
     private static Set buildset(Vector combination, Vector couldremove) {
@@ -77,21 +190,31 @@ public class GraphAnalysis {
     }
     private static void increment(Vector combination, Vector couldremove) {
 	boolean incremented=false;
+	boolean forcereset=false;
 	for(int i=0;i<combination.size();i++) {
 	    int newindex=((Integer)combination.get(i)).intValue()+1;
-	    while(combination.contains(new Integer(newindex)))
-		newindex++;
-	    if (newindex==couldremove.size()) {
-		newindex=0;
-		combination.set(i,new Integer(newindex));
+	    if (newindex==couldremove.size()||forcereset) {
+		forcereset=false;
+		if ((i+1)==combination.size()) {
+		    newindex=1;
+		} else
+		    newindex=((Integer)combination.get(i+1)).intValue()+2;
+		for(int j=i;j>=0;j--) {
+		    combination.set(j,new Integer(newindex));
+		    newindex++;
+		}
+		if (newindex>couldremove.size())
+		    forcereset=true;
 	    } else {
 		incremented=true;
 		combination.set(i,new Integer(newindex));
 		break;
 	    }
 	}
-	if (incremented==false) /* Increase length */
+	if (incremented==false) /* Increase length */ {
 	    combination.add(new Integer(0));
+	    System.out.println("Expanding to :"+combination.size());
+	}
     }
 
     /* This function checks the graph as a whole for bad cycles */
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index e9b3f59..83d7257 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -8,6 +8,12 @@ public class OpExpr extends Expr {
     Expr right;
     Opcode opcode;
 
+    public void findmatch(Descriptor d, Set  s) {
+	left.findmatch(d,s);
+	if (right!=null)
+	    right.findmatch(d,s);
+    }
+
     public static boolean isInt(Expr e) {
 	if ((e instanceof IntegerLiteralExpr)||
 	    ((e instanceof OpExpr)&&(((OpExpr)e).getLeftExpr() instanceof IntegerLiteralExpr)))
@@ -168,38 +174,54 @@ public class OpExpr extends Expr {
 	if (left instanceof RelationExpr)
 	    return new int[] {AbstractRepair.MODIFYRELATION};
 	if (left instanceof SizeofExpr) {
+	    Opcode op=opcode;
+	    if (negated) {
+		/* 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 isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
 	    if (isRelation) {
-		if (opcode==Opcode.EQ)
+		if (op==Opcode.EQ) {
 		    if (((IntegerLiteralExpr)right).getValue()==0)
 			return new int[] {AbstractRepair.REMOVEFROMRELATION};
 		    else
 			return new int[] {AbstractRepair.ADDTORELATION,
-					      AbstractRepair.REMOVEFROMRELATION};
-		if (((opcode==Opcode.GE)&&!negated)||
-		    ((opcode==Opcode.LE)&&negated)) {
-		    if (((IntegerLiteralExpr)right).getValue()==0)
-			return new int[0];
-		    else
-			return new int[]{AbstractRepair.ADDTORELATION}; }
-		else
+					  AbstractRepair.REMOVEFROMRELATION};
+		} else if (op==Opcode.GE||op==Opcode.GT) {
+		    return new int[]{AbstractRepair.ADDTORELATION}; 
+		} else if (op==Opcode.LE||op==Opcode.LT) {
 		    return new int[]{AbstractRepair.REMOVEFROMRELATION};
+		} else if (op==Opcode.NE) {
+		    return new int[]{AbstractRepair.ADDTORELATION};
+		} else throw new Error();
 	    } else {
-		if (opcode==Opcode.EQ)
+		if (op==Opcode.EQ) {
 		    if (((IntegerLiteralExpr)right).getValue()==0)
 			return new int[] {AbstractRepair.REMOVEFROMSET};			
 		    else
 			return new int[] {AbstractRepair.ADDTOSET,
 					      AbstractRepair.REMOVEFROMSET};
-		
-		if (((opcode==Opcode.GE)&&!negated)||
-		    ((opcode==Opcode.LE)&&negated)) {
-		    if (((IntegerLiteralExpr)right).getValue()==0)
-			return new int[0];
-		    else
-			return new int[] {AbstractRepair.ADDTOSET}; }
-		else
+		} else if (op==Opcode.GE||op==Opcode.GT) {
+		    return new int[] {AbstractRepair.ADDTOSET}; 
+		} else if (op==Opcode.LE||op==Opcode.LT) {
 		    return new int[] {AbstractRepair.REMOVEFROMSET};
+		} else if (op==Opcode.NE) {
+		    return new int[] {AbstractRepair.ADDTOSET};
+		} else throw new Error();
 	    }
 	}
 	throw new Error("BAD");
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 52631d4..94ee278 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -171,7 +171,7 @@ public class RepairGenerator {
 		    craux.outputline(methodcall);
 		    craux.startblock();
 		    craux.outputline("int maybe=0;");
-		    final SymbolTable st2 = un.getRule().getSymbolTable();                
+		    final SymbolTable st2 = un.getRule().getSymbolTable();
 		    CodeWriter cr2 = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st2; }
                     };
@@ -942,7 +942,10 @@ public class RepairGenerator {
 	    generateremove=true;
 	} else if (opcode==Opcode.EQ) {
 	    cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
-	    generateadd=true;
+	    if (size==0)
+		generateadd=false;
+	    else 
+		generateadd=true;
 	    generateremove=true;
 	} else if (opcode==Opcode.NE) {
 	    cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
@@ -988,7 +991,7 @@ public class RepairGenerator {
 		Rule r=(Rule)state.vRules.get(i);
 		if (r.getInclusion().getTargetDescriptors().contains(d)) {
 		    for(int j=0;j<munremove.numUpdates();j++) {
-			UpdateNode un=munremove.getUpdate(i);
+			UpdateNode un=munremove.getUpdate(j);
 			if (un.getRule()==r) {
 				/* Update for rule rule r */
 			    String name=(String)updatenames.get(un);
@@ -1009,7 +1012,7 @@ public class RepairGenerator {
 	    cr.startblock();
 	    VarDescriptor newobject=VarDescriptor.makeNew("newobject");
 	    if (d instanceof RelationDescriptor) {
-		VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
+		VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
 		RelationDescriptor rd=(RelationDescriptor)d;
 		if (sources.relsetSource(rd,!ep.inverted())) {
 		    /* Set Source */
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 689a5d2..48212d1 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -49,11 +49,13 @@ public class Termination {
 
 	HashSet superset=new HashSet();
 	superset.addAll(conjunctions);
+	HashSet closureset=new HashSet();
+	//	closureset.addAll(updatenodes);
 	//superset.addAll(abstractrepair);
 	//superset.addAll(updatenodes);
 	//superset.addAll(scopenodes);
 	//superset.addAll(consequencenodes);
-	GraphNode.computeclosure(superset,null);
+	GraphNode.computeclosure(superset,closureset);
 	try {
 	    GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
 	} catch (Exception e) {
@@ -69,11 +71,27 @@ public class Termination {
 	}
 	GraphAnalysis ga=new GraphAnalysis(this);
 	removedset=ga.doAnalysis();
+	if (removedset==null) {
+	    System.out.println("Can't generate terminating repair algorithm!");
+	    System.exit(-1);
+	}
 	System.out.println("Removing:");
 	for(Iterator it=removedset.iterator();it.hasNext();) {
 	    GraphNode gn=(GraphNode)it.next();
 	    System.out.println(gn.getTextLabel());
 	}
+
+	superset=new HashSet();
+	superset.addAll(conjunctions);
+	superset.removeAll(removedset);
+	GraphNode.computeclosure(superset,removedset);
+	try {
+	    GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
+	} catch (Exception e) {
+	    e.printStackTrace();
+	    System.exit(-1);
+	}
+
     }
     
     void generateconjunctionnodes() {
@@ -92,6 +110,40 @@ public class Termination {
 		((Set)conjunctionmap.get(c)).add(gn);
 		conjtonodemap.put(dnf.get(j),gn);
 	    }
+	    for(int j=0;j<c.numQuantifiers();j++) {
+		Quantifier q=c.getQuantifier(j);
+		if (q instanceof SetQuantifier) {
+		    SetQuantifier sq=(SetQuantifier)q;
+		    VarExpr ve=new VarExpr(sq.getVar());
+		    InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
+		    DNFConstraint dconst=new DNFConstraint(ip);
+		    dconst=dconst.not();
+		    TermNode tn=new TermNode(c,dconst.get(0));
+		    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
+					       "Conj ("+i+","+j+") "+dconst.get(0).name()
+					       ,tn);
+		    conjunctions.add(gn);
+		    if (!conjunctionmap.containsKey(c))
+			conjunctionmap.put(c,new HashSet());
+		    ((Set)conjunctionmap.get(c)).add(gn);
+		    conjtonodemap.put(dconst.get(0),gn);
+		} else if (q instanceof RelationQuantifier) {
+		    RelationQuantifier rq=(RelationQuantifier)q;
+		    VarExpr ve=new VarExpr(rq.y);
+		    InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
+		    DNFConstraint dconst=new DNFConstraint(ip);
+		    dconst=dconst.not();
+		    TermNode tn=new TermNode(c,dconst.get(0));
+		    GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
+					       "Conj ("+i+","+j+") "+dconst.get(0).name()
+					       ,tn);
+		    conjunctions.add(gn);
+		    if (!conjunctionmap.containsKey(c))
+			conjunctionmap.put(c,new HashSet());
+		    ((Set)conjunctionmap.get(c)).add(gn);
+		    conjtonodemap.put(dconst.get(0),gn);
+		}
+	    }
 	}
     }
 
@@ -166,7 +218,7 @@ public class Termination {
 		Constraint constr=tn2.getConstraint();
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
-		    if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
+		    if (AbstractInterferes.interferes(sn,dp)||
 			AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 			GraphNode gnconseq=(GraphNode)consequence.get(sn);
diff --git a/Repair/RepairCompiler/MCC/Runtime/redblack.c b/Repair/RepairCompiler/MCC/Runtime/redblack.c
index 8d4c53d..c4a2349 100755
--- a/Repair/RepairCompiler/MCC/Runtime/redblack.c
+++ b/Repair/RepairCompiler/MCC/Runtime/redblack.c
@@ -1,4 +1,4 @@
-static char rcsid[]="$Id: redblack.c,v 1.1 2004/03/07 22:02:43 bdemsky Exp $";
+static char rcsid[]="$Id: redblack.c,v 1.2 2004/03/10 06:15:03 bdemsky Exp $";
 
 /*
    Redblack balanced tree algorithm
@@ -380,7 +380,7 @@ static struct rbnode * rb_lookup(const void *low, const void *high, struct rbtre
   
   /* walk x down the tree */
   while(x!=RBNULL) {
-    if (low<x->high &&
+    if (low<x->high&&
 	x->key<high)
       return x;
     if (x->left!=RBNULL && x->left->max>low)
@@ -923,6 +923,19 @@ dumptree(struct rbnode *x, int n)
 
 /*
  * $Log: redblack.c,v $
+ * Revision 1.2  2004/03/10 06:15:03  bdemsky
+ *
+ *
+ * Added:
+ * Concrete Interference rule that falsify a rule that quantifies over a set can't
+ * remove the last element of the set.
+ *
+ * Concrete Interference rule that updates that definitely falsify a rule can't modify
+ * the inclusion condition causing a possible addition.
+ *
+ * Intelligence in the GraphAnalysis package that computes must & cant remove sets.
+ * Search through only unique combinations.
+ *
  * Revision 1.1  2004/03/07 22:02:43  bdemsky
  *
  *
-- 
2.34.1