Fixed some analysis problems...

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 359dcc7a1dfe448d5590d174b4ab098c730ac274..3e534324ee6a97d6fd0cbbfeed523e50769cd45e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -99,6 +99,77 @@ class AbstractInterferes {
        return false;
     }
 
+    /** This method checks whether a modify relation abstract repair
+     * to satisfy ar may violate dp.  It returns true if there is no
+     * interference. */
+
+    private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
+       boolean neg1=ar.isNegated();
+       Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
+       Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;    
+       Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
+       RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
+       
+       boolean neg2=dp.isNegated();
+       Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+       Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
+       Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
+       
+       /* Translate the opcodes */
+       op1=Opcode.translateOpcode(neg1,op1);
+       op2=Opcode.translateOpcode(neg2,op2);
+       
+       if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
+           ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
+           !rexpr2.usesDescriptor(updated_des)) {
+           Hashtable varmap=new Hashtable();
+           Expr l1=lexpr1;
+           Expr l2=lexpr2;
+
+           boolean initialrelation=true;
+           boolean onetoone=true;
+           while(true) {
+               if ((l1 instanceof VarExpr)&&
+                   (l2 instanceof VarExpr)) {
+                   VarDescriptor vd1=((VarExpr)l1).getVar();
+                   VarDescriptor vd2=((VarExpr)l2).getVar();
+                   varmap.put(vd1,vd2);
+                   break;
+               } else if ((l1 instanceof RelationExpr)&&
+                          (l2 instanceof RelationExpr)) {
+                   RelationExpr re1=(RelationExpr)l1;
+                   RelationExpr re2=(RelationExpr)l2;
+                   if (re1.getRelation()!=re2.getRelation()||
+                       re1.inverted()!=re2.inverted())
+                       return false;
+
+                   if (!initialrelation) {
+                       if (!(
+                             ConstraintDependence.rulesensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)||
+                             ConstraintDependence.constraintsensurefunction(termination.state, re1.getRelation(),re1.getExpr().getSet(),!re1.inverted(),true)))
+                           onetoone=false;
+                       //need check one-to-one property here
+                   } else initialrelation=false;
+                   l1=re1.getExpr();
+                   l2=re2.getExpr();
+               } else return false; // bad match
+           }
+           Set freevars=rexpr1.freeVars();
+           for(Iterator it=freevars.iterator();it.hasNext();) {
+               VarDescriptor vd=(VarDescriptor)it.next();
+               if (vd.isGlobal())
+                   continue; //globals are fine
+               else if (varmap.containsKey(vd)&&onetoone) //the mapped variable is fine if we have a 1-1 mapping
+                   continue;
+               else if (termination.maxsize.getsize(vd.getSet())==1)
+                   continue;
+               return false;
+           }
+           return rexpr1.equals(varmap,rexpr2);
+       }
+       return false;
+    }
+
     /** Does performing the AbstractRepair ar falsify the predicate dp */
 
     public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
@@ -210,13 +281,10 @@ class AbstractInterferes {
                ((op2==Opcode.LT)||
                 (op2==Opcode.LE)))
                return false;
-           // FIXME
-           if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
-               ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
-               expr1.equals(null,expr2)) {
-               // Need to check free variables...
+
+           if (interferemodifies(ar.getPredicate(),dp))
                return false;
-           }
+
            if (isInt1&&isInt2) {
                if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
                    ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index 1d32666322f3c4bf40cbb47e3bfc52f7de922a20..d7f9a023a8f940e809342cf7af77e876367827ba 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -170,7 +170,7 @@ class AbstractRepair {
        SetDescriptor sd=getPredicate().getPredicate().inverted()?getRangeSet():getDomainSet(); 
        if (ConstraintDependence.rulesensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(), false))
            return false;
-       if (ConstraintDependence.constraintsensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted()))
+       if (ConstraintDependence.constraintsensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(),false))
            return false;
        return true;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index c36d9138d585ef5a923966863af49e7d3767d5e1..d6dc251382ff1a89bb786aab0759d52beb656d44 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -217,6 +217,10 @@ public class ConstraintDependence {
     }
  
     static private Set providesfunction(State state, Function f) {
+       return providesfunction(state,f,false);
+    }
+
+    static private Set providesfunction(State state, Function f, boolean isPartial) {
        HashSet set=new HashSet();
        for(int i=0;i<state.vConstraints.size();i++) {
            Constraint c=(Constraint)state.vConstraints.get(i);
@@ -233,7 +237,7 @@ public class ConstraintDependence {
                        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
                        if (ep.isRightInt()&&
                            ep.rightSize()==1&&
-                           ep.getOp()==Opcode.EQ&&
+                           (ep.getOp()==Opcode.EQ||(ep.getOp()==Opcode.LE&&isPartial))&&
                            ep.inverted()==f.isInverse()&&
                            ep.getDescriptor()==f.getRelation()) {
                            ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
@@ -279,8 +283,8 @@ public class ConstraintDependence {
      * evaluated on the domain sd is either a function (if
      * isPartial=false) or a partial function (if isPartial=true). */
 
-    static public boolean constraintsensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse) {
-       Set constraints=providesfunction(state, new Function(r,sd,inverse,null));
+    static public boolean constraintsensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse,boolean isPartial) {
+       Set constraints=providesfunction(state, new Function(r,sd,inverse,null),isPartial);
        return (!constraints.isEmpty());
     }