From 3130348ee177f1716488b6caca6c7852fe47754c Mon Sep 17 00:00:00 2001
From: Tim Chevalier <chevalier@alum.wellesley.edu>
Date: Thu, 24 Mar 2011 12:12:04 -0700
Subject: Started adding support for typestate checking.

I added a new field to the ast "ann" type for typestate information.
Currently, the field contains a record of a precondition bit vector and
postcondition vector, but I tried to structure things so as to make
it easy to change the representation of the typestate annotation type.
I also had to add annotations to some syntactic forms that didn't have
them before (fail, ret, be...), with all the boilerplate changes
that that would imply.

The main call to the typestate_check entry point is commented out and
the actual pre-postcondition algorithm only has a few cases
implemented, though the overall AST traversal is there. The rest of
the typestate algorithm isn't implemented yet.
---
 src/comp/util/typestate_ann.rs | 61 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 src/comp/util/typestate_ann.rs

(limited to 'src/comp/util')

diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
new file mode 100644
index 00000000..a4698c5d
--- /dev/null
+++ b/src/comp/util/typestate_ann.rs
@@ -0,0 +1,61 @@
+import front.ast.ident;
+import std._vec;
+import std.bitv;
+
+/* 
+   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; /* 1 means "this variable must be initialized"
+                           0 means "don't care about this variable" */
+type postcond = bitv.t; /* 1 means "this variable is initialized"
+                           0 means "don't know about this variable */
+
+/* named thus so as not to confuse with prestate and poststate */
+type pre_and_post = rec(precond precondition, postcond postcondition);
+/* FIXME: once it's implemented: */
+//  : ((*.precondition).nbits == (*.postcondition).nbits);
+
+type ts_ann = pre_and_post;
+
+fn true_precond(uint num_vars) -> precond {
+  be bitv.create(num_vars, false);
+}
+
+fn true_postcond(uint num_vars) -> postcond {
+  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)));
+}
+
+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);
+}
+
+fn union(&precond p1, &precond p2) -> bool {
+  be bitv.difference(p1, p2);
+}
+
+fn pps_len(&pre_and_post p) -> uint {
+  // gratuitous check
+  check (p.precondition.nbits == p.postcondition.nbits);
+  ret p.precondition.nbits;
+}
+
+impure 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, false);
+}
\ No newline at end of file
-- 
cgit v1.2.3