src/comp/middle/tstate/pre_post_conditions.rs

   1
   2 import core::{vec, option};
   3 import option::{none, some};
   4
   5 import tstate::ann::*;
   6 import aux::*;
   7 import bitvectors::{bit_num, seq_preconds, seq_postconds,
   8                     intersect_states,
   9                     relax_precond_block, gen};
  10 import tritv::*;
  11 import syntax::ast::*;
  12 import syntax::ast_util::*;
  13 import syntax::visit;
  14 import util::common::{new_def_hash, log_expr, field_exprs,
  15                       has_nonlocal_exits, log_stmt};
  16 import syntax::codemap::span;
  17
  18 fn find_pre_post_mod(_m: _mod) -> _mod {
  19     #debug("implement find_pre_post_mod!");
  20     fail;
  21 }
  22
  23 fn find_pre_post_native_mod(_m: native_mod) -> native_mod {
  24     #debug("implement find_pre_post_native_mod");
  25     fail;
  26 }
  27
  28 fn find_pre_post_method(ccx: crate_ctxt, m: @method) {
  29     assert (ccx.fm.contains_key(m.id));
  30     let fcx: fn_ctxt =
  31         {enclosing: ccx.fm.get(m.id),
  32          id: m.id,
  33          name: m.ident,
  34          ccx: ccx};
  35     find_pre_post_fn(fcx, m.body);
  36 }
  37
  38 fn find_pre_post_item(ccx: crate_ctxt, i: item) {
  39     alt i.node {
  40       item_const(_, e) {
  41         // make a fake fcx
  42         let v: @mutable [node_id] = @mutable [];
  43         let fake_fcx =
  44             {
  45              // just bogus
  46              enclosing:
  47                  {constrs: @new_def_hash::<constraint>(),
  48                   num_constraints: 0u,
  49                   cf: return_val,
  50                   i_return: ninit(0, ""),
  51                   i_diverge: ninit(0, ""),
  52                   used_vars: v},
  53              id: 0,
  54              name: "",
  55              ccx: ccx};
  56         find_pre_post_expr(fake_fcx, e);
  57       }
  58       item_fn(_, _, body) {
  59         assert (ccx.fm.contains_key(i.id));
  60         let fcx =
  61             {enclosing: ccx.fm.get(i.id), id: i.id, name: i.ident, ccx: ccx};
  62         find_pre_post_fn(fcx, body);
  63       }
  64       item_mod(m) { find_pre_post_mod(m); }
  65       item_native_mod(nm) { find_pre_post_native_mod(nm); }
  66       item_ty(_, _) | item_tag(_, _) | item_iface(_, _) { ret; }
  67       item_res(_, _, body, dtor_id, _) {
  68         let fcx =
  69             {enclosing: ccx.fm.get(dtor_id),
  70              id: dtor_id,
  71              name: i.ident,
  72              ccx: ccx};
  73         find_pre_post_fn(fcx, body);
  74       }
  75       item_obj(o, _, _) {for m in o.methods { find_pre_post_method(ccx, m); }}
  76       item_impl(_, _, _, ms) { for m in ms { find_pre_post_method(ccx, m); } }
  77     }
  78 }
  79
  80
  81 /* Finds the pre and postcondition for each expr in <args>;
  82    sets the precondition in a to be the result of combining
  83    the preconditions for <args>, and the postcondition in a to
  84    be the union of all postconditions for <args> */
  85 fn find_pre_post_exprs(fcx: fn_ctxt, args: [@expr], id: node_id) {
  86     if vec::len::<@expr>(args) > 0u {
  87         #debug("find_pre_post_exprs: oper =");
  88         log_expr(*args[0]);
  89     }
  90     fn do_one(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
  91     for e: @expr in args { do_one(fcx, e); }
  92
  93     fn get_pp(ccx: crate_ctxt, &&e: @expr) -> pre_and_post {
  94         ret expr_pp(ccx, e);
  95     }
  96     let pps = vec::map(args, bind get_pp(fcx.ccx, _));
  97
  98     set_pre_and_post(fcx.ccx, id, seq_preconds(fcx, pps),
  99                      seq_postconds(fcx, vec::map(pps, get_post)));
 100 }
 101
 102 fn find_pre_post_loop(fcx: fn_ctxt, l: @local, index: @expr, body: blk,
 103                       id: node_id) {
 104     find_pre_post_expr(fcx, index);
 105     find_pre_post_block(fcx, body);
 106     pat_bindings(l.node.pat) {|p|
 107         let ident = alt p.node { pat_bind(id, _) { id } };
 108         let v_init = ninit(p.id, ident);
 109         relax_precond_block(fcx, bit_num(fcx, v_init) as node_id, body);
 110         // Hack: for-loop index variables are frequently ignored,
 111         // so we pretend they're used
 112         use_var(fcx, p.id);
 113     };
 114
 115     let loop_precond =
 116         seq_preconds(fcx, [expr_pp(fcx.ccx, index), block_pp(fcx.ccx, body)]);
 117     let loop_postcond =
 118         intersect_states(expr_postcond(fcx.ccx, index),
 119                          block_postcond(fcx.ccx, body));
 120     copy_pre_post_(fcx.ccx, id, loop_precond, loop_postcond);
 121 }
 122
 123 // Generates a pre/post assuming that a is the
 124 // annotation for an if-expression with consequent conseq
 125 // and alternative maybe_alt
 126 fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
 127                   maybe_alt: option::t<@expr>, id: node_id, chck: if_ty) {
 128     find_pre_post_expr(fcx, antec);
 129     find_pre_post_block(fcx, conseq);
 130     alt maybe_alt {
 131       none. {
 132         alt chck {
 133           if_check. {
 134             let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
 135             gen(fcx, antec.id, c.node);
 136           }
 137           _ { }
 138         }
 139
 140         let precond_res =
 141             seq_preconds(fcx,
 142                          [expr_pp(fcx.ccx, antec),
 143                           block_pp(fcx.ccx, conseq)]);
 144         set_pre_and_post(fcx.ccx, id, precond_res,
 145                          expr_poststate(fcx.ccx, antec));
 146       }
 147       some(altern) {
 148         /*
 149           if check = if_check, then
 150           be sure that the predicate implied by antec
 151           is *not* true in the alternative
 152          */
 153         find_pre_post_expr(fcx, altern);
 154         let precond_false_case =
 155             seq_preconds(fcx,
 156                          [expr_pp(fcx.ccx, antec), expr_pp(fcx.ccx, altern)]);
 157         let postcond_false_case =
 158             seq_postconds(fcx,
 159                           [expr_postcond(fcx.ccx, antec),
 160                            expr_postcond(fcx.ccx, altern)]);
 161
 162         /* Be sure to set the bit for the check condition here,
 163          so that it's *not* set in the alternative. */
 164         alt chck {
 165           if_check. {
 166             let c: sp_constr = expr_to_constr(fcx.ccx.tcx, antec);
 167             gen(fcx, antec.id, c.node);
 168           }
 169           _ { }
 170         }
 171         let precond_true_case =
 172             seq_preconds(fcx,
 173                          [expr_pp(fcx.ccx, antec),
 174                           block_pp(fcx.ccx, conseq)]);
 175         let postcond_true_case =
 176             seq_postconds(fcx,
 177                           [expr_postcond(fcx.ccx, antec),
 178                            block_postcond(fcx.ccx, conseq)]);
 179
 180         let precond_res =
 181             seq_postconds(fcx, [precond_true_case, precond_false_case]);
 182         let postcond_res =
 183             intersect_states(postcond_true_case, postcond_false_case);
 184         set_pre_and_post(fcx.ccx, id, precond_res, postcond_res);
 185       }
 186     }
 187 }
 188
 189 fn gen_if_local(fcx: fn_ctxt, lhs: @expr, rhs: @expr, larger_id: node_id,
 190                 new_var: node_id, pth: @path) {
 191     alt node_id_to_def(fcx.ccx, new_var) {
 192       some(d) {
 193         alt d {
 194           def_local(d_id, _) {
 195             find_pre_post_expr(fcx, rhs);
 196             let p = expr_pp(fcx.ccx, rhs);
 197             set_pre_and_post(fcx.ccx, larger_id, p.precondition,
 198                              p.postcondition);
 199             gen(fcx, larger_id,
 200                 ninit(d_id.node, path_to_ident(fcx.ccx.tcx, pth)));
 201           }
 202           _ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); }
 203         }
 204       }
 205       _ { find_pre_post_exprs(fcx, [lhs, rhs], larger_id); }
 206     }
 207 }
 208
 209 fn handle_update(fcx: fn_ctxt, parent: @expr, lhs: @expr, rhs: @expr,
 210                  ty: oper_type) {
 211     find_pre_post_expr(fcx, rhs);
 212     alt lhs.node {
 213       expr_path(p) {
 214         let post = expr_postcond(fcx.ccx, parent);
 215         let tmp = tritv_clone(post);
 216
 217         alt ty {
 218           oper_move. {
 219             if is_path(rhs) { forget_in_postcond(fcx, parent.id, rhs.id); }
 220           }
 221           oper_swap. {
 222             forget_in_postcond_still_init(fcx, parent.id, lhs.id);
 223             forget_in_postcond_still_init(fcx, parent.id, rhs.id);
 224           }
 225           oper_assign. {
 226             forget_in_postcond_still_init(fcx, parent.id, lhs.id);
 227           }
 228           _ {
 229             // pure and assign_op require the lhs to be init'd
 230             let df = node_id_to_def_strict(fcx.ccx.tcx, lhs.id);
 231             alt df {
 232               def_local(d_id, _) {
 233                 let i =
 234                     bit_num(fcx,
 235                             ninit(d_id.node, path_to_ident(fcx.ccx.tcx, p)));
 236                 require_and_preserve(i, expr_pp(fcx.ccx, lhs));
 237               }
 238               _ { }
 239             }
 240           }
 241         }
 242
 243         gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p);
 244         alt rhs.node {
 245           expr_path(p1) {
 246             let d = local_node_id_to_local_def_id(fcx, lhs.id);
 247             let d1 = local_node_id_to_local_def_id(fcx, rhs.id);
 248             alt d {
 249               some(id) {
 250                 alt d1 {
 251                   some(id1) {
 252                     let instlhs =
 253                         {ident: path_to_ident(fcx.ccx.tcx, p), node: id};
 254                     let instrhs =
 255                         {ident: path_to_ident(fcx.ccx.tcx, p1), node: id1};
 256                     copy_in_poststate_two(fcx, tmp, post, instlhs, instrhs,
 257                                           ty);
 258                   }
 259                   _ { }
 260                 }
 261               }
 262               _ { }
 263             }
 264           }
 265           _ {/* do nothing */ }
 266         }
 267       }
 268       _ { find_pre_post_expr(fcx, lhs); }
 269     }
 270 }
 271
 272 fn handle_var(fcx: fn_ctxt, rslt: pre_and_post, id: node_id, name: ident) {
 273     handle_var_def(fcx, rslt, node_id_to_def_strict(fcx.ccx.tcx, id), name);
 274 }
 275
 276 fn handle_var_def(fcx: fn_ctxt, rslt: pre_and_post, def: def, name: ident) {
 277     log(debug, ("handle_var_def: ", def, name));
 278     alt def {
 279       def_local(d_id, _) | def_arg(d_id, _) {
 280         use_var(fcx, d_id.node);
 281         let i = bit_num(fcx, ninit(d_id.node, name));
 282         require_and_preserve(i, rslt);
 283       }
 284       _ {/* nothing to check */ }
 285     }
 286 }
 287
 288 fn forget_args_moved_in(fcx: fn_ctxt, parent: @expr, modes: [ty::mode],
 289                         operands: [@expr]) {
 290     let i = 0u;
 291     for mode: ty::mode in modes {
 292         if mode == by_move {
 293             forget_in_postcond(fcx, parent.id, operands[i].id);
 294         }
 295         i += 1u;
 296     }
 297 }
 298
 299 fn find_pre_post_expr_fn_upvars(fcx: fn_ctxt, e: @expr) {
 300     let rslt = expr_pp(fcx.ccx, e);
 301     clear_pp(rslt);
 302     for def in *freevars::get_freevars(fcx.ccx.tcx, e.id) {
 303         log(debug, ("handle_var_def: def=", def));
 304         handle_var_def(fcx, rslt, def.def, "upvar");
 305     }
 306 }
 307
 308 /* Fills in annotations as a side effect. Does not rebuild the expr */
 309 fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
 310     let enclosing = fcx.enclosing;
 311     let num_local_vars = num_constraints(enclosing);
 312     fn do_rand_(fcx: fn_ctxt, e: @expr) { find_pre_post_expr(fcx, e); }
 313
 314
 315     alt e.node {
 316       expr_call(operator, operands, _) {
 317         /* copy */
 318
 319         let args = operands;
 320         args += [operator];
 321
 322         find_pre_post_exprs(fcx, args, e.id);
 323         /* see if the call has any constraints on its type */
 324         for c: @ty::constr in constraints_expr(fcx.ccx.tcx, operator) {
 325             let i =
 326                 bit_num(fcx, substitute_constr_args(fcx.ccx.tcx, args, c));
 327             require(i, expr_pp(fcx.ccx, e));
 328         }
 329
 330         forget_args_moved_in(fcx, e, callee_modes(fcx, operator.id),
 331                              operands);
 332
 333         /* if this is a failing call, its postcondition sets everything */
 334         alt controlflow_expr(fcx.ccx, operator) {
 335           noreturn. { set_postcond_false(fcx.ccx, e.id); }
 336           _ { }
 337         }
 338       }
 339       expr_vec(args, _) { find_pre_post_exprs(fcx, args, e.id); }
 340       expr_path(p) {
 341         let rslt = expr_pp(fcx.ccx, e);
 342         clear_pp(rslt);
 343         handle_var(fcx, rslt, e.id, path_to_ident(fcx.ccx.tcx, p));
 344       }
 345       expr_log(_, lvl, arg) {
 346         find_pre_post_exprs(fcx, [lvl, arg], e.id);
 347       }
 348       expr_fn(_, _, _, cap_clause) {
 349         find_pre_post_expr_fn_upvars(fcx, e);
 350
 351         let use_cap_item = fn@(&&cap_item: @capture_item) {
 352             let d = local_node_id_to_local_def_id(fcx, cap_item.id);
 353             option::may(d, { |id| use_var(fcx, id) });
 354         };
 355         vec::iter(cap_clause.copies, use_cap_item);
 356         vec::iter(cap_clause.moves, use_cap_item);
 357
 358         vec::iter(cap_clause.moves) { |cap_item|
 359             log(debug, ("forget_in_postcond: ", cap_item));
 360             forget_in_postcond(fcx, e.id, cap_item.id);
 361         }
 362       }
 363       expr_fn_block(_, _) {
 364         find_pre_post_expr_fn_upvars(fcx, e);
 365       }
 366       expr_block(b) {
 367         find_pre_post_block(fcx, b);
 368         let p = block_pp(fcx.ccx, b);
 369         set_pre_and_post(fcx.ccx, e.id, p.precondition, p.postcondition);
 370       }
 371       expr_rec(fields, maybe_base) {
 372         let es = field_exprs(fields);
 373         alt maybe_base { none. {/* no-op */ } some(b) { es += [b]; } }
 374         find_pre_post_exprs(fcx, es, e.id);
 375       }
 376       expr_tup(elts) { find_pre_post_exprs(fcx, elts, e.id); }
 377       expr_copy(a) {
 378         find_pre_post_expr(fcx, a);
 379         copy_pre_post(fcx.ccx, e.id, a);
 380       }
 381       expr_move(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_move); }
 382       expr_swap(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_swap); }
 383       expr_assign(lhs, rhs) { handle_update(fcx, e, lhs, rhs, oper_assign); }
 384       expr_assign_op(_, lhs, rhs) {
 385         /* Different from expr_assign in that the lhs *must*
 386            already be initialized */
 387
 388         find_pre_post_exprs(fcx, [lhs, rhs], e.id);
 389         forget_in_postcond_still_init(fcx, e.id, lhs.id);
 390       }
 391       expr_lit(_) { clear_pp(expr_pp(fcx.ccx, e)); }
 392       expr_ret(maybe_val) {
 393         alt maybe_val {
 394           none. {
 395             clear_precond(fcx.ccx, e.id);
 396             set_postcond_false(fcx.ccx, e.id);
 397           }
 398           some(ret_val) {
 399             find_pre_post_expr(fcx, ret_val);
 400             set_precondition(node_id_to_ts_ann(fcx.ccx, e.id),
 401                              expr_precond(fcx.ccx, ret_val));
 402             set_postcond_false(fcx.ccx, e.id);
 403           }
 404         }
 405       }
 406       expr_be(val) {
 407         find_pre_post_expr(fcx, val);
 408         set_pre_and_post(fcx.ccx, e.id, expr_prestate(fcx.ccx, val),
 409                          false_postcond(num_local_vars));
 410       }
 411       expr_if(antec, conseq, maybe_alt) {
 412         join_then_else(fcx, antec, conseq, maybe_alt, e.id, plain_if);
 413       }
 414       expr_ternary(_, _, _) { find_pre_post_expr(fcx, ternary_to_if(e)); }
 415       expr_binary(bop, l, r) {
 416         if lazy_binop(bop) {
 417             find_pre_post_expr(fcx, l);
 418             find_pre_post_expr(fcx, r);
 419             let overall_pre =
 420                 seq_preconds(fcx, [expr_pp(fcx.ccx, l), expr_pp(fcx.ccx, r)]);
 421             set_precondition(node_id_to_ts_ann(fcx.ccx, e.id), overall_pre);
 422             set_postcondition(node_id_to_ts_ann(fcx.ccx, e.id),
 423                               expr_postcond(fcx.ccx, l));
 424         } else { find_pre_post_exprs(fcx, [l, r], e.id); }
 425       }
 426       expr_unary(_, operand) {
 427         find_pre_post_expr(fcx, operand);
 428         copy_pre_post(fcx.ccx, e.id, operand);
 429       }
 430       expr_cast(operand, _) {
 431         find_pre_post_expr(fcx, operand);
 432         copy_pre_post(fcx.ccx, e.id, operand);
 433       }
 434       expr_while(test, body) {
 435         find_pre_post_expr(fcx, test);
 436         find_pre_post_block(fcx, body);
 437         set_pre_and_post(fcx.ccx, e.id,
 438                          seq_preconds(fcx,
 439                                       [expr_pp(fcx.ccx, test),
 440                                        block_pp(fcx.ccx, body)]),
 441                          intersect_states(expr_postcond(fcx.ccx, test),
 442                                           block_postcond(fcx.ccx, body)));
 443       }
 444       expr_do_while(body, test) {
 445         find_pre_post_block(fcx, body);
 446         find_pre_post_expr(fcx, test);
 447         let loop_postcond =
 448             seq_postconds(fcx,
 449                           [block_postcond(fcx.ccx, body),
 450                            expr_postcond(fcx.ccx, test)]);
 451         /* conservative approximation: if the body
 452            could break or cont, the test may never be executed */
 453
 454         if has_nonlocal_exits(body) {
 455             loop_postcond = empty_poststate(num_local_vars);
 456         }
 457         set_pre_and_post(fcx.ccx, e.id,
 458                          seq_preconds(fcx,
 459                                       [block_pp(fcx.ccx, body),
 460                                        expr_pp(fcx.ccx, test)]),
 461                          loop_postcond);
 462       }
 463       expr_for(d, index, body) {
 464         find_pre_post_loop(fcx, d, index, body, e.id);
 465       }
 466       expr_index(val, sub) { find_pre_post_exprs(fcx, [val, sub], e.id); }
 467       expr_alt(ex, alts) {
 468         find_pre_post_expr(fcx, ex);
 469         fn do_an_alt(fcx: fn_ctxt, an_alt: arm) -> pre_and_post {
 470             alt an_alt.guard {
 471               some(e) { find_pre_post_expr(fcx, e); }
 472               _ {}
 473             }
 474             find_pre_post_block(fcx, an_alt.body);
 475             ret block_pp(fcx.ccx, an_alt.body);
 476         }
 477         let alt_pps = [];
 478         for a: arm in alts { alt_pps += [do_an_alt(fcx, a)]; }
 479         fn combine_pp(antec: pre_and_post, fcx: fn_ctxt, &&pp: pre_and_post,
 480                       &&next: pre_and_post) -> pre_and_post {
 481             union(pp.precondition, seq_preconds(fcx, [antec, next]));
 482             intersect(pp.postcondition, next.postcondition);
 483             ret pp;
 484         }
 485         let antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
 486         let e_pp =
 487             @{precondition: empty_prestate(num_local_vars),
 488               postcondition: false_postcond(num_local_vars)};
 489         let g = bind combine_pp(antec_pp, fcx, _, _);
 490         let alts_overall_pp =
 491             vec::foldl(e_pp, alt_pps, g);
 492         set_pre_and_post(fcx.ccx, e.id, alts_overall_pp.precondition,
 493                          alts_overall_pp.postcondition);
 494       }
 495       expr_field(operator, _, _) {
 496         find_pre_post_expr(fcx, operator);
 497         copy_pre_post(fcx.ccx, e.id, operator);
 498       }
 499       expr_fail(maybe_val) {
 500         let prestate;
 501         alt maybe_val {
 502           none. { prestate = empty_prestate(num_local_vars); }
 503           some(fail_val) {
 504             find_pre_post_expr(fcx, fail_val);
 505             prestate = expr_precond(fcx.ccx, fail_val);
 506           }
 507         }
 508         set_pre_and_post(fcx.ccx, e.id,
 509                          /* if execution continues after fail,
 510                             then everything is true! */
 511                          prestate, false_postcond(num_local_vars));
 512       }
 513       expr_assert(p) {
 514         find_pre_post_expr(fcx, p);
 515         copy_pre_post(fcx.ccx, e.id, p);
 516       }
 517       expr_check(_, p) {
 518         find_pre_post_expr(fcx, p);
 519         copy_pre_post(fcx.ccx, e.id, p);
 520         /* predicate p holds after this expression executes */
 521
 522         let c: sp_constr = expr_to_constr(fcx.ccx.tcx, p);
 523         gen(fcx, e.id, c.node);
 524       }
 525       expr_if_check(p, conseq, maybe_alt) {
 526         join_then_else(fcx, p, conseq, maybe_alt, e.id, if_check);
 527       }
 528
 529
 530
 531
 532
 533
 534       expr_bind(operator, maybe_args) {
 535         let args = [];
 536         let cmodes = callee_modes(fcx, operator.id);
 537         let modes = [];
 538         let i = 0;
 539         for expr_opt: option::t<@expr> in maybe_args {
 540             alt expr_opt {
 541               none. {/* no-op */ }
 542               some(expr) { modes += [cmodes[i]]; args += [expr]; }
 543             }
 544             i += 1;
 545         }
 546         args += [operator]; /* ??? order of eval? */
 547         forget_args_moved_in(fcx, e, modes, args);
 548         find_pre_post_exprs(fcx, args, e.id);
 549       }
 550       expr_break. { clear_pp(expr_pp(fcx.ccx, e)); }
 551       expr_cont. { clear_pp(expr_pp(fcx.ccx, e)); }
 552       expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
 553       expr_anon_obj(anon_obj) {
 554         alt anon_obj.inner_obj {
 555           some(ex) {
 556             find_pre_post_expr(fcx, ex);
 557             copy_pre_post(fcx.ccx, e.id, ex);
 558           }
 559           none. { clear_pp(expr_pp(fcx.ccx, e)); }
 560         }
 561       }
 562     }
 563 }
 564
 565 fn find_pre_post_stmt(fcx: fn_ctxt, s: stmt) {
 566     #debug("stmt =");
 567     log_stmt(s);
 568     alt s.node {
 569       stmt_decl(adecl, id) {
 570         alt adecl.node {
 571           decl_local(alocals) {
 572             let e_pp;
 573             let prev_pp = empty_pre_post(num_constraints(fcx.enclosing));
 574             for (_, alocal) in alocals {
 575                 alt alocal.node.init {
 576                   some(an_init) {
 577                     /* LHS always becomes initialized,
 578                      whether or not this is a move */
 579                     find_pre_post_expr(fcx, an_init.expr);
 580                     pat_bindings(alocal.node.pat) {|p|
 581                         copy_pre_post(fcx.ccx, p.id, an_init.expr);
 582                     };
 583                     /* Inherit ann from initializer, and add var being
 584                        initialized to the postcondition */
 585                     copy_pre_post(fcx.ccx, id, an_init.expr);
 586
 587                     let p = none;
 588                     alt an_init.expr.node {
 589                       expr_path(_p) { p = some(_p); }
 590                       _ { }
 591                     }
 592
 593                     pat_bindings(alocal.node.pat) {|pat|
 594                         /* FIXME: This won't be necessary when typestate
 595                         works well enough for pat_bindings to return a
 596                         refinement-typed thing. */
 597                         let ident = alt pat.node { pat_bind(n, _) { n } };
 598                         alt p {
 599                           some(p) {
 600                             copy_in_postcond(fcx, id,
 601                                              {ident: ident, node: pat.id},
 602                                              {ident:
 603                                                   path_to_ident(fcx.ccx.tcx,
 604                                                                 p),
 605                                               node: an_init.expr.id},
 606                                              op_to_oper_ty(an_init.op));
 607                           }
 608                           none. { }
 609                         }
 610                         gen(fcx, id, ninit(pat.id, ident));
 611                     };
 612
 613                     if an_init.op == init_move && is_path(an_init.expr) {
 614                         forget_in_postcond(fcx, id, an_init.expr.id);
 615                     }
 616
 617                     /* Clear out anything that the previous initializer
 618                     guaranteed */
 619                     e_pp = expr_pp(fcx.ccx, an_init.expr);
 620                     tritv_copy(prev_pp.precondition,
 621                                seq_preconds(fcx, [prev_pp, e_pp]));
 622                     /* Include the LHSs too, since those aren't in the
 623                      postconds of the RHSs themselves */
 624                     pat_bindings(alocal.node.pat) {|pat|
 625                         alt pat.node {
 626                           pat_bind(n, _) {
 627                             set_in_postcond(bit_num(fcx, ninit(pat.id, n)),
 628                                             prev_pp);
 629                           }
 630                         }
 631                     };
 632                     copy_pre_post_(fcx.ccx, id, prev_pp.precondition,
 633                                    prev_pp.postcondition);
 634                   }
 635                   none. {
 636                     pat_bindings(alocal.node.pat) {|p|
 637                         clear_pp(node_id_to_ts_ann(fcx.ccx, p.id).conditions);
 638                     };
 639                     clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
 640                   }
 641                 }
 642             }
 643           }
 644           decl_item(anitem) {
 645             clear_pp(node_id_to_ts_ann(fcx.ccx, id).conditions);
 646             find_pre_post_item(fcx.ccx, *anitem);
 647           }
 648         }
 649       }
 650       stmt_expr(e, id) | stmt_semi(e, id) {
 651         find_pre_post_expr(fcx, e);
 652         copy_pre_post(fcx.ccx, id, e);
 653       }
 654     }
 655 }
 656
 657 fn find_pre_post_block(fcx: fn_ctxt, b: blk) {
 658     /* Want to say that if there is a break or cont in this
 659      block, then that invalidates the poststate upheld by
 660     any of the stmts after it.
 661     Given that the typechecker has run, we know any break will be in
 662     a block that forms a loop body. So that's ok. There'll never be an
 663     expr_break outside a loop body, therefore, no expr_break outside a block.
 664     */
 665
 666     /* Conservative approximation for now: This says that if a block contains
 667      *any* breaks or conts, then its postcondition doesn't promise anything.
 668      This will mean that:
 669      x = 0;
 670      break;
 671
 672      won't have a postcondition that says x is initialized, but that's ok.
 673      */
 674
 675     let nv = num_constraints(fcx.enclosing);
 676     fn do_one_(fcx: fn_ctxt, s: @stmt) {
 677         find_pre_post_stmt(fcx, *s);
 678         /*
 679                 #error("pre_post for stmt:");
 680                 log_stmt_err(*s);
 681                 #error("is:");
 682                 log_pp_err(stmt_pp(fcx.ccx, *s));
 683         */
 684     }
 685     for s: @stmt in b.node.stmts { do_one_(fcx, s); }
 686     fn do_inner_(fcx: fn_ctxt, &&e: @expr) { find_pre_post_expr(fcx, e); }
 687     let do_inner = bind do_inner_(fcx, _);
 688     option::map::<@expr, ()>(b.node.expr, do_inner);
 689
 690     let pps: [pre_and_post] = [];
 691     for s: @stmt in b.node.stmts { pps += [stmt_pp(fcx.ccx, *s)]; }
 692     alt b.node.expr {
 693       none. {/* no-op */ }
 694       some(e) { pps += [expr_pp(fcx.ccx, e)]; }
 695     }
 696
 697     let block_precond = seq_preconds(fcx, pps);
 698
 699     let postconds = [];
 700     for pp: pre_and_post in pps { postconds += [get_post(pp)]; }
 701
 702     /* A block may be empty, so this next line ensures that the postconds
 703        vector is non-empty. */
 704     postconds += [block_precond];
 705
 706     let block_postcond = empty_poststate(nv);
 707     /* conservative approximation */
 708
 709     if !has_nonlocal_exits(b) {
 710         block_postcond = seq_postconds(fcx, postconds);
 711     }
 712     set_pre_and_post(fcx.ccx, b.node.id, block_precond, block_postcond);
 713 }
 714
 715 fn find_pre_post_fn(fcx: fn_ctxt, body: blk) {
 716     // hack
 717     use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_return));
 718     use_var(fcx, tsconstr_to_node_id(fcx.enclosing.i_diverge));
 719
 720     find_pre_post_block(fcx, body);
 721
 722     // Treat the tail expression as a return statement
 723     alt body.node.expr {
 724       some(tailexpr) { set_postcond_false(fcx.ccx, tailexpr.id); }
 725       none. {/* fallthrough */ }
 726     }
 727 }
 728
 729 fn fn_pre_post(fk: visit::fn_kind, decl: fn_decl, body: blk, sp: span,
 730                id: node_id,
 731                ccx: crate_ctxt, v: visit::vt<crate_ctxt>) {
 732     visit::visit_fn(fk, decl, body, sp, id, ccx, v);
 733     assert (ccx.fm.contains_key(id));
 734     let fcx =
 735         {enclosing: ccx.fm.get(id),
 736          id: id,
 737          name: visit::name_of_fn(fk),
 738          ccx: ccx};
 739     find_pre_post_fn(fcx, body);
 740 }
 741
 742 //
 743 // Local Variables:
 744 // mode: rust
 745 // fill-column: 78;
 746 // indent-tabs-mode: nil
 747 // c-basic-offset: 4
 748 // buffer-file-coding-system: utf-8-unix
 749 // End:
 750 //