mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Restructure the "checking" pass in typestate

Browse Source 
I noticed that typestate was being lazier than it should be,
because it was only checking typestate for statements and
top-level expression (that is, the expression in a stmt_expr, but
not any subexpressions). So I rewrote the checks in tstate/ck.rs
to use walk, which exposed a few bugs in typestate that I fixed.

Also added some more test cases for if-check.
This commit is contained in:
Tim Chevalier 2011-06-17 19:07:23 -07:00
parent a4eb6630f3
commit 7fc89f573d
9 changed files with 386 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/comp/middle/tstate/ann.rs
View File

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

27
src/comp/middle/tstate/auxiliary.rs
View File

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

45
src/comp/middle/tstate/bitvectors.rs
View File

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

90
src/comp/middle/tstate/ck.rs
View File

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

76
src/comp/middle/tstate/pre_post_conditions.rs
View File

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

201
src/comp/middle/tstate/states.rs
View File

@ -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,

30
src/test/compile-fail/if-check-precond-fail.rs Normal file
View File

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

29
src/test/run-pass/if-check-precond.rs Normal file
View File

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

1
src/test/run-pass/if-check.rs
View File

@ -1,5 +1,4 @@
// xfail-stage0
pred even(uint x) -> bool {
if (x < 2u) {
ret false;