From e42df38646c0a562630c6dcdb0de97698c191bb2 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 20 Apr 2011 12:11:01 -0700 Subject: [PATCH 01/11] Further work on typestate_check Lots of work on typestate_check, seems to get a lot of the way through checking the standard library. * Added for, for_each, assign_op, bind, cast, put, check, break, and cont. (I'm not sure break and cont are actually handled correctly.) * Fixed side-effect bug in seq_preconds so that unioning the preconditions of a sequence of statements or expressions is handled correctly. * Pass poststate correctly through a stmt_decl. * Handle expr_ret and expr_fail properly (after execution of a ret or fail, everything is true -- this is needed to handle ifs and alts where one branch is a ret or fail) * Fixed bug in set_prestate_ann where a thing that needed to be mutated wasn't getting passed as an alias * Fixed bug in how expr_alt was treated (zero is not the identity for intersect, who knew, right?) * Update logging to reflect log_err vs. log * Fixed find_locals so as to return all local decls and exclude function arguments. * Make union_postconds work on an empty vector (needed to handle empty blocks correctly) * Added _vec.cat_options, which takes a list of option[T] to a list of T, ignoring any Nones * Added two test cases. --- src/comp/middle/typestate_check.rs | 462 ++++++++++++++++++++------- src/comp/util/common.rs | 74 ++++- src/comp/util/typestate_ann.rs | 21 +- src/lib/_vec.rs | 15 + src/test/run-pass/use-uninit-alt.rs | 21 ++ src/test/run-pass/use-uninit-alt2.rs | 21 ++ 6 files changed, 483 insertions(+), 131 deletions(-) create mode 100644 src/test/run-pass/use-uninit-alt.rs create mode 100644 src/test/run-pass/use-uninit-alt2.rs diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 8a6e840a4284e..04aeebdf37ca4 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -101,14 +101,19 @@ import util.common.uistr; import util.common.elt_exprs; import util.common.field_exprs; import util.common.log_expr; +import util.common.log_expr_err; import util.common.log_stmt; import util.common.log_block; +import util.common.log_stmt_err; +import util.common.log_block_err; +import util.common.decl_lhs; import util.typestate_ann; import util.typestate_ann.ts_ann; import util.typestate_ann.empty_pre_post; import util.typestate_ann.empty_poststate; import util.typestate_ann.true_precond; import util.typestate_ann.true_postcond; +import util.typestate_ann.false_postcond; import util.typestate_ann.postcond; import util.typestate_ann.precond; import util.typestate_ann.poststate; @@ -131,8 +136,10 @@ import util.typestate_ann.empty_prestate; import util.typestate_ann.empty_ann; import util.typestate_ann.extend_prestate; import util.typestate_ann.extend_poststate; +import util.typestate_ann.relax_prestate; import util.typestate_ann.intersect; import util.typestate_ann.pp_clone; +import util.typestate_ann.clone; import middle.ty; import middle.ty.ann_to_type; @@ -156,6 +163,7 @@ import std._vec.push; import std._vec.slice; import std._vec.unzip; import std._vec.plus_option; +import std._vec.cat_options; import std.option; import std.option.t; import std.option.some; @@ -184,7 +192,7 @@ import util.typestate_ann.require_and_preserve; /**** debugging junk ****/ -fn log_bitv(fn_info enclosing, bitv.t v) { +fn bitv_to_str(fn_info enclosing, bitv.t v) -> str { auto s = ""; for each (@tup(def_id, tup(uint, ident)) p in enclosing.items()) { @@ -192,8 +200,15 @@ fn log_bitv(fn_info enclosing, bitv.t v) { s += " " + p._1._1 + " "; } } + ret s; +} + +fn log_bitv(fn_info enclosing, bitv.t v) { + log(bitv_to_str(enclosing, v)); +} - log(s); +fn log_bitv_err(fn_info enclosing, bitv.t v) { + log_err(bitv_to_str(enclosing, v)); } fn log_cond(vec[uint] v) -> () { @@ -217,6 +232,15 @@ fn log_pp(&pre_and_post pp) -> () { log_cond(p2); } +fn log_states(&pre_and_post_state pp) -> () { + auto p1 = bitv.to_vec(pp.prestate); + auto p2 = bitv.to_vec(pp.poststate); + log("prestate:"); + log_cond(p1); + log("poststate:"); + log_cond(p2); +} + fn print_ident(&ident i) -> () { log(" " + i + " "); } @@ -256,18 +280,19 @@ fn num_locals(fn_info m) -> uint { ret m.size(); } -fn find_locals(_fn f) -> vec[tup(ident,def_id)] { - auto res = _vec.alloc[tup(ident,def_id)](0u); +fn collect_local(&@vec[tup(ident, def_id)] vars, &span sp, @ast.local loc) + -> @decl { + log("collect_local: pushing " + loc.ident); + _vec.push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id)); + ret @respan(sp, decl_local(loc)); +} - for each (@tup(ident, block_index_entry) p - in f.body.node.index.items()) { - alt (p._1) { - case (ast.bie_local(?loc)) { - res += vec(tup(loc.ident,loc.id)); - } - case (_) { } - } - } +fn find_locals(_fn f) -> @vec[tup(ident,def_id)] { + auto res = @_vec.alloc[tup(ident,def_id)](0u); + + auto fld = fold.new_identity_fold[@vec[tup(ident, def_id)]](); + fld = @rec(fold_decl_local = bind collect_local(_,_,_) with *fld); + auto ignore = fold.fold_fn[@vec[tup(ident, def_id)]](res, fld, f); ret res; } @@ -285,12 +310,12 @@ fn mk_fn_info(_fn f) -> fn_info { let uint next = 0u; let vec[ast.arg] f_args = f.decl.inputs; - for (ast.arg v in f_args) { - next = add_var(v.id, v.ident, next, res); - } + /* ignore args, which we know are initialized; + just collect locally declared vars */ - let vec[tup(ident,def_id)] locals = find_locals(f); - for (tup(ident,def_id) p in locals) { + let @vec[tup(ident,def_id)] locals = find_locals(f); + log(uistr(_vec.len[tup(ident, def_id)](*locals)) + " locals"); + for (tup(ident,def_id) p in *locals) { next = add_var(p._1, p._0, next, res); } @@ -435,6 +460,12 @@ fn expr_ann(&expr e) -> ann { case (ast.expr_chan(_,?a)) { ret a; } + case (expr_break(?a)) { + ret a; + } + case (expr_cont(?a)) { + ret a; + } } } @@ -679,8 +710,9 @@ fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond { let precond rest = seq_preconds(num_vars, slice[pre_and_post](pps, 1u, sz)); difference(rest, first.postcondition); - union(first.precondition, rest); - ret first.precondition; + auto res = clone(first.precondition); + union(res, rest); + ret res; } else { ret true_precond(num_vars); @@ -701,10 +733,13 @@ fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond { ret first; } -fn union_postconds(&vec[postcond] pcs) -> postcond { - check (len[postcond](pcs) > 0u); - - ret union_postconds_go(bitv.clone(pcs.(0)), pcs); +fn union_postconds(uint nv, &vec[postcond] pcs) -> postcond { + if (len[postcond](pcs) > 0u) { + ret union_postconds_go(bitv.clone(pcs.(0)), pcs); + } + else { + ret empty_prestate(nv); + } } /* Gee, maybe we could use foldl or something */ @@ -804,6 +839,8 @@ fn find_pre_post_item(fn_info_map fm, fn_info enclosing, &item i) -> () { be the union of all postconditions for */ fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing, &vec[@expr] args, ann a) { + auto nv = num_locals(enclosing); + fn do_one(fn_info_map fm, fn_info enclosing, &@expr e) -> () { find_pre_post_expr(fm, enclosing, *e); @@ -820,9 +857,22 @@ fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing, auto h = get_post; set_pre_and_post(a, - rec(precondition=seq_preconds(num_locals(enclosing), pps), + rec(precondition=seq_preconds(nv, pps), postcondition=union_postconds - (_vec.map[pre_and_post, postcond](h, pps)))); + (nv, (_vec.map[pre_and_post, postcond](h, pps))))); +} + +fn find_pre_post_loop(&fn_info_map fm, &fn_info enclosing, &@decl d, + &@expr index, &block body, &ann a) -> () { + find_pre_post_expr(fm, enclosing, *index); + find_pre_post_block(fm, enclosing, body); + auto loop_precond = declare_var(enclosing, decl_lhs(d), + seq_preconds(num_locals(enclosing), vec(expr_pp(*index), + block_pp(body)))); + auto loop_postcond = intersect_postconds + (vec(expr_postcond(*index), block_postcond(body))); + set_pre_and_post(a, rec(precondition=loop_precond, + postcondition=loop_postcond)); } /* Fills in annotations as a side effect. Does not rebuild the expr */ @@ -833,21 +883,26 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { find_pre_post_expr(fm, enclosing, *e); } fn pp_one(&@expr e) -> pre_and_post { - be expr_pp(*e); + ret expr_pp(*e); } - - /* log("find_pre_post_expr (num_locals =" + + /* + log("find_pre_post_expr (num_locals =" + uistr(num_local_vars) + "):"); log_expr(e); */ - - alt(e.node) { - case(expr_call(?operator, ?operands, ?a)) { + alt (e.node) { + case (expr_call(?operator, ?operands, ?a)) { auto args = _vec.clone[@expr](operands); _vec.push[@expr](args, operator); find_pre_post_exprs(fm, enclosing, args, a); } - case(expr_path(?p, ?maybe_def, ?a)) { + case (expr_vec(?args, _, ?a)) { + find_pre_post_exprs(fm, enclosing, args, a); + } + case (expr_tup(?elts, ?a)) { + find_pre_post_exprs(fm, enclosing, elt_exprs(elts), a); + } + case (expr_path(?p, ?maybe_def, ?a)) { auto df; alt (maybe_def) { case (none[def]) @@ -872,6 +927,17 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { find_pre_post_expr(fm, enclosing, *arg); set_pre_and_post(a, expr_pp(*arg)); } + case(expr_put(?opt, ?a)) { + alt (opt) { + case (some[@expr](?arg)) { + find_pre_post_expr(fm, enclosing, *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(fm, enclosing, b); set_pre_and_post(a, block_pp(b)); @@ -886,6 +952,8 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) { find_pre_post_expr(fm, enclosing, *rhs); set_pre_and_post(a, expr_pp(*rhs)); + log("gen:"); + log_expr(e); gen(enclosing, a, d_id); } case (_) { @@ -895,19 +963,26 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { } } } + case (expr_assign_op(_, ?lhs, ?rhs, ?a)) { + /* Different from expr_assign in that the lhs *must* + already be initialized */ + find_pre_post_exprs(fm, enclosing, vec(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, empty_pre_post(num_local_vars)); + 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(fm, enclosing, *ret_val); let pre_and_post pp = rec(precondition=expr_precond(*ret_val), - postcondition=empty_poststate(num_local_vars)); + postcondition=false_postcond(num_local_vars)); set_pre_and_post(a, pp); } } @@ -930,14 +1005,17 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { seq_preconds(num_local_vars, vec(expr_pp(*antec), block_pp(conseq))); auto postcond_true_case = union_postconds - (vec(expr_postcond(*antec), block_postcond(conseq))); + (num_local_vars, + vec(expr_postcond(*antec), block_postcond(conseq))); auto precond_false_case = seq_preconds (num_local_vars, vec(expr_pp(*antec), expr_pp(*altern))); auto postcond_false_case = union_postconds - (vec(expr_postcond(*antec), expr_postcond(*altern))); - auto precond_res = union_postconds(vec(precond_true_case, - precond_false_case)); + (num_local_vars, + vec(expr_postcond(*antec), expr_postcond(*altern))); + auto precond_res = union_postconds + (num_local_vars, + vec(precond_true_case, precond_false_case)); auto postcond_res = intersect_postconds (vec(postcond_true_case, postcond_false_case)); set_pre_and_post(a, rec(precondition=precond_res, @@ -954,6 +1032,10 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { find_pre_post_expr(fm, enclosing, *operand); set_pre_and_post(a, expr_pp(*operand)); } + case (expr_cast(?operand, _, ?a)) { + find_pre_post_expr(fm, enclosing, *operand); + set_pre_and_post(a, expr_pp(*operand)); + } case (expr_while(?test, ?body, ?a)) { find_pre_post_expr(fm, enclosing, *test); find_pre_post_block(fm, enclosing, body); @@ -966,6 +1048,12 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { intersect_postconds(vec(expr_postcond(*test), block_postcond(body))))); } + case (expr_for(?d, ?index, ?body, ?a)) { + find_pre_post_loop(fm, enclosing, d, index, body, a); + } + case (expr_for_each(?d, ?index, ?body, ?a)) { + find_pre_post_loop(fm, enclosing, d, index, body, a); + } case (expr_index(?e, ?sub, ?a)) { find_pre_post_exprs(fm, enclosing, vec(e, sub), a); } @@ -998,12 +1086,27 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { } 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=true_postcond(num_local_vars))); + postcondition=false_postcond(num_local_vars))); + } + case (expr_check_expr(?p, ?a)) { + /* will need to change when we support arbitrary predicates... */ + find_pre_post_expr(fm, enclosing, *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(fm, enclosing, args, a); + } + case (expr_break(?a)) { + set_pre_and_post(a, empty_pre_post(num_local_vars)); } case(_) { - log("this sort of expr isn't implemented!"); - log_expr(e); + log_err("this sort of expr isn't implemented!"); + log_expr_err(e); fail; } } @@ -1012,10 +1115,18 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { fn gen(&fn_info enclosing, &ann a, def_id id) -> bool { check(enclosing.contains_key(id)); let uint i = (enclosing.get(id))._0; - ret set_in_postcond(i, (ann_to_ts_ann_fail_more(a)).conditions); } +fn declare_var(&fn_info enclosing, def_id id, prestate pre) + -> prestate { + check(enclosing.contains_key(id)); + let uint i = (enclosing.get(id))._0; + auto res = clone(pre); + relax_prestate(i, res); + ret res; +} + fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool { check(enclosing.contains_key(id)); let uint i = (enclosing.get(id))._0; @@ -1039,7 +1150,13 @@ fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s) /* 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(enclosing, a, alocal.id); + /* log_err("for stmt"); + log_stmt(s); + log_err("pp = "); + log_pp(stmt_pp(s)); */ } case(none[ast.initializer]) { auto pp = empty_pre_post(num_local_vars); @@ -1064,6 +1181,8 @@ fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s) fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) -> () { + auto nv = num_locals(enclosing); + fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () { find_pre_post_stmt(fm, i, *s); } @@ -1089,13 +1208,13 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) 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(num_locals(enclosing), pps); + auto block_precond = seq_preconds(nv, 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 = union_postconds(postconds); + auto block_postcond = union_postconds(nv, postconds); set_pre_and_post(b.node.a, rec(precondition=block_precond, postcondition=block_postcond)); } @@ -1142,11 +1261,11 @@ fn find_pre_post_state_item(fn_info_map fm, fn_info enclosing, @item i) } } -fn set_prestate_ann(ann a, prestate pre) -> bool { - alt (a) { +fn set_prestate_ann(@ann a, prestate pre) -> bool { + alt (*a) { case (ann_type(_,_,?ts_a)) { check (! is_none[@ts_ann](ts_a)); - ret set_prestate(*get[@ts_ann](ts_a), pre); + ret set_prestate(get[@ts_ann](ts_a), pre); } case (ann_none) { log("set_prestate_ann: expected an ann_type here"); @@ -1246,17 +1365,37 @@ fn pure_exp(&ann a, &prestate p) -> bool { ret changed; } +fn find_pre_post_state_loop(fn_info_map fm, fn_info enclosing, + 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(fm, enclosing, pres, index) + || changed; + /* in general, would need the intersection of + (poststate of index, poststate of body) */ + changed = find_pre_post_state_block(fm, enclosing, + expr_poststate(*index), body) || changed; + auto res_p = intersect_postconds(vec(expr_poststate(*index), + block_poststate(body))); + + changed = extend_poststate_ann(a, res_p) || changed; + ret changed; +} + fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, &prestate pres, &@expr e) -> bool { auto changed = false; auto num_local_vars = num_locals(enclosing); + /* FIXME could get rid of some of the copy/paste */ alt (e.node) { case (expr_vec(?elts, _, ?a)) { - be find_pre_post_state_exprs(fm, enclosing, pres, a, elts); + ret find_pre_post_state_exprs(fm, enclosing, pres, a, elts); } case (expr_tup(?elts, ?a)) { - be find_pre_post_state_exprs(fm, enclosing, pres, a, elt_exprs(elts)); + ret find_pre_post_state_exprs(fm, enclosing, pres, a, elt_exprs(elts)); } case (expr_call(?operator, ?operands, ?a)) { /* do the prestate for the rator */ @@ -1267,15 +1406,37 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, expr_poststate(*operator), a, operands) || changed); } + case (expr_bind(?operator, ?maybe_args, ?a)) { + changed = find_pre_post_state_expr(fm, enclosing, pres, operator) + || changed; + ret (find_pre_post_state_exprs(fm, enclosing, + 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(fm, enclosing, pres, e); changed = extend_prestate_ann(a, pres) || changed; changed = extend_poststate_ann(a, expr_poststate(*e)) || changed; ret changed; } + case (expr_put(?maybe_e, ?a)) { + alt (maybe_e) { + case (some[@expr](?arg)) { + changed = find_pre_post_state_expr(fm, enclosing, 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); } @@ -1327,7 +1488,7 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, } case (expr_ret(?maybe_ret_val, ?a)) { changed = extend_prestate_ann(a, pres) || changed; - set_poststate_ann(a, empty_poststate(num_local_vars)); + set_poststate_ann(a, false_postcond(num_local_vars)); alt(maybe_ret_val) { case (none[@expr]) { /* do nothing */ } case (some[@expr](?ret_val)) { @@ -1368,6 +1529,16 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, 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(fm, enclosing, pres, lhs) + || changed; + changed = find_pre_post_state_expr(fm, + enclosing, 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 @@ -1387,6 +1558,12 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, block_poststate(body)))) || changed; ret changed; } + case (expr_for(?d, ?index, ?body, ?a)) { + ret find_pre_post_state_loop(fm, enclosing, pres, d, index, body, a); + } + case (expr_for_each(?d, ?index, ?body, ?a)) { + ret find_pre_post_state_loop(fm, enclosing, pres, d, index, body, a); + } case (expr_index(?e, ?sub, ?a)) { changed = extend_prestate_ann(a, pres) || changed; changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed; @@ -1399,13 +1576,21 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, changed = extend_prestate_ann(a, pres) || changed; changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed; auto e_post = expr_poststate(*e); - auto a_post = ann_to_poststate(a); - for (arm an_alt in alts) { - changed = find_pre_post_state_block(fm, enclosing, e_post, - an_alt.block) || changed; - changed = intersect(a_post, block_poststate(an_alt.block)) - || changed; + 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(fm, enclosing, 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)) { @@ -1422,14 +1607,36 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, || changed; ret changed; } + case (expr_cast(?operand, _, ?a)) { + changed = find_pre_post_state_expr(fm, enclosing, 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; - changed = set_poststate_ann(a, true_postcond(num_local_vars)) + /* if execution continues after fail, then everything is true! woo! */ + changed = set_poststate_ann(a, false_postcond(num_local_vars)) || changed; + /* log_err("fail: poststate = "); + log_bitv(enclosing, expr_poststate(*e)); */ + ret changed; + } + case (expr_check_expr(?p, ?a)) { + changed = extend_prestate_ann(a, pres) || changed; + changed = find_pre_post_state_expr(fm, enclosing, pres, p) || changed; + /* p is pure, so the poststate must be the same as the prestate */ + changed = extend_poststate_ann(a, pres) || changed; ret changed; } + case (expr_break(?a)) { + ret pure_exp(a, pres); + } case (_) { - log("find_pre_post_state_expr: implement this case!"); + log_err("find_pre_post_state_expr: implement this case!"); + log_expr_err(*e); fail; } } @@ -1442,41 +1649,41 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, auto stmt_ann_ = stmt_to_ann(*s); check (!is_none[@ts_ann](stmt_ann_)); auto stmt_ann = *(get[@ts_ann](stmt_ann_)); - /* - log("*At beginning: stmt = "); + /* + log_err("*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_err("*prestate = "); + log_err(bitv.to_str(stmt_ann.states.prestate)); + log_err("*poststate ="); + log_err(bitv.to_str(stmt_ann.states.poststate)); + log_err("*changed ="); log(changed); - */ + */ alt (s.node) { case (stmt_decl(?adecl, ?a)) { alt (adecl.node) { case (ast.decl_local(?alocal)) { alt (alocal.init) { case (some[ast.initializer](?an_init)) { - changed = find_pre_post_state_expr - (fm, enclosing, pres, an_init.expr) || changed; - changed = extend_poststate(stmt_ann.states.poststate, - expr_poststate(*an_init.expr)) - || changed; - changed = gen_poststate(enclosing, a, alocal.id) || changed; - - /* - log("Summary: stmt = "); + changed = extend_prestate(stmt_ann.states.prestate, pres) + || changed; + changed = find_pre_post_state_expr + (fm, enclosing, pres, an_init.expr) || changed; + changed = extend_poststate(stmt_ann.states.poststate, + expr_poststate(*an_init.expr)) + || changed; + changed = gen_poststate(enclosing, a, alocal.id) || changed; + /* + log_err("Summary: stmt = "); log_stmt(*s); - log("prestate = "); - log(bitv.to_str(stmt_ann.states.prestate)); + log_err("prestate = "); + log_err(bitv.to_str(stmt_ann.states.prestate)); log_bitv(enclosing, stmt_ann.states.prestate); - log("poststate ="); + log_err("poststate ="); log_bitv(enclosing, stmt_ann.states.poststate); - log("changed ="); - log(changed); - */ - + log_err("changed ="); + log_err(changed); + */ ret changed; } case (none[ast.initializer]) { @@ -1489,7 +1696,11 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, } } case (ast.decl_item(?an_item)) { - be find_pre_post_state_item(fm, enclosing, 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(fm, enclosing, an_item) || changed); } } } @@ -1499,16 +1710,16 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, || changed; changed = extend_poststate(stmt_ann.states.poststate, expr_poststate(*e)) || changed; - /* - log("Summary: stmt = "); + + /* log_err("Summary: stmt = "); log_stmt(*s); - log("prestate = "); - log(bitv.to_str(stmt_ann.states.prestate)); + log_err("prestate = "); + log_err(bitv.to_str(stmt_ann.states.prestate)); log_bitv(enclosing, stmt_ann.states.prestate); - log("poststate ="); + log_err("poststate ="); log_bitv(enclosing, stmt_ann.states.poststate); - log("changed ="); - log(changed); + log_err("changed ="); + log_err(changed); */ ret changed; } @@ -1519,7 +1730,7 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, /* 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_info_map fm, &fn_info enclosing, - &prestate pres0, block b) + &prestate pres0, &block b) -> bool { auto changed = false; @@ -1545,8 +1756,20 @@ fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing, post = expr_poststate(*e); } } - set_prestate_ann(b.node.a, pres0); + set_prestate_ann(@b.node.a, pres0); set_poststate_ann(b.node.a, post); + + /* + log_err("For block:"); + log_block(b); + log_err("poststate = "); + log_states(block_states(b)); + log_err("pres0:"); + log_bitv(enclosing, pres0); + log_err("post:"); + log_bitv(enclosing, post); + */ + ret changed; } @@ -1579,12 +1802,12 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () { let prestate pres = expr_prestate(e); if (!implies(pres, prec)) { - log("check_states_expr: unsatisfied precondition for "); - log_expr(e); - log("Precondition: "); - log_bitv(enclosing, prec); - log("Prestate: "); - log_bitv(enclosing, pres); + log_err("check_states_expr: unsatisfied precondition for "); + log_expr_err(e); + log_err("Precondition: "); + log_bitv_err(enclosing, prec); + log_err("Prestate: "); + log_bitv_err(enclosing, pres); fail; } } @@ -1608,12 +1831,12 @@ fn check_states_stmt(fn_info enclosing, &stmt s) -> () { */ if (!implies(pres, prec)) { - log("check_states_stmt: unsatisfied precondition for "); - log_stmt(s); - log("Precondition: "); - log_bitv(enclosing, prec); - log("Prestate: "); - log_bitv(enclosing, pres); + log_err("check_states_stmt: unsatisfied precondition for "); + log_stmt_err(s); + log_err("Precondition: "); + log_bitv_err(enclosing, prec); + log_err("Prestate: "); + log_bitv_err(enclosing, pres); fail; } } @@ -1680,8 +1903,12 @@ fn check_obj_state(&fn_info_map f_info_map, vec[obj_field] fields, fn init_ann(&fn_info fi, ann a) -> ann { alt (a) { case (ann_none) { - log("init_ann: shouldn't see ann_none"); - fail; + // log("init_ann: shouldn't see ann_none"); + // fail; + log("warning: init_ann: saw ann_none"); + ret a; // Would be better to fail so we can catch bugs that + // result in an uninitialized ann -- but don't want to have to + // write code to handle native_mods properly } case (ann_type(?t,?ps,_)) { ret ann_type(t, ps, some[@ts_ann](@empty_ann(num_locals(fi)))); @@ -1692,8 +1919,10 @@ fn init_ann(&fn_info fi, ann a) -> ann { fn init_blank_ann(&() ignore, ann a) -> ann { alt (a) { case (ann_none) { - log("init_ann: shouldn't see ann_none"); - fail; + // log("init_blank_ann: shouldn't see ann_none"); + //fail; + log("warning: init_blank_ann: saw ann_none"); + ret a; } case (ann_type(?t,?ps,_)) { ret ann_type(t, ps, some[@ts_ann](@empty_ann(0u))); @@ -1706,7 +1935,7 @@ fn init_block(&fn_info fi, &span sp, &block_ b) -> block { log_block(respan(sp, b)); alt(b.a) { case (ann_none) { - log("init_ann: shouldn't see ann_none"); + log("init_block: shouldn't see ann_none"); fail; } case (ann_type(?t,?ps,_)) { @@ -1730,7 +1959,6 @@ fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast._fn f, auto fld0 = fold.new_identity_fold[fn_info](); fld0 = @rec(fold_ann = bind init_ann(_,_) - // fold_block = bind init_block(_,_,_) with *fld0); ret fold.fold_item[fn_info] @@ -1999,11 +2227,6 @@ fn annotate_mod(&fn_info_map fm, &ast._mod m) -> ast._mod { } ret rec(items=new_items, index=new_index with m); } -fn annotate_native_mod(&fn_info_map fm, &ast.native_mod m) - -> ast.native_mod { - log("implement annotate_native_mod!"); - fail; -} fn annotate_method(&fn_info_map fm, &@method m) -> @method { auto f_info = get_fn_info(fm, m.node.id); auto fld0 = fold.new_identity_fold[fn_info](); @@ -2044,9 +2267,7 @@ fn annotate_item_inner(&fn_info_map fm, &@ast.item item) -> @ast.item { ast.item_mod(ident, annotate_mod(fm, mm), id)); } case (ast.item_native_mod(?ident, ?mm, ?id)) { - ret @respan(item.span, - ast.item_native_mod(ident, - annotate_native_mod(fm, mm), id)); + ret item; } case (ast.item_ty(_,_,_,_,_)) { ret item; @@ -2090,6 +2311,9 @@ fn annotate_item(&fn_info_map fm, &@ast.item item) -> @ast.item { auto outer = fold.fold_item[()]((), fld0, item); ret annotate_item_inner(fm, outer); } + case (ast.item_native_mod(?i, ?nm, ?id)) { + ret item; + } case (ast.item_ty(_,_,_,_,_)) { ret item; } diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs index a9e02c20e03ce..d2ed72a0ff341 100644 --- a/src/comp/util/common.rs +++ b/src/comp/util/common.rs @@ -98,9 +98,9 @@ fn uistr(uint i) -> str { fn elt_expr(&ast.elt e) -> @ast.expr { ret e.expr; } -fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] { +fn elt_exprs(&vec[ast.elt] elts) -> vec[@ast.expr] { auto f = elt_expr; - be _vec.map[ast.elt, @ast.expr](f, elts); + ret _vec.map[ast.elt, @ast.expr](f, elts); } fn field_expr(&ast.field f) -> @ast.expr { ret f.expr; } @@ -115,18 +115,25 @@ fn plain_ann(middle.ty.ctxt tcx) -> ast.ann { none[vec[middle.ty.t]], none[@ts_ann]); } -fn log_expr(&ast.expr e) -> () { +fn expr_to_str(&ast.expr e) -> str { let str_writer s = string_writer(); auto out_ = mkstate(s.get_writer(), 80u); auto out = @rec(s=out_, comments=none[vec[front.lexer.cmnt]], mutable cur_cmnt=0u); - print_expr(out, @e); - log(s.get_str()); + ret s.get_str(); } -fn log_block(&ast.block b) -> () { +fn log_expr(&ast.expr e) -> () { + log(expr_to_str(e)); +} + +fn log_expr_err(&ast.expr e) -> () { + log_err(expr_to_str(e)); +} + +fn block_to_str(&ast.block b) -> str { let str_writer s = string_writer(); auto out_ = mkstate(s.get_writer(), 80u); auto out = @rec(s=out_, @@ -134,7 +141,15 @@ fn log_block(&ast.block b) -> () { mutable cur_cmnt=0u); print_block(out, b); - log(s.get_str()); + ret s.get_str(); +} + +fn log_block(&ast.block b) -> () { + log(block_to_str(b)); +} + +fn log_block_err(&ast.block b) -> () { + log_err(block_to_str(b)); } fn log_ann(&ast.ann a) -> () { @@ -148,7 +163,7 @@ fn log_ann(&ast.ann a) -> () { } } -fn log_stmt(ast.stmt st) -> () { +fn stmt_to_str(&ast.stmt st) -> str { let str_writer s = string_writer(); auto out_ = mkstate(s.get_writer(), 80u); auto out = @rec(s=out_, @@ -163,7 +178,48 @@ fn log_stmt(ast.stmt st) -> () { } case (_) { /* do nothing */ } } - log(s.get_str()); + ret s.get_str(); +} + +fn log_stmt(&ast.stmt st) -> () { + log(stmt_to_str(st)); +} + +fn log_stmt_err(&ast.stmt st) -> () { + log_err(stmt_to_str(st)); +} + +fn decl_lhs(@ast.decl d) -> ast.def_id { + alt (d.node) { + case (ast.decl_local(?l)) { + ret l.id; + } + case (ast.decl_item(?an_item)) { + alt (an_item.node) { + case (ast.item_const(_,_,_,?d,_)) { + ret d; + } + case (ast.item_fn(_,_,_,?d,_)) { + ret d; + } + case (ast.item_mod(_,_,?d)) { + ret d; + } + case (ast.item_native_mod(_,_,?d)) { + ret d; + } + case (ast.item_ty(_,_,_,?d,_)) { + ret d; + } + case (ast.item_tag(_,_,_,?d,_)) { + ret d; + } + case (ast.item_obj(_,_,_,?d,_)) { + ret d.ctor; /* This doesn't really make sense */ + } + } + } + } } // diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs index 9ad6e01e8dd27..b7fbc3cc25d58 100644 --- a/src/comp/util/typestate_ann.rs +++ b/src/comp/util/typestate_ann.rs @@ -44,6 +44,10 @@ fn empty_poststate(uint num_vars) -> poststate { be true_precond(num_vars); } +fn false_postcond(uint num_vars) -> postcond { + be bitv.create(num_vars, true); +} + fn empty_pre_post(uint num_vars) -> pre_and_post { ret(rec(precondition=empty_prestate(num_vars), postcondition=empty_poststate(num_vars))); @@ -119,7 +123,7 @@ fn set_postcondition(&ts_ann a, &postcond p) -> () { // Sets all the bits in a's prestate to equal the // corresponding bit in p's prestate. -fn set_prestate(&ts_ann a, &prestate p) -> bool { +fn set_prestate(@ts_ann a, &prestate p) -> bool { ret bitv.copy(a.states.prestate, p); } @@ -139,6 +143,13 @@ fn extend_poststate(&poststate p, &poststate new) -> bool { ret bitv.union(p, new); } +// Clears the given bit in p +fn relax_prestate(uint i, &prestate p) -> bool { + auto was_set = bitv.get(p, i); + bitv.set(p, i, false); + ret was_set; +} + fn ann_precond(&ts_ann a) -> precond { ret a.conditions.precondition; } @@ -148,8 +159,12 @@ fn ann_prestate(&ts_ann a) -> prestate { } fn pp_clone(&pre_and_post p) -> pre_and_post { - ret rec(precondition=bitv.clone(p.precondition), - postcondition=bitv.clone(p.postcondition)); + ret rec(precondition=clone(p.precondition), + postcondition=clone(p.postcondition)); +} + +fn clone(prestate p) -> prestate { + ret bitv.clone(p); } // returns true if a implies b diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs index cc8fabcaf1606..21a6cff560d94 100644 --- a/src/lib/_vec.rs +++ b/src/lib/_vec.rs @@ -280,6 +280,21 @@ fn plus_option[T](&vec[T] v, &option.t[T] o) -> () { } } +fn cat_options[T](&vec[option.t[T]] v) -> vec[T] { + let vec[T] res = vec(); + + for (option.t[T] o in v) { + alt (o) { + case (none[T]) { } + case (some[T](?t)) { + res += vec(t); + } + } + } + + ret res; +} + // TODO: Remove in favor of built-in "freeze" operation when it's implemented. fn freeze[T](vec[mutable T] v) -> vec[T] { let vec[T] result = vec(); diff --git a/src/test/run-pass/use-uninit-alt.rs b/src/test/run-pass/use-uninit-alt.rs new file mode 100644 index 0000000000000..a7c77bba2eaac --- /dev/null +++ b/src/test/run-pass/use-uninit-alt.rs @@ -0,0 +1,21 @@ +fn foo[T](&myoption[T] o) -> int { + let int x = 5; + + alt (o) { + case (none[T]) { } + case (some[T](?t)) { + x += 1; + } + } + + ret x; +} + +tag myoption[T] { + none; + some(T); +} + +fn main() { + log(5); +} \ No newline at end of file diff --git a/src/test/run-pass/use-uninit-alt2.rs b/src/test/run-pass/use-uninit-alt2.rs new file mode 100644 index 0000000000000..36514d13ce139 --- /dev/null +++ b/src/test/run-pass/use-uninit-alt2.rs @@ -0,0 +1,21 @@ +fn foo[T](&myoption[T] o) -> int { + let int x; + + alt (o) { + case (none[T]) { fail; } + case (some[T](?t)) { + x = 5; + } + } + + ret x; +} + +tag myoption[T] { + none; + some(T); +} + +fn main() { + log(5); +} \ No newline at end of file From 54e27d265f9287c1e4680ab578334a53c0747d9e Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Thu, 21 Apr 2011 17:39:04 -0700 Subject: [PATCH 02/11] Support all expression forms in typestate Added support for self_method, cont, chan, port, recv, send, be, do_while, spawn, and ext; handled break and cont correctly. (However, there are no non-xfailed test cases for ext or spawn in stage0 currently.) Although the standard library compiles and all test cases pass with typestate enabled, I left typestate checking disabled as rustc terminates abnormally when building the standard library if so, even though it does generate code correctly. --- src/comp/middle/typestate_check.rs | 210 +++++++++++++++++++++++-- src/comp/util/common.rs | 32 ++++ src/test/compile-fail/break-uninit.rs | 22 +++ src/test/compile-fail/break-uninit2.rs | 22 +++ 4 files changed, 274 insertions(+), 12 deletions(-) create mode 100644 src/test/compile-fail/break-uninit.rs create mode 100644 src/test/compile-fail/break-uninit2.rs diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 04aeebdf37ca4..693521778ddd5 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -106,6 +106,7 @@ import util.common.log_stmt; import util.common.log_block; import util.common.log_stmt_err; import util.common.log_block_err; +import util.common.has_nonlocal_exits; import util.common.decl_lhs; import util.typestate_ann; import util.typestate_ann.ts_ann; @@ -466,6 +467,9 @@ fn expr_ann(&expr e) -> ann { case (expr_cont(?a)) { ret a; } + case (expr_self_method(_, ?a)) { + ret a; + } } } @@ -896,6 +900,11 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { _vec.push[@expr](args, operator); find_pre_post_exprs(fm, enclosing, args, a); } + case (expr_spawn(_, _, ?operator, ?operands, ?a)) { + auto args = _vec.clone[@expr](operands); + _vec.push[@expr](args, operator); + find_pre_post_exprs(fm, enclosing, args, a); + } case (expr_vec(?args, _, ?a)) { find_pre_post_exprs(fm, enclosing, args, a); } @@ -923,10 +932,19 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { // 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(fm, enclosing, *arg); set_pre_and_post(a, expr_pp(*arg)); } + case (expr_chan(?arg, ?a)) { + find_pre_post_expr(fm, enclosing, *arg); + set_pre_and_post(a, expr_pp(*arg)); + } case(expr_put(?opt, ?a)) { alt (opt) { case (some[@expr](?arg)) { @@ -963,6 +981,22 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { } } } + case (expr_recv(?lhs, ?rhs, ?a)) { + alt (lhs.node) { + case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) { + find_pre_post_expr(fm, enclosing, *rhs); + set_pre_and_post(a, expr_pp(*rhs)); + log("gen:"); + log_expr(e); + gen(enclosing, a, d_id); + } + case (_) { + // doesn't check that lhs is an lval, but + // that's probably ok + find_pre_post_exprs(fm, enclosing, vec(lhs, rhs), a); + } + } + } case (expr_assign_op(_, ?lhs, ?rhs, ?a)) { /* Different from expr_assign in that the lhs *must* already be initialized */ @@ -987,6 +1021,11 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { } } } + case (expr_be(?e, ?a)) { + find_pre_post_expr(fm, enclosing, *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(fm, enclosing, *antec); find_pre_post_block(fm, enclosing, conseq); @@ -1028,6 +1067,9 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { FIXME */ find_pre_post_exprs(fm, enclosing, vec(l, r), a); } + case (expr_send(?l, ?r, ?a)) { + find_pre_post_exprs(fm, enclosing, vec(l, r), a); + } case (expr_unary(_,?operand,?a)) { find_pre_post_expr(fm, enclosing, *operand); set_pre_and_post(a, expr_pp(*operand)); @@ -1048,6 +1090,24 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { intersect_postconds(vec(expr_postcond(*test), block_postcond(body))))); } + case (expr_do_while(?body, ?test, ?a)) { + find_pre_post_block(fm, enclosing, body); + find_pre_post_expr(fm, enclosing, *test); + + auto loop_postcond = union_postconds(num_local_vars, + vec(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(num_local_vars, + vec(block_pp(body), + expr_pp(*test))), + postcondition=loop_postcond)); + } case (expr_for(?d, ?index, ?body, ?a)) { find_pre_post_loop(fm, enclosing, d, index, body, a); } @@ -1104,10 +1164,15 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { case (expr_break(?a)) { set_pre_and_post(a, empty_pre_post(num_local_vars)); } - case(_) { - log_err("this sort of expr isn't implemented!"); - log_expr_err(e); - fail; + 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(fm, enclosing, *expanded); + set_pre_and_post(a, expr_pp(*expanded)); } } } @@ -1181,6 +1246,22 @@ fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s) fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, 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(enclosing); fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () { @@ -1214,7 +1295,11 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) /* 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 = union_postconds(nv, postconds); + 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)); } @@ -1406,6 +1491,12 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, expr_poststate(*operator), a, operands) || changed); } + case (expr_spawn(_, _, ?operator, ?operands, ?a)) { + changed = find_pre_post_state_expr(fm, enclosing, pres, operator); + ret(find_pre_post_state_exprs(fm, enclosing, + expr_poststate(*operator), a, operands) + || changed); + } case (expr_bind(?operator, ?maybe_args, ?a)) { changed = find_pre_post_state_expr(fm, enclosing, pres, operator) || changed; @@ -1423,6 +1514,19 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, changed = extend_poststate_ann(a, expr_poststate(*e)) || changed; ret changed; } + case (expr_chan(?e, ?a)) { + changed = find_pre_post_state_expr(fm, enclosing, 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(fm, enclosing, 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)) { @@ -1486,6 +1590,32 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, } ret changed; } + case (expr_recv(?lhs, ?rhs, ?a)) { + extend_prestate_ann(a, pres); + + alt (lhs.node) { + case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) { + // receive to local var + changed = pure_exp(a_lhs, pres) || changed; + changed = find_pre_post_state_expr(fm, enclosing, pres, rhs) + || changed; + changed = extend_poststate_ann(a, expr_poststate(*rhs)) + || changed; + changed = gen_poststate(enclosing, a, d_id) || changed; + } + case (_) { + // receive to something that must already have been init'd + changed = find_pre_post_state_expr(fm, enclosing, pres, lhs) + || changed; + changed = find_pre_post_state_expr(fm, enclosing, + 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)); @@ -1498,6 +1628,12 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, } 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(fm, enclosing, 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(fm, enclosing, pres, antec) @@ -1529,6 +1665,15 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, 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(fm, enclosing, pres, l) + || changed; + changed = find_pre_post_state_expr(fm, + enclosing, 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; @@ -1558,6 +1703,27 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, 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(fm, enclosing, pres, body) + || changed; + changed = find_pre_post_state_expr(fm, enclosing, + 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(fm, enclosing, pres, d, index, body, a); } @@ -1634,13 +1800,16 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, case (expr_break(?a)) { ret pure_exp(a, pres); } - case (_) { - log_err("find_pre_post_state_expr: implement this case!"); - log_expr_err(*e); - fail; + 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_info_map fm, &fn_info enclosing, @@ -1733,6 +1902,8 @@ fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing, &prestate pres0, &block b) -> bool { + /* FIXME handle non-local exits */ + auto changed = false; auto num_local_vars = num_locals(enclosing); @@ -1756,6 +1927,20 @@ fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing, 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); @@ -1802,7 +1987,7 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () { let prestate pres = expr_prestate(e); if (!implies(pres, prec)) { - log_err("check_states_expr: unsatisfied precondition for "); + log_err("check_states_expr: Unsatisfied precondition constraint for "); log_expr_err(e); log_err("Precondition: "); log_bitv_err(enclosing, prec); @@ -1831,7 +2016,8 @@ fn check_states_stmt(fn_info enclosing, &stmt s) -> () { */ if (!implies(pres, prec)) { - log_err("check_states_stmt: unsatisfied precondition for "); + log_err("check_states_stmt: " + + "Unsatisfied precondition constraint for "); log_stmt_err(s); log_err("Precondition: "); log_bitv_err(enclosing, prec); diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs index d2ed72a0ff341..fd0d688bab8e8 100644 --- a/src/comp/util/common.rs +++ b/src/comp/util/common.rs @@ -1,3 +1,5 @@ +import std.map; +import std.map.hashmap; import std._uint; import std._int; import std._vec; @@ -5,6 +7,9 @@ import std.option.none; import front.ast; import util.typestate_ann.ts_ann; +import middle.fold; +import middle.fold.respan; + import std.io.stdout; import std.io.str_writer; import std.io.string_writer; @@ -16,6 +21,7 @@ import pretty.pp.mkstate; type filename = str; type span = rec(uint lo, uint hi); type spanned[T] = rec(T node, span span); +type flag = hashmap[str, ()]; tag ty_mach { ty_i8; @@ -222,6 +228,32 @@ fn decl_lhs(@ast.decl d) -> ast.def_id { } } +fn has_nonlocal_exits(&ast.block b) -> bool { + /* overkill, but just passing around a mutable bool doesn't seem + to work in rustboot */ + auto has_exits = new_str_hash[()](); + + fn set_break(&flag f, &span sp, ast.ann a) -> @ast.expr { + f.insert("foo", ()); + ret @respan(sp, ast.expr_break(a)); + } + fn set_cont(&flag f, &span sp, ast.ann a) -> @ast.expr { + f.insert("foo", ()); + ret @respan(sp, ast.expr_cont(a)); + } + fn check_b(&flag f) -> bool { + ret (f.size() == 0u); + } + + auto fld0 = fold.new_identity_fold[flag](); + + fld0 = @rec(fold_expr_break = bind set_break(_,_,_), + fold_expr_cont = bind set_cont(_,_,_), + keep_going = bind check_b(_) with *fld0); + fold.fold_block[flag](has_exits, fld0, b); + + ret (has_exits.size() > 0u); +} // // Local Variables: // mode: rust diff --git a/src/test/compile-fail/break-uninit.rs b/src/test/compile-fail/break-uninit.rs new file mode 100644 index 0000000000000..e9085dd25e823 --- /dev/null +++ b/src/test/compile-fail/break-uninit.rs @@ -0,0 +1,22 @@ +// xfail-boot +// xfail-stage0 +// error-pattern:Unsatisfied precondition + +fn foo() -> int { + let int x; + let int i; + + do { + i = 0; + break; + x = 0; + } while ((x = 0) != 0); + + log(x); + + ret 17; +} + +fn main() { + log(foo()); +} diff --git a/src/test/compile-fail/break-uninit2.rs b/src/test/compile-fail/break-uninit2.rs new file mode 100644 index 0000000000000..8ef83f08cf5ec --- /dev/null +++ b/src/test/compile-fail/break-uninit2.rs @@ -0,0 +1,22 @@ +// xfail-boot +// xfail-stage0 +// error-pattern:Unsatisfied precondition + +fn foo() -> int { + let int x; + let int i; + + do { + i = 0; + break; + x = 0; + } while (1 != 2); + + log(x); + + ret 17; +} + +fn main() { + log(foo()); +} From e5f7f929ce0604ec724f542457c5454b2c9570c6 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 11:08:47 -0700 Subject: [PATCH 03/11] Fixed bug in typeck that wasn't filling in anns for stmts (needed for typestate_check). Also changed a (log; fail) to (log_err; fail) in typestate_check, and added some more logging funs in util.common. --- src/comp/middle/typeck.rs | 9 ++++++--- src/comp/middle/typestate_check.rs | 18 +++++++++++++----- src/comp/util/common.rs | 20 ++++++++++++++++++++ 3 files changed, 39 insertions(+), 8 deletions(-) diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index ce22999969562..0f96c3eb6b767 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -2623,22 +2623,25 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt { case (ast.decl_local(_)) { auto decl_1 = check_decl_local(fcx, decl); ret @fold.respan[ast.stmt_](stmt.span, - ast.stmt_decl(decl_1, a)); + ast.stmt_decl(decl_1, plain_ann(fcx.ccx.tystore))); } case (ast.decl_item(_)) { // Ignore for now. We'll return later. + ret @fold.respan[ast.stmt_](stmt.span, + ast.stmt_decl(decl, plain_ann(fcx.ccx.tystore))); } } - ret stmt; + // ret stmt; } case (ast.stmt_expr(?expr,?a)) { auto expr_t = check_expr(fcx, expr); expr_t = Pushdown.pushdown_expr(fcx, expr_ty(fcx.ccx.tcx, expr_t), expr_t); - ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t, a)); + ret @fold.respan[ast.stmt_](stmt.span, + ast.stmt_expr(expr_t, plain_ann(fcx.ccx.tystore))); } } diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 693521778ddd5..7ddfa94b1d055 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -105,6 +105,8 @@ import util.common.log_expr_err; import util.common.log_stmt; import util.common.log_block; import util.common.log_stmt_err; +import util.common.log_fn_err; +import util.common.log_fn; import util.common.log_block_err; import util.common.has_nonlocal_exits; import util.common.decl_lhs; @@ -889,11 +891,11 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { fn pp_one(&@expr e) -> pre_and_post { ret expr_pp(*e); } - /* + log("find_pre_post_expr (num_locals =" + uistr(num_local_vars) + "):"); - log_expr(e); - */ + log_expr(e); + alt (e.node) { case (expr_call(?operator, ?operands, ?a)) { auto args = _vec.clone[@expr](operands); @@ -1201,6 +1203,9 @@ fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool { fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s) -> () { + log("stmt ="); + log_stmt(s); + auto num_local_vars = num_locals(enclosing); alt(s.node) { case(ast.stmt_decl(?adecl, ?a)) { @@ -1311,6 +1316,9 @@ fn find_pre_post_fn(&fn_info_map fm, &fn_info fi, &_fn f) -> () { fn check_item_fn(&fn_info_map fm, &span sp, ident i, &ast._fn f, vec[ast.ty_param] ty_params, def_id id, ann a) -> @item { + log("check_item_fn:"); + log_fn(f, i, ty_params); + check (fm.contains_key(id)); find_pre_post_fn(fm, fm.get(id), f); @@ -1413,7 +1421,7 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () { set_postcondition(t, pp.postcondition); } case (ann_none) { - log("set_pre_and_post: expected an ann_type here"); + log_err("set_pre_and_post: expected an ann_type here"); fail; } } @@ -1749,7 +1757,7 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, changed = find_pre_post_state_block(fm, enclosing, e_post, an_alt.block) || changed; changed = intersect(a_post, block_poststate(an_alt.block)) - || changed; + || changed; } } else { diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs index fd0d688bab8e8..7484b4cf76f49 100644 --- a/src/comp/util/common.rs +++ b/src/comp/util/common.rs @@ -16,6 +16,7 @@ import std.io.string_writer; import pretty.pprust.print_block; import pretty.pprust.print_expr; import pretty.pprust.print_decl; +import pretty.pprust.print_fn; import pretty.pp.mkstate; type filename = str; @@ -169,6 +170,25 @@ fn log_ann(&ast.ann a) -> () { } } +fn fun_to_str(&ast._fn f, str name, vec[ast.ty_param] params) -> str { + let str_writer s = string_writer(); + auto out_ = mkstate(s.get_writer(), 80u); + auto out = @rec(s=out_, + comments=none[vec[front.lexer.cmnt]], + mutable cur_cmnt=0u); + + print_fn(out, f.decl, name, params); + ret s.get_str(); +} + +fn log_fn(&ast._fn f, str name, vec[ast.ty_param] params) -> () { + log(fun_to_str(f, name, params)); +} + +fn log_fn_err(&ast._fn f, str name, vec[ast.ty_param] params) -> () { + log_err(fun_to_str(f, name, params)); +} + fn stmt_to_str(&ast.stmt st) -> str { let str_writer s = string_writer(); auto out_ = mkstate(s.get_writer(), 80u); From ad288e1dd380e0aec0c64604e85c060253685214 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 14:23:54 -0700 Subject: [PATCH 04/11] Fix bug in handling of expr_alt (postcond for alts was being intersected with postcond for scrutinee) --- src/comp/middle/typestate_check.rs | 154 +++++++++++++++++++---------- src/test/run-pass/alt-join.rs | 34 +++++++ 2 files changed, 136 insertions(+), 52 deletions(-) create mode 100644 src/test/run-pass/alt-join.rs diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 7ddfa94b1d055..2bbcc3e722520 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -214,7 +214,7 @@ fn log_bitv_err(fn_info enclosing, bitv.t v) { log_err(bitv_to_str(enclosing, v)); } -fn log_cond(vec[uint] v) -> () { +fn tos (vec[uint] v) -> str { auto res = ""; for (uint i in v) { if (i == 0u) { @@ -224,8 +224,16 @@ fn log_cond(vec[uint] v) -> () { res += "1"; } } - log(res); + ret res; +} + +fn log_cond(vec[uint] v) -> () { + log(tos(v)); +} +fn log_cond_err(vec[uint] v) -> () { + log_err(tos(v)); } + fn log_pp(&pre_and_post pp) -> () { auto p1 = bitv.to_vec(pp.precondition); auto p2 = bitv.to_vec(pp.postcondition); @@ -235,6 +243,15 @@ fn log_pp(&pre_and_post pp) -> () { log_cond(p2); } +fn log_pp_err(&pre_and_post pp) -> () { + auto p1 = bitv.to_vec(pp.precondition); + auto p2 = bitv.to_vec(pp.postcondition); + log_err("pre:"); + log_cond_err(p1); + log_err("post:"); + log_cond_err(p2); +} + fn log_states(&pre_and_post_state pp) -> () { auto p1 = bitv.to_vec(pp.prestate); auto p2 = bitv.to_vec(pp.poststate); @@ -244,6 +261,15 @@ fn log_states(&pre_and_post_state pp) -> () { log_cond(p2); } +fn log_states_err(&pre_and_post_state pp) -> () { + auto p1 = bitv.to_vec(pp.prestate); + auto p2 = bitv.to_vec(pp.poststate); + log_err("prestate:"); + log_cond_err(p1); + log_err("poststate:"); + log_cond_err(p2); +} + fn print_ident(&ident i) -> () { log(" " + i + " "); } @@ -707,17 +733,27 @@ fn with_pp(ann a, pre_and_post p) -> ann { // return the precondition for evaluating each expr in order. // So, if e0's post is {x} and e1's pre is {x, y, z}, the entire // precondition shouldn't include x. -fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond { +fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond { let uint sz = len[pre_and_post](pps); - + let uint num_vars = num_locals(enclosing); + if (sz >= 1u) { auto first = pps.(0); check (pps_len(first) == num_vars); - let precond rest = seq_preconds(num_vars, + let precond rest = seq_preconds(enclosing, slice[pre_and_post](pps, 1u, sz)); difference(rest, first.postcondition); auto res = clone(first.precondition); union(res, rest); + + log("seq_preconds:"); + log("first.postcondition ="); + log_bitv(enclosing, first.postcondition); + log("rest ="); + log_bitv(enclosing, rest); + log("returning"); + log_bitv(enclosing, res); + ret res; } else { @@ -863,7 +899,7 @@ fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing, auto h = get_post; set_pre_and_post(a, - rec(precondition=seq_preconds(nv, pps), + rec(precondition=seq_preconds(enclosing, pps), postcondition=union_postconds (nv, (_vec.map[pre_and_post, postcond](h, pps))))); } @@ -873,7 +909,7 @@ fn find_pre_post_loop(&fn_info_map fm, &fn_info enclosing, &@decl d, find_pre_post_expr(fm, enclosing, *index); find_pre_post_block(fm, enclosing, body); auto loop_precond = declare_var(enclosing, decl_lhs(d), - seq_preconds(num_locals(enclosing), vec(expr_pp(*index), + seq_preconds(enclosing, vec(expr_pp(*index), block_pp(body)))); auto loop_postcond = intersect_postconds (vec(expr_postcond(*index), block_postcond(body))); @@ -1033,7 +1069,7 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { find_pre_post_block(fm, enclosing, conseq); alt (maybe_alt) { case (none[@expr]) { - auto precond_res = seq_preconds(num_local_vars, + auto precond_res = seq_preconds(enclosing, vec(expr_pp(*antec), block_pp(conseq))); set_pre_and_post(a, rec(precondition=precond_res, @@ -1043,13 +1079,13 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { case (some[@expr](?altern)) { find_pre_post_expr(fm, enclosing, *altern); auto precond_true_case = - seq_preconds(num_local_vars, + seq_preconds(enclosing, vec(expr_pp(*antec), block_pp(conseq))); auto postcond_true_case = union_postconds (num_local_vars, vec(expr_postcond(*antec), block_postcond(conseq))); auto precond_false_case = seq_preconds - (num_local_vars, + (enclosing, vec(expr_pp(*antec), expr_pp(*altern))); auto postcond_false_case = union_postconds (num_local_vars, @@ -1085,7 +1121,7 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { find_pre_post_block(fm, enclosing, body); set_pre_and_post(a, rec(precondition= - seq_preconds(num_local_vars, + seq_preconds(enclosing, vec(expr_pp(*test), block_pp(body))), postcondition= @@ -1105,7 +1141,7 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { } set_pre_and_post(a, - rec(precondition=seq_preconds(num_local_vars, + rec(precondition=seq_preconds(enclosing, vec(block_pp(body), expr_pp(*test))), postcondition=loop_postcond)); @@ -1129,18 +1165,22 @@ fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () { auto f = bind do_an_alt(fm, enclosing, _); auto alt_pps = _vec.map[arm, pre_and_post](f, alts); fn combine_pp(pre_and_post antec, - uint num_local_vars, &pre_and_post pp, + fn_info enclosing, &pre_and_post pp, &pre_and_post next) -> pre_and_post { - union(pp.precondition, seq_preconds(num_local_vars, + union(pp.precondition, seq_preconds(enclosing, vec(antec, next))); intersect(pp.postcondition, next.postcondition); ret pp; } - auto e_pp1 = expr_pp(*e); - auto e_pp = pp_clone(e_pp1); - auto g = bind combine_pp(e_pp, num_local_vars, _, _); - set_pre_and_post(a, _vec.foldl[pre_and_post, pre_and_post] - (g, e_pp, alt_pps)); + 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, 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(fm, enclosing, *operator); @@ -1271,6 +1311,10 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () { find_pre_post_stmt(fm, i, *s); + log("pre_post for stmt:"); + log_stmt(*s); + log("is:"); + log_pp(stmt_pp(*s)); } auto do_one = bind do_one_(fm, enclosing, _); @@ -1294,7 +1338,8 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) 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(nv, pps); + + auto block_precond = seq_preconds(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 @@ -1305,6 +1350,7 @@ fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b) 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)); } @@ -1661,6 +1707,13 @@ fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing, changed = extend_poststate_ann(a, poststate_res) || changed; } } + log("if:"); + log_expr(*e); + log("new prestate:"); + log_bitv(enclosing, pres); + log("new poststate:"); + log_bitv(enclosing, expr_poststate(*e)); + ret changed; } case (expr_binary(?bop, ?l, ?r, ?a)) { @@ -1826,16 +1879,15 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, auto stmt_ann_ = stmt_to_ann(*s); check (!is_none[@ts_ann](stmt_ann_)); auto stmt_ann = *(get[@ts_ann](stmt_ann_)); - /* - log_err("*At beginning: stmt = "); + log("*At beginning: stmt = "); log_stmt(*s); - log_err("*prestate = "); - log_err(bitv.to_str(stmt_ann.states.prestate)); - log_err("*poststate ="); - log_err(bitv.to_str(stmt_ann.states.poststate)); - log_err("*changed ="); + log("*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) { @@ -1850,17 +1902,16 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, expr_poststate(*an_init.expr)) || changed; changed = gen_poststate(enclosing, a, alocal.id) || changed; - /* - log_err("Summary: stmt = "); + log("Summary: stmt = "); log_stmt(*s); - log_err("prestate = "); - log_err(bitv.to_str(stmt_ann.states.prestate)); + log("prestate = "); + log(bitv.to_str(stmt_ann.states.prestate)); log_bitv(enclosing, stmt_ann.states.prestate); - log_err("poststate ="); + log("poststate ="); log_bitv(enclosing, stmt_ann.states.poststate); - log_err("changed ="); - log_err(changed); - */ + log("changed ="); + log(changed); + ret changed; } case (none[ast.initializer]) { @@ -1888,16 +1939,17 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, changed = extend_poststate(stmt_ann.states.poststate, expr_poststate(*e)) || changed; - /* log_err("Summary: stmt = "); + log("Summary: stmt = "); log_stmt(*s); - log_err("prestate = "); - log_err(bitv.to_str(stmt_ann.states.prestate)); + log("prestate = "); + log(bitv.to_str(stmt_ann.states.prestate)); log_bitv(enclosing, stmt_ann.states.prestate); - log_err("poststate ="); + log("poststate ="); + log(bitv.to_str(stmt_ann.states.poststate)); log_bitv(enclosing, stmt_ann.states.poststate); - log_err("changed ="); - log_err(changed); - */ + log("changed ="); + log(changed); + ret changed; } case (_) { ret false; } @@ -1909,9 +1961,7 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing, &prestate pres0, &block b) -> bool { - - /* FIXME handle non-local exits */ - + auto changed = false; auto num_local_vars = num_locals(enclosing); @@ -1952,16 +2002,16 @@ fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing, set_prestate_ann(@b.node.a, pres0); set_poststate_ann(b.node.a, post); - /* - log_err("For block:"); + + log("For block:"); log_block(b); - log_err("poststate = "); + log("poststate = "); log_states(block_states(b)); - log_err("pres0:"); + log("pres0:"); log_bitv(enclosing, pres0); - log_err("post:"); + log("post:"); log_bitv(enclosing, post); - */ + ret changed; } diff --git a/src/test/run-pass/alt-join.rs b/src/test/run-pass/alt-join.rs new file mode 100644 index 0000000000000..152fac5d7bc17 --- /dev/null +++ b/src/test/run-pass/alt-join.rs @@ -0,0 +1,34 @@ +use std; +import std.option; +import std.option.t; +import std.option.none; +import std.option.some; + +fn foo[T](&option.t[T] y) { + let int x; + + let vec[int] res = vec(); + + /* tests that x doesn't get put in the precondition for the + entire if expression */ + if (true) { + } + else { + alt (y) { + case (none[T]) { + x = 17; + } + case (_) { + x = 42; + } + } + res += vec(x); + } + + ret; +} + +fn main() { + log("hello"); + foo[int](some[int](5)); +} \ No newline at end of file From c2dc536c3e8bd57f987addff3d23377f76a4bd81 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 14:40:07 -0700 Subject: [PATCH 05/11] Fix nested patterns in rustboot The code for taking pattern-bound variables was being interspersed with pattern code, so that if a nested pattern failed partway through, a variable would be taken but never dropped (because the drop code is inside the block representing the action for the pattern). For example, in the pattern foo(?i, bar(some[t](_)), _), if the scrutinee was foo(x, bar(none[t]), y), the variable i would be taken but never dropped. The patch fixes this bug. --- src/boot/me/trans.ml | 50 ++++++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 16 deletions(-) diff --git a/src/boot/me/trans.ml b/src/boot/me/trans.ml index 1b3ad5d45440f..d34d19d8dc63d 100644 --- a/src/boot/me/trans.ml +++ b/src/boot/me/trans.ml @@ -4793,18 +4793,28 @@ let trans_visitor let trans_arm arm : quad_idx = let (pat, block) = arm.node in - (* Translates the pattern and returns the addresses of the branch - * instructions that are taken if the match fails. + (* Translates the pattern and returns a pair where the first + component is a list of the addresses of the branch + instructions that are taken if the match fails, + and the second component is a thunk that, when invoked, + emits initialization code for the variables bound in this pattern. + + trans_pat can't just emit the initialization code itself, because + then, pattern-bound variables could be taken without ever being + dropped if a nested pattern fails partway through (because the + drop code is part of the action for the pattern). *) let rec trans_pat (pat:Ast.pat) (src_cell:Il.cell) (src_ty:Ast.ty) - : quad_idx list = + : (quad_idx list * + (unit -> unit)) = match pat with Ast.PAT_lit lit -> - trans_compare_simple Il.JNE (trans_lit lit) (Il.Cell src_cell) + (trans_compare_simple Il.JNE (trans_lit lit) (Il.Cell src_cell), + fun _ -> ()) | Ast.PAT_tag (lval, pats) -> let tag_ident = @@ -4815,7 +4825,7 @@ let trans_visitor | Ast.LVAL_base { node = Ast.BASE_app (id, _); id = _ } -> id | _ -> bug cx "expected lval ending in ident" - in + in let ttag = match strip_mutable_or_constrained_ty src_ty with Ast.TY_tag ttag -> ttag @@ -4843,7 +4853,8 @@ let trans_visitor let tup_cell:Il.cell = get_variant_ptr union_cell i in - let trans_elem_pat i elem_pat : quad_idx list = + let trans_elem_pat i elem_pat : + (quad_idx list * (unit -> unit)) = let elem_cell = get_element_ptr_dyn_in_current_frame tup_cell i in @@ -4852,24 +4863,31 @@ let trans_visitor in let elem_jumps = - List.concat (Array.to_list (Array.mapi trans_elem_pat pats)) + (Array.to_list (Array.mapi trans_elem_pat pats)) in + let (elem_jump_addrs, ks) = List.split elem_jumps in - next_jumps @ elem_jumps + (next_jumps @ (List.concat elem_jump_addrs), + (* Compose all the var-initialization thunks together + to make one thunk that initializes all the vars *) + List.fold_left (fun g f -> (fun x -> f (g x))) + (fun _ -> ()) ks) | Ast.PAT_slot (dst, _) -> let dst_slot = get_slot cx dst.id in let dst_cell = cell_of_block_slot dst.id in - trans_init_slot_from_cell - (get_ty_params_of_current_frame()) - CLONE_none dst_cell dst_slot - src_cell src_ty; - [] (* irrefutable *) - - | Ast.PAT_wild -> [] (* irrefutable *) + (* irrefutable *) + ([], (fun () -> (* init the slot later, inside the block, + once we know we had a match *) + trans_init_slot_from_cell + (get_ty_params_of_current_frame()) + CLONE_none dst_cell dst_slot + src_cell src_ty)) + | Ast.PAT_wild -> ([], fun _ -> ()) (* irrefutable *) in let (lval_cell, lval_ty) = trans_lval at.Ast.alt_tag_lval in - let next_jumps = trans_pat pat lval_cell lval_ty in + let (next_jumps, prologue) = trans_pat pat lval_cell lval_ty in + prologue (); (* binds any pattern-bound variables *) trans_block block; let last_jump = mark() in emit (Il.jmp Il.JMP Il.CodeNone); From 8ce7228eae4dcbd3a0052ffa71829bc766611f12 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 14:41:54 -0700 Subject: [PATCH 06/11] Slightly more helpful error message for "null lib handle" I changed the error message to also suggest checking the -L flag when this happens. --- src/rt/rust_crate_cache.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/rt/rust_crate_cache.cpp b/src/rt/rust_crate_cache.cpp index 3fdb33b9896b2..3ab4a822e2ea8 100644 --- a/src/rt/rust_crate_cache.cpp +++ b/src/rt/rust_crate_cache.cpp @@ -49,7 +49,8 @@ rust_crate_cache::c_sym::c_sym(rust_dom *dom, lib *library, char const *name) DLOG(dom, cache, "resolved symbol '%s' to 0x%" PRIxPTR, name, val); } else { - DLOG_ERR(dom, cache, "unresolved symbol '%s', null lib handle", name); + DLOG_ERR(dom, cache, "unresolved symbol '%s', null lib handle\n" + "(did you omit a -L flag?)", name); } } From 8b336fd2eded9bfbae5495a3fb395296fd574299 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 14:55:55 -0700 Subject: [PATCH 07/11] Fix some nested patterns in rustc In rustc, nested patterns were potentially matching when they shouldn't match, because a loop index wasn't being incremented. Fixed it and added one test case. --- src/comp/middle/trans.rs | 2 ++ src/test/run-pass/nested-pattern.rs | 29 +++++++++++++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 src/test/run-pass/nested-pattern.rs diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs index 3e316ab4a244f..776ef53531cd4 100644 --- a/src/comp/middle/trans.rs +++ b/src/comp/middle/trans.rs @@ -3772,6 +3772,8 @@ fn trans_pat_match(@block_ctxt cx, @ast.pat pat, ValueRef llval, auto subpat_res = trans_pat_match(matched_cx, subpat, llsubval, next_cx); matched_cx = subpat_res.bcx; + + i += 1; } } diff --git a/src/test/run-pass/nested-pattern.rs b/src/test/run-pass/nested-pattern.rs new file mode 100644 index 0000000000000..e59c2dd5a4160 --- /dev/null +++ b/src/test/run-pass/nested-pattern.rs @@ -0,0 +1,29 @@ +// a bug was causing this to complain about leaked memory on exit + +use std; +import std.option; +import std.option.some; +import std.option.none; + +tag t { + foo(int, uint); + bar(int, option.t[int]); +} + +fn nested(t o) { + + alt (o) { + case (bar(?i, some[int](_))) { + log_err "wrong pattern matched"; + fail; + } + case (_) { + log_err "succeeded"; + } + } + +} + +fn main() { + nested (bar (1, none[int])); +} \ No newline at end of file From 78ef522565544badd93c1131882e1d39d5417a87 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 15:39:01 -0700 Subject: [PATCH 08/11] Reindented things and removed superfluous comments, nothing to see here --- src/comp/middle/typestate_check.rs | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 2bbcc3e722520..d08ae82d603d7 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -367,8 +367,6 @@ fn mk_fn_info_item_obj(&fn_info_map fi, &span sp, ident i, &ast._obj o, auto all_methods = _vec.clone[@method](o.methods); plus_option[@method](all_methods, o.dtor); for (@method m in all_methods) { - /* FIXME: also need to pass in fields so we can say - they're initialized? */ fi.insert(m.node.id, mk_fn_info(m.node.meth)); log(m.node.ident + " has " + uistr(num_locals(mk_fn_info(m.node.meth))) + " local vars"); @@ -1938,7 +1936,7 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, || changed; changed = extend_poststate(stmt_ann.states.poststate, expr_poststate(*e)) || changed; - + /* log("Summary: stmt = "); log_stmt(*s); log("prestate = "); @@ -1949,7 +1947,7 @@ fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing, log_bitv(enclosing, stmt_ann.states.poststate); log("changed ="); log(changed); - + */ ret changed; } case (_) { ret false; } @@ -2105,12 +2103,12 @@ fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () { fn check_fn_states(&fn_info_map f_info_map, &fn_info f_info, &ast._fn f) -> () { /* Compute the pre- and post-states for this function */ - auto g = find_pre_post_state_fn; - fixed_point_states(f_info_map, f_info, g, f); - + auto g = find_pre_post_state_fn; + fixed_point_states(f_info_map, f_info, g, f); + /* Now compare each expr's pre-state to its precondition and post-state to its postcondition */ - check_states_against_conditions(f_info, f); + check_states_against_conditions(f_info, f); } fn check_item_fn_state(&fn_info_map f_info_map, &span sp, ident i, @@ -2598,13 +2596,8 @@ fn check_crate(@ast.crate crate) -> @ast.crate { auto fm = mk_f_to_fn_info(crate); /* Add a blank ts_ann to every statement (and expression) */ - /* - auto fld0 = fold.new_identity_fold[fn_info_map](); - fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_) - with *fld0); - */ auto with_anns = annotate_crate(fm, crate); - + /* Compute the pre and postcondition for every subexpression */ auto fld = fold.new_identity_fold[fn_info_map](); fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld); From 39c6ddd44d179eb11323418e47fc0eec434f55af Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 11:23:49 -0700 Subject: [PATCH 09/11] Add a session field to ty_ctxt and change an err to span_err I changed instantiate to print out a more helpful error message, which required passing it a session argument. To avoid threading extra arguments through a lot of functions, I added a session field to ty_ctxt. --- src/comp/driver/rustc.rs | 4 ++-- src/comp/middle/ty.rs | 4 ++-- src/comp/middle/typeck.rs | 22 ++++++++++++++-------- 3 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs index c321b3a09738a..584d81ad7f235 100644 --- a/src/comp/driver/rustc.rs +++ b/src/comp/driver/rustc.rs @@ -80,8 +80,8 @@ fn compile_input(session.session sess, crate = resolve.resolve_crate(sess, crate); capture.check_for_captures(sess, crate); - auto ty_cx = ty.mk_ctxt(); - auto typeck_result = typeck.check_crate(sess, ty_cx, crate); + auto ty_cx = ty.mk_ctxt(sess); + auto typeck_result = typeck.check_crate(ty_cx, crate); crate = typeck_result._0; auto type_cache = typeck_result._1; // FIXME: uncomment once typestate_check works diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs index f5cea365d9232..47442f2b8035f 100644 --- a/src/comp/middle/ty.rs +++ b/src/comp/middle/ty.rs @@ -46,7 +46,7 @@ type mt = rec(t ty, ast.mutability mut); // Contains information needed to resolve types and (in the future) look up // the types of AST nodes. -type ctxt = rec(@type_store ts); +type ctxt = rec(@type_store ts, session.session sess); type ty_ctxt = ctxt; // Needed for disambiguation from Unify.ctxt. // Convert from method type to function type. Pretty easy; we just drop @@ -200,7 +200,7 @@ fn mk_type_store() -> @type_store { others=map.mk_hashmap[t,t](hasher, eqer)); } -fn mk_ctxt() -> ctxt { ret rec(ts=mk_type_store()); } +fn mk_ctxt(session.session s) -> ctxt { ret rec(ts=mk_type_store(), sess=s); } // Type constructors diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 0f96c3eb6b767..3354fe46ad963 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -106,7 +106,7 @@ fn substitute_ty_params(&@crate_ctxt ccx, // Returns the type parameter count and the type for the given definition. -fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.def defn) +fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.span sp, &ast.def defn) -> ty_param_count_and_ty { alt (defn) { case (ast.def_arg(?id)) { @@ -157,7 +157,7 @@ fn ty_param_count_and_ty_for_def(@fn_ctxt fcx, &ast.def defn) } case (ast.def_ty(_)) { - fcx.ccx.sess.err("expected value but found type"); + fcx.ccx.sess.span_err(sp, "expected value but found type"); fail; } @@ -308,7 +308,10 @@ fn ast_ty_to_ty(ty.ctxt tcx, ty_getter getter, &@ast.ty ast_ty) -> ty.t { typ = instantiate(tcx, getter, id, path.node.types); } case (ast.def_ty_arg(?id)) { typ = ty.mk_param(tcx, id); } - case (_) { fail; } + case (_) { + tcx.sess.span_err(ast_ty.span, + "found type name used as a variable"); + fail; } } cname = some(path_to_str(path)); @@ -1839,7 +1842,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { check (defopt != none[ast.def]); auto defn = option.get[ast.def](defopt); - auto tpt = ty_param_count_and_ty_for_def(fcx, defn); + auto tpt = ty_param_count_and_ty_for_def(fcx, expr.span, defn); if (ty.def_has_ty_params(defn)) { auto ann = instantiate_path(fcx, pth, tpt, expr.span); @@ -2623,13 +2626,15 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt { case (ast.decl_local(_)) { auto decl_1 = check_decl_local(fcx, decl); ret @fold.respan[ast.stmt_](stmt.span, - ast.stmt_decl(decl_1, plain_ann(fcx.ccx.tystore))); + ast.stmt_decl(decl_1, + plain_ann(fcx.ccx.tcx))); } case (ast.decl_item(_)) { // Ignore for now. We'll return later. ret @fold.respan[ast.stmt_](stmt.span, - ast.stmt_decl(decl, plain_ann(fcx.ccx.tystore))); + ast.stmt_decl(decl, + plain_ann(fcx.ccx.tcx))); } } @@ -2641,7 +2646,7 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt { expr_t = Pushdown.pushdown_expr(fcx, expr_ty(fcx.ccx.tcx, expr_t), expr_t); ret @fold.respan[ast.stmt_](stmt.span, - ast.stmt_expr(expr_t, plain_ann(fcx.ccx.tystore))); + ast.stmt_expr(expr_t, plain_ann(fcx.ccx.tcx))); } } @@ -2790,8 +2795,9 @@ fn eq_unify_cache_entry(&unify_cache_entry a, &unify_cache_entry b) -> bool { type typecheck_result = tup(@ast.crate, ty.type_cache); -fn check_crate(session.session sess, ty.ctxt tcx, @ast.crate crate) +fn check_crate(ty.ctxt tcx, @ast.crate crate) -> typecheck_result { + auto sess = tcx.sess; auto result = Collect.collect_item_types(sess, tcx, crate); let vec[ast.obj_field] fields = vec(); From e2bd0ab064342a65ff15ab61639a25948ee8cfc4 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 15:41:53 -0700 Subject: [PATCH 10/11] Enable typestate_check Enable typestate checking (just for uninitialized vars) and un-XFAIL the relevant tests for stage0. --- src/test/compile-fail/break-uninit.rs | 1 - src/test/compile-fail/break-uninit2.rs | 1 - src/test/compile-fail/fru-typestate.rs | 1 - src/test/compile-fail/return-uninit.rs | 1 - src/test/compile-fail/use-uninit-2.rs | 1 - src/test/compile-fail/use-uninit-3.rs | 1 - src/test/compile-fail/use-uninit-dtor.rs | 1 - src/test/compile-fail/use-uninit.rs | 1 - src/test/compile-fail/while-bypass.rs | 1 - src/test/compile-fail/while-expr.rs | 1 - src/test/compile-fail/writing-through-uninit-vec.rs | 1 - 11 files changed, 11 deletions(-) diff --git a/src/test/compile-fail/break-uninit.rs b/src/test/compile-fail/break-uninit.rs index e9085dd25e823..097312b2b6408 100644 --- a/src/test/compile-fail/break-uninit.rs +++ b/src/test/compile-fail/break-uninit.rs @@ -1,5 +1,4 @@ // xfail-boot -// xfail-stage0 // error-pattern:Unsatisfied precondition fn foo() -> int { diff --git a/src/test/compile-fail/break-uninit2.rs b/src/test/compile-fail/break-uninit2.rs index 8ef83f08cf5ec..45d758f61943d 100644 --- a/src/test/compile-fail/break-uninit2.rs +++ b/src/test/compile-fail/break-uninit2.rs @@ -1,5 +1,4 @@ // xfail-boot -// xfail-stage0 // error-pattern:Unsatisfied precondition fn foo() -> int { diff --git a/src/test/compile-fail/fru-typestate.rs b/src/test/compile-fail/fru-typestate.rs index 74fcdb265205d..86c68e5b9056d 100644 --- a/src/test/compile-fail/fru-typestate.rs +++ b/src/test/compile-fail/fru-typestate.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // -*- rust -*- // error-pattern: precondition diff --git a/src/test/compile-fail/return-uninit.rs b/src/test/compile-fail/return-uninit.rs index 047db518fab43..3711716927a39 100644 --- a/src/test/compile-fail/return-uninit.rs +++ b/src/test/compile-fail/return-uninit.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern: precondition constraint fn f() -> int { diff --git a/src/test/compile-fail/use-uninit-2.rs b/src/test/compile-fail/use-uninit-2.rs index c77676b80999f..79cebe2811f87 100644 --- a/src/test/compile-fail/use-uninit-2.rs +++ b/src/test/compile-fail/use-uninit-2.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern:Unsatisfied precondition fn foo(int x) { diff --git a/src/test/compile-fail/use-uninit-3.rs b/src/test/compile-fail/use-uninit-3.rs index 5dd3926ba0dfc..e65454518a328 100644 --- a/src/test/compile-fail/use-uninit-3.rs +++ b/src/test/compile-fail/use-uninit-3.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern:Unsatisfied precondition fn foo(int x) { diff --git a/src/test/compile-fail/use-uninit-dtor.rs b/src/test/compile-fail/use-uninit-dtor.rs index be2f1727a6ffc..fed90df61f696 100644 --- a/src/test/compile-fail/use-uninit-dtor.rs +++ b/src/test/compile-fail/use-uninit-dtor.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern:Unsatisfied precondition fn main() { diff --git a/src/test/compile-fail/use-uninit.rs b/src/test/compile-fail/use-uninit.rs index bd2e9f416a2ee..03dafdcc00384 100644 --- a/src/test/compile-fail/use-uninit.rs +++ b/src/test/compile-fail/use-uninit.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern:Unsatisfied precondition fn foo(int x) { diff --git a/src/test/compile-fail/while-bypass.rs b/src/test/compile-fail/while-bypass.rs index b49152b3e98cb..1de89e909dafb 100644 --- a/src/test/compile-fail/while-bypass.rs +++ b/src/test/compile-fail/while-bypass.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern: precondition constraint fn f() -> int { diff --git a/src/test/compile-fail/while-expr.rs b/src/test/compile-fail/while-expr.rs index 295752f8e0299..9077c18fd62f4 100644 --- a/src/test/compile-fail/while-expr.rs +++ b/src/test/compile-fail/while-expr.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern: precondition constraint fn main() { diff --git a/src/test/compile-fail/writing-through-uninit-vec.rs b/src/test/compile-fail/writing-through-uninit-vec.rs index 7757609df7839..55edbf8787515 100644 --- a/src/test/compile-fail/writing-through-uninit-vec.rs +++ b/src/test/compile-fail/writing-through-uninit-vec.rs @@ -1,4 +1,3 @@ -// xfail-stage0 // error-pattern: Unsatisfied precondition constraint fn test() { From 4a200c70cbd7e3ff9131e63a5cf26407d685bfd1 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 27 Apr 2011 19:04:46 -0700 Subject: [PATCH 11/11] Enable typestate_check This was supposed to be in a previous commit. I don't know what happened. --- src/comp/driver/rustc.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs index 584d81ad7f235..99c736025db8e 100644 --- a/src/comp/driver/rustc.rs +++ b/src/comp/driver/rustc.rs @@ -84,8 +84,7 @@ fn compile_input(session.session sess, auto typeck_result = typeck.check_crate(ty_cx, crate); crate = typeck_result._0; auto type_cache = typeck_result._1; - // FIXME: uncomment once typestate_check works - // crate = typestate_check.check_crate(crate); + crate = typestate_check.check_crate(crate); trans.trans_crate(sess, crate, ty_cx, type_cache, output, shared, optimize, verify, save_temps, ot); }