Fixed some errors in the Repair Generator code.

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
index aecc4e995b0022f5819dc46b77656db0ff58f36f..153677fff76fc516d2cd6521596c08f27cd85ecf 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractRepair.java
@@ -1,4 +1,5 @@
 package MCC.IR;
+import MCC.State;
 
 class AbstractRepair {
     public final static int ADDTOSET=1;
@@ -150,6 +151,17 @@ class AbstractRepair {
        return descriptor;
     }
 
+
+    /** Thie method tells whether the repair needs to remove objects *
+     *  from the relation, or whether the model definition rules make
+     *  the remove unnecessary.*/
+
+    public boolean needsRemoves(State state) {
+       assert type==MODIFYRELATION;
+       SetDescriptor sd=getPredicate().getPredicate().inverted()?getRangeSet():getDomainSet();
+       return !ConstraintDependence.rulesensurefunction(state,(RelationDescriptor)getDescriptor(), sd, getPredicate().getPredicate().inverted(), true);
+    }
+
     public AbstractRepair(DNFPredicate dp,int typ, Descriptor d, Sources s) {
        torepair=dp;
        type=typ;

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index cd3eb99f5a143608aa3eeb33a66f74792db5b98a..ae1ac7a1c088b44c72cf94c603fa29c692f31f0e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -199,13 +199,15 @@ public class ConstraintDependence {
                SetQuantifier sq=(SetQuantifier)q;
                if (ve.getVar()!=sq.getVar())
                    return false;
-               if (!sq.getSet().isSubset(f.getSet()))
-                   return false;
-               if (!(((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
-                      ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))||isPartial)
-                   return false;
+               if (!isPartial) {
+                   if (!sq.getSet().isSubset(f.getSet()))
+                       return false;
+                   if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+                          ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+                       return false;
+               }
                Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
-               if (e2.isSafe())
+               if (isPartial||e2.isSafe())
                    foundrule=true;
                else
                    return false;

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 3a5d56fdaa06b1e847f865adc7f543bcf1e57b19..16a51f781861c0a263d3f88e263f629778309427 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -359,7 +359,7 @@ public class GraphAnalysis {
                        if (!containsgn3)
                            cantremove.remove(gn3);
                    }
-                   if (ismodify&&((numadd==0)||(numremove==0))) {
+                   if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
                        for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                            GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
                            GraphNode gn3=e2.getTarget();
@@ -529,7 +529,7 @@ public class GraphAnalysis {
                            numremove++;
                    }
                }
-               if ((numadd==0)||(numremove==0)) {
+               if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
                    for(Iterator it2=gn.edges();it2.hasNext();) {
                        GraphNode.Edge edge=(GraphNode.Edge)it2.next();
                        GraphNode gn2=edge.getTarget();

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index c09637293fc32f3bee4cab08acd536e2db4b74e2..79b89a65c7cda0189d94cd05ad8b30146d42f3e0 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -753,13 +753,7 @@ public class RepairGenerator {
     }
 
     private void generate_checks() {
-
         /* do constraint checks */
-       //        Vector constraints = state.vConstraints;
-
-
-       //        for (int i = 0; i < constraints.size(); i++) {
-       //            Constraint constraint = (Constraint) constraints.elementAt(i); 
        Iterator i;
        if (Compiler.REPAIR)
            i=termination.constraintdependence.computeOrdering().iterator();
@@ -845,14 +839,14 @@ public class RepairGenerator {
                            p.generate(cr,predvalue);
                            if (k==0)
                                cr.outputline("int "+costvar.getSafeSymbol()+"=0;");
-
+                           
                            if (negate)
                                cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
                            else
                                cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
                            cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
                        }
-
+                       
                        if(!first) {
                            cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
                            cr.startblock();
@@ -868,7 +862,6 @@ public class RepairGenerator {
                for(int j=0;j<dnfconst.size();j++) {
                    GraphNode gn=(GraphNode)dnfconst.get(j);
                    Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
-
                    if (removed.contains(gn))
                        continue;
                    cr.outputline("case "+j+":");
@@ -902,7 +895,7 @@ public class RepairGenerator {
                    cr.outputline("break;");
                }
                cr.outputline("}");
-
+               
                cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
                cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
                cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
@@ -932,10 +925,19 @@ public class RepairGenerator {
        cr.endblock();
        cr.outputline("rebuild:");
        cr.outputline(";");     
-       
     }
     
     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
+       Set nodes=getmultupdatenodeset(conj,dpred,repairtype);
+       Iterator it=nodes.iterator();
+       if (it.hasNext())
+           return (MultUpdateNode)it.next();
+       else
+           return null;
+    }
+
+    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();) {
@@ -950,23 +952,54 @@ public class RepairGenerator {
                        if (!removed.contains(gn3)) {
                            TermNode tn3=(TermNode)gn3.getOwner();
                            if (tn3.getType()==TermNode.UPDATE) {
-                               mun=tn3.getUpdate();
-                               break;
+                               hs.add(mun);
                            }
                        }
                    }
                }
            }
        }
-       return mun;
+       return hs;
+    }
+
+    private AbstractRepair getabstractrepair(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();) {
+           GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
+           TermNode tn2=(TermNode)gn2.getOwner();
+           if (tn2.getType()==TermNode.ABSTRACT) {
+               AbstractRepair ar=tn2.getAbstract();
+               if (((repairtype==-1)||(ar.getType()==repairtype))&&
+                   ar.getPredicate()==dpred) {
+                   return ar;
+               }
+           }
+       }
+       return null;
     }
 
+
     /** Generates abstract (and concrete) repair for a comparison */
 
     private void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
-       MultUpdateNode munmodify=getmultupdatenode(conj,dpred,AbstractRepair.MODIFYRELATION);
-       MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
-       MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
+       Set updates=getmultupdatenodeset(conj,dpred,AbstractRepair.MODIFYRELATION);
+       AbstractRepair ar=getabstractrepair(conj,dpred,AbstractRepair.MODIFYRELATION);
+       MultUpdateNode munmodify=null;
+       MultUpdateNode munadd=null;
+       MultUpdateNode munremove=null;
+       for(Iterator it=updates.iterator();it.hasNext();) {
+           MultUpdateNode mun=(MultUpdateNode)it.next();
+           if (mun.getType()==MultUpdateNode.ADD) {
+               munadd=mun;
+           } else if (mun.getType()==MultUpdateNode.REMOVE) { 
+               munremove=mun;
+           } else if (mun.getType()==MultUpdateNode.MODIFY) {
+               munmodify=mun;
+           }
+       }
+       
        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
        RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
        boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
@@ -1053,22 +1086,23 @@ public class RepairGenerator {
                    }
                }
            }
-
        } else {
            /* Start with scheduling removal */
-           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+");");
+           
+           if (ar.needsRemoves(state))
+               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+");");
+                           }
                        }
                    }
                }
-           }
            /* Now do addition */
            UpdateNode un=munadd.getUpdate(0);
            String name=(String)updatenames.get(un);

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 5e4bc91aac5f1013dcebf2e16b89e81fa31fd535..d0197b5d8b000337659ead3f847cdd95b978cef4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -547,7 +547,8 @@ public class Termination {
                generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
                /* Generate remove/add pairs */
-               generateremovefromsetrelation(gn,ar);
+               if (ar.needsRemoves(state))
+                   generateremovefromsetrelation(gn,ar);
                generateaddtosetrelation(gn,ar);
                /* Generate atomic modify */
                generatemodifyrelation(gn,ar);