bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

Further work on typestate. Handles expr_rec and expr_assign now.

Browse source 
Also changed the ts_ann field on statements to be an ann instead,
which explains most of the changes.

As well, got rid of the "warning: no type for expression" error
by filling in annotations for local decls in typeck (not sure whether
this was my fault or not).

Finally, in bitv, added a clone() function to copy a bit vector,
and fixed is_true, is_false, and to_str to not be nonsense.
This commit is contained in:
Tim Chevalier 2011-04-12 12:16:21 -07:00 • committed by Graydon Hoare
parent 87d17c3a2c
commit d7e8818414
8 changed files with 547 additions and 251 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/comp/front/ast.rs
View file

@ -215,8 +215,10 @@ tag mode {
type stmt = spanned[stmt_];
tag stmt_ {
stmt_decl(@decl, option.t[@ts_ann]);
stmt_expr(@expr, option.t[@ts_ann]);
/* Only the ts_ann field is meaningful for statements,
but we make it an ann to make traversals simpler */
stmt_decl(@decl, ann);
stmt_expr(@expr, ann);
// These only exist in crate-level blocks.
stmt_crate_directive(@crate_directive);
}

16
src/comp/front/parser.rs
View file

@ -11,7 +11,7 @@ import util.common;
import util.common.filename;
import util.common.span;
import util.common.new_str_hash;
import util.typestate_ann.ts_ann;
import util.common.plain_ann;
tag restriction {
UNRESTRICTED;
@ -1562,14 +1562,15 @@ impure fn parse_source_stmt(parser p) -> @ast.stmt {
case (token.LET) {
auto decl = parse_let(p);
ret @spanned(lo, decl.span.hi,
ast.stmt_decl(decl, none[@ts_ann]));
auto hi = p.get_span();
ret @spanned
(lo, decl.span.hi, ast.stmt_decl(decl, plain_ann()));
}
case (token.AUTO) {
auto decl = parse_auto(p);
ret @spanned(lo, decl.span.hi,
ast.stmt_decl(decl, none[@ts_ann]));
auto hi = p.get_span();
ret @spanned(lo, decl.span.hi, ast.stmt_decl(decl, plain_ann()));
}
case (_) {
@ -1578,12 +1579,13 @@ impure fn parse_source_stmt(parser p) -> @ast.stmt {
auto i = parse_item(p);
auto hi = i.span.hi;
auto decl = @spanned(lo, hi, ast.decl_item(i));
ret @spanned(lo, hi, ast.stmt_decl(decl, none[@ts_ann]));
ret @spanned(lo, hi, ast.stmt_decl(decl, plain_ann()));
} else {
// Remainder are line-expr stmts.
auto e = parse_expr(p);
ret @spanned(lo, e.span.hi, ast.stmt_expr(e, none[@ts_ann]));
auto hi = p.get_span();
ret @spanned(lo, e.span.hi, ast.stmt_expr(e, plain_ann()));
}
}
}

22
src/comp/middle/fold.rs
View file

@ -232,11 +232,11 @@ type ast_fold[ENV] =
// Stmt folds.
(fn(&ENV e, &span sp,
@decl decl, option.t[@ts_ann] a)
@decl decl, ann a)
-> @stmt) fold_stmt_decl,
(fn(&ENV e, &span sp,
@expr e, option.t[@ts_ann] a)
@expr e, ann a)
-> @stmt) fold_stmt_expr,
// Item folds.
@ -470,7 +470,9 @@ fn fold_decl[ENV](&ENV env, ast_fold[ENV] fld, @decl d) -> @decl {
}
case (_) { /* fall through */ }
}
let @ast.local local_ = @rec(ty=ty_, init=init_ with *local);
auto ann_ = fld.fold_ann(env_, local.ann);
let @ast.local local_ =
@rec(ty=ty_, init=init_, ann=ann_ with *local);
ret fld.fold_decl_local(env_, d.span, local_);
}
@ -830,12 +832,14 @@ fn fold_stmt[ENV](&ENV env, ast_fold[ENV] fld, &@stmt s) -> @stmt {
alt (s.node) {
case (ast.stmt_decl(?d, ?a)) {
auto dd = fold_decl(env_, fld, d);
ret fld.fold_stmt_decl(env_, s.span, dd, a);
auto aa = fld.fold_ann(env_, a);
ret fld.fold_stmt_decl(env_, s.span, dd, aa);
}
case (ast.stmt_expr(?e, ?a)) {
auto ee = fold_expr(env_, fld, e);
ret fld.fold_stmt_expr(env_, s.span, ee, a);
auto aa = fld.fold_ann(env_, a);
ret fld.fold_stmt_expr(env_, s.span, ee, aa);
}
}
fail;
@ -1426,13 +1430,11 @@ fn identity_fold_pat_tag[ENV](&ENV e, &span sp, path p, vec[@pat] args,
// Stmt identities.
fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d,
option.t[@ts_ann] a) -> @stmt {
fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d, ann a) -> @stmt {
ret @respan(sp, ast.stmt_decl(d, a));
}
fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x,
option.t[@ts_ann] a) -> @stmt {
fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x, ann a) -> @stmt {
ret @respan(sp, ast.stmt_expr(x, a));
}
@ -1705,7 +1707,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
bind identity_fold_native_item_ty[ENV](_,_,_,_),
fold_item_tag = bind identity_fold_item_tag[ENV](_,_,_,_,_,_,_),
fold_item_obj = bind identity_fold_item_obj[ENV](_,_,_,_,_,_,_),
fold_view_item_use =
bind identity_fold_view_item_use[ENV](_,_,_,_,_,_),
fold_view_item_import =

