Still adding code to construct termination graph, abstract repair actions, concrete...

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 5122d074c430a05cf0041575855a36c76989c14b..569485c7fc1cbc73b587c10b57e4cd5040109672 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -92,9 +92,93 @@ class AbstractInterferes {
                    (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
                    return false;
            } 
+       }
+       return true;
+    }
 
+    static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
+       if ((des!=dp.getPredicate().getDescriptor()) &&
+           ((des instanceof SetDescriptor)||
+            !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
+           return false;
 
+       /* This if handles all the c comparisons in the paper */
+       if (des==dp.getPredicate().getDescriptor()&&
+           (satisfy)&&
+           (dp.getPredicate() instanceof ExprPredicate)&&
+           (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+           boolean neg2=dp.isNegated();
+           Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           {
+               if ((!neg2&&(op2==Opcode.GE))||
+                   (!neg2&&(op2==Opcode.GT))||
+                   (neg2&&(op2==Opcode.LE))||
+                   (neg2&&(op2==Opcode.LT)))
+                   return false;
+           }
+       }
+       /* This if handles all the c comparisons in the paper */
+       if (des==dp.getPredicate().getDescriptor()&&
+           (!satisfy)&&
+           (dp.getPredicate() instanceof ExprPredicate)&&
+           (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+           boolean neg2=dp.isNegated();
+           Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+           int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+           {
+               if ((neg2&&(op2==Opcode.GE))||
+                   (neg2&&(op2==Opcode.GT))||
+                   (!neg2&&(op2==Opcode.LE))||
+                   (!neg2&&(op2==Opcode.LT)))
+                   return false;
+           } 
        }
        return true;
     }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+       for(int i=0;i<r.numQuantifiers();i++) {
+           Quantifier q=r.getQuantifier(i);
+           if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
+               if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
+                   return true;
+           } else if (q instanceof ForQuantifier) {
+               if (q.getRequiredDescriptors().contains(des))
+                   return true;
+           } else throw new Error("Unrecognized Quantifier");
+       }
+       /* Scan DNF form */
+       DNFRule drule=r.getDNFGuardExpr();
+       for(int i=0;i<drule.size();i++) {
+           RuleConjunction rconj=drule.get(i);
+           for(int j=0;j<rconj.size();j++) {
+               DNFExpr dexpr=rconj.get(j);
+               Expr expr=dexpr.getExpr();
+               boolean negated=dexpr.getNegation();
+               /*
+                 satisfy  negated
+                 Yes      No             Yes
+                 Yes      Yes            No
+                 No       No             No
+                 No       Yes            Yes
+               */
+               boolean satisfiesrule=(satisfy^negated);/*XOR of these */
+               if (satisfiesrule==satisfyrule) {
+                   /* Effect is the one being tested for */
+                   /* Only expr's to be concerned with are TupleOfExpr and
+                      ElementOfExpr */
+                   if (expr.getRequiredDescriptors().contains(des)) {
+                       if (((expr instanceof ElementOfExpr)||
+                           (expr instanceof TupleOfExpr))&&
+                           (expr.getRequiredDescriptors().size()==1))
+                           return true;
+                       else
+                           throw new Error("Unrecognized EXPR");
+                   }
+               }
+           }
+       }
+       return false;
+    }
 }

diff --git a/Repair/RepairCompiler/MCC/IR/Binding.java b/Repair/RepairCompiler/MCC/IR/Binding.java
new file mode 100755 (executable)
index 0000000..585107c
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Binding.java
@@ -0,0 +1,20 @@
+package MCC.IR;
+
+class Binding {
+    VarDescriptor var;
+    int position;
+
+    public Binding(VarDescriptor vd,int pos) {
+       var=vd;
+       position=pos;
+    }
+
+    int getPosition() {
+       return position;
+    }
+
+    VarDescriptor getVar() {
+       return var;
+    }
+
+}

diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
new file mode 100755 (executable)
index 0000000..d728062
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -0,0 +1,24 @@
+package MCC.IR;
+
+class ConcreteInterferes {
+    static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+       for(int i=0;i<mun.numUpdates();i++) {
+           UpdateNode un=mun.getUpdate(i);
+           for (int j=0;j<un.numUpdates();j++) {
+               Updates update=un.getUpdate(j);
+               Descriptor des=update.getDescriptor();
+               DNFRule drule=r.getDNFGuardExpr();
+               for(int k=0;k<drule.size();k++) {
+                   RuleConjunction rconj=drule.get(k);
+                   for(int l=0;l<rconj.size();l++) {
+                       DNFExpr dexpr=rconj.get(l);
+                       
+                   }
+               }
+           }
+       }
+       return false;
+    }
+
+
+}

