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

Tests for while loops that may invalidate constraints

Browse Source 
Wrote some small test cases that use while loops and moves, to
make sure the poststate for the loop body gets propagated into the
new prestate and deinitialization gets reflected.

Along with that, rewrite the code for intersecting states. I still
find it dodgy, but I guess I'll continue trying to add more tests.
Also, I'll probably feel better about it once I start formalizing
the algorithm.
This commit is contained in:
Tim Chevalier 2011-06-27 18:12:37 -07:00
parent 6d1050b1c7
commit 85b5b2a8e4
9 changed files with 200 additions and 96 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -112,7 +112,7 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool {
// sets the ith bit in p's post
auto was_set = tritv_get(p.postcondition, i);
tritv_set(i, p.postcondition, ttrue);
ret was_set == dont_care;
ret was_set != ttrue;
}
fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
@ -123,7 +123,7 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
fn set_in_poststate_(uint i, &poststate p) -> bool {
auto was_set = tritv_get(p, i);
tritv_set(i, p, ttrue);
ret was_set == dont_care;
ret was_set != ttrue;
}
@ -135,14 +135,25 @@ fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool {
fn clear_in_poststate_(uint i, &poststate s) -> bool {
auto was_set = tritv_get(s, i);
tritv_set(i, s, tfalse);
ret was_set == dont_care;
ret was_set != tfalse;
}
fn clear_in_prestate(uint i, &pre_and_post_state s) -> bool {
// sets the ith bit in p's pre
ret clear_in_prestate_(i, s.prestate);
}
fn clear_in_prestate_(uint i, &prestate s) -> bool {
auto was_set = tritv_get(s, i);
tritv_set(i, s, tfalse);
ret was_set != tfalse;
}
fn clear_in_postcond(uint i, &pre_and_post s) -> bool {
// sets the ith bit in p's post
auto was_set = tritv_get(s.postcondition, i);
tritv_set(i, s.postcondition, tfalse);
ret was_set == dont_care;
ret was_set != tfalse;
}
// Sets all the bits in a's precondition to equal the

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

@ -43,6 +43,7 @@
import tstate::ann::set_in_poststate;
import tstate::ann::set_in_poststate_;
import tstate::ann::clear_in_poststate;
import tstate::ann::clear_in_prestate;
import tstate::ann::clear_in_poststate_;
import tritv::*;
@ -147,22 +148,10 @@ fn seq_preconds_go(&fn_ctxt fcx, &vec[pre_and_post] pps,
} else { ret true_precond(num_vars); }
}
/* Gee, maybe we could use foldl or something */
fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
auto sz = vec::len[postcond](rest);
if (sz > 0u) {
auto other = rest.(0);
intersect(first, other);
intersect_postconds_go(first,
slice[postcond](rest, 1u,
len[postcond](rest)));
}
ret first;
}
fn intersect_postconds(&vec[postcond] pcs) -> postcond {
assert (len[postcond](pcs) > 0u);
ret intersect_postconds_go(tritv_clone(pcs.(0)), pcs);
fn intersect_states(&prestate p, &prestate q) -> prestate {
auto rslt = tritv_clone(p);
tritv_intersect(rslt, q);
ret rslt;
}
fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
@ -219,6 +208,11 @@ fn gen_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
node_id_to_ts_ann(fcx.ccx, id).states);
}
fn kill_prestate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
ret clear_in_prestate(bit_num(fcx, c),
node_id_to_ts_ann(fcx.ccx, id).states);
}
fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
log "kill_poststate";
ret clear_in_poststate(bit_num(fcx, c),
@ -254,6 +248,16 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t);
}
fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
&node_id parent) -> bool {
ret kill_poststate(fcx, parent, rec(id=id, c=ninit(ident)));
}
fn clear_in_prestate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
&node_id parent) -> bool {
ret kill_prestate(fcx, parent, rec(id=id, c=ninit(ident)));
}
//
// Local Variables:
// mode: rust

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

