Restructure the "checking" pass in typestate

I noticed that typestate was being lazier than it should be,
because it was only checking typestate for statements and
top-level expression (that is, the expression in a stmt_expr, but
not any subexpressions). So I rewrote the checks in tstate/ck.rs
to use walk, which exposed a few bugs in typestate that I fixed.

Also added some more test cases for if-check.

6 files changed, 324 insertions, 119 deletions

diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs
index 108d050757f..a1b5508e2a2 100644
--- a/src/comp/middle/tstate/ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -168,7 +168,6 @@ fn extend_poststate(&poststate p, &poststate new) -> bool {
     ret bitv::union(p, new);
 }
 
-
 // Clears the given bit in p
 fn relax_prestate(uint i, &prestate p) -> bool {
     auto was_set = bitv::get(p, i);
@@ -176,6 +175,15 @@ fn relax_prestate(uint i, &prestate p) -> bool {
     ret was_set;
 }
 
+// Clears the given bit in p
+fn relax_poststate(uint i, &poststate p) -> bool {
+    ret relax_prestate(i, p);
+}
+
+// Clears the given bit in p
+fn relax_precond(uint i, &precond p) {
+    relax_prestate(i, p);
+}
 
 // Clears all the bits in p
 fn clear(&precond p) { bitv::clear(p); }
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 91359eb8231..e7013752ded 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -358,10 +358,18 @@ fn stmt_poststate(&crate_ctxt ccx, &stmt s) -> poststate {
     ret stmt_states(ccx, s).poststate;
 }
 
+fn block_precond(&crate_ctxt ccx, &block b) -> precond {
+    ret block_pp(ccx, b).precondition;
+}
+
 fn block_postcond(&crate_ctxt ccx, &block b) -> postcond {
     ret block_pp(ccx, b).postcondition;
 }
 
+fn block_prestate(&crate_ctxt ccx, &block b) -> prestate {
+    ret block_states(ccx, b).prestate;
+}
+
 fn block_poststate(&crate_ctxt ccx, &block b) -> poststate {
     ret block_states(ccx, b).poststate;
 }
@@ -402,11 +410,15 @@ fn set_pre_and_post(&crate_ctxt ccx, &ann a, &precond pre, &postcond post) {
 fn copy_pre_post(&crate_ctxt ccx, &ann a, &@expr sub) {
     log "set_pre_and_post";
     auto p = expr_pp(ccx, sub);
-    auto t = ann_to_ts_ann(ccx, a);
-    set_precondition(t, p.precondition);
-    set_postcondition(t, p.postcondition);
+    copy_pre_post_(ccx, a, p.precondition, p.postcondition);
 }
 
+fn copy_pre_post_(&crate_ctxt ccx, &ann a, &prestate pre, &poststate post) {
+    log "set_pre_and_post";
+    auto t = ann_to_ts_ann(ccx, a);
+    set_precondition(t, pre);
+    set_postcondition(t, post);
+}
 
 /* sets all bits to *1* */
 fn set_postcond_false(&crate_ctxt ccx, &ann a) {
@@ -548,7 +560,9 @@ fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use {
         }
         case (expr_lit(?l, _)) { ret @respan(e.span, carg_lit(l)); }
         case (_) {
-            tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg");
+            tcx.sess.span_err(e.span,
+                              "Arguments to constrained functions must be "
+                              + "literals or local variables");
         }
     }
 }
@@ -626,6 +640,11 @@ fn path_to_ident(&ty::ctxt cx, &path p) -> ident {
         case (some(?i)) { ret i; }
     }
 }
+
+tag if_ty { 
+    if_check;
+    plain_if;
+}
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index 99b4c80820e..850add38d5e 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -15,6 +15,12 @@ import aux::npred;
 import aux::pred_desc;
 import aux::match_args;
 import aux::constr_;
+import aux::block_precond;
+import aux::stmt_precond;
+import aux::expr_precond;
+import aux::block_prestate;
+import aux::expr_prestate;
+import aux::stmt_prestate;
 import tstate::aux::ann_to_ts_ann;
 import tstate::ann::pre_and_post;
 import tstate::ann::precond;
@@ -22,6 +28,8 @@ import tstate::ann::postcond;
 import tstate::ann::prestate;
 import tstate::ann::poststate;
 import tstate::ann::relax_prestate;
