From 94f62079ed1aec461df5e3e493664abe38cf61f9 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 29 Jul 2004 22:21:58 +0000
Subject: [PATCH] Updates to allow repairing backpointers.

---
 .../MCC/IR/AbstractInterferes.java            | 40 +++++++++++++++
 .../RepairCompiler/MCC/IR/AbstractRepair.java |  3 --
 .../MCC/IR/ConcreteInterferes.java            | 51 ++++++++++++++++++-
 Repair/RepairCompiler/MCC/IR/Termination.java |  5 ++
 Repair/RepairCompiler/MCC/IR/VarExpr.java     |  2 +
 5 files changed, 96 insertions(+), 5 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index a4c1ba3..fc683a9 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -59,6 +59,46 @@ class AbstractInterferes {
 	return false;
     }
 
+    public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
+	if (c.numQuantifiers()==1&&
+	    (c.getQuantifier(0) instanceof RelationQuantifier)) {
+	    RelationQuantifier rq=(RelationQuantifier)c.getQuantifier(0);
+	    if (rq.getRelation()==ar.getDescriptor()) {
+		Hashtable ht=new Hashtable();
+		if (ar.getDomainSet()!=null)
+		    ht.put(rq.x,ar.getDomainSet());
+		if (ar.getRangeSet()!=null)
+		    ht.put(rq.y,ar.getRangeSet());
+		DNFConstraint dconst=c.dnfconstraint;
+	    conjloop:
+		for(int i=0;i<dconst.size();i++) {
+		    Conjunction conj=dconst.get(i);
+		predloop:
+		    for(int j=0;j<conj.size();j++) {
+			DNFPredicate dpred=conj.get(j);
+			Predicate p=dpred.getPredicate();
+			if ((p instanceof InclusionPredicate)&&(!dpred.isNegated())) {
+			    InclusionPredicate ip=(InclusionPredicate)p;
+			    if (ip.expr instanceof VarExpr&&
+				ip.setexpr.getDescriptor() instanceof SetDescriptor) {
+				VarDescriptor vd=((VarExpr)ip.expr).getVar();
+				if (ht.containsKey(vd)) {
+				    SetDescriptor td=(SetDescriptor)ip.setexpr.getDescriptor();
+				    SetDescriptor s=(SetDescriptor)ht.get(vd);
+				    if (td.isSubset(s))
+					continue predloop;
+				}
+			    }
+			}
+			continue conjloop;
+		    }
+		    return true;
+		}
+	    }
+	}
+	return false;
+    }
+
     /** Does performing the AbstractRepair ar falsify the predicate dp */
 
     public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index 3cb9b03..aecc4e9 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -138,9 +138,6 @@ class AbstractRepair {
 	return null;
     }
 
-
-    
-
     public int getType() {
 	return type;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index 083a506..2e657ef 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -26,7 +26,7 @@ public class ConcreteInterferes {
 		//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;
@@ -39,7 +39,6 @@ public class ConcreteInterferes {
 		    continue;
 
 
-
 		// See if the update interferes with the inclusion
 		// condition for the rule
 		if (r.getInclusion().usesDescriptor(updated_des)) {
@@ -68,6 +67,22 @@ public class ConcreteInterferes {
 			} 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
@@ -95,6 +110,18 @@ public class ConcreteInterferes {
                                              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))
 			    return true;
 		    }
@@ -103,6 +130,26 @@ public class ConcreteInterferes {
 	}
 	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();
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 3cf53b9..5e4bc91 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -277,6 +277,11 @@ public class Termination {
 		TermNode tn2=(TermNode)gn2.getOwner();
 		Conjunction conj=tn2.getConjunction();
 		Constraint cons=tn2.getConstraint();
+		/* See if this is a relation wellformedness constraint
+                   that is trivially satisfied. */
+		System.out.println(gn.getTextLabel()+"---"+gn2.getTextLabel());
+		if (abstractinterferes.checkrelationconstraint(ar, cons))
+		    continue;
 
 		for(int i=0;i<conj.size();i++) {
 		    DNFPredicate dp=conj.get(i);
diff --git a/Repair/RepairCompiler/MCC/IR/VarExpr.java b/Repair/RepairCompiler/MCC/IR/VarExpr.java
index b25e543..12a47f3 100755
--- a/Repair/RepairCompiler/MCC/IR/VarExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/VarExpr.java
@@ -26,6 +26,8 @@ public class VarExpr extends Expr {
     }
 
     public SetDescriptor getSet() {
+	if (vd==null)
+	    return null;
 	return vd.getSet();
     }
 
-- 
2.34.1