diff --git a/src/rustc/middle/tstate/auxiliary.rs b/src/rustc/middle/tstate/auxiliary.rs index 343fd07a1d5..ecd6b43a7f0 100644 --- a/src/rustc/middle/tstate/auxiliary.rs +++ b/src/rustc/middle/tstate/auxiliary.rs @@ -49,18 +49,10 @@ fn comma_str(args: [@constr_arg_use]) -> str { } fn constraint_to_str(tcx: ty::ctxt, c: sp_constr) -> str { - alt c.node { - ninit(id, i) { - ret #fmt("init(%s id=%d - arising from %s)", - i, id, codemap::span_to_str(c.span, tcx.sess.codemap)); - } - npred(p, _, args) { - ret #fmt("%s(%s) - arising from %s", - path_to_str(p), - comma_str(args), - codemap::span_to_str(c.span, tcx.sess.codemap)); - } - } + ret #fmt("%s(%s) - arising from %s", + path_to_str(c.node.path), + comma_str(c.node.args), + codemap::span_to_str(c.span, tcx.sess.codemap)); } fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> str { @@ -167,16 +159,14 @@ fn print_idents(&idents: [ident]) { /* Two different data structures represent constraints in different contexts: constraint and norm_constraint. -constraint gets used to record constraints in a table keyed by def_ids. -cinit constraints represent a single constraint, for the initialization -state of a variable; a cpred constraint, with a single operator and a -list of possible argument lists, could represent several constraints at -once. +constraint gets used to record constraints in a table keyed by def_ids. Each +constraint has a single operator but a list of possible argument lists, and +thus represents several constraints at once, one for each possible argument +list. -norm_constraint, in contrast, gets used when handling an instance -of a constraint rather than a definition of a constraint. It can -also be init or pred (ninit or npred), but the npred case just has -a single argument list. +norm_constraint, in contrast, gets used when handling an instance of a +constraint rather than a definition of a constraint. It has only a single +argument list. The representation of constraints, where multiple instances of the same predicate are collapsed into one entry in the table, makes it @@ -198,37 +188,23 @@ type pred_args = spanned; // for this local. type constr_arg_use = spanned>; -/* - A constraint is either an init constraint, referring to the initialization - state of a variable (not initialized, definitely initialized, or maybe - initialized) or a predicate constraint, referring to the truth value of a - predicate on variables (definitely false, maybe true, or definitely true). - - cinit and ninit represent init constraints, while cpred and npred - represent predicate constraints. - - In a predicate constraint, the field (and the field - in the npred constructor) names a user-defined function that may - be the operator in a "check" expression in the source. - */ - -enum constraint { - cinit(uint, span, ident), +/* Predicate constraints refer to the truth value of a predicate on variables +(definitely false, maybe true, or definitely true). The field (and the + field in the npred constructor) names a user-defined function that +may be the operator in a "check" expression in the source. */ +type constraint = { + path: @path, // FIXME: really only want it to be mut during collect_locals. // freeze it after that. - cpred(@path, @mut [pred_args]), -} + descs: @mut [pred_args] +}; -// An ninit variant has a node_id because it refers to a local var. -// An npred has a def_id since the definition of the typestate -// predicate need not be local. -// FIXME: would be nice to give both a def_id field, -// and give ninit a constraint saying it's local. -enum tsconstr { - ninit(node_id, ident), - npred(@path, def_id, [@constr_arg_use]), -} +type tsconstr = { + path: @path, + def_id: def_id, + args: [@constr_arg_use] +}; type sp_constr = spanned; @@ -238,34 +214,8 @@ type constr_map = std::map::hashmap; /* Contains stuff that has to be computed up front */ /* For easy access, the fn_info stores two special constraints for each -function. i_return holds if all control paths in this function terminate -in either a return expression, or an appropriate tail expression. -i_diverge holds if all control paths in this function terminate in a fail -or diverging call. - -It might be tempting to use a single constraint C for both properties, -where C represents i_return and !C represents i_diverge. This is -inadvisable, because then the sense of the bit depends on context. If we're -inside a ! function, that reverses the sense of the bit: C would be -i_diverge and !C would be i_return. That's awkward, because we have to -pass extra context around to functions that shouldn't care. - -Okay, suppose C represents i_return and !C represents i_diverge, regardless -of context. Consider this code: - -if (foo) { ret; } else { fail; } - -C is true in the consequent and false in the alternative. What's T `join` -F, then? ? doesn't work, because this code should definitely-return if the -context is a returning function (and be definitely-rejected if the context -is a ! function). F doesn't work, because then the code gets incorrectly -rejected if the context is a returning function. T would work, but it -doesn't make sense for T `join` F to be T (consider init constraints, for -example).; - -So we need context. And so it seems clearer to just have separate -constraints. -*/ +function. So we need context. And so it seems clearer to just have separate +constraints. */ type fn_info = /* list, accumulated during pre/postcondition computation, of all local variables that may be @@ -274,21 +224,8 @@ type fn_info = {constrs: constr_map, num_constraints: uint, cf: ret_style, - i_return: tsconstr, - i_diverge: tsconstr, used_vars: @mut [node_id]}; -fn tsconstr_to_def_id(t: tsconstr) -> def_id { - alt t { ninit(id, _) { local_def(id) } npred(_, id, _) { id } } -} - -fn tsconstr_to_node_id(t: tsconstr) -> node_id { - alt t { - ninit(id, _) { id } - npred(_, id, _) { fail "tsconstr_to_node_id called on pred constraint" } - } -} - /* mapping from node ID to typestate annotation */ type node_ann_table = @mut [mut ts_ann]; @@ -534,20 +471,15 @@ fn node_id_to_def(ccx: crate_ctxt, id: node_id) -> option { } fn norm_a_constraint(id: def_id, c: constraint) -> [norm_constraint] { - alt c { - cinit(n, sp, i) { - ret [{bit_num: n, c: respan(sp, ninit(id.node, i))}]; - } - cpred(p, descs) { - let mut rslt: [norm_constraint] = []; - for vec::each(*descs) {|pd| - rslt += - [{bit_num: pd.node.bit_num, - c: respan(pd.span, npred(p, id, pd.node.args))}]; - } - ret rslt; - } + let mut rslt: [norm_constraint] = []; + for vec::each(*c.descs) {|pd| + rslt += + [{bit_num: pd.node.bit_num, + c: respan(pd.span, {path: c.path, + def_id: id, + args: pd.node.args})}]; } + ret rslt; } @@ -630,8 +562,9 @@ fn expr_to_constr(tcx: ty::ctxt, e: @expr) -> sp_constr { alt operator.node { expr_path(p) { ret respan(e.span, - npred(p, def_id_for_constr(tcx, operator.id), - exprs_to_constr_args(tcx, args))); + {path: p, + def_id: def_id_for_constr(tcx, operator.id), + args: exprs_to_constr_args(tcx, args)}); } _ { tcx.sess.span_bug(operator.span, @@ -657,7 +590,9 @@ fn substitute_constr_args(cx: ty::ctxt, actuals: [@expr], c: @ty::constr) -> for c.node.args.each {|a| rslt += [substitute_arg(cx, actuals, a)]; } - ret npred(c.node.path, c.node.id, rslt); + ret {path: c.node.path, + def_id: c.node.id, + args: rslt}; } fn substitute_arg(cx: ty::ctxt, actuals: [@expr], a: @constr_arg) -> @@ -718,31 +653,22 @@ enum dest { type subst = [{from: inst, to: inst}]; -fn find_instances(_fcx: fn_ctxt, subst: subst, c: constraint) -> - [{from: uint, to: uint}] { +fn find_instances(_fcx: fn_ctxt, subst: subst, + c: constraint) -> [{from: uint, to: uint}] { - let mut rslt = []; - if vec::len(subst) == 0u { ret rslt; } - - alt c { - cinit(_, _, _) {/* this is dealt with separately */ } - cpred(p, descs) { - // FIXME (#2280): this temporary shouldn't be - // necessary, but seems to be, for borrowing. - let ds = copy *descs; - for vec::each(ds) {|d| - if args_mention(d.node.args, find_in_subst_bool, subst) { - let old_bit_num = d.node.bit_num; - let newv = replace(subst, d); - alt find_instance_(newv, *descs) { - some(d1) { rslt += [{from: old_bit_num, to: d1}]; } - _ { } - } + if vec::len(subst) == 0u { ret []; } + let mut res = []; + for (*c.descs).each { |d| + if args_mention(d.node.args, find_in_subst_bool, subst) { + let old_bit_num = d.node.bit_num; + let newv = replace(subst, d); + alt find_instance_(newv, *c.descs) { + some(d1) {res += [{from: old_bit_num, to: d1}]} + _ {} } - } - } + } else {} } - rslt + ret res; } fn find_in_subst(id: node_id, s: subst) -> option { @@ -912,25 +838,6 @@ fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) { } } -fn forget_in_postcond_still_init(fcx: fn_ctxt, parent_exp: node_id, - dead_v: node_id) { - // In the postcondition given by parent_exp, clear the bits - // for any constraints mentioning dead_v - let d = local_node_id_to_local_def_id(fcx, dead_v); - alt d { - some(d_id) { - for constraints(fcx).each {|c| - if non_init_constraint_mentions(fcx, c, d_id) { - clear_in_postcond(c.bit_num, - node_id_to_ts_ann(fcx.ccx, - parent_exp).conditions); - } - } - } - _ { } - } -} - fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool { // In the poststate given by parent_exp, clear the bits // for any constraints mentioning dead_v @@ -949,25 +856,6 @@ fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool { ret changed; } -fn forget_in_poststate_still_init(fcx: fn_ctxt, p: poststate, dead_v: node_id) - -> bool { - // In the poststate given by parent_exp, clear the bits - // for any constraints mentioning dead_v - let d = local_node_id_to_local_def_id(fcx, dead_v); - let mut changed = false; - alt d { - some(d_id) { - for constraints(fcx).each {|c| - if non_init_constraint_mentions(fcx, c, d_id) { - changed |= clear_in_poststate_(c.bit_num, p); - } - } - } - _ { } - } - ret changed; -} - fn any_eq(v: [node_id], d: node_id) -> bool { for v.each {|i| if i == d { ret true; } } false @@ -975,18 +863,7 @@ fn any_eq(v: [node_id], d: node_id) -> bool { fn constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id) -> bool { - ret alt c.c.node { - ninit(id, _) { v == id } - npred(_, _, args) { args_mention(args, any_eq, [v]) } - }; -} - -fn non_init_constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id) - -> bool { - ret alt c.c.node { - ninit(_, _) { false } - npred(_, _, args) { args_mention(args, any_eq, [v]) } - }; + ret args_mention(c.c.node.args, any_eq, [v]); } fn args_mention(args: [@constr_arg_use], @@ -1063,8 +940,9 @@ fn args_to_constr_args(tcx: ty::ctxt, args: [arg], fn ast_constr_to_ts_constr(tcx: ty::ctxt, args: [arg], c: @constr) -> tsconstr { let tconstr = ty::ast_constr_to_constr(tcx, c); - ret npred(tconstr.node.path, tconstr.node.id, - args_to_constr_args(tcx, args, tconstr.node.args)); + ret {path: tconstr.node.path, + def_id: tconstr.node.id, + args: args_to_constr_args(tcx, args, tconstr.node.args)}; } fn ast_constr_to_sp_constr(tcx: ty::ctxt, args: [arg], c: @constr) -> diff --git a/src/rustc/middle/tstate/bitvectors.rs b/src/rustc/middle/tstate/bitvectors.rs index 1020f1a001a..e2ce69cc91e 100644 --- a/src/rustc/middle/tstate/bitvectors.rs +++ b/src/rustc/middle/tstate/bitvectors.rs @@ -15,36 +15,19 @@ import driver::session::session; import std::map::hashmap; fn bit_num(fcx: fn_ctxt, c: tsconstr) -> uint { - let d = tsconstr_to_def_id(c); + let d = c.def_id; assert (fcx.enclosing.constrs.contains_key(d)); let rslt = fcx.enclosing.constrs.get(d); - alt c { - ninit(_, _) { - alt rslt { - cinit(n, _, _) { ret n; } - _ { - fcx.ccx.tcx.sess.bug("bit_num: asked for init constraint," + - " found a pred constraint"); - } - } - } - npred(_, _, args) { - alt rslt { - cpred(_, descs) { ret match_args(fcx, descs, args); } - _ { - fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint," + - " found an init constraint"); - } - } - } - } + match_args(fcx, rslt.descs, c.args) } fn promises(fcx: fn_ctxt, p: poststate, c: tsconstr) -> bool { ret promises_(bit_num(fcx, c), p); } -fn promises_(n: uint, p: poststate) -> bool { ret tritv_get(p, n) == ttrue; } +fn promises_(n: uint, p: poststate) -> bool { + ret tritv_get(p, n) == ttrue; +} // v "happens after" u fn seq_trit(u: trit, v: trit) -> trit { @@ -184,51 +167,15 @@ fn kill_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool { node_id_to_ts_ann(fcx.ccx, id).states); } -fn clear_in_poststate_expr(fcx: fn_ctxt, e: @expr, t: poststate) { - alt e.node { - expr_path(p) { - alt local_node_id_to_def(fcx, e.id) { - some(def_local(nid, _)) { - clear_in_poststate_(bit_num(fcx, ninit(nid, vec::last(p.idents))), - t); - } - some(_) {/* ignore args (for now...) */ } - _ { fcx.ccx.tcx.sess.bug("clear_in_poststate_expr: unbound var"); } - } - } - _ {/* do nothing */ } - } -} - fn kill_poststate_(fcx: fn_ctxt, c: tsconstr, post: poststate) -> bool { #debug("kill_poststate_"); ret clear_in_poststate_(bit_num(fcx, c), post); } -fn set_in_poststate_ident(fcx: fn_ctxt, id: node_id, ident: ident, - t: poststate) -> bool { - ret set_in_poststate_(bit_num(fcx, ninit(id, ident)), t); -} - fn set_in_prestate_constr(fcx: fn_ctxt, c: tsconstr, t: prestate) -> bool { ret set_in_poststate_(bit_num(fcx, c), t); } -fn clear_in_poststate_ident(fcx: fn_ctxt, id: node_id, ident: ident, - parent: node_id) -> bool { - ret kill_poststate(fcx, parent, ninit(id, ident)); -} - -fn clear_in_prestate_ident(fcx: fn_ctxt, id: node_id, ident: ident, - parent: node_id) -> bool { - ret kill_prestate(fcx, parent, ninit(id, ident)); -} - -fn clear_in_poststate_ident_(fcx: fn_ctxt, id: node_id, ident: ident, - post: poststate) -> bool { - ret kill_poststate_(fcx, ninit(id, ident), post); -} - // // Local Variables: // mode: rust diff --git a/src/rustc/middle/tstate/ck.rs b/src/rustc/middle/tstate/ck.rs index a8c06cd322a..1cc3a7df9dc 100644 --- a/src/rustc/middle/tstate/ck.rs +++ b/src/rustc/middle/tstate/ck.rs @@ -17,22 +17,6 @@ import states::find_pre_post_state_fn; import driver::session::session; import std::map::hashmap; -fn check_unused_vars(fcx: fn_ctxt) { - - // FIXME: could be more efficient - for constraints(fcx).each {|c| - alt c.c.node { - ninit(id, v) { - if !vec_contains(fcx.enclosing.used_vars, id) && v[0] != '_' as u8 - { - fcx.ccx.tcx.sess.span_warn(c.c.span, "unused variable " + v); - } - } - _ {/* ignore pred constraints */ } - } - } -} - fn check_states_expr(e: @expr, fcx: fn_ctxt, v: visit::vt) { visit::visit_expr(e, fcx, v); @@ -109,39 +93,6 @@ fn check_states_against_conditions(fcx: fn_ctxt, visit_fn: bind do_nothing::(_, _, _, _, _, _, _) with *visit::default_visitor::()}); visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor); - - /* Check that the return value is initialized */ - let post = aux::block_poststate(fcx.ccx, f_body); - let is_ctor = alt fk { visit::fk_ctor(_,_,_,_) { true } _ { false } }; - if !is_ctor && !promises(fcx, post, fcx.enclosing.i_return) && - !ty::type_is_nil(ty::ty_fn_ret(ty::node_id_to_type( - fcx.ccx.tcx, id))) && - f_decl.cf == return_val { - let fn_ty = ty::node_id_to_type(fcx.ccx.tcx, id); - fcx.ccx.tcx.sess.span_err(f_body.span, - #fmt("in function `%s`, not all control paths \ - return a value", fcx.name)); - fcx.ccx.tcx.sess.span_fatal(f_decl.output.span, - #fmt("see function return type of `%s`", - ty_to_str(fcx.ccx.tcx, - ty::ty_fn_ret(fn_ty)))); - } else if f_decl.cf == noreturn { - - // check that this really always fails - // Note that it's ok for i_diverge and i_return to both be true. - // In fact, i_diverge implies i_return. (But not vice versa!) - - if !promises(fcx, post, fcx.enclosing.i_diverge) { - fcx.ccx.tcx.sess.span_fatal(f_body.span, - "in non-returning function " + - fcx.name + - ", some control paths may \ - return to the caller"); - } - } - - /* Finally, check for unused variables */ - check_unused_vars(fcx); } fn check_fn_states(fcx: fn_ctxt, diff --git a/src/rustc/middle/tstate/collect_locals.rs b/src/rustc/middle/tstate/collect_locals.rs index 88a353f4cd8..bfa2fa58f77 100644 --- a/src/rustc/middle/tstate/collect_locals.rs +++ b/src/rustc/middle/tstate/collect_locals.rs @@ -11,13 +11,6 @@ import std::map::hashmap; type ctxt = {cs: @mut [sp_constr], tcx: ty::ctxt}; -fn collect_local(loc: @local, cx: ctxt, v: visit::vt) { - pat_bindings(cx.tcx.def_map, loc.node.pat) {|p_id, _s, id| - *cx.cs += [respan(loc.span, ninit(p_id, path_to_ident(id)))]; - }; - visit::visit_local(loc, cx, v); -} - fn collect_pred(e: @expr, cx: ctxt, v: visit::vt) { alt e.node { expr_check(_, ch) { *cx.cs += [expr_to_constr(cx.tcx, ch)]; } @@ -48,8 +41,7 @@ fn find_locals(tcx: ty::ctxt, let cx: ctxt = {cs: @mut [], tcx: tcx}; let visitor = visit::default_visitor::(); let visitor = - @{visit_local: collect_local, - visit_expr: collect_pred, + @{visit_expr: collect_pred, visit_fn: bind do_nothing(_, _, _, _, _, _, _) with *visitor}; visit::visit_fn(fk, f_decl, f_body, sp, @@ -61,27 +53,17 @@ fn add_constraint(tcx: ty::ctxt, c: sp_constr, next: uint, tbl: constr_map) -> uint { log(debug, constraint_to_str(tcx, c) + " |-> " + uint::str(next)); - 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(_, _, _) { - tcx.sess.bug("add_constraint: same def_id used" + - " as a variable and a pred"); - } - cpred(_, pds) { - *pds += [respan(c.span, {args: args, bit_num: next})]; - } - } - } - none { - let rslt: @mut [pred_args] = - @mut [respan(c.span, {args: args, bit_num: next})]; - tbl.insert(d_id, cpred(p, rslt)); - } - } + + let {path: p, def_id: d_id, args: args} = c.node; + alt tbl.find(d_id) { + some(ct) { + let {path: _, descs: pds} = ct; + *pds += [respan(c.span, {args: args, bit_num: next})]; + } + none { + let rslt: @mut [pred_args] = + @mut [respan(c.span, {args: args, bit_num: next})]; + tbl.insert(d_id, {path:p, descs:rslt}); } } ret next + 1u; @@ -106,7 +88,7 @@ fn mk_fn_info(ccx: crate_ctxt, let mut i = 0u, l = vec::len(*cx.cs); while i < l { - next = add_constraint(cx.tcx, cx.cs[i], next, res_map); + next = add_constraint(cx.tcx, copy cx.cs[i], next, res_map); i += 1u; } /* if this function has any constraints, instantiate them to the @@ -116,38 +98,11 @@ fn mk_fn_info(ccx: crate_ctxt, next = add_constraint(cx.tcx, sc, next, res_map); } - /* Need to add constraints for args too, b/c they - can be deinitialized */ - for f_decl.inputs.each {|a| - 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 - (see the type definition for auxiliary::fn_info for an explanation) */ - - // use the function name for the "returns" constraint" - let returns_id = ccx.tcx.sess.next_node_id(); - let returns_constr = ninit(returns_id, name); - next = - add_constraint(cx.tcx, respan(f_sp, returns_constr), next, res_map); - // and the name of the function, with a '!' appended to it, for the - // "diverges" constraint - let diverges_id = ccx.tcx.sess.next_node_id(); - let diverges_constr = ninit(diverges_id, name + "!"); - next = add_constraint(cx.tcx, respan(f_sp, diverges_constr), next, - res_map); - let v: @mut [node_id] = @mut []; let rslt = {constrs: res_map, num_constraints: next, cf: f_decl.cf, - i_return: returns_constr, - i_diverge: diverges_constr, used_vars: v}; ccx.fm.insert(id, rslt); #debug("%s has %u constraints", name, num_constraints(rslt)); diff --git a/src/rustc/middle/tstate/pre_post_conditions.rs b/src/rustc/middle/tstate/pre_post_conditions.rs index 3d1db2f6e66..20a1c7bff85 100644 --- a/src/rustc/middle/tstate/pre_post_conditions.rs +++ b/src/rustc/middle/tstate/pre_post_conditions.rs @@ -88,17 +88,9 @@ fn find_pre_post_exprs(fcx: fn_ctxt, args: [@expr], id: node_id) { seq_postconds(fcx, vec::map(pps, get_post))); } -fn find_pre_post_loop(fcx: fn_ctxt, l: @local, index: @expr, body: blk, - id: node_id) { +fn find_pre_post_loop(fcx: fn_ctxt, index: @expr, body: blk, id: node_id) { find_pre_post_expr(fcx, index); find_pre_post_block(fcx, body); - pat_bindings(fcx.ccx.tcx.def_map, l.node.pat) {|p_id, _s, n| - let v_init = ninit(p_id, path_to_ident(n)); - relax_precond_block(fcx, bit_num(fcx, v_init) as node_id, body); - // Hack: for-loop index variables are frequently ignored, - // so we pretend they're used - use_var(fcx, p_id); - }; let loop_precond = seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]); @@ -184,8 +176,6 @@ fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id, let p = expr_pp(fcx.ccx, rhs); set_pre_and_post(fcx.ccx, larger_id, p.precondition, p.postcondition); - gen(fcx, larger_id, - ninit(nid, path_to_ident(pth))); } _ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); } } @@ -207,23 +197,13 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr, if is_path(rhs) { forget_in_postcond(fcx, parent.id, rhs.id); } } oper_swap { - forget_in_postcond_still_init(fcx, parent.id, lhs.id); - forget_in_postcond_still_init(fcx, parent.id, rhs.id); + forget_in_postcond(fcx, parent.id, lhs.id); + forget_in_postcond(fcx, parent.id, rhs.id); } oper_assign { - forget_in_postcond_still_init(fcx, parent.id, lhs.id); - } - _ { - // pure and assign_op require the lhs to be init'd - let df = node_id_to_def_strict(fcx.ccx.tcx, lhs.id); - alt df { - def_local(nid, _) { - let i = bit_num(fcx, ninit(nid, path_to_ident(p))); - require_and_preserve(i, expr_pp(fcx.ccx, lhs)); - } - _ { } - } + forget_in_postcond(fcx, parent.id, lhs.id); } + _ { } } gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p); @@ -255,22 +235,6 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr, } } -fn handle_var(fcx: fn_ctxt, rslt: pre_and_post, id: node_id, name: ident) { - handle_var_def(fcx, rslt, node_id_to_def_strict(fcx.ccx.tcx, id), name); -} - -fn handle_var_def(fcx: fn_ctxt, rslt: pre_and_post, def: def, name: ident) { - log(debug, ("handle_var_def: ", def, name)); - alt def { - def_local(nid, _) | def_arg(nid, _) { - use_var(fcx, nid); - let i = bit_num(fcx, ninit(nid, name)); - require_and_preserve(i, rslt); - } - _ {/* nothing to check */ } - } -} - fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [mode], operands: [@expr]) { vec::iteri(modes) {|i,mode| @@ -284,10 +248,6 @@ fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [mode], fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) { let rslt = expr_pp(fcx.ccx, e); clear_pp(rslt); - for vec::each(*freevars::get_freevars(fcx.ccx.tcx, e.id)) {|def| - log(debug, ("handle_var_def: def=", def)); - handle_var_def(fcx, rslt, def.def, "upvar"); - } } /* Fills in annotations as a side effect. Does not rebuild the expr */ @@ -332,7 +292,6 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) { expr_path(p) { let rslt = expr_pp(fcx.ccx, e); clear_pp(rslt); - handle_var(fcx, rslt, e.id, path_to_ident(p)); } expr_new(p, _, v) { find_pre_post_exprs(fcx, [p, v], e.id); @@ -374,7 +333,7 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) { already be initialized */ find_pre_post_exprs(fcx, [lhs, rhs], e.id); - forget_in_postcond_still_init(fcx, e.id, lhs.id); + forget_in_postcond(fcx, e.id, lhs.id); } expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); } expr_ret(maybe_val) { @@ -555,25 +514,16 @@ fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) { } none { } } - gen(fcx, id, ninit(p_id, ident)); }; - if an_init.op == init_move && is_path(an_init.expr) { - forget_in_postcond(fcx, id, an_init.expr.id); - } - /* Clear out anything that the previous initializer guaranteed */ let e_pp = expr_pp(fcx.ccx, an_init.expr); tritv_copy(prev_pp.precondition, seq_preconds(fcx, [prev_pp, e_pp])); + /* Include the LHSs too, since those aren't in the postconds of the RHSs themselves */ - pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat) - {|pat_id, _s, n| - set_in_postcond(bit_num(fcx, - ninit(pat_id, path_to_ident(n))), prev_pp); - }; copy_pre_post_(fcx.ccx, id, prev_pp.precondition, prev_pp.postcondition); } @@ -659,10 +609,6 @@ fn find_pre_post_block(fcx: fn_ctxt, b: blk) { } fn find_pre_post_fn(fcx: fn_ctxt, body: blk) { - // hack - use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_return)); - use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_diverge)); - find_pre_post_block(fcx, body); // Treat the tail expression as a return statement diff --git a/src/rustc/middle/tstate/states.rs b/src/rustc/middle/tstate/states.rs index 4e484fccd07..abfe2989f78 100644 --- a/src/rustc/middle/tstate/states.rs +++ b/src/rustc/middle/tstate/states.rs @@ -55,22 +55,6 @@ fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path, } } -fn handle_fail(fcx: fn_ctxt, pres:prestate, post:poststate) { - // Remember what the old value of the "I return" trit was, so that - // we can avoid changing that (if it was true, there was a return - // that dominates this fail and the fail is unreachable) - if !promises(fcx, pres, fcx.enclosing.i_return) - // (only if we're in a diverging function -- you can fail when - // you're supposed to return, but not vice versa). - && fcx.enclosing.cf == noreturn { - kill_poststate_(fcx, fcx.enclosing.i_return, post); - } else { - // This code is unreachable (it's dominated by a return), - // so doesn't diverge. - kill_poststate_(fcx, fcx.enclosing.i_diverge, post); - } -} - fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) -> {changed: bool, post: poststate} { let mut changed = false; @@ -90,12 +74,6 @@ fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) -> } _ { } } - alt d { - local_dest(i) { - set_in_poststate_ident(fcx, i.node, i.ident, post); - } - _ {} - } } // Forget the RHS if we just moved it. @@ -104,15 +82,6 @@ fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) -> } } none { - for b.lhs.each {|d| - // variables w/o an initializer - alt check d { - // would be an error to pass something uninit'd to a call - local_dest(i) { - clear_in_poststate_ident_(fcx, i.node, i.ident, post); - } - } - } } } } @@ -158,16 +127,15 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr, alt ty { oper_move { if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); } - forget_in_poststate_still_init(fcx, post, lhs.id); + forget_in_poststate(fcx, post, lhs.id); } oper_swap { - forget_in_poststate_still_init(fcx, post, lhs.id); - forget_in_poststate_still_init(fcx, post, rhs.id); + forget_in_poststate(fcx, post, lhs.id); + forget_in_poststate(fcx, post, rhs.id); } - _ { forget_in_poststate_still_init(fcx, post, lhs.id); } + _ { forget_in_poststate(fcx, post, lhs.id); } } - gen_if_local(fcx, post, lhs); alt rhs.node { expr_path(p1) { let d = local_node_id_to_local_def_id(fcx, lhs.id); @@ -222,7 +190,6 @@ fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id, alt cf { noreturn { let post = false_postcond(num_constraints(fcx.enclosing)); - handle_fail(fcx, pres, post); changed |= set_poststate_ann(fcx.ccx, id, post); } _ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); } @@ -240,16 +207,9 @@ fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local, set_prestate_ann(fcx.ccx, id, loop_pres) | find_pre_post_state_expr(fcx, pres, index); - // Make sure the index vars are considered initialized - // in the body let index_post = tritv_clone(expr_poststate(fcx.ccx, index)); - pat_bindings(fcx.ccx.tcx.def_map, l.node.pat) {|p_id, _s, n| - set_in_poststate_ident(fcx, p_id, path_to_ident(n), index_post); - }; - changed |= find_pre_post_state_block(fcx, index_post, body); - if has_nonlocal_exits(body) { // See [Break-unsound] ret changed | set_poststate_ann(fcx.ccx, id, pres); @@ -261,20 +221,6 @@ fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local, } } -fn gen_if_local(fcx: fn_ctxt, p: poststate, e: @expr) -> bool { - alt e.node { - expr_path(pth) { - alt fcx.ccx.tcx.def_map.find(e.id) { - some(def_local(nid, _)) { - ret set_in_poststate_ident(fcx, nid, path_to_ident(pth), p); - } - _ { ret false; } - } - } - _ { ret false; } - } -} - fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk, maybe_alt: option<@expr>, id: node_id, chk: if_ty, pres: prestate) -> bool { @@ -465,13 +411,10 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool { } expr_ret(maybe_ret_val) { let mut changed = set_prestate_ann(fcx.ccx, e.id, pres); - /* normally, everything is true if execution continues after + /* everything is true if execution continues after a ret expression (since execution never continues locally after a ret expression */ - // FIXME should factor this out let post = false_postcond(num_constrs); - // except for the "diverges" bit... - kill_poststate_(fcx, fcx.enclosing.i_diverge, post); set_poststate_ann(fcx.ccx, e.id, post); @@ -593,7 +536,6 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool { /* if execution continues after fail, then everything is true! woo! */ let post = false_postcond(num_constrs); - handle_fail(fcx, pres, post); ret set_prestate_ann(fcx.ccx, e.id, pres) | set_poststate_ann(fcx.ccx, e.id, post) | option::map_default(maybe_fail_val, false, {|fail_val| @@ -727,13 +669,8 @@ fn find_pre_post_state_fn(fcx: fn_ctxt, // This ensures that intersect works correctly. kill_all_prestate(fcx, f_body.node.id); - // Arguments start out initialized - let block_pre = block_prestate(fcx.ccx, f_body); - for f_decl.inputs.each {|a| - set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre); - } - // Instantiate any constraints on the arguments so we can use them + let block_pre = block_prestate(fcx.ccx, f_body); for f_decl.constraints.each {|c| let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c); set_in_prestate_constr(fcx, tsc, block_pre); @@ -741,23 +678,6 @@ fn find_pre_post_state_fn(fcx: fn_ctxt, let mut changed = find_pre_post_state_block(fcx, block_pre, f_body); - // Treat the tail expression as a return statement - alt f_body.node.expr { - some(tailexpr) { - - // We don't want to clear the diverges bit for bottom typed things, - // which really do diverge. I feel like there is a cleaner way - // to do this than checking the type. - if !type_is_bot(expr_ty(fcx.ccx.tcx, tailexpr)) { - let post = false_postcond(num_constrs); - // except for the "diverges" bit... - kill_poststate_(fcx, fcx.enclosing.i_diverge, post); - set_poststate_ann(fcx.ccx, f_body.node.id, post); - } - } - none {/* fallthrough */ } - } - /* #error("find_pre_post_state_fn"); log(error, changed); diff --git a/src/test/compile-fail/liveness-unused.rs b/src/test/compile-fail/liveness-unused.rs index 2a19c9808c7..83f0c9b802a 100644 --- a/src/test/compile-fail/liveness-unused.rs +++ b/src/test/compile-fail/liveness-unused.rs @@ -1,20 +1,14 @@ fn f1(x: int) { //!^ WARNING unused variable: `x` - //!^^ WARNING unused variable x - // (the 2nd one is from tstate) } fn f1b(&x: int) { //!^ WARNING unused variable: `x` - //!^^ WARNING unused variable x - // (the 2nd one is from tstate) } fn f2() { let x = 3; //!^ WARNING unused variable: `x` - //!^^ WARNING unused variable x - // (the 2nd one is from tstate) } fn f3() { diff --git a/src/test/run-pass/liveness-loop-break.rs b/src/test/run-pass/liveness-loop-break.rs index 58274555202..cec9c25e67a 100644 --- a/src/test/run-pass/liveness-loop-break.rs +++ b/src/test/run-pass/liveness-loop-break.rs @@ -1,5 +1,3 @@ -// xfail-test --- tstate incorrectly fails this - fn test() { let v; loop {