Redo typestate-related data structures to support predicate constraints. No actual support yet, just infrastructure.

8 files changed, 473 insertions, 147 deletions

diff --git a/src/comp/middle/tstate/annotate.rs b/src/comp/middle/tstate/annotate.rs
index cd820ba2885..e49262e05af 100644
--- a/src/comp/middle/tstate/annotate.rs
+++ b/src/comp/middle/tstate/annotate.rs
@@ -51,7 +51,7 @@ import util::common::log_stmt;
 
 import aux::fn_info;
 import aux::fn_info_map;
-import aux::num_locals;
+import aux::num_constraints;
 import aux::get_fn_info;
 import aux::crate_ctxt;
 import aux::add_node;
@@ -109,19 +109,19 @@ fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
     }
 }
 
-fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f,
+fn visit_fn(&crate_ctxt ccx, uint num_constraints, &_fn f,
             &span sp, &ident i, &def_id d, &ann a) -> () {
     let vec[uint] node_ids_ = [];
     let @vec[uint] node_ids = @node_ids_;
     node_ids_in_fn(f, sp, i, d, a, node_ids);
-    init_vecs(ccx, node_ids, num_locals);
+    init_vecs(ccx, node_ids, num_constraints);
 }
 
 fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &span sp, &ident i,
                   &def_id f_id, &ann a)
     -> () {
     auto f_info = get_fn_info(ccx, f_id);
-    visit_fn(ccx, num_locals(f_info), f, sp, i, f_id, a);
+    visit_fn(ccx, num_constraints(f_info), f, sp, i, f_id, a);
 }
 
 fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 9f78504b737..4aa178d6c5c 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -8,35 +8,21 @@ import std::option::none;
 import std::option::some;
 import std::option::maybe;
 
-import front::ast;
-import front::ast::def;
-import front::ast::def_fn;
-import front::ast::_fn;
-import front::ast::def_obj_field;
-import front::ast::def_id;
-import front::ast::expr_path;
-import front::ast::ident;
-import front::ast::controlflow;
-import front::ast::ann;
-import front::ast::stmt;
-import front::ast::expr;
-import front::ast::block;
-import front::ast::block_;
-import front::ast::stmt_decl;
-import front::ast::stmt_expr;
-import front::ast::stmt_crate_directive;
-import front::ast::return;
-import front::ast::expr_field;
+import front::ast::*;
 
 import middle::ty::expr_ann;
 
 import util::common;
 import util::common::span;
+import util::common::respan;
 import util::common::log_block;
 import util::common::new_def_hash;
 import util::common::new_uint_hash;
 import util::common::log_expr_err;
 import util::common::uistr;
+import util::common::lit_eq;
+import pretty::pprust::path_to_str;
+import pretty::pprust::lit_to_str;
 
 import tstate::ann::pre_and_post;
 import tstate::ann::pre_and_post_state;
@@ -63,14 +49,51 @@ fn def_id_to_str(def_id d) -> str {
    ret (istr(d._0) + "," + istr(d._1));
 }
 
+fn comma_str(vec[@constr_arg] args) -> str {
+    auto res = "";
+    auto comma = false;
+    for (@constr_arg a in args) {
+        if (comma) {
+            res += ", ";
+        }
+        else {
+            comma = true;
+        }
+        alt (a.node) {
+            case (carg_base) {
+                res += "*";
+            }
+            case (carg_ident(?i)) {
+                res += i;
+            }
+            case (carg_lit(?l)) {
+                res += lit_to_str(l);
+            }
+        }
+    }
+    ret res;
+}
+
+fn constraint_to_str(ty::ctxt tcx, constr c) -> str {
+    alt (c.node) {
+        case (ninit(?i)) {
+            ret "init(" + i + " [" + tcx.sess.span_str(c.span) + "])";
+        }
+        case (npred(?p, ?args)) {
+            ret path_to_str(p) + "(" + comma_str(args) + ")"
+                + "[" + tcx.sess.span_str(c.span) + "]";
+        }
+    }
+}
+
 fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
   auto s = "";
   auto comma = false;
 
