2 bug fixes to getRequiredConstraints
[repair.git] / Repair / RepairCompiler / MCC / IR / UpdateNode.java
index 00ac87f5b7718d0cb37f61f77657afbcc6171097..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) {
@@ -340,17 +391,27 @@ class UpdateNode {
                u.getRightExpr().generate(cr,right);
                break;
            case Updates.POSITION:
-               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");
+           case Updates.ACCESSPATH:
+               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();
            }
+
+           if (u.getType()==Updates.ACCESSPATH) {
+               VarDescriptor newright=VarDescriptor.makeNew("right");
+               generate_accesspath(cr, right,newright,u);
+               right=newright;
+           }
            VarDescriptor left=VarDescriptor.makeNew("left");
            u.getLeftExpr().generate(cr,left);
            Opcode op=u.getOpcode();
@@ -384,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));
@@ -409,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()+";");
@@ -425,22 +486,98 @@ class UpdateNode {
        }
     }
 
+
+    private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
+       Vector dotvector=new Vector();
+       Expr ptr=u.getRightExpr();
+       VarExpr rightve=new VarExpr(right);
+       right.td=ReservedTypeDescriptor.INT;
+
+       while(true) {
+           /* Does something other than a dereference? */
+           dotvector.add(ptr);
+           if (ptr instanceof DotExpr)
+               ptr=((DotExpr)ptr).left;
+           else if (ptr instanceof CastExpr)
+               ptr=((CastExpr)ptr).getExpr();
+           if (ptr instanceof VarExpr) {
+               /* Finished constructing vector */
+               break;
+           }
+       }
+       ArrayAnalysis.AccessPath ap=u.getAccessPath();
+       VarDescriptor init=VarDescriptor.makeNew("init");
+       if (ap.isSet()) {
+           cr.addDeclaration("int", init.getSafeSymbol());
+           cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
+           init.td=ap.getSet().getType();
+       } else {
+           init=ap.getVar();
+       }
+       Expr newexpr=new VarExpr(init);
+       int apindex=0;
+       for(int i=dotvector.size()-1;i>=0;i--) {
+           Expr e=(Expr)dotvector.get(i);
+           if (e instanceof CastExpr) {
+               newexpr.td=e.td;
+               newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
+           } else if (e instanceof DotExpr) {
+               DotExpr de=(DotExpr)e;
+               if (de.getField() instanceof ArrayDescriptor) {
+                   DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
+                   de2.fd=de.fd;
+                   de2.fieldtype=de.fieldtype;
+                   de2.td=de.td;
+                   OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
+                   OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
+                   if (u.getRightPos()==apindex) {
+                       index.generate(cr,newright);
+                       return;
+                   } else {
+                       DotExpr de3=new DotExpr(newexpr,de.field,index);
+                       de3.fd=de.fd;
+                       de3.td=de.td;
+                       de3.fieldtype=de.fieldtype;
+                       newexpr=de3;
+                   }
+               } else {
+                   DotExpr de2=new DotExpr(newexpr,de.field,null);
+                   de2.fd=de.fd;
+                   de2.fieldtype=de.fieldtype;
+                   de2.td=de.td;
+                   newexpr=de2;
+               }
+               apindex++;
+           } else throw new Error();
+       }
+       throw new Error();
+    }
+
     private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
        for(int i=0;i<bindings.size();i++) {
            Binding b=(Binding)bindings.get(i);
-           if (b.getType()!=Binding.POSITION)
-               throw new Error("Only position bindings implemented!");
 
-           VarDescriptor vd=b.getVar();
-           switch(b.getPosition()) {
-           case 0:
-               cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot0+";");
-               break;
-           case 1:
-               cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot1+";");
-               break;
-           default:
-               throw new Error("Slot >1 doesn't exist.");
+           if (b.getType()==Binding.SEARCH) {
+               VarDescriptor vd=b.getVar();
+               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());
+           } else {
+               VarDescriptor vd=b.getVar();
+               switch(b.getPosition()) {
+               case 0:
+                   cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+                   cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
+                   break;
+               case 1:
+                   cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+                   cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
+                   break;
+               default:
+                   throw new Error("Slot >1 doesn't exist.");
+               }
            }
        }
     }