fn parse_dtor(parser p) -> @ast::method {
auto lo = p.get_last_lo_pos();
let ast::block b = parse_block(p);
- let vec[ast::arg] inputs = vec();
+ let vec[ast::arg] inputs = [];
let @ast::ty output = @spanned(lo, lo, ast::ty_nil);
let ast::fn_decl d = rec(inputs=inputs,
- output=output,
- purity=ast::impure_fn);
+ output=output,
+ purity=ast::impure_fn,
+ cf=ast::return);
let ast::_fn f = rec(decl = d,
- proto = ast::proto_fn,
- body = b);
+ proto = ast::proto_fn,
+ body = b);
let ast::method_ m = rec(ident="drop",
meth=f,
id=p.next_def_id(),
fn fold_fn_decl[ENV](&ENV env, &ast_fold[ENV] fld,
&ast::fn_decl decl) -> ast::fn_decl {
- let vec[ast::arg] inputs = vec();
+ let vec[ast::arg] inputs = [];
for (ast::arg a in decl.inputs) {
- inputs += vec(fold_arg(env, fld, a));
+ inputs += [fold_arg(env, fld, a)];
}
auto output = fold_ty[ENV](env, fld, decl.output);
- ret fld.fold_fn_decl(env, inputs, output, decl.purity);
+ ret fld.fold_fn_decl(env, inputs, output, decl.purity, decl.cf);
}
fn fold_fn[ENV](&ENV env, &ast_fold[ENV] fld, &ast::_fn f) -> ast::_fn {
auto lhs_false_cx = new_scope_block_ctxt(cx, "lhs false");
auto lhs_false_res = res(lhs_false_cx, C_bool(false));
- // are done within the block for rhs. This is necessary
+ // The following line ensures that any cleanups for rhs
++ // are done within the block for rhs. This is necessary
+ // because and/or are lazy. So the rhs may never execute,
+ // and the cleanups can't be pushed into later code.
+ auto rhs_bcx = trans_block_cleanups(rhs_res.bcx, rhs_cx);
+
lhs_res.bcx.build.CondBr(lhs_res.val,
rhs_cx.llbb,
lhs_false_cx.llbb);
-
ret join_results(cx, T_bool(),
- [lhs_false_res, rhs_res]);
- vec(lhs_false_res, rec(bcx=rhs_bcx with rhs_res)));
++ [lhs_false_res, rec(bcx=rhs_bcx with rhs_res)]);
}
case (ast::or) {
rhs_cx.llbb);
ret join_results(cx, T_bool(),
- [lhs_true_res, rhs_res]);
- vec(lhs_true_res, rec(bcx=rhs_bcx with rhs_res)));
++ [lhs_true_res, rec(bcx=rhs_bcx with rhs_res)]);
}
case (_) {
--- /dev/null
- let vec[@stmt] new_stmts = vec();
+ import std::_vec;
+ import std::option;
+ import std::option::some;
+ import std::option::none;
+
+ import front::ast;
+
+ import front::ast::ident;
+ import front::ast::def_id;
+ import front::ast::ann;
+ import front::ast::item;
+ import front::ast::_fn;
+ import front::ast::_mod;
+ import front::ast::crate;
+ import front::ast::_obj;
+ import front::ast::ty_param;
+ import front::ast::item_fn;
+ import front::ast::item_obj;
+ import front::ast::item_ty;
+ import front::ast::item_tag;
+ import front::ast::item_const;
+ import front::ast::item_mod;
+ import front::ast::item_native_mod;
+ import front::ast::expr;
+ import front::ast::elt;
+ import front::ast::field;
+ import front::ast::decl;
+ import front::ast::decl_local;
+ import front::ast::decl_item;
+ import front::ast::initializer;
+ import front::ast::local;
+ import front::ast::arm;
+ import front::ast::expr_call;
+ import front::ast::expr_vec;
+ import front::ast::expr_tup;
+ import front::ast::expr_path;
+ import front::ast::expr_field;
+ import front::ast::expr_index;
+ import front::ast::expr_log;
+ import front::ast::expr_block;
+ import front::ast::expr_rec;
+ import front::ast::expr_if;
+ import front::ast::expr_binary;
+ import front::ast::expr_unary;
+ import front::ast::expr_assign;
+ import front::ast::expr_assign_op;
+ import front::ast::expr_while;
+ import front::ast::expr_do_while;
+ import front::ast::expr_alt;
+ import front::ast::expr_lit;
+ import front::ast::expr_ret;
+ import front::ast::expr_self_method;
+ import front::ast::expr_bind;
+ import front::ast::expr_spawn;
+ import front::ast::expr_ext;
+ import front::ast::expr_fail;
+ import front::ast::expr_break;
+ import front::ast::expr_cont;
+ import front::ast::expr_send;
+ import front::ast::expr_recv;
+ import front::ast::expr_put;
+ import front::ast::expr_port;
+ import front::ast::expr_chan;
+ import front::ast::expr_be;
+ import front::ast::expr_check;
+ import front::ast::expr_assert;
+ import front::ast::expr_cast;
+ import front::ast::expr_for;
+ import front::ast::expr_for_each;
+ import front::ast::stmt;
+ import front::ast::stmt_decl;
+ import front::ast::stmt_expr;
+ import front::ast::block;
+ import front::ast::block_;
+ import front::ast::method;
+
+ import middle::fold;
+ import middle::fold::respan;
+ import middle::fold::new_identity_fold;
+ import middle::fold::fold_crate;
+ import middle::fold::fold_item;
+ import middle::fold::fold_method;
+
+ import util::common::uistr;
+ import util::common::span;
+ import util::common::new_str_hash;
+
+ import middle::tstate::aux::fn_info;
+ import middle::tstate::aux::fn_info_map;
+ import middle::tstate::aux::num_locals;
+ import middle::tstate::aux::init_ann;
+ import middle::tstate::aux::init_blank_ann;
+ import middle::tstate::aux::get_fn_info;
+
+ fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &_fn f,
+ vec[ty_param] ty_params, def_id id, ann a) -> @item {
+
+ assert (fm.contains_key(id));
+ auto f_info = fm.get(id);
+
+ log(i + " has " + uistr(num_locals(f_info)) + " local vars");
+
+ auto fld0 = new_identity_fold[fn_info]();
+
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ with *fld0);
+
+ ret fold_item[fn_info]
+ (f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a)));
+ }
+
+ /* FIXME: rewrite this with walk instead of fold */
+
+ /* This is painstakingly written as an explicit recursion b/c the
+ standard ast.fold doesn't traverse in the correct order:
+ consider
+ fn foo() {
+ fn bar() {
+ auto x = 5;
+ log(x);
+ }
+ }
+ With fold, first bar() would be processed and its subexps would
+ correctly be annotated with length-1 bit vectors.
+ But then, the process would be repeated with (fn bar()...) as
+ a subexp of foo, which has 0 local variables -- so then
+ the body of bar() would be incorrectly annotated with length-0 bit
+ vectors. */
+ fn annotate_exprs(&fn_info_map fm, &vec[@expr] es) -> vec[@expr] {
+ fn one(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind one(fm,_);
+ ret _vec::map[@expr, @expr](f, es);
+ }
+ fn annotate_elts(&fn_info_map fm, &vec[elt] es) -> vec[elt] {
+ fn one(fn_info_map fm, &elt e) -> elt {
+ ret rec(mut=e.mut,
+ expr=annotate_expr(fm, e.expr));
+ }
+ auto f = bind one(fm,_);
+ ret _vec::map[elt, elt](f, es);
+ }
+ fn annotate_fields(&fn_info_map fm, &vec[field] fs) -> vec[field] {
+ fn one(fn_info_map fm, &field f) -> field {
+ ret rec(mut=f.mut,
+ ident=f.ident,
+ expr=annotate_expr(fm, f.expr));
+ }
+ auto f = bind one(fm,_);
+ ret _vec::map[field, field](f, fs);
+ }
+ fn annotate_option_exp(&fn_info_map fm, &option::t[@expr] o)
+ -> option::t[@expr] {
+ fn one(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind one(fm,_);
+ ret option::map[@expr, @expr](f, o);
+ }
+ fn annotate_option_exprs(&fn_info_map fm, &vec[option::t[@expr]] es)
+ -> vec[option::t[@expr]] {
+ fn one(fn_info_map fm, &option::t[@expr] o) -> option::t[@expr] {
+ ret annotate_option_exp(fm, o);
+ }
+ auto f = bind one(fm,_);
+ ret _vec::map[option::t[@expr], option::t[@expr]](f, es);
+ }
+ fn annotate_decl(&fn_info_map fm, &@decl d) -> @decl {
+ auto d1 = d.node;
+ alt (d.node) {
+ case (decl_local(?l)) {
+ alt(l.init) {
+ case (some[initializer](?init)) {
+ let option::t[initializer] an_i =
+ some[initializer]
+ (rec(expr=annotate_expr(fm, init.expr)
+ with init));
+ let @local new_l = @rec(init=an_i with *l);
+ d1 = decl_local(new_l);
+ }
+ case (_) { /* do nothing */ }
+ }
+ }
+ case (decl_item(?item)) {
+ d1 = decl_item(annotate_item(fm, item));
+ }
+ }
+ ret @respan(d.span, d1);
+ }
+ fn annotate_alts(&fn_info_map fm, &vec[arm] alts) -> vec[arm] {
+ fn one(fn_info_map fm, &arm a) -> arm {
+ ret rec(pat=a.pat,
+ block=annotate_block(fm, a.block));
+ }
+ auto f = bind one(fm,_);
+ ret _vec::map[arm, arm](f, alts);
+
+ }
+ fn annotate_expr(&fn_info_map fm, &@expr e) -> @expr {
+ auto e1 = e.node;
+ alt (e.node) {
+ case (expr_vec(?es, ?m, ?a)) {
+ e1 = expr_vec(annotate_exprs(fm, es), m, a);
+ }
+ case (expr_tup(?es, ?a)) {
+ e1 = expr_tup(annotate_elts(fm, es), a);
+ }
+ case (expr_rec(?fs, ?maybe_e, ?a)) {
+ e1 = expr_rec(annotate_fields(fm, fs),
+ annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_call(?e, ?es, ?a)) {
+ e1 = expr_call(annotate_expr(fm, e),
+ annotate_exprs(fm, es), a);
+ }
+ case (expr_self_method(_,_)) {
+ // no change
+ }
+ case (expr_bind(?e, ?maybe_es, ?a)) {
+ e1 = expr_bind(annotate_expr(fm, e),
+ annotate_option_exprs(fm, maybe_es),
+ a);
+ }
+ case (expr_spawn(?s, ?maybe_s, ?e, ?es, ?a)) {
+ e1 = expr_spawn(s, maybe_s, annotate_expr(fm, e),
+ annotate_exprs(fm, es), a);
+ }
+ case (expr_binary(?bop, ?w, ?x, ?a)) {
+ e1 = expr_binary(bop, annotate_expr(fm, w),
+ annotate_expr(fm, x), a);
+ }
+ case (expr_unary(?uop, ?w, ?a)) {
+ e1 = expr_unary(uop, annotate_expr(fm, w), a);
+ }
+ case (expr_lit(_,_)) {
+ /* no change */
+ }
+ case (expr_cast(?e,?t,?a)) {
+ e1 = expr_cast(annotate_expr(fm, e), t, a);
+ }
+ case (expr_if(?e, ?b, ?maybe_e, ?a)) {
+ e1 = expr_if(annotate_expr(fm, e),
+ annotate_block(fm, b),
+ annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_while(?e, ?b, ?a)) {
+ e1 = expr_while(annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_for(?d, ?e, ?b, ?a)) {
+ e1 = expr_for(annotate_decl(fm, d),
+ annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_for_each(?d, ?e, ?b, ?a)) {
+ e1 = expr_for_each(annotate_decl(fm, d),
+ annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_do_while(?b, ?e, ?a)) {
+ e1 = expr_do_while(annotate_block(fm, b),
+ annotate_expr(fm, e), a);
+ }
+ case (expr_alt(?e, ?alts, ?a)) {
+ e1 = expr_alt(annotate_expr(fm, e),
+ annotate_alts(fm, alts), a);
+ }
+ case (expr_block(?b, ?a)) {
+ e1 = expr_block(annotate_block(fm, b), a);
+ }
+ case (expr_assign(?l, ?r, ?a)) {
+ e1 = expr_assign(annotate_expr(fm, l), annotate_expr(fm, r), a);
+ }
+ case (expr_assign_op(?bop, ?l, ?r, ?a)) {
+ e1 = expr_assign_op(bop,
+ annotate_expr(fm, l), annotate_expr(fm, r), a);
+ }
+ case (expr_send(?l, ?r, ?a)) {
+ e1 = expr_send(annotate_expr(fm, l),
+ annotate_expr(fm, r), a);
+ }
+ case (expr_recv(?l, ?r, ?a)) {
+ e1 = expr_recv(annotate_expr(fm, l),
+ annotate_expr(fm, r), a);
+ }
+ case (expr_field(?e, ?i, ?a)) {
+ e1 = expr_field(annotate_expr(fm, e),
+ i, a);
+ }
+ case (expr_index(?e, ?sub, ?a)) {
+ e1 = expr_index(annotate_expr(fm, e),
+ annotate_expr(fm, sub), a);
+ }
+ case (expr_path(_,_)) {
+ /* no change */
+ }
+ case (expr_ext(?p, ?es, ?s_opt, ?e, ?a)) {
+ e1 = expr_ext(p, annotate_exprs(fm, es),
+ s_opt,
+ annotate_expr(fm, e), a);
+ }
+ /* no change, next 3 cases */
+ case (expr_fail(_)) { }
+ case (expr_break(_)) { }
+ case (expr_cont(_)) { }
+ case (expr_ret(?maybe_e, ?a)) {
+ e1 = expr_ret(annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_put(?maybe_e, ?a)) {
+ e1 = expr_put(annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_be(?e, ?a)) {
+ e1 = expr_be(annotate_expr(fm, e), a);
+ }
+ case (expr_log(?n, ?e, ?a)) {
+ e1 = expr_log(n, annotate_expr(fm, e), a);
+ }
+ case (expr_assert(?e, ?a)) {
+ e1 = expr_assert(annotate_expr(fm, e), a);
+ }
+ case (expr_check(?e, ?a)) {
+ e1 = expr_check(annotate_expr(fm, e), a);
+ }
+ case (expr_port(_)) { /* no change */ }
+ case (expr_chan(?e, ?a)) {
+ e1 = expr_chan(annotate_expr(fm, e), a);
+ }
+ }
+ ret @respan(e.span, e1);
+ }
+
+ fn annotate_stmt(&fn_info_map fm, &@stmt s) -> @stmt {
+ alt (s.node) {
+ case (stmt_decl(?d, ?a)) {
+ ret @respan(s.span, stmt_decl(annotate_decl(fm, d), a));
+ }
+ case (stmt_expr(?e, ?a)) {
+ ret @respan(s.span, stmt_expr(annotate_expr(fm, e), a));
+ }
+ }
+ }
+ fn annotate_block(&fn_info_map fm, &block b) -> block {
- let vec[@item] new_items = vec();
++ let vec[@stmt] new_stmts = [];
+
+ for (@stmt s in b.node.stmts) {
+ auto new_s = annotate_stmt(fm, s);
+ _vec::push[@stmt](new_stmts, new_s);
+ }
+ fn ann_e(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind ann_e(fm,_);
+
+ auto new_e = option::map[@expr, @expr](f, b.node.expr);
+
+ ret respan(b.span,
+ rec(stmts=new_stmts, expr=new_e with b.node));
+ }
+ fn annotate_fn(&fn_info_map fm, &_fn f) -> _fn {
+ // subexps have *already* been annotated based on
+ // f's number-of-locals
+ ret rec(body=annotate_block(fm, f.body) with f);
+ }
+ fn annotate_mod(&fn_info_map fm, &_mod m) -> _mod {
- let vec[@item] new_items = vec();
++ let vec[@item] new_items = [];
+
+ for (@item i in m.items) {
+ auto new_i = annotate_item(fm, i);
+ _vec::push[@item](new_items, new_i);
+ }
+ ret rec(items=new_items with m);
+ }
+ fn annotate_method(&fn_info_map fm, &@method m) -> @method {
+ auto f_info = get_fn_info(fm, m.node.id);
+ auto fld0 = new_identity_fold[fn_info]();
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ with *fld0);
+ auto outer = fold_method[fn_info](f_info, fld0, m);
+ auto new_fn = annotate_fn(fm, outer.node.meth);
+ ret @respan(m.span,
+ rec(meth=new_fn with m.node));
+ }
+
+ fn annotate_obj(&fn_info_map fm, &_obj o) -> _obj {
+ fn one(fn_info_map fm, &@method m) -> @method {
+ ret annotate_method(fm, m);
+ }
+ auto f = bind one(fm,_);
+ auto new_methods = _vec::map[@method, @method](f, o.methods);
+ auto new_dtor = option::map[@method, @method](f, o.dtor);
+ ret rec(methods=new_methods, dtor=new_dtor with o);
+ }
+
+
+ // Only annotates the components of the item recursively.
+ fn annotate_item_inner(&fn_info_map fm, &@item item) -> @item {
+ alt (item.node) {
+ /* FIXME can't skip this case -- exprs contain blocks contain stmts,
+ which contain decls */
+ case (item_const(_,_,_,_,_)) {
+ // this has already been annotated by annotate_item
+ ret item;
+ }
+ case (item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
+ ret @respan(item.span,
+ item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
+ }
+ case (item_mod(?ident, ?mm, ?id)) {
+ ret @respan(item.span,
+ item_mod(ident, annotate_mod(fm, mm), id));
+ }
+ case (item_native_mod(?ident, ?mm, ?id)) {
+ ret item;
+ }
+ case (item_ty(_,_,_,_,_)) {
+ ret item;
+ }
+ case (item_tag(_,_,_,_,_)) {
+ ret item;
+ }
+ case (item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
+ ret @respan(item.span,
+ item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
+ }
+ }
+ }
+
+ fn annotate_item(&fn_info_map fm, &@item item) -> @item {
+ // Using a fold, recursively set all anns in this item
+ // to be blank.
+ // *Then*, call annotate_item recursively to do the right
+ // thing for any nested items inside this one.
+
+ alt (item.node) {
+ case (item_const(_,_,_,_,_)) {
+ auto fld0 = new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ ret fold_item[()]((), fld0, item);
+ }
+ case (item_fn(?i,?ff,?tps,?id,?ann)) {
+ auto f_info = get_fn_info(fm, id);
+ auto fld0 = new_identity_fold[fn_info]();
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ with *fld0);
+ auto outer = fold_item[fn_info](f_info, fld0, item);
+ // now recurse into any nested items
+ ret annotate_item_inner(fm, outer);
+ }
+ case (item_mod(?i, ?mm, ?id)) {
+ auto fld0 = new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ auto outer = fold_item[()]((), fld0, item);
+ ret annotate_item_inner(fm, outer);
+ }
+ case (item_native_mod(?i, ?nm, ?id)) {
+ ret item;
+ }
+ case (item_ty(_,_,_,_,_)) {
+ ret item;
+ }
+ case (item_tag(_,_,_,_,_)) {
+ ret item;
+ }
+ case (item_obj(?i,?ob,?tps,?odid,?ann)) {
+ auto fld0 = new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ auto outer = fold_item[()]((), fld0, item);
+ ret annotate_item_inner(fm, outer);
+ }
+ }
+ }
+
+ fn annotate_module(&fn_info_map fm, &_mod module) -> _mod {
++ let vec[@item] new_items = [];
+
+ for (@item i in module.items) {
+ auto new_item = annotate_item(fm, i);
+ _vec::push[@item](new_items, new_item);
+ }
+
+ ret rec(items = new_items with module);
+ }
+
+ fn annotate_crate(&fn_info_map fm, &@crate crate) -> @crate {
+ ret @respan(crate.span,
+ rec(module = annotate_module(fm, crate.node.module)
+ with crate.node));
+ }
--- /dev/null
- seq_preconds(fcx.enclosing, vec(expr_pp(index),
- block_pp(body))));
+ import std::_vec;
+ import std::_vec::plus_option;
+ import std::option;
+ import std::option::none;
+ import std::option::some;
+
+ import tstate::ann::pre_and_post;
+ import tstate::ann::get_post;
+ import tstate::ann::postcond;
+ import tstate::ann::true_precond;
+ import tstate::ann::false_postcond;
+ import tstate::ann::empty_pre_post;
+ import tstate::ann::empty_poststate;
+ import tstate::ann::require_and_preserve;
+ import tstate::ann::union;
+ import tstate::ann::intersect;
+ import tstate::ann::pp_clone;
+ import tstate::ann::empty_prestate;
+ import aux::var_info;
+ import aux::crate_ctxt;
+ import aux::fn_ctxt;
+ import aux::num_locals;
+ import aux::expr_pp;
+ import aux::stmt_pp;
+ import aux::block_pp;
+ import aux::set_pre_and_post;
+ import aux::expr_precond;
+ import aux::expr_postcond;
+ import aux::expr_prestate;
+ import aux::expr_poststate;
+ import aux::block_postcond;
+ import aux::fn_info;
+ import aux::log_pp;
+ import aux::ann_to_def;
+ import aux::ann_to_def_strict;
+
+ import bitvectors::seq_preconds;
+ import bitvectors::union_postconds;
+ import bitvectors::intersect_postconds;
+ import bitvectors::declare_var;
+ import bitvectors::bit_num;
+ import bitvectors::gen;
+
+ import front::ast::_mod;
+ import front::ast;
+ import front::ast::method;
+ import front::ast::ann;
+ import front::ast::ty;
+ import front::ast::mutability;
+ import front::ast::item;
+ import front::ast::item_const;
+ import front::ast::item_mod;
+ import front::ast::item_ty;
+ import front::ast::item_tag;
+ import front::ast::item_native_mod;
+ import front::ast::obj_field;
+ import front::ast::stmt;
+ import front::ast::stmt_;
+ import front::ast::stmt_decl;
+ import front::ast::ident;
+ import front::ast::def_id;
+ import front::ast::ann;
+ import front::ast::expr;
+ import front::ast::path;
+ import front::ast::crate_directive;
+ import front::ast::fn_decl;
+ import front::ast::_obj;
+ import front::ast::native_mod;
+ import front::ast::variant;
+ import front::ast::ty_param;
+ import front::ast::ty;
+ import front::ast::proto;
+ import front::ast::pat;
+ import front::ast::binop;
+ import front::ast::unop;
+ import front::ast::def;
+ import front::ast::lit;
+ import front::ast::init_op;
+ import front::ast::controlflow;
+ import front::ast::return;
+ import front::ast::noreturn;
+ import front::ast::_fn;
+ import front::ast::ann_none;
+ import front::ast::ann_type;
+ import front::ast::_obj;
+ import front::ast::_mod;
+ import front::ast::crate;
+ import front::ast::item_fn;
+ import front::ast::item_obj;
+ import front::ast::def_local;
+ import front::ast::def_fn;
+ import front::ast::ident;
+ import front::ast::def_id;
+ import front::ast::ann;
+ import front::ast::item;
+ import front::ast::item_fn;
+ import front::ast::expr;
+ import front::ast::elt;
+ import front::ast::field;
+ import front::ast::decl;
+ import front::ast::decl_local;
+ import front::ast::decl_item;
+ import front::ast::initializer;
+ import front::ast::local;
+ import front::ast::arm;
+ import front::ast::expr_call;
+ import front::ast::expr_vec;
+ import front::ast::expr_tup;
+ import front::ast::expr_path;
+ import front::ast::expr_field;
+ import front::ast::expr_index;
+ import front::ast::expr_log;
+ import front::ast::expr_block;
+ import front::ast::expr_rec;
+ import front::ast::expr_if;
+ import front::ast::expr_binary;
+ import front::ast::expr_unary;
+ import front::ast::expr_assign;
+ import front::ast::expr_assign_op;
+ import front::ast::expr_while;
+ import front::ast::expr_do_while;
+ import front::ast::expr_alt;
+ import front::ast::expr_lit;
+ import front::ast::expr_ret;
+ import front::ast::expr_self_method;
+ import front::ast::expr_bind;
+ import front::ast::expr_spawn;
+ import front::ast::expr_ext;
+ import front::ast::expr_fail;
+ import front::ast::expr_break;
+ import front::ast::expr_cont;
+ import front::ast::expr_send;
+ import front::ast::expr_recv;
+ import front::ast::expr_put;
+ import front::ast::expr_port;
+ import front::ast::expr_chan;
+ import front::ast::expr_be;
+ import front::ast::expr_check;
+ import front::ast::expr_assert;
+ import front::ast::expr_cast;
+ import front::ast::expr_for;
+ import front::ast::expr_for_each;
+ import front::ast::stmt;
+ import front::ast::stmt_decl;
+ import front::ast::stmt_expr;
+ import front::ast::block;
+ import front::ast::block_;
+ import front::ast::method;
+
+ import middle::fold::span;
+ import middle::fold::respan;
+
+ import util::common::new_def_hash;
+ import util::common::decl_lhs;
+ import util::common::uistr;
+ import util::common::log_expr;
+ import util::common::log_fn;
+ import util::common::elt_exprs;
+ import util::common::field_exprs;
+ import util::common::has_nonlocal_exits;
+ import util::common::log_stmt;
+ import util::common::log_expr_err;
+
+ fn find_pre_post_mod(&_mod m) -> _mod {
+ log("implement find_pre_post_mod!");
+ fail;
+ }
+
+ fn find_pre_post_native_mod(&native_mod m) -> native_mod {
+ log("implement find_pre_post_native_mod");
+ fail;
+ }
+
+
+ fn find_pre_post_obj(&crate_ctxt ccx, _obj o) -> () {
+ fn do_a_method(crate_ctxt ccx, &@method m) -> () {
+ assert (ccx.fm.contains_key(m.node.id));
+ let fn_ctxt fcx = rec(enclosing=ccx.fm.get(m.node.id),
+ id=m.node.id, name=m.node.ident, ccx=ccx);
+ find_pre_post_fn(fcx, m.node.meth);
+ }
+ auto f = bind do_a_method(ccx,_);
+ _vec::map[@method, ()](f, o.methods);
+ option::map[@method, ()](f, o.dtor);
+ }
+
+ fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
+ alt (i.node) {
+ case (item_const(?id, ?t, ?e, ?di, ?a)) {
+ // make a fake fcx
+ auto fake_fcx = rec(enclosing=rec(vars=@new_def_hash[var_info](),
+ cf=return),
+ id=tup(0,0),
+ name="",
+ ccx=ccx);
+ find_pre_post_expr(fake_fcx, e);
+ }
+ case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
+ assert (ccx.fm.contains_key(di));
+ auto fcx = rec(enclosing=ccx.fm.get(di),
+ id=di, name=id, ccx=ccx);
+ find_pre_post_fn(fcx, f);
+ }
+ case (item_mod(?id, ?m, ?di)) {
+ find_pre_post_mod(m);
+ }
+ case (item_native_mod(?id, ?nm, ?di)) {
+ find_pre_post_native_mod(nm);
+ }
+ case (item_ty(_,_,_,_,_)) {
+ ret;
+ }
+ case (item_tag(_,_,_,_,_)) {
+ ret;
+ }
+ case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
+ find_pre_post_obj(ccx, o);
+ }
+ }
+ }
+
+ /* 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(&fn_ctxt fcx, &vec[@expr] args, ann a) {
+ auto enclosing = fcx.enclosing;
+ auto fm = fcx.ccx.fm;
+ auto nv = num_locals(enclosing);
+
+ fn do_one(fn_ctxt fcx, &@expr e) -> () {
+ find_pre_post_expr(fcx, e);
+ }
+ auto f = bind do_one(fcx, _);
+
+ _vec::map[@expr, ()](f, args);
+
+ fn get_pp(&@expr e) -> pre_and_post {
+ ret expr_pp(e);
+ }
+ auto g = get_pp;
+ auto pps = _vec::map[@expr, pre_and_post](g, args);
+ auto h = get_post;
+
+ set_pre_and_post(a,
+ rec(precondition=seq_preconds(enclosing, pps),
+ postcondition=union_postconds
+ (nv, (_vec::map[pre_and_post, postcond](h, pps)))));
+ }
+
+ fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
+ &block body, &ann a) -> () {
+ find_pre_post_expr(fcx, index);
+ find_pre_post_block(fcx, body);
+ auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
- (vec(expr_postcond(index), block_postcond(body)));
++ seq_preconds(fcx.enclosing, [expr_pp(index),
++ block_pp(body)]));
+ auto loop_postcond = intersect_postconds
- case (_) { find_pre_post_exprs(fcx, vec(lhs, rhs), larger_ann); }
++ ([expr_postcond(index), block_postcond(body)]);
+ set_pre_and_post(a, rec(precondition=loop_precond,
+ postcondition=loop_postcond));
+ }
+
+ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var) -> () {
+ alt (ann_to_def(fcx.ccx, new_var)) {
+ case (some[def](def_local(?d_id))) {
+ find_pre_post_expr(fcx, rhs);
+ set_pre_and_post(larger_ann, expr_pp(rhs));
+ gen(fcx, larger_ann, d_id);
+ }
- find_pre_post_exprs(fcx, vec(lhs, rhs), a);
++ case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
+ }
+ }
+
+ /* Fills in annotations as a side effect. Does not rebuild the expr */
+ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
+ auto enclosing = fcx.enclosing;
+ auto num_local_vars = num_locals(enclosing);
+
+ fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
+ find_pre_post_expr(fcx, e);
+ }
+ fn pp_one(&@expr e) -> pre_and_post {
+ ret expr_pp(e);
+ }
+
+ /*
+ log_err("find_pre_post_expr (num_locals =" +
+ uistr(num_local_vars) + "):");
+ log_expr_err(*e);
+ */
+
+ alt (e.node) {
+ case (expr_call(?operator, ?operands, ?a)) {
+ auto args = _vec::clone[@expr](operands);
+ _vec::push[@expr](args, operator);
+ find_pre_post_exprs(fcx, args, a);
+ }
+ case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+ auto args = _vec::clone[@expr](operands);
+ _vec::push[@expr](args, operator);
+ find_pre_post_exprs(fcx, args, a);
+ }
+ case (expr_vec(?args, _, ?a)) {
+ find_pre_post_exprs(fcx, args, a);
+ }
+ case (expr_tup(?elts, ?a)) {
+ find_pre_post_exprs(fcx, elt_exprs(elts), a);
+ }
+ case (expr_path(?p, ?a)) {
+ auto res = empty_pre_post(num_local_vars);
+
+ auto df = ann_to_def_strict(fcx.ccx, a);
+ alt (df) {
+ case (def_local(?d_id)) {
+ auto i = bit_num(d_id, enclosing);
+ require_and_preserve(i, res);
+ }
+ case (_) { /* nothing to check */ }
+ }
+
+ // Otherwise, variable is global, so it must be initialized
+ set_pre_and_post(a, res);
+ }
+ case (expr_self_method(?v, ?a)) {
+ /* v is a method of the enclosing obj, so it must be
+ initialized, right? */
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ case(expr_log(_, ?arg, ?a)) {
+ find_pre_post_expr(fcx, arg);
+ set_pre_and_post(a, expr_pp(arg));
+ }
+ case (expr_chan(?arg, ?a)) {
+ find_pre_post_expr(fcx, arg);
+ set_pre_and_post(a, expr_pp(arg));
+ }
+ case(expr_put(?opt, ?a)) {
+ alt (opt) {
+ case (some[@expr](?arg)) {
+ find_pre_post_expr(fcx, arg);
+ set_pre_and_post(a, expr_pp(arg));
+ }
+ case (none[@expr]) {
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ }
+ }
+ case (expr_block(?b, ?a)) {
+ find_pre_post_block(fcx, b);
+ set_pre_and_post(a, block_pp(b));
+ }
+ case (expr_rec(?fields,?maybe_base,?a)) {
+ auto es = field_exprs(fields);
+ _vec::plus_option[@expr](es, maybe_base);
+ find_pre_post_exprs(fcx, es, a);
+ }
+ case (expr_assign(?lhs, ?rhs, ?a)) {
+ alt (lhs.node) {
+ case (expr_path(?p, ?a_lhs)) {
+ gen_if_local(fcx, lhs, rhs, a, a_lhs);
+ }
+ case (_) {
- find_pre_post_exprs(fcx, vec(lhs, rhs), a);
++ find_pre_post_exprs(fcx, [lhs, rhs], a);
+ }
+ }
+ }
+ case (expr_recv(?lhs, ?rhs, ?a)) {
+ alt (lhs.node) {
+ case (expr_path(?p, ?a_lhs)) {
+ gen_if_local(fcx, lhs, rhs, a, a_lhs);
+ }
+ case (_) {
+ // doesn't check that lhs is an lval, but
+ // that's probably ok
- find_pre_post_exprs(fcx, vec(lhs, rhs), a);
++ find_pre_post_exprs(fcx, [lhs, rhs], a);
+ }
+ }
+ }
+ case (expr_assign_op(_, ?lhs, ?rhs, ?a)) {
+ /* Different from expr_assign in that the lhs *must*
+ already be initialized */
- vec(expr_pp(antec),
- block_pp(conseq)));
++ find_pre_post_exprs(fcx, [lhs, rhs], a);
+ }
+ case (expr_lit(_,?a)) {
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ case (expr_ret(?maybe_val, ?a)) {
+ alt (maybe_val) {
+ case (none[@expr]) {
+ set_pre_and_post(a,
+ rec(precondition=true_precond(num_local_vars),
+ postcondition=false_postcond(num_local_vars)));
+ }
+ case (some[@expr](?ret_val)) {
+ find_pre_post_expr(fcx, ret_val);
+ let pre_and_post pp =
+ rec(precondition=expr_precond(ret_val),
+ postcondition=false_postcond(num_local_vars));
+ set_pre_and_post(a, pp);
+ }
+ }
+ }
+ case (expr_be(?e, ?a)) {
+ find_pre_post_expr(fcx, e);
+ set_pre_and_post(a,
+ rec(precondition=expr_prestate(e),
+ postcondition=false_postcond(num_local_vars)));
+ }
+ case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
+ find_pre_post_expr(fcx, antec);
+ find_pre_post_block(fcx, conseq);
+ alt (maybe_alt) {
+ case (none[@expr]) {
+ auto precond_res = seq_preconds(enclosing,
- vec(expr_pp(antec), block_pp(conseq)));
++ [expr_pp(antec),
++ block_pp(conseq)]);
+ set_pre_and_post(a, rec(precondition=precond_res,
+ postcondition=
+ expr_poststate(antec)));
+ }
+ case (some[@expr](?altern)) {
+ find_pre_post_expr(fcx, altern);
+ auto precond_true_case =
+ seq_preconds(enclosing,
- vec(expr_postcond(antec), block_postcond(conseq)));
++ [expr_pp(antec), block_pp(conseq)]);
+ auto postcond_true_case = union_postconds
+ (num_local_vars,
- vec(expr_pp(antec), expr_pp(altern)));
++ [expr_postcond(antec), block_postcond(conseq)]);
+ auto precond_false_case = seq_preconds
+ (enclosing,
- vec(expr_postcond(antec), expr_postcond(altern)));
++ [expr_pp(antec), expr_pp(altern)]);
+ auto postcond_false_case = union_postconds
+ (num_local_vars,
- vec(precond_true_case, precond_false_case));
++ [expr_postcond(antec), expr_postcond(altern)]);
+ auto precond_res = union_postconds
+ (num_local_vars,
- (vec(postcond_true_case, postcond_false_case));
++ [precond_true_case, precond_false_case]);
+ auto postcond_res = intersect_postconds
- find_pre_post_exprs(fcx, vec(l, r), a);
++ ([postcond_true_case, postcond_false_case]);
+ set_pre_and_post(a, rec(precondition=precond_res,
+ postcondition=postcond_res));
+ }
+ }
+ }
+ case (expr_binary(?bop,?l,?r,?a)) {
+ /* *unless* bop is lazy (e.g. and, or)?
+ FIXME */
- find_pre_post_exprs(fcx, vec(l, r), a);
++ find_pre_post_exprs(fcx, [l, r], a);
+ }
+ case (expr_send(?l, ?r, ?a)) {
- vec(expr_pp(test),
- block_pp(body))),
++ find_pre_post_exprs(fcx, [l, r], a);
+ }
+ case (expr_unary(_,?operand,?a)) {
+ find_pre_post_expr(fcx, operand);
+ set_pre_and_post(a, expr_pp(operand));
+ }
+ case (expr_cast(?operand, _, ?a)) {
+ find_pre_post_expr(fcx, operand);
+ set_pre_and_post(a, expr_pp(operand));
+ }
+ case (expr_while(?test, ?body, ?a)) {
+ find_pre_post_expr(fcx, test);
+ find_pre_post_block(fcx, body);
+ set_pre_and_post(a,
+ rec(precondition=
+ seq_preconds(enclosing,
- intersect_postconds(vec(expr_postcond(test),
- block_postcond(body)))));
++ [expr_pp(test),
++ block_pp(body)]),
+ postcondition=
- vec(block_postcond(body), expr_postcond(test)));
++ intersect_postconds([expr_postcond(test),
++ block_postcond(body)])));
+ }
+ case (expr_do_while(?body, ?test, ?a)) {
+ find_pre_post_block(fcx, body);
+ find_pre_post_expr(fcx, test);
+
+ auto loop_postcond = union_postconds(num_local_vars,
- vec(block_pp(body),
- expr_pp(test))),
++ [block_postcond(body), expr_postcond(test)]);
+ /* conservative approximination: if the body
+ could break or cont, the test may never be executed */
+ if (has_nonlocal_exits(body)) {
+ loop_postcond = empty_poststate(num_local_vars);
+ }
+
+ set_pre_and_post(a,
+ rec(precondition=seq_preconds(enclosing,
- find_pre_post_exprs(fcx, vec(e, sub), a);
++ [block_pp(body),
++ expr_pp(test)]),
+ postcondition=loop_postcond));
+ }
+ case (expr_for(?d, ?index, ?body, ?a)) {
+ find_pre_post_loop(fcx, d, index, body, a);
+ }
+ case (expr_for_each(?d, ?index, ?body, ?a)) {
+ find_pre_post_loop(fcx, d, index, body, a);
+ }
+ case (expr_index(?e, ?sub, ?a)) {
- vec(antec, next)));
++ find_pre_post_exprs(fcx, [e, sub], a);
+ }
+ case (expr_alt(?e, ?alts, ?a)) {
+ find_pre_post_expr(fcx, e);
+ fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
+ find_pre_post_block(fcx, an_alt.block);
+ ret block_pp(an_alt.block);
+ }
+ auto f = bind do_an_alt(fcx, _);
+ auto alt_pps = _vec::map[arm, pre_and_post](f, alts);
+ fn combine_pp(pre_and_post antec,
+ fn_info enclosing, &pre_and_post pp,
+ &pre_and_post next) -> pre_and_post {
+ union(pp.precondition, seq_preconds(enclosing,
- let vec[pre_and_post] pps = vec();
++ [antec, next]));
+ intersect(pp.postcondition, next.postcondition);
+ ret pp;
+ }
+ auto antec_pp = pp_clone(expr_pp(e));
+ auto e_pp = rec(precondition=empty_prestate(num_local_vars),
+ postcondition=false_postcond(num_local_vars));
+ auto g = bind combine_pp(antec_pp, fcx.enclosing, _, _);
+
+ auto alts_overall_pp = _vec::foldl[pre_and_post, pre_and_post]
+ (g, e_pp, alt_pps);
+
+ set_pre_and_post(a, alts_overall_pp);
+ }
+ case (expr_field(?operator, _, ?a)) {
+ find_pre_post_expr(fcx, operator);
+ set_pre_and_post(a, expr_pp(operator));
+ }
+ case (expr_fail(?a)) {
+ set_pre_and_post(a,
+ /* if execution continues after fail,
+ then everything is true! */
+ rec(precondition=empty_prestate(num_local_vars),
+ postcondition=false_postcond(num_local_vars)));
+ }
+ case (expr_assert(?p, ?a)) {
+ find_pre_post_expr(fcx, p);
+ set_pre_and_post(a, expr_pp(p));
+ }
+ case (expr_check(?p, ?a)) {
+ /* will need to change when we support arbitrary predicates... */
+ find_pre_post_expr(fcx, p);
+ set_pre_and_post(a, expr_pp(p));
+ }
+ case(expr_bind(?operator, ?maybe_args, ?a)) {
+ auto args = _vec::cat_options[@expr](maybe_args);
+ _vec::push[@expr](args, operator); /* ??? order of eval? */
+ find_pre_post_exprs(fcx, args, a);
+ }
+ case (expr_break(?a)) {
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ case (expr_cont(?a)) {
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ case (expr_port(?a)) {
+ set_pre_and_post(a, empty_pre_post(num_local_vars));
+ }
+ case (expr_ext(_, _, _, ?expanded, ?a)) {
+ find_pre_post_expr(fcx, expanded);
+ set_pre_and_post(a, expr_pp(expanded));
+ }
+ }
+ }
+
+
+ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
+ -> () {
+ log("stmt =");
+ log_stmt(s);
+
+ auto enclosing = fcx.enclosing;
+ auto num_local_vars = num_locals(enclosing);
+ alt(s.node) {
+ case(stmt_decl(?adecl, ?a)) {
+ alt(adecl.node) {
+ case(decl_local(?alocal)) {
+ alt(alocal.init) {
+ case(some[initializer](?an_init)) {
+ find_pre_post_expr(fcx, an_init.expr);
+ auto rhs_pp = expr_pp(an_init.expr);
+ set_pre_and_post(alocal.ann, rhs_pp);
+
+ /* Inherit ann from initializer, and add var being
+ initialized to the postcondition */
+ set_pre_and_post(a, rhs_pp);
+ /* log("gen (decl):");
+ log_stmt(s); */
+ gen(fcx, a, alocal.id);
+ /* log_err("for stmt");
+ log_stmt(s);
+ log_err("pp = ");
+ log_pp(stmt_pp(s)); */
+ }
+ case(none[initializer]) {
+ auto pp = empty_pre_post(num_local_vars);
+ set_pre_and_post(alocal.ann, pp);
+ set_pre_and_post(a, pp);
+ }
+ }
+ }
+ case(decl_item(?anitem)) {
+ auto pp = empty_pre_post(num_local_vars);
+ set_pre_and_post(a, pp);
+ find_pre_post_item(fcx.ccx, *anitem);
+ }
+ }
+ }
+ case(stmt_expr(?e,?a)) {
+ find_pre_post_expr(fcx, e);
+ set_pre_and_post(a, expr_pp(e));
+ }
+ }
+ }
+
+ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
+ /* 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.
+ */
+ auto nv = num_locals(fcx.enclosing);
+
+ fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
+ find_pre_post_stmt(fcx, *s);
+ log("pre_post for stmt:");
+ log_stmt(*s);
+ log("is:");
+ log_pp(stmt_pp(*s));
+ }
+ auto do_one = bind do_one_(fcx, _);
+
+ _vec::map[@stmt, ()](do_one, b.node.stmts);
+ fn do_inner_(fn_ctxt fcx, &@expr e) -> () {
+ find_pre_post_expr(fcx, e);
+ }
+ auto do_inner = bind do_inner_(fcx, _);
+ option::map[@expr, ()](do_inner, b.node.expr);
+
++ let vec[pre_and_post] pps = [];
+
+ fn get_pp_stmt(&@stmt s) -> pre_and_post {
+ ret stmt_pp(*s);
+ }
+ auto f = get_pp_stmt;
+ pps += _vec::map[@stmt, pre_and_post](f, b.node.stmts);
+ fn get_pp_expr(&@expr e) -> pre_and_post {
+ ret expr_pp(e);
+ }
+ auto g = get_pp_expr;
+ plus_option[pre_and_post](pps,
+ option::map[@expr, pre_and_post](g, b.node.expr));
+
+ auto block_precond = seq_preconds(fcx.enclosing, pps);
+ auto h = get_post;
+ auto postconds = _vec::map[pre_and_post, postcond](h, pps);
+ /* A block may be empty, so this next line ensures that the postconds
+ vector is non-empty. */
+ _vec::push[postcond](postconds, block_precond);
+ auto block_postcond = empty_poststate(nv);
+ /* conservative approximation */
+ if (! has_nonlocal_exits(b)) {
+ block_postcond = union_postconds(nv, postconds);
+ }
+
+ set_pre_and_post(b.node.a, rec(precondition=block_precond,
+ postcondition=block_postcond));
+ }
+
+ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
+ find_pre_post_block(fcx, f.body);
+ }
+
+ fn check_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
+ &vec[ty_param] ty_params,
+ &def_id id, &ann a) -> @item {
+ log("check_item_fn:");
+ log_fn(f, i, ty_params);
+
+ assert (ccx.fm.contains_key(id));
+ auto fcx = rec(enclosing=ccx.fm.get(id),
+ id=id, name=i, ccx=ccx);
+ find_pre_post_fn(fcx, f);
+
+ ret @respan(sp, item_fn(i, f, ty_params, id, a));
+ }
+
+ //
+ // 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:
+ //
+
--- /dev/null
- auto res_p = intersect_postconds(vec(expr_poststate(index),
- block_poststate(body)));
+ import std::bitv;
+ import std::_vec;
+ import std::_vec::plus_option;
+ import std::_vec::cat_options;
+ 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::pp_clone;
+ 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::var_info;
+ import aux::crate_ctxt;
+ import aux::fn_ctxt;
+ import aux::num_locals;
+ import aux::expr_pp;
+ import aux::stmt_pp;
+ import aux::block_pp;
+ import aux::set_pre_and_post;
+ import aux::expr_prestate;
+ import aux::stmt_poststate;
+ import aux::expr_poststate;
+ import aux::block_poststate;
+ import aux::fn_info;
+ import aux::log_pp;
+ 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;
+ import aux::stmt_to_ann;
+ import aux::log_states;
+ import aux::block_states;
+ import aux::controlflow_expr;
+ import aux::ann_to_def;
+
+ import bitvectors::seq_preconds;
+ import bitvectors::union_postconds;
+ import bitvectors::intersect_postconds;
+ import bitvectors::declare_var;
+ import bitvectors::bit_num;
+ import bitvectors::gen_poststate;
+
+ import front::ast::_mod;
+ import front::ast;
+ import front::ast::_fn;
+ import front::ast::method;
+ import front::ast::ann;
+ import front::ast::ty;
+ import front::ast::mutability;
+ import front::ast::item;
+ import front::ast::obj_field;
+ import front::ast::stmt;
+ import front::ast::stmt_;
+ import front::ast::stmt_decl;
+ import front::ast::ident;
+ import front::ast::def_id;
+ import front::ast::ann;
+ import front::ast::expr;
+ import front::ast::path;
+ import front::ast::crate_directive;
+ import front::ast::fn_decl;
+ import front::ast::_obj;
+ import front::ast::native_mod;
+ import front::ast::variant;
+ import front::ast::ty_param;
+ import front::ast::ty;
+ import front::ast::proto;
+ import front::ast::pat;
+ import front::ast::binop;
+ import front::ast::unop;
+ import front::ast::def;
+ import front::ast::lit;
+ import front::ast::init_op;
+ import front::ast::controlflow;
+ import front::ast::return;
+ import front::ast::noreturn;
+ import front::ast::ann_none;
+ import front::ast::ann_type;
+ import front::ast::_obj;
+ import front::ast::_mod;
+ import front::ast::crate;
+ import front::ast::item_fn;
+ import front::ast::item_mod;
+ import front::ast::item_ty;
+ import front::ast::item_tag;
+ import front::ast::item_native_mod;
+ import front::ast::item_obj;
+ import front::ast::item_const;
+ import front::ast::def_local;
+ import front::ast::def_fn;
+ import front::ast::ident;
+ import front::ast::def_id;
+ import front::ast::ann;
+ import front::ast::item;
+ import front::ast::item_fn;
+ import front::ast::expr;
+ import front::ast::elt;
+ import front::ast::field;
+ import front::ast::decl;
+ import front::ast::decl_local;
+ import front::ast::decl_item;
+ import front::ast::initializer;
+ import front::ast::local;
+ import front::ast::arm;
+ import front::ast::expr_call;
+ import front::ast::expr_vec;
+ import front::ast::expr_tup;
+ import front::ast::expr_path;
+ import front::ast::expr_field;
+ import front::ast::expr_index;
+ import front::ast::expr_log;
+ import front::ast::expr_block;
+ import front::ast::expr_rec;
+ import front::ast::expr_if;
+ import front::ast::expr_binary;
+ import front::ast::expr_unary;
+ import front::ast::expr_assign;
+ import front::ast::expr_assign_op;
+ import front::ast::expr_while;
+ import front::ast::expr_do_while;
+ import front::ast::expr_alt;
+ import front::ast::expr_lit;
+ import front::ast::expr_ret;
+ import front::ast::expr_self_method;
+ import front::ast::expr_bind;
+ import front::ast::expr_spawn;
+ import front::ast::expr_ext;
+ import front::ast::expr_fail;
+ import front::ast::expr_break;
+ import front::ast::expr_cont;
+ import front::ast::expr_send;
+ import front::ast::expr_recv;
+ import front::ast::expr_put;
+ import front::ast::expr_port;
+ import front::ast::expr_chan;
+ import front::ast::expr_be;
+ import front::ast::expr_check;
+ import front::ast::expr_assert;
+ import front::ast::expr_cast;
+ import front::ast::expr_for;
+ import front::ast::expr_for_each;
+ import front::ast::stmt;
+ import front::ast::stmt_decl;
+ import front::ast::stmt_expr;
+ import front::ast::block;
+ import front::ast::block_;
+ import front::ast::method;
+
+ import middle::fold::span;
+ import middle::fold::respan;
+
+ import util::common::new_def_hash;
+ import util::common::decl_lhs;
+ import util::common::uistr;
+ import util::common::log_expr;
+ import util::common::log_block;
+ 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;
+ import util::common::log_expr_err;
+
+ fn find_pre_post_state_mod(&_mod m) -> bool {
+ log("implement find_pre_post_state_mod!");
+ fail;
+ }
+
+ fn find_pre_post_state_native_mod(&native_mod m) -> bool {
+ log("implement find_pre_post_state_native_mod!");
+ fail;
+ }
+
+ 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(e);
+ }
+
+ ret tup(changed, post);
+ }
+
+ fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres,
+ &ann a, &vec[@expr] es) -> bool {
+ auto res = seq_states(fcx, pres, es);
+ auto changed = res._0;
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, res._1) || changed;
+ ret changed;
+ }
+
+ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
+ &@expr index, &block body, &ann a) -> bool {
+ auto changed = false;
+
+ /* same issues as while */
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, index) || changed;
+ /* in general, would need the intersection of
+ (poststate of index, poststate of body) */
+ changed = find_pre_post_state_block(fcx, expr_poststate(index), body)
+ || changed;
- (vec(block_poststate(conseq), expr_poststate(altern)));
++ auto res_p = intersect_postconds([expr_poststate(index),
++ block_poststate(body)]);
+
+ changed = extend_poststate_ann(a, res_p) || changed;
+ ret changed;
+ }
+
+ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
+ alt (ann_to_def(fcx.ccx, a_new_var)) {
+ case (some[def](def_local(?d))) { ret gen_poststate(fcx, a, d); }
+ case (_) { ret false; }
+ }
+ }
+
+ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
+ auto changed = false;
+ auto num_local_vars = num_locals(fcx.enclosing);
+
+ /*
+ log_err("states:");
+ log_expr_err(*e);
+ log_err(ast.ann_tag(middle.ty.expr_ann(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);
+ }
+ 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 */
+ changed = find_pre_post_state_expr(fcx, pres, operator)
+ || changed;
+ /* rands go left-to-right */
+ changed = find_pre_post_state_exprs(fcx,
+ expr_poststate(operator), a, operands)
+ || changed;
+ /* if this is a failing call, it sets the return value */
+ alt (controlflow_expr(fcx.ccx, operator)) {
+ case (noreturn) {
+ /*
+ log_err("Call that might fail! to");
+ log_expr_err(*operator);
+ */
+ changed = gen_poststate(fcx, a, fcx.id) || changed;
+ }
+ case (_) {
+ /* log_err("non-failing call, to:");
+ log_expr_err(*operator);
+ */
+ }
+ }
+ ret changed;
+ }
+ case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, operator);
+ ret(find_pre_post_state_exprs(fcx,
+ expr_poststate(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(operator), a, cat_options[@expr](maybe_args))
+ || changed);
+ }
+ case (expr_path(_,?a)) {
+ ret pure_exp(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(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+ ret changed;
+ }
+ case (expr_chan(?e, ?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, e);
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+ ret changed;
+ }
+ case (expr_ext(_, _, _, ?expanded, ?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, expanded);
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(expanded))
+ || changed;
+ ret changed;
+ }
+ case (expr_put(?maybe_e, ?a)) {
+ alt (maybe_e) {
+ case (some[@expr](?arg)) {
+ changed = find_pre_post_state_expr(fcx, pres, arg);
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(arg))
+ || changed;
+ ret changed;
+ }
+ case (none[@expr]) {
+ ret pure_exp(a, pres);
+ }
+ }
+ }
+ case (expr_lit(?l,?a)) {
+ ret pure_exp(a, pres);
+ }
+ case (expr_block(?b,?a)) {
+ changed = find_pre_post_state_block(fcx, pres, b)
+ || changed;
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, block_poststate(b)) || changed;
+ ret changed;
+ }
+ case (expr_rec(?fields,?maybe_base,?a)) {
+ changed = find_pre_post_state_exprs(fcx, pres, a,
+ field_exprs(fields)) || changed;
+ alt (maybe_base) {
+ case (none[@expr]) { /* do nothing */ }
+ case (some[@expr](?base)) {
+ changed = find_pre_post_state_expr(fcx, pres, base)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(base))
+ || changed;
+ }
+ }
+ ret changed;
+ }
+ case (expr_assign(?lhs, ?rhs, ?a)) {
+ extend_prestate_ann(a, pres);
+
+ alt (lhs.node) {
+ case (expr_path(?p, ?a_lhs)) {
+ // assignment to local var
+ changed = pure_exp(a_lhs, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, rhs)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(rhs))
+ || changed;
+ changed = gen_if_local(fcx, a_lhs, a)|| 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(lhs), rhs) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(rhs))
+ || changed;
+ }
+ }
+ ret changed;
+ }
+ case (expr_recv(?lhs, ?rhs, ?a)) {
+ extend_prestate_ann(a, pres);
+
+ alt (lhs.node) {
+ case (expr_path(?p, ?a_lhs)) {
+ // receive to local var
+ changed = pure_exp(a_lhs, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, rhs)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(rhs))
+ || changed;
+ changed = gen_if_local(fcx, a_lhs, a) || changed;
+ }
+ case (_) {
+ // receive 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(lhs), rhs) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(rhs))
+ || changed;
+ }
+ }
+ ret changed;
+ }
+
+ case (expr_ret(?maybe_ret_val, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ set_poststate_ann(a, false_postcond(num_local_vars));
+ alt(maybe_ret_val) {
+ case (none[@expr]) { /* do nothing */ }
+ case (some[@expr](?ret_val)) {
+ changed = find_pre_post_state_expr(fcx,
+ pres, ret_val) || changed;
+ }
+ }
+ ret changed;
+ }
+ case (expr_be(?e, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ set_poststate_ann(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)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, antec)
+ || changed;
+ changed = find_pre_post_state_block(fcx,
+ expr_poststate(antec), conseq) || changed;
+ alt (maybe_alt) {
+ case (none[@expr]) {
+ changed = extend_poststate_ann(a, expr_poststate(antec))
+ || changed;
+ }
+ case (some[@expr](?altern)) {
+ changed = find_pre_post_state_expr(fcx,
+ expr_poststate(antec), altern) || changed;
+ auto poststate_res = intersect_postconds
- intersect_postconds(vec(expr_poststate(test),
- block_poststate(body)))) || changed;
++ ([block_poststate(conseq), expr_poststate(altern)]);
+ changed = extend_poststate_ann(a, poststate_res) || changed;
+ }
+ }
+ log("if:");
+ log_expr(*e);
+ log("new prestate:");
+ log_bitv(fcx.enclosing, pres);
+ log("new poststate:");
+ log_bitv(fcx.enclosing, expr_poststate(e));
+
+ ret changed;
+ }
+ case (expr_binary(?bop, ?l, ?r, ?a)) {
+ /* FIXME: what if bop is lazy? */
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, l)
+ || changed;
+ changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+ ret changed;
+ }
+ case (expr_send(?l, ?r, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, l)
+ || changed;
+ changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+ ret changed;
+ }
+ case (expr_assign_op(?op, ?lhs, ?rhs, ?a)) {
+ /* quite similar to binary -- should abstract this */
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, lhs)
+ || changed;
+ changed = find_pre_post_state_expr(fcx, expr_poststate(lhs), rhs)
+ || changed;
+ changed = extend_poststate_ann(a, expr_poststate(rhs)) || changed;
+ ret changed;
+ }
+ case (expr_while(?test, ?body, ?a)) {
+ changed = extend_prestate_ann(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?
+ */
+ changed = find_pre_post_state_expr(fcx, pres, test)
+ || changed;
+ changed = find_pre_post_state_block(fcx, expr_poststate(test), body)
+ || changed;
+ changed = extend_poststate_ann(a,
++ intersect_postconds([expr_poststate(test),
++ block_poststate(body)])) || changed;
+ ret changed;
+ }
+ case (expr_do_while(?body, ?test, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_block(fcx, pres, body)
+ || changed;
+ changed = find_pre_post_state_expr(fcx,
+ block_poststate(body), test) || 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) */
+ if (has_nonlocal_exits(body)) {
+ changed = set_poststate_ann(a, pres) || changed;
+ }
+ else {
+ changed = extend_poststate_ann(a, expr_poststate(test))
+ || changed;
+ }
+
+ 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(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+ changed = find_pre_post_state_expr(fcx,
+ expr_poststate(e), sub) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(sub));
+ ret changed;
+ }
+ case (expr_alt(?e, ?alts, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+ auto e_post = expr_poststate(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;
+ changed = intersect(a_post, block_poststate(an_alt.block))
+ || changed;
+ }
+ }
+ else {
+ // No alts; poststate is the poststate of the test
+ a_post = e_post;
+ }
+ changed = extend_poststate_ann(a, a_post);
+ ret changed;
+ }
+ case (expr_field(?e, _, ?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, e);
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+ ret changed;
+ }
+ case (expr_unary(_,?operand,?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, operand)
+ || changed;
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(operand))
+ || changed;
+ ret changed;
+ }
+ case (expr_cast(?operand, _, ?a)) {
+ changed = find_pre_post_state_expr(fcx, pres, operand)
+ || changed;
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(operand))
+ || changed;
+ ret changed;
+ }
+ case (expr_fail(?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ /* if execution continues after fail, then everything is true! woo! */
+ changed = set_poststate_ann(a, false_postcond(num_local_vars))
+ || changed;
+ ret changed;
+ }
+ case (expr_assert(?p, ?a)) {
+ ret pure_exp(a, pres);
+ }
+ case (expr_check(?p, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fcx, pres, p) || changed;
+ /* FIXME: update the postcondition to reflect that p holds */
+ changed = extend_poststate_ann(a, pres) || changed;
+ ret changed;
+ }
+ case (expr_break(?a)) {
+ ret pure_exp(a, pres);
+ }
+ case (expr_cont(?a)) {
+ ret pure_exp(a, pres);
+ }
+ case (expr_port(?a)) {
+ ret pure_exp(a, pres);
+ }
+ case (expr_self_method(_, ?a)) {
+ ret pure_exp(a, pres);
+ }
+ }
+ }
+
+ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
+ auto changed = false;
+ auto stmt_ann_ = stmt_to_ann(*s);
+ assert (!is_none[@ts_ann](stmt_ann_));
+ auto stmt_ann = *(get[@ts_ann](stmt_ann_));
+ log("*At beginning: stmt = ");
+ log_stmt(*s);
+ log("*prestate = ");
+ log(bitv::to_str(stmt_ann.states.prestate));
+ log("*poststate =");
+ log(bitv::to_str(stmt_ann.states.poststate));
+ log("*changed =");
+ log(changed);
+
+ alt (s.node) {
+ case (stmt_decl(?adecl, ?a)) {
+ alt (adecl.node) {
+ case (decl_local(?alocal)) {
+ alt (alocal.init) {
+ case (some[initializer](?an_init)) {
+ changed = extend_prestate(stmt_ann.states.prestate, pres)
+ || changed;
+ changed = find_pre_post_state_expr
+ (fcx, pres, an_init.expr) || changed;
+ changed = extend_poststate(stmt_ann.states.poststate,
+ expr_poststate(an_init.expr))
+ || changed;
+ changed = gen_poststate(fcx, a, alocal.id)
+ || changed;
+ log("Summary: stmt = ");
+ log_stmt(*s);
+ log("prestate = ");
+ log(bitv::to_str(stmt_ann.states.prestate));
+ log_bitv(fcx.enclosing, stmt_ann.states.prestate);
+ log("poststate =");
+ log_bitv(fcx.enclosing, stmt_ann.states.poststate);
+ log("changed =");
+ log(changed);
+
+ ret changed;
+ }
+ case (none[initializer]) {
+ changed = extend_prestate(stmt_ann.states.prestate, pres)
+ || changed;
+ changed = extend_poststate(stmt_ann.states.poststate, pres)
+ || changed;
+ ret changed;
+ }
+ }
+ }
+ case (decl_item(?an_item)) {
+ changed = extend_prestate(stmt_ann.states.prestate, pres)
+ || changed;
+ changed = extend_poststate(stmt_ann.states.poststate, pres)
+ || changed;
+ ret (find_pre_post_state_item(fcx, an_item) || changed);
+ }
+ }
+ }
+ case (stmt_expr(?e, _)) {
+ changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+ changed = extend_prestate(stmt_ann.states.prestate, expr_prestate(e))
+ || changed;
+ changed = extend_poststate(stmt_ann.states.poststate,
+ expr_poststate(e)) || changed;
+ /*
+ log("Summary: stmt = ");
+ 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);
+ */
+ ret changed;
+ }
+ case (_) { ret false; }
+ }
+ }
+
+ /* 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(&fn_ctxt fcx, &prestate pres0, &block b)
+ -> bool {
+
+ auto changed = false;
+ auto num_local_vars = num_locals(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(*s, num_local_vars);
+ }
+
+ auto post = pres;
+
+ alt (b.node.expr) {
+ case (none[@expr]) {}
+ case (some[@expr](?e)) {
+ changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+ post = expr_poststate(e);
+ }
+ }
+
+ /*
+ log_err("block:");
+ log_block_err(b);
+ log_err("has non-local exits?");
+ log_err(has_nonlocal_exits(b));
+ */
+
+ /* conservative approximation: if a block contains a break
+ or cont, we assume nothing about the poststate */
+ if (has_nonlocal_exits(b)) {
+ post = pres0;
+ }
+
+ set_prestate_ann(b.node.a, pres0);
+ set_poststate_ann(b.node.a, post);
+
+ log("For block:");
+ log_block(b);
+ log("poststate = ");
+ log_states(block_states(b));
+ log("pres0:");
+ log_bitv(fcx.enclosing, pres0);
+ log("post:");
+ log_bitv(fcx.enclosing, post);
+
+ ret changed;
+ }
+
+ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
+ /* FIXME: where do we set args as being initialized?
+ What about for methods? */
+ auto num_local_vars = num_locals(fcx.enclosing);
+ ret find_pre_post_state_block(fcx,
+ empty_prestate(num_local_vars), f.body);
+ }
+
+ fn find_pre_post_state_obj(crate_ctxt ccx, _obj o) -> bool {
+ fn do_a_method(crate_ctxt ccx, &@method m) -> bool {
+ assert (ccx.fm.contains_key(m.node.id));
+ ret find_pre_post_state_fn(rec(enclosing=ccx.fm.get(m.node.id),
+ id=m.node.id,
+ name=m.node.ident,
+ ccx=ccx),
+ m.node.meth);
+ }
+ auto f = bind do_a_method(ccx,_);
+ auto flags = _vec::map[@method, bool](f, o.methods);
+ auto changed = _vec::or(flags);
+ changed = changed || maybe[@method, bool](false, f, o.dtor);
+ ret changed;
+ }
+
+ fn find_pre_post_state_item(&fn_ctxt fcx, @item i) -> bool {
+ alt (i.node) {
+ case (item_const(?id, ?t, ?e, ?di, ?a)) {
+ ret find_pre_post_state_expr(fcx,
+ empty_prestate(num_locals(fcx.enclosing)), e);
+ }
+ case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
+ assert (fcx.ccx.fm.contains_key(di));
+ ret find_pre_post_state_fn(rec(enclosing=fcx.ccx.fm.get(di),
+ id=di, name=id with fcx), f);
+ }
+ case (item_mod(?id, ?m, ?di)) {
+ ret find_pre_post_state_mod(m);
+ }
+ case (item_native_mod(?id, ?nm, ?di)) {
+ ret find_pre_post_state_native_mod(nm);
+ }
+ case (item_ty(_,_,_,_,_)) {
+ ret false;
+ }
+ case (item_tag(_,_,_,_,_)) {
+ ret false;
+ }
+ case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
+ ret find_pre_post_state_obj(fcx.ccx, o);
+ }
+ }
+ }
}
case (ty_bound_param(?id)) {
- s += "''" + _str::unsafe_from_bytes(vec(('a' as u8) +
- (id as u8)));
+ s += "''" + _str::unsafe_from_bytes([('a' as u8) +
+ (id as u8)]);
}
+
+ case (_) {
+ s += ty_to_short_str(cx, typ);
+ }
+
}
ret s;
}
// Get the types of the arguments of the variant.
- let vec[ty::t] tparams = vec();
+
++ let vec[ty::t] tparams = [];
+ auto j = 0u;
+ auto actual_ty_params =
+ ty::ann_to_type_params(fcx.ccx.node_types, ann);
+
+ for (ty::t some_ty in tag_tps) {
+ let ty::t t1 = some_ty;
+ let ty::t t2 = actual_ty_params.(j);
+
+ let ty::t res = Demand::simple(fcx,
+ pat.span,
+ t1, t2);
+
+ _vec::push(tparams, res);
+ j += 1u;
+ }
+
auto arg_tys;
alt (fcx.ccx.tcx.def_map.get(ast::ann_tag(ann))) {
case (ast::def_variant(_, ?vdefid)) {
projects / rust.git / commitdiff