Fixed inteferes bug, improved precision of other analysis to allow

specs to still work.

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 5ae9aaac4beb8b97d73c7e82c051fc533828d4ac..2fe4aeff43261ed0be2fbba1a5e51e10aa19272c 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -98,7 +98,6 @@ class AbstractInterferes {
                    return false;
            }
        }
                    return false;
            }
        }

-

        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
            (dp.getPredicate() instanceof ExprPredicate)&&
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
            (dp.getPredicate() instanceof ExprPredicate)&&


@@ -122,13 +121,12 @@ class AbstractInterferes {
                (op2==Opcode.GT))
                return false;
        }
                (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)) {
        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();
            boolean neg1=ar.getPredicate().isNegated();
            Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
            boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();


@@ -140,7 +138,18 @@ class AbstractInterferes {
            Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
            boolean isInt2=((ExprPredicate)dp.getPredicate()).isRightInt();
            int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
            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;
+           Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+
+           {
+               Expr lexpr1=((RelationExpr)((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).getLeftExpr()).getExpr();
+               Expr lexpr2=((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).getLeftExpr()).getExpr();
+               SetDescriptor sd1=lexpr1.getSet();
+               SetDescriptor sd2=lexpr2.getSet();
+               if (termination.mutuallyexclusive(sd1,sd2))
+                   return false;
+           }
+
+

 
            /* Translate the opcodes */
            op1=Opcode.translateOpcode(neg1,op1);
 
            /* Translate the opcodes */
            op1=Opcode.translateOpcode(neg1,op1);


@@ -152,19 +161,16 @@ class AbstractInterferes {
                ((op2==Opcode.GT)||
                 (op2==Opcode.GE)))
                return false;
                ((op2==Opcode.GT)||
                 (op2==Opcode.GE)))
                return false;

-

            if (((op1==Opcode.LT)||
                (op1==Opcode.LE))&&
                ((op2==Opcode.LT)||
                 (op2==Opcode.LE)))
                return false;
            if (((op1==Opcode.LT)||
                (op1==Opcode.LE))&&
                ((op2==Opcode.LT)||
                 (op2==Opcode.LE)))
                return false;

-               

            if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
                ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
                expr1.equals(null,expr2)) {
                return false;
            }
            if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
                ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
                expr1.equals(null,expr2)) {
                return false;
            }

-

            if (isInt1&&isInt2) {
                if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
                    ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
            if (isInt1&&isInt2) {
                if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
                    ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&


@@ -183,52 +189,42 @@ class AbstractInterferes {
                    size2a++;
                if (op2==Opcode.LT)
                    size2a--;
                    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.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.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.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.LE)||(op2==Opcode.LT))&&
                    (size1a<=size2a))
                    return false;

-

                if ((op1==Opcode.EQ)&&
                    ((op2==Opcode.GE)||(op2==Opcode.GT))&&
                    (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 (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)&&
                    (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.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;
            }
        }
                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)&&
        /* This handles all the c comparisons in the paper */
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&


@@ -277,7 +273,6 @@ class AbstractInterferes {
                (op2==Opcode.LE)||
                (op2==Opcode.LT))
                return false;
                (op2==Opcode.LE)||
                (op2==Opcode.LT))
                return false;

-           

        }
        if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
            (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
        }
        if ((ar.getDescriptor()==dp.getPredicate().getDescriptor())&&
            (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&


@@ -290,7 +285,6 @@ class AbstractInterferes {
            (dp.getPredicate() instanceof InclusionPredicate)&&
            (dp.isNegated()==true))
            return false; /* Could only satisfy this predicate */
            (dp.getPredicate() instanceof InclusionPredicate)&&
            (dp.isNegated()==true))
            return false; /* Could only satisfy this predicate */

-         

        return true;
     }
 
        return true;
     }
 

