VarDescriptor getVar() {
return var;
}
-
+ public String toString() {
+ if (search)
+ return "SEARCHFOR"+var.toString();
+ else
+ return var.toString()+"="+String.valueOf(position);
+ }
}
TypeDescriptor type;
Expr expr;
+ public Set freeVars() {
+ return expr.freeVars();
+ }
+
public CastExpr(TypeDescriptor type, Expr expr) {
this.type = type;
this.expr = expr;
package MCC.IR;
+import java.util.*;
class ConcreteInterferes {
static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
for(int l=0;l<rconj.size();l++) {
DNFExpr dexpr=rconj.get(l);
/* See if update interferes w/ dexpr */
-
- if (!dexpr.getExpr().usesDescriptor(updated_des))
- continue; /* No use of the descriptor */
-
- return true;
+ if (interferes(un,update, r,dexpr))
+ return true;
}
}
}
}
return false;
}
+
+ 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();
+ Opcode op1=update.getOpcode();
+ Expr lexpr1=update.getLeftExpr();
+ Expr rexpr1=update.getRightExpr();
+ boolean good=true;
+ for(Iterator it=vars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (un.getBinding(vd)!=null) {
+ /* VarDescriptor isn't a global */
+ if (update.getVar()!=vd) {
+ good=false;
+ break;
+ }
+ }
+ }
+ if (good&&(dexpr.getExpr() instanceof OpExpr)) {
+ OpExpr expr=(OpExpr)dexpr.getExpr();
+ Expr lexpr2=expr.getLeftExpr();
+ Expr rexpr2=expr.getRightExpr();
+ Opcode op2=expr.getOpcode();
+ if (dexpr.getNegation()) {
+ /* remove negation through opcode translation */
+ if (op2==Opcode.GT)
+ op2=Opcode.LE;
+ else if (op2==Opcode.GE)
+ op2=Opcode.LT;
+ else if (op2==Opcode.EQ)
+ op2=Opcode.NE;
+ else if (op2==Opcode.NE)
+ op2=Opcode.EQ;
+ else if (op2==Opcode.LT)
+ op2=Opcode.GE;
+ else if (op2==Opcode.LE)
+ op2=Opcode.GT;
+ }
+ good=true;
+ vars=rexpr2.freeVars();
+ VarDescriptor leftdescriptor=null;
+ if (lexpr2 instanceof VarExpr)
+ leftdescriptor=((VarExpr)lexpr2).getVar();
+ else if (lexpr2 instanceof DotExpr) {
+ Expr e=lexpr2;
+ for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ leftdescriptor=((VarExpr)e).getVar();
+ } else throw new Error("Bad Expr");
+
+ for(Iterator it=vars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (un.getBinding(vd)!=null) {
+ /* VarDescriptor isn't a global */
+ if (leftdescriptor!=vd) {
+ good=false;
+ break;
+ }
+ }
+ }
+ if (good) {
+ HashMap remap=new HashMap();
+ remap.put(update.getVar(),leftdescriptor);
+ if ((op1==op2)&&
+ lexpr1.equals(remap,lexpr2)&&
+ rexpr1.equals(remap,rexpr2))
+ return false;
+ }
+ }
+ }
+ return true;
+ }
}
String field;
Expr index;
+ public Set freeVars() {
+ Set lset=left.freeVars();
+ Set iset=null;
+ if (index!=null)
+ iset=index.freeVars();
+ if (lset==null)
+ return iset;
+ if (iset!=null)
+ lset.addAll(iset);
+ return lset;
+ }
+
/*
static int memoryindents = 0;
Expr element;
SetDescriptor set;
+ public Set freeVars() {
+ return element.freeVars();
+ }
+
public ElementOfExpr(Expr element, SetDescriptor set) {
if (element == null || set == null) {
throw new NullPointerException();
System.out.println(this.getClass().getName());
throw new Error("UNIMPLEMENTED");
}
-
+ public boolean isNull() {
+ return false;
+ }
+ public boolean isNonNull() {
+ return false;
+ }
+ public Set freeVars() {
+ return null;
+ }
}
}
public void discover(int time) {
- discoverytime = time++;
+ discoverytime = time;
status = PROCESSING;
}
public void finish(int time) {
assert status == PROCESSING;
- finishingtime = time++;
+ finishingtime = time;
status = FINISHED;
}
return finishingtime;
}
+
public static class DOTVisitor {
java.io.PrintWriter output;
output.println("\tremincross=true;");*/
output.println("\tnode [fontsize=10,height=\"0.1\", width=\"0.1\"];");
output.println("\tedge [fontsize=6];");
-
traverse();
-
output.println("}\n");
}
private void traverse() {
+ Set cycleset=GraphNode.findcycles(nodes);
+
Iterator i = nodes.iterator();
while (i.hasNext()) {
GraphNode gn = (GraphNode) i.next();
Iterator edges = gn.edges();
String label = gn.getTextLabel(); // + " [" + gn.discoverytime + "," + gn.finishingtime + "];";
- output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + "];");
+ String option="";
+ if (cycleset.contains(gn))
+ option=",style=bold";
+ output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];");
while (edges.hasNext()) {
Edge edge = (Edge) edges.next();
}
}
}
+
+ /* XXXXXXXX Should use SCC algorithm here - will change */
+ public static Set findcycles(Collection nodes) {
+ Stack st=new Stack();
+ HashSet acyclic=new HashSet();
+ HashSet cycles=new HashSet();
+ for(Iterator it=nodes.iterator();it.hasNext();) {
+ GraphNode node=(GraphNode)it.next();
+ if (acyclic.contains(node))
+ continue;
+ if (cycles.contains(node))
+ continue;
+ findcycles(cycles, acyclic, st,node,nodes);
+ }
+ return cycles;
+ }
+
+ private static boolean findcycles(Set cycles, Set acyclic, Stack visited, GraphNode gn, Collection nodes) {
+ if (visited.contains(gn)) {/* Found cycle */
+ cycles.addAll(visited.subList(visited.indexOf(gn),visited.size())); /* Add this cycle */
+ return true;
+ }
+ boolean acyclicflag=true;
+ visited.push(gn);
+ for(Iterator it=gn.edges();it.hasNext();) {
+ Edge e=(Edge) it.next();
+ GraphNode node = e.getTarget();
+ if (!nodes.contains(node))
+ continue; /* Don't visit stuff outside set */
+ if (acyclic.contains(node))
+ continue;
+ if (findcycles(cycles,acyclic,visited,node,nodes)) {
+ /* Found cycle */
+ acyclicflag=false;
+ }
+ }
+ visited.pop();
+ if (acyclicflag) {
+ acyclic.add(gn); /* no cycles through gn */
+ return false;
+ } else
+ return true; /* found cycle */
+ }
/**
* DFS encapsulates the depth first search algorithm
this.nodes = nodes;
}
- public static void depthFirstSearch(Collection nodes) {
+ public static boolean depthFirstSearch(Collection nodes) {
if (nodes == null) {
throw new NullPointerException();
}
DFS dfs = new DFS(nodes);
- dfs.go();
+ return dfs.go();
}
- private void go() {
+ private boolean go() {
Iterator i;
time = 0;
-
+ boolean acyclic=true;
i = nodes.iterator();
while (i.hasNext()) {
GraphNode gn = (GraphNode) i.next();
GraphNode gn = (GraphNode) i.next();
assert gn.getStatus() != PROCESSING;
if (gn.getStatus() == UNVISITED) {
- dfs(gn);
+ if (!dfs(gn))
+ acyclic=false;
}
}
+ return acyclic;
}
- private void dfs(GraphNode gn) {
+ private boolean dfs(GraphNode gn) {
+ boolean acyclic=true;
gn.discover(time++);
Iterator edges = gn.edges();
Edge edge = (Edge) edges.next();
GraphNode node = edge.getTarget();
if (node.getStatus() == UNVISITED) {
- dfs(node);
- }
+ if (!dfs(node))
+ acyclic=false;
+ } else if (node.getStatus()==PROCESSING) {
+ acyclic=false;
+ }
}
gn.finish(time++);
- }
+ return acyclic;
+ }
} /* end DFS */
this.inverse = false;
}
+ public Set freeVars() {
+ HashSet hs=new HashSet();
+ hs.add(vd);
+ return hs;
+ }
+
public String name() {
String name=vd.toString()+".";
if (inverse)
return (new Integer(value)).toString();
}
+ public boolean isNull() {
+ return value==0;
+ }
+
public boolean equals(Map remap, Expr e) {
if (e==null)
return false;
this.op=op;
}
+ public String toString() {
+ String st="";
+ for(int i=0;i<updates.size();i++)
+ st+=updates.get(i).toString()+"OR\n";
+ return st;
+ }
+
public MultUpdateNode(ScopeNode sn) {
updates=new Vector();
scopenode=sn;
assert (right == null && opcode == Opcode.NOT) || (right != null);
}
+ public Expr getRightExpr() {
+ return right;
+ }
+
+ public Expr getLeftExpr() {
+ return left;
+ }
+
+ public Set freeVars() {
+ Set lset=left.freeVars();
+ Set rset=null;
+ if (right!=null)
+ rset=right.freeVars();
+ if (lset==null)
+ return rset;
+ if (rset!=null)
+ lset.addAll(rset);
+ return lset;
+ }
+
public String name() {
if (opcode==Opcode.NOT)
return "!("+left.name()+")";
this.inverse = inverse;
}
+ public Set freeVars() {
+ return expr.freeVars();
+ }
+
public String name() {
String name=expr.name()+".";
if (inverse)
SetExpr setexpr;
+ public Set freeVars() {
+ return setexpr.freeVars();
+ }
+
public SizeofExpr(SetExpr setexpr) {
if (setexpr == null) {
throw new NullPointerException();
HashSet superset=new HashSet();
superset.addAll(conjunctions);
- superset.addAll(abstractrepair);
+ //superset.addAll(abstractrepair);
//superset.addAll(updatenodes);
//superset.addAll(scopenodes);
//superset.addAll(consequencenodes);
- //GraphNode.computeclosure(superset);
+ GraphNode.computeclosure(superset);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} catch (Exception e) {
e.printStackTrace();
System.exit(-1);
}
+ for(Iterator it=updatenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ MultUpdateNode mun=tn.getUpdate();
+ System.out.println(gn.getTextLabel());
+ System.out.println(mun.toString());
+ }
}
void generateconjunctionnodes() {
for(int j=0;j<array.length;j++) {
AbstractRepair ar=new AbstractRepair(dp,array[j],d);
TermNode tn2=new TermNode(ar);
- GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
+ GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
gn.addEdge(e);
abstractrepair.add(gn2);
continue;
}
}
-
+ if (!un.checkupdates()) /* Make sure we have a good update */
+ continue;
+
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
goodflag=false;break;
}
}
+ if (!un.checkupdates()) {
+ goodflag=false;
+ break;
+ }
mun.addUpdate(un);
}
if (goodflag) {
GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
if (processquantifers(gn2,un, r)&&debugdd()&&
- processconjunction(un,ruleconj)) {
+ processconjunction(un,ruleconj)&&
+ un.checkupdates()) {
//System.out.println("Attempting to generate add to set #5");
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
Expr right = null;
RelationDescriptor relation = null;
+ public Set freeVars() {
+ Set lset=left.freeVars();
+ Set rset=right.freeVars();
+ if (lset==null)
+ return rset;
+ if (rset!=null)
+ lset.addAll(rset);
+ return lset;
+ }
+
public TupleOfExpr(Expr left, Expr right, RelationDescriptor relation) {
if ((left == null) || (right == null) || (relation == null)) {
throw new NullPointerException();
binding=new Hashtable();
}
+ public String toString() {
+ String st="";
+ for(int i=0;i<bindings.size();i++)
+ st+=bindings.get(i).toString()+"\n";
+ st+="---------------------\n";
+ for(int i=0;i<updates.size();i++)
+ st+=updates.get(i).toString()+"\n";
+ return st;
+ }
+
public void addBindings(Vector v) {
for (int i=0;i<v.size();i++) {
- bindings.add((Binding)v.get(i));
+ addBinding((Binding)v.get(i));
+ }
+ }
+
+ public boolean checkupdates() {
+ if (!checkconflicts()) /* Do we have conflicting concrete updates */
+ return false;
+ if (computeordering()) /* Ordering exists */
+ return true;
+ return false;
+ }
+
+ private boolean computeordering() {
+ /* Build dependency graph between updates */
+ HashSet graph=new HashSet();
+ Hashtable mapping=new Hashtable();
+ for(int i=0;i<updates.size();i++) {
+ Updates u=(Updates)updates.get(i);
+ GraphNode gn=new GraphNode(String.valueOf(i),u);
+ mapping.put(u, gn);
+ graph.add(gn);
+ }
+ for(int i=0;i<updates.size();i++) {
+ Updates u1=(Updates)updates.get(i);
+ if (u1.isAbstract())
+ continue;
+ for(int j=0;j<updates.size();j++) {
+ Updates u2=(Updates)updates.get(j);
+ if (!u2.isExpr())
+ continue;
+ Descriptor d=u1.getDescriptor();
+ if (u2.getRightExpr().usesDescriptor(d)) {
+ /* Add edge for dependency */
+ GraphNode gn1=(GraphNode) mapping.get(u1);
+ GraphNode gn2=(GraphNode) mapping.get(u2);
+ GraphNode.Edge e=new GraphNode.Edge("dependency",gn2);
+ gn1.addEdge(e);
+ }
+ }
}
+
+ if (!GraphNode.DFS.depthFirstSearch(graph)) /* DFS & check for acyclicity */
+ return false;
+
+ TreeSet topologicalsort = new TreeSet(new Comparator() {
+ public boolean equals(Object obj) { return false; }
+ public int compare(Object o1, Object o2) {
+ GraphNode g1 = (GraphNode) o1;
+ GraphNode g2 = (GraphNode) o2;
+ return g2.getFinishingTime() - g1.getFinishingTime();
+ }
+ });
+ topologicalsort.addAll(graph);
+ Vector sortedvector=new Vector();
+ for(Iterator sort=topologicalsort.iterator();sort.hasNext();) {
+ GraphNode gn=(GraphNode)sort.next();
+ sortedvector.add(gn.getOwner());
+ }
+ updates=sortedvector; //replace updates with the sorted array
+ return true;
}
- public boolean checkconflicts() {
+ private boolean checkconflicts() {
Set toremove=new HashSet();
for(int i=0;i<updates.size();i++) {
Updates u1=(Updates)updates.get(i);
for(int j=0;j<updates.size();j++) {
Updates u2=(Updates)updates.get(j);
+ if (i==j)
+ continue;
if (u1.isAbstract()||u2.isAbstract())
continue; /* Abstract updates are already accounted for by graph */
if (u1.getDescriptor()!=u2.getDescriptor())
if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
(u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
continue;
+ if ((u1.getOpcode()==u2.getOpcode())&&
+ u1.isExpr()&&u2.isExpr()&&
+ u1.getRightExpr().equals(null, u2.getRightExpr())) {
+ /*We'll remove the second occurence*/
+ if (i>j)
+ toremove.add(u1);
+ else
+ toremove.add(u2);
+ continue;
+ }
+
+ /* Handle = or != NULL */
+ if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
+ ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
+ (((u1.isExpr()&&u1.getRightExpr().isNull())&&(!u2.isExpr()||u2.getRightExpr().isNonNull()))
+ ||((!u1.isExpr()||u1.getRightExpr().isNonNull())&&(u2.isExpr()&&u2.getRightExpr().isNull())))) {
+ if (u1.getOpcode()==Opcode.NE)
+ toremove.add(u1);
+ else
+ toremove.add(u2);
+ continue;
+ }
+
+ /* Handle = and != to different constants */
+ if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
+ ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
+ (u1.isExpr()&&u1.getRightExpr() instanceof LiteralExpr)&&
+ (u2.isExpr()&&u2.getRightExpr() instanceof LiteralExpr)&&
+ !u1.getRightExpr().equals(u2.getRightExpr())) {
+ if (u1.getOpcode()==Opcode.NE)
+ toremove.add(u1);
+ else
+ toremove.add(u2);
+ continue;
+ }
-
+ /* Compatible operations < & <= */
+ if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
+ ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
+ continue;
+
+ /* Compatible operations > & >= */
+ if (((u1.getOpcode()==Opcode.GT)||(u1.getOpcode()==Opcode.GE))&&
+ ((u2.getOpcode()==Opcode.GT)||(u2.getOpcode()==Opcode.GE)))
+ continue;
+ /* Ranges */
+
+ //XXXXXX: TODO
+ /* Equality & Comparisons */
+ //XXXXXX: TODO
+
return false; /* They interfere */
}
}
- updates.remove(toremove);
- return false;
+ updates.removeAll(toremove);
+ return true;
}
public void addBinding(Binding b) {
boolean negate=false;
public String toString() {
- String st="type="+type+"\n";
- st+="rightposition="+rightposition+"\n";
- if (rightexpr!=null)
- st+="rightexpr="+rightexpr.name()+"\n";
- if (leftexpr!=null)
- st+="leftexpr="+leftexpr.name()+"\n";
- st+="opcode="+opcode+"\n";
- st+="negate="+negate+"\n";
- return st;
+ if (type==EXPR)
+ return leftexpr.name()+opcode.toString()+rightexpr.name();
+ else if (type==POSITION)
+ return leftexpr.name()+opcode.toString()+"Position("+String.valueOf(rightposition)+")";
+ else if (type==ABSTRACT) {
+ if (negate) return "!"+leftexpr.name();
+ else return leftexpr.name();
+ } else throw new Error("Unrecognized type");
}
public Updates(Expr lexpr, Expr rexpr, Opcode op, boolean negate) {
else if (op==Opcode.LE)
op=Opcode.GT;
}
-
- opcode=Opcode.EQ;
- /* Get rid of everything but NE */
- if (op==Opcode.GT) {
- rightexpr=new OpExpr(Opcode.ADD,rexpr,new IntegerLiteralExpr(1));
- } else if (op==Opcode.GE) {
- rightexpr=rexpr;
- } else if (op==Opcode.LT) {
- rightexpr=new OpExpr(Opcode.SUB,rexpr,new IntegerLiteralExpr(1));
- } else if (op==Opcode.LE) {
- rightexpr=rexpr;
- } else if (op==Opcode.EQ) {
- rightexpr=rexpr;
- } else if (op==Opcode.NE) {
- rightexpr=rexpr;
- opcode=Opcode.NE;
- }
+ opcode=op;
+ rightexpr=rexpr;
}
boolean isGlobal() {
else return false;
}
-
+ VarDescriptor getVar() {
+ if (isGlobal()) {
+ return ((VarExpr)leftexpr).getVar();
+ } else if (isField()) {
+ Expr e=leftexpr;
+ for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ;
+ return ((VarExpr)e).getVar();
+ } else {
+ System.out.println(toString());
+ throw new Error("Unrecognized Update");
+ }
+ }
Descriptor getDescriptor() {
if (isGlobal()) {
return false;
}
+ boolean isExpr() {
+ return type==Updates.EXPR;
+ }
+
Opcode getOpcode() {
return opcode;
VarDescriptor vd = null;
boolean typechecked = false;
+ public Set freeVars() {
+ HashSet hs=new HashSet();
+ hs.add(vd);
+ return hs;
+ }
+
public VarExpr(String varname) {
this.varname = varname;
}
return false;
}
+ public boolean isNonNull() {
+ return true;
+ }
+
public boolean equals(Map remap, Expr e) {
if (e==null||!(e instanceof VarExpr))
return false;
if (ve.vd==null)
throw new Error("e has uninitialized VarDescriptor");
VarDescriptor nvd=vd;
- if (remap.containsKey(nvd))
+ if (remap!=null&&remap.containsKey(nvd))
nvd=(VarDescriptor)remap.get(nvd);
if (nvd!=ve.vd)
return false;
projects / repair.git / commitdiff