package MCC.IR;
class AbstractInterferes {
+ static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
+ boolean mayadd=false;
+ boolean mayremove=false;
+ switch (ar.getType()) {
+ case AbstractRepair.ADDTOSET:
+ case AbstractRepair.ADDTORELATION:
+ if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+ return true;
+ mayadd=true;
+ break;
+ case AbstractRepair.REMOVEFROMSET:
+ case AbstractRepair.REMOVEFROMRELATION:
+ if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+ return true;
+ mayremove=true;
+ break;
+ case AbstractRepair.MODIFYRELATION:
+ if (interferesquantifier(ar.getDescriptor(), true, r, satisfy))
+ return true;
+ if (interferesquantifier(ar.getDescriptor(), false, r, satisfy))
+ return true;
+ mayadd=true;
+ mayremove=true;
+ break;
+ default:
+ throw new Error("Unrecognized Abstract Repair");
+ }
+ DNFRule drule=null;
+ if (satisfy)
+ 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++) {
+ DNFExpr dexpr=rconj.get(j);
+ Expr expr=dexpr.getExpr();
+ if (expr.usesDescriptor(ar.getDescriptor())) {
+ /* Need to check */
+ if ((mayadd&&!dexpr.getNegation())||(mayremove&&dexpr.getNegation()))
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+
static public boolean interferes(AbstractRepair ar, DNFPredicate dp) {
if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
((ar.getDescriptor() instanceof SetDescriptor)||
class ConcreteInterferes {
static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+ if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
+ return false;
for(int i=0;i<mun.numUpdates();i++) {
UpdateNode un=mun.getUpdate(i);
for (int j=0;j<un.numUpdates();j++) {
if (satisfy)
drule=r.getDNFNegGuardExpr();
+
if (!update.isAbstract()) {
Descriptor updated_des=update.getDescriptor();
assert updated_des!=null;
+ /* Update is local to this rule, and the effect is intentional */
+ /* If we're adding something, a side effect could be to falsify some other binding
+ If we're removing something, there is no similar side effect */
+ if ((un.getRule()==r)&&
+ (((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
+ (r.numQuantifiers()==1)&&
+ (r.getQuantifier(0) instanceof SetQuantifier)&&
+ update.isField()&&
+ (((DotExpr)update.getLeftExpr()).getExpr() instanceof VarExpr)&&
+ ((SetQuantifier)r.getQuantifier(0)).getVar()==((VarExpr)((DotExpr)update.getLeftExpr()).getExpr()).getVar())
+ continue;
+ if ((un.getRule()==r)&&
+ (((mun.op==MultUpdateNode.ADD)&&satisfy)||(mun.op==MultUpdateNode.REMOVE))&&
+ (r.numQuantifiers()==0))
+ continue;
+
+
if (r.getInclusion().usesDescriptor(updated_des))
return true; /* Interferes with inclusion condition */
for(int k=0;k<drule.size();k++) {
RuleConjunction rconj=drule.get(k);
for(int l=0;l<rconj.size();l++) {
+
+
DNFExpr dexpr=rconj.get(l);
/* See if update interferes w/ dexpr */
if (interferes(un,update, r,dexpr))
return false;
}
+ static private boolean initialinterferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+ AbstractRepair ar=mun.getRepair();
+ if (satisfy)
+ return true;
+ if (ar==null)
+ return true;
+ if (ar.getType()!=AbstractRepair.ADDTOSET)
+ return true;
+ // if (mun.op!=MultUpdateNode.ADD) (Redundant)
+ // return true;
+ if (!r.getInclusion().getTargetDescriptors().contains(ar.getDescriptor()))
+ return true;
+ boolean negated=ar.getPredicate().isNegated();
+ Predicate p=ar.getPredicate().getPredicate();
+ if (!(p instanceof ExprPredicate))
+ return true;
+ ExprPredicate ep=(ExprPredicate)p;
+ if (ep.getType()!=ExprPredicate.SIZE)
+ return true;
+ if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==1)&&!negated)
+ return false;
+ if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==1)&&negated)
+ return false;
+
+ if ((ep.getOp()==Opcode.NE)&&(ep.leftsize()==0)&&!negated)
+ return false;
+ if ((ep.getOp()==Opcode.EQ)&&(ep.leftsize()==0)&&negated)
+ return false;
+
+
+
+ if ((ep.getOp()==Opcode.GT)&&(ep.leftsize()==0)&&!negated)
+ return false;
+ if ((ep.getOp()==Opcode.LE)&&(ep.leftsize()==0)&&negated)
+ return false;
+
+ if ((ep.getOp()==Opcode.GE)&&(ep.leftsize()==1)&&!negated)
+ return false;
+ if ((ep.getOp()==Opcode.LT)&&(ep.leftsize()==1)&&negated)
+ return false;
+
+ return true;
+
+
+ }
+
static private boolean interferes(UpdateNode un,Updates update, Rule r,DNFExpr dexpr) {
Descriptor descriptor=update.getDescriptor();
if (!dexpr.getExpr().usesDescriptor(descriptor))
return false;
+
/* We need to pair the variables */
if (update.isExpr()) {
Set vars=update.getRightExpr().freeVars();
--- /dev/null
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class GraphAnalysis {
+ Termination termination;
+ static final int WORKS=0;
+ static final int ERR_NOREPAIR=1;
+ static final int ERR_CYCLE=2;
+ static final int ERR_RULE=3;
+ static final int ERR_ABSTRACT=4;
+
+ public GraphAnalysis(Termination t) {
+ termination=t;
+ }
+ /* This function checks that
+ 1) All abstract repairs have a corresponding data structure update
+ that isn't removed.
+ 2) All scope nodes have either a consequence node or a compensation
+ node that isn't removed.
+ */
+ public int checkRepairs(Set removed) {
+ Set nodes=new HashSet();
+ nodes.addAll(termination.conjunctions);
+ nodes.removeAll(removed);
+ GraphNode.computeclosure(nodes,removed);
+ Set toretain=new HashSet();
+ toretain.addAll(termination.abstractrepair);
+ toretain.addAll(termination.scopenodes);
+ nodes.retainAll(toretain);
+ /* Nodes is now the reachable set of abstractrepairs */
+ /* Check to see that each has an implementation */
+ for(Iterator it=nodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ if (tn.getType()==TermNode.RULESCOPE) {
+ boolean foundnode=false;
+ for (Iterator edgeit=gn.edges();it.hasNext();) {
+ GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=edge.getTarget();
+ if (!removed.contains(gn2)) {
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()==TermNode.CONSEQUENCE||
+ tn2.getType()==TermNode.UPDATE) {
+ foundnode=true;
+ break;
+ }
+ }
+ }
+ if (!foundnode)
+ return ERR_RULE;
+ } else if (tn.getType()==TermNode.ABSTRACT) {
+ boolean foundnode=false;
+ for (Iterator edgeit=gn.edges();it.hasNext();) {
+ GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=edge.getTarget();
+ if (!removed.contains(gn2)) {
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()==TermNode.UPDATE) {
+ foundnode=true;
+ break;
+ }
+ }
+ }
+ if (!foundnode)
+ return ERR_ABSTRACT;
+ } else throw new Error("Unanticipated Node");
+ }
+ return WORKS;
+ }
+ /* This method checks that all constraints have a conjunction nodes
+ and that there are no bad cycles in the abstract portion of the graph.
+ */
+ public int checkAbstract(Set removed) {
+ Vector constraints=termination.state.vConstraints;
+ for(int i=0;i<constraints.size();i++) {
+ Constraint c=(Constraint)constraints.get(i);
+ Set conjunctionset=(Set)termination.conjunctionmap.get(c);
+
+ boolean foundrepair=false;
+ for(Iterator it=conjunctionset.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ if (!removed.contains(gn)) {
+ foundrepair=true;
+ }
+ }
+ if (!foundrepair)
+ return ERR_NOREPAIR;
+ }
+ Set abstractnodes=new HashSet();
+ abstractnodes.addAll(termination.conjunctions);
+ abstractnodes.removeAll(removed);
+ GraphNode.computeclosure(abstractnodes,removed);
+
+ Set tset=new HashSet();
+ tset.addAll(termination.conjunctions);
+ tset.addAll(termination.abstractrepair);
+ tset.addAll(termination.scopenodes);
+ tset.addAll(termination.consequencenodes);
+ abstractnodes.retainAll(tset);
+ Set cycles=GraphNode.findcycles(abstractnodes);
+
+ for(Iterator it=cycles.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ switch(tn.getType()) {
+ case TermNode.CONJUNCTION:
+ case TermNode.ABSTRACT:
+ return ERR_CYCLE;
+ case TermNode.UPDATE:
+ throw new Error("No Update Nodes should be here");
+ default:
+ }
+ }
+ return WORKS;
+ }
+}
return owner;
}
- public static void computeclosure(Set nodes) {
+ public static void computeclosure(Set nodes, Set removed) {
Stack tovisit=new Stack();
tovisit.addAll(nodes);
while(!tovisit.isEmpty()) {
Edge edge=(Edge)it.next();
GraphNode target=edge.getTarget();
if (!nodes.contains(target)) {
- nodes.add(target);
- tovisit.push(target);
+ if ((removed!=null)&&
+ (!removed.contains(target))) {
+ nodes.add(target);
+ tovisit.push(target);
+ }
}
}
}
i = nodes.iterator();
while (i.hasNext()) {
GraphNode gn = (GraphNode) i.next();
- assert gn.getStatus() != PROCESSING;
+ assert gn.getStatus() != PROCESSING;
if (gn.getStatus() == UNVISITED) {
if (!dfs(gn))
acyclic=false;
while (edges.hasNext()) {
Edge edge = (Edge) edges.next();
GraphNode node = edge.getTarget();
+ if (!nodes.contains(node)) /* Skip nodes which aren't in the set */
+ continue;
if (node.getStatus() == UNVISITED) {
if (!dfs(node))
acyclic=false;
public MultUpdateNode(ScopeNode sn) {
updates=new Vector();
scopenode=sn;
+ op=MultUpdateNode.REMOVE;
}
void addUpdate(UpdateNode un) {
updates.add(un);
return ((RelationInclusion)inc).getRelation();
else throw new Error("Unrecognized Inclusion");
}
+
+ public Rule getRule() {
+ return rule;
+ }
public boolean getSatisfy() {
return satisfy;
}
ScopeNode scope;
MultUpdateNode update;
+ public int getType() {
+ return type;
+ }
+
public TermNode(Constraint constr, Conjunction conj) {
this.constr=constr;
this.conj=conj;
//superset.addAll(updatenodes);
//superset.addAll(scopenodes);
//superset.addAll(consequencenodes);
- GraphNode.computeclosure(superset);
+ GraphNode.computeclosure(superset,null);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} catch (Exception e) {
System.out.println(gn.getTextLabel());
System.out.println(mun.toString());
}
+ GraphAnalysis ga=new GraphAnalysis(this);
}
void generateconjunctionnodes() {
"Conj ("+i+","+j+") "+dnf.get(j).name()
,tn);
conjunctions.add(gn);
- conjunctionmap.put(c,gn);
+ if (!conjunctionmap.containsKey(c))
+ conjunctionmap.put(c,new HashSet());
+ ((Set)conjunctionmap.get(c)).add(gn);
}
}
}
}
}
}
+
+ for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
+ GraphNode gn2=(GraphNode)scopeiterator.next();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ ScopeNode sn2=tn2.getScope();
+ if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+ GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ gn.addEdge(e);
+ }
+ }
}
}
MultUpdateNode mun=new MultUpdateNode(sn);
TermNode tn2=new TermNode(mun);
GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
un.addBindings(bindings);
if (j<r.numQuantifiers()) {
/* Remove quantifier */
boolean goodflag=true;
for(int i=0;i<possiblerules.size();i++) {
Rule r=(Rule)possiblerules.get(i);
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
/* Construct bindings */
Vector bindings=new Vector();
constructbindings(bindings, r,true);
DNFRule dnfrule=r.getDNFGuardExpr();
for(int j=0;j<dnfrule.size();j++) {
Inclusion inc=r.getInclusion();
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
un.addBindings(bindings);
/* Now build update for tuple/set inclusion condition */
if(inc instanceof SetInclusion) {
Vector updates;
Vector bindings;
Hashtable binding;
+ Rule rule;
+
- public UpdateNode() {
+ public UpdateNode(Rule r) {
updates=new Vector();
bindings=new Vector();
binding=new Hashtable();
+ rule=r;
+ }
+
+ public Rule getRule() {
+ return rule;
}
public String toString() {
projects / repair.git / commitdiff