Added code to correctly order checks...

Added code to search through sets for bindings of size 1.

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index 49d4cb97ab78e675dad361513f0f7d9bca42c7c9..7ae89cb7143fc41e9b47a875ecae9da2eec0c7bc 100755 (executable)
--- 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 7be110b36f79832bebad74224bdc51288f211ccf..32bf470223d68b039b033fa73e5feb034d9618f2 100755 (executable)
--- 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 8bff95979b21a2b555a82e1a6d67102e13b9607f..356c56da2c500e290cb3cd51d502452d97320d43 100755 (executable)
--- 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 14d1549da43ecb4cfa369ecb6fda90c26c380d4e..1ec1dc202a1b7322d15dd724f0dc7ad966df8029 100755 (executable)
--- 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 00ac87f5b7718d0cb37f61f77657afbcc6171097..e50b63fd15f344b7424dd634f73e4b5b04122cd7 100755 (executable)
--- 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.");
+               }
            }
        }
     }