Further work on typestate_check

Lots of work on typestate_check, seems to get a lot of the way
through checking the standard library.

* Added for, for_each, assign_op, bind, cast, put, check, break,
and cont. (I'm not sure break and cont are actually handled correctly.)

* Fixed side-effect bug in seq_preconds so that unioning the
preconditions of a sequence of statements or expressions
is handled correctly.

* Pass poststate correctly through a stmt_decl.

* Handle expr_ret and expr_fail properly (after execution of a ret
or fail, everything is true -- this is needed to handle ifs and alts
where one branch is a ret or fail)

* Fixed bug in set_prestate_ann where a thing that needed to be
mutated wasn't getting passed as an alias

* Fixed bug in how expr_alt was treated (zero is not the identity
for intersect, who knew, right?)

* Update logging to reflect log_err vs. log

* Fixed find_locals so as to return all local decls and exclude
function arguments.

* Make union_postconds work on an empty vector (needed to handle
empty blocks correctly)

* Added _vec.cat_options, which takes a list of option[T] to a list
of T, ignoring any Nones

* Added two test cases.

2 files changed, 83 insertions, 12 deletions

diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index a9e02c20..d2ed72a0 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -98,9 +98,9 @@ fn uistr(uint i) -> str {
 
 fn elt_expr(&ast.elt e) -> @ast.expr { ret e.expr; }
 
-fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] {
+fn elt_exprs(&vec[ast.elt] elts) -> vec[@ast.expr] {
     auto f = elt_expr;
-    be _vec.map[ast.elt, @ast.expr](f, elts);
+    ret _vec.map[ast.elt, @ast.expr](f, elts);
 }
 
 fn field_expr(&ast.field f) -> @ast.expr { ret f.expr; }
@@ -115,18 +115,25 @@ fn plain_ann(middle.ty.ctxt tcx) -> ast.ann {
                    none[vec[middle.ty.t]], none[@ts_ann]);
 }
 
-fn log_expr(&ast.expr e) -> () {
+fn expr_to_str(&ast.expr e) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
                   comments=none[vec[front.lexer.cmnt]],
                   mutable cur_cmnt=0u);
-
   print_expr(out, @e);
-  log(s.get_str());
+  ret s.get_str();
 }
 
-fn log_block(&ast.block b) -> () {
+fn log_expr(&ast.expr e) -> () {
+    log(expr_to_str(e));
+}
+
+fn log_expr_err(&ast.expr e) -> () {
+    log_err(expr_to_str(e));
+}
+
+fn block_to_str(&ast.block b) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
@@ -134,7 +141,15 @@ fn log_block(&ast.block b) -> () {
                   mutable cur_cmnt=0u);
 
   print_block(out, b);
-  log(s.get_str());
+  ret s.get_str();
+}
+
+fn log_block(&ast.block b) -> () {
+    log(block_to_str(b));
+}
+
+fn log_block_err(&ast.block b) -> () {
+    log_err(block_to_str(b));
 }
 
 fn log_ann(&ast.ann a) -> () {
@@ -148,7 +163,7 @@ fn log_ann(&ast.ann a) -> () {
     }
 }
 
-fn log_stmt(ast.stmt st) -> () {
+fn stmt_to_str(&ast.stmt st) -> str {
   let str_writer s = string_writer();
   auto out_ = mkstate(s.get_writer(), 80u);
   auto out = @rec(s=out_,
@@ -163,7 +178,48 @@ fn log_stmt(ast.stmt st) -> () {
     }
     case (_) { /* do nothing */ }
   }
-  log(s.get_str());
+  ret s.get_str();
+}
+
+fn log_stmt(&ast.stmt st) -> () {
+    log(stmt_to_str(st));
+}
+
+fn log_stmt_err(&ast.stmt st) -> () {
+    log_err(stmt_to_str(st));
+}
+
+fn decl_lhs(@ast.decl d) -> ast.def_id {
+    alt (d.node) {
+        case (ast.decl_local(?l)) {
+            ret l.id;
+        }
+        case (ast.decl_item(?an_item)) {
+            alt (an_item.node) {
+                case (ast.item_const(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_fn(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_mod(_,_,?d)) {
+                    ret d;
+                }
+                case (ast.item_native_mod(_,_,?d)) {
+                    ret d;
+                }
+                case (ast.item_ty(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_tag(_,_,_,?d,_)) {
+                    ret d;
+                }
+                case (ast.item_obj(_,_,_,?d,_)) {
+                    ret d.ctor; /* This doesn't really make sense */
+                }
+            }
+        } 
+    }
 }
 
 //
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index 9ad6e01e..b7fbc3cc 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -44,6 +44,10 @@ fn empty_poststate(uint num_vars) -> poststate {
   be true_precond(num_vars);
 }
 
+fn false_postcond(uint num_vars) -> postcond {
+    be bitv.create(num_vars, true);
+}
+
 fn empty_pre_post(uint num_vars) -> pre_and_post {
   ret(rec(precondition=empty_prestate(num_vars),
           postcondition=empty_poststate(num_vars)));
@@ -119,7 +123,7 @@ fn set_postcondition(&ts_ann a, &postcond p) -> () {
 
 // Sets all the bits in a's prestate to equal the
 // corresponding bit in p's prestate.
-fn set_prestate(&ts_ann a, &prestate p) -> bool {
+fn set_prestate(@ts_ann a, &prestate p) -> bool {
   ret bitv.copy(a.states.prestate, p);
 }
 
@@ -139,6 +143,13 @@ fn extend_poststate(&poststate p, &poststate new) -> bool {
   ret bitv.union(p, new);
 }
 
+// Clears the given bit in p
+fn relax_prestate(uint i, &prestate p) -> bool {
+    auto was_set = bitv.get(p, i);
+    bitv.set(p, i, false);
+    ret was_set;
+}
+
 fn ann_precond(&ts_ann a) -> precond {
   ret a.conditions.precondition;
 }
@@ -148,8 +159,12 @@ fn ann_prestate(&ts_ann a) -> prestate {
 }
 
 fn pp_clone(&pre_and_post p) -> pre_and_post {
-  ret rec(precondition=bitv.clone(p.precondition),
-          postcondition=bitv.clone(p.postcondition));
+  ret rec(precondition=clone(p.precondition),
+          postcondition=clone(p.postcondition));
+}
+
+fn clone(prestate p) -> prestate {
+    ret bitv.clone(p);
 }
 
 // returns true if a implies b