From 3f3c9caf4d2c434982d840e65c4014c1787f8d47 Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Tue, 29 May 2012 18:22:38 -0700
Subject: [PATCH] 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
---
src/rustc/middle/tstate/states.rs | 16 ++++++++++------
src/rustc/middle/tstate/tritv.rs | 18 ------------------
src/test/compile-fail/loop-pred-constraints.rs | 1 -
3 files changed, 10 insertions(+), 25 deletions(-)
diff --git a/src/rustc/middle/tstate/states.rs b/src/rustc/middle/tstate/states.rs
index c6f927e6efa..eaf4be1955c 100644
--- a/src/rustc/middle/tstate/states.rs
+++ b/src/rustc/middle/tstate/states.rs
@@ -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));
diff --git a/src/rustc/middle/tstate/tritv.rs b/src/rustc/middle/tstate/tritv.rs
index e6f68f7edb3..05fcbca9633 100644
--- a/src/rustc/middle/tstate/tritv.rs
+++ b/src/rustc/middle/tstate/tritv.rs
@@ -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 {
diff --git a/src/test/compile-fail/loop-pred-constraints.rs b/src/test/compile-fail/loop-pred-constraints.rs
index b085de80a23..a55fe477ba7 100644
--- a/src/test/compile-fail/loop-pred-constraints.rs
+++ b/src/test/compile-fail/loop-pred-constraints.rs
@@ -1,4 +1,3 @@
-// xfail-test
// https://github.com/mozilla/rust/issues/2374
// error-pattern:unsatisfied precondition constraint (for example, even(y