Further work on typestate. Handles expr_rec and expr_assign now.

Also changed the ts_ann field on statements to be an ann instead,
which explains most of the changes.

As well, got rid of the "warning: no type for expression" error
by filling in annotations for local decls in typeck (not sure whether
this was my fault or not).

Finally, in bitv, added a clone() function to copy a bit vector,
and fixed is_true, is_false, and to_str to not be nonsense.

2 files changed, 73 insertions, 12 deletions

diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 68d518da..58109126 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -1,8 +1,17 @@
 import std._uint;
 import std._int;
 import std._vec;
+import std.option.none;
 import front.ast;
+import util.typestate_ann.ts_ann;
 
+import std.io.stdout;
+import std.io.str_writer;
+import std.io.string_writer;
+import pretty.pprust.print_block;
+import pretty.pprust.print_expr;
+import pretty.pprust.print_decl;
+import pretty.pp.mkstate;
 
 type filename = str;
 type span = rec(uint lo, uint hi);
@@ -94,6 +103,40 @@ fn elt_exprs(vec[ast.elt] elts) -> vec[@ast.expr] {
     be _vec.map[ast.elt, @ast.expr](f, elts);
 }
 
+fn field_expr(&ast.field f) -> @ast.expr { ret f.expr; }
+
+fn field_exprs(vec[ast.field] fields) -> vec [@ast.expr] {
+    auto f = field_expr;
+    ret _vec.map[ast.field, @ast.expr](f, fields);
+}
+
+fn plain_ann() -> ast.ann {
+  ret ast.ann_type(middle.ty.plain_ty(middle.ty.ty_nil),
+                   none[vec[@middle.ty.t]], none[@ts_ann]);
+}
+
+fn log_expr(@ast.expr e) -> () {
+  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());
+}
+
+fn log_block(&ast.block b) -> () {
+  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_block(out, b);
+  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 c8d23321..0218df1c 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -72,7 +72,7 @@ fn difference(&precond p1, &precond p2) -> bool {
 }
 
 fn union(&precond p1, &precond p2) -> bool {
-  be bitv.difference(p1, p2);
+  be bitv.union(p1, p2);
 }
 
 fn pps_len(&pre_and_post p) -> uint {
@@ -87,38 +87,52 @@ impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
   bitv.set(p.postcondition, i, true);
 }
 
-impure fn set_in_postcond(uint i, &pre_and_post p) -> () {
+impure fn set_in_postcond(uint i, &pre_and_post p) -> bool {
   // sets the ith bit in p's post
+  auto was_set = bitv.get(p.postcondition, i);
   bitv.set(p.postcondition, i, true);
+  ret !was_set;
+}
+
+impure fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
+  // sets the ith bit in p's post
+  auto was_set = bitv.get(s.poststate, i);
+  bitv.set(s.poststate, i, true);
+  ret !was_set;
 }
 
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
 impure fn set_precondition(&ts_ann a, &precond p) -> () {
-  bitv.copy(p, a.conditions.precondition);
+  bitv.copy(a.conditions.precondition, p);
 }
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
 impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
-  bitv.copy(p, a.conditions.postcondition);
+  bitv.copy(a.conditions.postcondition, p);
 }
 
 // Sets all the bits in a's prestate to equal the
 // corresponding bit in p's prestate.
-impure fn set_prestate(&ts_ann a, &prestate p) -> () {
-  bitv.copy(p, a.states.prestate);
+impure fn set_prestate(&ts_ann a, &prestate p) -> bool {
+  ret bitv.copy(a.states.prestate, p);
 }
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
-impure fn set_poststate(&ts_ann a, &poststate p) -> () {
-  bitv.copy(p, a.states.poststate);
+impure fn set_poststate(&ts_ann a, &poststate p) -> bool {
+  ret bitv.copy(a.states.poststate, p);
+}
+
+// Set all the bits in p that are set in new
+impure fn extend_prestate(&prestate p, &poststate new) -> bool {
+  ret bitv.union(p, new);
 }
 
 // Set all the bits in p that are set in new
-impure fn extend_prestate(&prestate p, &poststate new) -> () {
-  bitv.union(p, new);
+impure fn extend_poststate(&poststate p, &poststate new) -> bool {
+  ret bitv.union(p, new);
 }
 
 fn ann_precond(&ts_ann a) -> precond {
@@ -129,7 +143,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
   ret a.states.prestate;
 }
 
+// returns true if a implies b
+// that is, returns true except if for some bits c and d,
+// c = 1 and d = 0
 impure fn implies(bitv.t a, bitv.t b) -> bool {
-  bitv.difference(b, a);
-  ret bitv.is_false(b);
+  auto tmp = bitv.clone(b);
+  bitv.difference(tmp, a);
+  ret bitv.is_false(tmp);
 }