Started adding support for return checking and non-returning function annotations

* Reorganized typestate into several modules.

* Made typestate check that any function with a non-nil return type
  returns a value. For now, the check is a warning and not an error
  (see next item).

* Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and
  fail that don't locally return a value that can be inspected. "bot"
  is distinct from "nil". There is no concrete syntax for _|_, while
  the concrete syntax for the nil type is ().

* Added support to the parser for a ! annotation on functions whose
  result type is _|_. Such a function is required to have either a
  fail or a call to another ! function that is reached in all control
  flow paths. The point of this annotation is to mark functions like
  unimpl() and span_err(), so that an alt with a call to err() in one
  case isn't a false positive for the return-value checker. I haven't
  actually annotated anything with it yet.

* Random bugfixes:

* * Fixed bug in trans::trans_binary that was throwing away the
    cleanups for nested subexpressions of an and or or
    (tests: box-inside-if and box-inside-if2).

** In typeck, unify the expected type arguments of a tag with the
   actual specified arguments.

19 files changed, 3205 insertions, 51 deletions

diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs
index d538e1711a6..d9d5633d05d 100644
--- a/src/comp/driver/rustc.rs
+++ b/src/comp/driver/rustc.rs
@@ -9,7 +9,7 @@ import middle::trans;
 import middle::resolve;
 import middle::ty;
 import middle::typeck;
-import middle::typestate_check;
+import middle::tstate::ck;
 import back::link;
 import lib::llvm;
 import util::common;
