Track spans for each local variable in typestate

This lets us print better messages in situations with name
shadowing.

Author: catamorphism

src/comp/middle/tstate/annotate.rs

@@ -91,14 +91,15 @@ fn collect_ids_decl(&@decl d, @vec[uint] res) -> () {
     }
 }
 
-fn node_ids_in_fn(&_fn f, &ident i, &def_id d, &ann a, @vec[uint] res) -> () {
+fn node_ids_in_fn(&_fn f, &span sp, &ident i, &def_id d, &ann a,
+                  @vec[uint] res) -> () {
     auto collect_ids = walk::default_visitor();
     collect_ids = rec(visit_expr_pre  = bind collect_ids_expr(_,res),
                       visit_block_pre = bind collect_ids_block(_,res),
                       visit_stmt_pre  = bind collect_ids_stmt(_,res),
                       visit_decl_pre  = bind collect_ids_decl(_,res)
                       with collect_ids);
-    walk::walk_fn(collect_ids, f, i, d, a);
+    walk::walk_fn(collect_ids, f, sp, i, d, a);
 }
 
 fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
@@ -108,23 +109,24 @@ fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
     }
 }
 
-fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f, &ident i,
-            &def_id d, &ann a) -> () {
+fn visit_fn(&crate_ctxt ccx, uint num_locals, &_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, i, d, a, node_ids);
+    node_ids_in_fn(f, sp, i, d, a, node_ids);
     init_vecs(ccx, node_ids, num_locals);
 }
 
-fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &ident i, &def_id f_id, &ann a)
+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, i, f_id, a);
+    visit_fn(ccx, num_locals(f_info), f, sp, i, f_id, a);
 }
 
 fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
     auto do_ann = walk::default_visitor();
-    do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx,_,_,_,_)
+    do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx,_,_,_,_,_)
                  with do_ann);
     walk::walk_crate(do_ann, crate);
 }

src/comp/middle/tstate/auxiliary.rs

@@ -18,7 +18,6 @@ import front::ast::expr_path;
 import front::ast::ident;
 import front::ast::controlflow;
 import front::ast::ann;
-import front::ast::ts_ann;
 import front::ast::stmt;
 import front::ast::expr;
 import front::ast::block;
@@ -54,26 +53,60 @@ import tstate::ann::extend_prestate;
 import tstate::ann::extend_poststate;
 import tstate::ann::set_precondition;
 import tstate::ann::set_postcondition;
+import tstate::ann::ts_ann;
+
+import util::common::istr;
 
 /* logging funs */
 
