diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index d6303b15fe63..c2a69c4426c0 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -1053,6 +1053,29 @@ fn op_to_oper_ty(init_op io) -> oper_type { fn do_nothing[T](&_fn f, &ty_param[] tp, &span sp, &fn_ident i, node_id iid, &T cx, &visit::vt[T] v) { } + + +fn args_to_constr_args(&span sp, &arg[] args) -> (@constr_arg_use)[] { + let (@constr_arg_use)[] actuals = ~[]; + for (arg a in args) { + actuals += ~[@respan(sp, carg_ident(tup(a.ident, a.id)))]; + } + ret actuals; +} + +fn ast_constr_to_ts_constr(&ty::ctxt tcx, &arg[] args, &@constr c) + -> tsconstr { + auto tconstr = ty::ast_constr_to_constr(tcx, c); + ret npred(tconstr.node.path, tconstr.node.id, + args_to_constr_args(tconstr.span, args)); +} + +fn ast_constr_to_sp_constr(&ty::ctxt tcx, &arg[] args, &@constr c) + -> sp_constr { + auto tconstr = ast_constr_to_ts_constr(tcx, args, c); + ret respan(c.span, tconstr); +} + // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index e7afe85f34f7..e3538d1527c6 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -233,6 +233,10 @@ fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident, ret set_in_poststate_(bit_num(fcx, ninit(id, ident)), t); } +fn set_in_prestate_constr(&fn_ctxt fcx, &tsconstr c, &prestate t) -> bool { + ret set_in_poststate_(bit_num(fcx, c), t); +} + fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident, &node_id parent) -> bool { ret kill_poststate(fcx, parent, ninit(id, ident)); diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index 5005ad5132b2..8d4fc6cc1199 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -1,4 +1,5 @@ - +import std::uint; +import std::int; import std::ivec; import syntax::ast::*; import util::ppaux::fn_ident_to_string; @@ -96,6 +97,7 @@ fn add_constraint(&ty::ctxt tcx, sp_constr c, uint next, constr_map tbl) -> to a bit number in the precondition/postcondition vectors */ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp, &span f_sp, &fn_ident f_name, node_id id) { + auto name = fn_ident_to_string(id, f_name); auto res_map = @new_def_hash[constraint](); let uint next = 0u; @@ -106,15 +108,23 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp, for (sp_constr c in { *cx.cs }) { next = add_constraint(cx.tcx, c, next, res_map); } + /* if this function has any constraints, instantiate them to the + argument names and add them */ + auto sc; + for (@constr c in f.decl.constraints) { + sc = ast_constr_to_sp_constr(cx.tcx, f.decl.inputs, c); + next = add_constraint(cx.tcx, sc, next, res_map); + } + /* add a pseudo-entry for the function's return value we can safely use the function's name itself for this purpose */ - auto name = fn_ident_to_string(id, f_name); add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map); let @mutable node_id[] v = @mutable ~[]; auto rslt = rec(constrs=res_map, - num_constraints=ivec::len(*cx.cs) + 1u, + num_constraints=ivec::len(*cx.cs) + ivec::len(f.decl.constraints) + + 1u, cf=f.decl.cf, used_vars=v); ccx.fm.insert(id, rslt); diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 88b21748a3f1..c91687be0f8b 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -1,3 +1,4 @@ +import syntax::print::pprust::path_to_str; import std::ivec; import std::option; import std::option::get; @@ -25,6 +26,8 @@ import tritv::tritv_clone; import tritv::tritv_set; import tritv::ttrue; +import bitvectors::*; +/* import bitvectors::set_in_poststate_ident; import bitvectors::clear_in_poststate_expr; import bitvectors::clear_in_prestate_ident; @@ -33,6 +36,7 @@ import bitvectors::gen_poststate; import bitvectors::kill_poststate; import bitvectors::clear_in_poststate_ident; import bitvectors::intersect_states; +*/ import syntax::ast::*; import middle::ty::expr_ty; import middle::ty::type_is_nil; @@ -731,9 +735,15 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { auto num_local_vars = num_constraints(fcx.enclosing); // make sure the return bit starts out False clear_in_prestate_ident(fcx, fcx.id, fcx.name, f.body.node.id); - auto changed = - find_pre_post_state_block(fcx, block_prestate(fcx.ccx, f.body), - f.body); + // Instantiate any constraints on the arguments so we can use them + auto block_pre = block_prestate(fcx.ccx, f.body); + auto tsc; + for (@constr c in f.decl.constraints) { + tsc = ast_constr_to_ts_constr(fcx.ccx.tcx, f.decl.inputs, c); + set_in_prestate_constr(fcx, tsc, block_pre); + } + + auto changed = find_pre_post_state_block(fcx, block_pre, f.body); // Treat the tail expression as a return statement alt (f.body.node.expr) { diff --git a/src/test/run-pass/typestate-transitive.rs b/src/test/run-pass/typestate-transitive.rs new file mode 100644 index 000000000000..86dacb2f8e0f --- /dev/null +++ b/src/test/run-pass/typestate-transitive.rs @@ -0,0 +1,8 @@ +pred p(int i) -> bool { true } + +fn f(int i) : p(i) -> int { i } + +fn g(int i) : p(i) -> int { f(i) } + +fn main() { +}