@ -70,9 +70,9 @@ fn check_states_expr(&fn_ctxt fcx, &@expr e) {
log_err("check_states_expr:");
util::common::log_expr_err(*e);
log_err("prec = ");
log_bitv_err(fcx, prec);
log_tritv_err(fcx, prec);
log_err("pres = ");
log_bitv_err(fcx, pres);
log_tritv_err(fcx, pres);
*/
if (!implies(pres, prec)) {
@ -99,9 +99,9 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
log_err("check_states_stmt:");
log_stmt_err(*s);
log_err("prec = ");
log_bitv_err(fcx, prec);
log_tritv_err(fcx, prec);
log_err("pres = ");
log_bitv_err(fcx, pres);
log_tritv_err(fcx, pres);
*/
if (!implies(pres, prec)) {

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

@ -59,7 +59,7 @@
import bitvectors::promises;
import bitvectors::seq_preconds;
import bitvectors::seq_postconds;
import bitvectors::intersect_postconds;
import bitvectors::intersect_states;
import bitvectors::declare_var;
import bitvectors::gen_poststate;
import bitvectors::relax_precond_block;
@ -180,9 +180,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block 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)]);
auto loop_postcond = intersect_states(expr_postcond(fcx.ccx, index),
block_postcond(fcx.ccx, body));
copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
}
@ -247,8 +246,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
seq_postconds(fcx, [precond_true_case,
precond_false_case]);
auto postcond_res =
intersect_postconds([postcond_true_case,
postcond_false_case]);
intersect_states(postcond_true_case, postcond_false_case);
set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
}
}
@ -459,10 +457,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
seq_preconds(fcx,
[expr_pp(fcx.ccx, test),
block_pp(fcx.ccx, body)]),
intersect_postconds([expr_postcond(fcx.ccx,
test),
block_postcond(fcx.ccx,
body)]));
intersect_states(expr_postcond(fcx.ccx, test),
block_postcond(fcx.ccx,
body)));
}
case (expr_do_while(?body, ?test)) {
find_pre_post_block(fcx, body);

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

@ -69,10 +69,12 @@
import bitvectors::set_in_poststate_ident;
import bitvectors::clear_in_poststate_expr;
import bitvectors::intersect_postconds;
import bitvectors::clear_in_prestate_ident;
import bitvectors::bit_num;
import bitvectors::gen_poststate;
import bitvectors::kill_poststate;
import bitvectors::clear_in_poststate_ident;
import bitvectors::intersect_states;
import front::ast;
import front::ast::*;
import middle::ty::expr_ty;
@ -188,23 +190,27 @@ fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, ast::node_id id,
fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l,
&@expr index, &block body, node_id id) -> bool {
/* same issues as while */
auto loop_pres = intersect_states(pres,
block_poststate(fcx.ccx, body));
// FIXME: also want to set l as initialized, no?
auto changed = set_prestate_ann(fcx.ccx, id, pres) |
auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
find_pre_post_state_expr(fcx, pres, index);
/* in general, would need the intersection of
(poststate of index, poststate of body) */
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body);
if (has_nonlocal_exits(body)) {
changed |= set_poststate_ann(fcx.ccx, id, pres);
// See [Break-unsound]
ret (changed | set_poststate_ann(fcx.ccx, id, pres));
}
else {
auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body));
/*
auto res_p =
intersect_postconds([expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body)]);
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
block_poststate(fcx.ccx, body)]); */
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
}
}
fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool {
@ -269,16 +275,18 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
find_pre_post_state_block(fcx, conseq_prestate, conseq);
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));
intersect_states(block_poststate(fcx.ccx, conseq),
expr_poststate(fcx.ccx, altern));
/*
fcx.ccx.tcx.sess.span_note(antec.span,
"poststate_res = " + aux::tritv_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)));
aux::tritv_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))); */
"conseq poststate = " + aux::tritv_to_str(fcx,
block_poststate(fcx.ccx, conseq)));
*/
changed |= set_poststate_ann(fcx.ccx, id, poststate_res);
}
@ -287,7 +295,7 @@ 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 num_local_vars = num_constraints(fcx.enclosing);
auto num_constrs = num_constraints(fcx.enclosing);
alt (e.node) {
case (expr_vec(?elts, _, _)) {
@ -381,7 +389,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
a ret expression (since execution never continues locally
after a ret expression */
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars));
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
/* return from an always-failing function clears the return bit */
alt (fcx.enclosing.cf) {
@ -401,7 +409,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
}
case (expr_be(?val)) {
auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars));
set_poststate_ann(fcx.ccx, e.id, false_postcond(num_constrs));
ret changed | find_pre_post_state_expr(fcx, pres, val);
}
case (expr_if(?antec, ?conseq, ?maybe_alt)) {
@ -423,55 +431,62 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
oper_assign);
}
case (expr_while(?test, ?body)) {
auto changed = set_prestate_ann(fcx.ccx, e.id, pres) |
/* to handle general predicates, we need to pass in
pres `intersect` (poststate(a))
like: auto test_pres = intersect_postconds(pres,
expr_postcond(a)); However, this doesn't work right now because
we would be passing in an all-zero prestate initially
FIXME
maybe need a "don't know" state in addition to 0 or 1?
/*
log_err "in a while loop:";
log_expr_err(*e);
aux::log_tritv_err(fcx, block_poststate(fcx.ccx, body));
aux::log_tritv_err(fcx, pres);
*/
find_pre_post_state_expr(fcx, pres, test) |
auto loop_pres = intersect_states
(block_poststate(fcx.ccx, body), pres);
// aux::log_tritv_err(fcx, loop_pres);
// log_err "---------------";
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres) |
find_pre_post_state_expr(fcx, loop_pres, test) |
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, test),
body);
/* conservative approximation: if a loop contains a break
or cont, we assume nothing about the poststate */
/* which is still unsound -- see [Break-unsound] */
if (has_nonlocal_exits(body)) {
changed |= set_poststate_ann(fcx.ccx, e.id, pres);
ret changed | set_poststate_ann(fcx.ccx, e.id, pres);
}
else {
auto e_post = expr_poststate(fcx.ccx, test);
auto b_post = block_poststate(fcx.ccx, body);
ret changed | set_poststate_ann
(fcx.ccx, e.id, intersect_states(e_post, b_post));
}
auto e_post = expr_poststate(fcx.ccx, test);
auto b_post = block_poststate(fcx.ccx, body);
ret changed | set_poststate_ann
(fcx.ccx, e.id, intersect_postconds([e_post, b_post]));
}
case (expr_do_while(?body, ?test)) {
auto changed = set_prestate_ann(fcx.ccx, e.id, pres);
auto changed0 = changed;
changed |= find_pre_post_state_block(fcx, pres, body);
auto loop_pres = intersect_states(expr_poststate(fcx.ccx, test),
pres);
auto changed = set_prestate_ann(fcx.ccx, e.id, loop_pres);
changed |= find_pre_post_state_block(fcx, loop_pres, body);
/* 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) */
changed |= find_pre_post_state_expr
(fcx, block_poststate(fcx.ccx, body), test);
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.id, pres);
changed = changed0;
}
changed |= find_pre_post_state_expr
(fcx, block_poststate(fcx.ccx, body), test);
if (breaks) {
set_poststate_ann(fcx.ccx, e.id, pres);
}
// FIXME [Break-unsound]
// This is unsound as it is -- consider
// while (true) {
// x <- y;
// break;
// }
// The poststate wouldn't take into account that
// y gets deinitialized
changed |= set_poststate_ann(fcx.ccx, e.id, pres);
}
else {
changed |= set_poststate_ann
(fcx.ccx, e.id, expr_poststate(fcx.ccx, test));
@ -493,7 +508,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
auto e_post = expr_poststate(fcx.ccx, val);
auto a_post;
if (vec::len[arm](alts) > 0u) {
a_post = false_postcond(num_local_vars);
a_post = false_postcond(num_constrs);
for (arm an_alt in alts) {
changed |= find_pre_post_state_block
(fcx, e_post, an_alt.block);
@ -524,7 +539,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
/* if execution continues after fail, then everything is true!
woo! */
set_poststate_ann(fcx.ccx, e.id,
false_postcond(num_local_vars));
false_postcond(num_constrs));
}
case (expr_assert(?p)) {
ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
@ -604,8 +619,12 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
*/
}
case (none) {
ret set_prestate(stmt_ann, pres) |
set_poststate(stmt_ann, pres);
// let int = x; => x is uninit in poststate
set_poststate_ann(fcx.ccx, id, pres);
clear_in_poststate_ident(fcx, alocal.node.id,
alocal.node.ident, id);
set_prestate(stmt_ann, pres);
ret false;
}
}
}
@ -683,6 +702,8 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
auto num_local_vars = num_constraints(fcx.enclosing);
// make sure the return bit starts out False
clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id);
auto changed =
find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body),
f.body);
@ -704,6 +725,13 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
}
case (none) {/* fallthrough */ }
}
/*
log_err "find_pre_post_state_fn";
log_err changed;
fcx.ccx.tcx.sess.span_note(f.body.span, fcx.name);
*/
ret changed;
}
//

