Committing changes to leftsize->rightSize, more comments, and handling

of MODIFYRELATION.

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 592b9d44d26e71605767b55364466ac2c03e49f1..ea024cdb22bf699d4474cdd40e2f6edc13836a3f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -2,6 +2,9 @@ package MCC.IR;
 import java.util.*;
 
 class AbstractInterferes {
+
+    /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
+     * Rule r */
     static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
        boolean mayadd=false;
        boolean mayremove=false;
@@ -50,6 +53,7 @@ class AbstractInterferes {
        return false;
     }
 
+    /** Does performing the AbstractRepair ar falsify the predicate dp */
 
     static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
        if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
@@ -66,10 +70,10 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg1=ar.getPredicate().isNegated();
            Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
-           int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
+           int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
            if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE))||
                (neg1&&((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.LT)||op1==Opcode.LE))) {
                int size1a=0;
@@ -107,16 +111,117 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
-           if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
-               (neg2&&(op2==Opcode.NE)&&(size2==0))||
-               (!neg2&&(op2==Opcode.GE))||
-               (!neg2&&(op2==Opcode.GT))||
-               (neg2&&(op2==Opcode.LE))||
-               (neg2&&(op2==Opcode.LT)))
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+
+           op2=translateOpcode(neg2,op2);
+
+           if (((op2==Opcode.EQ)&&(size2==0))||
+               (op2==Opcode.GE)||
+               (op2==Opcode.GT))
                return false;
        }
 
+       if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+           
+           (ar.getType()==AbstractRepair.MODIFYRELATION)&&
+           (dp.getPredicate() instanceof ExprPredicate)&&
+           (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+           (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+
+           boolean neg1=ar.getPredicate().isNegated();
+           Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+           boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
+           int size1=isInt1?((ExprPredicate)ar.getPredicate().getPredicate()).rightSize():0;
+           Expr expr1=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
+
+
+           boolean neg2=dp.isNegated();
+           Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+           boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
+           int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
+           Expr expr2=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).right;
+
+           /* Translate the opcodes */
+           op1=translateOpcode(neg1,op1);
+           op2=translateOpcode(neg2,op2);
+           
+           /* Obvious cases which can't interfere */
+           if (((op1==Opcode.GT)||
+               (op1==Opcode.GE))&&
+               ((op2==Opcode.GT)||
+                (op2==Opcode.GE)))
+               return false;
+
+           if (((op1==Opcode.LT)||
+               (op1==Opcode.LE))&&
+               ((op2==Opcode.LT)||
+                (op2==Opcode.LE)))
+               return false;
+               
+           if (isInt1&&isInt2) {
+               if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
+                   ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
+                   size1==size2)
+                   return false;
+               int size1a=size1;
+               int size2a=size2;
+               if (op1==Opcode.GT)
+                   size1a++;
+               if (op1==Opcode.LT)
+                   size1a--;
+               if (op1==Opcode.NE)
+                   size1a++; /*FLAGNE this is current behavior for NE repairs */
+               
+               if (op2==Opcode.GT)
+                   size2a++;
+               if (op2==Opcode.LT)
+                   size2a--;
+
+               if (((op1==Opcode.GE)||(op1==Opcode.GT))&&
+                   ((op2==Opcode.LE)||(op2==Opcode.EQ)||(op2==Opcode.LT))&&
+                   (size1a<=size2a))
+                   return false;
+
+               if (((op1==Opcode.LE)||(op1==Opcode.LT))&&
+                   ((op2==Opcode.GE)||(op2==Opcode.EQ)||(op2==Opcode.GT))&&
+                   (size1a>=size2a))
+                   return false;
+               
+               if ((op1==Opcode.EQ)&&(op2==Opcode.EQ)&&
+                   (size1a==size2a))
+                   return false;
+
+               if ((op1==Opcode.EQ)&&
+                   ((op2==Opcode.LE)||(op2==Opcode.LT))&&
+                   (size1a<=size2a))
+                   return false;
+
+               if ((op1==Opcode.EQ)&&
+                   ((op2==Opcode.GE)||(op2==Opcode.GT))&&
+                   (size1a>=size2a))
+                   return false;
+
+               if (op2==Opcode.NE)  /*FLAGNE this is current behavior for NE repairs */
+                   if (size1a!=size2)
+                       return false;
+
+               if ((op1==Opcode.NE)&&
+                   (op2==Opcode.EQ)&&
+                   (size1!=size2))
+                   return false;
+
+               if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
+                   ((op2==Opcode.GT)||(op2==Opcode.GE))&&
+                   (size1!=size2a))
+                   return false;
+
+               if ((op1==Opcode.NE)&& /* FLAGNE relies on increasing or decreasing by 1 */
+                   ((op2==Opcode.LT)||(op2==Opcode.LE))&&
+                   (size1!=size2a))
+                   return false;
+           }
+       }
+
        /* This handles all the c comparisons in the paper */
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
@@ -126,37 +231,28 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg1=ar.getPredicate().isNegated();
            Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
