---

yaml
---
r: 4317
b: refs/heads/master
c: 5cf5f50
h: refs/heads/master
i:
  4315: 573056b
v: v3

Author: catamorphism

[refs]

@@ -1,2 +1,2 @@
 ---
-refs/heads/master: c9b16ac4c28ab5696d318dc7e414c73e27f9d631
+refs/heads/master: 5cf5f5024d5efcbb0b399433fa2117e1146292c2

trunk/src/comp/middle/tstate/auxiliary.rs

@@ -238,21 +238,58 @@ type norm_constraint = {bit_num: uint, c: sp_constr};
 
 type constr_map = @std::map::hashmap[def_id, constraint];
 
+/* Contains stuff that has to be computed up front */
 type fn_info =
-    /* list, accumulated during pre/postcondition
-     computation, of all local variables that may be
-     used*/
-    // Doesn't seem to work without the @ --
-    // bug?
     {constrs: constr_map,
      num_constraints: uint,
      cf: controlflow,
+/* For easy access, the fn_info stores two special constraints for each
+   function.  i_return holds if all control paths in this function terminate
+   in either a return expression, or an appropriate tail expression.
+   i_diverge holds if all control paths in this function terminate in a fail
+   or diverging call.
+
+   It might be tempting to use a single constraint C for both properties,
+   where C represents i_return and !C represents i_diverge. This is
+   inadvisable, because then the sense of the bit depends on context. If we're
+   inside a ! function, that reverses the sense of the bit: C would be
+   i_diverge and !C would be i_return.  That's awkward, because we have to
+   pass extra context around to functions that shouldn't care.
+
+   Okay, suppose C represents i_return and !C represents i_diverge, regardless
+   of context. Consider this code:
+
+     if (foo) { ret; } else { fail; }
+
+   C is true in the consequent and false in the alternative. What's T `join`
+   F, then?  ? doesn't work, because this code should definitely-return if the
+   context is a returning function (and be definitely-rejected if the context
+   is a ! function).  F doesn't work, because then the code gets incorrectly
+   rejected if the context is a returning function. T would work, but it
+   doesn't make sense for T `join` F to be T (consider init constraints, for
+   example).;
+
+   So we need context. And so it seems clearer to just have separate
+   constraints.
+*/
+     i_return: tsconstr,
+     i_diverge: tsconstr,
+    /* list, accumulated during pre/postcondition
+     computation, of all local variables that may be
+     used */
+// Doesn't seem to work without the @ -- bug
      used_vars: @mutable node_id[]};
 
 fn tsconstr_to_def_id(t: &tsconstr) -> def_id {
     alt t { ninit(id, _) { local_def(id) } npred(_, id, _) { id } }
 }
 
+fn tsconstr_to_node_id(t: &tsconstr) -> node_id {
+    alt t { ninit(id, _) { id }
+            npred(_, id, _) {
+              fail "tsconstr_to_node_id called on pred constraint" } }
+}
+
 /* mapping from node ID to typestate annotation */
 type node_ann_table = @mutable ts_ann[mutable ];
 
@@ -261,7 +298,10 @@ type node_ann_table = @mutable ts_ann[mutable ];
 type fn_info_map = @std::map::hashmap[node_id, fn_info];
 
 type fn_ctxt =
-    {enclosing: fn_info, id: node_id, name: ident, ccx: crate_ctxt};
+    {enclosing: fn_info,
+     id: node_id,
+     name: ident,
+     ccx: crate_ctxt};
 
 type crate_ctxt = {tcx: ty::ctxt, node_anns: node_ann_table, fm: fn_info_map};
 

trunk/src/comp/middle/tstate/ck.rs

@@ -40,7 +40,7 @@ import std::option::none;
 import aux::*;
 import syntax::print::pprust::ty_to_str;
 import util::common::log_stmt_err;
-import bitvectors::promises;
+import bitvectors::*;
 import annotate::annotate_crate;
 import collect_locals::mk_f_to_fn_info;
 import pre_post_conditions::fn_pre_post;
