From 5cf5f5024d5efcbb0b399433fa2117e1146292c2 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 1 Aug 2011 20:55:04 -0700 Subject: Handle bang functions correctly in typestate The logic for how the "returns" constraint was handled was always dodgy, for reasons explained in the comments I added to auxiliary::fn_info in this commit. Fixed it by adding distinct "returns" and "diverges" constraints for each function, which are both handled positively (that is: for a ! function, the "diverges" constraint must be true on every exit path; for any other function, the "returns" constraint must be true on every exit path). Closes #779 --- src/comp/middle/tstate/auxiliary.rs | 52 ++++++++++++++++--- src/comp/middle/tstate/ck.rs | 21 ++++---- src/comp/middle/tstate/collect_locals.rs | 20 ++++++-- src/comp/middle/tstate/pre_post_conditions.rs | 6 ++- src/comp/middle/tstate/states.rs | 73 +++++++++++++-------------- 5 files changed, 113 insertions(+), 59 deletions(-) (limited to 'src/comp') diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index 7ad070446f8..e1a01731ea1 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -238,21 +238,58 @@ type norm_constraint = {bit_num: uint, c: sp_constr}; type constr_map = @std::map::hashmap[def_id, constraint]; +/* Contains stuff that has to be computed up front */ type fn_info = - /* list, accumulated during pre/postcondition - computation, of all local variables that may be - used*/ - // Doesn't seem to work without the @ -- - // bug? {constrs: constr_map, num_constraints: uint, cf: controlflow, +/* 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. +*/ + i_return: tsconstr, + i_diverge: tsconstr, + /* list, accumulated during pre/postcondition + computation, of all local variables that may be + used */ +// Doesn't seem to work without the @ -- bug used_vars: @mutable 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 = @mutable ts_ann[mutable ]; @@ -261,7 +298,10 @@ type node_ann_table = @mutable ts_ann[mutable ]; type fn_info_map = @std::map::hashmap[node_id, fn_info]; type fn_ctxt = - {enclosing: fn_info, id: node_id, name: ident, ccx: crate_ctxt}; + {enclosing: fn_info, + id: node_id, + name: ident, + ccx: crate_ctxt}; type crate_ctxt = {tcx: ty::ctxt, node_anns: node_ann_table, fm: fn_info_map}; diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs index 37eace68d5d..73b845ac3bf 100644 --- a/src/comp/middle/tstate/ck.rs +++ b/src/comp/middle/tstate/ck.rs @@ -40,7 +40,7 @@ import std::option::none; import aux::*; import syntax::print::pprust::ty_to_str; import util::common::log_stmt_err; -import bitvectors::promises; +import bitvectors::*; import annotate::annotate_crate; import collect_locals::mk_f_to_fn_info; import pre_post_conditions::fn_pre_post; @@ -141,11 +141,11 @@ fn check_states_against_conditions(fcx: &fn_ctxt, f: &_fn, /* Check that the return value is initialized */ let post = aux::block_poststate(fcx.ccx, f.body); - let ret_c: tsconstr = ninit(fcx.id, fcx.name); - if f.proto == ast::proto_fn && !promises(fcx, post, ret_c) && - !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) && - f.decl.cf == return { - fcx.ccx.tcx.sess.span_note(f.body.span, + if f.proto == ast::proto_fn && + !promises(fcx, post, fcx.enclosing.i_return) && + !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) && + f.decl.cf == return { + fcx.ccx.tcx.sess.span_err(f.body.span, "In function " + fcx.name + ", not all control paths \ return a value"); @@ -153,12 +153,11 @@ fn check_states_against_conditions(fcx: &fn_ctxt, f: &_fn, "see declared return type of '" + ty_to_str(*f.decl.output) + "'"); } else if (f.decl.cf == noreturn) { - - // check that this really always fails - // the fcx.id bit means "returns" for a returning fn, - // "diverges" for a non-returning fn - if !promises(fcx, post, ret_c) { + // 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 + diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index 4dd9750c7db..3f85007d0cb 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -109,16 +109,28 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &ty_param[], f_sp: &span, next = add_constraint(cx.tcx, sc, next, res_map); } - /* add a pseudo-entry for the function's return value - we can safely use the function's name itself for this purpose */ + /* add the special i_diverge and i_return constraints + (see the type definition for auxiliary::fn_info for an explanation) */ + + // use the name of the function for the "return" constraint + next = add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), 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_name = name + "!"; + add_constraint(cx.tcx, respan(f_sp, ninit(diverges_id, diverges_name)), + next, res_map); - add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map); let v: @mutable node_id[] = @mutable ~[]; let rslt = {constrs: res_map, num_constraints: - ivec::len(*cx.cs) + ivec::len(f.decl.constraints) + 1u, + // add 2 to account for the i_return and i_diverge constraints + ivec::len(*cx.cs) + ivec::len(f.decl.constraints) + 2u, cf: f.decl.cf, + i_return: ninit(id, name), + i_diverge: ninit(diverges_id, diverges_name), used_vars: v}; ccx.fm.insert(id, rslt); log name + " has " + std::uint::str(num_constraints(rslt)) + diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 84c75fa1686..54e53af0ff3 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -79,6 +79,9 @@ fn find_pre_post_item(ccx: &crate_ctxt, i: &item) { {constrs: @new_def_hash[constraint](), num_constraints: 0u, cf: return, + // just bogus + i_return: ninit(0, ""), + i_diverge: ninit(0, ""), used_vars: v}, id: 0, name: "", @@ -692,7 +695,8 @@ fn find_pre_post_block(fcx: &fn_ctxt, b: blk) { fn find_pre_post_fn(fcx: &fn_ctxt, f: &_fn) { // hack - use_var(fcx, fcx.id); + 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, f.body); diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 90a7cd88eff..66c2b4324ab 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -1,4 +1,5 @@ import syntax::print::pprust::path_to_str; +import util::ppaux::ty_to_str; import std::ivec; import std::option; import std::option::get; @@ -6,21 +7,7 @@ import std::option::is_none; import std::option::none; import std::option::some; import std::option::maybe; -import tstate::ann::set_in_poststate_; -import tstate::ann::pre_and_post; -import tstate::ann::get_post; -import tstate::ann::postcond; -import tstate::ann::empty_pre_post; -import tstate::ann::empty_poststate; -import tstate::ann::clear_in_poststate; -import tstate::ann::intersect; -import tstate::ann::empty_prestate; -import tstate::ann::prestate; -import tstate::ann::poststate; -import tstate::ann::false_postcond; -import tstate::ann::ts_ann; -import tstate::ann::set_prestate; -import tstate::ann::set_poststate; +import ann::*; import aux::*; import tritv::tritv_clone; import tritv::tritv_set; @@ -189,9 +176,8 @@ fn find_pre_post_state_exprs(fcx: &fn_ctxt, pres: &prestate, id: node_id, /* if this is a failing call, it sets everything as initialized */ alt cf { noreturn. { - changed |= - set_poststate_ann(fcx.ccx, id, - false_postcond(num_constraints(fcx.enclosing))); + let post = false_postcond(num_constraints(fcx.enclosing)); + changed |= set_poststate_ann(fcx.ccx, id, post); } _ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); } } @@ -403,15 +389,14 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) -> /* normally, 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, false_postcond(num_constrs)); - /* return from an always-failing function clears the return bit */ + set_poststate_ann(fcx.ccx, e.id, post); - alt fcx.enclosing.cf { - noreturn. { kill_poststate(fcx, e.id, ninit(fcx.id, fcx.name)); } - _ { } - } - alt maybe_ret_val { + alt maybe_ret_val { none. {/* do nothing */ } some(ret_val) { changed |= find_pre_post_state_expr(fcx, pres, ret_val); @@ -421,7 +406,10 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) -> } expr_be(val) { let changed = set_prestate_ann(fcx.ccx, e.id, pres); - set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs)); + 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); ret changed | find_pre_post_state_expr(fcx, pres, val); } expr_if(antec, conseq, maybe_alt) { @@ -558,12 +546,20 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) -> ret find_pre_post_state_sub(fcx, pres, operand, e.id, none); } expr_fail(maybe_fail_val) { + // FIXME Should factor out this code, + // which also appears in find_pre_post_state_exprs + /* if execution continues after fail, then everything is true! + woo! */ + let post = false_postcond(num_constrs); + alt fcx.enclosing.cf { + noreturn. { + kill_poststate_(fcx, ninit(fcx.id, fcx.name), post); + } + _ {} + } ret set_prestate_ann(fcx.ccx, e.id, pres) | - /* if execution continues after fail, then everything is true! - woo! */ - set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs)) - | - alt maybe_fail_val { + set_poststate_ann(fcx.ccx, e.id, post) + | alt maybe_fail_val { none. { false } some(fail_val) { find_pre_post_state_expr(fcx, pres, fail_val) @@ -710,9 +706,11 @@ fn find_pre_post_state_block(fcx: &fn_ctxt, pres0: &prestate, b: &blk) -> fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool { - let num_local_vars = num_constraints(fcx.enclosing); - // make sure the return bit starts out False - clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id); + let num_constrs = num_constraints(fcx.enclosing); + // make sure the return and diverge bits start out False + kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_return); + kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_diverge); + // Instantiate any constraints on the arguments so we can use them let block_pre = block_prestate(fcx.ccx, f.body); let tsc; @@ -728,15 +726,16 @@ fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool { some(tailexpr) { let tailty = expr_ty(fcx.ccx.tcx, tailexpr); - // Since blocks and alts and ifs that don't have results // implicitly result in nil, we have to be careful to not // interpret nil-typed block results as the result of a // function with some other return type if !type_is_nil(fcx.ccx.tcx, tailty) && !type_is_bot(fcx.ccx.tcx, tailty) { - let p = false_postcond(num_local_vars); - set_poststate_ann(fcx.ccx, f.body.node.id, p); + 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 */ } -- cgit 1.4.1-3-g733a5