1) Cleaned up CLI/Compiler classes that Dan provided.
2) Typecheck Constraints.
3) Repair dependence analysis (to order repair of constraints)
A) checks for functions
4) Added class to compute exact sizes of sets (and constraints which
establish these sizes)
* files.
*
* @author le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.2 2004/04/15 05:41:46 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.3 2004/04/21 21:15:48 bdemsky Exp $</tt>
*/
public class CLI {
- /**
- * Target value indicating that the compiler should produce its
- * default output.
- */
- public static final int DEFAULT = 0;
-
- /**
- * Target value indicating that the compiler should scan the input
- * and stop.
- */
- public static final int SCAN = 1;
-
- /**
- * Target value indicating that the compiler should scan and parse
- * its input, and stop.
- */
- public static final int PARSE = 2;
-
- /**
- * Target value indicating that the compiler should produce a
- * high-level intermediate representation from its input, and stop.
- * This is not one of the segment targets for Fall 2000, but you
- * may wish to use it for your own purposes.
- */
- public static final int INTER = 3;
-
- /**
- * Target value indicating that the compiler should produce a
- * low-level intermediate representation from its input, and stop.
- */
- public static final int LOWIR = 4;
-
- /**
- * Target value indicating that the compiler should produce
- * assembly from its input.
- */
- public static final int ASSEMBLY = 5;
-
/**
* Array indicating which optimizations should be performed. If
* a particular element is true, it indicates that the optimization
*/
public String infile;
- /**
- * The target stage. This should be one of the integer constants
- * defined elsewhere in this package.
- */
- public int target;
-
/**
* The debug flag. This is true if <tt>-debug</tt> was passed on
* the command line, requesting debugging output.
*/
public boolean debug;
- /**
- * Native MIPS architecture is specified by "-native". The default
- * is SPIM.
- */
- public boolean fNative;
-
- /**
- * Runs IRVis on final node tree.
- */
- public boolean fVis;
- public String visClass;
- public String visMethod;
-
- /**
- * Dumps the before and after Node structure to two files that can be diffed.
- */
- public boolean fDiff;
- public String diffFile;
-
- /**
- * Maximum optimization iterations.
- */
- public int numIterations = 5;
-
/**
* Verbose output
*/
public CLI() {
outfile = null;
infile = null;
- target = DEFAULT;
extras = new Vector();
extraopts = new Vector();
- fNative = false;
- fVis = false;
verbose = 0;
- visClass = "";
- visMethod = "";
- fDiff = false;
- diffFile = "";
}
/**
if (args[i].equals("-debug")) {
context = 0;
debug = true;
- } else if (args[i].equals("-native")) {
- context = 0;
- fNative = true;
} else if (args[i].equals("-checkonly")) {
Compiler.REPAIR=false;
- } else if (args[i].equals("-vis")) {
- context = 4;
- fVis = true;
- } else if (args[i].equals("-diff")) {
- context = 5;
- fDiff = true;
- } else if (args[i].equals("-i")) {
- context = 6;
} else if (args[i].equals("-verbose") || args[i].equals("-v")) {
context = 0;
verbose++;
context = 1;
else if (args[i].equals("-o"))
context = 2;
- else if (args[i].equals("-target"))
- context = 3;
else if (context == 1) {
boolean hit = false;
for (int j = 0; j < optnames.length; j++) {
}
if (!hit)
extraopts.addElement(args[i]);
- }
- else if (context == 2) {
+ } else if (context == 2) {
outfile = args[i];
context = 0;
- }
- else if (context == 3) {
- // Process case insensitive.
- String argSansCase = args[i].toLowerCase();
- // accept "scan" and "scanner" due to handout mistake
- if (argSansCase.equals("scan") ||
- argSansCase.equals("scanner"))
- target = SCAN;
- else if (argSansCase.equals("parse"))
- target = PARSE;
- else if (argSansCase.equals("inter"))
- target = INTER;
- else if (argSansCase.equals("lowir"))
- target = LOWIR;
- else if (argSansCase.equals("assembly") ||
- argSansCase.equals("codegen"))
- target = ASSEMBLY;
- else
- target = DEFAULT; // Anything else is just default
- context = 0;
- } else if (context == 4) { // -vis
- StringTokenizer st = new StringTokenizer(args[i], ".");
- visClass = st.nextToken();
- visMethod = st.nextToken();
- context = 0;
- } else if (context == 5) { // -diff
- diffFile = args[i]; // argument following is filename
- context = 0;
- } else if (context == 6) { // -i <iterations>
- numIterations = Integer.parseInt(args[i]);
- context = 0;
} else {
boolean hit = false;
for (int j = 0; j < optnames.length; j++) {
}
i++;
}
-
- // create outfile name
- switch (target) {
- case SCAN:
- ext = ".scan";
- break;
- case PARSE:
- ext = ".parse";
- break;
- case INTER:
- ext = ".ir";
- break;
- case LOWIR:
- ext = ".lowir";
- break;
- case ASSEMBLY:
- ext = ".s";
- break;
- case DEFAULT:
- default:
- ext = ".out";
- break;
- }
-
- if (outfile == null && infile != null) {
- int dot = infile.lastIndexOf('.');
- int slash = infile.lastIndexOf('/');
- // Last dot comes after last slash means that the file
- // has an extention. Note that the base case where dot
- // or slash are -1 also work.
- if (dot <= slash)
- outfile = infile + ext;
- else
- outfile = infile.substring(0, dot) + ext;
- }
}
}
System.exit(-1);
}
- if (cli.target == CLI.ASSEMBLY || cli.target == CLI.DEFAULT) {
- if (state.debug) {
- System.out.println("Compiling " + cli.infile + ".");
- }
-
- success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
- success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
- success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
-
-
- Termination termination=null;
- /* Check partition constraints */
- (new ImplicitSchema(state)).update();
- termination=new Termination(state);
-
- state.printall();
- (new DependencyBuilder(state)).calculate();
-
- try {
- Vector nodes = new Vector(state.constraintnodes.values());
- nodes.addAll(state.rulenodes.values());
-
- FileOutputStream dotfile;
- dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
- GraphNode.useEdgeLabels = true;
- GraphNode.DOTVisitor.visit(dotfile, nodes);
- dotfile.close();
-
- dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");
- GraphNode.useEdgeLabels = false;
- GraphNode.DOTVisitor.visit(dotfile, nodes);
- dotfile.close();
- } catch (Exception e) {
- e.printStackTrace();
- System.exit(-1);
- }
-
- try {
- FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
-
-
- // do model optimizations
- //(new Optimizer(state)).optimize();
-
-
-
- FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
- FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
- RepairGenerator wg = new RepairGenerator(state,termination);
- wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
- gcode2.close();
- gcode3.close();
- /* } else {
- WorklistGenerator ng = new WorklistGenerator(state);
+ if (state.debug) {
+ System.out.println("Compiling " + cli.infile + ".");
+ }
+
+ success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
+ success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
+ success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
+
+
+ Termination termination=null;
+ /* Check partition constraints */
+ (new ImplicitSchema(state)).update();
+ termination=new Termination(state);
+
+ state.printall();
+ (new DependencyBuilder(state)).calculate();
+
+ try {
+ Vector nodes = new Vector(state.constraintnodes.values());
+ nodes.addAll(state.rulenodes.values());
+
+ FileOutputStream dotfile;
+ dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
+ GraphNode.useEdgeLabels = true;
+ GraphNode.DOTVisitor.visit(dotfile, nodes);
+ dotfile.close();
+
+ dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");
+ GraphNode.useEdgeLabels = false;
+ GraphNode.DOTVisitor.visit(dotfile, nodes);
+ dotfile.close();
+ } catch (Exception e) {
+ e.printStackTrace();
+ System.exit(-1);
+ }
+
+ try {
+ FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
+
+
+ // do model optimizations
+ //(new Optimizer(state)).optimize();
+
+ FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
+ FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
+ RepairGenerator wg = new RepairGenerator(state,termination);
+ wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
+ gcode2.close();
+ gcode3.close();
+ /* } else {
+ WorklistGenerator ng = new WorklistGenerator(state);
SetInclusion.worklist=true;
RelationInclusion.worklist=true;
ng.generate(gcode);
}*/
- gcode.close();
- } catch (Exception e) {
- e.printStackTrace();
- System.exit(-1);
- }
-
- if (state.debug) {
- System.out.println("Compilation of " + state.infile + " successful.");
- System.out.println("#SUCCESS#");
- }
- } else if (cli.target == CLI.INTER) {
- if (state.debug) {
- System.out.println("Semantic analysis for " + cli.infile + ".");
- }
-
- success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
- success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
- success = semantics(state) || error(state, "Semantic analysis failed.");
-
- if (state.debug) {
- System.out.println("Semantic analysis of " + state.infile + " successful.");
- System.out.println("#SUCCESS#");
- }
- } else if (cli.target == CLI.PARSE) {
- if (state.debug) {
- System.out.println("Parsing " + cli.infile + ".");
- }
-
- success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
- success = parse(state) || error(state, "Parsing failed.");
-
- if (state.debug) {
- System.out.println("Parsing of " + state.infile + " successful.");
- System.out.println("#SUCCESS#");
- }
- } else if (cli.target == CLI.SCAN) {
- if (state.debug) {
- System.out.println("Scanning " + cli.infile + ".");
- }
-
- success = scan(state) || error(state, "Scanning failed.");
-
- if (state.debug) {
- System.out.println("Scanning of " + state.infile + " successful.");
- System.out.println("#SUCCESS#");
- }
- }
+ gcode.close();
+ } catch (Exception e) {
+ e.printStackTrace();
+ System.exit(-1);
+ }
+
+ if (state.debug) {
+ System.out.println("Compilation of " + state.infile + " successful.");
+ System.out.println("#SUCCESS#");
+ }
}
private static void printArgInfo(CLI cli) {
System.out.println("Printing debugging information...");
System.out.println("Input filename: " + cli.infile);
System.out.println("Output filename: " + cli.outfile);
- System.out.print("Target: ");
-
- switch(cli.target) {
- case CLI.ASSEMBLY:
- System.out.println("ASSEMBLY");
- break;
- case CLI.DEFAULT:
- System.out.println("DEFAULT");
- break;
- case CLI.INTER:
- System.out.println("INTER");
- break;
- case CLI.LOWIR:
- System.out.println("LOWIR");
- break;
- case CLI.PARSE:
- System.out.println("PARSE");
- break;
- case CLI.SCAN:
- System.out.println("SCAN");
- break;
- default:
- System.out.println("not recognized");
- break;
- }
for (int i = 0; i < cli.opts.length; i++) {
if (cli.opts[i]) {
predicates.add(pred);
}
Conjunction(Vector preds){
- predicates=preds ;
+ predicates=preds;
}
String name() {
String name="";
set.addAll(getRequiredDescriptorsFromLogicStatement());
return set;
}
-
}
--- /dev/null
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+public class ConstraintDependence {
+ State state;
+ HashSet constnodes;
+ HashSet nodes;
+ Hashtable constonode;
+ Hashtable nodetonode;
+ Termination termination;
+
+ ConstraintDependence(State state, Termination t) {
+ this.state=state;
+ this.termination=t;
+ constnodes=new HashSet();
+ nodes=new HashSet();
+ constonode=new Hashtable();
+ nodetonode=new Hashtable();
+ constructnodes();
+ constructconjunctionnodes();
+ constructconjunctionedges();
+ }
+
+ public void addNode(GraphNode gn) {
+ GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
+ nodes.add(gn2);
+ nodetonode.put(gn,gn2);
+ }
+
+ public void associateWithConstraint(GraphNode gn, Constraint c) {
+ GraphNode ggn=(GraphNode)nodetonode.get(gn);
+ GraphNode gc=(GraphNode)constonode.get(c);
+ GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
+ gc.addEdge(e);
+ }
+
+ public void requiresConstraint(GraphNode gn, Constraint c) {
+ GraphNode ggn=(GraphNode)nodetonode.get(gn);
+ GraphNode gc=(GraphNode)constonode.get(c);
+ GraphNode.Edge e=new GraphNode.Edge("requires",gc);
+ ggn.addEdge(e);
+ }
+
+ /** Constructs a node for each Constraint */
+ private void constructnodes() {
+ for(int i=0;i<state.vConstraints.size();i++) {
+ Constraint c=(Constraint)state.vConstraints.get(i);
+ GraphNode gn=new GraphNode(c.toString(),c);
+ constonode.put(c,gn);
+ constnodes.add(gn);
+ }
+ }
+
+ private void constructconjunctionnodes() {
+ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode conjnode=(GraphNode)it.next();
+ TermNode tn=(TermNode)conjnode.getOwner();
+ Conjunction conj=tn.getConjunction();
+ addNode(conjnode);
+ }
+ for(int i=0;i<state.vConstraints.size();i++) {
+ Constraint c=(Constraint)state.vConstraints.get(i);
+ Set conjset=(Set)termination.conjunctionmap.get(c);
+ for(Iterator it=conjset.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ associateWithConstraint(gn,c);
+ }
+ }
+ }
+
+ private void constructconjunctionedges() {
+ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode conjnode=(GraphNode)it.next();
+ TermNode tn=(TermNode)conjnode.getOwner();
+ Conjunction conj=tn.getConjunction();
+ for(int i=0;i<conj.size();i++) {
+ DNFPredicate dpred=conj.get(i);
+ Predicate pred=dpred.getPredicate();
+ Expr expr=null;
+ if (pred instanceof InclusionPredicate) {
+ InclusionPredicate ip=(InclusionPredicate)pred;
+ expr=ip.expr;
+ } else if (pred instanceof ExprPredicate) {
+ ExprPredicate ep=(ExprPredicate)pred;
+ expr=ep.expr;
+ } else throw new Error("Unrecognized Predicate");
+ Set functions=expr.getfunctions();
+ if (functions==null)
+ continue;
+ for(Iterator fit=functions.iterator();fit.hasNext();) {
+ Function f=(Function)fit.next();
+ if (rulesensurefunction(f))
+ continue; //no constraint needed to ensure
+
+ Set s=providesfunction(f);
+ if (s.size()==0) {
+ System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+ System.exit(-1);
+ }
+ Constraint c=(Constraint)s.iterator().next(); //Take the first one
+ requiresConstraint(conjnode,c);
+ }
+ }
+ }
+ }
+
+ private boolean rulesensurefunction(Function f) {
+ boolean foundrule=false;
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule)state.vRules.get(i);
+ if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
+ RelationInclusion ri=(RelationInclusion)r.getInclusion();
+ Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
+ SetDescriptor sd=e.getSet();
+ if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
+ continue; /* This rule doesn't effect the function */
+ if (foundrule) /* two different rules are a problem */
+ return false;
+ if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
+ return false;
+ VarExpr ve=(VarExpr)e;
+ Quantifier q=r.getQuantifier(0);
+ if (!(q instanceof SetQuantifier))
+ return false;
+ SetQuantifier sq=(SetQuantifier)q;
+ if (ve.getVar()!=sq.getVar())
+ return false;
+ if (!sq.getSet().isSubset(f.getSet()))
+ return false;
+ if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+ ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+ return false;
+ Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
+ if (e2.isSafe())
+ foundrule=true;
+ else
+ return false;
+ }
+ }
+ return foundrule;
+ }
+
+ private Set providesfunction(Function f) {
+ HashSet set=new HashSet();
+ for(int i=0;i<state.vConstraints.size();i++) {
+ Constraint c=(Constraint)state.vConstraints.get(i);
+ boolean goodconstraint=true;
+ DNFConstraint dnfconst=c.dnfconstraint;
+ for(int j=0;j<dnfconst.size();j++) {
+ Conjunction conj=dnfconst.get(j);
+ boolean conjprovides=false;
+ for(int k=0;k<conj.size();k++) {
+ DNFPredicate dpred=conj.get(k);
+ if (!dpred.isNegated()&&
+ (dpred.getPredicate() instanceof ExprPredicate)&&
+ ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
+ ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
+ if (ep.isRightInt()&&
+ ep.rightSize()==1&&
+ ep.getOp()==Opcode.EQ&&
+ ep.inverted()==f.isInverse()&&
+ ep.getDescriptor()==f.getRelation()) {
+ ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
+ VarDescriptor vd=se.getVar();
+ if (c.numQuantifiers()==1) {
+ for(int l=0;l<c.numQuantifiers();l++) {
+ Quantifier q=c.getQuantifier(l);
+ if (q instanceof SetQuantifier&&
+ ((SetQuantifier)q).getVar()==vd) {
+ SetDescriptor sd=((SetQuantifier)q).getSet();
+ if (sd.isSubset(f.getSet()))
+ conjprovides=true;
+ }
+ }
+ } else
+ break;
+ }
+ }
+ }
+ if (!conjprovides) {
+ goodconstraint=false;
+ break;
+ }
+ }
+ if (goodconstraint)
+ set.add(c);
+ }
+ return set;
+ }
+
+ public static class Function {
+ private RelationDescriptor rd;
+ private SetDescriptor sd;
+ private boolean inverse;
+
+ public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+ this.inverse=inverse;
+ this.sd=sd;
+ this.rd=r;
+ }
+
+ public SetDescriptor getSet() {
+ return sd;
+ }
+
+ public RelationDescriptor getRelation() {
+ return rd;
+ }
+
+ public boolean isInverse() {
+ return inverse;
+ }
+ }
+
+}
static boolean DOTYPECHECKS=false;
static boolean DONULL=false;
+ public boolean isSafe() {
+ if (!left.isSafe())
+ return false;
+ FieldDescriptor tmpfd=fd;
+ if (tmpfd instanceof ArrayDescriptor)
+ return false; // Arrays could be out of bounds
+ if (tmpfd.getPtr()) // Pointers cound be invalid
+ return false;
+ return true;
+ }
+
public void findmatch(Descriptor d, Set s) {
if (d==fd)
s.add(this);
--- /dev/null
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+
+class ExactSize {
+ State state;
+ private Hashtable sizemap;
+ private Hashtable constraintmap;
+
+ public ExactSize(State state) {
+ this.state=state;
+ this.sizemap=new Hashtable();
+ this.constraintmap=new Hashtable();
+ computesizes();
+ }
+
+ public int getsize(SetDescriptor sd) {
+ if (sizemap.contains(sd))
+ return ((Integer)sizemap.get(sd)).intValue();
+ else
+ return -1;
+ }
+ public Constraint getConstraint(SetDescriptor sd) {
+ return (Constraint)constraintmap.get(sd);
+ }
+
+ private void computesizes() {
+ for(Iterator it=state.stSets.descriptors();it.hasNext();) {
+ SetDescriptor sd=(SetDescriptor)it.next();
+ for(int i=0;i<state.vConstraints.size();i++) {
+ Constraint c=(Constraint)state.vConstraints.get(i);
+ DNFConstraint dconst=c.dnfconstraint;
+ int oldsize=-1;
+ boolean matches=true;
+ for(int j=0;j<dconst.size();j++) {
+ Conjunction conj=dconst.get(j);
+ boolean goodmatch=false;
+ for(int k=0;k<conj.size();k++) {
+ DNFPredicate dpred=conj.get(k);
+ if (!dpred.isNegated()) {
+ Predicate p=dpred.getPredicate();
+ if (p instanceof ExprPredicate) {
+ ExprPredicate ep=(ExprPredicate)p;
+ if (ep.getType()==ExprPredicate.SIZE&&
+ ep.getOp()==Opcode.EQ&&
+ ep.getDescriptor()==sd&&
+ ep.isRightInt()) {
+ if (k==0) {
+ oldsize=ep.rightSize();
+ } else {
+ if (oldsize==ep.rightSize()) {
+ goodmatch=true;
+ break;
+ }
+ }
+ }
+ }
+ }
+ }
+ if (!goodmatch) {
+ matches=false;
+ break; //this constraint won't work
+ }
+ }
+ if (matches) {
+ sizemap.put(sd,new Integer(oldsize));
+ constraintmap.put(sd,c);
+ }
+ }
+ }
+ }
+}
public void findmatch(Descriptor d, Set s) {
}
+
+ public Set getfunctions() {
+ return null;
+ }
+
+ public SetDescriptor getSet() {
+ throw new Error("No Set for this Expr");
+ }
+
+ public boolean isSafe() {
+ return true;
+ }
}
public static final int SIZE=1;
public static final int COMPARISON=2;
+ public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+ TypeDescriptor t=expr.typecheck(sa);
+ return t;
+ }
+
public String name() {
return expr.name();
}
}
public int rightSize() {
+ assert isRightInt();
return OpExpr.getInt(((OpExpr)expr).right);
}
Expr expr;
SetExpr setexpr;
+ public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+ TypeDescriptor t=expr.typecheck(sa);
+ TypeDescriptor ts=setexpr.typecheck(sa);
+ if (t!=ts)
+ return null;
+
+ return ReservedTypeDescriptor.INT;
+ }
+
public boolean inverted() {
return setexpr.inverted();
}
return set;
}
+ public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+ TypeDescriptor lt=left.typecheck(sa);
+ if (lt!=ReservedTypeDescriptor.INT)
+ return null;
+ TypeDescriptor rt;
+ if (op!=NOT) {
+ rt=right.typecheck(sa);
+ if (rt!=ReservedTypeDescriptor.INT)
+ return null;
+ }
+ return ReservedTypeDescriptor.INT;
+ }
+
public DNFConstraint constructDNF() {
if (op==AND) {
DNFConstraint leftd=left.constructDNF();
Expr right;
Opcode opcode;
+ public boolean isSafe() {
+ if (right==null)
+ return left.isSafe();
+ return left.isSafe()&&right.isSafe();
+ }
+
+ public Set getfunctions() {
+ Set leftfunctions=left.getfunctions();
+ Set rightfunctions=right.getfunctions();
+ if (leftfunctions!=null&&rightfunctions!=null) {
+ HashSet functions=new HashSet();
+ functions.addAll(leftfunctions);
+ functions.addAll(rightfunctions);
+ return functions;
+ }
+ if (leftfunctions!=null)
+ return leftfunctions;
+ return rightfunctions;
+ }
+
public void findmatch(Descriptor d, Set s) {
left.findmatch(d,s);
if (right!=null)
RelationDescriptor relation;
boolean inverse;
+ public Set getfunctions() {
+ HashSet functions=new HashSet();
+ Set exprfunctions=expr.getfunctions();
+ if (exprfunctions!=null)
+ functions.addAll(exprfunctions);
+ functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse));
+
+ return functions;
+ }
+
+ public SetDescriptor getSet() {
+ if (inverse)
+ return relation.domain;
+ else
+ return relation.range;
+ }
+
public RelationExpr(Expr expr, RelationDescriptor relation, boolean inverse) {
this.expr = expr;
this.relation = relation;
{
final SymbolTable st = constraint.getSymbolTable();
- CodeWriter cr = new StandardCodeWriter(outputaux) {
- public SymbolTable getSymbolTable() { return st; }
- };
+ CodeWriter cr = new StandardCodeWriter(outputaux);
+ cr.pushSymbolTable(constraint.getSymbolTable());
+
cr.outputline("// checking " + escape(constraint.toString()));
cr.startblock();
ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
OpExpr expr=(OpExpr)ep.expr;
Opcode opcode=expr.getOpcode();
- {
- boolean negated=dpred.isNegated();
- if (negated)
- if (opcode==Opcode.GT) {
- opcode=Opcode.LE;
- } else if (opcode==Opcode.GE) {
- opcode=Opcode.LT;
- } else if (opcode==Opcode.LT) {
- opcode=Opcode.GE;
- } else if (opcode==Opcode.LE) {
- opcode=Opcode.GT;
- } else if (opcode==Opcode.EQ) {
- opcode=Opcode.NE;
- } else if (opcode==Opcode.NE) {
- opcode=Opcode.EQ;
- } else {
- throw new Error("Unrecognized Opcode");
- }
- }
+ opcode=Opcode.translateOpcode(dpred.isNegated(),opcode);
+
MultUpdateNode munremove;
MultUpdateNode munadd;
} else {
throw new Error("Unrecognized Opcode");
}
+
+// In some cases the analysis has determined that generating removes
+// is unnecessary
+ if (generateremove&&munremove==null)
+ generateremove=false;
+
Descriptor d=ep.getDescriptor();
if (generateremove) {
cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
boolean ok = true;
ParseNodeVector constraints = pn.getChildren();
-
+
for (int i = 0; i < constraints.size(); i++) {
ParseNode constraint = constraints.elementAt(i);
assert constraint.getLabel().equals("constraint");
/* do any post checks... (type constraints, etc?) */
+ Iterator consiterator = state.vConstraints.iterator();
+
+ while (consiterator.hasNext()) {
+ Constraint cons = (Constraint) consiterator.next();
+
+ final SymbolTable consst = cons.getSymbolTable();
+ SemanticAnalyzer sa = new SemanticAnalyzer() {
+ public IRErrorReporter getErrorReporter() { return er; }
+ public SymbolTable getSymbolTable() { return consst; }
+ };
+
+ TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
+
+ if (constype == null) {
+ ok = false;
+ } else if (constype != ReservedTypeDescriptor.INT) {
+ er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
+ ok = false;
+ }
+ }
+
return ok;
}
}
}
}
-
+
/* get body */
LogicStatement logicexpr = parse_body(pn.getChild("body"));
assert sts.empty();
/* add to vConstraints */
- vConstraints.addElement(constraint);
+ vConstraints.addElement(constraint);
return ok;
}
SetDescriptor set = parse_set(pn.getChild("set"));
assert set != null;
sq.setSet(set);
+ vd.setSet(set);
vd.setType(set.getType());
rq.setRelation(rd);
vd1.setType(rd.getDomain().getType());
+ vd1.setSet(rd.getDomain());
vd2.setType(rd.getRange().getType());
+ vd2.setSet(rd.getRange());
return rq;
} else if (pn.getChild("for") != null) { /* for j = x to y */
ForQuantifier fq = new ForQuantifier();
return null;
}
+ vd.setSet(lookupSet("int", false));
vd.setType(ReservedTypeDescriptor.INT);
fq.setVar(vd);
}
}
}
-
- } else {
+ } else {
throw new IRException("shouldn't be any other typedescriptor classes");
}
-
}
// #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
/* do semantic check and if valid, add it to symbol table
and add it to the quantifier as well */
if (sts.peek().contains(varname)) {
- return new VarDescriptor(varname);
+ VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
+ return vdold;
+ /* Dan was creating a new VarDescriptor...This seems
+ like the wrong thing to do. We'll just lookup the
+ other one.
+ --------------------------------------------------
+ VarDescriptor vd=new VarDescriptor(varname);
+ vd.setSet(vdold.getSet()); return vd;*/
} else {
/* Semantic Error: undefined variable */
er.report(pn, "Undefined variable '" + varname + "'");
TypeDescriptor td=sd.getType();
Expr e=td.getSizeExpr();
VarDescriptor size=VarDescriptor.makeNew("size");
+ cr.pushSymbolTable(state.stGlobals);
e.generate(cr, size);
+ cr.popSymbolTable();
cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
}
TypeDescriptor td=sd.getType();
Expr e=td.getSizeExpr();
VarDescriptor size=VarDescriptor.makeNew("size");
+ cr.pushSymbolTable(state.stGlobals);
e.generate(cr, size);
+ cr.popSymbolTable();
cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
}
ComputeMaxSize maxsize;
State state;
AbstractInterferes abstractinterferes;
-
+ ConstraintDependence constraintdependence;
+ ExactSize exactsize;
public Termination(State state) {
this.state=state;
if (!Compiler.REPAIR)
return;
-
+
for(int i=0;i<state.vRules.size();i++)
System.out.println(state.vRules.get(i));
for(int i=0;i<state.vConstraints.size();i++)
System.out.println(state.vConstraints.get(i));
-
maxsize=new ComputeMaxSize(state);
+ exactsize=new ExactSize(state);
abstractinterferes=new AbstractInterferes(this);
generateconjunctionnodes();
generateabstractedges();
generatescopeedges();
generateupdateedges();
+ constraintdependence=new ConstraintDependence(state,this);
HashSet superset=new HashSet();
superset.addAll(conjunctions);
HashSet closureset=new HashSet();
- // closureset.addAll(updatenodes);
- //superset.addAll(abstractrepair);
- //superset.addAll(updatenodes);
- //superset.addAll(scopenodes);
- //superset.addAll(consequencenodes);
+
GraphNode.computeclosure(superset,closureset);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
conjunctionmap.put(c,new HashSet());
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dnf.get(j),gn);
+
+
}
// Construct quantifier "conjunction" nodes
for(int j=0;j<c.numQuantifiers();j++) {
conjunctionmap.put(c,new HashSet());
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dconst.get(0),gn);
+
} else if (q instanceof RelationQuantifier) {
RelationQuantifier rq=(RelationQuantifier)q;
VarExpr ve=new VarExpr(rq.y);
conjunctionmap.put(c,new HashSet());
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dconst.get(0),gn);
+
}
}
}
goodupdate=true;
} else {
/* Create new element to bind to */
- Binding binding=new Binding(vd,set,createorsearch(set));
+ // search if the set 'set' has a size
+ Binding binding=new Binding(vd,set,exactsize.getsize(set)!=-1);
bindings.add(binding);
goodupdate=true;
- //FIXME
+
}
} else if (q instanceof RelationQuantifier) {
RelationQuantifier rq=(RelationQuantifier)q;
return goodupdate;
}
- /** Returns true if we search for an element from sd
- * false if we create an element for sd */
- private boolean createorsearch(SetDescriptor sd) {
- return false;
- }
-
static int addtocount=0;
void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule) state.vRules.get(i);
/* See if this is a good rule*/
if ((r.getInclusion() instanceof SetInclusion&&
- ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
+ ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
(r.getInclusion() instanceof RelationInclusion&&
ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
-
+
/* First solve for quantifiers */
Vector bindings=new Vector();
/* Construct bindings */
GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
addtocount++;
gn.addEdge(e);
- updatenodes.add(gn2);}
+ updatenodes.add(gn2);
+ }
}
}
}
} else if (q instanceof SetQuantifier) {
SetQuantifier sq=(SetQuantifier)q;
+ if (un.getBinding(sq.var).getType()==Binding.SEARCH)
+ continue; /* Don't need to ensure addition for search */
+
ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
eoe.td=ReservedTypeDescriptor.INT;
Updates u=new Updates(eoe,false);
TypeDescriptor td = null;
+ SetDescriptor sd=null;
+
+ public SetDescriptor getSet() {
+ return sd;
+ }
+
+ public void setSet(SetDescriptor sd) {
+ this.sd=sd;
+ }
+
public VarDescriptor(String name) {
super(name);
}
return hs;
}
+ public SetDescriptor getSet() {
+ return vd.getSet();
+ }
+
public VarExpr(String varname) {
- this.varname = varname;
+ this.varname = varname;
}
public VarExpr(VarDescriptor vd) {
}
public void generate(CodeWriter writer, VarDescriptor dest) {
-
// #TBD#: bit of a hack, really should have been type checked properly
-
- vd = (VarDescriptor) writer.getSymbolTable().get(varname);
+ vd = (VarDescriptor) writer.getSymbolTable().get(varname);
assert vd != null;
assert vd.getType() != null;
- this.td = vd.getType();
+ this.td = vd.getType();
writer.outputline(vd.getType().getGenerateType().getSafeSymbol() + " " + dest.getSafeSymbol() +
projects / repair.git / commitdiff