From b7dd75c904277630675e432b3398a584d882b5ac Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Mon, 18 Apr 2011 15:33:10 -0700
Subject: [PATCH] Handle nested items correctly in typestate_check

Summary says it all. Actually, only nested objects and functions
are handled, but that's better than before. The fold that I was using
before to traverse a crate wasn't working correctly, because annotations
have to reflect the number of local variables of the nearest enclosing
function (in turn, because annotations are represented as bit vectors).
The fold was traversing the AST in the wrong order, first filling in
the annotations correctly, but then re-traversing them with the bit
vector length for any outer nested functions, and so on.

Remedying this required writing a lot of tedious boilerplate code
because I scrapped the idea of using a fold altogether.

I also made typestate_check handle unary, field, alt, and fail.

Also, some miscellaneous changes:
* added annotations to blocks in typeck
* fix pprust so it can handle spawn
* added more logging functions in util.common
* fixed _vec.or
* added maybe and from_maybe in option
* removed fold_block field from ast_fold, since it was never used
---
 src/comp/middle/fold.rs                  |   3 -
 src/comp/middle/typeck.rs                |   3 +-
 src/comp/middle/typestate_check.rs       | 842 ++++++++++++++++++++---
 src/comp/pretty/pprust.rs                |  17 +
 src/comp/util/common.rs                  |  29 +
 src/comp/util/typestate_ann.rs           |  16 +
 src/lib/_vec.rs                          |   2 +-
 src/lib/option.rs                        |  12 +-
 src/test/compile-fail/use-uninit-dtor.rs |  12 +
 9 files changed, 835 insertions(+), 101 deletions(-)
 create mode 100644 src/test/compile-fail/use-uninit-dtor.rs

diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index ef592fc8ab3..25617640734 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -291,8 +291,6 @@ type ast_fold[ENV] =
      (fn(&ENV e, ann a) -> ann)                   fold_ann,
 
      // Additional nodes.
-     (fn(&ENV e, &span sp,
-         &ast.block_) -> block)                   fold_block,
 
      (fn(&ENV e, &fn_decl decl,
          ast.proto proto,
@@ -1716,7 +1714,6 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
 
          fold_ann = bind identity_fold_ann[ENV](_,_),
 
-         fold_block = bind identity_fold_block[ENV](_,_,_),
          fold_fn = bind identity_fold_fn[ENV](_,_,_,_),
          fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_),
          fold_mod = bind identity_fold_mod[ENV](_,_),
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index 87c11a7b90a..95ed4c2fd3a 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -1469,7 +1469,8 @@ mod Pushdown {
             }
             case (none[@ast.expr]) {
                 Demand.simple(fcx, bloc.span, expected, plain_ty(ty.ty_nil));
-                ret bloc;
+                ret fold.respan[ast.block_](bloc.span,
+                      rec(a = boring_ann() with bloc.node));
             }
         }
     }
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 7d7108ff82a..3e67cf2e109 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -1,12 +1,16 @@
 import front.ast;
 import front.ast.ann;
+import front.ast.method;
 import front.ast.ty;
 import front.ast.mutability;
 import front.ast.item;
 import front.ast.block;
 import front.ast.block_;
 import front.ast.block_index_entry;
+import front.ast.mod_index_entry;
+import front.ast.obj_field;
 import front.ast.decl;
+import front.ast.arm;
 import front.ast.stmt;
 import front.ast.stmt_;
 import front.ast.stmt_decl;
@@ -17,6 +21,7 @@ import front.ast.decl_item;
 import front.ast.ident;
 import front.ast.def_id;
 import front.ast.ann;
+import front.ast.field;
 import front.ast.expr;
 import front.ast.expr_call;
 import front.ast.expr_vec;
@@ -29,11 +34,33 @@ 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_expr;
+import front.ast.expr_cast;
+import front.ast.expr_for;
+import front.ast.expr_for_each;
 import front.ast.path;
+import front.ast.elt;
 import front.ast.crate_directive;
 import front.ast.fn_decl;
 import front.ast._obj;
@@ -59,6 +86,7 @@ import front.ast.crate;
 import front.ast.mod_index_entry;
 import front.ast.mie_item;
 import front.ast.item_fn;
+import front.ast.item_obj;
 import front.ast.def_local;
 
 import middle.fold;
@@ -73,6 +101,8 @@ import util.common.uistr;
 import util.common.elt_exprs;
 import util.common.field_exprs;
 import util.common.log_expr;
+import util.common.log_stmt;
+import util.common.log_block;
 import util.typestate_ann;
 import util.typestate_ann.ts_ann;
 import util.typestate_ann.empty_pre_post;
