Track arguments in typestate

Add the infrastructure for arguments -- as well as local vars --
to be deinitialized with move-mode calls. Address Issue #819

diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
index ad975f54216c2b96cf03a39ed56ac264b07b06fb..44d48c5037ce36ebdd232b9e819fe6de7a6ff1c4 100644 (file)
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -109,6 +109,14 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &[ty_param], f_sp: &span,
         next = add_constraint(cx.tcx, sc, next, res_map);
     }
 
+    /* Need to add constraints for args too, b/c they
+    can be deinitialized */
+    for a:arg in f.decl.inputs {
+        next = add_constraint(cx.tcx, respan(f_sp,
+                                             ninit(a.id, a.ident)),
+                              next, res_map);
+    }
+
     /* add the special i_diverge and i_return constraints
     (see the type definition for auxiliary::fn_info for an explanation) */
 
@@ -127,7 +135,8 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &[ty_param], f_sp: &span,
         {constrs: res_map,
          num_constraints:
          // add 2 to account for the i_return and i_diverge constraints
-             vec::len(*cx.cs) + vec::len(f.decl.constraints) + 2u,
+             vec::len(*cx.cs) + vec::len(f.decl.constraints)
+                 + vec::len(f.decl.inputs) + 2u,
          cf: f.decl.cf,
          i_return: ninit(id, name),
          i_diverge: ninit(diverges_id, diverges_name),

diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 5f6d0dcdf01c639a9b8159f1c95c7d16872244f7..af6614d8debaa96f1983a2809a703eccd63d3d95 100644 (file)
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -303,10 +303,11 @@ fn handle_update(fcx: &fn_ctxt, parent: &@expr, lhs: &@expr, rhs: &@expr,
     }
 }
 
+/* FIXME: Can't deinitialize an upvar -- tests for that? */
 fn handle_var(fcx: &fn_ctxt, rslt: &pre_and_post, id: node_id, name: ident) {
     let df = node_id_to_def_upvar_strict(fcx, id);
     alt df {
-      def_local(d_id) {
+      def_local(d_id) | def_arg(d_id) {
         let i = bit_num(fcx, ninit(d_id.node, name));
         use_var(fcx, d_id.node);
         require_and_preserve(i, rslt);
@@ -318,12 +319,12 @@ fn handle_var(fcx: &fn_ctxt, rslt: &pre_and_post, id: node_id, name: ident) {
 fn forget_args_moved_in(fcx: &fn_ctxt, parent: &@expr,
                         modes: &[ty::mode],
                         operands: &[@expr]) {
-    let i = 0;
+    let i = 0u;
     for mode: ty::mode in modes {
         if mode == ty::mo_move {
             forget_in_postcond(fcx, parent.id, operands.(i).id);
         }
-        i += 1;
+        i += 1u;
     }
 }
 
@@ -672,10 +673,12 @@ fn find_pre_post_block(fcx: &fn_ctxt, b: blk) {
     let nv = num_constraints(fcx.enclosing);
     fn do_one_(fcx: fn_ctxt, s: &@stmt) {
         find_pre_post_stmt(fcx, *s);
-        log "pre_post for stmt:";
-        log_stmt(*s);
-        log "is:";
-        log_pp(stmt_pp(fcx.ccx, *s));
+/*
+        log_err "pre_post for stmt:";
+        log_stmt_err(*s);
+        log_err "is:";
+        log_pp_err(stmt_pp(fcx.ccx, *s));
+*/
     }
     for s: @stmt in b.node.stmts { do_one_(fcx, s); }
     fn do_inner_(fcx: fn_ctxt, e: &@expr) { find_pre_post_expr(fcx, e); }

diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 787f3ba2e031041af70dd0912d48b484bdf3b51c..b39093d29d8f89f353508662793f9470efc04efc 100644 (file)
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -165,6 +165,7 @@ fn find_pre_post_state_call(fcx: &fn_ctxt, pres: &prestate, a: &@expr,
                             id: node_id, ops: &[init_op], bs: &[@expr],
                             cf: controlflow) -> bool {
     let changed = find_pre_post_state_expr(fcx, pres, a);
+    // FIXME: This could be a typestate constraint
     if vec::len(bs) != vec::len(ops) {
         fcx.ccx.tcx.sess.span_bug(a.span,
                                   #fmt("mismatched arg lengths: \
@@ -605,6 +606,7 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
 fn find_pre_post_state_stmt(fcx: &fn_ctxt, pres: &prestate, s: @stmt)
     -> bool {
     let stmt_ann = stmt_to_ann(fcx.ccx, *s);
+
 /*
     log_err ("[" + fcx.name + "]");
     log_err "*At beginning: stmt = ";
@@ -727,8 +729,13 @@ fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool {
     // This ensures that intersect works correctly.
     kill_all_prestate(fcx, f.body.node.id);
 
-    // Instantiate any constraints on the arguments so we can use them
+    // Arguments start out initialized
     let block_pre = block_prestate(fcx.ccx, f.body);
+    for a:arg in f.decl.inputs {
+        set_in_prestate_constr(fcx, ninit(a.id, a.ident), block_pre);
+    }
+
+    // Instantiate any constraints on the arguments so we can use them
     let tsc;
     for c: @constr in f.decl.constraints {
         tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c);

diff --git a/src/test/compile-fail/use-after-send.rs b/src/test/compile-fail/use-after-send.rs
new file mode 100644 (file)
index 0000000..212fa50
--- /dev/null
+++ b/src/test/compile-fail/use-after-send.rs
@@ -0,0 +1,18 @@
+// error-pattern: Unsatisfied precondition constraint
+fn send<~T>(ch : _chan<T>, data : -T) {
+    log ch;
+    log data;
+    fail;
+}
+type _chan<T> = int;
+
+// Tests that "log message;" is flagged as using
+// message after the send deinitializes it
+fn test00_start(ch: _chan<int>, message: int, count: int) {
+    send(ch, message);
+    log message;
+}
+
+fn main() {
+    fail;
+}
\ No newline at end of file