diff --git a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
index dfdcfb83682ad1610d216a4ec4f394d42e9a092e..cb8f81eca87f58fa0e5d18b3200a70e70b5f8028 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ModelRuleDependence.java
@@ -104,8 +104,17 @@ class ModelRuleDependence {
     private void generateEdge(Rule r1,Rule r2) {
        Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
        int dep=checkBody(d,r2.getDNFGuardExpr());
     private void generateEdge(Rule r1,Rule r2) {
        Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
        int dep=checkBody(d,r2.getDNFGuardExpr());

-       if (dep==NODEPENDENCY)
-           dep=checkQuantifiers(d,r2);
+       if (dep==NODEPENDENCY) {
+           SetDescriptor bsd=null;
+           if (d instanceof SetDescriptor) {
+               SetInclusion si=(SetInclusion)r1.getInclusion();
+               if (si.getExpr() instanceof VarExpr) {
+                   VarDescriptor vd=((VarExpr)si.getExpr()).getVar();
+                   bsd=vd.getSet();
+               }
+           }
+           dep=checkQuantifiers(bsd,d,r2);
+       }

        if (dep==NODEPENDENCY)
            return;
        GraphNode gn1=(GraphNode) ruletonode.get(r1);
        if (dep==NODEPENDENCY)
            return;
        GraphNode gn1=(GraphNode) ruletonode.get(r1);


@@ -138,10 +147,17 @@ class ModelRuleDependence {
            return NODEPENDENCY;
     }
 
            return NODEPENDENCY;
     }
 

-    private int checkQuantifiers(Descriptor d, Quantifiers qs) {
+    private int checkQuantifiers(SetDescriptor bsd, Descriptor d, Quantifiers qs) {

        for (int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);
        for (int i=0;i<qs.numQuantifiers();i++) {
            Quantifier q=qs.getQuantifier(i);

-           if (q.getRequiredDescriptors().contains(d))
+           if (q instanceof SetQuantifier&&
+               d instanceof SetDescriptor) {
+               SetQuantifier sq=(SetQuantifier)q;
+               SetDescriptor sd=(SetDescriptor)d;
+               if (sq.getSet().isSubset(sd)&&
+                   ((bsd==null)||!bsd.isSubset(sq.getSet())))
+                   return NORMDEPENDENCY;
+           } else if (q.getRequiredDescriptors().contains(d))

                return NORMDEPENDENCY;
        }
        return NODEPENDENCY;
                return NORMDEPENDENCY;
        }
        return NODEPENDENCY;

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 23644364db60649b6a49b0e227405be1b741fa91..0dadae2701c75da28594875e956037c7c7950fb6 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -44,7 +44,8 @@ public class OpExpr extends Expr {
 
     public Set getfunctions() {
        Set leftfunctions=left.getfunctions();
 
     public Set getfunctions() {
        Set leftfunctions=left.getfunctions();

-       Set rightfunctions=right.getfunctions();
+       Set rightfunctions=null;
+       if (right!=null) rightfunctions=right.getfunctions();

        if (leftfunctions!=null&&rightfunctions!=null) {
            HashSet functions=new HashSet();
            functions.addAll(leftfunctions);
        if (leftfunctions!=null&&rightfunctions!=null) {
            HashSet functions=new HashSet();
            functions.addAll(leftfunctions);

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 772756717c6de06a60066396f317efa2461bfc34..32b4a1b56866113aee0e9125c231f9a4a84aedd4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -256,6 +256,7 @@ public class Termination {
 
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
 
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);

+                   System.out.println("Checking "+gn.getTextLabel()+" --> "+gn2.getTextLabel());

                    if (AbstractInterferes.interferes(ar,cons)||
                        abstractinterferes.interferes(ar,dp)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                    if (AbstractInterferes.interferes(ar,cons)||
                        abstractinterferes.interferes(ar,dp)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);


@@ -1114,4 +1115,42 @@ public class Termination {
        }
        return true;
     }
        }
        return true;
     }

+
+    public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+       if (mutualexclusive(sd1,sd2)||
+           mutualexclusive(sd2,sd1))
+           return true;
+       else
+           return false;
+    }
+
+    private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
+       Vector rules=state.vRules;
+       for(int i=0;i<rules.size();i++) {
+           Rule r=(Rule)rules.get(i);
+           if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
+               /* Rule may add items to sd1 */
+               SetInclusion si=(SetInclusion)r.getInclusion();
+               Expr ve=si.getExpr();
+               DNFRule drule=r.getDNFGuardExpr();
+               for(int j=0;j<drule.size();j++) {
+                   RuleConjunction rconj=drule.get(j);
+                   boolean containsexclusion=false;
+                   for (int k=0;k<rconj.size();k++) {
+                       DNFExpr dexpr=rconj.get(k);
+                       if (dexpr.getNegation()&&
+                           dexpr.getExpr() instanceof ElementOfExpr&&
+                           ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
+                           SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
+                           if (sd.isSubset(sd2))
+                               containsexclusion=true;
+                       }
+                   }
+                   if (!containsexclusion)
+                       return false;
+               }
+           }
+       }
+       return true;
+    }

 }
 }