+import tstate::ann::relax_precond;
+import tstate::ann::relax_poststate;
 import tstate::ann::pps_len;
 import tstate::ann::true_precond;
 import tstate::ann::empty_prestate;
@@ -136,9 +144,46 @@ fn gen(&fn_ctxt fcx, &ann a, &constr_ c) -> bool {
 fn declare_var(&fn_ctxt fcx, &constr_ c, prestate pre) -> prestate {
     auto res = clone(pre);
     relax_prestate(bit_num(fcx, c), res);
+    // idea is this is scoped
+    relax_poststate(bit_num(fcx, c), res);
     ret res;
 }
 
+fn relax_precond_block_non_recursive(&fn_ctxt fcx, uint i, &block b) {
+    relax_precond(i, block_precond(fcx.ccx, b));
+}
+
+fn relax_precond_expr(&fn_ctxt fcx, uint i, &@expr e) {
+    relax_precond(i, expr_precond(fcx.ccx, e));
+}
+
+fn relax_precond_stmt(&fn_ctxt fcx, uint i, &@stmt s) {
+    relax_precond(i, stmt_precond(fcx.ccx, *s));
+}
+
+fn relax_precond_block(&fn_ctxt fcx, uint i, &block b) {
+    relax_precond_block_non_recursive(fcx, i, b);
+    // FIXME: should use visit instead
+    // could at least generalize this pattern 
+    // (also seen in ck::check_states_against_conditions)
+    let @mutable bool keepgoing = @mutable true;
+
+    fn quit(@mutable bool keepgoing, &@item i) {
+        *keepgoing = false;
+    }
+    fn kg(@mutable bool keepgoing) -> bool { ret *keepgoing; }
+
+    auto v = rec(visit_block_pre = bind
+                    relax_precond_block_non_recursive(fcx, i, _),
+                 visit_expr_pre  = bind relax_precond_expr(fcx, i, _),
+                 visit_stmt_pre  = bind relax_precond_stmt(fcx, i, _),
+                  visit_item_pre=bind quit(keepgoing, _),
+                  keep_going=bind kg(keepgoing)
+
+                   with walk::default_visitor());
+    walk::walk_block(v, b);
+}
+
 fn gen_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool {
     log "gen_poststate";
     ret set_in_poststate(bit_num(fcx, c), ann_to_ts_ann(fcx.ccx, a).states);
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 4a4c7c47490..ce170fb1db9 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -61,9 +61,19 @@ import collect_locals::mk_f_to_fn_info;
 import pre_post_conditions::fn_pre_post;
 import states::find_pre_post_state_fn;
 
-fn check_states_expr(&fn_ctxt fcx, @expr e) {
+fn check_states_expr(&fn_ctxt fcx, &@expr e) {
     let precond prec = expr_precond(fcx.ccx, e);
     let prestate pres = expr_prestate(fcx.ccx, e);
+
+    /*
+    log_err("check_states_expr:");
+      util::common::log_expr_err(*e);
+      log_err("prec = ");
+      log_bitv_err(fcx, prec);
+      log_err("pres = ");
+      log_bitv_err(fcx, pres);
+    */
+
     if (!implies(pres, prec)) {
         auto s = "";
         auto diff = first_difference_string(fcx, prec, pres);
@@ -79,26 +89,27 @@ fn check_states_expr(&fn_ctxt fcx, @expr e) {
     }
 }
 
-fn check_states_stmt(&fn_ctxt fcx, &stmt s) {
-    auto a = stmt_to_ann(fcx.ccx, s);
+fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
+    auto a = stmt_to_ann(fcx.ccx, *s);
     let precond prec = ann_precond(a);
     let prestate pres = ann_prestate(a);
 
-    /*    
+    /*
       log_err("check_states_stmt:");
-      log_stmt_err(s);
+      log_stmt_err(*s);
       log_err("prec = ");
-      log_bitv_err(fcx.enclosing, prec);
+      log_bitv_err(fcx, prec);
       log_err("pres = ");
-      log_bitv_err(fcx.enclosing, pres);
+      log_bitv_err(fcx, pres);
     */
+
     if (!implies(pres, prec)) {
         auto ss = "";
         auto diff = first_difference_string(fcx, prec, pres);
         ss +=
             "Unsatisfied precondition constraint (for example, " + diff +
                 ") for statement:\n";
-        ss += pretty::pprust::stmt_to_str(s);
+        ss += pretty::pprust::stmt_to_str(*s);
         ss += "\nPrecondition:\n";
         ss += bitv_to_str(fcx, prec);
         ss += "\nPrestate: \n";
@@ -107,29 +118,37 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) {
     }
 }
 
-fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) {
-    auto enclosing = fcx.enclosing;
-    auto nv = num_constraints(enclosing);
-    auto post = @mutable empty_poststate(nv);
-    fn do_one_(fn_ctxt fcx, &@stmt s, @mutable poststate post) {
-        check_states_stmt(fcx, *s);
-        *post = stmt_poststate(fcx.ccx, *s);
+fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a,
+                                   &span sp, &ident i, &def_id d) {
+    /* Postorder traversal instead of pre is important
+       because we want the smallest possible erroneous statement
+       or expression. */
+
+    let @mutable bool keepgoing = @mutable true;
+    
+    /* TODO probably should use visit instead */
+
+    fn quit(@mutable bool keepgoing, &@ast::item i) {
+        *keepgoing = false;
     }
-    auto do_one = bind do_one_(fcx, _, post);
-    vec::map[@stmt, ()](do_one, f.body.node.stmts);
-    fn do_inner_(fn_ctxt fcx, &@expr e, @mutable poststate post) {
-        check_states_expr(fcx, e);
-        *post = expr_poststate(fcx.ccx, e);
+    fn kg(@mutable bool keepgoing) -> bool { 
+        ret *keepgoing;
     }
-    auto do_inner = bind do_inner_(fcx, _, post);
-    option::map[@expr, ()](do_inner, f.body.node.expr);
-    auto cf = fcx.enclosing.cf;
-    /* Finally, check that the return value is initialized */
 
+    auto v = rec (visit_stmt_post=bind check_states_stmt(fcx, _),
+                  visit_expr_post=bind check_states_expr(fcx, _),
+                  visit_item_pre=bind quit(keepgoing, _),
+                  keep_going=bind kg(keepgoing)
+                  with walk::default_visitor());
+
+    walk::walk_fn(v, f, sp, i, d, a);
+
+    /* Finally, check that the return value is initialized */
+    auto post = aux::block_poststate(fcx.ccx, f.body);
     let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name));
-    if (f.proto == ast::proto_fn && !promises(fcx, { *post }, ret_c) &&
+    if (f.proto == ast::proto_fn && !promises(fcx, post, ret_c) &&
             !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, a)) &&
-            cf == return) {
+            f.decl.cf == return) {
         fcx.ccx.tcx.sess.span_note(f.body.span,
                                    "In function " + fcx.name +
                                        ", not all control paths \
@@ -137,12 +156,12 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) {
         fcx.ccx.tcx.sess.span_err(f.decl.output.span,
                                   "see declared return type of '" +
                                       ty_to_str(*f.decl.output) + "'");
-    } else if (cf == noreturn) {
+    } else if (f.decl.cf == noreturn) {
 
         // check that this really always fails
         // the fcx.id bit means "returns" for a returning fn,
         // "diverges" for a non-returning fn
-        if (!promises(fcx, { *post }, ret_c)) {
+        if (!promises(fcx, post, ret_c)) {
             fcx.ccx.tcx.sess.span_err(f.body.span,
                                       "In non-returning function " + fcx.name
                                           +
@@ -152,7 +171,8 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) {
     }
 }
 
-fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) {
+fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a, &span sp, &ident i,
+                   &def_id d) {
     /* Compute the pre- and post-states for this function */
 
     auto g = find_pre_post_state_fn;
@@ -160,7 +180,7 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) {
     /* Now compare each expr's pre-state to its precondition
        and post-state to its postcondition */
 
-    check_states_against_conditions(fcx, f, a);
+    check_states_against_conditions(fcx, f, a, sp, i, d);
 }
 
 fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id,
@@ -170,7 +190,7 @@ fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id,
     assert (ccx.fm.contains_key(id));
     auto f_info = ccx.fm.get(id);
     auto fcx = rec(enclosing=f_info, id=id, name=i, ccx=ccx);
-    check_fn_states(fcx, f, a);
+    check_fn_states(fcx, f, a, sp, i, id);
 }
 
 fn check_crate(ty::ctxt cx, @crate crate) {
@@ -185,7 +205,7 @@ fn check_crate(ty::ctxt cx, @crate crate) {
 
     auto do_pre_post = walk::default_visitor();
     do_pre_post =
-        rec(visit_fn_pre=bind fn_pre_post(ccx, _, _, _, _, _)
+        rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _, _)
             with do_pre_post);
     walk::walk_crate(do_pre_post, *crate);
     /* Check the pre- and postcondition against the pre- and poststate
@@ -193,7 +213,7 @@ fn check_crate(ty::ctxt cx, @crate crate) {
 
     auto do_states = walk::default_visitor();
     do_states =
-        rec(visit_fn_pre=bind fn_states(ccx, _, _, _, _, _) with do_states);
+        rec(visit_fn_post=bind fn_states(ccx, _, _, _, _, _) with do_states);
     walk::walk_crate(do_states, *crate);
 }
 //
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 3eaf3cfba66..42b12323437 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -32,6 +32,7 @@ import aux::clear_pp;
 import aux::clear_precond;
 import aux::set_pre_and_post;
 import aux::copy_pre_post;
+import aux::copy_pre_post_;
 import aux::expr_precond;
 import aux::expr_postcond;
 import aux::expr_prestate;
@@ -45,8 +46,10 @@ import aux::ann_to_ts_ann;
 import aux::set_postcond_false;
 import aux::controlflow_expr;
 import aux::expr_to_constr;
+import aux::if_ty;
+import aux::if_check;
+import aux::plain_if;
 
-//import aux::constr_to_constr_occ;
 import aux::constraints_expr;
 import aux::substitute_constr_args;
 import aux::ninit;
@@ -55,9 +58,9 @@ import aux::path_to_ident;
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
 import bitvectors::intersect_postconds;
-import bitvectors::declare_var;
 import bitvectors::bit_num;
 import bitvectors::gen;
+import bitvectors::relax_precond_block;
 import front::ast::*;
 import middle::ty::expr_ann;
 import util::common::new_def_hash;
@@ -161,26 +164,37 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
                       &ann a) {
     find_pre_post_expr(fcx, index);
     find_pre_post_block(fcx, body);
+    auto v_init = rec(id=l.node.id, c=ninit(l.node.ident));
+    relax_precond_block(fcx, bit_num(fcx, v_init), body);
+
     auto loop_precond =
-        declare_var(fcx, rec(id=l.node.id, c=ninit(l.node.ident)),
-                    seq_preconds(fcx,
-                                 [expr_pp(fcx.ccx, index),
-                                  block_pp(fcx.ccx, 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)]);
-    set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
+    copy_pre_post_(fcx.ccx, a, loop_precond, loop_postcond);
 }
 
 // Generates a pre/post assuming that a is the 
 // annotation for an if-expression with consequent conseq
 // and alternative maybe_alt
 fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
-                  &option::t[@expr] maybe_alt, &ann a) {
+                  &option::t[@expr] maybe_alt, &ann a, &if_ty chck) {
     auto num_local_vars = num_constraints(fcx.enclosing);
+    find_pre_post_expr(fcx, antec);
     find_pre_post_block(fcx, conseq);
     alt (maybe_alt) {
         case (none) {
+            alt (chck) {
+                case (if_check) {
+                    let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
+                    gen(fcx, expr_ann(antec), c.node);
+                }
+                case (_) {}
+            }
+
             auto precond_res =
                 seq_preconds(fcx,
                              [expr_pp(fcx.ccx, antec),
@@ -189,15 +203,12 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                              expr_poststate(fcx.ccx, antec));
         }
         case (some(?altern)) {
+            /*
+              if check = if_check, then
+              be sure that the predicate implied by antec
+              is *not* true in the alternative
+             */
             find_pre_post_expr(fcx, altern);
-            auto precond_true_case =
-                seq_preconds(fcx,
-                             [expr_pp(fcx.ccx, antec),
-                              block_pp(fcx.ccx, conseq)]);
-            auto postcond_true_case =
-                union_postconds(num_local_vars,
-                                [expr_postcond(fcx.ccx, antec),
-                                 block_postcond(fcx.ccx, conseq)]);
             auto precond_false_case =
                 seq_preconds(fcx,
                              [expr_pp(fcx.ccx, antec),
@@ -206,6 +217,25 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                 union_postconds(num_local_vars,
                                 [expr_postcond(fcx.ccx, antec),
                                  expr_postcond(fcx.ccx, altern)]);
+
+            /* Be sure to set the bit for the check condition here,
+             so that it's *not* set in the alternative. */
+            alt (chck) {
+                case (if_check) {
+                    let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
+                    gen(fcx, expr_ann(antec), c.node);
+                }
+                case (_) {}
+            }
+            auto precond_true_case =
+                seq_preconds(fcx,
+                             [expr_pp(fcx.ccx, antec),
+                              block_pp(fcx.ccx, conseq)]);
+            auto postcond_true_case =
+                union_postconds(num_local_vars,
+                                [expr_postcond(fcx.ccx, antec),
+                                 block_postcond(fcx.ccx, conseq)]);
+
             auto precond_res =
                 union_postconds(num_local_vars,
                                 [precond_true_case,
@@ -396,8 +426,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
                              false_postcond(num_local_vars));
         }
         case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
-            find_pre_post_expr(fcx, antec);
-            join_then_else(fcx, antec, conseq, maybe_alt, a);
+            join_then_else(fcx, antec, conseq, maybe_alt, a, plain_if);
         }
         case (expr_binary(?bop, ?l, ?r, ?a)) {
             /* *unless* bop is lazy (e.g. and, or)? 
@@ -504,16 +533,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
             gen(fcx, a, c.node);
         }
         case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) {
-            find_pre_post_expr(fcx, p);
-            copy_pre_post(fcx.ccx, a, p);
-            /* the typestate for the whole expression */
-            join_then_else(fcx, p, conseq, maybe_alt, a);
-
-            /* predicate p holds inside the "thn" expression */
-            /* (so far, the negation of p does *not* hold inside
-             the "elsopt" expression) */
-            let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
-            gen(fcx, conseq.node.a, c.node);
+            join_then_else(fcx, p, conseq, maybe_alt, a, if_check);
         }
 
         case (expr_bind(?operator, ?maybe_args, ?a)) {
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 841a53702d1..b7c710e85c2 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -32,19 +32,27 @@ import aux::stmt_pp;
 import aux::block_pp;
 import aux::set_pre_and_post;
 import aux::expr_prestate;
+import aux::expr_precond;
+import aux::expr_postcond;
 import aux::stmt_poststate;
 import aux::expr_poststate;
+import aux::block_prestate;
 import aux::block_poststate;
+import aux::block_precond;
+import aux::block_postcond;
 import aux::fn_info;
 import aux::log_pp;
+import aux::log_pp_err;
 import aux::extend_prestate_ann;
 import aux::extend_poststate_ann;
 import aux::set_prestate_ann;
 import aux::set_poststate_ann;
 import aux::pure_exp;
 import aux::log_bitv;
+import aux::log_bitv_err;
 import aux::stmt_to_ann;
 import aux::log_states;
+import aux::log_states_err;
 import aux::block_states;
 import aux::controlflow_expr;
 import aux::ann_to_def;
@@ -52,6 +60,10 @@ import aux::expr_to_constr;
 import aux::ninit;
 import aux::npred;
 import aux::path_to_ident;
+import aux::if_ty;
+import aux::if_check;
+import aux::plain_if;
+
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
 import bitvectors::intersect_postconds;
@@ -69,11 +81,13 @@ import util::common::new_def_hash;
 import util::common::uistr;
 import util::common::log_expr;
 import util::common::log_block;
+import util::common::log_block_err;
 import util::common::log_fn;
 import util::common::elt_exprs;
 import util::common::field_exprs;
 import util::common::has_nonlocal_exits;
 import util::common::log_stmt;
+import util::common::log_stmt_err;
 import util::common::log_expr_err;
 
 fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs) ->
@@ -111,6 +125,11 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
     changed =
         find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body)
             || changed;
+
+    if (has_nonlocal_exits(body)) { 
+        changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
+    }
+
     auto res_p =
         intersect_postconds([expr_poststate(fcx.ccx, index),
                              block_poststate(fcx.ccx, body)]);
@@ -130,14 +149,35 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool {
 }
 
 fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
-                  &option::t[@expr] maybe_alt, &ann a) -> bool {
+                  &option::t[@expr] maybe_alt, &ann a, &if_ty chk,
+                  &prestate pres) -> bool {
     auto changed = false;
 
-    changed =
-        find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
-                                  conseq) || changed;
+    changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+    changed = find_pre_post_state_expr(fcx, pres, antec) || changed;
+    
+    /*
+    log_err("join_then_else:");
+    log_expr_err(*antec);
+    log_bitv_err(fcx, expr_prestate(fcx.ccx, antec));
+    log_bitv_err(fcx, expr_poststate(fcx.ccx, antec));
+    log_block_err(conseq);
+    log_bitv_err(fcx, block_prestate(fcx.ccx, conseq));
+    log_bitv_err(fcx, block_poststate(fcx.ccx, conseq));
+    log_err("****");
+    log_bitv_err(fcx, expr_precond(fcx.ccx, antec));
+    log_bitv_err(fcx, expr_postcond(fcx.ccx, antec));
+    log_bitv_err(fcx, block_precond(fcx.ccx, conseq));
+    log_bitv_err(fcx, block_postcond(fcx.ccx, conseq));
+    */
+
     alt (maybe_alt) {
         case (none) {
+
+            changed =
+                find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
+                                  conseq) || changed;
+   
             changed =
                 extend_poststate_ann(fcx.ccx, a,
                                      expr_poststate(fcx.ccx, antec))
@@ -149,10 +189,35 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
                                          expr_poststate(fcx.ccx,
                                                         antec),
                                          altern) || changed;
+
+            auto conseq_prestate = expr_poststate(fcx.ccx, antec);
+            alt (chk) {
+                case (if_check) {
+                    let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
+                    conseq_prestate = bitv::clone(conseq_prestate);
+                    bitv::set(conseq_prestate, bit_num(fcx, c.node), true);
+                }
+                case (_) {}
+            }
+
+
+            changed =
+                find_pre_post_state_block(fcx, conseq_prestate, conseq)
+                || changed;
+   
             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));
+            fcx.ccx.tcx.sess.span_note(antec.span,
+               "altern poststate = " +
+                aux::bitv_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))); */
+
             changed =
                 extend_poststate_ann(fcx.ccx, a, poststate_res) ||
                 changed;