@@ -105,7 +105,8 @@ fn compile_input(session::session sess,
 
     if (sess.get_opts().run_typestate) {
         crate = time(time_passes, "typestate checking",
-                     bind typestate_check::check_crate(crate, def_map));
+                     bind middle::tstate::ck::check_crate(node_type_table,
+                                                          ty_cx, crate));
     }
 
     auto llmod = time[llvm::ModuleRef](time_passes, "translation",
diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index d795d6c2363..5dfc2d8ddfa 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -1,4 +1,3 @@
-
 import std::map::hashmap;
 import std::option;
 import std::_str;
@@ -7,7 +6,7 @@ import util::common::span;
 import util::common::spanned;
 import util::common::ty_mach;
 import util::common::filename;
-import util::typestate_ann::ts_ann;
+import middle::tstate::ann::ts_ann;
 
 type ident = str;
 
@@ -323,6 +322,12 @@ type ty_method = rec(proto proto, ident ident,
 type ty = spanned[ty_];
 tag ty_ {
     ty_nil;
+    ty_bot; /* return type of ! functions and type of
+             ret/fail/break/cont. there is no syntax
+             for this type. */
+    /* bot represents the value of functions that don't return a value
+       locally to their context. in contrast, things like log that do
+       return, but don't return a meaningful value, have result type nil. */
     ty_bool;
     ty_int;
     ty_uint;
@@ -354,12 +359,19 @@ type constr = spanned[constr_];
 type arg = rec(mode mode, @ty ty, ident ident, def_id id);
 type fn_decl = rec(vec[arg] inputs,
                    @ty output,
-                   purity purity);
+                   purity purity,
+                   controlflow cf);
 tag purity {
     pure_fn;   // declared with "pred"
     impure_fn; // declared with "fn"
 }
 
+tag controlflow {
+    noreturn; // functions with return type _|_ that always
+              // raise an error or exit (i.e. never return to the caller)
+    return;  // everything else
+}
+
 type _fn = rec(fn_decl decl,
                proto proto,
                block body);
diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs
index d0b49b10637..63270579075 100644
--- a/src/comp/front/parser.rs
+++ b/src/comp/front/parser.rs
@@ -23,6 +23,11 @@ tag file_type {
     SOURCE_FILE;
 }
 
+tag ty_or_bang {
+    a_ty(@ast::ty);
+    a_bang;
+}
+
 state type parser =
     state obj {
           fn peek() -> token::token;
@@ -448,6 +453,13 @@ fn parse_ty_constrs(@ast::ty t, parser p) -> @ast::ty {
    ret t;
 }
 
+fn parse_ty_or_bang(parser p) -> ty_or_bang {
+    alt (p.peek()) {
+        case (token::NOT) { p.bump(); ret a_bang; }
+        case (_)         { ret a_ty(parse_ty(p)); }
+    }
+}
+
 fn parse_ty(parser p) -> @ast::ty {
     auto lo = p.get_lo_pos();
     auto hi = lo;
@@ -1713,7 +1725,7 @@ fn parse_fn_decl(parser p, ast::purity purity) -> ast::fn_decl {
          some(token::COMMA),
          pf, p);
 
-    let @ast::ty output;
+    let ty_or_bang res;
 
     // FIXME: dropping constrs on the floor at the moment.
     // pick them up when they're used by typestate pass.
@@ -1721,12 +1733,23 @@ fn parse_fn_decl(parser p, ast::purity purity) -> ast::fn_decl {
 
     if (p.peek() == token::RARROW) {
         p.bump();
-        output = parse_ty(p);
+        res = parse_ty_or_bang(p);
     } else {
-        output = @spanned(inputs.span.lo, inputs.span.hi, ast::ty_nil);
+        res = a_ty(@spanned(inputs.span.lo, inputs.span.hi, ast::ty_nil));
+    }
+
+    alt (res) {
+        case (a_ty(?t)) {
+            ret rec(inputs=inputs.node, output=t,
+              purity=purity, cf=ast::return);
+        }
+        case (a_bang) {
+            ret rec(inputs=inputs.node,
+                    output=@spanned(p.get_lo_pos(),
+                                    p.get_hi_pos(), ast::ty_bot),
+                    purity=purity, cf=ast::noreturn);
+        }
     }
-    // FIXME
-    ret rec(inputs=inputs.node, output=output, purity=purity);
 }
 
 fn parse_fn(parser p, ast::proto proto, ast::purity purity) -> ast::_fn {
@@ -1778,11 +1801,12 @@ fn parse_dtor(parser p) -> @ast::method {
     let vec[ast::arg] inputs = vec();
     let @ast::ty output = @spanned(lo, lo, ast::ty_nil);
     let ast::fn_decl d = rec(inputs=inputs,
-                            output=output,
-                            purity=ast::impure_fn);
+                             output=output,
+                             purity=ast::impure_fn,
+                             cf=ast::return); 
     let ast::_fn f = rec(decl = d,
-                        proto = ast::proto_fn,
-                        body = b);
+                         proto = ast::proto_fn,
+                         body = b);
     let ast::method_ m = rec(ident="drop",
                             meth=f,
                             id=p.next_def_id(),
diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index 7a9a67ddfca..81675fbeedf 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -7,13 +7,14 @@ import util::common::new_str_hash;
 import util::common::spanned;
 import util::common::span;
 import util::common::ty_mach;
-import util::typestate_ann::ts_ann;
+import middle::tstate::ann::ts_ann;
 
 import front::ast;
 import front::ast::fn_decl;
 import front::ast::ident;
 import front::ast::path;
 import front::ast::mutability;
+import front::ast::controlflow;
 import front::ast::ty;
 import front::ast::expr;
 import front::ast::stmt;
@@ -44,6 +45,7 @@ type ast_fold[ENV] =
 
      // Type folds.
      (fn(&ENV e, &span sp) -> @ty)                fold_ty_nil,
+     (fn(&ENV e, &span sp) -> @ty)                fold_ty_bot,
      (fn(&ENV e, &span sp) -> @ty)                fold_ty_bool,
      (fn(&ENV e, &span sp) -> @ty)                fold_ty_int,
      (fn(&ENV e, &span sp) -> @ty)                fold_ty_uint,
@@ -314,7 +316,7 @@ type ast_fold[ENV] =
      (fn(&ENV e,
          &vec[arg] inputs,
          &@ty output,
-         &purity p) -> ast::fn_decl)              fold_fn_decl,
+         &purity p, &controlflow c) -> ast::fn_decl) fold_fn_decl,
 
      (fn(&ENV e, &ast::_mod m) -> ast::_mod)      fold_mod,
 
@@ -375,6 +377,7 @@ fn fold_ty[ENV](&ENV env, &ast_fold[ENV] fld, &@ty t) -> @ty {
 
     alt (t.node) {
         case (ast::ty_nil) { ret fld.fold_ty_nil(env_, t.span); }
+        case (ast::ty_bot) { ret fld.fold_ty_bot(env_, t.span); }
         case (ast::ty_bool) { ret fld.fold_ty_bool(env_, t.span); }
         case (ast::ty_int) { ret fld.fold_ty_int(env_, t.span); }
         case (ast::ty_uint) { ret fld.fold_ty_uint(env_, t.span); }
@@ -926,7 +929,7 @@ fn fold_fn_decl[ENV](&ENV env, &ast_fold[ENV] fld,
         inputs += vec(fold_arg(env, fld, a));
     }
     auto output = fold_ty[ENV](env, fld, decl.output);
-    ret fld.fold_fn_decl(env, inputs, output, decl.purity);
+    ret fld.fold_fn_decl(env, inputs, output, decl.purity, decl.cf);
 }
 
 fn fold_fn[ENV](&ENV env, &ast_fold[ENV] fld, &ast::_fn f) -> ast::_fn {
@@ -1202,6 +1205,10 @@ fn identity_fold_ty_nil[ENV](&ENV env, &span sp) -> @ty {
     ret @respan(sp, ast::ty_nil);
 }
 
+fn identity_fold_ty_bot[ENV](&ENV env, &span sp) -> @ty {
+    ret @respan(sp, ast::ty_bot);
+}
+
 fn identity_fold_ty_bool[ENV](&ENV env, &span sp) -> @ty {
     ret @respan(sp, ast::ty_bool);
 }
@@ -1622,8 +1629,8 @@ fn identity_fold_block[ENV](&ENV e, &span sp, &ast::block_ blk) -> block {
 fn identity_fold_fn_decl[ENV](&ENV e,
                               &vec[arg] inputs,
                               &@ty output,
-                              &purity p) -> ast::fn_decl {
-    ret rec(inputs=inputs, output=output, purity=p);
+                              &purity p, &controlflow c) -> ast::fn_decl {
+    ret rec(inputs=inputs, output=output, purity=p, cf=c);
 }
 
 fn identity_fold_fn[ENV](&ENV e,
@@ -1722,6 +1729,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
          fold_path       = bind identity_fold_path[ENV](_,_,_),
 
          fold_ty_nil     = bind identity_fold_ty_nil[ENV](_,_),
+         fold_ty_bot     = bind identity_fold_ty_bot[ENV](_,_),
          fold_ty_bool    = bind identity_fold_ty_bool[ENV](_,_),
          fold_ty_int     = bind identity_fold_ty_int[ENV](_,_),
          fold_ty_uint    = bind identity_fold_ty_uint[ENV](_,_),
@@ -1821,7 +1829,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
          fold_ann = bind identity_fold_ann[ENV](_,_),
 
          fold_fn = bind identity_fold_fn[ENV](_,_,_,_),
-         fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_,_),
+         fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_,_,_),
          fold_mod = bind identity_fold_mod[ENV](_,_),
          fold_native_mod = bind identity_fold_native_mod[ENV](_,_),
          fold_crate = bind identity_fold_crate[ENV](_,_,_,_),
diff --git a/src/comp/middle/resolve.rs b/src/comp/middle/resolve.rs
index f530d3f412f..8d27d5cd4c9 100644
--- a/src/comp/middle/resolve.rs
+++ b/src/comp/middle/resolve.rs
@@ -10,7 +10,7 @@ import util::common::new_int_hash;
 import util::common::new_uint_hash;
 import util::common::new_str_hash;
 import util::common::span;
-import util::typestate_ann::ts_ann;
+import middle::tstate::ann::ts_ann;
 import std::map::hashmap;
 import std::list::list;
 import std::list::nil;
diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index aaf65fe270e..869ad125fcc 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -757,6 +757,7 @@ fn type_of_inner(&@crate_ctxt cx, &ty::t t) -> TypeRef {
     alt (ty::struct(cx.tcx, t)) {
         case (ty::ty_native) { llty = T_ptr(T_i8()); }
         case (ty::ty_nil) { llty = T_nil(); }
+        case (ty::ty_bot) { llty = T_nil(); } /* ...I guess? */
         case (ty::ty_bool) { llty = T_bool(); }
         case (ty::ty_int) { llty = T_int(); }
         case (ty::ty_float) { llty = T_float(); }
@@ -3186,8 +3187,8 @@ fn copy_ty(&@block_ctxt cx,
     if (ty::type_is_scalar(cx.fcx.lcx.ccx.tcx, t) ||
             ty::type_is_native(cx.fcx.lcx.ccx.tcx, t)) {
         ret res(cx, cx.build.Store(src, dst));
-
-    } else if (ty::type_is_nil(cx.fcx.lcx.ccx.tcx, t)) {
+    } else if (ty::type_is_nil(cx.fcx.lcx.ccx.tcx, t) ||
+               ty::type_is_bot(cx.fcx.lcx.ccx.tcx, t)) {
         ret res(cx, C_nil());
 
     } else if (ty::type_is_boxed(cx.fcx.lcx.ccx.tcx, t)) {
@@ -3552,6 +3553,8 @@ fn autoderef(&@block_ctxt cx, ValueRef v, &ty::t t) -> result {
             }
         }
     }
+
+    fail; // fools the return-checker
 }
 
 fn autoderefed_ty(&@crate_ctxt ccx, &ty::t t) -> ty::t {
@@ -3567,6 +3570,8 @@ fn autoderefed_ty(&@crate_ctxt ccx, &ty::t t) -> ty::t {
             }
         }
     }
+
+    fail; // fools the return-checker
 }
 
 fn trans_binary(&@block_ctxt cx, ast::binop op,
@@ -3591,12 +3596,17 @@ fn trans_binary(&@block_ctxt cx, ast::binop op,
             auto lhs_false_cx = new_scope_block_ctxt(cx, "lhs false");
             auto lhs_false_res = res(lhs_false_cx, C_bool(false));
 
+            // The following line ensures that any cleanups for rhs
+            // are done within the block for rhs. This is necessary 
+            // because and/or are lazy. So the rhs may never execute,
+            // and the cleanups can't be pushed into later code.
+            auto rhs_bcx = trans_block_cleanups(rhs_res.bcx, rhs_cx);
+
             lhs_res.bcx.build.CondBr(lhs_res.val,
                                      rhs_cx.llbb,
                                      lhs_false_cx.llbb);
-
             ret join_results(cx, T_bool(),
-                             vec(lhs_false_res, rhs_res));
+                  vec(lhs_false_res, rec(bcx=rhs_bcx with rhs_res)));
         }
 
         case (ast::or) {
@@ -3615,12 +3625,15 @@ fn trans_binary(&@block_ctxt cx, ast::binop op,
             auto lhs_true_cx = new_scope_block_ctxt(cx, "lhs true");
             auto lhs_true_res = res(lhs_true_cx, C_bool(true));
 
+            // see the and case for an explanation
+            auto rhs_bcx = trans_block_cleanups(rhs_res.bcx, rhs_cx);
+
             lhs_res.bcx.build.CondBr(lhs_res.val,
                                      lhs_true_cx.llbb,
                                      rhs_cx.llbb);
 
             ret join_results(cx, T_bool(),
-                             vec(lhs_true_res, rhs_res));
+                  vec(lhs_true_res, rec(bcx=rhs_bcx with rhs_res)));
         }
 
         case (_) {
@@ -4984,6 +4997,8 @@ fn trans_bind(&@block_ctxt cx, &@ast::expr f,
             ret res(bcx, pair_v);
         }
     }
+
+    fail; // sadly needed b/c the compiler doesn't know yet that unimpl fails
 }
 
 fn trans_arg_expr(&@block_ctxt cx,
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/middle/tstate/ann.rs
index 249dc5ca61d..6dbc3970a25 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -111,13 +111,13 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
 
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
-fn set_precondition(&ts_ann a, &precond p) -> () {
+fn set_precondition(@ts_ann a, &precond p) -> () {
   bitv::copy(a.conditions.precondition, p);
 }
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
-fn set_postcondition(&ts_ann a, &postcond p) -> () {
+fn set_postcondition(@ts_ann a, &postcond p) -> () {
   bitv::copy(a.conditions.postcondition, p);
 }
 
@@ -158,6 +158,10 @@ fn ann_prestate(&ts_ann a) -> prestate {
   ret a.states.prestate;
 }
 
+fn ann_poststate(&ts_ann a) -> poststate {
+  ret a.states.poststate;
+}
+
 fn pp_clone(&pre_and_post p) -> pre_and_post {
   ret rec(precondition=clone(p.precondition),
           postcondition=clone(p.postcondition));
diff --git a/src/comp/middle/tstate/annotate.rs b/src/comp/middle/tstate/annotate.rs
new file mode 100644
index 00000000000..b2d35a401ee
--- /dev/null
+++ b/src/comp/middle/tstate/annotate.rs
@@ -0,0 +1,492 @@
+import std::_vec;
+import std::option;
+import std::option::some;
+import std::option::none;
+
+import front::ast;
+
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ann;
+import front::ast::item;
+import front::ast::_fn;
+import front::ast::_mod;
+import front::ast::crate;
+import front::ast::_obj;
+import front::ast::ty_param;
+import front::ast::item_fn;
+import front::ast::item_obj;
+import front::ast::item_ty;
+import front::ast::item_tag;
+import front::ast::item_const;
+import front::ast::item_mod;
+import front::ast::item_native_mod;
+import front::ast::expr;
+import front::ast::elt;
+import front::ast::field;
+import front::ast::decl;
+import front::ast::decl_local;
+import front::ast::decl_item;
+import front::ast::initializer;
+import front::ast::local;
+import front::ast::arm;
+import front::ast::expr_call;
+import front::ast::expr_vec;
+import front::ast::expr_tup;
+import front::ast::expr_path;
+import front::ast::expr_field;
+import front::ast::expr_index;
+import front::ast::expr_log;
+import front::ast::expr_block;
+import front::ast::expr_rec;
+import front::ast::expr_if;
+import front::ast::expr_binary;
+import front::ast::expr_unary;
+import front::ast::expr_assign;
+import front::ast::expr_assign_op;
+import front::ast::expr_while;
+import front::ast::expr_do_while;
+import front::ast::expr_alt;
+import front::ast::expr_lit;
+import front::ast::expr_ret;
+import front::ast::expr_self_method;
+import front::ast::expr_bind;
+import front::ast::expr_spawn;
+import front::ast::expr_ext;
+import front::ast::expr_fail;
+import front::ast::expr_break;
+import front::ast::expr_cont;
+import front::ast::expr_send;
+import front::ast::expr_recv;
+import front::ast::expr_put;
+import front::ast::expr_port;
+import front::ast::expr_chan;
+import front::ast::expr_be;
+import front::ast::expr_check;
+import front::ast::expr_assert;
+import front::ast::expr_cast;
+import front::ast::expr_for;
+import front::ast::expr_for_each;
+import front::ast::stmt;
+import front::ast::stmt_decl;
+import front::ast::stmt_expr;
+import front::ast::block;
+import front::ast::block_;
+import front::ast::method;
+
+import middle::fold;
+import middle::fold::respan;
+import middle::fold::new_identity_fold;
+import middle::fold::fold_crate;
+import middle::fold::fold_item;
+import middle::fold::fold_method;
+
+import util::common::uistr;
+import util::common::span;
+import util::common::new_str_hash;
+
+import middle::tstate::aux::fn_info;
+import middle::tstate::aux::fn_info_map;
+import middle::tstate::aux::num_locals;
+import middle::tstate::aux::init_ann;
+import middle::tstate::aux::init_blank_ann;
+import middle::tstate::aux::get_fn_info;
+
+fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &_fn f,
+                vec[ty_param] ty_params, def_id id, ann a) -> @item {
+
+    assert (fm.contains_key(id));
+    auto f_info = fm.get(id);
+
+    log(i + " has " + uistr(num_locals(f_info)) + " local vars");
+
+    auto fld0 = new_identity_fold[fn_info]();
+
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                    with *fld0);
+
+    ret fold_item[fn_info]
+           (f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a))); 
+}
+
+/* FIXME: rewrite this with walk instead of fold */
+
+/* This is painstakingly written as an explicit recursion b/c the
+   standard ast.fold doesn't traverse in the correct order:
+   consider
+   fn foo() {
+      fn bar() {
+        auto x = 5;
+        log(x);
+      }
+   }
+   With fold, first bar() would be processed and its subexps would
+   correctly be annotated with length-1 bit vectors.
+   But then, the process would be repeated with (fn bar()...) as
+   a subexp of foo, which has 0 local variables -- so then
+   the body of bar() would be incorrectly annotated with length-0 bit
+   vectors. */
+fn annotate_exprs(&fn_info_map fm, &vec[@expr] es) -> vec[@expr] {
+    fn one(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind one(fm,_);
+    ret _vec::map[@expr, @expr](f, es);
+}
+fn annotate_elts(&fn_info_map fm, &vec[elt] es) -> vec[elt] {
+    fn one(fn_info_map fm, &elt e) -> elt {
+        ret rec(mut=e.mut,
+                expr=annotate_expr(fm, e.expr));
+    }
+    auto f = bind one(fm,_);
+    ret _vec::map[elt, elt](f, es);
+}
+fn annotate_fields(&fn_info_map fm, &vec[field] fs) -> vec[field] {
+    fn one(fn_info_map fm, &field f) -> field {
+        ret rec(mut=f.mut,
+                 ident=f.ident,
+                 expr=annotate_expr(fm, f.expr));
+    }
+    auto f = bind one(fm,_);
+    ret _vec::map[field, field](f, fs);
+}
+fn annotate_option_exp(&fn_info_map fm, &option::t[@expr] o)
+  -> option::t[@expr] {
+    fn one(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind one(fm,_);
+    ret option::map[@expr, @expr](f, o);
+}
+fn annotate_option_exprs(&fn_info_map fm, &vec[option::t[@expr]] es)
+  -> vec[option::t[@expr]] {
+    fn one(fn_info_map fm, &option::t[@expr] o) -> option::t[@expr] {
+        ret annotate_option_exp(fm, o);
+    }
+    auto f = bind one(fm,_);
+    ret _vec::map[option::t[@expr], option::t[@expr]](f, es);
+}
+fn annotate_decl(&fn_info_map fm, &@decl d) -> @decl {
+    auto d1 = d.node;
+    alt (d.node) {
+        case (decl_local(?l)) {
+            alt(l.init) {
+                case (some[initializer](?init)) {
+                    let option::t[initializer] an_i =
+                        some[initializer]
+                          (rec(expr=annotate_expr(fm, init.expr)
+                                 with init));
+                    let @local new_l = @rec(init=an_i with *l);
+                    d1 = decl_local(new_l);
+                }
+                case (_) { /* do nothing */ }
+            }
+        }
+        case (decl_item(?item)) {
+            d1 = decl_item(annotate_item(fm, item));
+        }
+    }
+    ret @respan(d.span, d1);
+}
+fn annotate_alts(&fn_info_map fm, &vec[arm] alts) -> vec[arm] {
+    fn one(fn_info_map fm, &arm a) -> arm {
+        ret rec(pat=a.pat,
+                 block=annotate_block(fm, a.block));
+    }
+    auto f = bind one(fm,_);
+    ret _vec::map[arm, arm](f, alts);
+
+}
+fn annotate_expr(&fn_info_map fm, &@expr e) -> @expr {
+    auto e1 = e.node;
+    alt (e.node) {
+        case (expr_vec(?es, ?m, ?a)) {
+            e1 = expr_vec(annotate_exprs(fm, es), m, a);
+        }
+        case (expr_tup(?es, ?a)) {
+            e1 = expr_tup(annotate_elts(fm, es), a);
+        }
+        case (expr_rec(?fs, ?maybe_e, ?a)) {
+            e1 = expr_rec(annotate_fields(fm, fs),
+                          annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_call(?e, ?es, ?a)) {
+            e1 = expr_call(annotate_expr(fm, e),
+                          annotate_exprs(fm, es), a);
+        }
+        case (expr_self_method(_,_)) {
+            // no change
+        }
+        case (expr_bind(?e, ?maybe_es, ?a)) {
+            e1 = expr_bind(annotate_expr(fm, e),
+                           annotate_option_exprs(fm, maybe_es),
+                           a);
+        }
+        case (expr_spawn(?s, ?maybe_s, ?e, ?es, ?a)) {
+            e1 = expr_spawn(s, maybe_s, annotate_expr(fm, e),
+                            annotate_exprs(fm, es), a);
+        }
+        case (expr_binary(?bop, ?w, ?x, ?a)) {
+            e1 = expr_binary(bop, annotate_expr(fm, w),
+                             annotate_expr(fm, x), a);
+        }
+        case (expr_unary(?uop, ?w, ?a)) {
+            e1 = expr_unary(uop, annotate_expr(fm, w), a);
+        }
+        case (expr_lit(_,_)) {
+            /* no change */
+        }
+        case (expr_cast(?e,?t,?a)) {
+            e1 = expr_cast(annotate_expr(fm, e), t, a);
+        }
+        case (expr_if(?e, ?b, ?maybe_e, ?a)) {
+            e1 = expr_if(annotate_expr(fm, e),
+                         annotate_block(fm, b),
+                         annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_while(?e, ?b, ?a)) {
+            e1 = expr_while(annotate_expr(fm, e),
+                            annotate_block(fm, b), a);
+        }
+        case (expr_for(?d, ?e, ?b, ?a)) {
+            e1 = expr_for(annotate_decl(fm, d),
+                          annotate_expr(fm, e),
+                          annotate_block(fm, b), a);
+        }
+        case (expr_for_each(?d, ?e, ?b, ?a)) {
+            e1 = expr_for_each(annotate_decl(fm, d),
+                          annotate_expr(fm, e),
+                          annotate_block(fm, b), a);
+        }
+        case (expr_do_while(?b, ?e, ?a)) {
+            e1 = expr_do_while(annotate_block(fm, b),
+                               annotate_expr(fm, e), a);
+        }
+        case (expr_alt(?e, ?alts, ?a)) {
+            e1 = expr_alt(annotate_expr(fm, e),
+                          annotate_alts(fm, alts), a);
+        }
+        case (expr_block(?b, ?a)) {
+            e1 = expr_block(annotate_block(fm, b), a);
+        }
+        case (expr_assign(?l, ?r, ?a)) {
+            e1 = expr_assign(annotate_expr(fm, l), annotate_expr(fm, r), a);
+        }
+        case (expr_assign_op(?bop, ?l, ?r, ?a)) {
+            e1 = expr_assign_op(bop,
+               annotate_expr(fm, l), annotate_expr(fm, r), a);
+        }
+        case (expr_send(?l, ?r, ?a)) {
+            e1 = expr_send(annotate_expr(fm, l),
+                           annotate_expr(fm, r), a);
+        }
+        case (expr_recv(?l, ?r, ?a)) {
+           e1 = expr_recv(annotate_expr(fm, l),
+                           annotate_expr(fm, r), a);
+        }
+        case (expr_field(?e, ?i, ?a)) {
+            e1 = expr_field(annotate_expr(fm, e),
+                            i, a);
+        }
+        case (expr_index(?e, ?sub, ?a)) {
+            e1 = expr_index(annotate_expr(fm, e),
+                            annotate_expr(fm, sub), a);
+        }
+        case (expr_path(_,_)) {
+            /* no change */
+        }
+        case (expr_ext(?p, ?es, ?s_opt, ?e, ?a)) {
+            e1 = expr_ext(p, annotate_exprs(fm, es),
+                          s_opt,
+                          annotate_expr(fm, e), a);
+        }
+        /* no change, next 3 cases */
+        case (expr_fail(_)) { }
+        case (expr_break(_)) { }
+        case (expr_cont(_)) { }
+        case (expr_ret(?maybe_e, ?a)) {
+            e1 = expr_ret(annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_put(?maybe_e, ?a)) {
+            e1 = expr_put(annotate_option_exp(fm, maybe_e), a);
+        }
+        case (expr_be(?e, ?a)) {
+            e1 = expr_be(annotate_expr(fm, e), a);
+        }
+        case (expr_log(?n, ?e, ?a)) {
+            e1 = expr_log(n, annotate_expr(fm, e), a);
+        }
+        case (expr_assert(?e, ?a)) {
+            e1 = expr_assert(annotate_expr(fm, e), a);
+        }
+        case (expr_check(?e, ?a)) {
+            e1 = expr_check(annotate_expr(fm, e), a);
+        }
+        case (expr_port(_)) { /* no change */ }
+        case (expr_chan(?e, ?a)) {
+            e1 = expr_chan(annotate_expr(fm, e), a);
+        }
+    }
+    ret @respan(e.span, e1);
+}
+
+fn annotate_stmt(&fn_info_map fm, &@stmt s) -> @stmt {
+    alt (s.node) {
+        case (stmt_decl(?d, ?a)) {
+            ret @respan(s.span, stmt_decl(annotate_decl(fm, d), a));
+        }
+        case (stmt_expr(?e, ?a)) {
+            ret @respan(s.span, stmt_expr(annotate_expr(fm, e), a));
+        }
+    }
+}
+fn annotate_block(&fn_info_map fm, &block b) -> block {
+    let vec[@stmt] new_stmts = vec();
+   
+    for (@stmt s in b.node.stmts) {
+        auto new_s = annotate_stmt(fm, s);
+        _vec::push[@stmt](new_stmts, new_s);
+    }
+    fn ann_e(fn_info_map fm, &@expr e) -> @expr {
+        ret annotate_expr(fm, e);
+    }
+    auto f = bind ann_e(fm,_);
+
+    auto new_e = option::map[@expr, @expr](f, b.node.expr);
+
+    ret respan(b.span,
+          rec(stmts=new_stmts, expr=new_e with b.node));
+}
+fn annotate_fn(&fn_info_map fm, &_fn f) -> _fn {
+    // subexps have *already* been annotated based on
+    // f's number-of-locals
+    ret rec(body=annotate_block(fm, f.body) with f);
+}
+fn annotate_mod(&fn_info_map fm, &_mod m) -> _mod {
+    let vec[@item] new_items = vec();
+   
+    for (@item i in m.items) {
+        auto new_i = annotate_item(fm, i);
+        _vec::push[@item](new_items, new_i);
+    }
+    ret rec(items=new_items with m);
+}
+fn annotate_method(&fn_info_map fm, &@method m) -> @method {
+    auto f_info = get_fn_info(fm, m.node.id);
+    auto fld0 = new_identity_fold[fn_info]();
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                with *fld0);
+    auto outer = fold_method[fn_info](f_info, fld0, m);
+    auto new_fn = annotate_fn(fm, outer.node.meth);
+    ret @respan(m.span,
+                rec(meth=new_fn with m.node));
+}
+
+fn annotate_obj(&fn_info_map fm, &_obj o) -> _obj {
+    fn one(fn_info_map fm, &@method m) -> @method {
+        ret annotate_method(fm, m);
+    }
+    auto f = bind one(fm,_);
+    auto new_methods = _vec::map[@method, @method](f, o.methods);
+    auto new_dtor    = option::map[@method, @method](f, o.dtor);
+    ret rec(methods=new_methods, dtor=new_dtor with o);
+}
+
+ 
+// Only annotates the components of the item recursively.
+fn annotate_item_inner(&fn_info_map fm, &@item item) -> @item {
+    alt (item.node) {
+        /* FIXME can't skip this case -- exprs contain blocks contain stmts,
+         which contain decls */
+        case (item_const(_,_,_,_,_)) {
+            // this has already been annotated by annotate_item
+            ret item;
+        }
+        case (item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
+            ret @respan(item.span,
+                       item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
+        }
+        case (item_mod(?ident, ?mm, ?id)) {
+            ret @respan(item.span,
+                       item_mod(ident, annotate_mod(fm, mm), id));
+        }
+        case (item_native_mod(?ident, ?mm, ?id)) {
+            ret item;
+        }
+        case (item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
+            ret @respan(item.span,
+              item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
+        }
+    } 
+}
+
+fn annotate_item(&fn_info_map fm, &@item item) -> @item {
+    // Using a fold, recursively set all anns in this item
+    // to be blank.
+    // *Then*, call annotate_item recursively to do the right
+    // thing for any nested items inside this one.
+    
+    alt (item.node) {
+        case (item_const(_,_,_,_,_)) {
+            auto fld0 = new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            ret fold_item[()]((), fld0, item);
+        }
+        case (item_fn(?i,?ff,?tps,?id,?ann)) {
+            auto f_info = get_fn_info(fm, id);
+            auto fld0 = new_identity_fold[fn_info]();
+            fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                        with *fld0);
+            auto outer = fold_item[fn_info](f_info, fld0, item);
+            // now recurse into any nested items
+            ret annotate_item_inner(fm, outer);
+         }
+        case (item_mod(?i, ?mm, ?id)) {
+            auto fld0 = new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+        case (item_native_mod(?i, ?nm, ?id)) {
+            ret item;
+        }
+        case (item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (item_obj(?i,?ob,?tps,?odid,?ann)) {
+            auto fld0 = new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+    }
+}
+
+fn annotate_module(&fn_info_map fm, &_mod module) -> _mod {
+    let vec[@item] new_items = vec();
+   
+    for (@item i in module.items) {
+        auto new_item = annotate_item(fm, i);
+        _vec::push[@item](new_items, new_item);
+    }
+
+    ret rec(items = new_items with module);
+}
+
+fn annotate_crate(&fn_info_map fm, &@crate crate) -> @crate {
+    ret @respan(crate.span,
+               rec(module = annotate_module(fm, crate.node.module)
+                   with crate.node));
+}
diff --git a/src/comp/middle/tstate/aux.rs b/src/comp/middle/tstate/aux.rs
new file mode 100644
index 00000000000..45d1aed94a1
--- /dev/null
+++ b/src/comp/middle/tstate/aux.rs
@@ -0,0 +1,482 @@
+import std::bitv;
+import std::_vec::len;
+import std::_vec::pop;
+import std::option;
+import std::option::none;
+import std::option::some;
+import std::option::maybe;
+
+import front::ast;
+import front::ast::ann_tag;
+import front::ast::def;
+import front::ast::def_fn;
+import front::ast::_fn;
+import front::ast::def_obj_field;
+import front::ast::def_id;
+import front::ast::expr_path;
+import front::ast::ident;
+import front::ast::controlflow;
+import front::ast::ann;
+import front::ast::ann_none;
+import front::ast::ann_type;
+import front::ast::ts_ann;
+import front::ast::stmt;
+import front::ast::expr;
+import front::ast::block;
+import front::ast::block_;
+import front::ast::stmt_decl;
+import front::ast::stmt_expr;
+import front::ast::stmt_crate_directive;
+import front::ast::return;
+import front::ast::expr_field;
+
+import middle::ty::expr_ann;
+import middle::fold;
+import middle::fold::respan;
+import middle::fold::new_identity_fold;
+import middle::fold::fold_block;
+
+import util::common;
+import util::common::span;
+import util::common::log_block;
+import util::common::new_def_hash;
+import util::common::log_expr_err;
+import util::common::uistr;
+
+import tstate::ann::pre_and_post;
+import tstate::ann::pre_and_post_state;
+import tstate::ann::empty_ann;
+import tstate::ann::prestate;
+import tstate::ann::poststate;
+import tstate::ann::precond;
+import tstate::ann::postcond;
+import tstate::ann::empty_states;
+import tstate::ann::pps_len;
+import tstate::ann::set_prestate;
+import tstate::ann::set_poststate;
+import tstate::ann::extend_prestate;
+import tstate::ann::extend_poststate;
+import tstate::ann::set_precondition;
+import tstate::ann::set_postcondition;
+
+/* logging funs */
+
+fn bitv_to_str(fn_info enclosing, bitv::t v) -> str {
+  auto s = "";
+
+  for each (@tup(def_id, tup(uint, ident)) p in enclosing.vars.items()) {
+    if (bitv::get(v, p._1._0)) {
+      s += " " + p._1._1 + " ";
+    }
+  }
+  ret s;
+}
+
+fn log_bitv(fn_info enclosing, bitv::t v) {
+    log(bitv_to_str(enclosing, v));
+}
+
+fn log_bitv_err(fn_info enclosing, bitv::t v) {
+    log_err(bitv_to_str(enclosing, v));
+}
+
+fn tos (vec[uint] v) -> str {
+  auto res = "";
+  for (uint i in v) {
+    if (i == 0u) {
+      res += "0";
+    }
+    else {
+      res += "1";
+    }
+  }
+  ret res;
+}
+
+fn log_cond(vec[uint] v) -> () {
+    log(tos(v));
+}
+fn log_cond_err(vec[uint] v) -> () {
+    log_err(tos(v));
+}
+
+fn log_pp(&pre_and_post pp) -> () {
+  auto p1 = bitv::to_vec(pp.precondition);
+  auto p2 = bitv::to_vec(pp.postcondition);
+  log("pre:");
+  log_cond(p1);
+  log("post:");
+  log_cond(p2);
+}
+
+fn log_pp_err(&pre_and_post pp) -> () {
+  auto p1 = bitv::to_vec(pp.precondition);
+  auto p2 = bitv::to_vec(pp.postcondition);
+  log_err("pre:");
+  log_cond_err(p1);
+  log_err("post:");
+  log_cond_err(p2);
+}
+
+fn log_states(&pre_and_post_state pp) -> () {
+  auto p1 = bitv::to_vec(pp.prestate);
+  auto p2 = bitv::to_vec(pp.poststate);
+  log("prestate:");
+  log_cond(p1);
+  log("poststate:");
+  log_cond(p2);
+}
+
+fn log_states_err(&pre_and_post_state pp) -> () {
+  auto p1 = bitv::to_vec(pp.prestate);
+  auto p2 = bitv::to_vec(pp.poststate);
+  log_err("prestate:");
+  log_cond_err(p1);
+  log_err("poststate:");
+  log_cond_err(p2);
+}
+
+fn print_ident(&ident i) -> () {
+  log(" " + i + " ");
+}
+
+fn print_idents(vec[ident] idents) -> () {
+  if (len[ident](idents) == 0u) {
+    ret;
+  }
+  else {
+    log("an ident: " + pop[ident](idents));
+    print_idents(idents);
+  }
+}
+
+
+/* data structures */
+
+/**********************************************************************/
+/* mapping from variable name (def_id is assumed to be for a local
+   variable in a given function) to bit number 
+   (also remembers the ident for error-logging purposes) */
+type var_info     = tup(uint, ident);
+type fn_info      = rec(@std::map::hashmap[def_id, var_info] vars,
+                        controlflow cf);
+/* mapping from function name to fn_info map */
+type fn_info_map = @std::map::hashmap[def_id, fn_info];
+
+type fn_ctxt    = rec(fn_info enclosing,
+                      def_id id,
+                      ident name,
+                      crate_ctxt ccx);
+
+type crate_ctxt = rec(ty::ctxt tcx,
+                      ty::node_type_table node_types,
+                      fn_info_map fm);
+
+fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
+    assert (fm.contains_key(did));
+    ret fm.get(did);
+}
+
+/********* utils ********/
+
+
+fn ann_to_ts_ann(ann a, uint nv) -> @ts_ann {
+    alt (ann_to_ts_ann_fail(a)) {
+        case (none[@ts_ann])         { ret @empty_ann(nv); }
+        case (some[@ts_ann](?t))     { ret t; }
+    }
+}
+
+
+fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] {
+  alt (a) {
+    case (ann_none(_)) { 
+          log("ann_to_ts_ann_fail: didn't expect ann_none here");
+          fail;
+      }
+    case (ann_type(_,_,_,?ty)) {
+          ret ty;
+      }
+  }
+}
+
+fn ann_to_ts_ann_strict(ann a) -> @ts_ann {
+    alt (ann_to_ts_ann_fail(a)) {
+        case (none[@ts_ann])         {    
+            log("ann_to_ts_ann_fail: didn't expect ann_none here");
+            fail;
+        }
+        case (some[@ts_ann](?t))        {     
+            ret t;
+        }
+    }
+}
+
+fn ann_to_poststate(ann a) -> poststate {
+    ret (ann_to_ts_ann_strict(a)).states.poststate;
+}
+
+fn stmt_to_ann(&stmt s) -> option::t[@ts_ann] {
+  alt (s.node) {
+    case (stmt_decl(_,?a)) {
+        ret ann_to_ts_ann_fail(a);
+    }
+    case (stmt_expr(_,?a)) {
+        ret ann_to_ts_ann_fail(a);
+    }
+    case (stmt_crate_directive(_)) {
+      ret none[@ts_ann];
+    }
+  }
+}
+
+fn stmt_to_ann_strict(&stmt s) -> @ts_ann {
+    alt (stmt_to_ann(s)) {
+        case (none[@ts_ann]) {
+            log_err("stmt_to_ann_strict: didn't expect none here");
+            fail;
+        }
+        case (some[@ts_ann](?a)) { ret a; }
+    }
+}
+
+/* fails if e has no annotation */
+fn expr_states(@expr e) -> pre_and_post_state {
+    ret (ann_to_ts_ann_strict(expr_ann(e)).states);
+}
+
+/* fails if e has no annotation */
+fn expr_pp(@expr e) -> pre_and_post {
+    ret (ann_to_ts_ann_strict(expr_ann(e)).conditions);
+}
+
+fn stmt_pp(&stmt s) -> pre_and_post {
+    ret (stmt_to_ann_strict(s).conditions);
+}
+
+/* fails if b has no annotation */
+fn block_pp(&block b) -> pre_and_post {
+    ret (ann_to_ts_ann_strict(b.node.a).conditions);
+}
+
+fn block_states(&block b) -> pre_and_post_state {
+    ret (ann_to_ts_ann_strict(b.node.a).states);
+}
+
+fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
+  alt (stmt_to_ann(s)) {
+    case (none[@ts_ann]) {
+      ret empty_states(nv);
+    }
+    case (some[@ts_ann](?a)) {
+      ret a.states;
+    }
+  }
+}
+
+fn expr_precond(@expr e) -> precond {
+  ret (expr_pp(e)).precondition;
+}
+
+fn expr_postcond(@expr e) -> postcond {
+  ret (expr_pp(e)).postcondition;
+}
+
+fn expr_prestate(@expr e) -> prestate {
+  ret (expr_states(e)).prestate;
+}
+
+fn expr_poststate(@expr e) -> poststate {
+  ret (expr_states(e)).poststate;
+}
+
+fn stmt_precond(&stmt s) -> precond {
+  ret (stmt_pp(s)).precondition;
+}
+
+fn stmt_postcond(&stmt s) -> postcond {
+  ret (stmt_pp(s)).postcondition;
+}
+
+fn states_to_poststate(&pre_and_post_state ss) -> poststate {
+  ret ss.poststate;
+}
+
+fn stmt_prestate(&stmt s, uint nv) -> prestate {
+  ret (stmt_states(s, nv)).prestate;
+}
+
+fn stmt_poststate(&stmt s, uint nv) -> poststate {
+  ret (stmt_states(s, nv)).poststate;
+}
+
+fn block_postcond(&block b) -> postcond {
+    ret (block_pp(b)).postcondition;
+}
+
+fn block_poststate(&block b) -> poststate {
+    ret (block_states(b)).poststate;
+}
+
+/* returns a new annotation where the pre_and_post is p */
+fn with_pp(ann a, pre_and_post p) -> ann {
+  alt (a) {
+    case (ann_none(_)) {
+      log("with_pp: the impossible happened");
+      fail; /* shouldn't happen b/c code is typechecked */
+    }
+    case (ann_type(?i, ?t, ?ps, _)) {
+        ret (ann_type(i, t, ps,
+                    some[@ts_ann]
+                    (@rec(conditions=p,
+                          states=empty_states(pps_len(p))))));
+    }
+  }
+}
+
+fn set_prestate_ann(&ann a, &prestate pre) -> bool {
+    ret set_prestate(ann_to_ts_ann_strict(a), pre);
+}
+
+
+fn extend_prestate_ann(&ann a, &prestate pre) -> bool {
+    ret extend_prestate(ann_to_ts_ann_strict(a).states.prestate, pre);
+}
+
+fn set_poststate_ann(&ann a, &poststate post) -> bool {
+    ret set_poststate(ann_to_ts_ann_strict(a), post);
+}
+
+fn extend_poststate_ann(&ann a, &poststate post) -> bool {
+    ret extend_poststate(ann_to_ts_ann_strict(a).states.poststate, post);
+}
+
+fn set_pre_and_post(&ann a, &pre_and_post pp) -> () {
+    auto t = ann_to_ts_ann_strict(a);
+    set_precondition(t, pp.precondition);
+    set_postcondition(t, pp.postcondition);
+}
+
+fn pure_exp(&ann a, &prestate p) -> bool {
+  auto changed = false;
+  changed = extend_prestate_ann(a, p) || changed;
+  changed = extend_poststate_ann(a, p) || changed;
+  ret changed;
+}
+
+fn fixed_point_states(&fn_ctxt fcx,
+    fn (&fn_ctxt, &_fn) -> bool f, &_fn start) -> () {
+
+  auto changed = f(fcx, start);
+
+  if (changed) {
+    ret fixed_point_states(fcx, f, start);
+  }
+  else {
+    // we're done!
+    ret;
+  }
+}
+
+fn init_ann(&fn_info fi, &ann a) -> ann {
+    alt (a) {
+        case (ann_none(_)) {
+            //            log("init_ann: shouldn't see ann_none");
+            // fail;
+            log("warning: init_ann: saw ann_none");
+            ret a; // Would be better to fail so we can catch bugs that
+            // result in an uninitialized ann -- but don't want to have to
+            // write code to handle native_mods properly
+        }
+        case (ann_type(?i, ?t, ?ps, _)) {
+            ret ann_type(i, t, ps, some[@ts_ann](@empty_ann(num_locals(fi))));
+        }
+    }
+}
+
+fn init_blank_ann(&() ignore, &ann a) -> ann {
+    alt (a) {
+        case (ann_none(_)) {
+            //            log("init_blank_ann: shouldn't see ann_none");
+            //fail;
+            log("warning: init_blank_ann: saw ann_none");
+            ret a;
+        }
+        case (ann_type(?i, ?t, ?ps,_)) {
+            ret ann_type(i, t, ps, some[@ts_ann](@empty_ann(0u)));
+        }
+    }
+}
+
+fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
+    log("init_block:");
+    log_block(respan(sp, b));
+    alt(b.a) {
+        case (ann_none(_)) {
+            log("init_block: shouldn't see ann_none");
+            fail;
+        }
+        case (ann_type(_, _, _, _)) {
+            auto fld0 = new_identity_fold[fn_info]();
+
+            fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+            ret fold_block[fn_info](fi, fld0, respan(sp, b)); 
+        }
+    }
+}
+
+fn num_locals(fn_info m) -> uint {
+  ret m.vars.size();
+}
+
+fn new_crate_ctxt(ty::node_type_table nt, ty::ctxt cx) -> crate_ctxt {
+    ret rec(tcx=cx, node_types=nt, fm=@new_def_hash[fn_info]());
+}
+
+fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
+    alt (ccx.fm.find(d)) {
+        case (some[fn_info](?fi)) { ret fi.cf; }
+        case (none[fn_info])      { ret return; } 
+    }
+}
+
+/* conservative approximation: uses the mapping if e refers to a known
+   function or method, assumes returning otherwise.
+   There's no case for fail b/c we assume e is the callee and it
+   seems unlikely that one would apply "fail" to arguments. */
+fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
+    auto f = ann_tag(expr_ann(e));
+    alt (ccx.tcx.def_map.find(f)) {
+        case (some[def](def_fn(?d)))        { ret controlflow_def_id(ccx, d); }
+        case (some[def](def_obj_field(?d))) { ret controlflow_def_id(ccx, d); }
+        case (_)                            { ret return; }
+    }
+}
+
+fn ann_to_def_strict(&crate_ctxt ccx, &ann a) -> def {
+    alt (ccx.tcx.def_map.find(ann_tag(a))) {
+        case (none[def]) { 
+            log_err("ann_to_def: node_id " +
+                    uistr(ann_tag(a)) +
+                    " has no def");
+            fail;
+        }
+        case (some[def](?d)) { ret d; }
+    }
+}
+
+fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
+    ret ccx.tcx.def_map.find(ann_tag(a));
+}
+
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
+
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
new file mode 100644
index 00000000000..667a0889e24
--- /dev/null
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -0,0 +1,137 @@
+import std::bitv;
+import std::_vec;
+import std::_vec::len;
+import std::_vec::slice;
+
+import front::ast;
+import front::ast::def_id;
+import front::ast::expr;
+import front::ast::ann;
+
+import aux::fn_ctxt;
+import aux::fn_info;
+import aux::log_bitv;
+import aux::num_locals;
+import aux::ann_to_ts_ann_strict;
+
+import tstate::ann::pre_and_post;
+import tstate::ann::precond;
+import tstate::ann::postcond;
+import tstate::ann::prestate;
+import tstate::ann::poststate;
+import tstate::ann::relax_prestate;
+import tstate::ann::pps_len;
+import tstate::ann::true_precond;
+import tstate::ann::empty_prestate;
+import tstate::ann::difference;
+import tstate::ann::union;
+import tstate::ann::intersect;
+import tstate::ann::clone;
+import tstate::ann::set_in_postcond;
+import tstate::ann::set_in_poststate;
+             
+fn bit_num(def_id v, fn_info m) -> uint {
+  assert (m.vars.contains_key(v));
+  ret m.vars.get(v)._0;
+}
+
+fn promises(&poststate p, def_id v, fn_info m) -> bool {
+    ret bitv::get(p, bit_num(v, m));
+}
+
+// Given a list of pres and posts for exprs e0 ... en,
+// return the precondition for evaluating each expr in order.
+// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
+// precondition shouldn't include x.
+fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
+  let uint sz = len[pre_and_post](pps);
+  let uint num_vars = num_locals(enclosing);
+
+  if (sz >= 1u) {
+    auto first   = pps.(0);
+    assert (pps_len(first) == num_vars);
+    let precond rest = seq_preconds(enclosing,
+                         slice[pre_and_post](pps, 1u, sz));
+    difference(rest, first.postcondition);
+    auto res = clone(first.precondition);
+    union(res, rest);
+
+    log("seq_preconds:");
+    log("first.postcondition =");
+    log_bitv(enclosing, first.postcondition);
+    log("rest =");
+    log_bitv(enclosing, rest);
+    log("returning");
+    log_bitv(enclosing, res);
+
+    ret res;
+  }
+  else {
+      ret true_precond(num_vars);
+  }
+}
+
+/* works on either postconds or preconds
+ should probably rethink the whole type synonym situation */
+fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
+  auto sz = _vec::len[postcond](rest);
+
+  if (sz > 0u) {
+    auto other = rest.(0);
+    union(first, other);
+    union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest)));
+  }
+
+  ret first;
+}
+
+fn union_postconds(uint nv, &vec[postcond] pcs) -> postcond {
+  if (len[postcond](pcs) > 0u) {
+      ret union_postconds_go(bitv::clone(pcs.(0)), pcs);
+  }
+  else {
+      ret empty_prestate(nv);
+  }
+}
+
+/* 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(bitv::clone(pcs.(0)), pcs);
+}
+
+fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+  assert (fcx.enclosing.vars.contains_key(id));
+  let uint i = (fcx.enclosing.vars.get(id))._0;
+  ret set_in_postcond(i, (ann_to_ts_ann_strict(a)).conditions);
+}
+
+fn declare_var(&fn_info enclosing, def_id id, prestate pre)
+   -> prestate {
+    assert (enclosing.vars.contains_key(id));
+    let uint i = (enclosing.vars.get(id))._0;
+    auto res = clone(pre);
+    relax_prestate(i, res);
+    ret res;
+}
+
+fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+  assert (fcx.enclosing.vars.contains_key(id));
+  let uint i = (fcx.enclosing.vars.get(id))._0;
+  ret set_in_poststate(i, (ann_to_ts_ann_strict(a)).states);
+}
+
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
new file mode 100644
index 00000000000..a1df6e0f55c
--- /dev/null
+++ b/src/comp/middle/tstate/ck.rs
@@ -0,0 +1,231 @@
+import front::ast;
+import front::ast::method;
+import front::ast::ann;
+import front::ast::item;
+import front::ast::item_fn;
+import front::ast::_fn;
+import front::ast::obj_field;
+import front::ast::_obj;
+import front::ast::stmt;
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ty_param;
+import front::ast::crate;
+
+import front::ast::expr;
+import middle::fold::respan;
+import middle::fold::new_identity_fold;
+import middle::fold::fold_crate;
+import middle::ty::type_is_nil;
+import middle::ty::ret_ty_of_fn;
+import util::common::span;
+import tstate::ann::ts_ann;
+import tstate::ann::empty_poststate;
+import tstate::ann::true_precond;
+import tstate::ann::true_postcond;
+import tstate::ann::false_postcond;
+import tstate::ann::precond;
+import tstate::ann::postcond;
+import tstate::ann::poststate;
+import tstate::ann::prestate;
+import tstate::ann::implies;
+import tstate::ann::ann_precond;
+import tstate::ann::ann_prestate;
+import std::_vec::map;
+import std::_vec;
+import std::_vec::slice;
+import std::_vec::unzip;
+import std::_vec::plus_option;
+import std::_vec::cat_options;
+
+import std::option;
+import std::option::t;
+import std::option::some;
+import std::option::none;
+
+import aux::fn_ctxt;
+import aux::crate_ctxt;
+import aux::new_crate_ctxt;
+import aux::expr_precond;
+import aux::expr_prestate;
+import aux::expr_poststate;
+import aux::stmt_poststate;
+import aux::stmt_to_ann;
+import aux::num_locals;
+import aux::fixed_point_states;
+import aux::bitv_to_str;
+
+import util::common::ty_to_str;
+import bitvectors::promises;
+
+import annotate::annotate_crate;
+import collect_locals::mk_f_to_fn_info;
+import pre_post_conditions::check_item_fn;
+import states::find_pre_post_state_fn;
+
+fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
+  let precond prec    = expr_precond(e);
+  let prestate pres   = expr_prestate(e);
+
+  if (!implies(pres, prec)) {
+      auto s = "";
+      s += ("Unsatisfied precondition constraint for expression:\n");
+      s += util::common::expr_to_str(e);
+      s += ("Precondition: ");
+      s += bitv_to_str(fcx.enclosing, prec);
+      s += ("Prestate: ");
+      s += bitv_to_str(fcx.enclosing, pres);
+      fcx.ccx.tcx.sess.span_err(e.span, s);
+  }
+}
+
+fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
+  alt (stmt_to_ann(s)) {
+    case (none[@ts_ann]) {
+      ret;
+    }
+    case (some[@ts_ann](?a)) {
+      let precond prec    = ann_precond(*a);
+      let prestate pres   = ann_prestate(*a);
+
+      /*
+      log("check_states_stmt:");
+      log_stmt(s);
+      log("prec = ");
+      log_bitv(enclosing, prec);
+      log("pres = ");
+      log_bitv(enclosing, pres);
+      */
+
+      if (!implies(pres, prec)) {
+          auto ss = "";
+          ss += ("Unsatisfied precondition constraint for statement:\n");
+          ss += util::common::stmt_to_str(s);
+          ss += ("Precondition: ");
+          ss += bitv_to_str(fcx.enclosing, prec);
+          ss += ("Prestate: ");
+          ss += bitv_to_str(fcx.enclosing, pres);
+          fcx.ccx.tcx.sess.span_err(s.span, ss);
+      }
+    }
+  }
+}
+
+fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
+    auto enclosing = fcx.enclosing;
+    auto nv   = num_locals(enclosing);
+    auto post = @empty_poststate(nv);
+
+    fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post, uint nv) -> () {
+        check_states_stmt(fcx, *s);
+        *post = stmt_poststate(*s, nv);
+    }
+
+    auto do_one = bind do_one_(fcx, _, post, nv);
+ 
+  _vec::map[@stmt, ()](do_one, f.body.node.stmts);
+  fn do_inner_(fn_ctxt fcx, &@expr e, @poststate post) -> () {
+    check_states_expr(fcx, e);
+    *post = expr_poststate(e);
+  }
+  auto do_inner = bind do_inner_(fcx, _, post);
+  option::map[@expr, ()](do_inner, f.body.node.expr);
+  
+  /* Finally, check that the return value is initialized */
+  if (f.proto == ast::proto_fn
+      && ! promises(*post, fcx.id, enclosing)
+      && ! type_is_nil(fcx.ccx.tcx,
+                       ret_ty_of_fn(fcx.ccx.node_types, fcx.ccx.tcx, a)) ) {
+      /* FIXME: make this an error, not warning, once I finish implementing
+         ! annotations */
+        /* fcx.ccx.tcx.sess.span_err(f.body.span, "Function " +
+           fcx.name + " may not return. Its declared return type is "
+           + util.common.ty_to_str(*f.decl.output)); */
+        log_err("WARNING: Function " +
+           fcx.name + " may not return. Its declared return type is "
+                + ty_to_str(*f.decl.output));
+    }
+
+}
+
+fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) -> () {
+    /* Compute the pre- and post-states for this function */
+    auto g = find_pre_post_state_fn;
+    fixed_point_states(fcx, g, f);
+    
+    /* Now compare each expr's pre-state to its precondition
+       and post-state to its postcondition */
+    check_states_against_conditions(fcx, f, a);
+}
+
+fn check_item_fn_state(&crate_ctxt ccx, &span sp, &ident i,
+                       &_fn f, &vec[ty_param] ty_params,
+                       &def_id id, &ann a) -> @item {
+
+    /* Look up the var-to-bit-num map for this function */
+    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);
+
+    /* Rebuild the same function */
+    ret @respan(sp, item_fn(i, f, ty_params, id, a));
+}
+
+fn check_method_states(&crate_ctxt ccx, @method m) -> () {
+    assert (ccx.fm.contains_key(m.node.id));
+    auto fcx = rec(enclosing=ccx.fm.get(m.node.id),
+                   id=m.node.id, name=m.node.ident, ccx=ccx);
+    check_fn_states(fcx, m.node.meth, m.node.ann);
+}
+
+fn check_obj_state(&crate_ctxt ccx, &vec[obj_field] fields,
+                   &vec[@method] methods,
+                   &option::t[@method] dtor) -> _obj {
+    fn one(crate_ctxt ccx, &@method m) -> () {
+        ret check_method_states(ccx, m);
+    }
+    auto f = bind one(ccx,_);
+    _vec::map[@method, ()](f, methods);
+    option::map[@method, ()](f, dtor);
+    ret rec(fields=fields, methods=methods, dtor=dtor);
+}
+
+/* FIXME use walk instead of fold where possible */
+
+fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
+    let crate_ctxt ccx = new_crate_ctxt(nt, cx);
+
+    /* Build the global map from function id to var-to-bit-num-map */
+    mk_f_to_fn_info(ccx, crate);
+  
+    /* Add a blank ts_ann to every statement (and expression) */
+    auto with_anns = annotate_crate(ccx.fm, crate);
+
+    /* Compute the pre and postcondition for every subexpression */
+    
+    auto fld = new_identity_fold[crate_ctxt]();
+    fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
+    auto with_pre_postconditions =
+           fold_crate[crate_ctxt](ccx, fld, with_anns);
+    
+    auto fld1 = new_identity_fold[crate_ctxt]();
+
+    fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_),
+                fold_obj     = bind check_obj_state(_,_,_,_)
+                with *fld1);
+    
+    ret fold_crate[crate_ctxt](ccx, fld1, with_pre_postconditions);
+}
+
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
new file mode 100644
index 00000000000..79761ceb72d
--- /dev/null
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -0,0 +1,122 @@
+import std::_vec;
+import std::_vec::plus_option;
+
+import front::ast;
+import front::ast::crate;
+import front::ast::ann;
+import front::ast::arg;
+import front::ast::method;
+import front::ast::local;
+import front::ast::item;
+import front::ast::item_fn;
+import front::ast::item_obj;
+import front::ast::_obj;
+import front::ast::obj_def_ids;
+import front::ast::_fn;
+import front::ast::ty_param;
+import front::ast::_mod;
+import front::ast::decl;
+import front::ast::decl_local;
+import front::ast::def_id;
+import front::ast::ident;
+import middle::fold::span;
+import middle::fold::respan;
+import middle::fold::new_identity_fold;
+import middle::fold::fold_block;
+import middle::fold::fold_fn;
+import middle::fold::fold_crate;
+
+import aux::fn_info;
+import aux::var_info;
+import aux::crate_ctxt;
+
+import util::common::new_def_hash;
+
+fn var_is_local(def_id v, fn_info m) -> bool {
+  ret (m.vars.contains_key(v));
+}
+
+fn collect_local(&@vec[tup(ident, def_id)] vars, &span sp, &@local loc)
+    -> @decl {
+    log("collect_local: pushing " + loc.ident);
+    _vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+    ret @respan(sp, decl_local(loc));
+}
+
+fn find_locals(_fn f) -> @vec[tup(ident,def_id)] {
+  auto res = @_vec::alloc[tup(ident,def_id)](0u);
+
+  auto fld = new_identity_fold[@vec[tup(ident, def_id)]]();
+  fld = @rec(fold_decl_local = bind collect_local(_,_,_) with *fld);
+  auto ignore = fold_fn[@vec[tup(ident, def_id)]](res, fld, f);
+
+  ret res;
+}
+
+
+fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+  log(nm + " |-> " + util::common::uistr(next));
+  tbl.vars.insert(v, tup(next,nm));
+  ret (next + 1u);
+}
+
+/* builds a table mapping each local var defined in f
+   to a bit number in the precondition/postcondition vectors */
+fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
+    auto res = rec(vars=@new_def_hash[var_info](),
+                   cf=f.decl.cf);
+    let uint next = 0u;
+    let vec[arg] f_args = f.decl.inputs;
+
+    /* ignore args, which we know are initialized;
+       just collect locally declared vars */
+
+    let @vec[tup(ident,def_id)] locals = find_locals(f);
+    // log (uistr(_vec::len[tup(ident, def_id)](locals)) + " locals");
+    for (tup(ident,def_id) p in *locals) {
+        next = add_var(p._1, p._0, next, res);
+    }
+    /* add a pseudo-entry for the function's return value
+       we can safely use the function's name itself for this purpose */
+    add_var(f_id, f_name, next, res);
+
+    ret res;
+}
+
+/* extends mk_fn_info to a function item, side-effecting the map fi from
+   function IDs to fn_info maps */
+fn mk_fn_info_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
+                 &vec[ty_param] ty_params, &def_id id, &ann a) -> @item {
+    auto f_inf = mk_fn_info(f, id, i);
+    ccx.fm.insert(id, f_inf);
+    //  log_err("inserting: " + i);
+    ret @respan(sp, item_fn(i, f, ty_params, id, a));
+}
+
+/* extends mk_fn_info to an obj item, side-effecting the map fi from
+   function IDs to fn_info maps */
+fn mk_fn_info_item_obj(&crate_ctxt ccx, &span sp, &ident i, &_obj o,
+                       &vec[ty_param] ty_params,
+                       &obj_def_ids odid, &ann a) -> @item {
+    auto all_methods = _vec::clone[@method](o.methods);
+    plus_option[@method](all_methods, o.dtor);
+    auto f_inf;
+    for (@method m in all_methods) {
+        f_inf = mk_fn_info(m.node.meth, m.node.id, m.node.ident);
+        ccx.fm.insert(m.node.id, f_inf);
+    }
+    ret @respan(sp, item_obj(i, o, ty_params, odid, a));
+}
+
+
+/* initializes the global fn_info_map (mapping each function ID, including
+   nested locally defined functions, onto a mapping from local variable name
+   to bit number) */
+fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) -> () {
+
+  auto fld = new_identity_fold[crate_ctxt]();
+  fld = @rec(fold_item_fn  = bind mk_fn_info_item_fn(_,_,_,_,_,_,_),
+             fold_item_obj = bind mk_fn_info_item_obj(_,_,_,_,_,_,_)
+               with *fld);
+  fold_crate[crate_ctxt](ccx, fld, c);
+}
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
new file mode 100644
index 00000000000..68c40191fa6
--- /dev/null
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -0,0 +1,711 @@
+import std::_vec;
+import std::_vec::plus_option;
+import std::option;
+import std::option::none;
+import std::option::some;
+
+import tstate::ann::pre_and_post;
+import tstate::ann::get_post;
+import tstate::ann::postcond;
+import tstate::ann::true_precond;
+import tstate::ann::false_postcond;
+import tstate::ann::empty_pre_post;
+import tstate::ann::empty_poststate;
+import tstate::ann::require_and_preserve;
+import tstate::ann::union;
+import tstate::ann::intersect;
+import tstate::ann::pp_clone;
+import tstate::ann::empty_prestate;
+import aux::var_info;
+import aux::crate_ctxt;
+import aux::fn_ctxt;
+import aux::num_locals;
+import aux::expr_pp;
+import aux::stmt_pp;
+import aux::block_pp;
+import aux::set_pre_and_post;
+import aux::expr_precond;
+import aux::expr_postcond;
+import aux::expr_prestate;
+import aux::expr_poststate;
+import aux::block_postcond;
+import aux::fn_info;
+import aux::log_pp;
+import aux::ann_to_def;
+import aux::ann_to_def_strict;
+
+import bitvectors::seq_preconds;
+import bitvectors::union_postconds;
+import bitvectors::intersect_postconds;
+import bitvectors::declare_var;
+import bitvectors::bit_num;
+import bitvectors::gen;
+
+import front::ast::_mod;
+import front::ast;
+import front::ast::method;
+import front::ast::ann;
+import front::ast::ty;
+import front::ast::mutability;
+import front::ast::item;
+import front::ast::item_const;
+import front::ast::item_mod;
+import front::ast::item_ty;
+import front::ast::item_tag;
+import front::ast::item_native_mod;
+import front::ast::obj_field;
+import front::ast::stmt;
+import front::ast::stmt_;
+import front::ast::stmt_decl;
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ann;
+import front::ast::expr;
+import front::ast::path;
+import front::ast::crate_directive;
+import front::ast::fn_decl;
+import front::ast::_obj;
+import front::ast::native_mod;
+import front::ast::variant;
+import front::ast::ty_param;
+import front::ast::ty;
+import front::ast::proto;
+import front::ast::pat;
+import front::ast::binop;
+import front::ast::unop;
+import front::ast::def;
+import front::ast::lit;
+import front::ast::init_op;
+import front::ast::controlflow;
+import front::ast::return;
+import front::ast::noreturn;
+import front::ast::_fn;
+import front::ast::ann_none;
+import front::ast::ann_type;
+import front::ast::_obj;
+import front::ast::_mod;
+import front::ast::crate;
+import front::ast::item_fn;
+import front::ast::item_obj;
+import front::ast::def_local;
+import front::ast::def_fn;
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ann;
+import front::ast::item;
+import front::ast::item_fn;
+import front::ast::expr;
+import front::ast::elt;
+import front::ast::field;
+import front::ast::decl;
+import front::ast::decl_local;
+import front::ast::decl_item;
+import front::ast::initializer;
+import front::ast::local;
+import front::ast::arm;
+import front::ast::expr_call;
+import front::ast::expr_vec;
+import front::ast::expr_tup;
+import front::ast::expr_path;
+import front::ast::expr_field;
+import front::ast::expr_index;
+import front::ast::expr_log;
+import front::ast::expr_block;
+import front::ast::expr_rec;
+import front::ast::expr_if;
+import front::ast::expr_binary;
+import front::ast::expr_unary;
+import front::ast::expr_assign;
+import front::ast::expr_assign_op;
+import front::ast::expr_while;
+import front::ast::expr_do_while;
+import front::ast::expr_alt;
+import front::ast::expr_lit;
+import front::ast::expr_ret;
+import front::ast::expr_self_method;
+import front::ast::expr_bind;
+import front::ast::expr_spawn;
+import front::ast::expr_ext;
+import front::ast::expr_fail;
+import front::ast::expr_break;
+import front::ast::expr_cont;
+import front::ast::expr_send;
+import front::ast::expr_recv;
+import front::ast::expr_put;
+import front::ast::expr_port;
+import front::ast::expr_chan;
+import front::ast::expr_be;
+import front::ast::expr_check;
+import front::ast::expr_assert;
+import front::ast::expr_cast;
+import front::ast::expr_for;
+import front::ast::expr_for_each;
+import front::ast::stmt;
+import front::ast::stmt_decl;
+import front::ast::stmt_expr;
+import front::ast::block;
+import front::ast::block_;
+import front::ast::method;
+
+import middle::fold::span;
+import middle::fold::respan;
+
+import util::common::new_def_hash;
+import util::common::decl_lhs;
+import util::common::uistr;
+import util::common::log_expr;
+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_expr_err;
+
+fn find_pre_post_mod(&_mod m) -> _mod {
+    log("implement find_pre_post_mod!");
+    fail;
+}
+
+fn find_pre_post_native_mod(&native_mod m) -> native_mod {
+    log("implement find_pre_post_native_mod");
+    fail;
+}
+
+
+fn find_pre_post_obj(&crate_ctxt ccx, _obj o) -> () {
+    fn do_a_method(crate_ctxt ccx, &@method m) -> () {
+        assert (ccx.fm.contains_key(m.node.id));
+        let fn_ctxt fcx = rec(enclosing=ccx.fm.get(m.node.id),
+                       id=m.node.id, name=m.node.ident, ccx=ccx);
+        find_pre_post_fn(fcx, m.node.meth);
+    }
+    auto f = bind do_a_method(ccx,_);
+    _vec::map[@method, ()](f, o.methods);
+    option::map[@method, ()](f, o.dtor);
+}
+
+fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
+    alt (i.node) {
+        case (item_const(?id, ?t, ?e, ?di, ?a)) {
+            // make a fake fcx
+            auto fake_fcx = rec(enclosing=rec(vars=@new_def_hash[var_info](),
+                                              cf=return),
+                                id=tup(0,0),
+                                name="",
+                                ccx=ccx);
+            find_pre_post_expr(fake_fcx, e);
+        }
+        case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
+            assert (ccx.fm.contains_key(di));
+            auto fcx = rec(enclosing=ccx.fm.get(di),
+                           id=di, name=id, ccx=ccx);
+            find_pre_post_fn(fcx, f);
+        }
+        case (item_mod(?id, ?m, ?di)) {
+            find_pre_post_mod(m);
+        }
+        case (item_native_mod(?id, ?nm, ?di)) {
+            find_pre_post_native_mod(nm);
+        }
+        case (item_ty(_,_,_,_,_)) {
+            ret;
+        }
+        case (item_tag(_,_,_,_,_)) {
+            ret;
+        }
+        case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
+            find_pre_post_obj(ccx, o);
+        }
+    }
+}
+
+/* Finds the pre and postcondition for each expr in <args>;
+   sets the precondition in a to be the result of combining
+   the preconditions for <args>, and the postcondition in a to 
+   be the union of all postconditions for <args> */
+fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
+    auto enclosing = fcx.enclosing;
+    auto fm        = fcx.ccx.fm;
+    auto nv        = num_locals(enclosing);
+
+    fn do_one(fn_ctxt fcx, &@expr e) -> () {
+        find_pre_post_expr(fcx, e);
+    }
+    auto f = bind do_one(fcx, _);
+
+    _vec::map[@expr, ()](f, args);
+
+    fn get_pp(&@expr e) -> pre_and_post {
+        ret expr_pp(e);
+    }
+    auto g = get_pp;
+    auto pps = _vec::map[@expr, pre_and_post](g, args);
+    auto h = get_post;
+
+    set_pre_and_post(a,
+       rec(precondition=seq_preconds(enclosing, pps),
+           postcondition=union_postconds
+           (nv, (_vec::map[pre_and_post, postcond](h, pps)))));
+}
+
+fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
+      &block body, &ann a) -> () {
+    find_pre_post_expr(fcx, index);
+    find_pre_post_block(fcx, body);
+    auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
+           seq_preconds(fcx.enclosing, vec(expr_pp(index),
+                                       block_pp(body))));
+    auto loop_postcond = intersect_postconds
+        (vec(expr_postcond(index), block_postcond(body)));
+    set_pre_and_post(a, rec(precondition=loop_precond,
+                            postcondition=loop_postcond));
+}
+
+fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var) -> () {
+  alt (ann_to_def(fcx.ccx, new_var)) {
+    case (some[def](def_local(?d_id))) {
+      find_pre_post_expr(fcx, rhs);
+      set_pre_and_post(larger_ann, expr_pp(rhs));
+      gen(fcx, larger_ann, d_id);
+    }
+    case (_) { find_pre_post_exprs(fcx, vec(lhs, rhs), larger_ann); }
+  }
+}
+
+/* Fills in annotations as a side effect. Does not rebuild the expr */
+fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
+    auto enclosing      = fcx.enclosing;
+    auto num_local_vars = num_locals(enclosing);
+
+    fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
+        find_pre_post_expr(fcx, e);
+    }
+    fn pp_one(&@expr e) -> pre_and_post {
+        ret expr_pp(e);
+    }
+    
+    /*
+    log_err("find_pre_post_expr (num_locals =" +
+        uistr(num_local_vars) + "):");
+    log_expr_err(*e);
+    */
+
+    alt (e.node) {
+        case (expr_call(?operator, ?operands, ?a)) {
+            auto args = _vec::clone[@expr](operands);
+            _vec::push[@expr](args, operator);
+            find_pre_post_exprs(fcx, args, a);
+        }
+        case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+            auto args = _vec::clone[@expr](operands);
+            _vec::push[@expr](args, operator);
+            find_pre_post_exprs(fcx, args, a);
+        }
+        case (expr_vec(?args, _, ?a)) {
+            find_pre_post_exprs(fcx, args, a);
+        }
+        case (expr_tup(?elts, ?a)) {
+            find_pre_post_exprs(fcx, elt_exprs(elts), a);
+        }
+        case (expr_path(?p, ?a)) {
+            auto res = empty_pre_post(num_local_vars);
+	    
+	    auto df = ann_to_def_strict(fcx.ccx, a);
+            alt (df) {
+                case (def_local(?d_id)) {
+                    auto i = bit_num(d_id, enclosing);
+                    require_and_preserve(i, res);
+                }
+                case (_) { /* nothing to check */ }
+            }
+
+            // Otherwise, variable is global, so it must be initialized
+            set_pre_and_post(a, res);
+        }
+        case (expr_self_method(?v, ?a)) {
+            /* v is a method of the enclosing obj, so it must be
+               initialized, right? */
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case(expr_log(_, ?arg, ?a)) {
+            find_pre_post_expr(fcx, arg);
+            set_pre_and_post(a, expr_pp(arg));
+        }
+        case (expr_chan(?arg, ?a)) {
+            find_pre_post_expr(fcx, arg);
+            set_pre_and_post(a, expr_pp(arg));
+        }
+        case(expr_put(?opt, ?a)) {
+            alt (opt) {
+                case (some[@expr](?arg)) {
+                    find_pre_post_expr(fcx, arg);
+                    set_pre_and_post(a, expr_pp(arg));
+                }
+                case (none[@expr]) {
+                    set_pre_and_post(a, empty_pre_post(num_local_vars));
+                }
+            }
+        }
+        case (expr_block(?b, ?a)) {
+            find_pre_post_block(fcx, b);
+            set_pre_and_post(a, block_pp(b));
+        }
+        case (expr_rec(?fields,?maybe_base,?a)) {
+            auto es = field_exprs(fields);
+            _vec::plus_option[@expr](es, maybe_base);
+            find_pre_post_exprs(fcx, es, a);
+        }
+        case (expr_assign(?lhs, ?rhs, ?a)) {
+            alt (lhs.node) {
+                case (expr_path(?p, ?a_lhs)) {
+		  gen_if_local(fcx, lhs, rhs, a, a_lhs);
+                }
+                case (_) {
+                    find_pre_post_exprs(fcx, vec(lhs, rhs), a);
+                }
+            }
+        }
+        case (expr_recv(?lhs, ?rhs, ?a)) {
+            alt (lhs.node) {
+                case (expr_path(?p, ?a_lhs)) {
+		  gen_if_local(fcx, lhs, rhs, a, a_lhs);
+                }
+                case (_) {
+                    // doesn't check that lhs is an lval, but
+                    // that's probably ok
+                    find_pre_post_exprs(fcx, vec(lhs, rhs), a);
+                }
+            }
+        }
+        case (expr_assign_op(_, ?lhs, ?rhs, ?a)) {
+            /* Different from expr_assign in that the lhs *must*
+               already be initialized */
+            find_pre_post_exprs(fcx, vec(lhs, rhs), a);
+        }
+        case (expr_lit(_,?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_ret(?maybe_val, ?a)) {
+            alt (maybe_val) {
+                case (none[@expr]) {
+                    set_pre_and_post(a,
+                      rec(precondition=true_precond(num_local_vars),
+                          postcondition=false_postcond(num_local_vars)));
+                }
+                case (some[@expr](?ret_val)) {
+                    find_pre_post_expr(fcx, ret_val);
+                    let pre_and_post pp =
+                        rec(precondition=expr_precond(ret_val),
+                            postcondition=false_postcond(num_local_vars));
+                    set_pre_and_post(a, pp);
+                }
+            }
+        }
+        case (expr_be(?e, ?a)) {
+            find_pre_post_expr(fcx, e);
+            set_pre_and_post(a,
+               rec(precondition=expr_prestate(e),
+                   postcondition=false_postcond(num_local_vars)));
+        }
+        case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
+            find_pre_post_expr(fcx, antec);
+            find_pre_post_block(fcx, conseq);
+            alt (maybe_alt) {
+                case (none[@expr]) {
+                    auto precond_res = seq_preconds(enclosing,
+                                                    vec(expr_pp(antec),
+                                                        block_pp(conseq)));
+                    set_pre_and_post(a, rec(precondition=precond_res,
+                                            postcondition=
+                                            expr_poststate(antec)));
+                }
+                case (some[@expr](?altern)) {
+                    find_pre_post_expr(fcx, altern);
+                    auto precond_true_case =
+                        seq_preconds(enclosing,
+                                     vec(expr_pp(antec), block_pp(conseq)));
+                    auto postcond_true_case = union_postconds
+                        (num_local_vars,
+                         vec(expr_postcond(antec), block_postcond(conseq)));
+                    auto precond_false_case = seq_preconds
+                        (enclosing,
+                         vec(expr_pp(antec), expr_pp(altern)));
+                    auto postcond_false_case = union_postconds
+                        (num_local_vars,
+                         vec(expr_postcond(antec), expr_postcond(altern)));
+                    auto precond_res = union_postconds
+                        (num_local_vars,
+                         vec(precond_true_case, precond_false_case));
+                    auto postcond_res = intersect_postconds
+                        (vec(postcond_true_case, postcond_false_case));
+                    set_pre_and_post(a, rec(precondition=precond_res,
+                                            postcondition=postcond_res));
+                }
+            }
+        }
+        case (expr_binary(?bop,?l,?r,?a)) {
+            /* *unless* bop is lazy (e.g. and, or)? 
+               FIXME */
+            find_pre_post_exprs(fcx, vec(l, r), a);
+        }
+        case (expr_send(?l, ?r, ?a)) {
+            find_pre_post_exprs(fcx, vec(l, r), a);
+        }
+        case (expr_unary(_,?operand,?a)) {
+            find_pre_post_expr(fcx, operand);
+            set_pre_and_post(a, expr_pp(operand));
+        }
+        case (expr_cast(?operand, _, ?a)) {
+            find_pre_post_expr(fcx, operand);
+            set_pre_and_post(a, expr_pp(operand));
+        }
+        case (expr_while(?test, ?body, ?a)) {
+            find_pre_post_expr(fcx, test);
+            find_pre_post_block(fcx, body);
+            set_pre_and_post(a,
+              rec(precondition=
+                    seq_preconds(enclosing,
+                               vec(expr_pp(test), 
+                                   block_pp(body))),
+                  postcondition=
+                    intersect_postconds(vec(expr_postcond(test),
+                                            block_postcond(body)))));
+        }
+        case (expr_do_while(?body, ?test, ?a)) {
+            find_pre_post_block(fcx, body);
+            find_pre_post_expr(fcx, test);
+   
+            auto loop_postcond = union_postconds(num_local_vars,
+                   vec(block_postcond(body), expr_postcond(test)));
+            /* conservative approximination: if the body
+               could break or cont, the test may never be executed */
+            if (has_nonlocal_exits(body)) {
+                loop_postcond = empty_poststate(num_local_vars);
+            }
+
+            set_pre_and_post(a, 
+              rec(precondition=seq_preconds(enclosing,
+                                            vec(block_pp(body),
+                                                expr_pp(test))),
+                  postcondition=loop_postcond));
+        }
+        case (expr_for(?d, ?index, ?body, ?a)) {
+            find_pre_post_loop(fcx, d, index, body, a);
+        }
+        case (expr_for_each(?d, ?index, ?body, ?a)) {
+            find_pre_post_loop(fcx, d, index, body, a);
+        }
+        case (expr_index(?e, ?sub, ?a)) {
+            find_pre_post_exprs(fcx, vec(e, sub), a);
+        }
+        case (expr_alt(?e, ?alts, ?a)) {
+            find_pre_post_expr(fcx, e);
+            fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
+                find_pre_post_block(fcx, an_alt.block);
+                ret block_pp(an_alt.block);
+            }
+            auto f = bind do_an_alt(fcx, _);
+            auto alt_pps = _vec::map[arm, pre_and_post](f, alts);
+            fn combine_pp(pre_and_post antec, 
+                          fn_info enclosing, &pre_and_post pp,
+                          &pre_and_post next) -> pre_and_post {
+                union(pp.precondition, seq_preconds(enclosing,
+                                                    vec(antec, next)));
+                intersect(pp.postcondition, next.postcondition);
+                ret pp;
+            }
+            auto antec_pp = pp_clone(expr_pp(e)); 
+            auto e_pp  = rec(precondition=empty_prestate(num_local_vars),
+                             postcondition=false_postcond(num_local_vars));
+            auto g = bind combine_pp(antec_pp, fcx.enclosing, _, _);
+
+            auto alts_overall_pp = _vec::foldl[pre_and_post, pre_and_post]
+                                    (g, e_pp, alt_pps);
+
+            set_pre_and_post(a, alts_overall_pp);
+        }
+        case (expr_field(?operator, _, ?a)) {
+            find_pre_post_expr(fcx, operator);
+            set_pre_and_post(a, expr_pp(operator));
+        }
+        case (expr_fail(?a)) {
+            set_pre_and_post(a,
+                             /* if execution continues after fail,
+                                then everything is true! */
+               rec(precondition=empty_prestate(num_local_vars),
+                   postcondition=false_postcond(num_local_vars)));
+        }
+        case (expr_assert(?p, ?a)) {
+            find_pre_post_expr(fcx, p);
+            set_pre_and_post(a, expr_pp(p));
+        }
+        case (expr_check(?p, ?a)) {
+            /* will need to change when we support arbitrary predicates... */
+            find_pre_post_expr(fcx, p);
+            set_pre_and_post(a, expr_pp(p));
+        }
+        case(expr_bind(?operator, ?maybe_args, ?a)) {
+            auto args = _vec::cat_options[@expr](maybe_args);
+            _vec::push[@expr](args, operator); /* ??? order of eval? */
+            find_pre_post_exprs(fcx, args, a);
+        }
+        case (expr_break(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_cont(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_port(?a)) {
+            set_pre_and_post(a, empty_pre_post(num_local_vars));
+        }
+        case (expr_ext(_, _, _, ?expanded, ?a)) {
+            find_pre_post_expr(fcx, expanded);
+            set_pre_and_post(a, expr_pp(expanded));
+        }
+    }
+}
+
+
+fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
+    -> () {
+    log("stmt =");
+    log_stmt(s);
+
+    auto enclosing      = fcx.enclosing;
+    auto num_local_vars = num_locals(enclosing);
+    alt(s.node) {
+        case(stmt_decl(?adecl, ?a)) {
+            alt(adecl.node) {
+                case(decl_local(?alocal)) {
+                    alt(alocal.init) {
+                        case(some[initializer](?an_init)) {
+                            find_pre_post_expr(fcx, an_init.expr);
+                            auto rhs_pp = expr_pp(an_init.expr);
+                            set_pre_and_post(alocal.ann, rhs_pp);
+
+                            /* Inherit ann from initializer, and add var being
+                               initialized to the postcondition */
+                            set_pre_and_post(a, rhs_pp);
+                            /*  log("gen (decl):");
+                                log_stmt(s); */
+                            gen(fcx, a, alocal.id); 
+                            /*                     log_err("for stmt");
+                                                   log_stmt(s);
+                                                   log_err("pp = ");
+                                                   log_pp(stmt_pp(s)); */
+                        }
+                        case(none[initializer]) {
+                            auto pp = empty_pre_post(num_local_vars);
+                            set_pre_and_post(alocal.ann, pp);
+                            set_pre_and_post(a, pp);
+                        }
+                    }
+                }
+                case(decl_item(?anitem)) {
+                    auto pp = empty_pre_post(num_local_vars);
+                    set_pre_and_post(a, pp);
+                    find_pre_post_item(fcx.ccx, *anitem);
+                }
+            }
+        }
+        case(stmt_expr(?e,?a)) {
+            find_pre_post_expr(fcx, e);
+            set_pre_and_post(a, expr_pp(e));
+        }    
+    }
+}
+
+fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
+    /* Want to say that if there is a break or cont in this
+     block, then that invalidates the poststate upheld by
+    any of the stmts after it. 
+    Given that the typechecker has run, we know any break will be in
+    a block that forms a loop body. So that's ok. There'll never be an
+    expr_break outside a loop body, therefore, no expr_break outside a block.
+    */
+
+    /* Conservative approximation for now: This says that if a block contains
+     *any* breaks or conts, then its postcondition doesn't promise anything.
+     This will mean that:
+     x = 0;
+     break;
+
+     won't have a postcondition that says x is initialized, but that's ok.
+     */
+    auto nv = num_locals(fcx.enclosing);
+
+    fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
+        find_pre_post_stmt(fcx, *s);
+        log("pre_post for stmt:");
+        log_stmt(*s);
+        log("is:");
+        log_pp(stmt_pp(*s));
+    }
+    auto do_one = bind do_one_(fcx, _);
+    
+    _vec::map[@stmt, ()](do_one, b.node.stmts);
+    fn do_inner_(fn_ctxt fcx, &@expr e) -> () {
+        find_pre_post_expr(fcx, e);
+    }
+    auto do_inner = bind do_inner_(fcx, _);
+    option::map[@expr, ()](do_inner, b.node.expr);
+
+    let vec[pre_and_post] pps = vec();
+
+    fn get_pp_stmt(&@stmt s) -> pre_and_post {
+        ret stmt_pp(*s);
+    }
+    auto f = get_pp_stmt;
+    pps += _vec::map[@stmt, pre_and_post](f, b.node.stmts);
+    fn get_pp_expr(&@expr e) -> pre_and_post {
+        ret expr_pp(e);
+    }
+    auto g = get_pp_expr;
+    plus_option[pre_and_post](pps,
+       option::map[@expr, pre_and_post](g, b.node.expr));
+
+    auto block_precond  = seq_preconds(fcx.enclosing, pps);
+    auto h = get_post;
+    auto postconds =  _vec::map[pre_and_post, postcond](h, pps);
+    /* A block may be empty, so this next line ensures that the postconds
+       vector is non-empty. */
+    _vec::push[postcond](postconds, block_precond);
+    auto block_postcond = empty_poststate(nv);
+    /* conservative approximation */
+    if (! has_nonlocal_exits(b)) {
+        block_postcond = union_postconds(nv, postconds);
+    }
+
+    set_pre_and_post(b.node.a, rec(precondition=block_precond,
+                                   postcondition=block_postcond));
+}
+
+fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
+    find_pre_post_block(fcx, f.body);
+}
+
+fn check_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
+                 &vec[ty_param] ty_params,
+                 &def_id id, &ann a) -> @item {
+    log("check_item_fn:");
+    log_fn(f, i, ty_params);
+
+    assert (ccx.fm.contains_key(id));
+    auto fcx = rec(enclosing=ccx.fm.get(id),
+                   id=id, name=i, ccx=ccx);
+    find_pre_post_fn(fcx, f);  
+
+    ret @respan(sp, item_fn(i, f, ty_params, id, a));
+}
+
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
+
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
new file mode 100644
index 00000000000..58de564dab5
--- /dev/null
+++ b/src/comp/middle/tstate/states.rs
@@ -0,0 +1,802 @@
+import std::bitv;
+import std::_vec;
+import std::_vec::plus_option;
+import std::_vec::cat_options;
+import std::option;
+import std::option::get;
+import std::option::is_none;
+import std::option::none;
+import std::option::some;
+import std::option::maybe;
+
+import tstate::ann::pre_and_post;
+import tstate::ann::get_post;
+import tstate::ann::postcond;
+import tstate::ann::empty_pre_post;
+import tstate::ann::empty_poststate;
+import tstate::ann::require_and_preserve;
+import tstate::ann::union;
+import tstate::ann::intersect;
+import tstate::ann::pp_clone;
+import tstate::ann::empty_prestate;
+import tstate::ann::prestate;
+import tstate::ann::poststate;
+import tstate::ann::false_postcond;
+import tstate::ann::ts_ann;
+import tstate::ann::extend_prestate;
+import tstate::ann::extend_poststate;
+import aux::var_info;
+import aux::crate_ctxt;
+import aux::fn_ctxt;
+import aux::num_locals;
+import aux::expr_pp;
+import aux::stmt_pp;
+import aux::block_pp;
+import aux::set_pre_and_post;
+import aux::expr_prestate;
+import aux::stmt_poststate;
+import aux::expr_poststate;
+import aux::block_poststate;
+import aux::fn_info;
+import aux::log_pp;
+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::stmt_to_ann;
+import aux::log_states;
+import aux::block_states;
+import aux::controlflow_expr;
+import aux::ann_to_def;
+
+import bitvectors::seq_preconds;
+import bitvectors::union_postconds;
+import bitvectors::intersect_postconds;
+import bitvectors::declare_var;
+import bitvectors::bit_num;
+import bitvectors::gen_poststate;
+
+import front::ast::_mod;
+import front::ast;
+import front::ast::_fn;
+import front::ast::method;
+import front::ast::ann;
+import front::ast::ty;
+import front::ast::mutability;
+import front::ast::item;
+import front::ast::obj_field;
+import front::ast::stmt;
+import front::ast::stmt_;
+import front::ast::stmt_decl;
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ann;
+import front::ast::expr;
+import front::ast::path;
+import front::ast::crate_directive;
+import front::ast::fn_decl;
+import front::ast::_obj;
+import front::ast::native_mod;
+import front::ast::variant;
+import front::ast::ty_param;
+import front::ast::ty;
+import front::ast::proto;
+import front::ast::pat;
+import front::ast::binop;
+import front::ast::unop;
+import front::ast::def;
+import front::ast::lit;
+import front::ast::init_op;
+import front::ast::controlflow;
+import front::ast::return;
+import front::ast::noreturn;
+import front::ast::ann_none;
+import front::ast::ann_type;
+import front::ast::_obj;
+import front::ast::_mod;
+import front::ast::crate;
+import front::ast::item_fn;
+import front::ast::item_mod;
+import front::ast::item_ty;
+import front::ast::item_tag;
+import front::ast::item_native_mod;
+import front::ast::item_obj;
+import front::ast::item_const;
+import front::ast::def_local;
+import front::ast::def_fn;
+import front::ast::ident;
+import front::ast::def_id;
+import front::ast::ann;
+import front::ast::item;
+import front::ast::item_fn;
+import front::ast::expr;
+import front::ast::elt;
+import front::ast::field;
+import front::ast::decl;
+import front::ast::decl_local;
+import front::ast::decl_item;
+import front::ast::initializer;
+import front::ast::local;
+import front::ast::arm;
+import front::ast::expr_call;
+import front::ast::expr_vec;
+import front::ast::expr_tup;
+import front::ast::expr_path;
+import front::ast::expr_field;
+import front::ast::expr_index;
+import front::ast::expr_log;
+import front::ast::expr_block;
+import front::ast::expr_rec;
+import front::ast::expr_if;
+import front::ast::expr_binary;
+import front::ast::expr_unary;
+import front::ast::expr_assign;
+import front::ast::expr_assign_op;
+import front::ast::expr_while;
+import front::ast::expr_do_while;
+import front::ast::expr_alt;
+import front::ast::expr_lit;
+import front::ast::expr_ret;
+import front::ast::expr_self_method;
+import front::ast::expr_bind;
+import front::ast::expr_spawn;
+import front::ast::expr_ext;
+import front::ast::expr_fail;
+import front::ast::expr_break;
+import front::ast::expr_cont;
+import front::ast::expr_send;
+import front::ast::expr_recv;
+import front::ast::expr_put;
+import front::ast::expr_port;
+import front::ast::expr_chan;
+import front::ast::expr_be;
+import front::ast::expr_check;
+import front::ast::expr_assert;
+import front::ast::expr_cast;
+import front::ast::expr_for;
+import front::ast::expr_for_each;
+import front::ast::stmt;
+import front::ast::stmt_decl;
+import front::ast::stmt_expr;
+import front::ast::block;
+import front::ast::block_;
+import front::ast::method;
+
+import middle::fold::span;
+import middle::fold::respan;
+
+import util::common::new_def_hash;
+import util::common::decl_lhs;
+import util::common::uistr;
+import util::common::log_expr;
+import util::common::log_block;
+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_expr_err;
+
+fn find_pre_post_state_mod(&_mod m) -> bool {
+    log("implement find_pre_post_state_mod!");
+    fail;
+}
+
+fn find_pre_post_state_native_mod(&native_mod m) -> bool {
+    log("implement find_pre_post_state_native_mod!");
+    fail;
+}
+
+fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs)
+     -> tup(bool, poststate) {
+  auto changed = false;
+  auto post = pres;
+
+  for (@expr e in exprs) {
+    changed = find_pre_post_state_expr(fcx, post, e) || changed;
+    post = expr_poststate(e);
+  }
+
+  ret tup(changed, post);
+}
+
+fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres,
+                             &ann a, &vec[@expr] es) -> bool {
+    auto res = seq_states(fcx, pres, es);
+    auto changed = res._0;
+    changed = extend_prestate_ann(a, pres) || changed;
+    changed = extend_poststate_ann(a, res._1) || changed;
+    ret changed;
+}
+
+fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
+  &@expr index, &block body, &ann a) -> bool {
+    auto changed = false;
+
+    /* same issues as while */
+    changed = extend_prestate_ann(a, pres) || changed;
+    changed = find_pre_post_state_expr(fcx, pres, index) || changed;
+    /* in general, would need the intersection of
+       (poststate of index, poststate of body) */
+    changed = find_pre_post_state_block(fcx, expr_poststate(index), body)
+                || changed;
+    auto res_p = intersect_postconds(vec(expr_poststate(index),
+                                         block_poststate(body)));
+  
+    changed = extend_poststate_ann(a, res_p) || changed;
+    ret changed;
+}
+
+fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
+  alt (ann_to_def(fcx.ccx, a_new_var)) {
+    case (some[def](def_local(?d))) { ret gen_poststate(fcx, a, d); }
+    case (_) { ret false; }
+  }
+}
+
+fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
+  auto changed = false;
+  auto num_local_vars = num_locals(fcx.enclosing);
+
+  /*
+  log_err("states:");
+  log_expr_err(*e);
+  log_err(ast.ann_tag(middle.ty.expr_ann(e)));
+  */
+
+  /* FIXME could get rid of some of the copy/paste */
+  alt (e.node) {
+    case (expr_vec(?elts, _, ?a)) {
+        ret find_pre_post_state_exprs(fcx, pres, a, elts); 
+    }
+    case (expr_tup(?elts, ?a)) {
+      ret find_pre_post_state_exprs(fcx, pres, a, elt_exprs(elts));
+    }
+    case (expr_call(?operator, ?operands, ?a)) {
+      /* do the prestate for the rator */
+      changed = find_pre_post_state_expr(fcx, pres, operator)
+        || changed;
+      /* rands go left-to-right */
+      changed = find_pre_post_state_exprs(fcx,
+                                    expr_poststate(operator), a, operands)
+          || changed;
+      /* if this is a failing call, it sets the return value */
+       alt (controlflow_expr(fcx.ccx, operator)) {
+          case (noreturn) {
+	    /*
+	    log_err("Call that might fail! to");
+	    log_expr_err(*operator);
+	    */
+	    changed = gen_poststate(fcx, a, fcx.id) || changed;
+          }
+          case (_) { 
+	    /*	    log_err("non-failing call, to:");
+	    log_expr_err(*operator);
+	    */
+	  }
+      }
+      ret changed;
+    }
+    case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, operator);
+        ret(find_pre_post_state_exprs(fcx,
+                 expr_poststate(operator), a, operands)
+          || changed);
+    }
+    case (expr_bind(?operator, ?maybe_args, ?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, operator)
+            || changed;
+        ret (find_pre_post_state_exprs(fcx,
+          expr_poststate(operator), a, cat_options[@expr](maybe_args))
+            || changed);
+    }
+    case (expr_path(_,?a)) {
+      ret pure_exp(a, pres);
+    }
+    case (expr_log(_,?e,?a)) {
+        /* factor out the "one exp" pattern */
+        changed = find_pre_post_state_expr(fcx, pres, e);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        ret changed;
+    }
+    case (expr_chan(?e, ?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, e);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        ret changed;
+    }
+    case (expr_ext(_, _, _, ?expanded, ?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, expanded);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(expanded))
+           || changed;
+        ret changed;
+    }
+    case (expr_put(?maybe_e, ?a)) {
+        alt (maybe_e) {
+            case (some[@expr](?arg)) {
+                changed = find_pre_post_state_expr(fcx, pres, arg);
+                changed = extend_prestate_ann(a, pres) || changed;
+                changed = extend_poststate_ann(a, expr_poststate(arg))
+                    || changed;
+                ret changed;
+            }
+            case (none[@expr]) {
+                ret pure_exp(a, pres);
+            }
+        }
+    }
+    case (expr_lit(?l,?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_block(?b,?a)) {
+        changed = find_pre_post_state_block(fcx, pres, b)
+           || changed;
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, block_poststate(b)) || changed;
+        ret changed;
+    }
+    case (expr_rec(?fields,?maybe_base,?a)) {
+        changed = find_pre_post_state_exprs(fcx, pres, a,
+                                            field_exprs(fields)) || changed;
+        alt (maybe_base) {
+            case (none[@expr]) { /* do nothing */ }
+            case (some[@expr](?base)) {
+                changed = find_pre_post_state_expr(fcx, pres, base)
+                    || changed;
+                changed = extend_poststate_ann(a, expr_poststate(base))
+                    || changed;
+            }
+        }
+        ret changed;
+    }
+    case (expr_assign(?lhs, ?rhs, ?a)) {
+        extend_prestate_ann(a, pres);
+
+        alt (lhs.node) {
+            case (expr_path(?p, ?a_lhs)) {
+                // assignment to local var
+                changed = pure_exp(a_lhs, pres) || changed;
+                changed = find_pre_post_state_expr(fcx, pres, rhs)
+                    || changed;
+                changed = extend_poststate_ann(a, expr_poststate(rhs))
+                    || changed;
+                changed = gen_if_local(fcx, a_lhs, a)|| changed;
+            }
+            case (_) {
+                // assignment to something that must already have been init'd
+                changed = find_pre_post_state_expr(fcx, pres, lhs)
+                    || changed;
+                changed = find_pre_post_state_expr(fcx,
+                     expr_poststate(lhs), rhs) || changed;
+                changed = extend_poststate_ann(a, expr_poststate(rhs))
+                    || changed;
+            }
+        }
+        ret changed;
+    }
+    case (expr_recv(?lhs, ?rhs, ?a)) {
+        extend_prestate_ann(a, pres);
+
+        alt (lhs.node) {
+            case (expr_path(?p, ?a_lhs)) {
+                // receive to local var
+                changed = pure_exp(a_lhs, pres) || changed;
+                changed = find_pre_post_state_expr(fcx, pres, rhs)
+                    || changed;
+                changed = extend_poststate_ann(a, expr_poststate(rhs))
+                    || changed;
+                changed = gen_if_local(fcx, a_lhs, a) || changed;
+            }
+            case (_) {
+                // receive to something that must already have been init'd
+                changed = find_pre_post_state_expr(fcx, pres, lhs)
+                    || changed;
+                changed = find_pre_post_state_expr(fcx,
+                     expr_poststate(lhs), rhs) || changed;
+                changed = extend_poststate_ann(a, expr_poststate(rhs))
+                    || changed;
+            }
+        }
+        ret changed;
+    }
+
+    case (expr_ret(?maybe_ret_val, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        set_poststate_ann(a, false_postcond(num_local_vars));
+        alt(maybe_ret_val) {
+            case (none[@expr]) { /* do nothing */ }
+            case (some[@expr](?ret_val)) {
+                changed = find_pre_post_state_expr(fcx,
+                             pres, ret_val) || changed;
+            }
+        }
+        ret changed;
+    }
+    case (expr_be(?e, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        set_poststate_ann(a, false_postcond(num_local_vars));
+        changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+        ret changed;
+    }
+    case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fcx, pres, antec)
+            || changed;
+        changed = find_pre_post_state_block(fcx,
+          expr_poststate(antec), conseq) || changed;
+        alt (maybe_alt) {
+            case (none[@expr]) {
+                changed = extend_poststate_ann(a, expr_poststate(antec))
+                    || changed;
+            }
+            case (some[@expr](?altern)) {
+                changed = find_pre_post_state_expr(fcx,
+                   expr_poststate(antec), altern) || changed;
+                auto poststate_res = intersect_postconds
+                    (vec(block_poststate(conseq), expr_poststate(altern)));
+                changed = extend_poststate_ann(a, poststate_res) || changed;
+            }
+        }
+        log("if:");
+        log_expr(*e);
+        log("new prestate:");
+        log_bitv(fcx.enclosing, pres);
+        log("new poststate:");
+        log_bitv(fcx.enclosing, expr_poststate(e));
+
+        ret changed;
+    }
+    case (expr_binary(?bop, ?l, ?r, ?a)) {
+        /* FIXME: what if bop is lazy? */
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fcx, pres, l)
+                    || changed;
+        changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+                    || changed;
+        changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+        ret changed;
+    }
+    case (expr_send(?l, ?r, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fcx, pres, l)
+                    || changed;
+        changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
+                    || changed;
+        changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
+        ret changed;
+    }
+    case (expr_assign_op(?op, ?lhs, ?rhs, ?a)) {
+        /* quite similar to binary -- should abstract this */
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fcx, pres, lhs)
+                    || changed;
+        changed = find_pre_post_state_expr(fcx, expr_poststate(lhs), rhs)
+                    || changed;
+        changed = extend_poststate_ann(a, expr_poststate(rhs)) || changed;
+        ret changed;
+    }
+    case (expr_while(?test, ?body, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        /* 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?
+        */
+        changed = find_pre_post_state_expr(fcx, pres, test)
+            || changed;
+        changed = find_pre_post_state_block(fcx, expr_poststate(test), body)
+                    || changed; 
+        changed = extend_poststate_ann(a,
+                    intersect_postconds(vec(expr_poststate(test),
+                                        block_poststate(body)))) || changed;
+        ret changed;
+    }
+    case (expr_do_while(?body, ?test, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_block(fcx, pres, body)
+            || changed;
+        changed = find_pre_post_state_expr(fcx,
+                     block_poststate(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(a, pres) || changed;
+        }
+        else {
+            changed = extend_poststate_ann(a, expr_poststate(test))
+              || changed;
+        }
+
+        ret changed;
+    }
+    case (expr_for(?d, ?index, ?body, ?a)) {
+        ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
+    }
+    case (expr_for_each(?d, ?index, ?body, ?a)) {
+        ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
+    }
+    case (expr_index(?e, ?sub, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed; 
+        changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+        changed = find_pre_post_state_expr(fcx,
+                     expr_poststate(e), sub) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(sub));
+        ret changed;
+    }
+    case (expr_alt(?e, ?alts, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed; 
+        changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+        auto e_post = expr_poststate(e);
+        auto a_post;
+        if (_vec::len[arm](alts) > 0u) {
+            a_post = false_postcond(num_local_vars);
+            for (arm an_alt in alts) {
+                changed = find_pre_post_state_block(fcx, e_post,
+                                                    an_alt.block) || changed;
+                changed = intersect(a_post, block_poststate(an_alt.block))
+                    || changed; 
+            }
+        }
+        else {
+            // No alts; poststate is the poststate of the test
+            a_post = e_post;
+        }
+        changed = extend_poststate_ann(a, a_post);
+        ret changed;
+    }
+    case (expr_field(?e, _, ?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, e);
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
+        ret changed;
+    }
+    case (expr_unary(_,?operand,?a)) {
+        changed = find_pre_post_state_expr(fcx, pres, operand)
+          || changed;
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(operand))
+          || changed;
+        ret changed;
+    }
+    case (expr_cast(?operand, _, ?a)) {
+           changed = find_pre_post_state_expr(fcx, pres, operand)
+          || changed;
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = extend_poststate_ann(a, expr_poststate(operand))
+          || changed;
+        ret changed;
+    }
+    case (expr_fail(?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        /* if execution continues after fail, then everything is true! woo! */
+        changed = set_poststate_ann(a, false_postcond(num_local_vars))
+          || changed;
+        ret changed;
+    }
+    case (expr_assert(?p, ?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_check(?p, ?a)) {
+        changed = extend_prestate_ann(a, pres) || changed;
+        changed = find_pre_post_state_expr(fcx, pres, p) || changed;
+        /* FIXME: update the postcondition to reflect that p holds */
+        changed = extend_poststate_ann(a, pres) || changed;
+        ret changed;
+    }
+    case (expr_break(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_cont(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_port(?a)) {
+        ret pure_exp(a, pres);
+    }
+    case (expr_self_method(_, ?a)) {
+        ret pure_exp(a, pres);
+    }
+  }
+}
+
+fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
+  auto changed = false;
+  auto stmt_ann_ = stmt_to_ann(*s);
+  assert (!is_none[@ts_ann](stmt_ann_));
+  auto stmt_ann = *(get[@ts_ann](stmt_ann_));
+              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);
+  
+  alt (s.node) {
+    case (stmt_decl(?adecl, ?a)) {
+      alt (adecl.node) {
+        case (decl_local(?alocal)) {
+          alt (alocal.init) {
+            case (some[initializer](?an_init)) {
+                changed = extend_prestate(stmt_ann.states.prestate, pres)
+                    || changed;
+                changed = find_pre_post_state_expr
+                    (fcx, pres, an_init.expr) || changed;
+                changed = extend_poststate(stmt_ann.states.poststate,
+                                           expr_poststate(an_init.expr))
+                    || changed;
+                changed = gen_poststate(fcx, a, alocal.id)
+                            || changed;
+              log("Summary: stmt = ");
+              log_stmt(*s);
+              log("prestate = ");
+              log(bitv::to_str(stmt_ann.states.prestate));
+              log_bitv(fcx.enclosing, stmt_ann.states.prestate);
+              log("poststate =");
+              log_bitv(fcx.enclosing, stmt_ann.states.poststate);
+              log("changed =");
+              log(changed);
+  
+              ret changed;
+            }
+            case (none[initializer]) {
+              changed = extend_prestate(stmt_ann.states.prestate, pres)
+                  || changed;
+              changed = extend_poststate(stmt_ann.states.poststate, pres)
+                  || changed;
+              ret changed;
+            }
+          }
+        }
+        case (decl_item(?an_item)) {
+            changed = extend_prestate(stmt_ann.states.prestate, pres)
+               || changed;
+            changed = extend_poststate(stmt_ann.states.poststate, pres)
+               || changed;
+            ret (find_pre_post_state_item(fcx, an_item) || changed);
+        }
+      }
+    }
+    case (stmt_expr(?e, _)) {
+      changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+      changed = extend_prestate(stmt_ann.states.prestate, expr_prestate(e))
+          || changed;
+      changed = extend_poststate(stmt_ann.states.poststate,
+                                 expr_poststate(e)) || changed;
+      /*
+                    log("Summary: stmt = ");
+              log_stmt(*s);
+              log("prestate = ");
+              log(bitv::to_str(stmt_ann.states.prestate));
+              log_bitv(enclosing, stmt_ann.states.prestate);
+              log("poststate =");
+              log(bitv::to_str(stmt_ann.states.poststate));
+              log_bitv(enclosing, stmt_ann.states.poststate);
+              log("changed =");
+              log(changed);
+      */
+      ret changed;
+    }
+    case (_) { ret false; }
+  }
+}
+
+/* Updates the pre- and post-states of statements in the block,
+   returns a boolean flag saying whether any pre- or poststates changed */
+fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
+  -> bool {
+    
+  auto changed = false;
+  auto num_local_vars = num_locals(fcx.enclosing);
+
+  /* First, set the pre-states and post-states for every expression */
+  auto pres = pres0;
+  
+  /* Iterate over each stmt. The new prestate is <pres>. The poststate
+   consist of improving <pres> with whatever variables this stmt initializes.
+  Then <pres> becomes the new poststate. */ 
+  for (@stmt s in b.node.stmts) {
+    changed = find_pre_post_state_stmt(fcx, pres, s) || changed;
+    pres = stmt_poststate(*s, num_local_vars);
+  }
+
+  auto post = pres;
+
+  alt (b.node.expr) {
+    case (none[@expr]) {}
+    case (some[@expr](?e)) {
+      changed = find_pre_post_state_expr(fcx, pres, e) || changed;
+      post = expr_poststate(e);
+    }
+  }
+
+  /*
+  log_err("block:");
+  log_block_err(b);
+  log_err("has non-local exits?");
+  log_err(has_nonlocal_exits(b));
+  */
+
+  /* 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(b.node.a, pres0);
+  set_poststate_ann(b.node.a, post);
+
+  log("For block:");
+  log_block(b);
+  log("poststate = ");
+  log_states(block_states(b));
+  log("pres0:");
+  log_bitv(fcx.enclosing, pres0);
+  log("post:");
+  log_bitv(fcx.enclosing, post);
+
+  ret changed;
+}
+
+fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
+    /* FIXME: where do we set args as being initialized?
+       What about for methods? */
+    auto num_local_vars = num_locals(fcx.enclosing);
+    ret find_pre_post_state_block(fcx,
+          empty_prestate(num_local_vars), f.body);
+}
+
+fn find_pre_post_state_obj(crate_ctxt ccx, _obj o) -> bool {
+    fn do_a_method(crate_ctxt ccx, &@method m) -> bool {
+        assert (ccx.fm.contains_key(m.node.id));
+        ret find_pre_post_state_fn(rec(enclosing=ccx.fm.get(m.node.id),
+                                       id=m.node.id,
+                                       name=m.node.ident,
+                                       ccx=ccx),
+                                   m.node.meth);
+    }
+    auto f = bind do_a_method(ccx,_);
+    auto flags = _vec::map[@method, bool](f, o.methods);
+    auto changed = _vec::or(flags);
+    changed = changed || maybe[@method, bool](false, f, o.dtor);
+    ret changed;
+}
+
+fn find_pre_post_state_item(&fn_ctxt fcx, @item i) -> bool {
+    alt (i.node) {
+        case (item_const(?id, ?t, ?e, ?di, ?a)) {
+            ret find_pre_post_state_expr(fcx,
+                  empty_prestate(num_locals(fcx.enclosing)), e);
+        }
+        case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
+            assert (fcx.ccx.fm.contains_key(di));
+            ret find_pre_post_state_fn(rec(enclosing=fcx.ccx.fm.get(di),
+                                           id=di, name=id with fcx), f);
+        }
+        case (item_mod(?id, ?m, ?di)) {
+            ret find_pre_post_state_mod(m);
+        }
+        case (item_native_mod(?id, ?nm, ?di)) {
+            ret find_pre_post_state_native_mod(nm);
+        }
+        case (item_ty(_,_,_,_,_)) {
+            ret false;
+        }
+        case (item_tag(_,_,_,_,_)) {
+            ret false;
+        }
+        case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
+            ret find_pre_post_state_obj(fcx.ccx, o);
+        }
+    }
+}
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index 1c947e693ef..bd076fd6ce5 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -31,7 +31,7 @@ import util::common::ty_f64;
 
 import util::common::new_def_hash;
 import util::common::span;
-import util::typestate_ann::ts_ann;
+import middle::tstate::ann::ts_ann;
 
 import util::interner;
 
@@ -86,6 +86,7 @@ type t = uint;
 // AST structure in front/ast::rs as well.
 tag sty {
     ty_nil;
+    ty_bot;
     ty_bool;
     ty_int;
     ty_float;
@@ -159,7 +160,8 @@ const uint idx_str      = 16u;
 const uint idx_task     = 17u;
 const uint idx_native   = 18u;
 const uint idx_type     = 19u;
-const uint idx_first_others = 20u;
+const uint idx_bot      = 20u;
+const uint idx_first_others = 21u;
 
 type type_store = interner::interner[raw_t];
 
@@ -190,6 +192,7 @@ fn mk_type_store() -> @type_store {
     intern(ts, ty_task, none[str]);
     intern(ts, ty_native, none[str]);
     intern(ts, ty_type, none[str]);
+    intern(ts, ty_bot, none[str]);
 
     assert _vec::len(ts.vect) == idx_first_others;
 
@@ -368,6 +371,7 @@ fn gen_ty(&ctxt cx, &sty st) -> t {
 }
 
 fn mk_nil(&ctxt cx) -> t          { ret idx_nil; }
+fn mk_bot(&ctxt cx) -> t          { ret idx_bot; }
 fn mk_bool(&ctxt cx) -> t         { ret idx_bool; }
 fn mk_int(&ctxt cx) -> t          { ret idx_int; }
 fn mk_float(&ctxt cx) -> t        { ret idx_float; }
@@ -564,6 +568,7 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
     alt (struct(cx, typ)) {
         case (ty_native)       { s += "native";                         }
         case (ty_nil)          { s += "()";                             }
+        case (ty_bot)          { s += "_|_";                            }
         case (ty_bool)         { s += "bool";                           }
         case (ty_int)          { s += "int";                            }
         case (ty_float)        { s += "float";                          }
@@ -576,6 +581,7 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
         case (ty_port(?t))     { s += "port[" + ty_to_str(cx, t) + "]"; }
         case (ty_chan(?t))     { s += "chan[" + ty_to_str(cx, t) + "]"; }
         case (ty_type)         { s += "type";                           }
+        case (ty_task)         { s += "task";                           }
 
         case (ty_tup(?elems)) {
             auto f = bind mt_to_str(cx, _);
@@ -632,6 +638,11 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
             s += "''" + _str::unsafe_from_bytes(vec(('a' as u8) +
                                                     (id as u8)));
         }
+
+        case (_) {
+            s += ty_to_short_str(cx, typ);
+        }
+
     }
 
     ret s;
@@ -652,6 +663,7 @@ type ty_walk = fn(t);
 fn walk_ty(ctxt cx, ty_walk walker, t ty) {
     alt (struct(cx, ty)) {
         case (ty_nil)           { /* no-op */ }
+        case (ty_bot)           { /* no-op */ }
         case (ty_bool)          { /* no-op */ }
         case (ty_int)           { /* no-op */ }
         case (ty_uint)          { /* no-op */ }
@@ -716,6 +728,7 @@ fn fold_ty(ctxt cx, ty_fold fld, t ty_0) -> t {
     auto ty = ty_0;
     alt (struct(cx, ty)) {
         case (ty_nil)           { /* no-op */ }
+        case (ty_bot)           { /* no-op */ }
         case (ty_bool)          { /* no-op */ }
         case (ty_int)           { /* no-op */ }
         case (ty_uint)          { /* no-op */ }
@@ -821,7 +834,13 @@ fn type_is_nil(&ctxt cx, &t ty) -> bool {
         case (ty_nil) { ret true; }
         case (_) { ret false; }
     }
-    fail;
+}
+
+fn type_is_bot(&ctxt cx, &t ty) -> bool {
+    alt (struct(cx, ty)) {
+        case (ty_bot) { ret true; }
+        case (_) { ret false; }
+    }
 }
 
 fn type_is_bool(&ctxt cx, &t ty) -> bool {
@@ -1130,6 +1149,7 @@ fn hash_type_structure(&sty st) -> uint {
         case (ty_bound_param(?pid)) { ret hash_uint(31u, pid); }
         case (ty_type) { ret 32u; }
         case (ty_native) { ret 33u; }
+        case (ty_bot) { ret 34u; }
     }
 }
 
@@ -1182,6 +1202,12 @@ fn equal_type_structures(&sty a, &sty b) -> bool {
                 case (_) { ret false; }
             }
         }
+        case (ty_bot) {
+            alt(b) {
+                case (ty_bot) { ret true; }
+                case (_)      { ret false; }
+            }
+        }
         case (ty_bool) {
             alt (b) {
                 case (ty_bool) { ret true; }
@@ -1476,7 +1502,12 @@ fn triv_ann(uint node_id, t typ) -> ast::ann {
 
 // Creates a nil type annotation.
 fn plain_ann(uint node_id, ctxt tcx) -> ast::ann {
-    ret ast::ann_type(node_id, mk_nil(tcx), none[vec[ty::t]], none[@ts_ann]);
+    ret ast::ann_type(node_id, mk_nil(tcx), none[vec[t]], none[@ts_ann]);
+}
+
+// Creates a _|_ type annotation.
+fn bot_ann(uint node_id, ctxt tcx) -> ast::ann {
+    ret ast::ann_type(node_id, mk_bot(tcx), none[vec[t]], none[@ts_ann]);
 }
 
 
@@ -2099,6 +2130,7 @@ mod unify {
 
         alt (struct(cx.tcx, expected)) {
             case (ty::ty_nil)        { ret struct_cmp(cx, expected, actual); }
+            case (ty::ty_bot)        { ret struct_cmp(cx, expected, actual); }
             case (ty::ty_bool)       { ret struct_cmp(cx, expected, actual); }
             case (ty::ty_int)        { ret struct_cmp(cx, expected, actual); }
             case (ty::ty_uint)       { ret struct_cmp(cx, expected, actual); }
@@ -2675,6 +2707,20 @@ fn lookup_item_type(session::session sess,
     }
 }
 
+fn ret_ty_of_fn_ty(ty_ctxt tcx, t a_ty) -> t {
+    alt (ty::struct(tcx, a_ty)) {
+        case (ty::ty_fn(_, _, ?ret_ty)) {
+            ret ret_ty;
+        }
+        case (_) { 
+            fail;
+        }
+    }
+}
+
+fn ret_ty_of_fn(node_type_table ntt, ty_ctxt tcx, ast::ann ann) -> t {
+    ret ret_ty_of_fn_ty(tcx, ann_to_type(ntt, ann));
+}
 
 // Local Variables:
 // mode: rust
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index 9a783fbfa7b..f8ce3468359 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -25,6 +25,7 @@ import middle::ty::node_type_table;
 import middle::ty::pat_ty;
 import middle::ty::path_to_str;
 import middle::ty::plain_ann;
+import middle::ty::bot_ann;
 import middle::ty::struct;
 import middle::ty::triv_ann;
 import middle::ty::ty_param_substs_opt_and_ty;
@@ -46,7 +47,7 @@ import std::option::none;
 import std::option::some;
 import std::option::from_maybe;
 
-import util::typestate_ann::ts_ann;
+import middle::tstate::ann::ts_ann;
 
 type ty_table = hashmap[ast::def_id, ty::t];
 
@@ -271,6 +272,7 @@ fn ast_ty_to_ty(&ty::ctxt tcx, &ty_getter getter, &@ast::ty ast_ty) -> ty::t {
     auto cname = none[str];
     alt (ast_ty.node) {
         case (ast::ty_nil)          { typ = ty::mk_nil(tcx); }
+        case (ast::ty_bot)          { typ = ty::mk_bot(tcx); }
         case (ast::ty_bool)         { typ = ty::mk_bool(tcx); }
         case (ast::ty_int)          { typ = ty::mk_int(tcx); }
         case (ast::ty_uint)         { typ = ty::mk_uint(tcx); }
@@ -1060,6 +1062,7 @@ fn variant_arg_types(&@crate_ctxt ccx, &span sp, &ast::def_id vid,
         }
     }
 
+    /* result is a vector of the *expected* types of all the fields */
     ret result;
 }
 
@@ -1120,11 +1123,29 @@ mod Pushdown {
                 }
 
                 // Get the types of the arguments of the variant.
+              
+                let vec[ty::t] tparams = vec();
+                auto j = 0u;
+                auto actual_ty_params =
+                  ty::ann_to_type_params(fcx.ccx.node_types, ann);
+
+                for (ty::t some_ty in tag_tps) {
+                    let ty::t t1 = some_ty;
+                    let ty::t t2 = actual_ty_params.(j);
+                    
+                    let ty::t res = Demand::simple(fcx, 
+                                                   pat.span,
+                                                   t1, t2);
+                    
+                    _vec::push(tparams, res);
+                    j += 1u;
+                }
+
                 auto arg_tys;
                 alt (fcx.ccx.tcx.def_map.get(ast::ann_tag(ann))) {
                     case (ast::def_variant(_, ?vdefid)) {
                         arg_tys = variant_arg_types(fcx.ccx, pat.span, vdefid,
-                                                    tag_tps);
+                                                    tparams);
                     }
                 }
 
@@ -1134,10 +1155,22 @@ mod Pushdown {
                     i += 1u;
                 }
 
+                auto tps = ty::ann_to_type_params(fcx.ccx.node_types, ann);
+                auto tt  = ann_to_type(fcx.ccx.node_types, ann);
+                
+                let ty_param_substs_and_ty res_t = Demand::full(fcx, pat.span,
+                      expected, tt, tps, NO_AUTODEREF);
+
+                auto a_1 = ast::ann_type(ast::ann_tag(ann),
+                                               res_t._1,
+                                               some[vec[ty::t]](res_t._0),
+                                         none[@ts_ann]);
+
                 // TODO: push down type from "expected".
-                write_type(fcx.ccx.node_types, ast::ann_tag(ann),
+                write_type(fcx.ccx.node_types, ast::ann_tag(a_1),
                     ty::ann_to_ty_param_substs_opt_and_ty(fcx.ccx.node_types,
-                                                          ann));
+                                                          a_1));
+                    
             }
         }
     }
@@ -1843,8 +1876,12 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
             case (ty::ty_native_fn(?abi, _, _))   {
                 t_0 = ty::mk_native_fn(fcx.ccx.tcx, abi, arg_tys_0, rt_0);
             }
-            case (_) {
-                log_err "check_call_or_bind(): fn expr doesn't have fn type";
+            case (?u) {
+                fcx.ccx.sess.span_err(f.span,
+                "check_call_or_bind(): fn expr doesn't have fn type,"
+                + " instead having: " +
+                ty_to_str(fcx.ccx.tcx, expr_ty(fcx.ccx.tcx,
+                                              fcx.ccx.node_types, f_0)));
                 fail;
             }
         }
@@ -2015,15 +2052,13 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
         }
 
         case (ast::expr_fail(?a)) {
-            // TODO: should be something like 'a or noret
-            auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+            auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
             write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
             ret @fold::respan[ast::expr_](expr.span, ast::expr_fail(new_ann));
         }
 
         case (ast::expr_break(?a)) {
-            // TODO: should be something like 'a or noret
-            auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+            auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
             write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
             ret @fold::respan[ast::expr_](expr.span,
                                           ast::expr_break(new_ann));
@@ -2031,13 +2066,12 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
 
         case (ast::expr_cont(?a)) {
             // TODO: should be something like 'a or noret
-            auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+            auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
             write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
             ret @fold::respan[ast::expr_](expr.span, ast::expr_cont(new_ann));
         }
 
         case (ast::expr_ret(?expr_opt, ?a)) {
-            // TODO: should be something like 'a or noret
             alt (expr_opt) {
                 case (none[@ast::expr]) {
                     auto nil = ty::mk_nil(fcx.ccx.tcx);
@@ -2046,7 +2080,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
                                          + "returning non-nil");
                     }
 
-                    auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+                    auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
                     write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types,
                                    ast::ann_tag(a));
 
@@ -2060,7 +2094,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
                     auto expr_1 = Pushdown::pushdown_expr(fcx, fcx.ret_ty,
                                                          expr_0);
 
-                    auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+                    auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
                     write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types,
                                    ast::ann_tag(a));
 
@@ -2109,8 +2143,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
             assert (ast::is_call_expr(e));
             auto expr_0 = check_expr(fcx, e);
             auto expr_1 = Pushdown::pushdown_expr(fcx, fcx.ret_ty, expr_0);
-
-            auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
+            auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
             write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
 
             ret @fold::respan(expr.span, ast::expr_be(expr_1, new_ann));
diff --git a/src/comp/middle/walk.rs b/src/comp/middle/walk.rs
index fbf3060e968..f8a5c288874 100644
--- a/src/comp/middle/walk.rs
+++ b/src/comp/middle/walk.rs
@@ -135,6 +135,7 @@ fn walk_ty(&ast_visitor v, @ast::ty t) {
     v.visit_ty_pre(t);
     alt (t.node) {
         case (ast::ty_nil) {}
+        case (ast::ty_bot) {}
         case (ast::ty_bool) {}
         case (ast::ty_int) {}
         case (ast::ty_uint) {}
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index 78c228c5bb2..e07ed285457 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -18,9 +18,21 @@ mod middle {
     mod metadata;
     mod resolve;
     mod typeck;
-    mod typestate_check;
+    
+    mod tstate {
+        mod ck;
+        mod annotate;
+        mod aux;
+        mod bitvectors;
+        mod collect_locals;
+        mod pre_post_conditions;
+        mod states;
+        mod ann;
+    }
+    
 }
 
+
 mod pretty {
     mod pprust;
     mod pp;
@@ -53,7 +65,6 @@ mod driver {
 mod util {
     mod common;
     mod interner;
-    mod typestate_ann;
 }
 
 auth front::creader::load_crate = unsafe;
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index bccd18ed6dc..602b1458cf9 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -5,7 +5,9 @@ import std::_int;
 import std::_vec;
 import std::option::none;
 import front::ast;
-import util::typestate_ann::ts_ann;
+import front::ast::ty;
+import front::ast::pat;
+import middle::tstate::ann::ts_ann;
 
 import middle::fold;
 import middle::fold::respan;
@@ -17,6 +19,7 @@ import pretty::pprust::print_block;
 import pretty::pprust::print_expr;
 import pretty::pprust::print_decl;
 import pretty::pprust::print_fn;
+import pretty::pprust::print_type;
 import pretty::pp::mkstate;
 
 type filename = str;
@@ -127,6 +130,16 @@ fn expr_to_str(&@ast::expr e) -> str {
   ret s.get_str();
 }
 
+fn ty_to_str(&ty t) -> str {
+  let str_writer s = string_writer();
+  auto out_ = mkstate(s.get_writer(), 80u);
+  auto out = @rec(s=out_,
+                  comments=none[vec[front::lexer::cmnt]],
+                  mutable cur_cmnt=0u);
+  print_type(out, @t);
+  ret s.get_str();
+}
+
 fn log_expr(&ast::expr e) -> () {
     log(expr_to_str(@e));
 }
@@ -135,6 +148,14 @@ fn log_expr_err(&ast::expr e) -> () {
     log_err(expr_to_str(@e));
 }
 
+fn log_ty_err(&ty t) -> () {
+    log_err(ty_to_str(t));
+}
+
+fn log_pat_err(&@pat p) -> () {
+    log_err(pretty::pprust::pat_to_str(p));
+}
+
 fn block_to_str(&ast::block b) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
@@ -269,6 +290,7 @@ fn has_nonlocal_exits(&ast::block b) -> bool {
 
     ret (has_exits.size() > 0u);
 }
+
 //
 // Local Variables:
 // mode: rust