More work on typestate. Sketched out code for computing and checking prestates and poststates. Still a long ways away.

4 files changed, 508 insertions, 80 deletions

diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index e105c7a9106..ab0262f1753 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -23,6 +23,7 @@ import middle.ty.ty_to_str;
 import middle.ty.type_is_integral;
 import middle.ty.type_is_scalar;
 import middle.ty.ty_params_opt_and_ty;
+import middle.ty.ty_nil;
 
 import std._str;
 import std._uint;
@@ -62,6 +63,12 @@ fn triv_ann(@ty.t t) -> ann {
     ret ast.ann_type(t, none[vec[@ty.t]], none[@ts_ann]);
 }
 
+// Used to fill in the annotation for things that have uninteresting
+// types
+fn boring_ann() -> ann {
+    ret triv_ann(plain_ty(ty_nil));
+}
+
 // Replaces parameter types inside a type with type variables.
 fn generalize_ty(@crate_ctxt cx, @ty.t t) -> @ty.t {
     state obj ty_generalizer(@crate_ctxt cx,
@@ -1361,7 +1368,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
                                  ann_to_type(ann), adk);
             e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(t));
         }
-        /* FIXME: this should probably check the type annotations */
+        /* FIXME: should this check the type annotations? */
         case (ast.expr_fail(_))  { e_1 = e.node; } 
         case (ast.expr_log(_,_)) { e_1 = e.node; } 
         case (ast.expr_break(_)) { e_1 = e.node; }
@@ -1771,16 +1778,19 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                                      ann));
         }
 
-        case (ast.expr_fail(_)) { // ??? ignoring ann
-            ret expr;
+        case (ast.expr_fail(_)) {
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_fail(boring_ann()));
         }
 
         case (ast.expr_break(_)) {
-            ret expr;
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_break(boring_ann()));
         }
 
         case (ast.expr_cont(_)) {
-            ret expr;
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_cont(boring_ann()));
         }
 
         case (ast.expr_ret(?expr_opt, _)) {
@@ -1792,14 +1802,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                          + "returning non-nil");
                     }
 
-                    ret expr;
+                    ret @fold.respan[ast.expr_]
+                        (expr.span,
+                         ast.expr_ret(none[@ast.expr], boring_ann()));
                 }
 
                 case (some[@ast.expr](?e)) {
                     auto expr_0 = check_expr(fcx, e);
                     auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
                     ret @fold.respan[ast.expr_]
-                        (expr.span, ast.expr_ret(some(expr_1), ann_none));
+                        (expr.span, ast.expr_ret(some(expr_1), boring_ann()));
                 }
             }
         }
@@ -1813,14 +1825,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                          + "putting non-nil");
                     }
 
-                    ret expr;
+                    ret @fold.respan[ast.expr_]
+                        (expr.span, ast.expr_put(none[@ast.expr],
+                                                 boring_ann()));
                 }
 
                 case (some[@ast.expr](?e)) {
                     auto expr_0 = check_expr(fcx, e);
                     auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
                     ret @fold.respan[ast.expr_]
-                        (expr.span, ast.expr_put(some(expr_1), ann_none));
+                        (expr.span, ast.expr_put(some(expr_1), boring_ann()));
                 }
             }
         }
