Refactor some typestate-related data structures

6 files changed, 142 insertions, 143 deletions

diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index d5d48bd67f8..9b5c44bc6ad 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 8ae65c5063f..52bde20f89c 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 9ba06711cd9..27e885e66d8 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 cda6405785c..e6691fce48f 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 5771b0fff7c..5eafeb8a1a5 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 2b2bfa01a42..e89fd1a6a83 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 (_) { }
                 }