From 557d78d01153990302d2f007b2d66edd05f5544a Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Sun, 18 Jul 2004 19:20:26 +0000
Subject: [PATCH] More checkins...

---
 Repair/RepairCompiler/MCC/CLI.java            | 18 +++++--
 Repair/RepairCompiler/MCC/Compiler.java       |  2 +
 Repair/RepairCompiler/MCC/IR/CastExpr.java    |  8 +++
 .../MCC/IR/ConcreteInterferes.java            |  2 +-
 Repair/RepairCompiler/MCC/IR/DotExpr.java     |  2 +-
 Repair/RepairCompiler/MCC/IR/Expr.java        |  2 +-
 Repair/RepairCompiler/MCC/IR/GraphNode.java   | 19 +++++++
 .../RepairCompiler/MCC/IR/ImplicitSchema.java | 44 ++++++++++++---
 Repair/RepairCompiler/MCC/IR/Termination.java | 53 +++++++++++++------
 Repair/RepairCompiler/MCC/IR/Updates.java     | 30 +++++++----
 10 files changed, 143 insertions(+), 37 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java
index 88847f6..f1f5d87 100755
--- a/Repair/RepairCompiler/MCC/CLI.java
+++ b/Repair/RepairCompiler/MCC/CLI.java
@@ -1,7 +1,7 @@
 package MCC;
 
