From 755ca8eb73e0bd8cb9df892973a3bb5faf3fd651 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 20 May 2011 19:50:29 -0700 Subject: [PATCH] Correctly check that ! functions always diverge Also make _|_ unify with any type. --- src/comp/middle/tstate/ann.rs | 7 +++++++ src/comp/middle/tstate/bitvectors.rs | 8 ++++++++ src/comp/middle/tstate/ck.rs | 16 +++++++++++++++- src/comp/middle/tstate/states.rs | 8 ++++++++ src/comp/middle/ty.rs | 3 ++- 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); }