Added support to printout data structure update nodes (bindings/updates)
authorbdemsky <bdemsky>
Thu, 5 Feb 2004 07:18:20 +0000 (07:18 +0000)
committerbdemsky <bdemsky>
Thu, 5 Feb 2004 07:18:20 +0000 (07:18 +0000)
Added support to simplify updates/determine if they are self consistent
Added support to sequence updates
Improved precision of data structure update analysis

18 files changed:
Repair/RepairCompiler/MCC/IR/Binding.java
Repair/RepairCompiler/MCC/IR/CastExpr.java
Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/ElementOfExpr.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/GraphNode.java
Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
Repair/RepairCompiler/MCC/IR/IntegerLiteralExpr.java
Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/RelationExpr.java
Repair/RepairCompiler/MCC/IR/SizeofExpr.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/TupleOfExpr.java
Repair/RepairCompiler/MCC/IR/UpdateNode.java
Repair/RepairCompiler/MCC/IR/Updates.java
Repair/RepairCompiler/MCC/IR/VarExpr.java

index 652c849..163f237 100755 (executable)
@@ -20,5 +20,10 @@ class Binding {
     VarDescriptor getVar() {
        return var;
     }
-
+    public String toString() {
+       if (search)
+           return "SEARCHFOR"+var.toString();
+       else
+           return var.toString()+"="+String.valueOf(position);
+    }
 }
index 4ccc637..88fde6d 100755 (executable)
@@ -7,6 +7,10 @@ public class CastExpr extends Expr {
     TypeDescriptor type;
     Expr expr;
 
+    public Set freeVars() {
+       return expr.freeVars();
+    }
+
     public CastExpr(TypeDescriptor type, Expr expr) {
         this.type = type;
         this.expr = expr;
index 9419563..c4855bc 100755 (executable)
@@ -1,4 +1,5 @@
 package MCC.IR;
+import java.util.*;
 
 class ConcreteInterferes {
     static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
@@ -22,11 +23,8 @@ class ConcreteInterferes {
                        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;
                        }
                    }
                }
@@ -34,4 +32,79 @@ class ConcreteInterferes {
        }
        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;
+    }
 }
index a380f4e..93beabc 100755 (executable)
@@ -8,6 +8,18 @@ public class DotExpr extends Expr {
     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;
 
index 1fdf42a..49b0064 100755 (executable)
@@ -7,6 +7,10 @@ public class ElementOfExpr extends Expr {
     Expr element;
     SetDescriptor set;
 
+    public Set freeVars() {
+       return element.freeVars();
+    }
+
     public ElementOfExpr(Expr element, SetDescriptor set) {
         if (element == null || set == null) {
             throw new NullPointerException();
index 6be665b..ab7cbee 100755 (executable)
@@ -53,5 +53,13 @@ public abstract class Expr {
        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;
+    }
 }
index da50a5a..5a3a85b 100755 (executable)
@@ -144,13 +144,13 @@ public class GraphNode {
     }
 
     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;
     }
 
@@ -158,6 +158,7 @@ public class GraphNode {
         return finishingtime;
     }
 
+
     public static class DOTVisitor {
         
         java.io.PrintWriter output;
@@ -194,19 +195,22 @@ public class GraphNode {
                          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();
@@ -219,6 +223,49 @@ public class GraphNode {
             }
         }
     }
+
+    /* 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 
@@ -232,19 +279,19 @@ public class GraphNode {
             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();
@@ -256,12 +303,15 @@ public class GraphNode {
                 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();
 
@@ -269,12 +319,16 @@ public class GraphNode {
                 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 */
 
index 152a4f8..2a61df6 100755 (executable)
@@ -14,6 +14,12 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = false;
     }
 
+    public Set freeVars() {
+       HashSet hs=new HashSet();
+       hs.add(vd);
+       return hs;
+    }
+
     public String name() {
        String name=vd.toString()+".";
        if (inverse)
index e3f0d73..f906386 100755 (executable)
@@ -18,6 +18,10 @@ public class IntegerLiteralExpr extends LiteralExpr {
        return (new Integer(value)).toString();
     }
 
+    public boolean isNull() {
+       return value==0;
+    }
+
     public boolean equals(Map remap, Expr e) {
        if (e==null)
            return false;
index 033c8d6..94c109b 100755 (executable)
@@ -16,6 +16,13 @@ class MultUpdateNode {
        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;
index 8f6aa59..5325c3b 100755 (executable)
@@ -16,6 +16,26 @@ public class OpExpr extends Expr {
         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()+")";
index 543b8e7..1b7336a 100755 (executable)
@@ -14,6 +14,10 @@ public class RelationExpr extends Expr {
         this.inverse = inverse;
     }
 
+    public Set freeVars() {
+       return expr.freeVars();
+    }
+
     public String name() {
        String name=expr.name()+".";
        if (inverse)
index 7570ddc..ec72e3f 100755 (executable)
@@ -6,6 +6,10 @@ public class SizeofExpr extends Expr {
 
     SetExpr setexpr;
 
+    public Set freeVars() {
+       return setexpr.freeVars();
+    }
+
     public SizeofExpr(SetExpr setexpr) {
         if (setexpr == null) {
             throw new NullPointerException();
index 271d9f2..f3d134f 100755 (executable)
@@ -47,17 +47,24 @@ public class Termination {
 
        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() {
@@ -180,7 +187,7 @@ public class Termination {
                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);
@@ -294,7 +301,9 @@ public class Termination {
                        continue;
                    }
                }
-
+               if (!un.checkupdates()) /* Make sure we have a good update */
+                   continue;
+               
                mun.addUpdate(un);
 
                GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
@@ -392,6 +401,10 @@ public class Termination {
                        goodflag=false;break;
                    }
                }
+               if (!un.checkupdates()) {
+                   goodflag=false;
+                   break;
+               }
                mun.addUpdate(un);
            }
            if (goodflag) {
@@ -593,7 +606,8 @@ public class Termination {
                    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);
index f0ccb85..941b37a 100755 (executable)
@@ -8,6 +8,16 @@ public class TupleOfExpr extends Expr {
     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();
index 4cf7d54..16388e0 100755 (executable)
@@ -12,18 +12,88 @@ class UpdateNode {
        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())
@@ -36,13 +106,62 @@ class UpdateNode {
                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) {
index 2c83ad6..5e3652b 100755 (executable)
@@ -12,15 +12,14 @@ class Updates {
     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) {
@@ -41,23 +40,8 @@ class Updates {
            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() {
@@ -66,7 +50,18 @@ class Updates {
        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()) {
@@ -87,6 +82,10 @@ class Updates {
            return false;
     }
     
+    boolean isExpr() {
+       return type==Updates.EXPR;
+    }
+
     
     Opcode getOpcode() {
        return opcode;
index 82cd341..ff52366 100755 (executable)
@@ -8,6 +8,12 @@ public class VarExpr extends Expr {
     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; 
     }
@@ -28,6 +34,10 @@ public class VarExpr extends Expr {
        return false;
     }
 
+    public boolean isNonNull() {
+       return true;
+    }
+
     public boolean equals(Map remap, Expr e) {
        if (e==null||!(e instanceof VarExpr))
            return false;
@@ -37,7 +47,7 @@ public class VarExpr extends Expr {
        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;