aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/comp/middle/fold.rs3
-rw-r--r--src/comp/middle/typeck.rs3
-rw-r--r--src/comp/middle/typestate_check.rs838
-rw-r--r--src/comp/pretty/pprust.rs17
-rw-r--r--src/comp/util/common.rs29
-rw-r--r--src/comp/util/typestate_ann.rs16
-rw-r--r--src/lib/_vec.rs2
-rw-r--r--src/lib/option.rs12
-rw-r--r--src/test/compile-fail/use-uninit-dtor.rs12
9 files changed, 833 insertions, 99 deletions
diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index ef592fc8..25617640 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -291,8 +291,6 @@ type ast_fold[ENV] =
(fn(&ENV e, ann a) -> ann) fold_ann,
// Additional nodes.
- (fn(&ENV e, &span sp,
- &ast.block_) -> block) fold_block,
(fn(&ENV e, &fn_decl decl,
ast.proto proto,
@@ -1716,7 +1714,6 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
fold_ann = bind identity_fold_ann[ENV](_,_),
- fold_block = bind identity_fold_block[ENV](_,_,_),
fold_fn = bind identity_fold_fn[ENV](_,_,_,_),
fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_),
fold_mod = bind identity_fold_mod[ENV](_,_),
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index 87c11a7b..95ed4c2f 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -1469,7 +1469,8 @@ mod Pushdown {
}
case (none[@ast.expr]) {
Demand.simple(fcx, bloc.span, expected, plain_ty(ty.ty_nil));
- ret bloc;
+ ret fold.respan[ast.block_](bloc.span,
+ rec(a = boring_ann() with bloc.node));
}
}
}
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 7d7108ff..3e67cf2e 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -1,12 +1,16 @@
import front.ast;
import front.ast.ann;
+import front.ast.method;
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.mod_index_entry;
+import front.ast.obj_field;
import front.ast.decl;
+import front.ast.arm;
import front.ast.stmt;
import front.ast.stmt_;
import front.ast.stmt_decl;
@@ -17,6 +21,7 @@ import front.ast.decl_item;
import front.ast.ident;
import front.ast.def_id;
import front.ast.ann;
+import front.ast.field;
import front.ast.expr;
import front.ast.expr_call;
import front.ast.expr_vec;
@@ -29,11 +34,33 @@ import front.ast.expr_block;
import front.ast.expr_rec;
import front.ast.expr_if;
import front.ast.expr_binary;
+import front.ast.expr_unary;
import front.ast.expr_assign;
+import front.ast.expr_assign_op;
import front.ast.expr_while;
+import front.ast.expr_do_while;
+import front.ast.expr_alt;
import front.ast.expr_lit;
import front.ast.expr_ret;
+import front.ast.expr_self_method;
+import front.ast.expr_bind;
+import front.ast.expr_spawn;
+import front.ast.expr_ext;
+import front.ast.expr_fail;
+import front.ast.expr_break;
+import front.ast.expr_cont;
+import front.ast.expr_send;
+import front.ast.expr_recv;
+import front.ast.expr_put;
+import front.ast.expr_port;
+import front.ast.expr_chan;
+import front.ast.expr_be;
+import front.ast.expr_check_expr;
+import front.ast.expr_cast;
+import front.ast.expr_for;
+import front.ast.expr_for_each;
import front.ast.path;
+import front.ast.elt;
import front.ast.crate_directive;
import front.ast.fn_decl;
import front.ast._obj;
@@ -59,6 +86,7 @@ import front.ast.crate;
import front.ast.mod_index_entry;
import front.ast.mie_item;
import front.ast.item_fn;
+import front.ast.item_obj;
import front.ast.def_local;
import middle.fold;
@@ -73,6 +101,8 @@ import util.common.uistr;
import util.common.elt_exprs;
import util.common.field_exprs;
import util.common.log_expr;
+import util.common.log_stmt;
+import util.common.log_block;
import util.typestate_ann;
import util.typestate_ann.ts_ann;
import util.typestate_ann.empty_pre_post;
@@ -102,6 +132,7 @@ import util.typestate_ann.empty_ann;
import util.typestate_ann.extend_prestate;
import util.typestate_ann.extend_poststate;
import util.typestate_ann.intersect;
+import util.typestate_ann.pp_clone;
import middle.ty;
import middle.ty.ann_to_type;
@@ -124,11 +155,13 @@ import std._vec.pop;
import std._vec.push;
import std._vec.slice;
import std._vec.unzip;
+import std._vec.plus_option;
import std.option;
import std.option.t;
import std.option.some;
import std.option.none;
import std.option.from_maybe;
+import std.option.maybe;
import std.option.is_none;
import std.option.get;
import std.map.hashmap;
@@ -151,24 +184,6 @@ import util.typestate_ann.require_and_preserve;
/**** debugging junk ****/
-fn log_stmt(stmt st) -> () {
- let str_writer s = string_writer();
- auto out_ = mkstate(s.get_writer(), 80u);
- auto out = @rec(s=out_,
- comments=option.none[vec[front.lexer.cmnt]],
- mutable cur_cmnt=0u);
- alt (st.node) {
- case (ast.stmt_decl(?decl,_)) {
- print_decl(out, decl);
- }
- case (ast.stmt_expr(?ex,_)) {
- print_expr(out, ex);
- }
- case (_) { /* do nothing */ }
- }
- log(s.get_str());
-}
-
fn log_bitv(fn_info enclosing, bitv.t v) {
auto s = "";
@@ -222,12 +237,16 @@ fn print_idents(vec[ident] idents) -> () {
type var_info = tup(uint, ident);
type fn_info = std.map.hashmap[def_id, var_info];
/* mapping from function name to fn_info map */
-type _fn_info_map = std.map.hashmap[def_id, fn_info];
+type fn_info_map = std.map.hashmap[def_id, fn_info];
fn bit_num(def_id v, fn_info m) -> uint {
check (m.contains_key(v));
ret m.get(v)._0;
}
+fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
+ check (fm.contains_key(did));
+ ret fm.get(did);
+}
fn var_is_local(def_id v, fn_info m) -> bool {
ret (m.contains_key(v));
@@ -254,6 +273,7 @@ fn find_locals(_fn f) -> vec[tup(ident,def_id)] {
}
fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
+ log(nm + " |-> " + util.common.uistr(next));
tbl.insert(v, tup(next,nm));
ret (next + 1u);
}
@@ -277,23 +297,42 @@ fn mk_fn_info(_fn f) -> fn_info {
ret res;
}
-/* extends mk_fn_info to an item, side-effecting the map fi from
+/* extends mk_fn_info to a function item, side-effecting the map fi from
function IDs to fn_info maps */
-fn mk_fn_info_item_fn(&_fn_info_map fi, &span sp, ident i, &ast._fn f,
+fn mk_fn_info_item_fn(&fn_info_map fi, &span sp, ident i, &ast._fn f,
vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
fi.insert(id, mk_fn_info(f));
+ log(i + " has " + uistr(num_locals(mk_fn_info(f))) + " local vars");
ret @respan(sp, item_fn(i, f, ty_params, id, a));
}
+/* extends mk_fn_info to an obj item, side-effecting the map fi from
+ function IDs to fn_info maps */
+fn mk_fn_info_item_obj(&fn_info_map fi, &span sp, ident i, &ast._obj o,
+ vec[ast.ty_param] ty_params, ast.obj_def_ids odid, ann a) -> @item {
+ auto all_methods = _vec.clone[@method](o.methods);
+ plus_option[@method](all_methods, o.dtor);
+ for (@method m in all_methods) {
+ /* FIXME: also need to pass in fields so we can say
+ they're initialized? */
+ fi.insert(m.node.id, mk_fn_info(m.node.meth));
+ log(m.node.ident + " has " +
+ uistr(num_locals(mk_fn_info(m.node.meth))) + " local vars");
+ }
+ ret @respan(sp, item_obj(i, o, ty_params, odid, a));
+}
+
/* initializes the global fn_info_map (mapping each function ID, including
nested locally defined functions, onto a mapping from local variable name
to bit number) */
-fn mk_f_to_fn_info(@ast.crate c) -> _fn_info_map {
+fn mk_f_to_fn_info(@ast.crate c) -> fn_info_map {
auto res = new_def_hash[fn_info]();
- auto fld = fold.new_identity_fold[_fn_info_map]();
- fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_) with *fld);
- fold.fold_crate[_fn_info_map](res, fld, c);
+ auto fld = fold.new_identity_fold[fn_info_map]();
+ fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_),
+ fold_item_obj = bind mk_fn_info_item_obj(_,_,_,_,_,_,_)
+ with *fld);
+ fold.fold_crate[fn_info_map](res, fld, c);
ret res;
}
@@ -438,6 +477,10 @@ fn ann_to_ts_ann_fail_more(ann a) -> @ts_ann {
}
}
+fn ann_to_poststate(ann a) -> poststate {
+ ret (ann_to_ts_ann_fail_more(a)).states.poststate;
+}
+
fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
alt (s.node) {
case (stmt_decl(_,?a)) {
@@ -452,13 +495,6 @@ fn stmt_to_ann(&stmt s) -> option.t[@ts_ann] {
}
}
-/*
-/* fails if no annotation */
-fn stmt_pp(&stmt s) -> pre_and_post {
- ret (stmt_ann(s)).conditions;
-}
-*/
-
/* fails if e has no annotation */
fn expr_states(&expr e) -> pre_and_post_state {
alt (expr_ann(e)) {
@@ -501,6 +537,18 @@ fn expr_pp(&expr e) -> pre_and_post {
}
}
+fn stmt_pp(&stmt s) -> pre_and_post {
+ alt (stmt_to_ann(s)) {
+ case (none[@ts_ann]) {
+ log "stmt_pp: the impossible happened (no annotation)";
+ fail;
+ }
+ case (some[@ts_ann](?p)) {
+ ret p.conditions;
+ }
+ }
+}
+
/* fails if b has no annotation */
/* FIXME: factor out code in the following two functions (block_ts_ann) */
fn block_pp(&block b) -> pre_and_post {
@@ -624,18 +672,19 @@ fn with_pp(ann a, pre_and_post p) -> ann {
// 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);
- check(sz >= 1u);
- auto first = pps.(0);
-
- if (sz > 1u) {
+
+ if (sz >= 1u) {
+ 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;
+ }
+ else {
+ ret true_precond(num_vars);
}
-
- ret (first.precondition);
}
/* works on either postconds or preconds
@@ -681,18 +730,48 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
/******* AST-traversing code ********/
fn find_pre_post_mod(&_mod m) -> _mod {
- ret m; /* FIXME */
+ log("implement find_pre_post_mod!");
+ fail;
+}
+
+fn find_pre_post_state_mod(&_mod m) -> bool {
+ log("implement find_pre_post_state_mod!");
+ fail;
}
fn find_pre_post_native_mod(&native_mod m) -> native_mod {
- ret m; /* FIXME */
+ log("implement find_pre_post_native_mod");
+ fail;
+}
+
+fn find_pre_post_state_native_mod(&native_mod m) -> bool {
+ log("implement find_pre_post_state_native_mod!");
+ fail;
}
-fn find_pre_post_obj(_obj o) -> _obj {
- ret o; /* FIXME */
+fn find_pre_post_obj(&fn_info_map fm, _obj o) -> () {
+ fn do_a_method(fn_info_map fm, &@method m) -> () {
+ check(fm.contains_key(m.node.id));
+ find_pre_post_fn(fm, fm.get(m.node.id), m.node.meth);
+ }
+ auto f = bind do_a_method(fm,_);
+ _vec.map[@method, ()](f, o.methods);
+ option.map[@method, ()](f, o.dtor);
}
-fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
+fn find_pre_post_state_obj(fn_info_map fm, _obj o) -> bool {
+ fn do_a_method(fn_info_map fm, &@method m) -> bool {
+ check(fm.contains_key(m.node.id));
+ ret find_pre_post_state_fn(fm, fm.get(m.node.id), m.node.meth);
+ }
+ auto f = bind do_a_method(fm,_);
+ auto flags = _vec.map[@method, bool](f, o.methods);
+ auto changed = _vec.or(flags);
+ changed = changed || maybe[@method, bool](false, f, o.dtor);
+ ret changed;
+}
+
+fn find_pre_post_item(fn_info_map fm, fn_info enclosing, &item i) -> () {
alt (i.node) {
case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
find_pre_post_expr(fm, enclosing, *e);
@@ -714,7 +793,7 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
ret;
}
case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
- find_pre_post_obj(o);
+ find_pre_post_obj(fm, o);
}
}
}
@@ -723,9 +802,9 @@ fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> () {
sets the precondition in a to be the result of combining
the preconditions for <args>, and the postcondition in a to
be the union of all postconditions for <args> */
-fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_exprs(&fn_info_map fm, &fn_info enclosing,
&vec[@expr] args, ann a) {
- fn do_one(_fn_info_map fm, fn_info enclosing,
+ fn do_one(fn_info_map fm, fn_info enclosing,
&@expr e) -> () {
find_pre_post_expr(fm, enclosing, *e);
}
@@ -747,16 +826,21 @@ fn find_pre_post_exprs(&_fn_info_map fm, &fn_info enclosing,
}
/* Fills in annotations as a side effect. Does not rebuild the expr */
-fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
+fn find_pre_post_expr(&fn_info_map fm, &fn_info enclosing, &expr e) -> () {
auto num_local_vars = num_locals(enclosing);
- fn do_rand_(_fn_info_map fm, fn_info enclosing, &@expr e) -> () {
+ fn do_rand_(fn_info_map fm, fn_info enclosing, &@expr e) -> () {
find_pre_post_expr(fm, enclosing, *e);
}
fn pp_one(&@expr e) -> pre_and_post {
be expr_pp(*e);
}
+ /* log("find_pre_post_expr (num_locals =" +
+ uistr(num_local_vars) + "):");
+ log_expr(e);
+ */
+
alt(e.node) {
case(expr_call(?operator, ?operands, ?a)) {
auto args = _vec.clone[@expr](operands);
@@ -866,6 +950,10 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
FIXME */
find_pre_post_exprs(fm, enclosing, vec(l, r), a);
}
+ case (expr_unary(_,?operand,?a)) {
+ find_pre_post_expr(fm, enclosing, *operand);
+ set_pre_and_post(a, expr_pp(*operand));
+ }
case (expr_while(?test, ?body, ?a)) {
find_pre_post_expr(fm, enclosing, *test);
find_pre_post_block(fm, enclosing, body);
@@ -881,8 +969,41 @@ fn find_pre_post_expr(&_fn_info_map fm, &fn_info enclosing, &expr e) -> () {
case (expr_index(?e, ?sub, ?a)) {
find_pre_post_exprs(fm, enclosing, vec(e, sub), a);
}
+ case (expr_alt(?e, ?alts, ?a)) {
+ find_pre_post_expr(fm, enclosing, *e);
+ fn do_an_alt(fn_info_map fm, fn_info enc, &arm an_alt)
+ -> pre_and_post {
+ find_pre_post_block(fm, enc, an_alt.block);
+ ret block_pp(an_alt.block);
+ }
+ auto f = bind do_an_alt(fm, enclosing, _);
+ auto alt_pps = _vec.map[arm, pre_and_post](f, alts);
+ fn combine_pp(pre_and_post antec,
+ uint num_local_vars, &pre_and_post pp,
+ &pre_and_post next) -> pre_and_post {
+ union(pp.precondition, seq_preconds(num_local_vars,
+ vec(antec, next)));
+ intersect(pp.postcondition, next.postcondition);
+ ret pp;
+ }
+ auto e_pp1 = expr_pp(*e);
+ auto e_pp = pp_clone(e_pp1);
+ auto g = bind combine_pp(e_pp, num_local_vars, _, _);
+ set_pre_and_post(a, _vec.foldl[pre_and_post, pre_and_post]
+ (g, e_pp, alt_pps));
+ }
+ case (expr_field(?operator, _, ?a)) {
+ find_pre_post_expr(fm, enclosing, *operator);
+ set_pre_and_post(a, expr_pp(*operator));
+ }
+ case (expr_fail(?a)) {
+ set_pre_and_post(a,
+ rec(precondition=empty_prestate(num_local_vars),
+ postcondition=true_postcond(num_local_vars)));
+ }
case(_) {
log("this sort of expr isn't implemented!");
+ log_expr(e);
fail;
}
}
@@ -902,7 +1023,7 @@ fn gen_poststate(&fn_info enclosing, &ann a, def_id id) -> bool {
ret set_in_poststate(i, (ann_to_ts_ann_fail_more(a)).states);
}
-fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
+fn find_pre_post_stmt(fn_info_map fm, &fn_info enclosing, &ast.stmt s)
-> () {
auto num_local_vars = num_locals(enclosing);
alt(s.node) {
@@ -941,27 +1062,49 @@ fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
}
}
-fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
+fn find_pre_post_block(&fn_info_map fm, &fn_info enclosing, block b)
-> () {
- fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> () {
+ fn do_one_(fn_info_map fm, fn_info i, &@stmt s) -> () {
find_pre_post_stmt(fm, i, *s);
}
auto do_one = bind do_one_(fm, enclosing, _);
_vec.map[@stmt, ()](do_one, b.node.stmts);
- fn do_inner_(_fn_info_map fm, fn_info i, &@expr e) -> () {
+ fn do_inner_(fn_info_map fm, fn_info i, &@expr e) -> () {
find_pre_post_expr(fm, i, *e);
}
auto do_inner = bind do_inner_(fm, enclosing, _);
option.map[@expr, ()](do_inner, b.node.expr);
- /* FIXME needs to set up the ann for b!!!!!!!!!!! */
+
+ let vec[pre_and_post] pps = vec();
+
+ fn get_pp_stmt(&@stmt s) -> pre_and_post {
+ ret stmt_pp(*s);
+ }
+ auto f = get_pp_stmt;
+ pps += _vec.map[@stmt, pre_and_post](f, b.node.stmts);
+ fn get_pp_expr(&@expr e) -> pre_and_post {
+ ret expr_pp(*e);
+ }
+ auto g = get_pp_expr;
+ plus_option[pre_and_post](pps,
+ option.map[@expr, pre_and_post](g, b.node.expr));
+ auto block_precond = seq_preconds(num_locals(enclosing), pps);
+ auto h = get_post;
+ auto postconds = _vec.map[pre_and_post, postcond](h, pps);
+ /* A block may be empty, so this next line ensures that the postconds
+ vector is non-empty. */
+ _vec.push[postcond](postconds, block_precond);
+ auto block_postcond = union_postconds(postconds);
+ set_pre_and_post(b.node.a, rec(precondition=block_precond,
+ postcondition=block_postcond));
}
-fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> () {
+fn find_pre_post_fn(&fn_info_map fm, &fn_info fi, &_fn f) -> () {
find_pre_post_block(fm, fi, f.body);
}
-fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
+fn check_item_fn(&fn_info_map fm, &span sp, ident i, &ast._fn f,
vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
check (fm.contains_key(id));
@@ -970,10 +1113,33 @@ fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
}
-/* FIXME */
-fn find_pre_post_state_item(_fn_info_map fm, @item i) -> bool {
- log("Implement find_pre_post_item!");
- fail;
+fn find_pre_post_state_item(fn_info_map fm, fn_info enclosing, @item i)
+ -> bool {
+ alt (i.node) {
+ case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
+ ret find_pre_post_state_expr(fm, enclosing,
+ empty_prestate(num_locals(enclosing)), e);
+ }
+ case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
+ check (fm.contains_key(di));
+ ret find_pre_post_state_fn(fm, fm.get(di), f);
+ }
+ case (ast.item_mod(?id, ?m, ?di)) {
+ ret find_pre_post_state_mod(m);
+ }
+ case (ast.item_native_mod(?id, ?nm, ?di)) {
+ ret find_pre_post_state_native_mod(nm);
+ }
+ case (ast.item_ty(_,_,_,_,_)) {
+ ret false;
+ }
+ case (ast.item_tag(_,_,_,_,_)) {
+ ret false;
+ }
+ case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
+ ret find_pre_post_state_obj(fm, o);
+ }
+ }
}
fn set_prestate_ann(ann a, prestate pre) -> bool {
@@ -1034,6 +1200,11 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
case (ann_type(_,_,?ts_a)) {
check (! is_none[@ts_ann](ts_a));
auto t = *get[@ts_ann](ts_a);
+ /* log("set_pre_and_post, old =");
+ log_pp(t.conditions);
+ log("new =");
+ log_pp(pp);
+ */
set_precondition(t, pp.precondition);
set_postcondition(t, pp.postcondition);
}
@@ -1044,7 +1215,7 @@ fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
}
}
-fn seq_states(&_fn_info_map fm, &fn_info enclosing,
+fn seq_states(&fn_info_map fm, &fn_info enclosing,
prestate pres, vec[@expr] exprs) -> tup(bool, poststate) {
auto changed = false;
auto post = pres;
@@ -1057,7 +1228,7 @@ fn seq_states(&_fn_info_map fm, &fn_info enclosing,
ret tup(changed, post);
}
-fn find_pre_post_state_exprs(&_fn_info_map fm,
+fn find_pre_post_state_exprs(&fn_info_map fm,
&fn_info enclosing,
&prestate pres,
&ann a, &vec[@expr] es) -> bool {
@@ -1075,7 +1246,7 @@ fn pure_exp(&ann a, &prestate p) -> bool {
ret changed;
}
-fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_expr(&fn_info_map fm, &fn_info enclosing,
&prestate pres, &@expr e) -> bool {
auto changed = false;
auto num_local_vars = num_locals(enclosing);
@@ -1224,6 +1395,39 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
changed = extend_poststate_ann(a, expr_poststate(*sub));
ret changed;
}
+ case (expr_alt(?e, ?alts, ?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
+ auto e_post = expr_poststate(*e);
+ auto a_post = ann_to_poststate(a);
+ for (arm an_alt in alts) {
+ changed = find_pre_post_state_block(fm, enclosing, e_post,
+ an_alt.block) || changed;
+ changed = intersect(a_post, block_poststate(an_alt.block))
+ || changed;
+ }
+ ret changed;
+ }
+ case (expr_field(?e,_,?a)) {
+ changed = find_pre_post_state_expr(fm, enclosing, pres, e);
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(*e)) || changed;
+ ret changed;
+ }
+ case (expr_unary(_,?operand,?a)) {
+ changed = find_pre_post_state_expr(fm, enclosing, pres, operand)
+ || changed;
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = extend_poststate_ann(a, expr_poststate(*operand))
+ || changed;
+ ret changed;
+ }
+ case (expr_fail(?a)) {
+ changed = extend_prestate_ann(a, pres) || changed;
+ changed = set_poststate_ann(a, true_postcond(num_local_vars))
+ || changed;
+ ret changed;
+ }
case (_) {
log("find_pre_post_state_expr: implement this case!");
fail;
@@ -1232,7 +1436,7 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
}
-fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_stmt(&fn_info_map fm, &fn_info enclosing,
&prestate pres, @stmt s) -> bool {
auto changed = false;
auto stmt_ann_ = stmt_to_ann(*s);
@@ -1285,7 +1489,7 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
}
}
case (ast.decl_item(?an_item)) {
- be find_pre_post_state_item(fm, an_item);
+ be find_pre_post_state_item(fm, enclosing, an_item);
}
}
}
@@ -1314,7 +1518,7 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
/* Updates the pre- and post-states of statements in the block,
returns a boolean flag saying whether any pre- or poststates changed */
-fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing,
+fn find_pre_post_state_block(&fn_info_map fm, &fn_info enclosing,
&prestate pres0, block b)
-> bool {
@@ -1332,24 +1536,31 @@ fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing,
pres = stmt_poststate(*s, num_local_vars);
}
+ auto post = pres;
+
alt (b.node.expr) {
case (none[@expr]) {}
case (some[@expr](?e)) {
changed = find_pre_post_state_expr(fm, enclosing, pres, e) || changed;
+ post = expr_poststate(*e);
}
}
+ set_prestate_ann(b.node.a, pres0);
+ set_poststate_ann(b.node.a, post);
ret changed;
}
-fn find_pre_post_state_fn(&_fn_info_map f_info, &fn_info fi, &ast._fn f)
+fn find_pre_post_state_fn(&fn_info_map f_info, &fn_info fi, &ast._fn f)
-> bool {
+ /* FIXME: where do we set args as being initialized?
+ What about for methods? */
auto num_local_vars = num_locals(fi);
ret find_pre_post_state_block(f_info, fi,
empty_prestate(num_local_vars), f.body);
}
-fn fixed_point_states(_fn_info_map fm, fn_info f_info,
- fn (&_fn_info_map, &fn_info, &ast._fn) -> bool f,
+fn fixed_point_states(fn_info_map fm, fn_info f_info,
+ fn (&fn_info_map, &fn_info, &ast._fn) -> bool f,
&ast._fn start) -> () {
auto changed = f(fm, f_info, start);
@@ -1368,7 +1579,7 @@ fn check_states_expr(fn_info enclosing, &expr e) -> () {
let prestate pres = expr_prestate(e);
if (!implies(pres, prec)) {
- log("check_states_stmt: unsatisfied precondition for ");
+ log("check_states_expr: unsatisfied precondition for ");
log_expr(e);
log("Precondition: ");
log_bitv(enclosing, prec);
@@ -1424,14 +1635,8 @@ fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
}
-fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
- &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
- ann a) -> @item {
-
- /* Look up the var-to-bit-num map for this function */
- check(f_info_map.contains_key(id));
- auto f_info = f_info_map.get(id);
-
+fn check_fn_states(&fn_info_map f_info_map, &fn_info f_info, &ast._fn f)
+ -> () {
/* Compute the pre- and post-states for this function */
auto g = find_pre_post_state_fn;
fixed_point_states(f_info_map, f_info, g, f);
@@ -1439,11 +1644,39 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
/* Now compare each expr's pre-state to its precondition
and post-state to its postcondition */
check_states_against_conditions(f_info, f);
+}
+
+fn check_item_fn_state(&fn_info_map f_info_map, &span sp, ident i,
+ &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
+ ann a) -> @item {
+
+ /* Look up the var-to-bit-num map for this function */
+ check(f_info_map.contains_key(id));
+ auto f_info = f_info_map.get(id);
+
+ check_fn_states(f_info_map, f_info, f);
/* Rebuild the same function */
ret @respan(sp, ast.item_fn(i, f, ty_params, id, a));
}
+fn check_method_states(&fn_info_map f_info_map, @method m) -> () {
+ check (f_info_map.contains_key(m.node.id));
+ auto f_info = f_info_map.get(m.node.id);
+ check_fn_states(f_info_map, f_info, m.node.meth);
+}
+
+fn check_obj_state(&fn_info_map f_info_map, vec[obj_field] fields,
+ vec[@method] methods, option.t[@method] dtor) -> ast._obj {
+ fn one(fn_info_map fm, &@method m) -> () {
+ ret check_method_states(fm, m);
+ }
+ auto f = bind one(f_info_map,_);
+ _vec.map[@method, ()](f, methods);
+ option.map[@method, ()](f, dtor);
+ ret rec(fields=fields, methods=methods, dtor=dtor);
+}
+
fn init_ann(&fn_info fi, ann a) -> ann {
alt (a) {
case (ann_none) {
@@ -1456,42 +1689,467 @@ fn init_ann(&fn_info fi, ann a) -> ann {
}
}
-fn item_fn_anns(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
+fn init_blank_ann(&() ignore, ann a) -> ann {
+ alt (a) {
+ case (ann_none) {
+ log("init_ann: shouldn't see ann_none");
+ fail;
+ }
+ case (ann_type(?t,?ps,_)) {
+ ret ann_type(t, ps, some[@ts_ann](@empty_ann(0u)));
+ }
+ }
+}
+
+fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
+ log("init_block:");
+ log_block(respan(sp, b));
+ alt(b.a) {
+ case (ann_none) {
+ log("init_ann: shouldn't see ann_none");
+ fail;
+ }
+ case (ann_type(?t,?ps,_)) {
+ auto fld0 = fold.new_identity_fold[fn_info]();
+
+ fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+ ret fold.fold_block[fn_info](fi, fld0, respan(sp, b));
+ }
+ }
+
+}
+
+fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast._fn f,
vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
check(fm.contains_key(id));
auto f_info = fm.get(id);
+ log(i + " has " + uistr(num_locals(f_info)) + " local vars");
+
auto fld0 = fold.new_identity_fold[fn_info]();
- fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ // fold_block = bind init_block(_,_,_)
+ with *fld0);
ret fold.fold_item[fn_info]
(f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a)));
}
-fn check_crate(@ast.crate crate) -> @ast.crate {
+/* This is painstakingly written as an explicit recursion b/c the
+ standard ast.fold doesn't traverse in the correct order:
+ consider
+ fn foo() {
+ fn bar() {
+ auto x = 5;
+ log(x);
+ }
+ }
+ With fold, first bar() would be processed and its subexps would
+ correctly be annotated with length-1 bit vectors.
+ But then, the process would be repeated with (fn bar()...) as
+ a subexp of foo, which has 0 local variables -- so then
+ the body of bar() would be incorrectly annotated with length-0 bit
+ vectors. */
+fn annotate_exprs(&fn_info_map fm, &vec[@expr] es) -> vec[@expr] {
+ fn one(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind one(fm,_);
+ ret _vec.map[@expr, @expr](f, es);
+}
+fn annotate_elts(&fn_info_map fm, &vec[elt] es) -> vec[elt] {
+ fn one(fn_info_map fm, &elt e) -> elt {
+ ret rec(mut=e.mut,
+ expr=annotate_expr(fm, e.expr));
+ }
+ auto f = bind one(fm,_);
+ ret _vec.map[elt, elt](f, es);
+}
+fn annotate_fields(&fn_info_map fm, &vec[field] fs) -> vec[field] {
+ fn one(fn_info_map fm, &field f) -> field {
+ ret rec(mut=f.mut,
+ ident=f.ident,
+ expr=annotate_expr(fm, f.expr));
+ }
+ auto f = bind one(fm,_);
+ ret _vec.map[field, field](f, fs);
+}
+fn annotate_option_exp(&fn_info_map fm, &option.t[@expr] o)
+ -> option.t[@expr] {
+ fn one(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind one(fm,_);
+ ret option.map[@expr, @expr](f, o);
+}
+fn annotate_option_exprs(&fn_info_map fm, &vec[option.t[@expr]] es)
+ -> vec[option.t[@expr]] {
+ fn one(fn_info_map fm, &option.t[@expr] o) -> option.t[@expr] {
+ ret annotate_option_exp(fm, o);
+ }
+ auto f = bind one(fm,_);
+ ret _vec.map[option.t[@expr], option.t[@expr]](f, es);
+}
+fn annotate_decl(&fn_info_map fm, &@decl d) -> @decl {
+ auto d1 = d.node;
+ alt (d.node) {
+ case (decl_local(?l)) {
+ alt(l.init) {
+ case (some[initializer](?init)) {
+ let option.t[initializer] an_i =
+ some[initializer]
+ (rec(expr=annotate_expr(fm, init.expr)
+ with init));
+ let @local new_l = @rec(init=an_i with *l);
+ d1 = decl_local(new_l);
+ }
+ case (_) { /* do nothing */ }
+ }
+ }
+ case (decl_item(?item)) {
+ d1 = decl_item(annotate_item(fm, item));
+ }
+ }
+ ret @respan(d.span, d1);
+}
+fn annotate_alts(&fn_info_map fm, &vec[arm] alts) -> vec[arm] {
+ fn one(fn_info_map fm, &arm a) -> arm {
+ ret rec(pat=a.pat,
+ block=annotate_block(fm, a.block),
+ index=a.index);
+ }
+ auto f = bind one(fm,_);
+ ret _vec.map[arm, arm](f, alts);
+}
+fn annotate_expr(&fn_info_map fm, &@expr e) -> @expr {
+ auto e1 = e.node;
+ alt (e.node) {
+ case (expr_vec(?es, ?m, ?a)) {
+ e1 = expr_vec(annotate_exprs(fm, es), m, a);
+ }
+ case (expr_tup(?es, ?a)) {
+ e1 = expr_tup(annotate_elts(fm, es), a);
+ }
+ case (expr_rec(?fs, ?maybe_e, ?a)) {
+ e1 = expr_rec(annotate_fields(fm, fs),
+ annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_call(?e, ?es, ?a)) {
+ e1 = expr_call(annotate_expr(fm, e),
+ annotate_exprs(fm, es), a);
+ }
+ case (expr_self_method(_,_)) {
+ // no change
+ }
+ case (expr_bind(?e, ?maybe_es, ?a)) {
+ e1 = expr_bind(annotate_expr(fm, e),
+ annotate_option_exprs(fm, maybe_es),
+ a);
+ }
+ case (expr_spawn(?s, ?maybe_s, ?e, ?es, ?a)) {
+ e1 = expr_spawn(s, maybe_s, annotate_expr(fm, e),
+ annotate_exprs(fm, es), a);
+ }
+ case (expr_binary(?bop, ?w, ?x, ?a)) {
+ e1 = expr_binary(bop, annotate_expr(fm, w),
+ annotate_expr(fm, x), a);
+ }
+ case (expr_unary(?uop, ?w, ?a)) {
+ e1 = expr_unary(uop, annotate_expr(fm, w), a);
+ }
+ case (expr_lit(_,_)) {
+ /* no change */
+ }
+ case (expr_cast(?e,?t,?a)) {
+ e1 = expr_cast(annotate_expr(fm, e), t, a);
+ }
+ case (expr_if(?e, ?b, ?maybe_e, ?a)) {
+ e1 = expr_if(annotate_expr(fm, e),
+ annotate_block(fm, b),
+ annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_while(?e, ?b, ?a)) {
+ e1 = expr_while(annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_for(?d, ?e, ?b, ?a)) {
+ e1 = expr_for(annotate_decl(fm, d),
+ annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_for_each(?d, ?e, ?b, ?a)) {
+ e1 = expr_for_each(annotate_decl(fm, d),
+ annotate_expr(fm, e),
+ annotate_block(fm, b), a);
+ }
+ case (expr_do_while(?b, ?e, ?a)) {
+ e1 = expr_do_while(annotate_block(fm, b),
+ annotate_expr(fm, e), a);
+ }
+ case (expr_alt(?e, ?alts, ?a)) {
+ e1 = expr_alt(annotate_expr(fm, e),
+ annotate_alts(fm, alts), a);
+ }
+ case (expr_block(?b, ?a)) {
+ e1 = expr_block(annotate_block(fm, b), a);
+ }
+ case (expr_assign(?l, ?r, ?a)) {
+ e1 = expr_assign(annotate_expr(fm, l), annotate_expr(fm, r), a);
+ }
+ case (expr_assign_op(?bop, ?l, ?r, ?a)) {
+ e1 = expr_assign_op(bop,
+ annotate_expr(fm, l), annotate_expr(fm, r), a);
+ }
+ case (expr_send(?l, ?r, ?a)) {
+ e1 = expr_send(annotate_expr(fm, l),
+ annotate_expr(fm, r), a);
+ }
+ case (expr_recv(?l, ?r, ?a)) {
+ e1 = expr_recv(annotate_expr(fm, l),
+ annotate_expr(fm, r), a);
+ }
+ case (expr_field(?e, ?i, ?a)) {
+ e1 = expr_field(annotate_expr(fm, e),
+ i, a);
+ }
+ case (expr_index(?e, ?sub, ?a)) {
+ e1 = expr_index(annotate_expr(fm, e),
+ annotate_expr(fm, sub), a);
+ }
+ case (expr_path(_,_,_)) {
+ /* no change */
+ }
+ case (expr_ext(?p, ?es, ?e_opt, ?e, ?a)) {
+ e1 = expr_ext(p, annotate_exprs(fm, es),
+ annotate_option_exp(fm, e_opt),
+ annotate_expr(fm, e), a);
+ }
+ /* no change, next 3 cases */
+ case (expr_fail(_)) { }
+ case (expr_break(_)) { }
+ case (expr_cont(_)) { }
+ case (expr_ret(?maybe_e, ?a)) {
+ e1 = expr_ret(annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_put(?maybe_e, ?a)) {
+ e1 = expr_put(annotate_option_exp(fm, maybe_e), a);
+ }
+ case (expr_be(?e, ?a)) {
+ e1 = expr_be(annotate_expr(fm, e), a);
+ }
+ case (expr_log(?n, ?e, ?a)) {
+ e1 = expr_log(n, annotate_expr(fm, e), a);
+ }
+ case (expr_check_expr(?e, ?a)) {
+ e1 = expr_check_expr(annotate_expr(fm, e), a);
+ }
+ case (expr_port(_)) { /* no change */ }
+ case (expr_chan(?e, ?a)) {
+ e1 = expr_chan(annotate_expr(fm, e), a);
+ }
+ }
+ ret @respan(e.span, e1);
+}
+
+fn annotate_stmt(&fn_info_map fm, &@stmt s) -> @stmt {
+ alt (s.node) {
+ case (stmt_decl(?d, ?a)) {
+ ret @respan(s.span, stmt_decl(annotate_decl(fm, d), a));
+ }
+ case (stmt_expr(?e, ?a)) {
+ ret @respan(s.span, stmt_expr(annotate_expr(fm, e), a));
+ }
+ }
+}
+fn annotate_block(&fn_info_map fm, &block b) -> block {
+ let vec[@stmt] new_stmts = vec();
+ auto new_index = new_str_hash[block_index_entry]();
+
+ for (@stmt s in b.node.stmts) {
+ auto new_s = annotate_stmt(fm, s);
+ _vec.push[@stmt](new_stmts, new_s);
+ ast.index_stmt(new_index, new_s);
+ }
+ fn ann_e(fn_info_map fm, &@expr e) -> @expr {
+ ret annotate_expr(fm, e);
+ }
+ auto f = bind ann_e(fm,_);
+
+ auto new_e = option.map[@expr, @expr](f, b.node.expr);
+
+ ret respan(b.span,
+ rec(stmts=new_stmts, expr=new_e, index=new_index with b.node));
+}
+fn annotate_fn(&fn_info_map fm, &ast._fn f) -> ast._fn {
+ // subexps have *already* been annotated based on
+ // f's number-of-locals
+ ret rec(body=annotate_block(fm, f.body) with f);
+}
+fn annotate_mod(&fn_info_map fm, &ast._mod m) -> ast._mod {
+ let vec[@item] new_items = vec();
+ auto new_index = new_str_hash[mod_index_entry]();
+
+ for (@item i in m.items) {
+ auto new_i = annotate_item(fm, i);
+ _vec.push[@item](new_items, new_i);
+ ast.index_item(new_index, new_i);
+ }
+ ret rec(items=new_items, index=new_index with m);
+}
+fn annotate_native_mod(&fn_info_map fm, &ast.native_mod m)
+ -> ast.native_mod {
+ log("implement annotate_native_mod!");
+ fail;
+}
+fn annotate_method(&fn_info_map fm, &@method m) -> @method {
+ auto f_info = get_fn_info(fm, m.node.id);
+ auto fld0 = fold.new_identity_fold[fn_info]();
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ with *fld0);
+ auto outer = fold.fold_method[fn_info](f_info, fld0, m);
+ auto new_fn = annotate_fn(fm, outer.node.meth);
+ ret @respan(m.span,
+ rec(meth=new_fn with m.node));
+}
+
+fn annotate_obj(&fn_info_map fm, &ast._obj o) -> ast._obj {
+ fn one(fn_info_map fm, &@method m) -> @method {
+ ret annotate_method(fm, m);
+ }
+ auto f = bind one(fm,_);
+ auto new_methods = _vec.map[@method, @method](f, o.methods);
+ auto new_dtor = option.map[@method, @method](f, o.dtor);
+ ret rec(methods=new_methods, dtor=new_dtor with o);
+}
+
+
+// Only annotates the components of the item recursively.
+fn annotate_item_inner(&fn_info_map fm, &@ast.item item) -> @ast.item {
+ alt (item.node) {
+ /* FIXME can't skip this case -- exprs contain blocks contain stmts,
+ which contain decls */
+ case (ast.item_const(_,_,_,_,_)) {
+ // this has already been annotated by annotate_item
+ ret item;
+ }
+ case (ast.item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
+ ret @respan(item.span,
+ ast.item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
+ }
+ case (ast.item_mod(?ident, ?mm, ?id)) {
+ ret @respan(item.span,
+ ast.item_mod(ident, annotate_mod(fm, mm), id));
+ }
+ case (ast.item_native_mod(?ident, ?mm, ?id)) {
+ ret @respan(item.span,
+ ast.item_native_mod(ident,
+ annotate_native_mod(fm, mm), id));
+ }
+ case (ast.item_ty(_,_,_,_,_)) {
+ ret item;
+ }
+ case (ast.item_tag(_,_,_,_,_)) {
+ ret item;
+ }
+ case (ast.item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
+ ret @respan(item.span,
+ ast.item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
+ }
+ }
+}
+
+fn annotate_item(&fn_info_map fm, &@ast.item item) -> @ast.item {
+ // Using a fold, recursively set all anns in this item
+ // to be blank.
+ // *Then*, call annotate_item recursively to do the right
+ // thing for any nested items inside this one.
+
+ alt (item.node) {
+ case (ast.item_const(_,_,_,_,_)) {
+ auto fld0 = fold.new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ ret fold.fold_item[()]((), fld0, item);
+ }
+ case (ast.item_fn(?i,?ff,?tps,?id,?ann)) {
+ auto f_info = get_fn_info(fm, id);
+ auto fld0 = fold.new_identity_fold[fn_info]();
+ fld0 = @rec(fold_ann = bind init_ann(_,_)
+ with *fld0);
+ auto outer = fold.fold_item[fn_info](f_info, fld0, item);
+ // now recurse into any nested items
+ ret annotate_item_inner(fm, outer);
+ }
+ case (ast.item_mod(?i, ?mm, ?id)) {
+ auto fld0 = fold.new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ auto outer = fold.fold_item[()]((), fld0, item);
+ ret annotate_item_inner(fm, outer);
+ }
+ case (ast.item_ty(_,_,_,_,_)) {
+ ret item;
+ }
+ case (ast.item_tag(_,_,_,_,_)) {
+ ret item;
+ }
+ case (ast.item_obj(?i,?ob,?tps,?odid,?ann)) {
+ auto fld0 = fold.new_identity_fold[()]();
+ fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
+ with *fld0);
+ auto outer = fold.fold_item[()]((), fld0, item);
+ ret annotate_item_inner(fm, outer);
+ }
+ }
+}
+
+fn annotate_module(&fn_info_map fm, &ast._mod module) -> ast._mod {
+ let vec[@item] new_items = vec();
+ auto new_index = new_str_hash[ast.mod_index_entry]();
+
+ for (@item i in module.items) {
+ auto new_item = annotate_item(fm, i);
+ _vec.push[@item](new_items, new_item);
+ ast.index_item(new_index, new_item);
+ }
+
+ ret rec(items = new_items, index = new_index with module);
+}
+
+fn annotate_crate(&fn_info_map fm, &@ast.crate crate) -> @ast.crate {
+ ret @respan(crate.span,
+ rec(module = annotate_module(fm, crate.node.module)
+ with crate.node));
+}
+
+fn check_crate(@ast.crate crate) -> @ast.crate {
/* Build the global map from function id to var-to-bit-num-map */
- auto fn_info_map = mk_f_to_fn_info(crate);
+ auto fm = mk_f_to_fn_info(crate);
/* Add a blank ts_ann to every statement (and expression) */
- auto fld0 = fold.new_identity_fold[_fn_info_map]();
- fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_) with *fld0);
- auto with_anns = fold.fold_crate[_fn_info_map](fn_info_map, fld0, crate);
+ /*
+ auto fld0 = fold.new_identity_fold[fn_info_map]();
+ fld0 = @rec(fold_item_fn = bind item_fn_anns(_,_,_,_,_,_,_)
+ with *fld0);
+ */
+ auto with_anns = annotate_crate(fm, crate);
/* Compute the pre and postcondition for every subexpression */
- auto fld = fold.new_identity_fold[_fn_info_map]();
+ auto fld = fold.new_identity_fold[fn_info_map]();
fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
- auto with_pre_postconditions = fold.fold_crate[_fn_info_map]
- (fn_info_map, fld, with_anns);
+ auto with_pre_postconditions = fold.fold_crate[fn_info_map]
+ (fm, fld, with_anns);
- auto fld1 = fold.new_identity_fold[_fn_info_map]();
+ auto fld1 = fold.new_identity_fold[fn_info_map]();
- fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_)
+ fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_),
+ fold_obj = bind check_obj_state(_,_,_,_)
with *fld1);
- ret fold.fold_crate[_fn_info_map](fn_info_map, fld1,
+ ret fold.fold_crate[fn_info_map](fm, fld1,
with_pre_postconditions);
}
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index cf606d9e..e49ed34e 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -475,6 +475,13 @@ fn print_expr(ps s, &@ast.expr expr) {
commasep[option.t[@ast.expr]](s, args, f);
pclose(s);
}
+ case (ast.expr_spawn(_,_,?e,?es,_)) {
+ wrd1(s, "spawn");
+ print_expr(s, e);
+ popen(s);
+ commasep_exprs(s, es);
+ pclose(s);
+ }
case (ast.expr_binary(?op,?lhs,?rhs,_)) {
auto prec = operator_prec(op);
print_maybe_parens(s, lhs, prec);
@@ -1018,3 +1025,13 @@ fn print_comment(ps s, lexer.cmnt_ cmnt) {
}
}
}
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/comp/util/common.rs b/src/comp/util/common.rs
index 006bccb0..af000cb6 100644
--- a/src/comp/util/common.rs
+++ b/src/comp/util/common.rs
@@ -137,6 +137,35 @@ fn log_block(&ast.block b) -> () {
log(s.get_str());
}
+fn log_ann(&ast.ann a) -> () {
+ alt (a) {
+ case (ast.ann_none) {
+ log("ann_none");
+ }
+ case (ast.ann_type(_,_,_)) {
+ log("ann_type");
+ }
+ }
+}
+
+fn log_stmt(ast.stmt st) -> () {
+ let str_writer s = string_writer();
+ auto out_ = mkstate(s.get_writer(), 80u);
+ auto out = @rec(s=out_,
+ comments=none[vec[front.lexer.cmnt]],
+ mutable cur_cmnt=0u);
+ alt (st.node) {
+ case (ast.stmt_decl(?decl,_)) {
+ print_decl(out, decl);
+ }
+ case (ast.stmt_expr(?ex,_)) {
+ print_expr(out, ex);
+ }
+ case (_) { /* do nothing */ }
+ }
+ log(s.get_str());
+}
+
//
// Local Variables:
// mode: rust
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index b1f12ffb..9ad6e01e 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -147,6 +147,11 @@ fn ann_prestate(&ts_ann a) -> prestate {
ret a.states.prestate;
}
+fn pp_clone(&pre_and_post p) -> pre_and_post {
+ ret rec(precondition=bitv.clone(p.precondition),
+ postcondition=bitv.clone(p.postcondition));
+}
+
// returns true if a implies b
// that is, returns true except if for some bits c and d,
// c = 1 and d = 0
@@ -155,3 +160,14 @@ fn implies(bitv.t a, bitv.t b) -> bool {
bitv.difference(tmp, a);
ret bitv.is_false(tmp);
}
+
+//
+// Local Variables:
+// mode: rust
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// compile-command: "make -k -C $RBUILD 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+// End:
+//
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index 6fc1d700..cc8fabca 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -266,7 +266,7 @@ fn unzip[T, U](&vec[tup(T, U)] v) -> tup(vec[T], vec[U]) {
fn or(&vec[bool] v) -> bool {
auto f = orb;
- be _vec.foldl[bool, bool](f, false, v);
+ ret _vec.foldl[bool, bool](f, false, v);
}
fn clone[T](&vec[T] v) -> vec[T] {
diff --git a/src/lib/option.rs b/src/lib/option.rs
index 66a41bca..e214c774 100644
--- a/src/lib/option.rs
+++ b/src/lib/option.rs
@@ -39,12 +39,16 @@ fn is_none[T](&t[T] opt) -> bool {
}
fn from_maybe[T](&T def, &t[T] opt) -> T {
- alt(opt) {
- case (none[T]) { ret def; }
- case (some[T](?t)) { ret t; }
- }
+ auto f = bind util.id[T](_);
+ ret maybe[T, T](def, f, opt);
}
+fn maybe[T, U](&U def, fn(&T) -> U f, &t[T] opt) -> U {
+ alt (opt) {
+ case (none[T]) { ret def; }
+ case (some[T](?t)) { ret f(t); }
+ }
+}
// Local Variables:
// mode: rust;
// fill-column: 78;
diff --git a/src/test/compile-fail/use-uninit-dtor.rs b/src/test/compile-fail/use-uninit-dtor.rs
new file mode 100644
index 00000000..be2f1727
--- /dev/null
+++ b/src/test/compile-fail/use-uninit-dtor.rs
@@ -0,0 +1,12 @@
+// xfail-stage0
+// error-pattern:Unsatisfied precondition
+
+fn main() {
+ state obj foo(int x) {
+ drop {
+ let int baz;
+ log(baz);
+ }
+ }
+ fail;
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 08:58:45 +0000