Made flag work for checking only...Added support for modify relation updates.

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 05c60339cc176a91cfa1cfc4eaa4ffb7d4983dbe..013c5c6c492693ce4631dec0c279f3099948884d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -17,6 +17,7 @@ import MCC.IR.*;
  */
 
 public class Compiler {
  */
 
 public class Compiler {

+    /* Set this flag to false to turn repairs off */

     public static boolean REPAIR=true;
     
     public static void main(String[] args) {
     public static boolean REPAIR=true;
     
     public static void main(String[] args) {


@@ -56,11 +57,10 @@ public class Compiler {
 
 
            Termination termination=null;
 
 
            Termination termination=null;

-           if (REPAIR) {
-               /* Check partition constraints */
-               (new ImplicitSchema(state)).update();
-               termination=new Termination(state);
-           }
+           /* Check partition constraints */
+           (new ImplicitSchema(state)).update();
+           termination=new Termination(state);
+

             state.printall();
             (new DependencyBuilder(state)).calculate();
             
             state.printall();
             (new DependencyBuilder(state)).calculate();
             


@@ -91,19 +91,19 @@ public class Compiler {
                 //(new Optimizer(state)).optimize();
 
 
                 //(new Optimizer(state)).optimize();
 
 

-               if(REPAIR) {
-                   FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
-                   FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
-                   RepairGenerator wg = new RepairGenerator(state,termination);
-                   wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
-                   gcode2.close();
-                   gcode3.close();
-               } else {
+
+               FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
+               FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
+               RepairGenerator wg = new RepairGenerator(state,termination);
+               wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
+               gcode2.close();
+               gcode3.close();
+               /*              } else {

                    WorklistGenerator ng = new WorklistGenerator(state);
                    SetInclusion.worklist=true;
                    RelationInclusion.worklist=true;
                    ng.generate(gcode);
                    WorklistGenerator ng = new WorklistGenerator(state);
                    SetInclusion.worklist=true;
                    RelationInclusion.worklist=true;
                    ng.generate(gcode);

-               }
+                   }*/

                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();
                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index cce92d29c3f569a197b8475e0f7eaf20aa4a54c7..58b3b631904ca543c98ddbc9bcc8d7c0a5b4a6cf 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -3,6 +3,7 @@ package MCC.IR;
 import java.io.*;
 import java.util.*;
 import MCC.State;
 import java.io.*;
 import java.util.*;
 import MCC.State;

+import MCC.Compiler;

 
 public class RepairGenerator {
     State state;
 
 public class RepairGenerator {
     State state;


@@ -35,7 +36,8 @@ public class RepairGenerator {
        removed=t.removedset;
        togenerate=new HashSet();
         togenerate.addAll(termination.conjunctions);
        removed=t.removedset;
        togenerate=new HashSet();
         togenerate.addAll(termination.conjunctions);

-        togenerate.removeAll(removed);
+       if (Compiler.REPAIR)
+           togenerate.removeAll(removed);

         GraphNode.computeclosure(togenerate,removed);
        cost=new Cost();
        sources=new Sources(state);
         GraphNode.computeclosure(togenerate,removed);
        cost=new Cost();
        sources=new Sources(state);


@@ -108,6 +110,7 @@ public class RepairGenerator {
     String strepairtable="repairtable";
     String stleft="left";
     String stright="right";
     String strepairtable="repairtable";
     String stleft="left";
     String stright="right";

+    String stnew="newvalue";

 
     private void generate_updates() {
        int count=0;
 
     private void generate_updates() {
        int count=0;


@@ -146,11 +149,11 @@ public class RepairGenerator {
                    CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
                     };
                    CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
                     };

-                   un.generate(cr, false, stleft,stright,this);
+                   un.generate(cr, false, false, stleft,stright, null,this);

                    craux.outputline("if (maybe) printf(\"REALLY BAD\");");
                    craux.endblock();
                    break;
                    craux.outputline("if (maybe) printf(\"REALLY BAD\");");
                    craux.endblock();
                    break;

-               case MultUpdateNode.REMOVE:
+               case MultUpdateNode.REMOVE: {

                    Rule r=un.getRule();
                    String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
                    for(int j=0;j<r.numQuantifiers();j++) {
                    Rule r=un.getRule();
                    String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
                    for(int j=0;j<r.numQuantifiers();j++) {


@@ -177,11 +180,45 @@ public class RepairGenerator {
                    CodeWriter cr2 = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st2; }
                     };
                    CodeWriter cr2 = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st2; }
                     };

-                   un.generate(cr2, true, null,null,this);
+                   un.generate(cr2, true, false, null,null, null,this);

                    craux.outputline("if (maybe) printf(\"REALLY BAD\");");
                    craux.endblock();
                    craux.outputline("if (maybe) printf(\"REALLY BAD\");");
                    craux.endblock();

+               }
+                   break;
+               case MultUpdateNode.MODIFY: {
+                   Rule r=un.getRule();
+                   String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
+                   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+=", "+stleft+", "+stright+", "+stnew;
+                   methodcall+=")";
+                   crhead.outputline(methodcall+";");
+                   craux.outputline(methodcall);
+                   craux.startblock();
+                   craux.outputline("int maybe=0;");
+                   final SymbolTable st2 = un.getRule().getSymbolTable();
+                   CodeWriter cr2 = new StandardCodeWriter(outputaux) {
+                        public SymbolTable getSymbolTable() { return st2; }
+                    };
+                   un.generate(cr2, false, true, stleft, stright, stnew, this);
+                   craux.outputline("if (maybe) printf(\"REALLY BAD\");");
+                   craux.endblock();
+               }

                    break;
                    break;

-               case MultUpdateNode.MODIFY:
+

                default:
                    throw new Error("Nonimplement Update");
                }
                default:
                    throw new Error("Nonimplement Update");
                }


@@ -533,15 +570,15 @@ public class RepairGenerator {
                        
                        rule.getGuardExpr().prettyPrint(cr);
                        cr.outputline("");
                        
                        rule.getGuardExpr().prettyPrint(cr);
                        cr.outputline("");

-
+                       

                        /* now we have to generate the guard test */
                        /* now we have to generate the guard test */

-        
+                       

                        VarDescriptor guardval = VarDescriptor.makeNew();
                        rule.getGuardExpr().generate(cr, guardval);
                        
                        cr.outputline("if (" + guardval.getSafeSymbol() + ")");
                        cr.startblock();
                        VarDescriptor guardval = VarDescriptor.makeNew();
                        rule.getGuardExpr().generate(cr, guardval);
                        
                        cr.outputline("if (" + guardval.getSafeSymbol() + ")");
                        cr.startblock();

-
+                       

                        /* now we have to generate the inclusion code */
                        currentrule=rule;
                        rule.getInclusion().generate(cr);
                        /* now we have to generate the inclusion code */
                        currentrule=rule;
                        rule.getInclusion().generate(cr);


@@ -550,10 +587,10 @@ public class RepairGenerator {
                        for (int j=0;j<rule.numQuantifiers();j++) {
                            cr.endblock();
                        }
                        for (int j=0;j<rule.numQuantifiers();j++) {
                            cr.endblock();
                        }

-
+                       

                        // close startblocks generated by DotExpr memory checks
                        //DotExpr.generate_memory_endblocks(cr);
                        // close startblocks generated by DotExpr memory checks
                        //DotExpr.generate_memory_endblocks(cr);

-
+                       

                        cr.endblock(); // end else-if WORKLIST ladder
                        
                        elseladder = "else if";
                        cr.endblock(); // end else-if WORKLIST ladder
                        
                        elseladder = "else if";


@@ -589,18 +626,14 @@ public class RepairGenerator {
         Vector constraints = state.vConstraints;
 
         for (int i = 0; i < constraints.size(); i++) {
         Vector constraints = state.vConstraints;
 
         for (int i = 0; i < constraints.size(); i++) {

-

             Constraint constraint = (Constraint) constraints.elementAt(i); 
             Constraint constraint = (Constraint) constraints.elementAt(i); 

-
+           

             {
             {

-
-                final SymbolTable st = constraint.getSymbolTable();
-                
-                CodeWriter cr = new StandardCodeWriter(outputaux) {
+               final SymbolTable st = constraint.getSymbolTable();
+               CodeWriter cr = new StandardCodeWriter(outputaux) {

                         public SymbolTable getSymbolTable() { return st; }
                     };
                         public SymbolTable getSymbolTable() { return st; }
                     };

-
-                cr.outputline("// checking " + escape(constraint.toString()));
+               cr.outputline("// checking " + escape(constraint.toString()));

                 cr.startblock();
 
                 ListIterator quantifiers = constraint.quantifiers();
                 cr.startblock();
 
                 ListIterator quantifiers = constraint.quantifiers();


@@ -619,15 +652,15 @@ public class RepairGenerator {
                 
                 cr.outputline("if (maybe)");
                 cr.startblock();
                 
                 cr.outputline("if (maybe)");
                 cr.startblock();

-                cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \");");
+                cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");

                 cr.outputline("exit(1);");
                 cr.endblock();
 
                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
                 cr.startblock();
                 cr.outputline("exit(1);");
                 cr.endblock();
 
                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
                 cr.startblock();

-                if (DEBUG)
-                   cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
-
+                if (!Compiler.REPAIR)
+                   cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \\n\");");
+               else {

                /* Do repairs */
                /* Build new repair table */
                cr.outputline("if ("+repairtable.getSafeSymbol()+")");
                /* Do repairs */
                /* Build new repair table */
                cr.outputline("if ("+repairtable.getSafeSymbol()+")");


@@ -721,9 +754,9 @@ public class RepairGenerator {
                cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
                cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
                cr.outputline("goto rebuild;");  /* Rebuild model and all */
                cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
                cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
                cr.outputline("goto rebuild;");  /* Rebuild model and all */

-
+               }

                 cr.endblock();
                 cr.endblock();

-
+               

                 while (quantifiers.hasPrevious()) {
                     Quantifier quantifier = (Quantifier) quantifiers.previous();
                     cr.endblock();
                 while (quantifiers.hasPrevious()) {
                     Quantifier quantifier = (Quantifier) quantifiers.previous();
                     cr.endblock();


@@ -775,7 +808,10 @@ public class RepairGenerator {
        return mun;
     }
 
        return mun;
     }
 

-    public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
+    /** 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);
        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
        MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
        MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();


@@ -850,27 +886,44 @@ public class RepairGenerator {
            }
        }
        /* Do concrete repairs */
            }
        }
        /* Do concrete repairs */

-       /* 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 (munmodify!=null) {
+           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<munmodify.numUpdates();j++) {
+                       UpdateNode un=munmodify.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+","+newvalue.getSafeSymbol()+");");
+                       }

                    }
                }
            }
                    }
                }
            }

-       }
-       /* Now do addition */
-       UpdateNode un=munadd.getUpdate(0);
-       String name=(String)updatenames.get(un);
-       if (!inverted) {
-           cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
+

        } else {
        } else {

-           cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
+           /* 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+");");
+                       }
+                   }
+               }
+           }
+           /* Now do addition */
+           UpdateNode un=munadd.getUpdate(0);
+           String name=(String)updatenames.get(un);
+           if (!inverted) {
+               cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
+           } else {
+               cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
+           }

        }
     }
 
        }
     }
 


@@ -1245,7 +1298,9 @@ public class RepairGenerator {
            cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
            cr.startblock(); {
                /* Have update to call into */
            cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
            cr.startblock(); {
                /* Have update to call into */

-               VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
+               VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr");
+               cr.outputline("int "+mdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->getrelation2("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
+

                String parttype="";
                for(int i=0;i<currentrule.numQuantifiers();i++) {
                    if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
                String parttype="";
                for(int i=0;i<currentrule.numQuantifiers();i++) {
                    if (currentrule.getQuantifier(i) instanceof RelationQuantifier)


@@ -1253,8 +1308,9 @@ public class RepairGenerator {
                    else
                        parttype=parttype+", int";
                }
                    else
                        parttype=parttype+", int";
                }

-               cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
-               cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
+               VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
+               VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr");
+

                String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
                for(int i=0;i<currentrule.numQuantifiers();i++) {
                    Quantifier q=currentrule.getQuantifier(i);
                String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
                for(int i=0;i<currentrule.numQuantifiers();i++) {
                    Quantifier q=currentrule.getQuantifier(i);


@@ -1270,8 +1326,25 @@ public class RepairGenerator {
                        methodcall+=","+fq.getVar().getSafeSymbol();
                    }
                }
                        methodcall+=","+fq.getVar().getSafeSymbol();
                    }
                }

-               methodcall+=");";
-               cr.outputline(methodcall);
+
+
+               
+               cr.outputline("void *"+tmpptr.getSafeSymbol()+"=");
+               cr.outputline("(void *) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
+               cr.outputline("if ("+mdfyptr.getSafeSymbol()+")");
+               {
+                   cr.startblock();
+                   cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)) "+tmpptr.getSafeSymbol());
+                   cr.outputline(methodcall+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
+                   cr.endblock();
+               }
+               cr.outputline("else ");
+               {
+                   cr.startblock();
+                   cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol());
+                   cr.outputline(methodcall+");");
+                   cr.endblock();
+               }

                cr.outputline("goto rebuild;");
            }
            cr.endblock();
                cr.outputline("goto rebuild;");
            }
            cr.endblock();

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index e8f5d74d8789d7ed31f268499395de5e88e07bd1..8aa0370964d51c712852ef95bbb73ea657fca7d7 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -2,6 +2,7 @@ package MCC.IR;
 import java.util.*;
 import java.io.*;
 import MCC.State;
 import java.util.*;
 import java.io.*;
 import MCC.State;

+import MCC.Compiler;

 
 public class Termination {
     HashSet conjunctions;
 
 public class Termination {
     HashSet conjunctions;


@@ -36,6 +37,8 @@ public class Termination {
        abstractadd=new Hashtable();
        abstractremove=new Hashtable();
        conjtonodemap=new Hashtable();
        abstractadd=new Hashtable();
        abstractremove=new Hashtable();
        conjtonodemap=new Hashtable();

+       if (!Compiler.REPAIR)
+           return;

 
        generateconjunctionnodes();
        generatescopenodes();
 
        generateconjunctionnodes();
        generatescopenodes();


@@ -428,7 +431,7 @@ public class Termination {
        if (possiblerules.size()==0)
            return;
        int[] count=new int[possiblerules.size()];
        if (possiblerules.size()==0)
            return;
        int[] count=new int[possiblerules.size()];

-       while(remains(count,possiblerules)) {
+       while(remains(count,possiblerules,true)) {

            MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
            TermNode tn=new TermNode(mun);
            GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
            MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
            TermNode tn=new TermNode(mun);
            GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);


@@ -490,33 +493,109 @@ public class Termination {
                gn.addEdge(e);
                updatenodes.add(gn2);
            }
                gn.addEdge(e);
                updatenodes.add(gn2);
            }

-           increment(count,possiblerules);
+           increment(count,possiblerules,true);

        }
     }
 
        }
     }
 

-    static void increment(int count[], Vector rules) {
+    static void increment(int count[], Vector rules,boolean isremove) {

        count[0]++;
        for(int i=0;i<(rules.size()-1);i++) {
        count[0]++;
        for(int i=0;i<(rules.size()-1);i++) {

-           if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+           int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
+           if (count[i]>=num) {

                count[i+1]++;
                count[i]=0;
            } else break;
        }
     }
 
                count[i+1]++;
                count[i]=0;
            } else break;
        }
     }
 

-    static boolean remains(int count[], Vector rules) {
+    static boolean remains(int count[], Vector rules, boolean isremove) {

        for(int i=0;i<rules.size();i++) {
        for(int i=0;i<rules.size();i++) {

-           if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+           int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
+           if (count[i]>=num) {

                return false;
            }
        }
        return true;
     }
                return false;
            }
        }
        return true;
     }

+

     /** This method generates data structure updates to implement the
      *         abstract atomic modification specified by ar. */
     /** This method generates data structure updates to implement the
      *         abstract atomic modification specified by ar. */

-
+    int modifycount=0;

     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {

-       
+       RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
+       ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
+       boolean inverted=exprPredicate.inverted();
+       int leftindex=0;
+       int rightindex=1;
+       if (inverted)
+           leftindex=2;
+       else 
+           rightindex=2;
+
+
+       Vector possiblerules=new Vector();
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           if ((r.getInclusion() instanceof RelationInclusion)&&
+               (rd==((RelationInclusion)r.getInclusion()).getRelation()))
+               possiblerules.add(r);
+       }
+       if (possiblerules.size()==0)
+           return;
+       int[] count=new int[possiblerules.size()];
+       while(remains(count,possiblerules,false)) {
+           MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
+           TermNode tn=new TermNode(mun);
+           GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
+
+           boolean goodflag=true;
+           for(int i=0;i<possiblerules.size();i++) {
+               Rule r=(Rule)possiblerules.get(i);
+               UpdateNode un=new UpdateNode(r);
+               /* No Need to construct bindings on modify */
+               
+               int c=count[i];
+               if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
+                   goodflag=false;break;
+               }
+               RelationInclusion ri=(RelationInclusion)r.getInclusion();
+               if (!(ri.getLeftExpr() instanceof VarExpr)) {
+                   Updates up=new Updates(ri.getLeftExpr(),leftindex);
+                   un.addUpdate(up);
+               } else {
+                   VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
+                   if (vd.isGlobal()) {
+                       Updates up=new Updates(ri.getLeftExpr(),leftindex);
+                       un.addUpdate(up);
+                   } else if (inverted)
+                       goodflag=false;
+               }
+               if (!(ri.getRightExpr() instanceof VarExpr)) {
+                   Updates up=new Updates(ri.getRightExpr(),rightindex);
+                   un.addUpdate(up);
+               } else {
+                   VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
+                   if (vd.isGlobal()) {
+                       Updates up=new Updates(ri.getRightExpr(),rightindex);
+                       un.addUpdate(up);
+                   } else if (!inverted) 
+                       goodflag=false;
+               }
+                               
+               if (!un.checkupdates()) {
+                   goodflag=false;
+                   break;
+               }
+               mun.addUpdate(un);
+           }
+           if (goodflag) {
+               GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
+               modifycount++;
+               gn.addEdge(e);
+               updatenodes.add(gn2);
+           }
+           increment(count,possiblerules,false);
+       }

     }
 
 
     }
 
 


@@ -768,7 +847,7 @@ public class Termination {
                }
            } else {
                System.out.println(e.getClass().getName());
                }
            } else {
                System.out.println(e.getClass().getName());

-               throw new Error("Error #213");
+               throw new Error("Unrecognized Expr");

            }
        }
        return okay;
            }
        }
        return okay;

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index ed6595b70fd60bbc7957d67d19fd11add56ab07f..0ed097d3c6bd3e57b721c6a3a26eff33223766cf 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -219,7 +219,7 @@ class UpdateNode {
        return mun;
     }
 
        return mun;
     }
 

-    public void generate_abstract(CodeWriter cr, boolean removal, String slot0, String slot1, Updates u, RepairGenerator rg) {
+    public void generate_abstract(CodeWriter cr, Updates u, RepairGenerator rg) {

        State state=rg.state;
        Expr abstractexpr=u.getLeftExpr();
        boolean negated=u.negate;
        State state=rg.state;
        Expr abstractexpr=u.getLeftExpr();
        boolean negated=u.negate;


@@ -316,14 +316,14 @@ class UpdateNode {
        
     }
 
        
     }
 

-    public void generate(CodeWriter cr, boolean removal, String slot0, String slot1, RepairGenerator rg) {
-       if (!removal)
+    public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
+       if (!removal&&!modify)

            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) {
            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) {

-               generate_abstract(cr, removal, slot0, slot1, u, rg);
+               generate_abstract(cr, u, rg);

                return;
            }
 
                return;
            }
 


@@ -336,6 +336,8 @@ class UpdateNode {
                    cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
                else if (u.getRightPos()==1)
                    cr.outputline("int "+right.getSafeSymbol()+"="+slot1+";");
                    cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
                else if (u.getRightPos()==1)
                    cr.outputline("int "+right.getSafeSymbol()+"="+slot1+";");

+               else if (u.getRightPos()==2)
+                   cr.outputline("int "+right.getSafeSymbol()+"="+slot2+";");

                else throw new Error("Error w/ Position");
                break;
            default:
                else throw new Error("Error w/ Position");
                break;
            default:

diff --git a/Repair/RepairCompiler/MCC/Makefile b/Repair/RepairCompiler/MCC/Makefile
index 77a20e01921f9b50bc3d205ba78ac1100d77f773..1c61451f0281905519fd9033f144f5877a4a8b20 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Makefile
+++ b/Repair/RepairCompiler/MCC/Makefile
@@ -14,6 +14,8 @@ TDLParser.java TDLParser.class \
 CDLParser.java CDLParser.class \
 SDLParser.java SDLParser.class
 
 CDLParser.java CDLParser.class \
 SDLParser.java SDLParser.class
 

+CLASSPATH = /usr/java/j2sdk1.4.2_03/jre/lib/charsets.jar:/usr/java/j2sdk1.4.2_03/jre/lib/jce.jar:/usr/java/j2sdk1.4.2_03/jre/lib/jsse.jar:/usr/java/j2sdk1.4.2_03/jre/lib/plugin.jar:/usr/java/j2sdk1.4.2_03/jre/lib/rt.jar:/usr/java/j2sdk1.4.2_03/jre/lib/sunrsasign.jar
+

 COMPILER_CLASS = Compiler.class
 CLI_CLASS = CLI.class
 OTHER_CLASS = State.class LineCount.class Symbol.class
 COMPILER_CLASS = Compiler.class
 CLI_CLASS = CLI.class
 OTHER_CLASS = State.class LineCount.class Symbol.class


@@ -93,10 +95,10 @@ parser: $(PARSERS) $(SCANNER).java
 
 %Parser.java: %.cup
        java -classpath ../ java_cup.Main -nosummary -symbols $(SYMBOLS) -parser $*Parser < $*.cup
 
 %Parser.java: %.cup
        java -classpath ../ java_cup.Main -nosummary -symbols $(SYMBOLS) -parser $*Parser < $*.cup

-       javac $(SYMBOLS).java
+       jikes -nowarn -bootclasspath $(CLASSPATH) $(SYMBOLS).java

 
 %.class: %.java
 
 %.class: %.java

-       javac -classpath ../ -source 1.4 $<
+       jikes -nowarn -bootclasspath $(CLASSPATH) -classpath ../ -source 1.4 $<

 #      jikes -classpath $(CLASSPATH):../ $<
 
 %.lex.java: %.lex
 #      jikes -classpath $(CLASSPATH):../ $<
 
 %.lex.java: %.lex

diff --git a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc
index 2f8370c5e3f2817f82ef9dba982b1addf32b5799..e2202765a54fbdd90378484c775c5cc28426fda2 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc
+++ b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.cc
@@ -328,11 +328,12 @@ SimpleHashException::SimpleHashException() {}
 // ************************************************************
 
 
 // ************************************************************
 
 

-RepairHashNode::RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data){
+RepairHashNode::RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data, int data2){

     this->setrelation = setrelation;
     this->lvalue=lvalue;
     this->rvalue=rvalue;
     this->data = data;
     this->setrelation = setrelation;
     this->lvalue=lvalue;
     this->rvalue=rvalue;
     this->data = data;

+    this->data2 = data2;

     this->next = 0;
     this->lnext=0;
     this->rule=rule;
     this->next = 0;
     this->lnext=0;
     this->rule=rule;


@@ -373,6 +374,10 @@ int RepairHash::addset(int setv, int rule, int value, int data) {
 }
 
 int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int data) {
 }
 
 int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int data) {

+  return addrelation(relation,rule,lvalue,rvalue,data, 0);
+}
+
+int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int data, int data2) {

     unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size;
     
     RepairHashNode **ptr = &bucket[hashkey];
     unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size;
     
     RepairHashNode **ptr = &bucket[hashkey];


@@ -384,13 +389,14 @@ int RepairHash::addrelation(int relation, int rule, int lvalue, int rvalue, int
            (*ptr)->rule==rule &&
            (*ptr)->lvalue==lvalue &&
            (*ptr)->rvalue==rvalue &&
            (*ptr)->rule==rule &&
            (*ptr)->lvalue==lvalue &&
            (*ptr)->rvalue==rvalue &&

-           (*ptr)->data == data) {
+           (*ptr)->data == data &&
+           (*ptr)->data2 == data2) {

             return 0;
         }
         ptr = &((*ptr)->next);
     }
     
             return 0;
         }
         ptr = &((*ptr)->next);
     }
     

