From 9bcbac11e044182472d004a1873e2175ef0bea49 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 4 Feb 2004 15:39:15 +0000
Subject: [PATCH] Adding changes to cvs...

---
 Repair/RepairCompiler/MCC/Compiler.java       |  7 +++--
 .../RepairCompiler/MCC/IR/ImplicitSchema.java |  7 ++---
 Repair/RepairCompiler/MCC/IR/Quantifiers.java |  6 ++++
 Repair/RepairCompiler/MCC/IR/Rule.java        |  2 +-
 Repair/RepairCompiler/MCC/IR/Termination.java | 18 ++++++------
 Repair/RepairCompiler/MCC/IR/UpdateNode.java  | 28 ++++++++++++++++++-
 Repair/RepairCompiler/MCC/IR/Updates.java     |  5 ++--
 Repair/RepairCompiler/MCC/link.constraints    |  1 -
 8 files changed, 53 insertions(+), 21 deletions(-)
 create mode 100755 Repair/RepairCompiler/MCC/IR/Quantifiers.java

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index ad98137..7773d7f 100755
--- 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 1be0068..fc83967 100755
--- 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
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 017e788..806b3f8 100755
--- 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 f9ae3bb..271d9f2 100755
--- 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 31e954c..4cf7d54 100755
--- 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 e0492d4..2c83ad6 100755
--- 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 24c3075..9e0c61b 100755
--- 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;
 
-- 
2.34.1