From: bdemsky <bdemsky>
Date: Wed, 25 Feb 2004 22:38:02 +0000 (+0000)
Subject: Checking in code that:
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=9c7a7b2df517d61e4e4e2431c005e152bd45e35c

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 206aeab..ae620fe 100755
--- 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 5a29683..bcf68f5 100755
--- 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 de6d4f3..b37fa11 100755
--- 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 69f7613..689a5d2 100755
--- 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 5bb9236..8eee4a8 100755
--- 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.");
+	    }
+	}
+    }
 }