@@ -164,10 +229,10 @@ 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 changed = false;
     auto num_local_vars = num_constraints(fcx.enclosing);
-
-    /*  
+    /*
     log_err("states:");
     log_expr_err(*e);
+    aux::log_bitv_err(fcx, expr_prestate(fcx.ccx, e));
     aux::log_bitv_err(fcx, expr_poststate(fcx.ccx, e));
     */
 
@@ -182,6 +247,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         case (expr_call(?operator, ?operands, ?a)) {
             /* do the prestate for the rator */
 
+            /*            fcx.ccx.tcx.sess.span_note(operator.span, 
+                         "pres = " + aux::bitv_to_str(fcx, pres));
+            */
+
             changed =
                 find_pre_post_state_expr(fcx, pres, operator) || changed;
             /* rands go left-to-right */
@@ -201,6 +270,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                 }
                 case (_) { }
             }
+
+            /*            fcx.ccx.tcx.sess.span_note(operator.span, 
+               "pres = " + aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, e)));
+            */
             ret changed;
         }
         case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
@@ -436,9 +509,8 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             ret changed;
         }
         case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
-            changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
-            changed = find_pre_post_state_expr(fcx, pres, antec) || changed;
-            changed = join_then_else(fcx, antec, conseq, maybe_alt, a)
+            changed = join_then_else(fcx, antec, conseq, maybe_alt, a,
+                                     plain_if, pres)
                 || changed;
 
             ret changed;