@@ -1831,20 +1845,21 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
             auto expr_0 = check_expr(fcx, e);
             auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
             ret @fold.respan[ast.expr_](expr.span,
-                                        ast.expr_be(expr_1, ann_none));
+                                        ast.expr_be(expr_1,
+                                                    boring_ann()));
         }
 
         case (ast.expr_log(?e,_)) {
             auto expr_t = check_expr(fcx, e);
             ret @fold.respan[ast.expr_]
-                (expr.span, ast.expr_log(expr_t, ann_none));
+                (expr.span, ast.expr_log(expr_t, boring_ann()));
         }
 
         case (ast.expr_check_expr(?e, _)) {
             auto expr_t = check_expr(fcx, e);
             demand(fcx, expr.span, plain_ty(ty.ty_bool), expr_ty(expr_t));
             ret @fold.respan[ast.expr_]
-                (expr.span, ast.expr_check_expr(expr_t, ann_none));
+                (expr.span, ast.expr_check_expr(expr_t, boring_ann()));
         }
 
         case (ast.expr_assign(?lhs, ?rhs, _)) {
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 361d70aecd1..295c4f1bfeb 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -20,6 +20,8 @@ import front.ast.expr;
 import front.ast.expr_call;
 import front.ast.expr_path;
 import front.ast.expr_log;
+import front.ast.expr_block;
+import front.ast.expr_lit;
 import front.ast.path;
 import front.ast.crate_directive;
 import front.ast.fn_decl;
@@ -42,6 +44,12 @@ 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.module;
+import front.ast.mod_index_entry;
+import front.ast.mie_item;
+import front.ast.item_fn;
+import front.ast.def_local;
 
 import middle.fold;
 import middle.fold.respan;
@@ -50,6 +58,7 @@ import util.common;
 import util.common.span;
 import util.common.spanned;
 import util.common.new_str_hash;
+import util.common.new_def_hash;
 import util.typestate_ann;
 import util.typestate_ann.ts_ann;
 import util.typestate_ann.empty_pre_post;
@@ -57,9 +66,14 @@ import util.typestate_ann.true_precond;
 import util.typestate_ann.true_postcond;
 import util.typestate_ann.postcond;
 import util.typestate_ann.precond;
+import util.typestate_ann.poststate;
+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.implies;
+import util.typestate_ann.pre_and_post_state;
+import util.typestate_ann.empty_states;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -91,6 +105,8 @@ import std.list.cons;
 import std.list.nil;
 import std.list.foldl;
 import std.list.find;
+import std._uint;
+import std.bitv;
 
 import util.typestate_ann;
 import util.typestate_ann.difference;
@@ -98,21 +114,134 @@ import util.typestate_ann.union;
 import util.typestate_ann.pps_len;
 import util.typestate_ann.require_and_preserve;
 
-/**********************************************************************/
-/* mapping from variable name to bit number */
-type fn_info = std.map.hashmap[ident, uint];
+/**** debugging junk  ****/
+fn log_expr(@expr e) -> () {
+  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);
+
+  print_expr(out, e);
+  log(s.get_str());
+}
+
+fn log_cond(vec[uint] v) -> () {
+  auto res = "";
+  for (uint i in v) {
+    if (i == 0u) {
+      res += "0";
+    }
+    else {
+      res += "1";
+    }
+  }
+  log(res);
+}
+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 bit_num(ident v, fn_info m) -> uint {
+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);
+  }
+}
+/**********************************************************************/
+/* mapping from variable name (def_id is assumed to be for a local
+   variable in a given function) to bit number */
+type fn_info      = std.map.hashmap[def_id, uint];
+/* mapping from function name to fn_info map */
+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);
 }
+
+fn var_is_local(def_id v, fn_info m) -> bool {
+  ret (m.contains_key(v));
+}
+
 fn num_locals(fn_info m) -> uint {
   ret m.size();
 }
 
+fn find_locals(_fn f) -> vec[def_id] {
+  auto res = _vec.alloc[def_id](0u);
+
+  for each (@tup(ident, block_index_entry) p
+          in f.body.node.index.items()) {
+    alt (p._1) {
+      case (ast.bie_local(?loc)) {
+        res += vec(loc.id);
+      }
+      case (_) { }
+    }
+  }
+
+  ret res;
+}
+
+fn add_var(def_id v, uint next, fn_info tbl) -> uint {
+  tbl.insert(v, next);
+  // log(v + " |-> " + _uint.to_str(next, 10u));
+  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) -> fn_info {
-  ret new_str_hash[uint](); /* FIXME: actually implement this */
+  auto res = new_def_hash[uint]();
+  let uint next = 0u;
+  let vec[ast.arg] f_args = f.decl.inputs;
+
+  for (ast.arg v in f_args) {
+    next = add_var(v.id, next, res);
+  }
+
+  let vec[def_id] locals = find_locals(f);
+  for (def_id v in locals) {
+    next = add_var(v, next, res);
+  }
+
+  ret res;
 }
