about summary refs log tree commit diff
diff options
context:
space:
mode:
authorPatrick Walton <pcwalton@mimiga.net>2011-07-04 23:29:15 -0700
committerPatrick Walton <pcwalton@mimiga.net>2011-07-06 15:14:19 -0700
commitabab04635afa5f9d26799d2d2ae4e4bcc521f419 (patch)
treec0b0c79a33778bf910433270da1384158fdf765a
parent6d1517cf3aa05cc669a80306e653d715b7420561 (diff)
downloadrust-abab04635afa5f9d26799d2d2ae4e4bcc521f419.tar.gz
rust-abab04635afa5f9d26799d2d2ae4e4bcc521f419.zip
rustc: Move middle::tstate::auxiliary and middle::tstate::bitvectors over to interior vectors
-rw-r--r--src/comp/middle/tstate/auxiliary.rs91
-rw-r--r--src/comp/middle/tstate/bitvectors.rs24
-rw-r--r--src/comp/middle/tstate/collect_locals.rs19
-rw-r--r--src/comp/middle/tstate/pre_post_conditions.rs114
-rw-r--r--src/comp/middle/tstate/tritv.rs6
5 files changed, 131 insertions, 123 deletions
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 3b8d689bc46..861a0a945b6 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -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
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index 371cfc0580f..4353ef56cd4 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -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); }
 }
 
diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs
index 764c66e52a0..4a190b6f6ae 100644
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -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,
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index f58fdb0f6cf..8a65df496ff 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -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_res =
-                seq_postconds(fcx, [precond_true_case,
-                                    precond_false_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_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);
-    }
-    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);
+
+    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 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 */
 
diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs
index 90be1810301..59ad4461689 100644
--- a/src/comp/middle/tstate/tritv.rs
+++ b/src/comp/middle/tstate/tritv.rs
@@ -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 } }];