2011-07-21 18:03:30 -05:00
|
|
|
import std::uint;
|
|
|
|
import std::int;
|
2011-07-05 17:52:08 -05:00
|
|
|
import std::ivec;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::ast::*;
|
|
|
|
import util::ppaux::fn_ident_to_string;
|
2011-06-22 17:41:39 -05:00
|
|
|
import std::option::*;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::walk;
|
|
|
|
import syntax::visit;
|
|
|
|
import walk::walk_crate;
|
|
|
|
import walk::walk_fn;
|
|
|
|
import walk::ast_visitor;
|
2011-07-12 13:26:14 -05:00
|
|
|
import aux::*;
|
2011-07-06 09:46:17 -05:00
|
|
|
import std::map::new_int_hash;
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::new_def_hash;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::codemap::span;
|
|
|
|
import syntax::ast::respan;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-07-19 19:52:34 -05:00
|
|
|
type ctxt = rec(@mutable (sp_constr[]) cs, ty::ctxt tcx);
|
2011-05-26 18:02:25 -05:00
|
|
|
|
2011-06-30 02:18:41 -05:00
|
|
|
fn collect_local(&@local loc, &ctxt cx, &visit::vt[ctxt] v) {
|
2011-06-15 13:19:50 -05:00
|
|
|
log "collect_local: pushing " + loc.node.ident;
|
2011-07-19 19:52:34 -05:00
|
|
|
*cx.cs += ~[respan(loc.span, ninit(loc.node.id, loc.node.ident))];
|
2011-06-30 02:18:41 -05:00
|
|
|
visit::visit_local(loc, cx, v);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-30 02:18:41 -05:00
|
|
|
fn collect_pred(&@expr e, &ctxt cx, &visit::vt[ctxt] v) {
|
2011-06-01 20:10:10 -05:00
|
|
|
alt (e.node) {
|
2011-06-28 18:29:37 -05:00
|
|
|
case (expr_check(_, ?ch)) {
|
2011-07-05 17:52:08 -05:00
|
|
|
*cx.cs += ~[expr_to_constr(cx.tcx, ch)];
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_if_check(?ex, _, _)) {
|
2011-07-05 17:52:08 -05:00
|
|
|
*cx.cs += ~[expr_to_constr(cx.tcx, ex)];
|
2011-06-10 21:12:42 -05:00
|
|
|
}
|
2011-06-15 17:14:30 -05:00
|
|
|
// If it's a call, generate appropriate instances of the
|
|
|
|
// call's constraints.
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_call(?operator, ?operands)) {
|
2011-07-19 19:52:34 -05:00
|
|
|
for (@ty::constr c in constraints_expr(cx.tcx, operator)) {
|
|
|
|
let sp_constr ct = respan(c.span,
|
|
|
|
aux::substitute_constr_args(cx.tcx, operands,
|
|
|
|
c));
|
2011-07-05 17:52:08 -05:00
|
|
|
*cx.cs += ~[ct];
|
2011-06-10 21:12:42 -05:00
|
|
|
}
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
|
|
|
case (_) { }
|
|
|
|
}
|
2011-06-30 02:18:41 -05:00
|
|
|
// visit subexpressions
|
|
|
|
visit::visit_expr(e, cx, v);
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
2011-07-13 17:44:09 -05:00
|
|
|
|
2011-07-06 21:00:00 -05:00
|
|
|
fn find_locals(&ty::ctxt tcx, &_fn f, &ty_param[] tps, &span sp, &fn_ident i,
|
|
|
|
node_id id) -> ctxt {
|
2011-07-05 17:52:08 -05:00
|
|
|
let ctxt cx = rec(cs=@mutable ~[], tcx=tcx);
|
2011-06-30 02:18:41 -05:00
|
|
|
auto visitor = visit::default_visitor[ctxt]();
|
|
|
|
|
2011-07-01 07:05:54 -05:00
|
|
|
visitor = @rec(visit_local=collect_local,
|
|
|
|
visit_expr=collect_pred,
|
|
|
|
visit_fn=do_nothing
|
|
|
|
with *visitor);
|
|
|
|
visit::visit_fn(f, tps, sp, i, id, cx, visit::mk_vt(visitor));
|
2011-06-01 20:10:10 -05:00
|
|
|
ret cx;
|
|
|
|
}
|
|
|
|
|
2011-07-19 19:52:34 -05:00
|
|
|
fn add_constraint(&ty::ctxt tcx, sp_constr c, uint next, constr_map tbl) ->
|
2011-06-15 13:19:50 -05:00
|
|
|
uint {
|
2011-07-19 19:52:34 -05:00
|
|
|
log constraint_to_str(tcx, c) + " |-> " + std::uint::str(next);
|
|
|
|
alt (c.node) {
|
|
|
|
case (ninit(?id, ?i)) { tbl.insert(local_def(id),
|
|
|
|
cinit(next, c.span, i)); }
|
|
|
|
case (npred(?p, ?d_id, ?args)) {
|
|
|
|
alt (tbl.find(d_id)) {
|
2011-06-13 20:10:33 -05:00
|
|
|
case (some(?ct)) {
|
2011-06-01 20:10:10 -05:00
|
|
|
alt (ct) {
|
2011-06-15 13:19:50 -05:00
|
|
|
case (cinit(_, _, _)) {
|
|
|
|
tcx.sess.bug("add_constraint: same def_id used" +
|
|
|
|
" as a variable and a pred");
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
2011-06-13 20:10:33 -05:00
|
|
|
case (cpred(_, ?pds)) {
|
2011-07-05 01:29:15 -05:00
|
|
|
*pds += ~[respan(c.span,
|
2011-07-19 19:52:34 -05:00
|
|
|
rec(args=args, bit_num=next))];
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-13 20:10:33 -05:00
|
|
|
case (none) {
|
2011-07-19 19:52:34 -05:00
|
|
|
let @mutable(pred_args[]) rslt = @mutable(~[respan(c.span,
|
|
|
|
rec(args=args,
|
|
|
|
bit_num=next))]);
|
|
|
|
tbl.insert(d_id, cpred(p, rslt));
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret next + 1u;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* builds a table mapping each local var defined in f
|
|
|
|
to a bit number in the precondition/postcondition vectors */
|
2011-07-06 21:00:00 -05:00
|
|
|
fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp,
|
|
|
|
&span f_sp, &fn_ident f_name, node_id id) {
|
2011-07-21 18:03:30 -05:00
|
|
|
auto name = fn_ident_to_string(id, f_name);
|
2011-07-19 19:52:34 -05:00
|
|
|
auto res_map = @new_def_hash[constraint]();
|
2011-05-14 21:02:30 -05:00
|
|
|
let uint next = 0u;
|
|
|
|
|
2011-06-30 02:18:41 -05:00
|
|
|
let ctxt cx = find_locals(ccx.tcx, f, tp, f_sp, f_name, id);
|
2011-06-01 20:10:10 -05:00
|
|
|
/* now we have to add bit nums for both the constraints
|
|
|
|
and the variables... */
|
|
|
|
|
2011-07-19 19:52:34 -05:00
|
|
|
for (sp_constr c in { *cx.cs }) {
|
2011-06-01 20:10:10 -05:00
|
|
|
next = add_constraint(cx.tcx, c, next, res_map);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-21 18:03:30 -05:00
|
|
|
/* if this function has any constraints, instantiate them to the
|
|
|
|
argument names and add them */
|
|
|
|
auto sc;
|
|
|
|
for (@constr c in f.decl.constraints) {
|
|
|
|
sc = ast_constr_to_sp_constr(cx.tcx, f.decl.inputs, c);
|
|
|
|
next = add_constraint(cx.tcx, sc, next, res_map);
|
|
|
|
}
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* add a pseudo-entry for the function's return value
|
|
|
|
we can safely use the function's name itself for this purpose */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-19 19:52:34 -05:00
|
|
|
add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map);
|
2011-07-05 01:29:15 -05:00
|
|
|
let @mutable node_id[] v = @mutable ~[];
|
2011-06-24 12:04:08 -05:00
|
|
|
auto rslt =
|
2011-06-15 13:19:50 -05:00
|
|
|
rec(constrs=res_map,
|
2011-07-21 18:03:30 -05:00
|
|
|
num_constraints=ivec::len(*cx.cs) + ivec::len(f.decl.constraints)
|
|
|
|
+ 1u,
|
2011-06-30 02:18:41 -05:00
|
|
|
cf=f.decl.cf,
|
|
|
|
used_vars=v);
|
2011-06-24 12:04:08 -05:00
|
|
|
ccx.fm.insert(id, rslt);
|
2011-07-06 09:46:17 -05:00
|
|
|
log name + " has " + std::uint::str(num_constraints(rslt)) +
|
|
|
|
" constraints";
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* initializes the global fn_info_map (mapping each function ID, including
|
|
|
|
nested locally defined functions, onto a mapping from local variable name
|
|
|
|
to bit number) */
|
2011-06-15 13:19:50 -05:00
|
|
|
fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) {
|
|
|
|
let ast_visitor vars_visitor = walk::default_visitor();
|
|
|
|
vars_visitor =
|
2011-06-30 02:18:41 -05:00
|
|
|
rec(visit_fn_pre=bind mk_fn_info(ccx, _, _, _, _, _)
|
2011-06-15 13:19:50 -05:00
|
|
|
with vars_visitor);
|
|
|
|
walk_crate(vars_visitor, *c);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-16 19:49:46 -05:00
|
|
|
//
|
|
|
|
// Local Variables:
|
|
|
|
// mode: rust
|
|
|
|
// fill-column: 78;
|
|
|
|
// indent-tabs-mode: nil
|
|
|
|
// c-basic-offset: 4
|
|
|
|
// buffer-file-coding-system: utf-8-unix
|
|
|
|
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
|
|
|
|
// End:
|
|
|
|
//
|