Checking in code that:

1) performs consistency checks
2) doesn abstract repairs
3) calls/schedules data structure updates
4) partially data structure update code

diff --git a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
index 206aeabdb03254cbca5e6d89e38bb3af6b096b3d..ae620fead375b9eb62fd87cf858a0a376404f808 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
@@ -28,6 +28,13 @@ class MultUpdateNode {
        scopenode=sn;
        op=MultUpdateNode.REMOVE;
     }
+
+    public Descriptor getDescriptor() {
+       if (abstractrepair!=null)
+           return abstractrepair.getDescriptor();
+       else
+           return scopenode.getDescriptor();
+    }
     void addUpdate(UpdateNode un) {
        updates.add(un);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 5a2968308ebb750c3522ea3ef18d3f6e036c9fb5..bcf68f565730a2ee8e62c1bddbeaf869ba1b111e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -21,6 +21,7 @@ public class RepairGenerator {
     HashSet usedupdates;
     Termination termination;
     Set removed;
+    HashSet togenerate;
     static boolean DEBUG=false;
     Cost cost;
     Sources sources;
@@ -31,6 +32,11 @@ public class RepairGenerator {
        usedupdates=new HashSet();
        termination=t;
        removed=t.removedset;
+       togenerate=new HashSet();
+        togenerate.addAll(termination.conjunctions);
+        togenerate.removeAll(removed);
+        GraphNode.computeclosure(togenerate,removed);
+
        cost=new Cost();
        sources=new Sources(state);
        Repair.repairgenerator=this;
@@ -42,6 +48,7 @@ public class RepairGenerator {
            GraphNode gn=(GraphNode) it.next();
            TermNode tn=(TermNode) gn.getOwner();
            MultUpdateNode mun=tn.getUpdate();
+           if (togenerate.contains(gn))
            for (int i=0;i<mun.numUpdates();i++) {
                UpdateNode un=mun.getUpdate(i);
                String name="update"+String.valueOf(count++);
@@ -69,9 +76,73 @@ public class RepairGenerator {
        CodeWriter craux = new StandardCodeWriter(this.outputaux);
        crhead.outputline("};");
        craux.outputline("};");
+       generate_updates();
     }
 
-    
+    private void generate_updates() {
+       int count=0;
+        CodeWriter crhead = new StandardCodeWriter(outputhead);        
+        CodeWriter craux = new StandardCodeWriter(outputaux);        
+       String state="state";
+       String model="model";
+       String repairtable="repairtable";
+       String left="left";
+       String right="right";
+       for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode) it.next();
+           TermNode tn=(TermNode) gn.getOwner();
+           MultUpdateNode mun=tn.getUpdate();
+           boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
+           if (togenerate.contains(gn))
+           for (int i=0;i<mun.numUpdates();i++) {
+               UpdateNode un=mun.getUpdate(i);
+               String methodname=(String)updatenames.get(un);
+               
+               switch(mun.op) {
+               case MultUpdateNode.ADD:
+                   if (isrelation) {
+                       crhead.outputline("void "+methodname+"("+name+"_state * " +state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+");");
+                       craux.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+")");
+                   } else {
+                       crhead.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+");");
+                       craux.outputline("void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+")");
+                   }
+                   craux.startblock();
+                   un.generate(craux, false, left,right);
+                   craux.endblock();
+                   break;
+               case MultUpdateNode.REMOVE:
+                   Rule r=un.getRule();
+                   String methodcall="void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable;
+                   for(int j=0;j<r.numQuantifiers();j++) {
+                       Quantifier q=r.getQuantifier(j);
+                       if (q instanceof SetQuantifier) {
+                           SetQuantifier sq=(SetQuantifier) q;
+                           methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
+                       } else if (q instanceof RelationQuantifier) {
+                           RelationQuantifier rq=(RelationQuantifier) q;
+                           
+                           methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
+                           methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
+                       } else if (q instanceof ForQuantifier) {
+                           ForQuantifier fq=(ForQuantifier) q;
+                           methodcall+=",int "+fq.getVar().getSafeSymbol();
+                       }
+                   }
+                   methodcall+=")";
+                   crhead.outputline(methodcall+";");
+                   craux.outputline(methodcall);
+                   craux.startblock();
+                   un.generate(craux, true, null,null);
+                   craux.endblock();
+                   break;
+               case MultUpdateNode.MODIFY:
+               default:
+                   throw new Error("Nonimplement Update");
+               }
+           }
+       }
+    }
 
     private void generate_call() {
         CodeWriter cr = new StandardCodeWriter(outputrepair);        
@@ -513,6 +584,7 @@ public class RepairGenerator {
                            cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
                        else
                            cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
+                       cr.startblock();
                        if (p instanceof InclusionPredicate)
                            generateinclusionrepair(conj,dpred, cr);
                        else if (p instanceof ExprPredicate) {
@@ -522,6 +594,7 @@ public class RepairGenerator {
                            else if (ep.getType()==ExprPredicate.COMPARISON)
                                generatecomparisonrepair(conj,dpred,cr);
                        } else throw new Error("Unrecognized Predicate");
+                       cr.endblock();
                    }
                    /* Update model */
                    
@@ -553,7 +626,6 @@ public class RepairGenerator {
     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
        MultUpdateNode mun=null;
        GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
-
        for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
            GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
            TermNode tn2=(TermNode)gn2.getOwner();
@@ -561,7 +633,7 @@ public class RepairGenerator {
                AbstractRepair ar=tn2.getAbstract();
                if (((repairtype==-1)||(ar.getType()==repairtype))&&
                    ar.getPredicate()==dpred) {
-                   for(Iterator edgeit2=gn2.edges();edgeit.hasNext();) {
+                   for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                        GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
                        if (!removed.contains(gn3)) {
                            TermNode tn3=(TermNode)gn3.getOwner();
@@ -796,8 +868,77 @@ public class RepairGenerator {
            cr.endblock();
        }
        if (generateadd) {
+
            cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
            cr.startblock();
+           VarDescriptor newobject=VarDescriptor.makeNew("newobject");
+           if (d instanceof RelationDescriptor) {
+               VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
+               RelationDescriptor rd=(RelationDescriptor)d;
+               if (sources.relsetSource(rd,!ep.inverted())) {
+                   /* Set Source */
+                   SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
+                   VarDescriptor iterator=VarDescriptor.makeNew("iterator");
+                   cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
+                   cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
+                   cr.startblock();
+                   if (ep.inverted()) {
+                       cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
+                   } else {
+                       cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
+                   }
+                   cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
+                   cr.outputline(iterator.getSafeSymbol()+"->next();");
+                   cr.endblock();
+               } else if (sources.relallocSource(rd,!ep.inverted())) {
+                   /* Allocation Source*/
+                   sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
+               } else throw new Error("No source for adding to Relation");
+               if (ep.inverted()) {
+                   boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+                   boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+                   if (usageimage)
+                       cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+                   if (usageinvimage)
+                       cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+
+                   UpdateNode un=munadd.getUpdate(0);
+                   String name=(String)updatenames.get(un);
+                   cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+               } else {
+                   boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+                   boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+                   if (usageimage)
+                       cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+                   if (usageinvimage)
+                       cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
+                   UpdateNode un=munadd.getUpdate(0);
+                   String name=(String)updatenames.get(un);
+                   cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+               }
+           } else {
+               SetDescriptor sd=(SetDescriptor)d;
+               if (sources.setSource(sd)) {
+                   /* Set Source */
+                   /* Set Source */
+                   SetDescriptor sourcesd=sources.getSourceSet(sd);
+                   VarDescriptor iterator=VarDescriptor.makeNew("iterator");
+                   cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
+                   cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
+                   cr.startblock();
+                   cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
+                   cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
+                   cr.outputline(iterator.getSafeSymbol()+"->next();");
+                   cr.endblock();
+               } else if (sources.allocSource(sd)) {
+                   /* Allocation Source*/
+                   sources.generateSourceAlloc(cr,newobject,sd);
+               } else throw new Error("No source for adding to Set");
+               cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+               UpdateNode un=munadd.getUpdate(0);
+               String name=(String)updatenames.get(un);
+               cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
+           }
            cr.endblock();
        }
     }

diff --git a/Repair/RepairCompiler/MCC/IR/Sources.java b/Repair/RepairCompiler/MCC/IR/Sources.java
index de6d4f37d7d9c31783995775870378622f5edfa4..b37fa1122b0882a6f3d4003c9a9240bdf700c54a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Sources.java
+++ b/Repair/RepairCompiler/MCC/IR/Sources.java
@@ -25,4 +25,27 @@ public class Sources {
        e.generate(cr, size);
        cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
     }
+
+    public boolean relsetSource(RelationDescriptor rd, boolean domain) {
+       return false;
+    }
+    public boolean relallocSource(RelationDescriptor rd, boolean domain) {
+       return true;
+    }
+    public SetDescriptor relgetSourceSet(RelationDescriptor rd, boolean domain) {
+       return null;
+    }
+    public void relgenerateSourceAlloc(CodeWriter cr,VarDescriptor vd, RelationDescriptor rd, boolean domain) {
+       SetDescriptor sd=null;
+       if (domain)
+           sd=rd.getDomain();
+       else
+           sd=rd.getRange();
+       TypeDescriptor td=sd.getType();
+       Expr e=td.getSizeExpr();
+       VarDescriptor size=VarDescriptor.makeNew("size");
+       e.generate(cr, size);
+       cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
+    }
+
 }

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 69f76136e1fb8891105bcf9628b26c207546b5b9..689a5d2382169d166d58fc60a370cb68c663e303 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -273,9 +273,10 @@ public class Termination {
            Rule r=(Rule) state.vRules.get(i);
            Vector possiblerules=new Vector();
            /* Construct bindings */
-           Vector bindings=new Vector();
-           constructbindings(bindings, r,true);
-           
+           /* No need to construct bindings on remove
+              Vector bindings=new Vector();
+              constructbindings(bindings, r,true);
+           */
            for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
                GraphNode gn=(GraphNode)scopesatisfy.get(r);
                TermNode tn=(TermNode) gn.getOwner();
@@ -284,7 +285,8 @@ public class Termination {
                TermNode tn2=new TermNode(mun);
                GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
                UpdateNode un=new UpdateNode(r);
-               un.addBindings(bindings);
+               //              un.addBindings(bindings);
+               // Not necessary
                if (j<r.numQuantifiers()) {
                    /* Remove quantifier */
                    Quantifier q=r.getQuantifier(j);
@@ -384,9 +386,10 @@ public class Termination {
                Rule r=(Rule)possiblerules.get(i);
                UpdateNode un=new UpdateNode(r);
                /* Construct bindings */
-               Vector bindings=new Vector();
-               constructbindings(bindings, r,true);
-               un.addBindings(bindings);
+               /* No Need to construct bindings on remove
+                  Vector bindings=new Vector();
+                  constructbindings(bindings, r,true);
+                 un.addBindings(bindings);*/
                if (count[i]<r.numQuantifiers()) {
                    /* Remove quantifier */
                    Quantifier q=r.getQuantifier(count[i]);

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 5bb92367fb1f67dcd78a77e2e774ee2bf3327ae2..8eee4a87df2375fe27a02939d3cfac165117393d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -193,4 +193,74 @@ class UpdateNode {
     public Updates getUpdate(int i) {
        return (Updates)updates.get(i);
     }
+    public void generate(CodeWriter cr, boolean removal, String slot0, String slot1) {
+       if (!removal)
+           generate_bindings(cr, slot0,slot1);
+       for(int i=0;i<updates.size();i++) {
+           Updates u=(Updates)updates.get(i);
+           VarDescriptor right=VarDescriptor.makeNew("right");
+           if (u.getType()==Updates.ABSTRACT)
+               throw new Error("Abstract update not implemented");
+
+           switch(u.getType()) {
+           case Updates.EXPR:
+               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 throw new Error("Error w/ Position");
+               break;
+           default:
+               throw new Error();
+           }
+           VarDescriptor left=VarDescriptor.makeNew("left");
+           u.getLeftExpr().generate(cr,left);
+           Opcode op=u.getOpcode();
+           cr.outputline("if ("+left.getSafeSymbol()+op+right.getSafeSymbol()+")");
+           cr.startblock();
+
+           if (op==Opcode.GT)
+               cr.outputline(right.getSafeSymbol()+"++;");
+           else if (op==Opcode.GE)
+               ;
+           else if (op==Opcode.EQ)
+               ;
+           else if (op==Opcode.NE)
+               cr.outputline(right.getSafeSymbol()+"++;");
+           else if (op==Opcode.LT)
+               cr.outputline(right.getSafeSymbol()+"--;");
+           else if (op==Opcode.LE)
+               ;
+           else throw new Error();
+           if (u.isGlobal()) {
+               VarDescriptor vd=((VarExpr)u.getLeftExpr()).getVar();
+               cr.outputline(vd.getSafeSymbol()+"="+right.getSafeSymbol()+";");
+           } else if (u.isField()) {
+               /* NEED TO FIX */
+           }
+           cr.endblock();
+           
+       }
+    }
+    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.search)
+               throw new Error("Search not implemented for bindings");
+           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.");
+           }
+       }
+    }
 }