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.

Author: catamorphism

src/comp/middle/tstate/ann.rs

@@ -1,36 +1,36 @@
 
 import front::ast::ident;
 import std::vec;
-import std::bitv;
+import tritv::*;
 
+type precond = t;
 
-/* 
-   This says: this expression requires the idents in <pre> to be initialized,
-   and given the precondition, it guarantees that the idents in <post> are
-   initialized.
- */
-type precond = bitv::t;
+/* 2 means "this constraint may or may not be true after execution" 
+   1 means "this constraint is definitely true after execution"
+   0 means "this constraint is definitely false after execution" */
+type postcond = t;
 
 
-/* 1 means "this variable must be initialized"
-  0 means "don't care about this variable" */
-type postcond = bitv::t;
+/* 2 means "don't know about this constraint"
+   1 means "this constraint is definitely true before entry"
+   0 means "this constraint is definitely false on entry" */
+type prestate = t;
 
 
-/* 1 means "this variable is initialized"
-  0 means "don't know about this variable */
-type prestate = bitv::t;
+/* similar to postcond */
+type poststate = t;
 
 
 /* 1 means "this variable is definitely initialized"
   0 means "don't know whether this variable is
   initialized" */
-type poststate = bitv::t;
-
 
-/* 1 means "this variable is definitely initialized"
-  0 means "don't know whether this variable is
-  initialized" */
+/* 
+   This says: this expression requires the constraints whose value is 1 in
+   <pre> to be true, and given the precondition, it guarantees that the
+   constraints in <post> whose values are 1 are true, and that the constraints
+   in <post> whose values are 0 are false.
+ */
 
 /* named thus so as not to confuse with prestate and poststate */
 type pre_and_post = @rec(precond precondition, postcond postcondition);
@@ -44,7 +44,7 @@ type pre_and_post_state = rec(prestate prestate, poststate poststate);
 type ts_ann = @rec(pre_and_post conditions, pre_and_post_state states);
 
 fn true_precond(uint num_vars) -> precond {
-    be bitv::create(num_vars, false);
+    be create_tritv(num_vars);
 }
 
 fn true_postcond(uint num_vars) -> postcond { be true_precond(num_vars); }
@@ -54,7 +54,9 @@ fn empty_prestate(uint num_vars) -> prestate { be true_precond(num_vars); }
 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);
+    auto res = create_tritv(num_vars);
+    tritv_set_all(res);
+    ret res;
 }
 
 fn empty_pre_post(uint num_vars) -> pre_and_post {
@@ -77,12 +79,16 @@ fn get_pre(&pre_and_post p) -> precond { ret p.precondition; }
 fn get_post(&pre_and_post p) -> postcond { ret p.postcondition; }
 
 fn difference(&precond p1, &precond p2) -> bool {
-    be bitv::difference(p1, p2);
+    ret tritv_difference(p1, p2);
 }
 
-fn union(&precond p1, &precond p2) -> bool { be bitv::union(p1, p2); }
+fn union(&precond p1, &precond p2) -> bool {
+    ret tritv_union(p1, p2);
+}
 
-fn intersect(&precond p1, &precond p2) -> bool { be bitv::intersect(p1, p2); }
+fn intersect(&precond p1, &precond p2) -> bool {
+    ret tritv_intersect(p1, p2);
+}
 
 fn pps_len(&pre_and_post p) -> uint {
     // gratuitous check
@@ -93,86 +99,88 @@ fn pps_len(&pre_and_post p) -> uint {
 
 fn require(uint i, &pre_and_post p) {
     // sets the ith bit in p's pre
-
-    bitv::set(p.precondition, i, true);
+    tritv_set(i, p.precondition, ttrue);
 }
 
 fn require_and_preserve(uint i, &pre_and_post p) {
     // sets the ith bit in p's pre and post
-
-    bitv::set(p.precondition, i, true);
-    bitv::set(p.postcondition, i, true);
+    tritv_set(i, p.precondition, ttrue);
+    tritv_set(i, p.postcondition, ttrue);
 }
 
 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;
+    auto was_set = tritv_get(p.postcondition, i);
+    tritv_set(i, p.postcondition, ttrue);
+    ret was_set != ttrue;
 }
 
 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;
+    auto was_set = tritv_get(s.poststate, i);
+    tritv_set(i, s.poststate, ttrue);
+    ret was_set != ttrue;
 }
 
 fn clear_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, false);
