diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/comp/middle/typeck.rs | 39 | ||||
| -rw-r--r-- | src/comp/middle/typestate_check.rs | 518 | ||||
| -rw-r--r-- | src/comp/rustc.rc | 2 | ||||
| -rw-r--r-- | src/comp/util/typestate_ann.rs | 29 |
4 files changed, 508 insertions, 80 deletions
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index e105c7a9..ab0262f1 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -23,6 +23,7 @@ import middle.ty.ty_to_str; import middle.ty.type_is_integral; import middle.ty.type_is_scalar; import middle.ty.ty_params_opt_and_ty; +import middle.ty.ty_nil; import std._str; import std._uint; @@ -62,6 +63,12 @@ fn triv_ann(@ty.t t) -> ann { ret ast.ann_type(t, none[vec[@ty.t]], none[@ts_ann]); } +// Used to fill in the annotation for things that have uninteresting +// types +fn boring_ann() -> ann { + ret triv_ann(plain_ty(ty_nil)); +} + // Replaces parameter types inside a type with type variables. fn generalize_ty(@crate_ctxt cx, @ty.t t) -> @ty.t { state obj ty_generalizer(@crate_ctxt cx, @@ -1361,7 +1368,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, ann_to_type(ann), adk); e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(t)); } - /* FIXME: this should probably check the type annotations */ + /* FIXME: should this check the type annotations? */ case (ast.expr_fail(_)) { e_1 = e.node; } case (ast.expr_log(_,_)) { e_1 = e.node; } case (ast.expr_break(_)) { e_1 = e.node; } @@ -1771,16 +1778,19 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { ann)); } - case (ast.expr_fail(_)) { // ??? ignoring ann - ret expr; + case (ast.expr_fail(_)) { + ret @fold.respan[ast.expr_](expr.span, + ast.expr_fail(boring_ann())); } case (ast.expr_break(_)) { - ret expr; + ret @fold.respan[ast.expr_](expr.span, + ast.expr_break(boring_ann())); } case (ast.expr_cont(_)) { - ret expr; + ret @fold.respan[ast.expr_](expr.span, + ast.expr_cont(boring_ann())); } case (ast.expr_ret(?expr_opt, _)) { @@ -1792,14 +1802,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { + "returning non-nil"); } - ret expr; + ret @fold.respan[ast.expr_] + (expr.span, + ast.expr_ret(none[@ast.expr], boring_ann())); } case (some[@ast.expr](?e)) { auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); ret @fold.respan[ast.expr_] - (expr.span, ast.expr_ret(some(expr_1), ann_none)); + (expr.span, ast.expr_ret(some(expr_1), boring_ann())); } } } @@ -1813,14 +1825,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { + "putting non-nil"); } - ret expr; + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_put(none[@ast.expr], + boring_ann())); } case (some[@ast.expr](?e)) { auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); ret @fold.respan[ast.expr_] - (expr.span, ast.expr_put(some(expr_1), ann_none)); + (expr.span, ast.expr_put(some(expr_1), boring_ann())); } } } @@ -1831,20 +1845,21 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); ret @fold.respan[ast.expr_](expr.span, - ast.expr_be(expr_1, ann_none)); + ast.expr_be(expr_1, + boring_ann())); } case (ast.expr_log(?e,_)) { auto expr_t = check_expr(fcx, e); ret @fold.respan[ast.expr_] - (expr.span, ast.expr_log(expr_t, ann_none)); + (expr.span, ast.expr_log(expr_t, boring_ann())); } case (ast.expr_check_expr(?e, _)) { auto expr_t = check_expr(fcx, e); demand(fcx, expr.span, plain_ty(ty.ty_bool), expr_ty(expr_t)); ret @fold.respan[ast.expr_] - (expr.span, ast.expr_check_expr(expr_t, ann_none)); + (expr.span, ast.expr_check_expr(expr_t, boring_ann())); } case (ast.expr_assign(?lhs, ?rhs, _)) { diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs index 361d70ae..295c4f1b 100644 --- a/src/comp/middle/typestate_check.rs +++ b/src/comp/middle/typestate_check.rs @@ -20,6 +20,8 @@ import front.ast.expr; import front.ast.expr_call; import front.ast.expr_path; import front.ast.expr_log; +import front.ast.expr_block; +import front.ast.expr_lit; import front.ast.path; import front.ast.crate_directive; import front.ast.fn_decl; @@ -42,6 +44,12 @@ import front.ast.ann_none; import front.ast.ann_type; import front.ast._obj; import front.ast._mod; +import front.ast.crate; +import front.ast.module; +import front.ast.mod_index_entry; +import front.ast.mie_item; +import front.ast.item_fn; +import front.ast.def_local; import middle.fold; import middle.fold.respan; @@ -50,6 +58,7 @@ import util.common; import util.common.span; import util.common.spanned; import util.common.new_str_hash; +import util.common.new_def_hash; import util.typestate_ann; import util.typestate_ann.ts_ann; import util.typestate_ann.empty_pre_post; @@ -57,9 +66,14 @@ import util.typestate_ann.true_precond; import util.typestate_ann.true_postcond; import util.typestate_ann.postcond; import util.typestate_ann.precond; +import util.typestate_ann.poststate; +import util.typestate_ann.prestate; import util.typestate_ann.pre_and_post; import util.typestate_ann.get_pre; import util.typestate_ann.get_post; +import util.typestate_ann.implies; +import util.typestate_ann.pre_and_post_state; +import util.typestate_ann.empty_states; import middle.ty; import middle.ty.ann_to_type; @@ -91,6 +105,8 @@ import std.list.cons; import std.list.nil; import std.list.foldl; import std.list.find; +import std._uint; +import std.bitv; import util.typestate_ann; import util.typestate_ann.difference; @@ -98,21 +114,134 @@ import util.typestate_ann.union; import util.typestate_ann.pps_len; import util.typestate_ann.require_and_preserve; -/**********************************************************************/ -/* mapping from variable name to bit number */ -type fn_info = std.map.hashmap[ident, uint]; +/**** 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_cond(vec[uint] v) -> () { + auto res = ""; + for (uint i in v) { + if (i == 0u) { + res += "0"; + } + else { + res += "1"; + } + } + log(res); +} +fn log_pp(&pre_and_post pp) -> () { + auto p1 = bitv.to_vec(pp.precondition); + auto p2 = bitv.to_vec(pp.postcondition); + log("pre:"); + log_cond(p1); + log("post:"); + log_cond(p2); +} -fn bit_num(ident v, fn_info m) -> uint { +fn print_ident(&ident i) -> () { + log(" " + i + " "); +} + +fn print_idents(vec[ident] idents) -> () { + if(len[ident](idents) == 0u) { + ret; + } + else { + log("an ident: " + pop[ident](idents)); + print_idents(idents); + } +} +/**********************************************************************/ +/* mapping from variable name (def_id is assumed to be for a local + variable in a given function) to bit number */ +type fn_info = std.map.hashmap[def_id, uint]; +/* mapping from function name to fn_info map */ +type _fn_info_map = std.map.hashmap[def_id, fn_info]; + +fn bit_num(def_id v, fn_info m) -> uint { + check (m.contains_key(v)); ret m.get(v); } + +fn var_is_local(def_id v, fn_info m) -> bool { + ret (m.contains_key(v)); +} + fn num_locals(fn_info m) -> uint { ret m.size(); } +fn find_locals(_fn f) -> vec[def_id] { + auto res = _vec.alloc[def_id](0u); + + for each (@tup(ident, block_index_entry) p + in f.body.node.index.items()) { + alt (p._1) { + case (ast.bie_local(?loc)) { + res += vec(loc.id); + } + case (_) { } + } + } + + ret res; +} + +fn add_var(def_id v, uint next, fn_info tbl) -> uint { + tbl.insert(v, next); + // log(v + " |-> " + _uint.to_str(next, 10u)); + ret (next + 1u); +} + +/* builds a table mapping each local var defined in f + to a bit number in the precondition/postcondition vectors */ fn mk_fn_info(_fn f) -> fn_info { - ret new_str_hash[uint](); /* FIXME: actually implement this */ + auto res = new_def_hash[uint](); + let uint next = 0u; + let vec[ast.arg] f_args = f.decl.inputs; + + for (ast.arg v in f_args) { + next = add_var(v.id, next, res); + } + + let vec[def_id] locals = find_locals(f); + for (def_id v in locals) { + next = add_var(v, next, res); + } + + ret res; } -/**********************************************************************/ + +/* extends mk_fn_info to an item, side-effecting the map fi from + function IDs to fn_info maps */ +fn mk_fn_info_item_fn(&_fn_info_map fi, &span sp, ident i, &ast._fn f, + vec[ast.ty_param] ty_params, def_id id, ann a) -> @item { + fi.insert(id, mk_fn_info(f)); + ret @respan(sp, item_fn(i, f, ty_params, id, a)); +} + +/* initializes the global fn_info_map (mapping each function ID, including + nested locally defined functions, onto a mapping from local variable name + to bit number) */ +fn mk_f_to_fn_info(@ast.crate c) -> _fn_info_map { + auto res = new_def_hash[fn_info](); + + auto fld = fold.new_identity_fold[_fn_info_map](); + fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_) with *fld); + fold.fold_crate[_fn_info_map](res, fld, c); + + ret res; +} +/**** Helpers ****/ fn expr_ann(&expr e) -> ann { alt(e.node) { case (ast.expr_vec(_,_,?a)) { @@ -214,8 +343,53 @@ fn expr_ann(&expr e) -> ann { } } -fn expr_pp(&@expr e) -> pre_and_post { - alt (expr_ann(*e)) { +/* returns ann_none if this is the sort + of statement where an ann doesn't make sense */ +fn stmt_ann(&stmt s) -> ann { + alt (s.node) { + case (stmt_decl(?d)) { + alt (d.node) { + case (decl_local(?l)) { + ret l.ann; + } + case (decl_item(?i)) { + ret ann_none; /* ????? */ + } + } + } + case (stmt_expr(?e)) { + ret expr_ann(*e); + } + case (_) { + ret ann_none; + } + } +} + +/* fails if e has no annotation */ +fn expr_pp(&expr e) -> pre_and_post { + alt (expr_ann(e)) { + case (ann_none) { + log "expr_pp: the impossible happened (no annotation)"; + fail; + } + case (ann_type(_, _, ?maybe_pp)) { + alt (maybe_pp) { + case (none[@ts_ann]) { + log "expr_pp: the impossible happened (no pre/post)"; + fail; + } + case (some[@ts_ann](?p)) { + ret p.conditions; + } + } + } + } +} + +/* fails if e has no annotation */ +fn expr_states(&expr e) -> pre_and_post_state { + alt (expr_ann(e)) { case (ann_none) { log "expr_pp: the impossible happened (no annotation)"; fail; @@ -227,7 +401,45 @@ fn expr_pp(&@expr e) -> pre_and_post { fail; } case (some[@ts_ann](?p)) { - ret *p; + ret p.states; + } + } + } + } +} + +/* fails if no annotation */ +fn stmt_pp(&stmt s) -> pre_and_post { + alt (stmt_ann(s)) { + case (ann_none) { + fail; + } + case (ann_type(_, _, ?maybe_pp)) { + alt (maybe_pp) { + case (none[@ts_ann]) { + fail; + } + case (some[@ts_ann](?p)) { + ret p.conditions; + } + } + } + } +} + +/* fails if no annotation */ +fn stmt_states(&stmt s) -> pre_and_post_state { + alt (stmt_ann(s)) { + case (ann_none) { + fail; + } + case (ann_type(_, _, ?maybe_pp)) { + alt (maybe_pp) { + case (none[@ts_ann]) { + fail; + } + case (some[@ts_ann](?p)) { + ret p.states; } } } @@ -235,21 +447,49 @@ fn expr_pp(&@expr e) -> pre_and_post { } fn expr_precond(&expr e) -> precond { - ret (expr_pp(@e)).precondition; + ret (expr_pp(e)).precondition; } -fn expr_postcond(&@expr e) -> postcond { +fn expr_postcond(&expr e) -> postcond { ret (expr_pp(e)).postcondition; } -fn with_pp(ann a, @pre_and_post p) -> ann { +fn expr_prestate(&expr e) -> prestate { + ret (expr_states(e)).prestate; +} + +fn expr_poststate(&expr e) -> poststate { + ret (expr_states(e)).poststate; +} + +fn stmt_precond(&stmt s) -> precond { + ret (stmt_pp(s)).precondition; +} + +fn stmt_postcond(&stmt s) -> postcond { + ret (stmt_pp(s)).postcondition; +} + +fn stmt_prestate(&stmt s) -> prestate { + ret (stmt_states(s)).prestate; +} + +fn stmt_poststate(&stmt s) -> poststate { + ret (stmt_states(s)).poststate; +} + +/* returns a new annotation where the pre_and_post is p */ +fn with_pp(ann a, pre_and_post p) -> ann { alt (a) { case (ann_none) { log("with_pp: the impossible happened"); fail; /* shouldn't happen b/c code is typechecked */ } case (ann_type(?t, ?ps, _)) { - ret (ann_type(t, ps, some[@ts_ann](p))); + ret (ann_type(t, ps, + some[@ts_ann] + (@rec(conditions=p, + states=empty_states(pps_len(p)))))); } } } @@ -276,9 +516,14 @@ fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond { } fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond { - auto other = rest.(0); - union(first, other); - union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest))); + auto sz = _vec.len[postcond](rest); + + if (sz > 0u) { + auto other = rest.(0); + union(first, other); + union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest))); + } + ret first; } @@ -288,19 +533,7 @@ fn union_postconds(&vec[postcond] pcs) -> postcond { be union_postconds_go(pcs.(0), pcs); } -fn print_ident(&ident i) -> () { - log(" " + i + " "); -} - -fn print_idents(vec[ident] idents) -> () { - if(len[ident](idents) == 0u) { - ret; - } - else { - log("an ident: " + pop[ident](idents)); - print_idents(idents); - } -} +/******* AST-traversing code ********/ fn find_pre_post_mod(&_mod m) -> _mod { ret m; /* FIXME */ @@ -314,26 +547,29 @@ fn find_pre_post_obj(_obj o) -> _obj { ret o; /* FIXME */ } -impure fn find_pre_post_item(fn_info enclosing, &item i) -> item { +fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> item { 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, - with_pp(a, @expr_pp(e_pp))))); + ast.item_const(id, t, e_pp, di, a))); } case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) { - auto f_pp = find_pre_post_fn(f); + 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))); } 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))); } 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))); } @@ -345,17 +581,23 @@ impure fn find_pre_post_item(fn_info enclosing, &item i) -> item { } 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))); } } } -impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr { +fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr { auto num_local_vars = num_locals(enclosing); fn do_rand_(fn_info enclosing, &@expr e) -> @expr { - be find_pre_post_expr(enclosing, *e); + log("for rand " ); + log_expr(e); + log("pp = "); + auto res = find_pre_post_expr(enclosing, *e); + log_pp(expr_pp(*res)); + ret res; } auto do_rand = bind do_rand_(enclosing,_); @@ -363,40 +605,78 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr { 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)); auto f = do_rand; auto pp_rands = _vec.map[@expr, @expr](f, rands); - auto g = expr_pp; - auto pps = _vec.map[@expr, pre_and_post] - (g, pp_rands); - _vec.push[pre_and_post](pps, expr_pp(pp_oper)); + 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 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), + 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))); } case(expr_path(?p, ?maybe_def, ?a)) { - check (len[ident](p.node.idents) > 0u); - auto referent = p.node.idents.(0); - auto i = bit_num(referent, enclosing); + 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); - require_and_preserve(i, *res); + + alt (df) { + case (def_local(?d_id)) { + auto i = bit_num(d_id, enclosing); + require_and_preserve(i, res); + } + case (_) { /* nothing to check */ } + } + + // 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)))); } - case(expr_log(?e, ?a)) { - auto e_pp = find_pre_post_expr(enclosing, *e); + 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))))); + expr_log(e_pp, with_pp(a, expr_pp(*e_pp))))); + } + 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(_) { log("this sort of expr isn't implemented!"); @@ -405,8 +685,8 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr { } } -impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s) - -> ast.stmt { +fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing, + &ast.stmt s) -> ast.stmt { auto num_local_vars = num_locals(enclosing); alt(s.node) { @@ -418,7 +698,7 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s) 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 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), @@ -443,24 +723,26 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s) } } case(decl_item(?anitem)) { - auto res_item = find_pre_post_item(enclosing, *anitem); + auto res_item = find_pre_post_item(fm, enclosing, *anitem); ret (respan(s.span, stmt_decl(@respan(adecl.span, decl_item(@res_item))))); } } } case(stmt_expr(?e)) { + log_expr(e); let @expr e_pp = find_pre_post_expr(enclosing, *e); ret (respan(s.span, stmt_expr(e_pp))); } } } -fn find_pre_post_block(fn_info enclosing, block b) -> block { - fn do_one_(fn_info i, &@stmt s) -> @stmt { - ret (@find_pre_post_for_each_stmt(i, *s)); +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_for_each_stmt(fm, i, *s)); } - auto do_one = bind do_one_(enclosing, _); + 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 { @@ -472,24 +754,134 @@ fn find_pre_post_block(fn_info enclosing, block b) -> block { ret respan(b.span, b_res); } -fn find_pre_post_fn(&_fn f) -> _fn { - let fn_info fi = mk_fn_info(f); +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(fi, f.body)); + body=find_pre_post_block(fm, fi, f.body)); } -fn check_item_fn(&@() ignore, &span sp, ident i, &ast._fn f, +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 { - auto res_f = find_pre_post_fn(f); + check (fm.contains_key(id)); + auto res_f = find_pre_post_fn(fm, fm.get(id), f); ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a)); } +/* Returns a pair of a new function, with possibly a changed pre- or + post-state, and a boolean flag saying whether the function's pre- or + poststate changed */ +fn find_pre_post_state_fn(fn_info f_info, &ast._fn f) -> tup(bool, ast._fn) { + log ("Implement find_pre_post_state_fn!"); + fail; +} + +fn fixed_point_states(fn_info f_info, + fn (fn_info, &ast._fn) -> tup(bool, ast._fn) f, + &ast._fn start) -> ast._fn { + auto next = f(f_info, start); + + if (next._0) { + // something changed + be fixed_point_states(f_info, f, next._1); + } + else { + // we're done! + ret next._1; + } +} + +fn check_states_expr(fn_info enclosing, &expr e) -> () { + let precond prec = expr_precond(e); + let postcond postc = expr_postcond(e); + let prestate pres = expr_prestate(e); + let poststate posts = expr_poststate(e); + + if (!implies(pres, prec)) { + log("check_states_expr: unsatisfied precondition"); + fail; + } + if (!implies(posts, postc)) { + log("check_states_expr: unsatisfied postcondition"); + fail; + } +} + +fn check_states_stmt(fn_info enclosing, &stmt s) -> () { + alt (stmt_ann(s)) { + case (ann_none) { + // Statement doesn't require an annotation -- do nothing + ret; + } + case (ann_type(_,_,?m_pp)) { + let precond prec = stmt_precond(s); + let postcond postc = stmt_postcond(s); + let prestate pres = stmt_prestate(s); + let poststate posts = stmt_poststate(s); + + if (!implies(pres, prec)) { + log("check_states_stmt: unsatisfied precondition"); + fail; + } + if (!implies(posts, postc)) { + log("check_states_stmt: unsatisfied postcondition"); + fail; + } + } + } +} + +fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () { + fn do_one_(fn_info i, &@stmt s) -> () { + check_states_stmt(i, *s); + } + auto do_one = bind do_one_(enclosing, _); + + _vec.map[@stmt, ()](do_one, f.body.node.stmts); + fn do_inner_(fn_info i, &@expr e) -> () { + check_states_expr(i, *e); + } + auto do_inner = bind do_inner_(enclosing, _); + option.map[@expr, ()](do_inner, f.body.node.expr); + +} + +fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i, + &ast._fn f, vec[ast.ty_param] ty_params, def_id id, + ann a) -> @item { + + /* Look up the var-to-bit-num map for this function */ + check(f_info_map.contains_key(id)); + auto f_info = f_info_map.get(id); + + /* Compute the pre- and post-states for this function */ + auto g = find_pre_post_state_fn; + auto res_f = fixed_point_states(f_info, g, f); + + /* Now compare each expr's pre-state to its precondition + and post-state to its postcondition */ + check_states_against_conditions(f_info, res_f); + + /* Rebuild the same function */ + ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a)); +} + fn check_crate(@ast.crate crate) -> @ast.crate { - auto fld = fold.new_identity_fold[@()](); + /* Build the global map from function id to var-to-bit-num-map */ + auto fn_info_map = mk_f_to_fn_info(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); + + auto fld1 = fold.new_identity_fold[_fn_info_map](); + + fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_) + with *fld1); - ret fold.fold_crate[@()](@(), fld, crate); + ret fold.fold_crate[_fn_info_map](fn_info_map, fld1, + with_pre_postconditions); } diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc index 952ea7e8..47a37f33 100644 --- a/src/comp/rustc.rc +++ b/src/comp/rustc.rc @@ -62,6 +62,8 @@ auth middle.typestate_check.log_expr = impure; auth lib.llvm = unsafe; auth pretty.pprust = impure; auth middle.typestate_check.find_pre_post_block = impure; +auth middle.typestate_check.find_pre_post_expr = impure; +auth util.typestate_ann.implies = impure; mod lib { alt (target_os) { diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs index a4698c5d..071f5513 100644 --- a/src/comp/util/typestate_ann.rs +++ b/src/comp/util/typestate_ann.rs @@ -12,12 +12,21 @@ type precond = bitv.t; /* 1 means "this variable must be initialized" type postcond = bitv.t; /* 1 means "this variable is initialized" 0 means "don't know about this variable */ +type prestate = bitv.t; /* 1 means "this variable is definitely initialized" + 0 means "don't know whether this variable is + initialized" */ +type poststate = bitv.t; /* 1 means "this variable is definitely initialized" + 0 means "don't know whether this variable is + initialized" */ + /* named thus so as not to confuse with prestate and poststate */ type pre_and_post = rec(precond precondition, postcond postcondition); /* FIXME: once it's implemented: */ // : ((*.precondition).nbits == (*.postcondition).nbits); -type ts_ann = pre_and_post; +type pre_and_post_state = rec(prestate prestate, poststate poststate); + +type ts_ann = rec(pre_and_post conditions, pre_and_post_state states); fn true_precond(uint num_vars) -> precond { be bitv.create(num_vars, false); @@ -27,11 +36,16 @@ fn true_postcond(uint num_vars) -> postcond { be true_precond(num_vars); } -fn empty_pre_post(uint num_vars) -> @pre_and_post { - ret(@rec(precondition=true_precond(num_vars), +fn empty_pre_post(uint num_vars) -> pre_and_post { + ret(rec(precondition=true_precond(num_vars), postcondition=true_postcond(num_vars))); } +fn empty_states(uint num_vars) -> pre_and_post_state { + ret(rec(prestate=true_precond(num_vars), + poststate=true_postcond(num_vars))); +} + fn get_pre(&pre_and_post p) -> precond { ret p.precondition; } @@ -57,5 +71,10 @@ fn pps_len(&pre_and_post p) -> uint { impure fn require_and_preserve(uint i, &pre_and_post p) -> () { // sets the ith bit in p's pre and post bitv.set(p.precondition, i, true); - bitv.set(p.postcondition, i, false); -}
\ No newline at end of file + bitv.set(p.postcondition, i, true); +} + +fn implies(bitv.t a, bitv.t b) -> bool { + bitv.difference(b, a); + ret (bitv.equal(b, bitv.create(b.nbits, false))); +} |