about summary refs log tree commit diff
diff options
context:
space:
mode:
-rw-r--r--src/rustc/middle/tstate/auxiliary.rs238
-rw-r--r--src/rustc/middle/tstate/bitvectors.rs63
-rw-r--r--src/rustc/middle/tstate/ck.rs49
-rw-r--r--src/rustc/middle/tstate/collect_locals.rs71
-rw-r--r--src/rustc/middle/tstate/pre_post_conditions.rs68
-rw-r--r--src/rustc/middle/tstate/states.rs92
-rw-r--r--src/test/compile-fail/liveness-unused.rs6
-rw-r--r--src/test/run-pass/liveness-loop-break.rs2
8 files changed, 89 insertions, 500 deletions
diff --git a/src/rustc/middle/tstate/auxiliary.rs b/src/rustc/middle/tstate/auxiliary.rs
index 343fd07a1d5..ecd6b43a7f0 100644
--- a/src/rustc/middle/tstate/auxiliary.rs
+++ b/src/rustc/middle/tstate/auxiliary.rs
@@ -49,18 +49,10 @@ fn comma_str(args: [@constr_arg_use]) -> str {
 }
 
 fn constraint_to_str(tcx: ty::ctxt, c: sp_constr) -> str {
-    alt c.node {
-      ninit(id, i) {
-        ret #fmt("init(%s id=%d - arising from %s)",
-                 i, id, codemap::span_to_str(c.span, tcx.sess.codemap));
-      }
-      npred(p, _, args) {
-          ret #fmt("%s(%s) - arising from %s",
-                   path_to_str(p),
-                   comma_str(args),
-                   codemap::span_to_str(c.span, tcx.sess.codemap));
-      }
-    }
+    ret #fmt("%s(%s) - arising from %s",
+             path_to_str(c.node.path),
+             comma_str(c.node.args),
+             codemap::span_to_str(c.span, tcx.sess.codemap));
 }
 
 fn tritv_to_str(fcx: fn_ctxt, v: tritv::t) -> str {
@@ -167,16 +159,14 @@ fn print_idents(&idents: [ident]) {
 /* Two different data structures represent constraints in different
  contexts: constraint and norm_constraint.
 
-constraint gets used to record constraints in a table keyed by def_ids.
-cinit constraints represent a single constraint, for the initialization
-state of a variable; a cpred constraint, with a single operator and a
-list of possible argument lists, could represent several constraints at
-once.
+constraint gets used to record constraints in a table keyed by def_ids.  Each
+constraint has a single operator but a list of possible argument lists, and
+thus represents several constraints at once, one for each possible argument
+list.
 
-norm_constraint, in contrast, gets used when handling an instance
-of a constraint rather than a definition of a constraint. It can
-also be init or pred (ninit or npred), but the npred case just has
-a single argument list.
+norm_constraint, in contrast, gets used when handling an instance of a
+constraint rather than a definition of a constraint. It has only a single
+argument list.
 
 The representation of constraints, where multiple instances of the
 same predicate are collapsed into one entry in the table, makes it
@@ -198,37 +188,23 @@ type pred_args = spanned<pred_args_>;
 // for this local.
 type constr_arg_use = spanned<constr_arg_general_<inst>>;
 
-/*
-  A constraint is either an init constraint, referring to the initialization
-  state of a variable (not initialized, definitely initialized, or maybe
-  initialized) or a predicate constraint, referring to the truth value of a
-  predicate on variables (definitely false, maybe true, or definitely true).
-
-  cinit and ninit represent init constraints, while cpred and npred
-  represent predicate constraints.
-
-  In a predicate constraint, the <path> field (and the <def_id> field
-  in the npred constructor) names a user-defined function that may
-  be the operator in a "check" expression in the source.
- */
-
-enum constraint {
-    cinit(uint, span, ident),
+/* Predicate constraints refer to the truth value of a predicate on variables
+(definitely false, maybe true, or definitely true).  The <path> field (and the
+<def_id> field in the npred constructor) names a user-defined function that
+may be the operator in a "check" expression in the source.  */
 
+type constraint = {
+    path: @path,
     // FIXME: really only want it to be mut during collect_locals.
     // freeze it after that.
-    cpred(@path, @mut [pred_args]),
-}
+    descs: @mut [pred_args]
+};
 
-// An ninit variant has a node_id because it refers to a local var.
-// An npred has a def_id since the definition of the typestate
-// predicate need not be local.
-// FIXME: would be nice to give both a def_id field,
-// and give ninit a constraint saying it's local.
-enum tsconstr {
-    ninit(node_id, ident),
-    npred(@path, def_id, [@constr_arg_use]),
-}
+type tsconstr = {
+    path: @path,
+    def_id: def_id,
+    args: [@constr_arg_use]
+};
 
 type sp_constr = spanned<tsconstr>;
 
@@ -238,34 +214,8 @@ type constr_map = std::map::hashmap<def_id, constraint>;
 
 /* Contains stuff that has to be computed up front */
 /* For easy access, the fn_info stores two special constraints for each
-function.  i_return holds if all control paths in this function terminate
-in either a return expression, or an appropriate tail expression.
-i_diverge holds if all control paths in this function terminate in a fail
-or diverging call.
-
-It might be tempting to use a single constraint C for both properties,
-where C represents i_return and !C represents i_diverge. This is
-inadvisable, because then the sense of the bit depends on context. If we're
-inside a ! function, that reverses the sense of the bit: C would be
-i_diverge and !C would be i_return.  That's awkward, because we have to
-pass extra context around to functions that shouldn't care.
-
-Okay, suppose C represents i_return and !C represents i_diverge, regardless
-of context. Consider this code:
-
-if (foo) { ret; } else { fail; }
-
-C is true in the consequent and false in the alternative. What's T `join`
-F, then?  ? doesn't work, because this code should definitely-return if the
-context is a returning function (and be definitely-rejected if the context
-is a ! function).  F doesn't work, because then the code gets incorrectly
-rejected if the context is a returning function. T would work, but it
-doesn't make sense for T `join` F to be T (consider init constraints, for
-example).;
-
-So we need context. And so it seems clearer to just have separate
-constraints.
-*/
+function.  So we need context. And so it seems clearer to just have separate
+constraints. */
 type fn_info =
     /* list, accumulated during pre/postcondition
     computation, of all local variables that may be
@@ -274,21 +224,8 @@ type fn_info =
     {constrs: constr_map,
      num_constraints: uint,
      cf: ret_style,
-     i_return: tsconstr,
-     i_diverge: tsconstr,
      used_vars: @mut [node_id]};
 
-fn tsconstr_to_def_id(t: tsconstr) -> def_id {
-    alt t { ninit(id, _) { local_def(id) } npred(_, id, _) { id } }
-}
-
-fn tsconstr_to_node_id(t: tsconstr) -> node_id {
-    alt t {
-      ninit(id, _) { id }
-      npred(_, id, _) { fail "tsconstr_to_node_id called on pred constraint" }
-    }
-}
-
 /* mapping from node ID to typestate annotation */
 type node_ann_table = @mut [mut ts_ann];
 
@@ -534,20 +471,15 @@ fn node_id_to_def(ccx: crate_ctxt, id: node_id) -> option<def> {
 }
 
 fn norm_a_constraint(id: def_id, c: constraint) -> [norm_constraint] {
-    alt c {
-      cinit(n, sp, i) {
-        ret [{bit_num: n, c: respan(sp, ninit(id.node, i))}];
-      }
-      cpred(p, descs) {
-        let mut rslt: [norm_constraint] = [];
-        for vec::each(*descs) {|pd|
-            rslt +=
-                [{bit_num: pd.node.bit_num,
-                  c: respan(pd.span, npred(p, id, pd.node.args))}];
-        }
-        ret rslt;
-      }
+    let mut rslt: [norm_constraint] = [];
+    for vec::each(*c.descs) {|pd|
+        rslt +=
+            [{bit_num: pd.node.bit_num,
+              c: respan(pd.span, {path: c.path,
+                                  def_id: id,
+                                  args: pd.node.args})}];
     }
+    ret rslt;
 }
 
 
@@ -630,8 +562,9 @@ fn expr_to_constr(tcx: ty::ctxt, e: @expr) -> sp_constr {
         alt operator.node {
           expr_path(p) {
             ret respan(e.span,
-                       npred(p, def_id_for_constr(tcx, operator.id),
-                             exprs_to_constr_args(tcx, args)));
+                       {path: p,
+                        def_id: def_id_for_constr(tcx, operator.id),
+                        args: exprs_to_constr_args(tcx, args)});
           }
           _ {
             tcx.sess.span_bug(operator.span,
@@ -657,7 +590,9 @@ fn substitute_constr_args(cx: ty::ctxt, actuals: [@expr], c: @ty::constr) ->
     for c.node.args.each {|a|
         rslt += [substitute_arg(cx, actuals, a)];
     }
-    ret npred(c.node.path, c.node.id, rslt);
+    ret {path: c.node.path,
+         def_id: c.node.id,
+         args: rslt};
 }
 
 fn substitute_arg(cx: ty::ctxt, actuals: [@expr], a: @constr_arg) ->
@@ -718,31 +653,22 @@ enum dest {
 
 type subst = [{from: inst, to: inst}];
 
-fn find_instances(_fcx: fn_ctxt, subst: subst, c: constraint) ->
-   [{from: uint, to: uint}] {
-
-    let mut rslt = [];
-    if vec::len(subst) == 0u { ret rslt; }
-
-    alt c {
-      cinit(_, _, _) {/* this is dealt with separately */ }
-      cpred(p, descs) {
-        // FIXME (#2280): this temporary shouldn't be
-        // necessary, but seems to be, for borrowing.
-        let ds = copy *descs;
-        for vec::each(ds) {|d|
-            if args_mention(d.node.args, find_in_subst_bool, subst) {
-                let old_bit_num = d.node.bit_num;
-                let newv = replace(subst, d);
-                alt find_instance_(newv, *descs) {
-                  some(d1) { rslt += [{from: old_bit_num, to: d1}]; }
-                  _ { }
-                }
+fn find_instances(_fcx: fn_ctxt, subst: subst,
+                  c: constraint) -> [{from: uint, to: uint}] {
+
+    if vec::len(subst) == 0u { ret []; }
+    let mut res = [];
+    for (*c.descs).each { |d|
+        if args_mention(d.node.args, find_in_subst_bool, subst) {
+            let old_bit_num = d.node.bit_num;
+            let newv = replace(subst, d);
+            alt find_instance_(newv, *c.descs) {
+              some(d1) {res += [{from: old_bit_num, to: d1}]}
+              _ {}
             }
-        }
-      }
+        } else {}
     }
-    rslt
+    ret res;
 }
 
 fn find_in_subst(id: node_id, s: subst) -> option<inst> {
@@ -912,25 +838,6 @@ fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) {
     }
 }
 
-fn forget_in_postcond_still_init(fcx: fn_ctxt, parent_exp: node_id,
-                                 dead_v: node_id) {
-    // In the postcondition given by parent_exp, clear the bits
-    // for any constraints mentioning dead_v
-    let d = local_node_id_to_local_def_id(fcx, dead_v);
-    alt d {
-      some(d_id) {
-        for constraints(fcx).each {|c|
-            if non_init_constraint_mentions(fcx, c, d_id) {
-                clear_in_postcond(c.bit_num,
-                                  node_id_to_ts_ann(fcx.ccx,
-                                                    parent_exp).conditions);
-            }
-        }
-      }
-      _ { }
-    }
-}
-
 fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool {
     // In the poststate given by parent_exp, clear the bits
     // for any constraints mentioning dead_v
@@ -949,25 +856,6 @@ fn forget_in_poststate(fcx: fn_ctxt, p: poststate, dead_v: node_id) -> bool {
     ret changed;
 }
 
-fn forget_in_poststate_still_init(fcx: fn_ctxt, p: poststate, dead_v: node_id)
-   -> bool {
-    // In the poststate given by parent_exp, clear the bits
-    // for any constraints mentioning dead_v
-    let d = local_node_id_to_local_def_id(fcx, dead_v);
-    let mut changed = false;
-    alt d {
-      some(d_id) {
-        for constraints(fcx).each {|c|
-            if non_init_constraint_mentions(fcx, c, d_id) {
-                changed |= clear_in_poststate_(c.bit_num, p);
-            }
-        }
-      }
-      _ { }
-    }
-    ret changed;
-}
-
 fn any_eq(v: [node_id], d: node_id) -> bool {
     for v.each {|i| if i == d { ret true; } }
     false
@@ -975,18 +863,7 @@ fn any_eq(v: [node_id], d: node_id) -> bool {
 
 fn constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id) ->
    bool {
-    ret alt c.c.node {
-          ninit(id, _) { v == id }
-          npred(_, _, args) { args_mention(args, any_eq, [v]) }
-        };
-}
-
-fn non_init_constraint_mentions(_fcx: fn_ctxt, c: norm_constraint, v: node_id)
-   -> bool {
-    ret alt c.c.node {
-          ninit(_, _) { false }
-          npred(_, _, args) { args_mention(args, any_eq, [v]) }
-        };
+    ret args_mention(c.c.node.args, any_eq, [v]);
 }
 
 fn args_mention<T>(args: [@constr_arg_use],
@@ -1063,8 +940,9 @@ fn args_to_constr_args(tcx: ty::ctxt, args: [arg],
 fn ast_constr_to_ts_constr(tcx: ty::ctxt, args: [arg], c: @constr) ->
    tsconstr {
     let tconstr = ty::ast_constr_to_constr(tcx, c);
-    ret npred(tconstr.node.path, tconstr.node.id,
-              args_to_constr_args(tcx, args, tconstr.node.args));
+    ret {path: tconstr.node.path,
+         def_id: tconstr.node.id,
+         args: args_to_constr_args(tcx, args, tconstr.node.args)};
 }
 
 fn ast_constr_to_sp_constr(tcx: ty::ctxt, args: [arg], c: @constr) ->
diff --git a/src/rustc/middle/tstate/bitvectors.rs b/src/rustc/middle/tstate/bitvectors.rs
index 1020f1a001a..e2ce69cc91e 100644
--- a/src/rustc/middle/tstate/bitvectors.rs
+++ b/src/rustc/middle/tstate/bitvectors.rs
@@ -15,36 +15,19 @@ import driver::session::session;
 import std::map::hashmap;
 
 fn bit_num(fcx: fn_ctxt, c: tsconstr) -> uint {
-    let d = tsconstr_to_def_id(c);
+    let d = c.def_id;
     assert (fcx.enclosing.constrs.contains_key(d));
     let rslt = fcx.enclosing.constrs.get(d);
-    alt c {
-      ninit(_, _) {
-        alt rslt {
-          cinit(n, _, _) { ret n; }
-          _ {
-            fcx.ccx.tcx.sess.bug("bit_num: asked for init constraint," +
-                                     " found a pred constraint");
-          }
-        }
-      }
-      npred(_, _, args) {
-        alt rslt {
-          cpred(_, descs) { ret match_args(fcx, descs, args); }
-          _ {
-            fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint," +
-                                     " found an init constraint");
-          }
-        }
-      }
-    }
+    match_args(fcx, rslt.descs, c.args)
 }
 
 fn promises(fcx: fn_ctxt, p: poststate, c: tsconstr) -> bool {
     ret promises_(bit_num(fcx, c), p);
 }
 
-fn promises_(n: uint, p: poststate) -> bool { ret tritv_get(p, n) == ttrue; }
+fn promises_(n: uint, p: poststate) -> bool {
+    ret tritv_get(p, n) == ttrue;
+}
 
 // v "happens after" u
 fn seq_trit(u: trit, v: trit) -> trit {
@@ -184,51 +167,15 @@ fn kill_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
                            node_id_to_ts_ann(fcx.ccx, id).states);
 }
 
-fn clear_in_poststate_expr(fcx: fn_ctxt, e: @expr, t: poststate) {
-    alt e.node {
-      expr_path(p) {
-        alt local_node_id_to_def(fcx, e.id) {
-          some(def_local(nid, _)) {
-            clear_in_poststate_(bit_num(fcx, ninit(nid, vec::last(p.idents))),
-                                t);
-          }
-          some(_) {/* ignore args (for now...) */ }
-          _ { fcx.ccx.tcx.sess.bug("clear_in_poststate_expr: unbound var"); }
-        }
-      }
-      _ {/* do nothing */ }
-    }
-}
-
 fn kill_poststate_(fcx: fn_ctxt, c: tsconstr, post: poststate) -> bool {
     #debug("kill_poststate_");
     ret clear_in_poststate_(bit_num(fcx, c), post);
 }
 
-fn set_in_poststate_ident(fcx: fn_ctxt, id: node_id, ident: ident,
-                          t: poststate) -> bool {
-    ret set_in_poststate_(bit_num(fcx, ninit(id, ident)), t);
-}
-
 fn set_in_prestate_constr(fcx: fn_ctxt, c: tsconstr, t: prestate) -> bool {
     ret set_in_poststate_(bit_num(fcx, c), t);
 }
 
-fn clear_in_poststate_ident(fcx: fn_ctxt, id: node_id, ident: ident,
-                            parent: node_id) -> bool {
-    ret kill_poststate(fcx, parent, ninit(id, ident));
-}
-
-fn clear_in_prestate_ident(fcx: fn_ctxt, id: node_id, ident: ident,
-                           parent: node_id) -> bool {
-    ret kill_prestate(fcx, parent, ninit(id, ident));
-}
-
-fn clear_in_poststate_ident_(fcx: fn_ctxt, id: node_id, ident: ident,
-                             post: poststate) -> bool {
-    ret kill_poststate_(fcx, ninit(id, ident), post);
-}
-
 //
 // Local Variables:
 // mode: rust
diff --git a/src/rustc/middle/tstate/ck.rs b/src/rustc/middle/tstate/ck.rs
index a8c06cd322a..1cc3a7df9dc 100644
--- a/src/rustc/middle/tstate/ck.rs
+++ b/src/rustc/middle/tstate/ck.rs
@@ -17,22 +17,6 @@ import states::find_pre_post_state_fn;
 import driver::session::session;
 import std::map::hashmap;
 
-fn check_unused_vars(fcx: fn_ctxt) {
-
-    // FIXME: could be more efficient
-    for constraints(fcx).each {|c|
-        alt c.c.node {
-          ninit(id, v) {
-            if !vec_contains(fcx.enclosing.used_vars, id) && v[0] != '_' as u8
-               {
-                fcx.ccx.tcx.sess.span_warn(c.c.span, "unused variable " + v);
-            }
-          }
-          _ {/* ignore pred constraints */ }
-        }
-    }
-}
-
 fn check_states_expr(e: @expr, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
     visit::visit_expr(e, fcx, v);
 
@@ -109,39 +93,6 @@ fn check_states_against_conditions(fcx: fn_ctxt,
           visit_fn: bind do_nothing::<fn_ctxt>(_, _, _, _, _, _, _)
           with *visit::default_visitor::<fn_ctxt>()});
     visit::visit_fn(fk, f_decl, f_body, sp, id, fcx, visitor);
-
-    /* Check that the return value is initialized */
-    let post = aux::block_poststate(fcx.ccx, f_body);
-    let is_ctor = alt fk { visit::fk_ctor(_,_,_,_) { true } _ { false } };
-    if !is_ctor && !promises(fcx, post, fcx.enclosing.i_return) &&
-       !ty::type_is_nil(ty::ty_fn_ret(ty::node_id_to_type(
-           fcx.ccx.tcx, id))) &&
-       f_decl.cf == return_val {
-        let fn_ty = ty::node_id_to_type(fcx.ccx.tcx, id);
-        fcx.ccx.tcx.sess.span_err(f_body.span,
-                    #fmt("in function `%s`, not all control paths \
-                          return a value", fcx.name));
-        fcx.ccx.tcx.sess.span_fatal(f_decl.output.span,
-                                    #fmt("see function return type of `%s`",
-                                         ty_to_str(fcx.ccx.tcx,
-                                           ty::ty_fn_ret(fn_ty))));
-    } else if f_decl.cf == noreturn {
-
-        // check that this really always fails
-        // Note that it's ok for i_diverge and i_return to both be true.
-        // In fact, i_diverge implies i_return. (But not vice versa!)
-
-        if !promises(fcx, post, fcx.enclosing.i_diverge) {
-            fcx.ccx.tcx.sess.span_fatal(f_body.span,
-                                        "in non-returning function " +
-                                        fcx.name +
-                                        ", some control paths may \
-                                         return to the caller");
-        }
-    }
-
-    /* Finally, check for unused variables */
-    check_unused_vars(fcx);
 }
 
 fn check_fn_states(fcx: fn_ctxt,
diff --git a/src/rustc/middle/tstate/collect_locals.rs b/src/rustc/middle/tstate/collect_locals.rs
index 88a353f4cd8..bfa2fa58f77 100644
--- a/src/rustc/middle/tstate/collect_locals.rs
+++ b/src/rustc/middle/tstate/collect_locals.rs
@@ -11,13 +11,6 @@ import std::map::hashmap;
 
 type ctxt = {cs: @mut [sp_constr], tcx: ty::ctxt};
 
-fn collect_local(loc: @local, cx: ctxt, v: visit::vt<ctxt>) {
-    pat_bindings(cx.tcx.def_map, loc.node.pat) {|p_id, _s, id|
-       *cx.cs += [respan(loc.span, ninit(p_id, path_to_ident(id)))];
-    };
-    visit::visit_local(loc, cx, v);
-}
-
 fn collect_pred(e: @expr, cx: ctxt, v: visit::vt<ctxt>) {
     alt e.node {
       expr_check(_, ch) { *cx.cs += [expr_to_constr(cx.tcx, ch)]; }
@@ -48,8 +41,7 @@ fn find_locals(tcx: ty::ctxt,
     let cx: ctxt = {cs: @mut [], tcx: tcx};
     let visitor = visit::default_visitor::<ctxt>();
     let visitor =
-        @{visit_local: collect_local,
-          visit_expr: collect_pred,
+        @{visit_expr: collect_pred,
           visit_fn: bind do_nothing(_, _, _, _, _, _, _)
           with *visitor};
     visit::visit_fn(fk, f_decl, f_body, sp,
@@ -61,27 +53,17 @@ fn add_constraint(tcx: ty::ctxt, c: sp_constr, next: uint, tbl: constr_map) ->
    uint {
     log(debug,
              constraint_to_str(tcx, c) + " |-> " + uint::str(next));
-    alt c.node {
-      ninit(id, i) { tbl.insert(local_def(id), cinit(next, c.span, i)); }
-      npred(p, d_id, args) {
-        alt tbl.find(d_id) {
-          some(ct) {
-            alt ct {
-              cinit(_, _, _) {
-                tcx.sess.bug("add_constraint: same def_id used" +
-                                 " as a variable and a pred");
-              }
-              cpred(_, pds) {
-                *pds += [respan(c.span, {args: args, bit_num: next})];
-              }
-            }
-          }
-          none {
-            let rslt: @mut [pred_args] =
-                @mut [respan(c.span, {args: args, bit_num: next})];
-            tbl.insert(d_id, cpred(p, rslt));
-          }
-        }
+
+    let {path: p, def_id: d_id, args: args} = c.node;
+    alt tbl.find(d_id) {
+      some(ct) {
+        let {path: _, descs: pds} = ct;
+        *pds += [respan(c.span, {args: args, bit_num: next})];
+      }
+      none {
+        let rslt: @mut [pred_args] =
+            @mut [respan(c.span, {args: args, bit_num: next})];
+        tbl.insert(d_id, {path:p, descs:rslt});
       }
     }
     ret next + 1u;
@@ -106,7 +88,7 @@ fn mk_fn_info(ccx: crate_ctxt,
 
     let mut i = 0u, l = vec::len(*cx.cs);
     while i < l {
-        next = add_constraint(cx.tcx, cx.cs[i], next, res_map);
+        next = add_constraint(cx.tcx, copy cx.cs[i], next, res_map);
         i += 1u;
     }
     /* if this function has any constraints, instantiate them to the
@@ -116,38 +98,11 @@ fn mk_fn_info(ccx: crate_ctxt,
         next = add_constraint(cx.tcx, sc, next, res_map);
     }
 
-    /* Need to add constraints for args too, b/c they
-    can be deinitialized */
-    for f_decl.inputs.each {|a|
-        next = add_constraint(
-            cx.tcx,
-            respan(f_sp, ninit(a.id, a.ident)),
-            next,
-            res_map);
-    }
-
-    /* add the special i_diverge and i_return constraints
-    (see the type definition for auxiliary::fn_info for an explanation) */
-
-    // use the function name for the "returns" constraint"
-    let returns_id = ccx.tcx.sess.next_node_id();
-    let returns_constr = ninit(returns_id, name);
-    next =
-        add_constraint(cx.tcx, respan(f_sp, returns_constr), next, res_map);
-    // and the name of the function, with a '!' appended to it, for the
-    // "diverges" constraint
-    let diverges_id = ccx.tcx.sess.next_node_id();
-    let diverges_constr = ninit(diverges_id, name + "!");
-    next = add_constraint(cx.tcx, respan(f_sp, diverges_constr), next,
-                          res_map);
-
     let v: @mut [node_id] = @mut [];
     let rslt =
         {constrs: res_map,
          num_constraints: next,
          cf: f_decl.cf,
-         i_return: returns_constr,
-         i_diverge: diverges_constr,
          used_vars: v};
     ccx.fm.insert(id, rslt);
     #debug("%s has %u constraints", name, num_constraints(rslt));
diff --git a/src/rustc/middle/tstate/pre_post_conditions.rs b/src/rustc/middle/tstate/pre_post_conditions.rs
index 3d1db2f6e66..20a1c7bff85 100644
--- a/src/rustc/middle/tstate/pre_post_conditions.rs
+++ b/src/rustc/middle/tstate/pre_post_conditions.rs
@@ -88,17 +88,9 @@ fn find_pre_post_exprs(fcx: fn_ctxt, args: [@expr], id: node_id) {
                      seq_postconds(fcx, vec::map(pps, get_post)));
 }
 
-fn find_pre_post_loop(fcx: fn_ctxt, l: @local, index: @expr, body: blk,
-                      id: node_id) {
+fn find_pre_post_loop(fcx: fn_ctxt, index: @expr, body: blk, id: node_id) {
     find_pre_post_expr(fcx, index);
     find_pre_post_block(fcx, body);
-    pat_bindings(fcx.ccx.tcx.def_map, l.node.pat) {|p_id, _s, n|
-        let v_init = ninit(p_id, path_to_ident(n));
-        relax_precond_block(fcx, bit_num(fcx, v_init) as node_id, body);
-        // Hack: for-loop index variables are frequently ignored,
-        // so we pretend they're used
-        use_var(fcx, p_id);
-    };
 
     let loop_precond =
         seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]);
@@ -184,8 +176,6 @@ fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id,
             let p = expr_pp(fcx.ccx, rhs);
             set_pre_and_post(fcx.ccx, larger_id, p.precondition,
                              p.postcondition);
-            gen(fcx, larger_id,
-                ninit(nid, path_to_ident(pth)));
           }
           _ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); }
         }
@@ -207,23 +197,13 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
             if is_path(rhs) { forget_in_postcond(fcx, parent.id, rhs.id); }
           }
           oper_swap {
-            forget_in_postcond_still_init(fcx, parent.id, lhs.id);
-            forget_in_postcond_still_init(fcx, parent.id, rhs.id);
+            forget_in_postcond(fcx, parent.id, lhs.id);
+            forget_in_postcond(fcx, parent.id, rhs.id);
           }
           oper_assign {
-            forget_in_postcond_still_init(fcx, parent.id, lhs.id);
-          }
-          _ {
-            // pure and assign_op require the lhs to be init'd
-            let df = node_id_to_def_strict(fcx.ccx.tcx, lhs.id);
-            alt df {
-              def_local(nid, _) {
-                let i = bit_num(fcx, ninit(nid, path_to_ident(p)));
-                require_and_preserve(i, expr_pp(fcx.ccx, lhs));
-              }
-              _ { }
-            }
+            forget_in_postcond(fcx, parent.id, lhs.id);
           }
+          _ { }
         }
 
         gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p);
@@ -255,22 +235,6 @@ fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
     }
 }
 
-fn handle_var(fcx: fn_ctxt, rslt: pre_and_post, id: node_id, name: ident) {
-    handle_var_def(fcx, rslt, node_id_to_def_strict(fcx.ccx.tcx, id), name);
-}
-
-fn handle_var_def(fcx: fn_ctxt, rslt: pre_and_post, def: def, name: ident) {
-    log(debug, ("handle_var_def: ", def, name));
-    alt def {
-      def_local(nid, _) | def_arg(nid, _) {
-        use_var(fcx, nid);
-        let i = bit_num(fcx, ninit(nid, name));
-        require_and_preserve(i, rslt);
-      }
-      _ {/* nothing to check */ }
-    }
-}
-
 fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [mode],
                         operands: [@expr]) {
     vec::iteri(modes) {|i,mode|
@@ -284,10 +248,6 @@ fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [mode],
 fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) {
     let rslt = expr_pp(fcx.ccx, e);
     clear_pp(rslt);
-    for vec::each(*freevars::get_freevars(fcx.ccx.tcx, e.id)) {|def|
-        log(debug, ("handle_var_def: def=", def));
-        handle_var_def(fcx, rslt, def.def, "upvar");
-    }
 }
 
 /* Fills in annotations as a side effect. Does not rebuild the expr */
@@ -332,7 +292,6 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
       expr_path(p) {
         let rslt = expr_pp(fcx.ccx, e);
         clear_pp(rslt);
-        handle_var(fcx, rslt, e.id, path_to_ident(p));
       }
       expr_new(p, _, v) {
         find_pre_post_exprs(fcx, [p, v], e.id);
@@ -374,7 +333,7 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
            already be initialized */
 
         find_pre_post_exprs(fcx, [lhs, rhs], e.id);
-        forget_in_postcond_still_init(fcx, e.id, lhs.id);
+        forget_in_postcond(fcx, e.id, lhs.id);
       }
       expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); }
       expr_ret(maybe_val) {
@@ -555,25 +514,16 @@ fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
                           }
                           none { }
                         }
-                        gen(fcx, id, ninit(p_id, ident));
                     };
 
-                    if an_init.op == init_move && is_path(an_init.expr) {
-                        forget_in_postcond(fcx, id, an_init.expr.id);
-                    }
-
                     /* Clear out anything that the previous initializer
                     guaranteed */
                     let e_pp = expr_pp(fcx.ccx, an_init.expr);
                     tritv_copy(prev_pp.precondition,
                                seq_preconds(fcx, [prev_pp, e_pp]));
+
                     /* Include the LHSs too, since those aren't in the
                      postconds of the RHSs themselves */
-                    pat_bindings(fcx.ccx.tcx.def_map, alocal.node.pat)
-                        {|pat_id, _s, n|
-                            set_in_postcond(bit_num(fcx,
-                               ninit(pat_id, path_to_ident(n))), prev_pp);
-                          };
                     copy_pre_post_(fcx.ccx, id, prev_pp.precondition,
                                    prev_pp.postcondition);
                   }
@@ -659,10 +609,6 @@ fn find_pre_post_block(fcx: fn_ctxt, b: blk) {
 }
 
 fn find_pre_post_fn(fcx: fn_ctxt, body: blk) {
-    // hack
-    use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_return));
-    use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_diverge));
-
     find_pre_post_block(fcx, body);
 
     // Treat the tail expression as a return statement
diff --git a/src/rustc/middle/tstate/states.rs b/src/rustc/middle/tstate/states.rs
index 4e484fccd07..abfe2989f78 100644
--- a/src/rustc/middle/tstate/states.rs
+++ b/src/rustc/middle/tstate/states.rs
@@ -55,22 +55,6 @@ fn handle_move_or_copy(fcx: fn_ctxt, post: poststate, rhs_path: @path,
     }
 }
 