@@ -495,6 +567,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             changed =
                 find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
                                           body) || changed;
+            /* conservative approximation: if a loop contains a break
+               or cont, we assume nothing about the poststate */
+            if (has_nonlocal_exits(body)) { 
+                changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
+            }
+
             changed =
                 {
                     auto e_post = expr_poststate(fcx.ccx, test);
@@ -508,22 +586,35 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         }
         case (expr_do_while(?body, ?test, ?a)) {
             changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+            auto changed0 = changed;
             changed = find_pre_post_state_block(fcx, pres, body) || changed;
-            changed =
-                find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body),
-                                         test) || changed;
             /* 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) */
 
-            if (has_nonlocal_exits(body)) {
-                changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
-            } else {
-                changed =
-                    extend_poststate_ann(fcx.ccx, a,
-                                         expr_poststate(fcx.ccx, test)) ||
-                        changed;
+            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.a, pres);
+                changed = changed0;
+            }
+
+            changed =
+                find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body),
+                                         test) || changed;
+
+            if (breaks) {
+                set_poststate_ann(fcx.ccx, a, pres);
+            }
+            else {
+                changed =  extend_poststate_ann(fcx.ccx, a,
+                                            expr_poststate(fcx.ccx, test)) ||
+                    changed;
             }
             ret changed;
         }
