Continued sketching out code for checking states against preconditions.

It's still sketchy. I added a typestate annotation field to statements
tagged stmt_decl or stmt_expr, because a stmt_decl statement has a typestate
that's different from that of its child node. This necessitated trivial
changes to a bunch of other files all over to the compiler. I also added a
few small standard library functions, some of which I didn't actually end
up using but which I thought might be useful anyway.

16 files changed, 343 insertions, 132 deletions

diff --git a/.gitignore b/.gitignore
index dbfd7846..184f1402 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,3 +52,4 @@ config.mk
 /test/
 /build/
 src/.DS_Store
+/stage0/
diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index d41e6d60..cf4145a5 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -215,8 +215,8 @@ tag mode {
 
 type stmt = spanned[stmt_];
 tag stmt_ {
-    stmt_decl(@decl);
-    stmt_expr(@expr);
+    stmt_decl(@decl, option.t[@ts_ann]);
+    stmt_expr(@expr, option.t[@ts_ann]);
     // These only exist in crate-level blocks.
     stmt_crate_directive(@crate_directive);
 }
@@ -495,7 +495,7 @@ fn index_native_view_item(native_mod_index index, @view_item it) {
 
 fn index_stmt(block_index index, @stmt s) {
     alt (s.node) {
-        case (ast.stmt_decl(?d)) {
+        case (ast.stmt_decl(?d,_)) {
             alt (d.node) {
                 case (ast.decl_local(?loc)) {
                     index.insert(loc.ident, ast.bie_local(loc));
diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs
index 27fdc7fe..7d1323cb 100644
--- a/src/comp/front/parser.rs
+++ b/src/comp/front/parser.rs
@@ -11,6 +11,7 @@ import util.common;
 import util.common.filename;
 import util.common.span;
 import util.common.new_str_hash;
+import util.typestate_ann.ts_ann;
 
 tag restriction {
     UNRESTRICTED;
@@ -1555,13 +1556,13 @@ impure fn parse_source_stmt(parser p) -> @ast.stmt {
         case (token.LET) {
             auto decl = parse_let(p);
             auto hi = p.get_span();
-            ret @spanned(lo, hi, ast.stmt_decl(decl));
+            ret @spanned(lo, hi, ast.stmt_decl(decl, none[@ts_ann]));
         }
 
         case (token.AUTO) {
             auto decl = parse_auto(p);
             auto hi = p.get_span();
-            ret @spanned(lo, hi, ast.stmt_decl(decl));
+            ret @spanned(lo, hi, ast.stmt_decl(decl, none[@ts_ann]));
         }
 
         case (_) {
@@ -1570,13 +1571,13 @@ impure fn parse_source_stmt(parser p) -> @ast.stmt {
                 auto i = parse_item(p);
                 auto hi = i.span;
                 auto decl = @spanned(lo, hi, ast.decl_item(i));
-                ret @spanned(lo, hi, ast.stmt_decl(decl));
+                ret @spanned(lo, hi, ast.stmt_decl(decl, none[@ts_ann]));
 
             } else {
                 // Remainder are line-expr stmts.
                 auto e = parse_expr(p);
                 auto hi = p.get_span();
-                ret @spanned(lo, hi, ast.stmt_expr(e));
+                ret @spanned(lo, hi, ast.stmt_expr(e, none[@ts_ann]));
             }
         }
     }
@@ -1613,7 +1614,7 @@ fn index_arm(@ast.pat pat) -> hashmap[ast.ident,ast.def_id] {
 
 fn stmt_to_expr(@ast.stmt stmt) -> option.t[@ast.expr] {
     alt (stmt.node) {
-        case (ast.stmt_expr(?e)) { ret some[@ast.expr](e); }
+        case (ast.stmt_expr(?e,_)) { ret some[@ast.expr](e); }
         case (_) { /* fall through */ }
     }
     ret none[@ast.expr];
@@ -1621,13 +1622,13 @@ fn stmt_to_expr(@ast.stmt stmt) -> option.t[@ast.expr] {
 
 fn stmt_ends_with_semi(@ast.stmt stmt) -> bool {
     alt (stmt.node) {
-        case (ast.stmt_decl(?d)) {
+        case (ast.stmt_decl(?d,_)) {
             alt (d.node) {
                 case (ast.decl_local(_)) { ret true; }
                 case (ast.decl_item(_)) { ret false; }
             }
         }
-        case (ast.stmt_expr(?e)) {
+        case (ast.stmt_expr(?e,_)) {
             alt (e.node) {
                 case (ast.expr_vec(_,_,_))      { ret true; }
                 case (ast.expr_tup(_,_))        { ret true; }
diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index 77c89836..fa85f791 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -7,6 +7,7 @@ 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 front.ast;
 import front.ast.fn_decl;
@@ -232,10 +233,12 @@ type ast_fold[ENV] =
 
      // Stmt folds.
      (fn(&ENV e, &span sp,
-         @decl decl) -> @stmt)                    fold_stmt_decl,
+         @decl decl, option.t[@ts_ann] a)
+      -> @stmt)                                   fold_stmt_decl,
 
      (fn(&ENV e, &span sp,
-         @expr e) -> @stmt)                       fold_stmt_expr,
+         @expr e, option.t[@ts_ann] a)
+      -> @stmt)                                   fold_stmt_expr,
 
      // Item folds.
      (fn(&ENV e, &span sp, ident ident,
@@ -788,14 +791,14 @@ fn fold_stmt[ENV](&ENV env, ast_fold[ENV] fld, &@stmt s) -> @stmt {
     }
 
     alt (s.node) {
-        case (ast.stmt_decl(?d)) {
+        case (ast.stmt_decl(?d, ?a)) {
             auto dd = fold_decl(env_, fld, d);
-            ret fld.fold_stmt_decl(env_, s.span, dd);
+            ret fld.fold_stmt_decl(env_, s.span, dd, a);
         }
 
-        case (ast.stmt_expr(?e)) {
+        case (ast.stmt_expr(?e, ?a)) {
             auto ee = fold_expr(env_, fld, e);
-            ret fld.fold_stmt_expr(env_, s.span, ee);
+            ret fld.fold_stmt_expr(env_, s.span, ee, a);
         }
     }
     fail;
@@ -1386,12 +1389,14 @@ fn identity_fold_pat_tag[ENV](&ENV e, &span sp, path p, vec[@pat] args,
 
 // Stmt identities.
 
-fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d) -> @stmt {
-    ret @respan(sp, ast.stmt_decl(d));
+fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d,
+                                option.t[@ts_ann] a) -> @stmt {
+    ret @respan(sp, ast.stmt_decl(d, a));
 }
 
-fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x) -> @stmt {
-    ret @respan(sp, ast.stmt_expr(x));
+fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x,
+                                option.t[@ts_ann] a) -> @stmt {
+    ret @respan(sp, ast.stmt_expr(x, a));
 }
 
 
@@ -1642,8 +1647,8 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
          fold_pat_bind    = bind identity_fold_pat_bind[ENV](_,_,_,_,_),
          fold_pat_tag     = bind identity_fold_pat_tag[ENV](_,_,_,_,_,_),
 
-         fold_stmt_decl   = bind identity_fold_stmt_decl[ENV](_,_,_),
-         fold_stmt_expr   = bind identity_fold_stmt_expr[ENV](_,_,_),
+         fold_stmt_decl   = bind identity_fold_stmt_decl[ENV](_,_,_,_),
+         fold_stmt_expr   = bind identity_fold_stmt_expr[ENV](_,_,_,_),
 
          fold_item_const= bind identity_fold_item_const[ENV](_,_,_,_,_,_,_),
          fold_item_fn   = bind identity_fold_item_fn[ENV](_,_,_,_,_,_,_),
diff --git a/src/comp/middle/resolve.rs b/src/comp/middle/resolve.rs
index 20e60971..28ae07dc 100644
--- a/src/comp/middle/resolve.rs
+++ b/src/comp/middle/resolve.rs
@@ -6,6 +6,7 @@ import front.creader;
 import driver.session;
 import util.common.new_def_hash;
 import util.common.span;
+import util.typestate_ann.ts_ann;
 import std.map.hashmap;
 import std.list.list;
 import std.list.nil;
@@ -348,7 +349,7 @@ fn lookup_name_wrapped(&env e, ast.ident i, namespace ns)
 
     fn found_decl_stmt(@ast.stmt s, namespace ns) -> def_wrap {
         alt (s.node) {
-            case (ast.stmt_decl(?d)) {
+            case (ast.stmt_decl(?d,_)) {
                 alt (d.node) {
                     case (ast.decl_local(?loc)) {
                         auto t = ast.def_local(loc.id);
diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index 980c88db..fff3f126 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -5208,11 +5208,11 @@ fn init_local(@block_ctxt cx, @ast.local local) -> result {
 fn trans_stmt(@block_ctxt cx, &ast.stmt s) -> result {
     auto bcx = cx;
     alt (s.node) {
-        case (ast.stmt_expr(?e)) {
+        case (ast.stmt_expr(?e,_)) {
             bcx = trans_expr(cx, e).bcx;
         }
 
-        case (ast.stmt_decl(?d)) {
+        case (ast.stmt_decl(?d,_)) {
             alt (d.node) {
                 case (ast.decl_local(?local)) {
                     bcx = init_local(bcx, local).bcx;
@@ -5302,7 +5302,7 @@ iter block_locals(&ast.block b) -> @ast.local {
     // use the index here.
     for (@ast.stmt s in b.node.stmts) {
         alt (s.node) {
-            case (ast.stmt_decl(?d)) {
+            case (ast.stmt_decl(?d,_)) {
                 alt (d.node) {
                     case (ast.decl_local(?local)) {
                         put local;
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index f83bece7..09c89fdf 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -731,7 +731,7 @@ fn item_ty(@ast.item it) -> ty_params_and_ty {
 
 fn stmt_ty(@ast.stmt s) -> @t {
     alt (s.node) {
-        case (ast.stmt_expr(?e)) {
+        case (ast.stmt_expr(?e,_)) {
             ret expr_ty(e);
         }
         case (_) {
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index ab0262f1..d969df5a 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -2479,12 +2479,12 @@ fn check_decl_local(&@fn_ctxt fcx, &@ast.decl decl) -> @ast.decl {
 
 fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
     alt (stmt.node) {
-        case (ast.stmt_decl(?decl)) {
+        case (ast.stmt_decl(?decl,?a)) {
             alt (decl.node) {
                 case (ast.decl_local(_)) {
                     auto decl_1 = check_decl_local(fcx, decl);
                     ret @fold.respan[ast.stmt_](stmt.span,
-                                                ast.stmt_decl(decl_1));
+                                                ast.stmt_decl(decl_1, a));
                 }
 
                 case (ast.decl_item(_)) {
@@ -2495,9 +2495,9 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
             ret stmt;
         }
 
-        case (ast.stmt_expr(?expr)) {
+        case (ast.stmt_expr(?expr,?a)) {
             auto expr_t = check_expr(fcx, expr);
-            ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t));
+            ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t, a));
         }
     }
 
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 64a17a7d..24bee1bd 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -11,6 +11,7 @@ import front.ast.stmt;
 import front.ast.stmt_;
 import front.ast.stmt_decl;
 import front.ast.stmt_expr;
+import front.ast.stmt_crate_directive;
 import front.ast.decl_local;
 import front.ast.decl_item;
 import front.ast.ident;
@@ -70,9 +71,17 @@ import util.typestate_ann.prestate;
 import util.typestate_ann.pre_and_post;
 import util.typestate_ann.get_pre;
 import util.typestate_ann.get_post;
+import util.typestate_ann.ann_precond;
+import util.typestate_ann.ann_prestate;
+import util.typestate_ann.set_precondition;
+import util.typestate_ann.set_postcondition;
+import util.typestate_ann.set_in_postcond;
 import util.typestate_ann.implies;
 import util.typestate_ann.pre_and_post_state;
 import util.typestate_ann.empty_states;
+import util.typestate_ann.empty_prestate;
+import util.typestate_ann.empty_ann;
+import util.typestate_ann.extend_prestate;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -97,6 +106,7 @@ import std.option;
 import std.option.t;
 import std.option.some;
 import std.option.none;
+import std.option.from_maybe;
 import std.map.hashmap;
 import std.list;
 import std.list.list;
@@ -106,6 +116,8 @@ import std.list.foldl;
 import std.list.find;
 import std._uint;
 import std.bitv;
+import std.util.fst;
+import std.util.snd;
 
 import util.typestate_ann;
 import util.typestate_ann.difference;
@@ -342,50 +354,41 @@ fn expr_ann(&expr e) -> ann {
   }
 }
 
-/* returns ann_none if this is the sort
- of statement where an ann doesn't make sense */
-fn stmt_ann(&stmt s) -> ann {
-  alt (s.node) {
-    case (stmt_decl(?d)) {
-      alt (d.node) {
-        case (decl_local(?l)) {
-          ret l.ann;
-        }
-        case (decl_item(?i)) {
-          ret ann_none; /* ????? */
-        }
+fn ann_to_ts_ann(ann a, uint nv) -> ts_ann {
+  alt (a) {
+    case (ann_none)         { ret empty_ann(nv); }
+    case (ann_type(_,_,?t)) {
+      alt (t) {
+        /* Kind of inconsistent. empty_ann()s everywhere
+         or an option of a ts_ann? */
+        case (none[@ts_ann])     { ret empty_ann(nv); }
+        case (some[@ts_ann](?t)) { ret *t; }
       }
     }
-    case (stmt_expr(?e)) {
-      ret expr_ann(*e);
-    }
-    case (_) {
-      ret ann_none;
-    }
   }
 }
 
-/* fails if e has no annotation */
-fn expr_pp(&expr e) -> pre_and_post {
-  alt (expr_ann(e)) {
-    case (ann_none) {
-      log "expr_pp: the impossible happened (no annotation)";
-      fail;
+fn stmt_ann(&stmt s) -> option.t[@ts_ann] {
+  alt (s.node) {
+    case (stmt_decl(_,?a)) {
+      ret a;
     }
-    case (ann_type(_, _, ?maybe_pp)) {
-      alt (maybe_pp) {
-        case (none[@ts_ann]) {
-          log "expr_pp: the impossible happened (no pre/post)";
-          fail;
-        }
-        case (some[@ts_ann](?p)) {
-          ret p.conditions;
-        }
-      }
+    case (stmt_expr(_,?a)) {
+      ret a;
+    }
+    case (stmt_crate_directive(_)) {
+      ret none[@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)) {
@@ -400,22 +403,24 @@ fn expr_states(&expr e) -> pre_and_post_state {
           fail;
         }
         case (some[@ts_ann](?p)) {
-          ret p.states;
+          // ret p.states;
         }
       }
     }
   }
 }
 
-/* fails if no annotation */
-fn stmt_pp(&stmt s) -> pre_and_post {
-  alt (stmt_ann(s)) {
+/* fails if e has no annotation */
+fn expr_pp(&expr e) -> pre_and_post {
+  alt (expr_ann(e)) {
     case (ann_none) {
+      log "expr_pp: the impossible happened (no annotation)";
       fail;
     }
     case (ann_type(_, _, ?maybe_pp)) {
       alt (maybe_pp) {
         case (none[@ts_ann]) {
+          log "expr_pp: the impossible happened (no pre/post)";
           fail;
         }
         case (some[@ts_ann](?p)) {
@@ -426,25 +431,18 @@ fn stmt_pp(&stmt s) -> pre_and_post {
   }
 }
 
-/* fails if no annotation */
-fn stmt_states(&stmt s) -> pre_and_post_state {
+fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
   alt (stmt_ann(s)) {
-    case (ann_none) {
-      fail;
+    case (none[@ts_ann]) {
+      ret empty_states(nv);
     }
-    case (ann_type(_, _, ?maybe_pp)) {
-      alt (maybe_pp) {
-        case (none[@ts_ann]) {
-          fail;
-        }
-        case (some[@ts_ann](?p)) {
-          ret p.states;
-        }
-      }
+    case (some[@ts_ann](?a)) {
+      ret a.states;
     }
   }
 }
 
+
 fn expr_precond(&expr e) -> precond {
   ret (expr_pp(e)).precondition;
 }
@@ -461,6 +459,7 @@ fn expr_poststate(&expr e) -> poststate {
   ret (expr_states(e)).poststate;
 }
 
+/*
 fn stmt_precond(&stmt s) -> precond {
   ret (stmt_pp(s)).precondition;
 }
@@ -468,13 +467,19 @@ fn stmt_precond(&stmt s) -> precond {
 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) -> prestate {
   ret (stmt_states(s)).prestate;
 }
-
-fn stmt_poststate(&stmt s) -> poststate {
-  ret (stmt_states(s)).poststate;
+*/
+fn stmt_poststate(&stmt s, uint nv) -> poststate {
+  ret (stmt_states(s, nv)).poststate;
 }
 
 /* returns a new annotation where the pre_and_post is p */
@@ -684,12 +689,19 @@ fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   }
 }
 
-fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
-                               &ast.stmt s) -> ast.stmt {
+impure fn gen(&fn_info enclosing, ts_ann a, def_id id) {
+  check(enclosing.contains_key(id));
+  let uint i = enclosing.get(id);
+
+  set_in_postcond(i, a.conditions);
+}
+
+fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
+  -> ast.stmt {
   auto num_local_vars = num_locals(enclosing);
 
   alt(s.node) {
-    case(ast.stmt_decl(?adecl)) {
+    case(ast.stmt_decl(?adecl, ?a)) {
       alt(adecl.node) {
         case(ast.decl_local(?alocal)) {
           alt(alocal.init) {
@@ -702,9 +714,25 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
                 @rec(ty=alocal.ty, infer=alocal.infer,
                      ident=alocal.ident, init=some[initializer](a_i),
                      id=alocal.id, ann=res_ann);
+
+              let ts_ann stmt_ann;
+              alt (a) {
+                case (none[@ts_ann]) {
+                  stmt_ann = empty_ann(num_local_vars);
+                }
+                case (some[@ts_ann](?aa)) {
+                  stmt_ann = *aa;
+                }
+              }
+              /* Inherit ann from initializer, and add var being
+                 initialized to the postcondition */
+              set_precondition(stmt_ann, expr_precond(*r));
+              set_postcondition(stmt_ann, expr_postcond(*r));
+              gen(enclosing, stmt_ann, alocal.id); 
               let stmt_ res = stmt_decl(@respan(adecl.span,
-                                                decl_local(res_local)));
-              ret (respan(s.span, res));
+                                                decl_local(res_local)),
+                                        some[@ts_ann](@stmt_ann));
+              ret (respan(s.span, res)); 
             }
             case(none[ast.initializer]) {
               // log("pre/post for init of " + alocal.ident + ": none");
@@ -716,22 +744,30 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
                      id=alocal.id, ann=res_ann);
               let stmt_ res =
                 stmt_decl
-                (@respan(adecl.span, decl_local(res_local)));
-              ret (respan (s.span, res));
+                (@respan(adecl.span, decl_local(res_local)),
+                 some[@ts_ann](@empty_ann(num_local_vars)));
+              ret respan(s.span, res); /* inherit ann from initializer */
             }
           }
         }
         case(decl_item(?anitem)) {
           auto res_item = find_pre_post_item(fm, enclosing, *anitem);
-          ret (respan(s.span, stmt_decl(@respan(adecl.span,
-                                               decl_item(@res_item))))); 
+          ret respan(s.span,
+                     stmt_decl(@respan(adecl.span,
+                                       decl_item(@res_item)),
+                               some[@ts_ann](@empty_ann(num_local_vars))));
         }
       }
     }
-    case(stmt_expr(?e)) {
+    case(stmt_expr(?e,_)) {
       log_expr(e);
       let @expr e_pp = find_pre_post_expr(enclosing, *e);
-      ret (respan(s.span, stmt_expr(e_pp)));
+      /* inherit ann from expr */
+      ret respan(s.span,
+                 stmt_expr(e_pp,
+                           some[@ts_ann]
+                           (@ann_to_ts_ann(expr_ann(*e_pp),
+                                           num_local_vars)))); 
     }    
   }
 }
@@ -739,7 +775,7 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
 fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
   -> block {
   fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> @stmt {
-    ret (@find_pre_post_for_each_stmt(fm, i, *s));
+    ret (@find_pre_post_stmt(fm, i, *s));
   }
   auto do_one = bind do_one_(fm, enclosing, _);
  
@@ -767,22 +803,93 @@ fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
   ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
 }
 
-/* Returns a pair of a new function, with possibly a changed pre- or
-   post-state, and a boolean flag saying whether the function's pre- or 
-   poststate changed */
-fn find_pre_post_state_fn(fn_info f_info, &ast._fn f) -> tup(bool, ast._fn) {
-  log ("Implement find_pre_post_state_fn!");
+/* FIXME */
+fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
+                            &prestate pres, expr e)
+  -> tup(bool, @expr) {
+  log("Implement find_pre_post_state_expr!");
   fail;
 }
 
-fn fixed_point_states(fn_info f_info,
-                      fn (fn_info, &ast._fn) -> tup(bool, ast._fn) f,
+/* FIXME: This isn't done yet. */
+fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
+                            &prestate pres, @stmt s) -> bool {
+  auto changed = false;
+  alt (s.node) {
+    case (stmt_decl(?adecl, ?a)) {
+      alt (adecl.node) {
+        case (ast.decl_local(?alocal)) {
+          alt (alocal.init) {
+            case (some[ast.initializer](?an_init)) {
+              auto p = find_pre_post_state_expr(fm, enclosing,
+                                                pres, *an_init.expr);
+              fail; /* FIXME */
+              /* Next: copy pres into a's prestate;
+                 find the poststate by taking p's poststate
+                 and setting the bit for alocal.id */
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+/* Returns a pair of a new block, with possibly a changed pre- or
+   post-state, and a boolean flag saying whether the function's pre- or 
+   poststate changed */
+fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, block b)
+  -> tup(bool, block) {
+  auto changed = false;
+  auto num_local_vars = num_locals(enclosing);
+
+  /* First, set the pre-states and post-states for every expression */
+  auto pres = empty_prestate(num_local_vars);
+  
+  /* 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 = changed || find_pre_post_state_stmt(fm, enclosing, pres, s);
+      /* Shouldn't need to rebuild the stmt.
+         This just updates bit-vectors
+         in a side-effecting way. */
+    extend_prestate(pres, stmt_poststate(*s, num_local_vars));
+  }
+
+  fn do_inner_(_fn_info_map fm, fn_info i, prestate p, &@expr e)
+    -> tup (bool, @expr) {
+    ret find_pre_post_state_expr(fm, i, p, *e);
+  }
+  auto do_inner = bind do_inner_(fm, enclosing, pres, _);
+  let option.t[tup(bool, @expr)] e_ =
+    option.map[@expr, tup(bool, @expr)](do_inner, b.node.expr);
+  auto s = snd[bool, @expr];
+  auto f = fst[bool, @expr];
+  changed = changed ||
+    from_maybe[bool](false,
+                     option.map[tup(bool, @expr), bool](f, e_));
+  let block_ b_res = rec(stmts=b.node.stmts,
+                         expr=option.map[tup(bool, @expr), @expr](s, e_),
+                         index=b.node.index);
+  ret tup(changed, respan(b.span, b_res));
+}
+
+fn find_pre_post_state_fn(_fn_info_map f_info, fn_info fi, &ast._fn f)
+  -> tup(bool, ast._fn) {
+  auto p = find_pre_post_state_block(f_info, fi, f.body);
+  ret tup(p._0, rec(decl=f.decl, proto=f.proto, body=p._1));
+}
+
+fn fixed_point_states(_fn_info_map fm, fn_info f_info,
+                      fn (_fn_info_map, fn_info, &ast._fn)
+                           -> tup(bool, ast._fn) f,
                       &ast._fn start) -> ast._fn {
-  auto next = f(f_info, start);
+  auto next = f(fm, f_info, start);
 
   if (next._0) {
     // something changed
-    be fixed_point_states(f_info, f, next._1);
+    be fixed_point_states(fm, f_info, f, next._1);
   }
   else {
     // we're done!
@@ -790,42 +897,29 @@ fn fixed_point_states(fn_info f_info,
   }
 }
 
-fn check_states_expr(fn_info enclosing, &expr e) -> () {
+impure fn check_states_expr(fn_info enclosing, &expr e) -> () {
   let precond prec    = expr_precond(e);
-  let postcond postc  = expr_postcond(e);
   let prestate pres   = expr_prestate(e);
-  let poststate posts = expr_poststate(e);
 
   if (!implies(pres, prec)) {
     log("check_states_expr: unsatisfied precondition");
     fail;
   }
-  if (!implies(posts, postc)) {
-    log("check_states_expr: unsatisfied postcondition");
-    fail;
-  }
 }
 
 fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
   alt (stmt_ann(s)) {
-    case (ann_none) {
-      // Statement doesn't require an annotation -- do nothing
+    case (none[@ts_ann]) {
       ret;
     }
-    case (ann_type(_,_,?m_pp)) {
-      let precond prec    = stmt_precond(s);
-      let postcond postc  = stmt_postcond(s);
-      let prestate pres   = stmt_prestate(s);
-      let poststate posts = stmt_poststate(s);
+    case (some[@ts_ann](?a)) {
+      let precond prec    = ann_precond(*a);
+      let prestate pres   = ann_prestate(*a);
 
       if (!implies(pres, prec)) {
         log("check_states_stmt: unsatisfied precondition");
         fail;
       }
-      if (!implies(posts, postc)) {
-        log("check_states_stmt: unsatisfied postcondition");
-        fail;
-      }
     }
   }
 }
@@ -855,7 +949,7 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
 
   /* Compute the pre- and post-states for this function */
   auto g = find_pre_post_state_fn;
-  auto res_f = fixed_point_states(f_info, g, f);
+  auto res_f = fixed_point_states(f_info_map, f_info, g, f);
 
   /* Now compare each expr's pre-state to its precondition
      and post-state to its postcondition */
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index 7e0fb6cb..ee11a43a 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -339,8 +339,8 @@ impure fn print_block(ps s, ast.block blk) {
         cur_line = st.span.hi.line;
         maybe_print_comment(s, st.span.lo);
         alt (st.node) {
-            case (ast.stmt_decl(?decl)) {print_decl(s, decl);}
-            case (ast.stmt_expr(?expr)) {print_expr(s, expr);}
+          case (ast.stmt_decl(?decl,_)) {print_decl(s, decl);}
+          case (ast.stmt_expr(?expr,_)) {print_expr(s, expr);}
         }
         if (front.parser.stmt_ends_with_semi(st)) {wrd(s.s, ";");}
         if (!maybe_print_line_comment(s, st.span)) {line(s.s);}
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index 47a37f33..e34d1fae 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -62,7 +62,11 @@ auth middle.typestate_check.log_expr = impure;
 auth lib.llvm = unsafe;
 auth pretty.pprust = impure;
 auth middle.typestate_check.find_pre_post_block = impure;
-auth middle.typestate_check.find_pre_post_expr = impure;
+auth middle.typestate_check.find_pre_post_state_block = impure;
+auth middle.typestate_check.find_pre_post_expr  = impure;
+auth middle.typestate_check.find_pre_post_stmt  = impure;
+auth middle.typestate_check.check_states_against_conditions = impure;
+auth middle.typestate_check.check_states_stmt   = impure;
 auth util.typestate_ann.implies = impure;
 
 mod lib {
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index 071f5513..53f9a71c 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -36,9 +36,17 @@ fn true_postcond(uint num_vars) -> postcond {
   be true_precond(num_vars);
 }
 
+fn empty_prestate(uint num_vars) -> prestate {
+  be true_precond(num_vars);
+}
+
+fn empty_poststate(uint num_vars) -> poststate {
+  be true_precond(num_vars);
+}
+
 fn empty_pre_post(uint num_vars) -> pre_and_post {
-  ret(rec(precondition=true_precond(num_vars),
-           postcondition=true_postcond(num_vars)));
+  ret(rec(precondition=empty_prestate(num_vars),
+          postcondition=empty_poststate(num_vars)));
 }
 
 fn empty_states(uint num_vars) -> pre_and_post_state {
@@ -46,6 +54,11 @@ fn empty_states(uint num_vars) -> pre_and_post_state {
            poststate=true_postcond(num_vars)));
 }
 
+fn empty_ann(uint num_vars) -> ts_ann {
+  ret(rec(conditions=empty_pre_post(num_vars),
+          states=empty_states(num_vars)));
+}
+
 fn get_pre(&pre_and_post p) -> precond {
   ret p.precondition;
 }
@@ -74,7 +87,37 @@ impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
   bitv.set(p.postcondition, i, true);
 }
 
-fn implies(bitv.t a, bitv.t b) -> bool {
+impure fn set_in_postcond(uint i, &pre_and_post p) -> () {
+  // sets the ith bit in p's post
+  bitv.set(p.postcondition, i, true);
+}
+
+// Sets all the bits in a's precondition to equal the
+// corresponding bit in p's precondition.
+impure fn set_precondition(&ts_ann a, &precond p) -> () {
+  bitv.copy(p, a.conditions.precondition);
+}
+
+// Sets all the bits in a's postcondition to equal the
+// corresponding bit in p's postcondition.
+impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
+  bitv.copy(p, a.conditions.postcondition);
+}
+
+// Set all the bits in p that are set in new
+impure fn extend_prestate(&prestate p, &poststate new) -> () {
+  bitv.union(p, new);
+}
+
+fn ann_precond(&ts_ann a) -> precond {
+  ret a.conditions.precondition;
+}
+
+fn ann_prestate(&ts_ann a) -> prestate {
+  ret a.states.prestate;
+}
+
+impure fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(b, a);
-  ret (bitv.equal(b, bitv.create(b.nbits, false)));
+  be bitv.is_false(b);
 }
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index f2b169ef..916a8205 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -1,5 +1,6 @@
 import option.none;
 import option.some;
+import util.orb;
 
 type vbuf = rustrt.vbuf;
 
@@ -230,6 +231,26 @@ fn foldl[T, U](fn (&U, &T) -> U p, &U z, &vec[T] v) -> U {
     }
 }
 
+fn unzip[T, U](&vec[tup(T, U)] v) -> tup(vec[T], vec[U]) {
+    auto sz = len[tup(T, U)](v);
+
+    if (sz == 0u) {
+        ret tup(alloc[T](0u), alloc[U](0u));
+    }
+    else {
+        auto rest = slice[tup(T, U)](v, 1u, sz);
+        auto tl   = unzip[T, U](rest);
+        auto a    = vec(v.(0)._0);
+        auto b    = vec(v.(0)._1);
+        ret tup(a + tl._0, b + tl._1);
+    }
+}
+
+fn or(&vec[bool] v) -> bool {
+    auto f = orb;
+    be _vec.foldl[bool, bool](f, false, v);
+}
+
 // Local Variables:
 // mode: rust;
 // fill-column: 78;
diff --git a/src/lib/bitv.rs b/src/lib/bitv.rs
index 2029ef52..98e6c040 100644
--- a/src/lib/bitv.rs
+++ b/src/lib/bitv.rs
@@ -135,6 +135,28 @@ impure fn set(&t v, uint i, bool x) {
     }
 }
 
+/* true if all bits are 1 */
+fn is_true(&t v) -> bool {
+    for(uint i in v.storage) {
+        if (i != 1u) {
+            ret false;
+        }
+    }
+
+    ret true;
+}
+
+/* true if all bits are non-1 */
+fn is_false(&t v) -> bool {
+    for(uint i in v.storage) {
+        if (i == 1u) {
+            ret false;
+        }
+    }
+
+    ret true;
+}
+
 fn init_to_vec(t v, uint i) -> uint {
     if (get(v, i)) {
         ret 1u;
diff --git a/src/lib/option.rs b/src/lib/option.rs
index 29a6f6eb..66a41bca 100644
--- a/src/lib/option.rs
+++ b/src/lib/option.rs
@@ -38,6 +38,13 @@ 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; }
+    }
+}
+
 // Local Variables:
 // mode: rust;
 // fill-column: 78;
diff --git a/src/lib/util.rs b/src/lib/util.rs
index 72844d5f..2f797f69 100644
--- a/src/lib/util.rs
+++ b/src/lib/util.rs
@@ -11,6 +11,18 @@ fn rational_leq(&rational x, &rational y) -> bool {
     ret x.num * y.den <= y.num * x.den;
 }
 
+fn fst[T, U](&tup(T, U) x) -> T {
+    ret x._0;
+}
+
+fn snd[T, U](&tup(T, U) x) -> U {
+    ret x._1;
+}
+
+fn orb(&bool a, &bool b) -> bool {
+    ret a || b;
+}
+
 // Local Variables:
 // mode: rust;
 // fill-column: 78;