-    *ptr = new RepairHashNode(relation,rule,lvalue,rvalue, data);
+    *ptr = new RepairHashNode(relation,rule,lvalue,rvalue, data,data2);

     (*ptr)->lnext=nodelist;
     nodelist=*ptr;
     numelements++;
     (*ptr)->lnext=nodelist;
     nodelist=*ptr;
     numelements++;


@@ -424,6 +430,24 @@ int RepairHash::getset(int setv, int rule, int value) {
   return getrelation(setv||SETFLAG, rule, value,0);
 }
 
   return getrelation(setv||SETFLAG, rule, value,0);
 }
 

+int RepairHash::getrelation2(int relation, int rule, int lvalue,int rvalue) {
+    unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size;
+    
+    RepairHashNode **ptr = &bucket[hashkey];
+
+    /* check that this key/object pair isn't already here */
+    // TBD can be optimized for set v. relation */
+    while (*ptr) {
+        if ((*ptr)->setrelation == relation && 
+           (*ptr)->rule==rule &&
+           (*ptr)->lvalue==lvalue &&
+           (*ptr)->rvalue==rvalue) {
+         return (*ptr)->data2;
+        }
+        ptr = &((*ptr)->next);
+    }
+    return 0;
+}

 int RepairHash::getrelation(int relation, int rule, int lvalue,int rvalue) {
     unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size;
     
 int RepairHash::getrelation(int relation, int rule, int lvalue,int rvalue) {
     unsigned int hashkey = ((unsigned int)(relation ^ rule ^ lvalue ^ rvalue)) % size;
     

diff --git a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h
index c55c2558002808979d321ec987cc7ec41365f2b0..da21f2f0faeed986d377f27cc6e055da72e635a9 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h
+++ b/Repair/RepairCompiler/MCC/Runtime/SimpleHash.h
@@ -170,11 +170,12 @@ class RepairHashNode {
     RepairHashNode *next;
     RepairHashNode *lnext;
     int data;
     RepairHashNode *next;
     RepairHashNode *lnext;
     int data;

+    int data2;

     int setrelation;  
     int lvalue;  
     int rvalue;  
     int rule;
     int setrelation;  
     int lvalue;  
     int rvalue;  
     int rule;

-    RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data);
+    RepairHashNode(int setrelation, int rule, int lvalue, int rvalue, int data, int data2);

 };
 
 class RepairHash {
 };
 
 class RepairHash {


@@ -191,10 +192,12 @@ public:
     ~RepairHash();
     int addset(int setv, int rule, int value, int data);
     int addrelation(int relation, int rule, int lvalue, int rvalue, int data);
     ~RepairHash();
     int addset(int setv, int rule, int value, int data);
     int addrelation(int relation, int rule, int lvalue, int rvalue, int data);

+    int addrelation(int relation, int rule, int lvalue, int rvalue, int data, int data2);

     bool containsset(int setv, int rule, int value);
     bool containsrelation(int relation, int rule, int lvalue, int rvalue);
     int getset(int setv, int rule, int value);
     int getrelation(int relation, int rule, int lvalue, int rvalue);
     bool containsset(int setv, int rule, int value);
     bool containsrelation(int relation, int rule, int lvalue, int rvalue);
     int getset(int setv, int rule, int value);
     int getrelation(int relation, int rule, int lvalue, int rvalue);

+    int getrelation2(int relation, int rule, int lvalue, int rvalue);

 };
 
 #endif
 };
 
 #endif