Continued sketching out code for checking states against preconditions.

It's still sketchy. I added a typestate annotation field to statements
tagged stmt_decl or stmt_expr, because a stmt_decl statement has a typestate
that's different from that of its child node. This necessitated trivial
changes to a bunch of other files all over to the compiler. I also added a
few small standard library functions, some of which I didn't actually end
up using but which I thought might be useful anyway.

1 files changed, 47 insertions, 4 deletions

diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index 071f55135f5..53f9a71cf22 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -36,9 +36,17 @@ fn true_postcond(uint num_vars) -> postcond {
   be true_precond(num_vars);
 }
 
+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 empty_pre_post(uint num_vars) -> pre_and_post {
-  ret(rec(precondition=true_precond(num_vars),
-           postcondition=true_postcond(num_vars)));
+  ret(rec(precondition=empty_prestate(num_vars),
+          postcondition=empty_poststate(num_vars)));
 }
 
 fn empty_states(uint num_vars) -> pre_and_post_state {
@@ -46,6 +54,11 @@ fn empty_states(uint num_vars) -> pre_and_post_state {
            poststate=true_postcond(num_vars)));
 }
 
+fn empty_ann(uint num_vars) -> ts_ann {
+  ret(rec(conditions=empty_pre_post(num_vars),
+          states=empty_states(num_vars)));
+}
+
 fn get_pre(&pre_and_post p) -> precond {
   ret p.precondition;
 }
@@ -74,7 +87,37 @@ impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
   bitv.set(p.postcondition, i, true);
 }
 
-fn implies(bitv.t a, bitv.t b) -> bool {
+impure fn set_in_postcond(uint i, &pre_and_post p) -> () {
+  // sets the ith bit in p's post
+  bitv.set(p.postcondition, i, true);
+}
+
+// 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);
+}
+
+// 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);
+}
+
+// Set all the bits in p that are set in new
+impure fn extend_prestate(&prestate p, &poststate new) -> () {
+  bitv.union(p, new);
+}
+
+fn ann_precond(&ts_ann a) -> precond {
+  ret a.conditions.precondition;
+}
+
+fn ann_prestate(&ts_ann a) -> prestate {
+  ret a.states.prestate;
+}
+
+impure fn implies(bitv.t a, bitv.t b) -> bool {
   bitv.difference(b, a);
-  ret (bitv.equal(b, bitv.create(b.nbits, false)));
+  be bitv.is_false(b);
 }