diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs index 108d050757f5..a1b5508e2a2d 100644 --- a/src/comp/middle/tstate/ann.rs +++ b/src/comp/middle/tstate/ann.rs @@ -168,7 +168,6 @@ fn extend_poststate(&poststate p, &poststate new) -> bool { ret bitv::union(p, new); } - // Clears the given bit in p fn relax_prestate(uint i, &prestate p) -> bool { auto was_set = bitv::get(p, i); @@ -176,6 +175,15 @@ fn relax_prestate(uint i, &prestate p) -> bool { ret was_set; } +// Clears the given bit in p +fn relax_poststate(uint i, &poststate p) -> bool { + ret relax_prestate(i, p); +} + +// Clears the given bit in p +fn relax_precond(uint i, &precond p) { + relax_prestate(i, p); +} // Clears all the bits in p fn clear(&precond p) { bitv::clear(p); } diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index 91359eb82311..e7013752ded4 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -358,10 +358,18 @@ fn stmt_poststate(&crate_ctxt ccx, &stmt s) -> poststate { ret stmt_states(ccx, s).poststate; } +fn block_precond(&crate_ctxt ccx, &block b) -> precond { + ret block_pp(ccx, b).precondition; +} + fn block_postcond(&crate_ctxt ccx, &block b) -> postcond { ret block_pp(ccx, b).postcondition; } +fn block_prestate(&crate_ctxt ccx, &block b) -> prestate { + ret block_states(ccx, b).prestate; +} + fn block_poststate(&crate_ctxt ccx, &block b) -> poststate { ret block_states(ccx, b).poststate; } @@ -402,11 +410,15 @@ fn set_pre_and_post(&crate_ctxt ccx, &ann a, &precond pre, &postcond post) { fn copy_pre_post(&crate_ctxt ccx, &ann a, &@expr sub) { log "set_pre_and_post"; auto p = expr_pp(ccx, sub); - auto t = ann_to_ts_ann(ccx, a); - set_precondition(t, p.precondition); - set_postcondition(t, p.postcondition); + copy_pre_post_(ccx, a, p.precondition, p.postcondition); } +fn copy_pre_post_(&crate_ctxt ccx, &ann a, &prestate pre, &poststate post) { + log "set_pre_and_post"; + auto t = ann_to_ts_ann(ccx, a); + set_precondition(t, pre); + set_postcondition(t, post); +} /* sets all bits to *1* */ fn set_postcond_false(&crate_ctxt ccx, &ann a) { @@ -548,7 +560,9 @@ fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use { } case (expr_lit(?l, _)) { ret @respan(e.span, carg_lit(l)); } case (_) { - tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg"); + tcx.sess.span_err(e.span, + "Arguments to constrained functions must be " + + "literals or local variables"); } } } @@ -626,6 +640,11 @@ fn path_to_ident(&ty::ctxt cx, &path p) -> ident { case (some(?i)) { ret i; } } } + +tag if_ty { + if_check; + plain_if; +} // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index 99b4c80820ea..850add38d5e1 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -15,6 +15,12 @@ import aux::npred; import aux::pred_desc; import aux::match_args; import aux::constr_; +import aux::block_precond; +import aux::stmt_precond; +import aux::expr_precond; +import aux::block_prestate; +import aux::expr_prestate; +import aux::stmt_prestate; import tstate::aux::ann_to_ts_ann; import tstate::ann::pre_and_post; import tstate::ann::precond; @@ -22,6 +28,8 @@ import tstate::ann::postcond; import tstate::ann::prestate; import tstate::ann::poststate; import tstate::ann::relax_prestate; +import tstate::ann::relax_precond; +import tstate::ann::relax_poststate; import tstate::ann::pps_len; import tstate::ann::true_precond; import tstate::ann::empty_prestate; @@ -136,9 +144,46 @@ fn gen(&fn_ctxt fcx, &ann a, &constr_ c) -> bool { fn declare_var(&fn_ctxt fcx, &constr_ c, prestate pre) -> prestate { auto res = clone(pre); relax_prestate(bit_num(fcx, c), res); + // idea is this is scoped + relax_poststate(bit_num(fcx, c), res); ret res; } +fn relax_precond_block_non_recursive(&fn_ctxt fcx, uint i, &block b) { + relax_precond(i, block_precond(fcx.ccx, b)); +} + +fn relax_precond_expr(&fn_ctxt fcx, uint i, &@expr e) { + relax_precond(i, expr_precond(fcx.ccx, e)); +} + +fn relax_precond_stmt(&fn_ctxt fcx, uint i, &@stmt s) { + relax_precond(i, stmt_precond(fcx.ccx, *s)); +} + +fn relax_precond_block(&fn_ctxt fcx, uint i, &block b) { + relax_precond_block_non_recursive(fcx, i, b); + // FIXME: should use visit instead + // could at least generalize this pattern + // (also seen in ck::check_states_against_conditions) + let @mutable bool keepgoing = @mutable true; + + fn quit(@mutable bool keepgoing, &@item i) { + *keepgoing = false; + } + fn kg(@mutable bool keepgoing) -> bool { ret *keepgoing; } + + auto v = rec(visit_block_pre = bind + relax_precond_block_non_recursive(fcx, i, _), + visit_expr_pre = bind relax_precond_expr(fcx, i, _), + visit_stmt_pre = bind relax_precond_stmt(fcx, i, _), + visit_item_pre=bind quit(keepgoing, _), + keep_going=bind kg(keepgoing) + + with walk::default_visitor()); + walk::walk_block(v, b); +} + fn gen_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool { log "gen_poststate"; ret set_in_poststate(bit_num(fcx, c), 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 4a4c7c47490d..ce170fb1db9e 100644 --- a/src/comp/middle/tstate/ck.rs +++ b/src/comp/middle/tstate/ck.rs @@ -61,9 +61,19 @@ import collect_locals::mk_f_to_fn_info; import pre_post_conditions::fn_pre_post; import states::find_pre_post_state_fn; -fn check_states_expr(&fn_ctxt fcx, @expr e) { +fn check_states_expr(&fn_ctxt fcx, &@expr e) { let precond prec = expr_precond(fcx.ccx, e); let prestate pres = expr_prestate(fcx.ccx, e); + + /* + log_err("check_states_expr:"); + util::common::log_expr_err(*e); + log_err("prec = "); + log_bitv_err(fcx, prec); + log_err("pres = "); + log_bitv_err(fcx, pres); + */ + if (!implies(pres, prec)) { auto s = ""; auto diff = first_difference_string(fcx, prec, pres); @@ -79,26 +89,27 @@ fn check_states_expr(&fn_ctxt fcx, @expr e) { } } -fn check_states_stmt(&fn_ctxt fcx, &stmt s) { - auto a = stmt_to_ann(fcx.ccx, s); +fn check_states_stmt(&fn_ctxt fcx, &@stmt s) { + auto a = stmt_to_ann(fcx.ccx, *s); let precond prec = ann_precond(a); let prestate pres = ann_prestate(a); - /* + /* log_err("check_states_stmt:"); - log_stmt_err(s); + log_stmt_err(*s); log_err("prec = "); - log_bitv_err(fcx.enclosing, prec); + log_bitv_err(fcx, prec); log_err("pres = "); - log_bitv_err(fcx.enclosing, pres); + log_bitv_err(fcx, pres); */ + if (!implies(pres, prec)) { auto ss = ""; auto diff = first_difference_string(fcx, prec, pres); ss += "Unsatisfied precondition constraint (for example, " + diff + ") for statement:\n"; - ss += pretty::pprust::stmt_to_str(s); + ss += pretty::pprust::stmt_to_str(*s); ss += "\nPrecondition:\n"; ss += bitv_to_str(fcx, prec); ss += "\nPrestate: \n"; @@ -107,29 +118,37 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) { } } -fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) { - auto enclosing = fcx.enclosing; - auto nv = num_constraints(enclosing); - auto post = @mutable empty_poststate(nv); - fn do_one_(fn_ctxt fcx, &@stmt s, @mutable poststate post) { - check_states_stmt(fcx, *s); - *post = stmt_poststate(fcx.ccx, *s); - } - auto do_one = bind do_one_(fcx, _, post); - vec::map[@stmt, ()](do_one, f.body.node.stmts); - fn do_inner_(fn_ctxt fcx, &@expr e, @mutable poststate post) { - check_states_expr(fcx, e); - *post = expr_poststate(fcx.ccx, e); - } - 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 */ +fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a, + &span sp, &ident i, &def_id d) { + /* Postorder traversal instead of pre is important + because we want the smallest possible erroneous statement + or expression. */ + let @mutable bool keepgoing = @mutable true; + + /* TODO probably should use visit instead */ + + fn quit(@mutable bool keepgoing, &@ast::item i) { + *keepgoing = false; + } + fn kg(@mutable bool keepgoing) -> bool { + ret *keepgoing; + } + + auto v = rec (visit_stmt_post=bind check_states_stmt(fcx, _), + visit_expr_post=bind check_states_expr(fcx, _), + visit_item_pre=bind quit(keepgoing, _), + keep_going=bind kg(keepgoing) + with walk::default_visitor()); + + walk::walk_fn(v, f, sp, i, d, a); + + /* Finally, check that the return value is initialized */ + auto post = aux::block_poststate(fcx.ccx, f.body); let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name)); - if (f.proto == ast::proto_fn && !promises(fcx, { *post }, ret_c) && + if (f.proto == ast::proto_fn && !promises(fcx, post, ret_c) && !type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, a)) && - cf == return) { + f.decl.cf == return) { fcx.ccx.tcx.sess.span_note(f.body.span, "In function " + fcx.name + ", not all control paths \ @@ -137,12 +156,12 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) { 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) { + } 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)) { + if (!promises(fcx, post, ret_c)) { fcx.ccx.tcx.sess.span_err(f.body.span, "In non-returning function " + fcx.name + @@ -152,7 +171,8 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) { } } -fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) { +fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a, &span sp, &ident i, + &def_id d) { /* Compute the pre- and post-states for this function */ auto g = find_pre_post_state_fn; @@ -160,7 +180,7 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) { /* Now compare each expr's pre-state to its precondition and post-state to its postcondition */ - check_states_against_conditions(fcx, f, a); + check_states_against_conditions(fcx, f, a, sp, i, d); } fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id, @@ -170,7 +190,7 @@ fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id, assert (ccx.fm.contains_key(id)); auto f_info = ccx.fm.get(id); auto fcx = rec(enclosing=f_info, id=id, name=i, ccx=ccx); - check_fn_states(fcx, f, a); + check_fn_states(fcx, f, a, sp, i, id); } fn check_crate(ty::ctxt cx, @crate crate) { @@ -185,7 +205,7 @@ fn check_crate(ty::ctxt cx, @crate crate) { auto do_pre_post = walk::default_visitor(); do_pre_post = - rec(visit_fn_pre=bind fn_pre_post(ccx, _, _, _, _, _) + rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _, _) with do_pre_post); walk::walk_crate(do_pre_post, *crate); /* Check the pre- and postcondition against the pre- and poststate @@ -193,7 +213,7 @@ fn check_crate(ty::ctxt cx, @crate crate) { auto do_states = walk::default_visitor(); do_states = - rec(visit_fn_pre=bind fn_states(ccx, _, _, _, _, _) with do_states); + rec(visit_fn_post=bind fn_states(ccx, _, _, _, _, _) with do_states); walk::walk_crate(do_states, *crate); } // diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 3eaf3cfba66a..42b12323437f 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -32,6 +32,7 @@ import aux::clear_pp; import aux::clear_precond; import aux::set_pre_and_post; import aux::copy_pre_post; +import aux::copy_pre_post_; import aux::expr_precond; import aux::expr_postcond; import aux::expr_prestate; @@ -45,8 +46,10 @@ import aux::ann_to_ts_ann; import aux::set_postcond_false; import aux::controlflow_expr; import aux::expr_to_constr; +import aux::if_ty; +import aux::if_check; +import aux::plain_if; -//import aux::constr_to_constr_occ; import aux::constraints_expr; import aux::substitute_constr_args; import aux::ninit; @@ -55,9 +58,9 @@ import aux::path_to_ident; import bitvectors::seq_preconds; import bitvectors::union_postconds; import bitvectors::intersect_postconds; -import bitvectors::declare_var; import bitvectors::bit_num; import bitvectors::gen; +import bitvectors::relax_precond_block; import front::ast::*; import middle::ty::expr_ann; import util::common::new_def_hash; @@ -161,26 +164,37 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body, &ann a) { find_pre_post_expr(fcx, index); find_pre_post_block(fcx, body); + auto v_init = rec(id=l.node.id, c=ninit(l.node.ident)); + relax_precond_block(fcx, bit_num(fcx, v_init), body); + auto loop_precond = - declare_var(fcx, rec(id=l.node.id, c=ninit(l.node.ident)), - seq_preconds(fcx, - [expr_pp(fcx.ccx, index), - block_pp(fcx.ccx, body)])); + seq_preconds(fcx, + [expr_pp(fcx.ccx, index), + block_pp(fcx.ccx, body)]); auto loop_postcond = intersect_postconds([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]); - set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond); + copy_pre_post_(fcx.ccx, a, loop_precond, loop_postcond); } // Generates a pre/post assuming that a is the // annotation for an if-expression with consequent conseq // and alternative maybe_alt fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, - &option::t[@expr] maybe_alt, &ann a) { + &option::t[@expr] maybe_alt, &ann a, &if_ty chck) { auto num_local_vars = num_constraints(fcx.enclosing); + find_pre_post_expr(fcx, antec); find_pre_post_block(fcx, conseq); alt (maybe_alt) { case (none) { + alt (chck) { + case (if_check) { + let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec); + gen(fcx, expr_ann(antec), c.node); + } + case (_) {} + } + auto precond_res = seq_preconds(fcx, [expr_pp(fcx.ccx, antec), @@ -189,15 +203,12 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, expr_poststate(fcx.ccx, antec)); } case (some(?altern)) { + /* + if check = if_check, then + be sure that the predicate implied by antec + is *not* true in the alternative + */ find_pre_post_expr(fcx, altern); - auto precond_true_case = - seq_preconds(fcx, - [expr_pp(fcx.ccx, antec), - block_pp(fcx.ccx, conseq)]); - auto postcond_true_case = - union_postconds(num_local_vars, - [expr_postcond(fcx.ccx, antec), - block_postcond(fcx.ccx, conseq)]); auto precond_false_case = seq_preconds(fcx, [expr_pp(fcx.ccx, antec), @@ -206,6 +217,25 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, union_postconds(num_local_vars, [expr_postcond(fcx.ccx, antec), expr_postcond(fcx.ccx, altern)]); + + /* Be sure to set the bit for the check condition here, + so that it's *not* set in the alternative. */ + alt (chck) { + case (if_check) { + let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec); + gen(fcx, expr_ann(antec), c.node); + } + case (_) {} + } + auto precond_true_case = + seq_preconds(fcx, + [expr_pp(fcx.ccx, antec), + block_pp(fcx.ccx, conseq)]); + auto postcond_true_case = + union_postconds(num_local_vars, + [expr_postcond(fcx.ccx, antec), + block_postcond(fcx.ccx, conseq)]); + auto precond_res = union_postconds(num_local_vars, [precond_true_case, @@ -396,8 +426,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { false_postcond(num_local_vars)); } case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { - find_pre_post_expr(fcx, antec); - join_then_else(fcx, antec, conseq, maybe_alt, a); + join_then_else(fcx, antec, conseq, maybe_alt, a, plain_if); } case (expr_binary(?bop, ?l, ?r, ?a)) { /* *unless* bop is lazy (e.g. and, or)? @@ -504,16 +533,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { gen(fcx, a, c.node); } case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) { - find_pre_post_expr(fcx, p); - copy_pre_post(fcx.ccx, a, p); - /* the typestate for the whole expression */ - join_then_else(fcx, p, conseq, maybe_alt, a); - - /* predicate p holds inside the "thn" expression */ - /* (so far, the negation of p does *not* hold inside - the "elsopt" expression) */ - let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); - gen(fcx, conseq.node.a, c.node); + join_then_else(fcx, p, conseq, maybe_alt, a, if_check); } case (expr_bind(?operator, ?maybe_args, ?a)) { diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 841a53702d11..b7c710e85c2a 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -32,19 +32,27 @@ import aux::stmt_pp; import aux::block_pp; import aux::set_pre_and_post; import aux::expr_prestate; +import aux::expr_precond; +import aux::expr_postcond; import aux::stmt_poststate; import aux::expr_poststate; +import aux::block_prestate; import aux::block_poststate; +import aux::block_precond; +import aux::block_postcond; import aux::fn_info; import aux::log_pp; +import aux::log_pp_err; import aux::extend_prestate_ann; import aux::extend_poststate_ann; import aux::set_prestate_ann; import aux::set_poststate_ann; import aux::pure_exp; import aux::log_bitv; +import aux::log_bitv_err; import aux::stmt_to_ann; import aux::log_states; +import aux::log_states_err; import aux::block_states; import aux::controlflow_expr; import aux::ann_to_def; @@ -52,6 +60,10 @@ import aux::expr_to_constr; import aux::ninit; import aux::npred; import aux::path_to_ident; +import aux::if_ty; +import aux::if_check; +import aux::plain_if; + import bitvectors::seq_preconds; import bitvectors::union_postconds; import bitvectors::intersect_postconds; @@ -69,11 +81,13 @@ import util::common::new_def_hash; import util::common::uistr; import util::common::log_expr; import util::common::log_block; +import util::common::log_block_err; import util::common::log_fn; import util::common::elt_exprs; import util::common::field_exprs; import util::common::has_nonlocal_exits; import util::common::log_stmt; +import util::common::log_stmt_err; import util::common::log_expr_err; fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs) -> @@ -111,6 +125,11 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l, changed = find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body) || changed; + + if (has_nonlocal_exits(body)) { + changed = set_poststate_ann(fcx.ccx, a, pres) || changed; + } + auto res_p = intersect_postconds([expr_poststate(fcx.ccx, index), block_poststate(fcx.ccx, body)]); @@ -130,14 +149,35 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool { } fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, - &option::t[@expr] maybe_alt, &ann a) -> bool { + &option::t[@expr] maybe_alt, &ann a, &if_ty chk, + &prestate pres) -> bool { auto changed = false; - changed = - find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec), - conseq) || changed; + changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; + changed = find_pre_post_state_expr(fcx, pres, antec) || changed; + + /* + log_err("join_then_else:"); + log_expr_err(*antec); + log_bitv_err(fcx, expr_prestate(fcx.ccx, antec)); + log_bitv_err(fcx, expr_poststate(fcx.ccx, antec)); + log_block_err(conseq); + log_bitv_err(fcx, block_prestate(fcx.ccx, conseq)); + log_bitv_err(fcx, block_poststate(fcx.ccx, conseq)); + log_err("****"); + log_bitv_err(fcx, expr_precond(fcx.ccx, antec)); + log_bitv_err(fcx, expr_postcond(fcx.ccx, antec)); + log_bitv_err(fcx, block_precond(fcx.ccx, conseq)); + log_bitv_err(fcx, block_postcond(fcx.ccx, conseq)); + */ + alt (maybe_alt) { case (none) { + + changed = + find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec), + conseq) || changed; + changed = extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, antec)) @@ -149,10 +189,35 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, expr_poststate(fcx.ccx, antec), altern) || changed; + + auto conseq_prestate = expr_poststate(fcx.ccx, antec); + alt (chk) { + case (if_check) { + let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec); + conseq_prestate = bitv::clone(conseq_prestate); + bitv::set(conseq_prestate, bit_num(fcx, c.node), true); + } + case (_) {} + } + + + changed = + find_pre_post_state_block(fcx, conseq_prestate, conseq) + || changed; + auto poststate_res = intersect_postconds([block_poststate(fcx.ccx, conseq), expr_poststate(fcx.ccx, altern)]); + /* fcx.ccx.tcx.sess.span_note(antec.span, + "poststate_res = " + aux::bitv_to_str(fcx, poststate_res)); + fcx.ccx.tcx.sess.span_note(antec.span, + "altern poststate = " + + aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, altern))); + fcx.ccx.tcx.sess.span_note(antec.span, + "conseq poststate = " + aux::bitv_to_str(fcx, + block_poststate(fcx.ccx, conseq))); */ + changed = extend_poststate_ann(fcx.ccx, a, poststate_res) || changed; @@ -164,10 +229,10 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { auto changed = false; auto num_local_vars = num_constraints(fcx.enclosing); - - /* + /* log_err("states:"); log_expr_err(*e); + aux::log_bitv_err(fcx, expr_prestate(fcx.ccx, e)); aux::log_bitv_err(fcx, expr_poststate(fcx.ccx, e)); */ @@ -182,6 +247,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { case (expr_call(?operator, ?operands, ?a)) { /* do the prestate for the rator */ + /* fcx.ccx.tcx.sess.span_note(operator.span, + "pres = " + aux::bitv_to_str(fcx, pres)); + */ + changed = find_pre_post_state_expr(fcx, pres, operator) || changed; /* rands go left-to-right */ @@ -201,6 +270,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { } case (_) { } } + + /* fcx.ccx.tcx.sess.span_note(operator.span, + "pres = " + aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, e))); + */ ret changed; } case (expr_spawn(_, _, ?operator, ?operands, ?a)) { @@ -436,9 +509,8 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { ret changed; } case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { - changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, antec) || changed; - changed = join_then_else(fcx, antec, conseq, maybe_alt, a) + changed = join_then_else(fcx, antec, conseq, maybe_alt, a, + plain_if, pres) || changed; ret changed; @@ -495,6 +567,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { changed = find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test), body) || changed; + /* conservative approximation: if a loop contains a break + or cont, we assume nothing about the poststate */ + if (has_nonlocal_exits(body)) { + changed = set_poststate_ann(fcx.ccx, a, pres) || changed; + } + changed = { auto e_post = expr_poststate(fcx.ccx, test); @@ -508,22 +586,35 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { } case (expr_do_while(?body, ?test, ?a)) { changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; + auto changed0 = changed; changed = find_pre_post_state_block(fcx, pres, body) || changed; - changed = - find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body), - test) || changed; /* conservative approximination: if the body of the loop could break or cont, we revert to the prestate (TODO: could treat cont differently from break, since if there's a cont, the test will execute) */ - if (has_nonlocal_exits(body)) { - changed = set_poststate_ann(fcx.ccx, a, pres) || changed; - } else { - changed = - extend_poststate_ann(fcx.ccx, a, - expr_poststate(fcx.ccx, test)) || - changed; + auto breaks = has_nonlocal_exits(body); + if (breaks) { + // this should probably be true_poststate and not pres, + // b/c the body could invalidate stuff + // FIXME + // This doesn't set "changed", as if the previous state + // was different, this might come back true every time + set_poststate_ann(fcx.ccx, body.node.a, pres); + changed = changed0; + } + + changed = + find_pre_post_state_expr(fcx, block_poststate(fcx.ccx, body), + test) || changed; + + if (breaks) { + set_poststate_ann(fcx.ccx, a, pres); + } + else { + changed = extend_poststate_ann(fcx.ccx, a, + expr_poststate(fcx.ccx, test)) || + changed; } ret changed; } @@ -605,7 +696,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { || changed; ret changed; } - case (expr_assert(?p, ?a)) { ret pure_exp(fcx.ccx, a, pres); } + case (expr_assert(?p, ?a)) { + changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; + changed = find_pre_post_state_expr(fcx, pres, p) || changed; + changed = extend_poststate_ann(fcx.ccx, a, pres) || changed; + ret changed; + } case (expr_check(?p, ?a)) { changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; changed = find_pre_post_state_expr(fcx, pres, p) || changed; @@ -617,13 +713,10 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { ret changed; } case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) { - changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, p) || changed; - let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); - changed = gen_poststate(fcx, expr_ann(p), c.node) || changed; - - changed = join_then_else(fcx, p, conseq, maybe_alt, a) + changed = join_then_else(fcx, p, conseq, maybe_alt, a, if_check, + pres) || changed; + ret changed; } case (expr_break(?a)) { ret pure_exp(fcx.ccx, a, pres); } @@ -651,14 +744,18 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { auto changed = false; auto stmt_ann = stmt_to_ann(fcx.ccx, *s); - log "*At beginning: stmt = "; - log_stmt(*s); - log "*prestate = "; - log bitv::to_str(stmt_ann.states.prestate); - log "*poststate ="; - log bitv::to_str(stmt_ann.states.poststate); - log "*changed ="; - log changed; + + /* + log_err "*At beginning: stmt = "; + log_stmt_err(*s); + log_err "*prestate = "; + log_err bitv::to_str(stmt_ann.states.prestate); + log_err "*poststate ="; + log_err bitv::to_str(stmt_ann.states.poststate); + log_err "*changed ="; + log_err changed; + */ + alt (s.node) { case (stmt_decl(?adecl, ?a)) { alt (adecl.node) { @@ -770,27 +867,21 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) -> post = expr_poststate(fcx.ccx, e); } } - /* - log_err("block:"); - log_block_err(b); - log_err("has non-local exits?"); - log_err(has_nonlocal_exits(b)); - */ - /* conservative approximation: if a block contains a break - or cont, we assume nothing about the poststate */ - - if (has_nonlocal_exits(b)) { post = pres0; } set_prestate_ann(fcx.ccx, b.node.a, pres0); set_poststate_ann(fcx.ccx, b.node.a, post); - log "For block:"; - log_block(b); - log "poststate = "; - log_states(block_states(fcx.ccx, b)); - log "pres0:"; - log_bitv(fcx, pres0); - log "post:"; - log_bitv(fcx, post); + + /* + log_err "For block:"; + log_block_err(b); + log_err "poststate = "; + log_states_err(block_states(fcx.ccx, b)); + log_err "pres0:"; + log_bitv_err(fcx, pres0); + log_err "post:"; + log_bitv_err(fcx, post); + */ + ret changed; } @@ -812,8 +903,10 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { // function with some other return type if (!type_is_nil(fcx.ccx.tcx, tailty) && !type_is_bot(fcx.ccx.tcx, tailty)) { - set_poststate_ann(fcx.ccx, tailann, - false_postcond(num_local_vars)); + auto p = false_postcond(num_local_vars); + set_poststate_ann(fcx.ccx, tailann, p); + // be sure to set the block poststate to the same thing + set_poststate_ann(fcx.ccx, f.body.node.a, p); alt (fcx.enclosing.cf) { case (noreturn) { kill_poststate(fcx, tailann, diff --git a/src/test/compile-fail/if-check-precond-fail.rs b/src/test/compile-fail/if-check-precond-fail.rs new file mode 100644 index 000000000000..e6c93db358c7 --- /dev/null +++ b/src/test/compile-fail/if-check-precond-fail.rs @@ -0,0 +1,30 @@ +// xfail-stage0 +// error-pattern:Unsatisfied precondition constraint +pred even(uint x) -> bool { + if (x < 2u) { + ret false; + } + else if (x == 2u) { + ret true; + } + else { + ret even(x - 2u); + } +} + +fn print_even(uint x) : even(x) { + log x; +} + +fn foo(uint x) -> () { + if check(even(x)) { + fail; + } + else { + print_even(x); + } +} + +fn main() { + foo(3u); +} diff --git a/src/test/run-pass/if-check-precond.rs b/src/test/run-pass/if-check-precond.rs new file mode 100644 index 000000000000..20a6090eb2a0 --- /dev/null +++ b/src/test/run-pass/if-check-precond.rs @@ -0,0 +1,29 @@ +// xfail-stage0 +pred even(uint x) -> bool { + if (x < 2u) { + ret false; + } + else if (x == 2u) { + ret true; + } + else { + ret even(x - 2u); + } +} + +fn print_even(uint x) : even(x) { + log x; +} + +fn foo(uint x) -> () { + if check(even(x)) { + print_even(x); + } + else { + fail; + } +} + +fn main() { + foo(2u); +} diff --git a/src/test/run-pass/if-check.rs b/src/test/run-pass/if-check.rs index f11a95781994..c647054abec7 100644 --- a/src/test/run-pass/if-check.rs +++ b/src/test/run-pass/if-check.rs @@ -1,5 +1,4 @@ // xfail-stage0 - pred even(uint x) -> bool { if (x < 2u) { ret false;