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
* 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 {
/**
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")) {
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;
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();
}
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 */
}
}
- public boolean isValue() {
+ public boolean isValue(TypeDescriptor td) {
FieldDescriptor tmpfd=fd;
if (tmpfd instanceof ArrayDescriptor)
tmpfd=((ArrayDescriptor)tmpfd).getField();
return null;
}
- public boolean isValue() {
+ public boolean isValue(TypeDescriptor td) {
return false;
}
}
}
+ 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();
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)&&
return false;
}
}
-
-
for(int i=0;i<rules.size();i++) {
Rule r=(Rule)rules.get(i);
Inclusion inc=r.getInclusion();
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)&&
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;
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 */
e.printStackTrace();
System.exit(-1);
}
+
+ generatedebuggraphs();
+
for(Iterator it=updatenodes.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
TermNode tn=(TermNode)gn.getOwner();
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
}
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)
} 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)
} 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;
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*/
} 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 */
} 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 */
} 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);
}
}
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;
}
}
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;
}
public Updates(Expr lexpr, Expr rexpr) {
- if (!lexpr.isValue())
+ if (!lexpr.isValue(null))
System.out.println("Building invalid update");
leftexpr=lexpr;
rightexpr=rexpr;
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;
}
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");
}
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;
projects / repair.git / commitdiff