Started adding support for return checking and non-returning function annotations
* Reorganized typestate into several modules.
* Made typestate check that any function with a non-nil return type
returns a value. For now, the check is a warning and not an error
(see next item).
* Added a "bot" type (prettyprinted as _|_), for constructs like be, ret, break, cont, and
fail that don't locally return a value that can be inspected. "bot"
is distinct from "nil". There is no concrete syntax for _|_, while
the concrete syntax for the nil type is ().
* Added support to the parser for a ! annotation on functions whose
result type is _|_. Such a function is required to have either a
fail or a call to another ! function that is reached in all control
flow paths. The point of this annotation is to mark functions like
unimpl() and span_err(), so that an alt with a call to err() in one
case isn't a false positive for the return-value checker. I haven't
actually annotated anything with it yet.
* Random bugfixes:
* * Fixed bug in trans::trans_binary that was throwing away the
cleanups for nested subexpressions of an and or or
(tests: box-inside-if and box-inside-if2).
** In typeck, unify the expected type arguments of a tag with the
actual specified arguments.
This commit is contained in:
Tim Chevalier
parent
c75125fcce
commit
971b5d5151
22 changed files with 3276 additions and 51 deletions
|
|
@ -9,7 +9,7 @@ import middle::trans;
|
|||
import middle::resolve;
|
||||
import middle::ty;
|
||||
import middle::typeck;
|
||||
import middle::typestate_check;
|
||||
import middle::tstate::ck;
|
||||
import back::link;
|
||||
import lib::llvm;
|
||||
import util::common;
|
||||
|
|
@ -105,7 +105,8 @@ fn compile_input(session::session sess,
|
|||
|
||||
if (sess.get_opts().run_typestate) {
|
||||
crate = time(time_passes, "typestate checking",
|
||||
bind typestate_check::check_crate(crate, def_map));
|
||||
bind middle::tstate::ck::check_crate(node_type_table,
|
||||
ty_cx, crate));
|
||||
}
|
||||
|
||||
auto llmod = time[llvm::ModuleRef](time_passes, "translation",
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
import std::map::hashmap;
|
||||
import std::option;
|
||||
import std::_str;
|
||||
|
|
@ -7,7 +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;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
|
||||
type ident = str;
|
||||
|
||||
|
|
@ -323,6 +322,12 @@ type ty_method = rec(proto proto, ident ident,
|
|||
type ty = spanned[ty_];
|
||||
tag ty_ {
|
||||
ty_nil;
|
||||
ty_bot; /* return type of ! functions and type of
|
||||
ret/fail/break/cont. there is no syntax
|
||||
for this type. */
|
||||
/* bot represents the value of functions that don't return a value
|
||||
locally to their context. in contrast, things like log that do
|
||||
return, but don't return a meaningful value, have result type nil. */
|
||||
ty_bool;
|
||||
ty_int;
|
||||
ty_uint;
|
||||
|
|
@ -354,12 +359,19 @@ type constr = spanned[constr_];
|
|||
type arg = rec(mode mode, @ty ty, ident ident, def_id id);
|
||||
type fn_decl = rec(vec[arg] inputs,
|
||||
@ty output,
|
||||
purity purity);
|
||||
purity purity,
|
||||
controlflow cf);
|
||||
tag purity {
|
||||
pure_fn; // declared with "pred"
|
||||
impure_fn; // declared with "fn"
|
||||
}
|
||||
|
||||
tag controlflow {
|
||||
noreturn; // functions with return type _|_ that always
|
||||
// raise an error or exit (i.e. never return to the caller)
|
||||
return; // everything else
|
||||
}
|
||||
|
||||
type _fn = rec(fn_decl decl,
|
||||
proto proto,
|
||||
block body);
|
||||
|
|
|
|||
|
|
@ -23,6 +23,11 @@ tag file_type {
|
|||
SOURCE_FILE;
|
||||
}
|
||||
|
||||
tag ty_or_bang {
|
||||
a_ty(@ast::ty);
|
||||
a_bang;
|
||||
}
|
||||
|
||||
state type parser =
|
||||
state obj {
|
||||
fn peek() -> token::token;
|
||||
|
|
@ -448,6 +453,13 @@ fn parse_ty_constrs(@ast::ty t, parser p) -> @ast::ty {
|
|||
ret t;
|
||||
}
|
||||
|
||||
fn parse_ty_or_bang(parser p) -> ty_or_bang {
|
||||
alt (p.peek()) {
|
||||
case (token::NOT) { p.bump(); ret a_bang; }
|
||||
case (_) { ret a_ty(parse_ty(p)); }
|
||||
}
|
||||
}
|
||||
|
||||
fn parse_ty(parser p) -> @ast::ty {
|
||||
auto lo = p.get_lo_pos();
|
||||
auto hi = lo;
|
||||
|
|
@ -1713,7 +1725,7 @@ fn parse_fn_decl(parser p, ast::purity purity) -> ast::fn_decl {
|
|||
some(token::COMMA),
|
||||
pf, p);
|
||||
|
||||
let @ast::ty output;
|
||||
let ty_or_bang res;
|
||||
|
||||
// FIXME: dropping constrs on the floor at the moment.
|
||||
// pick them up when they're used by typestate pass.
|
||||
|
|
@ -1721,12 +1733,23 @@ fn parse_fn_decl(parser p, ast::purity purity) -> ast::fn_decl {
|
|||
|
||||
if (p.peek() == token::RARROW) {
|
||||
p.bump();
|
||||
output = parse_ty(p);
|
||||
res = parse_ty_or_bang(p);
|
||||
} else {
|
||||
output = @spanned(inputs.span.lo, inputs.span.hi, ast::ty_nil);
|
||||
res = a_ty(@spanned(inputs.span.lo, inputs.span.hi, ast::ty_nil));
|
||||
}
|
||||
|
||||
alt (res) {
|
||||
case (a_ty(?t)) {
|
||||
ret rec(inputs=inputs.node, output=t,
|
||||
purity=purity, cf=ast::return);
|
||||
}
|
||||
case (a_bang) {
|
||||
ret rec(inputs=inputs.node,
|
||||
output=@spanned(p.get_lo_pos(),
|
||||
p.get_hi_pos(), ast::ty_bot),
|
||||
purity=purity, cf=ast::noreturn);
|
||||
}
|
||||
}
|
||||
// FIXME
|
||||
ret rec(inputs=inputs.node, output=output, purity=purity);
|
||||
}
|
||||
|
||||
fn parse_fn(parser p, ast::proto proto, ast::purity purity) -> ast::_fn {
|
||||
|
|
@ -1778,11 +1801,12 @@ fn parse_dtor(parser p) -> @ast::method {
|
|||
let vec[ast::arg] inputs = vec();
|
||||
let @ast::ty output = @spanned(lo, lo, ast::ty_nil);
|
||||
let ast::fn_decl d = rec(inputs=inputs,
|
||||
output=output,
|
||||
purity=ast::impure_fn);
|
||||
output=output,
|
||||
purity=ast::impure_fn,
|
||||
cf=ast::return);
|
||||
let ast::_fn f = rec(decl = d,
|
||||
proto = ast::proto_fn,
|
||||
body = b);
|
||||
proto = ast::proto_fn,
|
||||
body = b);
|
||||
let ast::method_ m = rec(ident="drop",
|
||||
meth=f,
|
||||
id=p.next_def_id(),
|
||||
|
|
|
|||
|
|
@ -7,13 +7,14 @@ import util::common::new_str_hash;
|
|||
import util::common::spanned;
|
||||
import util::common::span;
|
||||
import util::common::ty_mach;
|
||||
import util::typestate_ann::ts_ann;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::fn_decl;
|
||||
import front::ast::ident;
|
||||
import front::ast::path;
|
||||
import front::ast::mutability;
|
||||
import front::ast::controlflow;
|
||||
import front::ast::ty;
|
||||
import front::ast::expr;
|
||||
import front::ast::stmt;
|
||||
|
|
@ -44,6 +45,7 @@ type ast_fold[ENV] =
|
|||
|
||||
// Type folds.
|
||||
(fn(&ENV e, &span sp) -> @ty) fold_ty_nil,
|
||||
(fn(&ENV e, &span sp) -> @ty) fold_ty_bot,
|
||||
(fn(&ENV e, &span sp) -> @ty) fold_ty_bool,
|
||||
(fn(&ENV e, &span sp) -> @ty) fold_ty_int,
|
||||
(fn(&ENV e, &span sp) -> @ty) fold_ty_uint,
|
||||
|
|
@ -314,7 +316,7 @@ type ast_fold[ENV] =
|
|||
(fn(&ENV e,
|
||||
&vec[arg] inputs,
|
||||
&@ty output,
|
||||
&purity p) -> ast::fn_decl) fold_fn_decl,
|
||||
&purity p, &controlflow c) -> ast::fn_decl) fold_fn_decl,
|
||||
|
||||
(fn(&ENV e, &ast::_mod m) -> ast::_mod) fold_mod,
|
||||
|
||||
|
|
@ -375,6 +377,7 @@ fn fold_ty[ENV](&ENV env, &ast_fold[ENV] fld, &@ty t) -> @ty {
|
|||
|
||||
alt (t.node) {
|
||||
case (ast::ty_nil) { ret fld.fold_ty_nil(env_, t.span); }
|
||||
case (ast::ty_bot) { ret fld.fold_ty_bot(env_, t.span); }
|
||||
case (ast::ty_bool) { ret fld.fold_ty_bool(env_, t.span); }
|
||||
case (ast::ty_int) { ret fld.fold_ty_int(env_, t.span); }
|
||||
case (ast::ty_uint) { ret fld.fold_ty_uint(env_, t.span); }
|
||||
|
|
@ -926,7 +929,7 @@ fn fold_fn_decl[ENV](&ENV env, &ast_fold[ENV] fld,
|
|||
inputs += vec(fold_arg(env, fld, a));
|
||||
}
|
||||
auto output = fold_ty[ENV](env, fld, decl.output);
|
||||
ret fld.fold_fn_decl(env, inputs, output, decl.purity);
|
||||
ret fld.fold_fn_decl(env, inputs, output, decl.purity, decl.cf);
|
||||
}
|
||||
|
||||
fn fold_fn[ENV](&ENV env, &ast_fold[ENV] fld, &ast::_fn f) -> ast::_fn {
|
||||
|
|
@ -1202,6 +1205,10 @@ fn identity_fold_ty_nil[ENV](&ENV env, &span sp) -> @ty {
|
|||
ret @respan(sp, ast::ty_nil);
|
||||
}
|
||||
|
||||
fn identity_fold_ty_bot[ENV](&ENV env, &span sp) -> @ty {
|
||||
ret @respan(sp, ast::ty_bot);
|
||||
}
|
||||
|
||||
fn identity_fold_ty_bool[ENV](&ENV env, &span sp) -> @ty {
|
||||
ret @respan(sp, ast::ty_bool);
|
||||
}
|
||||
|
|
@ -1622,8 +1629,8 @@ fn identity_fold_block[ENV](&ENV e, &span sp, &ast::block_ blk) -> block {
|
|||
fn identity_fold_fn_decl[ENV](&ENV e,
|
||||
&vec[arg] inputs,
|
||||
&@ty output,
|
||||
&purity p) -> ast::fn_decl {
|
||||
ret rec(inputs=inputs, output=output, purity=p);
|
||||
&purity p, &controlflow c) -> ast::fn_decl {
|
||||
ret rec(inputs=inputs, output=output, purity=p, cf=c);
|
||||
}
|
||||
|
||||
fn identity_fold_fn[ENV](&ENV e,
|
||||
|
|
@ -1722,6 +1729,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
|
|||
fold_path = bind identity_fold_path[ENV](_,_,_),
|
||||
|
||||
fold_ty_nil = bind identity_fold_ty_nil[ENV](_,_),
|
||||
fold_ty_bot = bind identity_fold_ty_bot[ENV](_,_),
|
||||
fold_ty_bool = bind identity_fold_ty_bool[ENV](_,_),
|
||||
fold_ty_int = bind identity_fold_ty_int[ENV](_,_),
|
||||
fold_ty_uint = bind identity_fold_ty_uint[ENV](_,_),
|
||||
|
|
@ -1821,7 +1829,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
|
|||
fold_ann = bind identity_fold_ann[ENV](_,_),
|
||||
|
||||
fold_fn = bind identity_fold_fn[ENV](_,_,_,_),
|
||||
fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_,_),
|
||||
fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_,_,_),
|
||||
fold_mod = bind identity_fold_mod[ENV](_,_),
|
||||
fold_native_mod = bind identity_fold_native_mod[ENV](_,_),
|
||||
fold_crate = bind identity_fold_crate[ENV](_,_,_,_),
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ import util::common::new_int_hash;
|
|||
import util::common::new_uint_hash;
|
||||
import util::common::new_str_hash;
|
||||
import util::common::span;
|
||||
import util::typestate_ann::ts_ann;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
import std::map::hashmap;
|
||||
import std::list::list;
|
||||
import std::list::nil;
|
||||
|
|
|
|||
|
|
@ -757,6 +757,7 @@ fn type_of_inner(&@crate_ctxt cx, &ty::t t) -> TypeRef {
|
|||
alt (ty::struct(cx.tcx, t)) {
|
||||
case (ty::ty_native) { llty = T_ptr(T_i8()); }
|
||||
case (ty::ty_nil) { llty = T_nil(); }
|
||||
case (ty::ty_bot) { llty = T_nil(); } /* ...I guess? */
|
||||
case (ty::ty_bool) { llty = T_bool(); }
|
||||
case (ty::ty_int) { llty = T_int(); }
|
||||
case (ty::ty_float) { llty = T_float(); }
|
||||
|
|
@ -3186,8 +3187,8 @@ fn copy_ty(&@block_ctxt cx,
|
|||
if (ty::type_is_scalar(cx.fcx.lcx.ccx.tcx, t) ||
|
||||
ty::type_is_native(cx.fcx.lcx.ccx.tcx, t)) {
|
||||
ret res(cx, cx.build.Store(src, dst));
|
||||
|
||||
} else if (ty::type_is_nil(cx.fcx.lcx.ccx.tcx, t)) {
|
||||
} else if (ty::type_is_nil(cx.fcx.lcx.ccx.tcx, t) ||
|
||||
ty::type_is_bot(cx.fcx.lcx.ccx.tcx, t)) {
|
||||
ret res(cx, C_nil());
|
||||
|
||||
} else if (ty::type_is_boxed(cx.fcx.lcx.ccx.tcx, t)) {
|
||||
|
|
@ -3552,6 +3553,8 @@ fn autoderef(&@block_ctxt cx, ValueRef v, &ty::t t) -> result {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
fail; // fools the return-checker
|
||||
}
|
||||
|
||||
fn autoderefed_ty(&@crate_ctxt ccx, &ty::t t) -> ty::t {
|
||||
|
|
@ -3567,6 +3570,8 @@ fn autoderefed_ty(&@crate_ctxt ccx, &ty::t t) -> ty::t {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
fail; // fools the return-checker
|
||||
}
|
||||
|
||||
fn trans_binary(&@block_ctxt cx, ast::binop op,
|
||||
|
|
@ -3591,12 +3596,17 @@ fn trans_binary(&@block_ctxt cx, ast::binop op,
|
|||
auto lhs_false_cx = new_scope_block_ctxt(cx, "lhs false");
|
||||
auto lhs_false_res = res(lhs_false_cx, C_bool(false));
|
||||
|
||||
// The following line ensures that any cleanups for rhs
|
||||
// are done within the block for rhs. This is necessary
|
||||
// because and/or are lazy. So the rhs may never execute,
|
||||
// and the cleanups can't be pushed into later code.
|
||||
auto rhs_bcx = trans_block_cleanups(rhs_res.bcx, rhs_cx);
|
||||
|
||||
lhs_res.bcx.build.CondBr(lhs_res.val,
|
||||
rhs_cx.llbb,
|
||||
lhs_false_cx.llbb);
|
||||
|
||||
ret join_results(cx, T_bool(),
|
||||
vec(lhs_false_res, rhs_res));
|
||||
vec(lhs_false_res, rec(bcx=rhs_bcx with rhs_res)));
|
||||
}
|
||||
|
||||
case (ast::or) {
|
||||
|
|
@ -3615,12 +3625,15 @@ fn trans_binary(&@block_ctxt cx, ast::binop op,
|
|||
auto lhs_true_cx = new_scope_block_ctxt(cx, "lhs true");
|
||||
auto lhs_true_res = res(lhs_true_cx, C_bool(true));
|
||||
|
||||
// see the and case for an explanation
|
||||
auto rhs_bcx = trans_block_cleanups(rhs_res.bcx, rhs_cx);
|
||||
|
||||
lhs_res.bcx.build.CondBr(lhs_res.val,
|
||||
lhs_true_cx.llbb,
|
||||
rhs_cx.llbb);
|
||||
|
||||
ret join_results(cx, T_bool(),
|
||||
vec(lhs_true_res, rhs_res));
|
||||
vec(lhs_true_res, rec(bcx=rhs_bcx with rhs_res)));
|
||||
}
|
||||
|
||||
case (_) {
|
||||
|
|
@ -4984,6 +4997,8 @@ fn trans_bind(&@block_ctxt cx, &@ast::expr f,
|
|||
ret res(bcx, pair_v);
|
||||
}
|
||||
}
|
||||
|
||||
fail; // sadly needed b/c the compiler doesn't know yet that unimpl fails
|
||||
}
|
||||
|
||||
fn trans_arg_expr(&@block_ctxt cx,
|
||||
|
|
|
|||
|
|
@ -111,13 +111,13 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
|
|||
|
||||
// Sets all the bits in a's precondition to equal the
|
||||
// corresponding bit in p's precondition.
|
||||
fn set_precondition(&ts_ann a, &precond p) -> () {
|
||||
fn set_precondition(@ts_ann a, &precond p) -> () {
|
||||
bitv::copy(a.conditions.precondition, p);
|
||||
}
|
||||
|
||||
// Sets all the bits in a's postcondition to equal the
|
||||
// corresponding bit in p's postcondition.
|
||||
fn set_postcondition(&ts_ann a, &postcond p) -> () {
|
||||
fn set_postcondition(@ts_ann a, &postcond p) -> () {
|
||||
bitv::copy(a.conditions.postcondition, p);
|
||||
}
|
||||
|
||||
|
|
@ -158,6 +158,10 @@ fn ann_prestate(&ts_ann a) -> prestate {
|
|||
ret a.states.prestate;
|
||||
}
|
||||
|
||||
fn ann_poststate(&ts_ann a) -> poststate {
|
||||
ret a.states.poststate;
|
||||
}
|
||||
|
||||
fn pp_clone(&pre_and_post p) -> pre_and_post {
|
||||
ret rec(precondition=clone(p.precondition),
|
||||
postcondition=clone(p.postcondition));
|
||||
492
src/comp/middle/tstate/annotate.rs
Normal file
492
src/comp/middle/tstate/annotate.rs
Normal file
|
|
@ -0,0 +1,492 @@
|
|||
import std::_vec;
|
||||
import std::option;
|
||||
import std::option::some;
|
||||
import std::option::none;
|
||||
|
||||
import front::ast;
|
||||
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ann;
|
||||
import front::ast::item;
|
||||
import front::ast::_fn;
|
||||
import front::ast::_mod;
|
||||
import front::ast::crate;
|
||||
import front::ast::_obj;
|
||||
import front::ast::ty_param;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::item_obj;
|
||||
import front::ast::item_ty;
|
||||
import front::ast::item_tag;
|
||||
import front::ast::item_const;
|
||||
import front::ast::item_mod;
|
||||
import front::ast::item_native_mod;
|
||||
import front::ast::expr;
|
||||
import front::ast::elt;
|
||||
import front::ast::field;
|
||||
import front::ast::decl;
|
||||
import front::ast::decl_local;
|
||||
import front::ast::decl_item;
|
||||
import front::ast::initializer;
|
||||
import front::ast::local;
|
||||
import front::ast::arm;
|
||||
import front::ast::expr_call;
|
||||
import front::ast::expr_vec;
|
||||
import front::ast::expr_tup;
|
||||
import front::ast::expr_path;
|
||||
import front::ast::expr_field;
|
||||
import front::ast::expr_index;
|
||||
import front::ast::expr_log;
|
||||
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;
|
||||
import front::ast::expr_assert;
|
||||
import front::ast::expr_cast;
|
||||
import front::ast::expr_for;
|
||||
import front::ast::expr_for_each;
|
||||
import front::ast::stmt;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::stmt_expr;
|
||||
import front::ast::block;
|
||||
import front::ast::block_;
|
||||
import front::ast::method;
|
||||
|
||||
import middle::fold;
|
||||
import middle::fold::respan;
|
||||
import middle::fold::new_identity_fold;
|
||||
import middle::fold::fold_crate;
|
||||
import middle::fold::fold_item;
|
||||
import middle::fold::fold_method;
|
||||
|
||||
import util::common::uistr;
|
||||
import util::common::span;
|
||||
import util::common::new_str_hash;
|
||||
|
||||
import middle::tstate::aux::fn_info;
|
||||
import middle::tstate::aux::fn_info_map;
|
||||
import middle::tstate::aux::num_locals;
|
||||
import middle::tstate::aux::init_ann;
|
||||
import middle::tstate::aux::init_blank_ann;
|
||||
import middle::tstate::aux::get_fn_info;
|
||||
|
||||
fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &_fn f,
|
||||
vec[ty_param] ty_params, def_id id, ann a) -> @item {
|
||||
|
||||
assert (fm.contains_key(id));
|
||||
auto f_info = fm.get(id);
|
||||
|
||||
log(i + " has " + uistr(num_locals(f_info)) + " local vars");
|
||||
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_)
|
||||
with *fld0);
|
||||
|
||||
ret fold_item[fn_info]
|
||||
(f_info, fld0, @respan(sp, item_fn(i, f, ty_params, id, a)));
|
||||
}
|
||||
|
||||
/* FIXME: rewrite this with walk instead of fold */
|
||||
|
||||
/* 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));
|
||||
}
|
||||
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, ?s_opt, ?e, ?a)) {
|
||||
e1 = expr_ext(p, annotate_exprs(fm, es),
|
||||
s_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_assert(?e, ?a)) {
|
||||
e1 = expr_assert(annotate_expr(fm, e), a);
|
||||
}
|
||||
case (expr_check(?e, ?a)) {
|
||||
e1 = expr_check(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();
|
||||
|
||||
for (@stmt s in b.node.stmts) {
|
||||
auto new_s = annotate_stmt(fm, s);
|
||||
_vec::push[@stmt](new_stmts, 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 with b.node));
|
||||
}
|
||||
fn annotate_fn(&fn_info_map fm, &_fn f) -> _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, &_mod m) -> _mod {
|
||||
let vec[@item] new_items = vec();
|
||||
|
||||
for (@item i in m.items) {
|
||||
auto new_i = annotate_item(fm, i);
|
||||
_vec::push[@item](new_items, new_i);
|
||||
}
|
||||
ret rec(items=new_items with m);
|
||||
}
|
||||
fn annotate_method(&fn_info_map fm, &@method m) -> @method {
|
||||
auto f_info = get_fn_info(fm, m.node.id);
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_)
|
||||
with *fld0);
|
||||
auto outer = 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, &_obj o) -> _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, &@item item) -> @item {
|
||||
alt (item.node) {
|
||||
/* FIXME can't skip this case -- exprs contain blocks contain stmts,
|
||||
which contain decls */
|
||||
case (item_const(_,_,_,_,_)) {
|
||||
// this has already been annotated by annotate_item
|
||||
ret item;
|
||||
}
|
||||
case (item_fn(?ident, ?ff, ?tps, ?id, ?ann)) {
|
||||
ret @respan(item.span,
|
||||
item_fn(ident, annotate_fn(fm, ff), tps, id, ann));
|
||||
}
|
||||
case (item_mod(?ident, ?mm, ?id)) {
|
||||
ret @respan(item.span,
|
||||
item_mod(ident, annotate_mod(fm, mm), id));
|
||||
}
|
||||
case (item_native_mod(?ident, ?mm, ?id)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_ty(_,_,_,_,_)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_tag(_,_,_,_,_)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_obj(?ident, ?ob, ?tps, ?odid, ?ann)) {
|
||||
ret @respan(item.span,
|
||||
item_obj(ident, annotate_obj(fm, ob), tps, odid, ann));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn annotate_item(&fn_info_map fm, &@item item) -> @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 (item_const(_,_,_,_,_)) {
|
||||
auto fld0 = new_identity_fold[()]();
|
||||
fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
|
||||
with *fld0);
|
||||
ret fold_item[()]((), fld0, item);
|
||||
}
|
||||
case (item_fn(?i,?ff,?tps,?id,?ann)) {
|
||||
auto f_info = get_fn_info(fm, id);
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_)
|
||||
with *fld0);
|
||||
auto outer = fold_item[fn_info](f_info, fld0, item);
|
||||
// now recurse into any nested items
|
||||
ret annotate_item_inner(fm, outer);
|
||||
}
|
||||
case (item_mod(?i, ?mm, ?id)) {
|
||||
auto fld0 = new_identity_fold[()]();
|
||||
fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
|
||||
with *fld0);
|
||||
auto outer = fold_item[()]((), fld0, item);
|
||||
ret annotate_item_inner(fm, outer);
|
||||
}
|
||||
case (item_native_mod(?i, ?nm, ?id)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_ty(_,_,_,_,_)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_tag(_,_,_,_,_)) {
|
||||
ret item;
|
||||
}
|
||||
case (item_obj(?i,?ob,?tps,?odid,?ann)) {
|
||||
auto fld0 = new_identity_fold[()]();
|
||||
fld0 = @rec(fold_ann = bind init_blank_ann(_,_)
|
||||
with *fld0);
|
||||
auto outer = fold_item[()]((), fld0, item);
|
||||
ret annotate_item_inner(fm, outer);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn annotate_module(&fn_info_map fm, &_mod module) -> _mod {
|
||||
let vec[@item] new_items = vec();
|
||||
|
||||
for (@item i in module.items) {
|
||||
auto new_item = annotate_item(fm, i);
|
||||
_vec::push[@item](new_items, new_item);
|
||||
}
|
||||
|
||||
ret rec(items = new_items with module);
|
||||
}
|
||||
|
||||
fn annotate_crate(&fn_info_map fm, &@crate crate) -> @crate {
|
||||
ret @respan(crate.span,
|
||||
rec(module = annotate_module(fm, crate.node.module)
|
||||
with crate.node));
|
||||
}
|
||||
482
src/comp/middle/tstate/aux.rs
Normal file
482
src/comp/middle/tstate/aux.rs
Normal file
|
|
@ -0,0 +1,482 @@
|
|||
import std::bitv;
|
||||
import std::_vec::len;
|
||||
import std::_vec::pop;
|
||||
import std::option;
|
||||
import std::option::none;
|
||||
import std::option::some;
|
||||
import std::option::maybe;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::ann_tag;
|
||||
import front::ast::def;
|
||||
import front::ast::def_fn;
|
||||
import front::ast::_fn;
|
||||
import front::ast::def_obj_field;
|
||||
import front::ast::def_id;
|
||||
import front::ast::expr_path;
|
||||
import front::ast::ident;
|
||||
import front::ast::controlflow;
|
||||
import front::ast::ann;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::ts_ann;
|
||||
import front::ast::stmt;
|
||||
import front::ast::expr;
|
||||
import front::ast::block;
|
||||
import front::ast::block_;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::stmt_expr;
|
||||
import front::ast::stmt_crate_directive;
|
||||
import front::ast::return;
|
||||
import front::ast::expr_field;
|
||||
|
||||
import middle::ty::expr_ann;
|
||||
import middle::fold;
|
||||
import middle::fold::respan;
|
||||
import middle::fold::new_identity_fold;
|
||||
import middle::fold::fold_block;
|
||||
|
||||
import util::common;
|
||||
import util::common::span;
|
||||
import util::common::log_block;
|
||||
import util::common::new_def_hash;
|
||||
import util::common::log_expr_err;
|
||||
import util::common::uistr;
|
||||
|
||||
import tstate::ann::pre_and_post;
|
||||
import tstate::ann::pre_and_post_state;
|
||||
import tstate::ann::empty_ann;
|
||||
import tstate::ann::prestate;
|
||||
import tstate::ann::poststate;
|
||||
import tstate::ann::precond;
|
||||
import tstate::ann::postcond;
|
||||
import tstate::ann::empty_states;
|
||||
import tstate::ann::pps_len;
|
||||
import tstate::ann::set_prestate;
|
||||
import tstate::ann::set_poststate;
|
||||
import tstate::ann::extend_prestate;
|
||||
import tstate::ann::extend_poststate;
|
||||
import tstate::ann::set_precondition;
|
||||
import tstate::ann::set_postcondition;
|
||||
|
||||
/* logging funs */
|
||||
|
||||
fn bitv_to_str(fn_info enclosing, bitv::t v) -> str {
|
||||
auto s = "";
|
||||
|
||||
for each (@tup(def_id, tup(uint, ident)) p in enclosing.vars.items()) {
|
||||
if (bitv::get(v, p._1._0)) {
|
||||
s += " " + p._1._1 + " ";
|
||||
}
|
||||
}
|
||||
ret s;
|
||||
}
|
||||
|
||||
fn log_bitv(fn_info enclosing, bitv::t v) {
|
||||
log(bitv_to_str(enclosing, v));
|
||||
}
|
||||
|
||||
fn log_bitv_err(fn_info enclosing, bitv::t v) {
|
||||
log_err(bitv_to_str(enclosing, v));
|
||||
}
|
||||
|
||||
fn tos (vec[uint] v) -> str {
|
||||
auto res = "";
|
||||
for (uint i in v) {
|
||||
if (i == 0u) {
|
||||
res += "0";
|
||||
}
|
||||
else {
|
||||
res += "1";
|
||||
}
|
||||
}
|
||||
ret res;
|
||||
}
|
||||
|
||||
fn log_cond(vec[uint] v) -> () {
|
||||
log(tos(v));
|
||||
}
|
||||
fn log_cond_err(vec[uint] v) -> () {
|
||||
log_err(tos(v));
|
||||
}
|
||||
|
||||
fn log_pp(&pre_and_post pp) -> () {
|
||||
auto p1 = bitv::to_vec(pp.precondition);
|
||||
auto p2 = bitv::to_vec(pp.postcondition);
|
||||
log("pre:");
|
||||
log_cond(p1);
|
||||
log("post:");
|
||||
log_cond(p2);
|
||||
}
|
||||
|
||||
fn log_pp_err(&pre_and_post pp) -> () {
|
||||
auto p1 = bitv::to_vec(pp.precondition);
|
||||
auto p2 = bitv::to_vec(pp.postcondition);
|
||||
log_err("pre:");
|
||||
log_cond_err(p1);
|
||||
log_err("post:");
|
||||
log_cond_err(p2);
|
||||
}
|
||||
|
||||
fn log_states(&pre_and_post_state pp) -> () {
|
||||
auto p1 = bitv::to_vec(pp.prestate);
|
||||
auto p2 = bitv::to_vec(pp.poststate);
|
||||
log("prestate:");
|
||||
log_cond(p1);
|
||||
log("poststate:");
|
||||
log_cond(p2);
|
||||
}
|
||||
|
||||
fn log_states_err(&pre_and_post_state pp) -> () {
|
||||
auto p1 = bitv::to_vec(pp.prestate);
|
||||
auto p2 = bitv::to_vec(pp.poststate);
|
||||
log_err("prestate:");
|
||||
log_cond_err(p1);
|
||||
log_err("poststate:");
|
||||
log_cond_err(p2);
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* data structures */
|
||||
|
||||
/**********************************************************************/
|
||||
/* mapping from variable name (def_id is assumed to be for a local
|
||||
variable in a given function) to bit number
|
||||
(also remembers the ident for error-logging purposes) */
|
||||
type var_info = tup(uint, ident);
|
||||
type fn_info = rec(@std::map::hashmap[def_id, var_info] vars,
|
||||
controlflow cf);
|
||||
/* mapping from function name to fn_info map */
|
||||
type fn_info_map = @std::map::hashmap[def_id, fn_info];
|
||||
|
||||
type fn_ctxt = rec(fn_info enclosing,
|
||||
def_id id,
|
||||
ident name,
|
||||
crate_ctxt ccx);
|
||||
|
||||
type crate_ctxt = rec(ty::ctxt tcx,
|
||||
ty::node_type_table node_types,
|
||||
fn_info_map fm);
|
||||
|
||||
fn get_fn_info(fn_info_map fm, def_id did) -> fn_info {
|
||||
assert (fm.contains_key(did));
|
||||
ret fm.get(did);
|
||||
}
|
||||
|
||||
/********* utils ********/
|
||||
|
||||
|
||||
fn ann_to_ts_ann(ann a, uint nv) -> @ts_ann {
|
||||
alt (ann_to_ts_ann_fail(a)) {
|
||||
case (none[@ts_ann]) { ret @empty_ann(nv); }
|
||||
case (some[@ts_ann](?t)) { ret t; }
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_,_,_,?ty)) {
|
||||
ret ty;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn ann_to_ts_ann_strict(ann a) -> @ts_ann {
|
||||
alt (ann_to_ts_ann_fail(a)) {
|
||||
case (none[@ts_ann]) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?t)) {
|
||||
ret t;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn ann_to_poststate(ann a) -> poststate {
|
||||
ret (ann_to_ts_ann_strict(a)).states.poststate;
|
||||
}
|
||||
|
||||
fn stmt_to_ann(&stmt s) -> option::t[@ts_ann] {
|
||||
alt (s.node) {
|
||||
case (stmt_decl(_,?a)) {
|
||||
ret ann_to_ts_ann_fail(a);
|
||||
}
|
||||
case (stmt_expr(_,?a)) {
|
||||
ret ann_to_ts_ann_fail(a);
|
||||
}
|
||||
case (stmt_crate_directive(_)) {
|
||||
ret none[@ts_ann];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn stmt_to_ann_strict(&stmt s) -> @ts_ann {
|
||||
alt (stmt_to_ann(s)) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err("stmt_to_ann_strict: didn't expect none here");
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?a)) { ret a; }
|
||||
}
|
||||
}
|
||||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_states(@expr e) -> pre_and_post_state {
|
||||
ret (ann_to_ts_ann_strict(expr_ann(e)).states);
|
||||
}
|
||||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_pp(@expr e) -> pre_and_post {
|
||||
ret (ann_to_ts_ann_strict(expr_ann(e)).conditions);
|
||||
}
|
||||
|
||||
fn stmt_pp(&stmt s) -> pre_and_post {
|
||||
ret (stmt_to_ann_strict(s).conditions);
|
||||
}
|
||||
|
||||
/* fails if b has no annotation */
|
||||
fn block_pp(&block b) -> pre_and_post {
|
||||
ret (ann_to_ts_ann_strict(b.node.a).conditions);
|
||||
}
|
||||
|
||||
fn block_states(&block b) -> pre_and_post_state {
|
||||
ret (ann_to_ts_ann_strict(b.node.a).states);
|
||||
}
|
||||
|
||||
fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
|
||||
alt (stmt_to_ann(s)) {
|
||||
case (none[@ts_ann]) {
|
||||
ret empty_states(nv);
|
||||
}
|
||||
case (some[@ts_ann](?a)) {
|
||||
ret a.states;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn expr_precond(@expr e) -> precond {
|
||||
ret (expr_pp(e)).precondition;
|
||||
}
|
||||
|
||||
fn expr_postcond(@expr e) -> postcond {
|
||||
ret (expr_pp(e)).postcondition;
|
||||
}
|
||||
|
||||
fn expr_prestate(@expr e) -> prestate {
|
||||
ret (expr_states(e)).prestate;
|
||||
}
|
||||
|
||||
fn expr_poststate(@expr e) -> poststate {
|
||||
ret (expr_states(e)).poststate;
|
||||
}
|
||||
|
||||
fn stmt_precond(&stmt s) -> precond {
|
||||
ret (stmt_pp(s)).precondition;
|
||||
}
|
||||
|
||||
fn stmt_postcond(&stmt s) -> postcond {
|
||||
ret (stmt_pp(s)).postcondition;
|
||||
}
|
||||
|
||||
fn states_to_poststate(&pre_and_post_state ss) -> poststate {
|
||||
ret ss.poststate;
|
||||
}
|
||||
|
||||
fn stmt_prestate(&stmt s, uint nv) -> prestate {
|
||||
ret (stmt_states(s, nv)).prestate;
|
||||
}
|
||||
|
||||
fn stmt_poststate(&stmt s, uint nv) -> poststate {
|
||||
ret (stmt_states(s, nv)).poststate;
|
||||
}
|
||||
|
||||
fn block_postcond(&block b) -> postcond {
|
||||
ret (block_pp(b)).postcondition;
|
||||
}
|
||||
|
||||
fn block_poststate(&block b) -> poststate {
|
||||
ret (block_states(b)).poststate;
|
||||
}
|
||||
|
||||
/* returns a new annotation where the pre_and_post is p */
|
||||
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(?i, ?t, ?ps, _)) {
|
||||
ret (ann_type(i, t, ps,
|
||||
some[@ts_ann]
|
||||
(@rec(conditions=p,
|
||||
states=empty_states(pps_len(p))))));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn set_prestate_ann(&ann a, &prestate pre) -> bool {
|
||||
ret set_prestate(ann_to_ts_ann_strict(a), pre);
|
||||
}
|
||||
|
||||
|
||||
fn extend_prestate_ann(&ann a, &prestate pre) -> bool {
|
||||
ret extend_prestate(ann_to_ts_ann_strict(a).states.prestate, pre);
|
||||
}
|
||||
|
||||
fn set_poststate_ann(&ann a, &poststate post) -> bool {
|
||||
ret set_poststate(ann_to_ts_ann_strict(a), post);
|
||||
}
|
||||
|
||||
fn extend_poststate_ann(&ann a, &poststate post) -> bool {
|
||||
ret extend_poststate(ann_to_ts_ann_strict(a).states.poststate, post);
|
||||
}
|
||||
|
||||
fn set_pre_and_post(&ann a, &pre_and_post pp) -> () {
|
||||
auto t = ann_to_ts_ann_strict(a);
|
||||
set_precondition(t, pp.precondition);
|
||||
set_postcondition(t, pp.postcondition);
|
||||
}
|
||||
|
||||
fn pure_exp(&ann a, &prestate p) -> bool {
|
||||
auto changed = false;
|
||||
changed = extend_prestate_ann(a, p) || changed;
|
||||
changed = extend_poststate_ann(a, p) || changed;
|
||||
ret changed;
|
||||
}
|
||||
|
||||
fn fixed_point_states(&fn_ctxt fcx,
|
||||
fn (&fn_ctxt, &_fn) -> bool f, &_fn start) -> () {
|
||||
|
||||
auto changed = f(fcx, start);
|
||||
|
||||
if (changed) {
|
||||
ret fixed_point_states(fcx, f, start);
|
||||
}
|
||||
else {
|
||||
// we're done!
|
||||
ret;
|
||||
}
|
||||
}
|
||||
|
||||
fn init_ann(&fn_info fi, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_ann: shouldn't see ann_none");
|
||||
// fail;
|
||||
log("warning: init_ann: saw ann_none");
|
||||
ret a; // Would be better to fail so we can catch bugs that
|
||||
// result in an uninitialized ann -- but don't want to have to
|
||||
// write code to handle native_mods properly
|
||||
}
|
||||
case (ann_type(?i, ?t, ?ps, _)) {
|
||||
ret ann_type(i, t, ps, some[@ts_ann](@empty_ann(num_locals(fi))));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn init_blank_ann(&() ignore, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_blank_ann: shouldn't see ann_none");
|
||||
//fail;
|
||||
log("warning: init_blank_ann: saw ann_none");
|
||||
ret a;
|
||||
}
|
||||
case (ann_type(?i, ?t, ?ps,_)) {
|
||||
ret ann_type(i, 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_block: shouldn't see ann_none");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _, _, _)) {
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
|
||||
ret fold_block[fn_info](fi, fld0, respan(sp, b));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn num_locals(fn_info m) -> uint {
|
||||
ret m.vars.size();
|
||||
}
|
||||
|
||||
fn new_crate_ctxt(ty::node_type_table nt, ty::ctxt cx) -> crate_ctxt {
|
||||
ret rec(tcx=cx, node_types=nt, fm=@new_def_hash[fn_info]());
|
||||
}
|
||||
|
||||
fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
|
||||
alt (ccx.fm.find(d)) {
|
||||
case (some[fn_info](?fi)) { ret fi.cf; }
|
||||
case (none[fn_info]) { ret return; }
|
||||
}
|
||||
}
|
||||
|
||||
/* conservative approximation: uses the mapping if e refers to a known
|
||||
function or method, assumes returning otherwise.
|
||||
There's no case for fail b/c we assume e is the callee and it
|
||||
seems unlikely that one would apply "fail" to arguments. */
|
||||
fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
|
||||
auto f = ann_tag(expr_ann(e));
|
||||
alt (ccx.tcx.def_map.find(f)) {
|
||||
case (some[def](def_fn(?d))) { ret controlflow_def_id(ccx, d); }
|
||||
case (some[def](def_obj_field(?d))) { ret controlflow_def_id(ccx, d); }
|
||||
case (_) { ret return; }
|
||||
}
|
||||
}
|
||||
|
||||
fn ann_to_def_strict(&crate_ctxt ccx, &ann a) -> def {
|
||||
alt (ccx.tcx.def_map.find(ann_tag(a))) {
|
||||
case (none[def]) {
|
||||
log_err("ann_to_def: node_id " +
|
||||
uistr(ann_tag(a)) +
|
||||
" has no def");
|
||||
fail;
|
||||
}
|
||||
case (some[def](?d)) { ret d; }
|
||||
}
|
||||
}
|
||||
|
||||
fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
|
||||
ret ccx.tcx.def_map.find(ann_tag(a));
|
||||
}
|
||||
|
||||
//
|
||||
// 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:
|
||||
//
|
||||
|
||||
137
src/comp/middle/tstate/bitvectors.rs
Normal file
137
src/comp/middle/tstate/bitvectors.rs
Normal file
|
|
@ -0,0 +1,137 @@
|
|||
import std::bitv;
|
||||
import std::_vec;
|
||||
import std::_vec::len;
|
||||
import std::_vec::slice;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::def_id;
|
||||
import front::ast::expr;
|
||||
import front::ast::ann;
|
||||
|
||||
import aux::fn_ctxt;
|
||||
import aux::fn_info;
|
||||
import aux::log_bitv;
|
||||
import aux::num_locals;
|
||||
import aux::ann_to_ts_ann_strict;
|
||||
|
||||
import tstate::ann::pre_and_post;
|
||||
import tstate::ann::precond;
|
||||
import tstate::ann::postcond;
|
||||
import tstate::ann::prestate;
|
||||
import tstate::ann::poststate;
|
||||
import tstate::ann::relax_prestate;
|
||||
import tstate::ann::pps_len;
|
||||
import tstate::ann::true_precond;
|
||||
import tstate::ann::empty_prestate;
|
||||
import tstate::ann::difference;
|
||||
import tstate::ann::union;
|
||||
import tstate::ann::intersect;
|
||||
import tstate::ann::clone;
|
||||
import tstate::ann::set_in_postcond;
|
||||
import tstate::ann::set_in_poststate;
|
||||
|
||||
fn bit_num(def_id v, fn_info m) -> uint {
|
||||
assert (m.vars.contains_key(v));
|
||||
ret m.vars.get(v)._0;
|
||||
}
|
||||
|
||||
fn promises(&poststate p, def_id v, fn_info m) -> bool {
|
||||
ret bitv::get(p, bit_num(v, m));
|
||||
}
|
||||
|
||||
// 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(fn_info enclosing, vec[pre_and_post] pps) -> precond {
|
||||
let uint sz = len[pre_and_post](pps);
|
||||
let uint num_vars = num_locals(enclosing);
|
||||
|
||||
if (sz >= 1u) {
|
||||
auto first = pps.(0);
|
||||
assert (pps_len(first) == num_vars);
|
||||
let precond rest = seq_preconds(enclosing,
|
||||
slice[pre_and_post](pps, 1u, sz));
|
||||
difference(rest, first.postcondition);
|
||||
auto res = clone(first.precondition);
|
||||
union(res, rest);
|
||||
|
||||
log("seq_preconds:");
|
||||
log("first.postcondition =");
|
||||
log_bitv(enclosing, first.postcondition);
|
||||
log("rest =");
|
||||
log_bitv(enclosing, rest);
|
||||
log("returning");
|
||||
log_bitv(enclosing, res);
|
||||
|
||||
ret res;
|
||||
}
|
||||
else {
|
||||
ret true_precond(num_vars);
|
||||
}
|
||||
}
|
||||
|
||||
/* works on either postconds or preconds
|
||||
should probably rethink the whole type synonym situation */
|
||||
fn union_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
|
||||
auto sz = _vec::len[postcond](rest);
|
||||
|
||||
if (sz > 0u) {
|
||||
auto other = rest.(0);
|
||||
union(first, other);
|
||||
union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest)));
|
||||
}
|
||||
|
||||
ret first;
|
||||
}
|
||||
|
||||
fn union_postconds(uint nv, &vec[postcond] pcs) -> postcond {
|
||||
if (len[postcond](pcs) > 0u) {
|
||||
ret union_postconds_go(bitv::clone(pcs.(0)), pcs);
|
||||
}
|
||||
else {
|
||||
ret empty_prestate(nv);
|
||||
}
|
||||
}
|
||||
|
||||
/* Gee, maybe we could use foldl or something */
|
||||
fn intersect_postconds_go(&postcond first, &vec[postcond] rest) -> postcond {
|
||||
auto sz = _vec::len[postcond](rest);
|
||||
|
||||
if (sz > 0u) {
|
||||
auto other = rest.(0);
|
||||
intersect(first, other);
|
||||
intersect_postconds_go(first, slice[postcond](rest, 1u,
|
||||
len[postcond](rest)));
|
||||
}
|
||||
|
||||
ret first;
|
||||
}
|
||||
|
||||
fn intersect_postconds(&vec[postcond] pcs) -> postcond {
|
||||
assert (len[postcond](pcs) > 0u);
|
||||
|
||||
ret intersect_postconds_go(bitv::clone(pcs.(0)), pcs);
|
||||
}
|
||||
|
||||
fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
|
||||
assert (fcx.enclosing.vars.contains_key(id));
|
||||
let uint i = (fcx.enclosing.vars.get(id))._0;
|
||||
ret set_in_postcond(i, (ann_to_ts_ann_strict(a)).conditions);
|
||||
}
|
||||
|
||||
fn declare_var(&fn_info enclosing, def_id id, prestate pre)
|
||||
-> prestate {
|
||||
assert (enclosing.vars.contains_key(id));
|
||||
let uint i = (enclosing.vars.get(id))._0;
|
||||
auto res = clone(pre);
|
||||
relax_prestate(i, res);
|
||||
ret res;
|
||||
}
|
||||
|
||||
fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
|
||||
assert (fcx.enclosing.vars.contains_key(id));
|
||||
let uint i = (fcx.enclosing.vars.get(id))._0;
|
||||
ret set_in_poststate(i, (ann_to_ts_ann_strict(a)).states);
|
||||
}
|
||||
|
||||
231
src/comp/middle/tstate/ck.rs
Normal file
231
src/comp/middle/tstate/ck.rs
Normal file
|
|
@ -0,0 +1,231 @@
|
|||
import front::ast;
|
||||
import front::ast::method;
|
||||
import front::ast::ann;
|
||||
import front::ast::item;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::_fn;
|
||||
import front::ast::obj_field;
|
||||
import front::ast::_obj;
|
||||
import front::ast::stmt;
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ty_param;
|
||||
import front::ast::crate;
|
||||
|
||||
import front::ast::expr;
|
||||
import middle::fold::respan;
|
||||
import middle::fold::new_identity_fold;
|
||||
import middle::fold::fold_crate;
|
||||
import middle::ty::type_is_nil;
|
||||
import middle::ty::ret_ty_of_fn;
|
||||
import util::common::span;
|
||||
import tstate::ann::ts_ann;
|
||||
import tstate::ann::empty_poststate;
|
||||
import tstate::ann::true_precond;
|
||||
import tstate::ann::true_postcond;
|
||||
import tstate::ann::false_postcond;
|
||||
import tstate::ann::precond;
|
||||
import tstate::ann::postcond;
|
||||
import tstate::ann::poststate;
|
||||
import tstate::ann::prestate;
|
||||
import tstate::ann::implies;
|
||||
import tstate::ann::ann_precond;
|
||||
import tstate::ann::ann_prestate;
|
||||
import std::_vec::map;
|
||||
import std::_vec;
|
||||
import std::_vec::slice;
|
||||
import std::_vec::unzip;
|
||||
import std::_vec::plus_option;
|
||||
import std::_vec::cat_options;
|
||||
|
||||
import std::option;
|
||||
import std::option::t;
|
||||
import std::option::some;
|
||||
import std::option::none;
|
||||
|
||||
import aux::fn_ctxt;
|
||||
import aux::crate_ctxt;
|
||||
import aux::new_crate_ctxt;
|
||||
import aux::expr_precond;
|
||||
import aux::expr_prestate;
|
||||
import aux::expr_poststate;
|
||||
import aux::stmt_poststate;
|
||||
import aux::stmt_to_ann;
|
||||
import aux::num_locals;
|
||||
import aux::fixed_point_states;
|
||||
import aux::bitv_to_str;
|
||||
|
||||
import util::common::ty_to_str;
|
||||
import bitvectors::promises;
|
||||
|
||||
import annotate::annotate_crate;
|
||||
import collect_locals::mk_f_to_fn_info;
|
||||
import pre_post_conditions::check_item_fn;
|
||||
import states::find_pre_post_state_fn;
|
||||
|
||||
fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
|
||||
let precond prec = expr_precond(e);
|
||||
let prestate pres = expr_prestate(e);
|
||||
|
||||
if (!implies(pres, prec)) {
|
||||
auto s = "";
|
||||
s += ("Unsatisfied precondition constraint for expression:\n");
|
||||
s += util::common::expr_to_str(e);
|
||||
s += ("Precondition: ");
|
||||
s += bitv_to_str(fcx.enclosing, prec);
|
||||
s += ("Prestate: ");
|
||||
s += bitv_to_str(fcx.enclosing, pres);
|
||||
fcx.ccx.tcx.sess.span_err(e.span, s);
|
||||
}
|
||||
}
|
||||
|
||||
fn check_states_stmt(&fn_ctxt fcx, &stmt s) -> () {
|
||||
alt (stmt_to_ann(s)) {
|
||||
case (none[@ts_ann]) {
|
||||
ret;
|
||||
}
|
||||
case (some[@ts_ann](?a)) {
|
||||
let precond prec = ann_precond(*a);
|
||||
let prestate pres = ann_prestate(*a);
|
||||
|
||||
/*
|
||||
log("check_states_stmt:");
|
||||
log_stmt(s);
|
||||
log("prec = ");
|
||||
log_bitv(enclosing, prec);
|
||||
log("pres = ");
|
||||
log_bitv(enclosing, pres);
|
||||
*/
|
||||
|
||||
if (!implies(pres, prec)) {
|
||||
auto ss = "";
|
||||
ss += ("Unsatisfied precondition constraint for statement:\n");
|
||||
ss += util::common::stmt_to_str(s);
|
||||
ss += ("Precondition: ");
|
||||
ss += bitv_to_str(fcx.enclosing, prec);
|
||||
ss += ("Prestate: ");
|
||||
ss += bitv_to_str(fcx.enclosing, pres);
|
||||
fcx.ccx.tcx.sess.span_err(s.span, ss);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto nv = num_locals(enclosing);
|
||||
auto post = @empty_poststate(nv);
|
||||
|
||||
fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post, uint nv) -> () {
|
||||
check_states_stmt(fcx, *s);
|
||||
*post = stmt_poststate(*s, nv);
|
||||
}
|
||||
|
||||
auto do_one = bind do_one_(fcx, _, post, nv);
|
||||
|
||||
_vec::map[@stmt, ()](do_one, f.body.node.stmts);
|
||||
fn do_inner_(fn_ctxt fcx, &@expr e, @poststate post) -> () {
|
||||
check_states_expr(fcx, e);
|
||||
*post = expr_poststate(e);
|
||||
}
|
||||
auto do_inner = bind do_inner_(fcx, _, post);
|
||||
option::map[@expr, ()](do_inner, f.body.node.expr);
|
||||
|
||||
/* Finally, check that the return value is initialized */
|
||||
if (f.proto == ast::proto_fn
|
||||
&& ! promises(*post, fcx.id, enclosing)
|
||||
&& ! type_is_nil(fcx.ccx.tcx,
|
||||
ret_ty_of_fn(fcx.ccx.node_types, fcx.ccx.tcx, a)) ) {
|
||||
/* FIXME: make this an error, not warning, once I finish implementing
|
||||
! annotations */
|
||||
/* fcx.ccx.tcx.sess.span_err(f.body.span, "Function " +
|
||||
fcx.name + " may not return. Its declared return type is "
|
||||
+ util.common.ty_to_str(*f.decl.output)); */
|
||||
log_err("WARNING: Function " +
|
||||
fcx.name + " may not return. Its declared return type is "
|
||||
+ ty_to_str(*f.decl.output));
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
fn check_fn_states(&fn_ctxt fcx, &_fn f, &ann a) -> () {
|
||||
/* Compute the pre- and post-states for this function */
|
||||
auto g = find_pre_post_state_fn;
|
||||
fixed_point_states(fcx, g, f);
|
||||
|
||||
/* Now compare each expr's pre-state to its precondition
|
||||
and post-state to its postcondition */
|
||||
check_states_against_conditions(fcx, f, a);
|
||||
}
|
||||
|
||||
fn check_item_fn_state(&crate_ctxt ccx, &span sp, &ident i,
|
||||
&_fn f, &vec[ty_param] ty_params,
|
||||
&def_id id, &ann a) -> @item {
|
||||
|
||||
/* Look up the var-to-bit-num map for this function */
|
||||
assert (ccx.fm.contains_key(id));
|
||||
auto f_info = ccx.fm.get(id);
|
||||
|
||||
auto fcx = rec(enclosing=f_info, id=id, name=i, ccx=ccx);
|
||||
check_fn_states(fcx, f, a);
|
||||
|
||||
/* Rebuild the same function */
|
||||
ret @respan(sp, item_fn(i, f, ty_params, id, a));
|
||||
}
|
||||
|
||||
fn check_method_states(&crate_ctxt ccx, @method m) -> () {
|
||||
assert (ccx.fm.contains_key(m.node.id));
|
||||
auto fcx = rec(enclosing=ccx.fm.get(m.node.id),
|
||||
id=m.node.id, name=m.node.ident, ccx=ccx);
|
||||
check_fn_states(fcx, m.node.meth, m.node.ann);
|
||||
}
|
||||
|
||||
fn check_obj_state(&crate_ctxt ccx, &vec[obj_field] fields,
|
||||
&vec[@method] methods,
|
||||
&option::t[@method] dtor) -> _obj {
|
||||
fn one(crate_ctxt ccx, &@method m) -> () {
|
||||
ret check_method_states(ccx, m);
|
||||
}
|
||||
auto f = bind one(ccx,_);
|
||||
_vec::map[@method, ()](f, methods);
|
||||
option::map[@method, ()](f, dtor);
|
||||
ret rec(fields=fields, methods=methods, dtor=dtor);
|
||||
}
|
||||
|
||||
/* FIXME use walk instead of fold where possible */
|
||||
|
||||
fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
|
||||
let crate_ctxt ccx = new_crate_ctxt(nt, cx);
|
||||
|
||||
/* Build the global map from function id to var-to-bit-num-map */
|
||||
mk_f_to_fn_info(ccx, crate);
|
||||
|
||||
/* Add a blank ts_ann to every statement (and expression) */
|
||||
auto with_anns = annotate_crate(ccx.fm, crate);
|
||||
|
||||
/* Compute the pre and postcondition for every subexpression */
|
||||
|
||||
auto fld = new_identity_fold[crate_ctxt]();
|
||||
fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
|
||||
auto with_pre_postconditions =
|
||||
fold_crate[crate_ctxt](ccx, fld, with_anns);
|
||||
|
||||
auto fld1 = new_identity_fold[crate_ctxt]();
|
||||
|
||||
fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_),
|
||||
fold_obj = bind check_obj_state(_,_,_,_)
|
||||
with *fld1);
|
||||
|
||||
ret fold_crate[crate_ctxt](ccx, fld1, with_pre_postconditions);
|
||||
}
|
||||
|
||||
//
|
||||
// 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:
|
||||
//
|
||||
122
src/comp/middle/tstate/collect_locals.rs
Normal file
122
src/comp/middle/tstate/collect_locals.rs
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
import std::_vec;
|
||||
import std::_vec::plus_option;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::crate;
|
||||
import front::ast::ann;
|
||||
import front::ast::arg;
|
||||
import front::ast::method;
|
||||
import front::ast::local;
|
||||
import front::ast::item;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::item_obj;
|
||||
import front::ast::_obj;
|
||||
import front::ast::obj_def_ids;
|
||||
import front::ast::_fn;
|
||||
import front::ast::ty_param;
|
||||
import front::ast::_mod;
|
||||
import front::ast::decl;
|
||||
import front::ast::decl_local;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ident;
|
||||
import middle::fold::span;
|
||||
import middle::fold::respan;
|
||||
import middle::fold::new_identity_fold;
|
||||
import middle::fold::fold_block;
|
||||
import middle::fold::fold_fn;
|
||||
import middle::fold::fold_crate;
|
||||
|
||||
import aux::fn_info;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
|
||||
import util::common::new_def_hash;
|
||||
|
||||
fn var_is_local(def_id v, fn_info m) -> bool {
|
||||
ret (m.vars.contains_key(v));
|
||||
}
|
||||
|
||||
fn collect_local(&@vec[tup(ident, def_id)] vars, &span sp, &@local loc)
|
||||
-> @decl {
|
||||
log("collect_local: pushing " + loc.ident);
|
||||
_vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
|
||||
ret @respan(sp, decl_local(loc));
|
||||
}
|
||||
|
||||
fn find_locals(_fn f) -> @vec[tup(ident,def_id)] {
|
||||
auto res = @_vec::alloc[tup(ident,def_id)](0u);
|
||||
|
||||
auto fld = new_identity_fold[@vec[tup(ident, def_id)]]();
|
||||
fld = @rec(fold_decl_local = bind collect_local(_,_,_) with *fld);
|
||||
auto ignore = fold_fn[@vec[tup(ident, def_id)]](res, fld, f);
|
||||
|
||||
ret res;
|
||||
}
|
||||
|
||||
|
||||
fn add_var(def_id v, ident nm, uint next, fn_info tbl) -> uint {
|
||||
log(nm + " |-> " + util::common::uistr(next));
|
||||
tbl.vars.insert(v, tup(next,nm));
|
||||
ret (next + 1u);
|
||||
}
|
||||
|
||||
/* builds a table mapping each local var defined in f
|
||||
to a bit number in the precondition/postcondition vectors */
|
||||
fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
|
||||
auto res = rec(vars=@new_def_hash[var_info](),
|
||||
cf=f.decl.cf);
|
||||
let uint next = 0u;
|
||||
let vec[arg] f_args = f.decl.inputs;
|
||||
|
||||
/* ignore args, which we know are initialized;
|
||||
just collect locally declared vars */
|
||||
|
||||
let @vec[tup(ident,def_id)] locals = find_locals(f);
|
||||
// log (uistr(_vec::len[tup(ident, def_id)](locals)) + " locals");
|
||||
for (tup(ident,def_id) p in *locals) {
|
||||
next = add_var(p._1, p._0, next, res);
|
||||
}
|
||||
/* add a pseudo-entry for the function's return value
|
||||
we can safely use the function's name itself for this purpose */
|
||||
add_var(f_id, f_name, next, res);
|
||||
|
||||
ret res;
|
||||
}
|
||||
|
||||
/* 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(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
|
||||
&vec[ty_param] ty_params, &def_id id, &ann a) -> @item {
|
||||
auto f_inf = mk_fn_info(f, id, i);
|
||||
ccx.fm.insert(id, f_inf);
|
||||
// log_err("inserting: " + i);
|
||||
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(&crate_ctxt ccx, &span sp, &ident i, &_obj o,
|
||||
&vec[ty_param] ty_params,
|
||||
&obj_def_ids odid, &ann a) -> @item {
|
||||
auto all_methods = _vec::clone[@method](o.methods);
|
||||
plus_option[@method](all_methods, o.dtor);
|
||||
auto f_inf;
|
||||
for (@method m in all_methods) {
|
||||
f_inf = mk_fn_info(m.node.meth, m.node.id, m.node.ident);
|
||||
ccx.fm.insert(m.node.id, f_inf);
|
||||
}
|
||||
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(&crate_ctxt ccx, @crate c) -> () {
|
||||
|
||||
auto fld = new_identity_fold[crate_ctxt]();
|
||||
fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_),
|
||||
fold_item_obj = bind mk_fn_info_item_obj(_,_,_,_,_,_,_)
|
||||
with *fld);
|
||||
fold_crate[crate_ctxt](ccx, fld, c);
|
||||
}
|
||||
711
src/comp/middle/tstate/pre_post_conditions.rs
Normal file
711
src/comp/middle/tstate/pre_post_conditions.rs
Normal file
|
|
@ -0,0 +1,711 @@
|
|||
import std::_vec;
|
||||
import std::_vec::plus_option;
|
||||
import std::option;
|
||||
import std::option::none;
|
||||
import std::option::some;
|
||||
|
||||
import tstate::ann::pre_and_post;
|
||||
import tstate::ann::get_post;
|
||||
import tstate::ann::postcond;
|
||||
import tstate::ann::true_precond;
|
||||
import tstate::ann::false_postcond;
|
||||
import tstate::ann::empty_pre_post;
|
||||
import tstate::ann::empty_poststate;
|
||||
import tstate::ann::require_and_preserve;
|
||||
import tstate::ann::union;
|
||||
import tstate::ann::intersect;
|
||||
import tstate::ann::pp_clone;
|
||||
import tstate::ann::empty_prestate;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::fn_ctxt;
|
||||
import aux::num_locals;
|
||||
import aux::expr_pp;
|
||||
import aux::stmt_pp;
|
||||
import aux::block_pp;
|
||||
import aux::set_pre_and_post;
|
||||
import aux::expr_precond;
|
||||
import aux::expr_postcond;
|
||||
import aux::expr_prestate;
|
||||
import aux::expr_poststate;
|
||||
import aux::block_postcond;
|
||||
import aux::fn_info;
|
||||
import aux::log_pp;
|
||||
import aux::ann_to_def;
|
||||
import aux::ann_to_def_strict;
|
||||
|
||||
import bitvectors::seq_preconds;
|
||||
import bitvectors::union_postconds;
|
||||
import bitvectors::intersect_postconds;
|
||||
import bitvectors::declare_var;
|
||||
import bitvectors::bit_num;
|
||||
import bitvectors::gen;
|
||||
|
||||
import front::ast::_mod;
|
||||
import front::ast;
|
||||
import front::ast::method;
|
||||
import front::ast::ann;
|
||||
import front::ast::ty;
|
||||
import front::ast::mutability;
|
||||
import front::ast::item;
|
||||
import front::ast::item_const;
|
||||
import front::ast::item_mod;
|
||||
import front::ast::item_ty;
|
||||
import front::ast::item_tag;
|
||||
import front::ast::item_native_mod;
|
||||
import front::ast::obj_field;
|
||||
import front::ast::stmt;
|
||||
import front::ast::stmt_;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ann;
|
||||
import front::ast::expr;
|
||||
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::controlflow;
|
||||
import front::ast::return;
|
||||
import front::ast::noreturn;
|
||||
import front::ast::_fn;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::_obj;
|
||||
import front::ast::_mod;
|
||||
import front::ast::crate;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::item_obj;
|
||||
import front::ast::def_local;
|
||||
import front::ast::def_fn;
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ann;
|
||||
import front::ast::item;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::expr;
|
||||
import front::ast::elt;
|
||||
import front::ast::field;
|
||||
import front::ast::decl;
|
||||
import front::ast::decl_local;
|
||||
import front::ast::decl_item;
|
||||
import front::ast::initializer;
|
||||
import front::ast::local;
|
||||
import front::ast::arm;
|
||||
import front::ast::expr_call;
|
||||
import front::ast::expr_vec;
|
||||
import front::ast::expr_tup;
|
||||
import front::ast::expr_path;
|
||||
import front::ast::expr_field;
|
||||
import front::ast::expr_index;
|
||||
import front::ast::expr_log;
|
||||
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;
|
||||
import front::ast::expr_assert;
|
||||
import front::ast::expr_cast;
|
||||
import front::ast::expr_for;
|
||||
import front::ast::expr_for_each;
|
||||
import front::ast::stmt;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::stmt_expr;
|
||||
import front::ast::block;
|
||||
import front::ast::block_;
|
||||
import front::ast::method;
|
||||
|
||||
import middle::fold::span;
|
||||
import middle::fold::respan;
|
||||
|
||||
import util::common::new_def_hash;
|
||||
import util::common::decl_lhs;
|
||||
import util::common::uistr;
|
||||
import util::common::log_expr;
|
||||
import util::common::log_fn;
|
||||
import util::common::elt_exprs;
|
||||
import util::common::field_exprs;
|
||||
import util::common::has_nonlocal_exits;
|
||||
import util::common::log_stmt;
|
||||
import util::common::log_expr_err;
|
||||
|
||||
fn find_pre_post_mod(&_mod m) -> _mod {
|
||||
log("implement find_pre_post_mod!");
|
||||
fail;
|
||||
}
|
||||
|
||||
fn find_pre_post_native_mod(&native_mod m) -> native_mod {
|
||||
log("implement find_pre_post_native_mod");
|
||||
fail;
|
||||
}
|
||||
|
||||
|
||||
fn find_pre_post_obj(&crate_ctxt ccx, _obj o) -> () {
|
||||
fn do_a_method(crate_ctxt ccx, &@method m) -> () {
|
||||
assert (ccx.fm.contains_key(m.node.id));
|
||||
let fn_ctxt fcx = rec(enclosing=ccx.fm.get(m.node.id),
|
||||
id=m.node.id, name=m.node.ident, ccx=ccx);
|
||||
find_pre_post_fn(fcx, m.node.meth);
|
||||
}
|
||||
auto f = bind do_a_method(ccx,_);
|
||||
_vec::map[@method, ()](f, o.methods);
|
||||
option::map[@method, ()](f, o.dtor);
|
||||
}
|
||||
|
||||
fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
|
||||
alt (i.node) {
|
||||
case (item_const(?id, ?t, ?e, ?di, ?a)) {
|
||||
// make a fake fcx
|
||||
auto fake_fcx = rec(enclosing=rec(vars=@new_def_hash[var_info](),
|
||||
cf=return),
|
||||
id=tup(0,0),
|
||||
name="",
|
||||
ccx=ccx);
|
||||
find_pre_post_expr(fake_fcx, e);
|
||||
}
|
||||
case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
|
||||
assert (ccx.fm.contains_key(di));
|
||||
auto fcx = rec(enclosing=ccx.fm.get(di),
|
||||
id=di, name=id, ccx=ccx);
|
||||
find_pre_post_fn(fcx, f);
|
||||
}
|
||||
case (item_mod(?id, ?m, ?di)) {
|
||||
find_pre_post_mod(m);
|
||||
}
|
||||
case (item_native_mod(?id, ?nm, ?di)) {
|
||||
find_pre_post_native_mod(nm);
|
||||
}
|
||||
case (item_ty(_,_,_,_,_)) {
|
||||
ret;
|
||||
}
|
||||
case (item_tag(_,_,_,_,_)) {
|
||||
ret;
|
||||
}
|
||||
case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
|
||||
find_pre_post_obj(ccx, o);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* Finds the pre and postcondition for each expr in <args>;
|
||||
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_ctxt fcx, &vec[@expr] args, ann a) {
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto fm = fcx.ccx.fm;
|
||||
auto nv = num_locals(enclosing);
|
||||
|
||||
fn do_one(fn_ctxt fcx, &@expr e) -> () {
|
||||
find_pre_post_expr(fcx, e);
|
||||
}
|
||||
auto f = bind do_one(fcx, _);
|
||||
|
||||
_vec::map[@expr, ()](f, args);
|
||||
|
||||
fn get_pp(&@expr e) -> pre_and_post {
|
||||
ret expr_pp(e);
|
||||
}
|
||||
auto g = get_pp;
|
||||
auto pps = _vec::map[@expr, pre_and_post](g, args);
|
||||
auto h = get_post;
|
||||
|
||||
set_pre_and_post(a,
|
||||
rec(precondition=seq_preconds(enclosing, pps),
|
||||
postcondition=union_postconds
|
||||
(nv, (_vec::map[pre_and_post, postcond](h, pps)))));
|
||||
}
|
||||
|
||||
fn find_pre_post_loop(&fn_ctxt fcx, &@decl d, &@expr index,
|
||||
&block body, &ann a) -> () {
|
||||
find_pre_post_expr(fcx, index);
|
||||
find_pre_post_block(fcx, body);
|
||||
auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
|
||||
seq_preconds(fcx.enclosing, vec(expr_pp(index),
|
||||
block_pp(body))));
|
||||
auto loop_postcond = intersect_postconds
|
||||
(vec(expr_postcond(index), block_postcond(body)));
|
||||
set_pre_and_post(a, rec(precondition=loop_precond,
|
||||
postcondition=loop_postcond));
|
||||
}
|
||||
|
||||
fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var) -> () {
|
||||
alt (ann_to_def(fcx.ccx, new_var)) {
|
||||
case (some[def](def_local(?d_id))) {
|
||||
find_pre_post_expr(fcx, rhs);
|
||||
set_pre_and_post(larger_ann, expr_pp(rhs));
|
||||
gen(fcx, larger_ann, d_id);
|
||||
}
|
||||
case (_) { find_pre_post_exprs(fcx, vec(lhs, rhs), larger_ann); }
|
||||
}
|
||||
}
|
||||
|
||||
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
||||
fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto num_local_vars = num_locals(enclosing);
|
||||
|
||||
fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
|
||||
find_pre_post_expr(fcx, e);
|
||||
}
|
||||
fn pp_one(&@expr e) -> pre_and_post {
|
||||
ret expr_pp(e);
|
||||
}
|
||||
|
||||
/*
|
||||
log_err("find_pre_post_expr (num_locals =" +
|
||||
uistr(num_local_vars) + "):");
|
||||
log_expr_err(*e);
|
||||
*/
|
||||
|
||||
alt (e.node) {
|
||||
case (expr_call(?operator, ?operands, ?a)) {
|
||||
auto args = _vec::clone[@expr](operands);
|
||||
_vec::push[@expr](args, operator);
|
||||
find_pre_post_exprs(fcx, args, a);
|
||||
}
|
||||
case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
|
||||
auto args = _vec::clone[@expr](operands);
|
||||
_vec::push[@expr](args, operator);
|
||||
find_pre_post_exprs(fcx, args, a);
|
||||
}
|
||||
case (expr_vec(?args, _, ?a)) {
|
||||
find_pre_post_exprs(fcx, args, a);
|
||||
}
|
||||
case (expr_tup(?elts, ?a)) {
|
||||
find_pre_post_exprs(fcx, elt_exprs(elts), a);
|
||||
}
|
||||
case (expr_path(?p, ?a)) {
|
||||
auto res = empty_pre_post(num_local_vars);
|
||||
|
||||
auto df = ann_to_def_strict(fcx.ccx, a);
|
||||
alt (df) {
|
||||
case (def_local(?d_id)) {
|
||||
auto i = bit_num(d_id, enclosing);
|
||||
require_and_preserve(i, res);
|
||||
}
|
||||
case (_) { /* nothing to check */ }
|
||||
}
|
||||
|
||||
// Otherwise, variable is global, so it must be initialized
|
||||
set_pre_and_post(a, res);
|
||||
}
|
||||
case (expr_self_method(?v, ?a)) {
|
||||
/* v is a method of the enclosing obj, so it must be
|
||||
initialized, right? */
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
case(expr_log(_, ?arg, ?a)) {
|
||||
find_pre_post_expr(fcx, arg);
|
||||
set_pre_and_post(a, expr_pp(arg));
|
||||
}
|
||||
case (expr_chan(?arg, ?a)) {
|
||||
find_pre_post_expr(fcx, arg);
|
||||
set_pre_and_post(a, expr_pp(arg));
|
||||
}
|
||||
case(expr_put(?opt, ?a)) {
|
||||
alt (opt) {
|
||||
case (some[@expr](?arg)) {
|
||||
find_pre_post_expr(fcx, arg);
|
||||
set_pre_and_post(a, expr_pp(arg));
|
||||
}
|
||||
case (none[@expr]) {
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_block(?b, ?a)) {
|
||||
find_pre_post_block(fcx, b);
|
||||
set_pre_and_post(a, block_pp(b));
|
||||
}
|
||||
case (expr_rec(?fields,?maybe_base,?a)) {
|
||||
auto es = field_exprs(fields);
|
||||
_vec::plus_option[@expr](es, maybe_base);
|
||||
find_pre_post_exprs(fcx, es, a);
|
||||
}
|
||||
case (expr_assign(?lhs, ?rhs, ?a)) {
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
gen_if_local(fcx, lhs, rhs, a, a_lhs);
|
||||
}
|
||||
case (_) {
|
||||
find_pre_post_exprs(fcx, vec(lhs, rhs), a);
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_recv(?lhs, ?rhs, ?a)) {
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
gen_if_local(fcx, lhs, rhs, a, a_lhs);
|
||||
}
|
||||
case (_) {
|
||||
// doesn't check that lhs is an lval, but
|
||||
// that's probably ok
|
||||
find_pre_post_exprs(fcx, vec(lhs, rhs), a);
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_assign_op(_, ?lhs, ?rhs, ?a)) {
|
||||
/* Different from expr_assign in that the lhs *must*
|
||||
already be initialized */
|
||||
find_pre_post_exprs(fcx, vec(lhs, rhs), a);
|
||||
}
|
||||
case (expr_lit(_,?a)) {
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
case (expr_ret(?maybe_val, ?a)) {
|
||||
alt (maybe_val) {
|
||||
case (none[@expr]) {
|
||||
set_pre_and_post(a,
|
||||
rec(precondition=true_precond(num_local_vars),
|
||||
postcondition=false_postcond(num_local_vars)));
|
||||
}
|
||||
case (some[@expr](?ret_val)) {
|
||||
find_pre_post_expr(fcx, ret_val);
|
||||
let pre_and_post pp =
|
||||
rec(precondition=expr_precond(ret_val),
|
||||
postcondition=false_postcond(num_local_vars));
|
||||
set_pre_and_post(a, pp);
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_be(?e, ?a)) {
|
||||
find_pre_post_expr(fcx, e);
|
||||
set_pre_and_post(a,
|
||||
rec(precondition=expr_prestate(e),
|
||||
postcondition=false_postcond(num_local_vars)));
|
||||
}
|
||||
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
|
||||
find_pre_post_expr(fcx, antec);
|
||||
find_pre_post_block(fcx, conseq);
|
||||
alt (maybe_alt) {
|
||||
case (none[@expr]) {
|
||||
auto precond_res = seq_preconds(enclosing,
|
||||
vec(expr_pp(antec),
|
||||
block_pp(conseq)));
|
||||
set_pre_and_post(a, rec(precondition=precond_res,
|
||||
postcondition=
|
||||
expr_poststate(antec)));
|
||||
}
|
||||
case (some[@expr](?altern)) {
|
||||
find_pre_post_expr(fcx, altern);
|
||||
auto precond_true_case =
|
||||
seq_preconds(enclosing,
|
||||
vec(expr_pp(antec), block_pp(conseq)));
|
||||
auto postcond_true_case = union_postconds
|
||||
(num_local_vars,
|
||||
vec(expr_postcond(antec), block_postcond(conseq)));
|
||||
auto precond_false_case = seq_preconds
|
||||
(enclosing,
|
||||
vec(expr_pp(antec), expr_pp(altern)));
|
||||
auto postcond_false_case = union_postconds
|
||||
(num_local_vars,
|
||||
vec(expr_postcond(antec), expr_postcond(altern)));
|
||||
auto precond_res = union_postconds
|
||||
(num_local_vars,
|
||||
vec(precond_true_case, precond_false_case));
|
||||
auto postcond_res = intersect_postconds
|
||||
(vec(postcond_true_case, postcond_false_case));
|
||||
set_pre_and_post(a, rec(precondition=precond_res,
|
||||
postcondition=postcond_res));
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_binary(?bop,?l,?r,?a)) {
|
||||
/* *unless* bop is lazy (e.g. and, or)?
|
||||
FIXME */
|
||||
find_pre_post_exprs(fcx, vec(l, r), a);
|
||||
}
|
||||
case (expr_send(?l, ?r, ?a)) {
|
||||
find_pre_post_exprs(fcx, vec(l, r), a);
|
||||
}
|
||||
case (expr_unary(_,?operand,?a)) {
|
||||
find_pre_post_expr(fcx, operand);
|
||||
set_pre_and_post(a, expr_pp(operand));
|
||||
}
|
||||
case (expr_cast(?operand, _, ?a)) {
|
||||
find_pre_post_expr(fcx, operand);
|
||||
set_pre_and_post(a, expr_pp(operand));
|
||||
}
|
||||
case (expr_while(?test, ?body, ?a)) {
|
||||
find_pre_post_expr(fcx, test);
|
||||
find_pre_post_block(fcx, body);
|
||||
set_pre_and_post(a,
|
||||
rec(precondition=
|
||||
seq_preconds(enclosing,
|
||||
vec(expr_pp(test),
|
||||
block_pp(body))),
|
||||
postcondition=
|
||||
intersect_postconds(vec(expr_postcond(test),
|
||||
block_postcond(body)))));
|
||||
}
|
||||
case (expr_do_while(?body, ?test, ?a)) {
|
||||
find_pre_post_block(fcx, body);
|
||||
find_pre_post_expr(fcx, test);
|
||||
|
||||
auto loop_postcond = union_postconds(num_local_vars,
|
||||
vec(block_postcond(body), expr_postcond(test)));
|
||||
/* conservative approximination: if the body
|
||||
could break or cont, the test may never be executed */
|
||||
if (has_nonlocal_exits(body)) {
|
||||
loop_postcond = empty_poststate(num_local_vars);
|
||||
}
|
||||
|
||||
set_pre_and_post(a,
|
||||
rec(precondition=seq_preconds(enclosing,
|
||||
vec(block_pp(body),
|
||||
expr_pp(test))),
|
||||
postcondition=loop_postcond));
|
||||
}
|
||||
case (expr_for(?d, ?index, ?body, ?a)) {
|
||||
find_pre_post_loop(fcx, d, index, body, a);
|
||||
}
|
||||
case (expr_for_each(?d, ?index, ?body, ?a)) {
|
||||
find_pre_post_loop(fcx, d, index, body, a);
|
||||
}
|
||||
case (expr_index(?e, ?sub, ?a)) {
|
||||
find_pre_post_exprs(fcx, vec(e, sub), a);
|
||||
}
|
||||
case (expr_alt(?e, ?alts, ?a)) {
|
||||
find_pre_post_expr(fcx, e);
|
||||
fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
|
||||
find_pre_post_block(fcx, an_alt.block);
|
||||
ret block_pp(an_alt.block);
|
||||
}
|
||||
auto f = bind do_an_alt(fcx, _);
|
||||
auto alt_pps = _vec::map[arm, pre_and_post](f, alts);
|
||||
fn combine_pp(pre_and_post antec,
|
||||
fn_info enclosing, &pre_and_post pp,
|
||||
&pre_and_post next) -> pre_and_post {
|
||||
union(pp.precondition, seq_preconds(enclosing,
|
||||
vec(antec, next)));
|
||||
intersect(pp.postcondition, next.postcondition);
|
||||
ret pp;
|
||||
}
|
||||
auto antec_pp = pp_clone(expr_pp(e));
|
||||
auto e_pp = rec(precondition=empty_prestate(num_local_vars),
|
||||
postcondition=false_postcond(num_local_vars));
|
||||
auto g = bind combine_pp(antec_pp, fcx.enclosing, _, _);
|
||||
|
||||
auto alts_overall_pp = _vec::foldl[pre_and_post, pre_and_post]
|
||||
(g, e_pp, alt_pps);
|
||||
|
||||
set_pre_and_post(a, alts_overall_pp);
|
||||
}
|
||||
case (expr_field(?operator, _, ?a)) {
|
||||
find_pre_post_expr(fcx, operator);
|
||||
set_pre_and_post(a, expr_pp(operator));
|
||||
}
|
||||
case (expr_fail(?a)) {
|
||||
set_pre_and_post(a,
|
||||
/* if execution continues after fail,
|
||||
then everything is true! */
|
||||
rec(precondition=empty_prestate(num_local_vars),
|
||||
postcondition=false_postcond(num_local_vars)));
|
||||
}
|
||||
case (expr_assert(?p, ?a)) {
|
||||
find_pre_post_expr(fcx, p);
|
||||
set_pre_and_post(a, expr_pp(p));
|
||||
}
|
||||
case (expr_check(?p, ?a)) {
|
||||
/* will need to change when we support arbitrary predicates... */
|
||||
find_pre_post_expr(fcx, p);
|
||||
set_pre_and_post(a, expr_pp(p));
|
||||
}
|
||||
case(expr_bind(?operator, ?maybe_args, ?a)) {
|
||||
auto args = _vec::cat_options[@expr](maybe_args);
|
||||
_vec::push[@expr](args, operator); /* ??? order of eval? */
|
||||
find_pre_post_exprs(fcx, args, a);
|
||||
}
|
||||
case (expr_break(?a)) {
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
case (expr_cont(?a)) {
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
case (expr_port(?a)) {
|
||||
set_pre_and_post(a, empty_pre_post(num_local_vars));
|
||||
}
|
||||
case (expr_ext(_, _, _, ?expanded, ?a)) {
|
||||
find_pre_post_expr(fcx, expanded);
|
||||
set_pre_and_post(a, expr_pp(expanded));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
|
||||
-> () {
|
||||
log("stmt =");
|
||||
log_stmt(s);
|
||||
|
||||
auto enclosing = fcx.enclosing;
|
||||
auto num_local_vars = num_locals(enclosing);
|
||||
alt(s.node) {
|
||||
case(stmt_decl(?adecl, ?a)) {
|
||||
alt(adecl.node) {
|
||||
case(decl_local(?alocal)) {
|
||||
alt(alocal.init) {
|
||||
case(some[initializer](?an_init)) {
|
||||
find_pre_post_expr(fcx, an_init.expr);
|
||||
auto rhs_pp = expr_pp(an_init.expr);
|
||||
set_pre_and_post(alocal.ann, rhs_pp);
|
||||
|
||||
/* Inherit ann from initializer, and add var being
|
||||
initialized to the postcondition */
|
||||
set_pre_and_post(a, rhs_pp);
|
||||
/* log("gen (decl):");
|
||||
log_stmt(s); */
|
||||
gen(fcx, a, alocal.id);
|
||||
/* log_err("for stmt");
|
||||
log_stmt(s);
|
||||
log_err("pp = ");
|
||||
log_pp(stmt_pp(s)); */
|
||||
}
|
||||
case(none[initializer]) {
|
||||
auto pp = empty_pre_post(num_local_vars);
|
||||
set_pre_and_post(alocal.ann, pp);
|
||||
set_pre_and_post(a, pp);
|
||||
}
|
||||
}
|
||||
}
|
||||
case(decl_item(?anitem)) {
|
||||
auto pp = empty_pre_post(num_local_vars);
|
||||
set_pre_and_post(a, pp);
|
||||
find_pre_post_item(fcx.ccx, *anitem);
|
||||
}
|
||||
}
|
||||
}
|
||||
case(stmt_expr(?e,?a)) {
|
||||
find_pre_post_expr(fcx, e);
|
||||
set_pre_and_post(a, expr_pp(e));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
|
||||
/* Want to say that if there is a break or cont in this
|
||||
block, then that invalidates the poststate upheld by
|
||||
any of the stmts after it.
|
||||
Given that the typechecker has run, we know any break will be in
|
||||
a block that forms a loop body. So that's ok. There'll never be an
|
||||
expr_break outside a loop body, therefore, no expr_break outside a block.
|
||||
*/
|
||||
|
||||
/* Conservative approximation for now: This says that if a block contains
|
||||
*any* breaks or conts, then its postcondition doesn't promise anything.
|
||||
This will mean that:
|
||||
x = 0;
|
||||
break;
|
||||
|
||||
won't have a postcondition that says x is initialized, but that's ok.
|
||||
*/
|
||||
auto nv = num_locals(fcx.enclosing);
|
||||
|
||||
fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
|
||||
find_pre_post_stmt(fcx, *s);
|
||||
log("pre_post for stmt:");
|
||||
log_stmt(*s);
|
||||
log("is:");
|
||||
log_pp(stmt_pp(*s));
|
||||
}
|
||||
auto do_one = bind do_one_(fcx, _);
|
||||
|
||||
_vec::map[@stmt, ()](do_one, b.node.stmts);
|
||||
fn do_inner_(fn_ctxt fcx, &@expr e) -> () {
|
||||
find_pre_post_expr(fcx, e);
|
||||
}
|
||||
auto do_inner = bind do_inner_(fcx, _);
|
||||
option::map[@expr, ()](do_inner, b.node.expr);
|
||||
|
||||
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(fcx.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 = empty_poststate(nv);
|
||||
/* conservative approximation */
|
||||
if (! has_nonlocal_exits(b)) {
|
||||
block_postcond = union_postconds(nv, postconds);
|
||||
}
|
||||
|
||||
set_pre_and_post(b.node.a, rec(precondition=block_precond,
|
||||
postcondition=block_postcond));
|
||||
}
|
||||
|
||||
fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
|
||||
find_pre_post_block(fcx, f.body);
|
||||
}
|
||||
|
||||
fn check_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
|
||||
&vec[ty_param] ty_params,
|
||||
&def_id id, &ann a) -> @item {
|
||||
log("check_item_fn:");
|
||||
log_fn(f, i, ty_params);
|
||||
|
||||
assert (ccx.fm.contains_key(id));
|
||||
auto fcx = rec(enclosing=ccx.fm.get(id),
|
||||
id=id, name=i, ccx=ccx);
|
||||
find_pre_post_fn(fcx, f);
|
||||
|
||||
ret @respan(sp, item_fn(i, f, ty_params, id, a));
|
||||
}
|
||||
|
||||
//
|
||||
// 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:
|
||||
//
|
||||
|
||||
802
src/comp/middle/tstate/states.rs
Normal file
802
src/comp/middle/tstate/states.rs
Normal file
|
|
@ -0,0 +1,802 @@
|
|||
import std::bitv;
|
||||
import std::_vec;
|
||||
import std::_vec::plus_option;
|
||||
import std::_vec::cat_options;
|
||||
import std::option;
|
||||
import std::option::get;
|
||||
import std::option::is_none;
|
||||
import std::option::none;
|
||||
import std::option::some;
|
||||
import std::option::maybe;
|
||||
|
||||
import tstate::ann::pre_and_post;
|
||||
import tstate::ann::get_post;
|
||||
import tstate::ann::postcond;
|
||||
import tstate::ann::empty_pre_post;
|
||||
import tstate::ann::empty_poststate;
|
||||
import tstate::ann::require_and_preserve;
|
||||
import tstate::ann::union;
|
||||
import tstate::ann::intersect;
|
||||
import tstate::ann::pp_clone;
|
||||
import tstate::ann::empty_prestate;
|
||||
import tstate::ann::prestate;
|
||||
import tstate::ann::poststate;
|
||||
import tstate::ann::false_postcond;
|
||||
import tstate::ann::ts_ann;
|
||||
import tstate::ann::extend_prestate;
|
||||
import tstate::ann::extend_poststate;
|
||||
import aux::var_info;
|
||||
import aux::crate_ctxt;
|
||||
import aux::fn_ctxt;
|
||||
import aux::num_locals;
|
||||
import aux::expr_pp;
|
||||
import aux::stmt_pp;
|
||||
import aux::block_pp;
|
||||
import aux::set_pre_and_post;
|
||||
import aux::expr_prestate;
|
||||
import aux::stmt_poststate;
|
||||
import aux::expr_poststate;
|
||||
import aux::block_poststate;
|
||||
import aux::fn_info;
|
||||
import aux::log_pp;
|
||||
import aux::extend_prestate_ann;
|
||||
import aux::extend_poststate_ann;
|
||||
import aux::set_prestate_ann;
|
||||
import aux::set_poststate_ann;
|
||||
import aux::pure_exp;
|
||||
import aux::log_bitv;
|
||||
import aux::stmt_to_ann;
|
||||
import aux::log_states;
|
||||
import aux::block_states;
|
||||
import aux::controlflow_expr;
|
||||
import aux::ann_to_def;
|
||||
|
||||
import bitvectors::seq_preconds;
|
||||
import bitvectors::union_postconds;
|
||||
import bitvectors::intersect_postconds;
|
||||
import bitvectors::declare_var;
|
||||
import bitvectors::bit_num;
|
||||
import bitvectors::gen_poststate;
|
||||
|
||||
import front::ast::_mod;
|
||||
import front::ast;
|
||||
import front::ast::_fn;
|
||||
import front::ast::method;
|
||||
import front::ast::ann;
|
||||
import front::ast::ty;
|
||||
import front::ast::mutability;
|
||||
import front::ast::item;
|
||||
import front::ast::obj_field;
|
||||
import front::ast::stmt;
|
||||
import front::ast::stmt_;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ann;
|
||||
import front::ast::expr;
|
||||
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::controlflow;
|
||||
import front::ast::return;
|
||||
import front::ast::noreturn;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::_obj;
|
||||
import front::ast::_mod;
|
||||
import front::ast::crate;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::item_mod;
|
||||
import front::ast::item_ty;
|
||||
import front::ast::item_tag;
|
||||
import front::ast::item_native_mod;
|
||||
import front::ast::item_obj;
|
||||
import front::ast::item_const;
|
||||
import front::ast::def_local;
|
||||
import front::ast::def_fn;
|
||||
import front::ast::ident;
|
||||
import front::ast::def_id;
|
||||
import front::ast::ann;
|
||||
import front::ast::item;
|
||||
import front::ast::item_fn;
|
||||
import front::ast::expr;
|
||||
import front::ast::elt;
|
||||
import front::ast::field;
|
||||
import front::ast::decl;
|
||||
import front::ast::decl_local;
|
||||
import front::ast::decl_item;
|
||||
import front::ast::initializer;
|
||||
import front::ast::local;
|
||||
import front::ast::arm;
|
||||
import front::ast::expr_call;
|
||||
import front::ast::expr_vec;
|
||||
import front::ast::expr_tup;
|
||||
import front::ast::expr_path;
|
||||
import front::ast::expr_field;
|
||||
import front::ast::expr_index;
|
||||
import front::ast::expr_log;
|
||||
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;
|
||||
import front::ast::expr_assert;
|
||||
import front::ast::expr_cast;
|
||||
import front::ast::expr_for;
|
||||
import front::ast::expr_for_each;
|
||||
import front::ast::stmt;
|
||||
import front::ast::stmt_decl;
|
||||
import front::ast::stmt_expr;
|
||||
import front::ast::block;
|
||||
import front::ast::block_;
|
||||
import front::ast::method;
|
||||
|
||||
import middle::fold::span;
|
||||
import middle::fold::respan;
|
||||
|
||||
import util::common::new_def_hash;
|
||||
import util::common::decl_lhs;
|
||||
import util::common::uistr;
|
||||
import util::common::log_expr;
|
||||
import util::common::log_block;
|
||||
import util::common::log_fn;
|
||||
import util::common::elt_exprs;
|
||||
import util::common::field_exprs;
|
||||
import util::common::has_nonlocal_exits;
|
||||
import util::common::log_stmt;
|
||||
import util::common::log_expr_err;
|
||||
|
||||
fn find_pre_post_state_mod(&_mod m) -> bool {
|
||||
log("implement find_pre_post_state_mod!");
|
||||
fail;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_native_mod(&native_mod m) -> bool {
|
||||
log("implement find_pre_post_state_native_mod!");
|
||||
fail;
|
||||
}
|
||||
|
||||
fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs)
|
||||
-> tup(bool, poststate) {
|
||||
auto changed = false;
|
||||
auto post = pres;
|
||||
|
||||
for (@expr e in exprs) {
|
||||
changed = find_pre_post_state_expr(fcx, post, e) || changed;
|
||||
post = expr_poststate(e);
|
||||
}
|
||||
|
||||
ret tup(changed, post);
|
||||
}
|
||||
|
||||
fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres,
|
||||
&ann a, &vec[@expr] es) -> bool {
|
||||
auto res = seq_states(fcx, pres, es);
|
||||
auto changed = res._0;
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, res._1) || changed;
|
||||
ret changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
|
||||
&@expr index, &block body, &ann a) -> bool {
|
||||
auto changed = false;
|
||||
|
||||
/* same issues as while */
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, index) || changed;
|
||||
/* in general, would need the intersection of
|
||||
(poststate of index, poststate of body) */
|
||||
changed = find_pre_post_state_block(fcx, expr_poststate(index), body)
|
||||
|| changed;
|
||||
auto res_p = intersect_postconds(vec(expr_poststate(index),
|
||||
block_poststate(body)));
|
||||
|
||||
changed = extend_poststate_ann(a, res_p) || changed;
|
||||
ret changed;
|
||||
}
|
||||
|
||||
fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a) -> bool {
|
||||
alt (ann_to_def(fcx.ccx, a_new_var)) {
|
||||
case (some[def](def_local(?d))) { ret gen_poststate(fcx, a, d); }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|
||||
auto changed = false;
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
|
||||
/*
|
||||
log_err("states:");
|
||||
log_expr_err(*e);
|
||||
log_err(ast.ann_tag(middle.ty.expr_ann(e)));
|
||||
*/
|
||||
|
||||
/* FIXME could get rid of some of the copy/paste */
|
||||
alt (e.node) {
|
||||
case (expr_vec(?elts, _, ?a)) {
|
||||
ret find_pre_post_state_exprs(fcx, pres, a, elts);
|
||||
}
|
||||
case (expr_tup(?elts, ?a)) {
|
||||
ret find_pre_post_state_exprs(fcx, pres, a, elt_exprs(elts));
|
||||
}
|
||||
case (expr_call(?operator, ?operands, ?a)) {
|
||||
/* do the prestate for the rator */
|
||||
changed = find_pre_post_state_expr(fcx, pres, operator)
|
||||
|| changed;
|
||||
/* rands go left-to-right */
|
||||
changed = find_pre_post_state_exprs(fcx,
|
||||
expr_poststate(operator), a, operands)
|
||||
|| changed;
|
||||
/* if this is a failing call, it sets the return value */
|
||||
alt (controlflow_expr(fcx.ccx, operator)) {
|
||||
case (noreturn) {
|
||||
/*
|
||||
log_err("Call that might fail! to");
|
||||
log_expr_err(*operator);
|
||||
*/
|
||||
changed = gen_poststate(fcx, a, fcx.id) || changed;
|
||||
}
|
||||
case (_) {
|
||||
/* log_err("non-failing call, to:");
|
||||
log_expr_err(*operator);
|
||||
*/
|
||||
}
|
||||
}
|
||||
ret changed;
|
||||
}
|
||||
case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, operator);
|
||||
ret(find_pre_post_state_exprs(fcx,
|
||||
expr_poststate(operator), a, operands)
|
||||
|| changed);
|
||||
}
|
||||
case (expr_bind(?operator, ?maybe_args, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, operator)
|
||||
|| changed;
|
||||
ret (find_pre_post_state_exprs(fcx,
|
||||
expr_poststate(operator), a, cat_options[@expr](maybe_args))
|
||||
|| changed);
|
||||
}
|
||||
case (expr_path(_,?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_log(_,?e,?a)) {
|
||||
/* factor out the "one exp" pattern */
|
||||
changed = find_pre_post_state_expr(fcx, pres, e);
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_chan(?e, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, e);
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(e)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_ext(_, _, _, ?expanded, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, expanded);
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(expanded))
|
||||
|| changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_put(?maybe_e, ?a)) {
|
||||
alt (maybe_e) {
|
||||
case (some[@expr](?arg)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, arg);
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(arg))
|
||||
|| changed;
|
||||
ret changed;
|
||||
}
|
||||
case (none[@expr]) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
}
|
||||
}
|
||||
case (expr_lit(?l,?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_block(?b,?a)) {
|
||||
changed = find_pre_post_state_block(fcx, pres, b)
|
||||
|| changed;
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, block_poststate(b)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_rec(?fields,?maybe_base,?a)) {
|
||||
changed = find_pre_post_state_exprs(fcx, pres, a,
|
||||
field_exprs(fields)) || changed;
|
||||
alt (maybe_base) {
|
||||
case (none[@expr]) { /* do nothing */ }
|
||||
case (some[@expr](?base)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, base)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(base))
|
||||
|| changed;
|
||||
}
|
||||
}
|
||||
ret changed;
|
||||
}
|
||||
case (expr_assign(?lhs, ?rhs, ?a)) {
|
||||
extend_prestate_ann(a, pres);
|
||||
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
// assignment to local var
|
||||
changed = pure_exp(a_lhs, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, rhs)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(rhs))
|
||||
|| changed;
|
||||
changed = gen_if_local(fcx, a_lhs, a)|| changed;
|
||||
}
|
||||
case (_) {
|
||||
// assignment to something that must already have been init'd
|
||||
changed = find_pre_post_state_expr(fcx, pres, lhs)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
expr_poststate(lhs), rhs) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(rhs))
|
||||
|| changed;
|
||||
}
|
||||
}
|
||||
ret changed;
|
||||
}
|
||||
case (expr_recv(?lhs, ?rhs, ?a)) {
|
||||
extend_prestate_ann(a, pres);
|
||||
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
// receive to local var
|
||||
changed = pure_exp(a_lhs, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, rhs)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(rhs))
|
||||
|| changed;
|
||||
changed = gen_if_local(fcx, a_lhs, a) || changed;
|
||||
}
|
||||
case (_) {
|
||||
// receive to something that must already have been init'd
|
||||
changed = find_pre_post_state_expr(fcx, pres, lhs)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
expr_poststate(lhs), rhs) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(rhs))
|
||||
|| changed;
|
||||
}
|
||||
}
|
||||
ret changed;
|
||||
}
|
||||
|
||||
case (expr_ret(?maybe_ret_val, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
set_poststate_ann(a, false_postcond(num_local_vars));
|
||||
alt(maybe_ret_val) {
|
||||
case (none[@expr]) { /* do nothing */ }
|
||||
case (some[@expr](?ret_val)) {
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
pres, ret_val) || changed;
|
||||
}
|
||||
}
|
||||
ret changed;
|
||||
}
|
||||
case (expr_be(?e, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
set_poststate_ann(a, false_postcond(num_local_vars));
|
||||
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, antec)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_block(fcx,
|
||||
expr_poststate(antec), conseq) || changed;
|
||||
alt (maybe_alt) {
|
||||
case (none[@expr]) {
|
||||
changed = extend_poststate_ann(a, expr_poststate(antec))
|
||||
|| changed;
|
||||
}
|
||||
case (some[@expr](?altern)) {
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
expr_poststate(antec), altern) || changed;
|
||||
auto poststate_res = intersect_postconds
|
||||
(vec(block_poststate(conseq), expr_poststate(altern)));
|
||||
changed = extend_poststate_ann(a, poststate_res) || changed;
|
||||
}
|
||||
}
|
||||
log("if:");
|
||||
log_expr(*e);
|
||||
log("new prestate:");
|
||||
log_bitv(fcx.enclosing, pres);
|
||||
log("new poststate:");
|
||||
log_bitv(fcx.enclosing, expr_poststate(e));
|
||||
|
||||
ret changed;
|
||||
}
|
||||
case (expr_binary(?bop, ?l, ?r, ?a)) {
|
||||
/* FIXME: what if bop is lazy? */
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, l)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_send(?l, ?r, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, l)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx, expr_poststate(l), r)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_assign_op(?op, ?lhs, ?rhs, ?a)) {
|
||||
/* quite similar to binary -- should abstract this */
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, lhs)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx, expr_poststate(lhs), rhs)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(rhs)) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_while(?test, ?body, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
/* to handle general predicates, we need to pass in
|
||||
pres `intersect` (poststate(a))
|
||||
like: auto test_pres = intersect_postconds(pres, expr_postcond(a));
|
||||
However, this doesn't work right now because we would be passing
|
||||
in an all-zero prestate initially
|
||||
FIXME
|
||||
maybe need a "don't know" state in addition to 0 or 1?
|
||||
*/
|
||||
changed = find_pre_post_state_expr(fcx, pres, test)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_block(fcx, expr_poststate(test), body)
|
||||
|| changed;
|
||||
changed = extend_poststate_ann(a,
|
||||
intersect_postconds(vec(expr_poststate(test),
|
||||
block_poststate(body)))) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_do_while(?body, ?test, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_block(fcx, pres, body)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
block_poststate(body), test) || changed;
|
||||
|
||||
/* conservative approximination: if the body of the loop
|
||||
could break or cont, we revert to the prestate
|
||||
(TODO: could treat cont differently from break, since
|
||||
if there's a cont, the test will execute) */
|
||||
if (has_nonlocal_exits(body)) {
|
||||
changed = set_poststate_ann(a, pres) || changed;
|
||||
}
|
||||
else {
|
||||
changed = extend_poststate_ann(a, expr_poststate(test))
|
||||
|| changed;
|
||||
}
|
||||
|
||||
ret changed;
|
||||
}
|
||||
case (expr_for(?d, ?index, ?body, ?a)) {
|
||||
ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
|
||||
}
|
||||
case (expr_for_each(?d, ?index, ?body, ?a)) {
|
||||
ret find_pre_post_state_loop(fcx, pres, d, index, body, a);
|
||||
}
|
||||
case (expr_index(?e, ?sub, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
||||
changed = find_pre_post_state_expr(fcx,
|
||||
expr_poststate(e), sub) || changed;
|
||||
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(fcx, pres, e) || changed;
|
||||
auto e_post = expr_poststate(e);
|
||||
auto a_post;
|
||||
if (_vec::len[arm](alts) > 0u) {
|
||||
a_post = false_postcond(num_local_vars);
|
||||
for (arm an_alt in alts) {
|
||||
changed = find_pre_post_state_block(fcx, e_post,
|
||||
an_alt.block) || changed;
|
||||
changed = intersect(a_post, block_poststate(an_alt.block))
|
||||
|| changed;
|
||||
}
|
||||
}
|
||||
else {
|
||||
// No alts; poststate is the poststate of the test
|
||||
a_post = e_post;
|
||||
}
|
||||
changed = extend_poststate_ann(a, a_post);
|
||||
ret changed;
|
||||
}
|
||||
case (expr_field(?e, _, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, 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(fcx, pres, operand)
|
||||
|| changed;
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = extend_poststate_ann(a, expr_poststate(operand))
|
||||
|| changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_cast(?operand, _, ?a)) {
|
||||
changed = find_pre_post_state_expr(fcx, 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;
|
||||
/* if execution continues after fail, then everything is true! woo! */
|
||||
changed = set_poststate_ann(a, false_postcond(num_local_vars))
|
||||
|| changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_assert(?p, ?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_check(?p, ?a)) {
|
||||
changed = extend_prestate_ann(a, pres) || changed;
|
||||
changed = find_pre_post_state_expr(fcx, pres, p) || changed;
|
||||
/* FIXME: update the postcondition to reflect that p holds */
|
||||
changed = extend_poststate_ann(a, pres) || changed;
|
||||
ret changed;
|
||||
}
|
||||
case (expr_break(?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_cont(?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_port(?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
case (expr_self_method(_, ?a)) {
|
||||
ret pure_exp(a, pres);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
|
||||
auto changed = false;
|
||||
auto stmt_ann_ = stmt_to_ann(*s);
|
||||
assert (!is_none[@ts_ann](stmt_ann_));
|
||||
auto stmt_ann = *(get[@ts_ann](stmt_ann_));
|
||||
log("*At beginning: stmt = ");
|
||||
log_stmt(*s);
|
||||
log("*prestate = ");
|
||||
log(bitv::to_str(stmt_ann.states.prestate));
|
||||
log("*poststate =");
|
||||
log(bitv::to_str(stmt_ann.states.poststate));
|
||||
log("*changed =");
|
||||
log(changed);
|
||||
|
||||
alt (s.node) {
|
||||
case (stmt_decl(?adecl, ?a)) {
|
||||
alt (adecl.node) {
|
||||
case (decl_local(?alocal)) {
|
||||
alt (alocal.init) {
|
||||
case (some[initializer](?an_init)) {
|
||||
changed = extend_prestate(stmt_ann.states.prestate, pres)
|
||||
|| changed;
|
||||
changed = find_pre_post_state_expr
|
||||
(fcx, pres, an_init.expr) || changed;
|
||||
changed = extend_poststate(stmt_ann.states.poststate,
|
||||
expr_poststate(an_init.expr))
|
||||
|| changed;
|
||||
changed = gen_poststate(fcx, a, alocal.id)
|
||||
|| changed;
|
||||
log("Summary: stmt = ");
|
||||
log_stmt(*s);
|
||||
log("prestate = ");
|
||||
log(bitv::to_str(stmt_ann.states.prestate));
|
||||
log_bitv(fcx.enclosing, stmt_ann.states.prestate);
|
||||
log("poststate =");
|
||||
log_bitv(fcx.enclosing, stmt_ann.states.poststate);
|
||||
log("changed =");
|
||||
log(changed);
|
||||
|
||||
ret changed;
|
||||
}
|
||||
case (none[initializer]) {
|
||||
changed = extend_prestate(stmt_ann.states.prestate, pres)
|
||||
|| changed;
|
||||
changed = extend_poststate(stmt_ann.states.poststate, pres)
|
||||
|| changed;
|
||||
ret changed;
|
||||
}
|
||||
}
|
||||
}
|
||||
case (decl_item(?an_item)) {
|
||||
changed = extend_prestate(stmt_ann.states.prestate, pres)
|
||||
|| changed;
|
||||
changed = extend_poststate(stmt_ann.states.poststate, pres)
|
||||
|| changed;
|
||||
ret (find_pre_post_state_item(fcx, an_item) || changed);
|
||||
}
|
||||
}
|
||||
}
|
||||
case (stmt_expr(?e, _)) {
|
||||
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
|
||||
changed = extend_prestate(stmt_ann.states.prestate, expr_prestate(e))
|
||||
|| changed;
|
||||
changed = extend_poststate(stmt_ann.states.poststate,
|
||||
expr_poststate(e)) || changed;
|
||||
/*
|
||||
log("Summary: stmt = ");
|
||||
log_stmt(*s);
|
||||
log("prestate = ");
|
||||
log(bitv::to_str(stmt_ann.states.prestate));
|
||||
log_bitv(enclosing, stmt_ann.states.prestate);
|
||||
log("poststate =");
|
||||
log(bitv::to_str(stmt_ann.states.poststate));
|
||||
log_bitv(enclosing, stmt_ann.states.poststate);
|
||||
log("changed =");
|
||||
log(changed);
|
||||
*/
|
||||
ret changed;
|
||||
}
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
|
||||
/* 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_ctxt fcx, &prestate pres0, &block b)
|
||||
-> bool {
|
||||
|
||||
auto changed = false;
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
|
||||
/* First, set the pre-states and post-states for every expression */
|
||||
auto pres = pres0;
|
||||
|
||||
/* Iterate over each stmt. The new prestate is <pres>. The poststate
|
||||
consist of improving <pres> with whatever variables this stmt initializes.
|
||||
Then <pres> becomes the new poststate. */
|
||||
for (@stmt s in b.node.stmts) {
|
||||
changed = find_pre_post_state_stmt(fcx, pres, s) || changed;
|
||||
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(fcx, pres, e) || changed;
|
||||
post = expr_poststate(e);
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
log_err("block:");
|
||||
log_block_err(b);
|
||||
log_err("has non-local exits?");
|
||||
log_err(has_nonlocal_exits(b));
|
||||
*/
|
||||
|
||||
/* conservative approximation: if a block contains a break
|
||||
or cont, we assume nothing about the poststate */
|
||||
if (has_nonlocal_exits(b)) {
|
||||
post = pres0;
|
||||
}
|
||||
|
||||
set_prestate_ann(b.node.a, pres0);
|
||||
set_poststate_ann(b.node.a, post);
|
||||
|
||||
log("For block:");
|
||||
log_block(b);
|
||||
log("poststate = ");
|
||||
log_states(block_states(b));
|
||||
log("pres0:");
|
||||
log_bitv(fcx.enclosing, pres0);
|
||||
log("post:");
|
||||
log_bitv(fcx.enclosing, post);
|
||||
|
||||
ret changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool {
|
||||
/* FIXME: where do we set args as being initialized?
|
||||
What about for methods? */
|
||||
auto num_local_vars = num_locals(fcx.enclosing);
|
||||
ret find_pre_post_state_block(fcx,
|
||||
empty_prestate(num_local_vars), f.body);
|
||||
}
|
||||
|
||||
fn find_pre_post_state_obj(crate_ctxt ccx, _obj o) -> bool {
|
||||
fn do_a_method(crate_ctxt ccx, &@method m) -> bool {
|
||||
assert (ccx.fm.contains_key(m.node.id));
|
||||
ret find_pre_post_state_fn(rec(enclosing=ccx.fm.get(m.node.id),
|
||||
id=m.node.id,
|
||||
name=m.node.ident,
|
||||
ccx=ccx),
|
||||
m.node.meth);
|
||||
}
|
||||
auto f = bind do_a_method(ccx,_);
|
||||
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_state_item(&fn_ctxt fcx, @item i) -> bool {
|
||||
alt (i.node) {
|
||||
case (item_const(?id, ?t, ?e, ?di, ?a)) {
|
||||
ret find_pre_post_state_expr(fcx,
|
||||
empty_prestate(num_locals(fcx.enclosing)), e);
|
||||
}
|
||||
case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
|
||||
assert (fcx.ccx.fm.contains_key(di));
|
||||
ret find_pre_post_state_fn(rec(enclosing=fcx.ccx.fm.get(di),
|
||||
id=di, name=id with fcx), f);
|
||||
}
|
||||
case (item_mod(?id, ?m, ?di)) {
|
||||
ret find_pre_post_state_mod(m);
|
||||
}
|
||||
case (item_native_mod(?id, ?nm, ?di)) {
|
||||
ret find_pre_post_state_native_mod(nm);
|
||||
}
|
||||
case (item_ty(_,_,_,_,_)) {
|
||||
ret false;
|
||||
}
|
||||
case (item_tag(_,_,_,_,_)) {
|
||||
ret false;
|
||||
}
|
||||
case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
|
||||
ret find_pre_post_state_obj(fcx.ccx, o);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -31,7 +31,7 @@ import util::common::ty_f64;
|
|||
|
||||
import util::common::new_def_hash;
|
||||
import util::common::span;
|
||||
import util::typestate_ann::ts_ann;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
|
||||
import util::interner;
|
||||
|
||||
|
|
@ -86,6 +86,7 @@ type t = uint;
|
|||
// AST structure in front/ast::rs as well.
|
||||
tag sty {
|
||||
ty_nil;
|
||||
ty_bot;
|
||||
ty_bool;
|
||||
ty_int;
|
||||
ty_float;
|
||||
|
|
@ -159,7 +160,8 @@ const uint idx_str = 16u;
|
|||
const uint idx_task = 17u;
|
||||
const uint idx_native = 18u;
|
||||
const uint idx_type = 19u;
|
||||
const uint idx_first_others = 20u;
|
||||
const uint idx_bot = 20u;
|
||||
const uint idx_first_others = 21u;
|
||||
|
||||
type type_store = interner::interner[raw_t];
|
||||
|
||||
|
|
@ -190,6 +192,7 @@ fn mk_type_store() -> @type_store {
|
|||
intern(ts, ty_task, none[str]);
|
||||
intern(ts, ty_native, none[str]);
|
||||
intern(ts, ty_type, none[str]);
|
||||
intern(ts, ty_bot, none[str]);
|
||||
|
||||
assert _vec::len(ts.vect) == idx_first_others;
|
||||
|
||||
|
|
@ -368,6 +371,7 @@ fn gen_ty(&ctxt cx, &sty st) -> t {
|
|||
}
|
||||
|
||||
fn mk_nil(&ctxt cx) -> t { ret idx_nil; }
|
||||
fn mk_bot(&ctxt cx) -> t { ret idx_bot; }
|
||||
fn mk_bool(&ctxt cx) -> t { ret idx_bool; }
|
||||
fn mk_int(&ctxt cx) -> t { ret idx_int; }
|
||||
fn mk_float(&ctxt cx) -> t { ret idx_float; }
|
||||
|
|
@ -564,6 +568,7 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
|
|||
alt (struct(cx, typ)) {
|
||||
case (ty_native) { s += "native"; }
|
||||
case (ty_nil) { s += "()"; }
|
||||
case (ty_bot) { s += "_|_"; }
|
||||
case (ty_bool) { s += "bool"; }
|
||||
case (ty_int) { s += "int"; }
|
||||
case (ty_float) { s += "float"; }
|
||||
|
|
@ -576,6 +581,7 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
|
|||
case (ty_port(?t)) { s += "port[" + ty_to_str(cx, t) + "]"; }
|
||||
case (ty_chan(?t)) { s += "chan[" + ty_to_str(cx, t) + "]"; }
|
||||
case (ty_type) { s += "type"; }
|
||||
case (ty_task) { s += "task"; }
|
||||
|
||||
case (ty_tup(?elems)) {
|
||||
auto f = bind mt_to_str(cx, _);
|
||||
|
|
@ -632,6 +638,11 @@ fn ty_to_str(ctxt cx, &t typ) -> str {
|
|||
s += "''" + _str::unsafe_from_bytes(vec(('a' as u8) +
|
||||
(id as u8)));
|
||||
}
|
||||
|
||||
case (_) {
|
||||
s += ty_to_short_str(cx, typ);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
ret s;
|
||||
|
|
@ -652,6 +663,7 @@ type ty_walk = fn(t);
|
|||
fn walk_ty(ctxt cx, ty_walk walker, t ty) {
|
||||
alt (struct(cx, ty)) {
|
||||
case (ty_nil) { /* no-op */ }
|
||||
case (ty_bot) { /* no-op */ }
|
||||
case (ty_bool) { /* no-op */ }
|
||||
case (ty_int) { /* no-op */ }
|
||||
case (ty_uint) { /* no-op */ }
|
||||
|
|
@ -716,6 +728,7 @@ fn fold_ty(ctxt cx, ty_fold fld, t ty_0) -> t {
|
|||
auto ty = ty_0;
|
||||
alt (struct(cx, ty)) {
|
||||
case (ty_nil) { /* no-op */ }
|
||||
case (ty_bot) { /* no-op */ }
|
||||
case (ty_bool) { /* no-op */ }
|
||||
case (ty_int) { /* no-op */ }
|
||||
case (ty_uint) { /* no-op */ }
|
||||
|
|
@ -821,7 +834,13 @@ fn type_is_nil(&ctxt cx, &t ty) -> bool {
|
|||
case (ty_nil) { ret true; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
fail;
|
||||
}
|
||||
|
||||
fn type_is_bot(&ctxt cx, &t ty) -> bool {
|
||||
alt (struct(cx, ty)) {
|
||||
case (ty_bot) { ret true; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
|
||||
fn type_is_bool(&ctxt cx, &t ty) -> bool {
|
||||
|
|
@ -1130,6 +1149,7 @@ fn hash_type_structure(&sty st) -> uint {
|
|||
case (ty_bound_param(?pid)) { ret hash_uint(31u, pid); }
|
||||
case (ty_type) { ret 32u; }
|
||||
case (ty_native) { ret 33u; }
|
||||
case (ty_bot) { ret 34u; }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1182,6 +1202,12 @@ fn equal_type_structures(&sty a, &sty b) -> bool {
|
|||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ty_bot) {
|
||||
alt(b) {
|
||||
case (ty_bot) { ret true; }
|
||||
case (_) { ret false; }
|
||||
}
|
||||
}
|
||||
case (ty_bool) {
|
||||
alt (b) {
|
||||
case (ty_bool) { ret true; }
|
||||
|
|
@ -1476,7 +1502,12 @@ fn triv_ann(uint node_id, t typ) -> ast::ann {
|
|||
|
||||
// Creates a nil type annotation.
|
||||
fn plain_ann(uint node_id, ctxt tcx) -> ast::ann {
|
||||
ret ast::ann_type(node_id, mk_nil(tcx), none[vec[ty::t]], none[@ts_ann]);
|
||||
ret ast::ann_type(node_id, mk_nil(tcx), none[vec[t]], none[@ts_ann]);
|
||||
}
|
||||
|
||||
// Creates a _|_ type annotation.
|
||||
fn bot_ann(uint node_id, ctxt tcx) -> ast::ann {
|
||||
ret ast::ann_type(node_id, mk_bot(tcx), none[vec[t]], none[@ts_ann]);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2099,6 +2130,7 @@ mod unify {
|
|||
|
||||
alt (struct(cx.tcx, expected)) {
|
||||
case (ty::ty_nil) { ret struct_cmp(cx, expected, actual); }
|
||||
case (ty::ty_bot) { ret struct_cmp(cx, expected, actual); }
|
||||
case (ty::ty_bool) { ret struct_cmp(cx, expected, actual); }
|
||||
case (ty::ty_int) { ret struct_cmp(cx, expected, actual); }
|
||||
case (ty::ty_uint) { ret struct_cmp(cx, expected, actual); }
|
||||
|
|
@ -2675,6 +2707,20 @@ fn lookup_item_type(session::session sess,
|
|||
}
|
||||
}
|
||||
|
||||
fn ret_ty_of_fn_ty(ty_ctxt tcx, t a_ty) -> t {
|
||||
alt (ty::struct(tcx, a_ty)) {
|
||||
case (ty::ty_fn(_, _, ?ret_ty)) {
|
||||
ret ret_ty;
|
||||
}
|
||||
case (_) {
|
||||
fail;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn ret_ty_of_fn(node_type_table ntt, ty_ctxt tcx, ast::ann ann) -> t {
|
||||
ret ret_ty_of_fn_ty(tcx, ann_to_type(ntt, ann));
|
||||
}
|
||||
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
|
|
|
|||
|
|
@ -25,6 +25,7 @@ import middle::ty::node_type_table;
|
|||
import middle::ty::pat_ty;
|
||||
import middle::ty::path_to_str;
|
||||
import middle::ty::plain_ann;
|
||||
import middle::ty::bot_ann;
|
||||
import middle::ty::struct;
|
||||
import middle::ty::triv_ann;
|
||||
import middle::ty::ty_param_substs_opt_and_ty;
|
||||
|
|
@ -46,7 +47,7 @@ import std::option::none;
|
|||
import std::option::some;
|
||||
import std::option::from_maybe;
|
||||
|
||||
import util::typestate_ann::ts_ann;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
|
||||
type ty_table = hashmap[ast::def_id, ty::t];
|
||||
|
||||
|
|
@ -271,6 +272,7 @@ fn ast_ty_to_ty(&ty::ctxt tcx, &ty_getter getter, &@ast::ty ast_ty) -> ty::t {
|
|||
auto cname = none[str];
|
||||
alt (ast_ty.node) {
|
||||
case (ast::ty_nil) { typ = ty::mk_nil(tcx); }
|
||||
case (ast::ty_bot) { typ = ty::mk_bot(tcx); }
|
||||
case (ast::ty_bool) { typ = ty::mk_bool(tcx); }
|
||||
case (ast::ty_int) { typ = ty::mk_int(tcx); }
|
||||
case (ast::ty_uint) { typ = ty::mk_uint(tcx); }
|
||||
|
|
@ -1060,6 +1062,7 @@ fn variant_arg_types(&@crate_ctxt ccx, &span sp, &ast::def_id vid,
|
|||
}
|
||||
}
|
||||
|
||||
/* result is a vector of the *expected* types of all the fields */
|
||||
ret result;
|
||||
}
|
||||
|
||||
|
|
@ -1120,11 +1123,29 @@ mod Pushdown {
|
|||
}
|
||||
|
||||
// Get the types of the arguments of the variant.
|
||||
|
||||
let vec[ty::t] tparams = vec();
|
||||
auto j = 0u;
|
||||
auto actual_ty_params =
|
||||
ty::ann_to_type_params(fcx.ccx.node_types, ann);
|
||||
|
||||
for (ty::t some_ty in tag_tps) {
|
||||
let ty::t t1 = some_ty;
|
||||
let ty::t t2 = actual_ty_params.(j);
|
||||
|
||||
let ty::t res = Demand::simple(fcx,
|
||||
pat.span,
|
||||
t1, t2);
|
||||
|
||||
_vec::push(tparams, res);
|
||||
j += 1u;
|
||||
}
|
||||
|
||||
auto arg_tys;
|
||||
alt (fcx.ccx.tcx.def_map.get(ast::ann_tag(ann))) {
|
||||
case (ast::def_variant(_, ?vdefid)) {
|
||||
arg_tys = variant_arg_types(fcx.ccx, pat.span, vdefid,
|
||||
tag_tps);
|
||||
tparams);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1134,10 +1155,22 @@ mod Pushdown {
|
|||
i += 1u;
|
||||
}
|
||||
|
||||
auto tps = ty::ann_to_type_params(fcx.ccx.node_types, ann);
|
||||
auto tt = ann_to_type(fcx.ccx.node_types, ann);
|
||||
|
||||
let ty_param_substs_and_ty res_t = Demand::full(fcx, pat.span,
|
||||
expected, tt, tps, NO_AUTODEREF);
|
||||
|
||||
auto a_1 = ast::ann_type(ast::ann_tag(ann),
|
||||
res_t._1,
|
||||
some[vec[ty::t]](res_t._0),
|
||||
none[@ts_ann]);
|
||||
|
||||
// TODO: push down type from "expected".
|
||||
write_type(fcx.ccx.node_types, ast::ann_tag(ann),
|
||||
write_type(fcx.ccx.node_types, ast::ann_tag(a_1),
|
||||
ty::ann_to_ty_param_substs_opt_and_ty(fcx.ccx.node_types,
|
||||
ann));
|
||||
a_1));
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1843,8 +1876,12 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
case (ty::ty_native_fn(?abi, _, _)) {
|
||||
t_0 = ty::mk_native_fn(fcx.ccx.tcx, abi, arg_tys_0, rt_0);
|
||||
}
|
||||
case (_) {
|
||||
log_err "check_call_or_bind(): fn expr doesn't have fn type";
|
||||
case (?u) {
|
||||
fcx.ccx.sess.span_err(f.span,
|
||||
"check_call_or_bind(): fn expr doesn't have fn type,"
|
||||
+ " instead having: " +
|
||||
ty_to_str(fcx.ccx.tcx, expr_ty(fcx.ccx.tcx,
|
||||
fcx.ccx.node_types, f_0)));
|
||||
fail;
|
||||
}
|
||||
}
|
||||
|
|
@ -2015,15 +2052,13 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
}
|
||||
|
||||
case (ast::expr_fail(?a)) {
|
||||
// TODO: should be something like 'a or noret
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
|
||||
ret @fold::respan[ast::expr_](expr.span, ast::expr_fail(new_ann));
|
||||
}
|
||||
|
||||
case (ast::expr_break(?a)) {
|
||||
// TODO: should be something like 'a or noret
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
|
||||
ret @fold::respan[ast::expr_](expr.span,
|
||||
ast::expr_break(new_ann));
|
||||
|
|
@ -2031,13 +2066,12 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
|
||||
case (ast::expr_cont(?a)) {
|
||||
// TODO: should be something like 'a or noret
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
|
||||
ret @fold::respan[ast::expr_](expr.span, ast::expr_cont(new_ann));
|
||||
}
|
||||
|
||||
case (ast::expr_ret(?expr_opt, ?a)) {
|
||||
// TODO: should be something like 'a or noret
|
||||
alt (expr_opt) {
|
||||
case (none[@ast::expr]) {
|
||||
auto nil = ty::mk_nil(fcx.ccx.tcx);
|
||||
|
|
@ -2046,7 +2080,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
+ "returning non-nil");
|
||||
}
|
||||
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types,
|
||||
ast::ann_tag(a));
|
||||
|
||||
|
|
@ -2060,7 +2094,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
auto expr_1 = Pushdown::pushdown_expr(fcx, fcx.ret_ty,
|
||||
expr_0);
|
||||
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types,
|
||||
ast::ann_tag(a));
|
||||
|
||||
|
|
@ -2109,8 +2143,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) -> @ast::expr {
|
|||
assert (ast::is_call_expr(e));
|
||||
auto expr_0 = check_expr(fcx, e);
|
||||
auto expr_1 = Pushdown::pushdown_expr(fcx, fcx.ret_ty, expr_0);
|
||||
|
||||
auto new_ann = plain_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
auto new_ann = bot_ann(ast::ann_tag(a), fcx.ccx.tcx);
|
||||
write_nil_type(fcx.ccx.tcx, fcx.ccx.node_types, ast::ann_tag(a));
|
||||
|
||||
ret @fold::respan(expr.span, ast::expr_be(expr_1, new_ann));
|
||||
|
|
|
|||
|
|
@ -135,6 +135,7 @@ fn walk_ty(&ast_visitor v, @ast::ty t) {
|
|||
v.visit_ty_pre(t);
|
||||
alt (t.node) {
|
||||
case (ast::ty_nil) {}
|
||||
case (ast::ty_bot) {}
|
||||
case (ast::ty_bool) {}
|
||||
case (ast::ty_int) {}
|
||||
case (ast::ty_uint) {}
|
||||
|
|
|
|||
|
|
@ -18,9 +18,21 @@ mod middle {
|
|||
mod metadata;
|
||||
mod resolve;
|
||||
mod typeck;
|
||||
mod typestate_check;
|
||||
|
||||
mod tstate {
|
||||
mod ck;
|
||||
mod annotate;
|
||||
mod aux;
|
||||
mod bitvectors;
|
||||
mod collect_locals;
|
||||
mod pre_post_conditions;
|
||||
mod states;
|
||||
mod ann;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
|
||||
mod pretty {
|
||||
mod pprust;
|
||||
mod pp;
|
||||
|
|
@ -53,7 +65,6 @@ mod driver {
|
|||
mod util {
|
||||
mod common;
|
||||
mod interner;
|
||||
mod typestate_ann;
|
||||
}
|
||||
|
||||
auth front::creader::load_crate = unsafe;
|
||||
|
|
|
|||
|
|
@ -5,7 +5,9 @@ import std::_int;
|
|||
import std::_vec;
|
||||
import std::option::none;
|
||||
import front::ast;
|
||||
import util::typestate_ann::ts_ann;
|
||||
import front::ast::ty;
|
||||
import front::ast::pat;
|
||||
import middle::tstate::ann::ts_ann;
|
||||
|
||||
import middle::fold;
|
||||
import middle::fold::respan;
|
||||
|
|
@ -17,6 +19,7 @@ import pretty::pprust::print_block;
|
|||
import pretty::pprust::print_expr;
|
||||
import pretty::pprust::print_decl;
|
||||
import pretty::pprust::print_fn;
|
||||
import pretty::pprust::print_type;
|
||||
import pretty::pp::mkstate;
|
||||
|
||||
type filename = str;
|
||||
|
|
@ -127,6 +130,16 @@ fn expr_to_str(&@ast::expr e) -> str {
|
|||
ret s.get_str();
|
||||
}
|
||||
|
||||
fn ty_to_str(&ty t) -> str {
|
||||
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);
|
||||
print_type(out, @t);
|
||||
ret s.get_str();
|
||||
}
|
||||
|
||||
fn log_expr(&ast::expr e) -> () {
|
||||
log(expr_to_str(@e));
|
||||
}
|
||||
|
|
@ -135,6 +148,14 @@ fn log_expr_err(&ast::expr e) -> () {
|
|||
log_err(expr_to_str(@e));
|
||||
}
|
||||
|
||||
fn log_ty_err(&ty t) -> () {
|
||||
log_err(ty_to_str(t));
|
||||
}
|
||||
|
||||
fn log_pat_err(&@pat p) -> () {
|
||||
log_err(pretty::pprust::pat_to_str(p));
|
||||
}
|
||||
|
||||
fn block_to_str(&ast::block b) -> str {
|
||||
let str_writer s = string_writer();
|
||||
auto out_ = mkstate(s.get_writer(), 80u);
|
||||
|
|
@ -269,6 +290,7 @@ fn has_nonlocal_exits(&ast::block b) -> bool {
|
|||
|
||||
ret (has_exits.size() > 0u);
|
||||
}
|
||||
|
||||
//
|
||||
// Local Variables:
|
||||
// mode: rust
|
||||
|
|
|
|||
21
src/test/compile-fail/forgot-ret.rs
Normal file
21
src/test/compile-fail/forgot-ret.rs
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
// xfail-stage0
|
||||
// xfail-stage1
|
||||
// xfail-stage2
|
||||
// xfail-stage3
|
||||
// -*- rust -*-
|
||||
|
||||
// error-pattern: may not return
|
||||
|
||||
fn god_exists(int a) -> bool {
|
||||
be god_exists(a);
|
||||
}
|
||||
|
||||
fn f(int a) -> int {
|
||||
if (god_exists(a)) {
|
||||
ret 5;
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
f(12);
|
||||
}
|
||||
25
src/test/run-pass/box-inside-if.rs
Normal file
25
src/test/run-pass/box-inside-if.rs
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
// -*- rust -*-
|
||||
// xfail-stage0
|
||||
use std;
|
||||
import std::_vec;
|
||||
|
||||
fn some_vec(int x) -> vec[int] {
|
||||
ret vec();
|
||||
}
|
||||
|
||||
fn is_odd(int n) -> bool { ret true; }
|
||||
|
||||
fn length_is_even(vec[int] vs) -> bool {
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn foo(int acc, int n) -> () {
|
||||
|
||||
if (is_odd(n) && length_is_even(some_vec(1))) {
|
||||
log_err("bloop");
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
foo(67, 5);
|
||||
}
|
||||
25
src/test/run-pass/box-inside-if2.rs
Normal file
25
src/test/run-pass/box-inside-if2.rs
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
// -*- rust -*-
|
||||
// xfail-stage0
|
||||
use std;
|
||||
import std::_vec;
|
||||
|
||||
fn some_vec(int x) -> vec[int] {
|
||||
ret vec();
|
||||
}
|
||||
|
||||
fn is_odd(int n) -> bool { ret true; }
|
||||
|
||||
fn length_is_even(vec[int] vs) -> bool {
|
||||
ret true;
|
||||
}
|
||||
|
||||
fn foo(int acc, int n) -> () {
|
||||
|
||||
if (is_odd(n) || length_is_even(some_vec(1))) {
|
||||
log_err("bloop");
|
||||
}
|
||||
}
|
||||
|
||||
fn main() {
|
||||
foo(67, 5);
|
||||
}
|
||||
Loading…
Reference in a new issue