node elimination.
return expr.freeVars();
}
+ public Expr getExpr() {
+ return expr;
+ }
+
public void findmatch(Descriptor d, Set s) {
expr.findmatch(d,s);
}
leftdescriptor=((VarExpr)lexpr2).getVar();
else if (lexpr2 instanceof DotExpr) {
Expr e=lexpr2;
- for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ do {
+ for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ if (e instanceof VarExpr)
+ break;
+ if (e instanceof CastExpr)
+ e=((CastExpr)e).getExpr();
+ else throw new Error("Bad Expr Type:"+e.name());
+ } while (true);
leftdescriptor=((VarExpr)e).getVar();
} else throw new Error("Bad Expr");
package MCC.IR;
import java.util.*;
+import java.io.*;
import MCC.State;
public class GraphAnalysis {
couldremove.addAll(optionalabstractrepair);
couldremove.retainAll(cycles);
-
/* Look for constraints which can only be satisfied one way */
Vector constraints=termination.state.vConstraints;
}
/* Search through conjunction which must be satisfied, and attempt
- to generate appropriate repair actions
+ to generate appropriate repair actions.
*/
HashSet newset=new HashSet();
for(Iterator cit=cantremove.iterator();cit.hasNext();) {
if (termination.conjunctions.contains(gn))
return null; // Out of luck
}
-
-
+
+ /* Search through abstract repair actions & correspond data structure updates */
+ for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()!=TermNode.UPDATE)
+ continue;
+
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
+
+ cantremove.add(gn);
+ cantremove.add(gn2);
+
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn2)) {
+ if (!mustremove.contains(gn2)) {
+ change=true;
+ mustremove.add(gn2);
+ }
+ }
+
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
+ }
+ }
+
+ /* Searches individual conjunctions + abstract action +updates for cycles */
for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
boolean foundnocycle=false;
if (tn3.getType()!=TermNode.UPDATE)
continue;
boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
boolean containsgn3=cantremove.contains(gn3);
cantremove.add(gn);
+ cantremove.add(gn2);
cantremove.add(gn3);
Set cycle=GraphNode.findcycles(cantremove);
if (cycle.contains(gn3)) {
}
if (!containsgn)
cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
if (!containsgn3)
cantremove.remove(gn3);
}
}
}
}
+
+ /* Searches scope nodes + compensation nodes */
+ for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ boolean foundcompensation=false;
+ if (nodes.contains(gn)) {
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+
+ if (tn2.getType()!=TermNode.UPDATE)
+ continue;
+ /* We have a compensation node */
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
+ cantremove.add(gn);
+ cantremove.add(gn2);
+
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn2)) {
+ if (!mustremove.contains(gn2)) {
+ change=true;
+ mustremove.add(gn2);
+ }
+ } else {
+ if (!mustremove.contains(gn2))
+ foundcompensation=true;
+ }
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
+ }
+ }
+ if (!foundcompensation) {
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()==TermNode.UPDATE) {
+ cantremove.add(gn2);
+ break;
+ }
+ }
+ }
+ }
couldremove.removeAll(mustremove);
couldremove.removeAll(cantremove);
if(change)
continue; //recalculate
+ try {
+ GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
+ } catch (Exception e) {
+ e.printStackTrace();
+ System.exit(-1);
+ }
+
System.out.println("Searching set of "+couldremove.size()+" nodes.");
System.out.println("Eliminated must "+mustremove.size()+" nodes");
System.out.println("Eliminated cant "+cantremove.size()+" nodes");
Hashtable conjunctionmap;
HashSet abstractrepair;
+ HashSet abstractrepairadd;
+
HashSet updatenodes;
HashSet consequencenodes;
conjunctions=new HashSet();
conjunctionmap=new Hashtable();
abstractrepair=new HashSet();
+ abstractrepairadd=new HashSet();
scopenodes=new HashSet();
scopesatisfy=new Hashtable();
scopefalsify=new Hashtable();
predtoabstractmap.put(tp,new HashSet());
((Set)predtoabstractmap.get(tp)).add(gn);
abstractrepair.add(gn);
+ abstractrepairadd.add(gn);
abstractadd.put(sd,gn);
DNFPredicate tp2=new DNFPredicate(true,ip);
predtoabstractmap.put(tp2,new HashSet());
((Set)predtoabstractmap.get(tp2)).add(gn2);
abstractrepair.add(gn2);
+ abstractrepairadd.add(gn2);
abstractremove.put(sd,gn2);
}
predtoabstractmap.put(tp,new HashSet());
((Set)predtoabstractmap.get(tp)).add(gn);
abstractrepair.add(gn);
+ abstractrepairadd.add(gn);
abstractadd.put(rd,gn);
DNFPredicate tp2=new DNFPredicate(true,ip);
predtoabstractmap.put(tp2,new HashSet());
((Set)predtoabstractmap.get(tp2)).add(gn2);
abstractrepair.add(gn2);
+ abstractrepairadd.add(gn2);
abstractremove.put(rd,gn2);
}
}
RelationInclusion ri=(RelationInclusion)r.getInclusion();
if (!(ri.getLeftExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getLeftExpr(),leftindex);
- un.addUpdate(up);
+ if (ri.getLeftExpr().isValue()) {
+ Updates up=new Updates(ri.getLeftExpr(),leftindex);
+ un.addUpdate(up);
+ } else
+ goodflag=false;
} else {
VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
if (vd.isGlobal()) {
goodflag=false;
}
if (!(ri.getRightExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getRightExpr(),rightindex);
- un.addUpdate(up);
+ if (ri.getRightExpr().isValue()) {
+ Updates up=new Updates(ri.getRightExpr(),rightindex);
+ un.addUpdate(up);
+ } else
+ goodflag=false;
} else {
VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
if (vd.isGlobal()) {
if(inc instanceof SetInclusion) {
SetInclusion si=(SetInclusion)inc;
if (!(si.elementexpr instanceof VarExpr)) {
- Updates up=new Updates(si.elementexpr,0);
- un.addUpdate(up);
+ if (si.elementexpr.isValue()) {
+ Updates up=new Updates(si.elementexpr,0);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(si.elementexpr,0);
un.addUpdate(up);
}
} else if (inc instanceof RelationInclusion) {
RelationInclusion ri=(RelationInclusion)inc;
if (!(ri.getLeftExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getLeftExpr(),0);
- un.addUpdate(up);
+ if (ri.getLeftExpr().isValue()) {
+ Updates up=new Updates(ri.getLeftExpr(),0);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(ri.getLeftExpr(),0);
un.addUpdate(up);
}
}
if (!(ri.getRightExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getRightExpr(),1);
- un.addUpdate(up);
+ if (ri.getRightExpr().isValue()) {
+ Updates up=new Updates(ri.getRightExpr(),1);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(ri.getRightExpr(),1);
un.addUpdate(up);
}
return ((VarExpr)leftexpr).getVar();
} else if (isField()) {
Expr e=leftexpr;
- for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ do {
+ for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ if (e instanceof VarExpr)
+ break;
+ if (e instanceof CastExpr)
+ e=((CastExpr)e).getExpr();
+ else throw new Error("Unrecognized Expr:"+e.name());
+ } while(true);
return ((VarExpr)e).getVar();
} else {
System.out.println(toString());