Compute typestate properly for move

typestate now drops constraints correctly in the post-state of
a move expression or a declaration whose op is a move. It doesn't
yet drop constraints mentioning variables that get updated.

To do this, I had to change typestate to use trit-vectors instead
of bit-vectors, because for every constraint, there are three
possible values: known-to-be-false (e.g. after x <- y, init(y) is
known-to-be-false), known-to-be-true, and unknown. Before, we
conflated known-to-be-false with unknown. But move requires them
to be treated differently. Consider:

(program a)
(a1) x = 1;
(a2) y <- x;
(a3) log x;

(program b)
(b1) x = 1;
(b2) y <- z;
(b3) log x;

With only two values, the postcondition of statement a2 for
constraint init(x) is the same as that of b2: 0. But in (a2)'s
postcondition, init(x) *must* be false, but in (b2)'s condition,
it's just whatever it was in the postcondition of the preceding statement.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 801dda99de4..87a1908f8e0 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -252,6 +252,15 @@ fn is_hex_digit(char c) -> bool {
 }
 
 fn is_bin_digit(char c) -> bool { ret c == '0' || c == '1'; }
+
+// FIXME move to vec
+fn any[T](&fn(&T) -> bool f, &vec[T] v) -> bool {
+    for (T t in v) {
+        if (f(t)) { ret true; } 
+    }
+    ret false;
+}
+
 //
 // Local Variables:
 // mode: rust