2011-06-15 13:19:50 -05:00
|
|
|
|
2011-12-13 18:25:51 -06:00
|
|
|
import core::{vec, option};
|
|
|
|
import option::{none, some};
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-08-18 19:17:50 -05:00
|
|
|
import tstate::ann::*;
|
2011-07-09 00:05:30 -05:00
|
|
|
import aux::*;
|
2011-11-10 10:41:42 -06:00
|
|
|
import bitvectors::{bit_num, seq_preconds, seq_postconds,
|
|
|
|
intersect_states,
|
2011-09-12 18:13:28 -05:00
|
|
|
relax_precond_block, gen};
|
2011-08-18 19:17:50 -05:00
|
|
|
import tritv::*;
|
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-07-12 13:26:14 -05:00
|
|
|
import syntax::visit;
|
2011-11-10 10:41:42 -06:00
|
|
|
import util::common::{new_def_hash, log_expr, field_exprs,
|
|
|
|
has_nonlocal_exits, log_stmt};
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::codemap::span;
|
2012-01-12 10:59:49 -06:00
|
|
|
import driver::session::session;
|
2011-05-26 18:02:25 -05:00
|
|
|
|
2012-01-14 18:05:07 -06:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_mod(_m: _mod) -> _mod {
|
2011-12-22 16:42:52 -06:00
|
|
|
#debug("implement find_pre_post_mod!");
|
2011-05-14 21:02:30 -05:00
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_native_mod(_m: native_mod) -> native_mod {
|
2011-12-22 16:42:52 -06:00
|
|
|
#debug("implement find_pre_post_native_mod");
|
2011-05-14 21:02:30 -05:00
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
2011-12-13 06:19:56 -06:00
|
|
|
fn find_pre_post_method(ccx: crate_ctxt, m: @method) {
|
2011-12-22 10:49:54 -06:00
|
|
|
assert (ccx.fm.contains_key(m.id));
|
2011-12-13 06:19:56 -06:00
|
|
|
let fcx: fn_ctxt =
|
2011-12-22 10:49:54 -06:00
|
|
|
{enclosing: ccx.fm.get(m.id),
|
|
|
|
id: m.id,
|
|
|
|
name: m.ident,
|
2011-12-13 06:19:56 -06:00
|
|
|
ccx: ccx};
|
2011-12-22 10:49:54 -06:00
|
|
|
find_pre_post_fn(fcx, m.body);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_item(ccx: crate_ctxt, i: item) {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt i.node {
|
|
|
|
item_const(_, e) {
|
|
|
|
// make a fake fcx
|
2011-08-19 17:16:48 -05:00
|
|
|
let v: @mutable [node_id] = @mutable [];
|
2011-07-27 07:19:39 -05:00
|
|
|
let fake_fcx =
|
2011-08-19 17:16:48 -05:00
|
|
|
{
|
|
|
|
// just bogus
|
|
|
|
enclosing:
|
2012-01-09 09:24:53 -06:00
|
|
|
{constrs: new_def_hash::<constraint>(),
|
2011-07-27 07:19:39 -05:00
|
|
|
num_constraints: 0u,
|
2011-09-14 03:38:23 -05:00
|
|
|
cf: return_val,
|
2011-09-02 17:34:58 -05:00
|
|
|
i_return: ninit(0, ""),
|
|
|
|
i_diverge: ninit(0, ""),
|
2011-07-27 07:19:39 -05:00
|
|
|
used_vars: v},
|
|
|
|
id: 0,
|
2011-09-02 17:34:58 -05:00
|
|
|
name: "",
|
2011-07-27 07:19:39 -05:00
|
|
|
ccx: ccx};
|
|
|
|
find_pre_post_expr(fake_fcx, e);
|
|
|
|
}
|
2011-12-22 10:49:54 -06:00
|
|
|
item_fn(_, _, body) {
|
2011-07-27 07:19:39 -05:00
|
|
|
assert (ccx.fm.contains_key(i.id));
|
|
|
|
let fcx =
|
|
|
|
{enclosing: ccx.fm.get(i.id), id: i.id, name: i.ident, ccx: ccx};
|
2011-12-22 10:49:54 -06:00
|
|
|
find_pre_post_fn(fcx, body);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
item_mod(m) { find_pre_post_mod(m); }
|
|
|
|
item_native_mod(nm) { find_pre_post_native_mod(nm); }
|
2012-01-25 07:34:31 -06:00
|
|
|
item_ty(_, _) | item_enum(_, _) | item_iface(_, _) { ret; }
|
2011-12-22 10:49:54 -06:00
|
|
|
item_res(_, _, body, dtor_id, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let fcx =
|
|
|
|
{enclosing: ccx.fm.get(dtor_id),
|
|
|
|
id: dtor_id,
|
|
|
|
name: i.ident,
|
|
|
|
ccx: ccx};
|
2011-12-22 10:49:54 -06:00
|
|
|
find_pre_post_fn(fcx, body);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-12-20 09:33:55 -06:00
|
|
|
item_impl(_, _, _, ms) { for m in ms { find_pre_post_method(ccx, m); } }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Finds the pre and postcondition for each expr in <args>;
|
|
|
|
sets the precondition in a to be the result of combining
|
2011-07-13 17:44:09 -05:00
|
|
|
the preconditions for <args>, and the postcondition in a to
|
2011-05-14 21:02:30 -05:00
|
|
|
be the union of all postconditions for <args> */
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_exprs(fcx: fn_ctxt, args: [@expr], id: node_id) {
|
2011-08-13 02:09:25 -05:00
|
|
|
if vec::len::<@expr>(args) > 0u {
|
2011-12-22 16:42:52 -06:00
|
|
|
#debug("find_pre_post_exprs: oper =");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_expr(*args[0]);
|
2011-05-18 17:43:05 -05:00
|
|
|
}
|
2011-09-12 04:27:30 -05:00
|
|
|
fn do_one(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
|
2011-08-15 23:54:52 -05:00
|
|
|
for e: @expr in args { do_one(fcx, e); }
|
2011-07-06 21:00:00 -05:00
|
|
|
|
2011-10-07 02:36:53 -05:00
|
|
|
fn get_pp(ccx: crate_ctxt, &&e: @expr) -> pre_and_post {
|
2011-05-18 17:43:05 -05:00
|
|
|
ret expr_pp(ccx, e);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-12-16 08:27:50 -06:00
|
|
|
let pps = vec::map(args, bind get_pp(fcx.ccx, _));
|
2011-07-05 01:29:15 -05:00
|
|
|
|
2011-07-06 21:00:00 -05:00
|
|
|
set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
|
2011-12-16 08:27:50 -06:00
|
|
|
seq_postconds(fcx, vec::map(pps, get_post)));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_loop(fcx: fn_ctxt, l: @local, index: @expr, body: blk,
|
2011-07-27 07:19:39 -05:00
|
|
|
id: node_id) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, index);
|
|
|
|
find_pre_post_block(fcx, body);
|
2012-01-14 18:05:07 -06:00
|
|
|
pat_bindings(normalize_pat(fcx.ccx.tcx, l.node.pat)) {|p|
|
|
|
|
let ident = alt p.node
|
|
|
|
{ pat_ident(id, _) { path_to_ident(id) } };
|
2011-07-28 05:01:45 -05:00
|
|
|
let v_init = ninit(p.id, ident);
|
|
|
|
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);
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
let loop_precond =
|
2011-08-19 17:16:48 -05:00
|
|
|
seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
let loop_postcond =
|
|
|
|
intersect_states(expr_postcond(fcx.ccx, index),
|
|
|
|
block_postcond(fcx.ccx, body));
|
2011-06-19 15:41:21 -05:00
|
|
|
copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-07-13 17:44:09 -05:00
|
|
|
// Generates a pre/post assuming that a is the
|
2011-06-16 13:56:34 -05:00
|
|
|
// annotation for an if-expression with consequent conseq
|
|
|
|
// and alternative maybe_alt
|
2011-09-12 04:27:30 -05:00
|
|
|
fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
|
|
|
|
maybe_alt: option::t<@expr>, id: node_id, chck: if_ty) {
|
2011-06-17 21:07:23 -05:00
|
|
|
find_pre_post_expr(fcx, antec);
|
2011-06-16 13:56:34 -05:00
|
|
|
find_pre_post_block(fcx, conseq);
|
2011-07-27 07:19:39 -05:00
|
|
|
alt maybe_alt {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt chck {
|
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);
|
|
|
|
gen(fcx, antec.id, c.node);
|
|
|
|
}
|
|
|
|
_ { }
|
|
|
|
}
|
|
|
|
|
|
|
|
let precond_res =
|
|
|
|
seq_preconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_pp(fcx.ccx, antec),
|
|
|
|
block_pp(fcx.ccx, conseq)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
set_pre_and_post(fcx.ccx, id, precond_res,
|
|
|
|
expr_poststate(fcx.ccx, antec));
|
|
|
|
}
|
|
|
|
some(altern) {
|
|
|
|
/*
|
|
|
|
if check = if_check, then
|
|
|
|
be sure that the predicate implied by antec
|
|
|
|
is *not* true in the alternative
|
|
|
|
*/
|
|
|
|
find_pre_post_expr(fcx, altern);
|
|
|
|
let precond_false_case =
|
|
|
|
seq_preconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
let postcond_false_case =
|
|
|
|
seq_postconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_postcond(fcx.ccx, antec),
|
|
|
|
expr_postcond(fcx.ccx, altern)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
/* Be sure to set the bit for the check condition here,
|
|
|
|
so that it's *not* set in the alternative. */
|
|
|
|
alt chck {
|
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);
|
|
|
|
gen(fcx, antec.id, c.node);
|
|
|
|
}
|
|
|
|
_ { }
|
|
|
|
}
|
|
|
|
let precond_true_case =
|
|
|
|
seq_preconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_pp(fcx.ccx, antec),
|
|
|
|
block_pp(fcx.ccx, conseq)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
let postcond_true_case =
|
|
|
|
seq_postconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_postcond(fcx.ccx, antec),
|
|
|
|
block_postcond(fcx.ccx, conseq)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
let precond_res =
|
2011-08-19 17:16:48 -05:00
|
|
|
seq_postconds(fcx, [precond_true_case, precond_false_case]);
|
2011-07-27 07:19:39 -05:00
|
|
|
let postcond_res =
|
|
|
|
intersect_states(postcond_true_case, postcond_false_case);
|
|
|
|
set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
|
|
|
|
}
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id,
|
2011-11-30 06:38:38 -06:00
|
|
|
new_var: node_id, pth: @path) {
|
2011-09-01 07:35:00 -05:00
|
|
|
alt node_id_to_def(fcx.ccx, new_var) {
|
2011-07-27 07:19:39 -05:00
|
|
|
some(d) {
|
|
|
|
alt d {
|
2011-09-15 07:08:54 -05:00
|
|
|
def_local(d_id, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
find_pre_post_expr(fcx, rhs);
|
|
|
|
let p = expr_pp(fcx.ccx, rhs);
|
|
|
|
set_pre_and_post(fcx.ccx, larger_id, p.precondition,
|
|
|
|
p.postcondition);
|
|
|
|
gen(fcx, larger_id,
|
2012-01-14 18:05:07 -06:00
|
|
|
ninit(d_id.node, path_to_ident(pth)));
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
_ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); }
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
_ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); }
|
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 handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
|
2011-07-27 07:19:39 -05:00
|
|
|
ty: oper_type) {
|
2011-07-09 00:05:30 -05:00
|
|
|
find_pre_post_expr(fcx, rhs);
|
2011-07-27 07:19:39 -05:00
|
|
|
alt lhs.node {
|
|
|
|
expr_path(p) {
|
|
|
|
let post = expr_postcond(fcx.ccx, parent);
|
|
|
|
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_postcond(fcx, parent.id, rhs.id); }
|
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
oper_swap {
|
2011-07-27 07:19:39 -05:00
|
|
|
forget_in_postcond_still_init(fcx, parent.id, lhs.id);
|
|
|
|
forget_in_postcond_still_init(fcx, parent.id, rhs.id);
|
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
oper_assign {
|
2011-07-27 07:19:39 -05:00
|
|
|
forget_in_postcond_still_init(fcx, parent.id, lhs.id);
|
|
|
|
}
|
|
|
|
_ {
|
|
|
|
// pure and assign_op require the lhs to be init'd
|
2011-09-01 07:35:00 -05:00
|
|
|
let df = node_id_to_def_strict(fcx.ccx.tcx, lhs.id);
|
2011-07-27 07:19:39 -05:00
|
|
|
alt df {
|
2011-09-15 07:08:54 -05:00
|
|
|
def_local(d_id, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let i =
|
|
|
|
bit_num(fcx,
|
2012-01-14 18:05:07 -06:00
|
|
|
ninit(d_id.node, path_to_ident(p)));
|
2011-07-27 07:19:39 -05:00
|
|
|
require_and_preserve(i, expr_pp(fcx.ccx, lhs));
|
|
|
|
}
|
|
|
|
_ { }
|
2011-07-09 00:05:30 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p);
|
|
|
|
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-07-09 00:05:30 -05:00
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
_ { find_pre_post_expr(fcx, lhs); }
|
2011-07-09 00:05:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn handle_var(fcx: fn_ctxt, rslt: pre_and_post, id: node_id, name: ident) {
|
2011-09-01 07:35:00 -05:00
|
|
|
handle_var_def(fcx, rslt, node_id_to_def_strict(fcx.ccx.tcx, id), name);
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn handle_var_def(fcx: fn_ctxt, rslt: pre_and_post, def: def, name: ident) {
|
2011-12-22 19:53:53 -06:00
|
|
|
log(debug, ("handle_var_def: ", def, name));
|
2011-09-01 07:35:00 -05:00
|
|
|
alt def {
|
2011-09-15 07:08:54 -05:00
|
|
|
def_local(d_id, _) | def_arg(d_id, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
use_var(fcx, d_id.node);
|
2011-09-01 07:35:00 -05:00
|
|
|
let i = bit_num(fcx, ninit(d_id.node, name));
|
2011-07-27 07:19:39 -05:00
|
|
|
require_and_preserve(i, rslt);
|
|
|
|
}
|
|
|
|
_ {/* nothing to check */ }
|
2011-07-22 20:04:40 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [ty::mode],
|
|
|
|
operands: [@expr]) {
|
2011-08-17 18:58:00 -05:00
|
|
|
let i = 0u;
|
2011-08-08 21:38:19 -05:00
|
|
|
for mode: ty::mode in modes {
|
2011-09-12 03:05:40 -05:00
|
|
|
if mode == by_move {
|
2011-08-19 17:16:48 -05:00
|
|
|
forget_in_postcond(fcx, parent.id, operands[i].id);
|
2011-08-08 21:38:19 -05:00
|
|
|
}
|
2011-08-17 18:58:00 -05:00
|
|
|
i += 1u;
|
2011-08-08 21:38:19 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-12-20 13:03:21 -06:00
|
|
|
fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) {
|
|
|
|
let rslt = expr_pp(fcx.ccx, e);
|
|
|
|
clear_pp(rslt);
|
|
|
|
for def in *freevars::get_freevars(fcx.ccx.tcx, e.id) {
|
2011-12-22 19:53:53 -06:00
|
|
|
log(debug, ("handle_var_def: def=", def));
|
2011-12-20 13:03:21 -06:00
|
|
|
handle_var_def(fcx, rslt, def.def, "upvar");
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let enclosing = fcx.enclosing;
|
|
|
|
let num_local_vars = num_constraints(enclosing);
|
2011-09-12 04:27:30 -05:00
|
|
|
fn do_rand_(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
|
|
|
|
alt e.node {
|
2011-10-21 07:11:24 -05:00
|
|
|
expr_call(operator, operands, _) {
|
2011-08-19 17:16:48 -05:00
|
|
|
/* copy */
|
|
|
|
|
|
|
|
let args = operands;
|
|
|
|
args += [operator];
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
|
|
|
/* see if the call has any constraints on its type */
|
2011-08-15 23:54:52 -05:00
|
|
|
for c: @ty::constr in constraints_expr(fcx.ccx.tcx, operator) {
|
2011-07-27 07:19:39 -05:00
|
|
|
let i =
|
|
|
|
bit_num(fcx, substitute_constr_args(fcx.ccx.tcx, args, c));
|
|
|
|
require(i, expr_pp(fcx.ccx, e));
|
|
|
|
}
|
|
|
|
|
2011-08-08 21:38:19 -05:00
|
|
|
forget_args_moved_in(fcx, e, callee_modes(fcx, operator.id),
|
|
|
|
operands);
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
/* if this is a failing call, its postcondition sets everything */
|
|
|
|
alt controlflow_expr(fcx.ccx, operator) {
|
2012-01-19 00:37:22 -06:00
|
|
|
noreturn { set_postcond_false(fcx.ccx, e.id); }
|
2011-07-27 07:19:39 -05:00
|
|
|
_ { }
|
|
|
|
}
|
|
|
|
}
|
2011-08-18 13:37:19 -05:00
|
|
|
expr_vec(args, _) { find_pre_post_exprs(fcx, args, e.id); }
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_path(p) {
|
|
|
|
let rslt = expr_pp(fcx.ccx, e);
|
|
|
|
clear_pp(rslt);
|
2012-01-14 18:05:07 -06:00
|
|
|
handle_var(fcx, rslt, e.id, path_to_ident(p));
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-12-21 16:31:31 -06:00
|
|
|
expr_log(_, lvl, arg) {
|
|
|
|
find_pre_post_exprs(fcx, [lvl, arg], e.id);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-12-29 22:07:55 -06:00
|
|
|
expr_fn(_, _, _, cap_clause) {
|
2011-12-20 13:03:21 -06:00
|
|
|
find_pre_post_expr_fn_upvars(fcx, e);
|
2011-12-18 22:45:30 -06:00
|
|
|
|
2012-01-09 18:12:37 -06:00
|
|
|
let use_cap_item = fn@(&&cap_item: @capture_item) {
|
2011-12-19 14:50:31 -06:00
|
|
|
let d = local_node_id_to_local_def_id(fcx, cap_item.id);
|
|
|
|
option::may(d, { |id| use_var(fcx, id) });
|
|
|
|
};
|
|
|
|
vec::iter(cap_clause.copies, use_cap_item);
|
|
|
|
vec::iter(cap_clause.moves, use_cap_item);
|
|
|
|
|
2011-12-18 22:45:30 -06:00
|
|
|
vec::iter(cap_clause.moves) { |cap_item|
|
2011-12-22 19:53:53 -06:00
|
|
|
log(debug, ("forget_in_postcond: ", cap_item));
|
2011-12-18 22:45:30 -06:00
|
|
|
forget_in_postcond(fcx, e.id, cap_item.id);
|
|
|
|
}
|
2011-12-20 13:03:21 -06:00
|
|
|
}
|
|
|
|
expr_fn_block(_, _) {
|
|
|
|
find_pre_post_expr_fn_upvars(fcx, e);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
expr_block(b) {
|
|
|
|
find_pre_post_block(fcx, b);
|
|
|
|
let p = block_pp(fcx.ccx, b);
|
|
|
|
set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
|
|
|
|
}
|
|
|
|
expr_rec(fields, maybe_base) {
|
|
|
|
let es = field_exprs(fields);
|
2012-01-19 00:37:22 -06:00
|
|
|
alt maybe_base { none {/* no-op */ } some(b) { es += [b]; } }
|
2011-07-27 07:19:39 -05:00
|
|
|
find_pre_post_exprs(fcx, es, e.id);
|
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
expr_tup(elts) { find_pre_post_exprs(fcx, elts, e.id); }
|
2011-08-15 17:35:40 -05:00
|
|
|
expr_copy(a) {
|
|
|
|
find_pre_post_expr(fcx, a);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, a);
|
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_move(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_move); }
|
|
|
|
expr_swap(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_swap); }
|
|
|
|
expr_assign(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_assign); }
|
|
|
|
expr_assign_op(_, lhs, rhs) {
|
|
|
|
/* Different from expr_assign in that the lhs *must*
|
|
|
|
already be initialized */
|
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
find_pre_post_exprs(fcx, [lhs, rhs], e.id);
|
2011-07-27 07:19:39 -05:00
|
|
|
forget_in_postcond_still_init(fcx, e.id, lhs.id);
|
|
|
|
}
|
|
|
|
expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
expr_ret(maybe_val) {
|
|
|
|
alt maybe_val {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {
|
2011-07-27 07:19:39 -05:00
|
|
|
clear_precond(fcx.ccx, e.id);
|
|
|
|
set_postcond_false(fcx.ccx, e.id);
|
|
|
|
}
|
|
|
|
some(ret_val) {
|
|
|
|
find_pre_post_expr(fcx, ret_val);
|
|
|
|
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
|
|
|
expr_precond(fcx.ccx, ret_val));
|
|
|
|
set_postcond_false(fcx.ccx, e.id);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
expr_be(val) {
|
|
|
|
find_pre_post_expr(fcx, val);
|
|
|
|
set_pre_and_post(fcx.ccx, e.id, expr_prestate(fcx.ccx, val),
|
|
|
|
false_postcond(num_local_vars));
|
|
|
|
}
|
|
|
|
expr_if(antec, conseq, maybe_alt) {
|
|
|
|
join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if);
|
|
|
|
}
|
|
|
|
expr_binary(bop, l, r) {
|
|
|
|
if lazy_binop(bop) {
|
|
|
|
find_pre_post_expr(fcx, l);
|
|
|
|
find_pre_post_expr(fcx, r);
|
|
|
|
let overall_pre =
|
2011-08-19 17:16:48 -05:00
|
|
|
seq_preconds(fcx, [expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id), overall_pre);
|
|
|
|
set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
|
|
|
expr_postcond(fcx.ccx, l));
|
2011-08-19 17:16:48 -05:00
|
|
|
} else { find_pre_post_exprs(fcx, [l, r], e.id); }
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
expr_unary(_, operand) {
|
|
|
|
find_pre_post_expr(fcx, operand);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, operand);
|
|
|
|
}
|
|
|
|
expr_cast(operand, _) {
|
|
|
|
find_pre_post_expr(fcx, operand);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, operand);
|
|
|
|
}
|
|
|
|
expr_while(test, body) {
|
|
|
|
find_pre_post_expr(fcx, test);
|
|
|
|
find_pre_post_block(fcx, body);
|
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
|
|
|
seq_preconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[expr_pp(fcx.ccx, test),
|
|
|
|
block_pp(fcx.ccx, body)]),
|
2011-07-27 07:19:39 -05:00
|
|
|
intersect_states(expr_postcond(fcx.ccx, test),
|
|
|
|
block_postcond(fcx.ccx, body)));
|
|
|
|
}
|
|
|
|
expr_do_while(body, test) {
|
|
|
|
find_pre_post_block(fcx, body);
|
|
|
|
find_pre_post_expr(fcx, test);
|
|
|
|
let loop_postcond =
|
|
|
|
seq_postconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[block_postcond(fcx.ccx, body),
|
|
|
|
expr_postcond(fcx.ccx, test)]);
|
2011-07-27 07:19:39 -05:00
|
|
|
/* conservative approximation: if the body
|
|
|
|
could break or cont, the test may never be executed */
|
|
|
|
|
|
|
|
if has_nonlocal_exits(body) {
|
|
|
|
loop_postcond = empty_poststate(num_local_vars);
|
|
|
|
}
|
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
|
|
|
seq_preconds(fcx,
|
2011-08-19 17:16:48 -05:00
|
|
|
[block_pp(fcx.ccx, body),
|
|
|
|
expr_pp(fcx.ccx, test)]),
|
2011-07-27 07:19:39 -05:00
|
|
|
loop_postcond);
|
|
|
|
}
|
|
|
|
expr_for(d, index, body) {
|
|
|
|
find_pre_post_loop(fcx, d, index, body, e.id);
|
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
expr_index(val, sub) { find_pre_post_exprs(fcx, [val, sub], e.id); }
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_alt(ex, alts) {
|
|
|
|
find_pre_post_expr(fcx, ex);
|
2011-09-12 04:27:30 -05:00
|
|
|
fn do_an_alt(fcx: fn_ctxt, an_alt: arm) -> pre_and_post {
|
2011-12-07 07:09:45 -06:00
|
|
|
alt an_alt.guard {
|
|
|
|
some(e) { find_pre_post_expr(fcx, e); }
|
|
|
|
_ {}
|
|
|
|
}
|
2011-08-10 17:38:41 -05:00
|
|
|
find_pre_post_block(fcx, an_alt.body);
|
|
|
|
ret block_pp(fcx.ccx, an_alt.body);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
let alt_pps = [];
|
|
|
|
for a: arm in alts { alt_pps += [do_an_alt(fcx, a)]; }
|
2011-10-06 05:26:12 -05:00
|
|
|
fn combine_pp(antec: pre_and_post, fcx: fn_ctxt, &&pp: pre_and_post,
|
|
|
|
&&next: pre_and_post) -> pre_and_post {
|
2011-08-19 17:16:48 -05:00
|
|
|
union(pp.precondition, seq_preconds(fcx, [antec, next]));
|
2011-07-27 07:19:39 -05:00
|
|
|
intersect(pp.postcondition, next.postcondition);
|
|
|
|
ret pp;
|
|
|
|
}
|
|
|
|
let antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
|
|
|
|
let e_pp =
|
|
|
|
@{precondition: empty_prestate(num_local_vars),
|
|
|
|
postcondition: false_postcond(num_local_vars)};
|
|
|
|
let g = bind combine_pp(antec_pp, fcx, _, _);
|
|
|
|
let alts_overall_pp =
|
2011-12-16 08:27:50 -06:00
|
|
|
vec::foldl(e_pp, alt_pps, g);
|
2011-07-27 07:19:39 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id, alts_overall_pp.precondition,
|
|
|
|
alts_overall_pp.postcondition);
|
|
|
|
}
|
2011-12-19 03:21:31 -06:00
|
|
|
expr_field(operator, _, _) {
|
2011-07-27 07:19:39 -05:00
|
|
|
find_pre_post_expr(fcx, operator);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, operator);
|
|
|
|
}
|
|
|
|
expr_fail(maybe_val) {
|
|
|
|
let prestate;
|
|
|
|
alt maybe_val {
|
2012-01-19 00:37:22 -06:00
|
|
|
none { prestate = empty_prestate(num_local_vars); }
|
2011-07-27 07:19:39 -05:00
|
|
|
some(fail_val) {
|
|
|
|
find_pre_post_expr(fcx, fail_val);
|
|
|
|
prestate = expr_precond(fcx.ccx, fail_val);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
|
|
|
/* if execution continues after fail,
|
|
|
|
then everything is true! */
|
|
|
|
prestate, false_postcond(num_local_vars));
|
|
|
|
}
|
|
|
|
expr_assert(p) {
|
|
|
|
find_pre_post_expr(fcx, p);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, p);
|
|
|
|
}
|
|
|
|
expr_check(_, p) {
|
|
|
|
find_pre_post_expr(fcx, p);
|
|
|
|
copy_pre_post(fcx.ccx, e.id, p);
|
|
|
|
/* predicate p holds after this expression executes */
|
|
|
|
|
|
|
|
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
|
|
|
|
gen(fcx, e.id, c.node);
|
|
|
|
}
|
|
|
|
expr_if_check(p, conseq, maybe_alt) {
|
|
|
|
join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check);
|
|
|
|
}
|
|
|
|
|
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
|
2011-09-02 17:34:58 -05:00
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
|
2011-09-12 05:39:38 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
expr_bind(operator, maybe_args) {
|
2011-08-19 17:16:48 -05:00
|
|
|
let args = [];
|
2011-08-08 21:38:19 -05:00
|
|
|
let cmodes = callee_modes(fcx, operator.id);
|
2011-08-19 17:16:48 -05:00
|
|
|
let modes = [];
|
2011-08-08 21:38:19 -05:00
|
|
|
let i = 0;
|
2011-08-12 09:15:18 -05:00
|
|
|
for expr_opt: option::t<@expr> in maybe_args {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt expr_opt {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* no-op */ }
|
2011-08-19 17:16:48 -05:00
|
|
|
some(expr) { modes += [cmodes[i]]; args += [expr]; }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-08-08 21:38:19 -05:00
|
|
|
i += 1;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
args += [operator]; /* ??? order of eval? */
|
2011-08-08 21:38:19 -05:00
|
|
|
forget_args_moved_in(fcx, e, modes, args);
|
2011-07-27 07:19:39 -05:00
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
expr_break { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
expr_cont { clear_pp(expr_pp(fcx.ccx, e)); }
|
2011-09-02 17:34:58 -05:00
|
|
|
expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
|
2011-12-22 16:42:52 -06:00
|
|
|
#debug("stmt =");
|
2011-05-14 21:02:30 -05:00
|
|
|
log_stmt(s);
|
2011-07-27 07:19:39 -05:00
|
|
|
alt s.node {
|
|
|
|
stmt_decl(adecl, id) {
|
|
|
|
alt adecl.node {
|
|
|
|
decl_local(alocals) {
|
2011-08-18 19:17:50 -05:00
|
|
|
let e_pp;
|
|
|
|
let prev_pp = empty_pre_post(num_constraints(fcx.enclosing));
|
2011-09-15 04:42:56 -05:00
|
|
|
for (_, alocal) in alocals {
|
2011-07-27 07:19:39 -05:00
|
|
|
alt alocal.node.init {
|
|
|
|
some(an_init) {
|
|
|
|
/* LHS always becomes initialized,
|
|
|
|
whether or not this is a move */
|
|
|
|
find_pre_post_expr(fcx, an_init.expr);
|
2011-10-21 05:41:42 -05:00
|
|
|
pat_bindings(alocal.node.pat) {|p|
|
2011-07-28 05:01:45 -05:00
|
|
|
copy_pre_post(fcx.ccx, p.id, an_init.expr);
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-07-27 07:19:39 -05:00
|
|
|
/* Inherit ann from initializer, and add var being
|
|
|
|
initialized to the postcondition */
|
|
|
|
copy_pre_post(fcx.ccx, id, an_init.expr);
|
|
|
|
|
2011-08-03 03:19:36 -05:00
|
|
|
let p = none;
|
2011-07-27 07:19:39 -05:00
|
|
|
alt an_init.expr.node {
|
2011-08-03 03:19:36 -05:00
|
|
|
expr_path(_p) { p = some(_p); }
|
|
|
|
_ { }
|
|
|
|
}
|
|
|
|
|
2012-01-14 18:05:07 -06:00
|
|
|
pat_bindings(normalize_pat(fcx.ccx.tcx, alocal.node.pat))
|
|
|
|
{|pat|
|
2011-08-18 19:17:50 -05:00
|
|
|
/* FIXME: This won't be necessary when typestate
|
|
|
|
works well enough for pat_bindings to return a
|
|
|
|
refinement-typed thing. */
|
2012-01-14 18:05:07 -06:00
|
|
|
let ident = alt pat.node
|
|
|
|
{ pat_ident(n, _) { path_to_ident(n) } };
|
2011-08-03 03:19:36 -05:00
|
|
|
alt p {
|
|
|
|
some(p) {
|
2011-07-28 05:01:45 -05:00
|
|
|
copy_in_postcond(fcx, id,
|
|
|
|
{ident: ident, node: pat.id},
|
|
|
|
{ident:
|
2012-01-14 18:05:07 -06:00
|
|
|
path_to_ident(p),
|
2011-07-28 05:01:45 -05:00
|
|
|
node: an_init.expr.id},
|
|
|
|
op_to_oper_ty(an_init.op));
|
2011-08-03 03:19:36 -05:00
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
none { }
|
2011-07-28 05:01:45 -05:00
|
|
|
}
|
2011-08-03 03:19:36 -05:00
|
|
|
gen(fcx, id, ninit(pat.id, ident));
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-07-27 07:19:39 -05:00
|
|
|
|
|
|
|
if an_init.op == init_move && is_path(an_init.expr) {
|
|
|
|
forget_in_postcond(fcx, id, an_init.expr.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-08-18 19:17:50 -05:00
|
|
|
|
|
|
|
/* Clear out anything that the previous initializer
|
|
|
|
guaranteed */
|
|
|
|
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 */
|
2012-01-14 18:05:07 -06:00
|
|
|
pat_bindings(normalize_pat(fcx.ccx.tcx, alocal.node.pat))
|
|
|
|
{|pat|
|
|
|
|
// FIXME
|
|
|
|
// Generalize this pattern? map_if_ident...
|
2011-08-18 19:17:50 -05:00
|
|
|
alt pat.node {
|
2012-01-14 18:05:07 -06:00
|
|
|
pat_ident(n, _) {
|
|
|
|
set_in_postcond(bit_num(fcx,
|
|
|
|
ninit(pat.id, path_to_ident(n))), prev_pp);
|
2011-08-18 19:17:50 -05:00
|
|
|
}
|
2011-08-19 17:16:48 -05:00
|
|
|
}
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-08-19 17:16:48 -05:00
|
|
|
copy_pre_post_(fcx.ccx, id, prev_pp.precondition,
|
2011-08-18 19:17:50 -05:00
|
|
|
prev_pp.postcondition);
|
2011-07-22 10:19:06 -05:00
|
|
|
}
|
2012-01-19 00:37:22 -06:00
|
|
|
none {
|
2011-10-21 05:41:42 -05:00
|
|
|
pat_bindings(alocal.node.pat) {|p|
|
2011-07-28 05:01:45 -05:00
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx, p.id).conditions);
|
2011-10-21 05:41:42 -05:00
|
|
|
};
|
2011-06-19 15:41:21 -05:00
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-07-27 07:19:39 -05:00
|
|
|
}
|
|
|
|
decl_item(anitem) {
|
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
|
|
|
|
find_pre_post_item(fcx.ccx, *anitem);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2012-01-04 16:16:41 -06:00
|
|
|
stmt_expr(e, id) | stmt_semi(e, id) {
|
2011-07-27 07:19:39 -05:00
|
|
|
find_pre_post_expr(fcx, e);
|
|
|
|
copy_pre_post(fcx.ccx, id, e);
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-09-12 04:27:30 -05:00
|
|
|
fn find_pre_post_block(fcx: fn_ctxt, b: blk) {
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Want to say that if there is a break or cont in this
|
|
|
|
block, then that invalidates the poststate upheld by
|
2011-07-13 17:44:09 -05:00
|
|
|
any of the stmts after it.
|
2011-05-14 21:02:30 -05:00
|
|
|
Given that the typechecker has run, we know any break will be in
|
|
|
|
a block that forms a loop body. So that's ok. There'll never be an
|
|
|
|
expr_break outside a loop body, therefore, no expr_break outside a block.
|
|
|
|
*/
|
|
|
|
|
|
|
|
/* Conservative approximation for now: This says that if a block contains
|
|
|
|
*any* breaks or conts, then its postcondition doesn't promise anything.
|
|
|
|
This will mean that:
|
|
|
|
x = 0;
|
|
|
|
break;
|
2011-07-27 07:48:34 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
won't have a postcondition that says x is initialized, but that's ok.
|
|
|
|
*/
|
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
let nv = num_constraints(fcx.enclosing);
|
2011-09-12 04:27:30 -05:00
|
|
|
fn do_one_(fcx: fn_ctxt, s: @stmt) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_stmt(fcx, *s);
|
2011-08-19 17:16:48 -05:00
|
|
|
/*
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("pre_post for stmt:");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_stmt_err(*s);
|
2011-12-22 16:42:52 -06:00
|
|
|
#error("is:");
|
2011-08-19 17:16:48 -05:00
|
|
|
log_pp_err(stmt_pp(fcx.ccx, *s));
|
|
|
|
*/
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-08-15 23:54:52 -05:00
|
|
|
for s: @stmt in b.node.stmts { do_one_(fcx, s); }
|
2011-10-06 05:26:12 -05:00
|
|
|
fn do_inner_(fcx: fn_ctxt, &&e: @expr) { find_pre_post_expr(fcx, e); }
|
2011-07-27 07:19:39 -05:00
|
|
|
let do_inner = bind do_inner_(fcx, _);
|
2011-12-16 08:27:50 -06:00
|
|
|
option::map::<@expr, ()>(b.node.expr, do_inner);
|
2011-07-05 01:29:15 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
let pps: [pre_and_post] = [];
|
|
|
|
for s: @stmt in b.node.stmts { pps += [stmt_pp(fcx.ccx, *s)]; }
|
2011-07-27 07:19:39 -05:00
|
|
|
alt b.node.expr {
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* no-op */ }
|
2011-08-19 17:16:48 -05:00
|
|
|
some(e) { pps += [expr_pp(fcx.ccx, e)]; }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
let block_precond = seq_preconds(fcx, pps);
|
2011-07-05 01:29:15 -05:00
|
|
|
|
2011-08-19 17:16:48 -05:00
|
|
|
let postconds = [];
|
|
|
|
for pp: pre_and_post in pps { postconds += [get_post(pp)]; }
|
2011-07-05 01:29:15 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* A block may be empty, so this next line ensures that the postconds
|
|
|
|
vector is non-empty. */
|
2011-08-19 17:16:48 -05:00
|
|
|
postconds += [block_precond];
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
let block_postcond = empty_poststate(nv);
|
2011-05-14 21:02:30 -05:00
|
|
|
/* conservative approximation */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-27 07:19:39 -05:00
|
|
|
if !has_nonlocal_exits(b) {
|
Compute typestate properly for move
typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.
To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:
(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;
(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;
With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.
2011-06-22 23:26:34 -05:00
|
|
|
block_postcond = seq_postconds(fcx, postconds);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-19 15:41:21 -05:00
|
|
|
set_pre_and_post(fcx.ccx, b.node.id, block_precond, block_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-12-20 13:03:21 -06:00
|
|
|
fn find_pre_post_fn(fcx: fn_ctxt, body: blk) {
|
2011-06-30 02:18:41 -05:00
|
|
|
// hack
|
2011-08-01 22:55:04 -05:00
|
|
|
use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_return));
|
|
|
|
use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_diverge));
|
2011-06-30 02:18:41 -05:00
|
|
|
|
2011-12-20 13:03:21 -06:00
|
|
|
find_pre_post_block(fcx, body);
|
2011-08-19 03:15:30 -05:00
|
|
|
|
2011-05-31 14:24:18 -05:00
|
|
|
// Treat the tail expression as a return statement
|
2011-12-20 13:03:21 -06:00
|
|
|
alt body.node.expr {
|
2011-07-27 07:19:39 -05:00
|
|
|
some(tailexpr) { set_postcond_false(fcx.ccx, tailexpr.id); }
|
2012-01-19 00:37:22 -06:00
|
|
|
none {/* fallthrough */ }
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-12-29 22:07:55 -06:00
|
|
|
fn fn_pre_post(fk: visit::fn_kind, decl: fn_decl, body: blk, sp: span,
|
|
|
|
id: node_id,
|
2011-09-12 04:27:30 -05:00
|
|
|
ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
|
2011-12-29 22:07:55 -06:00
|
|
|
visit::visit_fn(fk, decl, body, sp, id, ccx, v);
|
2011-05-14 21:02:30 -05:00
|
|
|
assert (ccx.fm.contains_key(id));
|
2011-07-27 07:19:39 -05:00
|
|
|
let fcx =
|
|
|
|
{enclosing: ccx.fm.get(id),
|
|
|
|
id: id,
|
2011-12-29 22:07:55 -06:00
|
|
|
name: visit::name_of_fn(fk),
|
2011-07-27 07:19:39 -05:00
|
|
|
ccx: ccx};
|
2011-12-20 13:03:21 -06:00
|
|
|
find_pre_post_fn(fcx, body);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-12-20 13:03:21 -06:00
|
|
|
|
2011-05-14 21:02:30 -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:
|
|
|
|
//
|