-fn handle_fail(fcx: fn_ctxt, pres:prestate, post:poststate) {
-    // Remember what the old value of the "I return" trit was, so that
-    // we can avoid changing that (if it was true, there was a return
-    // that dominates this fail and the fail is unreachable)
-    if !promises(fcx, pres, fcx.enclosing.i_return)
-        // (only if we're in a diverging function -- you can fail when
-        // you're supposed to return, but not vice versa).
-        && fcx.enclosing.cf == noreturn {
-          kill_poststate_(fcx, fcx.enclosing.i_return, post);
-    } else {
-        // This code is unreachable (it's dominated by a return),
-        // so doesn't diverge.
-        kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
-    }
-}
-
 fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) ->
    {changed: bool, post: poststate} {
     let mut changed = false;
@@ -90,12 +74,6 @@ fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) ->
                   }
                   _ { }
                 }
-                alt d {
-                  local_dest(i) {
-                      set_in_poststate_ident(fcx, i.node, i.ident, post);
-                  }
-                  _ {}
-                }
             }
 
             // Forget the RHS if we just moved it.
@@ -104,15 +82,6 @@ fn seq_states(fcx: fn_ctxt, pres: prestate, bindings: [binding]) ->
             }
           }
           none {
-            for b.lhs.each {|d|
-                // variables w/o an initializer
-                 alt check d {
-                   // would be an error to pass something uninit'd to a call
-                   local_dest(i) {
-                     clear_in_poststate_ident_(fcx, i.node, i.ident, post);
-                   }
-                 }
-            }
           }
         }
     }