@@ -102,6 +132,7 @@ import util.typestate_ann.empty_ann;
 import util.typestate_ann.extend_prestate;
 import util.typestate_ann.extend_poststate;
 import util.typestate_ann.intersect;
+import util.typestate_ann.pp_clone;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -124,11 +155,13 @@ import std._vec.pop;
 import std._vec.push;
 import std._vec.slice;
 import std._vec.unzip;
+import std._vec.plus_option;
 import std.option;
 import std.option.t;
 import std.option.some;
 import std.option.none;
 import std.option.from_maybe;
+import std.option.maybe;
 import std.option.is_none;
 import std.option.get;
 import std.map.hashmap;
@@ -151,24 +184,6 @@ import util.typestate_ann.require_and_preserve;
 
 /**** debugging junk  ****/
 
-fn log_stmt(stmt st) -> () {
-  let str_writer s = string_writer();
-  auto out_ = mkstate(s.get_writer(), 80u);
-  auto out = @rec(s=out_,
-                  comments=option.none[vec[front.lexer.cmnt]],
-                  mutable cur_cmnt=0u);
-  alt (st.node) {
-    case (ast.stmt_decl(?decl,_)) {
-      print_decl(out, decl);
-    }
-    case (ast.stmt_expr(?ex,_)) {
-      print_expr(out, ex);
-    }
-    case (_) { /* do nothing */ }
-  }
-  log(s.get_str());
-}
-
 fn log_bitv(fn_info enclosing, bitv.t v) {
   auto s = "";
 
@@ -222,12 +237,16 @@ fn print_idents(vec[ident] idents) -> () {
 type var_info     = tup(uint, ident);
 type fn_info      = std.map.hashmap[def_id, var_info];
 /* mapping from function name to fn_info map */
-type _fn_info_map = std.map.hashmap[def_id, fn_info];
+type fn_info_map = std.map.hashmap[def_id, fn_info];
  
 fn bit_num(def_id v, fn_info m) -> uint {
   check (m.contains_key(v));
   ret m.get(v)._0;
 }
+fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
+    check (fm.contains_key(did));
+    ret fm.get(did);
+}
 
 fn var_is_local(def_id v, fn_info m) -> bool {
   ret (m.contains_key(v));
@@ -254,6 +273,7 @@ fn find_locals(_fn f) -> vec[tup(ident,def_id)] {
 }
 
 fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+    log(nm + " |-> " + util.common.uistr(next));
   tbl.insert(v, tup(next,nm));
   ret (next + 1u);
 }
@@ -277,23 +297,42 @@ fn mk_fn_info(_fn f) -> fn_info {
   ret res;
 }
 
-/* extends mk_fn_info to an item, side-effecting the map fi from
+/* 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(&_fn_info_map fi, &span sp, ident i, &ast._fn f,
+fn mk_fn_info_item_fn(&fn_info_map fi, &span sp, ident i, &ast._fn f,
                  vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
   fi.insert(id, mk_fn_info(f));
+  log(i + " has " + uistr(num_locals(mk_fn_info(f))) + " local vars");
   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(&fn_info_map fi, &span sp, ident i, &ast._obj o,
+     vec[ast.ty_param] ty_params, ast.obj_def_ids odid, ann a) -> @item {
+    auto all_methods = _vec.clone[@method](o.methods);
+    plus_option[@method](all_methods, o.dtor);
+    for (@method m in all_methods) {
+        /* FIXME: also need to pass in fields so we can say
+           they're initialized? */
+        fi.insert(m.node.id, mk_fn_info(m.node.meth));
+        log(m.node.ident + " has " +
+            uistr(num_locals(mk_fn_info(m.node.meth))) + " local vars");
+    }
+    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(@ast.crate c) -> _fn_info_map {
+fn mk_f_to_fn_info(@ast.crate c) -> fn_info_map {
   auto res = new_def_hash[fn_info]();
 
-  auto fld = fold.new_identity_fold[_fn_info_map]();
-  fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_) with *fld);
-  fold.fold_crate[_fn_info_map](res, fld, c);
+  auto fld = fold.new_identity_fold[fn_info_map]();
+  fld = @rec(fold_item_fn  = bind mk_fn_info_item_fn(_,_,_,_,_,_,_),
+             fold_item_obj = bind mk_fn_info_item_obj(_,_,_,_,_,_,_)
+               with *fld);
+  fold.fold_crate[fn_info_map](res, fld, c);
 
   ret res;
 }
@@ -438,6 +477,10 @@ fn ann_to_ts_ann_fail_more(ann a) -> @ts_ann {
   }
 }
 
+fn ann_to_poststate(ann a) -> poststate {
+    ret (ann_to_ts_ann_fail_more(a)).states.poststate;
+}
+
 fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
   alt (s.node) {
     case (stmt_decl(_,?a)) {
@@ -452,13 +495,6 @@ fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
   }
 }
 
