2011-07-06 21:00:00 -05:00
|
|
|
import std::ivec;
|
2011-05-17 13:41:41 -05:00
|
|
|
import std::vec;
|
|
|
|
import std::vec::plus_option;
|
|
|
|
import std::vec::cat_options;
|
2011-05-14 21:02:30 -05:00
|
|
|
import std::option;
|
|
|
|
import std::option::get;
|
|
|
|
import std::option::is_none;
|
|
|
|
import std::option::none;
|
|
|
|
import std::option::some;
|
|
|
|
import std::option::maybe;
|
2011-06-25 00:17:17 -05:00
|
|
|
import tstate::ann::set_in_poststate_;
|
2011-05-14 21:02:30 -05:00
|
|
|
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;
|
2011-06-25 00:17:17 -05:00
|
|
|
import tstate::ann::clear_in_poststate;
|
2011-05-14 21:02:30 -05:00
|
|
|
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;
|
2011-06-25 00:17:17 -05:00
|
|
|
import tstate::ann::set_prestate;
|
|
|
|
import tstate::ann::set_poststate;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::crate_ctxt;
|
|
|
|
import aux::fn_ctxt;
|
2011-06-01 20:10:10 -05:00
|
|
|
import aux::num_constraints;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::expr_pp;
|
|
|
|
import aux::stmt_pp;
|
|
|
|
import aux::block_pp;
|
|
|
|
import aux::set_pre_and_post;
|
|
|
|
import aux::expr_prestate;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::expr_precond;
|
|
|
|
import aux::expr_postcond;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::stmt_poststate;
|
|
|
|
import aux::expr_poststate;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::block_prestate;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::block_poststate;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::block_precond;
|
|
|
|
import aux::block_postcond;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::fn_info;
|
|
|
|
import aux::log_pp;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::log_pp_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::extend_prestate_ann;
|
|
|
|
import aux::extend_poststate_ann;
|
|
|
|
import aux::set_prestate_ann;
|
|
|
|
import aux::set_poststate_ann;
|
|
|
|
import aux::pure_exp;
|
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
|
|
|
import aux::log_tritv;
|
|
|
|
import aux::log_tritv_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::stmt_to_ann;
|
|
|
|
import aux::log_states;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::log_states_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::block_states;
|
|
|
|
import aux::controlflow_expr;
|
2011-06-19 15:41:21 -05:00
|
|
|
import aux::node_id_to_def;
|
2011-06-09 11:56:35 -05:00
|
|
|
import aux::expr_to_constr;
|
2011-06-13 20:10:33 -05:00
|
|
|
import aux::ninit;
|
|
|
|
import aux::npred;
|
|
|
|
import aux::path_to_ident;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::if_ty;
|
|
|
|
import aux::if_check;
|
|
|
|
import aux::plain_if;
|
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
|
|
|
import aux::forget_in_poststate;
|
2011-06-25 00:17:17 -05:00
|
|
|
import aux::forget_in_poststate_still_init;
|
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
|
|
|
import tritv::tritv_clone;
|
|
|
|
import tritv::tritv_set;
|
|
|
|
import tritv::ttrue;
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-25 00:17:17 -05:00
|
|
|
import bitvectors::set_in_poststate_ident;
|
|
|
|
import bitvectors::clear_in_poststate_expr;
|
2011-06-27 20:12:37 -05:00
|
|
|
import bitvectors::clear_in_prestate_ident;
|
2011-05-14 21:02:30 -05:00
|
|
|
import bitvectors::bit_num;
|
|
|
|
import bitvectors::gen_poststate;
|
2011-05-20 21:50:29 -05:00
|
|
|
import bitvectors::kill_poststate;
|
2011-06-27 20:12:37 -05:00
|
|
|
import bitvectors::clear_in_poststate_ident;
|
|
|
|
import bitvectors::intersect_states;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::ast::*;
|
2011-05-31 14:24:18 -05:00
|
|
|
import middle::ty::expr_ty;
|
|
|
|
import middle::ty::type_is_nil;
|
|
|
|
import middle::ty::type_is_bot;
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::new_def_hash;
|
|
|
|
import util::common::log_expr;
|
|
|
|
import util::common::log_block;
|
2011-06-17 21:07:23 -05:00
|
|
|
import util::common::log_block_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
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;
|
2011-06-17 21:07:23 -05:00
|
|
|
import util::common::log_stmt_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::log_expr_err;
|
|
|
|
|
2011-06-25 00:17:17 -05:00
|
|
|
// Used to communicate which operands should be invalidated
|
|
|
|
// to helper functions
|
|
|
|
tag oper_type {
|
|
|
|
oper_move;
|
|
|
|
oper_swap;
|
|
|
|
oper_assign;
|
|
|
|
oper_pure;
|
|
|
|
}
|
|
|
|
|
2011-07-06 21:00:00 -05:00
|
|
|
fn seq_states(&fn_ctxt fcx, prestate pres, &(@expr)[] exprs) ->
|
2011-06-15 13:19:50 -05:00
|
|
|
tup(bool, poststate) {
|
|
|
|
auto changed = false;
|
|
|
|
auto post = pres;
|
|
|
|
for (@expr e in exprs) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr(fcx, post, e) || changed;
|
2011-06-25 00:17:17 -05:00
|
|
|
// log_err("Seq_states: changed =");
|
|
|
|
// log_err changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
post = expr_poststate(fcx.ccx, e);
|
|
|
|
}
|
|
|
|
ret tup(changed, post);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-25 00:17:17 -05:00
|
|
|
fn find_pre_post_state_sub(&fn_ctxt fcx, &prestate pres, &@expr e,
|
|
|
|
node_id parent, option::t[aux::constr_] c)
|
|
|
|
-> bool {
|
|
|
|
auto changed = find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
|
|
|
|
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
|
|
|
|
|
|
|
|
auto post = tritv_clone(expr_poststate(fcx.ccx, e));
|
|
|
|
alt (c) {
|
|
|
|
case (none) {}
|
|
|
|
case (some(?c1)) {
|
|
|
|
set_in_poststate_(bit_num(fcx, c1), post);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_state_two(&fn_ctxt fcx, &prestate pres, &@expr a, &@expr b,
|
|
|
|
node_id parent, oper_type op) -> bool {
|
|
|
|
auto changed = set_prestate_ann(fcx.ccx, parent, pres);
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, a) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, a), b)
|
|
|
|
|| changed;
|
|
|
|
|
|
|
|
// for termination, need to make sure intermediate changes don't set
|
|
|
|
// changed flag
|
|
|
|
auto post = tritv_clone(expr_poststate(fcx.ccx, b));
|
|
|
|
alt (op) {
|
|
|
|
case (oper_move) {
|
|
|
|
forget_in_poststate(fcx, post, b.id);
|
|
|
|
gen_if_local(fcx, post, a);
|
|
|
|
}
|
|
|
|
case (oper_swap) {
|
|
|
|
forget_in_poststate_still_init(fcx, post, a.id);
|
|
|
|
forget_in_poststate_still_init(fcx, post, b.id);
|
|
|
|
}
|
|
|
|
case (oper_assign) {
|
|
|
|
forget_in_poststate_still_init(fcx, post, a.id);
|
|
|
|
gen_if_local(fcx, post, a);
|
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_state_call(&fn_ctxt fcx, &prestate pres, &@expr a,
|
2011-07-06 21:00:00 -05:00
|
|
|
node_id id, &(@expr)[] bs,
|
2011-06-25 00:17:17 -05:00
|
|
|
controlflow cf) -> bool {
|
|
|
|
auto 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-05 04:48:19 -05:00
|
|
|
fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, node_id id,
|
2011-07-06 21:00:00 -05:00
|
|
|
&(@expr)[] es, controlflow cf) -> bool {
|
2011-06-25 10:45:49 -05:00
|
|
|
auto rs = seq_states(fcx, pres, es);
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = rs._0 | 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 */
|
|
|
|
alt (cf) {
|
|
|
|
case (noreturn) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= set_poststate_ann
|
|
|
|
(fcx.ccx, id, false_postcond(num_constraints(fcx.enclosing)));
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
|
|
|
case (_) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= set_poststate_ann(fcx.ccx, id, rs._1);
|
2011-06-25 00:17:17 -05:00
|
|
|
}
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-06-13 19:04:15 -05:00
|
|
|
fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
|
2011-06-19 15:41:21 -05:00
|
|
|
&@expr index, &block body, node_id id) -> bool {
|
2011-06-27 20:12:37 -05:00
|
|
|
auto loop_pres = intersect_states(pres,
|
|
|
|
block_poststate(fcx.ccx, body));
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-06-27 20:12:37 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
|
2011-06-25 10:29:50 -05:00
|
|
|
find_pre_post_state_expr(fcx, pres, index);
|
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
if (has_nonlocal_exits(body)) {
|
2011-06-27 20:12:37 -05:00
|
|
|
// See [Break-unsound]
|
|
|
|
ret (changed | set_poststate_ann(fcx.ccx, id, pres));
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
2011-06-27 20:12:37 -05:00
|
|
|
else {
|
|
|
|
auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
|
|
|
|
block_poststate(fcx.ccx, body));
|
|
|
|
/*
|
2011-06-15 13:19:50 -05:00
|
|
|
auto res_p =
|
|
|
|
intersect_postconds([expr_poststate(fcx.ccx, index),
|
2011-06-27 20:12:37 -05:00
|
|
|
block_poststate(fcx.ccx, body)]); */
|
|
|
|
|
|
|
|
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-25 00:17:17 -05:00
|
|
|
fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool {
|
|
|
|
alt (e.node) {
|
|
|
|
case (expr_path(?pth)) {
|
|
|
|
alt (node_id_to_def(fcx.ccx, e.id)) {
|
|
|
|
case (some(def_local(?loc))) {
|
|
|
|
ret set_in_poststate_ident(fcx, loc._1,
|
|
|
|
path_to_ident(fcx.ccx.tcx, pth), p);
|
|
|
|
}
|
|
|
|
case (_) { ret false; }
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-25 00:17:17 -05:00
|
|
|
case (_) { ret false; }
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
|
2011-07-05 04:48:19 -05:00
|
|
|
&option::t[@expr] maybe_alt, node_id id, &if_ty chk,
|
2011-06-17 21:07:23 -05:00
|
|
|
&prestate pres) -> bool {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, id, pres) |
|
|
|
|
find_pre_post_state_expr(fcx, pres, antec);
|
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-06-16 13:56:34 -05:00
|
|
|
alt (maybe_alt) {
|
|
|
|
case (none) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_block
|
|
|
|
(fcx, expr_poststate(fcx.ccx, antec), conseq) |
|
2011-06-25 00:17:17 -05:00
|
|
|
set_poststate_ann(fcx.ccx, id,
|
2011-06-25 10:29:50 -05:00
|
|
|
expr_poststate(fcx.ccx, antec));
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
case (some(?altern)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr
|
|
|
|
(fcx, expr_poststate(fcx.ccx, antec), altern);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
auto conseq_prestate = expr_poststate(fcx.ccx, antec);
|
|
|
|
alt (chk) {
|
|
|
|
case (if_check) {
|
|
|
|
let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
|
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
|
|
|
conseq_prestate = tritv_clone(conseq_prestate);
|
|
|
|
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |=
|
|
|
|
find_pre_post_state_block(fcx, conseq_prestate, conseq);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
auto poststate_res =
|
2011-06-27 20:12:37 -05:00
|
|
|
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));
|
2011-06-17 21:07:23 -05:00
|
|
|
fcx.ccx.tcx.sess.span_note(antec.span,
|
|
|
|
"altern poststate = " +
|
2011-06-27 20:12:37 -05:00
|
|
|
aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
|
2011-06-17 21:07:23 -05:00
|
|
|
fcx.ccx.tcx.sess.span_note(antec.span,
|
2011-06-27 20:12:37 -05:00
|
|
|
"conseq poststate = " + aux::tritv_to_str(fcx,
|
|
|
|
block_poststate(fcx.ccx, conseq)));
|
|
|
|
*/
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|
2011-06-27 20:12:37 -05:00
|
|
|
auto num_constrs = num_constraints(fcx.enclosing);
|
2011-06-15 13:19:50 -05:00
|
|
|
|
|
|
|
alt (e.node) {
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_vec(?elts, _, _)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_exprs(fcx, pres, e.id, elts, return);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_tup(?elts)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_exprs(fcx, pres, e.id,
|
|
|
|
elt_exprs(elts), return);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_call(?operator, ?operands)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
ret find_pre_post_state_call
|
|
|
|
(fcx, pres, operator, e.id, operands,
|
|
|
|
controlflow_expr(fcx.ccx, operator));
|
2011-05-27 19:38:52 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_spawn(_, _, ?operator, ?operands)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_call(fcx, pres, operator, e.id, operands,
|
|
|
|
return);
|
2011-06-25 10:29:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_bind(?operator, ?maybe_args)) {
|
2011-07-06 21:00:00 -05:00
|
|
|
auto args = ~[];
|
|
|
|
for (option::t[@expr] a_opt in maybe_args) {
|
|
|
|
alt (a_opt) {
|
|
|
|
case (none) { /* no-op */ }
|
|
|
|
case (some(?a)) { args += ~[a]; }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
ret find_pre_post_state_call(fcx, pres, operator, e.id, args,
|
|
|
|
return);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_path(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
|
|
|
|
case (expr_log(_, ?ex)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, ex, e.id, none);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_chan(?ex)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, ex, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_ext(_, _, _, ?expanded)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, expanded, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_put(?maybe_e)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (maybe_e) {
|
|
|
|
case (some(?arg)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, arg, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (none) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_lit(?l)) { ret pure_exp(fcx.ccx, e.id, pres); }
|
|
|
|
case (expr_fn(?f)) { ret pure_exp(fcx.ccx, e.id, pres); }
|
|
|
|
case (expr_block(?b)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
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-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_rec(?fields, ?maybe_base)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = find_pre_post_state_exprs
|
|
|
|
(fcx, pres, e.id, field_exprs(fields), return);
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (maybe_base) {
|
|
|
|
case (none) {/* do nothing */ }
|
|
|
|
case (some(?base)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr(fcx, pres, base) |
|
|
|
|
set_poststate_ann(fcx.ccx, e.id,
|
|
|
|
expr_poststate(fcx.ccx, base));
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_move(?lhs, ?rhs)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_two(fcx, pres, lhs, rhs,
|
|
|
|
e.id, oper_move);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_assign(?lhs, ?rhs)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_two(fcx, pres, lhs, rhs,
|
|
|
|
e.id, oper_assign);
|
2011-05-20 21:50:29 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_swap(?lhs, ?rhs)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
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
|
2011-06-16 18:55:46 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_recv(?lhs, ?rhs)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
// Opposite order as most other binary operations,
|
|
|
|
// so not using find_pre_post_state_two
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
|
|
|
|
find_pre_post_state_expr(fcx, pres, lhs) |
|
|
|
|
find_pre_post_state_expr
|
|
|
|
(fcx, expr_poststate(fcx.ccx, lhs), rhs);
|
2011-06-25 00:17:17 -05:00
|
|
|
auto post = tritv_clone(expr_poststate(fcx.ccx, rhs));
|
|
|
|
forget_in_poststate_still_init(fcx, post, rhs.id);
|
|
|
|
gen_if_local(fcx, post, rhs);
|
2011-06-25 10:29:50 -05:00
|
|
|
ret changed | set_poststate_ann(fcx.ccx, e.id, post);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_ret(?maybe_ret_val)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
|
2011-06-15 13:19:50 -05:00
|
|
|
/* normally, everything is true if execution continues after
|
|
|
|
a ret expression (since execution never continues locally
|
|
|
|
after a ret expression */
|
|
|
|
|
2011-06-27 20:12:37 -05:00
|
|
|
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
|
2011-06-15 13:19:50 -05:00
|
|
|
/* return from an always-failing function clears the return bit */
|
|
|
|
|
|
|
|
alt (fcx.enclosing.cf) {
|
|
|
|
case (noreturn) {
|
2011-06-21 15:16:40 -05:00
|
|
|
kill_poststate(fcx, e.id, rec(id=fcx.id,
|
|
|
|
c=ninit(fcx.name)));
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
case (_) { }
|
|
|
|
}
|
|
|
|
alt (maybe_ret_val) {
|
|
|
|
case (none) {/* do nothing */ }
|
|
|
|
case (some(?ret_val)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr(fcx, pres, ret_val);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_be(?val)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
|
2011-06-27 20:12:37 -05:00
|
|
|
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
|
2011-06-25 10:29:50 -05:00
|
|
|
ret changed | find_pre_post_state_expr(fcx, pres, val);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_if(?antec, ?conseq, ?maybe_alt)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
ret join_then_else
|
|
|
|
(fcx, antec, conseq, maybe_alt, e.id, plain_if, pres);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-23 17:15:50 -05:00
|
|
|
case (expr_ternary(_, _, _)) {
|
|
|
|
ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_binary(?bop, ?l, ?r)) {
|
2011-06-28 15:07:05 -05:00
|
|
|
if (lazy_binop(bop)) {
|
|
|
|
auto 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-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_send(?l, ?r)) {
|
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-06-21 15:16:40 -05:00
|
|
|
case (expr_assign_op(?op, ?lhs, ?rhs)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id,
|
|
|
|
oper_assign);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_while(?test, ?body)) {
|
2011-06-27 20:12:37 -05:00
|
|
|
/*
|
|
|
|
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);
|
2011-06-15 13:19:50 -05:00
|
|
|
*/
|
2011-06-27 20:12:37 -05:00
|
|
|
auto loop_pres = intersect_states
|
|
|
|
(block_poststate(fcx.ccx, body), pres);
|
|
|
|
// aux::log_tritv_err(fcx, loop_pres);
|
|
|
|
// log_err "---------------";
|
|
|
|
|
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres) |
|
|
|
|
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-06-17 21:07:23 -05:00
|
|
|
/* conservative approximation: if a loop contains a break
|
|
|
|
or cont, we assume nothing about the poststate */
|
2011-06-27 20:12:37 -05:00
|
|
|
/* which is still unsound -- see [Break-unsound] */
|
2011-06-17 21:07:23 -05:00
|
|
|
if (has_nonlocal_exits(body)) {
|
2011-06-27 20:12:37 -05:00
|
|
|
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
|
|
|
|
}
|
|
|
|
else {
|
|
|
|
auto e_post = expr_poststate(fcx.ccx, test);
|
|
|
|
auto b_post = block_poststate(fcx.ccx, body);
|
|
|
|
ret changed | set_poststate_ann
|
|
|
|
(fcx.ccx, e.id, intersect_states(e_post, b_post));
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_do_while(?body, ?test)) {
|
2011-06-27 20:12:37 -05:00
|
|
|
auto loop_pres = intersect_states(expr_poststate(fcx.ccx, test),
|
|
|
|
pres);
|
|
|
|
|
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
|
|
|
|
changed |= find_pre_post_state_block(fcx, loop_pres, body);
|
2011-06-15 13:19:50 -05:00
|
|
|
/* 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) */
|
|
|
|
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr
|
|
|
|
(fcx, block_poststate(fcx.ccx, body), test);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-27 20:12:37 -05:00
|
|
|
auto breaks = has_nonlocal_exits(body);
|
2011-06-17 21:07:23 -05:00
|
|
|
if (breaks) {
|
2011-06-27 20:12:37 -05:00
|
|
|
// 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);
|
|
|
|
}
|
2011-06-17 21:07:23 -05:00
|
|
|
else {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= set_poststate_ann
|
|
|
|
(fcx.ccx, e.id, expr_poststate(fcx.ccx, test));
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_for(?d, ?index, ?body)) {
|
|
|
|
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_for_each(?d, ?index, ?body)) {
|
|
|
|
ret find_pre_post_state_loop(fcx, pres, d, index, body, e.id);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_index(?val, ?sub)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_alt(?val, ?alts)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
|
|
|
|
find_pre_post_state_expr(fcx, pres, val);
|
2011-06-21 15:16:40 -05:00
|
|
|
auto e_post = expr_poststate(fcx.ccx, val);
|
2011-06-15 13:19:50 -05:00
|
|
|
auto a_post;
|
2011-07-06 21:00:00 -05:00
|
|
|
if (ivec::len(alts) > 0u) {
|
2011-06-27 20:12:37 -05:00
|
|
|
a_post = false_postcond(num_constrs);
|
2011-06-15 13:19:50 -05:00
|
|
|
for (arm an_alt in alts) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_block
|
|
|
|
(fcx, e_post, an_alt.block);
|
2011-06-15 13:19:50 -05:00
|
|
|
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-05-14 21:02:30 -05:00
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
} else {
|
|
|
|
// No alts; poststate is the poststate of the test
|
|
|
|
|
|
|
|
a_post = e_post;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-25 10:29:50 -05:00
|
|
|
ret changed | set_poststate_ann(fcx.ccx, e.id, a_post);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_field(?val, _)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, val, e.id, none);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_unary(_, ?operand)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_cast(?operand, _)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-07-01 13:33:15 -05:00
|
|
|
case (expr_fail(?maybe_fail_val)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
ret set_prestate_ann(fcx.ccx, e.id, pres) |
|
2011-06-15 13:19:50 -05:00
|
|
|
/* if execution continues after fail, then everything is true!
|
|
|
|
woo! */
|
2011-06-25 10:29:50 -05:00
|
|
|
set_poststate_ann(fcx.ccx, e.id,
|
2011-07-01 13:33:15 -05:00
|
|
|
false_postcond(num_constrs)) |
|
|
|
|
alt(maybe_fail_val) {
|
|
|
|
case (none) { false }
|
|
|
|
case (some(?fail_val)) {
|
|
|
|
find_pre_post_state_expr(fcx, pres, fail_val)
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_assert(?p)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
2011-06-28 18:29:37 -05:00
|
|
|
case (expr_check(_, ?p)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
/* predicate p holds after this expression executes */
|
|
|
|
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
|
2011-06-25 10:29:50 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_if_check(?p, ?conseq, ?maybe_alt)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
ret join_then_else
|
|
|
|
(fcx, p, conseq, maybe_alt, e.id, if_check, pres);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_break) { ret pure_exp(fcx.ccx, e.id, pres); }
|
|
|
|
case (expr_cont) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-06-28 17:54:16 -05:00
|
|
|
case (expr_port(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_self_method(_)) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-07-06 13:29:22 -05:00
|
|
|
case (expr_anon_obj(?anon_obj, _)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (anon_obj.with_obj) {
|
2011-06-21 15:16:40 -05:00
|
|
|
case (some(?wt)) {
|
2011-06-25 00:17:17 -05:00
|
|
|
ret find_pre_post_state_sub(fcx, pres, wt, e.id, none);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (none) { ret pure_exp(fcx.ccx, e.id, pres); }
|
2011-05-20 19:41:36 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
|
2011-05-18 17:43:05 -05:00
|
|
|
auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-25 00:17:17 -05:00
|
|
|
/*
|
2011-06-17 21:07:23 -05:00
|
|
|
log_err "*At beginning: stmt = ";
|
|
|
|
log_stmt_err(*s);
|
|
|
|
log_err "*prestate = ";
|
2011-06-25 00:17:17 -05:00
|
|
|
log_err tritv::to_str(stmt_ann.states.prestate);
|
2011-06-17 21:07:23 -05:00
|
|
|
log_err "*poststate =";
|
2011-06-25 00:17:17 -05:00
|
|
|
log_err tritv::to_str(stmt_ann.states.poststate);
|
|
|
|
log_err "pres = ";
|
|
|
|
log_err tritv::to_str(pres);
|
2011-06-17 21:07:23 -05:00
|
|
|
*/
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
alt (s.node) {
|
2011-06-19 15:41:21 -05:00
|
|
|
case (stmt_decl(?adecl, ?id)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
alt (adecl.node) {
|
|
|
|
case (decl_local(?alocal)) {
|
2011-06-16 17:58:25 -05:00
|
|
|
alt (alocal.node.init) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?an_init)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
auto changed = set_prestate(stmt_ann, pres) |
|
2011-06-15 13:19:50 -05:00
|
|
|
find_pre_post_state_expr(fcx, pres,
|
2011-06-25 10:29:50 -05:00
|
|
|
an_init.expr);
|
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-06-25 00:17:17 -05:00
|
|
|
auto post = tritv_clone(expr_poststate(fcx.ccx,
|
|
|
|
an_init.expr));
|
2011-06-25 05:16:48 -05:00
|
|
|
if (an_init.op == init_move) {
|
|
|
|
clear_in_poststate_expr(fcx, an_init.expr,
|
|
|
|
post);
|
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-06-25 00:17:17 -05:00
|
|
|
set_in_poststate_ident(fcx, alocal.node.id,
|
|
|
|
alocal.node.ident, post);
|
|
|
|
|
|
|
|
/* important to do this in one step to ensure
|
|
|
|
termination (don't want to set changed to true
|
|
|
|
for intermediate changes) */
|
2011-06-25 10:29:50 -05:00
|
|
|
ret changed | set_poststate(stmt_ann, post);
|
2011-06-25 00:17:17 -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
|
|
|
/*
|
|
|
|
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-05-18 17:43:05 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-06-27 20:12:37 -05:00
|
|
|
// let int = x; => x is uninit in poststate
|
|
|
|
set_poststate_ann(fcx.ccx, id, pres);
|
|
|
|
clear_in_poststate_ident(fcx, alocal.node.id,
|
2011-06-29 17:11:20 -05:00
|
|
|
alocal.node.ident, id);
|
2011-06-27 20:12:37 -05:00
|
|
|
set_prestate(stmt_ann, pres);
|
|
|
|
ret false;
|
2011-05-18 17:43:05 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (decl_item(?an_item)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
ret set_prestate(stmt_ann, pres) |
|
|
|
|
set_poststate(stmt_ann, pres);
|
2011-05-18 20:03:48 -05:00
|
|
|
/* the outer "walk" will recurse into the item */
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (stmt_expr(?ex, _)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
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-05-18 17:43:05 -05:00
|
|
|
/*
|
2011-06-25 00:17:17 -05:00
|
|
|
log_err "Finally:";
|
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
|
|
|
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);
|
2011-05-18 17:43:05 -05:00
|
|
|
*/
|
|
|
|
}
|
|
|
|
case (_) { 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-06-25 10:29:50 -05:00
|
|
|
fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
|
|
|
|
-> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
/* First, set the pre-states and post-states for every expression */
|
|
|
|
|
|
|
|
auto 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-06-25 10:29:50 -05:00
|
|
|
auto changed = false;
|
2011-06-15 13:19:50 -05:00
|
|
|
for (@stmt s 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-06-15 13:19:50 -05:00
|
|
|
auto post = pres;
|
|
|
|
alt (b.node.expr) {
|
|
|
|
case (none) { }
|
|
|
|
case (some(?e)) {
|
2011-06-25 10:29:50 -05:00
|
|
|
changed |= find_pre_post_state_expr(fcx, pres, e);
|
2011-06-15 13:19:50 -05:00
|
|
|
post = expr_poststate(fcx.ccx, e);
|
|
|
|
}
|
|
|
|
}
|
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-06-15 13:19:50 -05:00
|
|
|
/*
|
2011-06-17 21:07:23 -05:00
|
|
|
log_err "For block:";
|
2011-06-15 13:19:50 -05:00
|
|
|
log_block_err(b);
|
2011-06-17 21:07:23 -05:00
|
|
|
log_err "poststate = ";
|
|
|
|
log_states_err(block_states(fcx.ccx, b));
|
|
|
|
log_err "pres0:";
|
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
|
|
|
log_tritv_err(fcx, pres0);
|
2011-06-17 21:07:23 -05:00
|
|
|
log_err "post:";
|
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
|
|
|
log_tritv_err(fcx, post);
|
2011-06-15 13:19:50 -05:00
|
|
|
*/
|
|
|
|
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
|
2011-06-01 20:10:10 -05:00
|
|
|
auto num_local_vars = num_constraints(fcx.enclosing);
|
2011-06-27 20:12:37 -05:00
|
|
|
// make sure the return bit starts out False
|
|
|
|
clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
|
2011-06-15 13:19:50 -05:00
|
|
|
auto changed =
|
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
|
|
|
find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
|
2011-06-15 13:19:50 -05:00
|
|
|
f.body);
|
2011-05-31 14:24:18 -05:00
|
|
|
// Treat the tail expression as a return statement
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-31 14:24:18 -05:00
|
|
|
alt (f.body.node.expr) {
|
|
|
|
case (some(?tailexpr)) {
|
|
|
|
auto 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
|
2011-06-15 13:19:50 -05:00
|
|
|
if (!type_is_nil(fcx.ccx.tcx, tailty) &&
|
|
|
|
!type_is_bot(fcx.ccx.tcx, tailty)) {
|
2011-06-17 21:07:23 -05:00
|
|
|
auto p = false_postcond(num_local_vars);
|
2011-06-19 15:41:21 -05:00
|
|
|
set_poststate_ann(fcx.ccx, f.body.node.id, p);
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (none) {/* fallthrough */ }
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
2011-06-27 20:12:37 -05:00
|
|
|
|
|
|
|
/*
|
|
|
|
log_err "find_pre_post_state_fn";
|
|
|
|
log_err changed;
|
|
|
|
fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name);
|
|
|
|
*/
|
|
|
|
|
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
|
|
|
|
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
|
|
|
|
// End:
|
|
|
|
//
|