From f4d787b23a126c58eec51c860f2b3d3bf8de7569 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Sun, 9 May 2004 00:47:18 +0000
Subject: [PATCH] 1) Added useDescriptor method to Expr's. 2) Generalized
 analysis to determine that an update effecting a rule won't change other
 bindings of the same rule...

---
 Repair/RepairCompiler/MCC/IR/CastExpr.java    |   4 +
 .../MCC/IR/ConcreteInterferes.java            | 147 +++++++++++++++---
 .../MCC/IR/ConstraintDependence.java          |   2 +
 Repair/RepairCompiler/MCC/IR/DotExpr.java     |  10 ++
 .../RepairCompiler/MCC/IR/ElementOfExpr.java  |   8 +
 Repair/RepairCompiler/MCC/IR/Expr.java        |   6 +-
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  16 +-
 .../RepairCompiler/MCC/IR/RelationExpr.java   |   8 +
 Repair/RepairCompiler/MCC/IR/SetExpr.java     |   7 +
 Repair/RepairCompiler/MCC/IR/SizeofExpr.java  |   4 +
 Repair/RepairCompiler/MCC/IR/Termination.java |  30 +++-
 Repair/RepairCompiler/MCC/IR/TupleOfExpr.java |   9 ++
 Repair/RepairCompiler/MCC/IR/VarExpr.java     |   7 +
 13 files changed, 222 insertions(+), 36 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index 44e085d..d36aabb 100755
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -38,6 +38,10 @@ public class CastExpr extends Expr {
 	else return ((this.type==((CastExpr)e).type)&&expr.equals(remap,((CastExpr)e).expr));
     }
 
+    public Set useDescriptor(Descriptor d) {
+	return expr.useDescriptor(d);
+    }
+
     public boolean usesDescriptor(Descriptor d) {
 	return expr.usesDescriptor(d);
     }
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index f8d82d5..af193f7 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -1,7 +1,13 @@
 package MCC.IR;
 import java.util.*;
 
-class ConcreteInterferes {
+public class ConcreteInterferes {
+    Termination termination;
+
+    public ConcreteInterferes(Termination t) {
+	this.termination=t;
+    }
+
 
     static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
 	Descriptor updated_des=update.getDescriptor();
@@ -148,7 +154,7 @@ class ConcreteInterferes {
     /** 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) {
+    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++) {
@@ -169,36 +175,45 @@ class ConcreteInterferes {
 		       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 */
+			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;
 			}
@@ -209,6 +224,90 @@ class ConcreteInterferes {
 	return false;
     }
 
+    private boolean interferes(Updates u, Rule r, Expr e) {
+	Set exprs=e.useDescriptor(u.getDescriptor());
+	for(Iterator eit=exprs.iterator();eit.hasNext();) {
+	    Expr e2=(Expr)eit.next();
+	    if (mayinterfere(u,r,e2))
+		return true;
+	}
+	return false;
+    }
+
+    private boolean mayinterfere(Updates u, Rule r, Expr e) {
+	// Note: rule of u must be r
+
+	Expr update_e=u.getLeftExpr();
+	HashSet quantifierset=new HashSet();
+
+	if (termination.analyzeQuantifiers(r,quantifierset))
+	    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();
+	    else if (e instanceof CastExpr)
+		e=((CastExpr)e).getExpr();
+	    else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
+		DotExpr de1=(DotExpr)update_e;
+		DotExpr de2=(DotExpr)e;
+		if (de1.isValue()&&!firstfield)
+		    return true; /* Could have aliasing from this */
+		if (de1.getField()!=de2.getField())
+		    return true; /* Different fields: not comparible */
+		firstfield=false;
+
+		Expr index1=de1.getIndex();
+		Expr index2=de2.getIndex();
+		if (index1!=null) {
+		    assert index2!=null;
+		    if ((index1 instanceof VarExpr)&&(index2 instanceof VarExpr)) {
+			VarDescriptor vd1=((VarExpr)index1).getVar();
+			VarDescriptor vd2=((VarExpr)index2).getVar();
+			if ((vd1==vd2)&&!vd1.isGlobal()) {
+			    quantifierset.add(getQuantifier(r,vd1));
+			    if (termination.analyzeQuantifiers(r,quantifierset))
+				return false; /* State is disjoint from any other example */
+			}
+		    }
+		}
+		update_e=de1.getExpr();
+		e=de2.getExpr();
+	    } else if ((update_e instanceof VarExpr)&&(e instanceof VarExpr)) {
+		VarDescriptor vd1=((VarExpr)update_e).getVar();
+		VarDescriptor vd2=((VarExpr)e).getVar();
+		if ((vd1==vd2)&&!vd1.isGlobal()) {
+		    quantifierset.add(getQuantifier(r,vd1));
+		    if (termination.analyzeQuantifiers(r,quantifierset))
+			return false; /* State is disjoint from any other example */
+		}
+		return true;
+	    } else return true;
+	}
+
+    }
+
+    static private Quantifier getQuantifier(Quantifiers qs, VarDescriptor vd) {
+	for (int i=0;i<qs.numQuantifiers();i++) {
+	    Quantifier q=qs.getQuantifier(i);
+	    if (q instanceof SetQuantifier) {
+		SetQuantifier sq=(SetQuantifier)q;
+		if (sq.getVar()==vd)
+		    return sq;
+	    } else if (q instanceof RelationQuantifier) {
+		RelationQuantifier rq=(RelationQuantifier)q;
+		if ((rq.x==vd)||(rq.y==vd))
+		    return rq;
+	    } else if (q instanceof ForQuantifier) {
+		ForQuantifier fq=(ForQuantifier)q;
+		if (fq.getVar()==vd)
+		    return fq;
+	    }
+	}
+	return null;
+    }
+    
     static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
 	AbstractRepair ar=mun.getRepair();
 	if (satisfy)
diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 7ae89cb..192e212 100755
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -179,6 +179,8 @@ public class ConstraintDependence {
 		RelationInclusion ri=(RelationInclusion)r.getInclusion();
 		Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
 		SetDescriptor sd=e.getSet();
+		if (sd==null)
+		    sd=f.isInverse()?ri.getRelation().getRange():ri.getRelation().getDomain();
 		if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
 		    continue; /* This rule doesn't effect the function */
 		if (foundrule) /* two different rules are a problem */
diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 684c4fe..b0a49a3 100755
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -67,6 +67,16 @@ public class DotExpr extends Expr {
 	return name;
     }
     
+    public Set useDescriptor(Descriptor d) {
+	HashSet newset=new HashSet();
+	if (d==fd)
+	    newset.add(this);
+	newset.addAll(left.useDescriptor(d));
+	if (intindex!=null)
+	    newset.addAll(intindex.useDescriptor(d));
+	return newset;
+    }
+
     public boolean usesDescriptor(Descriptor d) {
 	if (d==fd)
 	    return true;
diff --git a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
index 49b0064..9630688 100755
--- a/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
@@ -23,6 +23,14 @@ public class ElementOfExpr extends Expr {
 	    return true;
 	return element.usesDescriptor(d);
     }
+    public Set useDescriptor(Descriptor d) {
+	HashSet newset=new HashSet();
+	if (d==set)
+	    newset.add(this);
+	newset.addAll(element.useDescriptor(d));
+	return newset;
+    }
+
     public String name() {
 	return element.name()+" in "+set.toString();
     }
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index 771b9f8..655004b 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -53,6 +53,10 @@ public abstract class Expr {
 	return false;
     }
 
+    public Set useDescriptor(Descriptor d) {
+	return new HashSet();
+    }
+
     public boolean usesDescriptor(Descriptor rd) {
 	System.out.println(this.getClass().getName());
 	throw new Error("UNIMPLEMENTED");
@@ -75,7 +79,7 @@ public abstract class Expr {
     }
 
     public SetDescriptor getSet() {
-	throw new Error("No Set for this Expr");
+	return null; /* unknown value */
     }
 
     public boolean isSafe() {
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 09895eb..89bc976 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -189,15 +189,17 @@ public class OpExpr extends Expr {
     }
 
     public boolean usesDescriptor(Descriptor d) {
-	if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
-	    opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
-	    return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
-	    //	    return right.usesDescriptor(d);
-	else
-	    return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
+	return left.usesDescriptor(d)||(right!=null&&right.usesDescriptor(d));
     }
-    
 
+    public Set useDescriptor(Descriptor d) {
+	HashSet newset=new HashSet();
+	newset.addAll(left.useDescriptor(d));
+	if (right!=null)
+	    newset.addAll(right.useDescriptor(d));
+	return newset;
+    }
+    
     public int[] getRepairs(boolean negated, Termination t) {
 	if (left instanceof RelationExpr)
 	    return new int[] {AbstractRepair.MODIFYRELATION};
diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index 355f461..def9576 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -66,6 +66,14 @@ public class RelationExpr extends Expr {
 	else
 	    return expr.usesDescriptor(rd);
     }
+
+    public Set useDescriptor(Descriptor rd) {
+	HashSet newset=new HashSet();
+	if (rd==relation)
+	    newset.add(this);
+	newset.addAll(expr.useDescriptor(rd));
+	return newset;
+    }
     
     public RelationDescriptor getRelation() {
         return relation;
diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java
index d50c50e..9deb8ac 100755
--- a/Repair/RepairCompiler/MCC/IR/SetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java
@@ -27,6 +27,13 @@ public class SetExpr extends Expr {
 	return (s==sd);
     }
 
+    public Set useDescriptor(Descriptor s) {
+	HashSet newset=new HashSet();
+	if (s==sd)
+	    newset.add(this);
+	return newset;
+    }
+
     public SetExpr() {
         this.sd = null;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
index ec72e3f..9cd29df 100755
--- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
@@ -33,6 +33,10 @@ public class SizeofExpr extends Expr {
 	return setexpr.usesDescriptor(rd);
     }
 
+    public Set useDescriptor(Descriptor rd) {
+	return setexpr.useDescriptor(rd);
+    }
+
 
     public Descriptor getDescriptor() {
 	return setexpr.getDescriptor();
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 830e075..4698b51 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -26,6 +26,7 @@ public class Termination {
     ComputeMaxSize maxsize;
     State state;
     AbstractInterferes abstractinterferes;
+    ConcreteInterferes concreteinterferes;
     ConstraintDependence constraintdependence;
     ExactSize exactsize;
     ArrayAnalysis arrayanalysis;
@@ -62,6 +63,7 @@ public class Termination {
 	arrayanalysis=new ArrayAnalysis(state,this);
 
 	abstractinterferes=new AbstractInterferes(this);
+	concreteinterferes=new ConcreteInterferes(this);
 	generateconjunctionnodes();
 	constraintdependence=new ConstraintDependence(state,this);
 
@@ -99,7 +101,6 @@ public class Termination {
 	    System.out.println("Can't generate terminating repair algorithm!");
 	    System.exit(-1);
 	}
-	constraintdependence.traversedependences(this);
 
 	System.out.println("Removing:");
 	for(Iterator it=removedset.iterator();it.hasNext();) {
@@ -117,7 +118,7 @@ public class Termination {
 	    e.printStackTrace();
 	    System.exit(-1);
 	}
-
+	constraintdependence.traversedependences(this);
     }
 
 
@@ -227,12 +228,12 @@ public class Termination {
 	    /* Cycle through the rules to look for possible conflicts */
 	    for(int i=0;i<state.vRules.size();i++) {
 		Rule r=(Rule) state.vRules.get(i);  
-		if (ConcreteInterferes.interferes(mun,r,true)) {
+		if (concreteinterferes.interferes(mun,r,true)) {
 		    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 		    gn.addEdge(e);
 		}
-		if (ConcreteInterferes.interferes(mun,r,false)) {
+		if (concreteinterferes.interferes(mun,r,false)) {
 		    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 		    gn.addEdge(e);
@@ -1092,4 +1093,25 @@ public class Termination {
 	}
 	return okay;
     }
+
+    public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
+	for(int i=0;i<qs.numQuantifiers();i++) {
+	    Quantifier q=qs.getQuantifier(i);
+	    if (set.contains(q))
+		continue;
+	    if (q instanceof SetQuantifier) {
+		SetDescriptor sd=((SetQuantifier)q).getSet();
+		if (maxsize.getsize(sd)<=1&&
+		    maxsize.getsize(sd)>=0)
+		    continue;
+	    } else if (q instanceof RelationQuantifier) {
+		RelationDescriptor rd=((RelationQuantifier)q).getRelation();
+		if (maxsize.getsize(rd)<=1&&
+		    maxsize.getsize(rd)>=0)
+		    continue;
+	    }
+	    return false;
+	}
+	return true;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
index 941b37a..eabd014 100755
--- a/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
@@ -39,6 +39,15 @@ public class TupleOfExpr extends Expr {
 	    return left.usesDescriptor(d)||right.usesDescriptor(d);
     }
 
+    public Set useDescriptor(Descriptor d) {
+	HashSet newset=new HashSet();
+	if (d==relation)
+	    newset.add(this);
+	newset.addAll(left.useDescriptor(d));
+	newset.addAll(right.useDescriptor(d));
+	return newset;
+    }
+
     public boolean equals(Map remap, Expr e) {
 	if (e==null||!(e instanceof TupleOfExpr))
 	    return false;
diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index 00e8394..ddc0e8e 100755
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -41,6 +41,13 @@ public class VarExpr extends Expr {
 	return false;
     }
 
+    public Set useDescriptor(Descriptor d) {
+	HashSet newset=new HashSet();
+	if (d==vd)
+	    newset.add(this);
+	return newset;
+    }
+
     public boolean isNonNull() {
 	return true;
     }
-- 
2.34.1