From: bdemsky <bdemsky>
Date: Thu, 29 Jul 2004 22:21:58 +0000 (+0000)
Subject: Updates to allow repairing backpointers.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=94f62079ed1aec461df5e3e493664abe38cf61f9;p=repair.git
Updates to allow repairing backpointers.
---
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();
}