user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of github.com:graydon/rust

Browse source
This commit is contained in:
Patrick Walton 2011-04-07 10:14:25 -07:00
commit 2a894cabc2
17 changed files with 462 additions and 156 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/comp/middle/fold.rs
View file

@ -7,6 +7,7 @@ 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 front.ast;
import front.ast.fn_decl;
@ -232,10 +233,12 @@ type ast_fold[ENV] =
// Stmt folds.
(fn(&ENV e, &span sp,
@decl decl) -> @stmt) fold_stmt_decl,
@decl decl, option.t[@ts_ann] a)
-> @stmt) fold_stmt_decl,
(fn(&ENV e, &span sp,
@expr e) -> @stmt) fold_stmt_expr,
@expr e, option.t[@ts_ann] a)
-> @stmt) fold_stmt_expr,
// Item folds.
(fn(&ENV e, &span sp, ident ident,
@ -788,14 +791,14 @@ fn fold_stmt[ENV](&ENV env, ast_fold[ENV] fld, &@stmt s) -> @stmt {
}
alt (s.node) {
case (ast.stmt_decl(?d)) {
case (ast.stmt_decl(?d, ?a)) {
auto dd = fold_decl(env_, fld, d);
ret fld.fold_stmt_decl(env_, s.span, dd);
ret fld.fold_stmt_decl(env_, s.span, dd, a);
}
case (ast.stmt_expr(?e)) {
case (ast.stmt_expr(?e, ?a)) {
auto ee = fold_expr(env_, fld, e);
ret fld.fold_stmt_expr(env_, s.span, ee);
ret fld.fold_stmt_expr(env_, s.span, ee, a);
}
}
fail;
@ -1386,12 +1389,14 @@ fn identity_fold_pat_tag[ENV](&ENV e, &span sp, path p, vec[@pat] args,
// Stmt identities.
fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d) -> @stmt {
ret @respan(sp, ast.stmt_decl(d));
fn identity_fold_stmt_decl[ENV](&ENV env, &span sp, @decl d,
option.t[@ts_ann] a) -> @stmt {
ret @respan(sp, ast.stmt_decl(d, a));
}
fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x) -> @stmt {
ret @respan(sp, ast.stmt_expr(x));
fn identity_fold_stmt_expr[ENV](&ENV e, &span sp, @expr x,
option.t[@ts_ann] a) -> @stmt {
ret @respan(sp, ast.stmt_expr(x, a));
}
@ -1642,8 +1647,8 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
fold_pat_bind = bind identity_fold_pat_bind[ENV](_,_,_,_,_),
fold_pat_tag = bind identity_fold_pat_tag[ENV](_,_,_,_,_,_),
fold_stmt_decl = bind identity_fold_stmt_decl[ENV](_,_,_),
fold_stmt_expr = bind identity_fold_stmt_expr[ENV](_,_,_),
fold_stmt_decl = bind identity_fold_stmt_decl[ENV](_,_,_,_),
fold_stmt_expr = bind identity_fold_stmt_expr[ENV](_,_,_,_),
fold_item_const= bind identity_fold_item_const[ENV](_,_,_,_,_,_,_),
fold_item_fn = bind identity_fold_item_fn[ENV](_,_,_,_,_,_,_),

3
src/comp/middle/resolve.rs
View file

@ -6,6 +6,7 @@ import front.creader;
import driver.session;
import util.common.new_def_hash;
import util.common.span;
import util.typestate_ann.ts_ann;
import std.map.hashmap;
import std.list.list;
import std.list.nil;
@ -348,7 +349,7 @@ fn lookup_name_wrapped(&env e, ast.ident i, namespace ns)
fn found_decl_stmt(@ast.stmt s, namespace ns) -> def_wrap {
alt (s.node) {
case (ast.stmt_decl(?d)) {
case (ast.stmt_decl(?d,_)) {
alt (d.node) {
case (ast.decl_local(?loc)) {
auto t = ast.def_local(loc.id);

77
src/comp/middle/trans.rs
View file

@ -5208,11 +5208,11 @@ fn init_local(@block_ctxt cx, @ast.local local) -> result {
fn trans_stmt(@block_ctxt cx, &ast.stmt s) -> result {
auto bcx = cx;
alt (s.node) {
case (ast.stmt_expr(?e)) {
case (ast.stmt_expr(?e,_)) {
bcx = trans_expr(cx, e).bcx;
}
case (ast.stmt_decl(?d)) {
case (ast.stmt_decl(?d,_)) {
alt (d.node) {
case (ast.decl_local(?local)) {
bcx = init_local(bcx, local).bcx;
@ -5302,7 +5302,7 @@ iter block_locals(&ast.block b) -> @ast.local {
// use the index here.
for (@ast.stmt s in b.node.stmts) {
alt (s.node) {
case (ast.stmt_decl(?d)) {
case (ast.stmt_decl(?d,_)) {
alt (d.node) {
case (ast.decl_local(?local)) {
put local;
@ -6599,12 +6599,71 @@ fn trap(@block_ctxt bcx) {
bcx.build.Call(bcx.fcx.ccx.intrinsics.get("llvm.trap"), v);
}
fn check_module(ModuleRef llmod) {
fn run_passes(ModuleRef llmod, bool opt) {
auto pm = mk_pass_manager();
llvm.LLVMAddVerifierPass(pm.llpm);
llvm.LLVMRunPassManager(pm.llpm, llmod);
// TODO: run the linter here also, once there are llvm-c bindings for it.
// FIXME: This is mostly a copy of the bits of opt's -O2 that are
// available in the C api.
// FIXME2: We might want to add optmization levels like -O1, -O2, -Os, etc
// FIXME3: Should we expose and use the pass lists used by the opt tool?
if (opt) {
auto fpm = mk_pass_manager();
// createStandardFunctionPasses
llvm.LLVMAddCFGSimplificationPass(fpm.llpm);
llvm.LLVMAddScalarReplAggregatesPass(fpm.llpm);
//llvm.LLVMAddEarlyCSEPass(fpm.llpm);
llvm.LLVMRunPassManager(fpm.llpm, llmod);
// createStandardModulePasses
llvm.LLVMAddGlobalOptimizerPass(pm.llpm);
llvm.LLVMAddIPSCCPPass(pm.llpm);
llvm.LLVMAddDeadArgEliminationPass(pm.llpm);
llvm.LLVMAddInstructionCombiningPass(pm.llpm);
llvm.LLVMAddCFGSimplificationPass(pm.llpm);
llvm.LLVMAddPruneEHPass(pm.llpm);
llvm.LLVMAddFunctionInliningPass(pm.llpm);
// FIXME: crashes!
// llvm.LLVMAddFunctionAttrsPass(pm.llpm);
// llvm.LLVMAddScalarReplAggregatesPassSSA(pm.llpm);
// llvm.LLVMAddEarlyCSEPass(pm.llpm);
llvm.LLVMAddSimplifyLibCallsPass(pm.llpm);
llvm.LLVMAddJumpThreadingPass(pm.llpm);
// llvm.LLVMAddCorrelatedValuePropagationPass(pm.llpm);
llvm.LLVMAddCFGSimplificationPass(pm.llpm);
llvm.LLVMAddInstructionCombiningPass(pm.llpm);
llvm.LLVMAddTailCallEliminationPass(pm.llpm);
llvm.LLVMAddCFGSimplificationPass(pm.llpm);
llvm.LLVMAddReassociatePass(pm.llpm);
llvm.LLVMAddLoopRotatePass(pm.llpm);
llvm.LLVMAddLICMPass(pm.llpm);
llvm.LLVMAddLoopUnswitchPass(pm.llpm);
llvm.LLVMAddInstructionCombiningPass(pm.llpm);
llvm.LLVMAddIndVarSimplifyPass(pm.llpm);
// llvm.LLVMAddLoopIdiomPass(pm.llpm);
llvm.LLVMAddLoopDeletionPass(pm.llpm);
llvm.LLVMAddLoopUnrollPass(pm.llpm);
llvm.LLVMAddInstructionCombiningPass(pm.llpm);
llvm.LLVMAddGVNPass(pm.llpm);
llvm.LLVMAddMemCpyOptPass(pm.llpm);
llvm.LLVMAddSCCPPass(pm.llpm);
llvm.LLVMAddInstructionCombiningPass(pm.llpm);
llvm.LLVMAddJumpThreadingPass(pm.llpm);
// llvm.LLVMAddCorrelatedValuePropagationPass(pm.llpm);
llvm.LLVMAddDeadStoreEliminationPass(pm.llpm);
llvm.LLVMAddAggressiveDCEPass(pm.llpm);
llvm.LLVMAddCFGSimplificationPass(pm.llpm);
llvm.LLVMAddStripDeadPrototypesPass(pm.llpm);
llvm.LLVMAddDeadTypeEliminationPass(pm.llpm);
llvm.LLVMAddConstantMergePass(pm.llpm);
}
llvm.LLVMAddVerifierPass(pm.llpm);
llvm.LLVMRunPassManager(pm.llpm, llmod);
}
fn decl_no_op_type_glue(ModuleRef llmod, type_names tn) -> ValueRef {
@ -6962,7 +7021,8 @@ fn make_common_glue(str output) {
trans_exit_task_glue(glues, new_str_hash[ValueRef](), tn, llmod);
check_module(llmod);
run_passes(llmod, true);
llvm.LLVMWriteBitcodeToFile(llmod, _str.buf(output));
llvm.LLVMDisposeModule(llmod);
}
@ -7031,7 +7091,8 @@ fn trans_crate(session.session sess, @ast.crate crate,
// Translate the metadata.
middle.metadata.write_metadata(cx, crate);
check_module(llmod);
// FIXME: Add an -O option
run_passes(llmod, true);
llvm.LLVMWriteBitcodeToFile(llmod, _str.buf(output));
llvm.LLVMDisposeModule(llmod);

2
src/comp/middle/ty.rs
View file

@ -731,7 +731,7 @@ fn item_ty(@ast.item it) -> ty_params_and_ty {
fn stmt_ty(@ast.stmt s) -> @t {
alt (s.node) {
case (ast.stmt_expr(?e)) {
case (ast.stmt_expr(?e,_)) {
ret expr_ty(e);
}
case (_) {

8
src/comp/middle/typeck.rs
View file

@ -2479,12 +2479,12 @@ fn check_decl_local(&@fn_ctxt fcx, &@ast.decl decl) -> @ast.decl {
fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
alt (stmt.node) {
case (ast.stmt_decl(?decl)) {
case (ast.stmt_decl(?decl,?a)) {
alt (decl.node) {
case (ast.decl_local(_)) {
auto decl_1 = check_decl_local(fcx, decl);
ret @fold.respan[ast.stmt_](stmt.span,
ast.stmt_decl(decl_1));
ast.stmt_decl(decl_1, a));
}
case (ast.decl_item(_)) {
@ -2495,9 +2495,9 @@ fn check_stmt(&@fn_ctxt fcx, &@ast.stmt stmt) -> @ast.stmt {
ret stmt;
}
case (ast.stmt_expr(?expr)) {
case (ast.stmt_expr(?expr,?a)) {
auto expr_t = check_expr(fcx, expr);
ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t));
ret @fold.respan[ast.stmt_](stmt.span, ast.stmt_expr(expr_t, a));
}
}

318
src/comp/middle/typestate_check.rs
View file

@ -11,6 +11,7 @@ import front.ast.stmt;
import front.ast.stmt_;
import front.ast.stmt_decl;
import front.ast.stmt_expr;
import front.ast.stmt_crate_directive;
import front.ast.decl_local;
import front.ast.decl_item;
import front.ast.ident;
@ -70,9 +71,17 @@ import util.typestate_ann.prestate;
import util.typestate_ann.pre_and_post;
import util.typestate_ann.get_pre;
import util.typestate_ann.get_post;
import util.typestate_ann.ann_precond;
import util.typestate_ann.ann_prestate;
import util.typestate_ann.set_precondition;
import util.typestate_ann.set_postcondition;
import util.typestate_ann.set_in_postcond;
import util.typestate_ann.implies;
import util.typestate_ann.pre_and_post_state;
import util.typestate_ann.empty_states;
import util.typestate_ann.empty_prestate;
import util.typestate_ann.empty_ann;
import util.typestate_ann.extend_prestate;
import middle.ty;
import middle.ty.ann_to_type;
@ -97,6 +106,7 @@ import std.option;
import std.option.t;
import std.option.some;
import std.option.none;
import std.option.from_maybe;
import std.map.hashmap;
import std.list;
import std.list.list;
@ -106,6 +116,8 @@ import std.list.foldl;
import std.list.find;
import std._uint;
import std.bitv;
import std.util.fst;
import std.util.snd;
import util.typestate_ann;
import util.typestate_ann.difference;
@ -342,25 +354,58 @@ fn expr_ann(&expr e) -> ann {
}
}
/* returns ann_none if this is the sort
of statement where an ann doesn't make sense */
fn stmt_ann(&stmt s) -> ann {
alt (s.node) {
case (stmt_decl(?d)) {
alt (d.node) {
case (decl_local(?l)) {
ret l.ann;
}
case (decl_item(?i)) {
ret ann_none; /* ????? */
}
fn ann_to_ts_ann(ann a, uint nv) -> ts_ann {
alt (a) {
case (ann_none) { ret empty_ann(nv); }
case (ann_type(_,_,?t)) {
alt (t) {
/* Kind of inconsistent. empty_ann()s everywhere
or an option of a ts_ann? */
case (none[@ts_ann]) { ret empty_ann(nv); }
case (some[@ts_ann](?t)) { ret *t; }
}
}
case (stmt_expr(?e)) {
ret expr_ann(*e);
}
}
fn stmt_ann(&stmt s) -> option.t[@ts_ann] {
alt (s.node) {
case (stmt_decl(_,?a)) {
ret a;
}
case (_) {
ret ann_none;
case (stmt_expr(_,?a)) {
ret a;
}
case (stmt_crate_directive(_)) {
ret none[@ts_ann];
}
}
}
/*
/* fails if no annotation */
fn stmt_pp(&stmt s) -> pre_and_post {
ret (stmt_ann(s)).conditions;
}
*/
/* fails if e has no annotation */
fn expr_states(&expr e) -> pre_and_post_state {
alt (expr_ann(e)) {
case (ann_none) {
log "expr_pp: the impossible happened (no annotation)";
fail;
}
case (ann_type(_, _, ?maybe_pp)) {
alt (maybe_pp) {
case (none[@ts_ann]) {
log "expr_pp: the impossible happened (no pre/post)";
fail;
}
case (some[@ts_ann](?p)) {
// ret p.states;
}
}
}
}
}
@ -386,64 +431,17 @@ fn expr_pp(&expr e) -> pre_and_post {
}
}
/* fails if e has no annotation */
fn expr_states(&expr e) -> pre_and_post_state {
alt (expr_ann(e)) {
case (ann_none) {
log "expr_pp: the impossible happened (no annotation)";
fail;
fn stmt_states(&stmt s, uint nv) -> pre_and_post_state {
alt (stmt_ann(s)) {
case (none[@ts_ann]) {
ret empty_states(nv);
}
case (ann_type(_, _, ?maybe_pp)) {
alt (maybe_pp) {
case (none[@ts_ann]) {
log "expr_pp: the impossible happened (no pre/post)";
fail;
}
case (some[@ts_ann](?p)) {
ret p.states;
}
}
case (some[@ts_ann](?a)) {
ret a.states;
}
}
}
/* fails if no annotation */
fn stmt_pp(&stmt s) -> pre_and_post {
alt (stmt_ann(s)) {
case (ann_none) {
fail;
}
case (ann_type(_, _, ?maybe_pp)) {
alt (maybe_pp) {
case (none[@ts_ann]) {
fail;
}
case (some[@ts_ann](?p)) {
ret p.conditions;
}
}
}
}
}
/* fails if no annotation */
fn stmt_states(&stmt s) -> pre_and_post_state {
alt (stmt_ann(s)) {
case (ann_none) {
fail;
}
case (ann_type(_, _, ?maybe_pp)) {
alt (maybe_pp) {
case (none[@ts_ann]) {
fail;
}
case (some[@ts_ann](?p)) {
ret p.states;
}
}
}
}
}
fn expr_precond(&expr e) -> precond {
ret (expr_pp(e)).precondition;
@ -461,6 +459,7 @@ fn expr_poststate(&expr e) -> poststate {
ret (expr_states(e)).poststate;
}
/*
fn stmt_precond(&stmt s) -> precond {
ret (stmt_pp(s)).precondition;
}
@ -468,13 +467,19 @@ fn stmt_precond(&stmt s) -> precond {
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) -> prestate {
ret (stmt_states(s)).prestate;
}
fn stmt_poststate(&stmt s) -> poststate {
ret (stmt_states(s)).poststate;
*/
fn stmt_poststate(&stmt s, uint nv) -> poststate {
ret (stmt_states(s, nv)).poststate;
}
/* returns a new annotation where the pre_and_post is p */
@ -684,12 +689,19 @@ fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
}
}
fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
&ast.stmt s) -> ast.stmt {
impure fn gen(&fn_info enclosing, ts_ann a, def_id id) {
check(enclosing.contains_key(id));
let uint i = enclosing.get(id);
set_in_postcond(i, a.conditions);
}
fn find_pre_post_stmt(_fn_info_map fm, &fn_info enclosing, &ast.stmt s)
-> ast.stmt {
auto num_local_vars = num_locals(enclosing);
alt(s.node) {
case(ast.stmt_decl(?adecl)) {
case(ast.stmt_decl(?adecl, ?a)) {
alt(adecl.node) {
case(ast.decl_local(?alocal)) {
alt(alocal.init) {
@ -702,9 +714,25 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
@rec(ty=alocal.ty, infer=alocal.infer,
ident=alocal.ident, init=some[initializer](a_i),
id=alocal.id, ann=res_ann);
let ts_ann stmt_ann;
alt (a) {
case (none[@ts_ann]) {
stmt_ann = empty_ann(num_local_vars);
}
case (some[@ts_ann](?aa)) {
stmt_ann = *aa;
}
}
/* Inherit ann from initializer, and add var being
initialized to the postcondition */
set_precondition(stmt_ann, expr_precond(*r));
set_postcondition(stmt_ann, expr_postcond(*r));
gen(enclosing, stmt_ann, alocal.id);
let stmt_ res = stmt_decl(@respan(adecl.span,
decl_local(res_local)));
ret (respan(s.span, res));
decl_local(res_local)),
some[@ts_ann](@stmt_ann));
ret (respan(s.span, res));
}
case(none[ast.initializer]) {
// log("pre/post for init of " + alocal.ident + ": none");
@ -716,22 +744,30 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
id=alocal.id, ann=res_ann);
let stmt_ res =
stmt_decl
(@respan(adecl.span, decl_local(res_local)));
ret (respan (s.span, res));
(@respan(adecl.span, decl_local(res_local)),
some[@ts_ann](@empty_ann(num_local_vars)));
ret respan(s.span, res); /* inherit ann from initializer */
}
}
}
case(decl_item(?anitem)) {
auto res_item = find_pre_post_item(fm, enclosing, *anitem);
ret (respan(s.span, stmt_decl(@respan(adecl.span,
decl_item(@res_item)))));
ret respan(s.span,
stmt_decl(@respan(adecl.span,
decl_item(@res_item)),
some[@ts_ann](@empty_ann(num_local_vars))));
}
}
}
case(stmt_expr(?e)) {
case(stmt_expr(?e,_)) {
log_expr(e);
let @expr e_pp = find_pre_post_expr(enclosing, *e);
ret (respan(s.span, stmt_expr(e_pp)));
/* inherit ann from expr */
ret respan(s.span,
stmt_expr(e_pp,
some[@ts_ann]
(@ann_to_ts_ann(expr_ann(*e_pp),
num_local_vars))));
}
}
}
@ -739,7 +775,7 @@ fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
-> block {
fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> @stmt {
ret (@find_pre_post_for_each_stmt(fm, i, *s));
ret (@find_pre_post_stmt(fm, i, *s));
}
auto do_one = bind do_one_(fm, enclosing, _);
@ -767,22 +803,93 @@ fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
}
/* Returns a pair of a new function, with possibly a changed pre- or
post-state, and a boolean flag saying whether the function's pre- or
poststate changed */
fn find_pre_post_state_fn(fn_info f_info, &ast._fn f) -> tup(bool, ast._fn) {
log ("Implement find_pre_post_state_fn!");
/* FIXME */
fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
&prestate pres, expr e)
-> tup(bool, @expr) {
log("Implement find_pre_post_state_expr!");
fail;
}
fn fixed_point_states(fn_info f_info,
fn (fn_info, &ast._fn) -> tup(bool, ast._fn) f,
/* FIXME: This isn't done yet. */
fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
&prestate pres, @stmt s) -> bool {
auto changed = false;
alt (s.node) {
case (stmt_decl(?adecl, ?a)) {
alt (adecl.node) {
case (ast.decl_local(?alocal)) {
alt (alocal.init) {
case (some[ast.initializer](?an_init)) {
auto p = find_pre_post_state_expr(fm, enclosing,
pres, *an_init.expr);
fail; /* FIXME */
/* Next: copy pres into a's prestate;
find the poststate by taking p's poststate
and setting the bit for alocal.id */
}
}
}
}
}
}
}
/* Returns a pair of a new block, with possibly a changed pre- or
post-state, and a boolean flag saying whether the function's pre- or
poststate changed */
fn find_pre_post_state_block(&_fn_info_map fm, &fn_info enclosing, block b)
-> tup(bool, block) {
auto changed = false;
auto num_local_vars = num_locals(enclosing);
/* First, set the pre-states and post-states for every expression */
auto pres = empty_prestate(num_local_vars);
/* 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 = changed || find_pre_post_state_stmt(fm, enclosing, pres, s);
/* Shouldn't need to rebuild the stmt.
This just updates bit-vectors
in a side-effecting way. */
extend_prestate(pres, stmt_poststate(*s, num_local_vars));
}
fn do_inner_(_fn_info_map fm, fn_info i, prestate p, &@expr e)
-> tup (bool, @expr) {
ret find_pre_post_state_expr(fm, i, p, *e);
}
auto do_inner = bind do_inner_(fm, enclosing, pres, _);
let option.t[tup(bool, @expr)] e_ =
option.map[@expr, tup(bool, @expr)](do_inner, b.node.expr);
auto s = snd[bool, @expr];
auto f = fst[bool, @expr];
changed = changed ||
from_maybe[bool](false,
option.map[tup(bool, @expr), bool](f, e_));
let block_ b_res = rec(stmts=b.node.stmts,
expr=option.map[tup(bool, @expr), @expr](s, e_),
index=b.node.index);
ret tup(changed, respan(b.span, b_res));
}
fn find_pre_post_state_fn(_fn_info_map f_info, fn_info fi, &ast._fn f)
-> tup(bool, ast._fn) {
auto p = find_pre_post_state_block(f_info, fi, f.body);
ret tup(p._0, rec(decl=f.decl, proto=f.proto, body=p._1));
}
fn fixed_point_states(_fn_info_map fm, fn_info f_info,
fn (_fn_info_map, fn_info, &ast._fn)
-> tup(bool, ast._fn) f,
&ast._fn start) -> ast._fn {
auto next = f(f_info, start);
auto next = f(fm, f_info, start);
if (next._0) {
// something changed
be fixed_point_states(f_info, f, next._1);
be fixed_point_states(fm, f_info, f, next._1);
}
else {
// we're done!
@ -790,42 +897,29 @@ fn fixed_point_states(fn_info f_info,
}
}
fn check_states_expr(fn_info enclosing, &expr e) -> () {
impure fn check_states_expr(fn_info enclosing, &expr e) -> () {
let precond prec = expr_precond(e);
let postcond postc = expr_postcond(e);
let prestate pres = expr_prestate(e);
let poststate posts = expr_poststate(e);
if (!implies(pres, prec)) {
log("check_states_expr: unsatisfied precondition");
fail;
}
if (!implies(posts, postc)) {
log("check_states_expr: unsatisfied postcondition");
fail;
}
}
fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
alt (stmt_ann(s)) {
case (ann_none) {
// Statement doesn't require an annotation -- do nothing
case (none[@ts_ann]) {
ret;
}
case (ann_type(_,_,?m_pp)) {
let precond prec = stmt_precond(s);
let postcond postc = stmt_postcond(s);
let prestate pres = stmt_prestate(s);
let poststate posts = stmt_poststate(s);
case (some[@ts_ann](?a)) {
let precond prec = ann_precond(*a);
let prestate pres = ann_prestate(*a);
if (!implies(pres, prec)) {
log("check_states_stmt: unsatisfied precondition");
fail;
}
if (!implies(posts, postc)) {
log("check_states_stmt: unsatisfied postcondition");
fail;
}
}
}
}
@ -855,7 +949,7 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
/* Compute the pre- and post-states for this function */
auto g = find_pre_post_state_fn;
auto res_f = fixed_point_states(f_info, g, f);
auto res_f = fixed_point_states(f_info_map, f_info, g, f);
/* Now compare each expr's pre-state to its precondition
and post-state to its postcondition */