2 bug fixes to getRequiredConstraints
[repair.git] / Repair / RepairCompiler / MCC / IR / UpdateNode.java
index 97ec85278329228bc73a1f1d5b5846f2089f7b88..89ffed905db057b1a0dd553c2269487e0a978e9b 100755 (executable)
@@ -5,13 +5,14 @@ import MCC.State;
 class UpdateNode {
     Vector updates;
     Vector bindings;
+    Vector invariants;
     Hashtable binding;
     Rule rule;
-    
 
     public UpdateNode(Rule r) {
        updates=new Vector();
        bindings=new Vector();
+       invariants=new Vector();
        binding=new Hashtable();
        rule=r;
     }
@@ -22,11 +23,18 @@ class UpdateNode {
 
     public String toString() {
        String st="";
+       st+="Bindings:\n";
        for(int i=0;i<bindings.size();i++)
            st+=bindings.get(i).toString()+"\n";
        st+="---------------------\n";
+       st+="Updates:\n";
        for(int i=0;i<updates.size();i++)
            st+=updates.get(i).toString()+"\n";
+       st+="---------------------\n";
+       st+="Invariants:\n";
+       for(int i=0;i<invariants.size();i++)
+           st+=((Expr)invariants.get(i)).name()+"\n";
+       st+="---------------------\n";
        return st;
     }
 
@@ -36,14 +44,29 @@ class UpdateNode {
        }
     }
 
-    public boolean checkupdates() {
+    public boolean checkupdates(State state) {
        if (!checkconflicts()) /* Do we have conflicting concrete updates */
            return false;
+        if (!checknoupdates(state))
+            return false;
        if (computeordering()) /* Ordering exists */
            return true;
        return false;
     }
 
+    private boolean checknoupdates(State state) {
+        Set noupdate=state.noupdate;
+        for(int i=0;i<updates.size();i++) {
+           Updates u=(Updates)updates.get(i);
+            if (u.isAbstract())
+                continue; /* Abstract updates don't change fields */
+            Descriptor d=u.getDescriptor();
+            if (noupdate.contains(d))
+                return false;
+        }
+        return true;
+    }
+
     private boolean computeordering() {
        /* Build dependency graph between updates */
        HashSet graph=new HashSet();
@@ -63,7 +86,16 @@ class UpdateNode {
                if (!u2.isExpr())
                    continue;
                Descriptor d=u1.getDescriptor();
-               if (u2.getRightExpr().usesDescriptor(d)) {
+               Expr subexpr=null;
+               Expr intindex=null;
+
+               if (u2.isField()) {
+                   subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
+                   intindex=((DotExpr)u2.getLeftExpr()).getIndex();
+               }
+               if (u2.getRightExpr().usesDescriptor(d)||
+                   (subexpr!=null&&subexpr.usesDescriptor(d))||
+                   (intindex!=null&&intindex.usesDescriptor(d))) {
                    /* Add edge for dependency */
                    GraphNode gn1=(GraphNode) mapping.get(u1);
                    GraphNode gn2=(GraphNode) mapping.get(u2);
@@ -98,6 +130,14 @@ class UpdateNode {
        Set toremove=new HashSet();
        for(int i=0;i<updates.size();i++) {
            Updates u1=(Updates)updates.get(i);
+           if (!u1.isAbstract()) {
+               Descriptor d=u1.getDescriptor();
+               for(int j=0;j<invariants.size();j++) {
+                   Expr invariant=(Expr)invariants.get(j);
+                   if (invariant.usesDescriptor(d))
+                       return false;
+               }
+           }
            for(int j=0;j<updates.size();j++) {
                Updates u2=(Updates)updates.get(j);
                if (i==j)
@@ -106,7 +146,7 @@ class UpdateNode {
                    continue;  /* Abstract updates are already accounted for by graph */
                if (u1.getDescriptor()!=u2.getDescriptor())
                    continue; /* No interference - different descriptors */
-               
+
                if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
                    (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
                    continue; /* Can be satisfied simultaneously */
@@ -149,7 +189,7 @@ class UpdateNode {
                        toremove.add(u2);
                    continue;
                }
-               
+
                /* Compatible operations < & <= */
                if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
                    ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
@@ -184,7 +224,7 @@ class UpdateNode {
     public Binding getBinding(int i) {
        return (Binding)bindings.get(i);
     }
-    
+
     public Binding getBinding(VarDescriptor vd) {
        if (binding.containsKey(vd))
            return (Binding)binding.get(vd);
@@ -192,6 +232,18 @@ class UpdateNode {
            return null;
     }
 
+    public void addInvariant(Expr e) {
+       invariants.add(e);
+    }
+
+    public int numInvariants() {
+       return invariants.size();
+    }
+
+    public Expr getInvariant(int i) {
+       return (Expr)invariants.get(i);
+    }
+
     public void addUpdate(Updates u) {
        updates.add(u);
     }
@@ -262,10 +314,10 @@ class UpdateNode {
                boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
                boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
                if (usageimage)
-                   cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
+                   cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
                if (usageinvimage)
-                   cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
-               
+                   cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+
                for(int i=0;i<state.vRules.size();i++) {
                    Rule r=(Rule)state.vRules.get(i);
                    if (r.getInclusion().getTargetDescriptors().contains(rd)) {
@@ -274,14 +326,14 @@ class UpdateNode {
                            if (un.getRule()==r) {
                                /* Update for rule rule r */
                                String name=(String)rg.updatenames.get(un);
-                               cr.outputline(rg.strepairtable+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
+                               cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
                            }
                        }
                    }
                }
            } else {
                SetDescriptor sd=(SetDescriptor) d;
-               cr.outputline(rg.stmodel+"->"+sd.getJustSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+               cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
 
                for(int i=0;i<state.vRules.size();i++) {
                    Rule r=(Rule)state.vRules.get(i);
@@ -291,7 +343,7 @@ class UpdateNode {
                            if (un.getRule()==r) {
                                /* Update for rule rule r */
                                String name=(String)rg.updatenames.get(un);
-                               cr.outputline(rg.strepairtable+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
+                               cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
                            }
                        }
                    }
@@ -304,16 +356,16 @@ class UpdateNode {
                boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
                boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
                if (usageimage)
-                   cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
+                   cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
                if (usageinvimage)
-                   cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+                   cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
 
                UpdateNode un=mun.getUpdate(0);
                String name=(String)rg.updatenames.get(un);
                cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
            } else {
                SetDescriptor sd=(SetDescriptor)d;
-               cr.outputline(rg.stmodel+"->"+sd.getJustSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+               cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
 
                UpdateNode un=mun.getUpdate(0);
                /* Update for rule rule r */
@@ -321,7 +373,6 @@ class UpdateNode {
                cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
            }
        }
-       
     }
 
     public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
@@ -341,13 +392,16 @@ class UpdateNode {
                break;
            case Updates.POSITION:
            case Updates.ACCESSPATH:
-               if (u.getRightPos()==0)
-                   cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
-               else if (u.getRightPos()==1)
-                   cr.outputline("int "+right.getSafeSymbol()+"="+slot1+";");
-               else if (u.getRightPos()==2)
-                   cr.outputline("int "+right.getSafeSymbol()+"="+slot2+";");
-               else throw new Error("Error w/ Position");
+               if (u.getRightPos()==0) {
+                   cr.addDeclaration("int", right.getSafeSymbol());
+                   cr.outputline(right.getSafeSymbol()+"="+slot0+";");
+               } else if (u.getRightPos()==1) {
+                   cr.addDeclaration("int", right.getSafeSymbol());
+                   cr.outputline(right.getSafeSymbol()+"="+slot1+";");
+               } else if (u.getRightPos()==2) {
+                   cr.addDeclaration("int", right.getSafeSymbol());
+                   cr.outputline(right.getSafeSymbol()+"="+slot2+";");
+               } else throw new Error("Error w/ Position");
                break;
            default:
                throw new Error();
@@ -391,11 +445,11 @@ class UpdateNode {
                    intindex.generate(cr,indexvd);
                FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
                StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
+               Expr offsetbits = std.getOffsetExpr(fd);
                if (fd instanceof ArrayDescriptor) {
                    fd = ((ArrayDescriptor) fd).getField();
                }
 
-               Expr offsetbits = std.getOffsetExpr(fd);
                if (intindex != null) {
                    Expr basesize = fd.getBaseSizeExpr();
                    offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
@@ -416,7 +470,7 @@ class UpdateNode {
                    } else if (rtd==ReservedTypeDescriptor.BIT) {
                        Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
                        Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
-                       Expr mask=new OpExpr(Opcode.SHR, new IntegerLiteralExpr(1), offset);
+                       Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
                        VarDescriptor maskvar=VarDescriptor.makeNew("mask");
                        mask.generate(cr,maskvar);
                        cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
@@ -454,7 +508,8 @@ class UpdateNode {
        ArrayAnalysis.AccessPath ap=u.getAccessPath();
        VarDescriptor init=VarDescriptor.makeNew("init");
        if (ap.isSet()) {
-           cr.outputline("int "+init.getSafeSymbol()+"="+ap.getSet().getSafeSymbol()+"_hash->firstkey();");
+           cr.addDeclaration("int", init.getSafeSymbol());
+           cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
            init.td=ap.getSet().getType();
        } else {
            init=ap.getVar();
@@ -504,7 +559,8 @@ class UpdateNode {
 
            if (b.getType()==Binding.SEARCH) {
                VarDescriptor vd=b.getVar();
-               cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+b.getSet().getSafeSymbol()+"->firstkey();");
+               cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+               cr.outputline(vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
            } else if (b.getType()==Binding.CREATE) {
                throw new Error("Creation not supported");
                //              source.generateSourceAlloc(cr,vd,b.getSet());
@@ -512,10 +568,12 @@ class UpdateNode {
                VarDescriptor vd=b.getVar();
                switch(b.getPosition()) {
                case 0:
-                   cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot0+";");
+                   cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+                   cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
                    break;
                case 1:
-                   cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot1+";");
+                   cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+                   cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
                    break;
                default:
                    throw new Error("Slot >1 doesn't exist.");