termination=t;
}
+
/** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
* Rule r. */
drule=r.getDNFGuardExpr();
else
drule=r.getDNFNegGuardExpr();
-
+
for(int i=0;i<drule.size();i++) {
RuleConjunction rconj=drule.get(i);
for(int j=0;j<rconj.size();j++) {
return false;
}
+ /** This method is designed to check that modifying a relation
+ * doesn't violate a relation well-formedness constraint
+ * (ie. [forall <a,b> in R], a in S1 and b in S2; */
+
public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
if (c.numQuantifiers()==1&&
(c.getQuantifier(0) instanceof RelationQuantifier)) {
return false;
}
+
+ /** 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;
+ }
+
/** 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 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)) {
return false;
}
- /** Does performing the AbstractRepair ar falsify the predicate dp */
+ /** Returns true if performing the AbstractRepair ar may falsify
+ the predicate dp. */
public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
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))||
(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 size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
-
+
/* If the left sides of the comparisons are both from
different sets, the update is orthogonal to the expr dp */
{
/* Translate the opcodes */
op1=Opcode.translateOpcode(neg1,op1);
op2=Opcode.translateOpcode(neg2,op2);
-
+
/* Obvious cases which can't interfere */
if (((op1==Opcode.GT)||
(op1==Opcode.GE))&&
size1a--;
if (op1==Opcode.NE)
size1a++; /*FLAGNE this is current behavior for NE repairs */
-
+
if (op2==Opcode.GT)
size2a++;
if (op2==Opcode.LT)
(op2==Opcode.LE)||
(op2==Opcode.LT))
return false;
- }
+ }
}
if ((des==dp.getPredicate().getDescriptor())&&
satisfy&&
import java.util.*;
public class Constraint implements Quantifiers {
-
+
private static int count = 1;
String label = null;
boolean crash = false;
SymbolTable st = new SymbolTable();
- Vector quantifiers = new Vector();
+ Vector quantifiers = new Vector();
LogicStatement logicstatement = null;
DNFConstraint dnfconstraint;
int num;
label = new String("c" + count++);
}
+ public DNFConstraint getDNFConstraint() {
+ return dnfconstraint;
+ }
+
public String toString() {
String name="";
for(int i=0;i<numQuantifiers();i++) {
public LogicStatement getLogicStatement() {
return logicstatement;
}
-
+
public void setCrash(boolean crash) {
this.crash = crash;
}
HashSet topdescriptors = new HashSet();
- for (int i = 0; i < quantifiers.size(); i++) {
+ for (int i = 0; i < quantifiers.size(); i++) {
Quantifier q = (Quantifier) quantifiers.elementAt(i);
topdescriptors.addAll(q.getRequiredDescriptors());
}
}
public Set getRequiredDescriptorsFromLogicStatement() {
-
+
HashSet topdescriptors = new HashSet();
topdescriptors.addAll(logicstatement.getRequiredDescriptors());
return SetDescriptor.expand(topdescriptors);
}
-
+
public Set getRequiredDescriptors() {
Set set = getRequiredDescriptorsFromQuantifiers();
set.addAll(getRequiredDescriptorsFromLogicStatement());
return set;
}
}
-
return new DNFConstraint(vector);
}
+ public DNFConstraint copyminus(Conjunction c) {
+ Vector vector=new Vector();
+ for (int i=0;i<size();i++) {
+ Conjunction cur_conj=get(i);
+ if (c!=cur_conj)
+ vector.add(cur_conj.copy());
+ }
+ return new DNFConstraint(vector);
+ }
+
public DNFConstraint and(DNFConstraint c) {
DNFConstraint newdnf=new DNFConstraint();
for(int i=0;i<size();i++) {
predtoabstractmap=new Hashtable();
if (!Compiler.REPAIR)
return;
-
+
for(int i=0;i<state.vRules.size();i++)
System.out.println(state.vRules.get(i));
DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
HashSet superset=new HashSet();
Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
-
+
if (di.conjunctionnum==-1) {
superset.addAll((Set)conjunctionmap.get(constr));
} else {
DNFConstraint dnf=constr.dnfconstraint;
superset.add(conjtonodemap.get(dnf.get(di.conjunctionnum)));
}
-
+
GraphNode.boundedcomputeclosure(superset,null,di.depth);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+(di.conjunctionnum==-1?"":"-"+di.conjunctionnum)+".dot"),superset);
}
/* Cycle through the rules to look for possible conflicts */
for(int i=0;i<state.vRules.size();i++) {
- Rule r=(Rule) state.vRules.get(i);
+ Rule r=(Rule) state.vRules.get(i);
if (concreteinterferes.interferes(mun,r,true)) {
GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
GraphNode gn=(GraphNode)absiterator.next();
TermNode tn=(TermNode)gn.getOwner();
AbstractRepair ar=(AbstractRepair)tn.getAbstract();
-
+
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
GraphNode gn2=(GraphNode)conjiterator.next();
TermNode tn2=(TermNode)gn2.getOwner();
Constraint cons=tn2.getConstraint();
/* See if this is a relation wellformedness constraint
that is trivially satisfied. */
- System.out.println(gn.getTextLabel()+"---"+gn2.getTextLabel());
if (abstractinterferes.checkrelationconstraint(ar, cons))
continue;
-
- for(int i=0;i<conj.size();i++) {
- DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferesquantifier(ar,cons)||
- abstractinterferes.interfereswithpredicate(ar,dp)) {
- GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
- gn.addEdge(e);
- break;
- }
- }
+ if (AbstractInterferes.interferesquantifier(ar,cons)) {
+ GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ gn.addEdge(e);
+ } else {
+ for(int i=0;i<conj.size();i++) {
+ DNFPredicate dp=conj.get(i);
+ if (getConstraint(gn)!=null&&
+ abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons))
+ continue;
+
+ if (abstractinterferes.interfereswithpredicate(ar,dp)) {
+ GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ gn.addEdge(e);
+ break;
+ }
+ }
+ }
}
for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
GraphNode gn2=(GraphNode)scopeiterator.next();
}
}
+ Constraint getConstraint(GraphNode gn) {
+ for(Iterator it=gn.inedges();it.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)it.next();
+ GraphNode gnsource=e.getSource();
+ TermNode tnsource=(TermNode)gnsource.getOwner();
+ if (tnsource.getType()==TermNode.CONJUNCTION) {
+ return tnsource.getConstraint();
+ }
+ }
+ return null;
+ }
+
void generatescopenodes() {
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule) state.vRules.get(i);
scopenodes.add(gnfalsify);
}
}
-
+
void generatescopeedges() {
for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
GraphNode gn=(GraphNode)scopeiterator.next();
TermNode tn=(TermNode)gn.getOwner();
ScopeNode sn=tn.getScope();
-
+
/* Interference edges with conjunctions */
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
GraphNode gn2=(GraphNode)conjiterator.next();
abstractrepair.add(gn);
abstractrepairadd.add(gn);
abstractadd.put(sd,gn);
-
+
DNFPredicate tp2=new DNFPredicate(true,ip);
AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd,sources);
TermNode tn2=new TermNode(ar2);
VarExpr ve2=new VarExpr("DUMMY2");
InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
-
+
DNFPredicate tp=new DNFPredicate(false,ip);
AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd,sources);
TermNode tn=new TermNode(ar);
abstractrepair.add(gn);
abstractrepairadd.add(gn);
abstractadd.put(rd,gn);
-
+
DNFPredicate tp2=new DNFPredicate(true,ip);
AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd,sources);
TermNode tn2=new TermNode(ar2);
}
if (!un.checkupdates()) /* Make sure we have a good update */
continue;
-
+
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
compensationcount++;
}
if (possiblerules.size()==0)
return;
-
+
/* Loop through different ways of falsifying each of these rules */
int[] count=new int[possiblerules.size()];
while(remains(count,possiblerules,true)) {
mun.addUpdate(un);
}
if (goodflag) {
- GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
- removefromcount++;
+ GraphNode.Edge e=new GraphNode.Edge("abstract"+(removefromcount++),gn2);
gn.addEdge(e);
updatenodes.add(gn2);
}
int rightindex=1;
if (inverted)
leftindex=2;
- else
+ else
rightindex=2;
// construct set of possible rules
while(remains(count,possiblerules,false)) {
MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
TermNode tn=new TermNode(mun);
- GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
+ GraphNode gn2=new GraphNode("UpdateMod"+modifycount,tn);
boolean goodflag=true;
for(int i=0;i<possiblerules.size();i++) {
Rule r=(Rule)possiblerules.get(i);
UpdateNode un=new UpdateNode(r);
-
+
int c=count[i];
if (!processconjunction(un,r.getDNFGuardExpr().get(c),null)) {
goodflag=false;break;
if (vd.isGlobal()) {
Updates up=new Updates(ri.getRightExpr(),rightindex,null);
un.addUpdate(up);
- } else if (!inverted)
+ } else if (!inverted)
goodflag=false;
}
-
+
if (!un.checkupdates()) {
goodflag=false;
break;
ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
(r.getInclusion() instanceof RelationInclusion&&
ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
-
+
/* First solve for quantifiers */
Vector bindings=new Vector();
/* Construct bindings */
if(inc instanceof SetInclusion) {
SetInclusion si=(SetInclusion)inc;
Expr e=si.elementexpr;
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=si.getSet().getType())
RelationInclusion ri=(RelationInclusion)inc;
Expr e=ri.getLeftExpr();
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=ri.getRelation().getDomain().getType())
un.addUpdate(up);
}
}
-
+
e=ri.getRightExpr();
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=ri.getRelation().getRange().getType())
if (set==null)
continue;
ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
-
+
if (rap==ArrayAnalysis.AccessPath.NONE||
!rap.equal(ap)||
!constructarrayupdate(un, e, rap, 1))
for (int i=ap.numFields()-1;i>=0;i--) {
if (e==null)
e=lexpr;
- else
+ else
e=((DotExpr)e).getExpr();
while (e instanceof CastExpr)
return false;
e=ce.getExpr();
}
-
+
if ((e instanceof VarExpr)&&
(((VarExpr)e).getVar()==vd)) {
/* Can solve for v */
return false;
e=ce.getExpr();
}
-
+
if ((e instanceof VarExpr)&&
(((VarExpr)e).getVar()==vd)) {
/* Can solve for v */
return false;
e=ce.getExpr();
}
-
+
if ((e instanceof VarExpr)&&
(((VarExpr)e).getVar()==vd)) {
/* Can solve for v */
SetInclusion si=(SetInclusion)inc;
Expr e=si.elementexpr;
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=td)
Expr e=ri.getLeftExpr();
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=ri.getRelation().getDomain().getType())
e=ri.getRightExpr();
-
+
while(e instanceof CastExpr) {
CastExpr ce=(CastExpr)e;
if (ce.getType()!=ri.getRelation().getRange().getType())
}
return goodupdate;
}
-
+
/** Adds updates that add an item to the appropriate set or
* relation quantified over by the model definition rule.. */
-
+
boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r,Hashtable setmapping) {
Inclusion inc=r.getInclusion();
for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
} else if (e instanceof TupleOfExpr) {
Updates up=new Updates(e,de.getNegation());
un.addUpdate(up);
- } else if (e instanceof BooleanLiteralExpr) {
+ } else if (e instanceof BooleanLiteralExpr) {
boolean truth=((BooleanLiteralExpr)e).getValue();
if (de.getNegation())
truth=!truth;
projects / repair.git / commitdiff