remove initedness checking from typestate, as best I could
This commit is contained in:
parent
0d3811e275
commit
f5c51b0a9c
@ -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<pred_args_>;
|
||||
// for this local.
|
||||
type constr_arg_use = spanned<constr_arg_general_<inst>>;
|
||||
|
||||
/*
|
||||
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 <path> field (and the <def_id> 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 <path> field (and the
|
||||
<def_id> 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<tsconstr>;
|
||||
|
||||
@ -238,34 +214,8 @@ type constr_map = std::map::hashmap<def_id, constraint>;
|
||||
|
||||
/* 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<def> {
|
||||
}
|
||||
|
||||
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<inst> {
|
||||
@ -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<T>(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) ->
|
||||
|
@ -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
|
||||
|
@ -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<fn_ctxt>) {
|
||||
visit::visit_expr(e, fcx, v);
|
||||
|
||||
@ -109,39 +93,6 @@ fn check_states_against_conditions(fcx: fn_ctxt,
|
||||
visit_fn: bind do_nothing::<fn_ctxt>(_, _, _, _, _, _, _)
|
||||
with *visit::default_visitor::<fn_ctxt>()});
|
||||
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,
|
||||
|
@ -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<ctxt>) {
|
||||
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<ctxt>) {
|
||||
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::<ctxt>();
|
||||
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));
|
||||
|
@ -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
|
||||
|
@ -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);
|
||||
|
@ -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() {
|
||||
|
@ -1,5 +1,3 @@
|
||||
// xfail-test --- tstate incorrectly fails this
|
||||
|
||||
fn test() {
|
||||
let v;
|
||||
loop {
|
||||
|
Loading…
Reference in New Issue
Block a user