-fn bitv_to_str(fn_info enclosing, bitv::t v) -> str {
+fn def_id_to_str(def_id d) -> str {
+   ret (istr(d._0) + "," + istr(d._1));
+}
+
+fn bitv_to_str(fn_ctxt fcx, bitv::t v) -> str {
   auto s = "";
+  auto comma = false;
 
-  for each (@tup(def_id, tup(uint, ident)) p in enclosing.vars.items()) {
-    if (bitv::get(v, p._1._0)) {
-      s += " " + p._1._1 + " ";
-    }
+  for each (@tup(def_id, var_info) p in fcx.enclosing.vars.items()) {
+      if (bitv::get(v, p._1.bit_num)) {
+          s += (if (comma) { ", " } else { comma = true; "" })
+               + p._1.name + " [" + fcx.ccx.tcx.sess.span_str(p._1.sp) + "]";
+      }
   }
   ret s;
 }
 
-fn log_bitv(fn_info enclosing, bitv::t v) {
-    log(bitv_to_str(enclosing, v));
+fn log_bitv(fn_ctxt fcx, bitv::t v) {
+    log(bitv_to_str(fcx, v));
+}
+
+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()) {
+        if (!done) {
+            if (bitv::get(expected, p._1.bit_num) &&
+                !bitv::get(actual, p._1.bit_num)) {
+                
+            /*
+              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) + "]");
+            
+            done = true;
+            }
+        }
+    }
+    ret s;
 }
 
-fn log_bitv_err(fn_info enclosing, bitv::t v) {
-    log_err(bitv_to_str(enclosing, v));
+fn log_bitv_err(fn_ctxt fcx, bitv::t v) {
+    log_err(bitv_to_str(fcx, v));
 }
 
 fn tos (vec[uint] v) -> str {
@@ -152,8 +185,10 @@ fn print_idents(vec[ident] idents) -> () {
 /**********************************************************************/
 /* 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 for error-logging purposes) */
-type var_info     = tup(uint, ident);
+   (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);
 

src/comp/middle/tstate/bitvectors.rs

@@ -33,7 +33,7 @@ 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)._0;
+  ret m.vars.get(v).bit_num;
 }
 
 fn promises(&poststate p, def_id v, fn_info m) -> bool {
@@ -44,26 +44,26 @@ fn promises(&poststate p, def_id v, fn_info m) -> bool {
 // 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_info enclosing, vec[pre_and_post] pps) -> precond {
+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(enclosing);
+  let uint num_vars = num_locals(fcx.enclosing);
 
   if (sz >= 1u) {
     auto first = pps.(0);
     assert (pps_len(first) == num_vars);
-    let precond rest = seq_preconds(enclosing,
+    let precond rest = seq_preconds(fcx,
                          slice[pre_and_post](pps, 1u, sz));
     difference(rest, first.postcondition);
     auto res = clone(first.precondition);
     union(res, rest);
 
     log("seq_preconds:");
     log("first.postcondition =");
-    log_bitv(enclosing, first.postcondition);
+    log_bitv(fcx, first.postcondition);
     log("rest =");
-    log_bitv(enclosing, rest);
+    log_bitv(fcx, rest);
     log("returning");
-    log_bitv(enclosing, res);
+    log_bitv(fcx, res);
 
     ret res;
   }
@@ -118,14 +118,14 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
 fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "gen";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
 }
 
 fn declare_var(&fn_info enclosing, def_id id, prestate pre)
    -> prestate {
     assert (enclosing.vars.contains_key(id));
-    let uint i = (enclosing.vars.get(id))._0;
+    let uint i = (enclosing.vars.get(id)).bit_num;
     auto res = clone(pre);
     relax_prestate(i, res);
     ret res;
@@ -134,14 +134,14 @@ fn declare_var(&fn_info enclosing, def_id id, prestate pre)
 fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "gen_poststate";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 
 fn kill_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
   log "kill_poststate";
   assert (fcx.enclosing.vars.contains_key(id));
-  let uint i = (fcx.enclosing.vars.get(id))._0;
+  let uint i = (fcx.enclosing.vars.get(id)).bit_num;
   ret clear_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
 }
 

src/comp/middle/tstate/ck.rs

@@ -53,6 +53,7 @@ import aux::stmt_to_ann;
 import aux::num_locals;
 import aux::fixed_point_states;
 import aux::bitv_to_str;
+import aux::first_difference_string;
 
 import util::common::ty_to_str;
 import util::common::log_stmt_err;
@@ -70,12 +71,14 @@ fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
 
     if (!implies(pres, prec)) {
         auto s = "";
-        s += ("Unsatisfied precondition constraint for expression:\n");
+        auto diff = first_difference_string(fcx, prec, pres);
+        s += ("Unsatisfied precondition constraint (for example, "
+              + diff + ") for expression:\n");
         s += util::common::expr_to_str(e);
         s += ("\nPrecondition:\n");
-        s += bitv_to_str(fcx.enclosing, prec);
+        s += bitv_to_str(fcx, prec);
         s += ("\nPrestate:\n");
-        s += bitv_to_str(fcx.enclosing, pres);
+        s += bitv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_err(e.span, s);
     }
 }
@@ -96,12 +99,14 @@ fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
 
     if (!implies(pres, prec)) {
         auto ss = "";
-        ss += ("Unsatisfied precondition constraint for statement:\n");
+        auto diff = first_difference_string(fcx, prec, pres);
+        ss += ("Unsatisfied precondition constraint (for example, "
+              + diff + ") for statement:\n");
         ss += util::common::stmt_to_str(s);
         ss += ("\nPrecondition:\n");
-        ss += bitv_to_str(fcx.enclosing, prec);
+        ss += bitv_to_str(fcx, prec);
         ss += ("\nPrestate: \n");
-        ss += bitv_to_str(fcx.enclosing, pres);
+        ss += bitv_to_str(fcx, pres);
         fcx.ccx.tcx.sess.span_err(s.span, ss);
     }
 }
@@ -162,7 +167,8 @@ fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) -> () {
     check_states_against_conditions(fcx, f, a);
 }
 
-fn fn_states(&crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
+fn fn_states(&crate_ctxt ccx, &_fn f, &span sp, &ident i,
+             &def_id id, &ann a) -> () {
     /* Look up the var-to-bit-num map for this function */
     assert (ccx.fm.contains_key(id));
     auto f_info = ccx.fm.get(id);
@@ -171,6 +177,8 @@ fn fn_states(&crate_ctxt ccx, &_fn f, &ident i, &def_id id, &ann a) -> () {
     check_fn_states(fcx, f, a);
 }
 
+
+
 fn check_crate(ty::ctxt cx, @crate crate) -> () {
     let crate_ctxt ccx = new_crate_ctxt(cx);
 
@@ -182,14 +190,14 @@ fn check_crate(ty::ctxt cx, @crate crate) -> () {
 
     /* Compute the pre and postcondition for every subexpression */
     auto do_pre_post = walk::default_visitor();
-    do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx,_,_,_,_)
+    do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx,_,_,_,_,_)
                       with do_pre_post);
     walk::walk_crate(do_pre_post, *crate);
 
     /* Check the pre- and postcondition against the pre- and poststate
        for every expression */
     auto do_states = walk::default_visitor();
-    do_states = rec(visit_fn_pre = bind fn_states(ccx,_,_,_,_)
+    do_states = rec(visit_fn_pre = bind fn_states(ccx,_,_,_,_,_)
                     with do_states);
     walk::walk_crate(do_states, *crate);
 }

src/comp/middle/tstate/collect_locals.rs

@@ -23,6 +23,7 @@ import front::ast::ident;
 import middle::walk::walk_crate;
 import middle::walk::walk_fn;
 import middle::walk::ast_visitor;
+import front::ast::span;
 
 import aux::fn_info;
 import aux::var_info;
@@ -31,39 +32,44 @@ import aux::crate_ctxt;
 import util::common::new_def_hash;
 import util::common::uistr;
 
+type identifier = rec(ident name, def_id id, span sp);
+
 fn var_is_local(def_id v, fn_info m) -> bool {
   ret (m.vars.contains_key(v));
 }
 
-fn collect_local(&@vec[tup(ident, def_id)] vars, &@decl d) -> () {
+fn collect_local(&@vec[identifier] vars, &@decl d) -> () {
     alt (d.node) {
       case (decl_local(?loc)) {
         log("collect_local: pushing " + loc.ident);
-        vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
+        vec::push[identifier](*vars, rec(name=loc.ident,
+                                         id=loc.id,
+                                         sp=d.span));
       }
       case (_) { ret; }
     }
 }
 
-fn find_locals(&_fn f, &ident i, &def_id d, &ann a)
-    -> @vec[tup(ident,def_id)] {
-  auto res = @vec::alloc[tup(ident,def_id)](0u);
+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, i, d, a);
+  walk_fn(visitor, f, sp, i, d, a);
   ret res;
 }
 
 
-fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+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, tup(next,nm));
+  tbl.vars.insert(v, rec(bit_num=next, name=nm, sp=sp));
   ret (next + 1u);
 }
 
 /* builds a table mapping each local var defined in f
    to a bit number in the precondition/postcondition vectors */
-fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
+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);
@@ -73,15 +79,15 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
     /* ignore args, which we know are initialized;
        just collect locally declared vars */
 
-    let @vec[tup(ident,def_id)] locals = find_locals(f, f_name, f_id, a);
-    for (tup(ident,def_id) p in *locals) {
-        next = add_var(p._1, p._0, next, res);
+    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);
     }
     /* 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_name, next, res);
+    add_var(f_id, f_sp, f_name, next, res);
 
-    log(f_name + " has " + uistr(vec::len[tup(ident, def_id)](*locals))
+    log(f_name + " has " + uistr(vec::len[identifier](*locals))
             + " locals");
 
     ccx.fm.insert(f_id, res);
@@ -92,7 +98,7 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ident f_name, &def_id f_id, &ann a)
    to bit number) */
 fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) -> () {
   let ast_visitor vars_visitor = walk::default_visitor();
-  vars_visitor = rec(visit_fn_pre=bind mk_fn_info(ccx,_,_,_,_)
+  vars_visitor = rec(visit_fn_pre=bind mk_fn_info(ccx,_,_,_,_,_)
                      with vars_visitor);
 
   walk_crate(vars_visitor, *c);