-import java.util.Vector;
-import java.util.StringTokenizer;
+import java.util.*;
+import MCC.IR.DebugItem;
 
 /**
  * A generic command-line interface for 6.035 compilers.  This class
@@ -11,7 +11,7 @@ import java.util.StringTokenizer;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.8 2004/05/31 14:19:10 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.9 2004/07/18 19:19:57 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -98,12 +98,24 @@ public class CLI {
 
         opts = new boolean[optnames.length];
 
+	if (args.length==0) {
+	    System.out.println("-debugcompiler -- print out debug messages");
+	    System.out.println("-depth depthnum constraintnum -- generate dependency graph from constraintnum with depf of depthnum");
+	    System.out.println("-instrument -- generate instrumentation code");
+	    System.out.println("-aggressivesearch");
+	    System.out.println("-prunequantifiernodes");
+	    System.exit(-1);
+	}
+
         for (int i = 0; i < args.length; i++) {
             if (args[i].equals("-debugcompiler")) {
                 context = 0;
                 debug = true;
 	    } else if (args[i].equals("-checkonly")) {
                 Compiler.REPAIR=false;
+	    } else if (args[i].equals("-depth")) {
+		Compiler.debuggraphs.add(new DebugItem(Integer.parseInt(args[i+1]),Integer.parseInt(args[i+2])));
+		i+=2;
 	    } else if (args[i].equals("-debug")) {
                 Compiler.GENERATEDEBUGHOOKS=true;
 	    } else if (args[i].equals("-instrument")) {
diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java
index 59609e9..a1f8bf6 100755
--- a/Repair/RepairCompiler/MCC/Compiler.java
+++ b/Repair/RepairCompiler/MCC/Compiler.java
@@ -24,6 +24,8 @@ public class Compiler {
     public static boolean GENERATEDEBUGHOOKS=false;
     public static boolean GENERATEDEBUGPRINT=false;
     public static boolean GENERATEINSTRUMENT=false;
+    
+    public static Vector debuggraphs=new Vector();
 
     public static void main(String[] args) {
         State state = null;
diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java
index c182a5d..0785749 100755
--- a/Repair/RepairCompiler/MCC/IR/CastExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java
@@ -7,6 +7,14 @@ public class CastExpr extends Expr {
     TypeDescriptor type;
     Expr expr;
 
+    public boolean isValue(TypeDescriptor td) {
+	if (td==null) /* Don't know type */
+	    return false;
+	if (!td.isSubtypeOf(type)) /* Not subtype of us */
+	    return false;
+	return expr.isValue(td);
+    }
+
     public Set freeVars() {
 	return expr.freeVars();
     }
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
index af193f7..f9e0c3a 100755
--- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -252,7 +252,7 @@ public class ConcreteInterferes {
 	    else if ((update_e instanceof DotExpr)&&(e instanceof DotExpr)) {
 		DotExpr de1=(DotExpr)update_e;
 		DotExpr de2=(DotExpr)e;
-		if (de1.isValue()&&!firstfield)
+		if (de1.isValue(null)&&!firstfield)
 		    return true; /* Could have aliasing from this */
 		if (de1.getField()!=de2.getField())
 		    return true; /* Different fields: not comparible */
diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 9fba88f..9361d5e 100755
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -340,7 +340,7 @@ public class DotExpr extends Expr {
         }
     }
 
-    public boolean isValue() {
+    public boolean isValue(TypeDescriptor td) {
 	FieldDescriptor tmpfd=fd;
 	if (tmpfd instanceof ArrayDescriptor)
 	    tmpfd=((ArrayDescriptor)tmpfd).getField();
diff --git a/Repair/RepairCompiler/MCC/IR/Expr.java b/Repair/RepairCompiler/MCC/IR/Expr.java
index aef0f28..d45280d 100755
--- a/Repair/RepairCompiler/MCC/IR/Expr.java
+++ b/Repair/RepairCompiler/MCC/IR/Expr.java
@@ -40,7 +40,7 @@ public abstract class Expr {
 	return null;
     }
 
-    public boolean isValue() {
+    public boolean isValue(TypeDescriptor td) {
 	return false;
     }
 
diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java
index d8d2649..601123e 100755
--- a/Repair/RepairCompiler/MCC/IR/GraphNode.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java
@@ -113,6 +113,25 @@ public class GraphNode {
 	}
     }
 
+    public static void boundedcomputeclosure(Collection nodes, Collection removed,int depth) {
+	Stack tovisit=new Stack();
+	tovisit.addAll(nodes);
+	for(int i=0;i<depth&&!tovisit.isEmpty();i++) {
+	    GraphNode gn=(GraphNode)tovisit.pop();
+	    for(Iterator it=gn.edges();it.hasNext();) {
+		Edge edge=(Edge)it.next();
+		GraphNode target=edge.getTarget();
+		if (!nodes.contains(target)) {
+		    if ((removed==null)||
+			(!removed.contains(target))) {
+			nodes.add(target);
+			tovisit.push(target);
+		    }
+		}
+	    }
+	}
+    }
+
     public void setDotNodeParameters(String param) {
         if (param == null) {
             throw new NullPointerException();
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
index 996083d..6947c03 100755
--- a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
+++ b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
@@ -29,6 +29,9 @@ public class ImplicitSchema {
 	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
 	if (sd instanceof ReservedSetDescriptor)
 	    return false;
+
+	/* See if there is a rule that adds the corresponding range or domain
+	   of the relation to the correct set */
 	for(int i=0;i<rules.size();i++) {
 	    Rule r=(Rule)rules.get(i);
 	    if ((r.numQuantifiers()==1)&&
@@ -45,8 +48,6 @@ public class ImplicitSchema {
 		    return false;
 	    }
 	}
-
-
 	for(int i=0;i<rules.size();i++) {
 	    Rule r=(Rule)rules.get(i);
 	    Inclusion inc=r.getInclusion();
@@ -55,9 +56,11 @@ public class ImplicitSchema {
 		boolean good=false;
 		RelationInclusion rinc=(RelationInclusion)inc;
 		Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
+		/* Check for varexpr's and quantification over */
 		if (expr instanceof VarExpr) {
 		    VarDescriptor vd=((VarExpr)expr).getVar();
 		    assert vd!=null;
+		    /* See if the var is from an appropriate quantifier */
 		    for (int j=0;j<r.numQuantifiers();j++) {
 			Quantifier q=r.getQuantifier(j);
 			if ((q instanceof SetQuantifier)&&
@@ -77,15 +80,15 @@ public class ImplicitSchema {
 			    good=true;
 			    break;
 			}
-			
 		    }
 		    if (good)
-			continue; /* Proved for this case */
+			continue; /* Checked for this case */
 		}
+		if (checkguard(r,isdomain))
+		    continue;
 		for(int j=0;j<rules.size();j++) {
 		    Rule r2=(Rule)rules.get(j);
 		    Inclusion inc2=r2.getInclusion();
-		    
 		    if (checkimplication(r,r2,isdomain)) {
 			good=true;
 			break;
@@ -94,12 +97,41 @@ public class ImplicitSchema {
 		if (good)
 		    continue;
 
-		return true; /* Couldn't prove we didn't need */
+		return true; /* Couldn't verify we didn't need */
 	    }
 	}
 	return false;
     }
 
+    boolean checkguard(Rule r,boolean isdomain) {
+	RelationInclusion inc=(RelationInclusion) r.getInclusion();
+	RelationDescriptor rd=inc.getRelation();
+	SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+	Expr expr=isdomain?inc.getLeftExpr():inc.getRightExpr();
+	DNFRule dnfGuard=r.getDNFGuardExpr();
+	for(int i=0;i<dnfGuard.size();i++) {
+	    RuleConjunction rconj=dnfGuard.get(i);
+	    boolean foundcheck=false;
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		if (!dexpr.getNegation()&&
+		    dexpr.getExpr() instanceof ElementOfExpr) {
+		    ElementOfExpr eoe=(ElementOfExpr)dexpr.getExpr();
+		    
+		    if (eoe.set==sd&&
+			eoe.element.equals(null,expr)) {
+			foundcheck=true;
+			break;
+		    }
+		}
+	    }
+	    if (!foundcheck) {
+		return false;
+	    }
+	}
+	return true;
+    }
+
     boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
 	/* r1 is the relation */
 	/* See if this rule guarantees relation */
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 32b4a1b..f5c8dac 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -88,6 +88,9 @@ public class Termination {
 	    e.printStackTrace();
 	    System.exit(-1);
 	}
+
+	generatedebuggraphs();
+
 	for(Iterator it=updatenodes.iterator();it.hasNext();) {
 	    GraphNode gn=(GraphNode)it.next();
 	    TermNode tn=(TermNode)gn.getOwner();
@@ -121,6 +124,24 @@ public class Termination {
 	constraintdependence.traversedependences(this);
     }
 
+    void generatedebuggraphs() {
+	for (int i=0;i<Compiler.debuggraphs.size();i++) {
+	    DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
+	    Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
+	    HashSet superset=new HashSet();
+	    superset.addAll((Set)conjunctionmap.get(constr));
+	    HashSet closureset=new HashSet();
+	    
+	    GraphNode.boundedcomputeclosure(superset,closureset,di.depth);
+	    try {
+		GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+".dot"),superset);
+	    } catch (Exception e) {
+		e.printStackTrace();
+		System.exit(-1);
+	    }
+	}
+    }
+
 
     /** This method generates a node for each conjunction in the DNF
      * form of each constraint.  It also converts the quantifiers into
@@ -682,8 +703,8 @@ public class Termination {
 		}
 		RelationInclusion ri=(RelationInclusion)r.getInclusion();
 		if (!(ri.getLeftExpr() instanceof VarExpr)) {
-		    if (ri.getLeftExpr().isValue()) {
-			Updates up=new Updates(ri.getLeftExpr(),leftindex);
+		    if (ri.getLeftExpr().isValue(ri.getRelation().getDomain().getType())) {
+			Updates up=new Updates(ri.getLeftExpr(),leftindex,ri.getRelation().getDomain().getType());
 			un.addUpdate(up);
 		    } else {
 			if (inverted)
@@ -693,14 +714,14 @@ public class Termination {
 		} else {
 		    VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 		    if (vd.isGlobal()) {
-			Updates up=new Updates(ri.getLeftExpr(),leftindex);
+			Updates up=new Updates(ri.getLeftExpr(),leftindex,null);
 			un.addUpdate(up);
 		    } else if (inverted)
 			goodflag=false;
 		}
 		if (!(ri.getRightExpr() instanceof VarExpr)) {
-		    if (ri.getRightExpr().isValue()) {
-			Updates up=new Updates(ri.getRightExpr(),rightindex);
+		    if (ri.getRightExpr().isValue(ri.getRelation().getRange().getType())) {
+			Updates up=new Updates(ri.getRightExpr(),rightindex,ri.getRelation().getRange().getType());
 			un.addUpdate(up);
 		    } else {
 			if (!inverted)
@@ -711,7 +732,7 @@ public class Termination {
 		} else {
 		    VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 		    if (vd.isGlobal()) {
-			Updates up=new Updates(ri.getRightExpr(),rightindex);
+			Updates up=new Updates(ri.getRightExpr(),rightindex,null);
 			un.addUpdate(up);
 		    } else if (!inverted) 
 			goodflag=false;
@@ -761,8 +782,8 @@ public class Termination {
 		    if(inc instanceof SetInclusion) {
 			SetInclusion si=(SetInclusion)inc;
 			if (!(si.elementexpr instanceof VarExpr)) {
-			    if (si.elementexpr.isValue()) {
-				Updates up=new Updates(si.elementexpr,0);
+			    if (si.elementexpr.isValue(si.getSet().getType())) {
+				Updates up=new Updates(si.elementexpr,0,si.getSet().getType());
 				un.addUpdate(up);
 			    } else {
 				/* We're an add to set*/
@@ -788,15 +809,15 @@ public class Termination {
 			} else {
 			    VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 			    if (vd.isGlobal()) {
-				Updates up=new Updates(si.elementexpr,0);
+				Updates up=new Updates(si.elementexpr,0,null);
 				un.addUpdate(up);
 			    }
 			}
 		    } else if (inc instanceof RelationInclusion) {
 			RelationInclusion ri=(RelationInclusion)inc;
 			if (!(ri.getLeftExpr() instanceof VarExpr)) {
-			    if (ri.getLeftExpr().isValue()) {
-				Updates up=new Updates(ri.getLeftExpr(),0);
+			    if (ri.getLeftExpr().isValue(ri.getRelation().getDomain().getType())) {
+				Updates up=new Updates(ri.getLeftExpr(),0,ri.getRelation().getDomain().getType());
 				un.addUpdate(up);
 			    } else {
 				/* We don't handly relation modifies */
@@ -818,13 +839,13 @@ public class Termination {
 			} else {
 			    VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 			    if (vd.isGlobal()) {
-				Updates up=new Updates(ri.getLeftExpr(),0);
+				Updates up=new Updates(ri.getLeftExpr(),0,null);
 				un.addUpdate(up);
 			    }
      			}
 			if (!(ri.getRightExpr() instanceof VarExpr)) {
-			    if (ri.getRightExpr().isValue()) {
-				Updates up=new Updates(ri.getRightExpr(),1);
+			    if (ri.getRightExpr().isValue(ri.getRelation().getRange().getType())) {
+				Updates up=new Updates(ri.getRightExpr(),1,ri.getRelation().getRange().getType());
 				un.addUpdate(up);
 			    } else {
 				/* We don't handly relation modifies */
@@ -846,7 +867,7 @@ public class Termination {
 			} else {
 			    VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 			    if (vd.isGlobal()) {
-				Updates up=new Updates(ri.getRightExpr(),1);
+				Updates up=new Updates(ri.getRightExpr(),1,null);
 				un.addUpdate(up);
 			    }
 			}
@@ -890,7 +911,7 @@ public class Termination {
 	    if (fd instanceof ArrayDescriptor) {
 		// We have an ArrayDescriptor!
 		Expr index=de.getIndex();
-		if (!index.isValue()) {/* Not assignable */
+		if (!index.isValue(null)) {/* Not assignable */
 		    System.out.println("ERROR:Index isn't assignable");
 		    return false;
 		}
diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
index acda79f..65e3839 100755
--- a/Repair/RepairCompiler/MCC/IR/Updates.java
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -26,7 +26,7 @@ class Updates {
     }
 
     public Updates(Expr lexpr, Expr rexpr, Opcode op, boolean negate) {
-	if (!lexpr.isValue())
+	if (!lexpr.isValue(null))
 	    System.out.println("Building invalid update");
 	leftexpr=lexpr;
 	type=Updates.EXPR;
@@ -38,7 +38,7 @@ class Updates {
     }
 
     public Updates(Expr lexpr, Expr rexpr) {
-	if (!lexpr.isValue())
+	if (!lexpr.isValue(null))
 	    System.out.println("Building invalid update");
 	leftexpr=lexpr;
 	rightexpr=rexpr;
@@ -46,8 +46,8 @@ class Updates {
 	opcode=Opcode.EQ;
     }
 
-    public Updates(Expr lexpr, int rpos) {
-	if (!lexpr.isValue())
+    public Updates(Expr lexpr, int rpos, TypeDescriptor td) {
+	if (!lexpr.isValue(td))
 	    System.out.println("Building invalid update");
 	leftexpr=lexpr;
 	rightposition=rpos;
@@ -83,10 +83,14 @@ class Updates {
     }
 
     Descriptor getDescriptor() {
+	Expr lexpr=leftexpr;
+	while (lexpr instanceof CastExpr)
+	    lexpr=((CastExpr)lexpr).getExpr();
+
 	if (isGlobal()) {
-	    return ((VarExpr)leftexpr).getVar();
+	    return ((VarExpr)lexpr).getVar();
 	} else if (isField()) {
-	    return ((DotExpr)leftexpr).getField();
+	    return ((DotExpr)lexpr).getField();
 	} else {
 	    System.out.println(toString());
 	    throw new Error("Unrecognized Update");
@@ -94,14 +98,22 @@ class Updates {
     }
 
     boolean isGlobal() {
-	if (leftexpr instanceof VarExpr)
+	Expr lexpr=leftexpr;
+	while (lexpr instanceof CastExpr)
+	    lexpr=((CastExpr)lexpr).getExpr();
+
+	if (lexpr instanceof VarExpr)
 	    return true;
 	else return false;
     }
 
     boolean isField() {
-	if (leftexpr instanceof DotExpr) {
-	    assert ((DotExpr)leftexpr).getIndex()==null;
+	Expr lexpr=leftexpr;
+	while (lexpr instanceof CastExpr)
+	    lexpr=((CastExpr)lexpr).getExpr();
+
+	if (lexpr instanceof DotExpr) {
+	    assert ((DotExpr)lexpr).getIndex()==null;
 	    return true;
 	} else
 	    return false;
-- 
2.34.1