-/*
-/* fails if no annotation */
-fn stmt_pp(&stmt s) -> pre_and_post {
-  ret (stmt_ann(s)).conditions;
-}
-*/
-
 /* fails if e has no annotation */
 fn expr_states(&expr e) -> pre_and_post_state {
   alt (expr_ann(e)) {
@@ -501,6 +537,18 @@ fn expr_pp(&expr e) -> pre_and_post {
   }
 }
 
+fn stmt_pp(&stmt s) -> pre_and_post {
+    alt (stmt_to_ann(s)) {
+        case (none[@ts_ann]) {
+            log "stmt_pp: the impossible happened (no annotation)";
+            fail;
+        }
+        case (some[@ts_ann](?p)) {
+            ret p.conditions;
+        }
+    }
+}
+
 /* fails if b has no annotation */
 /* FIXME: factor out code in the following two functions (block_ts_ann) */
 fn block_pp(&block b) -> pre_and_post {
@@ -624,18 +672,19 @@ fn with_pp(ann a, pre_and_post p) -> ann {
 // precondition shouldn't include x.
 fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
   let uint sz = len[pre_and_post](pps);
-  check(sz >= 1u);
-  auto first   = pps.(0);
-
-  if (sz > 1u) {
+ 
+  if (sz >= 1u) {
+    auto first   = pps.(0);
     check (pps_len(first) == num_vars);
     let precond rest = seq_preconds(num_vars,
                          slice[pre_and_post](pps, 1u, sz));
     difference(rest, first.postcondition);
     union(first.precondition, rest);
+    ret first.precondition;
+  }
+  else {
+      ret true_precond(num_vars);
   }
-
-  ret (first.precondition);
 }
 
 /* works on either postconds or preconds
@@ -681,18 +730,48 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
 /******* AST-traversing code ********/
 
 fn find_pre_post_mod(&_mod m) -> _mod {
-  ret m; /* FIXME */
+    log("implement find_pre_post_mod!");
+    fail;
+}
+
+fn find_pre_post_state_mod(&_mod m) -> bool {
+    log("implement find_pre_post_state_mod!");
+    fail;
 }
 
 fn find_pre_post_native_mod(&native_mod m) -> native_mod {
-  ret m; /* FIXME */
-}
- 
-fn find_pre_post_obj(_obj o) -> _obj {
-  ret o; /* FIXME */
+    log("implement find_pre_post_native_mod");
+    fail;
 }
 
-fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
+fn find_pre_post_state_native_mod(&native_mod m) -> bool {
+    log("implement find_pre_post_state_native_mod!");
+    fail;
+}
+ 
+fn find_pre_post_obj(&fn_info_map fm, _obj o) -> () {
+    fn do_a_method(fn_info_map fm, &@method m) -> () {
+        check(fm.contains_key(m.node.id));
+        find_pre_post_fn(fm, fm.get(m.node.id), m.node.meth);
+    }
+    auto f = bind do_a_method(fm,_);
+    _vec.map[@method, ()](f, o.methods);
+    option.map[@method, ()](f, o.dtor);
+}
+
+fn find_pre_post_state_obj(fn_info_map fm, _obj o) -> bool {
+    fn do_a_method(fn_info_map fm, &@method m) -> bool {
+        check(fm.contains_key(m.node.id));
+        ret find_pre_post_state_fn(fm, fm.get(m.node.id), m.node.meth);
+    }
+    auto f = bind do_a_method(fm,_);
+    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_item(fn_info_map fm, fn_info enclosing, &item i) -> () {
   alt (i.node) {
     case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
         find_pre_post_expr(fm, enclosing, *e);
@@ -714,7 +793,7 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
       ret;
     }
     case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
-      find_pre_post_obj(o);
+        find_pre_post_obj(fm, o);
     }
   }
 }
@@ -723,9 +802,9 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
    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_info_map fm, &fn_info enclosing,
+fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing,
                        &vec[@expr] args, ann a) {
-    fn do_one(_fn_info_map fm, fn_info enclosing,
+    fn do_one(fn_info_map fm, fn_info enclosing,
               &@expr e) -> () {
         find_pre_post_expr(fm, enclosing, *e);
     }
@@ -747,16 +826,21 @@ fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
 }
 
 /* Fills in annotations as a side effect. Does not rebuild the expr */
-fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
+fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
     auto num_local_vars = num_locals(enclosing);
 
-    fn do_rand_(_fn_info_map fm, fn_info enclosing, &@expr e) -> () {
+    fn do_rand_(fn_info_map fm, fn_info enclosing, &@expr e) -> () {
         find_pre_post_expr(fm, enclosing, *e);
     }
     fn pp_one(&@expr e) -> pre_and_post {
         be expr_pp(*e);
     }
 
+    /*    log("find_pre_post_expr (num_locals =" +
+             uistr(num_local_vars) + "):");
+          log_expr(e);
+    */
+
     alt(e.node) {
         case(expr_call(?operator, ?operands, ?a)) {
             auto args = _vec.clone[@expr](operands);
@@ -866,6 +950,10 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
              FIXME */
             find_pre_post_exprs(fm, enclosing, vec(l, r), a);
         }
+        case (expr_unary(_,?operand,?a)) {
+            find_pre_post_expr(fm, enclosing, *operand);
+            set_pre_and_post(a, expr_pp(*operand));
+        }
         case (expr_while(?test, ?body, ?a)) {
             find_pre_post_expr(fm, enclosing, *test);
             find_pre_post_block(fm, enclosing, body);
@@ -881,8 +969,41 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
         case (expr_index(?e, ?sub, ?a)) {
             find_pre_post_exprs(fm, enclosing, vec(e, sub), a);
         }
+        case (expr_alt(?e, ?alts, ?a)) {
+            find_pre_post_expr(fm, enclosing, *e);
+            fn do_an_alt(fn_info_map fm, fn_info enc, &arm an_alt)
+                -> pre_and_post {
+                find_pre_post_block(fm, enc, an_alt.block);
+                ret block_pp(an_alt.block);
+            }
+            auto f = bind do_an_alt(fm, enclosing, _);
+            auto alt_pps = _vec.map[arm, pre_and_post](f, alts);
+            fn combine_pp(pre_and_post antec, 
+                          uint num_local_vars, &pre_and_post pp,
+                          &pre_and_post next) -> pre_and_post {
+                union(pp.precondition, seq_preconds(num_local_vars,
+                                         vec(antec, next)));
+                intersect(pp.postcondition, next.postcondition);
+                ret pp;
+            }
+            auto e_pp1 = expr_pp(*e);
+            auto e_pp  = pp_clone(e_pp1);
+            auto g = bind combine_pp(e_pp, num_local_vars, _, _);
+            set_pre_and_post(a, _vec.foldl[pre_and_post, pre_and_post]
+                             (g, e_pp, alt_pps));
+        }
+        case (expr_field(?operator, _, ?a)) {
+            find_pre_post_expr(fm, enclosing, *operator);
+            set_pre_and_post(a, expr_pp(*operator));
+        }
+        case (expr_fail(?a)) {
+            set_pre_and_post(a,
+               rec(precondition=empty_prestate(num_local_vars),
+                   postcondition=true_postcond(num_local_vars)));
+        }
         case(_) {
             log("this sort of expr isn't implemented!");
+            log_expr(e);
             fail;
         }
     }
@@ -902,7 +1023,7 @@ fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
   ret set_in_poststate(i, (ann_to_ts_ann_fail_more(a)).states);
 }
 
-fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
+fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
     -> () {
   auto num_local_vars = num_locals(enclosing);
   alt(s.node) {
@@ -941,27 +1062,49 @@ fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
   }
 }
 
-fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
+fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b)
     -> () {
-    fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> () {
+    fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () {
         find_pre_post_stmt(fm, i, *s);
     }
     auto do_one = bind do_one_(fm, enclosing, _);
     
     _vec.map[@stmt, ()](do_one, b.node.stmts);
-    fn do_inner_(_fn_info_map fm, fn_info i, &@expr e) -> () {
+    fn do_inner_(fn_info_map fm, fn_info i, &@expr e) -> () {
         find_pre_post_expr(fm, i, *e);
     }
     auto do_inner = bind do_inner_(fm, enclosing, _);
     option.map[@expr, ()](do_inner, b.node.expr);
-    /* FIXME needs to set up the ann for b!!!!!!!!!!! */
+
+    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(num_locals(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 = union_postconds(postconds);
+    set_pre_and_post(b.node.a, rec(precondition=block_precond,
+                                   postcondition=block_postcond));
 }
 
-fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> () {
+fn find_pre_post_fn(&fn_info_map fm, &fn_info fi, &_fn f) -> () {
     find_pre_post_block(fm, fi, f.body);
 }
 
-fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
+fn check_item_fn(&fn_info_map fm, &span sp, ident i, &ast._fn f,
                  vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
 
   check (fm.contains_key(id));
@@ -970,10 +1113,33 @@ fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
   ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
 }
 
-/* FIXME */
-fn find_pre_post_state_item(_fn_info_map fm, @item i) -> bool {
-  log("Implement find_pre_post_item!");
-  fail;
+fn find_pre_post_state_item(fn_info_map fm, fn_info enclosing, @item i)
+   -> bool {
+ alt (i.node) {
+    case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
+        ret find_pre_post_state_expr(fm, enclosing,
+              empty_prestate(num_locals(enclosing)), e);
+    }
+    case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
+      check (fm.contains_key(di));
+      ret find_pre_post_state_fn(fm, fm.get(di), f);
+    }
+    case (ast.item_mod(?id, ?m, ?di)) {
+      ret find_pre_post_state_mod(m);
+    }
+    case (ast.item_native_mod(?id, ?nm, ?di)) {
+      ret find_pre_post_state_native_mod(nm);
+    }
+    case (ast.item_ty(_,_,_,_,_)) {
+      ret false;
+    }
+    case (ast.item_tag(_,_,_,_,_)) {
+      ret false;
+    }
+    case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
+        ret find_pre_post_state_obj(fm, o);
+    }
+  }
 }
 
 fn set_prestate_ann(ann a, prestate pre) -> bool {
@@ -1034,6 +1200,11 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
         case (ann_type(_,_,?ts_a)) {
             check (! is_none[@ts_ann](ts_a));
             auto t = *get[@ts_ann](ts_a);
+            /*  log("set_pre_and_post, old =");
+            log_pp(t.conditions);
+            log("new =");
+            log_pp(pp);
+            */
             set_precondition(t, pp.precondition);
             set_postcondition(t, pp.postcondition);
         }
@@ -1044,7 +1215,7 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
     }
 }
 
-fn seq_states(&_fn_info_map fm, &fn_info enclosing,
+fn seq_states(&fn_info_map fm, &fn_info enclosing,
     prestate pres, vec[@expr] exprs) -> tup(bool, poststate) {
   auto changed = false;
   auto post = pres;
@@ -1057,7 +1228,7 @@ fn seq_states(&_fn_info_map fm, &fn_info enclosing,
   ret tup(changed, post);
 }
 
-fn find_pre_post_state_exprs(&_fn_info_map fm,
+fn find_pre_post_state_exprs(&fn_info_map fm,
                              &fn_info enclosing,
                              &prestate pres,
                              &ann a, &vec[@expr] es) -> bool {
@@ -1075,7 +1246,7 @@ fn pure_exp(&ann a, &prestate p) -> bool {
   ret changed;
 }
 
-fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
                             &prestate pres, &@expr e) -> bool {
   auto changed = false;
   auto num_local_vars = num_locals(enclosing);
@@ -1224,6 +1395,39 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
         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(fm, enclosing, pres, e) || changed;
+        auto e_post = expr_poststate(*e);
+        auto a_post = ann_to_poststate(a);
+        for (arm an_alt in alts) {
+            changed = find_pre_post_state_block(fm, enclosing, e_post,
+                        an_alt.block) || changed;
+            changed = intersect(a_post, block_poststate(an_alt.block))
+               || changed;
+        }
+        ret changed;
+    }
+    case (expr_field(?e,_,?a)) {
+        changed = find_pre_post_state_expr(fm, enclosing, 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(fm, enclosing, 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;
+        changed = set_poststate_ann(a, true_postcond(num_local_vars))
+          || changed;
+        ret changed;
+    }
     case (_) {
       log("find_pre_post_state_expr: implement this case!");
       fail;
@@ -1232,7 +1436,7 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
 
 }
 
-fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
                             &prestate pres, @stmt s) -> bool {
   auto changed = false;
   auto stmt_ann_ = stmt_to_ann(*s);
@@ -1285,7 +1489,7 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
           }
         }
         case (ast.decl_item(?an_item)) {
-          be find_pre_post_state_item(fm, an_item);
+            be find_pre_post_state_item(fm, enclosing, an_item);
         }
       }
     }
@@ -1314,7 +1518,7 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
 
 /* 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_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing,
                              &prestate pres0, block b)
   -> bool {
 
@@ -1332,24 +1536,31 @@ fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing,
     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(fm, enclosing, pres, e) || changed;
+      post = expr_poststate(*e);
     }
   }
+  set_prestate_ann(b.node.a, pres0);
+  set_poststate_ann(b.node.a, post);
   ret changed;
 }
 
-fn find_pre_post_state_fn(&_fn_info_map f_info, &fn_info fi, &ast._fn f)
+fn find_pre_post_state_fn(&fn_info_map f_info, &fn_info fi, &ast._fn f)
   -> bool {
+    /* FIXME: where do we set args as being initialized?
+       What about for methods? */
     auto num_local_vars = num_locals(fi);
     ret find_pre_post_state_block(f_info, fi,
                                   empty_prestate(num_local_vars), f.body);
 }
 
-fn fixed_point_states(_fn_info_map fm, fn_info f_info,
-                      fn (&_fn_info_map, &fn_info, &ast._fn) -> bool f,
+fn fixed_point_states(fn_info_map fm, fn_info f_info,
+                      fn (&fn_info_map, &fn_info, &ast._fn) -> bool f,
                       &ast._fn start) -> () {
 
   auto changed = f(fm, f_info, start);
@@ -1368,7 +1579,7 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () {
   let prestate pres   = expr_prestate(e);
 
   if (!implies(pres, prec)) {
-      log("check_states_stmt: unsatisfied precondition for ");
+      log("check_states_expr: unsatisfied precondition for ");
       log_expr(e);
       log("Precondition: ");
       log_bitv(enclosing, prec);
@@ -1424,14 +1635,8 @@ fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
   
 }
 
-fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
-                       &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
-                       ann a) -> @item {
-
-  /* Look up the var-to-bit-num map for this function */
-  check(f_info_map.contains_key(id));
-  auto f_info = f_info_map.get(id);
-
+fn check_fn_states(&fn_info_map f_info_map, &fn_info f_info, &ast._fn f)
+    -> () {
   /* Compute the pre- and post-states for this function */
   auto g = find_pre_post_state_fn;
   fixed_point_states(f_info_map, f_info, g, f);
@@ -1439,11 +1644,39 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
   /* Now compare each expr's pre-state to its precondition
      and post-state to its postcondition */
   check_states_against_conditions(f_info, f);
+}
+
+fn check_item_fn_state(&fn_info_map f_info_map, &span sp, ident i,
+                       &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
+                       ann a) -> @item {
+
+  /* Look up the var-to-bit-num map for this function */
+  check(f_info_map.contains_key(id));
+  auto f_info = f_info_map.get(id);
+
+  check_fn_states(f_info_map, f_info, f);
 
   /* Rebuild the same function */
   ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
 }
 
+fn check_method_states(&fn_info_map f_info_map, @method m) -> () {
+    check (f_info_map.contains_key(m.node.id));
+    auto f_info = f_info_map.get(m.node.id);
+    check_fn_states(f_info_map, f_info, m.node.meth);
+}
+
+fn check_obj_state(&fn_info_map f_info_map, vec[obj_field] fields,
+                  vec[@method] methods, option.t[@method] dtor) -> ast._obj {
+    fn one(fn_info_map fm, &@method m) -> () {
+        ret check_method_states(fm, m);
+    }
+    auto f = bind one(f_info_map,_);
+    _vec.map[@method, ()](f, methods);
+    option.map[@method, ()](f, dtor);
+    ret rec(fields=fields, methods=methods, dtor=dtor);
+}
+
 fn init_ann(&fn_info fi, ann a) -> ann {
     alt (a) {
         case (ann_none) {
@@ -1456,42 +1689,467 @@ fn init_ann(&fn_info fi, ann a) -> ann {
     }
 }
 
-fn item_fn_anns(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
+fn init_blank_ann(&() ignore, ann a) -> ann {
+    alt (a) {
+        case (ann_none) {
+            log("init_ann: shouldn't see ann_none");
+            fail;
+        }
+        case (ann_type(?t,?ps,_)) {
+            ret ann_type(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_ann: shouldn't see ann_none");
+            fail;
+        }
+        case (ann_type(?t,?ps,_)) {
+            auto fld0 = fold.new_identity_fold[fn_info]();
+
+            fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+            ret fold.fold_block[fn_info](fi, fld0, respan(sp, b)); 
+        }
+    }
+    
+}
+
+fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast._fn f,
                 vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
 
     check(fm.contains_key(id));
     auto f_info = fm.get(id);
 
+    log(i + " has " + uistr(num_locals(f_info)) + " local vars");
+
     auto fld0 = fold.new_identity_fold[fn_info]();
 
-    fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                //   fold_block = bind init_block(_,_,_)
+                    with *fld0);
 
     ret fold.fold_item[fn_info]
            (f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a))); 
 }
 
-fn check_crate(@ast.crate crate) -> @ast.crate {
+/* 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),
+                 index=a.index);
+    }
+    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, ?e_opt, ?e, ?a)) {
+            e1 = expr_ext(p, annotate_exprs(fm, es),
+                          annotate_option_exp(fm, e_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_check_expr(?e, ?a)) {
+            e1 = expr_check_expr(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();
+    auto new_index = new_str_hash[block_index_entry]();
+
+    for (@stmt s in b.node.stmts) {
+        auto new_s = annotate_stmt(fm, s);
+        _vec.push[@stmt](new_stmts, new_s);
+        ast.index_stmt(new_index, 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, index=new_index with b.node));
+}
+fn annotate_fn(&fn_info_map fm, &ast._fn f) -> ast._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, &ast._mod m) -> ast._mod {
+    let vec[@item] new_items = vec();
+    auto new_index = new_str_hash[mod_index_entry]();
+
+    for (@item i in m.items) {
+        auto new_i = annotate_item(fm, i);
+        _vec.push[@item](new_items, new_i);
+        ast.index_item(new_index, new_i);
+    }
+    ret rec(items=new_items, index=new_index with m);
+}
+fn annotate_native_mod(&fn_info_map fm, &ast.native_mod m)
+       -> ast.native_mod {
+    log("implement annotate_native_mod!");
+    fail;
+}
+fn annotate_method(&fn_info_map fm, &@method m) -> @method {
+    auto f_info = get_fn_info(fm, m.node.id);
+    auto fld0 = fold.new_identity_fold[fn_info]();
+    fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                with *fld0);
+    auto outer = fold.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, &ast._obj o) -> ast._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, &@ast.item item) -> @ast.item {
+    alt (item.node) {
+        /* FIXME can't skip this case -- exprs contain blocks contain stmts,
+         which contain decls */
+        case (ast.item_const(_,_,_,_,_)) {
+            // this has already been annotated by annotate_item
+            ret item;
+        }
+        case (ast.item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
+            ret @respan(item.span,
+                       ast.item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
+        }
+        case (ast.item_mod(?ident, ?mm, ?id)) {
+            ret @respan(item.span,
+                       ast.item_mod(ident, annotate_mod(fm, mm), id));
+        }
+        case (ast.item_native_mod(?ident, ?mm, ?id)) {
+            ret @respan(item.span,
+                  ast.item_native_mod(ident, 
+                    annotate_native_mod(fm, mm), id));
+        }
+        case (ast.item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
+            ret @respan(item.span,
+              ast.item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
+        }
+    } 
+}
+
+fn annotate_item(&fn_info_map fm, &@ast.item item) -> @ast.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 (ast.item_const(_,_,_,_,_)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            ret fold.fold_item[()]((), fld0, item);
+        }
+        case (ast.item_fn(?i,?ff,?tps,?id,?ann)) {
+            auto f_info = get_fn_info(fm, id);
+            auto fld0 = fold.new_identity_fold[fn_info]();
+            fld0 = @rec(fold_ann = bind init_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[fn_info](f_info, fld0, item);
+            // now recurse into any nested items
+            ret annotate_item_inner(fm, outer);
+         }
+        case (ast.item_mod(?i, ?mm, ?id)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+        case (ast.item_ty(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_tag(_,_,_,_,_)) {
+            ret item;
+        }
+        case (ast.item_obj(?i,?ob,?tps,?odid,?ann)) {
+            auto fld0 = fold.new_identity_fold[()]();
+            fld0 = @rec(fold_ann = bind init_blank_ann(_,_) 
+                        with *fld0);
+            auto outer = fold.fold_item[()]((), fld0, item);
+            ret annotate_item_inner(fm, outer);
+        }
+    }
+}
+
+fn annotate_module(&fn_info_map fm, &ast._mod module) -> ast._mod {
+    let vec[@item] new_items = vec();
+    auto new_index = new_str_hash[ast.mod_index_entry]();
+
+    for (@item i in module.items) {
+        auto new_item = annotate_item(fm, i);
+        _vec.push[@item](new_items, new_item);
+        ast.index_item(new_index, new_item);
+    }
+
+    ret rec(items = new_items, index = new_index with module);
+}
+
+fn annotate_crate(&fn_info_map fm, &@ast.crate crate) -> @ast.crate {
+    ret @respan(crate.span,
+               rec(module = annotate_module(fm, crate.node.module)
+                   with crate.node));
+}
+
+fn check_crate(@ast.crate crate) -> @ast.crate {
   /* Build the global map from function id to var-to-bit-num-map */
-  auto fn_info_map = mk_f_to_fn_info(crate);
+  auto fm = mk_f_to_fn_info(crate);
   
   /* Add a blank ts_ann to every statement (and expression) */
-  auto fld0 = fold.new_identity_fold[_fn_info_map]();
-  fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_) with *fld0);
-  auto with_anns = fold.fold_crate[_fn_info_map](fn_info_map, fld0, crate);
+  /*
+  auto fld0 = fold.new_identity_fold[fn_info_map]();
+  fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_)
+              with *fld0);
+  */
+  auto with_anns = annotate_crate(fm, crate);
   
   /* Compute the pre and postcondition for every subexpression */
-  auto fld = fold.new_identity_fold[_fn_info_map]();
+  auto fld = fold.new_identity_fold[fn_info_map]();
   fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
-  auto with_pre_postconditions = fold.fold_crate[_fn_info_map]
-    (fn_info_map, fld, with_anns);
+  auto with_pre_postconditions = fold.fold_crate[fn_info_map]
+    (fm, fld, with_anns);
 
-  auto fld1 = fold.new_identity_fold[_fn_info_map]();
+  auto fld1 = fold.new_identity_fold[fn_info_map]();
 
-  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_)
+  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_),
+              fold_obj     = bind check_obj_state(_,_,_,_)
               with *fld1);
 
-  ret fold.fold_crate[_fn_info_map](fn_info_map, fld1,
+  ret fold.fold_crate[fn_info_map](fm, fld1,
                                     with_pre_postconditions);
 }
 
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index cf606d9e6f1..e49ed34e948 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -475,6 +475,13 @@ fn print_expr(ps s, &@ast.expr expr) {
             commasep[option.t[@ast.expr]](s, args, f);
             pclose(s);
         }
+    case (ast.expr_spawn(_,_,?e,?es,_)) {
+          wrd1(s, "spawn");
+          print_expr(s, e);
+          popen(s);
+          commasep_exprs(s, es);
+          pclose(s);
+        }
         case (ast.expr_binary(?op,?lhs,?rhs,_)) {
             auto prec = operator_prec(op);
             print_maybe_parens(s, lhs, prec);
@@ -1018,3 +1025,13 @@ fn print_comment(ps s, lexer.cmnt_ cmnt) {
         }
     }
 }
+//
+// 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/util/common.rs b/src/comp/util/common.rs
index 006bccb0683..af000cb6d0a 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -137,6 +137,35 @@ fn log_block(&ast.block b) -> () {
   log(s.get_str());
 }
 
+fn log_ann(&ast.ann a) -> () {
+    alt (a) {
+        case (ast.ann_none) {
+            log("ann_none");
+        }
+        case (ast.ann_type(_,_,_)) {
+            log("ann_type");
+        }
+    }
+}
+
+fn log_stmt(ast.stmt st) -> () {
+  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);
+  alt (st.node) {
+    case (ast.stmt_decl(?decl,_)) {
+      print_decl(out, decl);
+    }
+    case (ast.stmt_expr(?ex,_)) {
+      print_expr(out, ex);
+    }
+    case (_) { /* do nothing */ }
+  }
+  log(s.get_str());
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index b1f12ffbc87..9ad6e01e8dd 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -147,6 +147,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
   ret a.states.prestate;
 }
 
+fn pp_clone(&pre_and_post p) -> pre_and_post {
+  ret rec(precondition=bitv.clone(p.precondition),
+          postcondition=bitv.clone(p.postcondition));
+}
+
 // returns true if a implies b
 // that is, returns true except if for some bits c and d,
 // c = 1 and d = 0
@@ -155,3 +160,14 @@ fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(tmp, a);
   ret bitv.is_false(tmp);
 }
+
+//
+// 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/lib/_vec.rs b/src/lib/_vec.rs
index 6fc1d700886..cc8fabcaf16 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -266,7 +266,7 @@ fn unzip[T, U](&vec[tup(T, U)] v) -> tup(vec[T], vec[U]) {
 
 fn or(&vec[bool] v) -> bool {
     auto f = orb;
-    be _vec.foldl[bool, bool](f, false, v);
+    ret _vec.foldl[bool, bool](f, false, v);
 }
 
 fn clone[T](&vec[T] v) -> vec[T] {
diff --git a/src/lib/option.rs b/src/lib/option.rs
index 66a41bcac68..e214c77487f 100644
--- a/src/lib/option.rs
+++ b/src/lib/option.rs
@@ -39,12 +39,16 @@ fn is_none[T](&t[T] opt) -> bool {
 }
 
 fn from_maybe[T](&T def, &t[T] opt) -> T {
-    alt(opt) {
-        case (none[T])     { ret def; }
-        case (some[T](?t)) { ret t; }
-    }
+    auto f = bind util.id[T](_);
+    ret maybe[T, T](def, f, opt);
 }
 
+fn maybe[T, U](&U def, fn(&T) -> U f, &t[T] opt) -> U {
+    alt (opt) {
+        case (none[T]) { ret def; }
+        case (some[T](?t)) { ret f(t); }
+    }
+}
 // Local Variables:
 // mode: rust;
 // fill-column: 78;
diff --git a/src/test/compile-fail/use-uninit-dtor.rs b/src/test/compile-fail/use-uninit-dtor.rs
new file mode 100644
index 00000000000..be2f1727a6f
--- /dev/null
+++ b/src/test/compile-fail/use-uninit-dtor.rs
@@ -0,0 +1,12 @@
+// xfail-stage0
+// error-pattern:Unsatisfied precondition
+
+fn main() {
+ state obj foo(int x) {
+        drop {
+          let int baz;
+          log(baz);
+        }
+ }
+ fail;
+}