-  for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
-      if (bitv::get(v, p._1.bit_num)) {
+  for (norm_constraint p in constraints(fcx)) {
+      if (bitv::get(v, p.bit_num)) {
           s += (if (comma) { ", " } else { comma = true; "" })
-               + p._1.name + " [" + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]";
+              + aux::constraint_to_str(fcx.ccx.tcx, p.c);
       }
   }
   ret s;
@@ -84,19 +107,19 @@ fn first_difference_string(&fn_ctxt fcx, &bitv::t expected,
                            &bitv::t actual) -> str {
     let str s = "";
     auto done = false;
-    for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
+    for (norm_constraint c in constraints(fcx)) {
         if (!done) {
-            if (bitv::get(expected, p._1.bit_num) &&
-                !bitv::get(actual, p._1.bit_num)) {
+            if (bitv::get(expected, c.bit_num) &&
+                !bitv::get(actual, c.bit_num)) {
                 
             /*
+              FIXME
               for fun, try either:
               * "ret s" after the assignment to s
               or
               * using break here
               */
-            s = (p._1.name + " ["
-                 + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]");
+                s = constraint_to_str(fcx.ccx.tcx, c.c);
             
             done = true;
             }
@@ -183,14 +206,35 @@ fn print_idents(vec[ident] idents) -> () {
 /* data structures */
 
 /**********************************************************************/
-/* mapping from variable name (def_id is assumed to be for a local
-   variable in a given function) to bit number 
-   (also remembers the ident and span for error-logging purposes) */
-type var_info     = rec(uint bit_num,
-                        ident name,
-                        span sp);
-type fn_info      = rec(@std::map::hashmap[def_id, var_info] vars,
-                        controlflow cf);
+/* mapping from def_id to bit number and other data
+   (ident/path/span are there for error-logging purposes) */
+
+type pred_desc_ = rec(vec[@constr_arg] args,
+                      uint bit_num);
+type pred_desc = spanned[pred_desc_];
+tag constraint {
+    cinit(uint, span, ident);
+    cpred(path, vec[pred_desc]);
+}
+tag constr_ {
+    ninit(ident);
+    npred(path, vec[@constr_arg]);
+}
+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]);
+}
+   
+type constr_map = @std::map::hashmap[def_id, constraint];
+
+type fn_info  = rec(constr_map constrs, uint num_constraints, controlflow cf);
 
 /* mapping from node ID to typestate annotation */
 type node_ann_table = @vec[ts_ann];
@@ -418,8 +462,8 @@ fn fixed_point_states(&fn_ctxt fcx,
   }
 }
 
-fn num_locals(fn_info m) -> uint {
-  ret m.vars.size();
+fn num_constraints(fn_info m) -> uint {
+    ret m.num_constraints;
 }
 
 fn new_crate_ctxt(ty::ctxt cx) -> crate_ctxt {
@@ -463,6 +507,89 @@ 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] {
+    alt (c) {
+        case (cinit(?n, ?sp, ?i)) {
+            ret [rec(bit_num=n, c=respan(sp, ninit(i)))];
+        }
+        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, pd.node.args))));
+            }
+            ret res;
+        }
+    }
+}
+
+// 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] res = [];
+    for each (@tup(def_id, constraint) p in
+              fcx.enclosing.constrs.items()) {
+        res += norm_a_constraint(p._1);
+    }
+    ret res;
+}
+
+fn arg_eq(@constr_arg a, @constr_arg b) -> bool {
+    alt (a.node) {
+        case (carg_base) {
+            alt (b.node) {
+                case (carg_base) {
+                    ret true;
+                }
+                case (_) {
+                    ret false;
+                }
+            }
+        }
+        case (carg_ident(?s)) {
+            alt (b.node) {
+                case (carg_ident(?t)) {
+                    ret (s == t);
+                }
+                case (_) {
+                    ret false;
+                }
+            }
+        }
+        case (carg_lit(?l)) {
+            alt (b.node) {
+                case (carg_lit(?m)) {
+                    ret lit_eq(l, m);
+                }
+                case (_) {
+                    ret false;
+                }
+            }
+        }
+    }
+}
+
+fn args_eq(vec[@constr_arg] a, vec[@constr_arg] b) -> bool {
+    let uint i = 0u;
+    for (@constr_arg arg in a) {
+        if (!arg_eq(arg, b.(i))) {
+            ret false;
+        }
+        i += 1u;
+    }
+    ret true;
+}
+
+fn match_args(&fn_ctxt fcx, vec[pred_desc] occs,
+              vec[@constr_arg] occ) -> uint {
+    for (pred_desc pd in occs) {
+        if (args_eq(pd.node.args, occ)) {
+            ret pd.node.bit_num;
+        }
+    }
+    fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");  
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs
index c3c79d68f57..0eb924eeaff 100644
--- a/src/comp/middle/tstate/bitvectors.rs
+++ b/src/comp/middle/tstate/bitvectors.rs
@@ -3,15 +3,19 @@ import std::vec;
 import std::vec::len;
 import std::vec::slice;
 
-import front::ast;
-import front::ast::def_id;
-import front::ast::expr;
-import front::ast::ann;
+import front::ast::*;
 
 import aux::fn_ctxt;
 import aux::fn_info;
 import aux::log_bitv;
-import aux::num_locals;
+import aux::num_constraints;
+import aux::constr_occ;
+import aux::occ_init;
+import aux::occ_args;
+import aux::cinit;
+import aux::cpred;
+import aux::pred_desc;
+import aux::match_args;
 
 import tstate::aux::ann_to_ts_ann;
 import tstate::ann::pre_and_post;
@@ -30,14 +34,38 @@ import tstate::ann::clone;
 import tstate::ann::set_in_postcond;
 import tstate::ann::set_in_poststate;
 import tstate::ann::clear_in_poststate;
-             
-fn bit_num(def_id v, fn_info m) -> uint {
-  assert (m.vars.contains_key(v));
-  ret m.vars.get(v).bit_num;
+           
+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) {
+            alt (res) {
+                case (cinit(?n,_,_)) {
+                    ret n;
+                }
+                case (_) {
+                    fcx.ccx.tcx.sess.bug("bit_num: asked for init constraint,"
+                                         + " found a pred constraint");
+                }
+            }
+        }
+        case (occ_args(?args)) {
+            alt (res) {
+                case (cpred(_, ?descs)) {
+                    ret match_args(fcx, descs, args);
+                }
+                case (_) {
+                    fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint,"
+                                         + " found an init constraint");
+                }
+            }
+        }
+    }
 }
 
