diff --git a/src/comp/middle/tstate/annotate.rs b/src/comp/middle/tstate/annotate.rs index 8a705be2dcb..3ed1a56928a 100644 --- a/src/comp/middle/tstate/annotate.rs +++ b/src/comp/middle/tstate/annotate.rs @@ -51,15 +51,15 @@ fn collect_ids_local(&@local l, @mutable vec[node_id] rs) { vec::push(*rs, l.node.id); } -fn node_ids_in_fn(&_fn f, &span sp, &fn_ident i, node_id id, - @mutable vec[node_id] rs) { +fn node_ids_in_fn(&_fn f, &vec[ty_param] tps, &span sp, &fn_ident i, + node_id id, @mutable vec[node_id] rs) { auto collect_ids = walk::default_visitor(); collect_ids = rec(visit_expr_pre=bind collect_ids_expr(_, rs), visit_block_pre=bind collect_ids_block(_, rs), visit_stmt_pre=bind collect_ids_stmt(_, rs), visit_local_pre=bind collect_ids_local(_, rs) with collect_ids); - walk::walk_fn(collect_ids, f, sp, i, id); + walk::walk_fn(collect_ids, f, tps, sp, i, id); } fn init_vecs(&crate_ctxt ccx, &vec[node_id] node_ids, uint len) { @@ -69,24 +69,24 @@ fn init_vecs(&crate_ctxt ccx, &vec[node_id] node_ids, uint len) { } } -fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f, &span sp, - &fn_ident i, node_id id) { +fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f, &vec[ty_param] tps, + &span sp, &fn_ident i, node_id id) { let @mutable vec[node_id] node_ids = @mutable []; - node_ids_in_fn(f, sp, i, id, node_ids); + node_ids_in_fn(f, tps, sp, i, id, node_ids); auto node_id_vec = *node_ids; init_vecs(ccx, node_id_vec, num_constraints); } -fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &fn_ident i, - node_id id) { +fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &vec[ty_param] tps, + &span sp, &fn_ident i, node_id id) { auto f_info = get_fn_info(ccx, id); - visit_fn(ccx, num_constraints(f_info), f, sp, i, id); + visit_fn(ccx, num_constraints(f_info), f, tps, sp, i, id); } fn annotate_crate(&crate_ctxt ccx, &crate crate) { auto do_ann = walk::default_visitor(); do_ann = - rec(visit_fn_pre=bind annotate_in_fn(ccx, _, _, _, _) with do_ann); + rec(visit_fn_pre=bind annotate_in_fn(ccx, _, _, _, _, _) with do_ann); walk::walk_crate(do_ann, crate); } // diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index bfd2743f7a0..02a1798ad1b 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -217,7 +217,15 @@ type norm_constraint = rec(uint bit_num, constr c); type constr_map = @std::map::hashmap[node_id, constraint]; -type fn_info = rec(constr_map constrs, uint num_constraints, controlflow cf); +type fn_info = rec(constr_map constrs, + uint num_constraints, + controlflow cf, + /* list, accumulated during pre/postcondition + computation, of all local variables that may be + used*/ + // Doesn't seem to work without the @ -- + // bug? + @mutable vec[node_id] used_vars); /* mapping from node ID to typestate annotation */ @@ -770,6 +778,16 @@ fn args_mention(&vec[@constr_arg_use] args, &def_id v) -> bool { ret util::common::any[@constr_arg_use](bind mentions(v,_), args); } +fn use_var(&fn_ctxt fcx, &node_id v) { + vec::push(*fcx.enclosing.used_vars, v); +} + +fn vec_contains(&@mutable vec[node_id] v, &node_id i) -> bool { + for (node_id d in *v) { + if (d == i) { ret true; } + } + ret false; +} // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs index 0c13c617c47..ebf5d7bab3c 100644 --- a/src/comp/middle/tstate/ck.rs +++ b/src/comp/middle/tstate/ck.rs @@ -42,26 +42,31 @@ import std::option; import std::option::t; import std::option::some; import std::option::none; -import aux::fn_ctxt; -import aux::crate_ctxt; -import aux::new_crate_ctxt; -import aux::expr_precond; -import aux::expr_prestate; -import aux::expr_poststate; -import aux::stmt_poststate; -import aux::stmt_to_ann; -import aux::num_constraints; -import aux::tritv_to_str; -import aux::first_difference_string; +import aux::*; import pretty::pprust::ty_to_str; import util::common::log_stmt_err; -import aux::log_tritv_err; import bitvectors::promises; import annotate::annotate_crate; import collect_locals::mk_f_to_fn_info; import pre_post_conditions::fn_pre_post; import states::find_pre_post_state_fn; +fn check_unused_vars(&fn_ctxt fcx) { + // FIXME: could be more efficient + for (norm_constraint c in constraints(fcx)) { + alt (c.c.node.c) { + case (ninit(?v)) { + if (!vec_contains(fcx.enclosing.used_vars, + c.c.node.id)) { + fcx.ccx.tcx.sess.span_warn(c.c.span, + "Unused variable " + v); + } + } + case (_) { /* ignore pred constraints */ } + } + } +} + fn check_states_expr(&fn_ctxt fcx, &@expr e) { let precond prec = expr_precond(fcx.ccx, e); let prestate pres = expr_prestate(fcx.ccx, e); @@ -119,8 +124,8 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) { } } -fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, node_id id, - &span sp, &fn_ident i) { +fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &vec[ast::ty_param] tps, + node_id id, &span sp, &fn_ident i) { /* Postorder traversal instead of pre is important because we want the smallest possible erroneous statement or expression. */ @@ -142,9 +147,9 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, node_id id, keep_going=bind kg(keepgoing) with walk::default_visitor()); - walk::walk_fn(v, f, sp, i, id); + walk::walk_fn(v, f, tps, sp, i, id); - /* Finally, check that the return value is initialized */ + /* Check that the return value is initialized */ auto post = aux::block_poststate(fcx.ccx, f.body); let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name)); if (f.proto == ast::proto_fn && !promises(fcx, post, ret_c) && @@ -170,9 +175,13 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, node_id id, return to the caller"); } } + + /* Finally, check for unused variables */ + check_unused_vars(fcx); } -fn check_fn_states(&fn_ctxt fcx, &_fn f, node_id id, &span sp, &fn_ident i) { +fn check_fn_states(&fn_ctxt fcx, &_fn f, &vec[ast::ty_param] tps, + node_id id, &span sp, &fn_ident i) { /* Compute the pre- and post-states for this function */ // Fixpoint iteration @@ -181,17 +190,18 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, node_id id, &span sp, &fn_ident i) { /* Now compare each expr's pre-state to its precondition and post-state to its postcondition */ - check_states_against_conditions(fcx, f, id, sp, i); + check_states_against_conditions(fcx, f, tps, id, sp, i); } -fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &fn_ident i, node_id id) { +fn fn_states(&crate_ctxt ccx, &_fn f, &vec[ast::ty_param] tps, + &span sp, &fn_ident i, node_id id) { /* Look up the var-to-bit-num map for this function */ assert (ccx.fm.contains_key(id)); auto f_info = ccx.fm.get(id); auto name = option::from_maybe("anon", i); auto fcx = rec(enclosing=f_info, id=id, name=name, ccx=ccx); - check_fn_states(fcx, f, id, sp, i); + check_fn_states(fcx, f, tps, id, sp, i); } fn check_crate(ty::ctxt cx, @crate crate) { @@ -206,7 +216,7 @@ fn check_crate(ty::ctxt cx, @crate crate) { auto do_pre_post = walk::default_visitor(); do_pre_post = - rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _) + rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _, _) with do_pre_post); walk::walk_crate(do_pre_post, *crate); /* Check the pre- and postcondition against the pre- and poststate @@ -214,7 +224,8 @@ fn check_crate(ty::ctxt cx, @crate crate) { auto do_states = walk::default_visitor(); do_states = - rec(visit_fn_post=bind fn_states(ccx, _, _, _, _) with do_states); + rec(visit_fn_post=bind fn_states(ccx, _, _, _, _, _) + with do_states); walk::walk_crate(do_states, *crate); } // diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index 79375c4b40d..f2e271f1afa 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -28,13 +28,14 @@ import util::common::respan; type ctxt = rec(@mutable vec[aux::constr] cs, ty::ctxt tcx); -fn collect_local(&ctxt cx, &@local loc) { +fn collect_local(&@local loc, &ctxt cx, &visit::vt[ctxt] v) { log "collect_local: pushing " + loc.node.ident; vec::push(*cx.cs, respan(loc.span, rec(id=loc.node.id, c=ninit(loc.node.ident)))); + visit::visit_local(loc, cx, v); } -fn collect_pred(&ctxt cx, &@expr e) { +fn collect_pred(&@expr e, &ctxt cx, &visit::vt[ctxt] v) { alt (e.node) { case (expr_check(_, ?ch)) { vec::push(*cx.cs, expr_to_constr(cx.tcx, ch)); @@ -55,16 +56,25 @@ fn collect_pred(&ctxt cx, &@expr e) { } case (_) { } } + // visit subexpressions + visit::visit_expr(e, cx, v); } -fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &fn_ident i, node_id id) +fn do_nothing(&@item i, &ctxt ignore1, &visit::vt[ctxt] ignore) { +} + +fn find_locals(&ty::ctxt tcx, &_fn f, &vec[ast::ty_param] tps, + &span sp, &fn_ident i, node_id id) -> ctxt { let ctxt cx = rec(cs=@mutable vec::alloc(0u), tcx=tcx); - auto visitor = walk::default_visitor(); + auto visitor = visit::default_visitor[ctxt](); + visitor = - rec(visit_local_pre=bind collect_local(cx, _), - visit_expr_pre=bind collect_pred(cx, _) with visitor); - walk_fn(visitor, f, sp, i, id); + @rec(visit_local=collect_local, + visit_expr=collect_pred, + visit_item=do_nothing + with *visitor); + visit::visit_fn(f, tps, sp, i, id, cx, visit::vtor(visitor)); ret cx; } @@ -104,7 +114,8 @@ fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) -> /* builds a table mapping each local var defined in f to a bit number in the precondition/postcondition vectors */ -fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &fn_ident f_name, +fn mk_fn_info(&crate_ctxt ccx, &_fn f, &vec[ast::ty_param] tp, + &span f_sp, &fn_ident f_name, node_id id) { auto res_map = @new_int_hash[constraint](); let uint next = 0u; @@ -112,7 +123,7 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &fn_ident f_name, /* ignore args, which we know are initialized; just collect locally declared vars */ - let ctxt cx = find_locals(ccx.tcx, f, f_sp, f_name, id); + let ctxt cx = find_locals(ccx.tcx, f, tp, f_sp, f_name, id); /* now we have to add bit nums for both the constraints and the variables... */ @@ -125,10 +136,12 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &fn_ident f_name, auto name = fn_ident_to_string(id, f_name); add_constraint(cx.tcx, respan(f_sp, rec(id=id, c=ninit(name))), next, res_map); + let @mutable vec[node_id] v = @mutable []; auto rslt = rec(constrs=res_map, num_constraints=vec::len(*cx.cs) + 1u, - cf=f.decl.cf); + cf=f.decl.cf, + used_vars=v); ccx.fm.insert(id, rslt); log name + " has " + uistr(num_constraints(rslt)) + " constraints"; } @@ -140,7 +153,7 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &fn_ident f_name, fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) { let ast_visitor vars_visitor = walk::default_visitor(); vars_visitor = - rec(visit_fn_pre=bind mk_fn_info(ccx, _, _, _, _) + rec(visit_fn_pre=bind mk_fn_info(ccx, _, _, _, _, _) with vars_visitor); walk_crate(vars_visitor, *c); } diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 7ce3c357bbf..207fd7d3a90 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -55,6 +55,7 @@ import aux::substitute_constr_args; import aux::ninit; import aux::npred; import aux::path_to_ident; +import aux::use_var; import bitvectors::bit_num; import bitvectors::promises; import bitvectors::seq_preconds; @@ -74,10 +75,12 @@ import util::common::elt_exprs; import util::common::field_exprs; import util::common::has_nonlocal_exits; import util::common::log_stmt; +import util::common::log_stmt_err; import util::common::log_expr_err; import util::common::log_block_err; import util::common::log_block; import util::common::span; +import util::common::istr; import pretty::ppaux::fn_ident_to_string; fn find_pre_post_mod(&_mod m) -> _mod { @@ -109,11 +112,12 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) { alt (i.node) { case (item_const(_, ?e)) { // make a fake fcx - + let @mutable vec[node_id] v = @mutable []; auto fake_fcx = rec(enclosing=rec(constrs=@new_int_hash[constraint](), num_constraints=0u, - cf=return), + cf=return, + used_vars=v), id=0, name="", ccx=ccx); @@ -323,6 +327,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { bit_num(fcx, rec(id=d_id._1, c=ninit(path_to_ident(fcx.ccx.tcx, p)))); + use_var(fcx, d_id._1); require_and_preserve(i, rslt); } case (_) {/* nothing to check */ } @@ -686,6 +691,9 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) { } fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) { + // hack + use_var(fcx, fcx.id); + find_pre_post_block(fcx, f.body); // Treat the tail expression as a return statement @@ -697,8 +705,8 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) { } } -fn fn_pre_post(crate_ctxt ccx, &_fn f, &span sp, &fn_ident i, - node_id id) { +fn fn_pre_post(crate_ctxt ccx, &_fn f, &vec[ty_param] tps, + &span sp, &fn_ident i, node_id id) { assert (ccx.fm.contains_key(id)); auto fcx = rec(enclosing=ccx.fm.get(id), id=id, name=fn_ident_to_string(id, i), ccx=ccx); diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 7c3116a4092..06c5a2e80ec 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1025,12 +1025,12 @@ mod writeback { fn visit_item_post(@mutable bool ignore, &@ast::item item) { *ignore = false; } - fn visit_fn_pre(@mutable bool ignore, &ast::_fn f, &span sp, - &ast::fn_ident i, ast::node_id d) { + fn visit_fn_pre(@mutable bool ignore, &ast::_fn f, &vec[ast::ty_param] tps, + &span sp, &ast::fn_ident i, ast::node_id d) { *ignore = true; } - fn visit_fn_post(@mutable bool ignore, &ast::_fn f, &span sp, - &ast::fn_ident i, ast::node_id d) { + fn visit_fn_post(@mutable bool ignore, &ast::_fn f, &vec[ast::ty_param] tps, + &span sp, &ast::fn_ident i, ast::node_id d) { *ignore = false; } fn keep_going(@mutable bool ignore) -> bool { ret !*ignore; } @@ -1038,8 +1038,8 @@ mod writeback { rec(keep_going=bind keep_going(ignore), visit_item_pre=bind visit_item_pre(ignore, _), visit_item_post=bind visit_item_post(ignore, _), - visit_fn_pre=bind visit_fn_pre(ignore, _, _, _, _), - visit_fn_post=bind visit_fn_post(ignore, _, _, _, _), + visit_fn_pre=bind visit_fn_pre(ignore, _, _, _, _, _), + visit_fn_post=bind visit_fn_post(ignore, _, _, _, _, _), visit_stmt_pre=bind visit_stmt_pre(fcx, _), visit_expr_pre=bind visit_expr_pre(fcx, _), visit_block_pre=bind visit_block_pre(fcx, _), diff --git a/src/comp/middle/walk.rs b/src/comp/middle/walk.rs index 91c5008480e..707eae8d30f 100644 --- a/src/comp/middle/walk.rs +++ b/src/comp/middle/walk.rs @@ -1,5 +1,6 @@ import front::ast; +import middle::ty::ty_param; import std::option; import std::option::some; import std::option::none; @@ -38,8 +39,8 @@ type ast_visitor = fn(&@ast::ty) visit_ty_pre, fn(&@ast::ty) visit_ty_post, fn(&@ast::constr) visit_constr, - fn(&ast::_fn, &span, &ast::fn_ident, ast::node_id) visit_fn_pre, - fn(&ast::_fn, &span, &ast::fn_ident, ast::node_id) visit_fn_post); + fn(&ast::_fn, &vec[ast::ty_param], &span, &ast::fn_ident, ast::node_id) visit_fn_pre, + fn(&ast::_fn, &vec[ast::ty_param], &span, &ast::fn_ident, ast::node_id) visit_fn_post); fn walk_crate(&ast_visitor v, &ast::crate c) { if (!v.keep_going()) { ret; } @@ -99,14 +100,14 @@ fn walk_item(&ast_visitor v, @ast::item i) { v.visit_item_pre(i); alt (i.node) { case (ast::item_const(?t, ?e)) { walk_ty(v, t); walk_expr(v, e); } - case (ast::item_fn(?f, _)) { - walk_fn(v, f, i.span, some(i.ident), i.id); + case (ast::item_fn(?f, ?tps)) { + walk_fn(v, f, tps, i.span, some(i.ident), i.id); } case (ast::item_mod(?m)) { walk_mod(v, m); } case (ast::item_native_mod(?nm)) { walk_native_mod(v, nm); } case (ast::item_ty(?t, _)) { walk_ty(v, t); } - case (ast::item_res(?f, ?dtor_id, _, _)) { - walk_fn(v, f, i.span, some(i.ident), dtor_id); + case (ast::item_res(?f, ?dtor_id, ?tps, _)) { + walk_fn(v, f, tps, i.span, some(i.ident), dtor_id); } case (ast::item_tag(?variants, _)) { for (ast::variant vr in variants) { @@ -119,14 +120,15 @@ fn walk_item(&ast_visitor v, @ast::item i) { for (ast::obj_field f in ob.fields) { walk_ty(v, f.ty); } for (@ast::method m in ob.methods) { v.visit_method_pre(m); - walk_fn(v, m.node.meth, m.span, + // Methods don't have ty params? + walk_fn(v, m.node.meth, [], m.span, some(m.node.ident), m.node.id); v.visit_method_post(m); } alt (ob.dtor) { case (none) { } case (some(?m)) { - walk_fn(v, m.node.meth, m.span, + walk_fn(v, m.node.meth, [], m.span, some(m.node.ident), m.node.id); } } @@ -220,13 +222,13 @@ fn walk_fn_decl(&ast_visitor v, &ast::fn_decl fd) { walk_ty(v, fd.output); } -fn walk_fn(&ast_visitor v, &ast::_fn f, &span sp, &ast::fn_ident i, - ast::node_id d) { +fn walk_fn(&ast_visitor v, &ast::_fn f, &vec[ast::ty_param] tps, + &span sp, &ast::fn_ident i, ast::node_id d) { if (!v.keep_going()) { ret; } - v.visit_fn_pre(f, sp, i, d); + v.visit_fn_pre(f, tps, sp, i, d); walk_fn_decl(v, f.decl); walk_block(v, f.body); - v.visit_fn_post(f, sp, i, d); + v.visit_fn_post(f, tps, sp, i, d); } fn walk_block(&ast_visitor v, &ast::block b) { @@ -343,7 +345,7 @@ fn walk_expr(&ast_visitor v, @ast::expr e) { } } case (ast::expr_fn(?f)) { - walk_fn(v, f, e.span, none, e.id); + walk_fn(v, f, [], e.span, none, e.id); } case (ast::expr_block(?b)) { walk_block(v, b); } case (ast::expr_assign(?a, ?b)) { @@ -407,7 +409,7 @@ fn walk_expr(&ast_visitor v, @ast::expr e) { // Methods for (@ast::method m in anon_obj.methods) { v.visit_method_pre(m); - walk_fn(v, m.node.meth, m.span, some(m.node.ident), + walk_fn(v, m.node.meth, [], m.span, some(m.node.ident), m.node.id); v.visit_method_post(m); } @@ -450,7 +452,8 @@ fn def_visit_ty(&@ast::ty t) { } fn def_visit_constr(&@ast::constr c) { } -fn def_visit_fn(&ast::_fn f, &span sp, &ast::fn_ident i, ast::node_id d) { } +fn def_visit_fn(&ast::_fn f, &vec[ast::ty_param] tps, + &span sp, &ast::fn_ident i, ast::node_id d) { } fn default_visitor() -> ast_visitor { ret rec(keep_going=def_keep_going,