X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FRepairGenerator.java;h=0f21555cc39f8cf04682f9f7c6ee3b2d2c75a19e;hp=66f2e38823f49e6a2df178c7ea522f8ef35980e1;hb=67dcbdb36743f6c386db45d66a9e2d17b4a71e43;hpb=2bad0dfb94fcdfc04e3c5725177803e7158158b0

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 66f2e38..0f21555 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -938,9 +938,8 @@ public class RepairGenerator {
 
     private Set getmultupdatenodeset(Conjunction conj, DNFPredicate dpred, int repairtype) {
 	HashSet hs=new HashSet();
-	MultUpdateNode mun=null;
 	GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
-	for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
+	for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 	    GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 	    TermNode tn2=(TermNode)gn2.getOwner();
 	    if (tn2.getType()==TermNode.ABSTRACT) {
@@ -952,7 +951,7 @@ public class RepairGenerator {
 			if (!removed.contains(gn3)) {
 			    TermNode tn3=(TermNode)gn3.getOwner();
 			    if (tn3.getType()==TermNode.UPDATE) {
-				hs.add(mun);
+				hs.add(tn3.getUpdate());
 			    }
 			}
 		    }
@@ -1011,7 +1010,16 @@ public class RepairGenerator {
 	VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 	VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 	VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
-	if (!inverted) {
+	boolean needremoveloop=ar.mayNeedFunctionEnforcement(state)&&ar.needsRemoves(state);
+
+	if (needremoveloop&&((munadd==null)||(munremove==null))) {
+	    System.out.println("Warning:  need to have individual remove operations for"+dpred.name());
+	    needremoveloop=false;
+	}
+	if (needremoveloop)
+	    cr.outputline("while (1) {");
+
+   	if (!inverted) {
 	    ((RelationExpr)expr.getLeftExpr()).getExpr().generate(cr,leftside);
 	    expr.getRightExpr().generate(cr,newvalue);
 	    cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
@@ -1022,22 +1030,8 @@ public class RepairGenerator {
 	    cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 	    cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 	}
-	if (negated)
-	    if (opcode==Opcode.GT) {
-		opcode=Opcode.LE;
-	    } else if (opcode==Opcode.GE) {
-		opcode=Opcode.LT;
-	    } else if (opcode==Opcode.LT) {
-		opcode=Opcode.GE;
-	    } else if (opcode==Opcode.LE) {
-		opcode=Opcode.GT;
-	    } else if (opcode==Opcode.EQ) {
-		opcode=Opcode.NE;
-	    } else if (opcode==Opcode.NE) {
-		opcode=Opcode.EQ;
-	    } else {
-		throw new Error("Unrecognized Opcode");
-	    }
+
+	opcode=Opcode.translateOpcode(negated,opcode);
 
 	if (opcode==Opcode.GT) {
 	    cr.outputline(newvalue.getSafeSymbol()+"++;");
@@ -1057,6 +1051,35 @@ public class RepairGenerator {
 	/* Do abstract repairs */
 	if (usageimage) {
 	    cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
+	}
+	if (usageinvimage) {
+	    cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
+	}
+
+	if (needremoveloop) {
+	    if (!inverted) {
+		cr.outputline("if ("+rd.getSafeSymbol()+"_hash->contains("+leftside.getSafeSymbol()+")) {");
+	    } else {
+		cr.outputline("if ("+rd.getSafeSymbol()+"_hashinv->contains("+rightside.getSafeSymbol()+")) {");
+	    }
+	    for(int i=0;i<state.vRules.size();i++) {
+		Rule r=(Rule)state.vRules.get(i);
+		if (r.getInclusion().getTargetDescriptors().contains(rd)) {
+		    for(int j=0;j<munremove.numUpdates();j++) {
+			UpdateNode un=munremove.getUpdate(i);
+			if (un.getRule()==r) {
+				/* Update for rule r */
+			    String name=(String)updatenames.get(un);
+			    cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
+			}
+		    }
+		}
+	    }
+	    cr.outputline("continue;");
+	    cr.outputline("}");
+	}
+
+	if (usageimage) {
 	    if (!inverted) {
 		cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 	    } else {
@@ -1064,7 +1087,6 @@ public class RepairGenerator {
 	    }
 	}
 	if (usageinvimage) {
-	    cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 	    if (!inverted) {
 		cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 	    } else {
@@ -1072,7 +1094,7 @@ public class RepairGenerator {
 	    }
 	}
 	/* Do concrete repairs */
-	if (munmodify!=null) {
+	if (munmodify!=null&&(!ar.mayNeedFunctionEnforcement(state))||(munadd==null)||(ar.needsRemoves(state)&&(munremove==null))) {
 	    for(int i=0;i<state.vRules.size();i++) {
 		Rule r=(Rule)state.vRules.get(i);
 		if (r.getInclusion().getTargetDescriptors().contains(rd)) {
@@ -1111,6 +1133,10 @@ public class RepairGenerator {
 		cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 	    }
 	}
+	if (needremoveloop) {
+	    cr.outputline("break;");
+	    cr.outputline("}");
+	}
     }
 
     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {