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

More work on typestate. Sketched out code for computing and checking prestates and poststates. Still a long ways away.

Browse Source
This commit is contained in:
Tim Chevalier 2011-04-04 14:31:49 -07:00 committed by Graydon Hoare
parent 4fc8de1969
commit 86d4601827
4 changed files with 513 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
src/comp/middle/typeck.rs
View File

@ -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, _)) {

528
src/comp/middle/typestate_check.rs
View File

@ -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);
fn bit_num(ident v, fn_info m) -> uint {
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 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 mk_fn_info(_fn f) -> fn_info {
ret new_str_hash[uint](); /* FIXME: actually implement this */
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 {
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,32 @@ 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;
@ -227,7 +380,66 @@ fn expr_pp(&@expr e) -> pre_and_post {
fail;
}
case (some[@ts_ann](?p)) {
ret *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;
}
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.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));
}
fn check_crate(@ast.crate crate) -> @ast.crate {
auto fld = fold.new_identity_fold[@()]();
fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
ret fold.fold_crate[@()](@(), fld, crate);
/* 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 {
/* 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[_fn_info_map](fn_info_map, fld1,
with_pre_postconditions);
}

2
src/comp/rustc.rc
View File

@ -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) {

29
src/comp/util/typestate_ann.rs
View File

@ -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);
}
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)));
}