2011-08-01 22:55:04 -05:00
|
|
|
import ann::*;
|
2011-07-09 00:05:30 -05:00
|
|
|
import aux::*;
|
2011-09-12 18:13:28 -05:00
|
|
|
import tritv::{tritv_clone, tritv_set, ttrue};
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-07-21 18:03:30 -05:00
|
|
|
import bitvectors::*;
|
2012-01-14 18:05:07 -06:00
|
|
|
import pat_util::*;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::ast::*;
|
2011-08-21 23:44:41 -05:00
|
|
|
import syntax::ast_util::*;
|
2011-09-06 17:26:57 -05:00
|
|
|
import syntax::codemap::span;
|
2011-11-10 10:41:42 -06:00
|
|
|
import middle::ty::{expr_ty, type_is_bot};
|
2012-01-19 19:22:41 -06:00
|
|
|
import util::common::*;
|
2012-01-12 10:59:49 -06:00
|
|
|
import driver::session::session;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn forbid_upvar(fcx: fn_ctxt, rhs_id: node_id, sp: span, t: oper_type) {
|
2011-09-06 17:26:57 -05:00
|
|
|
alt t {
|
2012-01-19 00:37:22 -06:00
|
|
|
oper_move {
|
2011-09-06 17:26:57 -05:00
|
|
|
alt local_node_id_to_def(fcx, rhs_id) {
|
2011-09-12 04:27:30 -05:00
|
|
|
some(def_upvar(_, _, _)) {
|
|
|
|
fcx.ccx.tcx.sess.span_err(sp,
|
|
|
|
"Tried to deinitialize a variable \
|
2011-09-06 17:26:57 -05:00
|
|
|
declared in a different scope");
|
2011-09-12 04:27:30 -05:00
|
|
|
}
|
|
|
|
_ { }
|
2011-09-06 17:26:57 -05:00
|
|
|
}
|
|
|
|
}
|
2011-09-12 04:27:30 -05:00
|
|
|
_ {/* do nothing */ }
|
2011-09-06 17:26:57 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-11-30 06:38:38 -06:00
|
|
|
fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
|
2011-09-12 04:27:30 -05:00
|
|
|
rhs_id: node_id, instlhs: inst, init_op: init_op) {
|
2011-09-06 17:26:57 -05:00
|
|
|
forbid_upvar(fcx, rhs_id, rhs_path.span, op_to_oper_ty(init_op));
|
|
|
|
|
|
|
|
let rhs_d_id = local_node_id_to_def_id(fcx, rhs_id);
|
|
|
|
alt rhs_d_id {
|
2011-07-29 17:59:38 -05:00
|
|
|
some(rhsid) {
|
|
|
|
// RHS is a local var
|
|
|
|
let instrhs =
|
2012-01-14 18:05:07 -06:00
|
|
|
{ident: path_to_ident(rhs_path), node: rhsid.node};
|
2011-07-29 17:59:38 -05:00
|
|
|
copy_in_poststate(fcx, post, instlhs, instrhs,
|
|
|
|
op_to_oper_ty(init_op));
|
|
|
|
}
|
|
|
|
_ {
|
|
|
|
// not a local -- do nothing
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2012-01-20 19:23:56 -06:00
|
|
|
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);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) ->
|
2011-08-19 17:16:48 -05:00
|
|
|
{changed: bool, post: poststate} {
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed = false;
|
2011-07-29 17:59:38 -05:00
|
|
|
let post = tritv_clone(pres);
|
2011-08-19 17:16:48 -05:00
|
|
|
for b: binding in bindings {
|
|
|
|
alt b.rhs {
|
2011-07-29 17:59:38 -05:00
|
|
|
some(an_init) {
|
|
|
|
// an expression, with or without a destination
|
2011-08-19 17:16:48 -05:00
|
|
|
changed |=
|
|
|
|
find_pre_post_state_expr(fcx, post, an_init.expr) || changed;
|
2011-07-29 17:59:38 -05:00
|
|
|
post = tritv_clone(expr_poststate(fcx.ccx, an_init.expr));
|
2011-07-28 05:01:45 -05:00
|
|
|
for i: inst in b.lhs {
|
2011-08-19 17:16:48 -05:00
|
|
|
alt an_init.expr.node {
|
2011-07-29 17:59:38 -05:00
|
|
|
expr_path(p) {
|
|
|
|
handle_move_or_copy(fcx, post, p, an_init.expr.id, i,
|
|
|
|
an_init.op);
|
|
|
|
}
|
2011-08-08 21:38:19 -05:00
|
|
|
_ { }
|
2011-07-29 17:59:38 -05:00
|
|
|
}
|
|
|
|
set_in_poststate_ident(fcx, i.node, i.ident, post);
|
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
|
2011-08-08 21:38:19 -05:00
|
|
|
// Forget the RHS if we just moved it.
|
|
|
|
if an_init.op == init_move {
|
|
|
|
forget_in_poststate(fcx, post, an_init.expr.id);
|
|
|
|
}
|
2011-07-28 05:01:45 -05:00
|
|
|
}
|
|
|
|
none {
|
|
|
|
for i: inst in b.lhs {
|
|
|
|
// variables w/o an initializer
|
|
|
|
clear_in_poststate_ident_(fcx, i.node, i.ident, post);
|
2011-07-29 17:59:38 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
ret {changed: changed, post: post};
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr,
|
2012-01-31 19:05:20 -06:00
|
|
|
parent: node_id, c: option<tsconstr>) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed = find_pre_post_state_expr(fcx, pres, e);
|
2011-06-25 00:17:17 -05:00
|
|
|
|
|
|
|
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 {
|
2012-01-19 00:37:22 -06:00
|
|
|
none { }
|
2011-07-27 07:19:39 -05:00
|
|
|
some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
|
|
|
|
rhs: @expr, parent: node_id, ty: oper_type) ->
|
2011-07-27 07:19:39 -05:00
|
|
|
bool {
|
|
|
|
let changed = set_prestate_ann(fcx.ccx, parent, pres);
|
2011-07-09 00:05:30 -05:00
|
|
|
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;
|
2011-09-06 17:26:57 -05:00
|
|
|
forbid_upvar(fcx, rhs.id, rhs.span, ty);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
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 {
|
2012-01-19 00:37:22 -06:00
|
|
|
oper_move {
|
2011-07-27 07:19:39 -05:00
|
|
|
if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
|
|
|
|
forget_in_poststate_still_init(fcx, post, lhs.id);
|
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
oper_swap {
|
2011-07-27 07:19:39 -05:00
|
|
|
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 =
|
2012-01-14 18:05:07 -06:00
|
|
|
{ident: path_to_ident(p), node: id};
|
2011-07-27 07:19:39 -05:00
|
|
|
let instrhs =
|
2012-01-14 18:05:07 -06:00
|
|
|
{ident: path_to_ident(p1), node: id1};
|
2011-07-27 07:19:39 -05:00
|
|
|
copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
|
|
|
|
ty);
|
|
|
|
}
|
|
|
|
_ { }
|
2011-07-09 00:05:30 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { }
|
2011-07-09 00:05:30 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ {/* do nothing */ }
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { }
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
|
|
|
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_call(fcx: fn_ctxt, pres: prestate, a: @expr,
|
|
|
|
id: node_id, ops: [init_op], bs: [@expr],
|
2011-09-14 03:38:23 -05:00
|
|
|
cf: ret_style) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed = find_pre_post_state_expr(fcx, pres, a);
|
2011-08-17 18:58:00 -05:00
|
|
|
// FIXME: This could be a typestate constraint
|
2011-08-15 18:38:23 -05:00
|
|
|
if vec::len(bs) != vec::len(ops) {
|
2011-08-28 02:24:28 -05:00
|
|
|
fcx.ccx.tcx.sess.span_bug(a.span,
|
2011-09-01 20:49:10 -05:00
|
|
|
#fmt["mismatched arg lengths: \
|
2011-08-08 21:38:19 -05:00
|
|
|
%u exprs vs. %u ops",
|
2011-08-28 02:24:28 -05:00
|
|
|
vec::len(bs), vec::len(ops)]);
|
2011-08-08 21:38:19 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
ret find_pre_post_state_exprs(fcx, expr_poststate(fcx.ccx, a), id, ops,
|
|
|
|
bs, cf) || changed;
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id,
|
2011-09-14 03:38:23 -05:00
|
|
|
ops: [init_op], es: [@expr], cf: ret_style) ->
|
2011-09-12 04:27:30 -05:00
|
|
|
bool {
|
2011-08-08 21:38:19 -05:00
|
|
|
let rs = seq_states(fcx, pres, anon_bindings(ops, es));
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed = rs.changed | set_prestate_ann(fcx.ccx, id, pres);
|
2011-06-25 00:17:17 -05:00
|
|
|
/* if this is a failing call, it sets everything as initialized */
|
2011-07-27 07:19:39 -05:00
|
|
|
alt cf {
|
2012-01-19 00:37:22 -06:00
|
|
|
noreturn {
|
2011-08-01 22:55:04 -05:00
|
|
|
let post = false_postcond(num_constraints(fcx.enclosing));
|
2012-01-20 19:23:56 -06:00
|
|
|
handle_fail(fcx, pres, post);
|
2011-08-01 22:55:04 -05:00
|
|
|
changed |= set_poststate_ann(fcx.ccx, id, post);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local,
|
|
|
|
index: @expr, body: blk, id: node_id) -> bool {
|
2012-01-30 23:00:57 -06:00
|
|
|
// I'm confused about this -- how does the poststate for the body
|
|
|
|
// ever grow larger? It seems like it can't?
|
2011-07-27 07:19:39 -05:00
|
|
|
let loop_pres = intersect_states(pres, block_poststate(fcx.ccx, body));
|
2011-06-15 13:19:50 -05:00
|
|
|
|
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);
|
2011-07-12 13:26:14 -05:00
|
|
|
|
2011-07-28 05:01:45 -05:00
|
|
|
// Make sure the index vars are considered initialized
|
2011-07-12 13:26:14 -05:00
|
|
|
// in the body
|
2011-07-27 07:19:39 -05:00
|
|
|
let index_post = tritv_clone(expr_poststate(fcx.ccx, index));
|
2012-01-30 23:00:57 -06:00
|
|
|
pat_bindings(pat_util::normalize_pat(fcx.ccx.tcx, l.node.pat))
|
|
|
|
{|p_id, _s, n|
|
|
|
|
set_in_poststate_ident(fcx, p_id, path_to_ident(n), index_post);
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-07-12 13:26:14 -05:00
|
|
|
|
|
|
|
changed |= find_pre_post_state_block(fcx, index_post, body);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
if has_nonlocal_exits(body) {
|
2011-06-27 20:12:37 -05:00
|
|
|
// 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));
|
2011-06-27 20:12:37 -05:00
|
|
|
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn gen_if_local(fcx: fn_ctxt, p: poststate, e: @expr) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt e.node {
|
|
|
|
expr_path(pth) {
|
2011-09-01 07:35:00 -05:00
|
|
|
alt fcx.ccx.tcx.def_map.find(e.id) {
|
2012-02-10 07:33:36 -06:00
|
|
|
some(def_local(loc)) {
|
2011-07-27 07:19:39 -05:00
|
|
|
ret set_in_poststate_ident(fcx, loc.node,
|
2012-01-14 18:05:07 -06:00
|
|
|
path_to_ident(pth), p);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { ret false; }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
_ { ret false; }
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
|
2012-01-31 19:05:20 -06:00
|
|
|
maybe_alt: option<@expr>, id: node_id, chk: if_ty,
|
2011-09-12 04:27:30 -05:00
|
|
|
pres: prestate) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed =
|
|
|
|
set_prestate_ann(fcx.ccx, id, pres) |
|
|
|
|
find_pre_post_state_expr(fcx, pres, antec);
|
2011-07-13 17:44:09 -05:00
|
|
|
|
2011-06-17 21:07:23 -05:00
|
|
|
/*
|
|
|
|
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 {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {
|
2011-09-02 20:43:50 -05:00
|
|
|
alt chk {
|
2012-01-19 00:37:22 -06:00
|
|
|
if_check {
|
2011-09-02 20:43:50 -05:00
|
|
|
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
|
|
|
|
let conseq_prestate = tritv_clone(expr_poststate(fcx.ccx, antec));
|
|
|
|
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
|
|
|
|
changed |=
|
|
|
|
find_pre_post_state_block(fcx, conseq_prestate, conseq) |
|
2011-09-12 04:27:30 -05:00
|
|
|
set_poststate_ann(fcx.ccx, id,
|
|
|
|
expr_poststate(fcx.ccx, antec));
|
2011-09-02 20:43:50 -05:00
|
|
|
}
|
|
|
|
_ {
|
|
|
|
changed |=
|
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
|
|
|
|
conseq) |
|
2011-09-12 04:27:30 -05:00
|
|
|
set_poststate_ann(fcx.ccx, id,
|
|
|
|
expr_poststate(fcx.ccx, antec));
|
2011-09-02 20:43:50 -05:00
|
|
|
}
|
|
|
|
}
|
2011-09-12 04:27:30 -05:00
|
|
|
}
|
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 {
|
2012-01-19 00:37:22 -06:00
|
|
|
if_check {
|
2011-07-27 07:19:39 -05:00
|
|
|
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);
|
|
|
|
}
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-12-18 22:45:30 -06:00
|
|
|
fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
|
|
|
|
pres: prestate, cap_clause: capture_clause)
|
|
|
|
-> bool
|
|
|
|
{
|
|
|
|
let ccx = fcx.ccx;
|
|
|
|
let pres_changed = set_prestate_ann(ccx, e_id, pres);
|
|
|
|
let post = tritv_clone(pres);
|
|
|
|
vec::iter(cap_clause.moves) { |cap_item|
|
|
|
|
forget_in_poststate(fcx, post, cap_item.id);
|
|
|
|
}
|
|
|
|
ret set_poststate_ann(ccx, e_id, post) || pres_changed;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
|
2011-07-27 07:19:39 -05:00
|
|
|
let num_constrs = num_constraints(fcx.enclosing);
|
|
|
|
|
|
|
|
|
|
|
|
alt e.node {
|
2011-08-18 13:37:19 -05:00
|
|
|
expr_vec(elts, _) {
|
2011-08-08 21:38:19 -05:00
|
|
|
ret find_pre_post_state_exprs(fcx, pres, e.id,
|
2012-01-18 15:02:29 -06:00
|
|
|
vec::init_elt(vec::len(elts),
|
|
|
|
init_assign), elts,
|
2011-09-14 03:38:23 -05:00
|
|
|
return_val);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-10-21 07:11:24 -05:00
|
|
|
expr_call(operator, operands, _) {
|
2011-08-08 21:38:19 -05:00
|
|
|
ret find_pre_post_state_call(fcx, pres, operator, e.id,
|
|
|
|
callee_arg_init_ops(fcx, operator.id),
|
|
|
|
operands,
|
2011-07-27 07:19:39 -05:00
|
|
|
controlflow_expr(fcx.ccx, operator));
|
|
|
|
}
|
|
|
|
expr_bind(operator, maybe_args) {
|
2011-08-19 17:16:48 -05:00
|
|
|
let args = [];
|
2011-08-08 21:38:19 -05:00
|
|
|
let callee_ops = callee_arg_init_ops(fcx, operator.id);
|
2011-08-19 17:16:48 -05:00
|
|
|
let ops = [];
|
2011-08-08 21:38:19 -05:00
|
|
|
let i = 0;
|
2012-01-31 19:05:20 -06:00
|
|
|
for a_opt: option<@expr> in maybe_args {
|
2011-08-08 21:38:19 -05:00
|
|
|
alt a_opt {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* no-op */ }
|
2011-08-19 17:16:48 -05:00
|
|
|
some(a) { ops += [callee_ops[i]]; args += [a]; }
|
2011-08-08 21:38:19 -05:00
|
|
|
}
|
|
|
|
i += 1;
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-08-08 21:38:19 -05:00
|
|
|
ret find_pre_post_state_call(fcx, pres, operator, e.id, ops, args,
|
2011-09-14 03:38:23 -05:00
|
|
|
return_val);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
expr_path(_) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-12-21 16:31:31 -06:00
|
|
|
expr_log(_, lvl, ex) {
|
|
|
|
ret find_pre_post_state_two(fcx, pres, lvl, ex, e.id, oper_pure);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-09-02 17:34:58 -05:00
|
|
|
expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_lit(l) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-12-29 22:07:55 -06:00
|
|
|
expr_fn(_, _, _, cap_clause) {
|
2011-12-18 22:45:30 -06:00
|
|
|
ret find_pre_post_state_cap_clause(fcx, e.id, pres, *cap_clause);
|
|
|
|
}
|
2011-12-20 13:03:21 -06:00
|
|
|
expr_fn_block(_, _) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_block(b) {
|
|
|
|
ret find_pre_post_state_block(fcx, pres, b) |
|
2011-06-25 10:29:50 -05:00
|
|
|
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) {
|
2012-01-19 19:22:41 -06:00
|
|
|
let exs = field_exprs(fields);
|
2011-07-27 07:19:39 -05:00
|
|
|
let changed =
|
2011-08-08 21:38:19 -05:00
|
|
|
find_pre_post_state_exprs(fcx, pres, e.id,
|
2012-01-18 15:02:29 -06:00
|
|
|
vec::init_elt(vec::len(fields),
|
|
|
|
init_assign),
|
2012-01-19 19:22:41 -06:00
|
|
|
exs, return_val);
|
|
|
|
|
|
|
|
let base_pres = alt vec::last(exs) { none { pres }
|
|
|
|
some(f) { expr_poststate(fcx.ccx, f) }};
|
|
|
|
option::may(maybe_base, {|base|
|
|
|
|
changed |= find_pre_post_state_expr(fcx, base_pres, base) |
|
|
|
|
set_poststate_ann(fcx.ccx, e.id,
|
|
|
|
expr_poststate(fcx.ccx, base))});
|
2011-07-27 07:19:39 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
2011-08-15 04:40:26 -05:00
|
|
|
expr_tup(elts) {
|
|
|
|
ret find_pre_post_state_exprs(fcx, pres, e.id,
|
2012-01-18 15:02:29 -06:00
|
|
|
vec::init_elt(vec::len(elts),
|
|
|
|
init_assign), elts,
|
2011-09-14 03:38:23 -05:00
|
|
|
return_val);
|
2011-08-15 17:35:40 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
expr_copy(a) { ret find_pre_post_state_sub(fcx, pres, a, e.id, none); }
|
2011-07-27 07:19:39 -05:00
|
|
|
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_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 */
|
2011-08-19 17:16:48 -05:00
|
|
|
// FIXME should factor this out
|
2011-08-01 22:55:04 -05:00
|
|
|
let post = false_postcond(num_constrs);
|
|
|
|
// except for the "diverges" bit...
|
|
|
|
kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
2011-08-01 22:55:04 -05:00
|
|
|
set_poststate_ann(fcx.ccx, e.id, post);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
alt maybe_ret_val {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* do nothing */ }
|
2011-07-27 07:19:39 -05:00
|
|
|
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);
|
2011-08-01 22:55:04 -05:00
|
|
|
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);
|
2011-07-27 07:19:39 -05:00
|
|
|
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_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 {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
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) {
|
|
|
|
/*
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("in a while loop:");
|
2011-07-27 07:19:39 -05:00
|
|
|
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);
|
2011-12-22 16:42:52 -06:00
|
|
|
// #error("---------------");
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
let changed =
|
|
|
|
set_prestate_ann(fcx.ccx, e.id, loop_pres) |
|
2011-06-27 20:12:37 -05:00
|
|
|
find_pre_post_state_expr(fcx, loop_pres, test) |
|
2011-06-15 13:19:50 -05:00
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
|
2011-06-25 10:29:50 -05:00
|
|
|
body);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
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_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;
|
2011-08-15 18:38:23 -05:00
|
|
|
if vec::len(alts) > 0u {
|
2011-07-27 07:19:39 -05:00
|
|
|
a_post = false_postcond(num_constrs);
|
2011-08-15 23:54:52 -05:00
|
|
|
for an_alt: arm in alts {
|
2011-12-07 07:09:45 -06:00
|
|
|
alt an_alt.guard {
|
|
|
|
some(e) {
|
|
|
|
changed |= find_pre_post_state_expr(fcx, e_post, e);
|
|
|
|
}
|
|
|
|
_ {}
|
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
changed |=
|
2011-08-10 17:38:41 -05:00
|
|
|
find_pre_post_state_block(fcx, e_post, an_alt.body);
|
|
|
|
intersect(a_post, block_poststate(fcx.ccx, an_alt.body));
|
2011-07-27 07:19:39 -05:00
|
|
|
// 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-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
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);
|
|
|
|
}
|
2011-12-19 03:21:31 -06:00
|
|
|
expr_field(val, _, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
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) {
|
2011-08-01 22:55:04 -05:00
|
|
|
// 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);
|
2012-01-20 19:23:56 -06:00
|
|
|
handle_fail(fcx, pres, post);
|
2011-07-27 07:19:39 -05:00
|
|
|
ret set_prestate_ann(fcx.ccx, e.id, pres) |
|
2011-08-19 17:16:48 -05:00
|
|
|
set_poststate_ann(fcx.ccx, e.id, post) |
|
2012-01-19 19:22:41 -06:00
|
|
|
option::maybe(false, maybe_fail_val, {|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);
|
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
expr_break { ret pure_exp(fcx.ccx, e.id, pres); }
|
|
|
|
expr_cont { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-05-20 19:41:36 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -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);
|
2011-08-17 18:58:00 -05:00
|
|
|
|
2012-01-19 19:22:41 -06:00
|
|
|
log(debug, "[" + fcx.name + "]");
|
|
|
|
#debug("*At beginning: stmt = ");
|
|
|
|
log_stmt(*s);
|
|
|
|
#debug("*prestate = ");
|
|
|
|
log(debug, tritv::to_str(stmt_ann.states.prestate));
|
|
|
|
#debug("*poststate =");
|
|
|
|
log(debug, tritv::to_str(stmt_ann.states.prestate));
|
2012-01-19 19:49:23 -06:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
alt s.node {
|
2011-07-27 07:19:39 -05:00
|
|
|
stmt_decl(adecl, id) {
|
2011-08-19 17:16:48 -05:00
|
|
|
alt adecl.node {
|
2011-07-27 07:19:39 -05:00
|
|
|
decl_local(alocals) {
|
2011-07-29 17:59:38 -05:00
|
|
|
set_prestate(stmt_ann, pres);
|
2012-01-14 18:05:07 -06:00
|
|
|
let c_and_p = seq_states(fcx, pres,
|
|
|
|
locals_to_bindings(fcx.ccx.tcx, alocals));
|
2011-07-29 17:59:38 -05:00
|
|
|
/* important to do this in one step to ensure
|
|
|
|
termination (don't want to set changed to true
|
|
|
|
for intermediate changes) */
|
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
let changed =
|
|
|
|
set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed;
|
2011-08-05 17:23:44 -05:00
|
|
|
|
2012-01-19 19:22:41 -06:00
|
|
|
#debug("Summary: stmt = ");
|
|
|
|
log_stmt(*s);
|
|
|
|
#debug("prestate = ");
|
|
|
|
log(debug, tritv::to_str(stmt_ann.states.prestate));
|
|
|
|
#debug("poststate =");
|
|
|
|
log(debug, tritv::to_str(stmt_ann.states.prestate));
|
|
|
|
#debug("changed =");
|
|
|
|
log(debug, changed);
|
2011-07-29 17:59:38 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
decl_item(an_item) {
|
2011-08-19 17:16:48 -05:00
|
|
|
ret set_prestate(stmt_ann, pres) | set_poststate(stmt_ann, pres);
|
2011-07-29 17:59:38 -05:00
|
|
|
/* the outer visitor will recurse into the item */
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2012-01-04 16:16:41 -06:00
|
|
|
stmt_expr(ex, _) | stmt_semi(ex, _) {
|
2011-08-19 17:16:48 -05:00
|
|
|
let changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, ex) |
|
2011-06-25 10:29:50 -05:00
|
|
|
set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) |
|
|
|
|
set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex));
|
2011-08-05 17:23:44 -05:00
|
|
|
|
2012-01-19 19:22:41 -06:00
|
|
|
|
|
|
|
#debug("Finally:");
|
|
|
|
log_stmt(*s);
|
|
|
|
log(debug, "prestate = ");
|
|
|
|
log(debug, tritv::to_str(stmt_ann.states.prestate));
|
|
|
|
#debug("poststate =");
|
|
|
|
log(debug, (tritv::to_str(stmt_ann.states.poststate)));
|
|
|
|
#debug("changed =");
|
2011-08-05 17:23:44 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
ret changed;
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { ret false; }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Updates the pre- and post-states of statements in the block,
|
|
|
|
returns a boolean flag saying whether any pre- or poststates changed */
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_state_block(fcx: fn_ctxt, pres0: prestate, b: blk) -> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
/* First, set the pre-states and post-states for every expression */
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
let pres = pres0;
|
2011-06-15 13:19:50 -05:00
|
|
|
/* 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;
|
2011-08-15 23:54:52 -05:00
|
|
|
for s: @stmt in b.node.stmts {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_stmt(fcx, pres, s);
|
2011-06-15 13:19:50 -05:00
|
|
|
pres = stmt_poststate(fcx.ccx, *s);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
let post = pres;
|
|
|
|
alt b.node.expr {
|
2012-01-19 00:37:22 -06:00
|
|
|
none { }
|
2011-07-27 07:19:39 -05:00
|
|
|
some(e) {
|
|
|
|
changed |= find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
post = expr_poststate(fcx.ccx, e);
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-19 15:41:21 -05:00
|
|
|
set_prestate_ann(fcx.ccx, b.node.id, pres0);
|
|
|
|
set_poststate_ann(fcx.ccx, b.node.id, post);
|
2011-06-25 00:17:17 -05:00
|
|
|
|
2011-07-29 17:59:38 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
/*
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("For block:");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_block_err(b);
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("poststate = ");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_states_err(block_states(fcx.ccx, b));
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("pres0:");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_tritv_err(fcx, pres0);
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("post:");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_tritv_err(fcx, post);
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("changed = ");
|
2011-12-22 19:53:53 -06:00
|
|
|
log(error, changed);
|
2011-08-19 17:16:48 -05:00
|
|
|
*/
|
2011-06-15 13:19:50 -05:00
|
|
|
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-12-20 13:03:21 -06:00
|
|
|
fn find_pre_post_state_fn(fcx: fn_ctxt,
|
|
|
|
f_decl: fn_decl,
|
|
|
|
f_body: blk) -> bool {
|
2011-08-01 22:55:04 -05:00
|
|
|
let num_constrs = num_constraints(fcx.enclosing);
|
2011-08-05 17:23:44 -05:00
|
|
|
// All constraints are considered false until proven otherwise.
|
|
|
|
// This ensures that intersect works correctly.
|
2011-12-20 13:03:21 -06:00
|
|
|
kill_all_prestate(fcx, f_body.node.id);
|
2011-08-01 22:55:04 -05:00
|
|
|
|
2011-08-17 18:58:00 -05:00
|
|
|
// Arguments start out initialized
|
2011-12-20 13:03:21 -06:00
|
|
|
let block_pre = block_prestate(fcx.ccx, f_body);
|
|
|
|
for a: arg in f_decl.inputs {
|
2011-08-17 18:58:00 -05:00
|
|
|
set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre);
|
|
|
|
}
|
|
|
|
|
|
|
|
// Instantiate any constraints on the arguments so we can use them
|
2011-12-20 13:03:21 -06:00
|
|
|
for c: @constr in f_decl.constraints {
|
|
|
|
let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c);
|
2011-07-21 18:03:30 -05:00
|
|
|
set_in_prestate_constr(fcx, tsc, block_pre);
|
|
|
|
}
|
|
|
|
|
2011-12-20 13:03:21 -06:00
|
|
|
let changed = find_pre_post_state_block(fcx, block_pre, f_body);
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-08-30 14:45:12 -05:00
|
|
|
// Treat the tail expression as a return statement
|
2011-12-20 13:03:21 -06:00
|
|
|
alt f_body.node.expr {
|
2011-07-27 07:19:39 -05:00
|
|
|
some(tailexpr) {
|
2011-09-02 17:34:58 -05:00
|
|
|
|
2011-08-30 14:45:12 -05:00
|
|
|
// 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.
|
2012-02-03 08:15:28 -06:00
|
|
|
if !type_is_bot(expr_ty(fcx.ccx.tcx, tailexpr)) {
|
2011-08-01 22:55:04 -05:00
|
|
|
let post = false_postcond(num_constrs);
|
|
|
|
// except for the "diverges" bit...
|
|
|
|
kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
|
2011-12-20 13:03:21 -06:00
|
|
|
set_poststate_ann(fcx.ccx, f_body.node.id, post);
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* fallthrough */ }
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
2011-06-27 20:12:37 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
/*
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("find_pre_post_state_fn");
|
2011-12-22 19:53:53 -06:00
|
|
|
log(error, changed);
|
2011-12-20 13:03:21 -06:00
|
|
|
fcx.ccx.tcx.sess.span_note(f_body.span, fcx.name);
|
2011-07-27 07:19:39 -05:00
|
|
|
*/
|
2011-06-27 20:12:37 -05:00
|
|
|
|
2011-05-31 14:24:18 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-18 17:43:05 -05:00
|
|
|
//
|
|
|
|
// Local Variables:
|
|
|
|
// mode: rust
|
|
|
|
// fill-column: 78;
|
|
|
|
// indent-tabs-mode: nil
|
|
|
|
// c-basic-offset: 4
|
|
|
|
// buffer-file-coding-system: utf-8-unix
|
|
|
|
// End:
|
|
|
|
//
|