-    ret was_set;
+    auto was_set = tritv_get(s.poststate, i);
+    tritv_set(i, s.poststate, tfalse);
+    ret was_set != tfalse;
 }
 
+fn clear_in_postcond(uint i, &pre_and_post s) -> bool {
+    // sets the ith bit in p's post
+    auto was_set = tritv_get(s.postcondition, i);
+    tritv_set(i, s.postcondition, tfalse);
+    ret was_set != tfalse;
+}
 
 // Sets all the bits in a's precondition to equal the
 // corresponding bit in p's precondition.
 fn set_precondition(ts_ann a, &precond p) {
-    bitv::copy(a.conditions.precondition, p);
+    tritv_copy(a.conditions.precondition, p);
 }
 
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
 fn set_postcondition(ts_ann a, &postcond p) {
-    bitv::copy(a.conditions.postcondition, p);
+    tritv_copy(a.conditions.postcondition, 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 {
-    ret bitv::copy(a.states.prestate, p);
+    ret tritv_copy(a.states.prestate, p);
 }
 
 
 // Sets all the bits in a's postcondition to equal the
 // corresponding bit in p's postcondition.
 fn set_poststate(ts_ann a, &poststate p) -> bool {
-    ret bitv::copy(a.states.poststate, p);
+    ret tritv_copy(a.states.poststate, p);
 }
 
 
 // Set all the bits in p that are set in new
 fn extend_prestate(&prestate p, &poststate new) -> bool {
-    ret bitv::union(p, new);
+    ret tritv_union(p, new);
 }
 
 
 // Set all the bits in p that are set in new
 fn extend_poststate(&poststate p, &poststate new) -> bool {
-    ret bitv::union(p, new);
+    ret tritv_union(p, new);
 }
 
-// Clears the given bit in p
+// Sets the given bit in p to "don't care"
+// FIXME: is this correct?
 fn relax_prestate(uint i, &prestate p) -> bool {
-    auto was_set = bitv::get(p, i);
-    bitv::set(p, i, false);
-    ret was_set;
+    auto was_set = tritv_get(p, i);
+    tritv_set(i, p, dont_care);
+    ret was_set != dont_care;
 }
 
 // Clears the given bit in p
@@ -185,12 +193,11 @@ fn relax_precond(uint i, &precond p) {
     relax_prestate(i, p);
 }
 
-// Clears all the bits in p
-fn clear(&precond p) { bitv::clear(p); }
-
+// Sets all the bits in p to "don't care"
+fn clear(&precond p) { tritv_clear(p); }
 
-// Sets all the bits in p
-fn set(&precond p) { bitv::set_all(p); }
+// Sets all the bits in p to true
+fn set(&precond p) { tritv_set_all(p); }
 
 fn ann_precond(&ts_ann a) -> precond { ret a.conditions.precondition; }
 
@@ -203,16 +210,17 @@ fn pp_clone(&pre_and_post p) -> pre_and_post {
              postcondition=clone(p.postcondition));
 }
 
-fn clone(prestate p) -> prestate { ret bitv::clone(p); }
+fn clone(prestate p) -> prestate { ret tritv_clone(p); }
 
 
 // returns true if a implies b
 // that is, returns true except if for some bits c and d,
-// c = 1 and d = 0
-fn implies(bitv::t a, bitv::t b) -> bool {
-    auto tmp = bitv::clone(b);
-    bitv::difference(tmp, a);
-    ret bitv::is_false(tmp);
+// c = 1 and d = either 0 or "don't know"
+// FIXME: is this correct?
+fn implies(t a, t b) -> bool {
+    auto tmp = tritv_clone(b);
+    tritv_difference(tmp, a);
+    ret tritv_doesntcare(tmp);
 }
 //
 // Local Variables: