Updates to allow repairing backpointers.

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index a4c1ba3cc33d42c709b7c609853369427ec50f7d..fc683a956400b00670d66032646130917c19576a 100755 (executable)
--- 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 3cb9b03c24c0cf5c78ee78760e7dbaa6b38ccf2b..aecc4e995b0022f5819dc46b77656db0ff58f36f 100755 (executable)
--- 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 083a5063680110a52ce616570553e5b8496466f9..2e657ef323d83019da8fc960abb86f43d7790e51 100755 (executable)
--- 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 3cf53b9e4b2dc437e1af61cf2e6b4f58223ca86c..5e4bc91aac5f1013dcebf2e16b89e81fa31fd535 100755 (executable)
--- 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 b25e5430780079719b2d6fbc662377bfe1a2381d..12a47f364ac74001bac92ae06c00aaf4fdd5b56b 100755 (executable)
--- 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();
     }