Initial implementation of typestate for closures.

There are still things not handled properly: relying on other preconditions
of upvars is likely to cause bad things to happen. We probably want to
disallow it.

3 files changed, 31 insertions, 13 deletions

diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 6a527d50eb6..e129fda3c90 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -486,6 +486,15 @@ fn constraints_expr(&ty::ctxt cx, @expr e) -> (@ty::constr)[] {
     }
 }
 
+fn node_id_to_def_upvar_strict(&fn_ctxt cx, node_id id) -> def {
+    alt (freevars::def_lookup(cx.ccx.tcx, cx.id, id)) {
+        case (none) {
+            log_err "node_id_to_def: node_id " + int::str(id) + " has no def";
+            fail;
+        }
+        case (some(?d)) { ret d; }
+    }
+}
 fn node_id_to_def_strict(&ty::ctxt cx, node_id id) -> def {
     alt (cx.def_map.find(id)) {
         case (none) {
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index eb3635a3b84..4082502d03a 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -299,6 +299,18 @@ fn handle_update(&fn_ctxt fcx, &@expr parent,
     }
 }
 
+fn handle_var(&fn_ctxt fcx, &pre_and_post rslt, node_id id, ident name) {
+    auto df = node_id_to_def_upvar_strict(fcx, id);
+    alt (df) {
+        case (def_local(?d_id)) {
+            auto i = bit_num(fcx, ninit(d_id.node, name));
+            use_var(fcx, d_id.node);
+            require_and_preserve(i, rslt);
+        }
+        case (_) {/* nothing to check */ }
+    }
+}
+
 /* Fills in annotations as a side effect. Does not rebuild the expr */
 fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
     auto enclosing = fcx.enclosing;
@@ -337,17 +349,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
         case (expr_path(?p)) {
             auto rslt = expr_pp(fcx.ccx, e);
             clear_pp(rslt);
-            auto df = node_id_to_def_strict(fcx.ccx.tcx, e.id);
-            alt (df) {
-                case (def_local(?d_id)) {
-                    auto i =
-                        bit_num(fcx,
-                          ninit(d_id.node, path_to_ident(fcx.ccx.tcx, p)));
-                    use_var(fcx, d_id.node);
-                    require_and_preserve(i, rslt);
-                }
-                case (_) {/* nothing to check */ }
-            }
+            handle_var(fcx, rslt, e.id, path_to_ident(fcx.ccx.tcx, p));
         }
         case (expr_self_method(?v)) { clear_pp(expr_pp(fcx.ccx, e)); }
         case (expr_log(_, ?arg)) {
@@ -367,7 +369,14 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
                 case (none) { clear_pp(expr_pp(fcx.ccx, e)); }
             }
         }
-        case (expr_fn(?f)) { clear_pp(expr_pp(fcx.ccx, e)); }
+        case (expr_fn(?f)) {
+            auto rslt = expr_pp(fcx.ccx, e);
+            clear_pp(rslt);
+            auto upvars = freevars::get_freevar_uses(fcx.ccx.tcx, e.id);
+            for (node_id id in *upvars) {
+                handle_var(fcx, rslt, id, "upvar");
+            }
+        }
         case (expr_block(?b)) {
             find_pre_post_block(fcx, b);
             auto p = block_pp(fcx.ccx, b);
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index cf8d60489c9..bc9864aa59c 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -208,7 +208,7 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
 fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool {
     alt (e.node) {
         case (expr_path(?pth)) {
-            alt (node_id_to_def(fcx.ccx, e.id)) {
+            alt (freevars::def_lookup(fcx.ccx.tcx, fcx.id, e.id)) {
                 case (some(def_local(?loc))) {
                     ret set_in_poststate_ident(fcx, loc.node,
                            path_to_ident(fcx.ccx.tcx, pth), p);