Adding changes to cvs...

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index ad98137f3611e38fa7e0f4e8e4db01d4bac5f307..7773d7fa9a47dd14b57f61dfff0c9aab590c2fa5 100755 (executable)
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -17,7 +17,7 @@ import MCC.IR.*;
  */
 
 public class Compiler {
-    public static boolean REPAIR=false;
+    public static boolean REPAIR=true;
     
     public static void main(String[] args) {
         State state = null;
@@ -54,10 +54,11 @@ public class Compiler {
            success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
            success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
 
-           /* Check partition constraints */
-           (new ImplicitSchema(state)).update();
+
 
            if (REPAIR) {
+               /* Check partition constraints */
+               (new ImplicitSchema(state)).update();
                Termination t=new Termination(state);
            }
             state.printall();

diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 1be006833b5a50bd199929d0175afd9f8a17e376..fc8396716618b2b9e4c54a3694a7df4dd03d1581 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -11,7 +11,7 @@ public class ImplicitSchema {
     }
 
     public void update() {
-       //      updaterules();
+       updaterules();
        updateconstraints();
        updaterelationconstraints();
     }
@@ -101,12 +101,11 @@ public class ImplicitSchema {
           1. match up quantifiers
           2. check inclusion condition
           3. see if guard expr of set rule is more general */
-
        RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
        RelationDescriptor rd=inc1.getRelation();
        SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
        Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
-
+       
        Inclusion inc2=r2.getInclusion();
        if (!(inc2 instanceof SetInclusion))
            return false;
@@ -294,7 +293,7 @@ public class ImplicitSchema {
                    for(Iterator superit=supersets.iterator();superit.hasNext();) {
                        SetDescriptor sd1=(SetDescriptor)superit.next();
                        Rule nr=new Rule();
-                       nr.guard=r.guard;
+                       nr.setGuardExpr(r.getGuardExpr());
                        nr.quantifiers=r.quantifiers;
                        nr.isstatic=r.isstatic;
                        nr.isdelay=r.isdelay;

diff --git a/Repair/RepairCompiler/MCC/IR/Quantifiers.java b/Repair/RepairCompiler/MCC/IR/Quantifiers.java
new file mode 100755 (executable)
index 0000000..6e84e76
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Quantifiers.java
@@ -0,0 +1,6 @@
+package MCC.IR;
+
+public interface Quantifiers {
+    public int numQuantifiers();
+    public Quantifier getQuantifier(int i);
+}

diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java
index 017e788c9ab67204cab931148b12a653f65957a0..806b3f8085bd5bb0876a7fcfec8604fd8598ad0c 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Rule.java
+++ b/Repair/RepairCompiler/MCC/IR/Rule.java
@@ -9,7 +9,7 @@ public class Rule implements Quantifiers {
     Vector quantifiers = new Vector();
     boolean isstatic = false;
     boolean isdelay = false;
-    Expr guard = null;
+    private Expr guard = null;
     Inclusion inclusion = null;    
     SymbolTable st = new SymbolTable();
     DNFRule dnfguard=null,dnfnegguard=null;

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index f9ae3bb5d6c3e04a5be791b38df7dbc1997e056e..271d9f2fca7744ba18f945b9e12ef036da4e58bb 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -523,13 +523,13 @@ public class Termination {
 
     static int addtocount=0;
     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
-       System.out.println("Attempting to generate add to set");
-       System.out.println(ar.getPredicate().getPredicate().name());
-       System.out.println(ar.getPredicate().isNegated());
+       //      System.out.println("Attempting to generate add to set");
+       //System.out.println(ar.getPredicate().getPredicate().name());
+       //System.out.println(ar.getPredicate().isNegated());
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            /* See if this is a good rule*/
-           System.out.println(r.getGuardExpr().name());
+           //System.out.println(r.getGuardExpr().name());
            if ((r.getInclusion() instanceof SetInclusion&&
                ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
                (r.getInclusion() instanceof RelationInclusion&&
@@ -538,10 +538,10 @@ public class Termination {
                /* First solve for quantifiers */
                Vector bindings=new Vector();
                /* Construct bindings */
-               System.out.println("Attempting to generate add to set: #2");
+               //System.out.println("Attempting to generate add to set: #2");
                if (!constructbindings(bindings,r,false))
                    continue;
-               System.out.println("Attempting to generate add to set: #3");
+               //System.out.println("Attempting to generate add to set: #3");
                //Generate add instruction
                DNFRule dnfrule=r.getDNFGuardExpr();
                for(int j=0;j<dnfrule.size();j++) {
@@ -587,14 +587,14 @@ public class Termination {
                    //Finally build necessary updates to satisfy conjunction
                    RuleConjunction ruleconj=dnfrule.get(j);
                    /* Add in updates for quantifiers */
-                   System.out.println("Attempting to generate add to set #4");
+                   //System.out.println("Attempting to generate add to set #4");
                    MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
                    TermNode tn=new TermNode(mun);
                    GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 
                    if (processquantifers(gn2,un, r)&&debugdd()&&
                        processconjunction(un,ruleconj)) {
-                       System.out.println("Attempting to generate add to set #5");
+                       //System.out.println("Attempting to generate add to set #5");
                        mun.addUpdate(un);
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
                        addtocount++;
@@ -606,7 +606,7 @@ public class Termination {
     }
 
     boolean debugdd() {
-       System.out.println("Attempting to generate add to set DD");
+       //System.out.println("Attempting to generate add to set DD");
        return true;
     }
 

diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
index 31e954c03c053ca3764d979346fb627fb3075326..4cf7d54a7d85dec5d570d90c407ce8510ac0e8c9 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/UpdateNode.java
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -18,6 +18,33 @@ class UpdateNode {
        }
     }
 
+    public boolean checkconflicts() {
+       Set toremove=new HashSet();
+       for(int i=0;i<updates.size();i++) {
+           Updates u1=(Updates)updates.get(i);
+           for(int j=0;j<updates.size();j++) {
+               Updates u2=(Updates)updates.get(j);
+               if (u1.isAbstract()||u2.isAbstract())
+                   continue;  /* Abstract updates are already accounted for by graph */
+               if (u1.getDescriptor()!=u2.getDescriptor())
+                   continue; /* No interference - different descriptors */
+               
+               if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
+                   (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
+                   continue; /* Can be satisfied simultaneously */
+
+               if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
+                   (u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
+                   continue;
+               
+               
+               return false; /* They interfere */
+           }
+       }
+       updates.remove(toremove);
+       return false;
+    }
+
     public void addBinding(Binding b) {
        bindings.add(b);
        binding.put(b.getVar(),b);
@@ -30,7 +57,6 @@ class UpdateNode {
            return null;
     }
 
-
     public void addUpdate(Updates u) {
        updates.add(u);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
index e0492d426b976d06a22fb6dba17b1bbb4e04cd91..2c83ad63589d3f6ea2bd56b0059fd2d9b3415b63 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Updates.java
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -9,7 +9,7 @@ class Updates {
     Expr rightexpr;
     Expr leftexpr;
     Opcode opcode;
-    boolean negate;
+    boolean negate=false;
 
     public String toString() {
        String st="type="+type+"\n";
@@ -55,6 +55,7 @@ class Updates {
        } else if (op==Opcode.EQ) {
            rightexpr=rexpr;
        } else if (op==Opcode.NE) {
+           rightexpr=rexpr;
            opcode=Opcode.NE;
        }
     }
@@ -102,7 +103,7 @@ class Updates {
        leftexpr=lexpr;
        rightposition=rpos;
        type=Updates.POSITION;
-       opcode=null;
+       opcode=Opcode.EQ;
     }
 
     boolean isAbstract() {

diff --git a/Repair/RepairCompiler/MCC/link.constraints b/Repair/RepairCompiler/MCC/link.constraints
index 24c3075593927dd679cc1dfef5c98ce7d2be4c4e..9e0c61bfa65ca314943a6e573c0a348296f4efa7 100755 (executable)
--- a/Repair/RepairCompiler/MCC/link.constraints
+++ b/Repair/RepairCompiler/MCC/link.constraints
@@ -1,6 +1,5 @@
 [], sizeof(Nodes) >= literal(1);
 [forall node in Nodes], sizeof(node.~nextnodes) <= literal(1);
-[forall node in Nodes], sizeof(node.~prevnodes) <= literal(1);
 [forall n in Nodes], 
        sizeof(n.nextnodes) = literal(0) or n.nextnodes.prevnodes = n;