diff options
Diffstat (limited to 'src/comp')
| -rw-r--r-- | src/comp/middle/tstate/ann.rs | 19 | ||||
| -rw-r--r-- | src/comp/middle/tstate/bitvectors.rs | 36 | ||||
| -rw-r--r-- | src/comp/middle/tstate/ck.rs | 8 | ||||
| -rw-r--r-- | src/comp/middle/tstate/pre_post_conditions.rs | 17 | ||||
| -rw-r--r-- | src/comp/middle/tstate/states.rs | 138 | ||||
| -rw-r--r-- | src/comp/middle/tstate/tritv.rs | 28 |
6 files changed, 150 insertions, 96 deletions
diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs index d8aae77e621..882dc4a42f7 100644 --- a/src/comp/middle/tstate/ann.rs +++ b/src/comp/middle/tstate/ann.rs @@ -112,7 +112,7 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool { // sets the ith bit in p's post auto was_set = tritv_get(p.postcondition, i); tritv_set(i, p.postcondition, ttrue); - ret was_set == dont_care; + ret was_set != ttrue; } fn set_in_poststate(uint i, &pre_and_post_state s) -> bool { @@ -123,7 +123,7 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool { fn set_in_poststate_(uint i, &poststate p) -> bool { auto was_set = tritv_get(p, i); tritv_set(i, p, ttrue); - ret was_set == dont_care; + ret was_set != ttrue; } @@ -135,14 +135,25 @@ fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool { fn clear_in_poststate_(uint i, &poststate s) -> bool { auto was_set = tritv_get(s, i); tritv_set(i, s, tfalse); - ret was_set == dont_care; + ret was_set != tfalse; +} + +fn clear_in_prestate(uint i, &pre_and_post_state s) -> bool { + // sets the ith bit in p's pre + ret clear_in_prestate_(i, s.prestate); +} + +fn clear_in_prestate_(uint i, &prestate s) -> bool { + auto was_set = tritv_get(s, i); + tritv_set(i, s, tfalse); + ret was_set != tfalse; } fn clear_in_postcond(uint i, &pre_and_post s) -> bool { // sets the ith bit in p's post auto was_set = tritv_get(s.postcondition, i); tritv_set(i, s.postcondition, tfalse); - ret was_set == dont_care; + ret was_set != tfalse; } // Sets all the bits in a's precondition to equal the diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index 21934ca04b7..c7e77881e85 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -43,6 +43,7 @@ import tstate::ann::set_in_postcond; import tstate::ann::set_in_poststate; import tstate::ann::set_in_poststate_; import tstate::ann::clear_in_poststate; +import tstate::ann::clear_in_prestate; import tstate::ann::clear_in_poststate_; import tritv::*; @@ -147,22 +148,10 @@ fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond { } else { ret true_precond(num_vars); } } -/* Gee, maybe we could use foldl or something */ -fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond { - auto sz = vec::len[postcond](rest); - if (sz > 0u) { - auto other = rest.(0); - intersect(first, other); - intersect_postconds_go(first, - slice[postcond](rest, 1u, - len[postcond](rest))); - } - ret first; -} - -fn intersect_postconds(&vec[postcond] pcs) -> postcond { - assert (len[postcond](pcs) > 0u); - ret intersect_postconds_go(tritv_clone(pcs.(0)), pcs); +fn intersect_states(&prestate p, &prestate q) -> prestate { + auto rslt = tritv_clone(p); + tritv_intersect(rslt, q); + ret rslt; } fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool { @@ -219,6 +208,11 @@ fn gen_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool { node_id_to_ts_ann(fcx.ccx, id).states); } +fn kill_prestate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool { + ret clear_in_prestate(bit_num(fcx, c), + node_id_to_ts_ann(fcx.ccx, id).states); +} + fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool { log "kill_poststate"; ret clear_in_poststate(bit_num(fcx, c), @@ -254,6 +248,16 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident, ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t); } +fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident, + &node_id parent) -> bool { + ret kill_poststate(fcx, parent, rec(id=id, c=ninit(ident))); +} + +fn clear_in_prestate_ident(&fn_ctxt fcx, &node_id id, &ident ident, + &node_id parent) -> bool { + ret kill_prestate(fcx, parent, rec(id=id, c=ninit(ident))); +} + // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs index a65dfbbc8c1..0c13c617c47 100644 --- a/src/comp/middle/tstate/ck.rs +++ b/src/comp/middle/tstate/ck.rs @@ -70,9 +70,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) { log_err("check_states_expr:"); util::common::log_expr_err(*e); log_err("prec = "); - log_bitv_err(fcx, prec); + log_tritv_err(fcx, prec); log_err("pres = "); - log_bitv_err(fcx, pres); + log_tritv_err(fcx, pres); */ if (!implies(pres, prec)) { @@ -99,9 +99,9 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) { log_err("check_states_stmt:"); log_stmt_err(*s); log_err("prec = "); - log_bitv_err(fcx, prec); + log_tritv_err(fcx, prec); log_err("pres = "); - log_bitv_err(fcx, pres); + log_tritv_err(fcx, pres); */ if (!implies(pres, prec)) { diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 672894c0675..d4495fee622 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -59,7 +59,7 @@ import bitvectors::bit_num; import bitvectors::promises; import bitvectors::seq_preconds; import bitvectors::seq_postconds; -import bitvectors::intersect_postconds; +import bitvectors::intersect_states; import bitvectors::declare_var; import bitvectors::gen_poststate; import bitvectors::relax_precond_block; @@ -180,9 +180,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body, seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]); - auto loop_postcond = - intersect_postconds([expr_postcond(fcx.ccx, index), - block_postcond(fcx.ccx, body)]); + auto loop_postcond = intersect_states(expr_postcond(fcx.ccx, index), + block_postcond(fcx.ccx, body)); copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond); } @@ -247,8 +246,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, seq_postconds(fcx, [precond_true_case, precond_false_case]); auto postcond_res = - intersect_postconds([postcond_true_case, - postcond_false_case]); + intersect_states(postcond_true_case, postcond_false_case); set_pre_and_post(fcx.ccx, id, precond_res, postcond_res); } } @@ -459,10 +457,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { seq_preconds(fcx, [expr_pp(fcx.ccx, test), block_pp(fcx.ccx, body)]), - intersect_postconds([expr_postcond(fcx.ccx, - test), - block_postcond(fcx.ccx, - body)])); + intersect_states(expr_postcond(fcx.ccx, test), + block_postcond(fcx.ccx, + body))); } case (expr_do_while(?body, ?test)) { find_pre_post_block(fcx, body); diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 0de5cf33fd4..d5676fad7ef 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -69,10 +69,12 @@ import tritv::ttrue; import bitvectors::set_in_poststate_ident; import bitvectors::clear_in_poststate_expr; -import bitvectors::intersect_postconds; +import bitvectors::clear_in_prestate_ident; import bitvectors::bit_num; import bitvectors::gen_poststate; import bitvectors::kill_poststate; +import bitvectors::clear_in_poststate_ident; +import bitvectors::intersect_states; import front::ast; import front::ast::*; import middle::ty::expr_ty; @@ -188,23 +190,27 @@ fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, ast::node_id id, fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l, &@expr index, &block body, node_id id) -> bool { - /* same issues as while */ + auto loop_pres = intersect_states(pres, + block_poststate(fcx.ccx, body)); - // FIXME: also want to set l as initialized, no? - auto changed = set_prestate_ann(fcx.ccx, id, pres) | + auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) | find_pre_post_state_expr(fcx, pres, index); - /* in general, would need the intersection of - (poststate of index, poststate of body) */ find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body); if (has_nonlocal_exits(body)) { - changed |= set_poststate_ann(fcx.ccx, id, pres); + // See [Break-unsound] + ret (changed | set_poststate_ann(fcx.ccx, id, pres)); } - + else { + auto res_p = intersect_states(expr_poststate(fcx.ccx, index), + block_poststate(fcx.ccx, body)); + /* auto res_p = intersect_postconds([expr_poststate(fcx.ccx, index), - block_poststate(fcx.ccx, body)]); - ret changed | set_poststate_ann(fcx.ccx, id, res_p); + block_poststate(fcx.ccx, body)]); */ + + ret changed | set_poststate_ann(fcx.ccx, id, res_p); + } } fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool { @@ -269,16 +275,18 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, find_pre_post_state_block(fcx, conseq_prestate, conseq); auto poststate_res = - intersect_postconds([block_poststate(fcx.ccx, conseq), - expr_poststate(fcx.ccx, altern)]); - /* fcx.ccx.tcx.sess.span_note(antec.span, - "poststate_res = " + aux::bitv_to_str(fcx, poststate_res)); + intersect_states(block_poststate(fcx.ccx, conseq), + expr_poststate(fcx.ccx, altern)); + /* + fcx.ccx.tcx.sess.span_note(antec.span, + "poststate_res = " + aux::tritv_to_str(fcx, poststate_res)); fcx.ccx.tcx.sess.span_note(antec.span, "altern poststate = " + - aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, altern))); + aux::tritv_to_str(fcx, expr_poststate(fcx.ccx, altern))); fcx.ccx.tcx.sess.span_note(antec.span, - "conseq poststate = " + aux::bitv_to_str(fcx, - block_poststate(fcx.ccx, conseq))); */ + "conseq poststate = " + aux::tritv_to_str(fcx, + block_poststate(fcx.ccx, conseq))); + */ changed |= set_poststate_ann(fcx.ccx, id, poststate_res); } @@ -287,7 +295,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, } fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { - auto num_local_vars = num_constraints(fcx.enclosing); + auto num_constrs = num_constraints(fcx.enclosing); alt (e.node) { case (expr_vec(?elts, _, _)) { @@ -381,7 +389,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { a ret expression (since execution never continues locally after a ret expression */ - set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars)); + set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs)); /* return from an always-failing function clears the return bit */ alt (fcx.enclosing.cf) { @@ -401,7 +409,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { } case (expr_be(?val)) { auto changed = set_prestate_ann(fcx.ccx, e.id, pres); - set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars)); + set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs)); ret changed | find_pre_post_state_expr(fcx, pres, val); } case (expr_if(?antec, ?conseq, ?maybe_alt)) { @@ -423,55 +431,62 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { oper_assign); } case (expr_while(?test, ?body)) { - auto changed = set_prestate_ann(fcx.ccx, e.id, pres) | - /* to handle general predicates, we need to pass in - pres `intersect` (poststate(a)) - like: auto test_pres = intersect_postconds(pres, - expr_postcond(a)); However, this doesn't work right now because - we would be passing in an all-zero prestate initially - FIXME - maybe need a "don't know" state in addition to 0 or 1? + /* + log_err "in a while loop:"; + log_expr_err(*e); + aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body)); + aux::log_tritv_err(fcx, pres); */ - find_pre_post_state_expr(fcx, pres, test) | + auto loop_pres = intersect_states + (block_poststate(fcx.ccx, body), pres); + // aux::log_tritv_err(fcx, loop_pres); + // log_err "---------------"; + + auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres) | + find_pre_post_state_expr(fcx, loop_pres, test) | find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test), body); /* conservative approximation: if a loop contains a break or cont, we assume nothing about the poststate */ + /* which is still unsound -- see [Break-unsound] */ if (has_nonlocal_exits(body)) { - changed |= set_poststate_ann(fcx.ccx, e.id, pres); + ret changed | set_poststate_ann(fcx.ccx, e.id, pres); + } + else { + auto e_post = expr_poststate(fcx.ccx, test); + auto b_post = block_poststate(fcx.ccx, body); + ret changed | set_poststate_ann + (fcx.ccx, e.id, intersect_states(e_post, b_post)); } - - auto e_post = expr_poststate(fcx.ccx, test); - auto b_post = block_poststate(fcx.ccx, body); - ret changed | set_poststate_ann - (fcx.ccx, e.id, intersect_postconds([e_post, b_post])); } case (expr_do_while(?body, ?test)) { - auto changed = set_prestate_ann(fcx.ccx, e.id, pres); - auto changed0 = changed; - changed |= find_pre_post_state_block(fcx, pres, body); + auto loop_pres = intersect_states(expr_poststate(fcx.ccx, test), + pres); + + auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres); + changed |= find_pre_post_state_block(fcx, loop_pres, body); /* 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) */ - auto breaks = has_nonlocal_exits(body); - if (breaks) { - // this should probably be true_poststate and not pres, - // b/c the body could invalidate stuff - // FIXME - // This doesn't set "changed", as if the previous state - // was different, this might come back true every time - set_poststate_ann(fcx.ccx, body.node.id, pres); - changed = changed0; - } - changed |= find_pre_post_state_expr (fcx, block_poststate(fcx.ccx, body), test); + auto breaks = has_nonlocal_exits(body); if (breaks) { - set_poststate_ann(fcx.ccx, e.id, pres); - } + // this should probably be true_poststate and not pres, + // b/c the body could invalidate stuff + // FIXME [Break-unsound] + // This is unsound as it is -- consider + // while (true) { + // x <- y; + // break; + // } + // The poststate wouldn't take into account that + // y gets deinitialized + changed |= set_poststate_ann(fcx.ccx, e.id, pres); + } else { changed |= set_poststate_ann (fcx.ccx, e.id, expr_poststate(fcx.ccx, test)); @@ -493,7 +508,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { auto e_post = expr_poststate(fcx.ccx, val); auto a_post; if (vec::len[arm](alts) > 0u) { - a_post = false_postcond(num_local_vars); + a_post = false_postcond(num_constrs); for (arm an_alt in alts) { changed |= find_pre_post_state_block (fcx, e_post, an_alt.block); @@ -524,7 +539,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { /* if execution continues after fail, then everything is true! woo! */ set_poststate_ann(fcx.ccx, e.id, - false_postcond(num_local_vars)); + false_postcond(num_constrs)); } case (expr_assert(?p)) { ret find_pre_post_state_sub(fcx, pres, p, e.id, none); @@ -604,8 +619,12 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { */ } case (none) { - ret set_prestate(stmt_ann, pres) | - set_poststate(stmt_ann, pres); + // let int = x; => x is uninit in poststate + set_poststate_ann(fcx.ccx, id, pres); + clear_in_poststate_ident(fcx, alocal.node.id, + alocal.node.ident, id); + set_prestate(stmt_ann, pres); + ret false; } } } @@ -683,6 +702,8 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { auto num_local_vars = num_constraints(fcx.enclosing); + // make sure the return bit starts out False + clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id); auto changed = find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body), f.body); @@ -704,6 +725,13 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { } case (none) {/* fallthrough */ } } + +/* + log_err "find_pre_post_state_fn"; + log_err changed; + fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name); +*/ + ret changed; } // diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs index 88bc74772b4..90be1810301 100644 --- a/src/comp/middle/tstate/tritv.rs +++ b/src/comp/middle/tstate/tritv.rs @@ -82,18 +82,32 @@ fn trit_or(trit a, trit b) -> trit { } } +// FIXME: This still seems kind of dodgy to me (that is, +// that 1 + ? = 1. But it might work out given that +// all variables start out in a 0 state. Probably I need +// to make it so that all constraints start out in a 0 state +// (we consider a constraint false until proven true), too. fn trit_and(trit a, trit b) -> trit { alt (a) { - case (dont_care) { dont_care } - case (ttrue) { - alt (b) { - case (dont_care) { dont_care } - case (ttrue) { ttrue } - case (tfalse) { dont_care } // ??? + case (dont_care) { b } // also seems wrong for case b = ttrue + case (ttrue) { + alt (b) { + case (dont_care) { ttrue } // ??? Seems wrong + case (ttrue) { ttrue } + // false wins, since if something is uninit + // on one path, we care + // (Rationale: it's always safe to assume that + // a var is uninitialized or that a constraint + // needs to be re-established) + case (tfalse) { tfalse } + } } - } + // Rationale: if it's uninit on one path, + // we can consider it as uninit on all paths case (tfalse) { tfalse } } + // if the result is dont_care, that means + // a and b were both dont_care } fn change(bool changed, trit old, trit new) -> bool { changed || new != old } |