From 63e87c102d7b57b697fe274c64b9c895113e9171 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Tue, 12 Apr 2011 19:03:52 -0700 Subject: [PATCH] typestate_check can now handle expr_block, expr_if, and expr_binary (caveat for the latter: it assumes that binary operations are strict; a TODO is to detect or and and and correctly reflect that they're lazy in the second argument). I had to add an ann field to ast.block, resulting in the usual boilerplate changes. Test cases that currently work (if you uncomment the typestate pass in the driver) (all these are under test/compile-fail): fru-typestate ret-uninit use-uninit use-uninit-2 use-uninit-3 --- src/comp/front/ast.rs | 3 +- src/comp/front/parser.rs | 2 +- src/comp/middle/fold.rs | 3 +- src/comp/middle/typeck.rs | 6 +- src/comp/middle/typestate_check.rs | 501 ++++++++++++++++++++--------- src/comp/util/typestate_ann.rs | 4 + 6 files changed, 358 insertions(+), 161 deletions(-) diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index dfc69695c269e..b0035ba618e3a 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -100,7 +100,8 @@ tag block_index_entry { } type block_ = rec(vec[@stmt] stmts, option.t[@expr] expr, - hashmap[ident,block_index_entry] index); + hashmap[ident,block_index_entry] index, + ann a); /* ann is only meaningful for the ts_ann field */ type variant_def = tup(def_id /* tag */, def_id /* variant */); diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs index 85badb1e7099c..ab44f6380d933 100644 --- a/src/comp/front/parser.rs +++ b/src/comp/front/parser.rs @@ -1598,7 +1598,7 @@ fn index_block(vec[@ast.stmt] stmts, option.t[@ast.expr] expr) -> ast.block_ { for (@ast.stmt s in stmts) { ast.index_stmt(index, s); } - ret rec(stmts=stmts, expr=expr, index=index); + ret rec(stmts=stmts, expr=expr, index=index, a=ast.ann_none); } fn index_arm(@ast.pat pat) -> hashmap[ast.ident,ast.def_id] { diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs index e9c4ee2a0ba50..fbf43c55a3381 100644 --- a/src/comp/middle/fold.rs +++ b/src/comp/middle/fold.rs @@ -871,7 +871,8 @@ fn fold_block[ENV](&ENV env, ast_fold[ENV] fld, &block blk) -> block { } } - ret respan(blk.span, rec(stmts=stmts, expr=expr, index=index)); + auto aa = fld.fold_ann(env, blk.node.a); + ret respan(blk.span, rec(stmts=stmts, expr=expr, index=index, a=aa)); } fn fold_arm[ENV](&ENV env, ast_fold[ENV] fld, &arm a) -> arm { diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 5c512e7eac5db..f87460569c8d4 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1399,7 +1399,8 @@ mod Pushdown { auto e_1 = pushdown_expr(fcx, expected, e_0); auto block_ = rec(stmts=bloc.node.stmts, expr=some[@ast.expr](e_1), - index=bloc.node.index); + index=bloc.node.index, + a=boring_ann()); ret fold.respan[ast.block_](bloc.span, block_); } case (none[@ast.expr]) { @@ -2569,7 +2570,8 @@ fn check_block(&@fn_ctxt fcx, &ast.block block) -> ast.block { ret fold.respan[ast.block_](block.span, rec(stmts=stmts, expr=expr, - index=block.node.index)); + index=block.node.index, + a=boring_ann())); } fn check_const(&@crate_ctxt ccx, &span sp, ast.ident ident, @ast.ty t, diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 8b51e1be72e0b..11aad9a2d4aa0 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -27,8 +27,11 @@ import front.ast.expr_index; import front.ast.expr_log; import front.ast.expr_block; import front.ast.expr_rec; +import front.ast.expr_if; +import front.ast.expr_binary; import front.ast.expr_assign; import front.ast.expr_lit; +import front.ast.expr_ret; import front.ast.path; import front.ast.crate_directive; import front.ast.fn_decl; @@ -71,6 +74,7 @@ import util.common.field_exprs; import util.typestate_ann; import util.typestate_ann.ts_ann; import util.typestate_ann.empty_pre_post; +import util.typestate_ann.empty_poststate; import util.typestate_ann.true_precond; import util.typestate_ann.true_postcond; import util.typestate_ann.postcond; @@ -95,6 +99,7 @@ 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 util.typestate_ann.intersect; import middle.ty; import middle.ty.ann_to_type; @@ -494,6 +499,48 @@ fn expr_pp(&expr e) -> pre_and_post { } } +/* fails if b has no annotation */ +/* FIXME: factor out code in the following two functions (block_ts_ann) */ +fn block_pp(&block b) -> pre_and_post { + alt (b.node.a) { + case (ann_none) { + log "block_pp: the impossible happened (no ann)"; + fail; + } + case (ann_type(_,_,?t)) { + alt (t) { + case (none[@ts_ann]) { + log "block_pp: the impossible happened (no ty)"; + fail; + } + case (some[@ts_ann](?ts)) { + ret ts.conditions; + } + } + } + } +} + +fn block_states(&block b) -> pre_and_post_state { + alt (b.node.a) { + case (ann_none) { + log "block_pp: the impossible happened (no ann)"; + fail; + } + case (ann_type(_,_,?t)) { + alt (t) { + case (none[@ts_ann]) { + log "block_states: the impossible happened (no ty)"; + fail; + } + case (some[@ts_ann](?ts)) { + ret ts.states; + } + } + } + } +} + fn stmt_states(&stmt s, uint nv) -> pre_and_post_state { alt (stmt_to_ann(s)) { case (none[@ts_ann]) { @@ -545,6 +592,14 @@ fn stmt_poststate(&stmt s, uint nv) -> poststate { ret (stmt_states(s, nv)).poststate; } +fn block_postcond(&block b) -> postcond { + ret (block_pp(b)).postcondition; +} + +fn block_poststate(&block b) -> poststate { + ret (block_states(b)).poststate; +} + /* returns a new annotation where the pre_and_post is p */ fn with_pp(ann a, pre_and_post p) -> ann { alt (a) { @@ -581,6 +636,8 @@ fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond { ret (first.precondition); } +/* works on either postconds or preconds + should probably rethink the whole type synonym situation */ fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond { auto sz = _vec.len[postcond](rest); @@ -599,6 +656,26 @@ fn union_postconds(&vec[postcond] pcs) -> postcond { ret union_postconds_go(bitv.clone(pcs.(0)), pcs); } +/* 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 { + check (len[postcond](pcs) > 0u); + + ret intersect_postconds_go(bitv.clone(pcs.(0)), pcs); +} + /******* AST-traversing code ********/ fn find_pre_post_mod(&_mod m) -> _mod { @@ -616,7 +693,7 @@ fn find_pre_post_obj(_obj o) -> _obj { 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)) { - find_pre_post_expr(enclosing, *e); + find_pre_post_expr(fm, enclosing, *e); } case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) { check (fm.contains_key(di)); @@ -641,167 +718,230 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () { } /* 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 find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () { + auto num_local_vars = num_locals(enclosing); - 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); - } + fn do_rand_(_fn_info_map fm, fn_info enclosing, &@expr e) -> () { + find_pre_post_expr(fm, enclosing, *e); + } + fn pp_one(&@expr e) -> pre_and_post { + be expr_pp(*e); + } - alt(e.node) { - case(expr_call(?operator, ?operands, ?a)) { - find_pre_post_expr(enclosing, *operator); + alt(e.node) { + case(expr_call(?operator, ?operands, ?a)) { + find_pre_post_expr(fm, enclosing, *operator); - auto do_rand = bind do_rand_(enclosing,_); - auto f = do_rand; - _vec.map[@expr, ()](f, operands); + 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); + 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; - } - case(expr_path(?p, ?maybe_def, ?a)) { - auto df; - alt (maybe_def) { - case (none[def]) - { log("expr_path should have a def"); fail; } - case (some[def](?d)) { df = d; } - } - - auto res = empty_pre_post(num_local_vars); - - alt (df) { - case (def_local(?d_id)) { - auto i = bit_num(d_id, enclosing); - require_and_preserve(i, res); + let pre_and_post pp = + rec(precondition=seq_preconds(num_local_vars, pps), + postcondition=res_postcond); + set_pre_and_post(a, pp); + ret; } - case (_) { /* nothing to check */ } - } + case(expr_path(?p, ?maybe_def, ?a)) { + auto df; + alt (maybe_def) { + case (none[def]) + { log("expr_path should have a def"); fail; } + case (some[def](?d)) { df = d; } + } - // Otherwise, variable is global, so it must be initialized - set_pre_and_post(a, res); - } - case(expr_log(?arg, ?a)) { - find_pre_post_expr(enclosing, *arg); - set_pre_and_post(a, expr_pp(*arg)); - } - case (expr_block(?b, ?a)) { - log("block!"); - fail; - } - 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); + auto res = empty_pre_post(num_local_vars); + + alt (df) { + case (def_local(?d_id)) { + auto i = bit_num(d_id, enclosing); + require_and_preserve(i, res); + } + case (_) { /* nothing to check */ } } - case (some[@expr](?base_exp)) { - find_pre_post_expr(enclosing, *base_exp); + + // Otherwise, variable is global, so it must be initialized + set_pre_and_post(a, res); + } + case(expr_log(?arg, ?a)) { + find_pre_post_expr(fm, enclosing, *arg); + set_pre_and_post(a, expr_pp(*arg)); + } + case (expr_block(?b, ?a)) { + find_pre_post_block(fm, enclosing, b); + 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); + 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; } - 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_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)); + + 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(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 (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))))); + } + case (_) { + log("find_pre_post_for_expr: non-lval on lhs of assign"); + fail; + } } - 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 (expr_ret(?maybe_val, ?a)) { + alt (maybe_val) { + case (none[@expr]) { + set_pre_and_post(a, empty_pre_post(num_local_vars)); + } + case (some[@expr](?ret_val)) { + find_pre_post_expr(fm, enclosing, *ret_val); + let pre_and_post pp = + rec(precondition=expr_precond(*ret_val), + postcondition=empty_poststate(num_local_vars)); + set_pre_and_post(a, pp); + } } } + case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { + find_pre_post_expr(fm, enclosing, *antec); + find_pre_post_block(fm, enclosing, conseq); + alt (maybe_alt) { + case (none[@expr]) { + auto precond_res = seq_preconds(num_local_vars, + vec(expr_pp(*antec), + block_pp(conseq))); + set_pre_and_post(a, rec(precondition=precond_res, + postcondition= + expr_poststate(*antec))); + } + case (some[@expr](?altern)) { + find_pre_post_expr(fm, enclosing, *altern); + auto precond_true_case = + seq_preconds(num_local_vars, + vec(expr_pp(*antec), block_pp(conseq))); + auto postcond_true_case = union_postconds + (vec(expr_postcond(*antec), block_postcond(conseq))); + auto precond_false_case = seq_preconds + (num_local_vars, + vec(expr_pp(*antec), expr_pp(*altern))); + auto postcond_false_case = union_postconds + (vec(expr_postcond(*antec), expr_postcond(*altern))); + auto precond_res = union_postconds(vec(precond_true_case, + precond_false_case)); + auto postcond_res = intersect_postconds + (vec(postcond_true_case, postcond_false_case)); + set_pre_and_post(a, rec(precondition=precond_res, + postcondition=postcond_res)); + } + } + } + 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))))); + } + case(_) { + log("this sort of expr isn't implemented!"); + 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!"); - fail; - } - } } impure fn gen(&fn_info enclosing, &ann a, def_id id) -> bool { @@ -827,7 +967,7 @@ fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s) case(ast.decl_local(?alocal)) { alt(alocal.init) { case(some[ast.initializer](?an_init)) { - find_pre_post_expr(enclosing, *an_init.expr); + find_pre_post_expr(fm, enclosing, *an_init.expr); auto rhs_pp = expr_pp(*an_init.expr); set_pre_and_post(alocal.ann, rhs_pp); @@ -851,7 +991,7 @@ fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s) } } case(stmt_expr(?e,?a)) { - find_pre_post_expr(enclosing, *e); + find_pre_post_expr(fm, enclosing, *e); set_pre_and_post(a, expr_pp(*e)); } } @@ -865,11 +1005,12 @@ fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b) 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); + fn do_inner_(_fn_info_map fm, fn_info i, &@expr e) -> () { + find_pre_post_expr(fm, i, *e); } - auto do_inner = bind do_inner_(enclosing, _); + auto do_inner = bind do_inner_(fm, enclosing, _); option.map[@expr, ()](do_inner, b.node.expr); + /* FIXME needs to set up the ann for b!!!!!!!!!!! */ } fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> () { @@ -993,8 +1134,7 @@ impure fn pure_exp(&ann a, &prestate p) -> bool { 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 */ + auto num_local_vars = num_locals(enclosing); alt (e.node) { case (expr_vec(?elts, _, ?a)) { @@ -1025,8 +1165,11 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing, ret pure_exp(a, pres); } case (expr_block(?b,?a)) { - log("find_pre_post_state_expr: block!"); - fail; + changed = find_pre_post_state_block(fm, enclosing, pres, b) + || changed; + changed = extend_prestate_ann(a, pres) || changed; + changed = extend_poststate_ann(a, block_poststate(b)) || changed; + ret changed; } case (expr_rec(?fields,?maybe_base,?a)) { changed = find_pre_post_state_exprs(fm, enclosing, pres, a, @@ -1067,6 +1210,49 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing, } ret changed; } + case (expr_ret(?maybe_ret_val, ?a)) { + changed = extend_prestate_ann(a, pres) || changed; + set_poststate_ann(a, empty_poststate(num_local_vars)); + alt(maybe_ret_val) { + case (none[@expr]) { /* do nothing */ } + case (some[@expr](?ret_val)) { + changed = find_pre_post_state_expr(fm, enclosing, + pres, ret_val) || changed; + } + } + ret changed; + } + case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { + changed = extend_prestate_ann(a, pres) || changed; + changed = find_pre_post_state_expr(fm, enclosing, pres, antec) + || changed; + changed = find_pre_post_state_block(fm, enclosing, + expr_poststate(*antec), conseq) || changed; + alt (maybe_alt) { + case (none[@expr]) { + changed = extend_poststate_ann(a, expr_poststate(*antec)) + || changed; + } + case (some[@expr](?altern)) { + changed = find_pre_post_state_expr(fm, enclosing, + expr_poststate(*antec), altern) || changed; + auto poststate_res = intersect_postconds + (vec(block_poststate(conseq), expr_poststate(*altern))); + changed = extend_poststate_ann(a, poststate_res) || changed; + } + } + ret changed; + } + case (expr_binary(?bop, ?l, ?r, ?a)) { + /* FIXME: what if bop is lazy? */ + changed = extend_prestate_ann(a, pres) || changed; + changed = find_pre_post_state_expr(fm, enclosing, pres, l) + || changed; + changed = find_pre_post_state_expr(fm, + enclosing, expr_poststate(*l), r) || changed; + changed = extend_poststate_ann(a, expr_poststate(*r)) || changed; + ret changed; + } case (_) { log("find_pre_post_state_expr: implement this case!"); fail; @@ -1157,14 +1343,15 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing, /* Updates the pre- and post-states of statements in the block, returns a boolean flag saying whether any pre- or poststates changed */ -fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, block b) +fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, + &prestate pres0, block b) -> bool { auto changed = false; auto num_local_vars = num_locals(enclosing); /* First, set the pre-states and post-states for every expression */ - auto pres = empty_prestate(num_local_vars); + auto pres = pres0; /* Iterate over each stmt. The new prestate is . The poststate consist of improving with whatever variables this stmt initializes. @@ -1185,7 +1372,9 @@ 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 { - ret find_pre_post_state_block(f_info, fi, f.body); + auto num_local_vars = num_locals(fi); + ret find_pre_post_state_block(f_info, fi, + empty_prestate(num_local_vars), f.body); } fn fixed_point_states(_fn_info_map fm, fn_info f_info, diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs index 0218df1c570c6..9ccb87318f3d5 100644 --- a/src/comp/util/typestate_ann.rs +++ b/src/comp/util/typestate_ann.rs @@ -75,6 +75,10 @@ fn union(&precond p1, &precond p2) -> bool { be bitv.union(p1, p2); } +fn intersect(&precond p1, &precond p2) -> bool { + be bitv.intersect(p1, p2); +} + fn pps_len(&pre_and_post p) -> uint { // gratuitous check check (p.precondition.nbits == p.postcondition.nbits);