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 ];
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};
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;
/* 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");
"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 +
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)) +
{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: "",
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);
import syntax::print::pprust::path_to_str;
+import util::ppaux::ty_to_str;
import std::ivec;
import std::option;
import std::option::get;
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;
/* 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); }
}
/* 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);
}
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) {
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)
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;
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 */ }
--- /dev/null
+// xfail-stage0
+// error-pattern: some control paths may return
+fn f() -> ! { 3 }
+fn main(){}
projects / rust.git / commitdiff