2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-05 01:29:15 -05:00
|
|
|
import std::ivec;
|
2011-05-14 21:02:30 -05:00
|
|
|
import std::option;
|
|
|
|
import std::option::none;
|
|
|
|
import std::option::some;
|
|
|
|
|
|
|
|
import tstate::ann::pre_and_post;
|
|
|
|
import tstate::ann::get_post;
|
|
|
|
import tstate::ann::postcond;
|
|
|
|
import tstate::ann::true_precond;
|
|
|
|
import tstate::ann::false_postcond;
|
|
|
|
import tstate::ann::empty_poststate;
|
2011-06-09 11:56:35 -05:00
|
|
|
import tstate::ann::require;
|
2011-05-14 21:02:30 -05:00
|
|
|
import tstate::ann::require_and_preserve;
|
|
|
|
import tstate::ann::union;
|
|
|
|
import tstate::ann::intersect;
|
|
|
|
import tstate::ann::pp_clone;
|
|
|
|
import tstate::ann::empty_prestate;
|
2011-05-18 17:43:05 -05:00
|
|
|
import tstate::ann::set_precondition;
|
|
|
|
import tstate::ann::set_postcondition;
|
2011-07-09 00:05:30 -05:00
|
|
|
import aux::*;
|
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 bitvectors::bit_num;
|
|
|
|
import bitvectors::promises;
|
2011-05-14 21:02:30 -05:00
|
|
|
import bitvectors::seq_preconds;
|
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 bitvectors::seq_postconds;
|
2011-06-27 20:12:37 -05:00
|
|
|
import bitvectors::intersect_states;
|
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 bitvectors::declare_var;
|
|
|
|
import bitvectors::gen_poststate;
|
2011-06-17 21:07:23 -05:00
|
|
|
import bitvectors::relax_precond_block;
|
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 bitvectors::gen;
|
2011-07-09 00:05:30 -05:00
|
|
|
import tritv::tritv_clone;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::ast::*;
|
2011-07-12 13:26:14 -05:00
|
|
|
import syntax::visit;
|
2011-07-06 09:46:17 -05:00
|
|
|
import std::map::new_int_hash;
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::new_def_hash;
|
|
|
|
import util::common::log_expr;
|
|
|
|
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-30 02:18:41 -05:00
|
|
|
import util::common::log_stmt_err;
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::log_expr_err;
|
2011-05-18 17:43:05 -05:00
|
|
|
import util::common::log_block_err;
|
|
|
|
import util::common::log_block;
|
2011-07-05 04:48:19 -05:00
|
|
|
import syntax::codemap::span;
|
|
|
|
import util::ppaux::fn_ident_to_string;
|
2011-05-26 18:02:25 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
fn find_pre_post_mod(&_mod m) -> _mod {
|
2011-06-15 13:19:50 -05:00
|
|
|
log "implement find_pre_post_mod!";
|
2011-05-14 21:02:30 -05:00
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_native_mod(&native_mod m) -> native_mod {
|
2011-06-15 13:19:50 -05:00
|
|
|
log "implement find_pre_post_native_mod";
|
2011-05-14 21:02:30 -05:00
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_obj(&crate_ctxt ccx, _obj o) {
|
|
|
|
fn do_a_method(crate_ctxt ccx, &@method m) {
|
2011-05-14 21:02:30 -05:00
|
|
|
assert (ccx.fm.contains_key(m.node.id));
|
2011-06-15 13:19:50 -05:00
|
|
|
let fn_ctxt fcx =
|
|
|
|
rec(enclosing=ccx.fm.get(m.node.id),
|
|
|
|
id=m.node.id,
|
|
|
|
name=m.node.ident,
|
|
|
|
ccx=ccx);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_fn(fcx, m.node.meth);
|
|
|
|
}
|
2011-07-06 21:00:00 -05:00
|
|
|
for (@method m in o.methods) { do_a_method(ccx, m); }
|
|
|
|
option::map[@method, ()](bind do_a_method(ccx, _), o.dtor);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_item(&crate_ctxt ccx, &item i) {
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (i.node) {
|
2011-06-16 04:53:06 -05:00
|
|
|
case (item_const(_, ?e)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
// make a fake fcx
|
2011-07-05 01:29:15 -05:00
|
|
|
let @mutable node_id[] v = @mutable ~[];
|
2011-06-15 13:19:50 -05:00
|
|
|
auto fake_fcx =
|
2011-07-19 19:52:34 -05:00
|
|
|
rec(enclosing=rec(constrs=@new_def_hash[constraint](),
|
2011-06-15 13:19:50 -05:00
|
|
|
num_constraints=0u,
|
2011-06-30 02:18:41 -05:00
|
|
|
cf=return,
|
|
|
|
used_vars=v),
|
2011-06-19 15:41:21 -05:00
|
|
|
id=0,
|
2011-06-15 13:19:50 -05:00
|
|
|
name="",
|
|
|
|
ccx=ccx);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fake_fcx, e);
|
|
|
|
}
|
2011-06-24 11:10:40 -05:00
|
|
|
case (item_fn(?f, _)) {
|
2011-06-16 04:53:06 -05:00
|
|
|
assert (ccx.fm.contains_key(i.id));
|
2011-06-16 18:55:46 -05:00
|
|
|
auto fcx =
|
|
|
|
rec(enclosing=ccx.fm.get(i.id),
|
|
|
|
id=i.id,
|
|
|
|
name=i.ident,
|
|
|
|
ccx=ccx);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_fn(fcx, f);
|
|
|
|
}
|
2011-06-16 04:53:06 -05:00
|
|
|
case (item_mod(?m)) { find_pre_post_mod(m); }
|
2011-06-16 18:55:46 -05:00
|
|
|
case (item_native_mod(?nm)) { find_pre_post_native_mod(nm); }
|
2011-06-16 04:53:06 -05:00
|
|
|
case (item_ty(_, _)) { ret; }
|
|
|
|
case (item_tag(_, _)) { ret; }
|
2011-06-24 11:10:40 -05:00
|
|
|
case (item_res(?dtor, ?dtor_id, _, _)) {
|
|
|
|
auto fcx = rec(enclosing=ccx.fm.get(dtor_id),
|
|
|
|
id=dtor_id,
|
|
|
|
name=i.ident,
|
|
|
|
ccx=ccx);
|
|
|
|
find_pre_post_fn(fcx, dtor);
|
|
|
|
}
|
2011-06-16 18:55:46 -05:00
|
|
|
case (item_obj(?o, _, _)) { find_pre_post_obj(ccx, o); }
|
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-07-06 21:00:00 -05:00
|
|
|
fn find_pre_post_exprs(&fn_ctxt fcx, &(@expr)[] args, node_id id) {
|
|
|
|
if (ivec::len[@expr](args) > 0u) {
|
2011-06-15 13:19:50 -05:00
|
|
|
log "find_pre_post_exprs: oper =";
|
|
|
|
log_expr(*args.(0));
|
2011-05-18 17:43:05 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
fn do_one(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
|
2011-07-06 21:00:00 -05:00
|
|
|
for (@expr e in args) { do_one(fcx, e); }
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
fn get_pp(crate_ctxt ccx, &@expr e) -> pre_and_post {
|
|
|
|
ret expr_pp(ccx, e);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-06 21:00:00 -05:00
|
|
|
auto pps = ivec::map[@expr, pre_and_post](bind get_pp(fcx.ccx, _), args);
|
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),
|
|
|
|
seq_postconds(fcx, ivec::map(get_post, pps)));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
|
2011-06-19 15:41:21 -05:00
|
|
|
node_id id) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, index);
|
|
|
|
find_pre_post_block(fcx, body);
|
2011-07-19 19:52:34 -05:00
|
|
|
auto v_init = ninit(l.node.id, l.node.ident);
|
2011-06-19 15:41:21 -05:00
|
|
|
relax_precond_block(fcx, bit_num(fcx, v_init) as node_id, body);
|
2011-07-13 17:44:09 -05:00
|
|
|
|
2011-06-30 12:41:06 -05:00
|
|
|
// Hack: for-loop index variables are frequently ignored,
|
|
|
|
// so we pretend they're used
|
|
|
|
use_var(fcx, l.node.id);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-07-05 01:29:15 -05:00
|
|
|
auto loop_precond = seq_preconds(fcx, ~[expr_pp(fcx.ccx, index),
|
|
|
|
block_pp(fcx.ccx, body)]);
|
2011-06-27 20:12:37 -05:00
|
|
|
auto 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
|
|
|
|
fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
|
2011-06-19 15:41:21 -05:00
|
|
|
&option::t[@expr] maybe_alt, node_id id, &if_ty chck) {
|
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);
|
|
|
|
alt (maybe_alt) {
|
|
|
|
case (none) {
|
2011-06-17 21:07:23 -05:00
|
|
|
alt (chck) {
|
|
|
|
case (if_check) {
|
2011-07-19 19:52:34 -05:00
|
|
|
let sp_constr c = expr_to_constr(fcx.ccx.tcx, antec);
|
2011-06-21 15:16:40 -05:00
|
|
|
gen(fcx, antec.id, c.node);
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
|
2011-07-05 01:29:15 -05:00
|
|
|
auto precond_res = seq_preconds(fcx,
|
|
|
|
~[expr_pp(fcx.ccx, antec), block_pp(fcx.ccx, conseq)]);
|
2011-06-19 15:41:21 -05:00
|
|
|
set_pre_and_post(fcx.ccx, id, precond_res,
|
2011-06-16 13:56:34 -05:00
|
|
|
expr_poststate(fcx.ccx, antec));
|
|
|
|
}
|
|
|
|
case (some(?altern)) {
|
2011-06-17 21:07:23 -05:00
|
|
|
/*
|
|
|
|
if check = if_check, then
|
|
|
|
be sure that the predicate implied by antec
|
|
|
|
is *not* true in the alternative
|
|
|
|
*/
|
2011-06-16 13:56:34 -05:00
|
|
|
find_pre_post_expr(fcx, altern);
|
2011-07-05 01:29:15 -05:00
|
|
|
auto precond_false_case = seq_preconds(fcx,
|
|
|
|
~[expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
|
|
|
|
auto postcond_false_case = seq_postconds(fcx,
|
|
|
|
~[expr_postcond(fcx.ccx, antec),
|
|
|
|
expr_postcond(fcx.ccx, altern)]);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
/* Be sure to set the bit for the check condition here,
|
|
|
|
so that it's *not* set in the alternative. */
|
|
|
|
alt (chck) {
|
|
|
|
case (if_check) {
|
2011-07-19 19:52:34 -05:00
|
|
|
let sp_constr c = expr_to_constr(fcx.ccx.tcx, antec);
|
2011-06-21 15:16:40 -05:00
|
|
|
gen(fcx, antec.id, c.node);
|
2011-06-17 21:07:23 -05:00
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
2011-07-05 01:29:15 -05:00
|
|
|
auto precond_true_case = seq_preconds(fcx,
|
|
|
|
~[expr_pp(fcx.ccx, antec), block_pp(fcx.ccx, conseq)]);
|
|
|
|
auto postcond_true_case = seq_postconds(fcx,
|
|
|
|
~[expr_postcond(fcx.ccx, antec),
|
|
|
|
block_postcond(fcx.ccx, conseq)]);
|
|
|
|
|
|
|
|
auto precond_res = seq_postconds(fcx, ~[precond_true_case,
|
|
|
|
precond_false_case]);
|
2011-06-16 13:56:34 -05:00
|
|
|
auto postcond_res =
|
2011-06-27 20:12:37 -05:00
|
|
|
intersect_states(postcond_true_case, postcond_false_case);
|
2011-06-19 15:41:21 -05:00
|
|
|
set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-06-19 15:41:21 -05:00
|
|
|
fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, node_id larger_id,
|
|
|
|
node_id new_var, &path pth) {
|
|
|
|
alt (node_id_to_def(fcx.ccx, new_var)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
case (some(?d)) {
|
|
|
|
alt (d) {
|
|
|
|
case (def_local(?d_id)) {
|
|
|
|
find_pre_post_expr(fcx, rhs);
|
|
|
|
auto p = expr_pp(fcx.ccx, rhs);
|
2011-06-19 15:41:21 -05:00
|
|
|
set_pre_and_post(fcx.ccx, larger_id, p.precondition,
|
2011-06-15 13:19:50 -05:00
|
|
|
p.postcondition);
|
2011-06-19 15:41:21 -05:00
|
|
|
gen(fcx, larger_id,
|
2011-07-19 19:52:34 -05:00
|
|
|
ninit(d_id._1, path_to_ident(fcx.ccx.tcx, pth)));
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-07-06 21:00:00 -05:00
|
|
|
case (_) { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
}
|
2011-07-06 21:00:00 -05:00
|
|
|
case (_) { 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-07-09 00:05:30 -05:00
|
|
|
fn handle_update(&fn_ctxt fcx, &@expr parent,
|
|
|
|
&@expr lhs, &@expr rhs, oper_type ty) {
|
|
|
|
find_pre_post_expr(fcx, rhs);
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p)) {
|
|
|
|
auto post = expr_postcond(fcx.ccx, parent);
|
|
|
|
auto tmp = tritv_clone(post);
|
2011-07-13 17:44:09 -05:00
|
|
|
|
2011-07-09 00:05:30 -05:00
|
|
|
alt (ty) {
|
|
|
|
case (oper_move) {
|
|
|
|
if (is_path(rhs)) {
|
|
|
|
forget_in_postcond(fcx, parent.id, rhs.id);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (oper_swap) {
|
|
|
|
forget_in_postcond_still_init(fcx, parent.id, lhs.id);
|
|
|
|
forget_in_postcond_still_init(fcx, parent.id, rhs.id);
|
|
|
|
}
|
|
|
|
case (oper_assign) {
|
|
|
|
forget_in_postcond_still_init(fcx, parent.id, lhs.id);
|
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
// pure and assign_op require the lhs to be init'd
|
|
|
|
auto df = node_id_to_def_strict(fcx.ccx.tcx, lhs.id);
|
|
|
|
alt (df) {
|
|
|
|
case (def_local(?d_id)) {
|
2011-07-13 17:44:09 -05:00
|
|
|
auto i =
|
2011-07-19 19:52:34 -05:00
|
|
|
bit_num(fcx, ninit(d_id._1,
|
|
|
|
path_to_ident(fcx.ccx.tcx, p)));
|
2011-07-09 00:05:30 -05:00
|
|
|
require_and_preserve(i, expr_pp(fcx.ccx, lhs));
|
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p);
|
|
|
|
alt (rhs.node) {
|
|
|
|
case (expr_path(?p1)) {
|
2011-07-19 19:52:34 -05:00
|
|
|
auto d = local_node_id_to_local_def_id(fcx, lhs.id);
|
|
|
|
auto d1 = local_node_id_to_local_def_id(fcx, rhs.id);
|
2011-07-09 00:05:30 -05:00
|
|
|
alt (d) {
|
|
|
|
case (some(?id)) {
|
|
|
|
alt (d1) {
|
|
|
|
case (some(?id1)) {
|
|
|
|
auto instlhs =
|
|
|
|
tup(path_to_ident(fcx.ccx.tcx,
|
|
|
|
p), id);
|
|
|
|
auto instrhs =
|
|
|
|
tup(path_to_ident(fcx.ccx.tcx,
|
|
|
|
p1), id1);
|
|
|
|
copy_in_poststate_two(fcx, tmp,
|
|
|
|
post, instlhs, instrhs, ty);
|
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (_) { /* do nothing */ }
|
|
|
|
}
|
|
|
|
}
|
2011-07-13 17:44:09 -05:00
|
|
|
case (_) {
|
2011-07-09 00:05:30 -05:00
|
|
|
find_pre_post_expr(fcx, lhs);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
|
|
|
auto enclosing = fcx.enclosing;
|
2011-06-01 20:10:10 -05:00
|
|
|
auto num_local_vars = num_constraints(enclosing);
|
2011-06-15 13:19:50 -05:00
|
|
|
fn do_rand_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
|
2011-06-25 00:17:17 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (e.node) {
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_call(?operator, ?operands)) {
|
2011-07-06 21:00:00 -05:00
|
|
|
auto args = /* copy */ operands;
|
|
|
|
args += ~[operator];
|
2011-07-05 01:29:15 -05:00
|
|
|
|
2011-06-21 15:16:40 -05:00
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
2011-06-15 17:14:30 -05:00
|
|
|
/* see if the call has any constraints on its type */
|
2011-07-19 19:52:34 -05:00
|
|
|
for (@ty::constr c in constraints_expr(fcx.ccx.tcx, operator))
|
2011-06-16 18:55:46 -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
|
|
|
auto i =
|
2011-07-19 19:52:34 -05:00
|
|
|
bit_num(fcx, substitute_constr_args(fcx.ccx.tcx,
|
|
|
|
args, c));
|
2011-06-25 00:17:17 -05:00
|
|
|
require(i, expr_pp(fcx.ccx, e));
|
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-16 18:55:46 -05:00
|
|
|
|
2011-05-27 22:41:48 -05:00
|
|
|
/* if this is a failing call, its postcondition sets everything */
|
|
|
|
alt (controlflow_expr(fcx.ccx, operator)) {
|
2011-06-21 15:16:40 -05:00
|
|
|
case (noreturn) { set_postcond_false(fcx.ccx, e.id); }
|
2011-05-27 22:41:48 -05:00
|
|
|
case (_) { }
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_spawn(_, _, ?operator, ?operands)) {
|
2011-07-06 21:00:00 -05:00
|
|
|
auto args = /* copy */ operands;
|
|
|
|
args += ~[operator];
|
2011-06-21 15:16:40 -05:00
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_vec(?args, _, _)) {
|
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_tup(?elts)) {
|
|
|
|
find_pre_post_exprs(fcx, elt_exprs(elts), e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_path(?p)) {
|
2011-06-24 12:04:08 -05:00
|
|
|
auto rslt = expr_pp(fcx.ccx, e);
|
|
|
|
clear_pp(rslt);
|
2011-06-21 15:16:40 -05:00
|
|
|
auto df = node_id_to_def_strict(fcx.ccx.tcx, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (df) {
|
|
|
|
case (def_local(?d_id)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
auto i =
|
|
|
|
bit_num(fcx,
|
2011-07-19 19:52:34 -05:00
|
|
|
ninit(d_id._1, path_to_ident(fcx.ccx.tcx, p)));
|
2011-06-30 02:18:41 -05:00
|
|
|
use_var(fcx, d_id._1);
|
2011-06-24 12:04:08 -05:00
|
|
|
require_and_preserve(i, rslt);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (_) {/* nothing to check */ }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_self_method(?v)) { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
case (expr_log(_, ?arg)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_chan(?arg)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_put(?opt)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (opt) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?arg)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (none) { clear_pp(expr_pp(fcx.ccx, e)); }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_fn(?f)) { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
case (expr_block(?b)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_block(fcx, b);
|
2011-05-18 17:43:05 -05:00
|
|
|
auto p = block_pp(fcx.ccx, b);
|
2011-06-21 15:16:40 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_rec(?fields, ?maybe_base)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
auto es = field_exprs(fields);
|
2011-07-06 21:00:00 -05:00
|
|
|
alt (maybe_base) {
|
|
|
|
case (none) { /* no-op */ }
|
|
|
|
case (some(?b)) { es += ~[b]; }
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
find_pre_post_exprs(fcx, es, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_move(?lhs, ?rhs)) {
|
2011-07-09 00:05:30 -05:00
|
|
|
handle_update(fcx, e, lhs, rhs, oper_move);
|
2011-05-27 19:38:52 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_swap(?lhs, ?rhs)) {
|
2011-07-09 00:05:30 -05:00
|
|
|
handle_update(fcx, e, lhs, rhs, oper_swap);
|
2011-06-13 19:34:54 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_assign(?lhs, ?rhs)) {
|
2011-07-09 00:05:30 -05:00
|
|
|
handle_update(fcx, e, lhs, rhs, oper_assign);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_recv(?lhs, ?rhs)) {
|
2011-07-09 00:05:30 -05:00
|
|
|
// note inversion of lhs and rhs
|
|
|
|
handle_update(fcx, e, rhs, lhs, oper_assign);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_assign_op(_, ?lhs, ?rhs)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Different from expr_assign in that the lhs *must*
|
|
|
|
already be initialized */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-06 21:00:00 -05:00
|
|
|
find_pre_post_exprs(fcx, ~[lhs, rhs], e.id);
|
2011-06-25 00:17:17 -05:00
|
|
|
forget_in_postcond_still_init(fcx, e.id, lhs.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_lit(_)) { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
case (expr_ret(?maybe_val)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (maybe_val) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-06-21 15:16:40 -05:00
|
|
|
clear_precond(fcx.ccx, e.id);
|
|
|
|
set_postcond_false(fcx.ccx, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?ret_val)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, ret_val);
|
2011-06-21 15:16:40 -05:00
|
|
|
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
2011-05-18 17:43:05 -05:00
|
|
|
expr_precond(fcx.ccx, ret_val));
|
2011-06-21 15:16:40 -05:00
|
|
|
set_postcond_false(fcx.ccx, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_be(?val)) {
|
|
|
|
find_pre_post_expr(fcx, val);
|
|
|
|
set_pre_and_post(fcx.ccx, e.id, expr_prestate(fcx.ccx, val),
|
2011-06-15 13:19:50 -05:00
|
|
|
false_postcond(num_local_vars));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_if(?antec, ?conseq, ?maybe_alt)) {
|
|
|
|
join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-23 17:15:50 -05:00
|
|
|
case (expr_ternary(_, _, _)) {
|
|
|
|
find_pre_post_expr(fcx, 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)) {
|
|
|
|
find_pre_post_expr(fcx, l);
|
|
|
|
find_pre_post_expr(fcx, r);
|
|
|
|
auto overall_pre = seq_preconds(fcx,
|
2011-07-05 01:29:15 -05:00
|
|
|
~[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
|
2011-06-28 15:07:05 -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));
|
|
|
|
}
|
|
|
|
else {
|
2011-07-06 21:00:00 -05:00
|
|
|
find_pre_post_exprs(fcx, ~[l, r], e.id);
|
2011-06-28 15:07:05 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_send(?l, ?r)) {
|
2011-07-06 21:00:00 -05:00
|
|
|
find_pre_post_exprs(fcx, ~[l, r], e.id);
|
2011-06-19 15:41:21 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_unary(_, ?operand)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, operand);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, operand);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_cast(?operand, _)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, operand);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, operand);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_while(?test, ?body)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, test);
|
|
|
|
find_pre_post_block(fcx, body);
|
2011-06-21 15:16:40 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
2011-07-05 01:29:15 -05:00
|
|
|
seq_preconds(fcx, ~[expr_pp(fcx.ccx, test),
|
|
|
|
block_pp(fcx.ccx, body)]),
|
2011-06-27 20:12:37 -05:00
|
|
|
intersect_states(expr_postcond(fcx.ccx, test),
|
2011-07-05 01:29:15 -05:00
|
|
|
block_postcond(fcx.ccx, body)));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_do_while(?body, ?test)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_block(fcx, body);
|
|
|
|
find_pre_post_expr(fcx, test);
|
2011-07-05 01:29:15 -05:00
|
|
|
auto loop_postcond = seq_postconds(fcx,
|
|
|
|
~[block_postcond(fcx.ccx, body),
|
|
|
|
expr_postcond(fcx.ccx, test)]);
|
|
|
|
/* conservative approximation: if the body
|
2011-05-14 21:02:30 -05:00
|
|
|
could break or cont, the test may never be executed */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
if (has_nonlocal_exits(body)) {
|
|
|
|
loop_postcond = empty_poststate(num_local_vars);
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
2011-06-15 13:19:50 -05:00
|
|
|
seq_preconds(fcx,
|
2011-07-05 01:29:15 -05:00
|
|
|
~[block_pp(fcx.ccx, body),
|
|
|
|
expr_pp(fcx.ccx, test)]),
|
2011-06-13 19:04:15 -05:00
|
|
|
loop_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_for(?d, ?index, ?body)) {
|
|
|
|
find_pre_post_loop(fcx, d, index, body, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_for_each(?d, ?index, ?body)) {
|
|
|
|
find_pre_post_loop(fcx, d, index, body, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_index(?val, ?sub)) {
|
2011-07-06 21:00:00 -05:00
|
|
|
find_pre_post_exprs(fcx, ~[val, sub], e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_alt(?ex, ?alts)) {
|
2011-05-27 22:41:48 -05:00
|
|
|
find_pre_post_expr(fcx, ex);
|
2011-05-14 21:02:30 -05:00
|
|
|
fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
|
|
|
|
find_pre_post_block(fcx, an_alt.block);
|
2011-05-18 17:43:05 -05:00
|
|
|
ret block_pp(fcx.ccx, an_alt.block);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-12 20:34:22 -05:00
|
|
|
auto alt_pps = ~[];
|
|
|
|
for (arm a in alts) { alt_pps += ~[do_an_alt(fcx, a)]; }
|
2011-05-26 18:02:25 -05:00
|
|
|
fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp,
|
2011-05-14 21:02:30 -05:00
|
|
|
&pre_and_post next) -> pre_and_post {
|
2011-07-05 01:29:15 -05:00
|
|
|
union(pp.precondition, seq_preconds(fcx, ~[antec, next]));
|
2011-05-14 21:02:30 -05:00
|
|
|
intersect(pp.postcondition, next.postcondition);
|
|
|
|
ret pp;
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
auto antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
|
|
|
|
auto e_pp =
|
|
|
|
@rec(precondition=empty_prestate(num_local_vars),
|
|
|
|
postcondition=false_postcond(num_local_vars));
|
2011-05-26 18:02:25 -05:00
|
|
|
auto g = bind combine_pp(antec_pp, fcx, _, _);
|
2011-06-15 13:19:50 -05:00
|
|
|
auto alts_overall_pp =
|
2011-07-12 20:34:22 -05:00
|
|
|
ivec::foldl[pre_and_post, pre_and_post](g, e_pp, alt_pps);
|
2011-06-21 15:16:40 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id, alts_overall_pp.precondition,
|
2011-05-18 17:43:05 -05:00
|
|
|
alts_overall_pp.postcondition);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_field(?operator, _)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, operator);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, operator);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-01 13:33:15 -05:00
|
|
|
case (expr_fail(?maybe_val)) {
|
|
|
|
auto prestate;
|
|
|
|
alt (maybe_val) {
|
|
|
|
case (none) { prestate = empty_prestate(num_local_vars); }
|
|
|
|
case (some(?fail_val)) {
|
|
|
|
find_pre_post_expr(fcx, fail_val);
|
|
|
|
prestate = expr_precond(fcx.ccx, fail_val);
|
|
|
|
}
|
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
set_pre_and_post(fcx.ccx, e.id,
|
2011-05-14 21:02:30 -05:00
|
|
|
/* if execution continues after fail,
|
|
|
|
then everything is true! */
|
2011-07-01 13:33:15 -05:00
|
|
|
prestate,
|
2011-06-15 13:19:50 -05:00
|
|
|
false_postcond(num_local_vars));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_assert(?p)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, p);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, p);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-28 18:29:37 -05:00
|
|
|
case (expr_check(_, ?p)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, p);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, p);
|
2011-06-09 11:56:35 -05:00
|
|
|
/* predicate p holds after this expression executes */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-07-19 19:52:34 -05:00
|
|
|
let sp_constr c = expr_to_constr(fcx.ccx.tcx, p);
|
2011-06-21 15:16:40 -05:00
|
|
|
gen(fcx, e.id, c.node);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_if_check(?p, ?conseq, ?maybe_alt)) {
|
|
|
|
join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check);
|
2011-06-16 13:56:34 -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] expr_opt in maybe_args) {
|
|
|
|
alt (expr_opt) {
|
|
|
|
case (none) { /* no-op */ }
|
|
|
|
case (some(?expr)) { args += ~[expr]; }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
args += ~[operator]; /* ??? order of eval? */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-06-21 15:16:40 -05:00
|
|
|
find_pre_post_exprs(fcx, args, e.id);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-21 15:16:40 -05:00
|
|
|
case (expr_break) { clear_pp(expr_pp(fcx.ccx, e)); }
|
|
|
|
case (expr_cont) { clear_pp(expr_pp(fcx.ccx, e)); }
|
2011-06-28 17:54:16 -05:00
|
|
|
case (expr_port(_)) { clear_pp(expr_pp(fcx.ccx, e)); }
|
2011-07-08 18:35:09 -05:00
|
|
|
case (expr_mac(_)) {
|
2011-07-06 17:22:23 -05:00
|
|
|
fcx.ccx.tcx.sess.bug("unexpanded macro");
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-06 13:29:22 -05:00
|
|
|
case (expr_anon_obj(?anon_obj, _)) {
|
2011-05-20 19:41:36 -05:00
|
|
|
alt (anon_obj.with_obj) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?ex)) {
|
2011-05-20 19:41:36 -05:00
|
|
|
find_pre_post_expr(fcx, ex);
|
2011-06-21 15:16:40 -05:00
|
|
|
copy_pre_post(fcx.ccx, e.id, ex);
|
2011-05-20 19:41:36 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (none) { clear_pp(expr_pp(fcx.ccx, e)); }
|
2011-05-20 19:41:36 -05:00
|
|
|
}
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) {
|
|
|
|
log "stmt =";
|
2011-05-14 21:02:30 -05:00
|
|
|
log_stmt(s);
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (s.node) {
|
2011-06-19 15:41:21 -05:00
|
|
|
case (stmt_decl(?adecl, ?id)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (adecl.node) {
|
|
|
|
case (decl_local(?alocal)) {
|
2011-06-16 17:58:25 -05:00
|
|
|
alt (alocal.node.init) {
|
2011-06-15 13:19:50 -05:00
|
|
|
case (some(?an_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
|
|
|
/* LHS always becomes initialized,
|
|
|
|
whether or not this is a move */
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, an_init.expr);
|
2011-07-13 17:44:09 -05:00
|
|
|
copy_pre_post(fcx.ccx, alocal.node.id,
|
2011-06-16 17:58:25 -05:00
|
|
|
an_init.expr);
|
2011-05-14 21:02:30 -05:00
|
|
|
/* Inherit ann from initializer, and add var being
|
|
|
|
initialized to the postcondition */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-06-19 15:41:21 -05:00
|
|
|
copy_pre_post(fcx.ccx, id, an_init.expr);
|
2011-07-09 00:05:30 -05:00
|
|
|
|
|
|
|
alt (an_init.expr.node) {
|
|
|
|
case (expr_path(?p)) {
|
|
|
|
copy_in_postcond(fcx, id,
|
|
|
|
tup(alocal.node.ident,
|
2011-07-19 19:52:34 -05:00
|
|
|
alocal.node.id),
|
2011-07-09 00:05:30 -05:00
|
|
|
tup(path_to_ident(fcx.ccx.tcx, p),
|
2011-07-19 19:52:34 -05:00
|
|
|
an_init.expr.id),
|
|
|
|
op_to_oper_ty(an_init.op));
|
2011-07-09 00:05:30 -05:00
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
|
2011-06-19 15:41:21 -05:00
|
|
|
gen(fcx, id,
|
2011-07-19 19:52:34 -05:00
|
|
|
ninit(alocal.node.id,
|
|
|
|
alocal.node.ident));
|
2011-07-09 00:05:30 -05:00
|
|
|
|
2011-06-25 05:16:48 -05:00
|
|
|
if (an_init.op == init_move &&
|
|
|
|
is_path(an_init.expr)) {
|
|
|
|
forget_in_postcond(fcx, id, an_init.expr.id);
|
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-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (none) {
|
2011-06-19 15:41:21 -05:00
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx,
|
|
|
|
alocal.node.id)
|
|
|
|
.conditions);
|
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx, id)
|
2011-06-16 17:58:25 -05:00
|
|
|
.conditions);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (decl_item(?anitem)) {
|
2011-06-19 15:41:21 -05:00
|
|
|
clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_item(fcx.ccx, *anitem);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-19 15:41:21 -05:00
|
|
|
case (stmt_expr(?e, ?id)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, e);
|
2011-06-19 15:41:21 -05:00
|
|
|
copy_pre_post(fcx.ccx, id, e);
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_block(&fn_ctxt fcx, block b) {
|
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-13 17:44:09 -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-06-15 13:19:50 -05:00
|
|
|
auto nv = num_constraints(fcx.enclosing);
|
|
|
|
fn do_one_(fn_ctxt fcx, &@stmt s) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_stmt(fcx, *s);
|
2011-06-15 13:19:50 -05:00
|
|
|
log "pre_post for stmt:";
|
2011-05-14 21:02:30 -05:00
|
|
|
log_stmt(*s);
|
2011-06-15 13:19:50 -05:00
|
|
|
log "is:";
|
2011-05-18 17:43:05 -05:00
|
|
|
log_pp(stmt_pp(fcx.ccx, *s));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-07-06 21:00:00 -05:00
|
|
|
for (@stmt s in b.node.stmts) { do_one_(fcx, s); }
|
2011-06-15 13:19:50 -05:00
|
|
|
fn do_inner_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
|
2011-05-14 21:02:30 -05:00
|
|
|
auto do_inner = bind do_inner_(fcx, _);
|
|
|
|
option::map[@expr, ()](do_inner, b.node.expr);
|
2011-07-05 01:29:15 -05:00
|
|
|
|
|
|
|
let pre_and_post[] pps = ~[];
|
|
|
|
for (@stmt s in b.node.stmts) { pps += ~[stmt_pp(fcx.ccx, *s)]; }
|
|
|
|
alt (b.node.expr) {
|
|
|
|
case (none) { /* no-op */ }
|
|
|
|
case (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-06-15 13:19:50 -05:00
|
|
|
auto block_precond = seq_preconds(fcx, pps);
|
2011-07-05 01:29:15 -05:00
|
|
|
|
|
|
|
auto postconds = ~[];
|
|
|
|
for (pre_and_post pp in pps) { postconds += ~[get_post(pp)]; }
|
|
|
|
|
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-07-05 01:29:15 -05:00
|
|
|
postconds += ~[block_precond];
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
auto block_postcond = empty_poststate(nv);
|
|
|
|
/* conservative approximation */
|
2011-06-15 13:19:50 -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-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) {
|
2011-06-30 02:18:41 -05:00
|
|
|
// hack
|
|
|
|
use_var(fcx, fcx.id);
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_block(fcx, f.body);
|
2011-05-31 14:24:18 -05:00
|
|
|
|
|
|
|
// Treat the tail expression as a return statement
|
|
|
|
alt (f.body.node.expr) {
|
|
|
|
case (some(?tailexpr)) {
|
2011-06-21 15:16:40 -05:00
|
|
|
set_postcond_false(fcx.ccx, tailexpr.id);
|
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-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-07-12 13:26:14 -05:00
|
|
|
fn fn_pre_post(&_fn f, &ty_param[] tps,
|
|
|
|
&span sp, &fn_ident i, node_id id, &crate_ctxt ccx,
|
|
|
|
&visit::vt[crate_ctxt] v) {
|
|
|
|
visit::visit_fn(f, tps, sp, i, id, ccx, v);
|
2011-05-14 21:02:30 -05:00
|
|
|
assert (ccx.fm.contains_key(id));
|
2011-06-24 17:11:22 -05:00
|
|
|
auto fcx = rec(enclosing=ccx.fm.get(id), id=id,
|
|
|
|
name=fn_ident_to_string(id, i), ccx=ccx);
|
2011-06-15 13:19:50 -05:00
|
|
|
find_pre_post_fn(fcx, f);
|
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
|
|
|
|
// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
|
|
|
|
// End:
|
|
|
|
//
|