squiid/rust
1
0
Fork 0
Code Issues Pull requests Projects Activity

Handle lazy binops properly in typestate

Browse source 
The typestate analysis now reflects that the second operand of a
logical and or or may not be evaluated.
This commit is contained in:
Tim Chevalier 2011-06-28 13:07:05 -07:00
parent a7c4c19d4b
commit 28459ca0eb
4 changed files with 44 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/comp/middle/tstate/pre_post_conditions.rs
View file

@ -434,10 +434,19 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
find_pre_post_expr(fcx, ternary_to_if(e));
}
case (expr_binary(?bop, ?l, ?r)) {
/* *unless* bop is lazy (e.g. and, or)?
FIXME */
find_pre_post_exprs(fcx, [l, r], e.id);
if (lazy_binop(bop)) {
find_pre_post_expr(fcx, l);
find_pre_post_expr(fcx, r);
auto overall_pre = seq_preconds(fcx,
[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
overall_pre);
set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
expr_postcond(fcx.ccx, l));
}
else {
find_pre_post_exprs(fcx, [l, r], e.id);
}
}
case (expr_send(?l, ?r)) {
find_pre_post_exprs(fcx, [l, r], e.id);

16
src/comp/middle/tstate/states.rs
View file

@ -420,8 +420,18 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
ret find_pre_post_state_expr(fcx, pres, ternary_to_if(e));
}
case (expr_binary(?bop, ?l, ?r)) {
/* FIXME: what if bop is lazy? */
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
if (lazy_binop(bop)) {
auto changed = find_pre_post_state_expr(fcx, pres, l);
changed |= find_pre_post_state_expr(fcx,
expr_poststate(fcx.ccx, l), r);
ret changed
| set_prestate_ann(fcx.ccx, e.id, pres)
| set_poststate_ann(fcx.ccx, e.id,
expr_poststate(fcx.ccx, l));
}
else {
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
}
}
case (expr_send(?l, ?r)) {
ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure);
@ -507,7 +517,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
find_pre_post_state_expr(fcx, pres, val);
auto e_post = expr_poststate(fcx.ccx, val);
auto a_post;
if (vec::len[arm](alts) > 0u) {
if (vec::len(alts) > 0u) {
a_post = false_postcond(num_constrs);
for (arm an_alt in alts) {
changed |= find_pre_post_state_block

9
src/test/compile-fail/and-init.rs Normal file
View file

@ -0,0 +1,9 @@
// xfail-stage0
// error-pattern: Unsatisfied precondition constraint (for example, init(i
fn main() {
let int i;
log (false && {i = 5; true});
log i;
}

9
src/test/compile-fail/or-init.rs Normal file
View file

@ -0,0 +1,9 @@
// xfail-stage0
// error-pattern: Unsatisfied precondition constraint (for example, init(i
fn main() {
let int i;
log (false || {i = 5; true});
log i;
}