Correctly check that ! functions always diverge

Also make _|_ unify with any type.

5 files changed, 40 insertions, 2 deletions

diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs
index a62829f3a10..29f1dab6ede 100644
--- a/src/comp/middle/tstate/ann.rs
+++ b/src/comp/middle/tstate/ann.rs
@@ -109,6 +109,13 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
   ret !was_set;
 }
 
+fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
+  // sets the ith bit in p's post
+  auto was_set = bitv::get(s.poststate, i);
+  bitv::set(s.poststate, i, false);
+  ret was_set;
+}
+
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
 fn set_precondition(ts_ann a, &precond p) -> () {
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index aa379e072af..8de90452b6d 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -29,6 +29,7 @@ import tstate::ann::intersect;
 import tstate::ann::clone;
 import tstate::ann::set_in_postcond;
 import tstate::ann::set_in_poststate;
+import tstate::ann::clear_in_poststate;
              
 fn bit_num(def_id v, fn_info m) -> uint {
   assert (m.vars.contains_key(v));
@@ -137,3 +138,10 @@ fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
+fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+  log "kill_poststate";
+  assert (fcx.enclosing.vars.contains_key(id));
+  let uint i = (fcx.enclosing.vars.get(id))._0;
+  ret clear_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
+}
+
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 48134d4d3f2..a94982e7c9d 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -11,6 +11,8 @@ import front::ast::ident;
 import front::ast::def_id;
 import front::ast::ty_param;
 import front::ast::crate;
+import front::ast::return;
+import front::ast::noreturn;
 
 import front::ast::expr;
 import middle::ty::type_is_nil;
@@ -124,17 +126,29 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     auto do_inner = bind do_inner_(fcx, _, post);
     option::map[@expr, ()](do_inner, f.body.node.expr);
   
+    auto cf = fcx.enclosing.cf;
     /* Finally, check that the return value is initialized */
     if (f.proto == ast::proto_fn
         && ! promises(*post, fcx.id, enclosing)
         && ! type_is_nil(fcx.ccx.tcx,
-                         ret_ty_of_fn(fcx.ccx.tcx, a)) ) {
+                         ret_ty_of_fn(fcx.ccx.tcx, a))
+        && cf == return) {
         fcx.ccx.tcx.sess.span_note(f.body.span, "In function " + fcx.name +
           ", not all control paths return a value");
         fcx.ccx.tcx.sess.span_err(f.decl.output.span,
             "see declared return type of '" + ty_to_str(*f.decl.output) +
             "'");
     }
+    else if (cf == noreturn) {
+        // check that this really always fails
+        // the fcx.id bit means "returns" for a returning fn,
+        // "diverges" for a non-returning fn (I need to use the word
+        if (! promises(*post, fcx.id, enclosing)) {
+            fcx.ccx.tcx.sess.span_err(f.body.span,
+              "In non-returning function " + fcx.name +
+              ", some control paths may return to the caller");
+        }
+    }
 
 }
 
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index ef1e86275ce..6175a48972f 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -56,6 +56,7 @@ import bitvectors::intersect_postconds;
 import bitvectors::declare_var;
 import bitvectors::bit_num;
 import bitvectors::gen_poststate;
+import bitvectors::kill_poststate;
 
 import front::ast;
 import front::ast::_fn;
@@ -373,6 +374,13 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
     case (expr_ret(?maybe_ret_val, ?a)) {
         changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
         set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
+        /* return from an always-failing function clears the return bit */
+        alt (fcx.enclosing.cf) {
+            case (noreturn) {
+                kill_poststate(fcx, a, fcx.id);
+            }
+            case (_) {}
+        }
         alt(maybe_ret_val) {
             case (none[@expr]) { /* do nothing */ }
             case (some[@expr](?ret_val)) {
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index b92b7fb61db..10db57626f0 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -2288,7 +2288,8 @@ mod unify {
 
         alt (struct(cx.tcx, expected)) {
             case (ty::ty_nil)        { ret struct_cmp(cx, expected, actual); }
-            case (ty::ty_bot)        { ret struct_cmp(cx, expected, actual); }
+            // _|_ unifies with anything
+            case (ty::ty_bot)        { ret ures_ok(expected);                }
             case (ty::ty_bool)       { ret struct_cmp(cx, expected, actual); }
             case (ty::ty_int)        { ret struct_cmp(cx, expected, actual); }
             case (ty::ty_uint)       { ret struct_cmp(cx, expected, actual); }