diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/comp/middle/typestate_check.rs | 210 | ||||
| -rw-r--r-- | src/comp/util/common.rs | 32 | ||||
| -rw-r--r-- | src/test/compile-fail/break-uninit.rs | 22 | ||||
| -rw-r--r-- | src/test/compile-fail/break-uninit2.rs | 22 |
4 files changed, 274 insertions, 12 deletions
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 04aeebdf..69352177 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 d2ed72a0..fd0d688b 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 00000000..e9085dd2 --- /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 00000000..8ef83f08 --- /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()); +} |