From 818e376c5aeeeb458febe75f3d6273a94f3bcf7d Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Mon, 22 Dec 2003 01:28:34 +0000
Subject: [PATCH] updates

---
 Repair/RepairCompiler/MCC/Compiler.java       |   5 +-
 .../RepairCompiler/MCC/IR/DNFPredicate.java   |   4 +
 Repair/RepairCompiler/MCC/IR/Expr.java        |  16 +++
 .../RepairCompiler/MCC/IR/ExprPredicate.java  |  43 +++++-
 .../RepairCompiler/MCC/IR/ImageSetExpr.java   |  12 ++
 .../MCC/IR/InclusionPredicate.java            |  13 ++
 Repair/RepairCompiler/MCC/IR/OpExpr.java      |  43 ++++++
 Repair/RepairCompiler/MCC/IR/Predicate.java   |   6 +-
 .../RepairCompiler/MCC/IR/RelationExpr.java   |  15 ++
 .../MCC/IR/RelationFunctionExpr.java          |  11 ++
 Repair/RepairCompiler/MCC/IR/SetExpr.java     |   4 +
 Repair/RepairCompiler/MCC/IR/SizeofExpr.java  |  13 ++
 Repair/RepairCompiler/MCC/IR/Termination.java | 128 ++++++++++++------
 13 files changed, 263 insertions(+), 50 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 8f90540..e87c112 100755
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -54,9 +54,10 @@ 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.");
 
-	    if (REPAIR)
+	    if (REPAIR) {
 		(new ImplicitSchema(state)).update();
-
+		Termination t=new Termination(state);
+	    }
             
             (new DependencyBuilder(state)).calculate();
             
