+
+ /** Check to see if performing the repair ar on repair_c does not
+ * inferere with interfere_c. Returns true if there is no
+ * interference. */
+
+ public boolean interferemodifies(AbstractRepair ar, Constraint repair_c, DNFPredicate interfere_pred, Constraint interfere_c) {
+ DNFConstraint precondition=repair_c.getDNFConstraint().not();
+ if (repair_c.numQuantifiers()!=1||
+ interfere_c.numQuantifiers()!=1||
+ !(repair_c.getQuantifier(0) instanceof SetQuantifier)||
+ !(interfere_c.getQuantifier(0) instanceof SetQuantifier)||
+ ((SetQuantifier)repair_c.getQuantifier(0)).getSet()!=((SetQuantifier)interfere_c.getQuantifier(0)).getSet())
+ return false;
+
+ Hashtable mapping=new Hashtable();
+ mapping.put(((SetQuantifier)repair_c.getQuantifier(0)).getVar(),
+ ((SetQuantifier)interfere_c.getQuantifier(0)).getVar());
+
+ if (ar.getType()!=AbstractRepair.MODIFYRELATION||
+ !(ar.getPredicate().getPredicate() instanceof ExprPredicate)||
+ !(interfere_pred.getPredicate() instanceof ExprPredicate))
+ return false;
+ Expr e=((ExprPredicate)interfere_pred.getPredicate()).expr;
+ Expr leftside=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).left;
+ Set relationset=e.useDescriptor(ar.getDescriptor());
+ for(Iterator relit=relationset.iterator();relit.hasNext();) {
+ Expr e2=(Expr)relit.next();
+ if (!leftside.equals(mapping,e2))
+ return false;
+ }
+ /* Prune precondition using any ar's in the same conjunction */
+ adjustcondition(precondition, ar);
+ Conjunction conj=findConjunction(repair_c.getDNFConstraint(),ar.getPredicate());
+ for(int i=0;i<conj.size();i++) {
+ DNFPredicate dp=conj.get(i);
+ Set s=(Set)termination.predtoabstractmap.get(dp);
+ for(Iterator it=s.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ AbstractRepair dp_ar=tn.getAbstract();
+ adjustcondition(precondition, dp_ar);
+ }
+ }
+ /* We now have precondition after interference */
+ if (precondition.size()==0)
+ return false;
+ DNFConstraint infr_const=interfere_c.getDNFConstraint();
+
+ next_conj:
+ for(int i=0;i<infr_const.size();i++) {
+ Conjunction infr_conj=infr_const.get(i);
+ for(int j=0;j<infr_conj.size();j++) {
+ DNFPredicate infr_dp=infr_conj.get(j);
+ next_pre_conj:
+ for(int i2=0;i2<precondition.size();i2++) {
+ Conjunction pre_conj=precondition.get(i2);
+ for(int j2=0;j2<pre_conj.size();j2++) {
+ DNFPredicate pre_dp=pre_conj.get(j2);
+ if (checkPreEnsures(pre_dp,infr_dp,mapping))
+ continue next_pre_conj;
+
+ }
+ continue next_conj; /* The precondition doesn't ensure this conjunction is true */
+ }
+ }
+ return true; /*Found a conjunction that must be
+ true...therefore the precondition
+ guarantees that the second constraint is
+ always true after repair*/
+ }
+ return false;
+ }
+
+ static private Conjunction findConjunction(DNFConstraint cons, DNFPredicate dp) {
+ for(int i=0;i<cons.size();i++) {
+ Conjunction conj=cons.get(i);
+ for(int j=0;j<conj.size();j++) {
+ DNFPredicate curr_dp=conj.get(j);
+ if (curr_dp==dp)
+ return conj;
+ }
+ }
+ throw new Error("Not found");
+ }
+
+ /** This method removes predicates that the abstract repair may
+ * violate. */
+
+ private void adjustcondition(DNFConstraint precond, AbstractRepair ar) {
+ HashSet conjremove=new HashSet();
+ for(int i=0;i<precond.size();i++) {
+ Conjunction conj=precond.get(i);
+ HashSet toremove=new HashSet();
+ for(int j=0;j<conj.size();j++) {
+ DNFPredicate dp=conj.get(j);
+ if (interfereswithpredicate(ar,dp)) {
+ /* Remove dp from precond */
+ toremove.add(dp);
+ }
+ }
+ conj.predicates.removeAll(toremove);
+ if (conj.size()==0)
+ conjremove.add(conj);
+ }
+ precond.conjunctions.removeAll(conjremove);
+ }
+
+ private boolean checkPreEnsures(DNFPredicate pre_dp, DNFPredicate infr_dp, Hashtable mapping) {
+ if (pre_dp.isNegated()==infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
+ (infr_dp.getPredicate() instanceof ExprPredicate)) {
+ if (((ExprPredicate)pre_dp.getPredicate()).expr.equals(mapping, ((ExprPredicate)infr_dp.getPredicate()).expr))
+ return true;
+ }
+ if ((!pre_dp.isNegated())&&infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
+ (infr_dp.getPredicate() instanceof ExprPredicate)) {
+ ExprPredicate pre_ep=(ExprPredicate)pre_dp.getPredicate();
+ ExprPredicate infr_ep=(ExprPredicate)infr_dp.getPredicate();
+ if (pre_ep.getType()==ExprPredicate.COMPARISON&&
+ infr_ep.getType()==ExprPredicate.COMPARISON&&
+ pre_ep.isRightInt()&&
+ infr_ep.isRightInt()&&
+ pre_ep.rightSize()!=infr_ep.rightSize()&&
+ pre_ep.getOp()==Opcode.EQ&&
+ infr_ep.getOp()==Opcode.EQ) {
+ if (((OpExpr)pre_ep.expr).left.equals(mapping,((OpExpr)infr_ep.expr).left))
+ return true;
+ }
+ }
+ return false;
+ }
+
projects / repair.git / commitdiff