@@ -158,16 +127,15 @@ fn find_pre_post_state_two(fcx: fn_ctxt, pres: prestate, lhs: @expr,
         alt ty {
           oper_move {
             if is_path(rhs) { forget_in_poststate(fcx, post, rhs.id); }
-            forget_in_poststate_still_init(fcx, post, lhs.id);
+            forget_in_poststate(fcx, post, lhs.id);
           }
           oper_swap {
-            forget_in_poststate_still_init(fcx, post, lhs.id);
-            forget_in_poststate_still_init(fcx, post, rhs.id);
+            forget_in_poststate(fcx, post, lhs.id);
+            forget_in_poststate(fcx, post, rhs.id);
           }
-          _ { forget_in_poststate_still_init(fcx, post, lhs.id); }
+          _ { forget_in_poststate(fcx, post, lhs.id); }
         }
 
-        gen_if_local(fcx, post, lhs);
         alt rhs.node {
           expr_path(p1) {
             let d = local_node_id_to_local_def_id(fcx, lhs.id);
@@ -222,7 +190,6 @@ fn find_pre_post_state_exprs(fcx: fn_ctxt, pres: prestate, id: node_id,
     alt cf {
       noreturn {
         let post = false_postcond(num_constraints(fcx.enclosing));
-        handle_fail(fcx, pres, post);
         changed |= set_poststate_ann(fcx.ccx, id, post);
       }
       _ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
@@ -240,16 +207,9 @@ fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local,
         set_prestate_ann(fcx.ccx, id, loop_pres) |
             find_pre_post_state_expr(fcx, pres, index);
 
-    // Make sure the index vars are considered initialized
-    // in the body
     let index_post = tritv_clone(expr_poststate(fcx.ccx, index));
-    pat_bindings(fcx.ccx.tcx.def_map, l.node.pat) {|p_id, _s, n|
-       set_in_poststate_ident(fcx, p_id, path_to_ident(n), index_post);
-    };
-
     changed |= find_pre_post_state_block(fcx, index_post, body);
 
-
     if has_nonlocal_exits(body) {
         // See [Break-unsound]
         ret changed | set_poststate_ann(fcx.ccx, id, pres);
@@ -261,20 +221,6 @@ fn find_pre_post_state_loop(fcx: fn_ctxt, pres: prestate, l: @local,
     }
 }
 
-fn gen_if_local(fcx: fn_ctxt, p: poststate, e: @expr) -> bool {
-    alt e.node {
-      expr_path(pth) {
-        alt fcx.ccx.tcx.def_map.find(e.id) {
-          some(def_local(nid, _)) {
-            ret set_in_poststate_ident(fcx, nid, path_to_ident(pth), p);
-          }
-          _ { ret false; }
-        }
-      }
-      _ { ret false; }
-    }
-}
-
 fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
                   maybe_alt: option<@expr>, id: node_id, chk: if_ty,
                   pres: prestate) -> bool {
@@ -465,13 +411,10 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
       }
       expr_ret(maybe_ret_val) {
         let mut changed = set_prestate_ann(fcx.ccx, e.id, pres);
-        /* normally, everything is true if execution continues after
+        /* everything is true if execution continues after
            a ret expression (since execution never continues locally
            after a ret expression */
-        // FIXME should factor this out
         let post = false_postcond(num_constrs);
-        // except for the "diverges" bit...
-        kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
 
         set_poststate_ann(fcx.ccx, e.id, post);
 
@@ -593,7 +536,6 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
         /* if execution continues after fail, then everything is true!
         woo! */
         let post = false_postcond(num_constrs);
-        handle_fail(fcx, pres, post);
         ret set_prestate_ann(fcx.ccx, e.id, pres) |
                 set_poststate_ann(fcx.ccx, e.id, post) |
                 option::map_default(maybe_fail_val, false, {|fail_val|
@@ -727,13 +669,8 @@ fn find_pre_post_state_fn(fcx: fn_ctxt,
     // This ensures that intersect works correctly.
     kill_all_prestate(fcx, f_body.node.id);
 
-    // Arguments start out initialized
-    let block_pre = block_prestate(fcx.ccx, f_body);
-    for f_decl.inputs.each {|a|
-        set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre);
-    }
-
     // Instantiate any constraints on the arguments so we can use them
+    let block_pre = block_prestate(fcx.ccx, f_body);
     for f_decl.constraints.each {|c|
         let tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f_decl.inputs, c);
         set_in_prestate_constr(fcx, tsc, block_pre);
@@ -741,23 +678,6 @@ fn find_pre_post_state_fn(fcx: fn_ctxt,
 
     let mut changed = find_pre_post_state_block(fcx, block_pre, f_body);
 
-    // Treat the tail expression as a return statement
-    alt f_body.node.expr {
-      some(tailexpr) {
-
-        // We don't want to clear the diverges bit for bottom typed things,
-        // which really do diverge. I feel like there is a cleaner way
-        // to do this than checking the type.
-        if !type_is_bot(expr_ty(fcx.ccx.tcx, tailexpr)) {
-            let post = false_postcond(num_constrs);
-            // except for the "diverges" bit...
-            kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
-            set_poststate_ann(fcx.ccx, f_body.node.id, post);
-        }
-      }
-      none {/* fallthrough */ }
-    }
-
     /*
         #error("find_pre_post_state_fn");
         log(error, changed);
diff --git a/src/test/compile-fail/liveness-unused.rs b/src/test/compile-fail/liveness-unused.rs
index 2a19c9808c7..83f0c9b802a 100644
--- a/src/test/compile-fail/liveness-unused.rs
+++ b/src/test/compile-fail/liveness-unused.rs
@@ -1,20 +1,14 @@
 fn f1(x: int) {
     //!^ WARNING unused variable: `x`
-    //!^^ WARNING unused variable x
-    // (the 2nd one is from tstate)
 }
 
 fn f1b(&x: int) {
     //!^ WARNING unused variable: `x`
-    //!^^ WARNING unused variable x
-    // (the 2nd one is from tstate)
 }
 
 fn f2() {
     let x = 3;
     //!^ WARNING unused variable: `x`
-    //!^^ WARNING unused variable x
-    // (the 2nd one is from tstate)
 }
 
 fn f3() {
diff --git a/src/test/run-pass/liveness-loop-break.rs b/src/test/run-pass/liveness-loop-break.rs
index 58274555202..cec9c25e67a 100644
--- a/src/test/run-pass/liveness-loop-break.rs
+++ b/src/test/run-pass/liveness-loop-break.rs
@@ -1,5 +1,3 @@
-// xfail-test --- tstate incorrectly fails this
-
 fn test() {
     let v;
     loop {