From 85567e24eab3f3ac593401cbb335a04a565d5c7a Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 20 Apr 2011 12:11:01 -0700 Subject: [PATCH 1/7] 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 0d0ca05da4bad..d1edcb3377ee9 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.type_store tystore) -> 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 30df202cdaf328302c849d136d339534f284963b Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Thu, 21 Apr 2011 17:39:04 -0700 Subject: [PATCH 2/7] 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 d1edcb3377ee9..775618cb4bb89 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 4e4debeb470cc60b0120326761e47d46444a856b Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 11:08:47 -0700 Subject: [PATCH 3/7] 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 f86e2c4f95c53..3d1267329b531 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -2620,15 +2620,17 @@ 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)) { @@ -2636,7 +2638,8 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt { expr_t = Pushdown.pushdown_expr(fcx, expr_ty(fcx.ccx.tystore, 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 775618cb4bb89..e78e969ba1311 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 f721849189b3bb412e50fd3a1c0c641aa2a1e082 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 11:23:49 -0700 Subject: [PATCH 4/7] Change err to span_err for "expected value but found type" error --- src/comp/middle/typeck.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 3d1267329b531..5b6b3b69ee98e 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -102,7 +102,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)) { @@ -153,7 +153,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; } @@ -1827,7 +1827,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); From 5377fd7c584674f410a5871dcc84ff622027f962 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 14:23:54 -0700 Subject: [PATCH 5/7] 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 3772d370cb443e300d5fee5a8d8f8a461d6d10a8 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 16:38:05 -0700 Subject: [PATCH 6/7] Make typeck.ast_ty_to_ty print out an error message instead of just failing This necessitated adding a session argument to ast_ty_to_ty and its subsidiaries. --- src/comp/middle/typeck.rs | 69 +++++++++++++++++++++++---------------- 1 file changed, 41 insertions(+), 28 deletions(-) diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 5b6b3b69ee98e..0ae626e8d91a2 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -205,23 +205,28 @@ fn instantiate_path(@fn_ctxt fcx, &ast.path pth, &ty_param_count_and_ty tpt, // Parses the programmer's textual representation of a type into our internal // notion of a type. `getter` is a function that returns the type // corresponding to a definition ID. -fn ast_ty_to_ty(@ty.type_store tystore, +fn ast_ty_to_ty(session.session sess, + @ty.type_store tystore, ty_getter getter, &@ast.ty ast_ty) -> ty.t { - fn ast_arg_to_arg(@ty.type_store tystore, + fn ast_arg_to_arg(session.session sess, + @ty.type_store tystore, ty_getter getter, &rec(ast.mode mode, @ast.ty ty) arg) -> rec(ast.mode mode, ty.t ty) { - ret rec(mode=arg.mode, ty=ast_ty_to_ty(tystore, getter, arg.ty)); + ret rec(mode=arg.mode, ty=ast_ty_to_ty(sess, tystore, + getter, arg.ty)); } - fn ast_mt_to_mt(@ty.type_store tystore, + fn ast_mt_to_mt(session.session sess, + @ty.type_store tystore, ty_getter getter, &ast.mt mt) -> ty.mt { - ret rec(ty=ast_ty_to_ty(tystore, getter, mt.ty), mut=mt.mut); + ret rec(ty=ast_ty_to_ty(sess, tystore, getter, mt.ty), mut=mt.mut); } - fn instantiate(@ty.type_store tystore, + fn instantiate(session.session sess, + @ty.type_store tystore, ty_getter getter, ast.def_id id, vec[@ast.ty] args) -> ty.t { @@ -240,7 +245,8 @@ fn ast_ty_to_ty(@ty.type_store tystore, auto bound_ty = bind_params_in_type(tystore, params_opt_and_ty._1); let vec[ty.t] param_bindings = vec(); for (@ast.ty ast_ty in args) { - param_bindings += vec(ast_ty_to_ty(tystore, getter, ast_ty)); + param_bindings += vec(ast_ty_to_ty(sess, tystore, + getter, ast_ty)); } ret ty.substitute_type_params(tystore, param_bindings, bound_ty); } @@ -258,40 +264,41 @@ fn ast_ty_to_ty(@ty.type_store tystore, case (ast.ty_char) { typ = ty.mk_char(tystore); } case (ast.ty_str) { typ = ty.mk_str(tystore); } case (ast.ty_box(?mt)) { - typ = ty.mk_box(tystore, ast_mt_to_mt(tystore, getter, mt)); + typ = ty.mk_box(tystore, ast_mt_to_mt(sess, tystore, getter, mt)); } case (ast.ty_vec(?mt)) { - typ = ty.mk_vec(tystore, ast_mt_to_mt(tystore, getter, mt)); + typ = ty.mk_vec(tystore, ast_mt_to_mt(sess, tystore, getter, mt)); } case (ast.ty_port(?t)) { - typ = ty.mk_port(tystore, ast_ty_to_ty(tystore, getter, t)); + typ = ty.mk_port(tystore, ast_ty_to_ty(sess, tystore, getter, t)); } case (ast.ty_chan(?t)) { - typ = ty.mk_chan(tystore, ast_ty_to_ty(tystore, getter, t)); + typ = ty.mk_chan(tystore, ast_ty_to_ty(sess, tystore, getter, t)); } case (ast.ty_tup(?fields)) { let vec[ty.mt] flds = vec(); for (ast.mt field in fields) { - _vec.push[ty.mt](flds, ast_mt_to_mt(tystore, getter, field)); + _vec.push[ty.mt](flds, ast_mt_to_mt(sess, tystore, + getter, field)); } typ = ty.mk_tup(tystore, flds); } case (ast.ty_rec(?fields)) { let vec[field] flds = vec(); for (ast.ty_field f in fields) { - auto tm = ast_mt_to_mt(tystore, getter, f.mt); + auto tm = ast_mt_to_mt(sess, tystore, getter, f.mt); _vec.push[field](flds, rec(ident=f.ident, mt=tm)); } typ = ty.mk_rec(tystore, flds); } case (ast.ty_fn(?proto, ?inputs, ?output)) { - auto f = bind ast_arg_to_arg(tystore, getter, _); + auto f = bind ast_arg_to_arg(sess, tystore, getter, _); auto i = _vec.map[ast.ty_arg, arg](f, inputs); - auto out_ty = ast_ty_to_ty(tystore, getter, output); + auto out_ty = ast_ty_to_ty(sess, tystore, getter, output); typ = ty.mk_fn(tystore, proto, i, out_ty); } @@ -299,14 +306,20 @@ fn ast_ty_to_ty(@ty.type_store tystore, check (def != none[ast.def]); alt (option.get[ast.def](def)) { case (ast.def_ty(?id)) { - typ = instantiate(tystore, getter, id, path.node.types); + typ = instantiate(sess, tystore, getter, + id, path.node.types); } case (ast.def_native_ty(?id)) { typ = getter(id)._1; } case (ast.def_obj(?id)) { - typ = instantiate(tystore, getter, id, path.node.types); + typ = instantiate(sess, tystore, getter, + id, path.node.types); } case (ast.def_ty_arg(?id)) { typ = ty.mk_param(tystore, id); } - case (_) { fail; } + case (_) { + sess.span_err(ast_ty.span, + "found type name used as a variable"); + fail; + } } cname = some(path_to_str(path)); @@ -314,10 +327,10 @@ fn ast_ty_to_ty(@ty.type_store tystore, case (ast.ty_obj(?meths)) { let vec[ty.method] tmeths = vec(); - auto f = bind ast_arg_to_arg(tystore, getter, _); + auto f = bind ast_arg_to_arg(sess, tystore, getter, _); for (ast.ty_method m in meths) { auto ins = _vec.map[ast.ty_arg, arg](f, m.inputs); - auto out = ast_ty_to_ty(tystore, getter, m.output); + auto out = ast_ty_to_ty(sess, tystore, getter, m.output); _vec.push[ty.method](tmeths, rec(proto=m.proto, ident=m.ident, @@ -345,7 +358,7 @@ fn ast_ty_to_ty_crate(@crate_ctxt ccx, &@ast.ty ast_ty) -> ty.t { ret ty.lookup_item_type(ccx.sess, ccx.tystore, ccx.type_cache, id); } auto f = bind getter(ccx, _); - ret ast_ty_to_ty(ccx.tystore, f, ast_ty); + ret ast_ty_to_ty(ccx.sess, ccx.tystore, f, ast_ty); } @@ -422,12 +435,12 @@ mod Collect { fn ty_of_arg(@ctxt cx, &ast.arg a) -> arg { auto f = bind getter(cx, _); - ret rec(mode=a.mode, ty=ast_ty_to_ty(cx.tystore, f, a.ty)); + ret rec(mode=a.mode, ty=ast_ty_to_ty(cx.sess, cx.tystore, f, a.ty)); } fn ty_of_method(@ctxt cx, &@ast.method m) -> method { auto get = bind getter(cx, _); - auto convert = bind ast_ty_to_ty(cx.tystore, get, _); + auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _); auto f = bind ty_of_arg(cx, _); auto inputs = _vec.map[ast.arg,arg](f, m.node.meth.decl.inputs); auto output = convert(m.node.meth.decl.output); @@ -458,7 +471,7 @@ mod Collect { let vec[arg] t_inputs = vec(); for (ast.obj_field f in obj_info.fields) { auto g = bind getter(cx, _); - auto t_field = ast_ty_to_ty(cx.tystore, g, f.ty); + auto t_field = ast_ty_to_ty(cx.sess, cx.tystore, g, f.ty); _vec.push[arg](t_inputs, rec(mode=ast.alias, ty=t_field)); } @@ -471,7 +484,7 @@ mod Collect { fn ty_of_item(@ctxt cx, @ast.item it) -> ty.ty_param_count_and_ty { auto get = bind getter(cx, _); - auto convert = bind ast_ty_to_ty(cx.tystore, get, _); + auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _); alt (it.node) { @@ -537,7 +550,7 @@ mod Collect { case (ast.native_item_fn(?ident, ?lname, ?fn_decl, ?params, ?def_id, _)) { auto get = bind getter(cx, _); - auto convert = bind ast_ty_to_ty(cx.tystore, get, _); + auto convert = bind ast_ty_to_ty(cx.sess, cx.tystore, get, _); auto f = bind ty_of_arg(cx, _); ret ty_of_native_fn_decl(cx, convert, f, fn_decl, abi, params, def_id); @@ -585,7 +598,7 @@ mod Collect { let vec[arg] args = vec(); for (ast.variant_arg va in variant.node.args) { - auto arg_ty = ast_ty_to_ty(cx.tystore, f, va.ty); + auto arg_ty = ast_ty_to_ty(cx.sess, cx.tystore, f, va.ty); args += vec(rec(mode=ast.alias, ty=arg_ty)); } auto tag_t = ty.mk_tag(cx.tystore, tag_id, ty_param_tys); @@ -735,7 +748,7 @@ mod Collect { } auto g = bind getter(e.cx, _); for (ast.obj_field fld in ob.fields) { - let ty.t fty = ast_ty_to_ty(e.cx.tystore, g, fld.ty); + let ty.t fty = ast_ty_to_ty(e.cx.sess, e.cx.tystore, g, fld.ty); let ast.obj_field f = rec(ann=triv_ann(fty) with fld ); From d908ec567e19e4e8dc5cdb121288e21623342115 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 22 Apr 2011 17:19:49 -0700 Subject: [PATCH 7/7] Make rustc's typestate pass happy by adding a fail in a case that should be unreachable, preventing a variable from being seen as possibly uninitialized. --- src/comp/middle/trans.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs index cf16d31728332..997e41e0cb963 100644 --- a/src/comp/middle/trans.rs +++ b/src/comp/middle/trans.rs @@ -1953,6 +1953,13 @@ fn make_drop_glue(@block_ctxt cx, ValueRef v0, ty.t t) { ty.type_is_nil(cx.fcx.lcx.ccx.tystore, t)) { rslt = res(cx, C_nil()); } + else { + // task, native_fn, var, local, param, bound_param + cx.fcx.lcx.ccx.sess.bug + ("unexpected type in trans.make_drop_glue: " + + ty.ty_to_str(cx.fcx.lcx.ccx.tystore, t)); + fail; + } } }