rustc: Move middle::tstate::auxiliary and middle::tstate::bitvectors over to interior vectors
This commit is contained in:
parent
702f88a3be
commit
cfc659009e
@ -1,3 +1,4 @@
|
||||
import std::ivec;
|
||||
import std::str;
|
||||
import std::vec;
|
||||
import std::vec::len;
|
||||
@ -48,7 +49,7 @@ fn def_id_to_str(def_id d) -> str {
|
||||
ret int::str(d._0) + "," + int::str(d._1);
|
||||
}
|
||||
|
||||
fn comma_str(vec[@constr_arg_use] args) -> str {
|
||||
fn comma_str(&(@constr_arg_use)[] args) -> str {
|
||||
auto rslt = "";
|
||||
auto comma = false;
|
||||
for (@constr_arg_use a in args) {
|
||||
@ -107,7 +108,7 @@ fn first_difference_string(&fn_ctxt fcx, &tritv::t expected, &tritv::t actual)
|
||||
|
||||
fn log_tritv_err(fn_ctxt fcx, tritv::t v) { log_err tritv_to_str(fcx, v); }
|
||||
|
||||
fn tos(vec[uint] v) -> str {
|
||||
fn tos(&uint[] v) -> str {
|
||||
auto rslt = "";
|
||||
for (uint i in v) { if (i == 0u) { rslt += "0"; }
|
||||
else if (i == 1u) { rslt += "1"; }
|
||||
@ -115,9 +116,9 @@ fn tos(vec[uint] v) -> str {
|
||||
ret rslt;
|
||||
}
|
||||
|
||||
fn log_cond(vec[uint] v) { log tos(v); }
|
||||
fn log_cond(&uint[] v) { log tos(v); }
|
||||
|
||||
fn log_cond_err(vec[uint] v) { log_err tos(v); }
|
||||
fn log_cond_err(&uint[] v) { log_err tos(v); }
|
||||
|
||||
fn log_pp(&pre_and_post pp) {
|
||||
auto p1 = tritv::to_vec(pp.precondition);
|
||||
@ -157,10 +158,10 @@ fn log_states_err(&pre_and_post_state pp) {
|
||||
|
||||
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); }
|
||||
fn print_idents(&mutable ident[] idents) {
|
||||
if (ivec::len[ident](idents) == 0u) { ret; }
|
||||
log "an ident: " + ivec::pop[ident](idents);
|
||||
print_idents(idents);
|
||||
}
|
||||
|
||||
|
||||
@ -194,7 +195,7 @@ to represent predicate *arguments* however. This type
|
||||
|
||||
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_ = rec((@constr_arg_use)[] args, uint bit_num);
|
||||
|
||||
type pred_desc = spanned[pred_desc_];
|
||||
|
||||
@ -202,10 +203,13 @@ type constr_arg_use = constr_arg_general[tup(ident, def_id)];
|
||||
|
||||
tag constraint {
|
||||
cinit(uint, span, ident);
|
||||
cpred(path, @mutable vec[pred_desc]);
|
||||
cpred(path, @mutable pred_desc[]);
|
||||
}
|
||||
|
||||
tag constr__ { ninit(ident); npred(path, vec[@constr_arg_use]); }
|
||||
tag constr__ {
|
||||
ninit(ident);
|
||||
npred(path, (@constr_arg_use)[]);
|
||||
}
|
||||
|
||||
type constr_ = rec(node_id id, constr__ c);
|
||||
|
||||
@ -223,11 +227,11 @@ type fn_info = rec(constr_map constrs,
|
||||
used*/
|
||||
// Doesn't seem to work without the @ --
|
||||
// bug?
|
||||
@mutable vec[node_id] used_vars);
|
||||
@mutable node_id[] used_vars);
|
||||
|
||||
|
||||
/* mapping from node ID to typestate annotation */
|
||||
type node_ann_table = @mutable vec[mutable ts_ann];
|
||||
type node_ann_table = @mutable ts_ann[mutable];
|
||||
|
||||
|
||||
/* mapping from function name to fn_info map */
|
||||
@ -243,15 +247,15 @@ fn get_fn_info(&crate_ctxt ccx, node_id id) -> fn_info {
|
||||
}
|
||||
|
||||
fn add_node(&crate_ctxt ccx, node_id i, &ts_ann a) {
|
||||
auto sz = len(*ccx.node_anns);
|
||||
auto sz = ivec::len(*ccx.node_anns);
|
||||
if (sz <= i as uint) {
|
||||
grow(*ccx.node_anns, (i as uint) - sz + 1u, empty_ann(0u));
|
||||
ivec::grow_mut(*ccx.node_anns, (i as uint) - sz + 1u, empty_ann(0u));
|
||||
}
|
||||
ccx.node_anns.(i) = a;
|
||||
}
|
||||
|
||||
fn get_ts_ann(&crate_ctxt ccx, node_id i) -> option::t[ts_ann] {
|
||||
if (i as uint < len(*ccx.node_anns)) {
|
||||
if (i as uint < ivec::len(*ccx.node_anns)) {
|
||||
ret some[ts_ann](ccx.node_anns.(i));
|
||||
} else { ret none[ts_ann]; }
|
||||
}
|
||||
@ -439,7 +443,7 @@ fn pure_exp(&crate_ctxt ccx, node_id id, &prestate p) -> bool {
|
||||
fn num_constraints(fn_info m) -> uint { ret m.num_constraints; }
|
||||
|
||||
fn new_crate_ctxt(ty::ctxt cx) -> crate_ctxt {
|
||||
let vec[mutable ts_ann] na = vec::empty_mut();
|
||||
let ts_ann[mutable] na = ~[mutable];
|
||||
ret rec(tcx=cx, node_anns=@mutable na, fm=@new_int_hash[fn_info]());
|
||||
}
|
||||
|
||||
@ -474,19 +478,18 @@ fn node_id_to_def(&crate_ctxt ccx, node_id id) -> option::t[def] {
|
||||
ret ccx.tcx.def_map.find(id);
|
||||
}
|
||||
|
||||
fn norm_a_constraint(node_id id, &constraint c) -> vec[norm_constraint] {
|
||||
fn norm_a_constraint(node_id id, &constraint c) -> norm_constraint[] {
|
||||
alt (c) {
|
||||
case (cinit(?n, ?sp, ?i)) {
|
||||
ret [rec(bit_num=n, c=respan(sp, rec(id=id, c=ninit(i))))];
|
||||
ret ~[rec(bit_num=n, c=respan(sp, rec(id=id, c=ninit(i))))];
|
||||
}
|
||||
case (cpred(?p, ?descs)) {
|
||||
let vec[norm_constraint] rslt = [];
|
||||
let norm_constraint[] rslt = ~[];
|
||||
for (pred_desc pd in *descs) {
|
||||
vec::push(rslt,
|
||||
rec(bit_num=pd.node.bit_num,
|
||||
rslt += ~[rec(bit_num=pd.node.bit_num,
|
||||
c=respan(pd.span,
|
||||
rec(id=id,
|
||||
c=npred(p, pd.node.args)))));
|
||||
c=npred(p, pd.node.args))))];
|
||||
}
|
||||
ret rslt;
|
||||
}
|
||||
@ -496,15 +499,15 @@ fn norm_a_constraint(node_id id, &constraint c) -> vec[norm_constraint] {
|
||||
|
||||
// Tried to write this as an iterator, but I got a
|
||||
// non-exhaustive match in trans.
|
||||
fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] {
|
||||
let vec[norm_constraint] rslt = [];
|
||||
fn constraints(&fn_ctxt fcx) -> norm_constraint[] {
|
||||
let norm_constraint[] rslt = ~[];
|
||||
for each (@tup(node_id, constraint) p in fcx.enclosing.constrs.items()) {
|
||||
rslt += norm_a_constraint(p._0, p._1);
|
||||
}
|
||||
ret rslt;
|
||||
}
|
||||
|
||||
fn match_args(&fn_ctxt fcx, vec[pred_desc] occs, &(@constr_arg_use)[] occ) ->
|
||||
fn match_args(&fn_ctxt fcx, &pred_desc[] occs, &(@constr_arg_use)[] occ) ->
|
||||
uint {
|
||||
log "match_args: looking at " +
|
||||
constr_args_to_str(std::util::fst[ident, def_id], occ);
|
||||
@ -564,10 +567,10 @@ fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use {
|
||||
}
|
||||
}
|
||||
|
||||
fn exprs_to_constr_args(ty::ctxt tcx, vec[@expr] args) ->
|
||||
vec[@constr_arg_use] {
|
||||
fn exprs_to_constr_args(ty::ctxt tcx, &(@expr)[] args)
|
||||
-> (@constr_arg_use)[] {
|
||||
auto f = bind expr_to_constr_arg(tcx, _);
|
||||
ret vec::map(f, args);
|
||||
ret ivec::map(f, args);
|
||||
}
|
||||
|
||||
fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
|
||||
@ -578,10 +581,14 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
|
||||
expr_call(?operator, ?args)) {
|
||||
alt (operator.node) {
|
||||
case (expr_path(?p)) {
|
||||
// FIXME: Remove this vec->ivec conversion.
|
||||
auto args_ivec = ~[];
|
||||
for (@expr e in args) { args_ivec += ~[e]; }
|
||||
|
||||
ret respan(e.span,
|
||||
rec(id=node_id_for_constr(tcx, operator.id),
|
||||
c=npred(p,
|
||||
exprs_to_constr_args(tcx, args))));
|
||||
c=npred(p, exprs_to_constr_args(tcx,
|
||||
args_ivec))));
|
||||
}
|
||||
case (_) {
|
||||
tcx.sess.span_fatal(operator.span,
|
||||
@ -609,20 +616,20 @@ fn pred_desc_to_str(&pred_desc p) -> str {
|
||||
constr_args_to_str(std::util::fst[ident, def_id], cau_ivec) + ">";
|
||||
}
|
||||
|
||||
fn substitute_constr_args(&ty::ctxt cx, &vec[@expr] actuals,
|
||||
fn substitute_constr_args(&ty::ctxt cx, &(@expr)[] actuals,
|
||||
&@ty::constr_def c) -> constr__ {
|
||||
let vec[@constr_arg_use] rslt = [];
|
||||
let (@constr_arg_use)[] rslt = ~[];
|
||||
for (@constr_arg a in c.node.args) {
|
||||
rslt += [substitute_arg(cx, actuals, a)];
|
||||
rslt += ~[substitute_arg(cx, actuals, a)];
|
||||
}
|
||||
ret npred(c.node.path, rslt);
|
||||
}
|
||||
|
||||
type subst = vec[tup(arg, @expr)];
|
||||
type subst = tup(arg, @expr)[];
|
||||
|
||||
fn substitute_arg(&ty::ctxt cx, &vec[@expr] actuals, @constr_arg a) ->
|
||||
fn substitute_arg(&ty::ctxt cx, &(@expr)[] actuals, @constr_arg a) ->
|
||||
@constr_arg_use {
|
||||
auto num_actuals = vec::len(actuals);
|
||||
auto num_actuals = ivec::len(actuals);
|
||||
alt (a.node) {
|
||||
case (carg_ident(?i)) {
|
||||
if (i < num_actuals) {
|
||||
@ -778,26 +785,28 @@ fn non_init_constraint_mentions(&fn_ctxt fcx, &norm_constraint c,
|
||||
}
|
||||
|
||||
|
||||
fn args_mention(&vec[@constr_arg_use] args, &def_id v) -> bool {
|
||||
fn args_mention(&(@constr_arg_use)[] args, &def_id v) -> bool {
|
||||
fn mentions(&def_id v, &@constr_arg_use a) -> bool {
|
||||
alt (a.node) {
|
||||
case (carg_ident(?p1)) { p1._1 == v }
|
||||
case (_) { false }
|
||||
}
|
||||
}
|
||||
ret util::common::any[@constr_arg_use](bind mentions(v,_), args);
|
||||
ret ivec::any[@constr_arg_use](bind mentions(v,_), args);
|
||||
}
|
||||
|
||||
fn use_var(&fn_ctxt fcx, &node_id v) {
|
||||
vec::push(*fcx.enclosing.used_vars, v);
|
||||
*fcx.enclosing.used_vars += ~[v];
|
||||
}
|
||||
|
||||
fn vec_contains(&@mutable vec[node_id] v, &node_id i) -> bool {
|
||||
// FIXME: This should be a function in std::ivec::.
|
||||
fn vec_contains(&@mutable (node_id[]) v, &node_id i) -> bool {
|
||||
for (node_id d in *v) {
|
||||
if (d == i) { ret true; }
|
||||
}
|
||||
ret false;
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
|
@ -1,10 +1,9 @@
|
||||
|
||||
import syntax::ast::*;
|
||||
import syntax::walk;
|
||||
import std::ivec;
|
||||
import std::option::*;
|
||||
import std::vec;
|
||||
import std::vec::len;
|
||||
import std::vec::slice;
|
||||
import aux::constr_arg_use;
|
||||
import aux::local_node_id_to_def;
|
||||
import aux::fn_ctxt;
|
||||
@ -70,7 +69,8 @@ fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
|
||||
for (@constr_arg_use cau in args) {
|
||||
cau_ivec += ~[cau];
|
||||
}
|
||||
ret match_args(fcx, *descs, cau_ivec);
|
||||
auto d = *descs;
|
||||
ret match_args(fcx, d, cau_ivec);
|
||||
}
|
||||
case (_) {
|
||||
fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint,"
|
||||
@ -106,11 +106,11 @@ fn seq_tritv(&postcond p, &postcond q) {
|
||||
}
|
||||
}
|
||||
|
||||
fn seq_postconds(&fn_ctxt fcx, &vec[postcond] ps) -> postcond {
|
||||
auto sz = vec::len(ps);
|
||||
fn seq_postconds(&fn_ctxt fcx, &postcond[] ps) -> postcond {
|
||||
auto sz = ivec::len(ps);
|
||||
if (sz >= 1u) {
|
||||
auto prev = tritv_clone(ps.(0));
|
||||
for (postcond p in slice(ps, 1u, sz)) {
|
||||
for (postcond p in ivec::slice(ps, 1u, sz)) {
|
||||
seq_tritv(prev, p);
|
||||
}
|
||||
ret prev;
|
||||
@ -124,14 +124,14 @@ fn seq_postconds(&fn_ctxt fcx, &vec[postcond] ps) -> postcond {
|
||||
// return the precondition for evaluating each expr in order.
|
||||
// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
|
||||
// precondition shouldn't include x.
|
||||
fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond {
|
||||
let uint sz = len(pps);
|
||||
fn seq_preconds(&fn_ctxt fcx, &pre_and_post[] pps) -> precond {
|
||||
let uint sz = ivec::len(pps);
|
||||
let uint num_vars = num_constraints(fcx.enclosing);
|
||||
|
||||
fn seq_preconds_go(&fn_ctxt fcx, &vec[pre_and_post] pps,
|
||||
fn seq_preconds_go(&fn_ctxt fcx, &pre_and_post[] pps,
|
||||
&pre_and_post first)
|
||||
-> precond {
|
||||
let uint sz = len(pps);
|
||||
let uint sz = ivec::len(pps);
|
||||
if (sz >= 1u) {
|
||||
auto second = pps.(0);
|
||||
assert (pps_len(second) == num_constraints(fcx.enclosing));
|
||||
@ -141,7 +141,7 @@ fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond {
|
||||
union(next_first, second_pre);
|
||||
auto next_first_post = clone(first.postcondition);
|
||||
seq_tritv(next_first_post, second.postcondition);
|
||||
ret seq_preconds_go(fcx, slice(pps, 1u, sz),
|
||||
ret seq_preconds_go(fcx, ivec::slice(pps, 1u, sz),
|
||||
@rec(precondition=next_first,
|
||||
postcondition=next_first_post));
|
||||
}
|
||||
@ -153,7 +153,7 @@ fn seq_preconds(&fn_ctxt fcx, &vec[pre_and_post] pps) -> precond {
|
||||
if (sz >= 1u) {
|
||||
auto first = pps.(0);
|
||||
assert (pps_len(first) == num_vars);
|
||||
ret seq_preconds_go(fcx, slice(pps, 1u, sz), first);
|
||||
ret seq_preconds_go(fcx, ivec::slice(pps, 1u, sz), first);
|
||||
} else { ret true_precond(num_vars); }
|
||||
}
|
||||
|
||||
|
@ -46,11 +46,15 @@ fn collect_pred(&@expr e, &ctxt cx, &visit::vt[ctxt] v) {
|
||||
// If it's a call, generate appropriate instances of the
|
||||
// call's constraints.
|
||||
case (expr_call(?operator, ?operands)) {
|
||||
// FIXME: Remove this vec->ivec conversion.
|
||||
auto operands_ivec = ~[];
|
||||
for (@expr opd in operands) { operands_ivec += ~[opd]; }
|
||||
|
||||
for (@ty::constr_def c in constraints_expr(cx.tcx, operator)) {
|
||||
let aux::constr ct = respan(c.span,
|
||||
rec(id=c.node.id._1,
|
||||
c=aux::substitute_constr_args(cx.tcx,
|
||||
operands, c)));
|
||||
operands_ivec, c)));
|
||||
vec::push(*cx.cs, ct);
|
||||
}
|
||||
}
|
||||
@ -93,18 +97,17 @@ fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) ->
|
||||
" as a variable and a pred");
|
||||
}
|
||||
case (cpred(_, ?pds)) {
|
||||
vec::push(*pds,
|
||||
respan(c.span,
|
||||
rec(args=args, bit_num=next)));
|
||||
*pds += ~[respan(c.span,
|
||||
rec(args=args, bit_num=next))];
|
||||
}
|
||||
}
|
||||
}
|
||||
case (none) {
|
||||
tbl.insert(c.node.id,
|
||||
cpred(p,
|
||||
@mutable [respan(c.span,
|
||||
rec(args=args,
|
||||
bit_num=next))]));
|
||||
@mutable ~[respan(c.span,
|
||||
rec(args=args,
|
||||
bit_num=next))]));
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -134,7 +137,7 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &vec[ty_param] tp,
|
||||
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);
|
||||
let @mutable vec[node_id] v = @mutable [];
|
||||
let @mutable node_id[] v = @mutable ~[];
|
||||
auto rslt =
|
||||
rec(constrs=res_map,
|
||||
num_constraints=vec::len(*cx.cs) + 1u,
|
||||
|
@ -1,4 +1,5 @@
|
||||
|
||||
import std::ivec;
|
||||
import std::vec;
|
||||
import std::vec::plus_option;
|
||||
import std::option;
|
||||
@ -110,7 +111,7 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) {
|
||||
alt (i.node) {
|
||||
case (item_const(_, ?e)) {
|
||||
// make a fake fcx
|
||||
let @mutable vec[node_id] v = @mutable [];
|
||||
let @mutable node_id[] v = @mutable ~[];
|
||||
auto fake_fcx =
|
||||
rec(enclosing=rec(constrs=@new_int_hash[constraint](),
|
||||
num_constraints=0u,
|
||||
@ -163,9 +164,13 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, node_id id) {
|
||||
}
|
||||
auto g = bind get_pp(fcx.ccx, _);
|
||||
auto pps = vec::map[@expr, pre_and_post](g, args);
|
||||
auto h = get_post;
|
||||
set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
|
||||
seq_postconds(fcx, vec::map(h, pps)));
|
||||
|
||||
// TODO: Remove this vec->ivec conversion.
|
||||
auto pps_ivec = ~[];
|
||||
for (pre_and_post pp in pps) { pps_ivec += ~[pp]; }
|
||||
|
||||
set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps_ivec),
|
||||
seq_postconds(fcx, ivec::map(get_post, pps_ivec)));
|
||||
}
|
||||
|
||||
fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
|
||||
@ -179,10 +184,8 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
|
||||
// so we pretend they're used
|
||||
use_var(fcx, l.node.id);
|
||||
|
||||
auto loop_precond =
|
||||
seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, index),
|
||||
block_pp(fcx.ccx, body)]);
|
||||
auto loop_precond = seq_preconds(fcx, ~[expr_pp(fcx.ccx, index),
|
||||
block_pp(fcx.ccx, body)]);
|
||||
auto loop_postcond = intersect_states(expr_postcond(fcx.ccx, index),
|
||||
block_postcond(fcx.ccx, body));
|
||||
copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
|
||||
@ -205,10 +208,8 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
|
||||
case (_) {}
|
||||
}
|
||||
|
||||
auto precond_res =
|
||||
seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, antec),
|
||||
block_pp(fcx.ccx, conseq)]);
|
||||
auto precond_res = seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec), block_pp(fcx.ccx, conseq)]);
|
||||
set_pre_and_post(fcx.ccx, id, precond_res,
|
||||
expr_poststate(fcx.ccx, antec));
|
||||
}
|
||||
@ -219,13 +220,11 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
|
||||
is *not* true in the alternative
|
||||
*/
|
||||
find_pre_post_expr(fcx, altern);
|
||||
auto precond_false_case =
|
||||
seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, antec),
|
||||
expr_pp(fcx.ccx, altern)]);
|
||||
auto postcond_false_case =
|
||||
seq_postconds(fcx, [expr_postcond(fcx.ccx, antec),
|
||||
expr_postcond(fcx.ccx, altern)]);
|
||||
auto precond_false_case = seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
|
||||
auto postcond_false_case = seq_postconds(fcx,
|
||||
~[expr_postcond(fcx.ccx, antec),
|
||||
expr_postcond(fcx.ccx, altern)]);
|
||||
|
||||
/* Be sure to set the bit for the check condition here,
|
||||
so that it's *not* set in the alternative. */
|
||||
@ -236,17 +235,14 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
|
||||
}
|
||||
case (_) {}
|
||||
}
|
||||
auto precond_true_case =
|
||||
seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, antec),
|
||||
block_pp(fcx.ccx, conseq)]);
|
||||
auto postcond_true_case =
|
||||
seq_postconds(fcx, [expr_postcond(fcx.ccx, antec),
|
||||
block_postcond(fcx.ccx, conseq)]);
|
||||
auto precond_true_case = seq_preconds(fcx,
|
||||
~[expr_pp(fcx.ccx, antec), block_pp(fcx.ccx, conseq)]);
|
||||
auto postcond_true_case = seq_postconds(fcx,
|
||||
~[expr_postcond(fcx.ccx, antec),
|
||||
block_postcond(fcx.ccx, conseq)]);
|
||||
|
||||
auto precond_res =
|
||||
seq_postconds(fcx, [precond_true_case,
|
||||
precond_false_case]);
|
||||
auto precond_res = seq_postconds(fcx, ~[precond_true_case,
|
||||
precond_false_case]);
|
||||
auto postcond_res =
|
||||
intersect_states(postcond_true_case, postcond_false_case);
|
||||
set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
|
||||
@ -286,6 +282,11 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
case (expr_call(?operator, ?operands)) {
|
||||
auto args = vec::clone(operands);
|
||||
vec::push(args, operator);
|
||||
|
||||
// TODO: Remove this vec->ivec conversion.
|
||||
auto operands_ivec = ~[];
|
||||
for (@expr e in operands) { operands_ivec += ~[e]; }
|
||||
|
||||
find_pre_post_exprs(fcx, args, e.id);
|
||||
/* see if the call has any constraints on its type */
|
||||
for (@ty::constr_def c in constraints_expr(fcx.ccx.tcx, operator))
|
||||
@ -294,7 +295,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
bit_num(fcx,
|
||||
rec(id=c.node.id._1,
|
||||
c=substitute_constr_args(fcx.ccx.tcx,
|
||||
operands, c)));
|
||||
operands_ivec,
|
||||
c)));
|
||||
require(i, expr_pp(fcx.ccx, e));
|
||||
}
|
||||
|
||||
@ -440,7 +442,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
find_pre_post_expr(fcx, l);
|
||||
find_pre_post_expr(fcx, r);
|
||||
auto overall_pre = seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
|
||||
~[expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
|
||||
set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
||||
overall_pre);
|
||||
set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
|
||||
@ -465,20 +467,18 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
find_pre_post_expr(fcx, test);
|
||||
find_pre_post_block(fcx, body);
|
||||
set_pre_and_post(fcx.ccx, e.id,
|
||||
seq_preconds(fcx,
|
||||
[expr_pp(fcx.ccx, test),
|
||||
block_pp(fcx.ccx, body)]),
|
||||
seq_preconds(fcx, ~[expr_pp(fcx.ccx, test),
|
||||
block_pp(fcx.ccx, body)]),
|
||||
intersect_states(expr_postcond(fcx.ccx, test),
|
||||
block_postcond(fcx.ccx,
|
||||
body)));
|
||||
block_postcond(fcx.ccx, body)));
|
||||
}
|
||||
case (expr_do_while(?body, ?test)) {
|
||||
find_pre_post_block(fcx, body);
|
||||
find_pre_post_expr(fcx, test);
|
||||
auto loop_postcond =
|
||||
seq_postconds(fcx, [block_postcond(fcx.ccx, body),
|
||||
expr_postcond(fcx.ccx, test)]);
|
||||
/* conservative approximination: if the body
|
||||
auto loop_postcond = seq_postconds(fcx,
|
||||
~[block_postcond(fcx.ccx, body),
|
||||
expr_postcond(fcx.ccx, test)]);
|
||||
/* conservative approximation: if the body
|
||||
could break or cont, the test may never be executed */
|
||||
|
||||
if (has_nonlocal_exits(body)) {
|
||||
@ -486,8 +486,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
}
|
||||
set_pre_and_post(fcx.ccx, e.id,
|
||||
seq_preconds(fcx,
|
||||
[block_pp(fcx.ccx, body),
|
||||
expr_pp(fcx.ccx, test)]),
|
||||
~[block_pp(fcx.ccx, body),
|
||||
expr_pp(fcx.ccx, test)]),
|
||||
loop_postcond);
|
||||
}
|
||||
case (expr_for(?d, ?index, ?body)) {
|
||||
@ -509,7 +509,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
|
||||
auto alt_pps = vec::map[arm, pre_and_post](f, alts);
|
||||
fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp,
|
||||
&pre_and_post next) -> pre_and_post {
|
||||
union(pp.precondition, seq_preconds(fcx, [antec, next]));
|
||||
union(pp.precondition, seq_preconds(fcx, ~[antec, next]));
|
||||
intersect(pp.postcondition, next.postcondition);
|
||||
ret pp;
|
||||
}
|
||||
@ -664,27 +664,23 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) {
|
||||
fn do_inner_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); }
|
||||
auto do_inner = bind do_inner_(fcx, _);
|
||||
option::map[@expr, ()](do_inner, b.node.expr);
|
||||
let vec[pre_and_post] pps = [];
|
||||
fn get_pp_stmt(crate_ctxt ccx, &@stmt s) -> pre_and_post {
|
||||
ret stmt_pp(ccx, *s);
|
||||
|
||||
let pre_and_post[] pps = ~[];
|
||||
for (@stmt s in b.node.stmts) { pps += ~[stmt_pp(fcx.ccx, *s)]; }
|
||||
alt (b.node.expr) {
|
||||
case (none) { /* no-op */ }
|
||||
case (some(?e)) { pps += ~[expr_pp(fcx.ccx, e)]; }
|
||||
}
|
||||
auto f = bind get_pp_stmt(fcx.ccx, _);
|
||||
pps += vec::map[@stmt, pre_and_post](f, b.node.stmts);
|
||||
fn get_pp_expr(crate_ctxt ccx, &@expr e) -> pre_and_post {
|
||||
ret expr_pp(ccx, e);
|
||||
}
|
||||
auto g = bind get_pp_expr(fcx.ccx, _);
|
||||
plus_option[pre_and_post](pps,
|
||||
option::map[@expr,
|
||||
pre_and_post](g, b.node.expr));
|
||||
|
||||
auto block_precond = seq_preconds(fcx, pps);
|
||||
auto h = get_post;
|
||||
auto postconds = vec::map[pre_and_post, postcond](h, pps);
|
||||
|
||||
auto postconds = ~[];
|
||||
for (pre_and_post pp in pps) { postconds += ~[get_post(pp)]; }
|
||||
|
||||
/* A block may be empty, so this next line ensures that the postconds
|
||||
vector is non-empty. */
|
||||
postconds += ~[block_precond];
|
||||
|
||||
vec::push[postcond](postconds, block_precond);
|
||||
auto block_postcond = empty_poststate(nv);
|
||||
/* conservative approximation */
|
||||
|
||||
|
@ -240,11 +240,11 @@ fn tritv_doesntcare(&t v) -> bool {
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn to_vec(&t v) -> vec[uint] {
|
||||
fn to_vec(&t v) -> uint[] {
|
||||
let uint i = 0u;
|
||||
let vec[uint] rslt = [];
|
||||
let uint[] rslt = ~[];
|
||||
while (i < v.nbits) {
|
||||
rslt += [alt (tritv_get(v, i)) {
|
||||
rslt += ~[alt (tritv_get(v, i)) {
|
||||
case (dont_care) { 2u }
|
||||
case (ttrue) { 1u }
|
||||
case (tfalse) { 0u } }];
|
||||
|
Loading…
Reference in New Issue
Block a user