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

Rewrite tstate.annotate to use walk instead of fold

Browse source 
and various other tidying in typestate
This commit is contained in:
Tim Chevalier 2011-05-18 15:43:05 -07:00 • committed by Graydon Hoare
parent dc83c84662
commit e16b097599
9 changed files with 629 additions and 892 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/comp/middle/tstate/ann.rs
View file

@ -20,13 +20,13 @@ type poststate = bitv::t; /* 1 means "this variable is definitely initialized"
initialized" */
/* named thus so as not to confuse with prestate and poststate */
type pre_and_post = rec(precond precondition, postcond postcondition);
type pre_and_post = @rec(precond precondition, postcond postcondition);
/* FIXME: once it's implemented: */
// : ((*.precondition).nbits == (*.postcondition).nbits);
type pre_and_post_state = rec(prestate prestate, poststate poststate);
type ts_ann = rec(pre_and_post conditions, pre_and_post_state states);
type ts_ann = @rec(pre_and_post conditions, pre_and_post_state states);
fn true_precond(uint num_vars) -> precond {
be bitv::create(num_vars, false);
@ -49,18 +49,18 @@ fn false_postcond(uint num_vars) -> postcond {
}
fn empty_pre_post(uint num_vars) -> pre_and_post {
ret(rec(precondition=empty_prestate(num_vars),
postcondition=empty_poststate(num_vars)));
ret(@rec(precondition=empty_prestate(num_vars),
postcondition=empty_poststate(num_vars)));
}
fn empty_states(uint num_vars) -> pre_and_post_state {
ret(rec(prestate=true_precond(num_vars),
poststate=true_postcond(num_vars)));
poststate=true_postcond(num_vars)));
}
fn empty_ann(uint num_vars) -> ts_ann {
ret(rec(conditions=empty_pre_post(num_vars),
states=empty_states(num_vars)));
ret(@rec(conditions=empty_pre_post(num_vars),
states=empty_states(num_vars)));
}
fn get_pre(&pre_and_post p) -> precond {
@ -111,25 +111,25 @@ 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);
}
// Sets all the bits in a's prestate to equal the
// corresponding bit in p's prestate.
fn set_prestate(@ts_ann a, &prestate p) -> bool {
fn set_prestate(ts_ann a, &prestate p) -> bool {
ret bitv::copy(a.states.prestate, p);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
fn set_poststate(@ts_ann a, &poststate p) -> bool {
fn set_poststate(ts_ann a, &poststate p) -> bool {
ret bitv::copy(a.states.poststate, p);
}
@ -150,6 +150,16 @@ fn relax_prestate(uint i, &prestate p) -> bool {
ret was_set;
}
// Clears all the bits in p
fn clear(&precond p) -> () {
bitv::clear(p);
}
// Sets all the bits in p
fn set(&precond p) -> () {
bitv::set_all(p);
}
fn ann_precond(&ts_ann a) -> precond {
ret a.conditions.precondition;
}
@ -163,8 +173,8 @@ fn ann_poststate(&ts_ann a) -> poststate {
}
fn pp_clone(&pre_and_post p) -> pre_and_post {
ret rec(precondition=clone(p.precondition),
postcondition=clone(p.postcondition));
ret @rec(precondition=clone(p.precondition),
postcondition=clone(p.postcondition));
}
fn clone(prestate p) -> prestate {

468
src/comp/middle/tstate/annotate.rs
View file

@ -4,7 +4,6 @@ import std::option::some;
import std::option::none;
import front::ast;
import front::ast::ident;
import front::ast::def_id;
import front::ast::ann;
@ -76,417 +75,104 @@ 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 middle::ty::expr_ann;
import util::common::uistr;
import util::common::span;
import util::common::new_str_hash;
import util::common::log_expr_err;
import util::common::log_block_err;
import util::common::log_item_err;
import util::common::log_stmt_err;
import util::common::log_expr;
import util::common::log_block;
import util::common::log_stmt;
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;
import middle::tstate::aux::crate_ctxt;
import middle::tstate::ann::empty_ann;
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)));
fn collect_ids_expr(&@expr e, @vec[uint] res) -> () {
vec::push(*res, (expr_ann(e)).id);
}
fn collect_ids_block(&block b, @vec[uint] res) -> () {
vec::push(*res, b.node.a.id);
}
/* 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);
fn collect_ids_stmt(&@stmt s, @vec[uint] res) -> () {
alt (s.node) {
case (stmt_decl(_,?a)) {
log("node_id " + uistr(a.id));
log_stmt(*s);
vec::push(*res, a.id);
}
case (stmt_expr(_,?a)) {
log("node_id " + uistr(a.id));
log_stmt(*s);
vec::push(*res, a.id);
}
case (_) {}
}
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;
fn collect_ids_decl(&@decl d, @vec[uint] res) -> () {
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 = [];
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 = [];
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);
vec::push(*res, l.ann.id);
}
case (_) {}
}
}
fn annotate_module(&fn_info_map fm, &_mod module) -> _mod {
let vec[@item] new_items = [];
for (@item i in module.items) {
auto new_item = annotate_item(fm, i);
vec::push[@item](new_items, new_item);
fn node_ids_in_fn(&_fn f, &def_id d, @vec[uint] res) -> () {
auto collect_ids = walk::default_visitor();
collect_ids = rec(visit_expr_pre = bind collect_ids_expr(_,res),
visit_block_pre = bind collect_ids_block(_,res),
visit_stmt_pre = bind collect_ids_stmt(_,res),
visit_decl_pre = bind collect_ids_decl(_,res)
with collect_ids);
walk::walk_fn(collect_ids, f, d);
}
fn init_vecs(&crate_ctxt ccx, @vec[uint] node_ids, uint len) -> () {
for (uint i in *node_ids) {
log(uistr(i) + " |-> " + uistr(len));
ccx.node_anns.insert(i, empty_ann(len));
}
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));
fn visit_fn(&crate_ctxt ccx, uint num_locals, &_fn f, &def_id d) -> () {
let vec[uint] node_ids_ = [];
let @vec[uint] node_ids = @node_ids_;
node_ids_in_fn(f, d, node_ids);
init_vecs(ccx, node_ids, num_locals);
}
fn annotate_in_fn(&crate_ctxt ccx, &_fn f, &def_id f_id) -> () {
auto f_info = get_fn_info(ccx, f_id);
visit_fn(ccx, num_locals(f_info), f, f_id);
}
fn annotate_crate(&crate_ctxt ccx, &crate crate) -> () {
auto do_ann = walk::default_visitor();
do_ann = rec(visit_fn_pre = bind annotate_in_fn(ccx, _, _)
with do_ann);
walk::walk_crate(do_ann, crate);
}
//
// 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:
//

241
src/comp/middle/tstate/auxiliary.rs
View file

@ -37,6 +37,7 @@ import util::common;
import util::common::span;
import util::common::log_block;
import util::common::new_def_hash;
import util::common::new_uint_hash;
import util::common::log_expr_err;
import util::common::uistr;
@ -157,6 +158,10 @@ fn print_idents(vec[ident] idents) -> () {
type var_info = tup(uint, ident);
type fn_info = rec(@std::map::hashmap[def_id, var_info] vars,
controlflow cf);
/* mapping from node ID to typestate annotation */
type node_ann_table = @std::map::hashmap[uint, ts_ann];
/* mapping from function name to fn_info map */
type fn_info_map = @std::map::hashmap[def_id, fn_info];
@ -167,176 +172,187 @@ type fn_ctxt = rec(fn_info enclosing,
type crate_ctxt = rec(ty::ctxt tcx,
ty::node_type_table node_types,
node_ann_table node_anns,
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);
fn get_fn_info(&crate_ctxt ccx, def_id did) -> fn_info {
assert (ccx.fm.contains_key(did));
ret ccx.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] { ret a.ts; }
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_strict: didn't expect none here");
fn ann_to_ts_ann(&crate_ctxt ccx, &ann a) -> ts_ann {
alt (ccx.node_anns.find(a.id)) {
case (none[ts_ann]) {
log_err ("ann_to_ts_ann: no ts_ann for node_id "
+ uistr(a.id));
fail;
}
case (some[@ts_ann](?t)) { ret t; }
case (some[ts_ann](?t)) { ret t; }
}
}
fn ann_to_poststate(ann a) -> poststate {
ret (ann_to_ts_ann_strict(a)).states.poststate;
fn ann_to_poststate(&crate_ctxt ccx, ann a) -> poststate {
log "ann_to_poststate";
ret (ann_to_ts_ann(ccx, a)).states.poststate;
}
fn stmt_to_ann(&stmt s) -> option::t[@ts_ann] {
fn stmt_to_ann(&crate_ctxt ccx, &stmt s) -> ts_ann {
log "stmt_to_ann";
alt (s.node) {
case (stmt_decl(_,?a)) {
ret ann_to_ts_ann_fail(a);
ret ann_to_ts_ann(ccx, a);
}
case (stmt_expr(_,?a)) {
ret ann_to_ts_ann_fail(a);
ret ann_to_ts_ann(ccx, a);
}
case (stmt_crate_directive(_)) {
ret none[@ts_ann];
log_err "expecting an annotated statement here";
fail;
}
}
}
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(&crate_ctxt ccx, @expr e) -> pre_and_post_state {
log "expr_states";
ret (ann_to_ts_ann(ccx, expr_ann(e)).states);
}
/* 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);
fn expr_pp(&crate_ctxt ccx, @expr e) -> pre_and_post {
log "expr_pp";
ret (ann_to_ts_ann(ccx, expr_ann(e)).conditions);
}
/* 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);
fn stmt_pp(&crate_ctxt ccx, &stmt s) -> pre_and_post {
ret (stmt_to_ann(ccx, 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_pp(&crate_ctxt ccx, &block b) -> pre_and_post {
log "block_pp";
ret (ann_to_ts_ann(ccx, b.node.a).conditions);
}
fn block_states(&block b) -> pre_and_post_state {
ret (ann_to_ts_ann_strict(b.node.a).states);
fn clear_pp(pre_and_post pp) {
ann::clear(pp.precondition);
ann::clear(pp.postcondition);
}
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 clear_precond(&crate_ctxt ccx, &ann a) {
auto pp = ann_to_ts_ann(ccx, a);
ann::clear(pp.conditions.precondition);
}
fn expr_precond(@expr e) -> precond {
ret (expr_pp(e)).precondition;
fn block_states(&crate_ctxt ccx, &block b) -> pre_and_post_state {
log "block_states";
ret (ann_to_ts_ann(ccx, b.node.a).states);
}
fn expr_postcond(@expr e) -> postcond {
ret (expr_pp(e)).postcondition;
fn stmt_states(&crate_ctxt ccx, &stmt s) -> pre_and_post_state {
ret (stmt_to_ann(ccx, s)).states;
}
fn expr_prestate(@expr e) -> prestate {
ret (expr_states(e)).prestate;
fn expr_precond(&crate_ctxt ccx, @expr e) -> precond {
ret (expr_pp(ccx, e)).precondition;
}
fn expr_poststate(@expr e) -> poststate {
ret (expr_states(e)).poststate;
fn expr_postcond(&crate_ctxt ccx, @expr e) -> postcond {
ret (expr_pp(ccx, e)).postcondition;
}
fn stmt_precond(&stmt s) -> precond {
ret (stmt_pp(s)).precondition;
fn expr_prestate(&crate_ctxt ccx, @expr e) -> prestate {
ret (expr_states(ccx, e)).prestate;
}
fn stmt_postcond(&stmt s) -> postcond {
ret (stmt_pp(s)).postcondition;
fn expr_poststate(&crate_ctxt ccx, @expr e) -> poststate {
ret (expr_states(ccx, e)).poststate;
}
fn stmt_precond(&crate_ctxt ccx, &stmt s) -> precond {
ret (stmt_pp(ccx, s)).precondition;
}
fn stmt_postcond(&crate_ctxt ccx, &stmt s) -> postcond {
ret (stmt_pp(ccx, 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_prestate(&crate_ctxt ccx, &stmt s) -> prestate {
ret (stmt_states(ccx, s)).prestate;
}
fn stmt_poststate(&stmt s, uint nv) -> poststate {
ret (stmt_states(s, nv)).poststate;
fn stmt_poststate(&crate_ctxt ccx, &stmt s) -> poststate {
ret (stmt_states(ccx, s)).poststate;
}
fn block_postcond(&block b) -> postcond {
ret (block_pp(b)).postcondition;
fn block_postcond(&crate_ctxt ccx, &block b) -> postcond {
ret (block_pp(ccx, b)).postcondition;
}
fn block_poststate(&block b) -> poststate {
ret (block_states(b)).poststate;
fn block_poststate(&crate_ctxt ccx, &block b) -> poststate {
ret (block_states(ccx, b)).poststate;
}
/* returns a new annotation where the pre_and_post is p */
fn with_pp(ann a, pre_and_post p) -> ann {
ret rec(id=a.id, ty=a.ty, tps=a.tps,
ts=some[@ts_ann](@rec(conditions=p,
states=empty_states(pps_len(p)))));
/* sets the pre_and_post for an ann */
fn with_pp(&crate_ctxt ccx, &ann a, pre_and_post p) {
ccx.node_anns.insert(a.id, @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 set_prestate_ann(&crate_ctxt ccx, &ann a, &prestate pre) -> bool {
log "set_prestate_ann";
ret set_prestate(ann_to_ts_ann(ccx, a), pre);
}
fn extend_prestate_ann(&ann a, &prestate pre) -> bool {
ret extend_prestate(ann_to_ts_ann_strict(a).states.prestate, pre);
fn extend_prestate_ann(&crate_ctxt ccx, &ann a, &prestate pre) -> bool {
log "extend_prestate_ann";
ret extend_prestate(ann_to_ts_ann(ccx, a).states.prestate, pre);
}
fn set_poststate_ann(&ann a, &poststate post) -> bool {
ret set_poststate(ann_to_ts_ann_strict(a), post);
fn set_poststate_ann(&crate_ctxt ccx, &ann a, &poststate post) -> bool {
log "set_poststate_ann";
ret set_poststate(ann_to_ts_ann(ccx, a), post);
}
fn extend_poststate_ann(&ann a, &poststate post) -> bool {
ret extend_poststate(ann_to_ts_ann_strict(a).states.poststate, post);
fn extend_poststate_ann(&crate_ctxt ccx, &ann a, &poststate post) -> bool {
log "extend_poststate_ann";
ret extend_poststate(ann_to_ts_ann(ccx, 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 set_pre_and_post(&crate_ctxt ccx, &ann a,
&precond pre, &postcond post) -> () {
log "set_pre_and_post";
auto t = ann_to_ts_ann(ccx, a);
set_precondition(t, pre);
set_postcondition(t, post);
}
fn pure_exp(&ann a, &prestate p) -> bool {
fn copy_pre_post(&crate_ctxt ccx, &ann a, &@expr sub) -> () {
log "set_pre_and_post";
auto p = expr_pp(ccx, sub);
auto t = ann_to_ts_ann(ccx, a);
set_precondition(t, p.precondition);
set_postcondition(t, p.postcondition);
}
/* sets all bits to *1* */
fn set_postcond_false(&crate_ctxt ccx, &ann a) {
auto p = ann_to_ts_ann(ccx, a);
ann::set(p.conditions.postcondition);
}
fn pure_exp(&crate_ctxt ccx, &ann a, &prestate p) -> bool {
auto changed = false;
changed = extend_prestate_ann(a, p) || changed;
changed = extend_poststate_ann(a, p) || changed;
changed = extend_prestate_ann(ccx, a, p) || changed;
changed = extend_poststate_ann(ccx, a, p) || changed;
ret changed;
}
@ -354,31 +370,14 @@ fn fixed_point_states(&fn_ctxt fcx,
}
}
fn init_ann(&fn_info fi, &ann a) -> ann {
ret rec(id=a.id, ty=a.ty, tps=a.tps,
ts=some[@ts_ann](@empty_ann(num_locals(fi))));
}
fn init_blank_ann(&() ignore, &ann a) -> ann {
ret rec(id=a.id, ty=a.ty, tps=a.tps, ts=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));
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]());
ret rec(tcx=cx, node_types=nt,
node_anns=@new_uint_hash[ts_ann](),
fm=@new_def_hash[fn_info]());
}
fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
@ -395,9 +394,15 @@ fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
auto f = expr_ann(e).id;
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; }
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;
}
}
}

10
src/comp/middle/tstate/bitvectors.rs
View file

@ -12,8 +12,8 @@ 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::aux::ann_to_ts_ann;
import tstate::ann::pre_and_post;
import tstate::ann::precond;
import tstate::ann::postcond;
@ -48,7 +48,7 @@ fn seq_preconds(fn_info enclosing, vec[pre_and_post] pps) -> precond {
let uint num_vars = num_locals(enclosing);
if (sz >= 1u) {
auto first = pps.(0);
auto first = pps.(0);
assert (pps_len(first) == num_vars);
let precond rest = seq_preconds(enclosing,
slice[pre_and_post](pps, 1u, sz));
@ -115,9 +115,10 @@ fn intersect_postconds(&vec[postcond] pcs) -> postcond {
}
fn gen(&fn_ctxt fcx, &ann a, def_id id) -> bool {
log "gen";
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);
ret set_in_postcond(i, (ann_to_ts_ann(fcx.ccx, a)).conditions);
}
fn declare_var(&fn_info enclosing, def_id id, prestate pre)
@ -130,8 +131,9 @@ fn declare_var(&fn_info enclosing, def_id id, prestate pre)
}
fn gen_poststate(&fn_ctxt fcx, &ann a, def_id id) -> bool {
log "gen_poststate";
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);
ret set_in_poststate(i, (ann_to_ts_ann(fcx.ccx, a)).states);
}

119
src/comp/middle/tstate/ck.rs
View file

@ -56,6 +56,8 @@ import aux::fixed_point_states;
import aux::bitv_to_str;
import util::common::ty_to_str;
import util::common::log_stmt_err;
import aux::log_bitv_err;
import bitvectors::promises;
import annotate::annotate_crate;
@ -64,51 +66,45 @@ 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);
let precond prec = expr_precond(fcx.ccx, e);
let prestate pres = expr_prestate(fcx.ccx, 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);
}
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);
auto a = stmt_to_ann(fcx.ccx, s);
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);
*/
/*
log_err("check_states_stmt:");
log_stmt_err(s);
log_err("prec = ");
log_bitv_err(fcx.enclosing, prec);
log_err("pres = ");
log_bitv_err(fcx.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);
}
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) -> () {
@ -116,33 +112,30 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f, &ann a) -> () {
auto nv = num_locals(enclosing);
auto post = @empty_poststate(nv);
fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post, uint nv) -> () {
fn do_one_(fn_ctxt fcx, &@stmt s, @poststate post) -> () {
check_states_stmt(fcx, *s);
*post = stmt_poststate(*s, nv);
*post = stmt_poststate(fcx.ccx, *s);
}
auto do_one = bind do_one_(fcx, _, post, nv);
auto do_one = bind do_one_(fcx, _, post);
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);
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(fcx.ccx, 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)); */
fcx.ccx.tcx.sess.span_warn(f.body.span, "not all control paths " +
"return a value");
/* 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: call span_err, not span_warn, once I finish implementing
! annotations */
fcx.ccx.tcx.sess.span_warn(f.body.span, "In function " + fcx.name +
", not all control paths return a value");
fcx.ccx.tcx.sess.span_note(f.decl.output.span,
"see declared return type of '" + ty_to_str(*f.decl.output) +
"'");
@ -202,15 +195,15 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
/* 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);
/* Add a blank ts_ann for every statement (and expression) */
annotate_crate(ccx, *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);
fold_crate[crate_ctxt](ccx, fld, crate);
auto fld1 = new_identity_fold[crate_ctxt]();

25
src/comp/middle/tstate/collect_locals.rs
View file

@ -31,22 +31,28 @@ import aux::var_info;
import aux::crate_ctxt;
import util::common::new_def_hash;
import util::common::uistr;
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, &@local loc) -> () {
log("collect_local: pushing " + loc.ident);
_vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
fn collect_local(&@vec[tup(ident, def_id)] vars, &@decl d) -> () {
alt (d.node) {
case (decl_local(?loc)) {
log("collect_local: pushing " + loc.ident);
vec::push[tup(ident, def_id)](*vars, tup(loc.ident, loc.id));
}
case (_) { ret; }
}
}
fn find_locals(_fn f) -> @vec[tup(ident,def_id)] {
fn find_locals(_fn f, def_id d) -> @vec[tup(ident,def_id)] {
auto res = @vec::alloc[tup(ident,def_id)](0u);
auto visitor = walk::default_visitor();
visitor = rec(visit_decl_pre=bind collect_local(res,_) with visitor);
walk_fn(visitor, f);
walk_fn(visitor, f, d);
ret res;
}
@ -69,7 +75,7 @@ fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
/* ignore args, which we know are initialized;
just collect locally declared vars */
let @vec[tup(ident,def_id)] locals = find_locals(f);
let @vec[tup(ident,def_id)] locals = find_locals(f, f_id);
// 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);
@ -78,6 +84,9 @@ fn mk_fn_info(_fn f, def_id f_id, ident f_name) -> fn_info {
we can safely use the function's name itself for this purpose */
add_var(f_id, f_name, next, res);
log(f_name + " has " + uistr(vec::len[tup(ident, def_id)](*locals))
+ " locals");
ret res;
}
@ -91,7 +100,7 @@ fn mk_fn_info_item (&crate_ctxt ccx, &@item i) -> () {
ccx.fm.insert(id, f_inf);
}
case (item_obj(?i,?o,?ty_params,?odid,?a)) {
auto all_methods = _vec::clone[@method](o.methods);
auto all_methods = vec::clone[@method](o.methods);
plus_option[@method](all_methods, o.dtor);
auto f_inf;
for (@method m in all_methods) {
@ -109,7 +118,7 @@ fn mk_fn_info_item (&crate_ctxt ccx, &@item i) -> () {
fn mk_f_to_fn_info(&crate_ctxt ccx, @crate c) -> () {
let ast_visitor vars_visitor = walk::default_visitor();
vars_visitor = rec(visit_item_post=bind mk_fn_info_item(ccx,_)
with vars_visitor);
with vars_visitor);
walk_crate(vars_visitor, *c);
}

224
src/comp/middle/tstate/pre_post_conditions.rs
View file

@ -9,13 +9,14 @@ 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 tstate::ann::set_precondition;
import tstate::ann::set_postcondition;
import aux::var_info;
import aux::crate_ctxt;
import aux::fn_ctxt;
@ -23,7 +24,10 @@ import aux::num_locals;
import aux::expr_pp;
import aux::stmt_pp;
import aux::block_pp;
import aux::clear_pp;
import aux::clear_precond;
import aux::set_pre_and_post;
import aux::copy_pre_post;
import aux::expr_precond;
import aux::expr_postcond;
import aux::expr_prestate;
@ -33,6 +37,8 @@ import aux::fn_info;
import aux::log_pp;
import aux::ann_to_def;
import aux::ann_to_def_strict;
import aux::ann_to_ts_ann;
import aux::set_postcond_false;
import bitvectors::seq_preconds;
import bitvectors::union_postconds;
@ -145,6 +151,8 @@ import util::common::field_exprs;
import util::common::has_nonlocal_exits;
import util::common::log_stmt;
import util::common::log_expr_err;
import util::common::log_block_err;
import util::common::log_block;
fn find_pre_post_mod(&_mod m) -> _mod {
log("implement find_pre_post_mod!");
@ -209,6 +217,11 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
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) {
if (vec::len[@expr](args) > 0u) {
log ("find_pre_post_exprs: oper =");
log_expr(*(args.(0)));
}
auto enclosing = fcx.enclosing;
auto fm = fcx.ccx.fm;
auto nv = num_locals(enclosing);
@ -220,37 +233,40 @@ fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
vec::map[@expr, ()](f, args);
fn get_pp(&@expr e) -> pre_and_post {
ret expr_pp(e);
fn get_pp(crate_ctxt ccx, &@expr e) -> pre_and_post {
ret expr_pp(ccx, e);
}
auto g = get_pp;
auto g = bind get_pp(fcx.ccx, _);
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)))));
set_pre_and_post(fcx.ccx, a, seq_preconds(enclosing, pps),
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);
log("222");
auto loop_precond = declare_var(fcx.enclosing, decl_lhs(d),
seq_preconds(fcx.enclosing, [expr_pp(index),
block_pp(body)]));
seq_preconds(fcx.enclosing, [expr_pp(fcx.ccx, index),
block_pp(fcx.ccx, body)]));
auto loop_postcond = intersect_postconds
([expr_postcond(index), block_postcond(body)]);
set_pre_and_post(a, rec(precondition=loop_precond,
postcondition=loop_postcond));
([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]);
set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
}
fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var) -> () {
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));
auto p = expr_pp(fcx.ccx, rhs);
set_pre_and_post(fcx.ccx, larger_ann,
p.precondition, p.postcondition);
gen(fcx, larger_ann, d_id);
}
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
@ -265,15 +281,10 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
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 =" +
log("find_pre_post_expr (num_locals =" +
uistr(num_local_vars) + "):");
log_expr_err(*e);
*/
log_expr(*e);
alt (e.node) {
case (expr_call(?operator, ?operands, ?a)) {
@ -293,9 +304,10 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
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);
auto res = expr_pp(fcx.ccx, e);
clear_pp(res);
auto df = ann_to_def_strict(fcx.ccx, a);
alt (df) {
case (def_local(?d_id)) {
auto i = bit_num(d_id, enclosing);
@ -303,37 +315,33 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
}
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));
clear_pp(expr_pp(fcx.ccx, e));
}
case(expr_log(_, ?arg, ?a)) {
find_pre_post_expr(fcx, arg);
set_pre_and_post(a, expr_pp(arg));
copy_pre_post(fcx.ccx, a, arg);
}
case (expr_chan(?arg, ?a)) {
find_pre_post_expr(fcx, arg);
set_pre_and_post(a, expr_pp(arg));
copy_pre_post(fcx.ccx, a, 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));
copy_pre_post(fcx.ccx, a, arg);
}
case (none[@expr]) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
clear_pp(expr_pp(fcx.ccx, e));
}
}
}
case (expr_block(?b, ?a)) {
find_pre_post_block(fcx, b);
set_pre_and_post(a, block_pp(b));
auto p = block_pp(fcx.ccx, b);
set_pre_and_post(fcx.ccx, a, p.precondition, p.postcondition);
}
case (expr_rec(?fields,?maybe_base,?a)) {
auto es = field_exprs(fields);
@ -343,7 +351,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
case (expr_assign(?lhs, ?rhs, ?a)) {
alt (lhs.node) {
case (expr_path(?p, ?a_lhs)) {
gen_if_local(fcx, lhs, rhs, a, a_lhs);
gen_if_local(fcx, lhs, rhs, a, a_lhs);
}
case (_) {
find_pre_post_exprs(fcx, [lhs, rhs], a);
@ -353,7 +361,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
case (expr_recv(?lhs, ?rhs, ?a)) {
alt (lhs.node) {
case (expr_path(?p, ?a_lhs)) {
gen_if_local(fcx, lhs, rhs, a, a_lhs);
gen_if_local(fcx, lhs, rhs, a, a_lhs);
}
case (_) {
// doesn't check that lhs is an lval, but
@ -368,63 +376,65 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
find_pre_post_exprs(fcx, [lhs, rhs], a);
}
case (expr_lit(_,?a)) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
clear_pp(expr_pp(fcx.ccx, e));
}
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)));
clear_precond(fcx.ccx, a);
set_postcond_false(fcx.ccx, a);
}
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);
set_precondition(ann_to_ts_ann(fcx.ccx, a),
expr_precond(fcx.ccx, ret_val));
set_postcond_false(fcx.ccx, a);
}
}
}
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)));
set_pre_and_post(fcx.ccx, a,
expr_prestate(fcx.ccx, e),
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]) {
log "333";
auto precond_res = seq_preconds(enclosing,
[expr_pp(antec),
block_pp(conseq)]);
set_pre_and_post(a, rec(precondition=precond_res,
postcondition=
expr_poststate(antec)));
[expr_pp(fcx.ccx, antec),
block_pp(fcx.ccx, conseq)]);
set_pre_and_post(fcx.ccx, a, precond_res,
expr_poststate(fcx.ccx, antec));
}
case (some[@expr](?altern)) {
find_pre_post_expr(fcx, altern);
log "444";
auto precond_true_case =
seq_preconds(enclosing,
[expr_pp(antec), block_pp(conseq)]);
[expr_pp(fcx.ccx, antec),
block_pp(fcx.ccx, conseq)]);
auto postcond_true_case = union_postconds
(num_local_vars,
[expr_postcond(antec), block_postcond(conseq)]);
[expr_postcond(fcx.ccx, antec),
block_postcond(fcx.ccx, conseq)]);
log "555";
auto precond_false_case = seq_preconds
(enclosing,
[expr_pp(antec), expr_pp(altern)]);
[expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
auto postcond_false_case = union_postconds
(num_local_vars,
[expr_postcond(antec), expr_postcond(altern)]);
[expr_postcond(fcx.ccx, antec),
expr_postcond(fcx.ccx, altern)]);
auto precond_res = union_postconds
(num_local_vars,
[precond_true_case, precond_false_case]);
auto postcond_res = intersect_postconds
([postcond_true_case, postcond_false_case]);
set_pre_and_post(a, rec(precondition=precond_res,
postcondition=postcond_res));
set_pre_and_post(fcx.ccx, a, precond_res, postcond_res);
}
}
}
@ -438,41 +448,42 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
}
case (expr_unary(_,?operand,?a)) {
find_pre_post_expr(fcx, operand);
set_pre_and_post(a, expr_pp(operand));
copy_pre_post(fcx.ccx, a, operand);
}
case (expr_cast(?operand, _, ?a)) {
find_pre_post_expr(fcx, operand);
set_pre_and_post(a, expr_pp(operand));
copy_pre_post(fcx.ccx, a, 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=
log "666";
set_pre_and_post(fcx.ccx, a,
seq_preconds(enclosing,
[expr_pp(test),
block_pp(body)]),
postcondition=
intersect_postconds([expr_postcond(test),
block_postcond(body)])));
[expr_pp(fcx.ccx, test),
block_pp(fcx.ccx, body)]),
intersect_postconds([expr_postcond(fcx.ccx, test),
block_postcond(fcx.ccx, 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,
[block_postcond(body), expr_postcond(test)]);
[block_postcond(fcx.ccx, body),
expr_postcond(fcx.ccx, 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,
[block_pp(body),
expr_pp(test)]),
postcondition=loop_postcond));
log "777";
set_pre_and_post(fcx.ccx, a,
seq_preconds(enclosing,
[block_pp(fcx.ccx, body),
expr_pp(fcx.ccx, test)]),
loop_postcond);
}
case (expr_for(?d, ?index, ?body, ?a)) {
find_pre_post_loop(fcx, d, index, body, a);
@ -487,47 +498,49 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
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);
ret block_pp(fcx.ccx, 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 {
log "777";
union(pp.precondition, seq_preconds(enclosing,
[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),
auto antec_pp = pp_clone(expr_pp(fcx.ccx, 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);
set_pre_and_post(fcx.ccx, a, alts_overall_pp.precondition,
alts_overall_pp.postcondition);
}
case (expr_field(?operator, _, ?a)) {
find_pre_post_expr(fcx, operator);
set_pre_and_post(a, expr_pp(operator));
copy_pre_post(fcx.ccx, a, operator);
}
case (expr_fail(?a)) {
set_pre_and_post(a,
set_pre_and_post(fcx.ccx, a,
/* if execution continues after fail,
then everything is true! */
rec(precondition=empty_prestate(num_local_vars),
postcondition=false_postcond(num_local_vars)));
empty_prestate(num_local_vars),
false_postcond(num_local_vars));
}
case (expr_assert(?p, ?a)) {
find_pre_post_expr(fcx, p);
set_pre_and_post(a, expr_pp(p));
copy_pre_post(fcx.ccx, a, 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));
copy_pre_post(fcx.ccx, a, p);
}
case(expr_bind(?operator, ?maybe_args, ?a)) {
auto args = vec::cat_options[@expr](maybe_args);
@ -535,17 +548,17 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
find_pre_post_exprs(fcx, args, a);
}
case (expr_break(?a)) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
clear_pp(expr_pp(fcx.ccx, e));
}
case (expr_cont(?a)) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
clear_pp(expr_pp(fcx.ccx, e));
}
case (expr_port(?a)) {
set_pre_and_post(a, empty_pre_post(num_local_vars));
clear_pp(expr_pp(fcx.ccx, e));
}
case (expr_ext(_, _, _, ?expanded, ?a)) {
find_pre_post_expr(fcx, expanded);
set_pre_and_post(a, expr_pp(expanded));
copy_pre_post(fcx.ccx, a, expanded);
}
}
}
@ -565,12 +578,11 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
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);
copy_pre_post(fcx.ccx, alocal.ann, an_init.expr);
/* Inherit ann from initializer, and add var being
initialized to the postcondition */
set_pre_and_post(a, rhs_pp);
copy_pre_post(fcx.ccx, a, an_init.expr);
/* log("gen (decl):");
log_stmt(s); */
gen(fcx, a, alocal.id);
@ -580,22 +592,21 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
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);
clear_pp(ann_to_ts_ann(fcx.ccx,
alocal.ann).conditions);
clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
}
}
}
case(decl_item(?anitem)) {
auto pp = empty_pre_post(num_local_vars);
set_pre_and_post(a, pp);
clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
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));
copy_pre_post(fcx.ccx, a, e);
}
}
}
@ -624,7 +635,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
log("pre_post for stmt:");
log_stmt(*s);
log("is:");
log_pp(stmt_pp(*s));
log_pp(stmt_pp(fcx.ccx, *s));
}
auto do_one = bind do_one_(fcx, _);
@ -637,15 +648,15 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
let vec[pre_and_post] pps = [];
fn get_pp_stmt(&@stmt s) -> pre_and_post {
ret stmt_pp(*s);
fn get_pp_stmt(crate_ctxt ccx, &@stmt s) -> pre_and_post {
ret stmt_pp(ccx, *s);
}
auto f = get_pp_stmt;
auto f = bind get_pp_stmt(fcx.ccx,_);
pps += vec::map[@stmt, pre_and_post](f, b.node.stmts);
fn get_pp_expr(&@expr e) -> pre_and_post {
ret expr_pp(e);
fn get_pp_expr(crate_ctxt ccx, &@expr e) -> pre_and_post {
ret expr_pp(ccx, e);
}
auto g = get_pp_expr;
auto g = bind get_pp_expr(fcx.ccx, _);
plus_option[pre_and_post](pps,
option::map[@expr, pre_and_post](g, b.node.expr));
@ -661,8 +672,7 @@ fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
block_postcond = union_postconds(nv, postconds);
}
set_pre_and_post(b.node.a, rec(precondition=block_precond,
postcondition=block_postcond));
set_pre_and_post(fcx.ccx, b.node.a, block_precond, block_postcond);
}
fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {

396
src/comp/middle/tstate/states.rs
View file

@ -17,7 +17,6 @@ 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;
@ -181,7 +180,7 @@ fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs)
for (@expr e in exprs) {
changed = find_pre_post_state_expr(fcx, post, e) || changed;
post = expr_poststate(e);
post = expr_poststate(fcx.ccx, e);
}
ret tup(changed, post);
@ -191,8 +190,8 @@ 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a, res._1) || changed;
ret changed;
}
@ -201,16 +200,16 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@decl d,
auto changed = false;
/* same issues as while */
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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([expr_poststate(index),
block_poststate(body)]);
changed = find_pre_post_state_block(fcx,
expr_poststate(fcx.ccx, index), body) || changed;
auto res_p = intersect_postconds([expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body)]);
changed = extend_poststate_ann(a, res_p) || changed;
changed = extend_poststate_ann(fcx.ccx, a, res_p) || changed;
ret changed;
}
@ -245,83 +244,85 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|| changed;
/* rands go left-to-right */
changed = find_pre_post_state_exprs(fcx,
expr_poststate(operator), a, operands)
|| changed;
expr_poststate(fcx.ccx, 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;
/*
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);
*/
}
/* 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)
expr_poststate(fcx.ccx, 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);
expr_poststate(fcx.ccx, operator), a,
cat_options[@expr](maybe_args)) || changed);
}
case (expr_path(_,?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, arg)) || changed;
ret changed;
}
case (none[@expr]) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, a, pres);
}
}
}
case (expr_lit(?l,?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
block_poststate(fcx.ccx, b)) || changed;
ret changed;
}
case (expr_rec(?fields,?maybe_base,?a)) {
@ -332,23 +333,23 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
case (some[@expr](?base)) {
changed = find_pre_post_state_expr(fcx, pres, base)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(base))
|| changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, base)) || changed;
}
}
ret changed;
}
case (expr_assign(?lhs, ?rhs, ?a)) {
extend_prestate_ann(a, pres);
extend_prestate_ann(fcx.ccx, a, pres);
alt (lhs.node) {
case (expr_path(?p, ?a_lhs)) {
// assignment to local var
changed = pure_exp(a_lhs, pres) || changed;
changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
changed = find_pre_post_state_expr(fcx, pres, rhs)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(rhs))
|| changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, rhs)) || changed;
changed = gen_if_local(fcx, a_lhs, a)|| changed;
}
case (_) {
@ -356,24 +357,24 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
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;
expr_poststate(fcx.ccx, lhs), rhs) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, rhs)) || changed;
}
}
ret changed;
}
case (expr_recv(?lhs, ?rhs, ?a)) {
extend_prestate_ann(a, pres);
extend_prestate_ann(fcx.ccx, a, pres);
alt (lhs.node) {
case (expr_path(?p, ?a_lhs)) {
// receive to local var
changed = pure_exp(a_lhs, pres) || changed;
changed = pure_exp(fcx.ccx, a_lhs, pres) || changed;
changed = find_pre_post_state_expr(fcx, pres, rhs)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(rhs))
|| changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, rhs)) || changed;
changed = gen_if_local(fcx, a_lhs, a) || changed;
}
case (_) {
@ -381,17 +382,17 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
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;
expr_poststate(fcx.ccx, lhs), rhs) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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));
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
set_poststate_ann(fcx.ccx, a, false_postcond(num_local_vars));
alt(maybe_ret_val) {
case (none[@expr]) { /* do nothing */ }
case (some[@expr](?ret_val)) {
@ -402,28 +403,30 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
ret changed;
}
case (expr_be(?e, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
set_poststate_ann(a, false_postcond(num_local_vars));
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
set_poststate_ann(fcx.ccx, 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 = extend_prestate_ann(fcx.ccx, 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;
expr_poststate(fcx.ccx, antec), conseq) || changed;
alt (maybe_alt) {
case (none[@expr]) {
changed = extend_poststate_ann(a, expr_poststate(antec))
|| changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, antec)) || changed;
}
case (some[@expr](?altern)) {
changed = find_pre_post_state_expr(fcx,
expr_poststate(antec), altern) || changed;
expr_poststate(fcx.ccx, antec), altern) || changed;
auto poststate_res = intersect_postconds
([block_poststate(conseq), expr_poststate(altern)]);
changed = extend_poststate_ann(a, poststate_res) || changed;
([block_poststate(fcx.ccx, conseq),
expr_poststate(fcx.ccx, altern)]);
changed = extend_poststate_ann(fcx.ccx, a, poststate_res)
|| changed;
}
}
log("if:");
@ -431,41 +434,44 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
log("new prestate:");
log_bitv(fcx.enclosing, pres);
log("new poststate:");
log_bitv(fcx.enclosing, expr_poststate(e));
log_bitv(fcx.enclosing, expr_poststate(fcx.ccx, e));
ret changed;
}
case (expr_binary(?bop, ?l, ?r, ?a)) {
/* FIXME: what if bop is lazy? */
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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 = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, r)) || changed;
ret changed;
}
case (expr_send(?l, ?r, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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 = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, l), r)
|| changed;
changed = extend_poststate_ann(a, expr_poststate(r)) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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 = extend_prestate_ann(fcx.ccx, 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;
changed = find_pre_post_state_expr(fcx,
expr_poststate(fcx.ccx, lhs), rhs) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, rhs)) || changed;
ret changed;
}
case (expr_while(?test, ?body, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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));
@ -476,30 +482,30 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
*/
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([expr_poststate(test),
block_poststate(body)])) || changed;
changed = find_pre_post_state_block(fcx,
expr_poststate(fcx.ccx, test), body) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
intersect_postconds([expr_poststate(fcx.ccx, test),
block_poststate(fcx.ccx, body)])) || changed;
ret changed;
}
case (expr_do_while(?body, ?test, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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;
block_poststate(fcx.ccx, 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;
changed = set_poststate_ann(fcx.ccx, a, pres) || changed;
}
else {
changed = extend_poststate_ann(a, expr_poststate(test))
|| changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, test)) || changed;
}
ret changed;
@ -511,169 +517,174 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
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 = extend_prestate_ann(fcx.ccx, 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));
expr_poststate(fcx.ccx, e), sub) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, sub));
ret changed;
}
case (expr_alt(?e, ?alts, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
auto e_post = expr_poststate(e);
auto e_post = expr_poststate(fcx.ccx, 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;
changed = intersect(a_post,
block_poststate(fcx.ccx,
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);
changed = extend_poststate_ann(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, 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;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
changed = extend_poststate_ann(fcx.ccx, a,
expr_poststate(fcx.ccx, operand)) || changed;
ret changed;
}
case (expr_fail(?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
/* if execution continues after fail, then everything is true! woo! */
changed = set_poststate_ann(a, false_postcond(num_local_vars))
|| changed;
changed = set_poststate_ann(fcx.ccx, a,
false_postcond(num_local_vars)) || changed;
ret changed;
}
case (expr_assert(?p, ?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, a, pres);
}
case (expr_check(?p, ?a)) {
changed = extend_prestate_ann(a, pres) || changed;
changed = extend_prestate_ann(fcx.ccx, 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;
changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
ret changed;
}
case (expr_break(?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, a, pres);
}
case (expr_cont(?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, a, pres);
}
case (expr_port(?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, a, pres);
}
case (expr_self_method(_, ?a)) {
ret pure_exp(a, pres);
ret pure_exp(fcx.ccx, 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);
auto changed = false;
auto stmt_ann = stmt_to_ann(fcx.ccx, *s);
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;
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(fcx.ccx, 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(fcx.ccx, e))
|| changed;
changed = extend_poststate(stmt_ann.states.poststate,
expr_poststate(fcx.ccx, e)) || 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;
*/
ret changed;
}
case (_) { ret false; }
}
case (_) { ret false; }
}
}
/* Updates the pre- and post-states of statements in the block,
@ -692,7 +703,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
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);
pres = stmt_poststate(fcx.ccx, *s);
}
auto post = pres;
@ -701,7 +712,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
case (none[@expr]) {}
case (some[@expr](?e)) {
changed = find_pre_post_state_expr(fcx, pres, e) || changed;
post = expr_poststate(e);
post = expr_poststate(fcx.ccx, e);
}
}
@ -718,13 +729,13 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b)
post = pres0;
}
set_prestate_ann(b.node.a, pres0);
set_poststate_ann(b.node.a, post);
set_prestate_ann(fcx.ccx, b.node.a, pres0);
set_poststate_ann(fcx.ccx, b.node.a, post);
log("For block:");
log_block(b);
log("poststate = ");
log_states(block_states(b));
log_states(block_states(fcx.ccx, b));
log("pres0:");
log_bitv(fcx.enclosing, pres0);
log("post:");
@ -785,3 +796,14 @@ fn find_pre_post_state_item(&fn_ctxt fcx, @item i) -> bool {
}
}
}
//
// 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:
//

2
src/lib/bitv.rs
View file

@ -114,7 +114,7 @@ fn clear(&t v) {
}
fn set_all(&t v) {
for each (uint i in _uint::range(0u, v.nbits)) {
for each (uint i in uint::range(0u, v.nbits)) {
set(v, i, true);
}
}