@@ -605,7 +696,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
                     || changed;
             ret changed;
         }
-        case (expr_assert(?p, ?a)) { ret pure_exp(fcx.ccx, a, pres); }
+        case (expr_assert(?p, ?a)) {
+            changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+            changed = find_pre_post_state_expr(fcx, pres, p) || changed;
+            changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
+            ret changed;
+        }
         case (expr_check(?p, ?a)) {
             changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
             changed = find_pre_post_state_expr(fcx, pres, p) || changed;
@@ -617,13 +713,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
             ret changed;
         }
         case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) {
-            changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
-            changed = find_pre_post_state_expr(fcx, pres, p) || changed;
-            let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
-            changed = gen_poststate(fcx, expr_ann(p), c.node) || changed;
-            
-            changed = join_then_else(fcx, p, conseq, maybe_alt, a)
+            changed = join_then_else(fcx, p, conseq, maybe_alt, a, if_check,
+                                     pres)
                 || changed;
+
             ret changed;
         }
         case (expr_break(?a)) { ret pure_exp(fcx.ccx, a, pres); }
@@ -651,14 +744,18 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
 fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
     auto changed = false;
     auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
-    log "*At beginning: stmt = ";
-    log_stmt(*s);
-    log "*prestate = ";
-    log bitv::to_str(stmt_ann.states.prestate);
-    log "*poststate =";
-    log bitv::to_str(stmt_ann.states.poststate);
-    log "*changed =";
-    log changed;
+
+    /*
+    log_err "*At beginning: stmt = ";
+    log_stmt_err(*s);
+    log_err "*prestate = ";
+    log_err bitv::to_str(stmt_ann.states.prestate);
+    log_err "*poststate =";
+    log_err bitv::to_str(stmt_ann.states.poststate);
+    log_err "*changed =";
+    log_err changed;
+    */
+
     alt (s.node) {
         case (stmt_decl(?adecl, ?a)) {
             alt (adecl.node) {
@@ -770,27 +867,21 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) ->
             post = expr_poststate(fcx.ccx, e);
         }
     }
