From a1bb4a4ded1128094066fb1b61f894d2a8dbc124 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 13 Jun 2011 18:10:33 -0700 Subject: [PATCH] Refactor some typestate-related data structures --- src/comp/middle/tstate/auxiliary.rs | 111 +++++++++--------- src/comp/middle/tstate/bitvectors.rs | 43 ++++--- src/comp/middle/tstate/ck.rs | 5 +- src/comp/middle/tstate/collect_locals.rs | 56 ++++----- src/comp/middle/tstate/pre_post_conditions.rs | 42 ++++--- src/comp/middle/tstate/states.rs | 28 ++--- 6 files changed, 142 insertions(+), 143 deletions(-) diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index d5d48bd67f8b..9b5c44bc6ad1 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -76,12 +76,12 @@ fn comma_str(vec[@constr_arg_use] args) -> str { ret res; } -fn constraint_to_str(ty::ctxt tcx, constr c) -> str { - alt (c.node) { - case (ninit(?i, _)) { +fn constraint_to_str(&ty::ctxt tcx, &constr c) -> str { + alt (c.node.c) { + case (ninit(?i)) { ret "init(" + i + " [" + tcx.sess.span_str(c.span) + "])"; } - case (npred(?p, _, ?args)) { + case (npred(?p, ?args)) { ret path_to_str(p) + "(" + comma_str(args) + ")" + "[" + tcx.sess.span_str(c.span) + "]"; } @@ -101,7 +101,7 @@ fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str { ret s; } -fn log_bitv(fn_ctxt fcx, bitv::t v) { +fn log_bitv(&fn_ctxt fcx, &bitv::t v) { log(bitv_to_str(fcx, v)); } @@ -208,43 +208,50 @@ fn print_idents(vec[ident] idents) -> () { /* data structures */ /**********************************************************************/ -/* mapping from def_id to bit number and other data - (ident/path/span are there for error-logging purposes) */ +/* Two different data structures represent constraints in different + contexts: constraint and norm_constraint. -/* FIXME very confused about why we have all these different types. */ +constraint gets used to record constraints in a table keyed by def_ids. +cinit constraints represent a single constraint, for the initialization +state of a variable; a cpred constraint, with a single operator and a +list of possible argument lists, could represent several constraints at +once. + +norm_constraint, in contrast, gets used when handling an instance +of a constraint rather than a definition of a constraint. It can +also be init or pred (ninit or npred), but the npred case just has +a single argument list. + +The representation of constraints, where multiple instances of the +same predicate are collapsed into one entry in the table, makes it +easier to look up a specific instance. + +Both types are in constrast with the constraint type defined in +front::ast, which is for predicate constraints only, and is what +gets generated by the parser. aux and ast share the same type +to represent predicate *arguments* however. This type +(constr_arg_general) is parameterized (see comments in front::ast). + +Both types store an ident and span, for error-logging purposes. +*/ type pred_desc_ = rec(vec[@constr_arg_use] args, uint bit_num); type pred_desc = spanned[pred_desc_]; tag constraint { - cinit(uint, span, def_id, ident); - cpred(path, def_id, @mutable vec[pred_desc]); + cinit(uint, span, ident); + cpred(path, @mutable vec[pred_desc]); } -tag constr_ { - ninit(ident, def_id); - npred(path, def_id, vec[@constr_arg_use]); +tag constr__ { + ninit(ident); + npred(path, vec[@constr_arg_use]); } +type constr_ = rec(def_id id, constr__ c); type constr = spanned[constr_]; type norm_constraint = rec(uint bit_num, constr c); -/* "constraint occurrence" to disambiguate - between constraints. either "this is an - init constraint", or the list of args for - a pred. */ -tag constr_occ { - occ_init; - occ_args(vec[@constr_arg_use]); -} - type constr_map = @std::map::hashmap[def_id, constraint]; -fn constr_id(&constr c) -> def_id { - ret (alt (c.node) { - case (ninit(_, ?i)) { i } - case (npred(_, ?i, _)) { i } - }) -} - type fn_info = rec(constr_map constrs, uint num_constraints, controlflow cf); /* mapping from node ID to typestate annotation */ @@ -529,16 +536,16 @@ fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] { ret ccx.tcx.def_map.find(a.id); } -fn norm_a_constraint(&constraint c) -> vec[norm_constraint] { +fn norm_a_constraint(&def_id id, &constraint c) -> vec[norm_constraint] { alt (c) { - case (cinit(?n, ?sp, ?id, ?i)) { - ret [rec(bit_num=n, c=respan(sp, ninit(i, id)))]; + case (cinit(?n, ?sp, ?i)) { + ret [rec(bit_num=n, c=respan(sp, rec(id=id, c=ninit(i))))]; } - case (cpred(?p, ?id, ?descs)) { + case (cpred(?p, ?descs)) { let vec[norm_constraint] res = []; for (pred_desc pd in *descs) { vec::push(res, rec(bit_num=pd.node.bit_num, - c=respan(pd.span, npred(p, id, pd.node.args)))); + c=respan(pd.span, rec(id=id, c=npred(p, pd.node.args))))); } ret res; } @@ -551,7 +558,7 @@ fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] { let vec[norm_constraint] res = []; for each (@tup(def_id, constraint) p in fcx.enclosing.constrs.items()) { - res += norm_a_constraint(p._1); + res += norm_a_constraint(p._0, p._1); } ret res; } @@ -572,13 +579,6 @@ fn match_args(&fn_ctxt fcx, vec[pred_desc] occs, fcx.ccx.tcx.sess.bug("match_args: no match for occurring args"); } -fn constr_to_constr_occ(&ty::ctxt tcx, &constr_ c) -> constr_occ { - alt (c) { - case (ninit(_, _)) { ret occ_init; } - case (npred(_, _, ?args)) { ret occ_args(args); } - } -} - fn def_id_for_constr(ty::ctxt tcx, uint t) -> def_id { alt (tcx.def_map.find(t)) { case (none) { @@ -627,8 +627,9 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr { alt (operator.node) { case (expr_path(?p, ?a)) { ret respan(e.span, - npred(p, def_id_for_constr(tcx, a.id), - exprs_to_constr_args(tcx, args))); + rec(id=def_id_for_constr(tcx, a.id), + c=npred(p, + exprs_to_constr_args(tcx, args)))); } case (_) { tcx.sess.span_err(operator.span, "Internal error: " + @@ -648,20 +649,14 @@ fn pred_desc_to_str(&pred_desc p) -> str { pretty::ppaux::constr_args_to_str_1(p.node.args) + ">"); } -fn substitute_constr_args_(&ty::ctxt cx, +fn substitute_constr_args(&ty::ctxt cx, &vec[@expr] actuals, &@ast::constr c) - -> vec[@constr_arg_use] { + -> constr__ { let vec[@constr_arg_use] res = []; for (@constr_arg a in c.node.args) { res += [substitute_arg(cx, actuals, a)]; } - ret res; - -} - -fn substitute_constr_args(&ty::ctxt cx, - &vec[@expr] actuals, &@ast::constr c) -> constr_occ { - ret occ_args(substitute_constr_args_(cx, actuals, c)); + ret npred(c.node.path, res); } type subst = vec[tup(arg, @expr)]; @@ -683,6 +678,16 @@ fn substitute_arg(&ty::ctxt cx, &vec[@expr] actuals, @ast::constr_arg a) } } +fn path_to_ident(&ty::ctxt cx, &path p) -> ident { + alt (vec::last(p.node.idents)) { + case (none) { + cx.sess.span_err(p.span, "Malformed path"); + } + case (some(?i)) { + ret i; + } + } +} // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index 8ae65c5063fc..52bde20f89ce 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -9,13 +9,13 @@ import aux::fn_ctxt; import aux::fn_info; import aux::log_bitv; import aux::num_constraints; -import aux::constr_occ; -import aux::occ_init; -import aux::occ_args; import aux::cinit; import aux::cpred; +import aux::ninit; +import aux::npred; import aux::pred_desc; import aux::match_args; +import aux::constr_; import tstate::aux::ann_to_ts_ann; import tstate::ann::pre_and_post; @@ -35,13 +35,13 @@ import tstate::ann::set_in_postcond; import tstate::ann::set_in_poststate; import tstate::ann::clear_in_poststate; -fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint { - assert (fcx.enclosing.constrs.contains_key(v)); - auto res = fcx.enclosing.constrs.get(v); - alt (o) { - case (occ_init) { +fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint { + assert (fcx.enclosing.constrs.contains_key(c.id)); + auto res = fcx.enclosing.constrs.get(c.id); + alt (c.c) { + case (ninit(_)) { alt (res) { - case (cinit(?n,_,_,_)) { + case (cinit(?n,_,_)) { ret n; } case (_) { @@ -50,9 +50,9 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint { } } } - case (occ_args(?args)) { + case (npred(_, ?args)) { alt (res) { - case (cpred(_, _, ?descs)) { + case (cpred(_, ?descs)) { ret match_args(fcx, *descs, args); } case (_) { @@ -64,8 +64,8 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint { } } -fn promises(&fn_ctxt fcx, &poststate p, &def_id v, &constr_occ o) -> bool { - ret bitv::get(p, bit_num(fcx, v, o)); +fn promises(&fn_ctxt fcx, &poststate p, &constr_ c) -> bool { + ret bitv::get(p, bit_num(fcx, c)); } // Given a list of pres and posts for exprs e0 ... en, @@ -143,27 +143,26 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond { ret intersect_postconds_go(bitv::clone(pcs.(0)), pcs); } -fn gen(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool { - ret set_in_postcond(bit_num(fcx, id, o), +fn gen(&fn_ctxt fcx, &ann a, &constr_ c) -> bool { + ret set_in_postcond(bit_num(fcx, c), (ann_to_ts_ann(fcx.ccx, a)).conditions); } -fn declare_var(&fn_ctxt fcx, def_id id, prestate pre) - -> prestate { +fn declare_var(&fn_ctxt fcx, &constr_ c, prestate pre) -> prestate { auto res = clone(pre); - relax_prestate(bit_num(fcx, id, occ_init), res); + relax_prestate(bit_num(fcx, c), res); ret res; } -fn gen_poststate(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool { +fn gen_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool { log "gen_poststate"; - ret set_in_poststate(bit_num(fcx, id, o), + ret set_in_poststate(bit_num(fcx, c), (ann_to_ts_ann(fcx.ccx, a)).states); } -fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id, &constr_occ o) -> bool { +fn kill_poststate(&fn_ctxt fcx, &ann a, &constr_ c) -> bool { log "kill_poststate"; - ret clear_in_poststate(bit_num(fcx, id, o), + ret clear_in_poststate(bit_num(fcx, c), (ann_to_ts_ann(fcx.ccx, a)).states); } diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs index 9ba06711cd96..27e885e66d8a 100644 --- a/src/comp/middle/tstate/ck.rs +++ b/src/comp/middle/tstate/ck.rs @@ -133,8 +133,9 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () { auto cf = fcx.enclosing.cf; /* Finally, check that the return value is initialized */ + let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name)); if (f.proto == ast::proto_fn - && ! promises(fcx, *post, fcx.id, aux::occ_init) + && ! promises(fcx, *post, ret_c) && ! type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, a)) && cf == return) { @@ -148,7 +149,7 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () { // check that this really always fails // the fcx.id bit means "returns" for a returning fn, // "diverges" for a non-returning fn - if (! promises(fcx, *post, fcx.id, aux::occ_init)) { + if (! promises(fcx, *post, ret_c)) { fcx.ccx.tcx.sess.span_err(f.body.span, "In non-returning function " + fcx.name + ", some control paths may return to the caller"); diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index cda6405785c7..e6691fce48f2 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -13,7 +13,6 @@ import aux::cinit; import aux::ninit; import aux::npred; import aux::cpred; -import aux::constr; import aux::constraint; import aux::fn_info; import aux::crate_ctxt; @@ -28,19 +27,19 @@ import util::common::uistr; import util::common::span; import util::common::respan; -type ctxt = rec(@mutable vec[constr] cs, - ty::ctxt tcx); +type ctxt = rec(@mutable vec[aux::constr] cs, ty::ctxt tcx); fn collect_local(&ctxt cx, &@local loc) -> () { log("collect_local: pushing " + loc.node.ident); - vec::push[constr](*cx.cs, respan(loc.span, - ninit(loc.node.ident, loc.node.id))); + vec::push(*cx.cs, respan(loc.span, + rec(id=loc.node.id, + c=ninit(loc.node.ident)))); } fn collect_pred(&ctxt cx, &@expr e) -> () { alt (e.node) { case (expr_check(?e, _)) { - vec::push[constr](*cx.cs, expr_to_constr(cx.tcx, e)); + vec::push(*cx.cs, expr_to_constr(cx.tcx, e)); } // If it's a call, generate appropriate instances of the // call's constraints. @@ -49,12 +48,10 @@ fn collect_pred(&ctxt cx, &@expr e) -> () { auto d_id = ann_to_def_strict(cx.tcx, c.node.ann); alt (d_id) { case (def_fn(?an_id)) { - let constr an_occ = respan(c.span, - npred(c.node.path, an_id, - aux::substitute_constr_args_(cx.tcx, - operands, - c))); - vec::push[constr](*cx.cs, an_occ); + let aux::constr ct = respan(c.span, + rec(id=an_id, c=aux::substitute_constr_args(cx.tcx, + operands, c))); + vec::push(*cx.cs, ct); } case (_) { cx.tcx.sess.span_err(c.span, @@ -70,7 +67,7 @@ fn collect_pred(&ctxt cx, &@expr e) -> () { fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a) -> ctxt { - let ctxt cx = rec(cs=@mutable vec::alloc[constr](0u), tcx=tcx); + let ctxt cx = rec(cs=@mutable vec::alloc(0u), tcx=tcx); auto visitor = walk::default_visitor(); visitor = rec(visit_local_pre=bind collect_local(cx,_), visit_expr_pre=bind collect_pred(cx,_) @@ -79,34 +76,32 @@ fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a) ret cx; } -fn add_constraint(&ty::ctxt tcx, constr c, uint next, constr_map tbl) +fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) -> uint { log(aux::constraint_to_str(tcx, c) + " |-> " + util::common::uistr(next)); - alt (c.node) { - case (ninit(?i, ?id)) { - tbl.insert(id, cinit(next, c.span, id, i)); + alt (c.node.c) { + case (ninit(?i)) { + tbl.insert(c.node.id, cinit(next, c.span, i)); } - case (npred(?p, ?id, ?args)) { - alt (tbl.find(id)) { - case (some[constraint](?ct)) { + case (npred(?p, ?args)) { + alt (tbl.find(c.node.id)) { + case (some(?ct)) { alt (ct) { - case (cinit(_,_,_,_)) { + case (cinit(_,_,_)) { tcx.sess.bug("add_constraint: same def_id used" + " as a variable and a pred"); } - case (cpred(_, _, ?pds)) { + case (cpred(_, ?pds)) { vec::push(*pds, respan(c.span, - rec(args=args, bit_num=next))); + rec(args=args, bit_num=next))); } } } - // FIXME: this suggests a cpred shouldn't really have a - // def_id as a field... - case (none[constraint]) { - tbl.insert(id, cpred(p, id, + case (none) { + tbl.insert(c.node.id, cpred(p, @mutable [respan(c.span, rec(args=args, - bit_num=next))])); + bit_num=next))])); } } } @@ -130,12 +125,13 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp, /* now we have to add bit nums for both the constraints and the variables... */ - for (constr c in {*cx.cs}) { + for (aux::constr c in {*cx.cs}) { next = add_constraint(cx.tcx, c, 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 */ - add_constraint(cx.tcx, respan(f_sp, ninit(f_name, f_id)), next, res_map); + add_constraint(cx.tcx, respan(f_sp, rec(id=f_id, c=ninit(f_name))), next, + res_map); auto res = rec(constrs=res_map, num_constraints=vec::len(*cx.cs) + 1u, diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 5771b0fff7cb..5eafeb8a1a52 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -22,10 +22,8 @@ import tstate::ann::set_precondition; import tstate::ann::set_postcondition; import aux::crate_ctxt; import aux::fn_ctxt; -import aux::occ_init; import aux::num_constraints; import aux::constraint; -import aux::constr_occ; import aux::expr_pp; import aux::stmt_pp; import aux::block_pp; @@ -46,10 +44,12 @@ import aux::ann_to_ts_ann; import aux::set_postcond_false; import aux::controlflow_expr; import aux::expr_to_constr; -import aux::constr_to_constr_occ; +//import aux::constr_to_constr_occ; import aux::constraints_expr; import aux::substitute_constr_args; -import aux::constr_id; +import aux::ninit; +import aux::npred; +import aux::path_to_ident; import bitvectors::seq_preconds; import bitvectors::union_postconds; @@ -174,7 +174,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body, &ann a) -> () { find_pre_post_expr(fcx, index); find_pre_post_block(fcx, body); - auto loop_precond = declare_var(fcx, l.node.id, + auto loop_precond = declare_var(fcx, rec(id=l.node.id, + c=ninit(l.node.ident)), seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)])); auto loop_postcond = intersect_postconds ([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]); @@ -182,7 +183,7 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, } fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, - &ann larger_ann, &ann new_var) -> () { + &ann larger_ann, &ann new_var, &path pth) -> () { alt (ann_to_def(fcx.ccx, new_var)) { case (some(?d)) { alt (d) { @@ -191,7 +192,8 @@ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, auto p = expr_pp(fcx.ccx, rhs); set_pre_and_post(fcx.ccx, larger_ann, p.precondition, p.postcondition); - gen(fcx, larger_ann, d_id, aux::occ_init); + gen(fcx, larger_ann, rec(id=d_id, + c=ninit(path_to_ident(fcx.ccx.tcx, pth)))); } case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); } } @@ -230,8 +232,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { auto id = ann_to_def(fcx.ccx, c.node.ann); alt (id) { case (some(def_fn(?d_id))) { - auto i = bit_num(fcx, d_id, - substitute_constr_args(fcx.ccx.tcx, operands, c)); + auto i = bit_num(fcx, rec(id=d_id, + c=substitute_constr_args(fcx.ccx.tcx, + operands, c))); require(i, pp); } case (_) { @@ -269,7 +272,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { auto df = ann_to_def_strict(fcx.ccx.tcx, a); alt (df) { case (def_local(?d_id)) { - auto i = bit_num(fcx, d_id, occ_init); + auto i = bit_num(fcx, rec(id=d_id, + c=ninit(path_to_ident(fcx.ccx.tcx, p)))); require_and_preserve(i, res); } case (_) { /* nothing to check */ } @@ -311,7 +315,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { // FIXME: this needs to deinitialize the rhs alt (lhs.node) { case (expr_path(?p, ?a_lhs)) { - gen_if_local(fcx, lhs, rhs, a, a_lhs); + gen_if_local(fcx, lhs, rhs, a, a_lhs, p); } case (_) { find_pre_post_exprs(fcx, [lhs, rhs], a); @@ -321,7 +325,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { case (expr_assign(?lhs, ?rhs, ?a)) { alt (lhs.node) { case (expr_path(?p, ?a_lhs)) { - gen_if_local(fcx, lhs, rhs, a, a_lhs); + gen_if_local(fcx, lhs, rhs, a, a_lhs, p); } case (_) { find_pre_post_exprs(fcx, [lhs, rhs], a); @@ -331,7 +335,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { case (expr_recv(?lhs, ?rhs, ?a)) { alt (lhs.node) { case (expr_path(?p, ?a_lhs)) { - gen_if_local(fcx, lhs, rhs, a, a_lhs); + gen_if_local(fcx, lhs, rhs, a, a_lhs, p); } case (_) { // doesn't check that lhs is an lval, but @@ -510,8 +514,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () { copy_pre_post(fcx.ccx, a, p); /* predicate p holds after this expression executes */ let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); - let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.node); - gen(fcx, a, constr_id(c), o); + gen(fcx, a, c.node); } case(expr_bind(?operator, ?maybe_args, ?a)) { auto args = vec::cat_options[@expr](maybe_args); @@ -565,13 +568,8 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) /* Inherit ann from initializer, and add var being initialized to the postcondition */ copy_pre_post(fcx.ccx, a, an_init.expr); - /* log("gen (decl):"); - log_stmt(s); */ - gen(fcx, a, alocal.id, occ_init); - /* log_err("for stmt"); - log_stmt(s); - log_err("pp = "); - log_pp(stmt_pp(s)); */ + gen(fcx, a, rec(id=alocal.id, + c=ninit(alocal.ident))); } case(none) { clear_pp(ann_to_ts_ann(fcx.ccx, diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 2b2bfa01a42a..e89fd1a6a838 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -48,11 +48,10 @@ import aux::log_states; import aux::block_states; import aux::controlflow_expr; import aux::ann_to_def; -import aux::occ_init; import aux::expr_to_constr; -import aux::constr_to_constr_occ; -import aux::constr_occ; -import aux::constr_id; +import aux::ninit; +import aux::npred; +import aux::path_to_ident; import bitvectors::seq_preconds; import bitvectors::union_postconds; @@ -123,10 +122,11 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l, ret changed; } -fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool { +fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool { alt (ann_to_def(fcx.ccx, a_new_var)) { case (some(def_local(?loc))) { - ret gen_poststate(fcx, a, loc, occ_init); + ret gen_poststate(fcx, a, rec(id=loc, + c=ninit(path_to_ident(fcx.ccx.tcx, p)))); } case (_) { ret false; } } @@ -257,7 +257,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { || changed; changed = extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, rhs)) || changed; - changed = gen_if_local(fcx, a_lhs, a)|| changed; + changed = gen_if_local(fcx, a_lhs, a, p)|| changed; } case (_) { // assignment to something that must already have been init'd @@ -282,7 +282,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { || changed; changed = extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, rhs)) || changed; - changed = gen_if_local(fcx, a_lhs, a)|| changed; + changed = gen_if_local(fcx, a_lhs, a, p)|| changed; } case (_) { // assignment to something that must already have been init'd @@ -307,7 +307,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { || changed; changed = extend_poststate_ann(fcx.ccx, a, expr_poststate(fcx.ccx, rhs)) || changed; - changed = gen_if_local(fcx, a_lhs, a) || changed; + changed = gen_if_local(fcx, a_lhs, a, p) || changed; } case (_) { // receive to something that must already have been init'd @@ -331,7 +331,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { /* return from an always-failing function clears the return bit */ alt (fcx.enclosing.cf) { case (noreturn) { - kill_poststate(fcx, a, fcx.id, occ_init); + kill_poststate(fcx, a, rec(id=fcx.id, c=ninit(fcx.name))); } case (_) {} } @@ -529,8 +529,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { changed = extend_poststate_ann(fcx.ccx, a, pres) || changed; /* predicate p holds after this expression executes */ let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); - let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.node); - changed = gen_poststate(fcx, a, constr_id(c), o) || changed; + changed = gen_poststate(fcx, a, c.node) || changed; ret changed; } case (expr_break(?a)) { @@ -590,7 +589,7 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { expr_poststate(fcx.ccx, an_init.expr)) || changed; changed = gen_poststate(fcx, a, - alocal.id, occ_init) + rec(id=alocal.id, c=ninit(alocal.ident))) || changed; log("Summary: stmt = "); log_stmt(*s); @@ -727,7 +726,8 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { false_postcond(num_local_vars)); alt (fcx.enclosing.cf) { case (noreturn) { - kill_poststate(fcx, tailann, fcx.id, occ_init); + kill_poststate(fcx, tailann, + rec(id=fcx.id, c=ninit(fcx.name))); } case (_) { } }