Modify the fn vistors in walk so that they can handle functions without names. Update the typestate code to understand this.
This commit is contained in:
parent
142ff011da
commit
f3717da1b1
@ -8,6 +8,8 @@ import util::common::ty_mach;
|
||||
import util::common::filename;
|
||||
|
||||
type ident = str;
|
||||
// Functions may or may not have names.
|
||||
type fn_ident = option::t[ident];
|
||||
|
||||
type path_ = rec(vec[ident] idents, vec[@ty] types);
|
||||
|
||||
|
@ -51,7 +51,7 @@ fn collect_ids_local(&@local l, @mutable vec[node_id] rs) {
|
||||
vec::push(*rs, l.node.id);
|
||||
}
|
||||
|
||||
fn node_ids_in_fn(&_fn f, &span sp, &ident i, node_id id,
|
||||
fn node_ids_in_fn(&_fn f, &span sp, &fn_ident i, node_id id,
|
||||
@mutable vec[node_id] rs) {
|
||||
auto collect_ids = walk::default_visitor();
|
||||
collect_ids =
|
||||
@ -69,15 +69,16 @@ fn init_vecs(&crate_ctxt ccx, &vec[node_id] node_ids, uint len) {
|
||||
}
|
||||
}
|
||||
|
||||
fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f, &span sp, &ident i,
|
||||
node_id id) {
|
||||
fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f, &span sp,
|
||||
&fn_ident i, node_id id) {
|
||||
let @mutable vec[node_id] node_ids = @mutable [];
|
||||
node_ids_in_fn(f, sp, i, id, node_ids);
|
||||
auto node_id_vec = *node_ids;
|
||||
init_vecs(ccx, node_id_vec, num_constraints);
|
||||
}
|
||||
|
||||
fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &ident i, node_id id) {
|
||||
fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &fn_ident i,
|
||||
node_id id) {
|
||||
auto f_info = get_fn_info(ccx, id);
|
||||
visit_fn(ccx, num_constraints(f_info), f, sp, i, id);
|
||||
}
|
||||
|
@ -8,6 +8,7 @@ import front::ast::obj_field;
|
||||
import front::ast::_obj;
|
||||
import front::ast::stmt;
|
||||
import front::ast::ident;
|
||||
import front::ast::fn_ident;
|
||||
import front::ast::node_id;
|
||||
import front::ast::def_id;
|
||||
import front::ast::local_def;
|
||||
@ -120,7 +121,7 @@ fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
|
||||
}
|
||||
|
||||
fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, node_id id,
|
||||
&span sp, &ident i) {
|
||||
&span sp, &fn_ident i) {
|
||||
/* Postorder traversal instead of pre is important
|
||||
because we want the smallest possible erroneous statement
|
||||
or expression. */
|
||||
@ -172,7 +173,7 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, node_id id,
|
||||
}
|
||||
}
|
||||
|
||||
fn check_fn_states(&fn_ctxt fcx, &_fn f, node_id id, &span sp, &ident i) {
|
||||
fn check_fn_states(&fn_ctxt fcx, &_fn f, node_id id, &span sp, &fn_ident i) {
|
||||
/* Compute the pre- and post-states for this function */
|
||||
|
||||
auto g = find_pre_post_state_fn;
|
||||
@ -183,12 +184,13 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, node_id id, &span sp, &ident i) {
|
||||
check_states_against_conditions(fcx, f, id, sp, i);
|
||||
}
|
||||
|
||||
fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i, node_id id) {
|
||||
fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &fn_ident i, node_id id) {
|
||||
/* Look up the var-to-bit-num map for this function */
|
||||
|
||||
assert (ccx.fm.contains_key(id));
|
||||
auto f_info = ccx.fm.get(id);
|
||||
auto fcx = rec(enclosing=f_info, id=id, name=i, ccx=ccx);
|
||||
auto name = option::from_maybe("anon", i);
|
||||
auto fcx = rec(enclosing=f_info, id=id, name=name, ccx=ccx);
|
||||
check_fn_states(fcx, f, id, sp, i);
|
||||
}
|
||||
|
||||
|
@ -3,6 +3,7 @@ import std::vec;
|
||||
import std::vec::plus_option;
|
||||
import front::ast;
|
||||
import front::ast::*;
|
||||
import pretty::ppaux::fn_ident_to_string;
|
||||
import std::option::*;
|
||||
import middle::walk::walk_crate;
|
||||
import middle::walk::walk_fn;
|
||||
@ -56,7 +57,7 @@ fn collect_pred(&ctxt cx, &@expr e) {
|
||||
}
|
||||
}
|
||||
|
||||
fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, node_id id)
|
||||
fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &fn_ident i, node_id id)
|
||||
-> ctxt {
|
||||
let ctxt cx = rec(cs=@mutable vec::alloc(0u), tcx=tcx);
|
||||
auto visitor = walk::default_visitor();
|
||||
@ -103,7 +104,7 @@ fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) ->
|
||||
|
||||
/* builds a table mapping each local var defined in f
|
||||
to a bit number in the precondition/postcondition vectors */
|
||||
fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &ident f_name,
|
||||
fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &fn_ident f_name,
|
||||
node_id id) {
|
||||
auto res_map = @new_int_hash[constraint]();
|
||||
let uint next = 0u;
|
||||
@ -121,14 +122,15 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, &ident f_name,
|
||||
/* add a pseudo-entry for the function's return value
|
||||
we can safely use the function's name itself for this purpose */
|
||||
|
||||
add_constraint(cx.tcx, respan(f_sp, rec(id=id, c=ninit(f_name))), next,
|
||||
auto name = fn_ident_to_string(id, f_name);
|
||||
add_constraint(cx.tcx, respan(f_sp, rec(id=id, c=ninit(name))), next,
|
||||
res_map);
|
||||
auto rslt =
|
||||
rec(constrs=res_map,
|
||||
num_constraints=vec::len(*cx.cs) + 1u,
|
||||
cf=f.decl.cf);
|
||||
ccx.fm.insert(id, rslt);
|
||||
log f_name + " has " + uistr(num_constraints(rslt)) + " constraints";
|
||||
log name + " has " + uistr(num_constraints(rslt)) + " constraints";
|
||||
}
|
||||
|
||||
|
||||
|
@ -78,6 +78,7 @@ import util::common::log_expr_err;
|
||||
import util::common::log_block_err;
|
||||
import util::common::log_block;
|
||||
import util::common::span;
|
||||
import pretty::ppaux::fn_ident_to_string;
|
||||
|
||||
fn find_pre_post_mod(&_mod m) -> _mod {
|
||||
log "implement find_pre_post_mod!";
|
||||
@ -686,10 +687,11 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) {
|
||||
}
|
||||
}
|
||||
|
||||
fn fn_pre_post(crate_ctxt ccx, &_fn f, &span sp, &ident i, node_id id) {
|
||||
fn fn_pre_post(crate_ctxt ccx, &_fn f, &span sp, &fn_ident i,
|
||||
node_id id) {
|
||||
assert (ccx.fm.contains_key(id));
|
||||
auto fcx = rec(enclosing=ccx.fm.get(id), id=id, name=i,
|
||||
ccx=ccx);
|
||||
auto fcx = rec(enclosing=ccx.fm.get(id), id=id,
|
||||
name=fn_ident_to_string(id, i), ccx=ccx);
|
||||
find_pre_post_fn(fcx, f);
|
||||
}
|
||||
//
|
||||
|
@ -6,8 +6,6 @@ import std::option::none;
|
||||
import util::common::span;
|
||||
import util::common::respan;
|
||||
|
||||
|
||||
// FIXME: Should visit patterns as well.
|
||||
type ast_visitor =
|
||||
rec(fn() -> bool keep_going,
|
||||
fn() -> bool want_crate_directives,
|
||||
@ -40,8 +38,8 @@ type ast_visitor =
|
||||
fn(&@ast::ty) visit_ty_pre,
|
||||
fn(&@ast::ty) visit_ty_post,
|
||||
fn(&@ast::constr) visit_constr,
|
||||
fn(&ast::_fn, &span, &ast::ident, ast::node_id) visit_fn_pre,
|
||||
fn(&ast::_fn, &span, &ast::ident, ast::node_id) visit_fn_post);
|
||||
fn(&ast::_fn, &span, &ast::fn_ident, ast::node_id) visit_fn_pre,
|
||||
fn(&ast::_fn, &span, &ast::fn_ident, ast::node_id) visit_fn_post);
|
||||
|
||||
fn walk_crate(&ast_visitor v, &ast::crate c) {
|
||||
if (!v.keep_going()) { ret; }
|
||||
@ -102,7 +100,7 @@ fn walk_item(&ast_visitor v, @ast::item i) {
|
||||
alt (i.node) {
|
||||
case (ast::item_const(?t, ?e)) { walk_ty(v, t); walk_expr(v, e); }
|
||||
case (ast::item_fn(?f, _)) {
|
||||
walk_fn(v, f, i.span, i.ident, i.id);
|
||||
walk_fn(v, f, i.span, some(i.ident), i.id);
|
||||
}
|
||||
case (ast::item_mod(?m)) { walk_mod(v, m); }
|
||||
case (ast::item_native_mod(?nm)) { walk_native_mod(v, nm); }
|
||||
@ -118,13 +116,15 @@ fn walk_item(&ast_visitor v, @ast::item i) {
|
||||
for (ast::obj_field f in ob.fields) { walk_ty(v, f.ty); }
|
||||
for (@ast::method m in ob.methods) {
|
||||
v.visit_method_pre(m);
|
||||
walk_fn(v, m.node.meth, m.span, m.node.ident, m.node.id);
|
||||
walk_fn(v, m.node.meth, m.span,
|
||||
some(m.node.ident), m.node.id);
|
||||
v.visit_method_post(m);
|
||||
}
|
||||
alt (ob.dtor) {
|
||||
case (none) { }
|
||||
case (some(?m)) {
|
||||
walk_fn(v, m.node.meth, m.span, m.node.ident, m.node.id);
|
||||
walk_fn(v, m.node.meth, m.span,
|
||||
some(m.node.ident), m.node.id);
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -217,7 +217,7 @@ fn walk_fn_decl(&ast_visitor v, &ast::fn_decl fd) {
|
||||
walk_ty(v, fd.output);
|
||||
}
|
||||
|
||||
fn walk_fn(&ast_visitor v, &ast::_fn f, &span sp, &ast::ident i,
|
||||
fn walk_fn(&ast_visitor v, &ast::_fn f, &span sp, &ast::fn_ident i,
|
||||
ast::node_id d) {
|
||||
if (!v.keep_going()) { ret; }
|
||||
v.visit_fn_pre(f, sp, i, d);
|
||||
@ -405,7 +405,8 @@ fn walk_expr(&ast_visitor v, @ast::expr e) {
|
||||
// Methods
|
||||
for (@ast::method m in anon_obj.methods) {
|
||||
v.visit_method_pre(m);
|
||||
walk_fn(v, m.node.meth, m.span, m.node.ident, m.node.id);
|
||||
walk_fn(v, m.node.meth, m.span, some(m.node.ident),
|
||||
m.node.id);
|
||||
v.visit_method_post(m);
|
||||
}
|
||||
}
|
||||
@ -447,7 +448,7 @@ fn def_visit_ty(&@ast::ty t) { }
|
||||
|
||||
fn def_visit_constr(&@ast::constr c) { }
|
||||
|
||||
fn def_visit_fn(&ast::_fn f, &span sp, &ast::ident i, ast::node_id d) { }
|
||||
fn def_visit_fn(&ast::_fn f, &span sp, &ast::fn_ident i, ast::node_id d) { }
|
||||
|
||||
fn default_visitor() -> ast_visitor {
|
||||
ret rec(keep_going=def_keep_going,
|
||||
|
@ -34,6 +34,13 @@ fn mode_str_1(&ty::mode m) -> str {
|
||||
}
|
||||
}
|
||||
|
||||
fn fn_ident_to_string(ast::node_id id, &ast::fn_ident i) -> str {
|
||||
ret alt (i) {
|
||||
case (none) { "anon" + istr(id) }
|
||||
case (some(?s)) { s }
|
||||
};
|
||||
}
|
||||
|
||||
fn ty_to_str(&ctxt cx, &t typ) -> str {
|
||||
fn fn_input_to_str(&ctxt cx, &rec(middle::ty::mode mode, t ty) input) ->
|
||||
str {
|
||||
|
Loading…
x
Reference in New Issue
Block a user