2011-05-17 13:41:41 -05:00
|
|
|
import std::vec;
|
|
|
|
import std::vec::plus_option;
|
2011-05-14 21:02:30 -05:00
|
|
|
import std::option;
|
|
|
|
import std::option::none;
|
|
|
|
import std::option::some;
|
|
|
|
|
2011-06-09 11:56:35 -05:00
|
|
|
// FIXME: needs to be tstate::ann because ann is also a type name...
|
|
|
|
// that's probably a bug.
|
2011-05-14 21:02:30 -05:00
|
|
|
import tstate::ann::pre_and_post;
|
|
|
|
import tstate::ann::get_post;
|
|
|
|
import tstate::ann::postcond;
|
|
|
|
import tstate::ann::true_precond;
|
|
|
|
import tstate::ann::false_postcond;
|
|
|
|
import tstate::ann::empty_poststate;
|
2011-06-09 11:56:35 -05:00
|
|
|
import tstate::ann::require;
|
2011-05-14 21:02:30 -05:00
|
|
|
import tstate::ann::require_and_preserve;
|
|
|
|
import tstate::ann::union;
|
|
|
|
import tstate::ann::intersect;
|
|
|
|
import tstate::ann::pp_clone;
|
|
|
|
import tstate::ann::empty_prestate;
|
2011-05-18 17:43:05 -05:00
|
|
|
import tstate::ann::set_precondition;
|
|
|
|
import tstate::ann::set_postcondition;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::crate_ctxt;
|
|
|
|
import aux::fn_ctxt;
|
2011-06-01 20:10:10 -05:00
|
|
|
import aux::num_constraints;
|
|
|
|
import aux::constraint;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::expr_pp;
|
|
|
|
import aux::stmt_pp;
|
|
|
|
import aux::block_pp;
|
2011-05-18 17:43:05 -05:00
|
|
|
import aux::clear_pp;
|
|
|
|
import aux::clear_precond;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::set_pre_and_post;
|
2011-05-18 17:43:05 -05:00
|
|
|
import aux::copy_pre_post;
|
2011-05-14 21:02:30 -05:00
|
|
|
import aux::expr_precond;
|
|
|
|
import aux::expr_postcond;
|
|
|
|
import aux::expr_prestate;
|
|
|
|
import aux::expr_poststate;
|
|
|
|
import aux::block_postcond;
|
|
|
|
import aux::fn_info;
|
|
|
|
import aux::log_pp;
|
|
|
|
import aux::ann_to_def;
|
|
|
|
import aux::ann_to_def_strict;
|
2011-05-18 17:43:05 -05:00
|
|
|
import aux::ann_to_ts_ann;
|
|
|
|
import aux::set_postcond_false;
|
2011-05-27 22:41:48 -05:00
|
|
|
import aux::controlflow_expr;
|
2011-06-09 11:56:35 -05:00
|
|
|
import aux::expr_to_constr;
|
2011-06-13 20:10:33 -05:00
|
|
|
//import aux::constr_to_constr_occ;
|
2011-06-09 11:56:35 -05:00
|
|
|
import aux::constraints_expr;
|
|
|
|
import aux::substitute_constr_args;
|
2011-06-13 20:10:33 -05:00
|
|
|
import aux::ninit;
|
|
|
|
import aux::npred;
|
|
|
|
import aux::path_to_ident;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
import bitvectors::seq_preconds;
|
|
|
|
import bitvectors::union_postconds;
|
|
|
|
import bitvectors::intersect_postconds;
|
|
|
|
import bitvectors::declare_var;
|
|
|
|
import bitvectors::bit_num;
|
|
|
|
import bitvectors::gen;
|
|
|
|
|
2011-05-31 20:24:06 -05:00
|
|
|
import front::ast::*;
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-05-31 14:24:18 -05:00
|
|
|
import middle::ty::expr_ann;
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
import util::common::new_def_hash;
|
|
|
|
import util::common::decl_lhs;
|
|
|
|
import util::common::uistr;
|
|
|
|
import util::common::log_expr;
|
|
|
|
import util::common::log_fn;
|
|
|
|
import util::common::elt_exprs;
|
|
|
|
import util::common::field_exprs;
|
|
|
|
import util::common::has_nonlocal_exits;
|
|
|
|
import util::common::log_stmt;
|
|
|
|
import util::common::log_expr_err;
|
2011-05-18 17:43:05 -05:00
|
|
|
import util::common::log_block_err;
|
|
|
|
import util::common::log_block;
|
2011-05-31 20:24:06 -05:00
|
|
|
import util::common::span;
|
2011-05-26 18:02:25 -05:00
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
fn find_pre_post_mod(&_mod m) -> _mod {
|
|
|
|
log("implement find_pre_post_mod!");
|
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_native_mod(&native_mod m) -> native_mod {
|
|
|
|
log("implement find_pre_post_native_mod");
|
|
|
|
fail;
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
fn find_pre_post_obj(&crate_ctxt ccx, _obj o) -> () {
|
|
|
|
fn do_a_method(crate_ctxt ccx, &@method m) -> () {
|
|
|
|
assert (ccx.fm.contains_key(m.node.id));
|
|
|
|
let fn_ctxt fcx = rec(enclosing=ccx.fm.get(m.node.id),
|
|
|
|
id=m.node.id, name=m.node.ident, ccx=ccx);
|
|
|
|
find_pre_post_fn(fcx, m.node.meth);
|
|
|
|
}
|
|
|
|
auto f = bind do_a_method(ccx,_);
|
2011-05-17 13:41:41 -05:00
|
|
|
vec::map[@method, ()](f, o.methods);
|
2011-05-14 21:02:30 -05:00
|
|
|
option::map[@method, ()](f, o.dtor);
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_item(&crate_ctxt ccx, &item i) -> () {
|
|
|
|
alt (i.node) {
|
|
|
|
case (item_const(?id, ?t, ?e, ?di, ?a)) {
|
|
|
|
// make a fake fcx
|
2011-06-01 20:10:10 -05:00
|
|
|
auto fake_fcx = rec(enclosing=
|
|
|
|
rec(constrs=@new_def_hash[constraint](),
|
|
|
|
num_constraints=0u,
|
|
|
|
cf=return),
|
2011-05-14 21:02:30 -05:00
|
|
|
id=tup(0,0),
|
|
|
|
name="",
|
|
|
|
ccx=ccx);
|
|
|
|
find_pre_post_expr(fake_fcx, e);
|
|
|
|
}
|
|
|
|
case (item_fn(?id, ?f, ?ps, ?di, ?a)) {
|
|
|
|
assert (ccx.fm.contains_key(di));
|
|
|
|
auto fcx = rec(enclosing=ccx.fm.get(di),
|
|
|
|
id=di, name=id, ccx=ccx);
|
|
|
|
find_pre_post_fn(fcx, f);
|
|
|
|
}
|
|
|
|
case (item_mod(?id, ?m, ?di)) {
|
|
|
|
find_pre_post_mod(m);
|
|
|
|
}
|
|
|
|
case (item_native_mod(?id, ?nm, ?di)) {
|
|
|
|
find_pre_post_native_mod(nm);
|
|
|
|
}
|
|
|
|
case (item_ty(_,_,_,_,_)) {
|
|
|
|
ret;
|
|
|
|
}
|
|
|
|
case (item_tag(_,_,_,_,_)) {
|
|
|
|
ret;
|
|
|
|
}
|
|
|
|
case (item_obj(?id, ?o, ?ps, ?di, ?a)) {
|
|
|
|
find_pre_post_obj(ccx, o);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/* Finds the pre and postcondition for each expr in <args>;
|
|
|
|
sets the precondition in a to be the result of combining
|
|
|
|
the preconditions for <args>, and the postcondition in a to
|
|
|
|
be the union of all postconditions for <args> */
|
|
|
|
fn find_pre_post_exprs(&fn_ctxt fcx, &vec[@expr] args, ann a) {
|
2011-05-18 17:43:05 -05:00
|
|
|
if (vec::len[@expr](args) > 0u) {
|
|
|
|
log ("find_pre_post_exprs: oper =");
|
|
|
|
log_expr(*(args.(0)));
|
|
|
|
}
|
|
|
|
|
2011-05-14 21:02:30 -05:00
|
|
|
auto enclosing = fcx.enclosing;
|
|
|
|
auto fm = fcx.ccx.fm;
|
2011-06-01 20:10:10 -05:00
|
|
|
auto nv = num_constraints(enclosing);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
fn do_one(fn_ctxt fcx, &@expr e) -> () {
|
|
|
|
find_pre_post_expr(fcx, e);
|
|
|
|
}
|
|
|
|
auto f = bind do_one(fcx, _);
|
|
|
|
|
2011-05-17 13:41:41 -05:00
|
|
|
vec::map[@expr, ()](f, args);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
fn get_pp(crate_ctxt ccx, &@expr e) -> pre_and_post {
|
|
|
|
ret expr_pp(ccx, e);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-18 17:43:05 -05:00
|
|
|
|
|
|
|
auto g = bind get_pp(fcx.ccx, _);
|
2011-05-17 13:41:41 -05:00
|
|
|
auto pps = vec::map[@expr, pre_and_post](g, args);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto h = get_post;
|
|
|
|
|
2011-05-26 18:02:25 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a, seq_preconds(fcx, pps),
|
2011-05-18 17:43:05 -05:00
|
|
|
union_postconds
|
|
|
|
(nv, (vec::map[pre_and_post, postcond](h, pps))));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-06-13 19:04:15 -05:00
|
|
|
fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index,
|
2011-05-14 21:02:30 -05:00
|
|
|
&block body, &ann a) -> () {
|
|
|
|
find_pre_post_expr(fcx, index);
|
|
|
|
find_pre_post_block(fcx, body);
|
2011-06-13 20:10:33 -05:00
|
|
|
auto loop_precond = declare_var(fcx, rec(id=l.node.id,
|
|
|
|
c=ninit(l.node.ident)),
|
2011-05-26 18:02:25 -05:00
|
|
|
seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]));
|
2011-05-14 21:02:30 -05:00
|
|
|
auto loop_postcond = intersect_postconds
|
2011-05-18 17:43:05 -05:00
|
|
|
([expr_postcond(fcx.ccx, index), block_postcond(fcx.ccx, body)]);
|
|
|
|
set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs,
|
2011-06-13 20:10:33 -05:00
|
|
|
&ann larger_ann, &ann new_var, &path pth) -> () {
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (ann_to_def(fcx.ccx, new_var)) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?d)) {
|
2011-05-26 18:02:25 -05:00
|
|
|
alt (d) {
|
|
|
|
case (def_local(?d_id)) {
|
|
|
|
find_pre_post_expr(fcx, rhs);
|
|
|
|
auto p = expr_pp(fcx.ccx, rhs);
|
|
|
|
set_pre_and_post(fcx.ccx, larger_ann,
|
|
|
|
p.precondition, p.postcondition);
|
2011-06-13 20:10:33 -05:00
|
|
|
gen(fcx, larger_ann, rec(id=d_id,
|
|
|
|
c=ninit(path_to_ident(fcx.ccx.tcx, pth))));
|
2011-05-26 18:02:25 -05:00
|
|
|
}
|
|
|
|
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
|
|
|
|
}
|
|
|
|
}
|
2011-05-16 21:04:45 -05:00
|
|
|
case (_) { find_pre_post_exprs(fcx, [lhs, rhs], larger_ann); }
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
/* Fills in annotations as a side effect. Does not rebuild the expr */
|
|
|
|
fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
|
|
|
|
auto enclosing = fcx.enclosing;
|
2011-06-01 20:10:10 -05:00
|
|
|
auto num_local_vars = num_constraints(enclosing);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
fn do_rand_(fn_ctxt fcx, &@expr e) -> () {
|
|
|
|
find_pre_post_expr(fcx, e);
|
|
|
|
}
|
|
|
|
|
2011-06-01 20:10:10 -05:00
|
|
|
log("find_pre_post_expr (num_constraints =" +
|
2011-05-14 21:02:30 -05:00
|
|
|
uistr(num_local_vars) + "):");
|
2011-05-18 17:43:05 -05:00
|
|
|
log_expr(*e);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
alt (e.node) {
|
|
|
|
case (expr_call(?operator, ?operands, ?a)) {
|
2011-05-17 13:41:41 -05:00
|
|
|
auto args = vec::clone[@expr](operands);
|
|
|
|
vec::push[@expr](args, operator);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_exprs(fcx, args, a);
|
2011-06-10 21:12:42 -05:00
|
|
|
|
|
|
|
/* should test higher-order constrained functions */
|
|
|
|
/* FIXME */
|
|
|
|
|
2011-06-09 11:56:35 -05:00
|
|
|
/* see if the call has any constraints on its in type */
|
2011-06-10 21:12:42 -05:00
|
|
|
log("a function: " );
|
|
|
|
log_expr(*operator);
|
|
|
|
auto pp = expr_pp(fcx.ccx, e);
|
|
|
|
for (@constr c in constraints_expr(fcx.ccx.tcx, operator)) {
|
|
|
|
auto id = ann_to_def(fcx.ccx, c.node.ann);
|
|
|
|
alt (id) {
|
|
|
|
case (some(def_fn(?d_id))) {
|
2011-06-13 20:10:33 -05:00
|
|
|
auto i = bit_num(fcx, rec(id=d_id,
|
|
|
|
c=substitute_constr_args(fcx.ccx.tcx,
|
|
|
|
operands, c)));
|
2011-06-09 11:56:35 -05:00
|
|
|
require(i, pp);
|
|
|
|
}
|
2011-06-10 21:12:42 -05:00
|
|
|
case (_) {
|
|
|
|
fcx.ccx.tcx.sess.span_err(c.span, "Unbound pred "
|
|
|
|
+ " or pred that's not bound to a function");
|
|
|
|
}
|
2011-06-09 11:56:35 -05:00
|
|
|
}
|
|
|
|
}
|
2011-06-10 21:12:42 -05:00
|
|
|
|
2011-06-09 11:56:35 -05:00
|
|
|
// FIXME: constraints on result type
|
|
|
|
|
2011-05-27 22:41:48 -05:00
|
|
|
/* if this is a failing call, its postcondition sets everything */
|
|
|
|
alt (controlflow_expr(fcx.ccx, operator)) {
|
|
|
|
case (noreturn) {
|
|
|
|
set_postcond_false(fcx.ccx, a);
|
|
|
|
}
|
|
|
|
case (_) { }
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_spawn(_, _, ?operator, ?operands, ?a)) {
|
2011-05-17 13:41:41 -05:00
|
|
|
auto args = vec::clone[@expr](operands);
|
|
|
|
vec::push[@expr](args, operator);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_exprs(fcx, args, a);
|
|
|
|
}
|
2011-06-09 19:11:21 -05:00
|
|
|
case (expr_vec(?args, _, _, ?a)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_exprs(fcx, args, a);
|
|
|
|
}
|
|
|
|
case (expr_tup(?elts, ?a)) {
|
|
|
|
find_pre_post_exprs(fcx, elt_exprs(elts), a);
|
|
|
|
}
|
|
|
|
case (expr_path(?p, ?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
auto res = expr_pp(fcx.ccx, e);
|
|
|
|
clear_pp(res);
|
|
|
|
|
2011-06-10 21:12:42 -05:00
|
|
|
auto df = ann_to_def_strict(fcx.ccx.tcx, a);
|
2011-05-14 21:02:30 -05:00
|
|
|
alt (df) {
|
|
|
|
case (def_local(?d_id)) {
|
2011-06-13 20:10:33 -05:00
|
|
|
auto i = bit_num(fcx, rec(id=d_id,
|
|
|
|
c=ninit(path_to_ident(fcx.ccx.tcx, p))));
|
2011-05-14 21:02:30 -05:00
|
|
|
require_and_preserve(i, res);
|
|
|
|
}
|
|
|
|
case (_) { /* nothing to check */ }
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (expr_self_method(?v, ?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case(expr_log(_, ?arg, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_chan(?arg, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case(expr_put(?opt, ?a)) {
|
|
|
|
alt (opt) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?arg)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, arg);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, arg);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-06-14 08:20:04 -05:00
|
|
|
// FIXME this was just put in here as a placeholder
|
|
|
|
case (expr_fn(?f, ?a)) {
|
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
case (expr_block(?b, ?a)) {
|
|
|
|
find_pre_post_block(fcx, b);
|
2011-05-18 17:43:05 -05:00
|
|
|
auto p = block_pp(fcx.ccx, b);
|
|
|
|
set_pre_and_post(fcx.ccx, a, p.precondition, p.postcondition);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_rec(?fields,?maybe_base,?a)) {
|
|
|
|
auto es = field_exprs(fields);
|
2011-05-17 13:41:41 -05:00
|
|
|
vec::plus_option[@expr](es, maybe_base);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_exprs(fcx, es, a);
|
|
|
|
}
|
2011-05-27 19:38:52 -05:00
|
|
|
case (expr_move(?lhs, ?rhs, ?a)) {
|
|
|
|
// FIXME: this needs to deinitialize the rhs
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p, ?a_lhs)) {
|
2011-06-13 20:10:33 -05:00
|
|
|
gen_if_local(fcx, lhs, rhs, a, a_lhs, p);
|
2011-05-27 19:38:52 -05:00
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
find_pre_post_exprs(fcx, [lhs, rhs], a);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
case (expr_assign(?lhs, ?rhs, ?a)) {
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p, ?a_lhs)) {
|
2011-06-13 20:10:33 -05:00
|
|
|
gen_if_local(fcx, lhs, rhs, a, a_lhs, p);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (_) {
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [lhs, rhs], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (expr_recv(?lhs, ?rhs, ?a)) {
|
|
|
|
alt (lhs.node) {
|
|
|
|
case (expr_path(?p, ?a_lhs)) {
|
2011-06-13 20:10:33 -05:00
|
|
|
gen_if_local(fcx, lhs, rhs, a, a_lhs, p);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (_) {
|
|
|
|
// doesn't check that lhs is an lval, but
|
|
|
|
// that's probably ok
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [lhs, rhs], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (expr_assign_op(_, ?lhs, ?rhs, ?a)) {
|
|
|
|
/* Different from expr_assign in that the lhs *must*
|
|
|
|
already be initialized */
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [lhs, rhs], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_lit(_,?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_ret(?maybe_val, ?a)) {
|
|
|
|
alt (maybe_val) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_precond(fcx.ccx, a);
|
|
|
|
set_postcond_false(fcx.ccx, a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?ret_val)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, ret_val);
|
2011-05-18 17:43:05 -05:00
|
|
|
set_precondition(ann_to_ts_ann(fcx.ccx, a),
|
|
|
|
expr_precond(fcx.ccx, ret_val));
|
|
|
|
set_postcond_false(fcx.ccx, a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (expr_be(?e, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, e);
|
2011-05-18 17:43:05 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a,
|
|
|
|
expr_prestate(fcx.ccx, e),
|
|
|
|
false_postcond(num_local_vars));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, antec);
|
|
|
|
find_pre_post_block(fcx, conseq);
|
|
|
|
alt (maybe_alt) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-05-18 17:43:05 -05:00
|
|
|
log "333";
|
2011-05-26 18:02:25 -05:00
|
|
|
auto precond_res = seq_preconds(fcx,
|
2011-05-18 17:43:05 -05:00
|
|
|
[expr_pp(fcx.ccx, antec),
|
|
|
|
block_pp(fcx.ccx, conseq)]);
|
|
|
|
set_pre_and_post(fcx.ccx, a, precond_res,
|
|
|
|
expr_poststate(fcx.ccx, antec));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?altern)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, altern);
|
2011-05-18 17:43:05 -05:00
|
|
|
log "444";
|
2011-05-14 21:02:30 -05:00
|
|
|
auto precond_true_case =
|
2011-05-26 18:02:25 -05:00
|
|
|
seq_preconds(fcx, [expr_pp(fcx.ccx, antec),
|
|
|
|
block_pp(fcx.ccx, conseq)]);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto postcond_true_case = union_postconds
|
|
|
|
(num_local_vars,
|
2011-05-18 17:43:05 -05:00
|
|
|
[expr_postcond(fcx.ccx, antec),
|
|
|
|
block_postcond(fcx.ccx, conseq)]);
|
|
|
|
log "555";
|
2011-05-14 21:02:30 -05:00
|
|
|
auto precond_false_case = seq_preconds
|
2011-05-26 18:02:25 -05:00
|
|
|
(fcx, [expr_pp(fcx.ccx, antec),
|
|
|
|
expr_pp(fcx.ccx, altern)]);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto postcond_false_case = union_postconds
|
|
|
|
(num_local_vars,
|
2011-05-18 17:43:05 -05:00
|
|
|
[expr_postcond(fcx.ccx, antec),
|
|
|
|
expr_postcond(fcx.ccx, altern)]);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto precond_res = union_postconds
|
|
|
|
(num_local_vars,
|
2011-05-16 21:04:45 -05:00
|
|
|
[precond_true_case, precond_false_case]);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto postcond_res = intersect_postconds
|
2011-05-16 21:04:45 -05:00
|
|
|
([postcond_true_case, postcond_false_case]);
|
2011-05-18 17:43:05 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a, precond_res, postcond_res);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case (expr_binary(?bop,?l,?r,?a)) {
|
|
|
|
/* *unless* bop is lazy (e.g. and, or)?
|
|
|
|
FIXME */
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [l, r], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_send(?l, ?r, ?a)) {
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [l, r], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_unary(_,?operand,?a)) {
|
|
|
|
find_pre_post_expr(fcx, operand);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, operand);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_cast(?operand, _, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, operand);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, operand);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_while(?test, ?body, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, test);
|
|
|
|
find_pre_post_block(fcx, body);
|
2011-05-18 17:43:05 -05:00
|
|
|
log "666";
|
|
|
|
set_pre_and_post(fcx.ccx, a,
|
2011-05-26 18:02:25 -05:00
|
|
|
seq_preconds(fcx,
|
2011-05-18 17:43:05 -05:00
|
|
|
[expr_pp(fcx.ccx, test),
|
|
|
|
block_pp(fcx.ccx, body)]),
|
|
|
|
intersect_postconds([expr_postcond(fcx.ccx, test),
|
|
|
|
block_postcond(fcx.ccx, body)]));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
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,
|
2011-05-18 17:43:05 -05:00
|
|
|
[block_postcond(fcx.ccx, body),
|
|
|
|
expr_postcond(fcx.ccx, test)]);
|
2011-05-14 21:02:30 -05:00
|
|
|
/* 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);
|
|
|
|
}
|
|
|
|
|
2011-06-13 19:04:15 -05:00
|
|
|
|
2011-05-26 18:02:25 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a, seq_preconds(fcx,
|
2011-06-13 19:04:15 -05:00
|
|
|
[block_pp(fcx.ccx, body),
|
|
|
|
expr_pp(fcx.ccx, test)]),
|
|
|
|
loop_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_for(?d, ?index, ?body, ?a)) {
|
|
|
|
find_pre_post_loop(fcx, d, index, body, a);
|
|
|
|
}
|
|
|
|
case (expr_for_each(?d, ?index, ?body, ?a)) {
|
|
|
|
find_pre_post_loop(fcx, d, index, body, a);
|
|
|
|
}
|
|
|
|
case (expr_index(?e, ?sub, ?a)) {
|
2011-05-16 21:04:45 -05:00
|
|
|
find_pre_post_exprs(fcx, [e, sub], a);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-27 22:41:48 -05:00
|
|
|
case (expr_alt(?ex, ?alts, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, ex);
|
2011-05-14 21:02:30 -05:00
|
|
|
fn do_an_alt(&fn_ctxt fcx, &arm an_alt) -> pre_and_post {
|
|
|
|
find_pre_post_block(fcx, an_alt.block);
|
2011-05-18 17:43:05 -05:00
|
|
|
ret block_pp(fcx.ccx, an_alt.block);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
auto f = bind do_an_alt(fcx, _);
|
2011-05-17 13:41:41 -05:00
|
|
|
auto alt_pps = vec::map[arm, pre_and_post](f, alts);
|
2011-05-26 18:02:25 -05:00
|
|
|
fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp,
|
2011-05-14 21:02:30 -05:00
|
|
|
&pre_and_post next) -> pre_and_post {
|
2011-05-18 17:43:05 -05:00
|
|
|
log "777";
|
2011-05-26 18:02:25 -05:00
|
|
|
union(pp.precondition, seq_preconds(fcx, [antec, next]));
|
2011-05-14 21:02:30 -05:00
|
|
|
intersect(pp.postcondition, next.postcondition);
|
|
|
|
ret pp;
|
|
|
|
}
|
2011-05-27 22:41:48 -05:00
|
|
|
auto antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
|
2011-05-18 17:43:05 -05:00
|
|
|
auto e_pp = @rec(precondition=empty_prestate(num_local_vars),
|
2011-05-14 21:02:30 -05:00
|
|
|
postcondition=false_postcond(num_local_vars));
|
2011-05-26 18:02:25 -05:00
|
|
|
auto g = bind combine_pp(antec_pp, fcx, _, _);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-05-17 13:41:41 -05:00
|
|
|
auto alts_overall_pp = vec::foldl[pre_and_post, pre_and_post]
|
2011-05-14 21:02:30 -05:00
|
|
|
(g, e_pp, alt_pps);
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a, alts_overall_pp.precondition,
|
|
|
|
alts_overall_pp.postcondition);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_field(?operator, _, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, operator);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, operator);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-06-08 02:58:52 -05:00
|
|
|
case (expr_fail(?a, _)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
set_pre_and_post(fcx.ccx, a,
|
2011-05-14 21:02:30 -05:00
|
|
|
/* if execution continues after fail,
|
|
|
|
then everything is true! */
|
2011-05-18 17:43:05 -05:00
|
|
|
empty_prestate(num_local_vars),
|
|
|
|
false_postcond(num_local_vars));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_assert(?p, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, p);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, p);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_check(?p, ?a)) {
|
2011-06-09 11:56:35 -05:00
|
|
|
/* FIXME: Can we bypass this by having a
|
|
|
|
node-id-to-constr_occ table? */
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, p);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, p);
|
2011-06-09 11:56:35 -05:00
|
|
|
/* predicate p holds after this expression executes */
|
2011-06-10 21:12:42 -05:00
|
|
|
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
|
2011-06-13 20:10:33 -05:00
|
|
|
gen(fcx, a, c.node);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case(expr_bind(?operator, ?maybe_args, ?a)) {
|
2011-05-17 13:41:41 -05:00
|
|
|
auto args = vec::cat_options[@expr](maybe_args);
|
|
|
|
vec::push[@expr](args, operator); /* ??? order of eval? */
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_exprs(fcx, args, a);
|
|
|
|
}
|
|
|
|
case (expr_break(?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_cont(?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_port(?a)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
case (expr_ext(_, _, _, ?expanded, ?a)) {
|
|
|
|
find_pre_post_expr(fcx, expanded);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, expanded);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-20 19:41:36 -05:00
|
|
|
case (expr_anon_obj(?anon_obj, _, _, ?a)) {
|
|
|
|
alt (anon_obj.with_obj) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case (some(?ex)) {
|
2011-05-20 19:41:36 -05:00
|
|
|
find_pre_post_expr(fcx, ex);
|
|
|
|
copy_pre_post(fcx.ccx, a, ex);
|
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case (none) {
|
2011-05-20 19:41:36 -05:00
|
|
|
clear_pp(expr_pp(fcx.ccx, e));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s)
|
|
|
|
-> () {
|
|
|
|
log("stmt =");
|
|
|
|
log_stmt(s);
|
|
|
|
|
|
|
|
auto enclosing = fcx.enclosing;
|
2011-06-01 20:10:10 -05:00
|
|
|
auto num_local_vars = num_constraints(enclosing);
|
2011-05-14 21:02:30 -05:00
|
|
|
alt(s.node) {
|
|
|
|
case(stmt_decl(?adecl, ?a)) {
|
|
|
|
alt(adecl.node) {
|
|
|
|
case(decl_local(?alocal)) {
|
|
|
|
alt(alocal.init) {
|
2011-05-30 23:39:19 -05:00
|
|
|
case(some(?an_init)) {
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_expr(fcx, an_init.expr);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, alocal.ann, an_init.expr);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
/* Inherit ann from initializer, and add var being
|
|
|
|
initialized to the postcondition */
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, an_init.expr);
|
2011-06-13 20:10:33 -05:00
|
|
|
gen(fcx, a, rec(id=alocal.id,
|
|
|
|
c=ninit(alocal.ident)));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-30 23:39:19 -05:00
|
|
|
case(none) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(ann_to_ts_ann(fcx.ccx,
|
|
|
|
alocal.ann).conditions);
|
|
|
|
clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case(decl_item(?anitem)) {
|
2011-05-18 17:43:05 -05:00
|
|
|
clear_pp(ann_to_ts_ann(fcx.ccx, a).conditions);
|
2011-05-14 21:02:30 -05:00
|
|
|
find_pre_post_item(fcx.ccx, *anitem);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
case(stmt_expr(?e,?a)) {
|
|
|
|
find_pre_post_expr(fcx, e);
|
2011-05-18 17:43:05 -05:00
|
|
|
copy_pre_post(fcx.ccx, a, e);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_block(&fn_ctxt fcx, block b) -> () {
|
|
|
|
/* Want to say that if there is a break or cont in this
|
|
|
|
block, then that invalidates the poststate upheld by
|
|
|
|
any of the stmts after it.
|
|
|
|
Given that the typechecker has run, we know any break will be in
|
|
|
|
a block that forms a loop body. So that's ok. There'll never be an
|
|
|
|
expr_break outside a loop body, therefore, no expr_break outside a block.
|
|
|
|
*/
|
|
|
|
|
|
|
|
/* Conservative approximation for now: This says that if a block contains
|
|
|
|
*any* breaks or conts, then its postcondition doesn't promise anything.
|
|
|
|
This will mean that:
|
|
|
|
x = 0;
|
|
|
|
break;
|
|
|
|
|
|
|
|
won't have a postcondition that says x is initialized, but that's ok.
|
|
|
|
*/
|
2011-06-01 20:10:10 -05:00
|
|
|
auto nv = num_constraints(fcx.enclosing);
|
2011-05-14 21:02:30 -05:00
|
|
|
|
|
|
|
fn do_one_(fn_ctxt fcx, &@stmt s) -> () {
|
|
|
|
find_pre_post_stmt(fcx, *s);
|
|
|
|
log("pre_post for stmt:");
|
|
|
|
log_stmt(*s);
|
|
|
|
log("is:");
|
2011-05-18 17:43:05 -05:00
|
|
|
log_pp(stmt_pp(fcx.ccx, *s));
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
auto do_one = bind do_one_(fcx, _);
|
|
|
|
|
2011-05-17 13:41:41 -05:00
|
|
|
vec::map[@stmt, ()](do_one, b.node.stmts);
|
2011-05-14 21:02:30 -05:00
|
|
|
fn do_inner_(fn_ctxt fcx, &@expr e) -> () {
|
|
|
|
find_pre_post_expr(fcx, e);
|
|
|
|
}
|
|
|
|
auto do_inner = bind do_inner_(fcx, _);
|
|
|
|
option::map[@expr, ()](do_inner, b.node.expr);
|
|
|
|
|
2011-05-16 21:04:45 -05:00
|
|
|
let vec[pre_and_post] pps = [];
|
2011-05-14 21:02:30 -05:00
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
fn get_pp_stmt(crate_ctxt ccx, &@stmt s) -> pre_and_post {
|
|
|
|
ret stmt_pp(ccx, *s);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-18 17:43:05 -05:00
|
|
|
auto f = bind get_pp_stmt(fcx.ccx,_);
|
2011-05-17 13:41:41 -05:00
|
|
|
pps += vec::map[@stmt, pre_and_post](f, b.node.stmts);
|
2011-05-18 17:43:05 -05:00
|
|
|
fn get_pp_expr(crate_ctxt ccx, &@expr e) -> pre_and_post {
|
|
|
|
ret expr_pp(ccx, e);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
2011-05-18 17:43:05 -05:00
|
|
|
auto g = bind get_pp_expr(fcx.ccx, _);
|
2011-05-14 21:02:30 -05:00
|
|
|
plus_option[pre_and_post](pps,
|
|
|
|
option::map[@expr, pre_and_post](g, b.node.expr));
|
|
|
|
|
2011-05-26 18:02:25 -05:00
|
|
|
auto block_precond = seq_preconds(fcx, pps);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto h = get_post;
|
2011-05-17 13:41:41 -05:00
|
|
|
auto postconds = vec::map[pre_and_post, postcond](h, pps);
|
2011-05-14 21:02:30 -05:00
|
|
|
/* A block may be empty, so this next line ensures that the postconds
|
|
|
|
vector is non-empty. */
|
2011-05-17 13:41:41 -05:00
|
|
|
vec::push[postcond](postconds, block_precond);
|
2011-05-14 21:02:30 -05:00
|
|
|
auto block_postcond = empty_poststate(nv);
|
|
|
|
/* conservative approximation */
|
|
|
|
if (! has_nonlocal_exits(b)) {
|
|
|
|
block_postcond = union_postconds(nv, postconds);
|
|
|
|
}
|
|
|
|
|
2011-05-18 17:43:05 -05:00
|
|
|
set_pre_and_post(fcx.ccx, b.node.a, block_precond, block_postcond);
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
|
|
|
fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
|
|
|
|
find_pre_post_block(fcx, f.body);
|
2011-05-31 14:24:18 -05:00
|
|
|
|
|
|
|
// Treat the tail expression as a return statement
|
|
|
|
alt (f.body.node.expr) {
|
|
|
|
case (some(?tailexpr)) {
|
|
|
|
auto tailann = expr_ann(tailexpr);
|
|
|
|
set_postcond_false(fcx.ccx, tailann);
|
|
|
|
}
|
|
|
|
case (none) { /* fallthrough */ }
|
|
|
|
}
|
2011-05-14 21:02:30 -05:00
|
|
|
}
|
|
|
|
|
2011-05-26 18:02:25 -05:00
|
|
|
fn fn_pre_post(crate_ctxt ccx, &_fn f, &span sp, &ident i, &def_id id,
|
|
|
|
&ann a) -> () {
|
2011-05-14 21:02:30 -05:00
|
|
|
assert (ccx.fm.contains_key(id));
|
|
|
|
auto fcx = rec(enclosing=ccx.fm.get(id),
|
|
|
|
id=id, name=i, ccx=ccx);
|
|
|
|
find_pre_post_fn(fcx, f);
|
|
|
|
}
|
|
|
|
|
|
|
|
//
|
|
|
|
// 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:
|
|
|
|
//
|