Track arguments in typestate

Add the infrastructure for arguments -- as well as local vars --
to be deinitialized with move-mode calls. Address Issue #819
This commit is contained in:
Tim Chevalier 2011-08-17 16:58:00 -07:00
parent 69d4838169
commit f023f82090
4 changed files with 46 additions and 9 deletions

View file

@ -109,6 +109,14 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &[ty_param], f_sp: &span,
next = add_constraint(cx.tcx, sc, next, res_map); next = add_constraint(cx.tcx, sc, next, res_map);
} }
/* Need to add constraints for args too, b/c they
can be deinitialized */
for a:arg in f.decl.inputs {
next = add_constraint(cx.tcx, respan(f_sp,
ninit(a.id, a.ident)),
next, res_map);
}
/* add the special i_diverge and i_return constraints /* add the special i_diverge and i_return constraints
(see the type definition for auxiliary::fn_info for an explanation) */ (see the type definition for auxiliary::fn_info for an explanation) */
@ -127,7 +135,8 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &[ty_param], f_sp: &span,
{constrs: res_map, {constrs: res_map,
num_constraints: num_constraints:
// add 2 to account for the i_return and i_diverge constraints // add 2 to account for the i_return and i_diverge constraints
vec::len(*cx.cs) + vec::len(f.decl.constraints) + 2u, vec::len(*cx.cs) + vec::len(f.decl.constraints)
+ vec::len(f.decl.inputs) + 2u,
cf: f.decl.cf, cf: f.decl.cf,
i_return: ninit(id, name), i_return: ninit(id, name),
i_diverge: ninit(diverges_id, diverges_name), i_diverge: ninit(diverges_id, diverges_name),

View file

@ -303,10 +303,11 @@ fn handle_update(fcx: &fn_ctxt, parent: &@expr, lhs: &@expr, rhs: &@expr,
} }
} }
/* FIXME: Can't deinitialize an upvar -- tests for that? */
fn handle_var(fcx: &fn_ctxt, rslt: &pre_and_post, id: node_id, name: ident) { fn handle_var(fcx: &fn_ctxt, rslt: &pre_and_post, id: node_id, name: ident) {
let df = node_id_to_def_upvar_strict(fcx, id); let df = node_id_to_def_upvar_strict(fcx, id);
alt df { alt df {
def_local(d_id) { def_local(d_id) | def_arg(d_id) {
let i = bit_num(fcx, ninit(d_id.node, name)); let i = bit_num(fcx, ninit(d_id.node, name));
use_var(fcx, d_id.node); use_var(fcx, d_id.node);
require_and_preserve(i, rslt); require_and_preserve(i, rslt);
@ -318,12 +319,12 @@ fn handle_var(fcx: &fn_ctxt, rslt: &pre_and_post, id: node_id, name: ident) {
fn forget_args_moved_in(fcx: &fn_ctxt, parent: &@expr, fn forget_args_moved_in(fcx: &fn_ctxt, parent: &@expr,
modes: &[ty::mode], modes: &[ty::mode],
operands: &[@expr]) { operands: &[@expr]) {
let i = 0; let i = 0u;
for mode: ty::mode in modes { for mode: ty::mode in modes {
if mode == ty::mo_move { if mode == ty::mo_move {
forget_in_postcond(fcx, parent.id, operands.(i).id); forget_in_postcond(fcx, parent.id, operands.(i).id);
} }
i += 1; i += 1u;
} }
} }
@ -672,10 +673,12 @@ fn find_pre_post_block(fcx: &fn_ctxt, b: blk) {
let nv = num_constraints(fcx.enclosing); let nv = num_constraints(fcx.enclosing);
fn do_one_(fcx: fn_ctxt, s: &@stmt) { fn do_one_(fcx: fn_ctxt, s: &@stmt) {
find_pre_post_stmt(fcx, *s); find_pre_post_stmt(fcx, *s);
log "pre_post for stmt:"; /*
log_stmt(*s); log_err "pre_post for stmt:";
log "is:"; log_stmt_err(*s);
log_pp(stmt_pp(fcx.ccx, *s)); log_err "is:";
log_pp_err(stmt_pp(fcx.ccx, *s));
*/
} }
for s: @stmt in b.node.stmts { do_one_(fcx, s); } for s: @stmt in b.node.stmts { do_one_(fcx, s); }
fn do_inner_(fcx: fn_ctxt, e: &@expr) { find_pre_post_expr(fcx, e); } fn do_inner_(fcx: fn_ctxt, e: &@expr) { find_pre_post_expr(fcx, e); }

View file

@ -165,6 +165,7 @@ fn find_pre_post_state_call(fcx: &fn_ctxt, pres: &prestate, a: &@expr,
id: node_id, ops: &[init_op], bs: &[@expr], id: node_id, ops: &[init_op], bs: &[@expr],
cf: controlflow) -> bool { cf: controlflow) -> bool {
let changed = find_pre_post_state_expr(fcx, pres, a); let changed = find_pre_post_state_expr(fcx, pres, a);
// FIXME: This could be a typestate constraint
if vec::len(bs) != vec::len(ops) { if vec::len(bs) != vec::len(ops) {
fcx.ccx.tcx.sess.span_bug(a.span, fcx.ccx.tcx.sess.span_bug(a.span,
#fmt("mismatched arg lengths: \ #fmt("mismatched arg lengths: \
@ -605,6 +606,7 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt) fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt)
-> bool { -> bool {
let stmt_ann = stmt_to_ann(fcx.ccx, *s); let stmt_ann = stmt_to_ann(fcx.ccx, *s);
/* /*
log_err ("[" + fcx.name + "]"); log_err ("[" + fcx.name + "]");
log_err "*At beginning: stmt = "; log_err "*At beginning: stmt = ";
@ -727,8 +729,13 @@ fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool {
// This ensures that intersect works correctly. // This ensures that intersect works correctly.
kill_all_prestate(fcx, f.body.node.id); kill_all_prestate(fcx, f.body.node.id);
// Instantiate any constraints on the arguments so we can use them // Arguments start out initialized
let block_pre = block_prestate(fcx.ccx, f.body); let block_pre = block_prestate(fcx.ccx, f.body);
for a:arg in f.decl.inputs {
set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre);
}
// Instantiate any constraints on the arguments so we can use them
let tsc; let tsc;
for c: @constr in f.decl.constraints { for c: @constr in f.decl.constraints {
tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c); tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c);

View file

@ -0,0 +1,18 @@
// error-pattern: Unsatisfied precondition constraint
fn send<~T>(ch : _chan<T>, data : -T) {
log ch;
log data;
fail;
}
type _chan<T> = int;
// Tests that "log message;" is flagged as using
// message after the send deinitializes it
fn test00_start(ch: _chan<int>, message: int, count: int) {
send(ch, message);
log message;
}
fn main() {
fail;
}