diff --git a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
index 2328bfc..a1e5a65 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
@@ -18,4 +18,8 @@ public class DNFPredicate {
     void negatePred() {
 	negate=!negate;
     }
+
+    boolean isNegated() {
+	return negate;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index cd82227..310e5ae 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -29,4 +29,20 @@ public abstract class Expr {
 	return new DNFRule(this);
     }
 
+    public Descriptor getDescriptor() {
+	return null;
+    }
+
+    public int[] getRepairs(boolean negated) {
+	return new int[0];
+    }
+
+    public boolean inverted() {
+	return false;
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	return false;
+    }
+
 }
diff --git a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
index 3242de1..43ac5ad 100755
--- a/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/ExprPredicate.java
@@ -3,14 +3,33 @@ package MCC.IR;
 import java.util.*;
 
 public class ExprPredicate extends Predicate {
-
+    
     Expr expr;
 
+
+    public static final int SIZE=1;
+    public static final int COMPARISON=2;
+
+    public int getType() {
+	if (((OpExpr)expr).left instanceof SizeofExpr)
+	    return SIZE;
+	else if (((OpExpr)expr).left instanceof RelationExpr)
+	    return COMPARISON;
+	else throw new Error("Unidentifiable Type");
+    }
+
+    public Opcode getOp() {
+	return ((OpExpr)expr).opcode;
+    }
+
+    public int leftsize() {
+	return ((IntegerLiteralExpr)((OpExpr)expr).right).getValue();
+    }
+
     public ExprPredicate(Expr expr) {
         if (expr == null) {
             throw new NullPointerException();
         }
-
         this.expr = expr;
     }
 
@@ -18,6 +37,22 @@ public class ExprPredicate extends Predicate {
         return expr.getInversedRelations();
     }
 
+    public int[] getRepairs(boolean negated) {
+	return expr.getRepairs(negated);
+    }
+
+    public Descriptor getDescriptor() {
+	return expr.getDescriptor();
+    }
+
+    public boolean inverted() {
+	return expr.inverted();
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	return expr.usesDescriptor(rd);
+    }
+
     public Set getRequiredDescriptors() {
         return expr.getRequiredDescriptors();
     }
@@ -25,9 +60,5 @@ public class ExprPredicate extends Predicate {
     public void generate(CodeWriter writer, VarDescriptor dest) {
         expr.generate(writer, dest);
     }
-
-    public int[] getRepairs(boolean negated) {
-	return new int[] {};
-    }
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
index c7f5079..66437e3 100755
--- a/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
@@ -22,6 +22,10 @@ public class ImageSetExpr extends SetExpr {
         this.inverse = inverse;
     }
 
+    public boolean inverted() {
+	return inverse;
+    }
+
     public VarDescriptor getVar() {
         return vd;
     }
@@ -30,6 +34,14 @@ public class ImageSetExpr extends SetExpr {
         return rd;
     }
 
+    public Descriptor getDescriptor() {
+	return rd;
+    }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	return (rd==this.rd);
+    }
+
     public Set getInversedRelations() {
         HashSet set = new HashSet();
         if (inverse) {
diff --git a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
index 26b9f4a..e0d0d77 100755
--- a/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
+++ b/Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
@@ -7,6 +7,11 @@ public class InclusionPredicate extends Predicate {
     Expr expr;
     SetExpr setexpr;
 
+    public boolean inverted() {
+	return setexpr.inverted();
+    }
+
+
     public InclusionPredicate(Expr expr, SetExpr setexpr) {
         if (expr == null) {
             throw new NullPointerException();
@@ -41,6 +46,13 @@ public class InclusionPredicate extends Predicate {
         //return set;
     }
 
+    public Descriptor getDescriptor() {
+	if (setexpr instanceof ImageSetExpr) {
+	    return ((ImageSetExpr)setexpr).getRelation();
+	} else
+	    return setexpr.sd;
+    }
+
     public int[] getRepairs(boolean negated) {
 	if (setexpr instanceof ImageSetExpr) {
 	    if (negated)
@@ -56,3 +68,4 @@ public class InclusionPredicate extends Predicate {
     }
 }
     
+
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index b576cbd..47a6fae 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -31,7 +31,50 @@ public class OpExpr extends Expr {
         } else throw new Error();
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	if (opcode==Opcode.GT||opcode==Opcode.GE||opcode==Opcode.LT||
+	    opcode==Opcode.LE||opcode==Opcode.EQ||opcode==Opcode.NE)
+	    return right.usesDescriptor(rd);
+	else
+	    return left.usesDescriptor(rd)||(right!=null&&right.usesDescriptor(rd));
+    }
+    
+    public int[] getRepairs(boolean negated) {
+	if (left instanceof RelationExpr)
+	    return new int[] {AbstractRepair.MODIFYRELATION};
+	if (left instanceof SizeofExpr) {
+	    boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
+	    if (isRelation) {
+		if (opcode==Opcode.EQ)
+		    return new int[] {AbstractRepair.ADDTORELATION,
+					  AbstractRepair.REMOVEFROMRELATION};
+		if (((opcode==Opcode.GE)&&!negated)||
+		    ((opcode==Opcode.LE)&&negated))
+		    return new int[]{AbstractRepair.ADDTORELATION};
+		else
+		    return new int[]{AbstractRepair.REMOVEFROMRELATION};
+	    } else {
+		if (opcode==Opcode.EQ)
+		    return new int[] {AbstractRepair.ADDTOSET,
+					  AbstractRepair.REMOVEFROMSET};
+		
+		if (((opcode==Opcode.GE)&&!negated)||
+		    ((opcode==Opcode.LE)&&negated))
+		    return new int[] {AbstractRepair.ADDTOSET};
+		else
+		    return new int[] {AbstractRepair.REMOVEFROMSET};
+	    }
+	}
+	throw new Error("BAD");
+    }
+    
+    public Descriptor getDescriptor() {
+	return left.getDescriptor();
+    }
 
+    public boolean inverted() {
+	return left.inverted();
+    }
 
     public Set getInversedRelations() {
         Set set = left.getInversedRelations();
diff --git a/Repair/RepairCompiler/MCC/IR/Predicate.java b/Repair/RepairCompiler/MCC/IR/Predicate.java
index 7ab2179..cb9aa39 100755
--- a/Repair/RepairCompiler/MCC/IR/Predicate.java
+++ b/Repair/RepairCompiler/MCC/IR/Predicate.java
@@ -7,6 +7,10 @@ public abstract class Predicate extends LogicStatement {
     public DNFConstraint constructDNF() {
 	return new DNFConstraint(this);
     }
-    public int[] getRepairs(boolean negated) {}
+    abstract public int[] getRepairs(boolean negated);
+    abstract public Descriptor getDescriptor();
+    abstract public boolean inverted();
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	return false;}
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
index 5a541f5..fc2a4c7 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java
@@ -17,11 +17,26 @@ public class RelationExpr extends Expr {
     public Expr getExpr() {
         return expr;
     }
+
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	if (rd==relation)
+	    return true;
+	else
+	    return expr.usesDescriptor(rd);
+    }
     
     public RelationDescriptor getRelation() {
         return relation;
     }
 
+    public Descriptor getDescriptor() {
+        return relation;
+    }
+
+    public boolean inverted() {
+        return inverse;
+    }
+
     public Set getInversedRelations() {
         Set set = expr.getInversedRelations();
         if (inverse) {
diff --git a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
index bb4050f..cfbde5d 100755
--- a/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/RelationFunctionExpr.java
@@ -17,6 +17,10 @@ public class RelationFunctionExpr extends Expr {
         this.rule = rule;
     }
 
+    public Descriptor getDescriptor() {
+	return relation;
+    }
+
     public RelationDescriptor getRelation() {
         return relation;
     }
@@ -31,6 +35,13 @@ public class RelationFunctionExpr extends Expr {
         return v;
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	if (rd==relation)
+	    return true;
+	else
+	    return expr.usesDescriptor(rd);
+    }
+
     public void generate(CodeWriter cr, VarDescriptor dest) {
         
         String destname = dest.getSafeSymbol();
diff --git a/Repair/RepairCompiler/MCC/IR/SetExpr.java b/Repair/RepairCompiler/MCC/IR/SetExpr.java
index b2a37cf..b084b8e 100755
--- a/Repair/RepairCompiler/MCC/IR/SetExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SetExpr.java
@@ -18,6 +18,10 @@ public class SetExpr extends Expr {
         return new HashSet();
     }
 
+    public Descriptor getDescriptor() {
+	return sd;
+    }
+
     public Set getRequiredDescriptors() {
         HashSet v = new HashSet();
         v.add(sd);
diff --git a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
index 09d37e4..3d7f9ac 100755
--- a/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/SizeofExpr.java
@@ -14,6 +14,19 @@ public class SizeofExpr extends Expr {
         this.setexpr = setexpr;
     }
 
+    public boolean usesDescriptor(RelationDescriptor rd) {
+	return setexpr.usesDescriptor(rd);
+    }
+
+
+    public Descriptor getDescriptor() {
+	return setexpr.getDescriptor();
+    }
+
+    public boolean inverted() {
+	return setexpr.inverted();
+    }
+
     public SetExpr getSetExpr() {
         return setexpr;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 14d144a..7f9adc0 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -1,18 +1,33 @@
 package MCC.IR;
 import java.util.*;
+import MCC.State;
 
-class Termination {
+public class Termination {
     HashSet conjunctions;
     Hashtable conjunctionmap;
 
     HashSet abstractrepair;
 
+    HashSet scopenodes;
+    Hashtable scopesatisfy;
+    Hashtable scopefalsify;
+
     State state;
 
     public Termination(State state) {
 	this.state=state;
+	conjunctions=new HashSet();
+	conjunctionmap=new Hashtable();
+	abstractrepair=new HashSet();
+	scopenodes=new HashSet();
+	scopesatisfy=new Hashtable();
+	scopefalsify=new Hashtable();
+
 	generateconjunctionnodes();
 	generaterepairnodes();
+	generateabstractedges();
+	generatedatastructureupdatenodes();
+	generatescopenodes();
     }
     
     void generateconjunctionnodes() {
@@ -29,6 +44,29 @@ class Termination {
 	}
     }
 
+    void generateabstractedges() {
+	for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+	    GraphNode gn=(GraphNode)absiterator.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    AbstractRepair ar=(AbstractRepair)tn.getAbstract();
+	
+	    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(ar,dp)) {
+			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+			gn.addEdge(e);
+			break;
+		    }
+		}
+	    }
+	}
+    }
+    
+
     void generaterepairnodes() {
 	for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 	    GraphNode gn=(GraphNode)conjiterator.next();
@@ -36,58 +74,66 @@ class Termination {
 	    Conjunction conj=tn.getConjunction();
 	    for(int i=0;i<conj.size();i++) {
 		DNFPredicate dp=conj.get(i);
-		int[] array=dp.getPredicate().getRepairs();
-		for {int j=0;j<array.length;j++) {
-		    AbstractRepair ar=new AbstractRepair(dp,array[j]);
-		    TermNode tn=new TermNode(ar);
-		    GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
-		    Edge e=new Edge("abstract",gn2);
+		int[] array=dp.getPredicate().getRepairs(dp.isNegated());
+		Descriptor d=dp.getPredicate().getDescriptor();
+		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.Edge e=new GraphNode.Edge("abstract",gn2);
 		    gn.addEdge(e);
 		    abstractrepair.add(gn2);
 		}
 	    }
 	}
     }
-}
-
-class AbstractRepair {
-    public final static int ADDTOSET=1;
-    public final static int REMOVEFROMSET=2;
-    public final static int ADDTORELATION=3;
-    public final static int REMOVEFROMRELATION=4;
-    public final static int MODIFYRELATION=5;
 
-    DNFPredicate torepair;
-    int type;
-
-    public AbstractRepair(DNFPredicate dp,int typ) {
-	torepair=dp;
-	type=typ;
+    void generatedatastructureupdatenodes() {
+	for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
+	    GraphNode gn=(GraphNode)absiterator.next();
+	    TermNode tn=(TermNode) gn.getOwner();
+	    AbstractRepair ar=tn.getAbstract();
+	    if (ar.getType()==AbstractRepair.ADDTOSET) {
+		generateaddtoset(ar);
+	    } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
+		generateremovefromset(ar);
+	    } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
+		generateaddtorelation(ar);
+	    } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
+		generateremovefromrelation(ar);
+	    } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+		generatemodifyrelation(ar);
+	    }
+	}
     }
-}
-
-class TermNode {
-    public final static int CONJUNCTION=1;
-    public final static int ABSTRACT=2;
 
-    Constraint constr;
-    Conjunction conj;
-    int type;
-    AbstractRepair repair;
+    void generateaddtoset(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
+		    
 
-    public TermNode(Constraint constr, Conjunction conj) {
-	this.constr=constr;
-	this.conj=conj;
-	type=CONJUNCTION;
+		}
+	    }
+	}
     }
 
-    public TermNode(AbstractRepair ar) {
-	repair=ar;
-	type=ABSTRACT;
-    }
+    void generatescopenodes() {
+	for(int i=0;i<state.vRules.size();i++) {
+	    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);
 
-    public Conjunction getConjunction() {
-	return conj;
+	    ScopeNode falsify=new ScopeNode(r,false);
+	    TermNode tnfalsify=new TermNode(falsify);
+	    GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
+	    scopesatisfy.put(r,gnsatisfy);
+	    scopefalsify.put(r,gnfalsify);
+	    scopenodes.add(gnsatisfy);
+	    scopenodes.add(gnfalsify);
+	}
     }
 }
-
-- 
2.34.1