2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
import std::bitv;
|
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;
|
|
|
|
import tstate::ann::pre_and_post;
|
|
|
|
import tstate::ann::get_post;
|
|
|
|
import tstate::ann::postcond;
|
|
|
|
import tstate::ann::empty_pre_post;
|
|
|
|
import tstate::ann::empty_poststate;
|
|
|
|
import tstate::ann::require_and_preserve;
|
|
|
|
import tstate::ann::union;
|
|
|
|
import tstate::ann::intersect;
|
|
|
|
import tstate::ann::empty_prestate;
|
|
|
|
import tstate::ann::prestate;
|
|
|
|
import tstate::ann::poststate;
|
|
|
|
import tstate::ann::false_postcond;
|
|
|
|
import tstate::ann::ts_ann;
|
|
|
|
import tstate::ann::extend_prestate;
|
|
|
|
import tstate::ann::extend_poststate;
|
|
|
|
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;
|
|
|
|
import aux::log_bitv;
|
2011-06-17 21:07:23 -05:00
|
|
|
import aux::log_bitv_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;
|
|
|
|
import aux::ann_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;
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
import bitvectors::seq_preconds;
|
|
|
|
import bitvectors::union_postconds;
|
|
|
|
import bitvectors::intersect_postconds;
|
|
|
|
import bitvectors::declare_var;
|
|
|
|
import bitvectors::bit_num;
|
|
|
|
import bitvectors::gen_poststate;
|
2011-05-20 21:50:29 -05:00
|
|
|
import bitvectors::kill_poststate;
|
2011-05-14 21:02:30 -05:00
|
|
|
import front::ast;
|
2011-05-31 20:24:06 -05:00
|
|
|
import front::ast::*;
|
2011-05-31 14:24:18 -05:00
|
|
|
import middle::ty::expr_ann;
|
|
|
|
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::uistr;
|
|
|
|
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-15 13:19:50 -05:00
|
|
|
fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs) ->
|
|
|
|
tup(bool, poststate) {
|
|
|
|
auto changed = false;
|
|
|
|
auto post = pres;
|
|
|
|
for (@expr e in exprs) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, post, e) || changed;
|
|
|
|
post = expr_poststate(fcx.ccx, e);
|
|
|
|
}
|
|
|
|
ret tup(changed, post);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, &ann a,
|
|
|
|
&vec[@expr] es) -> bool {
|
2011-05-14 21:02:30 -05:00
|
|
|
auto res = seq_states(fcx, pres, es);
|
|
|
|
auto changed = res._0;
|
2011-05-18 17:43:05 -05:00
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = extend_poststate_ann(fcx.ccx, a, res._1) || changed;
|
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-15 13:19:50 -05:00
|
|
|
&@expr index, &block body, &ann a) -> bool {
|
2011-05-14 21:02:30 -05:00
|
|
|
auto changed = false;
|
|
|
|
/* same issues as while */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-06-13 19:04:15 -05:00
|
|
|
// FIXME: also want to set l as initialized, no?
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
changed = find_pre_post_state_expr(fcx, pres, index) || changed;
|
|
|
|
/* in general, would need the intersection of
|
|
|
|
(poststate of index, poststate of body) */
|
2011-06-15 13:19:50 -05:00
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body)
|
|
|
|
|| changed;
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
if (has_nonlocal_exits(body)) {
|
|
|
|
changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
auto res_p =
|
|
|
|
intersect_postconds([expr_poststate(fcx.ccx, index),
|
|
|
|
block_poststate(fcx.ccx, body)]);
|
2011-05-18 17:43:05 -05:00
|
|
|
changed = extend_poststate_ann(fcx.ccx, a, res_p) || changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
|
2011-06-13 20:10:33 -05:00
|
|
|
fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool {
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (ann_to_def(fcx.ccx, a_new_var)) {
|
|
|
|
case (some(def_local(?loc))) {
|
|
|
|
ret gen_poststate(fcx, a,
|
|
|
|
rec(id=loc,
|
|
|
|
c=ninit(path_to_ident(fcx.ccx.tcx, p))));
|
|
|
|
}
|
|
|
|
case (_) { ret false; }
|
|
|
|
}
|
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-06-17 21:07:23 -05:00
|
|
|
&option::t[@expr] maybe_alt, &ann a, &if_ty chk,
|
|
|
|
&prestate pres) -> bool {
|
2011-06-16 13:56:34 -05:00
|
|
|
auto changed = false;
|
|
|
|
|
2011-06-17 21:07:23 -05:00
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, antec) || changed;
|
|
|
|
|
|
|
|
/*
|
|
|
|
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-17 21:07:23 -05:00
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
|
|
|
|
conseq) || changed;
|
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, antec))
|
|
|
|
|| changed;
|
|
|
|
}
|
|
|
|
case (some(?altern)) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx,
|
|
|
|
expr_poststate(fcx.ccx,
|
|
|
|
antec),
|
|
|
|
altern) || changed;
|
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);
|
|
|
|
conseq_prestate = bitv::clone(conseq_prestate);
|
|
|
|
bitv::set(conseq_prestate, bit_num(fcx, c.node), true);
|
|
|
|
}
|
|
|
|
case (_) {}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_block(fcx, conseq_prestate, conseq)
|
|
|
|
|| changed;
|
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
auto poststate_res =
|
|
|
|
intersect_postconds([block_poststate(fcx.ccx, conseq),
|
|
|
|
expr_poststate(fcx.ccx,
|
|
|
|
altern)]);
|
2011-06-17 21:07:23 -05:00
|
|
|
/* fcx.ccx.tcx.sess.span_note(antec.span,
|
|
|
|
"poststate_res = " + aux::bitv_to_str(fcx, poststate_res));
|
|
|
|
fcx.ccx.tcx.sess.span_note(antec.span,
|
|
|
|
"altern poststate = " +
|
|
|
|
aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
|
|
|
|
fcx.ccx.tcx.sess.span_note(antec.span,
|
|
|
|
"conseq poststate = " + aux::bitv_to_str(fcx,
|
|
|
|
block_poststate(fcx.ccx, conseq))); */
|
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, poststate_res) ||
|
|
|
|
changed;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
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-15 13:19:50 -05:00
|
|
|
auto changed = false;
|
|
|
|
auto num_local_vars = num_constraints(fcx.enclosing);
|
2011-06-17 21:07:23 -05:00
|
|
|
/*
|
2011-06-15 13:19:50 -05:00
|
|
|
log_err("states:");
|
|
|
|
log_expr_err(*e);
|
2011-06-17 21:07:23 -05:00
|
|
|
aux::log_bitv_err(fcx, expr_prestate(fcx.ccx, e));
|
2011-06-15 13:19:50 -05:00
|
|
|
aux::log_bitv_err(fcx, expr_poststate(fcx.ccx, e));
|
|
|
|
*/
|
|
|
|
|
|
|
|
/* FIXME could get rid of some of the copy/paste */
|
|
|
|
alt (e.node) {
|
|
|
|
case (expr_vec(?elts, _, _, ?a)) {
|
|
|
|
ret find_pre_post_state_exprs(fcx, pres, a, elts);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_tup(?elts, ?a)) {
|
|
|
|
ret find_pre_post_state_exprs(fcx, pres, a, elt_exprs(elts));
|
|
|
|
}
|
|
|
|
case (expr_call(?operator, ?operands, ?a)) {
|
|
|
|
/* do the prestate for the rator */
|
|
|
|
|
2011-06-17 21:07:23 -05:00
|
|
|
/* fcx.ccx.tcx.sess.span_note(operator.span,
|
|
|
|
"pres = " + aux::bitv_to_str(fcx, pres));
|
|
|
|
*/
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, operator) || changed;
|
|
|
|
/* rands go left-to-right */
|
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_exprs(fcx,
|
|
|
|
expr_poststate(fcx.ccx, operator),
|
|
|
|
a, operands) || changed;
|
|
|
|
/* if this is a failing call, it sets everything as initialized */
|
|
|
|
|
|
|
|
alt (controlflow_expr(fcx.ccx, operator)) {
|
|
|
|
case (noreturn) {
|
|
|
|
changed =
|
|
|
|
set_poststate_ann(fcx.ccx, a,
|
|
|
|
false_postcond(num_local_vars)) ||
|
|
|
|
changed;
|
|
|
|
}
|
|
|
|
case (_) { }
|
2011-05-27 19:38:52 -05:00
|
|
|
}
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
/* fcx.ccx.tcx.sess.span_note(operator.span,
|
|
|
|
"pres = " + aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, e)));
|
|
|
|
*/
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-27 19:38:52 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, operator);
|
|
|
|
ret find_pre_post_state_exprs(fcx,
|
|
|
|
expr_poststate(fcx.ccx, operator),
|
|
|
|
a, operands) || changed;
|
|
|
|
}
|
|
|
|
case (expr_bind(?operator, ?maybe_args, ?a)) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, operator) || changed;
|
|
|
|
ret find_pre_post_state_exprs(fcx,
|
|
|
|
expr_poststate(fcx.ccx, operator),
|
|
|
|
a, cat_options[@expr](maybe_args))
|
2011-05-27 19:38:52 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
case (expr_path(_, ?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (expr_log(_, ?e, ?a)) {
|
|
|
|
/* factor out the "one exp" pattern */
|
|
|
|
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, e))
|
2011-05-27 19:38:52 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_chan(?e, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, e))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_ext(_, _, _, ?expanded, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, expanded);
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, expanded)) ||
|
|
|
|
changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_put(?maybe_e, ?a)) {
|
|
|
|
alt (maybe_e) {
|
|
|
|
case (some(?arg)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, arg);
|
|
|
|
changed =
|
|
|
|
extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, arg)) ||
|
|
|
|
changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (none) { ret pure_exp(fcx.ccx, a, pres); }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
case (expr_lit(?l, ?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (
|
|
|
|
// FIXME This was just put in here as a placeholder
|
|
|
|
expr_fn(?f, ?a)) {
|
|
|
|
ret pure_exp(fcx.ccx, a, pres);
|
|
|
|
}
|
|
|
|
case (expr_block(?b, ?a)) {
|
|
|
|
changed = find_pre_post_state_block(fcx, pres, b) || changed;
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, block_poststate(fcx.ccx, b))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_rec(?fields, ?maybe_base, ?a)) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_exprs(fcx, pres, a, field_exprs(fields))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
alt (maybe_base) {
|
|
|
|
case (none) {/* do nothing */ }
|
|
|
|
case (some(?base)) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, base) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, base)) ||
|
|
|
|
changed;
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_move(?lhs, ?rhs, ?a)) {
|
|
|
|
// FIXME: this needs to deinitialize the rhs
|
|
|
|
|
|
|
|
extend_prestate_ann(fcx.ccx, a, pres);
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p, ?a_lhs)) {
|
|
|
|
// assignment to local var
|
|
|
|
|
|
|
|
changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, rhs) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, rhs)) ||
|
|
|
|
changed;
|
|
|
|
changed = gen_if_local(fcx, a_lhs, a, p) || changed;
|
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
// assignment to something that must already have been
|
|
|
|
// init'd
|
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx,
|
|
|
|
expr_poststate(fcx.ccx, lhs),
|
|
|
|
rhs) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, rhs)) ||
|
|
|
|
changed;
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_assign(?lhs, ?rhs, ?a)) {
|
|
|
|
extend_prestate_ann(fcx.ccx, a, pres);
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p, ?a_lhs)) {
|
|
|
|
// assignment to local var
|
|
|
|
|
|
|
|
changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, rhs) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, rhs)) ||
|
|
|
|
changed;
|
|
|
|
changed = gen_if_local(fcx, a_lhs, a, p) || changed;
|
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
// assignment to something that must already have been
|
|
|
|
// init'd
|
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx,
|
|
|
|
expr_poststate(fcx.ccx, lhs),
|
|
|
|
rhs) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, rhs)) ||
|
|
|
|
changed;
|
|
|
|
}
|
2011-05-20 21:50:29 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-20 21:50:29 -05:00
|
|
|
}
|
2011-06-13 19:34:54 -05:00
|
|
|
case (expr_swap(?lhs, ?rhs, ?a)) {
|
|
|
|
/* quite similar to binary -- should abstract this */
|
2011-06-16 18:55:46 -05:00
|
|
|
|
2011-06-13 19:34:54 -05:00
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
2011-06-16 18:55:46 -05:00
|
|
|
changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
2011-06-13 19:34:54 -05:00
|
|
|
changed =
|
2011-06-16 18:55:46 -05:00
|
|
|
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs),
|
2011-06-13 19:34:54 -05:00
|
|
|
rhs) || changed;
|
|
|
|
changed =
|
2011-06-16 18:55:46 -05:00
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, rhs))
|
|
|
|
|| changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_recv(?lhs, ?rhs, ?a)) {
|
|
|
|
extend_prestate_ann(fcx.ccx, a, pres);
|
2011-06-18 22:16:30 -05:00
|
|
|
alt (rhs.node) {
|
|
|
|
case (expr_path(?p, ?a_rhs)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
// receive to local var
|
|
|
|
|
2011-06-18 22:16:30 -05:00
|
|
|
changed = pure_exp(fcx.ccx, a_rhs, pres) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
2011-06-18 22:16:30 -05:00
|
|
|
find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
2011-06-18 22:16:30 -05:00
|
|
|
expr_poststate(fcx.ccx, lhs)) ||
|
2011-06-15 13:19:50 -05:00
|
|
|
changed;
|
2011-06-18 22:16:30 -05:00
|
|
|
changed = gen_if_local(fcx, a_rhs, a, p) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
// receive to something that must already have been init'd
|
|
|
|
|
|
|
|
changed =
|
2011-06-18 22:16:30 -05:00
|
|
|
find_pre_post_state_expr(fcx, pres, rhs) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx,
|
2011-06-18 22:16:30 -05:00
|
|
|
expr_poststate(fcx.ccx, rhs),
|
|
|
|
lhs) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
2011-06-18 22:16:30 -05:00
|
|
|
expr_poststate(fcx.ccx, lhs)) ||
|
2011-06-15 13:19:50 -05:00
|
|
|
changed;
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_ret(?maybe_ret_val, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
/* normally, everything is true if execution continues after
|
|
|
|
a ret expression (since execution never continues locally
|
|
|
|
after a ret expression */
|
|
|
|
|
|
|
|
set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
|
|
|
|
/* return from an always-failing function clears the return bit */
|
|
|
|
|
|
|
|
alt (fcx.enclosing.cf) {
|
|
|
|
case (noreturn) {
|
|
|
|
kill_poststate(fcx, a, rec(id=fcx.id, c=ninit(fcx.name)));
|
|
|
|
}
|
|
|
|
case (_) { }
|
|
|
|
}
|
|
|
|
alt (maybe_ret_val) {
|
|
|
|
case (none) {/* do nothing */ }
|
|
|
|
case (some(?ret_val)) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres, ret_val) ||
|
|
|
|
changed;
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_be(?e, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
|
2011-06-17 21:07:23 -05:00
|
|
|
changed = join_then_else(fcx, antec, conseq, maybe_alt, a,
|
|
|
|
plain_if, pres)
|
2011-06-16 13:56:34 -05:00
|
|
|
|| changed;
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_binary(?bop, ?l, ?r, ?a)) {
|
|
|
|
/* FIXME: what if bop is lazy? */
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, l) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, r))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_send(?l, ?r, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, l) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, r))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_assign_op(?op, ?lhs, ?rhs, ?a)) {
|
|
|
|
/* quite similar to binary -- should abstract this */
|
|
|
|
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs),
|
|
|
|
rhs) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, rhs))
|
2011-05-14 21:02:30 -05:00
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_while(?test, ?body, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
/* to handle general predicates, we need to pass in
|
|
|
|
pres `intersect` (poststate(a))
|
|
|
|
like: auto test_pres = intersect_postconds(pres,
|
|
|
|
expr_postcond(a)); However, this doesn't work right now because
|
|
|
|
we would be passing in an all-zero prestate initially
|
|
|
|
FIXME
|
|
|
|
maybe need a "don't know" state in addition to 0 or 1?
|
|
|
|
*/
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
changed = find_pre_post_state_expr(fcx, pres, test) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
|
|
|
|
body) || changed;
|
2011-06-17 21:07:23 -05:00
|
|
|
/* conservative approximation: if a loop contains a break
|
|
|
|
or cont, we assume nothing about the poststate */
|
|
|
|
if (has_nonlocal_exits(body)) {
|
|
|
|
changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
}
|
|
|
|
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
{
|
|
|
|
auto e_post = expr_poststate(fcx.ccx, test);
|
|
|
|
auto b_post = block_poststate(fcx.ccx, body);
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
intersect_postconds([e_post,
|
2011-06-16 18:55:46 -05:00
|
|
|
b_post])) ||
|
|
|
|
changed
|
2011-06-15 13:19:50 -05:00
|
|
|
};
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_do_while(?body, ?test, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
2011-06-17 21:07:23 -05:00
|
|
|
auto changed0 = changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed = find_pre_post_state_block(fcx, pres, body) || changed;
|
|
|
|
/* 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-17 21:07:23 -05:00
|
|
|
auto breaks = has_nonlocal_exits(body);
|
|
|
|
if (breaks) {
|
|
|
|
// this should probably be true_poststate and not pres,
|
|
|
|
// b/c the body could invalidate stuff
|
|
|
|
// FIXME
|
|
|
|
// This doesn't set "changed", as if the previous state
|
|
|
|
// was different, this might come back true every time
|
|
|
|
set_poststate_ann(fcx.ccx, body.node.a, pres);
|
|
|
|
changed = changed0;
|
|
|
|
}
|
|
|
|
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body),
|
|
|
|
test) || changed;
|
|
|
|
|
|
|
|
if (breaks) {
|
|
|
|
set_poststate_ann(fcx.ccx, a, pres);
|
|
|
|
}
|
|
|
|
else {
|
|
|
|
changed = extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, test)) ||
|
|
|
|
changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_for(?d, ?index, ?body, ?a)) {
|
|
|
|
ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
|
|
|
|
}
|
|
|
|
case (expr_for_each(?d, ?index, ?body, ?a)) {
|
|
|
|
ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
|
|
|
|
}
|
|
|
|
case (expr_index(?e, ?sub, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, e), sub)
|
|
|
|
|| changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, sub));
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_alt(?e, ?alts, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
|
|
|
auto e_post = expr_poststate(fcx.ccx, e);
|
|
|
|
auto a_post;
|
|
|
|
if (vec::len[arm](alts) > 0u) {
|
|
|
|
a_post = false_postcond(num_local_vars);
|
|
|
|
for (arm an_alt in alts) {
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_block(fcx, e_post, an_alt.block)
|
|
|
|
|| changed;
|
|
|
|
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-15 13:19:50 -05:00
|
|
|
changed = extend_poststate_ann(fcx.ccx, a, a_post) || changed;
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_field(?e, _, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, e))
|
|
|
|
|| changed;
|
|
|
|
ret changed;
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_unary(_, ?operand, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, operand) || changed;
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, operand)) ||
|
|
|
|
changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_cast(?operand, _, ?a)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, operand) || changed;
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, operand)) ||
|
|
|
|
changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (expr_fail(?a, _)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
/* if execution continues after fail, then everything is true!
|
|
|
|
woo! */
|
|
|
|
|
|
|
|
changed =
|
|
|
|
set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars))
|
|
|
|
|| changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-17 21:07:23 -05:00
|
|
|
case (expr_assert(?p, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, p) || changed;
|
|
|
|
changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (expr_check(?p, ?a)) {
|
|
|
|
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, p) || changed;
|
|
|
|
changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
/* predicate p holds after this expression executes */
|
|
|
|
|
|
|
|
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
|
|
|
|
changed = gen_poststate(fcx, a, c.node) || changed;
|
|
|
|
ret changed;
|
2011-06-16 13:56:34 -05:00
|
|
|
}
|
|
|
|
case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) {
|
2011-06-17 21:07:23 -05:00
|
|
|
changed = join_then_else(fcx, p, conseq, maybe_alt, a, if_check,
|
|
|
|
pres)
|
2011-06-16 13:56:34 -05:00
|
|
|
|| changed;
|
2011-06-17 21:07:23 -05:00
|
|
|
|
2011-06-16 13:56:34 -05:00
|
|
|
ret changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
|
|
|
case (expr_break(?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (expr_cont(?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (expr_port(?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (expr_self_method(_, ?a)) { ret pure_exp(fcx.ccx, a, pres); }
|
|
|
|
case (expr_anon_obj(?anon_obj, _, _, ?a)) {
|
|
|
|
alt (anon_obj.with_obj) {
|
|
|
|
case (some(?e)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e);
|
|
|
|
changed =
|
|
|
|
extend_prestate_ann(fcx.ccx, a, pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate_ann(fcx.ccx, a,
|
|
|
|
expr_poststate(fcx.ccx, e)) ||
|
|
|
|
changed;
|
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
case (none) { ret pure_exp(fcx.ccx, a, 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 changed = false;
|
|
|
|
auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
/*
|
|
|
|
log_err "*At beginning: stmt = ";
|
|
|
|
log_stmt_err(*s);
|
|
|
|
log_err "*prestate = ";
|
|
|
|
log_err bitv::to_str(stmt_ann.states.prestate);
|
|
|
|
log_err "*poststate =";
|
|
|
|
log_err bitv::to_str(stmt_ann.states.poststate);
|
|
|
|
log_err "*changed =";
|
|
|
|
log_err changed;
|
|
|
|
*/
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
alt (s.node) {
|
|
|
|
case (stmt_decl(?adecl, ?a)) {
|
|
|
|
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-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_prestate(stmt_ann.states.prestate,
|
|
|
|
pres) || changed;
|
|
|
|
changed =
|
|
|
|
find_pre_post_state_expr(fcx, pres,
|
2011-06-16 17:58:25 -05:00
|
|
|
an_init.expr)
|
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_poststate(stmt_ann.states.poststate,
|
|
|
|
expr_poststate(fcx.ccx,
|
|
|
|
an_init.expr))
|
|
|
|
|| changed;
|
|
|
|
changed =
|
|
|
|
gen_poststate(fcx, a,
|
2011-06-16 17:58:25 -05:00
|
|
|
rec(id=alocal.node.id,
|
|
|
|
c=ninit(alocal.node.ident)))
|
|
|
|
|| changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
log "Summary: stmt = ";
|
2011-05-18 17:43:05 -05:00
|
|
|
log_stmt(*s);
|
2011-06-15 13:19:50 -05:00
|
|
|
log "prestate = ";
|
|
|
|
log bitv::to_str(stmt_ann.states.prestate);
|
2011-05-26 18:02:25 -05:00
|
|
|
log_bitv(fcx, stmt_ann.states.prestate);
|
2011-06-15 13:19:50 -05:00
|
|
|
log "poststate =";
|
2011-05-26 18:02:25 -05:00
|
|
|
log_bitv(fcx, stmt_ann.states.poststate);
|
2011-06-15 13:19:50 -05:00
|
|
|
log "changed =";
|
|
|
|
log changed;
|
2011-05-18 17:43:05 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_prestate(stmt_ann.states.prestate,
|
|
|
|
pres) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate(stmt_ann.states.poststate,
|
|
|
|
pres) || changed;
|
2011-05-18 17:43:05 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (decl_item(?an_item)) {
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_prestate(stmt_ann.states.prestate, pres) ||
|
|
|
|
changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate(stmt_ann.states.poststate, pres) ||
|
|
|
|
changed;
|
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-18 20:03:48 -05:00
|
|
|
ret changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
2011-05-18 17:43:05 -05:00
|
|
|
case (stmt_expr(?e, _)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
2011-06-15 13:19:50 -05:00
|
|
|
changed =
|
|
|
|
extend_prestate(stmt_ann.states.prestate,
|
|
|
|
expr_prestate(fcx.ccx, e)) || changed;
|
|
|
|
changed =
|
|
|
|
extend_poststate(stmt_ann.states.poststate,
|
|
|
|
expr_poststate(fcx.ccx, e)) || changed;
|
2011-05-18 17:43:05 -05:00
|
|
|
/*
|
|
|
|
log("Summary: stmt = ");
|
2011-05-14 21:02:30 -05:00
|
|
|
log_stmt(*s);
|
|
|
|
log("prestate = ");
|
|
|
|
log(bitv::to_str(stmt_ann.states.prestate));
|
|
|
|
log_bitv(enclosing, stmt_ann.states.prestate);
|
|
|
|
log("poststate =");
|
|
|
|
log(bitv::to_str(stmt_ann.states.poststate));
|
|
|
|
log_bitv(enclosing, stmt_ann.states.poststate);
|
|
|
|
log("changed =");
|
|
|
|
log(changed);
|
2011-05-18 17:43:05 -05:00
|
|
|
*/
|
2011-06-15 13:19:50 -05:00
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
ret changed;
|
|
|
|
}
|
|
|
|
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-15 13:19:50 -05:00
|
|
|
fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) ->
|
|
|
|
bool {
|
|
|
|
auto changed = false;
|
|
|
|
auto num_local_vars = num_constraints(fcx.enclosing);
|
|
|
|
/* 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. */
|
|
|
|
|
|
|
|
for (@stmt s in b.node.stmts) {
|
|
|
|
changed = find_pre_post_state_stmt(fcx, pres, s) || changed;
|
|
|
|
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)) {
|
|
|
|
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
|
|
|
post = expr_poststate(fcx.ccx, e);
|
|
|
|
}
|
|
|
|
}
|
2011-06-17 21:07:23 -05:00
|
|
|
|
|
|
|
set_prestate_ann(fcx.ccx, b.node.a, pres0);
|
|
|
|
set_poststate_ann(fcx.ccx, b.node.a, post);
|
|
|
|
|
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:";
|
|
|
|
log_bitv_err(fcx, pres0);
|
|
|
|
log_err "post:";
|
|
|
|
log_bitv_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-15 13:19:50 -05:00
|
|
|
auto changed =
|
|
|
|
find_pre_post_state_block(fcx, empty_prestate(num_local_vars),
|
|
|
|
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 tailann = expr_ann(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);
|
|
|
|
set_poststate_ann(fcx.ccx, tailann, p);
|
|
|
|
// be sure to set the block poststate to the same thing
|
|
|
|
set_poststate_ann(fcx.ccx, f.body.node.a, p);
|
2011-05-31 14:24:18 -05:00
|
|
|
alt (fcx.enclosing.cf) {
|
|
|
|
case (noreturn) {
|
2011-06-13 20:10:33 -05:00
|
|
|
kill_poststate(fcx, tailann,
|
|
|
|
rec(id=fcx.id, c=ninit(fcx.name)));
|
2011-05-31 14:24:18 -05:00
|
|
|
}
|
|
|
|
case (_) { }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-15 13:19:50 -05:00
|
|
|
case (none) {/* fallthrough */ }
|
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:
|
|
|
|
//
|