Skip to content

Typestate 2 #328

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

Typestate 2 #328

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
454eeb5
Make expr_while work in typestate_check
catamorphism Apr 13, 2011
9755cc2
rm unused import
catamorphism Apr 13, 2011
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
204 changes: 90 additions & 114 deletions src/comp/middle/typestate_check.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ import front.ast.expr_rec;
import front.ast.expr_if;
import front.ast.expr_binary;
import front.ast.expr_assign;
import front.ast.expr_while;
import front.ast.expr_lit;
import front.ast.expr_ret;
import front.ast.path;
Expand Down Expand Up @@ -71,6 +72,7 @@ import util.common.new_def_hash;
import util.common.uistr;
import util.common.elt_exprs;
import util.common.field_exprs;
import util.common.log_expr;
import util.typestate_ann;
import util.typestate_ann.ts_ann;
import util.typestate_ann.empty_pre_post;
Expand Down Expand Up @@ -717,6 +719,33 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
}
}

/* Finds the pre and postcondition for each expr in <args>;
sets the precondition in a to be the result of combining
the preconditions for <args>, and the postcondition in a to
be the union of all postconditions for <args> */
fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
&vec[@expr] args, ann a) {
fn do_one(_fn_info_map fm, fn_info enclosing,
&@expr e) -> () {
find_pre_post_expr(fm, enclosing, *e);
}
auto f = bind do_one(fm, enclosing, _);

_vec.map[@expr, ()](f, args);

fn get_pp(&@expr e) -> pre_and_post {
ret expr_pp(*e);
}
auto g = get_pp;
auto pps = _vec.map[@expr, pre_and_post](g, args);
auto h = get_post;

set_pre_and_post(a,
rec(precondition=seq_preconds(num_locals(enclosing), pps),
postcondition=union_postconds
(_vec.map[pre_and_post, postcond](h, pps))));
}