-           int size1=((ExprPredicate)ar.getPredicate().getPredicate()).leftsize();
+           int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
-           if ((!neg1&&((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE))||
-               (neg1&&((op1==Opcode.EQ)||(op1==Opcode.GT)||op1==Opcode.GE)||(op1==Opcode.NE))) {
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+           /* Translate the opcodes */
+           op1=translateOpcode(neg1,op1);
+           op2=translateOpcode(neg2,op2);
+
+           if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
                int size1a=0;
-               if (neg1) {
-                   if((op1==Opcode.EQ)||(op1==Opcode.GE))
-                       size1a=size1-1;
-                   if((op1==Opcode.GT)||(op1==Opcode.NE))
-                       size1a=size1;
-               }
-               if (!neg1) {
-                   if((op1==Opcode.EQ)||(op1==Opcode.LE))
-                       size1a=size1;
-                   if((op1==Opcode.LT)||(op1==Opcode.NE))
-                       size1a=size1-1;
-               }
-               if ((!neg2&&(op2==Opcode.EQ)&&(size1a==size2))||
-                   (neg2&&(op2==Opcode.EQ)&&(size1a!=size2))||
-                   (!neg2&&(op2==Opcode.NE)&&(size1a!=size2))||
-                   (neg2&&(op2==Opcode.NE)&&(size1a==size2))||
-                   (neg2&&(op2==Opcode.GE))||
-                   (neg2&&(op2==Opcode.GT))||
-                   (!neg2&&(op2==Opcode.LE))||
-                   (!neg2&&(op2==Opcode.LT))||
-                   (!neg2&&(op2==Opcode.GE)&&(size1a>=size2))||
-                   (!neg2&&(op2==Opcode.GT)&&(size1a>size2))||
-                   (neg2&&(op2==Opcode.LE)&&(size1a>size2))||
-                   (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
+
+               if((op1==Opcode.EQ)||(op1==Opcode.LE))
+                   size1a=size1;
+               if((op1==Opcode.LT)||(op1==Opcode.NE))
+                   size1a=size1-1;
+
+               if (((op2==Opcode.EQ)&&(size1a==size2))||
+                   ((op2==Opcode.NE)&&(size1a!=size2))||
+                   (op2==Opcode.LE)||
+                   (op2==Opcode.LT)||
+                   ((op2==Opcode.GE)&&(size1a>=size2))||
+                   ((op2==Opcode.GT)&&(size1a>size2)))
                    return false;
            }
        }
@@ -167,7 +263,7 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
            if ((!neg2&&(op2==Opcode.EQ)&&(size2==0))||
                (neg2&&(op2==Opcode.NE)&&(size2==0))||
                (neg2&&(op2==Opcode.GE))||
@@ -192,6 +288,29 @@ class AbstractInterferes {
        return true;
     }
 
+    static private Opcode translateOpcode(boolean neg, Opcode op) {
+       if (neg) {
+        /* remove negation through opcode translation */
+            if (op==Opcode.GT)
+                op=Opcode.LE;
+            else if (op==Opcode.GE)
+                op=Opcode.LT;
+            else if (op==Opcode.EQ)
+                op=Opcode.NE;
+            else if (op==Opcode.NE)
+                op=Opcode.EQ;
+            else if (op==Opcode.LT)
+                op=Opcode.GE;
+            else if (op==Opcode.LE)
+                op=Opcode.GT;
+        }
+
+       return op;
+    }
+
+    /** Does the increase (or decrease) in scope of a model defintion rule represented by sn
+     * falsify the predicate dp */
+
     static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
        if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
            Rule r=sn.getRule();
@@ -213,7 +332,7 @@ class AbstractInterferes {
                (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
                boolean neg=dp.isNegated();
                Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
-               int size=((ExprPredicate)dp.getPredicate()).leftsize();
+               int size=((ExprPredicate)dp.getPredicate()).rightSize();
                if (neg) {
                    /* remove negation through opcode translation */
                    if (op==Opcode.GT)
@@ -240,6 +359,9 @@ class AbstractInterferes {
        return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
     }
 
+    /** Does increasing (or decreasing if satisfy=false) the size of the set or relation des
+     * falsify the predicate dp */
+
     static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
        if ((des!=dp.getPredicate().getDescriptor()) &&
            ((des instanceof SetDescriptor)||
@@ -253,7 +375,7 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
            {
                if ((!neg2&&(op2==Opcode.GE))||
                    (!neg2&&(op2==Opcode.GT))||
@@ -271,7 +393,7 @@ class AbstractInterferes {
            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
            boolean neg2=dp.isNegated();
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
-           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           int size2=((ExprPredicate)dp.getPredicate()).rightSize();
            {
                if ((neg2&&(op2==Opcode.GE))||
                    (neg2&&(op2==Opcode.GT))||

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index 2c7d59e9b60d9c618b2a4f401ac7825c934a4f0d..eefde7f2f733ad659d9665426cf6625899178330 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -159,6 +159,9 @@ class ConcreteInterferes {
        return true;
     }
 
+    /** 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) {
        if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
            return false;
@@ -178,19 +181,22 @@ class ConcreteInterferes {
                    /* Update is local to this rule, and the effect is intentional */
                    /* If we're adding something, a side effect could be to falsify some other binding
                       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))&&
+                       (((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))&&
+                       (((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) {
@@ -236,26 +242,26 @@ class ConcreteInterferes {
        ExprPredicate ep=(ExprPredicate)p;
        if (ep.getType()!=ExprPredicate.SIZE)
            return true;
-       if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==1)&&!negated)
+       if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==1)&&!negated)
            return false;
-       if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==1)&&negated)
+       if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==1)&&negated)
            return false;
 
-       if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==0)&&!negated)
+       if ((ep.getOp()==Opcode.NE)&&(ep.rightSize()==0)&&!negated)
            return false;
-       if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==0)&&negated)
+       if ((ep.getOp()==Opcode.EQ)&&(ep.rightSize()==0)&&negated)
            return false;
 
 
 
-       if ((ep.getOp()==Opcode.GT)&&(ep.leftsize()==0)&&!negated)
+       if ((ep.getOp()==Opcode.GT)&&(ep.rightSize()==0)&&!negated)
            return false;
-       if ((ep.getOp()==Opcode.LE)&&(ep.leftsize()==0)&&negated)
+       if ((ep.getOp()==Opcode.LE)&&(ep.rightSize()==0)&&negated)
            return false;
 
-       if ((ep.getOp()==Opcode.GE)&&(ep.leftsize()==1)&&!negated)
+       if ((ep.getOp()==Opcode.GE)&&(ep.rightSize()==1)&&!negated)
            return false;
-       if ((ep.getOp()==Opcode.LT)&&(ep.leftsize()==1)&&negated)
+       if ((ep.getOp()==Opcode.LT)&&(ep.rightSize()==1)&&negated)
            return false;
        
        return true;

diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 04b223ac205163fbdae870416e09c7cc7ed5eb64..4bed2313f7468f854b7fc2ffb7db3fab749ed9ef 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -26,8 +26,12 @@ public class ExprPredicate extends Predicate {
        return ((OpExpr)expr).opcode;
     }
 
-    public int leftsize() {
-       return ((IntegerLiteralExpr)((OpExpr)expr).right).getValue();
+    public int rightSize() {
+       return OpExpr.getInt(((OpExpr)expr).right);
+    }
+
+    public boolean isRightInt() {
+       return OpExpr.isInt(((OpExpr)expr).right);
     }
 
     public ExprPredicate(Expr expr) {

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 53f424c85c9cdf295f64cb2175556052b3a280b0..ab4d0262f594381e9485342117243dde01942e5e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -870,7 +870,7 @@ public class RepairGenerator {
            /* Equal */
        } else if (opcode==Opcode.EQ) {
            /* Equal */
-       } else if (opcode==Opcode.NE) {
+       } else if (opcode==Opcode.NE) { /* search for FLAGNE if this is changed*/
            cr.outputline(newvalue.getSafeSymbol()+"++;");
        } else {
            throw new Error("Unrecognized Opcode");
@@ -898,7 +898,7 @@ public class RepairGenerator {
                Rule r=(Rule)state.vRules.get(i);
                if (r.getInclusion().getTargetDescriptors().contains(rd)) {
                    for(int j=0;j<munmodify.numUpdates();j++) {
-                       UpdateNode un=munmodify.getUpdate(i);
+                       UpdateNode un=munmodify.getUpdate(j);
                        if (un.getRule()==r) {
                            /* Update for rule r */
                            String name=(String)updatenames.get(un);
@@ -967,7 +967,7 @@ public class RepairGenerator {
            munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
            munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
        }
-       int size=ep.leftsize();
+       int size=ep.rightSize();
        VarDescriptor sizevar=VarDescriptor.makeNew("size");
        ((OpExpr)expr).left.generate(cr, sizevar);
        VarDescriptor change=VarDescriptor.makeNew("change");