user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Handle bang functions correctly in typestate

Browse source 
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
This commit is contained in:
Tim Chevalier 2011-08-01 20:55:04 -07:00
parent c9b16ac4c2
commit 5cf5f5024d
6 changed files with 117 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/comp/middle/tstate/auxiliary.rs
View file

@ -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};

21
src/comp/middle/tstate/ck.rs
View file

@ -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 +

20
src/comp/middle/tstate/collect_locals.rs
View file

@ -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)) +

6
src/comp/middle/tstate/pre_post_conditions.rs
View file

@ -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);

73
src/comp/middle/tstate/states.rs
View file

@ -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 */ }

4
src/test/compile-fail/bang-tailexpr.rs Normal file
View file

@ -0,0 +1,4 @@
// xfail-stage0
// error-pattern: some control paths may return
fn f() -> ! { 3 }
fn main(){}