rust/src/comp/middle/tstate/states.rs

771 lines
26 KiB
Rust
Raw Normal View History

import syntax::print::pprust::path_to_str;
import std::ivec;
import std::option;
import std::option::get;
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 aux::*;
import tritv::tritv_clone;
import tritv::tritv_set;
import tritv::ttrue;
import bitvectors::*;
import syntax::ast::*;
import middle::ty::expr_ty;
import middle::ty::type_is_nil;
import middle::ty::type_is_bot;
import util::common::new_def_hash;
import util::common::log_expr;
import util::common::log_block;
import util::common::log_block_err;
import util::common::log_fn;
import util::common::elt_exprs;
import util::common::field_exprs;
import util::common::has_nonlocal_exits;
import util::common::log_stmt;
import util::common::log_stmt_err;
import util::common::log_expr_err;
fn handle_move_or_copy(fcx: &fn_ctxt, post: &poststate, rhs_path: &path,
rhs_id: &node_id, instlhs: &inst, init_op: &init_op) {
let rhs_d = local_node_id_to_def_id(fcx, rhs_id);
alt (rhs_d) {
some(rhsid) {
// RHS is a local var
let instrhs =
{ident: path_to_ident(fcx.ccx.tcx, rhs_path), node: rhsid.node};
copy_in_poststate(fcx, post, instlhs, instrhs,
op_to_oper_ty(init_op));
}
_ {
// not a local -- do nothing
}
}
if (init_op == init_move) {
forget_in_poststate(fcx, post, rhs_id);
}
}
fn seq_states(fcx: &fn_ctxt, pres: &prestate, bindings: &binding[])
-> {changed: bool, post: poststate} {
2011-07-27 07:19:39 -05:00
let changed = false;
let post = tritv_clone(pres);
for b:binding in bindings {
alt (b.rhs) {
some(an_init) {
// an expression, with or without a destination
changed |= find_pre_post_state_expr(fcx, post, an_init.expr)
|| changed;
post = tritv_clone(expr_poststate(fcx.ccx, an_init.expr));
alt (b.lhs) {
some(i) {
alt (an_init.expr.node) {
expr_path(p) {
handle_move_or_copy(fcx, post, p, an_init.expr.id, i,
an_init.op);
}
_ {}
}
set_in_poststate_ident(fcx, i.node, i.ident, post);
}
_ {
//This is an expression that doesn't get named.
// So, nothing more to do.
}
}
}
none {
alt (b.lhs) {
some(i) {
// variable w/o an initializer
clear_in_poststate_ident_(fcx, i.node, i.ident, post);
}
none { fcx.ccx.tcx.sess.bug("seq_states: binding has \
neither an lhs nor an rhs");
}
}
}
}
}
2011-07-27 07:19:39 -05:00
ret {changed: changed, post: post};
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_sub(fcx: &fn_ctxt, pres: &prestate, e: &@expr,
parent: node_id, c: option::t[tsconstr]) -> bool {
let changed = find_pre_post_state_expr(fcx, pres, e);
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
2011-07-27 07:19:39 -05:00
let post = tritv_clone(expr_poststate(fcx.ccx, e));
alt c {
none. { }
some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_two(fcx: &fn_ctxt, pres: &prestate, lhs: &@expr,
rhs: &@expr, parent: node_id, ty: oper_type) ->
bool {
let changed = set_prestate_ann(fcx.ccx, parent, pres);
changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
2011-07-27 07:19:39 -05:00
changed =
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs), rhs) ||
changed;
let post = tritv_clone(expr_poststate(fcx.ccx, rhs));
alt lhs.node {
expr_path(p) {
// for termination, need to make sure intermediate changes don't set
// changed flag
// tmp remembers "old" constraints we'd otherwise forget,
// for substitution purposes
let tmp = tritv_clone(post);
alt ty {
oper_move. {
if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
forget_in_poststate_still_init(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_still_init(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);
let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
alt d {
some(id) {
alt d1 {
some(id1) {
let instlhs =
{ident: path_to_ident(fcx.ccx.tcx, p), node: id};
let instrhs =
{ident: path_to_ident(fcx.ccx.tcx, p1), node: id1};
copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
ty);
}
_ { }
}
2011-07-27 07:19:39 -05:00
}
_ { }
}
2011-07-27 07:19:39 -05:00
}
_ {/* do nothing */ }
}
2011-07-27 07:19:39 -05:00
}
_ { }
}
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
ret changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_call(fcx: &fn_ctxt, pres: &prestate, a: &@expr,
id: node_id, bs: &(@expr)[], cf: controlflow) ->
bool {
let changed = find_pre_post_state_expr(fcx, pres, a);
ret find_pre_post_state_exprs(fcx, expr_poststate(fcx.ccx, a), id, bs, cf)
|| changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_exprs(fcx: &fn_ctxt, pres: &prestate, id: node_id,
es: &(@expr)[], cf: controlflow) -> bool {
let rs = seq_states(fcx, pres, anon_bindings(es));
2011-07-27 07:19:39 -05:00
let changed = rs.changed | set_prestate_ann(fcx.ccx, id, pres);
/* if this is a failing call, it sets everything as initialized */
2011-07-27 07:19:39 -05:00
alt cf {
noreturn. {
changed |=
set_poststate_ann(fcx.ccx, id,
false_postcond(num_constraints(fcx.enclosing)));
}
_ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
}
ret changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_loop(fcx: &fn_ctxt, pres: prestate, l: &@local,
index: &@expr, body: &blk, id: node_id) -> bool {
let loop_pres = intersect_states(pres, block_poststate(fcx.ccx, body));
2011-07-27 07:19:39 -05:00
let changed =
set_prestate_ann(fcx.ccx, id, loop_pres) |
find_pre_post_state_expr(fcx, pres, index);
// Make sure the index var is considered initialized
// in the body
2011-07-27 07:19:39 -05:00
let index_post = tritv_clone(expr_poststate(fcx.ccx, index));
set_in_poststate_ident(fcx, l.node.id, l.node.ident, index_post);
changed |= find_pre_post_state_block(fcx, index_post, body);
2011-07-27 07:19:39 -05:00
if has_nonlocal_exits(body) {
// See [Break-unsound]
2011-07-27 07:19:39 -05:00
ret changed | set_poststate_ann(fcx.ccx, id, pres);
} else {
let res_p =
intersect_states(expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body));
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
}
}
2011-07-27 07:19:39 -05:00
fn gen_if_local(fcx: &fn_ctxt, p: &poststate, e: &@expr) -> bool {
alt e.node {
expr_path(pth) {
alt freevars::def_lookup(fcx.ccx.tcx, fcx.id, e.id) {
some(def_local(loc)) {
ret set_in_poststate_ident(fcx, loc.node,
path_to_ident(fcx.ccx.tcx, pth), p);
}
_ { ret false; }
}
}
_ { ret false; }
}
}
2011-07-27 07:19:39 -05:00
fn join_then_else(fcx: &fn_ctxt, antec: &@expr, conseq: &blk,
maybe_alt: &option::t[@expr], id: node_id, chk: &if_ty,
pres: &prestate) -> bool {
let changed =
set_prestate_ann(fcx.ccx, id, pres) |
find_pre_post_state_expr(fcx, pres, antec);
/*
log_err("join_then_else:");
log_expr_err(*antec);
log_bitv_err(fcx, expr_prestate(fcx.ccx, antec));
log_bitv_err(fcx, expr_poststate(fcx.ccx, antec));
log_block_err(conseq);
log_bitv_err(fcx, block_prestate(fcx.ccx, conseq));
log_bitv_err(fcx, block_poststate(fcx.ccx, conseq));
log_err("****");
log_bitv_err(fcx, expr_precond(fcx.ccx, antec));
log_bitv_err(fcx, expr_postcond(fcx.ccx, antec));
log_bitv_err(fcx, block_precond(fcx.ccx, conseq));
log_bitv_err(fcx, block_postcond(fcx.ccx, conseq));
*/
2011-07-27 07:19:39 -05:00
alt maybe_alt {
none. {
changed |=
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
conseq) |
set_poststate_ann(fcx.ccx, id,
expr_poststate(fcx.ccx, antec));
2011-07-27 07:19:39 -05:00
}
some(altern) {
changed |=
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, antec),
altern);
let conseq_prestate = expr_poststate(fcx.ccx, antec);
alt chk {
if_check. {
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
conseq_prestate = tritv_clone(conseq_prestate);
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
}
_ { }
}
changed |= find_pre_post_state_block(fcx, conseq_prestate, conseq);
let poststate_res =
intersect_states(block_poststate(fcx.ccx, conseq),
expr_poststate(fcx.ccx, altern));
/*
fcx.ccx.tcx.sess.span_note(antec.span,
"poststate_res = " + aux::tritv_to_str(fcx, poststate_res));
fcx.ccx.tcx.sess.span_note(antec.span,
"altern poststate = " +
aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
fcx.ccx.tcx.sess.span_note(antec.span,
"conseq poststate = " + aux::tritv_to_str(fcx,
block_poststate(fcx.ccx, conseq)));
*/
changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
}
}
ret changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
bool {
let num_constrs = num_constraints(fcx.enclosing);
alt e.node {
expr_vec(elts, _, _) {
ret find_pre_post_state_exprs(fcx, pres, e.id, elts, return);
}
expr_call(operator, operands) {
ret find_pre_post_state_call(fcx, pres, operator, e.id, operands,
controlflow_expr(fcx.ccx, operator));
}
expr_spawn(_, _, operator, operands) {
ret find_pre_post_state_call(fcx, pres, operator, e.id, operands,
return);
}
expr_bind(operator, maybe_args) {
let args = ~[];
for a_opt: option::t[@expr] in maybe_args {
alt a_opt { none. {/* no-op */ } some(a) { args += ~[a]; } }
}
ret find_pre_post_state_call(fcx, pres, operator, e.id, args, return);
}
expr_path(_) { ret pure_exp(fcx.ccx, e.id, pres); }
expr_log(_, ex) {
ret find_pre_post_state_sub(fcx, pres, ex, e.id, none);
}
expr_chan(ex) {
ret find_pre_post_state_sub(fcx, pres, ex, e.id, none);
}
expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
expr_put(maybe_e) {
alt maybe_e {
some(arg) {
ret find_pre_post_state_sub(fcx, pres, arg, e.id, none);
}
none. { ret pure_exp(fcx.ccx, e.id, pres); }
}
}
expr_lit(l) { ret pure_exp(fcx.ccx, e.id, pres); }
expr_fn(f) { ret pure_exp(fcx.ccx, e.id, pres); }
expr_block(b) {
ret find_pre_post_state_block(fcx, pres, b) |
set_prestate_ann(fcx.ccx, e.id, pres) |
set_poststate_ann(fcx.ccx, e.id, block_poststate(fcx.ccx, b));
2011-07-27 07:19:39 -05:00
}
expr_rec(fields, maybe_base) {
let changed =
find_pre_post_state_exprs(fcx, pres, e.id, field_exprs(fields),
return);
alt maybe_base {
none. {/* do nothing */ }
some(base) {
changed |=
find_pre_post_state_expr(fcx, pres, base) |
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, base));
}
}
ret changed;
}
expr_move(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_move);
}
expr_assign(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_assign);
}
expr_swap(lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_swap);
// Could be more precise and actually swap the role of
// lhs and rhs in constraints
}
expr_recv(lhs, rhs) {
// Opposite order as most other binary operations,
// so not using find_pre_post_state_two
let changed =
set_prestate_ann(fcx.ccx, e.id, pres) |
find_pre_post_state_expr(fcx, pres, lhs) |
2011-07-27 07:19:39 -05:00
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs),
rhs);
let post = tritv_clone(expr_poststate(fcx.ccx, rhs));
forget_in_poststate_still_init(fcx, post, rhs.id);
gen_if_local(fcx, post, rhs);
ret changed | set_poststate_ann(fcx.ccx, e.id, post);
}
expr_ret(maybe_ret_val) {
let changed = set_prestate_ann(fcx.ccx, e.id, pres);
/* normally, everything is true if execution continues after
a ret expression (since execution never continues locally
after a ret expression */
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
/* return from an always-failing function clears the return bit */
alt fcx.enclosing.cf {
noreturn. { kill_poststate(fcx, e.id, ninit(fcx.id, fcx.name)); }
_ { }
}
alt maybe_ret_val {
none. {/* do nothing */ }
some(ret_val) {
changed |= find_pre_post_state_expr(fcx, pres, ret_val);
}
}
ret changed;
}
expr_be(val) {
let changed = set_prestate_ann(fcx.ccx, e.id, pres);
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
ret changed | find_pre_post_state_expr(fcx, pres, val);
}
expr_if(antec, conseq, maybe_alt) {
ret join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if,
pres);
}
expr_ternary(_, _, _) {
ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
}
expr_binary(bop, l, r) {
if lazy_binop(bop) {
let changed = find_pre_post_state_expr(fcx, pres, l);
changed |=
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r);
ret changed | set_prestate_ann(fcx.ccx, e.id, pres) |
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, l));
} else {
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
}
2011-07-27 07:19:39 -05:00
}
expr_send(l, r) {
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
}
expr_assign_op(op, lhs, rhs) {
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id,
oper_assign_op);
}
expr_while(test, body) {
/*
log_err "in a while loop:";
log_expr_err(*e);
aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body));
aux::log_tritv_err(fcx, pres);
*/
let loop_pres =
intersect_states(block_poststate(fcx.ccx, body), pres);
// aux::log_tritv_err(fcx, loop_pres);
// log_err "---------------";
let changed =
set_prestate_ann(fcx.ccx, e.id, loop_pres) |
find_pre_post_state_expr(fcx, loop_pres, test) |
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
body);
2011-07-27 07:19:39 -05:00
/* conservative approximation: if a loop contains a break
or cont, we assume nothing about the poststate */
/* which is still unsound -- see [Break-unsound] */
if has_nonlocal_exits(body) {
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
} else {
let e_post = expr_poststate(fcx.ccx, test);
let b_post = block_poststate(fcx.ccx, body);
ret changed |
set_poststate_ann(fcx.ccx, e.id,
intersect_states(e_post, b_post));
}
}
expr_do_while(body, test) {
let loop_pres = intersect_states(expr_poststate(fcx.ccx, test), pres);
let changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
changed |= find_pre_post_state_block(fcx, loop_pres, body);
/* conservative approximination: if the body of the loop
could break or cont, we revert to the prestate
(TODO: could treat cont differently from break, since
if there's a cont, the test will execute) */
changed |=
find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body),
test);
let breaks = has_nonlocal_exits(body);
if breaks {
// this should probably be true_poststate and not pres,
// b/c the body could invalidate stuff
// FIXME [Break-unsound]
// This is unsound as it is -- consider
// while (true) {
// x <- y;
// break;
// }
// The poststate wouldn't take into account that
// y gets deinitialized
changed |= set_poststate_ann(fcx.ccx, e.id, pres);
} else {
changed |=
set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, test));
}
ret changed;
}
expr_for(d, index, body) {
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
}
expr_for_each(d, index, body) {
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
}
expr_index(val, sub) {
ret find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure);
}
expr_alt(val, alts) {
let changed =
set_prestate_ann(fcx.ccx, e.id, pres) |
find_pre_post_state_expr(fcx, pres, val);
let e_post = expr_poststate(fcx.ccx, val);
let a_post;
if ivec::len(alts) > 0u {
a_post = false_postcond(num_constrs);
for an_alt: arm in alts {
changed |=
find_pre_post_state_block(fcx, e_post, an_alt.block);
intersect(a_post, block_poststate(fcx.ccx, an_alt.block));
// We deliberately do *not* update changed here, because
// we'd go into an infinite loop that way, and the change
// gets made after the if expression.
}
2011-07-27 07:19:39 -05:00
} else {
// No alts; poststate is the poststate of the test
a_post = e_post;
}
ret changed | set_poststate_ann(fcx.ccx, e.id, a_post);
}
expr_field(val, _) {
ret find_pre_post_state_sub(fcx, pres, val, e.id, none);
}
expr_unary(_, operand) {
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
}
expr_cast(operand, _) {
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
}
expr_fail(maybe_fail_val) {
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 {
none. { false }
some(fail_val) {
find_pre_post_state_expr(fcx, pres, fail_val)
}
}
2011-07-27 07:19:39 -05:00
}
expr_assert(p) {
ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
}
expr_check(_, p) {
/* predicate p holds after this expression executes */
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));
}
expr_if_check(p, conseq, maybe_alt) {
ret join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check, pres);
}
expr_break. { ret pure_exp(fcx.ccx, e.id, pres); }
expr_cont. { ret pure_exp(fcx.ccx, e.id, pres); }
expr_port(_) { ret pure_exp(fcx.ccx, e.id, pres); }
expr_self_method(_) { ret pure_exp(fcx.ccx, e.id, pres); }
expr_anon_obj(anon_obj) {
alt anon_obj.inner_obj {
2011-07-27 07:19:39 -05:00
some(wt) { ret find_pre_post_state_sub(fcx, pres, wt, e.id, none); }
none. { ret pure_exp(fcx.ccx, e.id, pres); }
}
}
2011-05-20 19:41:36 -05:00
}
}
fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt)
-> bool {
2011-07-27 07:19:39 -05:00
let stmt_ann = stmt_to_ann(fcx.ccx, *s);
/*
log_err "*At beginning: stmt = ";
log_stmt_err(*s);
log_err "*prestate = ";
log_tritv_err(fcx, stmt_ann.states.prestate);
log_err "*poststate =";
log_tritv_err(fcx, stmt_ann.states.poststate);
log_err "pres = ";
log_tritv_err(fcx, pres);
*/
alt (s.node) {
2011-07-27 07:19:39 -05:00
stmt_decl(adecl, id) {
alt (adecl.node) {
2011-07-27 07:19:39 -05:00
decl_local(alocals) {
set_prestate(stmt_ann, pres);
let c_and_p = seq_states(fcx, pres,
locals_to_bindings(alocals));
/* important to do this in one step to ensure
termination (don't want to set changed to true
for intermediate changes) */
let changed = (set_poststate(stmt_ann, c_and_p.post)
| c_and_p.changed);
/*
log_err "Summary: stmt = ";
log_stmt_err(*s);
log_err "prestate = ";
log_tritv_err(fcx, stmt_ann.states.prestate);
log_err "poststate =";
log_tritv_err(fcx, stmt_ann.states.poststate);
log_err "changed =";
log_err changed;
*/
2011-07-27 07:19:39 -05:00
ret changed;
}
decl_item(an_item) {
ret set_prestate(stmt_ann, pres) |
set_poststate(stmt_ann, pres);
/* the outer visitor will recurse into the item */
2011-07-27 07:19:39 -05:00
}
}
}
stmt_expr(ex, _) {
ret find_pre_post_state_expr(fcx, pres, ex) |
set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) |
set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex));
2011-07-27 07:19:39 -05:00
/*
log_err "Finally:";
log_stmt_err(*s);
log_err("prestate = ");
// log_err(bitv::to_str(stmt_ann.states.prestate));
log_tritv_err(fcx, stmt_ann.states.prestate);
log_err("poststate =");
// log_err(bitv::to_str(stmt_ann.states.poststate));
log_tritv_err(fcx, stmt_ann.states.poststate);
log_err("changed =");
log_err(changed);
*/
}
_ { ret false; }
}
}
/* Updates the pre- and post-states of statements in the block,
returns a boolean flag saying whether any pre- or poststates changed */
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_block(fcx: &fn_ctxt, pres0: &prestate, b: &blk) ->
bool {
/* First, set the pre-states and post-states for every expression */
2011-07-27 07:19:39 -05:00
let pres = pres0;
/* Iterate over each stmt. The new prestate is <pres>. The poststate
consist of improving <pres> with whatever variables this stmt
initializes. Then <pres> becomes the new poststate. */
2011-07-27 07:19:39 -05:00
let changed = false;
for s: @stmt in b.node.stmts {
changed |= find_pre_post_state_stmt(fcx, pres, s);
pres = stmt_poststate(fcx.ccx, *s);
}
2011-07-27 07:19:39 -05:00
let post = pres;
alt b.node.expr {
none. { }
some(e) {
changed |= find_pre_post_state_expr(fcx, pres, e);
post = expr_poststate(fcx.ccx, e);
}
}
set_prestate_ann(fcx.ccx, b.node.id, pres0);
set_poststate_ann(fcx.ccx, b.node.id, post);
/*
log_err "For block:";
log_block_err(b);
log_err "poststate = ";
log_states_err(block_states(fcx.ccx, b));
log_err "pres0:";
log_tritv_err(fcx, pres0);
log_err "post:";
log_tritv_err(fcx, post);
log_err "changed = ";
log_err changed;
*/
ret changed;
}
2011-07-27 07:19:39 -05:00
fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool {
2011-07-27 07:19:39 -05:00
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);
// Instantiate any constraints on the arguments so we can use them
2011-07-27 07:19:39 -05:00
let block_pre = block_prestate(fcx.ccx, f.body);
let tsc;
for c: @constr in f.decl.constraints {
tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c);
set_in_prestate_constr(fcx, tsc, block_pre);
}
2011-07-27 07:19:39 -05:00
let changed = find_pre_post_state_block(fcx, block_pre, f.body);
// Treat the tail expression as a return statement
2011-07-27 07:19:39 -05:00
alt f.body.node.expr {
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);
}
2011-07-27 07:19:39 -05:00
}
none. {/* fallthrough */ }
}
2011-07-27 07:19:39 -05:00
/*
log_err "find_pre_post_state_fn";
log_err changed;
fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name);
*/
ret changed;
}
//
// Local Variables:
// mode: rust
// fill-column: 78;
// indent-tabs-mode: nil
// c-basic-offset: 4
// buffer-file-coding-system: utf-8-unix
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
// End:
//