From 7f5349f8ce0cad85a83e9485b3d083296f9f7737 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Thu, 22 Apr 2004 20:55:30 +0000
Subject: [PATCH] Added code to correctly order checks...

Added code to search through sets for bindings of size 1.
---
 .../MCC/IR/ConstraintDependence.java          | 88 ++++++++++++++++---
 Repair/RepairCompiler/MCC/IR/ExactSize.java   |  9 +-
 .../MCC/IR/RepairGenerator.java               |  9 +-
 Repair/RepairCompiler/MCC/IR/Termination.java | 27 ++++--
 Repair/RepairCompiler/MCC/IR/UpdateNode.java  | 30 ++++---
 5 files changed, 126 insertions(+), 37 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 49d4cb9..7ae89cb 100755
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -18,10 +18,29 @@ public class ConstraintDependence {
 	constonode=new Hashtable();
 	nodetonode=new Hashtable();
 	constructnodes();
-	constructconjunctionnodes();
-	constructconjunctionedges();
     }
     
+    public Set computeOrdering() {
+	HashSet allnodes=new HashSet();
+	allnodes.addAll(constnodes);
+	allnodes.addAll(nodes);
+	boolean acyclic=GraphNode.DFS.depthFirstSearch(allnodes);
+	if (!acyclic) {
+	    throw new Error("Cylic dependency between constraints.");
+	}
+	TreeSet topologicalsort = new TreeSet(new Comparator() {
+                public boolean equals(Object obj) { return false; }
+                public int compare(Object o1, Object o2) {
+                    GraphNode g1 = (GraphNode) o1;
+                    GraphNode g2 = (GraphNode) o2;
+                    return g1.getFinishingTime() - g2.getFinishingTime();
+                }
+            });
+	
+        topologicalsort.addAll(constnodes);
+	return topologicalsort;
+    }
+
     public void addNode(GraphNode gn) {
 	GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
 	nodes.add(gn2);
@@ -29,6 +48,9 @@ public class ConstraintDependence {
     }
 
     public void associateWithConstraint(GraphNode gn, Constraint c) {
+	if (!nodetonode.containsKey(gn)) {
+	    addNode(gn);
+	}
 	GraphNode ggn=(GraphNode)nodetonode.get(gn);
 	GraphNode gc=(GraphNode)constonode.get(c);
 	GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
@@ -36,12 +58,49 @@ public class ConstraintDependence {
     }
 
     public void requiresConstraint(GraphNode gn, Constraint c) {
+	if (!nodetonode.containsKey(gn)) {
+	    addNode(gn);
+	}
 	GraphNode ggn=(GraphNode)nodetonode.get(gn);
 	GraphNode gc=(GraphNode)constonode.get(c);
 	GraphNode.Edge e=new GraphNode.Edge("requires",gc);
 	ggn.addEdge(e);
     }
 
+    public void traversedependences(Termination termination) {
+	constructconjunctionnodes(termination);
+	constructconjunctionedges(termination);
+	Set removedset=termination.removedset;
+
+	for(int i=0;i<state.vConstraints.size();i++) {
+	    Constraint c=(Constraint)state.vConstraints.get(i);
+	    Set conjset=(Set)termination.conjunctionmap.get(c);
+	    HashSet exploredset=new HashSet();
+
+	    for(Iterator it=conjset.iterator();it.hasNext();) {
+		GraphNode gn=(GraphNode)it.next();
+		recursedependence(c,termination,exploredset,gn);
+	    }
+	}
+    }
+
+    void recursedependence(Constraint c,Termination termination, HashSet exploredset, GraphNode gn) {
+	Set removedset=termination.removedset;
+	Set conjunctionset=termination.conjunctions;
+
+	if (removedset.contains(gn))
+	    return;
+	exploredset.add(gn);
+	associateWithConstraint(gn,c);
+	for(Iterator it=gn.edges();it.hasNext();) {
+	    GraphNode.Edge e=(GraphNode.Edge) it.next();
+	    GraphNode gn2=e.getTarget();
+	    if (!(exploredset.contains(gn2)||
+		  conjunctionset.contains(gn2)))
+		recursedependence(c,termination,exploredset,gn2);
+	}
+    }
+
     /** Constructs a node for each Constraint */
     private void constructnodes() {
 	for(int i=0;i<state.vConstraints.size();i++) {
@@ -52,26 +111,33 @@ public class ConstraintDependence {
   	}
     }
     
-    private void constructconjunctionnodes() {
-	for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
-	    GraphNode conjnode=(GraphNode)it.next();
-	    TermNode tn=(TermNode)conjnode.getOwner();
-	    Conjunction conj=tn.getConjunction();
-	    addNode(conjnode);
-	}
+    private void constructconjunctionnodes(Termination termination) {
+	/*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+	  GraphNode conjnode=(GraphNode)it.next();
+	  TermNode tn=(TermNode)conjnode.getOwner();
+	  Conjunction conj=tn.getConjunction();
+	  addNode(conjnode);
+	  }*/
+	Set removedset=termination.removedset;
+
 	for(int i=0;i<state.vConstraints.size();i++) {
 	    Constraint c=(Constraint)state.vConstraints.get(i);
 	    Set conjset=(Set)termination.conjunctionmap.get(c);
 	    for(Iterator it=conjset.iterator();it.hasNext();) {
 		GraphNode gn=(GraphNode)it.next();
-		associateWithConstraint(gn,c);
+		if (!removedset.contains(gn))
+		    associateWithConstraint(gn,c);
 	    }
 	}
     }
 
-    private void constructconjunctionedges() {
+    private void constructconjunctionedges(Termination termination) {
+	Set removedset=termination.removedset;
 	for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 	    GraphNode conjnode=(GraphNode)it.next();
+	    if (removedset.contains(conjnode))
+		continue;
+	    
 	    TermNode tn=(TermNode)conjnode.getOwner();
 	    Conjunction conj=tn.getConjunction();
 	    for(int i=0;i<conj.size();i++) {
diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
index 7be110b..32bf470 100755
--- a/Repair/RepairCompiler/MCC/IR/ExactSize.java
+++ b/Repair/RepairCompiler/MCC/IR/ExactSize.java
@@ -16,7 +16,7 @@ class ExactSize {
     }
     
     public int getsize(SetDescriptor sd) {
-	if (sizemap.contains(sd))
+	if (sizemap.containsKey(sd))
 	    return ((Integer)sizemap.get(sd)).intValue();
 	else
 	    return -1;
@@ -30,6 +30,8 @@ class ExactSize {
 	    SetDescriptor sd=(SetDescriptor)it.next();
 	    for(int i=0;i<state.vConstraints.size();i++) {
 		Constraint c=(Constraint)state.vConstraints.get(i);
+		if (c.numQuantifiers()!=0)
+		    continue;
 		DNFConstraint dconst=c.dnfconstraint;
 		int oldsize=-1;
 		boolean matches=true;
@@ -46,8 +48,10 @@ class ExactSize {
 				    ep.getOp()==Opcode.EQ&&
 				    ep.getDescriptor()==sd&&
 				    ep.isRightInt()) {
-				    if (k==0) {
+				    if (j==0) {
 					oldsize=ep.rightSize();
+					goodmatch=true;
+					break;
 				    } else {
 					if (oldsize==ep.rightSize()) {
 					    goodmatch=true;
@@ -64,6 +68,7 @@ class ExactSize {
 		    }
 		}
 		if (matches) {
+		    System.out.println("Set "+sd.toString()+" has size "+oldsize);
 		    sizemap.put(sd,new Integer(oldsize));
 		    constraintmap.put(sd,c);
 		}
diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index 8bff959..356c56d 100755
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -630,10 +630,13 @@ public class RepairGenerator {
     private void generate_checks() {
 
         /* do constraint checks */
-        Vector constraints = state.vConstraints;
+	//        Vector constraints = state.vConstraints;
 
-        for (int i = 0; i < constraints.size(); i++) {
-            Constraint constraint = (Constraint) constraints.elementAt(i); 
+
+	//        for (int i = 0; i < constraints.size(); i++) {
+	//            Constraint constraint = (Constraint) constraints.elementAt(i); 
+	for (Iterator i = termination.constraintdependence.computeOrdering().iterator(); i.hasNext();) {
+	    Constraint constraint = (Constraint) ((GraphNode)i.next()).getOwner();
 	    
             {
 		final SymbolTable st = constraint.getSymbolTable();
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 14d1549..1ec1dc2 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -59,6 +59,8 @@ public class Termination {
 
 	abstractinterferes=new AbstractInterferes(this);
 	generateconjunctionnodes();
+	constraintdependence=new ConstraintDependence(state,this);
+
 	generatescopenodes();
 	generaterepairnodes();
 	generatedatastructureupdatenodes();
@@ -67,7 +69,7 @@ public class Termination {
 	generateabstractedges();
 	generatescopeedges();
 	generateupdateedges();
-	constraintdependence=new ConstraintDependence(state,this);
+
 
 	HashSet superset=new HashSet();
 	superset.addAll(conjunctions);
@@ -93,6 +95,8 @@ public class Termination {
 	    System.out.println("Can't generate terminating repair algorithm!");
 	    System.exit(-1);
 	}
+	constraintdependence.traversedependences(this);
+
 	System.out.println("Removing:");
 	for(Iterator it=removedset.iterator();it.hasNext();) {
 	    GraphNode gn=(GraphNode)it.next();
@@ -701,14 +705,15 @@ public class Termination {
 			   Binding binding=new Binding(vd);
 			   bindings.add(binding);*/
 			goodupdate=true;
-		    } else {
+		    } else if (q instanceof SetQuantifier) {
 			/* Create new element to bind to */
 			// search if the set 'set' has a size
-			Binding binding=new Binding(vd,set,exactsize.getsize(set)!=-1);
+			Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
 			bindings.add(binding);
 			goodupdate=true;
 
-		    }
+		    } else
+			goodupdate=false;
 	    } else if (q instanceof RelationQuantifier) {
 		RelationQuantifier rq=(RelationQuantifier)q;
 		for(int k=0;k<2;k++) {
@@ -831,7 +836,7 @@ public class Termination {
 		    TermNode tn=new TermNode(mun);
 		    GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 
-		    if (processquantifers(gn2,un, r)&&
+		    if (processquantifiers(gn2,un, r)&&
 			processconjunction(un,ruleconj)&&
 			un.checkupdates()) {
 			mun.addUpdate(un);
@@ -848,7 +853,7 @@ public class Termination {
     /** Adds updates that add an item to the appropriate set or
      * relation quantified over by the model definition rule.. */
     
-    boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
+    boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) {
 	Inclusion inc=r.getInclusion();
 	for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 	    Quantifier q=(Quantifier)iterator.next();
@@ -860,7 +865,7 @@ public class Termination {
 		toe.td=ReservedTypeDescriptor.INT;
 		Updates u=new Updates(toe,false);
 		un.addUpdate(u);
-		if (abstractremove.containsKey(rq.relation)) {
+		if (abstractadd.containsKey(rq.relation)) {
 		    GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
 		    GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 		    gn.addEdge(e);
@@ -870,14 +875,18 @@ public class Termination {
 		
 	    } else if (q instanceof SetQuantifier) {
 		SetQuantifier sq=(SetQuantifier)q;
-		if (un.getBinding(sq.var).getType()==Binding.SEARCH)
+		if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
+		    Binding b=un.getBinding(sq.var);
+		    Constraint reqc=exactsize.getConstraint(b.getSet());
+		    constraintdependence.requiresConstraint(gn,reqc);
 		    continue; /* Don't need to ensure addition for search */
+		}
 
 		ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 		eoe.td=ReservedTypeDescriptor.INT;
 		Updates u=new Updates(eoe,false);
 		un.addUpdate(u);
-		if (abstractremove.containsKey(sq.set)) {
+		if (abstractadd.containsKey(sq.set)) {
 		    GraphNode agn=(GraphNode)abstractadd.get(sq.set);
 		    GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 		    gn.addEdge(e);
diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 00ac87f..e50b63f 100755
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -428,19 +428,25 @@ class UpdateNode {
     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.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+b.getSet().getSafeSymbol()+"->firstkey();");
+	    } 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.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.");
+		}
 	    }
 	}
     }
-- 
2.34.1