From 3130348ee177f1716488b6caca6c7852fe47754c Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Thu, 24 Mar 2011 12:12:04 -0700 Subject: [PATCH] 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/driver/rustc.rs | 5 +- src/comp/front/ast.rs | 21 +- src/comp/front/lexer.rs | 2 +- src/comp/front/parser.rs | 36 +-- src/comp/middle/fold.rs | 98 +++--- src/comp/middle/trans.rs | 23 +- src/comp/middle/ty.rs | 14 +- src/comp/middle/typeck.rs | 249 +++++++-------- src/comp/middle/typestate_check.rs | 496 +++++++++++++++++++++++++++++ src/comp/pretty/pprust.rs | 16 +- src/comp/rustc.rc | 3 + src/comp/util/typestate_ann.rs | 61 ++++ src/lib/_vec.rs | 23 ++ 13 files changed, 813 insertions(+), 234 deletions(-) create mode 100644 src/comp/middle/typestate_check.rs create mode 100644 src/comp/util/typestate_ann.rs diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs index 9ab216228a5..a1fdb387d7f 100644 --- a/src/comp/driver/rustc.rs +++ b/src/comp/driver/rustc.rs @@ -8,6 +8,7 @@ import middle.trans; import middle.resolve; import middle.ty; import middle.typeck; +import middle.typestate_check; import util.common; import std.map.mk_hashmap; @@ -63,11 +64,11 @@ impure fn compile_input(session.session sess, auto crate = parse_input(sess, p, input); crate = creader.read_crates(sess, crate, library_search_paths); crate = resolve.resolve_crate(sess, crate); - auto typeck_result = typeck.check_crate(sess, crate); crate = typeck_result._0; auto type_cache = typeck_result._1; - + // FIXME: uncomment once typestate_check works + // crate = typestate_check.check_crate(crate); trans.trans_crate(sess, crate, type_cache, output, shared); } diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index 0bd183828b9..46666a34378 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); } diff --git a/src/comp/front/lexer.rs b/src/comp/front/lexer.rs index 6cead0bc6e2..5a9c2b11dc0 100644 --- a/src/comp/front/lexer.rs +++ b/src/comp/front/lexer.rs @@ -419,7 +419,7 @@ impure fn scan_number(mutable char c, reader rdr) -> token.token { if (is_dec_integer) { accum_int = digits_to_string(dec_str); } - + c = rdr.curr(); n = rdr.next(); diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs index f7d355a4ba6..4c3e6cf03be 100644 --- a/src/comp/front/parser.rs +++ b/src/comp/front/parser.rs @@ -794,14 +794,14 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr { case (token.FAIL) { p.bump(); - ex = ast.expr_fail; + ex = ast.expr_fail(ast.ann_none); } case (token.LOG) { p.bump(); auto e = parse_expr(p); auto hi = e.span; - ex = ast.expr_log(e); + ex = ast.expr_log(e, ast.ann_none); } case (token.CHECK) { @@ -810,7 +810,7 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr { case (token.LPAREN) { auto e = parse_expr(p); auto hi = e.span; - ex = ast.expr_check_expr(e); + ex = ast.expr_check_expr(e, ast.ann_none); } case (_) { p.get_session().unimpl("constraint-check stmt"); @@ -822,36 +822,36 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr { p.bump(); alt (p.peek()) { case (token.SEMI) { - ex = ast.expr_ret(none[@ast.expr]); + ex = ast.expr_ret(none[@ast.expr], ast.ann_none); } case (_) { auto e = parse_expr(p); hi = e.span; - ex = ast.expr_ret(some[@ast.expr](e)); + ex = ast.expr_ret(some[@ast.expr](e), ast.ann_none); } } } case (token.BREAK) { p.bump(); - ex = ast.expr_break; + ex = ast.expr_break(ast.ann_none); } case (token.CONT) { p.bump(); - ex = ast.expr_cont; + ex = ast.expr_cont(ast.ann_none); } case (token.PUT) { p.bump(); alt (p.peek()) { case (token.SEMI) { - ex = ast.expr_put(none[@ast.expr]); + ex = ast.expr_put(none[@ast.expr], ast.ann_none); } case (_) { auto e = parse_expr(p); hi = e.span; - ex = ast.expr_put(some[@ast.expr](e)); + ex = ast.expr_put(some[@ast.expr](e), ast.ann_none); } } } @@ -862,7 +862,7 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr { // FIXME: Is this the right place for this check? if /*check*/ (ast.is_call_expr(e)) { hi = e.span; - ex = ast.expr_be(e); + ex = ast.expr_be(e, ast.ann_none); } else { p.err("Non-call expression in tail call"); @@ -1651,14 +1651,14 @@ fn stmt_ends_with_semi(@ast.stmt stmt) -> bool { case (ast.expr_field(_,_,_)) { ret true; } case (ast.expr_index(_,_,_)) { ret true; } case (ast.expr_path(_,_,_)) { ret true; } - case (ast.expr_fail) { ret true; } - case (ast.expr_break) { ret true; } - case (ast.expr_cont) { ret true; } - case (ast.expr_ret(_)) { ret true; } - case (ast.expr_put(_)) { ret true; } - case (ast.expr_be(_)) { ret true; } - case (ast.expr_log(_)) { ret true; } - case (ast.expr_check_expr(_)) { ret true; } + case (ast.expr_fail(_)) { ret true; } + case (ast.expr_break(_)) { ret true; } + case (ast.expr_cont(_)) { ret true; } + case (ast.expr_ret(_,_)) { ret true; } + case (ast.expr_put(_,_)) { ret true; } + case (ast.expr_be(_,_)) { ret true; } + case (ast.expr_log(_,_)) { ret true; } + case (ast.expr_check_expr(_,_)) { ret true; } } } // We should not be calling this on a cdir. diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs index 8138d1a3dc9..d7a18783cbb 100644 --- a/src/comp/middle/fold.rs +++ b/src/comp/middle/fold.rs @@ -178,26 +178,26 @@ type ast_fold[ENV] = @expr expanded, ann a) -> @expr) fold_expr_ext, - (fn(&ENV e, &span sp) -> @expr) fold_expr_fail, + (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_fail, - (fn(&ENV e, &span sp) -> @expr) fold_expr_break, + (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_break, - (fn(&ENV e, &span sp) -> @expr) fold_expr_cont, + (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_cont, (fn(&ENV e, &span sp, - &option.t[@expr] rv) -> @expr) fold_expr_ret, + &option.t[@expr] rv, ann a) -> @expr) fold_expr_ret, (fn(&ENV e, &span sp, - &option.t[@expr] rv) -> @expr) fold_expr_put, + &option.t[@expr] rv, ann a) -> @expr) fold_expr_put, (fn(&ENV e, &span sp, - @expr e) -> @expr) fold_expr_be, + @expr e, ann a) -> @expr) fold_expr_be, (fn(&ENV e, &span sp, - @expr e) -> @expr) fold_expr_log, + @expr e, ann a) -> @expr) fold_expr_log, (fn(&ENV e, &span sp, - @expr e) -> @expr) fold_expr_check_expr, + @expr e, ann a) -> @expr) fold_expr_check_expr, (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_port, @@ -717,19 +717,19 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr { exp, t); } - case (ast.expr_fail) { - ret fld.fold_expr_fail(env_, e.span); + case (ast.expr_fail(?t)) { + ret fld.fold_expr_fail(env_, e.span, t); } - case (ast.expr_break) { - ret fld.fold_expr_break(env_, e.span); + case (ast.expr_break(?t)) { + ret fld.fold_expr_break(env_, e.span, t); } - case (ast.expr_cont) { - ret fld.fold_expr_cont(env_, e.span); + case (ast.expr_cont(?t)) { + ret fld.fold_expr_cont(env_, e.span, t); } - case (ast.expr_ret(?oe)) { + case (ast.expr_ret(?oe, ?t)) { auto oee = none[@expr]; alt (oe) { case (some[@expr](?x)) { @@ -737,10 +737,10 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr { } case (_) { /* fall through */ } } - ret fld.fold_expr_ret(env_, e.span, oee); + ret fld.fold_expr_ret(env_, e.span, oee, t); } - case (ast.expr_put(?oe)) { + case (ast.expr_put(?oe, ?t)) { auto oee = none[@expr]; alt (oe) { case (some[@expr](?x)) { @@ -748,22 +748,22 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr { } case (_) { /* fall through */ } } - ret fld.fold_expr_put(env_, e.span, oee); + ret fld.fold_expr_put(env_, e.span, oee, t); } - case (ast.expr_be(?x)) { + case (ast.expr_be(?x, ?t)) { auto ee = fold_expr(env_, fld, x); - ret fld.fold_expr_be(env_, e.span, ee); + ret fld.fold_expr_be(env_, e.span, ee, t); } - case (ast.expr_log(?x)) { + case (ast.expr_log(?x, ?t)) { auto ee = fold_expr(env_, fld, x); - ret fld.fold_expr_log(env_, e.span, ee); + ret fld.fold_expr_log(env_, e.span, ee, t); } - case (ast.expr_check_expr(?x)) { + case (ast.expr_check_expr(?x, ?t)) { auto ee = fold_expr(env_, fld, x); - ret fld.fold_expr_check_expr(env_, e.span, ee); + ret fld.fold_expr_check_expr(env_, e.span, ee, t); } case (ast.expr_port(?t)) { @@ -1308,38 +1308,40 @@ fn identity_fold_expr_ext[ENV](&ENV env, &span sp, ret @respan(sp, ast.expr_ext(p, args, body, expanded, a)); } -fn identity_fold_expr_fail[ENV](&ENV env, &span sp) -> @expr { - ret @respan(sp, ast.expr_fail); +fn identity_fold_expr_fail[ENV](&ENV env, &span sp, ann a) -> @expr { + ret @respan(sp, ast.expr_fail(a)); } -fn identity_fold_expr_break[ENV](&ENV env, &span sp) -> @expr { - ret @respan(sp, ast.expr_break); +fn identity_fold_expr_break[ENV](&ENV env, &span sp, ann a) -> @expr { + ret @respan(sp, ast.expr_break(a)); } -fn identity_fold_expr_cont[ENV](&ENV env, &span sp) -> @expr { - ret @respan(sp, ast.expr_cont); +fn identity_fold_expr_cont[ENV](&ENV env, &span sp, ann a) -> @expr { + ret @respan(sp, ast.expr_cont(a)); } fn identity_fold_expr_ret[ENV](&ENV env, &span sp, - &option.t[@expr] rv) -> @expr { - ret @respan(sp, ast.expr_ret(rv)); + &option.t[@expr] rv, ann a) -> @expr { + ret @respan(sp, ast.expr_ret(rv, a)); } fn identity_fold_expr_put[ENV](&ENV env, &span sp, - &option.t[@expr] rv) -> @expr { - ret @respan(sp, ast.expr_put(rv)); + &option.t[@expr] rv, ann a) -> @expr { + ret @respan(sp, ast.expr_put(rv, a)); } -fn identity_fold_expr_be[ENV](&ENV env, &span sp, @expr x) -> @expr { - ret @respan(sp, ast.expr_be(x)); +fn identity_fold_expr_be[ENV](&ENV env, &span sp, @expr x, ann a) -> @expr { + ret @respan(sp, ast.expr_be(x, a)); } -fn identity_fold_expr_log[ENV](&ENV e, &span sp, @expr x) -> @expr { - ret @respan(sp, ast.expr_log(x)); +fn identity_fold_expr_log[ENV](&ENV e, &span sp, @expr x, + ann a) -> @expr { + ret @respan(sp, ast.expr_log(x, a)); } -fn identity_fold_expr_check_expr[ENV](&ENV e, &span sp, @expr x) -> @expr { - ret @respan(sp, ast.expr_check_expr(x)); +fn identity_fold_expr_check_expr[ENV](&ENV e, &span sp, @expr x, ann a) + -> @expr { + ret @respan(sp, ast.expr_check_expr(x, a)); } fn identity_fold_expr_port[ENV](&ENV e, &span sp, ann a) -> @expr { @@ -1621,15 +1623,15 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] { fold_expr_index = bind identity_fold_expr_index[ENV](_,_,_,_,_), fold_expr_path = bind identity_fold_expr_path[ENV](_,_,_,_,_), fold_expr_ext = bind identity_fold_expr_ext[ENV](_,_,_,_,_,_,_), - fold_expr_fail = bind identity_fold_expr_fail[ENV](_,_), - fold_expr_break = bind identity_fold_expr_break[ENV](_,_), - fold_expr_cont = bind identity_fold_expr_cont[ENV](_,_), - fold_expr_ret = bind identity_fold_expr_ret[ENV](_,_,_), - fold_expr_put = bind identity_fold_expr_put[ENV](_,_,_), - fold_expr_be = bind identity_fold_expr_be[ENV](_,_,_), - fold_expr_log = bind identity_fold_expr_log[ENV](_,_,_), + fold_expr_fail = bind identity_fold_expr_fail[ENV](_,_,_), + fold_expr_break = bind identity_fold_expr_break[ENV](_,_,_), + fold_expr_cont = bind identity_fold_expr_cont[ENV](_,_,_), + fold_expr_ret = bind identity_fold_expr_ret[ENV](_,_,_,_), + fold_expr_put = bind identity_fold_expr_put[ENV](_,_,_,_), + fold_expr_be = bind identity_fold_expr_be[ENV](_,_,_,_), + fold_expr_log = bind identity_fold_expr_log[ENV](_,_,_,_), fold_expr_check_expr - = bind identity_fold_expr_check_expr[ENV](_,_,_), + = bind identity_fold_expr_check_expr[ENV](_,_,_,_), fold_expr_port = bind identity_fold_expr_port[ENV](_,_,_), fold_expr_chan = bind identity_fold_expr_chan[ENV](_,_,_,_), diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs index c018ad57ee2..eb848f768c8 100644 --- a/src/comp/middle/trans.rs +++ b/src/comp/middle/trans.rs @@ -2497,7 +2497,7 @@ fn node_ann_type(@crate_ctxt cx, &ast.ann a) -> @ty.t { case (ast.ann_none) { cx.sess.bug("missing type annotation"); } - case (ast.ann_type(?t, _)) { + case (ast.ann_type(?t, _, _)) { ret target_type(cx, t); } } @@ -2509,7 +2509,7 @@ fn node_ann_ty_params(&ast.ann a) -> vec[@ty.t] { log "missing type annotation"; fail; } - case (ast.ann_type(_, ?tps_opt)) { + case (ast.ann_type(_, ?tps_opt, _)) { alt (tps_opt) { case (none[vec[@ty.t]]) { log "type annotation has no ty params"; @@ -3638,7 +3638,7 @@ fn lval_generic_fn(@block_ctxt cx, cx.fcx.ccx.sess.bug("no type annotation for path!"); fail; } - case (ast.ann_type(?monoty_, ?tps)) { + case (ast.ann_type(?monoty_, ?tps, _)) { monoty = monoty_; tys = option.get[vec[@ty.t]](tps); } @@ -4775,35 +4775,35 @@ fn trans_expr(@block_ctxt cx, @ast.expr e) -> result { ret trans_expr(cx, expanded); } - case (ast.expr_fail) { + case (ast.expr_fail(_)) { ret trans_fail(cx, e.span, "explicit failure"); } - case (ast.expr_log(?a)) { + case (ast.expr_log(?a, _)) { ret trans_log(cx, a); } - case (ast.expr_check_expr(?a)) { + case (ast.expr_check_expr(?a, _)) { ret trans_check_expr(cx, a); } - case (ast.expr_break) { + case (ast.expr_break(?a)) { ret trans_break(cx); } - case (ast.expr_cont) { + case (ast.expr_cont(?a)) { ret trans_cont(cx); } - case (ast.expr_ret(?e)) { + case (ast.expr_ret(?e, _)) { ret trans_ret(cx, e); } - case (ast.expr_put(?e)) { + case (ast.expr_put(?e, _)) { ret trans_put(cx, e); } - case (ast.expr_be(?e)) { + case (ast.expr_be(?e, _)) { ret trans_be(cx, e); } @@ -4855,6 +4855,7 @@ fn trans_log(@block_ctxt cx, @ast.expr e) -> result { auto sub = trans_expr(cx, e); auto e_ty = ty.expr_ty(e); + if (ty.type_is_fp(e_ty)) { let TypeRef tr; let bool is32bit = false; diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs index 829a5e5f096..d0b5fe102cc 100644 --- a/src/comp/middle/ty.rs +++ b/src/comp/middle/ty.rs @@ -593,7 +593,7 @@ fn ann_to_type(&ast.ann ann) -> @t { log "ann_to_type() called on node with no type"; fail; } - case (ast.ann_type(?ty, _)) { + case (ast.ann_type(?ty, _, _)) { ret ty; } } @@ -785,12 +785,12 @@ fn expr_ty(@ast.expr expr) -> @t { case (ast.expr_send(_, _, ?ann)) { ret ann_to_type(ann); } case (ast.expr_recv(_, _, ?ann)) { ret ann_to_type(ann); } - case (ast.expr_fail) { ret plain_ty(ty_nil); } - case (ast.expr_log(_)) { ret plain_ty(ty_nil); } - case (ast.expr_check_expr(_)) { ret plain_ty(ty_nil); } - case (ast.expr_ret(_)) { ret plain_ty(ty_nil); } - case (ast.expr_put(_)) { ret plain_ty(ty_nil); } - case (ast.expr_be(_)) { ret plain_ty(ty_nil); } + case (ast.expr_fail(_)) { ret plain_ty(ty_nil); } + case (ast.expr_log(_,_)) { ret plain_ty(ty_nil); } + case (ast.expr_check_expr(_,_)) { ret plain_ty(ty_nil); } + case (ast.expr_ret(_,_)) { ret plain_ty(ty_nil); } + case (ast.expr_put(_,_)) { ret plain_ty(ty_nil); } + case (ast.expr_be(_,_)) { ret plain_ty(ty_nil); } } fail; } diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index d0481b6a64a..f726ae588c9 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1,5 +1,6 @@ import front.ast; import front.ast.ann; +import front.ast.ann_none; import front.ast.mutability; import front.creader; import middle.fold; @@ -32,6 +33,8 @@ import std.option; import std.option.none; import std.option.some; +import util.typestate_ann.ts_ann; + type ty_table = hashmap[ast.def_id, @ty.t]; tag any_item { @@ -54,6 +57,11 @@ type fn_ctxt = rec(@ty.t ret_ty, // Used for ast_ty_to_ty() below. type ty_getter = fn(ast.def_id) -> ty.ty_params_opt_and_ty; +// Turns a type into an ann_type, using defaults for other fields. +fn triv_ann(@ty.t t) -> ann { + ret ast.ann_type(t, none[vec[@ty.t]], none[@ts_ann]); +} + // Replaces parameter types inside a type with type variables. fn generalize_ty(@crate_ctxt cx, @ty.t t) -> @ty.t { state obj ty_generalizer(@crate_ctxt cx, @@ -227,7 +235,7 @@ fn instantiate_path(@fn_ctxt fcx, &ast.path pth, &ty_params_opt_and_ty tpt, } } - ret ast.ann_type(t, ty_substs_opt); + ret ast.ann_type(t, ty_substs_opt, none[@ts_ann]); } // Returns the type parameters and polytype of an item, if it's an item that @@ -674,9 +682,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) auto tpt = tup(params_opt, result_ty); type_cache.insert(variant.node.id, tpt); - - auto variant_t = rec( - ann=ast.ann_type(result_ty, none[vec[@ty.t]]) + auto variant_t = rec(ann=triv_ann(result_ty) with variant.node ); result += vec(fold.respan[ast.variant_](variant.span, variant_t)); @@ -767,8 +773,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) ast.def_id id, ast.ann a) -> @ast.item { check (e.type_cache.contains_key(id)); auto typ = e.type_cache.get(id)._1; - auto item = ast.item_const(i, t, ex, id, - ast.ann_type(typ, none[vec[@ty.t]])); + auto item = ast.item_const(i, t, ex, id, triv_ann(typ)); ret @fold.respan[ast.item_](sp, item); } @@ -777,8 +782,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) ast.def_id id, ast.ann a) -> @ast.item { check (e.type_cache.contains_key(id)); auto typ = e.type_cache.get(id)._1; - auto item = ast.item_fn(i, f, ty_params, id, - ast.ann_type(typ, none[vec[@ty.t]])); + auto item = ast.item_fn(i, f, ty_params, id, triv_ann(typ)); ret @fold.respan[ast.item_](sp, item); } @@ -788,7 +792,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) check (e.type_cache.contains_key(id)); auto typ = e.type_cache.get(id)._1; auto item = ast.native_item_fn(i, ln, d, ty_params, id, - ast.ann_type(typ, none[vec[@ty.t]])); + triv_ann(typ)); ret @fold.respan[ast.native_item_](sp, item); } @@ -832,8 +836,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) auto meth_tfn = plain_ty(ty.ty_fn(meth_ty.proto, meth_ty.inputs, meth_ty.output)); - m_ = rec( - ann=ast.ann_type(meth_tfn, none[vec[@ty.t]]) + m_ = rec(ann=triv_ann(meth_tfn) with meth.node ); m = @rec(node=m_ with *meth); @@ -842,8 +845,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) auto g = bind getter(e.sess, e.id_to_ty_item, e.type_cache, _); for (ast.obj_field fld in ob.fields) { let @ty.t fty = ast_ty_to_ty(g, fld.ty); - let ast.obj_field f = rec( - ann=ast.ann_type(fty, none[vec[@ty.t]]) + let ast.obj_field f = rec(ann=triv_ann(fty) with fld ); _vec.push[ast.obj_field](fields, f); @@ -852,8 +854,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) auto ob_ = rec(methods = methods, fields = fields with ob); - auto item = ast.item_obj(i, ob_, ty_params, odid, - ast.ann_type(t, none[vec[@ty.t]])); + auto item = ast.item_obj(i, ob_, ty_params, odid, triv_ann(t)); ret @fold.respan[ast.item_](sp, item); } @@ -862,8 +863,7 @@ fn collect_item_types(session.session sess, @ast.crate crate) ast.def_id id, ast.ann a) -> @ast.item { check (e.type_cache.contains_key(id)); auto typ = e.type_cache.get(id)._1; - auto item = ast.item_ty(i, t, ty_params, id, - ast.ann_type(typ, none[vec[@ty.t]])); + auto item = ast.item_ty(i, t, ty_params, id, triv_ann(typ)); ret @fold.respan[ast.item_](sp, item); } @@ -879,7 +879,8 @@ fn collect_item_types(session.session sess, @ast.crate crate) ty_params); auto typ = e.type_cache.get(id)._1; auto item = ast.item_tag(i, variants_t, ty_params, id, - ast.ann_type(typ, none[vec[@ty.t]])); + ast.ann_type(typ, none[vec[@ty.t]], + none[@ts_ann])); ret @fold.respan[ast.item_](sp, item); } @@ -1034,16 +1035,20 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat { alt (pat.node) { case (ast.pat_wild(?ann)) { auto t = demand(fcx, pat.span, expected, ann_to_type(ann)); - p_1 = ast.pat_wild(ast.ann_type(t, none[vec[@ty.t]])); + p_1 = ast.pat_wild(ast.ann_type(t, none[vec[@ty.t]], + none[@ts_ann])); } case (ast.pat_lit(?lit, ?ann)) { auto t = demand(fcx, pat.span, expected, ann_to_type(ann)); - p_1 = ast.pat_lit(lit, ast.ann_type(t, none[vec[@ty.t]])); + p_1 = ast.pat_lit(lit, ast.ann_type(t, none[vec[@ty.t]], + none[@ts_ann])); } case (ast.pat_bind(?id, ?did, ?ann)) { auto t = demand(fcx, pat.span, expected, ann_to_type(ann)); fcx.locals.insert(did, t); - p_1 = ast.pat_bind(id, did, ast.ann_type(t, none[vec[@ty.t]])); + p_1 = ast.pat_bind(id, did, ast.ann_type(t, + none[vec[@ty.t]], + none[@ts_ann])); } case (ast.pat_tag(?id, ?subpats, ?vdef_opt, ?ann)) { auto t = demand(fcx, pat.span, expected, ann_to_type(ann)); @@ -1086,7 +1091,8 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat { // Nullary tag variant. check (subpats_len == 0u); p_1 = ast.pat_tag(id, subpats, vdef_opt, - ast.ann_type(t, tps_opt)); + ast.ann_type(t, tps_opt, + none[@ts_ann])); } case (ty.ty_fn(_, ?args, ?tag_ty)) { // N-ary tag variant. @@ -1101,7 +1107,8 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat { i += 1u; } p_1 = ast.pat_tag(id, new_subpats, vdef_opt, - ast.ann_type(tag_ty, tps_opt)); + ast.ann_type(tag_ty, tps_opt, + none[@ts_ann])); } } } @@ -1142,7 +1149,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, fail; } } - e_1 = ast.expr_vec(es_1, mut, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_vec(es_1, mut, triv_ann(t)); } case (ast.expr_tup(?es_0, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); @@ -1161,7 +1168,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, fail; } } - e_1 = ast.expr_tup(elts_1, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_tup(elts_1, triv_ann(t)); } case (ast.expr_rec(?fields_0, ?base_0, ?ann)) { @@ -1214,12 +1221,11 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, fail; } } - e_1 = ast.expr_rec(fields_1, base_1, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_rec(fields_1, base_1, triv_ann(t)); } case (ast.expr_bind(?sube, ?es, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_bind(sube, es, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_bind(sube, es, triv_ann(t)); } case (ast.expr_call(?sube, ?es, ?ann)) { // NB: we call 'demand_full' and pass in adk only in cases where @@ -1227,35 +1233,30 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, // like expr_binary or expr_bind can't, so there's no need. auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_call(sube, es, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_call(sube, es, triv_ann(t)); } case (ast.expr_call_self(?sube, ?es, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_call_self(sube, - es, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_call_self(sube, es, triv_ann(t)); } case (ast.expr_binary(?bop, ?lhs, ?rhs, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_binary(bop, lhs, rhs, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_binary(bop, lhs, rhs, triv_ann(t)); } case (ast.expr_unary(?uop, ?sube, ?ann)) { // See note in expr_unary for why we're calling demand_full. auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_unary(uop, sube, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_unary(uop, sube, triv_ann(t)); } case (ast.expr_lit(?lit, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_lit(lit, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_lit(lit, triv_ann(t)); } case (ast.expr_cast(?sube, ?ast_ty, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_cast(sube, ast_ty, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_cast(sube, ast_ty, triv_ann(t)); } case (ast.expr_if(?cond, ?then_0, ?else_0, ?ann)) { auto t = demand_full(fcx, e.span, expected, @@ -1270,60 +1271,52 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, else_1 = some[@ast.expr](e_1); } } - e_1 = ast.expr_if(cond, then_1, else_1, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_if(cond, then_1, else_1, triv_ann(t)); } case (ast.expr_for(?decl, ?seq, ?bloc, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_for(decl, seq, bloc, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_for(decl, seq, bloc, triv_ann(t)); } case (ast.expr_for_each(?decl, ?seq, ?bloc, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_for_each(decl, seq, bloc, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_for_each(decl, seq, bloc, triv_ann(t)); } case (ast.expr_while(?cond, ?bloc, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_while(cond, bloc, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_while(cond, bloc, triv_ann(t)); } case (ast.expr_do_while(?bloc, ?cond, ?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_do_while(bloc, cond, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_do_while(bloc, cond, triv_ann(t)); } case (ast.expr_block(?bloc, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_block(bloc, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_block(bloc, triv_ann(t)); } case (ast.expr_assign(?lhs_0, ?rhs_0, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); auto lhs_1 = demand_expr(fcx, expected, lhs_0); auto rhs_1 = demand_expr(fcx, expected, rhs_0); - e_1 = ast.expr_assign(lhs_1, rhs_1, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_assign(lhs_1, rhs_1, triv_ann(t)); } case (ast.expr_assign_op(?op, ?lhs_0, ?rhs_0, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); auto lhs_1 = demand_expr(fcx, expected, lhs_0); auto rhs_1 = demand_expr(fcx, expected, rhs_0); - e_1 = ast.expr_assign_op(op, lhs_1, rhs_1, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_assign_op(op, lhs_1, rhs_1, triv_ann(t)); } case (ast.expr_field(?lhs, ?rhs, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_field(lhs, rhs, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_field(lhs, rhs, triv_ann(t)); } case (ast.expr_index(?base, ?index, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_index(base, index, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_index(base, index, triv_ann(t)); } case (ast.expr_path(?pth, ?d, ?ann)) { auto t = demand_full(fcx, e.span, expected, @@ -1338,7 +1331,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, "did you pass it to check_expr() first?"; fail; } - case (ast.ann_type(_, ?tps_opt)) { + case (ast.ann_type(_, ?tps_opt, _)) { alt (tps_opt) { case (none[vec[@ty.t]]) { auto defn = option.get[ast.def](d); @@ -1359,26 +1352,28 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, } } - e_1 = ast.expr_path(pth, d, ast.ann_type(t, ty_params_opt)); + e_1 = ast.expr_path(pth, d, + ast.ann_type(t, ty_params_opt, + none[@ts_ann])); } case (ast.expr_ext(?p, ?args, ?body, ?expanded, ?ann)) { auto t = demand_full(fcx, e.span, expected, ann_to_type(ann), adk); - e_1 = ast.expr_ext(p, args, body, expanded, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(t)); } - case (ast.expr_fail) { e_1 = e.node; } - case (ast.expr_log(_)) { e_1 = e.node; } - case (ast.expr_break) { e_1 = e.node; } - case (ast.expr_cont) { e_1 = e.node; } - case (ast.expr_ret(_)) { e_1 = e.node; } - case (ast.expr_put(_)) { e_1 = e.node; } - case (ast.expr_be(_)) { e_1 = e.node; } - case (ast.expr_check_expr(_)) { e_1 = e.node; } + /* FIXME: this should probably check the type annotations */ + case (ast.expr_fail(_)) { e_1 = e.node; } + case (ast.expr_log(_,_)) { e_1 = e.node; } + case (ast.expr_break(_)) { e_1 = e.node; } + case (ast.expr_cont(_)) { e_1 = e.node; } + case (ast.expr_ret(_,_)) { e_1 = e.node; } + case (ast.expr_put(_,_)) { e_1 = e.node; } + case (ast.expr_be(_,_)) { e_1 = e.node; } + case (ast.expr_check_expr(_,_)) { e_1 = e.node; } case (ast.expr_port(?ann)) { auto t = demand(fcx, e.span, expected, ann_to_type(ann)); - e_1 = ast.expr_port(ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_port(triv_ann(t)); } case (ast.expr_chan(?es, ?ann)) { @@ -1394,7 +1389,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, fail; } } - e_1 = ast.expr_chan(es_1, ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_chan(es_1, triv_ann(t)); } case (ast.expr_alt(?discrim, ?arms_0, ?ann)) { @@ -1407,8 +1402,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e, index=arm_0.index); arms_1 += vec(arm_1); } - e_1 = ast.expr_alt(discrim, arms_1, - ast.ann_type(t, none[vec[@ty.t]])); + e_1 = ast.expr_alt(discrim, arms_1, triv_ann(t)); } case (_) { @@ -1449,8 +1443,7 @@ fn writeback_local(&option.t[@fn_ctxt] env, &span sp, @ast.local local) + local.ident); } auto local_ty = fcx.locals.get(local.id); - auto local_wb = @rec( - ann=ast.ann_type(local_ty, none[vec[@ty.t]]) + auto local_wb = @rec(ann=triv_ann(local_ty) with *local ); ret @fold.respan[ast.decl_](sp, ast.decl_local(local_wb)); @@ -1502,15 +1495,13 @@ fn check_pat(&@fn_ctxt fcx, @ast.pat pat) -> @ast.pat { auto new_pat; alt (pat.node) { case (ast.pat_wild(_)) { - new_pat = ast.pat_wild(ast.ann_type(next_ty_var(fcx.ccx), - none[vec[@ty.t]])); + new_pat = ast.pat_wild(triv_ann(next_ty_var(fcx.ccx))); } case (ast.pat_lit(?lt, _)) { - new_pat = ast.pat_lit(lt, ast.ann_type(check_lit(lt), - none[vec[@ty.t]])); + new_pat = ast.pat_lit(lt, triv_ann(check_lit(lt))); } case (ast.pat_bind(?id, ?def_id, _)) { - auto ann = ast.ann_type(next_ty_var(fcx.ccx), none[vec[@ty.t]]); + auto ann = triv_ann(next_ty_var(fcx.ccx)); new_pat = ast.pat_bind(id, def_id, ann); } case (ast.pat_tag(?p, ?subpats, ?vdef_opt, _)) { @@ -1670,7 +1661,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto lhs_1 = demand_expr(fcx, rhs_t0, lhs_0); auto rhs_1 = demand_expr(fcx, expr_ty(lhs_1), rhs_0); - auto ann = ast.ann_type(rhs_t0, none[vec[@ty.t]]); + auto ann = triv_ann(rhs_t0); ret tup(lhs_1, rhs_1, ann); } @@ -1698,7 +1689,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { alt (expr.node) { case (ast.expr_lit(?lit, _)) { auto typ = check_lit(lit); - auto ann = ast.ann_type(typ, none[vec[@ty.t]]); + auto ann = triv_ann(typ); ret @fold.respan[ast.expr_](expr.span, ast.expr_lit(lit, ann)); } @@ -1726,7 +1717,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (_) { /* fall through */ } } - auto ann = ast.ann_type(t, none[vec[@ty.t]]); + auto ann = triv_ann(t); ret @fold.respan[ast.expr_](expr.span, ast.expr_binary(binop, lhs_1, rhs_1, ann)); @@ -1757,7 +1748,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (_) { oper_t = strip_boxes(oper_t); } } - auto ann = ast.ann_type(oper_t, none[vec[@ty.t]]); + auto ann = triv_ann(oper_t); ret @fold.respan[ast.expr_](expr.span, ast.expr_unary(unop, oper_1, ann)); } @@ -1775,25 +1766,25 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (ast.expr_ext(?p, ?args, ?body, ?expanded, _)) { auto exp_ = check_expr(fcx, expanded); auto t = expr_ty(exp_); - auto ann = ast.ann_type(t, none[vec[@ty.t]]); + auto ann = triv_ann(t); ret @fold.respan[ast.expr_](expr.span, ast.expr_ext(p, args, body, exp_, ann)); } - case (ast.expr_fail) { + case (ast.expr_fail(_)) { // ??? ignoring ann ret expr; } - case (ast.expr_break) { + case (ast.expr_break(_)) { ret expr; } - case (ast.expr_cont) { + case (ast.expr_cont(_)) { ret expr; } - case (ast.expr_ret(?expr_opt)) { + case (ast.expr_ret(?expr_opt, _)) { alt (expr_opt) { case (none[@ast.expr]) { auto nil = plain_ty(ty.ty_nil); @@ -1808,13 +1799,13 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (some[@ast.expr](?e)) { auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); - ret @fold.respan[ast.expr_](expr.span, - ast.expr_ret(some(expr_1))); + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_ret(some(expr_1), ann_none)); } } } - case (ast.expr_put(?expr_opt)) { + case (ast.expr_put(?expr_opt, _)) { alt (expr_opt) { case (none[@ast.expr]) { auto nil = plain_ty(ty.ty_nil); @@ -1829,31 +1820,32 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (some[@ast.expr](?e)) { auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); - ret @fold.respan[ast.expr_](expr.span, - ast.expr_put(some(expr_1))); + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_put(some(expr_1), ann_none)); } } } - case (ast.expr_be(?e)) { + case (ast.expr_be(?e, _)) { /* FIXME: prove instead of check */ check (ast.is_call_expr(e)); auto expr_0 = check_expr(fcx, e); auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0); ret @fold.respan[ast.expr_](expr.span, - ast.expr_be(expr_1)); + ast.expr_be(expr_1, ann_none)); } - case (ast.expr_log(?e)) { + case (ast.expr_log(?e,_)) { auto expr_t = check_expr(fcx, e); - ret @fold.respan[ast.expr_](expr.span, ast.expr_log(expr_t)); + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_log(expr_t, ann_none)); } - case (ast.expr_check_expr(?e)) { + case (ast.expr_check_expr(?e, _)) { auto expr_t = check_expr(fcx, e); demand(fcx, expr.span, plain_ty(ty.ty_bool), expr_ty(expr_t)); - ret @fold.respan[ast.expr_](expr.span, - ast.expr_check_expr(expr_t)); + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_check_expr(expr_t, ann_none)); } case (ast.expr_assign(?lhs, ?rhs, _)) { @@ -1891,7 +1883,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } auto rhs_1 = demand_expr(fcx, item_t, rhs_0); - auto ann = ast.ann_type(chan_t, none[vec[@ty.t]]); + auto ann = triv_ann(chan_t); auto newexpr = ast.expr_send(lhs_1, rhs_1, ann); ret @fold.respan[ast.expr_](expr.span, newexpr); } @@ -1914,7 +1906,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } auto lhs_1 = demand_expr(fcx, item_t, lhs_0); - auto ann = ast.ann_type(item_t, none[vec[@ty.t]]); + auto ann = triv_ann(item_t); auto newexpr = ast.expr_recv(lhs_1, rhs_1, ann); ret @fold.respan[ast.expr_](expr.span, newexpr); } @@ -1943,7 +1935,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto thn_1 = demand_block(fcx, elsopt_t, thn_0); - auto ann = ast.ann_type(elsopt_t, none[vec[@ty.t]]); + auto ann = triv_ann(elsopt_t); ret @fold.respan[ast.expr_](expr.span, ast.expr_if(cond_1, thn_1, elsopt_1, ann)); @@ -1957,7 +1949,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { // FIXME: enforce that the type of the decl is the element type // of the seq. - auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(ty.ty_nil)); ret @fold.respan[ast.expr_](expr.span, ast.expr_for(decl_1, seq_1, body_1, ann)); @@ -1968,7 +1960,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto seq_1 = check_expr(fcx, seq); auto body_1 = check_block(fcx, body); - auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(ty.ty_nil)); ret @fold.respan[ast.expr_](expr.span, ast.expr_for_each(decl_1, seq_1, body_1, ann)); @@ -1979,7 +1971,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto cond_1 = demand_expr(fcx, plain_ty(ty.ty_bool), cond_0); auto body_1 = check_block(fcx, body); - auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(ty.ty_nil)); ret @fold.respan[ast.expr_](expr.span, ast.expr_while(cond_1, body_1, ann)); } @@ -1989,7 +1981,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto cond_1 = demand_expr(fcx, plain_ty(ty.ty_bool), cond_0); auto body_1 = check_block(fcx, body); - auto ann = ast.ann_type(block_ty(body_1), none[vec[@ty.t]]); + auto ann = triv_ann(block_ty(body_1)); ret @fold.respan[ast.expr_](expr.span, ast.expr_do_while(body_1, cond_1, ann)); @@ -2039,7 +2031,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto expr_1 = demand_expr(fcx, pattern_ty, expr_0); - auto ann = ast.ann_type(result_ty, none[vec[@ty.t]]); + auto ann = triv_ann(result_ty); ret @fold.respan[ast.expr_](expr.span, ast.expr_alt(expr_1, arms_1, ann)); } @@ -2049,10 +2041,10 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto ann; alt (b_0.node.expr) { case (some[@ast.expr](?expr)) { - ann = ast.ann_type(expr_ty(expr), none[vec[@ty.t]]); + ann = triv_ann(expr_ty(expr)); } case (none[@ast.expr]) { - ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]); + ann = triv_ann(plain_ty(ty.ty_nil)); } } ret @fold.respan[ast.expr_](expr.span, @@ -2092,7 +2084,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } auto t_1 = plain_ty(ty.ty_fn(proto_1, arg_tys_1, rt_1)); - auto ann = ast.ann_type(t_1, none[vec[@ty.t]]); + auto ann = triv_ann(t_1); ret @fold.respan[ast.expr_](expr.span, ast.expr_bind(result._0, result._1, ann)); @@ -2114,7 +2106,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } } - auto ann = ast.ann_type(rt_1, none[vec[@ty.t]]); + auto ann = triv_ann(rt_1); ret @fold.respan[ast.expr_](expr.span, ast.expr_call(f_1, args_1, ann)); } @@ -2143,7 +2135,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { // FIXME: Other typechecks needed - auto ann = ast.ann_type(plain_ty(ty.ty_task), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(ty.ty_task)); ret @fold.respan[ast.expr_](expr.span, ast.expr_spawn(dom, name, f_1, args_1, ann)); @@ -2162,7 +2154,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { + ty_to_str(t_1)); } - auto ann = ast.ann_type(t_1, none[vec[@ty.t]]); + auto ann = triv_ann(t_1); ret @fold.respan[ast.expr_](expr.span, ast.expr_cast(e_1, t, ann)); } @@ -2186,7 +2178,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } auto vec_sty = ty.ty_vec(rec(ty=t, mut=mut)); - auto ann = ast.ann_type(plain_ty(vec_sty), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(vec_sty)); ret @fold.respan[ast.expr_](expr.span, ast.expr_vec(args_1, mut, ann)); } @@ -2202,8 +2194,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { elts_mt += vec(rec(ty=expr_t, mut=e.mut)); } - auto ann = ast.ann_type(plain_ty(ty.ty_tup(elts_mt)), - none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(ty.ty_tup(elts_mt))); ret @fold.respan[ast.expr_](expr.span, ast.expr_tup(elts_1, ann)); } @@ -2234,8 +2225,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { alt (base) { case (none[@ast.expr]) { - ann = ast.ann_type(plain_ty(ty.ty_rec(fields_t)), - none[vec[@ty.t]]); + ann = triv_ann(plain_ty(ty.ty_rec(fields_t))); } case (some[@ast.expr](?bexpr)) { @@ -2255,7 +2245,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } } - ann = ast.ann_type(bexpr_t, none[vec[@ty.t]]); + ann = triv_ann(bexpr_t); for (ty.field f in fields_t) { auto found = false; @@ -2290,7 +2280,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { fcx.ccx.sess.span_err(expr.span, "bad index on tuple"); } - auto ann = ast.ann_type(args.(ix).ty, none[vec[@ty.t]]); + auto ann = triv_ann(args.(ix).ty); ret @fold.respan[ast.expr_](expr.span, ast.expr_field(base_1, field, @@ -2304,8 +2294,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { fcx.ccx.sess.span_err(expr.span, "bad index on record"); } - auto ann = ast.ann_type(fields.(ix).mt.ty, - none[vec[@ty.t]]); + auto ann = triv_ann(fields.(ix).mt.ty); ret @fold.respan[ast.expr_](expr.span, ast.expr_field(base_1, field, @@ -2322,7 +2311,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto meth = methods.(ix); auto t = plain_ty(ty.ty_fn(meth.proto, meth.inputs, meth.output)); - auto ann = ast.ann_type(t, none[vec[@ty.t]]); + auto ann = triv_ann(t); ret @fold.respan[ast.expr_](expr.span, ast.expr_field(base_1, field, @@ -2352,7 +2341,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { "non-integral type of vec index: " + ty_to_str(idx_t)); } - auto ann = ast.ann_type(mt.ty, none[vec[@ty.t]]); + auto ann = triv_ann(mt.ty); ret @fold.respan[ast.expr_](expr.span, ast.expr_index(base_1, idx_1, @@ -2366,7 +2355,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { + ty_to_str(idx_t)); } auto t = ty.ty_machine(common.ty_u8); - auto ann = ast.ann_type(plain_ty(t), none[vec[@ty.t]]); + auto ann = triv_ann(plain_ty(t)); ret @fold.respan[ast.expr_](expr.span, ast.expr_index(base_1, idx_1, @@ -2384,7 +2373,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { case (ast.expr_port(_)) { auto t = next_ty_var(fcx.ccx); auto pt = plain_ty(ty.ty_port(t)); - auto ann = ast.ann_type(pt, none[vec[@ty.t]]); + auto ann = triv_ann(pt); ret @fold.respan[ast.expr_](expr.span, ast.expr_port(ann)); } @@ -2394,7 +2383,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { alt (port_t.struct) { case (ty.ty_port(?subtype)) { auto ct = plain_ty(ty.ty_chan(subtype)); - auto ann = ast.ann_type(ct, none[vec[@ty.t]]); + auto ann = triv_ann(ct); ret @fold.respan[ast.expr_](expr.span, ast.expr_chan(expr_1, ann)); } @@ -2573,7 +2562,7 @@ fn check_item_fn(&@crate_ctxt ccx, &span sp, ast.ident ident, &ast._fn f, auto output_ty = ast_ty_to_ty_crate(ccx, f.decl.output); auto fn_sty = ty.ty_fn(f.proto, inputs, output_ty); - auto fn_ann = ast.ann_type(plain_ty(fn_sty), none[vec[@ty.t]]); + auto fn_ann = triv_ann(plain_ty(fn_sty)); auto item = ast.item_fn(ident, f, ty_params, id, fn_ann); ret @fold.respan[ast.item_](sp, item); diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs new file mode 100644 index 00000000000..9b670fc1ea0 --- /dev/null +++ b/src/comp/middle/typestate_check.rs @@ -0,0 +1,496 @@ +import front.ast; +import front.ast.ann; +import front.ast.ty; +import front.ast.mutability; +import front.ast.item; +import front.ast.block; +import front.ast.block_; +import front.ast.block_index_entry; +import front.ast.decl; +import front.ast.stmt; +import front.ast.stmt_; +import front.ast.stmt_decl; +import front.ast.stmt_expr; +import front.ast.decl_local; +import front.ast.decl_item; +import front.ast.ident; +import front.ast.def_id; +import front.ast.ann; +import front.ast.init; +import front.ast.expr; +import front.ast.expr_call; +import front.ast.expr_path; +import front.ast.expr_log; +import front.ast.path; +import front.ast.crate_directive; +import front.ast.fn_decl; +import front.ast._obj; +import front.ast.native_mod; +import front.ast.variant; +import front.ast.ty_param; +import front.ast.ty; +import front.ast.proto; +import front.ast.pat; +import front.ast.binop; +import front.ast.unop; +import front.ast.def; +import front.ast.lit; +import front.ast.init_op; +import front.ast.initializer; +import front.ast.local; +import front.ast._fn; +import front.ast.ann_none; +import front.ast.ann_type; +import front.ast._obj; +import front.ast._mod; + +import middle.fold; +import middle.fold.respan; +import driver.session; +import util.common; +import util.common.span; +import util.common.spanned; +import util.common.new_str_hash; +import util.typestate_ann; +import util.typestate_ann.ts_ann; +import util.typestate_ann.empty_pre_post; +import util.typestate_ann.true_precond; +import util.typestate_ann.true_postcond; +import util.typestate_ann.postcond; +import util.typestate_ann.precond; +import util.typestate_ann.pre_and_post; +import util.typestate_ann.get_pre; +import util.typestate_ann.get_post; + +import middle.ty; +import middle.ty.ann_to_type; +import middle.ty.arg; +import middle.ty.block_ty; +import middle.ty.expr_ty; +import middle.ty.ty_to_str; + +import pretty.pprust.print_block; +import pretty.pprust.print_expr; +import pretty.pp.mkstate; +import std.io.stdout; +import std.io.str_writer; +import std.io.string_writer; +import std._vec.map; +import std._vec; +import std._vec.len; +import std._vec.pop; +import std._vec.push; +import std._vec.slice; +import std.option; +import std.option.t; +import std.option.some; +import std.option.none; +import std.map.hashmap; +import std.list; +import std.list.list; +import std.list.cons; +import std.list.nil; +import std.list.foldl; +import std.list.find; + +import util.typestate_ann; +import util.typestate_ann.difference; +import util.typestate_ann.union; +import util.typestate_ann.pps_len; +import util.typestate_ann.require_and_preserve; + +/**********************************************************************/ +/* mapping from variable name to bit number */ +type fn_info = std.map.hashmap[ident, uint]; + +fn bit_num(ident v, fn_info m) -> uint { + ret m.get(v); +} +fn num_locals(fn_info m) -> uint { + ret m.size(); +} + +fn mk_fn_info(_fn f) -> fn_info { + ret new_str_hash[uint](); /* FIXME: actually implement this */ +} +/**********************************************************************/ +fn expr_ann(&expr e) -> ann { + alt(e.node) { + case (ast.expr_vec(_,_,?a)) { + ret a; + } + case (ast.expr_tup(_,?a)) { + ret a; + } + case (ast.expr_rec(_,_,?a)) { + ret a; + } + case (ast.expr_call(_,_,?a)) { + ret a; + } + case (ast.expr_bind(_,_,?a)) { + ret a; + } + case (ast.expr_binary(_,_,_,?a)) { + ret a; + } + case (ast.expr_unary(_,_,?a)) { + ret a; + } + case (ast.expr_lit(_,?a)) { + ret a; + } + case (ast.expr_cast(_,_,?a)) { + ret a; + } + case (ast.expr_if(_,_,_,?a)) { + ret a; + } + case (ast.expr_while(_,_,?a)) { + ret a; + } + case (ast.expr_for(_,_,_,?a)) { + ret a; + } + case (ast.expr_for_each(_,_,_,?a)) { + ret a; + } + case (ast.expr_do_while(_,_,?a)) { + ret a; + } + case (ast.expr_alt(_,_,?a)) { + ret a; + } + case (ast.expr_block(_,?a)) { + ret a; + } + case (ast.expr_assign(_,_,?a)) { + ret a; + } + case (ast.expr_assign_op(_,_,_,?a)) { + ret a; + } + case (ast.expr_send(_,_,?a)) { + ret a; + } + case (ast.expr_recv(_,_,?a)) { + ret a; + } + case (ast.expr_field(_,_,?a)) { + ret a; + } + case (ast.expr_index(_,_,?a)) { + ret a; + } + case (ast.expr_path(_,_,?a)) { + ret a; + } + case (ast.expr_ext(_,_,_,_,?a)) { + ret a; + } + case (ast.expr_fail(?a)) { + ret a; + } + case (ast.expr_ret(_,?a)) { + ret a; + } + case (ast.expr_put(_,?a)) { + ret a; + } + case (ast.expr_be(_,?a)) { + ret a; + } + case (ast.expr_log(_,?a)) { + ret a; + } + case (ast.expr_check_expr(_,?a)) { + ret a; + } + case (ast.expr_port(?a)) { + ret a; + } + case (ast.expr_chan(_,?a)) { + ret a; + } + } +} + +fn expr_pp(&@expr e) -> pre_and_post { + alt (expr_ann(*e)) { + case (ann_none) { + log "expr_pp: the impossible happened (no annotation)"; + fail; + } + case (ann_type(_, _, ?maybe_pp)) { + alt (maybe_pp) { + case (none[@ts_ann]) { + log "expr_pp: the impossible happened (no pre/post)"; + fail; + } + case (some[@ts_ann](?p)) { + ret *p; + } + } + } + } +} + +fn expr_precond(&expr e) -> precond { + ret (expr_pp(@e)).precondition; +} + +fn expr_postcond(&@expr e) -> postcond { + ret (expr_pp(e)).postcondition; +} + +fn with_pp(ann a, @pre_and_post p) -> ann { + alt (a) { + case (ann_none) { + log("with_pp: the impossible happened"); + fail; /* shouldn't happen b/c code is typechecked */ + } + case (ann_type(?t, ?ps, _)) { + ret (ann_type(t, ps, some[@ts_ann](p))); + } + } +} + +// Given a list of pres and posts for exprs e0 ... en, +// return the precondition for evaluating each expr in order. +// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire +// precondition shouldn't include x. +fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond { + let uint sz = len[pre_and_post](pps); + + if (sz == 0u) { + ret true_precond(num_vars); + } + else { + auto first = pps.(0); + check (pps_len(first) == num_vars); + let precond rest = seq_preconds(num_vars, + slice[pre_and_post](pps, 1u, sz)); + difference(rest, first.postcondition); + union(first.precondition, rest); + ret (first.precondition); + } +} + +fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond { + auto other = rest.(0); + union(first, other); + union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest))); + ret first; +} + +fn union_postconds(&vec[postcond] pcs) -> postcond { + check (len[postcond](pcs) > 0u); + + be union_postconds_go(pcs.(0), pcs); +} + +fn print_ident(&ident i) -> () { + log(" " + i + " "); +} + +fn print_idents(vec[ident] idents) -> () { + if(len[ident](idents) == 0u) { + ret; + } + else { + log("an ident: " + pop[ident](idents)); + print_idents(idents); + } +} + +fn find_pre_post_mod(&_mod m) -> _mod { + ret m; /* FIXME */ +} + +fn find_pre_post_native_mod(&native_mod m) -> native_mod { + ret m; /* FIXME */ +} + +fn find_pre_post_obj(_obj o) -> _obj { + ret o; /* FIXME */ +} + +impure fn find_pre_post_item(fn_info enclosing, &item i) -> item { + alt (i.node) { + case (ast.item_const(?id, ?t, ?e, ?di, ?a)) { + auto e_pp = find_pre_post_expr(enclosing, *e); + ret (respan(i.span, + ast.item_const(id, t, e_pp, di, + with_pp(a, @expr_pp(e_pp))))); + } + case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) { + auto f_pp = find_pre_post_fn(f); + ret (respan(i.span, + ast.item_fn(id, f_pp, ps, di, a))); + } + case (ast.item_mod(?id, ?m, ?di)) { + auto m_pp = find_pre_post_mod(m); + ret (respan(i.span, + ast.item_mod(id, m_pp, di))); + } + case (ast.item_native_mod(?id, ?nm, ?di)) { + auto n_pp = find_pre_post_native_mod(nm); + ret (respan(i.span, + ast.item_native_mod(id, n_pp, di))); + } + case (ast.item_ty(_,_,_,_,_)) { + ret i; + } + case (ast.item_tag(_,_,_,_)) { + ret i; + } + case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) { + auto o_pp = find_pre_post_obj(o); + ret (respan(i.span, + ast.item_obj(id, o_pp, ps, di, a))); + } + } +} + +impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr { + auto num_local_vars = num_locals(enclosing); + + fn do_rand_(fn_info enclosing, &@expr e) -> @expr { + be find_pre_post_expr(enclosing, *e); + } + + auto do_rand = bind do_rand_(enclosing,_); + + alt(e.node) { + case(expr_call(?oper, ?rands, ?a)) { + auto pp_oper = find_pre_post_expr(enclosing, *oper); + + auto f = do_rand; + auto pp_rands = _vec.map[@expr, @expr](f, rands); + + auto g = expr_pp; + auto pps = _vec.map[@expr, pre_and_post] + (g, pp_rands); + _vec.push[pre_and_post](pps, expr_pp(pp_oper)); + auto h = get_post; + auto res_postconds = _vec.map[pre_and_post, postcond](h, pps); + auto res_postcond = union_postconds(res_postconds); + let @pre_and_post pp = + @rec(precondition=seq_preconds(num_local_vars, pps), + postcondition=res_postcond); + let ann a_res = with_pp(a, pp); + ret (@respan(e.span, + expr_call(pp_oper, pp_rands, a_res))); + + } + case(expr_path(?p, ?maybe_def, ?a)) { + check (len[ident](p.node.idents) > 0u); + auto referent = p.node.idents.(0); + auto i = bit_num(referent, enclosing); + auto res = empty_pre_post(num_local_vars); + require_and_preserve(i, *res); + ret (@respan + (e.span, + expr_path(p, maybe_def, + with_pp(a, res)))); + } + case(expr_log(?e, ?a)) { + auto e_pp = find_pre_post_expr(enclosing, *e); + ret (@respan(e.span, + expr_log(e_pp, with_pp(a, @expr_pp(e_pp))))); + } + case(_) { + log("this sort of expr isn't implemented!"); + fail; + } + } +} + +impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s) + -> ast.stmt { + auto num_local_vars = num_locals(enclosing); + + alt(s.node) { + case(ast.stmt_decl(?adecl)) { + alt(adecl.node) { + case(ast.decl_local(?alocal)) { + alt(alocal.init) { + case(some[ast.initializer](?an_init)) { + let @expr r = find_pre_post_expr(enclosing, *an_init.expr); + let init_op o = an_init.op; + let initializer a_i = rec(op=o, expr=r); + let ann res_ann = with_pp(alocal.ann, @expr_pp(r)); + let @local res_local = + @rec(ty=alocal.ty, infer=alocal.infer, + ident=alocal.ident, init=some[initializer](a_i), + id=alocal.id, ann=res_ann); + let stmt_ res = stmt_decl(@respan(adecl.span, + decl_local(res_local))); + ret (respan(s.span, res)); + } + case(none[ast.initializer]) { + // log("pre/post for init of " + alocal.ident + ": none"); + let ann res_ann = with_pp(alocal.ann, + empty_pre_post(num_local_vars)); + let @local res_local = + @rec(ty=alocal.ty, infer=alocal.infer, + ident=alocal.ident, init=none[initializer], + id=alocal.id, ann=res_ann); + let stmt_ res = + stmt_decl + (@respan(adecl.span, decl_local(res_local))); + ret (respan (s.span, res)); + } + } + } + case(decl_item(?anitem)) { + auto res_item = find_pre_post_item(enclosing, *anitem); + ret (respan(s.span, stmt_decl(@respan(adecl.span, + decl_item(@res_item))))); + } + } + } + case(stmt_expr(?e)) { + let @expr e_pp = find_pre_post_expr(enclosing, *e); + ret (respan(s.span, stmt_expr(e_pp))); + } + } +} + +fn find_pre_post_block(fn_info enclosing, block b) -> block { + fn do_one_(fn_info i, &@stmt s) -> @stmt { + ret (@find_pre_post_for_each_stmt(i, *s)); + } + auto do_one = bind do_one_(enclosing, _); + + auto ss = _vec.map[@stmt, @stmt](do_one, b.node.stmts); + fn do_inner_(fn_info i, &@expr e) -> @expr { + ret find_pre_post_expr(i, *e); + } + auto do_inner = bind do_inner_(enclosing, _); + let option.t[@expr] e_ = option.map[@expr, @expr](do_inner, b.node.expr); + let block_ b_res = rec(stmts=ss, expr=e_, index=b.node.index); + ret respan(b.span, b_res); +} + +fn find_pre_post_fn(&_fn f) -> _fn { + let fn_info fi = mk_fn_info(f); + ret rec(decl=f.decl, proto=f.proto, + body=find_pre_post_block(fi, f.body)); +} + +fn check_item_fn(&@() ignore, &span sp, ident i, &ast._fn f, + vec[ast.ty_param] ty_params, def_id id, ann a) -> @item { + + auto res_f = find_pre_post_fn(f); + + ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a)); +} + +fn check_crate(@ast.crate crate) -> @ast.crate { + auto fld = fold.new_identity_fold[@()](); + + fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld); + + ret fold.fold_crate[@()](@(), fld, crate); +} diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs index f3b0f3fe979..b0d6fb94187 100644 --- a/src/comp/pretty/pprust.rs +++ b/src/comp/pretty/pprust.rs @@ -611,16 +611,16 @@ impure fn print_expr(ps s, &@ast.expr expr) { case (ast.expr_path(?path,_,_)) { print_path(s, path); } - case (ast.expr_fail) { + case (ast.expr_fail(_)) { wrd(s.s, "fail"); } - case (ast.expr_break) { + case (ast.expr_break(_)) { wrd(s.s, "break"); } - case (ast.expr_cont) { + case (ast.expr_cont(_)) { wrd(s.s, "cont"); } - case (ast.expr_ret(?result)) { + case (ast.expr_ret(?result,_)) { wrd(s.s, "ret"); alt (result) { case (option.some[@ast.expr](?expr)) { @@ -630,7 +630,7 @@ impure fn print_expr(ps s, &@ast.expr expr) { case (_) {} } } - case (ast.expr_put(?result)) { + case (ast.expr_put(?result,_)) { wrd(s.s, "put"); alt (result) { case (option.some[@ast.expr](?expr)) { @@ -640,15 +640,15 @@ impure fn print_expr(ps s, &@ast.expr expr) { case (_) {} } } - case (ast.expr_be(?result)) { + case (ast.expr_be(?result,_)) { wrd1(s, "be"); print_expr(s, result); } - case (ast.expr_log(?expr)) { + case (ast.expr_log(?expr,_)) { wrd1(s, "log"); print_expr(s, expr); } - case (ast.expr_check_expr(?expr)) { + case (ast.expr_check_expr(?expr,_)) { wrd1(s, "check"); popen_h(s); print_expr(s, expr); diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc index e15d1842759..afa84711707 100644 --- a/src/comp/rustc.rc +++ b/src/comp/rustc.rc @@ -39,6 +39,7 @@ mod pretty { mod util { mod common; + mod typestate_ann; } auth driver.rustc.main = impure; @@ -55,8 +56,10 @@ auth middle.trans.copy_any_self_to_alloca = impure; auth middle.trans.copy_args_to_allocas = impure; auth middle.trans.trans_block = impure; auth middle.trans.alloc_ty = impure; +auth middle.typestate_check.log_expr = impure; auth lib.llvm = unsafe; auth pretty.pprust = impure; +auth middle.typestate_check.find_pre_post_block = impure; mod lib { alt (target_os) { diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs new file mode 100644 index 00000000000..a4698c5d40f --- /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 
 to be initialized,
+   and given the precondition, it guarantees that the idents in  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
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index c3fc7035a84..f2b169efb2c 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -207,6 +207,29 @@ fn map2[T,U,V](&operator2[T,U,V] f, &vec[mutable? T] v0, &vec[mutable? U] v1)
     ret u;
 }
 
+fn find[T](fn (&T) -> bool f, &vec[mutable? T] v) -> option.t[T] {
+    for (T elt in v) {
+        if (f(elt)) {
+            ret some[T](elt);
+        }
+    }
+
+    ret none[T];
+}
+
+fn foldl[T, U](fn (&U, &T) -> U p, &U z, &vec[T] v) -> U {
+    auto sz = len[T](v);
+
+    if (sz == 0u) {
+        ret z;
+    }
+    else {
+        auto rest = slice[T](v, 1u, sz);
+
+        ret (p(foldl[T,U](p, z, rest), v.(0)));
+    }
+}
+
 // Local Variables:
 // mode: rust;
 // fill-column: 78;