/* Fills in annotations as a side effect. Does not rebuild the expr */
fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
auto num_local_vars = num_locals(enclosing);
Expand All @@ -730,24 +759,9 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {

alt(e.node) {
case(expr_call(?operator, ?operands, ?a)) {
find_pre_post_expr(fm, enclosing, *operator);

auto do_rand = bind do_rand_(fm, enclosing,_);
auto f = do_rand;
_vec.map[@expr, ()](f, operands);

auto g = pp_one;
auto pps = _vec.map[@expr, pre_and_post](g, operands);
_vec.push[pre_and_post](pps, expr_pp(*operator));
auto h = get_post;
auto res_postconds = _vec.map[pre_and_post, postcond](h, pps);
auto res_postcond = union_postconds(res_postconds);

let pre_and_post pp =
rec(precondition=seq_preconds(num_local_vars, pps),
postcondition=res_postcond);
set_pre_and_post(a, pp);
ret;
auto args = _vec.clone[@expr](operands);
_vec.push[@expr](args, operator);
find_pre_post_exprs(fm, enclosing, args, a);
}
case(expr_path(?p, ?maybe_def, ?a)) {
auto df;
Expand Down Expand Up @@ -779,98 +793,21 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
set_pre_and_post(a, block_pp(b));
}
case (expr_rec(?fields,?maybe_base,?a)) {
/* factor out this code */
auto es = field_exprs(fields);
auto do_rand = bind do_rand_(fm, enclosing,_);
auto f = do_rand;
_vec.map[@expr, ()](f, es);
auto g = pp_one;
auto h = get_post;
/* FIXME avoid repeated code */
alt (maybe_base) {
case (none[@expr]) {
auto pps = _vec.map[@expr, pre_and_post](g, es);
auto res_postconds = _vec.map[pre_and_post, postcond]
(h, pps);
auto res_postcond = union_postconds(res_postconds);
let pre_and_post pp =
rec(precondition=seq_preconds(num_local_vars, pps),
postcondition=res_postcond);
set_pre_and_post(a, pp);
}
case (some[@expr](?base_exp)) {
find_pre_post_expr(fm, enclosing, *base_exp);

es += vec(base_exp);
auto pps = _vec.map[@expr, pre_and_post](g, es);
auto res_postconds = _vec.map[pre_and_post, postcond]
(h, pps);
auto res_postcond = union_postconds(res_postconds);

let pre_and_post pp =
rec(precondition=seq_preconds(num_local_vars, pps),
postcondition=res_postcond);
set_pre_and_post(a, pp);
}
}
ret;
_vec.plus_option[@expr](es, maybe_base);
find_pre_post_exprs(fm, enclosing, es, a);
}
case (expr_assign(?lhs, ?rhs, ?a)) {
// what's below should be compressed into two cases:
// path of a local, and non-path-of-a-local
alt (lhs.node) {
case (expr_field(?e,?id,?a_lhs)) {
// lhs is already initialized, so this doesn't initialize
// anything anew
find_pre_post_expr(fm, enclosing, *e);
set_pre_and_post(a_lhs, expr_pp(*e));

case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) {
find_pre_post_expr(fm, enclosing, *rhs);
let pre_and_post expr_assign_pp =
rec(precondition=seq_preconds
(num_local_vars,
vec(expr_pp(*e), expr_pp(*rhs))),
postcondition=union_postconds
(vec(expr_postcond(*e), expr_postcond(*rhs))));
set_pre_and_post(a, expr_assign_pp);
}
case (expr_path(?p,?maybe_def,?a_lhs)) {
find_pre_post_expr(fm, enclosing, *rhs);
set_pre_and_post(a_lhs, empty_pre_post(num_local_vars));
find_pre_post_expr(fm, enclosing, *rhs);
alt (maybe_def) {
// is this a local variable?
// if so, the only case in which an assign actually
// causes a variable to become initialized
case (some[def](def_local(?d_id))) {
set_pre_and_post(a, expr_pp(*rhs));
gen(enclosing, a, d_id);
}
case (_) {
// already initialized
set_pre_and_post(a, expr_pp(*rhs));
}
}
}
case (expr_index(?e,?sub,_)) {
// lhs is already initialized
// assuming the array subscript gets evaluated before the
// array
find_pre_post_expr(fm, enclosing, *lhs);
find_pre_post_expr(fm, enclosing, *rhs);
set_pre_and_post(a,
rec(precondition=
seq_preconds
(num_local_vars, vec(expr_pp(*lhs),
expr_pp(*rhs))),
postcondition=
union_postconds(vec(expr_postcond(*lhs),
expr_postcond(*rhs)))));

set_pre_and_post(a, expr_pp(*rhs));
gen(enclosing, a, d_id);
}
case (_) {
log("find_pre_post_for_expr: non-lval on lhs of assign");
fail;
// doesn't check that lhs is an lval, but
// that's probably ok
find_pre_post_exprs(fm, enclosing, vec(lhs, rhs), a);
}
}
}
Expand Down Expand Up @@ -927,15 +864,22 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
case (expr_binary(?bop,?l,?r,?a)) {
/* *unless* bop is lazy (e.g. and, or)?
FIXME */
find_pre_post_expr(fm, enclosing, *l);
find_pre_post_expr(fm, enclosing, *r);
set_pre_and_post(a,
rec(precondition=
seq_preconds(num_local_vars,
vec(expr_pp(*l), expr_pp(*r))),
postcondition=
union_postconds(vec(expr_postcond(*l),
expr_postcond(*r)))));
find_pre_post_exprs(fm, enclosing, vec(l, r), a);
}
case (expr_while(?test, ?body, ?a)) {
find_pre_post_expr(fm, enclosing, *test);
find_pre_post_block(fm, enclosing, body);
set_pre_and_post(a,
rec(precondition=
seq_preconds(num_local_vars,
vec(expr_pp(*test),
block_pp(body))),
postcondition=
intersect_postconds(vec(expr_postcond(*test),
block_postcond(body)))));
}
case (expr_index(?e, ?sub, ?a)) {
find_pre_post_exprs(fm, enclosing, vec(e, sub), a);
}
case(_) {
log("this sort of expr isn't implemented!");
Expand Down Expand Up @@ -1253,6 +1197,33 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
changed = extend_poststate_ann(a, expr_poststate(*r)) || changed;
ret changed;
}
case (expr_while(?test, ?body, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
/* 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?
*/
changed = find_pre_post_state_expr(fm, enclosing, pres, test)
|| changed;
changed = find_pre_post_state_block(fm,
enclosing, expr_poststate(*test), body) || changed;
changed = extend_poststate_ann(a,
intersect_postconds(vec(expr_poststate(*test),
block_poststate(body)))) || changed;
ret changed;
}
case (expr_index(?e, ?sub, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
changed = find_pre_post_state_expr(fm, enclosing,
expr_poststate(*e), sub) || changed;
changed = extend_poststate_ann(a, expr_poststate(*sub));
ret changed;
}
case (_) {
log("find_pre_post_state_expr: implement this case!");
fail;
Expand Down Expand Up @@ -1397,8 +1368,13 @@ impure fn check_states_expr(fn_info enclosing, &expr e) -> () {
let prestate pres = expr_prestate(e);

if (!implies(pres, prec)) {
log("check_states_expr: unsatisfied precondition");
fail;
log("check_states_stmt: unsatisfied precondition for ");
log_expr(e);
log("Precondition: ");
log_bitv(enclosing, prec);
log("Prestate: ");
log_bitv(enclosing, pres);
fail;
}
}

Expand Down
4 changes: 2 additions & 2 deletions src/comp/util/common.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,14 +115,14 @@ fn plain_ann() -> ast.ann {
none[vec[@middle.ty.t]], none[@ts_ann]);
}

fn log_expr(@ast.expr e) -> () {
fn log_expr(&ast.expr e) -> () {
let str_writer s = string_writer();
auto out_ = mkstate(s.get_writer(), 80u);
auto out = @rec(s=out_,
comments=none[vec[front.lexer.cmnt]],
mutable cur_cmnt=0u);

print_expr(out, e);
print_expr(out, @e);
log(s.get_str());
}

Expand Down
11 changes: 11 additions & 0 deletions src/lib/_vec.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -251,6 +251,17 @@ fn or(&vec[bool] v) -> bool {
be _vec.foldl[bool, bool](f, false, v);
}

fn clone[T](&vec[T] v) -> vec[T] {
ret slice[T](v, 0u, len[T](v));
}

fn plus_option[T](&vec[T] v, &option.t[T] o) -> () {
alt (o) {
case (none[T]) {}
case (some[T](?x)) { v += vec(x); }
}
}

// Local Variables:
// mode: rust;
// fill-column: 78;
Expand Down