1
Fork 0

Correctly check that ! functions always diverge

Also make _|_ unify with any type.
This commit is contained in:
Tim Chevalier 2011-05-20 19:50:29 -07:00
parent 699986d192
commit 755ca8eb73
5 changed files with 40 additions and 2 deletions

View file

@ -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) -> () {

View file

@ -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);
}

View file

@ -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");
}
}
}

View file

@ -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)) {

View file

@ -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); }