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.

1 files changed, 12 insertions, 9 deletions

diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index 0bd18382..46666a34 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -6,6 +6,7 @@ import util.common.span;
 import util.common.spanned;
 import util.common.ty_mach;
 import util.common.filename;
+import util.typestate_ann.ts_ann;
 
 type ident = str;
 
@@ -21,7 +22,9 @@ type ty_param = rec(ident ident, def_id id);
 // Annotations added during successive passes.
 tag ann {
     ann_none;
-    ann_type(@middle.ty.t, option.t[vec[@middle.ty.t]] /* ty param substs */);
+    ann_type(@middle.ty.t,
+             option.t[vec[@middle.ty.t]], /* ty param substs */
+             option.t[@ts_ann]); /* pre- and postcondition for typestate */
 }
 
 tag def {
@@ -274,14 +277,14 @@ tag expr_ {
     expr_index(@expr, @expr, ann);
     expr_path(path, option.t[def], ann);
     expr_ext(path, vec[@expr], option.t[@expr], @expr, ann);
-    expr_fail;
-    expr_break;
-    expr_cont;
-    expr_ret(option.t[@expr]);
-    expr_put(option.t[@expr]);
-    expr_be(@expr);
-    expr_log(@expr);
-    expr_check_expr(@expr);
+    expr_fail(ann);
+    expr_break(ann);
+    expr_cont(ann);
+    expr_ret(option.t[@expr], ann);
+    expr_put(option.t[@expr], ann);
+    expr_be(@expr, ann);
+    expr_log(@expr, ann);
+    expr_check_expr(@expr, ann);
     expr_port(ann);
     expr_chan(@expr, ann);
 }