-/**********************************************************************/
+
+/* extends mk_fn_info to an 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,
+                 vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
+  fi.insert(id, mk_fn_info(f));
+  ret @respan(sp, item_fn(i, f, ty_params, id, 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 {
+  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);
+
+  ret res;
+}
+/**** Helpers ****/
 fn expr_ann(&expr e) -> ann {
   alt(e.node) {
     case (ast.expr_vec(_,_,?a)) {
@@ -214,8 +343,53 @@ fn expr_ann(&expr e) -> ann {
   }
 }
 
-fn expr_pp(&@expr e) -> pre_and_post {
-  alt (expr_ann(*e)) {
+/* 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; /* ????? */
+        }
+      }
+    }
+    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;
+    }
+    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;
+        }
+      }
+    }
+  }
+}
+
+/* fails if e has no annotation */
+fn expr_states(&expr e) -> pre_and_post_state {
+  alt (expr_ann(e)) {
     case (ann_none) {
       log "expr_pp: the impossible happened (no annotation)";
       fail;
@@ -227,7 +401,45 @@ fn expr_pp(&@expr e) -> pre_and_post {
           fail;
         }
         case (some[@ts_ann](?p)) {
-          ret *p;
+          ret p.states;
+        }
+      }
+    }
+  }
+}
+
+/* fails if no annotation */
+fn stmt_pp(&stmt s) -> pre_and_post {
+  alt (stmt_ann(s)) {
+    case (ann_none) {
+      fail;
+    }
+    case (ann_type(_, _, ?maybe_pp)) {
+      alt (maybe_pp) {
+        case (none[@ts_ann]) {
+          fail;
+        }
+        case (some[@ts_ann](?p)) {
+          ret p.conditions;
+        }
+      }
+    }
+  }
+}
+
+/* fails if no annotation */
+fn stmt_states(&stmt s) -> pre_and_post_state {
+  alt (stmt_ann(s)) {
+    case (ann_none) {
+      fail;
+    }
+    case (ann_type(_, _, ?maybe_pp)) {
+      alt (maybe_pp) {
+        case (none[@ts_ann]) {
+          fail;
+        }
+        case (some[@ts_ann](?p)) {
+          ret p.states;
         }
       }
     }
@@ -235,21 +447,49 @@ fn expr_pp(&@expr e) -> pre_and_post {
 }
 
 fn expr_precond(&expr e) -> precond {
-  ret (expr_pp(@e)).precondition;
+  ret (expr_pp(e)).precondition;
 }
 
-fn expr_postcond(&@expr e) -> postcond {
+fn expr_postcond(&expr e) -> postcond {
   ret (expr_pp(e)).postcondition;
 }
 
-fn with_pp(ann a, @pre_and_post p) -> ann {
+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 stmt_prestate(&stmt s) -> prestate {
+  ret (stmt_states(s)).prestate;
+}
+
+fn stmt_poststate(&stmt s) -> poststate {
+  ret (stmt_states(s)).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(?t, ?ps, _)) {
-      ret (ann_type(t, ps, some[@ts_ann](p)));
+      ret (ann_type(t, ps,
+                    some[@ts_ann]
+                    (@rec(conditions=p,
+                          states=empty_states(pps_len(p))))));
     }
   }
 }
@@ -276,9 +516,14 @@ fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
 }
 
 fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond {
-  auto other = rest.(0);
-  union(first, other);
-  union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest)));
+  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;
 }
 
@@ -288,19 +533,7 @@ fn union_postconds(&vec[postcond] pcs) -> postcond {
   be union_postconds_go(pcs.(0), pcs);
 }
 