@@ -141,24 +141,23 @@ fn check_states_against_conditions(fcx: &fn_ctxt, f: &_fn,
 
     /* Check that the return value is initialized */
     let post = aux::block_poststate(fcx.ccx, f.body);
-    let ret_c: tsconstr = ninit(fcx.id, fcx.name);
-    if f.proto == ast::proto_fn && !promises(fcx, post, ret_c) &&
-           !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) &&
-           f.decl.cf == return {
-        fcx.ccx.tcx.sess.span_note(f.body.span,
+    if f.proto == ast::proto_fn &&
+        !promises(fcx, post, fcx.enclosing.i_return) &&
+        !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) &&
+        f.decl.cf == return {
+        fcx.ccx.tcx.sess.span_err(f.body.span,
                                    "In function " + fcx.name +
                                        ", not all control paths \
                                         return a value");
         fcx.ccx.tcx.sess.span_fatal(f.decl.output.span,
                                     "see declared return type of '" +
                                         ty_to_str(*f.decl.output) + "'");
     } else if (f.decl.cf == noreturn) {
-
-
         // check that this really always fails
-        // the fcx.id bit means "returns" for a returning fn,
-        // "diverges" for a non-returning fn
-        if !promises(fcx, post, ret_c) {
+        // Note that it's ok for i_diverge and i_return to both be true.
+        // In fact, i_diverge implies i_return. (But not vice versa!)
+
+        if !promises(fcx, post, fcx.enclosing.i_diverge) {
             fcx.ccx.tcx.sess.span_fatal(f.body.span,
                                         "In non-returning function " +
                                             fcx.name +

trunk/src/comp/middle/tstate/collect_locals.rs

@@ -109,16 +109,28 @@ fn mk_fn_info(ccx: &crate_ctxt, f: &_fn, tp: &ty_param[], f_sp: &span,
         next = add_constraint(cx.tcx, sc, next, res_map);
     }
 
-    /* add a pseudo-entry for the function's return value
-       we can safely use the function's name itself for this purpose */
+    /* add the special i_diverge and i_return constraints
+    (see the type definition for auxiliary::fn_info for an explanation) */
+
+    // use the name of the function for the "return" constraint
+    next = add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next,
+                          res_map);
+    // and the name of the function, with a '!' appended to it, for the
+    // "diverges" constraint
+    let diverges_id = ccx.tcx.sess.next_node_id();
+    let diverges_name = name + "!";
+    add_constraint(cx.tcx, respan(f_sp, ninit(diverges_id, diverges_name)),
+                   next, res_map);
 
-    add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map);
     let v: @mutable node_id[] = @mutable ~[];
     let rslt =
         {constrs: res_map,
          num_constraints:
-             ivec::len(*cx.cs) + ivec::len(f.decl.constraints) + 1u,
+         // add 2 to account for the i_return and i_diverge constraints
+             ivec::len(*cx.cs) + ivec::len(f.decl.constraints) + 2u,
          cf: f.decl.cf,
+         i_return: ninit(id, name),
+         i_diverge: ninit(diverges_id, diverges_name),
          used_vars: v};
     ccx.fm.insert(id, rslt);
     log name + " has " + std::uint::str(num_constraints(rslt)) +

trunk/src/comp/middle/tstate/pre_post_conditions.rs

@@ -79,6 +79,9 @@ fn find_pre_post_item(ccx: &crate_ctxt, i: &item) {
                  {constrs: @new_def_hash[constraint](),
                   num_constraints: 0u,
                   cf: return,
+                  // just bogus
+                  i_return: ninit(0, ""),
+                  i_diverge: ninit(0, ""),
                   used_vars: v},
              id: 0,
              name: "",
@@ -692,7 +695,8 @@ fn find_pre_post_block(fcx: &fn_ctxt, b: blk) {
 
 fn find_pre_post_fn(fcx: &fn_ctxt, f: &_fn) {
     // hack
-    use_var(fcx, fcx.id);
+    use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_return));
+    use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_diverge));
 
     find_pre_post_block(fcx, f.body);
 

trunk/src/comp/middle/tstate/states.rs

@@ -1,26 +1,13 @@
 import syntax::print::pprust::path_to_str;
+import util::ppaux::ty_to_str;
 import std::ivec;
 import std::option;
 import std::option::get;
 import std::option::is_none;
 import std::option::none;
 import std::option::some;
 import std::option::maybe;
-import tstate::ann::set_in_poststate_;
-import tstate::ann::pre_and_post;
-import tstate::ann::get_post;
-import tstate::ann::postcond;
-import tstate::ann::empty_pre_post;
-import tstate::ann::empty_poststate;
-import tstate::ann::clear_in_poststate;
-import tstate::ann::intersect;
-import tstate::ann::empty_prestate;
-import tstate::ann::prestate;
-import tstate::ann::poststate;
-import tstate::ann::false_postcond;
-import tstate::ann::ts_ann;
-import tstate::ann::set_prestate;
-import tstate::ann::set_poststate;
+import ann::*;
 import aux::*;
 import tritv::tritv_clone;
 import tritv::tritv_set;
@@ -189,9 +176,8 @@ fn find_pre_post_state_exprs(fcx: &fn_ctxt, pres: &prestate, id: node_id,
     /* if this is a failing call, it sets everything as initialized */
     alt cf {
       noreturn. {
-        changed |=
-            set_poststate_ann(fcx.ccx, id,
-                              false_postcond(num_constraints(fcx.enclosing)));
+        let post = false_postcond(num_constraints(fcx.enclosing));
+        changed |= set_poststate_ann(fcx.ccx, id, post);
       }
       _ { changed |= set_poststate_ann(fcx.ccx, id, rs.post); }
     }
@@ -403,15 +389,14 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
         /* normally, everything is true if execution continues after
            a ret expression (since execution never continues locally
            after a ret expression */
+// FIXME should factor this out
+        let post = false_postcond(num_constrs);
+        // except for the "diverges" bit...
+        kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
 
-        set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
-        /* return from an always-failing function clears the return bit */
+        set_poststate_ann(fcx.ccx, e.id, post);
 
-        alt fcx.enclosing.cf {
-          noreturn. { kill_poststate(fcx, e.id, ninit(fcx.id, fcx.name)); }
-          _ { }
-        }
-        alt maybe_ret_val {
+       alt maybe_ret_val {
           none. {/* do nothing */ }
           some(ret_val) {
             changed |= find_pre_post_state_expr(fcx, pres, ret_val);
@@ -421,7 +406,10 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
       }
       expr_be(val) {
         let changed = set_prestate_ann(fcx.ccx, e.id, pres);
-        set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
+        let post = false_postcond(num_constrs);
+        // except for the "diverges" bit...
+        kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
+        set_poststate_ann(fcx.ccx, e.id, post);
         ret changed | find_pre_post_state_expr(fcx, pres, val);
       }
       expr_if(antec, conseq, maybe_alt) {
@@ -558,12 +546,20 @@ fn find_pre_post_state_expr(fcx: &fn_ctxt, pres: &prestate, e: @expr) ->
         ret find_pre_post_state_sub(fcx, pres, operand, e.id, none);
       }
       expr_fail(maybe_fail_val) {
+        // FIXME Should factor out this code,
+        // which also appears in find_pre_post_state_exprs
+        /* if execution continues after fail, then everything is true!
+        woo! */
+        let post = false_postcond(num_constrs);
+        alt fcx.enclosing.cf {
+          noreturn. {
+            kill_poststate_(fcx, ninit(fcx.id, fcx.name), post);
+          }
+          _ {}
+        }
         ret set_prestate_ann(fcx.ccx, e.id, pres) |
-                /* if execution continues after fail, then everything is true!
-                   woo! */
-                set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs))
-                |
-                alt maybe_fail_val {
+            set_poststate_ann(fcx.ccx, e.id, post)
+                | alt maybe_fail_val {
                   none. { false }
                   some(fail_val) {
                     find_pre_post_state_expr(fcx, pres, fail_val)
@@ -710,9 +706,11 @@ fn find_pre_post_state_block(fcx: &fn_ctxt, pres0: &prestate, b: &blk) ->
 
 fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool {
 
-    let num_local_vars = num_constraints(fcx.enclosing);
-    // make sure the return bit starts out False
-    clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
+    let num_constrs = num_constraints(fcx.enclosing);
+    // make sure the return and diverge bits start out False
+    kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_return);
+    kill_prestate(fcx, f.body.node.id, fcx.enclosing.i_diverge);
+
     // Instantiate any constraints on the arguments so we can use them
     let block_pre = block_prestate(fcx.ccx, f.body);
     let tsc;
@@ -728,15 +726,16 @@ fn find_pre_post_state_fn(fcx: &fn_ctxt, f: &_fn) -> bool {
       some(tailexpr) {
         let tailty = expr_ty(fcx.ccx.tcx, tailexpr);
 
-
         // Since blocks and alts and ifs that don't have results
         // implicitly result in nil, we have to be careful to not
         // interpret nil-typed block results as the result of a
         // function with some other return type
         if !type_is_nil(fcx.ccx.tcx, tailty) &&
                !type_is_bot(fcx.ccx.tcx, tailty) {
-            let p = false_postcond(num_local_vars);
-            set_poststate_ann(fcx.ccx, f.body.node.id, p);
+            let post = false_postcond(num_constrs);
+            // except for the "diverges" bit...
+            kill_poststate_(fcx, fcx.enclosing.i_diverge, post);
+            set_poststate_ann(fcx.ccx, f.body.node.id, post);
         }
       }
       none. {/* fallthrough */ }

trunk/src/test/compile-fail/bang-tailexpr.rs

@@ -0,0 +1,4 @@
+// xfail-stage0
+// error-pattern: some control paths may return
+fn f() -> ! { 3 }
+fn main(){}