diff --git a/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java b/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java
new file mode 100755 (executable)
index 0000000..17b8385
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java
@@ -0,0 +1,6 @@
+package MCC.IR;
+
+class ConsequenceNode {
+    public ConsequenceNode() {
+    }
+}

diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 1f3849ff52d1737272e29af06d901c5040b297c0..4aff0d5949a193636ac49a816e6446c6eeedef21 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -63,7 +63,7 @@ public class DNFConstraint {
     public DNFConstraint not() {
        DNFConstraint copy=copy();
        for (int i=0;i<size();i++) {
-           Conjunction conj=get(i);
+           Conjunction conj=copy.get(i);
            for (int j=0;j<conj.size();j++) {
                DNFPredicate dp=conj.get(j);
                dp.negatePred();

diff --git a/Repair/RepairCompiler/MCC/IR/DNFExpr.java b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
index ce039db35092ac86b0bf7d9a3303190e29530b9b..ac5d8be1a35ccc23b12f1b62b182c986e7665fc4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
@@ -16,4 +16,12 @@ public class DNFExpr {
     void negatePred() {
        negate=!negate;
     }
+
+    public Expr getExpr() {
+       return predicate;
+    }
+
+    public boolean getNegation() {
+       return negate;
+    }
 }

diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
index 942f7f63d83641c4bcae6e22b3aa19cba51f42f0..ab76f579f200aec5b304bb1626508242654300a1 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DNFRule.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -63,7 +63,7 @@ public class DNFRule {
     public DNFRule not() {
        DNFRule copy=copy();
        for (int i=0;i<size();i++) {
-           RuleConjunction conj=get(i);
+           RuleConjunction conj=copy.get(i);
            for (int j=0;j<conj.size();j++) {
                DNFExpr dp=conj.get(j);
                dp.negatePred();

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 5336065a8855a3f4e34e7b93cb70e087ba09764c..bf911bd8aafc6eb04d3a4ae46a6e067d7092800d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -20,10 +20,29 @@ public class DotExpr extends Expr {
     }
     */
 
+    FieldDescriptor fd;
+    TypeDescriptor fieldtype;
+    Expr intindex;
+    
     public DotExpr(Expr left, String field, Expr index) {
         this.left = left;
         this.field = field;
         this.index = index;
+
+        FieldDescriptor fd = struct.getField(field);
+        LabelDescriptor ld = struct.getLabel(field);        
+       if (ld != null) { /* label */
+            assert fd == null;
+            fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
+            fd = ld.getField();
+            assert fd != null;
+            assert intindex == null;
+            intindex = ld.getIndex();
+        } else {
+            fieldtype = fd.getType();
+           intindex=index;
+        }
+       this.fd=fd;
     }
 
     public Set getRequiredDescriptors() {
@@ -32,7 +51,6 @@ public class DotExpr extends Expr {
         if (index != null) {
             v.addAll(index.getRequiredDescriptors());
         }
-
         return v;
     }
 
@@ -40,6 +58,14 @@ public class DotExpr extends Expr {
         return left;
     }
 
+    public FieldDescriptor getField() {
+       return fd;
+    }
+
+    public Expr getIndex() {
+       return intindex;
+    }
+
     public void generate(CodeWriter writer, VarDescriptor dest) {
         VarDescriptor leftd = VarDescriptor.makeNew("left");
 
@@ -54,23 +80,9 @@ public class DotExpr extends Expr {
         writer.outputline("");
       
         StructureTypeDescriptor struct = (StructureTypeDescriptor) left.getType();        
-        FieldDescriptor fd = struct.getField(field);
-        LabelDescriptor ld = struct.getLabel(field);        
-        TypeDescriptor fieldtype;
         Expr intindex = index;
         Expr offsetbits;
 
-        if (ld != null) { /* label */
-            assert fd == null;
-            fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
-            fd = ld.getField();
-            assert fd != null;
-            assert intindex == null;
-            intindex = ld.getIndex();
-        } else {
-            fieldtype = fd.getType();
-        }
-
         // #ATTN#: getOffsetExpr needs to be called with the fielddescriptor obect that is in teh vector list
         // this means that if the field is an arraydescriptor you have to call getOffsetExpr with the array 
         // descriptor not the underlying field descriptor

diff --git a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
index e4150d246cd4be234ea7198945280a529f64b4a5..5739d6320cf3862a4a12b460ecc68e1cfb4e3904 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
@@ -14,13 +14,21 @@ public class ForQuantifier extends Quantifier {
         this.var = vd;
     }
 
+    public VarDescriptor getVar() {
+       return var;
+    }
+
+
     public void setBounds(Expr lower, Expr upper) {
         this.lower = lower;
         this.upper = upper;
     }
 
     public Set getRequiredDescriptors() {
-        return new HashSet();
+        HashSet set=new HashSet();
+       set.addAll(lower.getRequiredDescriptors());
+       set.addAll(upper.getRequiredDescriptors());
+       return set;
     }
 
     public String toString() {

diff --git a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
new file mode 100755 (executable)
index 0000000..fdddbeb
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
@@ -0,0 +1,23 @@
+package MCC.IR;
+import java.util.*;
+
+class MultUpdateNode {
+    Vector updates;
+    AbstractRepair abstractrepair;
+    public MultUpdateNode(AbstractRepair ar) {
+       updates=new Vector();
+       abstractrepair=ar;
+    }
+    void addUpdate(UpdateNode un) {
+       updates.add(un);
+    }
+    int numUpdates() {
+       return updates.size();
+    }
+    AbstractRepair getRepair() {
+       return abstractrepair;
+    }
+    UpdateNode getUpdate(int i) {
+       return (UpdateNode)updates.get(i);
+    }
+}

diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 47a6faeae00a3316d374ee0ceea0f655d256bc11..b3af82790dede1e7479e376f8d0e9da86b5970ca 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -16,6 +16,10 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public Opcode getOpcode() {
+       return opcode;
+    }
+
     public DNFRule constructDNF() {
         if (opcode==Opcode.AND) {
             DNFRule leftd=left.constructDNF();
@@ -28,7 +32,7 @@ public class OpExpr extends Expr {
         } else if (opcode==Opcode.NOT) {
             DNFRule leftd=left.constructDNF();
             return leftd.not();
-        } else throw new Error();
+        } else return new DNFRule(this);
     }
 
     public boolean usesDescriptor(RelationDescriptor rd) {

diff --git a/Repair/RepairCompiler/MCC/IR/Quantifier.java b/Repair/RepairCompiler/MCC/IR/Quantifier.java
index 3f302b8a1e9a994c540c1782ca4eb267da7ab2eb..2f5c170bcbc70dafaa058baa9c40ea6f4461f012 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Quantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/Quantifier.java
@@ -3,7 +3,6 @@ package MCC.IR;
 import java.util.*;
 
 public abstract class Quantifier {
-
     public abstract Set getRequiredDescriptors();
 
     public abstract void generate_open(CodeWriter writer);

diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java
index 69e8d0d45ec7da2fec4eb47080b4fafa0cacb826..12650d93a46bda2fcbe021328db9071bfe420e93 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Rule.java
+++ b/Repair/RepairCompiler/MCC/IR/Rule.java
@@ -12,7 +12,8 @@ public class Rule {
     Expr guard = null;
     Inclusion inclusion = null;    
     SymbolTable st = new SymbolTable();
-    
+    DNFRule dnfguard=null,dnfnegguard=null;
+
     String label;
     
     int num;
@@ -22,6 +23,14 @@ public class Rule {
         label = new String("rule" + count++);
     }
     
+    public int numQuantifiers() {
+       return quantifiers.size();
+    }
+
+    public Quantifier getQuantifier(int i) {
+       return (Quantifier) quantifiers.get(i);
+    }
+
     public int getNum() {
         return num;
     }
@@ -48,12 +57,23 @@ public class Rule {
 
     public void setGuardExpr(Expr guard) {
         this.guard = guard;
+       dnfguard=guard.constructDNF();
+       OpExpr opexpr=new OpExpr(Opcode.NOT,guard,null);
+       dnfnegguard=opexpr.constructDNF();
     }
     
     public Expr getGuardExpr() {
         return guard;
     }
 
+    public DNFRule getDNFGuardExpr() {
+        return dnfguard;
+    }
+
+    public DNFRule getDNFNegGuardExpr() {
+        return dnfnegguard;
+    }
+
     public void setInclusion(Inclusion inclusion) {
         this.inclusion = inclusion;
     }

diff --git a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
index c1aa03bbb5bdd9d4c82566a88f5ffb9f8d2b9a48..b2723bcd598d87338320ffe3f8b0779fe032b96f 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
+++ b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
@@ -34,7 +34,7 @@ public class RuleConjunction {
 
     public RuleConjunction copy() {
        Vector vector=new Vector();
-       for (int i=0;i<=size();i++) {
+       for (int i=0;i<size();i++) {
            DNFExpr dp=get(i);
            vector.add(new DNFExpr(dp));
        }

diff --git a/Repair/RepairCompiler/MCC/IR/ScopeNode.java b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
index 8a10b6d49b3bd3edb2ba06e2e8c1a3a63c3ca783..168117d0bd250146a1de534063d9372b16ef2be1 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ScopeNode.java
+++ b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
@@ -8,4 +8,15 @@ class ScopeNode {
        rule=r;
        this.satisfy=satisfy;
     }
+    public Descriptor getDescriptor() {
+       Inclusion inc=rule.getInclusion();
+       if (inc instanceof SetInclusion)
+           return ((SetInclusion)inc).getSet();
+       else if (inc instanceof RelationInclusion)
+           return ((RelationInclusion)inc).getRelation();
+       else throw new Error("Unrecognized Inclusion");
+    }
+    public boolean getSatisfy() {
+       return satisfy;
+    }
 }

diff --git a/Repair/RepairCompiler/MCC/IR/TermNode.java b/Repair/RepairCompiler/MCC/IR/TermNode.java
index 46b9f749e77c586c92410310d59475fec4ff08ca..9e3dbe8b113a4d90af70b8aa0304869abef93b9e 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/TermNode.java
+++ b/Repair/RepairCompiler/MCC/IR/TermNode.java
@@ -5,14 +5,15 @@ class TermNode {
     public final static int ABSTRACT=2;
     public final static int UPDATE=3;
     public final static int RULESCOPE=4;
-    
+    public final static int CONSEQUENCE=5;
 
+    ConsequenceNode conseqnode;
     Constraint constr;
     Conjunction conj;
     int type;
     AbstractRepair repair;
     ScopeNode scope;
-
+    MultUpdateNode update;
 
     public TermNode(Constraint constr, Conjunction conj) {
        this.constr=constr;
@@ -25,11 +26,28 @@ class TermNode {
        type=ABSTRACT;
     }
 
+    public TermNode(ConsequenceNode cn) {
+       conseqnode=cn;
+       type=CONSEQUENCE;
+    }
+
     public TermNode(ScopeNode sn) {
        scope=sn;
        type=RULESCOPE;
     }
 
+    public TermNode(MultUpdateNode un) {
+       update=un;
+       type=UPDATE;
+    }
+
+    public ConsequenceNode getConsequence() {
+       if (type!=CONSEQUENCE)
+           throw new Error("Not Consequence Node!");
+       else
+           return conseqnode;
+    }
+
     public Conjunction getConjunction() {
        if (type!=CONJUNCTION)
            throw new Error("Not Conjunction Node!");
@@ -37,6 +55,20 @@ class TermNode {
            return conj;
     }
 
+    public MultUpdateNode getUpdate() {
+       if (type!=UPDATE)
+           throw new Error("Not Update Node!");
+       else
+           return update;
+    }
+
+    public ScopeNode getScope() {
+       if (type!=RULESCOPE)
+           throw new Error("Not Scope Node!");
+       else
+           return scope;
+    }
+
     public AbstractRepair getAbstract() {
        if (type!=ABSTRACT)
            throw new Error("Not Abstract Repair Node!");

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 7f9adc08e8ace7d684e15effdc8be5f7e2c6cfd3..bfbe8db16066c3780a67597b4554f36590471a26 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -1,5 +1,6 @@
 package MCC.IR;
 import java.util.*;
+import java.io.*;
 import MCC.State;
 
 public class Termination {
@@ -7,10 +8,13 @@ public class Termination {
     Hashtable conjunctionmap;
 
     HashSet abstractrepair;
+    HashSet updatenodes;
+    HashSet consequencenodes;
 
     HashSet scopenodes;
     Hashtable scopesatisfy;
     Hashtable scopefalsify;
+    Hashtable consequence;
 
     State state;
 
@@ -22,12 +26,31 @@ public class Termination {
        scopenodes=new HashSet();
        scopesatisfy=new Hashtable();
        scopefalsify=new Hashtable();
+       consequence=new Hashtable();
+       updatenodes=new HashSet();
+       consequencenodes=new HashSet();
 
        generateconjunctionnodes();
+       generatescopenodes();
        generaterepairnodes();
-       generateabstractedges();
        generatedatastructureupdatenodes();
-       generatescopenodes();
+
+       generateabstractedges();
+       generatescopeedges();
+       generateupdateedges();
+
+       HashSet superset=new HashSet();
+       superset.addAll(conjunctions);
+       superset.addAll(abstractrepair);
+       superset.addAll(updatenodes);
+       superset.addAll(scopenodes);
+       superset.addAll(consequencenodes);
+       try {
+           GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
+       } catch (Exception e) {
+           e.printStackTrace();
+           System.exit(-1);
+       }
     }
     
     void generateconjunctionnodes() {
@@ -37,13 +60,37 @@ public class Termination {
            DNFConstraint dnf=c.dnfconstraint;
            for(int j=0;j<dnf.size();j++) {
                TermNode tn=new TermNode(c,dnf.get(j));
-               GraphNode gn=new GraphNode("Conjunction"+i+","+j,tn);
+               GraphNode gn=new GraphNode("Conjunction"+i+"B"+j,tn);
                conjunctions.add(gn);
                conjunctionmap.put(c,gn);
            }
        }
     }
 
+    void generateupdateedges() {
+       for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
+           GraphNode gn=(GraphNode)updateiterator.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           MultUpdateNode mun=tn.getUpdate();
+           /* Cycle through the rules to look for possible conflicts */
+           for(int i=0;i<state.vRules.size();i++) {
+               Rule r=(Rule) state.vRules.get(i);  
+               if (ConcreteInterferes.interferes(mun,r,true)) {
+                   GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
+                   GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
+                   gnconseq.addEdge(e);
+               }
+               if (ConcreteInterferes.interferes(mun,r,false)) {
+                   GraphNode scopenode=(GraphNode)scopefalsify.get(r);
+                   GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
+                   gnconseq.addEdge(e);
+               }
+           }
+       }
+    }
+
     void generateabstractedges() {
        for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
            GraphNode gn=(GraphNode)absiterator.next();
@@ -66,6 +113,47 @@ public class Termination {
        }
     }
     
+    void generatescopeedges() {
+       for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
+           GraphNode gn=(GraphNode)scopeiterator.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           ScopeNode sn=tn.getScope();
+           
+           /* Interference edges with conjunctions */
+           for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+               GraphNode gn2=(GraphNode)conjiterator.next();
+               TermNode tn2=(TermNode)gn2.getOwner();
+               Conjunction conj=tn2.getConjunction();
+               for(int i=0;i<conj.size();i++) {
+                   DNFPredicate dp=conj.get(i);
+                   if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
+                       GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                       GraphNode gnconseq=(GraphNode)consequence.get(sn);
+                       gnconseq.addEdge(e);
+                       break;
+                   }
+               }
+           }
+
+           /* Now see if this could effect other model defintion rules */
+           for(int i=0;i<state.vRules.size();i++) {
+               Rule r=(Rule) state.vRules.get(i);
+               if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
+                   GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
+                   GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
+                   gnconseq.addEdge(e);
+               }
+               if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
+                   GraphNode scopenode=(GraphNode)scopefalsify.get(r);
+                   GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+                   GraphNode gnconseq=(GraphNode)consequence.get(sn);
+                   gnconseq.addEdge(e);
+               }
+           }
+       }
+    }
+
 
     void generaterepairnodes() {
        for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
@@ -79,7 +167,7 @@ public class Termination {
                for(int j=0;j<array.length;j++) {
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d);
                    TermNode tn2=new TermNode(ar);
-                   GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn2);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+j,tn2);
                    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
                    abstractrepair.add(gn2);
@@ -94,27 +182,212 @@ public class Termination {
            TermNode tn=(TermNode) gn.getOwner();
            AbstractRepair ar=tn.getAbstract();
            if (ar.getType()==AbstractRepair.ADDTOSET) {
-               generateaddtoset(ar);
+               generateaddtoset(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
-               generateremovefromset(ar);
+               generateremovefromset(gn,ar);
            } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
-               generateaddtorelation(ar);
+               generateaddtorelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
-               generateremovefromrelation(ar);
+               generateremovefromrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
-               generatemodifyrelation(ar);
+               generatemodifyrelation(gn,ar);
            }
        }
     }
 
-    void generateaddtoset(AbstractRepair ar) {
+    void generateremovefromset(GraphNode gn,AbstractRepair ar) {
+       Vector possiblerules=new Vector();
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule) state.vRules.get(i);
+           if ((r.getInclusion() instanceof SetInclusion)&&
+               (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
+               possiblerules.add(r);
+       }
+       int[] count=new int[possiblerules.size()];
+       while(remains(count,possiblerules)) {
+           MultUpdateNode mun=new MultUpdateNode(ar);
+           for(int i=0;i<possiblerules.size();i++) {
+               UpdateNode un=new UpdateNode();
+               mun.addUpdate(un);
+               /* CODE HERE*/
+           }
+           increment(count,possiblerules);
+       }
+    }
+
+    static void increment(int count[], Vector rules) {
+       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()))) {
+               count[i+1]++;
+               count[i]=0;
+           } else break;
+       }
+    }
+
+    static boolean remains(int count[], Vector rules) {
+       for(int i=0;i<rules.size();i++) {
+           if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+               return false;
+           }
+       }
+       return true;
+    }
+
+    void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {}
+    void generateaddtorelation(GraphNode gn,AbstractRepair ar) {}
+    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {}
+
+    static int addtocount=0;
+    void generateaddtoset(GraphNode gn, AbstractRepair ar) {
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            if (r.getInclusion() instanceof SetInclusion) {
                if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
                    //Generate add instruction
-                   
-
+                   DNFRule dnfrule=r.getDNFGuardExpr();
+                   for(int j=0;j<dnfrule.size();j++) {
+                       Inclusion inc=r.getInclusion();
+                       UpdateNode un=new UpdateNode();
+                       /* First solve for quantifiers */
+                       boolean goodupdate=true;
+                       for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+                           Quantifier q=(Quantifier)iterator.next();
+                           boolean foundall=true;
+                           if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
+                               VarDescriptor vd=null;
+                               if (q instanceof SetQuantifier)
+                                   vd=((SetQuantifier)q).getVar();
+                               else
+                                   vd=((ForQuantifier)q).getVar();
+                               if(inc instanceof SetInclusion) {
+                                   SetInclusion si=(SetInclusion)inc;
+                                   if ((si.elementexpr instanceof VarExpr)&&
+                                       (((VarExpr)si.elementexpr).getVar()==vd)) {
+                                       /* Can solve for v */
+                                       Binding binding=new Binding(vd,0);
+                                       un.addBinding(binding);
+                                   } else
+                                       foundall=false;
+                               } else if (inc instanceof RelationInclusion) {
+                                   RelationInclusion ri=(RelationInclusion)inc;
+                                   boolean f1=true;
+                                   boolean f2=true;
+                                   if ((ri.getLeftExpr() instanceof VarExpr)&&
+                                       (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                                       /* Can solve for v */
+                                       Binding binding=new Binding(vd,0);
+                                       un.addBinding(binding);
+                                   } else f1=false;
+                                   if ((ri.getRightExpr() instanceof VarExpr)&&
+                                       (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                                       /* Can solve for v */
+                                       Binding binding=new Binding(vd,0);
+                                       un.addBinding(binding);
+                                   } else f2=false;
+                                   if (!(f1||f2))
+                                       foundall=false;
+                               } else throw new Error("Inclusion not recognized");
+                           } else if (q instanceof RelationQuantifier) {
+                               RelationQuantifier rq=(RelationQuantifier)q;
+                               for(int k=0;k<2;k++) {
+                                   VarDescriptor vd=(k==0)?rq.x:rq.y;
+                                   if(inc instanceof SetInclusion) {
+                                       SetInclusion si=(SetInclusion)inc;
+                                       if ((si.elementexpr instanceof VarExpr)&&
+                                           (((VarExpr)si.elementexpr).getVar()==vd)) {
+                                           /* Can solve for v */
+                                           Binding binding=new Binding(vd,0);
+                                           un.addBinding(binding);
+                                       } else
+                                           foundall=false;
+                                   } else if (inc instanceof RelationInclusion) {
+                                       RelationInclusion ri=(RelationInclusion)inc;
+                                       boolean f1=true;
+                                       boolean f2=true;
+                                       if ((ri.getLeftExpr() instanceof VarExpr)&&
+                                           (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+                                           /* Can solve for v */
+                                           Binding binding=new Binding(vd,0);
+                                           un.addBinding(binding);
+                                       } else f1=false;
+                                       if ((ri.getRightExpr() instanceof VarExpr)&&
+                                                  (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+                                           /* Can solve for v */
+                                           Binding binding=new Binding(vd,0);
+                                           un.addBinding(binding);
+                                       } else f2=false;
+                                       if (!(f1||f2))
+                                           foundall=false;
+                                   } else throw new Error("Inclusion not recognized");
+                               }
+                           } else throw new Error("Quantifier not recognized");
+                           if (!foundall) {
+                               goodupdate=false;
+                               break;
+                           }
+                           /* Now build update for tuple/set inclusion condition */
+                           if(inc instanceof SetInclusion) {
+                               SetInclusion si=(SetInclusion)inc;
+                               if (!(si.elementexpr instanceof VarExpr)) {
+                                   Updates up=new Updates(si.elementexpr,0);
+                                   un.addUpdate(up);
+                               }
+                           } 
+                           if (inc instanceof RelationInclusion) {
+                               RelationInclusion ri=(RelationInclusion)inc;
+                               if (!(ri.getLeftExpr() instanceof VarExpr)) {
+                                   Updates up=new Updates(ri.getLeftExpr(),0);
+                                   un.addUpdate(up);
+                               }
+                               if (!(ri.getRightExpr() instanceof VarExpr)) {
+                                   Updates up=new Updates(ri.getRightExpr(),0);
+                                   un.addUpdate(up);
+                               }
+                           }
+                           //Finally build necessary updates to satisfy conjunction
+                           RuleConjunction ruleconj=dnfrule.get(j);
+                           for(int k=0;k<ruleconj.size();k++) {
+                               DNFExpr de=ruleconj.get(k);
+                               Expr e=de.getExpr();
+                               if (e instanceof OpExpr) {
+                                   OpExpr ex=(OpExpr)de.getExpr();
+                                   Opcode op=ex.getOpcode();
+                                   if (de.getNegation()) {
+                                       /* remove negation through opcode translation */
+                                       if (op==Opcode.GT)
+                                           op=Opcode.LE;
+                                       else if (op==Opcode.GE)
+                                           op=Opcode.LT;
+                                       else if (op==Opcode.EQ)
+                                           op=Opcode.NE;
+                                       else if (op==Opcode.NE)
+                                           op=Opcode.EQ;
+                                       else if (op==Opcode.LT)
+                                           op=Opcode.GE;
+                                       else if (op==Opcode.LE)
+                                           op=Opcode.GT;
+                                   }
+                                   Updates up=new Updates(ex.left,ex.right,op);
+                                   un.addUpdate(up);
+                               } else if (e instanceof ElementOfExpr) {
+                                   Updates up=new Updates(e,de.getNegation());
+                                   un.addUpdate(up);
+                               } else if (e instanceof TupleOfExpr) {
+                                   Updates up=new Updates(e,de.getNegation());
+                                   un.addUpdate(up);
+                               } else throw new Error("Error #213");
+                           }
+                       }
+                       MultUpdateNode mun=new MultUpdateNode(ar);
+                       mun.addUpdate(un);
+                       TermNode tn=new TermNode(mun);
+                       GraphNode gn2=new GraphNode("Update"+addtocount,tn);
+                       GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
+                       addtocount++;
+                       gn.addEdge(e);
+                       updatenodes.add(gn2);
+                   }
                }
            }
        }
@@ -125,14 +398,28 @@ public class Termination {
            Rule r=(Rule) state.vRules.get(i);
            ScopeNode satisfy=new ScopeNode(r,true);
            TermNode tnsatisfy=new TermNode(satisfy);
-           GraphNode gnsatisfy=new GraphNode("Satisfy Rule"+i,tnsatisfy);
+           GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
+           ConsequenceNode cnsatisfy=new ConsequenceNode();
+           TermNode ctnsatisfy=new TermNode(cnsatisfy);
+           GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
+           consequence.put(satisfy,cgnsatisfy);
+           GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
+           gnsatisfy.addEdge(esat);
+           consequencenodes.add(cgnsatisfy);
+           scopesatisfy.put(r,gnsatisfy);
+           scopenodes.add(gnsatisfy);
 
            ScopeNode falsify=new ScopeNode(r,false);
            TermNode tnfalsify=new TermNode(falsify);
-           GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
-           scopesatisfy.put(r,gnsatisfy);
+           GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
+           ConsequenceNode cnfalsify=new ConsequenceNode();
+           TermNode ctnfalsify=new TermNode(cnfalsify);
+           GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
+           consequence.put(falsify,cgnfalsify);
+           GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
+           gnfalsify.addEdge(efals);
+           consequencenodes.add(cgnfalsify);
            scopefalsify.put(r,gnfalsify);
-           scopenodes.add(gnsatisfy);
            scopenodes.add(gnfalsify);
        }
     }

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
new file mode 100755 (executable)
index 0000000..3a02c37
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -0,0 +1,27 @@
+package MCC.IR;
+import java.util.*;
+
+class UpdateNode {
+    Vector updates;
+    Vector bindings;
+
+    public UpdateNode() {
+       updates=new Vector();
+       bindings=new Vector();
+    }
+
+    public void addBinding(Binding b) {
+       bindings.add(b);
+    }
+
+    public void addUpdate(Updates u) {
+       updates.add(u);
+    }
+
+    public int numUpdates() {
+       return updates.size();
+    }
+    public Updates getUpdate(int i) {
+       return (Updates)updates.get(i);
+    }
+}

diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
new file mode 100755 (executable)
index 0000000..7e4dbd3
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -0,0 +1,95 @@
+package MCC.IR;
+
+class Updates {
+    static public final int EXPR=0;
+    static public final int POSITION=1;
+    static public final int ABSTRACT=2;
+    int type=-1;
+    int rightposition;
+    Expr rightexpr;
+    Expr leftexpr;
+    Opcode opcode;
+    boolean negate;
+
+    public Updates(Expr lexpr, Expr rexpr, Opcode op) {
+       leftexpr=lexpr;
+       type=Updates.EXPR;
+       opcode=Opcode.EQ;
+       /* Get rid of everything but NE */
+       if (op==Opcode.GT) {
+           rightexpr=new OpExpr(Opcode.ADD,rexpr,new IntegerLiteralExpr(1));
+       } else if (op==Opcode.GE) {
+           rightexpr=rexpr;
+       } else if (op==Opcode.LT) {
+           rightexpr=new OpExpr(Opcode.SUB,rexpr,new IntegerLiteralExpr(1));
+       } else if (op==Opcode.LE) {
+           rightexpr=rexpr;
+       } else if (op==Opcode.EQ) {
+           rightexpr=rexpr;
+       } else if (op==Opcode.NE) {
+           opcode=Opcode.NE;
+       }
+    }
+
+    boolean isGlobal() {
+       if (leftexpr instanceof VarExpr)
+           return true;
+       else return false;
+    }
+
+    Descriptor getDescriptor() {
+       if (isGlobal()) {
+           return ((VarExpr)leftexpr).getVar();
+       } else if (isField()) {
+           return ((DotExpr)leftexpr).getField();
+       } else throw New Error("Unrecognized Update");
+    }
+
+    boolean isField() {
+       if (leftexpr instanceof DotExpr) {
+           assert ((DotExpr)leftexpr).getIndex()==null;
+           return true;
+       } else
+           return false;
+    }
+    
+    
+    Opcode getOpcode() {
+       return opcode;
+    }
+
+    public Updates(Expr lexpr, Expr rexpr) {
+       leftexpr=lexpr;
+       rightexpr=rexpr;
+       type=Updates.EXPR;
+       opcode=Opcode.EQ;
+    }
+
+    public Updates(Expr lexpr, int rpos) {
+       leftexpr=lexpr;
+       rightposition=rpos;
+       type=Updates.POSITION;
+       opcode=null;
+    }
+    public Updates(Expr lexpr,boolean negates) {
+       leftexpr=lexpr;
+       type=Updates.ABSTRACT;
+       negate=negates;
+       opcode=null;
+    }
+
+    public int getType() {
+       return type;
+    }
+    public Expr getLeftExpr() {
+       return leftexpr;
+    }
+    public int getRightPos() {
+       assert type==Updates.POSITION;
+       return rightposition;
+    }
+    public Expr getRightExpr() {
+       assert type==Updates.EXPR;
+       return rightexpr;
+    }
+}

diff --git a/Repair/RepairCompiler/MCC/Makefile b/Repair/RepairCompiler/MCC/Makefile
index b1d5648285f7d9c239557cd376f715d9ea043ff0..59652ed90e12468677e80fc70394707912c999d5 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Makefile
+++ b/Repair/RepairCompiler/MCC/Makefile
@@ -82,6 +82,7 @@ parser: $(PARSERS) $(SCANNER).java
 
 %.class: %.java
        javac -classpath ../ -source 1.4 $<
+#      jikes -classpath $(CLASSPATH):../ $<
 
 %.lex.java: %.lex
        java -classpath ../ JLex.Main $<