-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);
-  }
-}
+/******* AST-traversing code ********/
 
 fn find_pre_post_mod(&_mod m) -> _mod {
   ret m; /* FIXME */
@@ -314,26 +547,29 @@ fn find_pre_post_obj(_obj o) -> _obj {
   ret o; /* FIXME */
 }
 
-impure fn find_pre_post_item(fn_info enclosing, &item i) -> item {
+fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> item {
   alt (i.node) {
     case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
       auto e_pp = find_pre_post_expr(enclosing, *e);
+      log("1");
       ret (respan(i.span,
-                   ast.item_const(id, t, e_pp, di,
-                              with_pp(a, @expr_pp(e_pp)))));
+                  ast.item_const(id, t, e_pp, di, a)));
     }
     case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
-      auto f_pp = find_pre_post_fn(f);
+      check (fm.contains_key(di));
+      auto f_pp = find_pre_post_fn(fm, fm.get(di), f);
       ret (respan(i.span, 
                    ast.item_fn(id, f_pp, ps, di, a)));
     }
     case (ast.item_mod(?id, ?m, ?di)) {
       auto m_pp = find_pre_post_mod(m);
+      log("3");
       ret (respan(i.span,
                    ast.item_mod(id, m_pp, di)));
     }
     case (ast.item_native_mod(?id, ?nm, ?di)) {
       auto n_pp = find_pre_post_native_mod(nm);
+      log("4");
       ret (respan(i.span,
                    ast.item_native_mod(id, n_pp, di)));
     }
@@ -345,17 +581,23 @@ impure fn find_pre_post_item(fn_info enclosing, &item i) -> item {
     }
     case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
       auto o_pp = find_pre_post_obj(o);
+      log("5");
       ret (respan(i.span,
                    ast.item_obj(id, o_pp, ps, di, a)));
     }
   }
 }
 
-impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
+fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   auto num_local_vars = num_locals(enclosing);
 
   fn do_rand_(fn_info enclosing, &@expr e) -> @expr {
-    be find_pre_post_expr(enclosing, *e);
+    log("for rand " );
+    log_expr(e);
+    log("pp = ");
+    auto res = find_pre_post_expr(enclosing, *e);
+    log_pp(expr_pp(*res));
+    ret res;
   }
 
   auto do_rand = bind do_rand_(enclosing,_);
@@ -363,40 +605,78 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   alt(e.node) {
     case(expr_call(?oper, ?rands, ?a)) {
       auto pp_oper = find_pre_post_expr(enclosing, *oper);
+      log("pp_oper =");
+      log_pp(expr_pp(*pp_oper));
       
       auto f = do_rand;
       auto pp_rands = _vec.map[@expr, @expr](f, rands);
       
-      auto g = expr_pp;
-      auto pps = _vec.map[@expr, pre_and_post]      
-        (g, pp_rands);
-      _vec.push[pre_and_post](pps, expr_pp(pp_oper));
+      fn pp_one(&@expr e) -> pre_and_post {
+        be expr_pp(*e);
+      }
+      auto g = pp_one;
+      auto pps = _vec.map[@expr, pre_and_post](g, pp_rands);
+      _vec.push[pre_and_post](pps, expr_pp(*pp_oper));
       auto h = get_post;
       auto res_postconds = _vec.map[pre_and_post, postcond](h, pps);
       auto res_postcond = union_postconds(res_postconds);
-      let @pre_and_post pp =
-        @rec(precondition=seq_preconds(num_local_vars, pps),
+      let pre_and_post pp =
+        rec(precondition=seq_preconds(num_local_vars, pps),
              postcondition=res_postcond);
       let ann a_res = with_pp(a, pp);
+      log("result for call");
+      log_expr(@e);
+      log("is:");
+      log_pp(pp);
       ret (@respan(e.span,
                    expr_call(pp_oper, pp_rands, a_res)));
                         
     }
     case(expr_path(?p, ?maybe_def, ?a)) {
-      check (len[ident](p.node.idents) > 0u);
-      auto referent = p.node.idents.(0);
-      auto i = bit_num(referent, enclosing);
+      auto df;
+      alt (maybe_def) {
+        case (none[def])
+          { log("expr_path should have a def"); fail; }
+        case (some[def](?d)) { df = d; }
+      }
+
       auto res = empty_pre_post(num_local_vars);
-      require_and_preserve(i, *res);
+
+      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
+      log("pre/post for:\n");
+      log_expr(@e);
+      log("is");
+      log_pp(res);
       ret (@respan
            (e.span,
             expr_path(p, maybe_def,
                       with_pp(a, res))));
     }
-    case(expr_log(?e, ?a)) {
-      auto e_pp = find_pre_post_expr(enclosing, *e);
+    case(expr_log(?arg, ?a)) {
+      log("log");
+      auto e_pp = find_pre_post_expr(enclosing, *arg);
+      log("pre/post for: ");
+      log_expr(arg);
+      log("is");
+      log_pp(expr_pp(*e_pp));
       ret (@respan(e.span,
-                   expr_log(e_pp, with_pp(a, @expr_pp(e_pp)))));
+                   expr_log(e_pp, with_pp(a, expr_pp(*e_pp)))));
+    }
+    case (expr_block(?b, ?a)) {
+      log("block!");
+      fail;
+    }
+    case (expr_lit(?l, ?a)) {
+      ret @respan(e.span,
+                  expr_lit(l, with_pp(a, empty_pre_post(num_local_vars))));
     }
     case(_) {
       log("this sort of expr isn't implemented!");
@@ -405,8 +685,8 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   }
 }
 
-impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
-  -> ast.stmt {
+fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
+                               &ast.stmt s) -> ast.stmt {
   auto num_local_vars = num_locals(enclosing);
 
   alt(s.node) {
@@ -418,7 +698,7 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
               let @expr r = find_pre_post_expr(enclosing, *an_init.expr);
               let init_op o = an_init.op;
               let initializer a_i = rec(op=o, expr=r);
-              let ann res_ann = with_pp(alocal.ann, @expr_pp(r));
+              let ann res_ann = with_pp(alocal.ann, expr_pp(*r));
               let @local res_local =
                 @rec(ty=alocal.ty, infer=alocal.infer,
                      ident=alocal.ident, init=some[initializer](a_i),
@@ -443,24 +723,26 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
           }
         }
         case(decl_item(?anitem)) {
-          auto res_item = find_pre_post_item(enclosing, *anitem);
+          auto res_item = find_pre_post_item(fm, enclosing, *anitem);
           ret (respan(s.span, stmt_decl(@respan(adecl.span,
                                                decl_item(@res_item))))); 
         }
       }
     }
     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)));
     }    
   }
 }
 
-fn find_pre_post_block(fn_info enclosing, block b) -> block {
-  fn do_one_(fn_info i, &@stmt s) -> @stmt {
-    ret (@find_pre_post_for_each_stmt(i, *s));
+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));
   }
-  auto do_one = bind do_one_(enclosing, _);
+  auto do_one = bind do_one_(fm, enclosing, _);
  
   auto ss = _vec.map[@stmt, @stmt](do_one, b.node.stmts);
   fn do_inner_(fn_info i, &@expr e) -> @expr {
@@ -472,24 +754,134 @@ fn find_pre_post_block(fn_info enclosing, block b) -> block {
   ret respan(b.span, b_res);
 }
 
-fn find_pre_post_fn(&_fn f) -> _fn {
-  let fn_info fi = mk_fn_info(f);
+fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> _fn {
   ret rec(decl=f.decl, proto=f.proto,
-          body=find_pre_post_block(fi, f.body));
+          body=find_pre_post_block(fm, fi, f.body));
 }
 
-fn check_item_fn(&@() ignore, &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 {
 
-  auto res_f = find_pre_post_fn(f);  
+  check (fm.contains_key(id));
+  auto res_f = find_pre_post_fn(fm, fm.get(id), 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!");
+  fail;
+}
+
+fn fixed_point_states(fn_info f_info,
+                      fn (fn_info, &ast._fn) -> tup(bool, ast._fn) f,
+                      &ast._fn start) -> ast._fn {
+  auto next = f(f_info, start);
+
+  if (next._0) {
+    // something changed
+    be fixed_point_states(f_info, f, next._1);
+  }
+  else {
+    // we're done!
+    ret next._1;
+  }
+}
+
+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
+      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);
+
+      if (!implies(pres, prec)) {
+        log("check_states_stmt: unsatisfied precondition");
+        fail;
+      }
+      if (!implies(posts, postc)) {
+        log("check_states_stmt: unsatisfied postcondition");
+        fail;
+      }
+    }
+  }
+}
+
+fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
+  fn do_one_(fn_info i, &@stmt s) -> () {
+    check_states_stmt(i, *s);
+  }
+  auto do_one = bind do_one_(enclosing, _);
+ 
+  _vec.map[@stmt, ()](do_one, f.body.node.stmts);
+  fn do_inner_(fn_info i, &@expr e) -> () {
+    check_states_expr(i, *e);
+  }
+  auto do_inner = bind do_inner_(enclosing, _);
+  option.map[@expr, ()](do_inner, f.body.node.expr);
+  
+}
+
+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);
+
+  /* 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);
+
+  /* Now compare each expr's pre-state to its precondition
+     and post-state to its postcondition */
+  check_states_against_conditions(f_info, res_f);
+
+  /* Rebuild the same function */
+  ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
+}
+
 fn check_crate(@ast.crate crate) -> @ast.crate {
-  auto fld = fold.new_identity_fold[@()]();
 
+  /* Build the global map from function id to var-to-bit-num-map */
+  auto fn_info_map = mk_f_to_fn_info(crate);
+
+  /* Compute the pre and postcondition for every subexpression */
+  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, crate);
+
+  auto fld1 = fold.new_identity_fold[_fn_info_map]();
+
+  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_)
+              with *fld1);
 
