2012-01-14 18:05:07 -06:00
|
|
|
import option::*;
|
|
|
|
import pat_util::*;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::ast::*;
|
2011-08-21 23:44:41 -05:00
|
|
|
import syntax::ast_util::*;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::visit;
|
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;
|
2011-08-21 23:44:41 -05:00
|
|
|
import syntax::ast_util::respan;
|
2012-01-12 10:59:49 -06:00
|
|
|
import driver::session::session;
|
2012-01-14 18:05:07 -06:00
|
|
|
import aux::*;
|
2012-03-07 18:48:57 -06:00
|
|
|
import std::map::hashmap;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-08-04 18:20:09 -05:00
|
|
|
type ctxt = {cs: @mutable [sp_constr], tcx: ty::ctxt};
|
2011-05-26 18:02:25 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn collect_local(loc: @local, cx: ctxt, v: visit::vt<ctxt>) {
|
2012-02-22 09:57:23 -06:00
|
|
|
pat_bindings(cx.tcx.def_map, loc.node.pat) {|p_id, _s, id|
|
2012-01-30 23:00:57 -06:00
|
|
|
*cx.cs += [respan(loc.span, ninit(p_id, path_to_ident(id)))];
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-06-30 02:18:41 -05:00
|
|
|
visit::visit_local(loc, cx, v);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn collect_pred(e: @expr, cx: ctxt, v: visit::vt<ctxt>) {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt e.node {
|
2011-08-19 17:16:48 -05:00
|
|
|
expr_check(_, ch) { *cx.cs += [expr_to_constr(cx.tcx, ch)]; }
|
|
|
|
expr_if_check(ex, _, _) { *cx.cs += [expr_to_constr(cx.tcx, ex)]; }
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
// If it's a call, generate appropriate instances of the
|
|
|
|
// call's constraints.
|
2011-10-21 07:11:24 -05:00
|
|
|
expr_call(operator, operands, _) {
|
2011-08-15 23:54:52 -05:00
|
|
|
for c: @ty::constr in constraints_expr(cx.tcx, operator) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let ct: sp_constr =
|
|
|
|
respan(c.span,
|
|
|
|
aux::substitute_constr_args(cx.tcx, operands, c));
|
2011-08-19 17:16:48 -05:00
|
|
|
*cx.cs += [ct];
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { }
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
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-12-20 13:03:21 -06:00
|
|
|
fn find_locals(tcx: ty::ctxt,
|
2011-12-29 22:07:55 -06:00
|
|
|
fk: visit::fn_kind,
|
2011-12-20 13:03:21 -06:00
|
|
|
f_decl: fn_decl,
|
|
|
|
f_body: blk,
|
|
|
|
sp: span,
|
2011-09-12 04:27:30 -05:00
|
|
|
id: node_id) -> ctxt {
|
2011-08-19 17:16:48 -05:00
|
|
|
let cx: ctxt = {cs: @mutable [], tcx: tcx};
|
2011-08-13 02:09:25 -05:00
|
|
|
let visitor = visit::default_visitor::<ctxt>();
|
2012-03-15 08:47:03 -05:00
|
|
|
let visitor =
|
2011-07-27 07:19:39 -05:00
|
|
|
@{visit_local: collect_local,
|
|
|
|
visit_expr: collect_pred,
|
2011-12-29 22:07:55 -06:00
|
|
|
visit_fn: bind do_nothing(_, _, _, _, _, _, _)
|
2011-12-20 13:03:21 -06:00
|
|
|
with *visitor};
|
2011-12-29 22:07:55 -06:00
|
|
|
visit::visit_fn(fk, f_decl, f_body, sp,
|
|
|
|
id, cx, visit::mk_vt(visitor));
|
2011-06-01 20:10:10 -05:00
|
|
|
ret cx;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn add_constraint(tcx: ty::ctxt, c: sp_constr, next: uint, tbl: constr_map) ->
|
|
|
|
uint {
|
2011-12-22 19:53:53 -06:00
|
|
|
log(debug,
|
2011-12-22 16:42:52 -06:00
|
|
|
constraint_to_str(tcx, c) + " |-> " + uint::str(next));
|
2011-07-27 07:19:39 -05:00
|
|
|
alt c.node {
|
|
|
|
ninit(id, i) { tbl.insert(local_def(id), cinit(next, c.span, i)); }
|
|
|
|
npred(p, d_id, args) {
|
|
|
|
alt tbl.find(d_id) {
|
|
|
|
some(ct) {
|
|
|
|
alt ct {
|
|
|
|
cinit(_, _, _) {
|
2011-09-02 17:34:58 -05:00
|
|
|
tcx.sess.bug("add_constraint: same def_id used" +
|
|
|
|
" as a variable and a pred");
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
cpred(_, pds) {
|
2011-08-19 17:16:48 -05:00
|
|
|
*pds += [respan(c.span, {args: args, bit_num: next})];
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
none {
|
2011-08-04 18:20:09 -05:00
|
|
|
let rslt: @mutable [pred_args] =
|
2011-08-19 17:16:48 -05:00
|
|
|
@mutable [respan(c.span, {args: args, bit_num: next})];
|
2011-07-27 07:19:39 -05:00
|
|
|
tbl.insert(d_id, cpred(p, rslt));
|
|
|
|
}
|
2011-06-01 20:10:10 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
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-12-20 13:03:21 -06:00
|
|
|
fn mk_fn_info(ccx: crate_ctxt,
|
2011-12-29 22:07:55 -06:00
|
|
|
fk: visit::fn_kind,
|
2011-12-20 13:03:21 -06:00
|
|
|
f_decl: fn_decl,
|
|
|
|
f_body: blk,
|
|
|
|
f_sp: span,
|
|
|
|
id: node_id) {
|
2011-12-29 22:07:55 -06:00
|
|
|
let name = visit::name_of_fn(fk);
|
2012-01-09 09:24:53 -06:00
|
|
|
let res_map = new_def_hash::<constraint>();
|
2012-03-15 08:47:03 -05:00
|
|
|
let mut next: uint = 0u;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-12-29 22:07:55 -06:00
|
|
|
let cx: ctxt = find_locals(ccx.tcx, fk, f_decl, f_body, f_sp, id);
|
2011-06-01 20:10:10 -05:00
|
|
|
/* now we have to add bit nums for both the constraints
|
|
|
|
and the variables... */
|
|
|
|
|
2011-08-15 23:54:52 -05:00
|
|
|
for c: sp_constr 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 */
|
2012-03-15 08:47:03 -05:00
|
|
|
let mut sc;
|
2011-12-20 13:03:21 -06:00
|
|
|
for c: @constr in f_decl.constraints {
|
|
|
|
sc = ast_constr_to_sp_constr(cx.tcx, f_decl.inputs, c);
|
2011-07-21 18:03:30 -05:00
|
|
|
next = add_constraint(cx.tcx, sc, next, res_map);
|
|
|
|
}
|
|
|
|
|
2011-08-17 18:58:00 -05:00
|
|
|
/* Need to add constraints for args too, b/c they
|
|
|
|
can be deinitialized */
|
2011-12-20 13:03:21 -06:00
|
|
|
for a: arg in f_decl.inputs {
|
|
|
|
next = add_constraint(
|
|
|
|
cx.tcx,
|
|
|
|
respan(f_sp, ninit(a.id, a.ident)),
|
|
|
|
next,
|
|
|
|
res_map);
|
2011-08-17 18:58:00 -05:00
|
|
|
}
|
|
|
|
|
2011-08-01 22:55:04 -05:00
|
|
|
/* add the special i_diverge and i_return constraints
|
|
|
|
(see the type definition for auxiliary::fn_info for an explanation) */
|
|
|
|
|
2012-01-19 21:07:29 -06:00
|
|
|
// use the function name for the "returns" constraint"
|
|
|
|
let returns_id = ccx.tcx.sess.next_node_id();
|
|
|
|
let returns_constr = ninit(returns_id, name);
|
2011-08-19 17:16:48 -05:00
|
|
|
next =
|
2012-01-19 21:07:29 -06:00
|
|
|
add_constraint(cx.tcx, respan(f_sp, returns_constr), next, res_map);
|
2011-08-01 22:55:04 -05:00
|
|
|
// and the name of the function, with a '!' appended to it, for the
|
|
|
|
// "diverges" constraint
|
|
|
|
let diverges_id = ccx.tcx.sess.next_node_id();
|
2012-01-19 21:07:29 -06:00
|
|
|
let diverges_constr = ninit(diverges_id, name + "!");
|
|
|
|
next = add_constraint(cx.tcx, respan(f_sp, diverges_constr), next,
|
|
|
|
res_map);
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
let v: @mutable [node_id] = @mutable [];
|
2011-07-27 07:19:39 -05:00
|
|
|
let rslt =
|
|
|
|
{constrs: res_map,
|
2011-09-28 05:23:08 -05:00
|
|
|
num_constraints: next,
|
2011-12-20 13:03:21 -06:00
|
|
|
cf: f_decl.cf,
|
2012-01-19 21:07:29 -06:00
|
|
|
i_return: returns_constr,
|
|
|
|
i_diverge: diverges_constr,
|
2011-07-27 07:19:39 -05:00
|
|
|
used_vars: v};
|
2011-06-24 12:04:08 -05:00
|
|
|
ccx.fm.insert(id, rslt);
|
2011-12-22 18:13:40 -06:00
|
|
|
#debug("%s has %u constraints", name, num_constraints(rslt));
|
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-09-12 04:27:30 -05:00
|
|
|
fn mk_f_to_fn_info(ccx: crate_ctxt, c: @crate) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let visitor =
|
2011-12-23 11:45:02 -06:00
|
|
|
visit::mk_simple_visitor(@{visit_fn:
|
2011-12-29 22:07:55 -06:00
|
|
|
bind mk_fn_info(ccx, _, _, _, _, _)
|
2011-12-20 13:03:21 -06:00
|
|
|
with *visit::default_simple_visitor()});
|
2011-07-26 09:47:13 -05:00
|
|
|
visit::visit_crate(*c, (), visitor);
|
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
|
|
|
|
// End:
|
|
|
|
//
|