Handle poststates of breaking loops correctly in typestate

The poststate should be one where all predicates are assumed false,
rather than the unchanged prestate.

Closes #2374
This commit is contained in:
Tim Chevalier 2012-05-29 18:22:38 -07:00
parent b30daa6eef
commit 3f3c9caf4d
3 changed files with 10 additions and 25 deletions

View File

@ -2,6 +2,7 @@ import ann::*;
import aux::*;
import tritv::{tritv_clone, tritv_set, ttrue};
import syntax::print::pprust::block_to_str;
import bitvectors::*;
import pat_util::*;
import syntax::ast::*;
@ -13,9 +14,6 @@ import driver::session::session;
import std::map::hashmap;
fn forbid_upvar(fcx: fn_ctxt, rhs_id: node_id, sp: span, t: oper_type) {
// fcx.ccx.tcx.sess.span_note(sp,
// #fmt("forbid_upvar: checking. %?", t));
alt t {
oper_move {
alt local_node_id_to_def(fcx, rhs_id) {
@ -457,12 +455,18 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
let mut changed = set_prestate_ann(fcx.ccx, e.id, loop_pres)
| find_pre_post_state_block(fcx, loop_pres, body);
/* conservative approximation: if a loop contains a break
or cont, we assume nothing about the poststate */
or cont, we assume nothing about the poststate (so, we
set all predicates to "don't know" */
/* which is still unsound -- see [Break-unsound] */
if may_break(body) {
/* Only do this if there are *breaks* not conts.
An infinite loop with conts is still an infinite loop. */
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
An infinite loop with conts is still an infinite loop.
We assume all preds are FALSE, not '?' -- because in the
worst case, the body could invalidate all preds and
deinitialize everything before breaking */
let post = empty_poststate(num_constrs);
tritv::tritv_kill(post);
ret changed | set_poststate_ann(fcx.ccx, e.id, post);
} else {
ret changed | set_poststate_ann(fcx.ccx, e.id,
false_postcond(num_constrs));

View File

@ -109,27 +109,14 @@ fn trit_or(a: trit, b: trit) -> trit {
fn trit_and(a: trit, b: trit) -> trit {
alt a {
dont_care { b }
// also seems wrong for case b = ttrue
ttrue {
alt b {
dont_care { ttrue }
// ??? Seems wrong
ttrue {
ttrue
}
// false wins, since if something is uninit
// on one path, we care
// (Rationale: it's always safe to assume that
@ -140,11 +127,6 @@ fn trit_and(a: trit, b: trit) -> trit {
}
}
}
// Rationale: if it's uninit on one path,
// we can consider it as uninit on all paths
tfalse {

View File

@ -1,4 +1,3 @@
// xfail-test
// https://github.com/mozilla/rust/issues/2374
// error-pattern:unsatisfied precondition constraint (for example, even(y