From 1c786bcc82424b9218f1ca52fa99a12ce353e590 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 5 Aug 2011 15:23:44 -0700 Subject: [PATCH] Initialize all constraints to False Previously, typestate was initializing the init constraint for a declared-but-not-initialized variable (like x in "let x;") to False, but other constraints to Don't-know. This led to over-lenient results when a variable was used before declaration (see the included test case). Now, everything gets initialized to False in the prestate/poststate- finding phase, and Don't-know should only be used in pre/postconditions. This aspect of the algorithm really needs formalization (just on paper), but for now, this closes #700 --- src/comp/middle/tstate/bitvectors.rs | 5 +++++ src/comp/middle/tstate/states.rs | 22 +++++++++++++--------- src/comp/middle/tstate/tritv.rs | 6 ++++++ src/test/compile-fail/alt-join.rs | 17 +++++++++++++++++ 4 files changed, 41 insertions(+), 9 deletions(-) create mode 100644 src/test/compile-fail/alt-join.rs diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index 7efa499b205f..a055187e2867 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -183,6 +183,11 @@ fn kill_prestate(fcx: &fn_ctxt, id: node_id, c: &tsconstr) -> bool { node_id_to_ts_ann(fcx.ccx, id).states); } +fn kill_all_prestate(fcx: &fn_ctxt, id: node_id) { + tritv::tritv_kill(node_id_to_ts_ann(fcx.ccx, id).states.prestate); +} + + fn kill_poststate(fcx: &fn_ctxt, id: node_id, c: &tsconstr) -> bool { log "kill_poststate"; ret clear_in_poststate(bit_num(fcx, c), diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index a78522fcf3de..0f7d920e6ce9 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -594,6 +594,7 @@ fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt) -> bool { let stmt_ann = stmt_to_ann(fcx.ccx, *s); /* + log_err ("[" + fcx.name + "]"); log_err "*At beginning: stmt = "; log_stmt_err(*s); log_err "*prestate = "; @@ -617,7 +618,8 @@ fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt) let changed = (set_poststate(stmt_ann, c_and_p.post) | c_and_p.changed); - /* + +/* log_err "Summary: stmt = "; log_stmt_err(*s); log_err "prestate = "; @@ -638,11 +640,12 @@ fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt) } } stmt_expr(ex, _) { - ret find_pre_post_state_expr(fcx, pres, ex) | + let changed = find_pre_post_state_expr(fcx, pres, ex) | set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) | set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex)); - /* - log_err "Finally:"; + +/* + log_err "Finally:"; log_stmt_err(*s); log_err("prestate = "); // log_err(bitv::to_str(stmt_ann.states.prestate)); @@ -651,8 +654,9 @@ fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt) // log_err(bitv::to_str(stmt_ann.states.poststate)); log_tritv_err(fcx, stmt_ann.states.poststate); log_err("changed ="); - log_err(changed); - */ +*/ + + ret changed; } _ { ret false; } } @@ -707,9 +711,9 @@ fn find_pre_post_state_block(fcx: &fn_ctxt, pres0: &prestate, b: &blk) -> fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool { let num_constrs = num_constraints(fcx.enclosing); - // make sure the return and diverge bits start out False - kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_return); - kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_diverge); + // All constraints are considered false until proven otherwise. + // This ensures that intersect works correctly. + kill_all_prestate(fcx, f.body.node.id); // Instantiate any constraints on the arguments so we can use them let block_pre = block_prestate(fcx.ccx, f.body); diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs index 7615b84aea8d..1d33292c9a9f 100644 --- a/src/comp/middle/tstate/tritv.rs +++ b/src/comp/middle/tstate/tritv.rs @@ -16,6 +16,7 @@ export tritv_union; export tritv_intersect; export tritv_copy; export tritv_clear; +export tritv_kill; export tritv_doesntcare; export to_str; @@ -218,6 +219,11 @@ fn tritv_clear(v: &t) { while i < v.nbits { tritv_set(i, v, dont_care); i += 1u; } } +fn tritv_kill(v: &t) { + let i: uint = 0u; + while i < v.nbits { tritv_set(i, v, tfalse); i += 1u; } +} + fn tritv_clone(v: &t) -> t { ret {uncertain: bitv::clone(v.uncertain), val: bitv::clone(v.val), diff --git a/src/test/compile-fail/alt-join.rs b/src/test/compile-fail/alt-join.rs new file mode 100644 index 000000000000..bbd4ac5c73aa --- /dev/null +++ b/src/test/compile-fail/alt-join.rs @@ -0,0 +1,17 @@ +// error-pattern:Unsatisfied precondition constraint +// a good test that we merge paths correctly in the presence of a +// variable that's used before it's declared +// should be rejected by typestate because we use x without initializing it + +fn my_fail() -> ! { fail; } + +fn main() { + + alt (true) { + false { my_fail(); } + true {} + } + + log x; + let x:int; +} \ No newline at end of file