rustc: Remove middle/tstate
I feel like I've done this before
This commit is contained in:
Brian Anderson
parent
f5be40384f
commit
a51a561852
@ -1,76 +0,0 @@
|
||||
|
||||
use syntax::ast::*;
|
||||
use syntax::visit;
|
||||
use syntax::codemap::span;
|
||||
use syntax::print::pprust::stmt_to_str;
|
||||
use aux::{num_constraints, get_fn_info, crate_ctxt, add_node};
|
||||
use ann::empty_ann;
|
||||
use pat_util::pat_binding_ids;
|
||||
|
||||
fn collect_ids_expr(e: @expr, rs: @mut ~[node_id]) { vec::push(*rs, e.id); }
|
||||
|
||||
fn collect_ids_block(b: blk, rs: @mut ~[node_id]) {
|
||||
vec::push(*rs, b.node.id);
|
||||
}
|
||||
|
||||
fn collect_ids_stmt(s: @stmt, rs: @mut ~[node_id]) {
|
||||
match s.node {
|
||||
stmt_decl(_, id) | stmt_expr(_, id) | stmt_semi(_, id) {
|
||||
debug!("node_id %s", int::str(id));
|
||||
debug!("%s", stmt_to_str(*s));
|
||||
vec::push(*rs, id);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn collect_ids_local(tcx: ty::ctxt, l: @local, rs: @mut ~[node_id]) {
|
||||
vec::push_all(*rs, pat_binding_ids(tcx.def_map, l.node.pat));
|
||||
}
|
||||
|
||||
fn node_ids_in_fn(tcx: ty::ctxt, body: blk, rs: @mut ~[node_id]) {
|
||||
let collect_ids =
|
||||
visit::mk_simple_visitor(@{visit_expr: |a| collect_ids_expr(a, rs),
|
||||
visit_block: |a| collect_ids_block(a, rs),
|
||||
visit_stmt: |a| collect_ids_stmt(a, rs),
|
||||
visit_local: |a|
|
||||
collect_ids_local(tcx, a, rs)
|
||||
with *visit::default_simple_visitor()});
|
||||
collect_ids.visit_block(body, (), collect_ids);
|
||||
}
|
||||
|
||||
fn init_vecs(ccx: crate_ctxt, node_ids: ~[node_id], len: uint) {
|
||||
for node_ids.each |i| {
|
||||
log(debug, int::str(i) + ~" |-> " + uint::str(len));
|
||||
add_node(ccx, *i, empty_ann(len));
|
||||
}
|
||||
}
|
||||
|
||||
fn visit_fn(ccx: crate_ctxt, num_constraints: uint, body: blk) {
|
||||
let node_ids: @mut ~[node_id] = @mut ~[];
|
||||
node_ids_in_fn(ccx.tcx, body, node_ids);
|
||||
let node_id_vec = *node_ids;
|
||||
init_vecs(ccx, node_id_vec, num_constraints);
|
||||
}
|
||||
|
||||
fn annotate_in_fn(ccx: crate_ctxt, _fk: visit::fn_kind, _decl: fn_decl,
|
||||
body: blk, _sp: span, id: node_id) {
|
||||
let f_info = get_fn_info(ccx, id);
|
||||
visit_fn(ccx, num_constraints(f_info), body);
|
||||
}
|
||||
|
||||
fn annotate_crate(ccx: crate_ctxt, crate: crate) {
|
||||
let do_ann =
|
||||
visit::mk_simple_visitor(
|
||||
@{visit_fn: |a,b,c,d,e| annotate_in_fn(ccx, a, b, c, d, e)
|
||||
with *visit::default_simple_visitor()});
|
||||
visit::visit_crate(crate, (), do_ann);
|
||||
}
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -1,988 +0,0 @@
|
||||
use option::*;
|
||||
use pat_util::*;
|
||||
use syntax::ast::*;
|
||||
use syntax::ast_util::*;
|
||||
use syntax::{visit, codemap};
|
||||
use codemap::span;
|
||||
use std::map::{hashmap, int_hash};
|
||||
use syntax::print::pprust::path_to_str;
|
||||
use tstate::ann::{pre_and_post, pre_and_post_state, empty_ann, prestate,
|
||||
poststate, precond, postcond,
|
||||
set_prestate, set_poststate, set_in_poststate_,
|
||||
extend_prestate, extend_poststate, set_precondition,
|
||||
set_postcondition, ts_ann,
|
||||
clear_in_postcond,
|
||||
clear_in_poststate_};
|
||||
use driver::session::session;
|
||||
use dvec::{dvec, extensions};
|
||||
use tritv::{trit, tfalse, ttrue, dont_care, t};
|
||||
|
||||
use syntax::print::pprust::{constr_args_to_str, lit_to_str};
|
||||
|
||||
// Used to communicate which operands should be invalidated
|
||||
// to helper functions
|
||||
enum oper_type {
|
||||
oper_move,
|
||||
oper_swap,
|
||||
oper_assign,
|
||||
oper_assign_op,
|
||||
oper_pure,
|
||||
}
|
||||
|
||||
/* logging funs */
|
||||
fn def_id_to_str(d: def_id) -> ~str {
|
||||
return int::str(d.crate) + ~"," + int::str(d.node);
|
||||
}
|
||||
|
||||
fn comma_str(args: ~[@constr_arg_use]) -> ~str {
|
||||
let mut rslt = ~"";
|
||||
let mut comma = false;
|
||||
for args.each |a| {
|
||||
if comma { rslt += ~", "; } else { comma = true; }
|
||||
match a.node {
|
||||
carg_base { rslt += ~"*"; }
|
||||
carg_ident(i) { rslt += *i.ident; }
|
||||
carg_lit(l) { rslt += lit_to_str(l); }
|
||||
}
|
||||
}
|
||||
return rslt;
|
||||
}
|
||||
|
||||
fn constraint_to_str(tcx: ty::ctxt, c: sp_constr) -> ~str {
|
||||
return fmt!("%s(%s) - arising from %s",
|
||||
path_to_str(c.node.path),
|
||||
comma_str(c.node.args),
|
||||
codemap::span_to_str(c.span, tcx.sess.codemap));
|
||||
}
|
||||
|
||||
fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> ~str {
|
||||
let mut s = ~"";
|
||||
let mut comma = false;
|
||||
for constraints(fcx).each |p| {
|
||||
match v.get(p.bit_num) {
|
||||
dont_care { }
|
||||
tt {
|
||||
s +=
|
||||
if comma { ~", " } else { comma = true; ~"" } +
|
||||
if tt == tfalse { ~"!" } else { ~"" } +
|
||||
constraint_to_str(fcx.ccx.tcx, p.c);
|
||||
}
|
||||
}
|
||||
}
|
||||
return s;
|
||||
}
|
||||
|
||||
fn log_tritv(fcx: fn_ctxt, v: tritv::t) {
|
||||
log(debug, tritv_to_str(fcx, v));
|
||||
}
|
||||
|
||||
fn first_difference_string(fcx: fn_ctxt, expected: tritv::t, actual: tritv::t)
|
||||
-> ~str {
|
||||
let mut s = ~"";
|
||||
for constraints(fcx).each |c| {
|
||||
if expected.get(c.bit_num) == ttrue &&
|
||||
actual.get(c.bit_num) != ttrue {
|
||||
s = constraint_to_str(fcx.ccx.tcx, c.c);
|
||||
break;
|
||||
}
|
||||
}
|
||||
return s;
|
||||
}
|
||||
|
||||
fn log_tritv_err(fcx: fn_ctxt, v: tritv::t) {
|
||||
log(error, tritv_to_str(fcx, v));
|
||||
}
|
||||
|
||||
fn tos(v: ~[uint]) -> ~str {
|
||||
let mut rslt = ~"";
|
||||
for v.each |i| {
|
||||
if i == 0u {
|
||||
rslt += ~"0";
|
||||
} else if i == 1u { rslt += ~"1"; } else { rslt += ~"?"; }
|
||||
}
|
||||
return rslt;
|
||||
}
|
||||
|
||||
fn log_cond(v: ~[uint]) { log(debug, tos(v)); }
|
||||
|
||||
fn log_cond_err(v: ~[uint]) { log(error, tos(v)); }
|
||||
|
||||
fn log_pp(pp: pre_and_post) {
|
||||
let p1 = pp.precondition.to_vec();
|
||||
let p2 = pp.postcondition.to_vec();
|
||||
debug!("pre:");
|
||||
log_cond(p1);
|
||||
debug!("post:");
|
||||
log_cond(p2);
|
||||
}
|
||||
|
||||
fn log_pp_err(pp: pre_and_post) {
|
||||
let p1 = pp.precondition.to_vec();
|
||||
let p2 = pp.postcondition.to_vec();
|
||||
error!("pre:");
|
||||
log_cond_err(p1);
|
||||
error!("post:");
|
||||
log_cond_err(p2);
|
||||
}
|
||||
|
||||
fn log_states(pp: pre_and_post_state) {
|
||||
let p1 = pp.prestate.to_vec();
|
||||
let p2 = pp.poststate.to_vec();
|
||||
debug!("prestate:");
|
||||
log_cond(p1);
|
||||
debug!("poststate:");
|
||||
log_cond(p2);
|
||||
}
|
||||
|
||||
fn log_states_err(pp: pre_and_post_state) {
|
||||
let p1 = pp.prestate.to_vec();
|
||||
let p2 = pp.poststate.to_vec();
|
||||
error!("prestate:");
|
||||
log_cond_err(p1);
|
||||
error!("poststate:");
|
||||
log_cond_err(p2);
|
||||
}
|
||||
|
||||
fn print_ident(i: ident) { log(debug, ~" " + *i + ~" "); }
|
||||
|
||||
fn print_idents(&idents: ~[ident]) {
|
||||
if vec::len::<ident>(idents) == 0u { return; }
|
||||
log(debug, ~"an ident: " + *vec::pop::<ident>(idents));
|
||||
print_idents(idents);
|
||||
}
|
||||
|
||||
|
||||
/* data structures */
|
||||
|
||||
/**********************************************************************/
|
||||
|
||||
/* Two different data structures represent constraints in different
|
||||
contexts: constraint and norm_constraint.
|
||||
|
||||
constraint gets used to record constraints in a table keyed by def_ids. Each
|
||||
constraint has a single operator but a list of possible argument lists, and
|
||||
thus represents several constraints at once, one for each possible argument
|
||||
list.
|
||||
|
||||
norm_constraint, in contrast, gets used when handling an instance of a
|
||||
constraint rather than a definition of a constraint. It has only a single
|
||||
argument list.
|
||||
|
||||
The representation of constraints, where multiple instances of the
|
||||
same predicate are collapsed into one entry in the table, makes it
|
||||
easier to look up a specific instance.
|
||||
|
||||
Both types are in constrast with the constraint type defined in
|
||||
syntax::ast, which is for predicate constraints only, and is what
|
||||
gets generated by the parser. aux and ast share the same type
|
||||
to represent predicate *arguments* however. This type
|
||||
(constr_arg_general) is parameterized (see comments in syntax::ast).
|
||||
|
||||
Both types store an ident and span, for error-logging purposes.
|
||||
*/
|
||||
type pred_args_ = {args: ~[@constr_arg_use], bit_num: uint};
|
||||
|
||||
type pred_args = spanned<pred_args_>;
|
||||
|
||||
// The attached node ID is the *defining* node ID
|
||||
// for this local.
|
||||
type constr_arg_use = spanned<constr_arg_general_<inst>>;
|
||||
|
||||
/* Predicate constraints refer to the truth value of a predicate on variables
|
||||
(definitely false, maybe true, or definitely true). The <path> field (and the
|
||||
<def_id> field in the npred constructor) names a user-defined function that
|
||||
may be the operator in a "check" expression in the source. */
|
||||
|
||||
type constraint = {
|
||||
path: @path,
|
||||
// FIXME (#2539): really only want it to be mut during
|
||||
// collect_locals. freeze it after that.
|
||||
descs: @dvec<pred_args>
|
||||
};
|
||||
|
||||
type tsconstr = {
|
||||
path: @path,
|
||||
def_id: def_id,
|
||||
args: ~[@constr_arg_use]
|
||||
};
|
||||
|
||||
type sp_constr = spanned<tsconstr>;
|
||||
|
||||
type norm_constraint = {bit_num: uint, c: sp_constr};
|
||||
|
||||
type constr_map = std::map::hashmap<def_id, constraint>;
|
||||
|
||||
/* Contains stuff that has to be computed up front */
|
||||
/* For easy access, the fn_info stores two special constraints for each
|
||||
function. So we need context. And so it seems clearer to just have separate
|
||||
constraints. */
|
||||
type fn_info =
|
||||
/* list, accumulated during pre/postcondition
|
||||
computation, of all local variables that may be
|
||||
used */
|
||||
// Doesn't seem to work without the @ -- bug
|
||||
{constrs: constr_map,
|
||||
num_constraints: uint,
|
||||
cf: ret_style,
|
||||
used_vars: @mut ~[node_id],
|
||||
ignore: bool};
|
||||
|
||||
/* mapping from node ID to typestate annotation */
|
||||
type node_ann_table = @mut ~[mut ts_ann];
|
||||
|
||||
|
||||
/* mapping from function name to fn_info map */
|
||||
type fn_info_map = std::map::hashmap<node_id, fn_info>;
|
||||
|
||||
type fn_ctxt =
|
||||
{enclosing: fn_info, id: node_id, name: ident, ccx: crate_ctxt};
|
||||
|
||||
type crate_ctxt = {tcx: ty::ctxt, node_anns: node_ann_table, fm: fn_info_map};
|
||||
|
||||
fn get_fn_info(ccx: crate_ctxt, id: node_id) -> fn_info {
|
||||
assert (ccx.fm.contains_key(id));
|
||||
return ccx.fm.get(id);
|
||||
}
|
||||
|
||||
fn add_node(ccx: crate_ctxt, i: node_id, a: ts_ann) {
|
||||
let sz = vec::len(*ccx.node_anns);
|
||||
if sz <= i as uint {
|
||||
vec::grow(*ccx.node_anns, (i as uint) - sz + 1u, empty_ann(0u));
|
||||
}
|
||||
ccx.node_anns[i] = a;
|
||||
}
|
||||
|
||||
fn get_ts_ann(ccx: crate_ctxt, i: node_id) -> Option<ts_ann> {
|
||||
if i as uint < vec::len(*ccx.node_anns) {
|
||||
return some::<ts_ann>(ccx.node_anns[i]);
|
||||
} else { return none::<ts_ann>; }
|
||||
}
|
||||
|
||||
|
||||
/********* utils ********/
|
||||
fn node_id_to_ts_ann(ccx: crate_ctxt, id: node_id) -> ts_ann {
|
||||
match get_ts_ann(ccx, id) {
|
||||
none {
|
||||
error!("node_id_to_ts_ann: no ts_ann for node_id %d", id);
|
||||
fail;
|
||||
}
|
||||
Some(tt) { return tt; }
|
||||
}
|
||||
}
|
||||
|
||||
fn node_id_to_poststate(ccx: crate_ctxt, id: node_id) -> poststate {
|
||||
debug!("node_id_to_poststate");
|
||||
return node_id_to_ts_ann(ccx, id).states.poststate;
|
||||
}
|
||||
|
||||
fn stmt_to_ann(ccx: crate_ctxt, s: stmt) -> ts_ann {
|
||||
debug!("stmt_to_ann");
|
||||
match s.node {
|
||||
stmt_decl(_, id) | stmt_expr(_, id) | stmt_semi(_, id) {
|
||||
return node_id_to_ts_ann(ccx, id);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_states(ccx: crate_ctxt, e: @expr) -> pre_and_post_state {
|
||||
debug!("expr_states");
|
||||
return node_id_to_ts_ann(ccx, e.id).states;
|
||||
}
|
||||
|
||||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_pp(ccx: crate_ctxt, e: @expr) -> pre_and_post {
|
||||
debug!("expr_pp");
|
||||
return node_id_to_ts_ann(ccx, e.id).conditions;
|
||||
}
|
||||
|
||||
fn stmt_pp(ccx: crate_ctxt, s: stmt) -> pre_and_post {
|
||||
return stmt_to_ann(ccx, s).conditions;
|
||||
}
|
||||
|
||||
|
||||
/* fails if b has no annotation */
|
||||
fn block_pp(ccx: crate_ctxt, b: blk) -> pre_and_post {
|
||||
debug!("block_pp");
|
||||
return node_id_to_ts_ann(ccx, b.node.id).conditions;
|
||||
}
|
||||
|
||||
fn clear_pp(pp: pre_and_post) {
|
||||
ann::clear(pp.precondition);
|
||||
ann::clear(pp.postcondition);
|
||||
}
|
||||
|
||||
fn clear_precond(ccx: crate_ctxt, id: node_id) {
|
||||
let pp = node_id_to_ts_ann(ccx, id);
|
||||
ann::clear(pp.conditions.precondition);
|
||||
}
|
||||
|
||||
fn block_states(ccx: crate_ctxt, b: blk) -> pre_and_post_state {
|
||||
debug!("block_states");
|
||||
return node_id_to_ts_ann(ccx, b.node.id).states;
|
||||
}
|
||||
|
||||
fn stmt_states(ccx: crate_ctxt, s: stmt) -> pre_and_post_state {
|
||||
return stmt_to_ann(ccx, s).states;
|
||||
}
|
||||
|
||||
fn expr_precond(ccx: crate_ctxt, e: @expr) -> precond {
|
||||
return expr_pp(ccx, e).precondition;
|
||||
}
|
||||
|
||||
fn expr_postcond(ccx: crate_ctxt, e: @expr) -> postcond {
|
||||
return expr_pp(ccx, e).postcondition;
|
||||
}
|
||||
|
||||
fn expr_prestate(ccx: crate_ctxt, e: @expr) -> prestate {
|
||||
return expr_states(ccx, e).prestate;
|
||||
}
|
||||
|
||||
fn expr_poststate(ccx: crate_ctxt, e: @expr) -> poststate {
|
||||
return expr_states(ccx, e).poststate;
|
||||
}
|
||||
|
||||
fn stmt_precond(ccx: crate_ctxt, s: stmt) -> precond {
|
||||
return stmt_pp(ccx, s).precondition;
|
||||
}
|
||||
|
||||
fn stmt_postcond(ccx: crate_ctxt, s: stmt) -> postcond {
|
||||
return stmt_pp(ccx, s).postcondition;
|
||||
}
|
||||
|
||||
fn states_to_poststate(ss: pre_and_post_state) -> poststate {
|
||||
return ss.poststate;
|
||||
}
|
||||
|
||||
fn stmt_prestate(ccx: crate_ctxt, s: stmt) -> prestate {
|
||||
return stmt_states(ccx, s).prestate;
|
||||
}
|
||||
|
||||
fn stmt_poststate(ccx: crate_ctxt, s: stmt) -> poststate {
|
||||
return stmt_states(ccx, s).poststate;
|
||||
}
|
||||
|
||||
fn block_precond(ccx: crate_ctxt, b: blk) -> precond {
|
||||
return block_pp(ccx, b).precondition;
|
||||
}
|
||||
|
||||
fn block_postcond(ccx: crate_ctxt, b: blk) -> postcond {
|
||||
return block_pp(ccx, b).postcondition;
|
||||
}
|
||||
|
||||
fn block_prestate(ccx: crate_ctxt, b: blk) -> prestate {
|
||||
return block_states(ccx, b).prestate;
|
||||
}
|
||||
|
||||
fn block_poststate(ccx: crate_ctxt, b: blk) -> poststate {
|
||||
return block_states(ccx, b).poststate;
|
||||
}
|
||||
|
||||
fn set_prestate_ann(ccx: crate_ctxt, id: node_id, pre: prestate) -> bool {
|
||||
debug!("set_prestate_ann");
|
||||
return set_prestate(node_id_to_ts_ann(ccx, id), pre);
|
||||
}
|
||||
|
||||
fn extend_prestate_ann(ccx: crate_ctxt, id: node_id, pre: prestate) -> bool {
|
||||
debug!("extend_prestate_ann");
|
||||
return extend_prestate(node_id_to_ts_ann(ccx, id).states.prestate, pre);
|
||||
}
|
||||
|
||||
fn set_poststate_ann(ccx: crate_ctxt, id: node_id, post: poststate) -> bool {
|
||||
debug!("set_poststate_ann");
|
||||
return set_poststate(node_id_to_ts_ann(ccx, id), post);
|
||||
}
|
||||
|
||||
fn extend_poststate_ann(ccx: crate_ctxt, id: node_id, post: poststate) ->
|
||||
bool {
|
||||
debug!("extend_poststate_ann");
|
||||
return extend_poststate(
|
||||
node_id_to_ts_ann(ccx, id).states.poststate, post);
|
||||
}
|
||||
|
||||
fn set_pre_and_post(ccx: crate_ctxt, id: node_id, pre: precond,
|
||||
post: postcond) {
|
||||
debug!("set_pre_and_post");
|
||||
let tt = node_id_to_ts_ann(ccx, id);
|
||||
set_precondition(tt, pre);
|
||||
set_postcondition(tt, post);
|
||||
}
|
||||
|
||||
fn copy_pre_post(ccx: crate_ctxt, id: node_id, sub: @expr) {
|
||||
debug!("set_pre_and_post");
|
||||
let p = expr_pp(ccx, sub);
|
||||
copy_pre_post_(ccx, id, p.precondition, p.postcondition);
|
||||
}
|
||||
|
||||
fn copy_pre_post_(ccx: crate_ctxt, id: node_id, pre: prestate,
|
||||
post: poststate) {
|
||||
debug!("set_pre_and_post");
|
||||
let tt = node_id_to_ts_ann(ccx, id);
|
||||
set_precondition(tt, pre);
|
||||
set_postcondition(tt, post);
|
||||
}
|
||||
|
||||
/* sets all bits to *1* */
|
||||
fn set_postcond_false(ccx: crate_ctxt, id: node_id) {
|
||||
let p = node_id_to_ts_ann(ccx, id);
|
||||
ann::set(p.conditions.postcondition);
|
||||
}
|
||||
|
||||
fn pure_exp(ccx: crate_ctxt, id: node_id, p: prestate) -> bool {
|
||||
return set_prestate_ann(ccx, id, p) | set_poststate_ann(ccx, id, p);
|
||||
}
|
||||
|
||||
fn num_constraints(m: fn_info) -> uint { return m.num_constraints; }
|
||||
|
||||
fn new_crate_ctxt(cx: ty::ctxt) -> crate_ctxt {
|
||||
let na: ~[mut ts_ann] = ~[mut];
|
||||
return {tcx: cx, node_anns: @mut na, fm: int_hash::<fn_info>()};
|
||||
}
|
||||
|
||||
/* Use e's type to determine whether it returns.
|
||||
If it has a function type with a ! annotation,
|
||||
the answer is noreturn. */
|
||||
fn controlflow_expr(ccx: crate_ctxt, e: @expr) -> ret_style {
|
||||
match ty::get(ty::node_id_to_type(ccx.tcx, e.id)).struct {
|
||||
ty::ty_fn(f) { return f.ret_style; }
|
||||
_ { return return_val; }
|
||||
}
|
||||
}
|
||||
|
||||
fn constraints_expr(cx: ty::ctxt, e: @expr) -> ~[@ty::constr] {
|
||||
match ty::get(ty::node_id_to_type(cx, e.id)).struct {
|
||||
ty::ty_fn(f) { return f.constraints; }
|
||||
_ { return ~[]; }
|
||||
}
|
||||
}
|
||||
|
||||
fn node_id_to_def_strict(cx: ty::ctxt, id: node_id) -> def {
|
||||
match cx.def_map.find(id) {
|
||||
none {
|
||||
error!("node_id_to_def: node_id %d has no def", id);
|
||||
fail;
|
||||
}
|
||||
Some(d) { return d; }
|
||||
}
|
||||
}
|
||||
|
||||
fn node_id_to_def(ccx: crate_ctxt, id: node_id) -> Option<def> {
|
||||
return ccx.tcx.def_map.find(id);
|
||||
}
|
||||
|
||||
fn norm_a_constraint(id: def_id, c: constraint) -> ~[norm_constraint] {
|
||||
let mut rslt: ~[norm_constraint] = ~[];
|
||||
for (*c.descs).each |pd| {
|
||||
vec::push(rslt,
|
||||
{bit_num: pd.node.bit_num,
|
||||
c: respan(pd.span, {path: c.path,
|
||||
def_id: id,
|
||||
args: pd.node.args})});
|
||||
}
|
||||
return rslt;
|
||||
}
|
||||
|
||||
|
||||
// Tried to write this as an iterator, but I got a
|
||||
// non-exhaustive match in trans.
|
||||
fn constraints(fcx: fn_ctxt) -> ~[norm_constraint] {
|
||||
let mut rslt: ~[norm_constraint] = ~[];
|
||||
for fcx.enclosing.constrs.each |key, val| {
|
||||
vec::push_all(rslt, norm_a_constraint(key, val));
|
||||
};
|
||||
return rslt;
|
||||
}
|
||||
|
||||
// FIXME (#2539): Would rather take an immutable vec as an argument,
|
||||
// should freeze it at some earlier point.
|
||||
fn match_args(fcx: fn_ctxt, occs: @dvec<pred_args>,
|
||||
occ: ~[@constr_arg_use]) -> uint {
|
||||
debug!("match_args: looking at %s",
|
||||
constr_args_to_str(fn@(i: inst) -> ~str { *i.ident }, occ));
|
||||
for (*occs).each |pd| {
|
||||
log(debug,
|
||||
~"match_args: candidate " + pred_args_to_str(pd));
|
||||
fn eq(p: inst, q: inst) -> bool { return p.node == q.node; }
|
||||
if ty::args_eq(eq, pd.node.args, occ) { return pd.node.bit_num; }
|
||||
}
|
||||
fcx.ccx.tcx.sess.bug(~"match_args: no match for occurring args");
|
||||
}
|
||||
|
||||
fn def_id_for_constr(tcx: ty::ctxt, t: node_id) -> def_id {
|
||||
match tcx.def_map.find(t) {
|
||||
none {
|
||||
tcx.sess.bug(~"node_id_for_constr: bad node_id " + int::str(t));
|
||||
}
|
||||
Some(def_fn(i, _)) { return i; }
|
||||
_ { tcx.sess.bug(~"node_id_for_constr: pred is not a function"); }
|
||||
}
|
||||
}
|
||||
|
||||
fn expr_to_constr_arg(tcx: ty::ctxt, e: @expr) -> @constr_arg_use {
|
||||
match e.node {
|
||||
expr_path(p) {
|
||||
match tcx.def_map.find(e.id) {
|
||||
Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
|
||||
Some(def_binding(nid, _)) | Some(def_upvar(nid, _, _, _)) {
|
||||
return @respan(p.span,
|
||||
carg_ident({ident: p.idents[0], node: nid}));
|
||||
}
|
||||
Some(what) {
|
||||
tcx.sess.span_bug(e.span,
|
||||
fmt!("exprs_to_constr_args: non-local variable %? \
|
||||
as pred arg", what));
|
||||
}
|
||||
none {
|
||||
tcx.sess.span_bug(e.span,
|
||||
~"exprs_to_constr_args: unbound id as pred arg");
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_lit(l) { return @respan(e.span, carg_lit(l)); }
|
||||
_ {
|
||||
tcx.sess.span_fatal(e.span,
|
||||
~"arguments to constrained functions must be " +
|
||||
~"literals or local variables");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn exprs_to_constr_args(tcx: ty::ctxt,
|
||||
args: ~[@expr]) -> ~[@constr_arg_use] {
|
||||
let f = |a| expr_to_constr_arg(tcx, a);
|
||||
let mut rslt: ~[@constr_arg_use] = ~[];
|
||||
for args.each |e| { vec::push(rslt, f(e)); }
|
||||
rslt
|
||||
}
|
||||
|
||||
fn expr_to_constr(tcx: ty::ctxt, e: @expr) -> sp_constr {
|
||||
match e.node {
|
||||
expr_call(operator, args, _) {
|
||||
match operator.node {
|
||||
expr_path(p) {
|
||||
return respan(e.span,
|
||||
{path: p,
|
||||
def_id: def_id_for_constr(tcx, operator.id),
|
||||
args: exprs_to_constr_args(tcx, args)});
|
||||
}
|
||||
_ {
|
||||
tcx.sess.span_bug(operator.span,
|
||||
~"ill-formed operator in predicate");
|
||||
}
|
||||
}
|
||||
}
|
||||
_ {
|
||||
tcx.sess.span_bug(e.span, ~"ill-formed predicate");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn pred_args_to_str(p: pred_args) -> ~str {
|
||||
~"<" + uint::str(p.node.bit_num) + ~", " +
|
||||
constr_args_to_str(fn@(i: inst) -> ~str {return *i.ident; },
|
||||
p.node.args)
|
||||
+ ~">"
|
||||
}
|
||||
|
||||
fn substitute_constr_args(cx: ty::ctxt, actuals: ~[@expr], c: @ty::constr) ->
|
||||
tsconstr {
|
||||
let mut rslt: ~[@constr_arg_use] = ~[];
|
||||
for c.node.args.each |a| {
|
||||
vec::push(rslt, substitute_arg(cx, actuals, a));
|
||||
}
|
||||
return {path: c.node.path,
|
||||
def_id: c.node.id,
|
||||
args: rslt};
|
||||
}
|
||||
|
||||
fn substitute_arg(cx: ty::ctxt, actuals: ~[@expr], a: @constr_arg) ->
|
||||
@constr_arg_use {
|
||||
let num_actuals = vec::len(actuals);
|
||||
match a.node {
|
||||
carg_ident(i) {
|
||||
if i < num_actuals {
|
||||
return expr_to_constr_arg(cx, actuals[i]);
|
||||
} else {
|
||||
cx.sess.span_fatal(a.span, ~"constraint argument out of bounds");
|
||||
}
|
||||
}
|
||||
carg_base { return @respan(a.span, carg_base); }
|
||||
carg_lit(l) { return @respan(a.span, carg_lit(l)); }
|
||||
}
|
||||
}
|
||||
|
||||
fn pred_args_matches(pattern: ~[constr_arg_general_<inst>],
|
||||
desc: pred_args) ->
|
||||
bool {
|
||||
let mut i = 0u;
|
||||
for desc.node.args.each |c| {
|
||||
let n = pattern[i];
|
||||
match c.node {
|
||||
carg_ident(p) {
|
||||
match n {
|
||||
carg_ident(q) { if p.node != q.node { return false; } }
|
||||
_ { return false; }
|
||||
}
|
||||
}
|
||||
carg_base { if n != carg_base { return false; } }
|
||||
carg_lit(l) {
|
||||
match n {
|
||||
carg_lit(m) { if !const_eval::lit_eq(l, m) { return false; } }
|
||||
_ { return false; }
|
||||
}
|
||||
}
|
||||
}
|
||||
i += 1u;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
fn find_instance_(pattern: ~[constr_arg_general_<inst>],
|
||||
descs: ~[pred_args]) ->
|
||||
Option<uint> {
|
||||
for descs.each |d| {
|
||||
if pred_args_matches(pattern, d) { return Some(d.node.bit_num); }
|
||||
}
|
||||
return none;
|
||||
}
|
||||
|
||||
type inst = {ident: ident, node: node_id};
|
||||
|
||||
enum dest {
|
||||
local_dest(inst), // RHS is assigned to a local variable
|
||||
call // RHS is passed to a function
|
||||
}
|
||||
|
||||
type subst = ~[{from: inst, to: inst}];
|
||||
|
||||
fn find_instances(_fcx: fn_ctxt, subst: subst,
|
||||
c: constraint) -> ~[{from: uint, to: uint}] {
|
||||
|
||||
if vec::len(subst) == 0u { return ~[]; }
|
||||
let mut res = ~[];
|
||||
do (*c.descs).swap |v| {
|
||||
let v <- vec::from_mut(v);
|
||||
for v.each |d| {
|
||||
if args_mention(d.node.args, find_in_subst_bool, subst) {
|
||||
let old_bit_num = d.node.bit_num;
|
||||
let newv = replace(subst, d);
|
||||
match find_instance_(newv, v) {
|
||||
Some(d1) {vec::push(res, {from: old_bit_num, to: d1})}
|
||||
_ {}
|
||||
}
|
||||
} else {}
|
||||
}
|
||||
vec::to_mut(v)
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
fn find_in_subst(id: node_id, s: subst) -> Option<inst> {
|
||||
for s.each |p| {
|
||||
if id == p.from.node { return Some(p.to); }
|
||||
}
|
||||
return none;
|
||||
}
|
||||
|
||||
fn find_in_subst_bool(s: subst, id: node_id) -> bool {
|
||||
is_some(find_in_subst(id, s))
|
||||
}
|
||||
|
||||
fn insts_to_str(stuff: ~[constr_arg_general_<inst>]) -> ~str {
|
||||
let mut rslt = ~"<";
|
||||
for stuff.each |i| {
|
||||
rslt +=
|
||||
~" " +
|
||||
match i {
|
||||
carg_ident(p) { *p.ident }
|
||||
carg_base { ~"*" }
|
||||
carg_lit(_) { ~"~[lit]" }
|
||||
} + ~" ";
|
||||
}
|
||||
rslt += ~">";
|
||||
rslt
|
||||
}
|
||||
|
||||
fn replace(subst: subst, d: pred_args) -> ~[constr_arg_general_<inst>] {
|
||||
let mut rslt: ~[constr_arg_general_<inst>] = ~[];
|
||||
for d.node.args.each |c| {
|
||||
match c.node {
|
||||
carg_ident(p) {
|
||||
match find_in_subst(p.node, subst) {
|
||||
Some(newv) { vec::push(rslt, carg_ident(newv)); }
|
||||
_ { vec::push(rslt, c.node); }
|
||||
}
|
||||
}
|
||||
_ {
|
||||
vec::push(rslt, c.node);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return rslt;
|
||||
}
|
||||
|
||||
enum if_ty { if_check, plain_if, }
|
||||
|
||||
fn for_constraints_mentioning(fcx: fn_ctxt, id: node_id,
|
||||
f: fn(norm_constraint)) {
|
||||
for constraints(fcx).each |c| {
|
||||
if constraint_mentions(fcx, c, id) { f(c); }
|
||||
};
|
||||
}
|
||||
|
||||
fn local_node_id_to_def_id_strict(fcx: fn_ctxt, sp: span, i: node_id) ->
|
||||
def_id {
|
||||
match local_node_id_to_def(fcx, i) {
|
||||
Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
|
||||
Some(def_upvar(nid, _, _)) {
|
||||
return local_def(nid);
|
||||
}
|
||||
Some(_) {
|
||||
fcx.ccx.tcx.sess.span_fatal(sp,
|
||||
~"local_node_id_to_def_id: id \
|
||||
isn't a local");
|
||||
}
|
||||
none {
|
||||
// should really be bug. span_bug()?
|
||||
fcx.ccx.tcx.sess.span_fatal(sp,
|
||||
~"local_node_id_to_def_id: id \
|
||||
is unbound");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn local_node_id_to_def(fcx: fn_ctxt, i: node_id) -> Option<def> {
|
||||
fcx.ccx.tcx.def_map.find(i)
|
||||
}
|
||||
|
||||
fn local_node_id_to_def_id(fcx: fn_ctxt, i: node_id) -> Option<def_id> {
|
||||
match local_node_id_to_def(fcx, i) {
|
||||
Some(def_local(nid, _)) | Some(def_arg(nid, _)) |
|
||||
Some(def_binding(nid, _)) | Some(def_upvar(nid, _, _)) {
|
||||
Some(local_def(nid))
|
||||
}
|
||||
_ { none }
|
||||
}
|
||||
}
|
||||
|
||||
fn local_node_id_to_local_def_id(fcx: fn_ctxt, i: node_id) ->
|
||||
Option<node_id> {
|
||||
match local_node_id_to_def_id(fcx, i) {
|
||||
Some(did) { Some(did.node) }
|
||||
_ { none }
|
||||
}
|
||||
}
|
||||
|
||||
fn copy_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dest: inst, src: inst,
|
||||
ty: oper_type) {
|
||||
let post =
|
||||
node_id_to_ts_ann(fcx.ccx, parent_exp).conditions.postcondition;
|
||||
copy_in_poststate_two(fcx, post, post, dest, src, ty);
|
||||
}
|
||||
|
||||
fn copy_in_poststate(fcx: fn_ctxt, post: poststate, dest: inst, src: inst,
|
||||
ty: oper_type) {
|
||||
copy_in_poststate_two(fcx, post, post, dest, src, ty);
|
||||
}
|
||||
|
||||
// In target_post, set the bits corresponding to copies of any
|
||||
// constraints mentioning src that are set in src_post, with
|
||||
// dest substituted for src.
|
||||
// (This doesn't create any new constraints. If a new, substituted
|
||||
// constraint isn't already in the bit vector, it's ignored.)
|
||||
fn copy_in_poststate_two(fcx: fn_ctxt, src_post: poststate,
|
||||
target_post: poststate, dest: inst, src: inst,
|
||||
ty: oper_type) {
|
||||
let mut subst;
|
||||
match ty {
|
||||
oper_swap { subst = ~[{from: dest, to: src}, {from: src, to: dest}]; }
|
||||
oper_assign_op {
|
||||
return; // Don't do any propagation
|
||||
}
|
||||
_ { subst = ~[{from: src, to: dest}]; }
|
||||
}
|
||||
|
||||
|
||||
for fcx.enclosing.constrs.each_value |val| {
|
||||
// replace any occurrences of the src def_id with the
|
||||
// dest def_id
|
||||
let insts = find_instances(fcx, subst, val);
|
||||
for insts.each |p| {
|
||||
if bitvectors::promises_(p.from, src_post) {
|
||||
set_in_poststate_(p.to, target_post);
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) {
|
||||
// In the postcondition given by parent_exp, clear the bits
|
||||
// for any constraints mentioning dead_v
|
||||
let d = local_node_id_to_local_def_id(fcx, dead_v);
|
||||
do option::iter(d) |d_id| {
|
||||
do for_constraints_mentioning(fcx, d_id) |c| {
|
||||
debug!("clearing constraint %u %s",
|
||||
c.bit_num,
|
||||
constraint_to_str(fcx.ccx.tcx, c.c));
|
||||
clear_in_postcond(c.bit_num,
|
||||
node_id_to_ts_ann(fcx.ccx,
|
||||
parent_exp).conditions);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool {
|
||||
// In the poststate given by parent_exp, clear the bits
|
||||
// for any constraints mentioning dead_v
|
||||
let d = local_node_id_to_local_def_id(fcx, dead_v);
|
||||
let mut changed = false;
|
||||
do option::iter(d) |d_id| {
|
||||
do for_constraints_mentioning(fcx, d_id) |c| {
|
||||
changed |= clear_in_poststate_(c.bit_num, p);
|
||||
}
|
||||
}
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn any_eq(v: ~[node_id], d: node_id) -> bool {
|
||||
for v.each |i| { if i == d { return true; } }
|
||||
false
|
||||
}
|
||||
|
||||
fn constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id) ->
|
||||
bool {
|
||||
return args_mention(c.c.node.args, any_eq, ~[v]);
|
||||
}
|
||||
|
||||
fn args_mention<T>(args: ~[@constr_arg_use],
|
||||
q: fn(~[T], node_id) -> bool,
|
||||
s: ~[T]) -> bool {
|
||||
|
||||
for args.each |a| {
|
||||
match a.node {
|
||||
carg_ident(p1) { if q(s, p1.node) { return true; } } _ { }
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
fn use_var(fcx: fn_ctxt, v: node_id) {
|
||||
vec::push(*fcx.enclosing.used_vars, v);
|
||||
}
|
||||
|
||||
fn op_to_oper_ty(io: init_op) -> oper_type {
|
||||
match io { init_move { oper_move } _ { oper_assign } }
|
||||
}
|
||||
|
||||
// default function visitor
|
||||
fn do_nothing<T>(_fk: visit::fn_kind, _decl: fn_decl, _body: blk,
|
||||
_sp: span, _id: node_id,
|
||||
_t: T, _v: visit::vt<T>) {
|
||||
}
|
||||
|
||||
|
||||
fn args_to_constr_args(tcx: ty::ctxt, args: ~[arg],
|
||||
indices: ~[@sp_constr_arg<uint>])
|
||||
-> ~[@constr_arg_use] {
|
||||
let mut actuals: ~[@constr_arg_use] = ~[];
|
||||
let num_args = vec::len(args);
|
||||
for indices.each |a| {
|
||||
vec::push(
|
||||
actuals,
|
||||
@respan(a.span,
|
||||
match a.node {
|
||||
carg_base { carg_base }
|
||||
carg_ident(i) {
|
||||
if i < num_args {
|
||||
carg_ident({ident: args[i].ident,
|
||||
node: args[i].id})
|
||||
} else {
|
||||
tcx.sess.span_bug(a.span,
|
||||
~"index out of bounds in \
|
||||
constraint arg");
|
||||
}
|
||||
}
|
||||
carg_lit(l) { carg_lit(l) }
|
||||
}));
|
||||
}
|
||||
return actuals;
|
||||
}
|
||||
|
||||
fn ast_constr_to_ts_constr(tcx: ty::ctxt, args: ~[arg], c: @constr) ->
|
||||
tsconstr {
|
||||
let tconstr = ty::ast_constr_to_constr(tcx, c);
|
||||
return {path: tconstr.node.path,
|
||||
def_id: tconstr.node.id,
|
||||
args: args_to_constr_args(tcx, args, tconstr.node.args)};
|
||||
}
|
||||
|
||||
fn ast_constr_to_sp_constr(tcx: ty::ctxt, args: ~[arg], c: @constr) ->
|
||||
sp_constr {
|
||||
let tconstr = ast_constr_to_ts_constr(tcx, args, c);
|
||||
return respan(c.span, tconstr);
|
||||
}
|
||||
|
||||
type binding = {lhs: ~[dest], rhs: Option<initializer>};
|
||||
|
||||
fn local_to_bindings(tcx: ty::ctxt, loc: @local) -> binding {
|
||||
let mut lhs = ~[];
|
||||
do pat_bindings(tcx.def_map, loc.node.pat) |_bm, p_id, _s, name| {
|
||||
vec::push(lhs, local_dest({ident: path_to_ident(name), node: p_id}));
|
||||
};
|
||||
{lhs: lhs, rhs: loc.node.init}
|
||||
}
|
||||
|
||||
fn locals_to_bindings(tcx: ty::ctxt, locals: ~[@local]) -> ~[binding] {
|
||||
let mut rslt = ~[];
|
||||
for locals.each |loc| { vec::push(rslt, local_to_bindings(tcx, loc)); }
|
||||
return rslt;
|
||||
}
|
||||
|
||||
fn callee_modes(fcx: fn_ctxt, callee: node_id) -> ~[mode] {
|
||||
let ty = ty::type_autoderef(fcx.ccx.tcx,
|
||||
ty::node_id_to_type(fcx.ccx.tcx, callee));
|
||||
match ty::get(ty).struct {
|
||||
ty::ty_fn(ref fn_ty) {
|
||||
return fn_ty.sig.inputs.map(|input| input.mode);
|
||||
}
|
||||
_ {
|
||||
// Shouldn't happen; callee should be ty_fn.
|
||||
fcx.ccx.tcx.sess.bug(~"non-fn callee type in callee_modes: " +
|
||||
util::ppaux::ty_to_str(fcx.ccx.tcx, ty));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn callee_arg_init_ops(fcx: fn_ctxt, callee: node_id) -> ~[init_op] {
|
||||
do vec::map(callee_modes(fcx, callee)) |m| {
|
||||
match ty::resolved_mode(fcx.ccx.tcx, m) {
|
||||
by_move { init_move }
|
||||
by_copy | by_ref | by_val | by_mutbl_ref { init_assign }
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn arg_bindings(ops: ~[init_op], es: ~[@expr]) -> ~[binding] {
|
||||
let mut bindings: ~[binding] = ~[];
|
||||
let mut i = 0u;
|
||||
for ops.each |op| {
|
||||
vec::push(bindings,
|
||||
{lhs: ~[call], rhs: Some({op: op, expr: es[i]})});
|
||||
i += 1u;
|
||||
}
|
||||
return bindings;
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -1,153 +0,0 @@
|
||||
|
||||
use syntax::ast;
|
||||
use ast::{stmt, fn_ident, node_id, crate, return_val, noreturn, expr};
|
||||
use syntax::{visit, print};
|
||||
use syntax::codemap::span;
|
||||
use middle::ty;
|
||||
use tstate::ann::{precond, prestate,
|
||||
implies, ann_precond, ann_prestate};
|
||||
use aux::*;
|
||||
|
||||
use util::ppaux::ty_to_str;
|
||||
use bitvectors::*;
|
||||
use annotate::annotate_crate;
|
||||
use collect_locals::mk_f_to_fn_info;
|
||||
use pre_post_conditions::fn_pre_post;
|
||||
use states::find_pre_post_state_fn;
|
||||
use syntax::print::pprust::expr_to_str;
|
||||
use driver::session::session;
|
||||
use std::map::hashmap;
|
||||
|
||||
fn check_states_expr(e: @expr, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
|
||||
visit::visit_expr(e, fcx, v);
|
||||
|
||||
let prec: precond = expr_precond(fcx.ccx, e);
|
||||
let pres: prestate = expr_prestate(fcx.ccx, e);
|
||||
|
||||
if !implies(pres, prec) {
|
||||
let mut s = ~"";
|
||||
let diff = first_difference_string(fcx, prec, pres);
|
||||
s +=
|
||||
~"unsatisfied precondition constraint (for example, " + diff +
|
||||
~") for expression:\n";
|
||||
s += syntax::print::pprust::expr_to_str(e);
|
||||
s += ~"\nprecondition:\n";
|
||||
s += tritv_to_str(fcx, prec);
|
||||
s += ~"\nprestate:\n";
|
||||
s += tritv_to_str(fcx, pres);
|
||||
fcx.ccx.tcx.sess.span_fatal(e.span, s);
|
||||
}
|
||||
}
|
||||
|
||||
fn check_states_stmt(s: @stmt, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
|
||||
visit::visit_stmt(s, fcx, v);
|
||||
|
||||
let a = stmt_to_ann(fcx.ccx, *s);
|
||||
let prec: precond = ann_precond(a);
|
||||
let pres: prestate = ann_prestate(a);
|
||||
|
||||
debug!("check_states_stmt:");
|
||||
log(debug, print::pprust::stmt_to_str(*s));
|
||||
debug!("prec = ");
|
||||
log_tritv(fcx, prec);
|
||||
debug!("pres = ");
|
||||
log_tritv(fcx, pres);
|
||||
|
||||
if !implies(pres, prec) {
|
||||
let mut ss = ~"";
|
||||
let diff = first_difference_string(fcx, prec, pres);
|
||||
ss +=
|
||||
~"unsatisfied precondition constraint (for example, " + diff +
|
||||
~") for statement:\n";
|
||||
ss += syntax::print::pprust::stmt_to_str(*s);
|
||||
ss += ~"\nprecondition:\n";
|
||||
ss += tritv_to_str(fcx, prec);
|
||||
ss += ~"\nprestate: \n";
|
||||
ss += tritv_to_str(fcx, pres);
|
||||
fcx.ccx.tcx.sess.span_fatal(s.span, ss);
|
||||
}
|
||||
}
|
||||
|
||||
fn check_states_against_conditions(fcx: fn_ctxt,
|
||||
fk: visit::fn_kind,
|
||||
f_decl: ast::fn_decl,
|
||||
f_body: ast::blk,
|
||||
sp: span,
|
||||
id: node_id) {
|
||||
/* Postorder traversal instead of pre is important
|
||||
because we want the smallest possible erroneous statement
|
||||
or expression. */
|
||||
let visitor = visit::mk_vt(
|
||||
@{visit_stmt: check_states_stmt,
|
||||
visit_expr: check_states_expr,
|
||||
visit_fn: |a,b,c,d,e,f,g| {
|
||||
do_nothing::<fn_ctxt>(a, b, c, d, e, f, g)
|
||||
}
|
||||
with *visit::default_visitor::<fn_ctxt>()});
|
||||
visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor);
|
||||
}
|
||||
|
||||
fn check_fn_states(fcx: fn_ctxt,
|
||||
fk: visit::fn_kind,
|
||||
f_decl: ast::fn_decl,
|
||||
f_body: ast::blk,
|
||||
sp: span,
|
||||
id: node_id) {
|
||||
/* Compute the pre- and post-states for this function */
|
||||
|
||||
// Fixpoint iteration
|
||||
while find_pre_post_state_fn(fcx, f_decl, f_body) { }
|
||||
|
||||
/* Now compare each expr's pre-state to its precondition
|
||||
and post-state to its postcondition */
|
||||
|
||||
check_states_against_conditions(fcx, fk, f_decl, f_body, sp, id);
|
||||
}
|
||||
|
||||
fn fn_states(fk: visit::fn_kind, f_decl: ast::fn_decl, f_body: ast::blk,
|
||||
sp: span, id: node_id,
|
||||
ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
|
||||
|
||||
visit::visit_fn(fk, f_decl, f_body, sp, id, ccx, v);
|
||||
|
||||
// We may not care about typestate for this function if it contains
|
||||
// no constrained calls
|
||||
if !ccx.fm.get(id).ignore {
|
||||
/* Look up the var-to-bit-num map for this function */
|
||||
|
||||
let f_info = ccx.fm.get(id);
|
||||
let name = visit::name_of_fn(fk);
|
||||
let fcx = {enclosing: f_info, id: id, name: name, ccx: ccx};
|
||||
check_fn_states(fcx, fk, f_decl, f_body, sp, id)
|
||||
}
|
||||
}
|
||||
|
||||
fn check_crate(cx: ty::ctxt, crate: @crate) {
|
||||
let ccx: crate_ctxt = new_crate_ctxt(cx);
|
||||
/* Build the global map from function id to var-to-bit-num-map */
|
||||
|
||||
mk_f_to_fn_info(ccx, crate);
|
||||
/* Add a blank ts_ann for every statement (and expression) */
|
||||
|
||||
annotate_crate(ccx, *crate);
|
||||
/* Compute the pre and postcondition for every subexpression */
|
||||
|
||||
let vtor = visit::default_visitor::<crate_ctxt>();
|
||||
let vtor = @{visit_fn: fn_pre_post with *vtor};
|
||||
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
|
||||
|
||||
/* Check the pre- and postcondition against the pre- and poststate
|
||||
for every expression */
|
||||
let vtor = visit::default_visitor::<crate_ctxt>();
|
||||
let vtor = @{visit_fn: fn_states with *vtor};
|
||||
visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
|
||||
}
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -1,165 +0,0 @@
|
||||
use option::*;
|
||||
use pat_util::*;
|
||||
use syntax::ast::*;
|
||||
use syntax::ast_util::*;
|
||||
use syntax::visit;
|
||||
use syntax::codemap::span;
|
||||
use syntax::ast_util::respan;
|
||||
use driver::session::session;
|
||||
use aux::*;
|
||||
use std::map::hashmap;
|
||||
use dvec::{dvec, extensions};
|
||||
|
||||
type ctxt = {cs: @mut ~[sp_constr], tcx: ty::ctxt};
|
||||
|
||||
fn collect_pred(e: @expr, cx: ctxt, v: visit::vt<ctxt>) {
|
||||
match e.node {
|
||||
expr_check(_, ch) { vec::push(*cx.cs, expr_to_constr(cx.tcx, ch)); }
|
||||
expr_if_check(ex, _, _) {
|
||||
vec::push(*cx.cs, expr_to_constr(cx.tcx, ex));
|
||||
}
|
||||
|
||||
// If it's a call, generate appropriate instances of the
|
||||
// call's constraints.
|
||||
expr_call(operator, operands, _) {
|
||||
for constraints_expr(cx.tcx, operator).each |c| {
|
||||
let ct: sp_constr =
|
||||
respan(c.span,
|
||||
aux::substitute_constr_args(cx.tcx, operands, c));
|
||||
vec::push(*cx.cs, ct);
|
||||
}
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
// visit subexpressions
|
||||
visit::visit_expr(e, cx, v);
|
||||
}
|
||||
|
||||
fn find_locals(tcx: ty::ctxt,
|
||||
fk: visit::fn_kind,
|
||||
f_decl: fn_decl,
|
||||
f_body: blk,
|
||||
sp: span,
|
||||
id: node_id) -> ctxt {
|
||||
let cx: ctxt = {cs: @mut ~[], tcx: tcx};
|
||||
let visitor = visit::default_visitor::<ctxt>();
|
||||
let visitor =
|
||||
@{visit_expr: collect_pred,
|
||||
visit_fn: do_nothing
|
||||
with *visitor};
|
||||
visit::visit_fn(fk, f_decl, f_body, sp,
|
||||
id, cx, visit::mk_vt(visitor));
|
||||
return cx;
|
||||
}
|
||||
|
||||
fn add_constraint(tcx: ty::ctxt, c: sp_constr, next: uint, tbl: constr_map) ->
|
||||
uint {
|
||||
log(debug,
|
||||
constraint_to_str(tcx, c) + ~" |-> " + uint::str(next));
|
||||
|
||||
let {path: p, def_id: d_id, args: args} = c.node;
|
||||
match tbl.find(d_id) {
|
||||
Some(ct) {
|
||||
(*ct.descs).push(respan(c.span, {args: args, bit_num: next}));
|
||||
}
|
||||
None {
|
||||
let rslt = @dvec();
|
||||
(*rslt).push(respan(c.span, {args: args, bit_num: next}));
|
||||
tbl.insert(d_id, {path:p, descs:rslt});
|
||||
}
|
||||
}
|
||||
return next + 1u;
|
||||
}
|
||||
|
||||
fn contains_constrained_calls(tcx: ty::ctxt, body: blk) -> bool {
|
||||
type cx = @{
|
||||
tcx: ty::ctxt,
|
||||
mut has: bool
|
||||
};
|
||||
let cx = @{
|
||||
tcx: tcx,
|
||||
mut has: false
|
||||
};
|
||||
let vtor = visit::default_visitor::<cx>();
|
||||
let vtor = @{visit_expr: visit_expr with *vtor};
|
||||
visit::visit_block(body, cx, visit::mk_vt(vtor));
|
||||
return cx.has;
|
||||
|
||||
fn visit_expr(e: @expr, &&cx: cx, v: visit::vt<cx>) {
|
||||
import syntax::print::pprust;
|
||||
debug!("visiting %?", pprust::expr_to_str(e));
|
||||
|
||||
visit::visit_expr(e, cx, v);
|
||||
|
||||
if constraints_expr(cx.tcx, e).is_not_empty() {
|
||||
debug!("has constraints");
|
||||
cx.has = true;
|
||||
} else {
|
||||
debug!("has not constraints");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* builds a table mapping each local var defined in f
|
||||
to a bit number in the precondition/postcondition vectors */
|
||||
fn mk_fn_info(ccx: crate_ctxt,
|
||||
fk: visit::fn_kind,
|
||||
f_decl: fn_decl,
|
||||
f_body: blk,
|
||||
f_sp: span,
|
||||
id: node_id) {
|
||||
let name = visit::name_of_fn(fk);
|
||||
let res_map = new_def_hash::<constraint>();
|
||||
let mut next: uint = 0u;
|
||||
|
||||
let cx: ctxt = find_locals(ccx.tcx, fk, f_decl, f_body, f_sp, id);
|
||||
/* now we have to add bit nums for both the constraints
|
||||
and the variables... */
|
||||
|
||||
let ignore = !contains_constrained_calls(ccx.tcx, f_body);
|
||||
|
||||
if !ignore {
|
||||
let mut i = 0u, l = vec::len(*cx.cs);
|
||||
while i < l {
|
||||
next = add_constraint(cx.tcx, copy cx.cs[i], next, res_map);
|
||||
i += 1u;
|
||||
}
|
||||
/* if this function has any constraints, instantiate them to the
|
||||
argument names and add them */
|
||||
for f_decl.constraints.each |c| {
|
||||
let sc = ast_constr_to_sp_constr(cx.tcx, f_decl.inputs, c);
|
||||
next = add_constraint(cx.tcx, sc, next, res_map);
|
||||
}
|
||||
}
|
||||
|
||||
let v: @mut ~[node_id] = @mut ~[];
|
||||
let rslt =
|
||||
{constrs: res_map,
|
||||
num_constraints: next,
|
||||
cf: f_decl.cf,
|
||||
used_vars: v,
|
||||
ignore: ignore};
|
||||
ccx.fm.insert(id, rslt);
|
||||
debug!("%s has %u constraints", *name, num_constraints(rslt));
|
||||
}
|
||||
|
||||
|
||||
/* initializes the global fn_info_map (mapping each function ID, including
|
||||
nested locally defined functions, onto a mapping from local variable name
|
||||
to bit number) */
|
||||
fn mk_f_to_fn_info(ccx: crate_ctxt, c: @crate) {
|
||||
let visitor =
|
||||
visit::mk_simple_visitor(@{
|
||||
visit_fn: |a,b,c,d,e| mk_fn_info(ccx, a, b, c, d, e)
|
||||
with *visit::default_simple_visitor()});
|
||||
visit::visit_crate(*c, (), visitor);
|
||||
}
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -1,617 +0,0 @@
|
||||
use tstate::ann::*;
|
||||
use aux::*;
|
||||
use bitvectors::{bit_num, seq_preconds, seq_postconds,
|
||||
intersect_states,
|
||||
relax_precond_block, gen};
|
||||
use tritv::*;
|
||||
|
||||
use pat_util::*;
|
||||
use syntax::ast::*;
|
||||
use syntax::ast_util::*;
|
||||
use syntax::print::pprust::{expr_to_str, stmt_to_str};
|
||||
use syntax::visit;
|
||||
use util::common::{field_exprs, has_nonlocal_exits};
|
||||
use syntax::codemap::span;
|
||||
use driver::session::session;
|
||||
use std::map::hashmap;
|
||||
|
||||
fn find_pre_post_mod(_m: _mod) -> _mod {
|
||||
debug!("implement find_pre_post_mod!");
|
||||
fail;
|
||||
}
|
||||
|
||||
fn find_pre_post_foreign_mod(_m: foreign_mod) -> foreign_mod {
|
||||
debug!("implement find_pre_post_foreign_mod");
|
||||
fail;
|
||||
}
|
||||
|
||||
fn find_pre_post_method(ccx: crate_ctxt, m: @method) {
|
||||
assert (ccx.fm.contains_key(m.id));
|
||||
let fcx: fn_ctxt =
|
||||
{enclosing: ccx.fm.get(m.id),
|
||||
id: m.id,
|
||||
name: m.ident,
|
||||
ccx: ccx};
|
||||
find_pre_post_fn(fcx, m.body);
|
||||
}
|
||||
|
||||
fn find_pre_post_item(ccx: crate_ctxt, i: item) {
|
||||
match i.node {
|
||||
item_const(_, e) {
|
||||
// do nothing -- item_consts don't refer to local vars
|
||||
}
|
||||
item_fn(_, _, body) {
|
||||
assert (ccx.fm.contains_key(i.id));
|
||||
let fcx =
|
||||
{enclosing: ccx.fm.get(i.id), id: i.id, name: i.ident, ccx: ccx};
|
||||
find_pre_post_fn(fcx, body);
|
||||
}
|
||||
item_mod(m) { find_pre_post_mod(m); }
|
||||
item_foreign_mod(nm) { find_pre_post_foreign_mod(nm); }
|
||||
item_ty(*) | item_enum(*) | item_trait(*) { return; }
|
||||
item_class(*) {
|
||||
fail ~"find_pre_post_item: shouldn't be called on item_class";
|
||||
}
|
||||
item_impl(_, _, _, ms) {
|
||||
for ms.each |m| { find_pre_post_method(ccx, m); }
|
||||
}
|
||||
item_mac(*) { fail ~"item macros unimplemented" }
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* Finds the pre and postcondition for each expr in <args>;
|
||||
sets the precondition in a to be the result of combining
|
||||
the preconditions for <args>, and the postcondition in a to
|
||||
be the union of all postconditions for <args> */
|
||||
fn find_pre_post_exprs(fcx: fn_ctxt, args: ~[@expr], id: node_id) {
|
||||
if vec::len::<@expr>(args) > 0u {
|
||||
debug!("find_pre_post_exprs: oper = %s", expr_to_str(args[0]));
|
||||
}
|
||||
fn do_one(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
|
||||
for args.each |e| { do_one(fcx, e); }
|
||||
|
||||
fn get_pp(ccx: crate_ctxt, &&e: @expr) -> pre_and_post {
|
||||
return expr_pp(ccx, e);
|
||||
}
|
||||
let pps = vec::map(args, |a| get_pp(fcx.ccx, a) );
|
||||
|
||||
set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
|
||||
seq_postconds(fcx, vec::map(pps, get_post)));
|
||||
}
|
||||
|
||||
fn find_pre_post_loop(fcx: fn_ctxt, index: @expr, body: blk, id: node_id) {
|
||||
find_pre_post_expr(fcx, index);
|
||||
find_pre_post_block(fcx, body);
|
||||
|
||||
let loop_precond =
|
||||
seq_preconds(fcx, ~[expr_pp(fcx.ccx, index),
|
||||
block_pp(fcx.ccx, body)]);
|
||||
let loop_postcond =
|
||||
intersect_states(expr_postcond(fcx.ccx, index),
|
||||
block_postcond(fcx.ccx, body));
|
||||
copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
|
||||
}
|
||||
|
||||
// Generates a pre/post assuming that a is the
|
||||
// annotation for an if-expression with consequent conseq
|
||||
// and alternative maybe_alt
|
||||
fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
|
||||
maybe_alt: Option<@expr>, id: node_id, chck: if_ty) {
|
||||
find_pre_post_expr(fcx, antec);
|
||||
find_pre_post_block(fcx, conseq);
|
||||
match maybe_alt {
|
||||
none {
|
||||
match chck {
|
||||
if_check {
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
|
||||
gen(fcx, antec.id, c.node);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
|
||||
let precond_res =
|
||||
seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec),
|
||||
block_pp(fcx.ccx, conseq)]);
|
||||
set_pre_and_post(fcx.ccx, id, precond_res,
|
||||
expr_poststate(fcx.ccx, antec));
|
||||
}
|
||||
Some(altern) {
|
||||
/*
|
||||
if check = if_check, then
|
||||
be sure that the predicate implied by antec
|
||||
is *not* true in the alternative
|
||||
*/
|
||||
find_pre_post_expr(fcx, altern);
|
||||
let precond_false_case =
|
||||
seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec),
|
||||
expr_pp(fcx.ccx, altern)]);
|
||||
let postcond_false_case =
|
||||
seq_postconds(fcx,
|
||||
~[expr_postcond(fcx.ccx, antec),
|
||||
expr_postcond(fcx.ccx, altern)]);
|
||||
|
||||
/* Be sure to set the bit for the check condition here,
|
||||
so that it's *not* set in the alternative. */
|
||||
match chck {
|
||||
if_check {
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
|
||||
gen(fcx, antec.id, c.node);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
let precond_true_case =
|
||||
seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec),
|
||||
block_pp(fcx.ccx, conseq)]);
|
||||
let postcond_true_case =
|
||||
seq_postconds(fcx,
|
||||
~[expr_postcond(fcx.ccx, antec),
|
||||
block_postcond(fcx.ccx, conseq)]);
|
||||
|
||||
let precond_res =
|
||||
seq_postconds(fcx, ~[precond_true_case, precond_false_case]);
|
||||
let postcond_res =
|
||||
intersect_states(postcond_true_case, postcond_false_case);
|
||||
set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id,
|
||||
new_var: node_id) {
|
||||
match node_id_to_def(fcx.ccx, new_var) {
|
||||
Some(d) {
|
||||
match d {
|
||||
def_local(nid, _) {
|
||||
find_pre_post_expr(fcx, rhs);
|
||||
let p = expr_pp(fcx.ccx, rhs);
|
||||
set_pre_and_post(fcx.ccx, larger_id, p.precondition,
|
||||
p.postcondition);
|
||||
}
|
||||
_ { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
|
||||
}
|
||||
}
|
||||
_ { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
|
||||
}
|
||||
}
|
||||
|
||||
fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
|
||||
ty: oper_type) {
|
||||
find_pre_post_expr(fcx, rhs);
|
||||
match lhs.node {
|
||||
expr_path(p) {
|
||||
let post = expr_postcond(fcx.ccx, parent);
|
||||
let tmp = post.clone();
|
||||
|
||||
match ty {
|
||||
oper_move {
|
||||
if is_path(rhs) { forget_in_postcond(fcx, parent.id, rhs.id); }
|
||||
}
|
||||
oper_swap {
|
||||
forget_in_postcond(fcx, parent.id, lhs.id);
|
||||
forget_in_postcond(fcx, parent.id, rhs.id);
|
||||
}
|
||||
oper_assign {
|
||||
forget_in_postcond(fcx, parent.id, lhs.id);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
|
||||
gen_if_local(fcx, lhs, rhs, parent.id, lhs.id);
|
||||
match rhs.node {
|
||||
expr_path(p1) {
|
||||
let d = local_node_id_to_local_def_id(fcx, lhs.id);
|
||||
let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
|
||||
match d {
|
||||
Some(id) {
|
||||
match d1 {
|
||||
Some(id1) {
|
||||
let instlhs =
|
||||
{ident: path_to_ident(p), node: id};
|
||||
let instrhs =
|
||||
{ident: path_to_ident(p1), node: id1};
|
||||
copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
|
||||
ty);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
_ {/* do nothing */ }
|
||||
}
|
||||
}
|
||||
_ { find_pre_post_expr(fcx, lhs); }
|
||||
}
|
||||
}
|
||||
|
||||
fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: ~[mode],
|
||||
operands: ~[@expr]) {
|
||||
do vec::iteri(modes) |i,mode| {
|
||||
match ty::resolved_mode(fcx.ccx.tcx, mode) {
|
||||
by_move { forget_in_postcond(fcx, parent.id, operands[i].id); }
|
||||
by_ref | by_val | by_mutbl_ref | by_copy { }
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) {
|
||||
let rslt = expr_pp(fcx.ccx, e);
|
||||
clear_pp(rslt);
|
||||
}
|
||||
|
||||
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
||||
fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
|
||||
let enclosing = fcx.enclosing;
|
||||
let num_local_vars = num_constraints(enclosing);
|
||||
fn do_rand_(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
|
||||
|
||||
|
||||
match e.node {
|
||||
expr_call(operator, operands, _) {
|
||||
/* copy */
|
||||
|
||||
let mut args = operands;
|
||||
vec::push(args, operator);
|
||||
|
||||
find_pre_post_exprs(fcx, args, e.id);
|
||||
/* see if the call has any constraints on its type */
|
||||
for constraints_expr(fcx.ccx.tcx, operator).each |c| {
|
||||
let i =
|
||||
bit_num(fcx, substitute_constr_args(fcx.ccx.tcx, args, c));
|
||||
require(i, expr_pp(fcx.ccx, e));
|
||||
}
|
||||
|
||||
forget_args_moved_in(fcx, e, callee_modes(fcx, operator.id),
|
||||
operands);
|
||||
|
||||
/* if this is a failing call, its postcondition sets everything */
|
||||
match controlflow_expr(fcx.ccx, operator) {
|
||||
noreturn { set_postcond_false(fcx.ccx, e.id); }
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
expr_vstore(ee, _) {
|
||||
find_pre_post_expr(fcx, ee);
|
||||
let p = expr_pp(fcx.ccx, ee);
|
||||
set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
|
||||
}
|
||||
expr_vec(args, _) {
|
||||
find_pre_post_exprs(fcx, args, e.id);
|
||||
}
|
||||
expr_path(p) {
|
||||
let rslt = expr_pp(fcx.ccx, e);
|
||||
clear_pp(rslt);
|
||||
}
|
||||
expr_new(p, _, v) {
|
||||
find_pre_post_exprs(fcx, ~[p, v], e.id);
|
||||
}
|
||||
expr_log(_, lvl, arg) {
|
||||
find_pre_post_exprs(fcx, ~[lvl, arg], e.id);
|
||||
}
|
||||
expr_fn(_, _, _, cap_clause) | expr_fn_block(_, _, cap_clause) {
|
||||
find_pre_post_expr_fn_upvars(fcx, e);
|
||||
|
||||
for (*cap_clause).each |cap_item| {
|
||||
let d = local_node_id_to_local_def_id(fcx, cap_item.id);
|
||||
option::iter(d, |id| use_var(fcx, id) );
|
||||
}
|
||||
|
||||
for (*cap_clause).each |cap_item| {
|
||||
if cap_item.is_move {
|
||||
log(debug, (~"forget_in_postcond: ", cap_item));
|
||||
forget_in_postcond(fcx, e.id, cap_item.id);
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_block(b) {
|
||||
find_pre_post_block(fcx, b);
|
||||
let p = block_pp(fcx.ccx, b);
|
||||
set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
|
||||
}
|
||||
expr_rec(fields, maybe_base) {
|
||||
let mut es = field_exprs(fields);
|
||||
match maybe_base { none {/* no-op */ } Some(b) { vec::push(es, b); } }
|
||||
find_pre_post_exprs(fcx, es, e.id);
|
||||
}
|
||||
expr_tup(elts) { find_pre_post_exprs(fcx, elts, e.id); }
|
||||
expr_move(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_move); }
|
||||
expr_swap(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_swap); }
|
||||
expr_assign(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_assign); }
|
||||
expr_assign_op(_, lhs, rhs) {
|
||||
/* Different from expr_assign in that the lhs *must*
|
||||
already be initialized */
|
||||
|
||||
find_pre_post_exprs(fcx, ~[lhs, rhs], e.id);
|
||||
forget_in_postcond(fcx, e.id, lhs.id);
|
||||
}
|
||||
expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); }
|
||||
expr_ret(maybe_val) {
|
||||
match maybe_val {
|
||||
none {
|
||||
clear_precond(fcx.ccx, e.id);
|
||||
set_postcond_false(fcx.ccx, e.id);
|
||||
}
|
||||
Some(ret_val) {
|
||||
find_pre_post_expr(fcx, ret_val);
|
||||
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
||||
expr_precond(fcx.ccx, ret_val));
|
||||
set_postcond_false(fcx.ccx, e.id);
|
||||
}
|
||||
}
|
||||
}
|
||||
expr_if(antec, conseq, maybe_alt) {
|
||||
join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if);
|
||||
}
|
||||
expr_binary(bop, l, r) {
|
||||
if lazy_binop(bop) {
|
||||
find_pre_post_expr(fcx, l);
|
||||
find_pre_post_expr(fcx, r);
|
||||
let overall_pre =
|
||||
seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
|
||||
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 { find_pre_post_exprs(fcx, ~[l, r], e.id); }
|
||||
}
|
||||
expr_addr_of(_, x) | expr_cast(x, _) | expr_unary(_, x) |
|
||||
expr_loop_body(x) | expr_do_body(x) | expr_assert(x) | expr_copy(x) {
|
||||
find_pre_post_expr(fcx, x);
|
||||
copy_pre_post(fcx.ccx, e.id, x);
|
||||
}
|
||||
expr_while(test, body) {
|
||||
find_pre_post_expr(fcx, test);
|
||||
find_pre_post_block(fcx, body);
|
||||
set_pre_and_post(fcx.ccx, e.id,
|
||||
seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, test),
|
||||
block_pp(fcx.ccx, body)]),
|
||||
intersect_states(expr_postcond(fcx.ccx, test),
|
||||
block_postcond(fcx.ccx, body)));
|
||||
}
|
||||
expr_loop(body) {
|
||||
find_pre_post_block(fcx, body);
|
||||
/* Infinite loop: if control passes it, everything is true. */
|
||||
let mut loop_postcond = false_postcond(num_local_vars);
|
||||
/* Conservative approximation: if the body has any nonlocal exits,
|
||||
the poststate is blank since we don't know what parts of it
|
||||
execute. */
|
||||
if has_nonlocal_exits(body) {
|
||||
loop_postcond = empty_poststate(num_local_vars);
|
||||
}
|
||||
set_pre_and_post(fcx.ccx, e.id, block_precond(fcx.ccx, body),
|
||||
loop_postcond);
|
||||
}
|
||||
expr_index(val, sub) { find_pre_post_exprs(fcx, ~[val, sub], e.id); }
|
||||
expr_match(ex, alts, _) {
|
||||
find_pre_post_expr(fcx, ex);
|
||||
fn do_an_alt(fcx: fn_ctxt, an_alt: arm) -> pre_and_post {
|
||||
match an_alt.guard {
|
||||
Some(e) { find_pre_post_expr(fcx, e); }
|
||||
_ {}
|
||||
}
|
||||
find_pre_post_block(fcx, an_alt.body);
|
||||
return block_pp(fcx.ccx, an_alt.body);
|
||||
}
|
||||
let mut alt_pps = ~[];
|
||||
for alts.each |a| { vec::push(alt_pps, do_an_alt(fcx, a)); }
|
||||
fn combine_pp(antec: pre_and_post, fcx: fn_ctxt, &&pp: pre_and_post,
|
||||
&&next: pre_and_post) -> pre_and_post {
|
||||
union(pp.precondition, seq_preconds(fcx, ~[antec, next]));
|
||||
intersect(pp.postcondition, next.postcondition);
|
||||
return pp;
|
||||
}
|
||||
let antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
|
||||
let e_pp =
|
||||
{precondition: empty_prestate(num_local_vars),
|
||||
postcondition: false_postcond(num_local_vars)};
|
||||
let g = |a,b| combine_pp(antec_pp, fcx, a, b);
|
||||
let alts_overall_pp =
|
||||
vec::foldl(e_pp, alt_pps, g);
|
||||
set_pre_and_post(fcx.ccx, e.id, alts_overall_pp.precondition,
|
||||
alts_overall_pp.postcondition);
|
||||
}
|
||||
expr_field(operator, _, _) {
|
||||
find_pre_post_expr(fcx, operator);
|
||||
copy_pre_post(fcx.ccx, e.id, operator);
|
||||
}
|
||||
expr_fail(maybe_val) {
|
||||
let mut prestate;
|
||||
match maybe_val {
|
||||
none { prestate = empty_prestate(num_local_vars); }
|
||||
Some(fail_val) {
|
||||
find_pre_post_expr(fcx, fail_val);
|
||||
prestate = expr_precond(fcx.ccx, fail_val);
|
||||
}
|
||||
}
|
||||
set_pre_and_post(fcx.ccx, e.id,
|
||||
/* if execution continues after fail,
|
||||
then everything is true! */
|
||||
prestate, false_postcond(num_local_vars));
|
||||
}
|
||||
expr_check(_, p) {
|
||||
find_pre_post_expr(fcx, p);
|
||||
copy_pre_post(fcx.ccx, e.id, p);
|
||||
/* predicate p holds after this expression executes */
|
||||
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
|
||||
gen(fcx, e.id, c.node);
|
||||
}
|
||||
expr_if_check(p, conseq, maybe_alt) {
|
||||
join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check);
|
||||
}
|
||||
expr_break { clear_pp(expr_pp(fcx.ccx, e)); }
|
||||
expr_again { clear_pp(expr_pp(fcx.ccx, e)); }
|
||||
expr_mac(_) { fcx.ccx.tcx.sess.bug(~"unexpanded macro"); }
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
|
||||
debug!("stmt = %s", stmt_to_str(s));
|
||||
match s.node {
|
||||
stmt_decl(adecl, id) {
|
||||
match adecl.node {
|
||||
decl_local(alocals) {
|
||||
let prev_pp = empty_pre_post(num_constraints(fcx.enclosing));
|
||||
for alocals.each |alocal| {
|
||||
match alocal.node.init {
|
||||
Some(an_init) {
|
||||
/* LHS always becomes initialized,
|
||||
whether or not this is a move */
|
||||
find_pre_post_expr(fcx, an_init.expr);
|
||||
do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
|
||||
|p_id, _s, _n| {
|
||||
copy_pre_post(fcx.ccx, p_id, an_init.expr);
|
||||
};
|
||||
/* Inherit ann from initializer, and add var being
|
||||
initialized to the postcondition */
|
||||
copy_pre_post(fcx.ccx, id, an_init.expr);
|
||||
|
||||
let mut p = none;
|
||||
match an_init.expr.node {
|
||||
expr_path(_p) { p = Some(_p); }
|
||||
_ { }
|
||||
}
|
||||
|
||||
do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
|
||||
|p_id, _s, n| {
|
||||
let ident = path_to_ident(n);
|
||||
match p {
|
||||
Some(p) {
|
||||
copy_in_postcond(fcx, id,
|
||||
{ident: ident, node: p_id},
|
||||
{ident:
|
||||
path_to_ident(p),
|
||||
node: an_init.expr.id},
|
||||
op_to_oper_ty(an_init.op));
|
||||
}
|
||||
none { }
|
||||
}
|
||||
};
|
||||
|
||||
/* Clear out anything that the previous initializer
|
||||
guaranteed */
|
||||
let e_pp = expr_pp(fcx.ccx, an_init.expr);
|
||||
prev_pp.precondition.become(
|
||||
seq_preconds(fcx, ~[prev_pp, e_pp]));
|
||||
|
||||
/* Include the LHSs too, since those aren't in the
|
||||
postconds of the RHSs themselves */
|
||||
copy_pre_post_(fcx.ccx, id, prev_pp.precondition,
|
||||
prev_pp.postcondition);
|
||||
}
|
||||
none {
|
||||
do pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
|
||||
|p_id, _s, _n| {
|
||||
clear_pp(node_id_to_ts_ann(fcx.ccx, p_id).conditions);
|
||||
};
|
||||
clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
decl_item(anitem) {
|
||||
clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
|
||||
find_pre_post_item(fcx.ccx, *anitem);
|
||||
}
|
||||
}
|
||||
}
|
||||
stmt_expr(e, id) | stmt_semi(e, id) {
|
||||
find_pre_post_expr(fcx, e);
|
||||
copy_pre_post(fcx.ccx, id, e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_block(fcx: fn_ctxt, b: blk) {
|
||||
/* Want to say that if there is a break or cont in this
|
||||
block, then that invalidates the poststate upheld by
|
||||
any of the stmts after it.
|
||||
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;
|
||||
|
||||
won't have a postcondition that says x is initialized, but that's ok.
|
||||
*/
|
||||
|
||||
let nv = num_constraints(fcx.enclosing);
|
||||
fn do_one_(fcx: fn_ctxt, s: @stmt) {
|
||||
find_pre_post_stmt(fcx, *s);
|
||||
}
|
||||
for b.node.stmts.each |s| { do_one_(fcx, s); }
|
||||
fn do_inner_(fcx: fn_ctxt, &&e: @expr) { find_pre_post_expr(fcx, e); }
|
||||
let do_inner = |a| do_inner_(fcx, a);
|
||||
option::map::<@expr, ()>(b.node.expr, do_inner);
|
||||
|
||||
let mut pps: ~[pre_and_post] = ~[];
|
||||
for b.node.stmts.each |s| { vec::push(pps, stmt_pp(fcx.ccx, *s)); }
|
||||
match b.node.expr {
|
||||
none {/* no-op */ }
|
||||
Some(e) { vec::push(pps, expr_pp(fcx.ccx, e)); }
|
||||
}
|
||||
|
||||
let block_precond = seq_preconds(fcx, pps);
|
||||
|
||||
let mut postconds = ~[];
|
||||
for pps.each |pp| { vec::push(postconds, get_post(pp)); }
|
||||
|
||||
/* A block may be empty, so this next line ensures that the postconds
|
||||
vector is non-empty. */
|
||||
vec::push(postconds, block_precond);
|
||||
|
||||
let mut block_postcond = empty_poststate(nv);
|
||||
/* conservative approximation */
|
||||
|
||||
if !has_nonlocal_exits(b) {
|
||||
block_postcond = seq_postconds(fcx, postconds);
|
||||
}
|
||||
set_pre_and_post(fcx.ccx, b.node.id, block_precond, block_postcond);
|
||||
}
|
||||
|
||||
fn find_pre_post_fn(fcx: fn_ctxt, body: blk) {
|
||||
find_pre_post_block(fcx, body);
|
||||
|
||||
// Treat the tail expression as a return statement
|
||||
match body.node.expr {
|
||||
Some(tailexpr) { set_postcond_false(fcx.ccx, tailexpr.id); }
|
||||
none {/* fallthrough */ }
|
||||
}
|
||||
}
|
||||
|
||||
fn fn_pre_post(fk: visit::fn_kind, decl: fn_decl, body: blk, sp: span,
|
||||
id: node_id,
|
||||
ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
|
||||
|
||||
visit::visit_fn(fk, decl, body, sp, id, ccx, v);
|
||||
assert (ccx.fm.contains_key(id));
|
||||
if !ccx.fm.get(id).ignore {
|
||||
let fcx =
|
||||
{enclosing: ccx.fm.get(id),
|
||||
id: id,
|
||||
name: visit::name_of_fn(fk),
|
||||
ccx: ccx};
|
||||
find_pre_post_fn(fcx, body);
|
||||
}
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
@ -1,623 +0,0 @@
|
||||
use ann::*;
|
||||
use aux::*;
|
||||
use tritv::*;
|
||||
|
||||
use syntax::print::pprust::block_to_str;
|
||||
use bitvectors::*;
|
||||
use pat_util::*;
|
||||
use syntax::ast::*;
|
||||
use syntax::ast_util::*;
|
||||
use syntax::print::pprust::{expr_to_str, stmt_to_str};
|
||||
use syntax::codemap::span;
|
||||
use middle::ty::{expr_ty, type_is_bot};
|
||||
use util::common::{field_exprs, has_nonlocal_exits, may_break};
|
||||
use driver::session::session;
|
||||
use std::map::hashmap;
|
||||
|
||||
fn forbid_upvar(fcx: fn_ctxt, rhs_id: node_id, sp: span, t: oper_type) {
|
||||
match t {
|
||||
oper_move {
|
||||
match local_node_id_to_def(fcx, rhs_id) {
|
||||
Some(def_upvar(_, _, _)) {
|
||||
fcx.ccx.tcx.sess.span_err(sp,
|
||||
~"tried to deinitialize a variable \
|
||||
declared in a different scope");
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
_ {/* do nothing */ }
|
||||
}
|
||||
}
|
||||
|
||||
fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
|
||||
rhs_id: node_id, destlhs: dest, init_op: init_op) {
|
||||
forbid_upvar(fcx, rhs_id, rhs_path.span, op_to_oper_ty(init_op));
|
||||
|
||||
let rhs_d_id = local_node_id_to_def_id(fcx, rhs_id);
|
||||
match rhs_d_id {
|
||||
Some(rhsid) {
|
||||
// RHS is a local var
|
||||
let instrhs =
|
||||
{ident: path_to_ident(rhs_path), node: rhsid.node};
|
||||
match destlhs {
|
||||
local_dest(instlhs) {
|
||||
copy_in_poststate(fcx, post, instlhs, instrhs,
|
||||
op_to_oper_ty(init_op));
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
}
|
||||
_ {
|
||||
// not a local -- do nothing
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: ~[binding]) ->
|
||||
{changed: bool, post: poststate} {
|
||||
let mut changed = false;
|
||||
let mut post = pres.clone();
|
||||
for bindings.each |b| {
|
||||
match b.rhs {
|
||||
Some(an_init) {
|
||||
// an expression, with or without a destination
|
||||
changed |=
|
||||
find_pre_post_state_expr(fcx, post, an_init.expr) || changed;
|
||||
post = expr_poststate(fcx.ccx, an_init.expr).clone();
|
||||
for b.lhs.each |d| {
|
||||
match an_init.expr.node {
|
||||
expr_path(p) {
|
||||
handle_move_or_copy(fcx, post, p, an_init.expr.id, d,
|
||||
an_init.op);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
|
||||
// Forget the RHS if we just moved it.
|
||||
if an_init.op == init_move {
|
||||
forget_in_poststate(fcx, post, an_init.expr.id);
|
||||
}
|
||||
}
|
||||
none {
|
||||
}
|
||||
}
|
||||
}
|
||||
return {changed: changed, post: post};
|
||||
}
|
||||
|
||||
fn find_pre_post_state_sub(fcx: fn_ctxt, pres: prestate, e: @expr,
|
||||
parent: node_id, c: Option<tsconstr>) -> bool {
|
||||
let mut changed = find_pre_post_state_expr(fcx, pres, e);
|
||||
|
||||
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
|
||||
|
||||
let post = expr_poststate(fcx.ccx, e).clone();
|
||||
match c {
|
||||
none { }
|
||||
Some(c1) { set_in_poststate_(bit_num(fcx, c1), post); }
|
||||
}
|
||||
|
||||
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
|
||||
rhs: @expr, parent: node_id, ty: oper_type) ->
|
||||
bool {
|
||||
let mut changed = set_prestate_ann(fcx.ccx, parent, pres);
|
||||
changed = find_pre_post_state_expr(fcx, pres, lhs) || changed;
|
||||
changed =
|
||||
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs), rhs) ||
|
||||
changed;
|
||||
forbid_upvar(fcx, rhs.id, rhs.span, ty);
|
||||
|
||||
let post = expr_poststate(fcx.ccx, rhs).clone();
|
||||
|
||||
match lhs.node {
|
||||
expr_path(p) {
|
||||
// for termination, need to make sure intermediate changes don't set
|
||||
// changed flag
|
||||
// tmp remembers "old" constraints we'd otherwise forget,
|
||||
// for substitution purposes
|
||||
let tmp = post.clone();
|
||||
|
||||
match ty {
|
||||
oper_move {
|
||||
if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
|
||||
forget_in_poststate(fcx, post, lhs.id);
|
||||
}
|
||||
oper_swap {
|
||||
forget_in_poststate(fcx, post, lhs.id);
|
||||
forget_in_poststate(fcx, post, rhs.id);
|
||||
}
|
||||
_ { forget_in_poststate(fcx, post, lhs.id); }
|
||||
}
|
||||
|
||||
match rhs.node {
|
||||
expr_path(p1) {
|
||||
let d = local_node_id_to_local_def_id(fcx, lhs.id);
|
||||
let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
|
||||
match d {
|
||||
Some(id) {
|
||||
match d1 {
|
||||
Some(id1) {
|
||||
let instlhs =
|
||||
{ident: path_to_ident(p), node: id};
|
||||
let instrhs =
|
||||
{ident: path_to_ident(p1), node: id1};
|
||||
copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
|
||||
ty);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
}
|
||||
_ {/* do nothing */ }
|
||||
}
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
changed = set_poststate_ann(fcx.ccx, parent, post) || changed;
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_call(fcx: fn_ctxt, pres: prestate, a: @expr,
|
||||
id: node_id, ops: ~[init_op], bs: ~[@expr],
|
||||
cf: ret_style) -> bool {
|
||||
let mut changed = find_pre_post_state_expr(fcx, pres, a);
|
||||
// FIXME (#2178): This could be a typestate constraint (except we're
|
||||
// not using them inside the compiler, I guess... see discussion in
|
||||
// bug)
|
||||
if vec::len(bs) != vec::len(ops) {
|
||||
fcx.ccx.tcx.sess.span_bug(a.span,
|
||||
fmt!("mismatched arg lengths: \
|
||||
%u exprs vs. %u ops",
|
||||
vec::len(bs), vec::len(ops)));
|
||||
}
|
||||
return find_pre_post_state_exprs(fcx, pres, id, ops,
|
||||
bs, cf) || changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id,
|
||||
ops: ~[init_op], es: ~[@expr],
|
||||
cf: ret_style) -> bool {
|
||||
let rs = seq_states(fcx, pres, arg_bindings(ops, es));
|
||||
let mut changed = rs.changed | set_prestate_ann(fcx.ccx, id, pres);
|
||||
/* if this is a failing call, it sets everything as initialized */
|
||||
match cf {
|
||||
noreturn {
|
||||
let post = false_postcond(num_constraints(fcx.enclosing));
|
||||
changed |= set_poststate_ann(fcx.ccx, id, post);
|
||||
}
|
||||
_ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
|
||||
}
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
|
||||
maybe_alt: Option<@expr>, id: node_id, chk: if_ty,
|
||||
pres: prestate) -> bool {
|
||||
let mut changed =
|
||||
set_prestate_ann(fcx.ccx, id, pres) |
|
||||
find_pre_post_state_expr(fcx, pres, antec);
|
||||
|
||||
match maybe_alt {
|
||||
none {
|
||||
match chk {
|
||||
if_check {
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
|
||||
let conseq_prestate = expr_poststate(fcx.ccx, antec).clone();
|
||||
conseq_prestate.set(bit_num(fcx, c.node), ttrue);
|
||||
changed |=
|
||||
find_pre_post_state_block(fcx, conseq_prestate, conseq) |
|
||||
set_poststate_ann(fcx.ccx, id,
|
||||
expr_poststate(fcx.ccx, antec));
|
||||
}
|
||||
_ {
|
||||
changed |=
|
||||
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
|
||||
conseq) |
|
||||
set_poststate_ann(fcx.ccx, id,
|
||||
expr_poststate(fcx.ccx, antec));
|
||||
}
|
||||
}
|
||||
}
|
||||
Some(altern) {
|
||||
changed |=
|
||||
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, antec),
|
||||
altern);
|
||||
|
||||
let mut conseq_prestate = expr_poststate(fcx.ccx, antec);
|
||||
match chk {
|
||||
if_check {
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
|
||||
conseq_prestate = conseq_prestate.clone();
|
||||
conseq_prestate.set(bit_num(fcx, c.node), ttrue);
|
||||
}
|
||||
_ { }
|
||||
}
|
||||
|
||||
|
||||
changed |= find_pre_post_state_block(fcx, conseq_prestate, conseq);
|
||||
|
||||
let poststate_res =
|
||||
intersect_states(block_poststate(fcx.ccx, conseq),
|
||||
expr_poststate(fcx.ccx, altern));
|
||||
/*
|
||||
fcx.ccx.tcx.sess.span_note(antec.span,
|
||||
"poststate_res = " + aux::tritv_to_str(fcx, poststate_res));
|
||||
fcx.ccx.tcx.sess.span_note(antec.span,
|
||||
"altern poststate = " +
|
||||
aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern)));
|
||||
fcx.ccx.tcx.sess.span_note(antec.span,
|
||||
"conseq poststate = " + aux::tritv_to_str(fcx,
|
||||
block_poststate(fcx.ccx, conseq)));
|
||||
*/
|
||||
|
||||
changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
|
||||
}
|
||||
}
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
|
||||
pres: prestate, cap_clause: capture_clause)
|
||||
-> bool
|
||||
{
|
||||
let ccx = fcx.ccx;
|
||||
let pres_changed = set_prestate_ann(ccx, e_id, pres);
|
||||
let post = pres.clone();
|
||||
for (*cap_clause).each |cap_item| {
|
||||
if cap_item.is_move {
|
||||
forget_in_poststate(fcx, post, cap_item.id);
|
||||
}
|
||||
}
|
||||
return set_poststate_ann(ccx, e_id, post) || pres_changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
|
||||
let num_constrs = num_constraints(fcx.enclosing);
|
||||
|
||||
match e.node {
|
||||
expr_new(p, _, v) {
|
||||
return find_pre_post_state_two(fcx, pres, p, v, e.id, oper_pure);
|
||||
}
|
||||
expr_vstore(ee, _) {
|
||||
let mut changed = find_pre_post_state_expr(fcx, pres, ee);
|
||||
set_prestate_ann(fcx.ccx, e.id, expr_prestate(fcx.ccx, ee));
|
||||
set_poststate_ann(fcx.ccx, e.id, expr_poststate(fcx.ccx, ee));
|
||||
return changed;
|
||||
}
|
||||
expr_vec(elts, _) {
|
||||
return find_pre_post_state_exprs(fcx, pres, e.id,
|
||||
vec::from_elem(vec::len(elts),
|
||||
init_assign), elts,
|
||||
return_val);
|
||||
}
|
||||
expr_call(operator, operands, _) {
|
||||
debug!("hey it's a call: %s", expr_to_str(e));
|
||||
return find_pre_post_state_call(fcx, pres, operator, e.id,
|
||||
callee_arg_init_ops(fcx, operator.id),
|
||||
operands,
|
||||
controlflow_expr(fcx.ccx, operator));
|
||||
}
|
||||
expr_path(_) { return pure_exp(fcx.ccx, e.id, pres); }
|
||||
expr_log(_, lvl, ex) {
|
||||
return find_pre_post_state_two(fcx, pres, lvl, ex, e.id, oper_pure);
|
||||
}
|
||||
expr_mac(_) { fcx.ccx.tcx.sess.bug(~"unexpanded macro"); }
|
||||
expr_lit(l) { return pure_exp(fcx.ccx, e.id, pres); }
|
||||
expr_fn(_, _, _, cap_clause) {
|
||||
return find_pre_post_state_cap_clause(fcx, e.id, pres, cap_clause);
|
||||
}
|
||||
expr_fn_block(_, _, cap_clause) {
|
||||
return find_pre_post_state_cap_clause(fcx, e.id, pres, cap_clause);
|
||||
}
|
||||
expr_block(b) {
|
||||
return 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));
|
||||
}
|
||||
expr_rec(fields, maybe_base) {
|
||||
let exs = field_exprs(fields);
|
||||
let mut changed =
|
||||
find_pre_post_state_exprs(fcx, pres, e.id,
|
||||
vec::from_elem(vec::len(fields),
|
||||
init_assign),
|
||||
exs, return_val);
|
||||
|
||||
let base_pres = match vec::last_opt(exs) { none { pres }
|
||||
Some(f) { expr_poststate(fcx.ccx, f) }};
|
||||
option::iter(maybe_base, |base| {
|
||||
changed |= find_pre_post_state_expr(fcx, base_pres, base) |
|
||||
set_poststate_ann(fcx.ccx, e.id,
|
||||
expr_poststate(fcx.ccx, base))
|
||||
});
|
||||
return changed;
|
||||
}
|
||||
expr_tup(elts) {
|
||||
return find_pre_post_state_exprs(fcx, pres, e.id,
|
||||
vec::from_elem(vec::len(elts),
|
||||
init_assign), elts,
|
||||
return_val);
|
||||
}
|
||||
expr_move(lhs, rhs) {
|
||||
return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_move);
|
||||
}
|
||||
expr_assign(lhs, rhs) {
|
||||
return find_pre_post_state_two(
|
||||
fcx, pres, lhs, rhs, e.id, oper_assign);
|
||||
}
|
||||
expr_swap(lhs, rhs) {
|
||||
return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, oper_swap);
|
||||
// Could be more precise and actually swap the role of
|
||||
// lhs and rhs in constraints
|
||||
}
|
||||
expr_ret(maybe_ret_val) {
|
||||
let mut changed = set_prestate_ann(fcx.ccx, e.id, pres);
|
||||
/* everything is true if execution continues after
|
||||
a return expression (since execution never continues locally
|
||||
after a return expression */
|
||||
let post = false_postcond(num_constrs);
|
||||
|
||||
set_poststate_ann(fcx.ccx, e.id, post);
|
||||
|
||||
match maybe_ret_val {
|
||||
none {/* do nothing */ }
|
||||
Some(ret_val) {
|
||||
changed |= find_pre_post_state_expr(fcx, pres, ret_val);
|
||||
}
|
||||
}
|
||||
return changed;
|
||||
}
|
||||
expr_if(antec, conseq, maybe_alt) {
|
||||
return join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if,
|
||||
pres);
|
||||
}
|
||||
expr_binary(bop, l, r) {
|
||||
if lazy_binop(bop) {
|
||||
let mut changed = find_pre_post_state_expr(fcx, pres, l);
|
||||
changed |=
|
||||
find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r);
|
||||
return changed | set_prestate_ann(fcx.ccx, e.id, pres) |
|
||||
set_poststate_ann(fcx.ccx, e.id,
|
||||
expr_poststate(fcx.ccx, l));
|
||||
} else {
|
||||
return find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
|
||||
}
|
||||
}
|
||||
expr_assign_op(op, lhs, rhs) {
|
||||
return find_pre_post_state_two(fcx, pres, lhs, rhs, e.id,
|
||||
oper_assign_op);
|
||||
}
|
||||
expr_while(test, body) {
|
||||
let loop_pres =
|
||||
intersect_states(block_poststate(fcx.ccx, body), pres);
|
||||
|
||||
let mut changed =
|
||||
set_prestate_ann(fcx.ccx, e.id, loop_pres) |
|
||||
find_pre_post_state_expr(fcx, loop_pres, test) |
|
||||
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
|
||||
body);
|
||||
|
||||
/* conservative approximation: if a loop contains a break
|
||||
or cont, we assume nothing about the poststate */
|
||||
/* which is still unsound -- see ~[Break-unsound] */
|
||||
if has_nonlocal_exits(body) {
|
||||
return changed | set_poststate_ann(fcx.ccx, e.id, pres);
|
||||
} else {
|
||||
let e_post = expr_poststate(fcx.ccx, test);
|
||||
let b_post = block_poststate(fcx.ccx, body);
|
||||
return changed |
|
||||
set_poststate_ann(fcx.ccx, e.id,
|
||||
intersect_states(e_post, b_post));
|
||||
}
|
||||
}
|
||||
expr_loop(body) {
|
||||
let loop_pres =
|
||||
intersect_states(block_poststate(fcx.ccx, body), pres);
|
||||
let mut changed = set_prestate_ann(fcx.ccx, e.id, loop_pres)
|
||||
| find_pre_post_state_block(fcx, loop_pres, body);
|
||||
/* conservative approximation: if a loop contains a break
|
||||
or cont, we assume nothing about the poststate (so, we
|
||||
set all predicates to "don't know" */
|
||||
/* which is still unsound -- see ~[Break-unsound] */
|
||||
if may_break(body) {
|
||||
/* Only do this if there are *breaks* not conts.
|
||||
An infinite loop with conts is still an infinite loop.
|
||||
We assume all preds are FALSE, not '?' -- because in the
|
||||
worst case, the body could invalidate all preds and
|
||||
deinitialize everything before breaking */
|
||||
let post = empty_poststate(num_constrs);
|
||||
post.kill();
|
||||
return changed | set_poststate_ann(fcx.ccx, e.id, post);
|
||||
} else {
|
||||
return changed | set_poststate_ann(fcx.ccx, e.id,
|
||||
false_postcond(num_constrs));
|
||||
}
|
||||
}
|
||||
expr_index(val, sub) {
|
||||
return find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure);
|
||||
}
|
||||
expr_match(val, alts, _) {
|
||||
let mut changed =
|
||||
set_prestate_ann(fcx.ccx, e.id, pres) |
|
||||
find_pre_post_state_expr(fcx, pres, val);
|
||||
let e_post = expr_poststate(fcx.ccx, val);
|
||||
let mut a_post;
|
||||
if vec::len(alts) > 0u {
|
||||
a_post = false_postcond(num_constrs);
|
||||
for alts.each |an_alt| {
|
||||
match an_alt.guard {
|
||||
Some(e) {
|
||||
changed |= find_pre_post_state_expr(fcx, e_post, e);
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
changed |=
|
||||
find_pre_post_state_block(fcx, e_post, an_alt.body);
|
||||
intersect(a_post, block_poststate(fcx.ccx, an_alt.body));
|
||||
// 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.
|
||||
|
||||
}
|
||||
} else {
|
||||
// No alts; poststate is the poststate of the test
|
||||
|
||||
a_post = e_post;
|
||||
}
|
||||
return changed | set_poststate_ann(fcx.ccx, e.id, a_post);
|
||||
}
|
||||
expr_field(x, _, _) | expr_loop_body(x) | expr_do_body(x) |
|
||||
expr_unary(_, x) |
|
||||
expr_addr_of(_, x) | expr_assert(x) | expr_cast(x, _) |
|
||||
expr_copy(x) {
|
||||
return find_pre_post_state_sub(fcx, pres, x, e.id, None);
|
||||
}
|
||||
expr_fail(maybe_fail_val) {
|
||||
/* if execution continues after fail, then everything is true!
|
||||
woo! */
|
||||
let post = false_postcond(num_constrs);
|
||||
return set_prestate_ann(fcx.ccx, e.id, pres) |
|
||||
set_poststate_ann(fcx.ccx, e.id, post) |
|
||||
option::map_default(
|
||||
maybe_fail_val, false,
|
||||
|fail_val|
|
||||
find_pre_post_state_expr(fcx, pres, fail_val) );
|
||||
}
|
||||
expr_check(_, p) {
|
||||
/* predicate p holds after this expression executes */
|
||||
let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
|
||||
return find_pre_post_state_sub(fcx, pres, p, e.id, Some(c.node));
|
||||
}
|
||||
expr_if_check(p, conseq, maybe_alt) {
|
||||
return join_then_else(
|
||||
fcx, p, conseq, maybe_alt, e.id, if_check, pres);
|
||||
}
|
||||
expr_break { return pure_exp(fcx.ccx, e.id, pres); }
|
||||
expr_again { return pure_exp(fcx.ccx, e.id, pres); }
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_state_stmt(fcx: fn_ctxt, pres: prestate, s: @stmt) -> bool {
|
||||
let stmt_ann = stmt_to_ann(fcx.ccx, *s);
|
||||
|
||||
debug!("[ %s ]", *fcx.name);
|
||||
debug!("*At beginning: stmt = %s", stmt_to_str(*s));
|
||||
debug!("*prestate = %s", stmt_ann.states.prestate.to_str());
|
||||
debug!("*poststate = %s", stmt_ann.states.prestate.to_str());
|
||||
|
||||
match s.node {
|
||||
stmt_decl(adecl, id) {
|
||||
match adecl.node {
|
||||
decl_local(alocals) {
|
||||
set_prestate(stmt_ann, pres);
|
||||
let c_and_p = seq_states(fcx, pres,
|
||||
locals_to_bindings(fcx.ccx.tcx, alocals));
|
||||
/* important to do this in one step to ensure
|
||||
termination (don't want to set changed to true
|
||||
for intermediate changes) */
|
||||
|
||||
let mut changed =
|
||||
set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed;
|
||||
|
||||
debug!("Summary: stmt = %s", stmt_to_str(*s));
|
||||
debug!("prestate = %s", stmt_ann.states.prestate.to_str());
|
||||
debug!("poststate = %s", stmt_ann.states.poststate.to_str());
|
||||
debug!("changed = %s", bool::to_str(changed));
|
||||
|
||||
return changed;
|
||||
}
|
||||
decl_item(an_item) {
|
||||
return set_prestate(stmt_ann, pres)
|
||||
| set_poststate(stmt_ann, pres);
|
||||
/* the outer visitor will recurse into the item */
|
||||
}
|
||||
}
|
||||
}
|
||||
stmt_expr(ex, _) | stmt_semi(ex, _) {
|
||||
let mut changed =
|
||||
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));
|
||||
|
||||
|
||||
debug!("Finally: %s", stmt_to_str(*s));
|
||||
debug!("prestate = %s", stmt_ann.states.prestate.to_str());
|
||||
debug!("poststate = %s", stmt_ann.states.poststate.to_str());
|
||||
debug!("changed = %s", bool::to_str(changed));
|
||||
|
||||
return changed;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* Updates the pre- and post-states of statements in the block,
|
||||
returns a boolean flag saying whether any pre- or poststates changed */
|
||||
fn find_pre_post_state_block(fcx: fn_ctxt, pres0: prestate, b: blk) -> bool {
|
||||
/* First, set the pre-states and post-states for every expression */
|
||||
|
||||
let mut 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. */
|
||||
|
||||
let mut changed = false;
|
||||
for b.node.stmts.each |s| {
|
||||
changed |= find_pre_post_state_stmt(fcx, pres, s);
|
||||
pres = stmt_poststate(fcx.ccx, *s);
|
||||
}
|
||||
let mut post = pres;
|
||||
match b.node.expr {
|
||||
none { }
|
||||
Some(e) {
|
||||
changed |= find_pre_post_state_expr(fcx, pres, e);
|
||||
post = expr_poststate(fcx.ccx, e);
|
||||
}
|
||||
}
|
||||
|
||||
set_prestate_ann(fcx.ccx, b.node.id, pres0);
|
||||
set_poststate_ann(fcx.ccx, b.node.id, post);
|
||||
|
||||
return changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_fn(fcx: fn_ctxt,
|
||||
f_decl: fn_decl,
|
||||
f_body: blk) -> bool {
|
||||
// All constraints are considered false until proven otherwise.
|
||||
// This ensures that intersect works correctly.
|
||||
kill_all_prestate(fcx, f_body.node.id);
|
||||
|
||||
// Instantiate any constraints on the arguments so we can use them
|
||||
let block_pre = block_prestate(fcx.ccx, f_body);
|
||||
for f_decl.constraints.each |c| {
|
||||
let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c);
|
||||
set_in_prestate_constr(fcx, tsc, block_pre);
|
||||
}
|
||||
|
||||
let mut changed = find_pre_post_state_block(fcx, block_pre, f_body);
|
||||
|
||||
/*
|
||||
error!("find_pre_post_state_fn");
|
||||
log(error, changed);
|
||||
fcx.ccx.tcx.sess.span_note(f_body.span, fcx.name);
|
||||
*/
|
||||
|
||||
return changed;
|
||||
}
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
//
|
||||
Loading…
x
Reference in New Issue
Block a user