-  ret fold.fold_crate[@()](@(), fld, crate);
+  ret fold.fold_crate[_fn_info_map](fn_info_map, fld1,
+                                    with_pre_postconditions);
 }
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index 952ea7e8c9e..47a37f3325f 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -62,6 +62,8 @@ 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 util.typestate_ann.implies = impure;
 
 mod lib {
     alt (target_os) {
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index a4698c5d40f..071f55135f5 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -12,12 +12,21 @@ type precond  = bitv.t; /* 1 means "this variable must be initialized"
 type postcond = bitv.t; /* 1 means "this variable is initialized"
                            0 means "don't know about this variable */
 
+type prestate = bitv.t; /* 1 means "this variable is definitely initialized"
+                           0 means "don't know whether this variable is
+                           initialized" */
+type poststate = bitv.t; /* 1 means "this variable is definitely initialized"
+                            0 means "don't know whether this variable is
+                            initialized" */
+
 /* named thus so as not to confuse with prestate and poststate */
 type pre_and_post = rec(precond precondition, postcond postcondition);
 /* FIXME: once it's implemented: */
 //  : ((*.precondition).nbits == (*.postcondition).nbits);
 
-type ts_ann = pre_and_post;
+type pre_and_post_state = rec(prestate prestate, poststate poststate);
+
+type ts_ann = rec(pre_and_post conditions, pre_and_post_state states);
 
 fn true_precond(uint num_vars) -> precond {
   be bitv.create(num_vars, false);
@@ -27,11 +36,16 @@ fn true_postcond(uint num_vars) -> postcond {
   be true_precond(num_vars);
 }
 
-fn empty_pre_post(uint num_vars) -> @pre_and_post {
-  ret(@rec(precondition=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)));
 }
 
+fn empty_states(uint num_vars) -> pre_and_post_state {
+  ret(rec(prestate=true_precond(num_vars),
+           poststate=true_postcond(num_vars)));
+}
+
 fn get_pre(&pre_and_post p) -> precond {
   ret p.precondition;
 }
@@ -57,5 +71,10 @@ fn pps_len(&pre_and_post p) -> uint {
 impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
   // sets the ith bit in p's pre and post
   bitv.set(p.precondition, i, true);
-  bitv.set(p.postcondition, i, false);
-}
\ No newline at end of file
+  bitv.set(p.postcondition, i, true);
+}
+
+fn implies(bitv.t a, bitv.t b) -> bool {
+  bitv.difference(b, a);
+  ret (bitv.equal(b, bitv.create(b.nbits, false)));
+}