+
+    set_prestate_ann(fcx.ccx, b.node.a, pres0);
+    set_poststate_ann(fcx.ccx, b.node.a, post);
+    
     /*
-    log_err("block:");
+    log_err "For block:";
     log_block_err(b);
-    log_err("has non-local exits?");
-    log_err(has_nonlocal_exits(b));
+    log_err "poststate = ";
+    log_states_err(block_states(fcx.ccx, b));
+    log_err "pres0:";
+    log_bitv_err(fcx, pres0);
+    log_err "post:";
+    log_bitv_err(fcx, post);
     */
 
-    /* conservative approximation: if a block contains a break
-       or cont, we assume nothing about the poststate */
-
-    if (has_nonlocal_exits(b)) { post = pres0; }
-    set_prestate_ann(fcx.ccx, b.node.a, pres0);
-    set_poststate_ann(fcx.ccx, b.node.a, post);
-    log "For block:";
-    log_block(b);
-    log "poststate = ";
-    log_states(block_states(fcx.ccx, b));
-    log "pres0:";
-    log_bitv(fcx, pres0);
-    log "post:";
-    log_bitv(fcx, post);
     ret changed;
 }
 
@@ -812,8 +903,10 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
             // function with some other return type
             if (!type_is_nil(fcx.ccx.tcx, tailty) &&
                     !type_is_bot(fcx.ccx.tcx, tailty)) {
-                set_poststate_ann(fcx.ccx, tailann,
-                                  false_postcond(num_local_vars));
+                auto p = false_postcond(num_local_vars);
+                set_poststate_ann(fcx.ccx, tailann, p);
+                // be sure to set the block poststate to the same thing
+                set_poststate_ann(fcx.ccx, f.body.node.a, p);
                 alt (fcx.enclosing.cf) {
                     case (noreturn) {
                         kill_poststate(fcx, tailann,