-fn promises(&poststate p, def_id v, fn_info m) -> bool {
-    ret bitv::get(p, bit_num(v, m));
+fn promises(&fn_ctxt fcx, &poststate p, &def_id v, &constr_occ o) -> bool {
+    ret bitv::get(p, bit_num(fcx, v, o));
 }
 
 // Given a list of pres and posts for exprs e0 ... en,
@@ -46,7 +74,7 @@ fn promises(&poststate p, def_id v, fn_info m) -> bool {
 // precondition shouldn't include x.
 fn seq_preconds(fn_ctxt fcx, vec[pre_and_post] pps) -> precond {
   let uint sz = len[pre_and_post](pps);
-  let uint num_vars = num_locals(fcx.enclosing);
+  let uint num_vars = num_constraints(fcx.enclosing);
 
   if (sz >= 1u) {
     auto first = pps.(0);
@@ -115,33 +143,38 @@ 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) -> bool {
+fn gen(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
   log "gen";
-  assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
-  ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
+  ret set_in_postcond(bit_num(fcx, id, o),
+                      (ann_to_ts_ann(fcx.ccx, a)).conditions);
 }
 
-fn declare_var(&fn_info enclosing, def_id id, prestate pre)
+fn declare_var(&fn_ctxt fcx, def_id id, prestate pre)
    -> prestate {
-    assert (enclosing.vars.contains_key(id));
-    let uint i = (enclosing.vars.get(id)).bit_num;
     auto res = clone(pre);
-    relax_prestate(i, res);
+    relax_prestate(bit_num(fcx, id, occ_init), res);
     ret res;
 }
 
-fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+fn gen_poststate(&fn_ctxt fcx, &ann a, &def_id id, &constr_occ o) -> bool {
   log "gen_poststate";
-  assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
-  ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
+  ret set_in_poststate(bit_num(fcx, id, o),
+                       (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
-fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
+fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id, &constr_occ o) -> bool {
   log "kill_poststate";
-  assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
-  ret clear_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
+  ret clear_in_poststate(bit_num(fcx, id, o),
+                         (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 02da5d01bc8..9ba06711cd9 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -50,7 +50,7 @@ import aux::expr_prestate;
 import aux::expr_poststate;
 import aux::stmt_poststate;
 import aux::stmt_to_ann;
-import aux::num_locals;
+import aux::num_constraints;
 import aux::fixed_point_states;
 import aux::bitv_to_str;
 import aux::first_difference_string;
@@ -113,7 +113,7 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
 
 fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     auto enclosing = fcx.enclosing;
-    auto nv   = num_locals(enclosing);
+    auto nv   = num_constraints(enclosing);
     auto post = @empty_poststate(nv);
 
     fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post) -> () {
@@ -134,7 +134,7 @@ 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 */
     if (f.proto == ast::proto_fn
-        && ! promises(*post, fcx.id, enclosing)
+        && ! promises(fcx, *post, fcx.id, aux::occ_init)
         && ! type_is_nil(fcx.ccx.tcx,
                          ret_ty_of_fn(fcx.ccx.tcx, a))
         && cf == return) {
@@ -147,8 +147,8 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     else if (cf == noreturn) {
         // check that this really always fails
         // the fcx.id bit means "returns" for a returning fn,
-        // "diverges" for a non-returning fn (I need to use the word
-        if (! promises(*post, fcx.id, enclosing)) {
+        // "diverges" for a non-returning fn
+        if (! promises(fcx, *post, fcx.id, aux::occ_init)) {
             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 4c0308d1821..8be160a865a 100644
--- a/src/comp/middle/tstate/collect_locals.rs
+++ b/src/comp/middle/tstate/collect_locals.rs
@@ -1,69 +1,158 @@
 import std::vec;
 import std::vec::plus_option;
 
-import front::ast;
-import front::ast::crate;
-import front::ast::ann;
-import front::ast::arg;
-import front::ast::method;
-import front::ast::local;
-import front::ast::item;
-import front::ast::item_fn;
-import front::ast::item_obj;
-import front::ast::_obj;
-import front::ast::obj_def_ids;
-import front::ast::_fn;
-import front::ast::ty_param;
-import front::ast::_mod;
-import front::ast::decl;
-import front::ast::decl_local;
-import front::ast::def_id;
-import front::ast::ident;
+import front::ast::*;
+import option::*;
 
 import middle::walk::walk_crate;
 import middle::walk::walk_fn;
 import middle::walk::ast_visitor;
 
+import aux::cinit;
+import aux::ninit;
+import aux::npred;
+import aux::cpred;
+import aux::constraint;
 import aux::fn_info;
-import aux::var_info;
 import aux::crate_ctxt;
+import aux::num_constraints;
+import aux::constr_map;
 
 import util::common::new_def_hash;
 import util::common::uistr;
 import util::common::span;
+import util::common::respan;
 
-type identifier = rec(ident name, def_id id, span sp);
+type ctxt = rec(@vec[constraint_info] cs,
+                ty::ctxt tcx);
 
-fn var_is_local(def_id v, fn_info m) -> bool {
-  ret (m.vars.contains_key(v));
-}
+type constraint_info = rec(def_id id, aux::constr c);
 
-fn collect_local(&@vec[identifier] vars, &@decl d) -> () {
+fn collect_local(&ctxt cx, &@decl d) -> () {
     alt (d.node) {
       case (decl_local(?loc)) {
         log("collect_local: pushing " + loc.ident);
-        vec::push[identifier](*vars, rec(name=loc.ident,
-                                         id=loc.id,
-                                         sp=d.span));
+        vec::push[constraint_info](*cx.cs,
+                                   rec(id=loc.id,
+                                       c=respan(d.span,
+                                                ninit(loc.ident))));
       }
       case (_) { ret; }
     }
 }
 
-fn find_locals(&_fn f, &span sp, &ident i, &def_id d, &ann a)
-    -> @vec[identifier] {
-  auto res = @vec::alloc[identifier](0u);
-  auto visitor = walk::default_visitor();
-  visitor = rec(visit_decl_pre=bind collect_local(res,_) with visitor);
-  walk_fn(visitor, f, sp, i, d, a);
-  ret res;
+fn exprs_to_constr_args(ty::ctxt tcx, vec[@expr] args) -> vec[@constr_arg] {
+    fn one(ty::ctxt tcx, &@expr e) -> @constr_arg {
+        alt (e.node) {
+            case (expr_path(?p, _)) {
+                if (vec::len(p.node.idents) == 1u) {
+                    ret @respan(p.span, carg_ident(p.node.idents.(0)));
+                }
+                else {
+                    tcx.sess.bug("exprs_to_constr_args: non-local variable "
+                                 + "as pred arg");
+                }
+            }
+            case (expr_lit(?l, _)) {
+                ret @respan(e.span, carg_lit(l));
+            }
+            case (_) {
+                tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg");
+            }
+        }
+    }
+    auto f = bind one(tcx, _);
+    ret vec::map(f, args); 
 }
 
+fn def_id_for_constr(ty::ctxt tcx, uint t) -> def_id {
+    alt (tcx.def_map.find(t)) {
+        case (none) {
+            tcx.sess.bug("def_id_for_constr: bad node_id " + uistr(t));
+         }
+        case (some(def_fn(?i))) {
+            ret i;
+        }
+        case (_) {
+            tcx.sess.bug("def_id_for_constr: pred is not a function");
+        }
+    }
+}
 
-fn add_var(def_id v, span sp, ident nm, uint next, fn_info tbl) -> uint {
-  log(nm + " |-> " + util::common::uistr(next));
-  tbl.vars.insert(v, rec(bit_num=next, name=nm, sp=sp));
-  ret (next + 1u);
+fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constraint_info {
+    alt (e.node) {
+        // change the first pattern to expr_path to test a typechecker bug
+        case (expr_call(?operator, ?args, _)) {
+            alt (operator.node) {
+                case (expr_path(?p, ?a)) {
+                    ret rec(id=def_id_for_constr(tcx, a.id),
+                            c=respan(e.span,
+                                npred(p, exprs_to_constr_args(tcx, args)))); 
+                }
+                case (_) {
+                    tcx.sess.span_err(operator.span, "Internal error: " +
+                       " ill-formed operator in predicate");
+                }
+            }
+        }
+        case (_) {
+            tcx.sess.span_err(e.span, "Internal error: " +
+                              " ill-formed predicate");
+        }
+    }
+}
+
+fn collect_pred(&ctxt cx, &@expr e) -> () {
+    alt (e.node) {
+        case (expr_check(?e, _)) {
+            vec::push[constraint_info](*cx.cs, expr_to_constr(cx.tcx, e));
+        }
+        case (_) { }
+    }
+}
+
+fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a)
+    -> ctxt {
+    let ctxt cx = rec(cs=@vec::alloc[constraint_info](0u), tcx=tcx);
+    auto visitor = walk::default_visitor();
+    visitor = rec(visit_decl_pre=bind collect_local(cx,_),
+                  visit_expr_pre=bind collect_pred(cx,_)
+                  with visitor);
+    walk_fn(visitor, f, sp, i, d, a);
+    ret cx;
+}
+
+fn add_constraint(&ty::ctxt tcx, constraint_info c, uint next, constr_map tbl)
+    -> uint {
+    log(aux::constraint_to_str(tcx, c.c) + " |-> "
+        + util::common::uistr(next));
+    let aux::constr cn = c.c;
+    alt (cn.node) {
+        case (ninit(?i)) {
+            tbl.insert(c.id, cinit(next, cn.span, i));
+        }
+        case (npred(?p, ?args)) {
+            alt (tbl.find(c.id)) {
+                case (some[constraint](?ct)) {
+                    alt (ct) {
+                        case (cinit(_,_,_)) {
+                            tcx.sess.bug("add_constraint: same def_id used"
+                                         + " as a variable and a pred");
+                        }
+                        case (cpred(_, ?pds)) {
+                            vec::push(pds, respan(cn.span,
+                              rec(args=args, bit_num=next)));
+                        }
+                    }
+                }
+                case (none[constraint]) {
+                    tbl.insert(c.id, cpred(p,
+                      [respan(cn.span, rec(args=args, bit_num=next))]));
+                }
+            }
+        }
+    }
+    ret (next + 1u);
 }
 
 /* builds a table mapping each local var defined in f
@@ -71,26 +160,33 @@ fn add_var(def_id v, span sp, ident nm, uint next, fn_info tbl) -> uint {
 fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp,
               &ident f_name, &def_id f_id, &ann a)
     -> () {
-    auto res = rec(vars=@new_def_hash[var_info](),
-                   cf=f.decl.cf);
+    auto res_map = @new_def_hash[constraint]();
     let uint next = 0u;
     let vec[arg] f_args = f.decl.inputs;
 
     /* ignore args, which we know are initialized;
        just collect locally declared vars */
 
-    let @vec[identifier] locals = find_locals(f, f_sp, f_name, f_id, a);
-    for (identifier p in *locals) {
-        next = add_var(p.id, p.sp, p.name, next, res);
+    let ctxt cx = find_locals(ccx.tcx, f, f_sp, f_name, f_id, a);
+    /* now we have to add bit nums for both the constraints
+       and the variables... */
+
+    for (constraint_info 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_var(f_id, f_sp, f_name, next, res);
+    add_constraint(cx.tcx, rec(id=f_id,
+                               c=respan(f_sp, ninit(f_name))), next, res_map);
+    
+    auto res = rec(constrs=res_map,
+                            num_constraints=vec::len(*cx.cs) + 1u,
+                   cf=f.decl.cf);
 
-    log(f_name + " has " + uistr(vec::len[identifier](*locals))
-            + " locals");
-   
     ccx.fm.insert(f_id, res);
+    
+    log(f_name + " has " + uistr(num_constraints(res)) + " constraints");
+
 }
 
 /* initializes the global fn_info_map (mapping each function ID, including
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 37598763058..d1df649f7a6 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -17,10 +17,11 @@ import tstate::ann::pp_clone;
 import tstate::ann::empty_prestate;
 import tstate::ann::set_precondition;
 import tstate::ann::set_postcondition;
-import aux::var_info;
 import aux::crate_ctxt;
 import aux::fn_ctxt;
-import aux::num_locals;
+import aux::occ_init;
+import aux::num_constraints;
+import aux::constraint;
 import aux::expr_pp;
 import aux::stmt_pp;
 import aux::block_pp;
@@ -93,8 +94,10 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
     alt (i.node) {
         case (item_const(?id, ?t, ?e, ?di, ?a)) {
             // make a fake fcx
-            auto fake_fcx = rec(enclosing=rec(vars=@new_def_hash[var_info](),
-                                              cf=return),
+            auto fake_fcx = rec(enclosing=
+                rec(constrs=@new_def_hash[constraint](),
+                    num_constraints=0u,
+                    cf=return),
                                 id=tup(0,0),
                                 name="",
                                 ccx=ccx);
@@ -136,7 +139,7 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
 
     auto enclosing = fcx.enclosing;
     auto fm        = fcx.ccx.fm;
-    auto nv        = num_locals(enclosing);
+    auto nv        = num_constraints(enclosing);
 
     fn do_one(fn_ctxt fcx, &@expr e) -> () {
         find_pre_post_expr(fcx, e);
@@ -163,7 +166,7 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
     find_pre_post_expr(fcx, index);
     find_pre_post_block(fcx, body);
     log("222");
-    auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
+    auto loop_precond = declare_var(fcx, decl_lhs(d),
       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)]);
@@ -180,7 +183,7 @@ 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);
+                  gen(fcx, larger_ann, d_id, aux::occ_init);
               }
               case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
           }
@@ -192,13 +195,13 @@ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
 /* Fills in annotations as a side effect. Does not rebuild the expr */
 fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
     auto enclosing      = fcx.enclosing;
-    auto num_local_vars = num_locals(enclosing);
+    auto num_local_vars = num_constraints(enclosing);
 
     fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
         find_pre_post_expr(fcx, e);
     }
     
-    log("find_pre_post_expr (num_locals =" +
+    log("find_pre_post_expr (num_constraints =" +
         uistr(num_local_vars) + "):");
     log_expr(*e);
 
@@ -233,7 +236,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             auto df = ann_to_def_strict(fcx.ccx, a);
             alt (df) {
                 case (def_local(?d_id)) {
-                    auto i = bit_num(d_id, enclosing);
+                    auto i = bit_num(fcx, d_id, occ_init);
                     require_and_preserve(i, res);
                 }
                 case (_) { /* nothing to check */ }
@@ -511,7 +514,7 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
     log_stmt(s);
 
     auto enclosing      = fcx.enclosing;
-    auto num_local_vars = num_locals(enclosing);
+    auto num_local_vars = num_constraints(enclosing);
     alt(s.node) {
         case(stmt_decl(?adecl, ?a)) {
             alt(adecl.node) {
@@ -526,11 +529,11 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
                             copy_pre_post(fcx.ccx, a, an_init.expr);
                             /*  log("gen (decl):");
                                 log_stmt(s); */
-                            gen(fcx, a, alocal.id); 
-                            /*                     log_err("for stmt");
-                                                   log_stmt(s);
-                                                   log_err("pp = ");
-                                                   log_pp(stmt_pp(s)); */
+                            gen(fcx, a, alocal.id, occ_init); 
+                            /*  log_err("for stmt");
+                                log_stmt(s);
+                                log_err("pp = ");
+                                log_pp(stmt_pp(s)); */
                         }
                         case(none) {
                             clear_pp(ann_to_ts_ann(fcx.ccx,
@@ -569,7 +572,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
 
      won't have a postcondition that says x is initialized, but that's ok.
      */
-    auto nv = num_locals(fcx.enclosing);
+    auto nv = num_constraints(fcx.enclosing);
 
     fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
         find_pre_post_stmt(fcx, *s);
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 206ac9c68df..37cc40b5c9e 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -24,10 +24,9 @@ import tstate::ann::false_postcond;
 import tstate::ann::ts_ann;
 import tstate::ann::extend_prestate;
 import tstate::ann::extend_poststate;
-import aux::var_info;
 import aux::crate_ctxt;
 import aux::fn_ctxt;
-import aux::num_locals;
+import aux::num_constraints;
 import aux::expr_pp;
 import aux::stmt_pp;
 import aux::block_pp;
@@ -49,6 +48,7 @@ import aux::log_states;
 import aux::block_states;
 import aux::controlflow_expr;
 import aux::ann_to_def;
+import aux::occ_init;
 
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
@@ -121,7 +121,7 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
 fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
   alt (ann_to_def(fcx.ccx, a_new_var)) {
       case (some(def_local(?loc))) {
-          ret gen_poststate(fcx, a, loc);
+          ret gen_poststate(fcx, a, loc, occ_init);
       }
       case (_) { ret false; }
   }
@@ -129,7 +129,7 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
 
 fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
   auto changed = false;
-  auto num_local_vars = num_locals(fcx.enclosing);
+  auto num_local_vars = num_constraints(fcx.enclosing);
 
   /*  
   log_err("states:");
@@ -319,11 +319,14 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
 
     case (expr_ret(?maybe_ret_val, ?a)) {
         changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
+        /* normally, everything is true if execution continues after
+           a ret expression (since execution never continues locally
+           after a ret expression */
         set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
         /* return from an always-failing function clears the return bit */
         alt (fcx.enclosing.cf) {
             case (noreturn) {
-                kill_poststate(fcx, a, fcx.id);
+                kill_poststate(fcx, a, fcx.id, occ_init);
             }
             case (_) {}
         }
@@ -578,7 +581,8 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
                                 (stmt_ann.states.poststate,
                                  expr_poststate(fcx.ccx, an_init.expr))
                                 || changed;
-                            changed = gen_poststate(fcx, a, alocal.id)
+                            changed = gen_poststate(fcx, a,
+                                                    alocal.id, occ_init)
                                 || changed;
                             log("Summary: stmt = ");
                             log_stmt(*s);
@@ -642,7 +646,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
   -> bool {
     
   auto changed = false;
-  auto num_local_vars = num_locals(fcx.enclosing);
+  auto num_local_vars = num_constraints(fcx.enclosing);
 
   /* First, set the pre-states and post-states for every expression */
   auto pres = pres0;
@@ -694,7 +698,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
 }
 
 fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
-    auto num_local_vars = num_locals(fcx.enclosing);
+    auto num_local_vars = num_constraints(fcx.enclosing);
     auto changed = find_pre_post_state_block(fcx,
                      empty_prestate(num_local_vars), f.body);
 
@@ -715,7 +719,7 @@ 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);
+                        kill_poststate(fcx, tailann, fcx.id, occ_init);
                     }
                     case (_) { }
                 }
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 33b89eff26c..2435c2610e7 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -9,6 +9,8 @@ import front::ast;
 import front::ast::ty;
 import front::ast::pat;
 import front::codemap::codemap;
+import front::ast::lit;
+import front::ast::path;
 import middle::walk;
 
 import std::io::stdout;
@@ -17,9 +19,11 @@ import std::io::string_writer;
 import pretty::pprust::print_block;
 import pretty::pprust::print_item;
 import pretty::pprust::print_expr;
+import pretty::pprust::print_path;
 import pretty::pprust::print_decl;
 import pretty::pprust::print_fn;
 import pretty::pprust::print_type;
+import pretty::pprust::print_literal;
 import pretty::pprust::mo_untyped;
 import pretty::pp::mk_printer;
 
@@ -227,6 +231,65 @@ fn local_rhs_span(&@ast::local l, &span def) -> span {
     }
 }
 
+fn lit_eq(&@ast::lit l, &@ast::lit m) -> bool {
+    alt (l.node) {
+        case (ast::lit_str(?s)) {
+            alt (m.node) {
+                case (ast::lit_str(?t)) { ret s == t; }
+                case (_)           { ret false; }
+            }
+        }
+        case (ast::lit_char(?c)) {
+            alt (m.node) {
+                case (ast::lit_char(?d)) { ret c == d; }
+                case (_)           { ret false; }
+            }
+        }
+        case (ast::lit_int(?i)) {
+            alt (m.node) {
+                case (ast::lit_int(?j)) { ret i == j; }
+                case (_)           { ret false; }
+            }
+        }
+        case (ast::lit_uint(?i)) {
+            alt (m.node) {
+                case (ast::lit_uint(?j)) { ret i == j; }
+                case (_)            { ret false; }
+            }
+        }
+        case (ast::lit_mach_int(_, ?i)) {
+            alt (m.node) {
+                case (ast::lit_mach_int(_, ?j)) { ret i == j; }
+                case (_)                    { ret false; }
+            }
+        }
+        case (ast::lit_float(?s)) {
+            alt (m.node) {
+                case (ast::lit_float(?t)) { ret s == t; }
+                case (_)             { ret false; }
+            }
+        }
+        case (ast::lit_mach_float(_,?s)) {
+            alt (m.node) {
+                case (ast::lit_mach_float(_,?t)) { ret s == t; }
+                case (_)               { ret false; }
+            }
+        }
+        case (ast::lit_nil) {
+            alt (m.node) {
+                case (ast::lit_nil) { ret true; }
+                case (_)       { ret false; }
+            }
+        }
+        case (ast::lit_bool(?b)) {
+            alt (m.node) {
+                case (ast::lit_bool(?c)) { ret b == c; }
+                case (_)            { ret false; }
+            }
+        }
+    }
+}
+
 fn respan[T](&span sp, &T t) -> spanned[T] {
     ret rec(node=t, span=sp);
 }