17
src/comp/middle/typeck.rs
View file

@ -1541,7 +1541,7 @@ fn resolve_local_types_in_block(&@fn_ctxt fcx, &ast.block block)
// FIXME: rustboot bug prevents us from using these functions directly
auto fld = fold.new_identity_fold[option.t[@fn_ctxt]]();
auto wbl = writeback_local;
auto rltia = resolve_local_types_in_annotation;
auto rltia = bind resolve_local_types_in_annotation(_,_);
auto uefi = update_env_for_item;
auto kg = keep_going;
fld = @rec(
@ -2551,6 +2551,10 @@ fn check_decl_local(&@fn_ctxt fcx, &@ast.decl decl) -> @ast.decl {
alt (decl.node) {
case (ast.decl_local(?local)) {
auto t;
t = plain_ty(middle.ty.ty_nil);
alt (local.ty) {
case (none[@ast.ty]) {
// Auto slot. Do nothing for now.
@ -2559,9 +2563,18 @@ fn check_decl_local(&@fn_ctxt fcx, &@ast.decl decl) -> @ast.decl {
case (some[@ast.ty](?ast_ty)) {
auto local_ty = ast_ty_to_ty_crate(fcx.ccx, ast_ty);
fcx.locals.insert(local.id, local_ty);
t = local_ty;
}
}
auto a_res = local.ann;
alt (a_res) {
case (ann_none) {
a_res = triv_ann(t);
}
case (_) {}
}
auto initopt = local.init;
alt (local.init) {
case (some[ast.initializer](?init)) {
@ -2583,7 +2596,7 @@ fn check_decl_local(&@fn_ctxt fcx, &@ast.decl decl) -> @ast.decl {
}
case (_) { /* fall through */ }
}
auto local_1 = @rec(init = initopt with *local);
auto local_1 = @rec(init = initopt, ann = a_res with *local);
ret @rec(node=ast.decl_local(local_1)
with *decl);
}

637
src/comp/middle/typestate_check.rs
View file

@ -22,8 +22,12 @@ import front.ast.expr_call;
import front.ast.expr_vec;
import front.ast.expr_tup;
import front.ast.expr_path;
import front.ast.expr_field;
import front.ast.expr_index;
import front.ast.expr_log;
import front.ast.expr_block;
import front.ast.expr_rec;
import front.ast.expr_assign;
import front.ast.expr_lit;
import front.ast.path;
import front.ast.crate_directive;
@ -63,6 +67,7 @@ import util.common.new_str_hash;
import util.common.new_def_hash;
import util.common.uistr;
import util.common.elt_exprs;
import util.common.field_exprs;
import util.typestate_ann;
import util.typestate_ann.ts_ann;
import util.typestate_ann.empty_pre_post;
@ -82,12 +87,14 @@ import util.typestate_ann.set_postcondition;
import util.typestate_ann.set_prestate;
import util.typestate_ann.set_poststate;
import util.typestate_ann.set_in_postcond;
import util.typestate_ann.set_in_poststate;
import util.typestate_ann.implies;
import util.typestate_ann.pre_and_post_state;
import util.typestate_ann.empty_states;
import util.typestate_ann.empty_prestate;
import util.typestate_ann.empty_ann;
import util.typestate_ann.extend_prestate;
import util.typestate_ann.extend_poststate;
import middle.ty;
import middle.ty.ann_to_type;
@ -136,16 +143,6 @@ import util.typestate_ann.pps_len;
import util.typestate_ann.require_and_preserve;
/**** debugging junk ****/
fn log_expr(@expr e) -> () {
let str_writer s = string_writer();
auto out_ = mkstate(s.get_writer(), 80u);
auto out = @rec(s=out_,
comments=option.none[vec[front.lexer.cmnt]],
mutable cur_cmnt=0u);
print_expr(out, e);
log(s.get_str());
}
fn log_stmt(stmt st) -> () {
let str_writer s = string_writer();
@ -409,13 +406,38 @@ fn ann_to_ts_ann(ann a, uint nv) -> ts_ann {
}
}
fn stmt_ann(&stmt s) -> option.t[@ts_ann] {
fn ann_to_ts_ann_fail(ann a) -> option.t[@ts_ann] {
alt (a) {
case (ann_none) {
log("ann_to_ts_ann_fail: didn't expect ann_none here");
fail;
}
case (ann_type(_,_,?t)) {
ret t;
}
}
}
fn ann_to_ts_ann_fail_more(ann a) -> @ts_ann {
alt (a) {
case (ann_none) {
log("ann_to_ts_ann_fail: didn't expect ann_none here");
fail;
}
case (ann_type(_,_,?t)) {
check (! is_none[@ts_ann](t));
ret get[@ts_ann](t);
}
}
}
fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
alt (s.node) {
case (stmt_decl(_,?a)) {
ret a;
ret ann_to_ts_ann_fail(a);
}
case (stmt_expr(_,?a)) {
ret a;
ret ann_to_ts_ann_fail(a);
}
case (stmt_crate_directive(_)) {
ret none[@ts_ann];
@ -473,7 +495,7 @@ fn expr_pp(&expr e) -> pre_and_post {
}
fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
alt (stmt_ann(s)) {
alt (stmt_to_ann(s)) {
case (none[@ts_ann]) {
ret empty_states(nv);
}
@ -545,22 +567,21 @@ fn with_pp(ann a, pre_and_post p) -> ann {
// precondition shouldn't include x.
fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
let uint sz = len[pre_and_post](pps);
if (sz == 0u) {
ret true_precond(num_vars);
}
else {
auto first = pps.(0);
check(sz >= 1u);
auto first = pps.(0);
if (sz > 1u) {
check (pps_len(first) == num_vars);
let precond rest = seq_preconds(num_vars,
slice[pre_and_post](pps, 1u, sz));
difference(rest, first.postcondition);
union(first.precondition, rest);
ret (first.precondition);
}
ret (first.precondition);
}
fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond {
fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
auto sz = _vec.len[postcond](rest);
if (sz > 0u) {
@ -575,7 +596,7 @@ fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond {
fn union_postconds(&vec[postcond] pcs) -> postcond {
check (len[postcond](pcs) > 0u);
be union_postconds_go(pcs.(0), pcs);
ret union_postconds_go(bitv.clone(pcs.(0)), pcs);
}
/******* AST-traversing code ********/
@ -592,90 +613,64 @@ fn find_pre_post_obj(_obj o) -> _obj {
ret o; /* FIXME */
}
fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> item {
fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
alt (i.node) {
case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
auto e_pp = find_pre_post_expr(enclosing, *e);
log("1");
ret (respan(i.span,
ast.item_const(id, t, e_pp, di, a)));
find_pre_post_expr(enclosing, *e);
}
case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
check (fm.contains_key(di));
auto f_pp = find_pre_post_fn(fm, fm.get(di), f);
ret (respan(i.span,
ast.item_fn(id, f_pp, ps, di, a)));
find_pre_post_fn(fm, fm.get(di), f);
}
case (ast.item_mod(?id, ?m, ?di)) {
auto m_pp = find_pre_post_mod(m);
log("3");
ret (respan(i.span,
ast.item_mod(id, m_pp, di)));
find_pre_post_mod(m);
}
case (ast.item_native_mod(?id, ?nm, ?di)) {
auto n_pp = find_pre_post_native_mod(nm);
log("4");
ret (respan(i.span,
ast.item_native_mod(id, n_pp, di)));
find_pre_post_native_mod(nm);
}
case (ast.item_ty(_,_,_,_,_)) {
ret i;
ret;
}
case (ast.item_tag(_,_,_,_,_)) {
ret i;
ret;
}
case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
auto o_pp = find_pre_post_obj(o);
log("5");
ret (respan(i.span,
ast.item_obj(id, o_pp, ps, di, a)));
find_pre_post_obj(o);
}
}
}
fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
/* Fills in annotations as a side effect. Does not rebuild the expr */
fn find_pre_post_expr(&fn_info enclosing, &expr e) -> () {
auto num_local_vars = num_locals(enclosing);
fn do_rand_(fn_info enclosing, &@expr e) -> @expr {
log("for rand " );
log_expr(e);
log("pp = ");
auto res = find_pre_post_expr(enclosing, *e);
log_pp(expr_pp(*res));
ret res;
fn do_rand_(fn_info enclosing, &@expr e) -> () {
find_pre_post_expr(enclosing, *e);
}
fn pp_one(&@expr e) -> pre_and_post {
be expr_pp(*e);
}
auto do_rand = bind do_rand_(enclosing,_);
alt(e.node) {
case(expr_call(?oper, ?rands, ?a)) {
auto pp_oper = find_pre_post_expr(enclosing, *oper);
log("pp_oper =");
log_pp(expr_pp(*pp_oper));
case(expr_call(?operator, ?operands, ?a)) {
find_pre_post_expr(enclosing, *operator);
auto do_rand = bind do_rand_(enclosing,_);
auto f = do_rand;
auto pp_rands = _vec.map[@expr, @expr](f, rands);
_vec.map[@expr, ()](f, operands);
fn pp_one(&@expr e) -> pre_and_post {
be expr_pp(*e);
}
auto g = pp_one;
auto pps = _vec.map[@expr, pre_and_post](g, pp_rands);
_vec.push[pre_and_post](pps, expr_pp(*pp_oper));
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);
let ann a_res = with_pp(a, pp);
log("result for call");
log_expr(@e);
log("is:");
log_pp(pp);
ret (@respan(e.span,
expr_call(pp_oper, pp_rands, a_res)));
set_pre_and_post(a, pp);
ret;
}
case(expr_path(?p, ?maybe_def, ?a)) {
auto df;
@ -696,32 +691,111 @@ fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
}
// Otherwise, variable is global, so it must be initialized
log("pre/post for:\n");
log_expr(@e);
log("is");
log_pp(res);
ret (@respan
(e.span,
expr_path(p, maybe_def,
with_pp(a, res))));
set_pre_and_post(a, res);
}
case(expr_log(?arg, ?a)) {
log("log");
auto e_pp = find_pre_post_expr(enclosing, *arg);
log("pre/post for: ");
log_expr(arg);
log("is");
log_pp(expr_pp(*e_pp));
ret (@respan(e.span,
expr_log(e_pp, with_pp(a, expr_pp(*e_pp)))));
find_pre_post_expr(enclosing, *arg);
set_pre_and_post(a, expr_pp(*arg));
}
case (expr_block(?b, ?a)) {
log("block!");
fail;
}
case (expr_lit(?l, ?a)) {
ret @respan(e.span,
expr_lit(l, with_pp(a, empty_pre_post(num_local_vars))));
case (expr_rec(?fields,?maybe_base,?a)) {
/* factor out this code */
auto es = field_exprs(fields);
auto do_rand = bind do_rand_(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(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;
}
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(enclosing, *e);
set_pre_and_post(a_lhs, expr_pp(*e));
find_pre_post_expr(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(enclosing, *rhs);
set_pre_and_post(a_lhs, empty_pre_post(num_local_vars));
find_pre_post_expr(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(enclosing, *lhs);
find_pre_post_expr(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)))));
}
case (_) {
log("find_pre_post_for_expr: non-lval on lhs of assign");
fail;
}
}
}
case (expr_lit(_,?a)) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
}
case(_) {
log("this sort of expr isn't implemented!");
@ -730,118 +804,85 @@ fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
}
}
impure fn gen(&fn_info enclosing, ts_ann a, def_id id) {
impure fn gen(&fn_info enclosing, &ann a, def_id id) -> bool {
check(enclosing.contains_key(id));
let uint i = (enclosing.get(id))._0;
set_in_postcond(i, a.conditions);
ret set_in_postcond(i, (ann_to_ts_ann_fail_more(a)).conditions);
}
impure fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
check(enclosing.contains_key(id));
let uint i = (enclosing.get(id))._0;
ret set_in_poststate(i, (ann_to_ts_ann_fail_more(a)).states);
}
fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
-> ast.stmt {
-> () {
auto num_local_vars = num_locals(enclosing);
alt(s.node) {
case(ast.stmt_decl(?adecl, ?a)) {
alt(adecl.node) {
case(ast.decl_local(?alocal)) {
alt(alocal.init) {
case(some[ast.initializer](?an_init)) {
let @expr r = find_pre_post_expr(enclosing, *an_init.expr);
let init_op o = an_init.op;
let initializer a_i = rec(op=o, expr=r);
let ann res_ann = with_pp(alocal.ann, expr_pp(*r));
let @local res_local =
@rec(ty=alocal.ty, infer=alocal.infer,
ident=alocal.ident, init=some[initializer](a_i),
id=alocal.id, ann=res_ann);
alt(adecl.node) {
case(ast.decl_local(?alocal)) {
alt(alocal.init) {
case(some[ast.initializer](?an_init)) {
find_pre_post_expr(enclosing, *an_init.expr);
auto rhs_pp = expr_pp(*an_init.expr);
set_pre_and_post(alocal.ann, rhs_pp);
let ts_ann stmt_ann;
alt (a) {
case (none[@ts_ann]) {
stmt_ann = empty_ann(num_local_vars);
/* Inherit ann from initializer, and add var being
initialized to the postcondition */
set_pre_and_post(a, rhs_pp);
gen(enclosing, a, alocal.id);
}
case(none[ast.initializer]) {
auto pp = empty_pre_post(num_local_vars);
set_pre_and_post(alocal.ann, pp);
set_pre_and_post(a, pp);
}
}
case (some[@ts_ann](?aa)) {
stmt_ann = *aa;
}
}
/* Inherit ann from initializer, and add var being
initialized to the postcondition */
set_precondition(stmt_ann, expr_precond(*r));
set_postcondition(stmt_ann, expr_postcond(*r));
gen(enclosing, stmt_ann, alocal.id);
let stmt_ res = stmt_decl(@respan(adecl.span,
decl_local(res_local)),
some[@ts_ann](@stmt_ann));
ret (respan(s.span, res));
}
case(none[ast.initializer]) {
// log("pre/post for init of " + alocal.ident + ": none");
let ann res_ann = with_pp(alocal.ann,
empty_pre_post(num_local_vars));
let @local res_local =
@rec(ty=alocal.ty, infer=alocal.infer,
ident=alocal.ident, init=none[initializer],
id=alocal.id, ann=res_ann);
let stmt_ res =
stmt_decl
(@respan(adecl.span, decl_local(res_local)),
some[@ts_ann](@empty_ann(num_local_vars)));
ret respan(s.span, res); /* inherit ann from initializer */
case(decl_item(?anitem)) {
auto pp = empty_pre_post(num_local_vars);
set_pre_and_post(a, pp);
find_pre_post_item(fm, enclosing, *anitem);
}
}
}
case(decl_item(?anitem)) {
auto res_item = find_pre_post_item(fm, enclosing, *anitem);
ret respan(s.span,
stmt_decl(@respan(adecl.span,
decl_item(@res_item)),
some[@ts_ann](@empty_ann(num_local_vars))));
}
}
}
case(stmt_expr(?e,_)) {
log_expr(e);
let @expr e_pp = find_pre_post_expr(enclosing, *e);
/* inherit ann from expr */
ret respan(s.span,
stmt_expr(e_pp,
some[@ts_ann]
(@ann_to_ts_ann(expr_ann(*e_pp),
num_local_vars))));
case(stmt_expr(?e,?a)) {
find_pre_post_expr(enclosing, *e);
set_pre_and_post(a, expr_pp(*e));
}
}
}
fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
-> block {
fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> @stmt {
ret (@find_pre_post_stmt(fm, i, *s));
}
auto do_one = bind do_one_(fm, enclosing, _);
auto ss = _vec.map[@stmt, @stmt](do_one, b.node.stmts);
fn do_inner_(fn_info i, &@expr e) -> @expr {
ret find_pre_post_expr(i, *e);
}
auto do_inner = bind do_inner_(enclosing, _);
let option.t[@expr] e_ = option.map[@expr, @expr](do_inner, b.node.expr);
let block_ b_res = rec(stmts=ss, expr=e_, index=b.node.index);
ret respan(b.span, b_res);
-> () {
fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> () {
find_pre_post_stmt(fm, i, *s);
}
auto do_one = bind do_one_(fm, enclosing, _);
_vec.map[@stmt, ()](do_one, b.node.stmts);
fn do_inner_(fn_info i, &@expr e) -> () {
find_pre_post_expr(i, *e);
}
auto do_inner = bind do_inner_(enclosing, _);
option.map[@expr, ()](do_inner, b.node.expr);
}
fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> _fn {
ret rec(decl=f.decl, proto=f.proto,
body=find_pre_post_block(fm, fi, f.body));
fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> () {
find_pre_post_block(fm, fi, f.body);
}
fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
check (fm.contains_key(id));
auto res_f = find_pre_post_fn(fm, fm.get(id), f);
find_pre_post_fn(fm, fm.get(id), f);
ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
}
/* FIXME */
@ -850,11 +891,11 @@ fn find_pre_post_state_item(_fn_info_map fm, @item i) -> bool {
fail;
}
impure fn set_prestate_ann(ann a, prestate pre) -> () {
impure fn set_prestate_ann(ann a, prestate pre) -> bool {
alt (a) {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
set_prestate(*get[@ts_ann](ts_a), pre);
ret set_prestate(*get[@ts_ann](ts_a), pre);
}
case (ann_none) {
log("set_prestate_ann: expected an ann_type here");
@ -863,11 +904,25 @@ impure fn set_prestate_ann(ann a, prestate pre) -> () {
}
}
impure fn set_poststate_ann(ann a, poststate post) -> () {
impure fn extend_prestate_ann(ann a, prestate pre) -> bool {
alt (a) {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
set_poststate(*get[@ts_ann](ts_a), post);
ret extend_prestate((*get[@ts_ann](ts_a)).states.prestate, pre);
}
case (ann_none) {
log("set_prestate_ann: expected an ann_type here");
fail;
}
}
}
impure fn set_poststate_ann(ann a, poststate post) -> bool {
alt (a) {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
ret set_poststate(*get[@ts_ann](ts_a), post);
}
case (ann_none) {
log("set_poststate_ann: expected an ann_type here");
@ -876,6 +931,34 @@ impure fn set_poststate_ann(ann a, poststate post) -> () {
}
}
impure fn extend_poststate_ann(ann a, poststate post) -> bool {
alt (a) {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
ret extend_poststate((*get[@ts_ann](ts_a)).states.poststate, post);
}
case (ann_none) {
log("set_poststate_ann: expected an ann_type here");
fail;
}
}
}
impure fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
alt (a) {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
auto t = *get[@ts_ann](ts_a);
set_precondition(t, pp.precondition);
set_postcondition(t, pp.postcondition);
}
case (ann_none) {
log("set_pre_and_post: expected an ann_type here");
fail;
}
}
}
fn seq_states(&_fn_info_map fm, &fn_info enclosing,
prestate pres, vec[@expr] exprs) -> tup(bool, poststate) {
auto changed = false;
@ -894,20 +977,25 @@ fn find_pre_post_state_exprs(&_fn_info_map fm,
&prestate pres,
&ann a, &vec[@expr] es) -> bool {
auto res = seq_states(fm, enclosing, pres, es);
set_prestate_ann(a, pres);
set_poststate_ann(a, res._1);
ret res._0;
auto changed = res._0;
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_poststate_ann(a, res._1) || changed;
ret changed;
}
impure fn pure_exp(&ann a, &prestate p) -> () {
set_prestate_ann(a, p);
set_poststate_ann(a, p);
impure fn pure_exp(&ann a, &prestate p) -> bool {
auto changed = false;
changed = extend_prestate_ann(a, p) || changed;
changed = extend_poststate_ann(a, p) || changed;
ret changed;
}
fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
&prestate pres, &@expr e) -> bool {
auto changed = false;
/* a bit confused about when setting the states happens */
alt (e.node) {
case (expr_vec(?elts, _, ?a)) {
be find_pre_post_state_exprs(fm, enclosing, pres, a, elts);
@ -925,13 +1013,58 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
|| changed);
}
case (expr_path(_,_,?a)) {
pure_exp(a, pres);
ret false;
ret pure_exp(a, pres);
}
case (expr_log(?e,?a)) {
changed = find_pre_post_state_expr(fm, enclosing, pres, e);
set_prestate_ann(a, pres);
set_poststate_ann(a, expr_poststate(*e));
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_poststate_ann(a, expr_poststate(*e)) || changed;
ret changed;
}
case (expr_lit(?l,?a)) {
ret pure_exp(a, pres);
}
case (expr_block(?b,?a)) {
log("find_pre_post_state_expr: block!");
fail;
}
case (expr_rec(?fields,?maybe_base,?a)) {
changed = find_pre_post_state_exprs(fm, enclosing, pres, a,
field_exprs(fields)) || changed;
alt (maybe_base) {
case (none[@expr]) { /* do nothing */ }
case (some[@expr](?base)) {
changed = find_pre_post_state_expr(fm, enclosing, pres, base)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(*base))
|| changed;
}
}
ret changed;
}
case (expr_assign(?lhs, ?rhs, ?a)) {
extend_prestate_ann(a, pres);
alt (lhs.node) {
case (expr_path(?p, some[def](def_local(?d_id)), ?a_lhs)) {
// assignment to local var
changed = pure_exp(a_lhs, pres) || changed;
changed = find_pre_post_state_expr(fm, enclosing, pres, rhs)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(*rhs))
|| changed;
changed = gen_poststate(enclosing, a, d_id) || changed;
}
case (_) {
// assignment to something that must already have been init'd
changed = find_pre_post_state_expr(fm, enclosing, pres, lhs)
|| changed;
changed = find_pre_post_state_expr(fm, enclosing,
expr_poststate(*lhs), rhs) || changed;
changed = extend_poststate_ann(a, expr_poststate(*rhs))
|| changed;
}
}
ret changed;
}
case (_) {
@ -945,26 +1078,52 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
&prestate pres, @stmt s) -> bool {
auto changed = false;
auto stmt_ann_ = stmt_to_ann(*s);
check (!is_none[@ts_ann](stmt_ann_));
auto stmt_ann = *(get[@ts_ann](stmt_ann_));
/*
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);
*/
alt (s.node) {
case (stmt_decl(?adecl, ?a)) {
/* a must be some(a') at this point */
check (! is_none[@ts_ann](a));
auto stmt_ann = *(get[@ts_ann](a));
alt (adecl.node) {
case (ast.decl_local(?alocal)) {
alt (alocal.init) {
case (some[ast.initializer](?an_init)) {
changed = find_pre_post_state_expr
(fm, enclosing, pres, an_init.expr) || changed;
set_prestate(stmt_ann, expr_prestate(*an_init.expr));
set_poststate(stmt_ann, expr_poststate(*an_init.expr));
gen(enclosing, stmt_ann, alocal.id);
changed = extend_poststate(stmt_ann.states.poststate,
expr_poststate(*an_init.expr))
|| changed;
changed = gen_poststate(enclosing, a, alocal.id) || changed;
/*
log("Summary: stmt = ");
log_stmt(*s);
log("prestate = ");
log(bitv.to_str(stmt_ann.states.prestate));
log_bitv(enclosing, stmt_ann.states.prestate);
log("poststate =");
log_bitv(enclosing, stmt_ann.states.poststate);
log("changed =");
log(changed);
*/
ret changed;
}
case (none[ast.initializer]) {
set_prestate(stmt_ann, pres);
set_poststate(stmt_ann, pres);
ret false;
changed = extend_prestate(stmt_ann.states.prestate, pres)
|| changed;
changed = extend_poststate(stmt_ann.states.poststate, pres)
|| changed;
ret changed;
}
}
}
@ -973,12 +1132,23 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
}
}
}
case (stmt_expr(?e, ?a)) {
check (! is_none[@ts_ann](a));
auto stmt_ann = *(get[@ts_ann](a));
case (stmt_expr(?e, _)) {
changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
set_prestate(stmt_ann, expr_prestate(*e));
set_poststate(stmt_ann, expr_poststate(*e));
changed = extend_prestate(stmt_ann.states.prestate, expr_prestate(*e))
|| changed;
changed = extend_poststate(stmt_ann.states.poststate,
expr_poststate(*e)) || changed;
/*
log("Summary: stmt = ");
log_stmt(*s);
log("prestate = ");
log(bitv.to_str(stmt_ann.states.prestate));
log_bitv(enclosing, stmt_ann.states.prestate);
log("poststate =");
log_bitv(enclosing, stmt_ann.states.poststate);
log("changed =");
log(changed);
*/
ret changed;
}
case (_) { ret false; }
@ -1000,17 +1170,14 @@ fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, block b)
consist of improving <pres> with whatever variables this stmt initializes.
Then <pres> becomes the new poststate. */
for (@stmt s in b.node.stmts) {
changed = changed || find_pre_post_state_stmt(fm, enclosing, pres, s);
/* Shouldn't need to rebuild the stmt.
This just updates bit-vectors
in a side-effecting way. */
extend_prestate(pres, stmt_poststate(*s, num_local_vars));
changed = find_pre_post_state_stmt(fm, enclosing, pres, s) || changed;
pres = stmt_poststate(*s, num_local_vars);
}
alt (b.node.expr) {
case (none[@expr]) {}
case (some[@expr](?e)) {
changed = changed || find_pre_post_state_expr(fm, enclosing, pres, e);
changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
}
}
ret changed;
@ -1018,7 +1185,7 @@ fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, block b)
fn find_pre_post_state_fn(&_fn_info_map f_info, &fn_info fi, &ast._fn f)
-> bool {
be find_pre_post_state_block(f_info, fi, f.body);
ret find_pre_post_state_block(f_info, fi, f.body);
}
fn fixed_point_states(_fn_info_map fm, fn_info f_info,
@ -1028,7 +1195,7 @@ fn fixed_point_states(_fn_info_map fm, fn_info f_info,
auto changed = f(fm, f_info, start);
if (changed) {
be fixed_point_states(fm, f_info, f, start);
ret fixed_point_states(fm, f_info, f, start);
}
else {
// we're done!
@ -1047,7 +1214,7 @@ impure fn check_states_expr(fn_info enclosing, &expr e) -> () {
}
fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
alt (stmt_ann(s)) {
alt (stmt_to_ann(s)) {
case (none[@ts_ann]) {
ret;
}
@ -1055,6 +1222,15 @@ fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
let precond prec = ann_precond(*a);
let prestate pres = ann_prestate(*a);
/*
log("check_states_stmt:");
log_stmt(s);
log("prec = ");
log_bitv(enclosing, prec);
log("pres = ");
log_bitv(enclosing, pres);
*/
if (!implies(pres, prec)) {
log("check_states_stmt: unsatisfied precondition for ");
log_stmt(s);
@ -1103,16 +1279,47 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
}
fn init_ann(&fn_info fi, ann a) -> ann {
alt (a) {
case (ann_none) {
log("init_ann: shouldn't see ann_none");
fail;
}
case (ann_type(?t,?ps,_)) {
ret ann_type(t, ps, some[@ts_ann](@empty_ann(num_locals(fi))));
}
}
}
fn item_fn_anns(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
check(fm.contains_key(id));
auto f_info = fm.get(id);
auto fld0 = fold.new_identity_fold[fn_info]();
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
ret fold.fold_item[fn_info]
(f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a)));
}
fn check_crate(@ast.crate crate) -> @ast.crate {
/* Build the global map from function id to var-to-bit-num-map */
auto fn_info_map = mk_f_to_fn_info(crate);
/* Add a blank ts_ann to every statement (and expression) */
auto fld0 = fold.new_identity_fold[_fn_info_map]();
fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_) with *fld0);
auto with_anns = fold.fold_crate[_fn_info_map](fn_info_map, fld0, crate);
/* Compute the pre and postcondition for every subexpression */
auto fld = fold.new_identity_fold[_fn_info_map]();
fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
auto with_pre_postconditions = fold.fold_crate[_fn_info_map]
(fn_info_map, fld, crate);
(fn_info_map, fld, with_anns);
auto fld1 = fold.new_identity_fold[_fn_info_map]();

43
src/comp/util/common.rs
View file

@ -1,8 +1,17 @@
import std._uint;
import std._int;
import std._vec;
import std.option.none;
import front.ast;
import util.typestate_ann.ts_ann;
import std.io.stdout;
import std.io.str_writer;
import std.io.string_writer;
import pretty.pprust.print_block;
import pretty.pprust.print_expr;
import pretty.pprust.print_decl;
import pretty.pp.mkstate;
type filename = str;
type span = rec(uint lo, uint hi);
@ -94,6 +103,40 @@ fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] {
be _vec.map[ast.elt, @ast.expr](f, elts);
}
fn field_expr(&ast.field f) -> @ast.expr { ret f.expr; }
fn field_exprs(vec[ast.field] fields) -> vec [@ast.expr] {
auto f = field_expr;
ret _vec.map[ast.field, @ast.expr](f, fields);
}
fn plain_ann() -> ast.ann {
ret ast.ann_type(middle.ty.plain_ty(middle.ty.ty_nil),
none[vec[@middle.ty.t]], none[@ts_ann]);
}
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);
log(s.get_str());
}
fn log_block(&ast.block b) -> () {
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_block(out, b);
log(s.get_str());
}
//
// Local Variables:
// mode: rust

42
src/comp/util/typestate_ann.rs
View file

@ -72,7 +72,7 @@ fn difference(&precond p1, &precond p2) -> bool {
}
fn union(&precond p1, &precond p2) -> bool {
be bitv.difference(p1, p2);
be bitv.union(p1, p2);
}
fn pps_len(&pre_and_post p) -> uint {
@ -87,38 +87,52 @@ impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
bitv.set(p.postcondition, i, true);
}
impure fn set_in_postcond(uint i, &pre_and_post p) -> () {
impure fn set_in_postcond(uint i, &pre_and_post p) -> bool {
// sets the ith bit in p's post
auto was_set = bitv.get(p.postcondition, i);
bitv.set(p.postcondition, i, true);
ret !was_set;
}
impure fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
// sets the ith bit in p's post
auto was_set = bitv.get(s.poststate, i);
bitv.set(s.poststate, i, true);
ret !was_set;
}
// Sets all the bits in a's precondition to equal the
// corresponding bit in p's precondition.
impure fn set_precondition(&ts_ann a, &precond p) -> () {
bitv.copy(p, a.conditions.precondition);
bitv.copy(a.conditions.precondition, p);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
bitv.copy(p, a.conditions.postcondition);
bitv.copy(a.conditions.postcondition, p);
}
// Sets all the bits in a's prestate to equal the
// corresponding bit in p's prestate.
impure fn set_prestate(&ts_ann a, &prestate p) -> () {
bitv.copy(p, a.states.prestate);
impure fn set_prestate(&ts_ann a, &prestate p) -> bool {
ret bitv.copy(a.states.prestate, p);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
impure fn set_poststate(&ts_ann a, &poststate p) -> () {
bitv.copy(p, a.states.poststate);
impure fn set_poststate(&ts_ann a, &poststate p) -> bool {
ret bitv.copy(a.states.poststate, p);
}
// Set all the bits in p that are set in new
impure fn extend_prestate(&prestate p, &poststate new) -> () {
bitv.union(p, new);
impure fn extend_prestate(&prestate p, &poststate new) -> bool {
ret bitv.union(p, new);
}
// Set all the bits in p that are set in new
impure fn extend_poststate(&poststate p, &poststate new) -> bool {
ret bitv.union(p, new);
}
fn ann_precond(&ts_ann a) -> precond {
@ -129,7 +143,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
ret a.states.prestate;
}
// returns true if a implies b
// that is, returns true except if for some bits c and d,
// c = 1 and d = 0
impure fn implies(bitv.t a, bitv.t b) -> bool {
bitv.difference(b, a);
ret bitv.is_false(b);
auto tmp = bitv.clone(b);
bitv.difference(tmp, a);
ret bitv.is_false(tmp);
}

15
src/lib/bitv.rs
View file

@ -74,6 +74,15 @@ impure fn copy(&t v0, t v1) -> bool {
ret process(sub, v0, v1);
}
fn clone(t v) -> t {
auto storage = _vec.init_elt_mut[uint](0u, v.nbits / uint_bits() + 1u);
auto len = _vec.len[mutable uint](v.storage);
for each (uint i in _uint.range(0u, len)) {
storage.(i) = v.storage.(i);
}
ret rec(storage = storage, nbits = v.nbits);
}
fn get(&t v, uint i) -> bool {
check (i < v.nbits);
@ -137,7 +146,7 @@ impure fn set(&t v, uint i, bool x) {
/* true if all bits are 1 */
fn is_true(&t v) -> bool {
for(uint i in v.storage) {
for (uint i in to_vec(v)) {
if (i != 1u) {
ret false;
}
@ -148,7 +157,7 @@ fn is_true(&t v) -> bool {
/* true if all bits are non-1 */
fn is_false(&t v) -> bool {
for(uint i in v.storage) {
for (uint i in to_vec(v)) {
if (i == 1u) {
ret false;
}
@ -173,7 +182,7 @@ fn to_vec(&t v) -> vec[uint] {
fn to_str(&t v) -> str {
auto res = "";
for(uint i in v.storage) {
for (uint i in bitv.to_vec(v)) {
if (i == 1u) {
res += "1";
}