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();
+ if (freevars!=null)
+ 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) {
//)
return false;
+
+ // If the update changes something in the middle of a size
+ // expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
+ (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
+ return true;
+ }
+
+ // If the update changes something in the middle of a
+ // comparison expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
+ (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
+ return true;
+ }
+
/* This if handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
return false;
}
}
+
+ /* This if handles all the c comparisons in the paper */
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (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();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
+ int size1a=0;
+ if((op1==Opcode.EQ)||(op1==Opcode.GE))
+ size1a=size1;
+ if((op1==Opcode.GT)||(op1==Opcode.NE))
+ size1a=size1+1;
+ if (size1a==size2)
+ 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.SIZE)) {
+ int size1=1;
+
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op2==Opcode.EQ)&&(size1==size2))||
+ ((op2==Opcode.NE)&&(size1!=size2))||
+ ((op2==Opcode.GE)&&(size1>=size2))||
+ ((op2==Opcode.GT)&&(size1>size2))||
+ ((op2==Opcode.LE)&&(size1<=size2))||
+ ((op2==Opcode.LT)&&(size1<size2)))
+ return false;
+ }
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
(op2==Opcode.GT))
return false;
}
+
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.MODIFYRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
((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))&&
}
}
+ /* This handles all the c comparisons in the paper */
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (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();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
+ int size1a=0;
+
+ if((op1==Opcode.EQ)||(op1==Opcode.LE))
+ size1a=size1;
+ if((op1==Opcode.LT)||(op1==Opcode.NE))
+ size1a=size1-1;
+
+ if (size1a==size2)
+ return false;
+ }
+ }
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
projects / repair.git / blobdiff