Updates to allow repairing backpointers.

[repair.git] / Repair / RepairCompiler / MCC / IR / ConcreteInterferes.java

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index 87418210200d241723519287204ac45770b41317..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,38 +130,59 @@ 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();
-       for(int i=0;i<un.numUpdates();i++) {
-           Updates u=un.getUpdate(i);
-           if (u.getType()==Updates.POSITION&&
-               ar.isNewObject(u.getRightPos()==0)) {
-               Expr newleftexpr=u.getLeftExpr();
-               Expr leftexpr=updates.getLeftExpr();
-               boolean foundfield=false;
-               while(true) {
-                   if (leftexpr.equals(null,newleftexpr)) {
-                       if (foundfield)
-                           return true;
-                       else
+       if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
+           for(int i=0;i<un.numUpdates();i++) {
+               Updates u=un.getUpdate(i);
+               if (u.getType()==Updates.POSITION&&
+                   ar.isNewObject(u.getRightPos()==0)) {
+                   Expr newleftexpr=u.getLeftExpr();
+                   Expr leftexpr=updates.getLeftExpr();
+                   boolean foundfield=false;
+                   while(true) {
+                       if (leftexpr.equals(null,newleftexpr)) {
+                           if (foundfield)
+                               return true;
+                           else
+                               break;
+                       } else if (leftexpr instanceof DotExpr) {
+                           if (!foundfield) {
+                               foundfield=true;
+                           } else {
+                               if (((DotExpr)leftexpr).isPtr())
+                                   break; //if its not a pointer, we're still in the structure
+                           }
+                           leftexpr=((DotExpr)leftexpr).getExpr();
+                       } else if (leftexpr instanceof CastExpr) {
+                           leftexpr=((CastExpr)leftexpr).getExpr();
+                       } else
                            break;
-                   } else if (leftexpr instanceof DotExpr) {
-                       if (!foundfield) {
-                           foundfield=true;
-                       } else {
-                           if (((DotExpr)leftexpr).isPtr())
-                               break; //if its not a pointer, we're still in the structure
-                       }
-                       leftexpr=((DotExpr)leftexpr).getExpr();
-                   } else if (leftexpr instanceof CastExpr) {
-                       leftexpr=((CastExpr)leftexpr).getExpr();
-                   } else
-                       break;
+                   }
                }
            }
-       }
-
+       
        return false;
     }