28
src/comp/middle/tstate/tritv.rs
View File

@ -82,18 +82,32 @@ fn trit_or(trit a, trit b) -> trit {
}
}
// FIXME: This still seems kind of dodgy to me (that is,
// that 1 + ? = 1. But it might work out given that
// all variables start out in a 0 state. Probably I need
// to make it so that all constraints start out in a 0 state
// (we consider a constraint false until proven true), too.
fn trit_and(trit a, trit b) -> trit {
alt (a) {
case (dont_care) { dont_care }
case (ttrue) {
alt (b) {
case (dont_care) { dont_care }
case (ttrue) { ttrue }
case (tfalse) { dont_care } // ???
case (dont_care) { b } // also seems wrong for case b = ttrue
case (ttrue) {
alt (b) {
case (dont_care) { ttrue } // ??? Seems wrong
case (ttrue) { ttrue }
// false wins, since if something is uninit
// on one path, we care
// (Rationale: it's always safe to assume that
// a var is uninitialized or that a constraint
// needs to be re-established)
case (tfalse) { tfalse }
}
}
}
// Rationale: if it's uninit on one path,
// we can consider it as uninit on all paths
case (tfalse) { tfalse }
}
// if the result is dont_care, that means
// a and b were both dont_care
}
fn change(bool changed, trit old, trit new) -> bool { changed || new != old }

17
src/test/compile-fail/do-while-constraints.rs Normal file
View File

@ -0,0 +1,17 @@
// xfail-stage0
// error-pattern: Unsatisfied precondition constraint (for example, init(y
fn main() {
let int y = 42;
let int x;
do {
log y;
do {
do {
do {
x <- y;
} while (true);
} while (true);
} while (true);
} while (true);
}

17
src/test/compile-fail/while-loop-constraints.rs Normal file
View File

@ -0,0 +1,17 @@
// xfail-stage0
// error-pattern: Unsatisfied precondition constraint (for example, init(y
fn main() {
let int y = 42;
let int x;
while (true) {
log y;
while (true) {
while (true) {
while (true) {
x <- y;
}
}
}
}
}

16
src/test/run-pass/while-loop-constraints-2.rs Normal file
View File

@ -0,0 +1,16 @@
// xfail-stage0
fn main() {
let int y = 42;
let int z = 42;
let int x;
while (z < 50) {
z += 1;
while (false) {
x <- y;
y = z;
}
log y;
}
assert (y == 42 && z == 50);
}