From b7dd75c904277630675e432b3398a584d882b5ac Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Mon, 18 Apr 2011 15:33:10 -0700
Subject: Handle nested items correctly in typestate_check

Summary says it all. Actually, only nested objects and functions
are handled, but that's better than before. The fold that I was using
before to traverse a crate wasn't working correctly, because annotations
have to reflect the number of local variables of the nearest enclosing
function (in turn, because annotations are represented as bit vectors).
The fold was traversing the AST in the wrong order, first filling in
the annotations correctly, but then re-traversing them with the bit
vector length for any outer nested functions, and so on.

Remedying this required writing a lot of tedious boilerplate code
because I scrapped the idea of using a fold altogether.

I also made typestate_check handle unary, field, alt, and fail.

Also, some miscellaneous changes:
* added annotations to blocks in typeck
* fix pprust so it can handle spawn
* added more logging functions in util.common
* fixed _vec.or
* added maybe and from_maybe in option
* removed fold_block field from ast_fold, since it was never used
---
 src/comp/util/common.rs        | 29 +++++++++++++++++++++++++++++
 src/comp/util/typestate_ann.rs | 16 ++++++++++++++++
 2 files changed, 45 insertions(+)

(limited to 'src/comp/util')

diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 006bccb0..af000cb6 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -137,6 +137,35 @@ fn log_block(&ast.block b) -> () {
   log(s.get_str());
 }
 
+fn log_ann(&ast.ann a) -> () {
+    alt (a) {
+        case (ast.ann_none) {
+            log("ann_none");
+        }
+        case (ast.ann_type(_,_,_)) {
+            log("ann_type");
+        }
+    }
+}
+
+fn log_stmt(ast.stmt st) -> () {
+  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);
+  alt (st.node) {
+    case (ast.stmt_decl(?decl,_)) {
+      print_decl(out, decl);
+    }
+    case (ast.stmt_expr(?ex,_)) {
+      print_expr(out, ex);
+    }
+    case (_) { /* do nothing */ }
+  }
+  log(s.get_str());
+}
+
 //
 // Local Variables:
 // mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index b1f12ffb..9ad6e01e 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -147,6 +147,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
   ret a.states.prestate;
 }
 
+fn pp_clone(&pre_and_post p) -> pre_and_post {
+  ret rec(precondition=bitv.clone(p.precondition),
+          postcondition=bitv.clone(p.postcondition));
+}
+
 // returns true if a implies b
 // that is, returns true except if for some bits c and d,
 // c = 1 and d = 0
@@ -155,3 +160,14 @@ fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(tmp, a);
   ret bitv.is_false(tmp);
 }
+
+//
+// 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:
+//
-- 
cgit v1.2.3