From 582e1f13f068dd85411405672e29ead829238fbc Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Fri, 24 Jun 2011 22:17:17 -0700 Subject: [PATCH] Invalidate constraints correctly after an assignment expression Modified typestate to throw away any constraints mentioning a variable on the LHS of an assignment, recv, assign_op, or on either side of a swap. Some code cleanup as well. --- src/comp/front/ast.rs | 3 + src/comp/middle/tstate/ann.rs | 33 +- src/comp/middle/tstate/auxiliary.rs | 108 +++- src/comp/middle/tstate/bitvectors.rs | 35 ++ src/comp/middle/tstate/pre_post_conditions.rs | 37 +- src/comp/middle/tstate/states.rs | 514 +++++++----------- src/comp/middle/tstate/tritv.rs | 50 +- src/lib/vec.rs | 2 +- src/test/compile-fail/pred-assign.rs | 20 + src/test/compile-fail/pred-swap.rs | 20 + 10 files changed, 444 insertions(+), 378 deletions(-) create mode 100644 src/test/compile-fail/pred-assign.rs create mode 100644 src/test/compile-fail/pred-swap.rs diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index b19644eb205..1778014da01 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -11,6 +11,9 @@ type ident = str; // Functions may or may not have names. type fn_ident = option::t[ident]; +// FIXME: with typestate constraint, could say +// idents and types are the same length, and are +// non-empty type path_ = rec(vec[ident] idents, vec[@ty] types); type path = spanned[path_]; diff --git a/src/comp/middle/tstate/ann.rs b/src/comp/middle/tstate/ann.rs index 8ea7b54de0c..d8aae77e621 100644 --- a/src/comp/middle/tstate/ann.rs +++ b/src/comp/middle/tstate/ann.rs @@ -112,28 +112,37 @@ fn set_in_postcond(uint i, &pre_and_post p) -> bool { // sets the ith bit in p's post auto was_set = tritv_get(p.postcondition, i); tritv_set(i, p.postcondition, ttrue); - ret was_set != ttrue; + ret was_set == dont_care; } fn set_in_poststate(uint i, &pre_and_post_state s) -> bool { // sets the ith bit in p's post - auto was_set = tritv_get(s.poststate, i); - tritv_set(i, s.poststate, ttrue); - ret was_set != ttrue; + ret set_in_poststate_(i, s.poststate); +} + +fn set_in_poststate_(uint i, &poststate p) -> bool { + auto was_set = tritv_get(p, i); + tritv_set(i, p, ttrue); + ret was_set == dont_care; + } fn clear_in_poststate(uint i, &pre_and_post_state s) -> bool { // sets the ith bit in p's post - auto was_set = tritv_get(s.poststate, i); - tritv_set(i, s.poststate, tfalse); - ret was_set != tfalse; + ret clear_in_poststate_(i, s.poststate); +} + +fn clear_in_poststate_(uint i, &poststate s) -> bool { + auto was_set = tritv_get(s, i); + tritv_set(i, s, tfalse); + ret was_set == dont_care; } fn clear_in_postcond(uint i, &pre_and_post s) -> bool { // sets the ith bit in p's post auto was_set = tritv_get(s.postcondition, i); tritv_set(i, s.postcondition, tfalse); - ret was_set != tfalse; + ret was_set == dont_care; } // Sets all the bits in a's precondition to equal the @@ -222,6 +231,14 @@ fn implies(t a, t b) -> bool { tritv_difference(tmp, a); ret tritv_doesntcare(tmp); } + +fn trit_str(trit t) -> str { + alt (t) { + case (dont_care) { "?" } + case (ttrue) { "1" } + case (tfalse) { "0" } + } +} // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs index af040ad38bf..e88b934ab05 100644 --- a/src/comp/middle/tstate/auxiliary.rs +++ b/src/comp/middle/tstate/auxiliary.rs @@ -39,6 +39,7 @@ import tstate::ann::set_postcondition; import tstate::ann::ts_ann; import tstate::ann::clear_in_postcond; import tstate::ann::clear_in_poststate; +import tstate::ann::clear_in_poststate_; import tritv::*; import pretty::ppaux::constr_args_to_str; @@ -655,8 +656,9 @@ tag if_ty { plain_if; } -fn local_node_id_to_def_id(&fn_ctxt fcx, &span sp, &node_id i) -> def_id { - alt (fcx.ccx.tcx.def_map.find(i)) { +fn local_node_id_to_def_id_strict(&fn_ctxt fcx, &span sp, &node_id i) + -> def_id { + alt (local_node_id_to_def(fcx, i)) { case (some(def_local(?d_id))) { ret d_id; } @@ -675,30 +677,86 @@ fn local_node_id_to_def_id(&fn_ctxt fcx, &span sp, &node_id i) -> def_id { } } -fn forget_in_postcond(&fn_ctxt fcx, &span dead_sp, - node_id parent_exp, node_id dead_v) { - // In the postcondition given by parent_exp, clear the bits - // for any constraints mentioning dead_v - auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v); - for (norm_constraint c in constraints(fcx)) { - if (constraint_mentions(fcx, c, d_id)) { - clear_in_postcond(c.bit_num, - node_id_to_ts_ann(fcx.ccx, parent_exp).conditions); - } +fn local_node_id_to_def(&fn_ctxt fcx, &node_id i) -> option::t[def] + { fcx.ccx.tcx.def_map.find(i) } + +fn local_node_id_to_def_id(&fn_ctxt fcx, &node_id i) -> option::t[def_id] { + alt (local_node_id_to_def(fcx, i)) { + case (some(def_local(?d_id))) { some(d_id) } + case (some (def_arg(?a_id))) { some(a_id) } + case (_) { none } } } -fn forget_in_poststate(&fn_ctxt fcx, &span dead_sp, - node_id parent_exp, node_id dead_v) -> bool { +/* FIXME should refactor this better */ +fn forget_in_postcond(&fn_ctxt fcx, node_id parent_exp, node_id dead_v) { + // In the postcondition given by parent_exp, clear the bits + // for any constraints mentioning dead_v + auto d = local_node_id_to_def_id(fcx, dead_v); + alt (d) { + case (some(?d_id)) { + for (norm_constraint c in constraints(fcx)) { + if (constraint_mentions(fcx, c, d_id)) { + clear_in_postcond(c.bit_num, + node_id_to_ts_ann(fcx.ccx, parent_exp).conditions); + } + } + } + case (_) {} + } +} + +fn forget_in_postcond_still_init(&fn_ctxt fcx, node_id parent_exp, + node_id dead_v) { + // In the postcondition given by parent_exp, clear the bits + // for any constraints mentioning dead_v + auto d = local_node_id_to_def_id(fcx, dead_v); + alt (d) { + case (some(?d_id)) { + for (norm_constraint c in constraints(fcx)) { + if (non_init_constraint_mentions(fcx, c, d_id)) { + clear_in_postcond(c.bit_num, + node_id_to_ts_ann(fcx.ccx, parent_exp).conditions); + } + } + } + case (_) { } + } +} + +fn forget_in_poststate(&fn_ctxt fcx, &poststate p, node_id dead_v) -> bool { // In the poststate given by parent_exp, clear the bits // for any constraints mentioning dead_v - auto d_id = local_node_id_to_def_id(fcx, dead_sp, dead_v); + auto d = local_node_id_to_def_id(fcx, dead_v); auto changed = false; - for (norm_constraint c in constraints(fcx)) { - if (constraint_mentions(fcx, c, d_id)) { - changed = clear_in_poststate(c.bit_num, - node_id_to_ts_ann(fcx.ccx, parent_exp).states) || changed; + alt (d) { + case (some(?d_id)) { + for (norm_constraint c in constraints(fcx)) { + if (constraint_mentions(fcx, c, d_id)) { + changed = clear_in_poststate_(c.bit_num, p) || changed; + } + } } + case (_) {} + } + ret changed; +} + +fn forget_in_poststate_still_init(&fn_ctxt fcx, &poststate p, node_id dead_v) + -> bool { + // In the poststate given by parent_exp, clear the bits + // for any constraints mentioning dead_v + auto d = local_node_id_to_def_id(fcx, dead_v); + auto changed = false; + alt (d) { + case (some(?d_id)) { + for (norm_constraint c in constraints(fcx)) { + if (non_init_constraint_mentions(fcx, c, d_id)) { + changed = clear_in_poststate_(c.bit_num, p) || changed; + } + } + } + case (_) {} } ret changed; } @@ -714,6 +772,18 @@ fn constraint_mentions(&fn_ctxt fcx, &norm_constraint c, &def_id v) -> bool { }); } +fn non_init_constraint_mentions(&fn_ctxt fcx, &norm_constraint c, + &def_id v) -> bool { + ret (alt (c.c.node.c) { + case (ninit(_)) { + false + } + case (npred(_, ?args)) { + args_mention(args, v) + } + }); +} + fn args_mention(&vec[@constr_arg_use] args, &def_id v) -> bool { fn mentions(&def_id v, &@constr_arg_use a) -> bool { diff --git a/src/comp/middle/tstate/bitvectors.rs b/src/comp/middle/tstate/bitvectors.rs index cbfda84d195..21934ca04b7 100644 --- a/src/comp/middle/tstate/bitvectors.rs +++ b/src/comp/middle/tstate/bitvectors.rs @@ -1,7 +1,10 @@ + import front::ast::*; +import std::option::*; import std::vec; import std::vec::len; import std::vec::slice; +import aux::local_node_id_to_def; import aux::fn_ctxt; import aux::fn_info; import aux::log_tritv; @@ -38,7 +41,9 @@ import tstate::ann::intersect; import tstate::ann::clone; import tstate::ann::set_in_postcond; import tstate::ann::set_in_poststate; +import tstate::ann::set_in_poststate_; import tstate::ann::clear_in_poststate; +import tstate::ann::clear_in_poststate_; import tritv::*; fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint { @@ -219,6 +224,36 @@ fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool { ret clear_in_poststate(bit_num(fcx, c), node_id_to_ts_ann(fcx.ccx, id).states); } + +fn clear_in_poststate_expr(&fn_ctxt fcx, &@expr e, &poststate t) { + alt (e.node) { + case (expr_path(?p)) { + alt (vec::last(p.node.idents)) { + case (some(?i)) { + alt (local_node_id_to_def(fcx, e.id)) { + case (some(def_local(?d_id))) { + clear_in_poststate_(bit_num(fcx, + rec(id=d_id._1, + c=ninit(i))), t); + } + case (some(_)) { /* ignore args (for now...) */ } + case (_) { + fcx.ccx.tcx.sess.bug("clear_in_poststate_expr: \ + unbound var"); } + } + } + case (_) { fcx.ccx.tcx.sess.bug("clear_in_poststate_expr"); } + } + } + case (_) { /* do nothing */ } + } +} + +fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident, + &poststate t) -> bool { + ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t); +} + // // Local Variables: // mode: rust diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 47b41f27e3e..4455f09bdc2 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -48,6 +48,7 @@ import aux::if_ty; import aux::if_check; import aux::plain_if; import aux::forget_in_postcond; +import aux::forget_in_postcond_still_init; import aux::constraints_expr; import aux::substitute_constr_args; @@ -61,7 +62,6 @@ import bitvectors::seq_postconds; import bitvectors::intersect_postconds; import bitvectors::declare_var; import bitvectors::gen_poststate; -import bitvectors::kill_poststate; import bitvectors::relax_precond_block; import bitvectors::gen; import front::ast::*; @@ -274,19 +274,13 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { auto enclosing = fcx.enclosing; auto num_local_vars = num_constraints(enclosing); fn do_rand_(fn_ctxt fcx, &@expr e) { find_pre_post_expr(fcx, e); } - log "find_pre_post_expr (num_constraints =" + uistr(num_local_vars) + - "):"; - log_expr(*e); + alt (e.node) { case (expr_call(?operator, ?operands)) { - auto args = vec::clone[@expr](operands); - vec::push[@expr](args, operator); + auto args = vec::clone(operands); + vec::push(args, operator); find_pre_post_exprs(fcx, args, e.id); /* see if the call has any constraints on its type */ - - log "a function: "; - log_expr(*operator); - auto pp = expr_pp(fcx.ccx, e); for (@ty::constr_def c in constraints_expr(fcx.ccx.tcx, operator)) { auto i = @@ -294,7 +288,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { rec(id=c.node.id._1, c=substitute_constr_args(fcx.ccx.tcx, operands, c))); - require(i, pp); + require(i, expr_pp(fcx.ccx, e)); } /* if this is a failing call, its postcondition sets everything */ @@ -304,8 +298,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { } } case (expr_spawn(_, _, ?operator, ?operands)) { - auto args = vec::clone[@expr](operands); - vec::push[@expr](args, operator); + auto args = vec::clone(operands); + vec::push(args, operator); find_pre_post_exprs(fcx, args, e.id); } case (expr_vec(?args, _, _)) { @@ -356,7 +350,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { } case (expr_rec(?fields, ?maybe_base)) { auto es = field_exprs(fields); - vec::plus_option[@expr](es, maybe_base); + vec::plus_option(es, maybe_base); find_pre_post_exprs(fcx, es, e.id); } case (expr_move(?lhs, ?rhs)) { @@ -366,17 +360,22 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { } case (_) { find_pre_post_exprs(fcx, [lhs, rhs], e.id); } } - forget_in_postcond(fcx, rhs.span, e.id, rhs.id); + forget_in_postcond(fcx, e.id, rhs.id); } case (expr_swap(?lhs, ?rhs)) { // Both sides must already be initialized find_pre_post_exprs(fcx, [lhs, rhs], e.id); + forget_in_postcond_still_init(fcx, e.id, lhs.id); + forget_in_postcond_still_init(fcx, e.id, rhs.id); + // Could be more precise and swap the roles of lhs and rhs + // in any constraints } case (expr_assign(?lhs, ?rhs)) { alt (lhs.node) { case (expr_path(?p)) { gen_if_local(fcx, lhs, rhs, e.id, lhs.id, p); + forget_in_postcond_still_init(fcx, e.id, lhs.id); } case (_) { find_pre_post_exprs(fcx, [lhs, rhs], e.id); } } @@ -385,7 +384,8 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { alt (rhs.node) { case (expr_path(?p)) { gen_if_local(fcx, rhs, lhs, e.id, rhs.id, p); - } + forget_in_postcond_still_init(fcx, e.id, lhs.id); + } case (_) { // doesn't check that rhs is an lval, but // that's probably ok @@ -399,6 +399,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { already be initialized */ find_pre_post_exprs(fcx, [lhs, rhs], e.id); + forget_in_postcond_still_init(fcx, e.id, lhs.id); } case (expr_lit(_)) { clear_pp(expr_pp(fcx.ccx, e)); } case (expr_ret(?maybe_val)) { @@ -585,8 +586,8 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) { alt (an_init.op) { case (init_move) { - forget_in_postcond(fcx, an_init.expr.span, - id, an_init.expr.id); + forget_in_postcond(fcx, id, + an_init.expr.id); } case (_) { /* nothing gets deinitialized */ } } diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 1e7a5bf6377..673186e4415 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -7,20 +7,21 @@ import std::option::is_none; import std::option::none; import std::option::some; import std::option::maybe; +import tstate::ann::set_in_poststate_; import tstate::ann::pre_and_post; import tstate::ann::get_post; import tstate::ann::postcond; import tstate::ann::empty_pre_post; import tstate::ann::empty_poststate; -import tstate::ann::require_and_preserve; +import tstate::ann::clear_in_poststate; import tstate::ann::intersect; import tstate::ann::empty_prestate; import tstate::ann::prestate; import tstate::ann::poststate; import tstate::ann::false_postcond; import tstate::ann::ts_ann; -import tstate::ann::extend_prestate; -import tstate::ann::extend_poststate; +import tstate::ann::set_prestate; +import tstate::ann::set_poststate; import aux::crate_ctxt; import aux::fn_ctxt; import aux::num_constraints; @@ -61,13 +62,14 @@ import aux::if_ty; import aux::if_check; import aux::plain_if; import aux::forget_in_poststate; +import aux::forget_in_poststate_still_init; import tritv::tritv_clone; import tritv::tritv_set; import tritv::ttrue; -import bitvectors::seq_preconds; +import bitvectors::set_in_poststate_ident; +import bitvectors::clear_in_poststate_expr; import bitvectors::intersect_postconds; -import bitvectors::declare_var; import bitvectors::bit_num; import bitvectors::gen_poststate; import bitvectors::kill_poststate; @@ -89,23 +91,101 @@ import util::common::log_stmt; import util::common::log_stmt_err; import util::common::log_expr_err; +// Used to communicate which operands should be invalidated +// to helper functions +tag oper_type { + oper_move; + oper_swap; + oper_assign; + oper_pure; +} + fn seq_states(&fn_ctxt fcx, prestate pres, vec[@expr] exprs) -> tup(bool, poststate) { auto changed = false; auto post = pres; for (@expr e in exprs) { changed = find_pre_post_state_expr(fcx, post, e) || changed; + // log_err("Seq_states: changed ="); + // log_err changed; post = expr_poststate(fcx.ccx, e); } ret tup(changed, post); } +fn find_pre_post_state_sub(&fn_ctxt fcx, &prestate pres, &@expr e, + node_id parent, option::t[aux::constr_] c) + -> bool { + auto changed = find_pre_post_state_expr(fcx, pres, e); + + changed = set_prestate_ann(fcx.ccx, parent, pres) || changed; + + auto post = tritv_clone(expr_poststate(fcx.ccx, e)); + alt (c) { + case (none) {} + case (some(?c1)) { + set_in_poststate_(bit_num(fcx, c1), post); + } + } + + changed = set_poststate_ann(fcx.ccx, parent, post) || changed; + ret changed; +} + +fn find_pre_post_state_two(&fn_ctxt fcx, &prestate pres, &@expr a, &@expr b, + node_id parent, oper_type op) -> bool { + auto changed = set_prestate_ann(fcx.ccx, parent, pres); + changed = find_pre_post_state_expr(fcx, pres, a) || changed; + changed = find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, a), b) + || changed; + + // for termination, need to make sure intermediate changes don't set + // changed flag + auto post = tritv_clone(expr_poststate(fcx.ccx, b)); + alt (op) { + case (oper_move) { + forget_in_poststate(fcx, post, b.id); + gen_if_local(fcx, post, a); + } + case (oper_swap) { + forget_in_poststate_still_init(fcx, post, a.id); + forget_in_poststate_still_init(fcx, post, b.id); + } + case (oper_assign) { + forget_in_poststate_still_init(fcx, post, a.id); + gen_if_local(fcx, post, a); + } + case (_) {} + } + changed = set_poststate_ann(fcx.ccx, parent, post) || changed; + ret changed; +} + +fn find_pre_post_state_call(&fn_ctxt fcx, &prestate pres, &@expr a, + node_id id, &vec[@expr] bs, + controlflow cf) -> bool { + auto changed = find_pre_post_state_expr(fcx, pres, a); + ret find_pre_post_state_exprs(fcx, + expr_poststate(fcx.ccx, a), id, bs, cf) || changed; +} + fn find_pre_post_state_exprs(&fn_ctxt fcx, &prestate pres, ast::node_id id, - &vec[@expr] es) -> bool { - auto rslt = seq_states(fcx, pres, es); - auto changed = rslt._0; - changed = extend_prestate_ann(fcx.ccx, id, pres) || changed; - changed = extend_poststate_ann(fcx.ccx, id, rslt._1) || changed; + &vec[@expr] es, controlflow cf) -> bool { + auto res = seq_states(fcx, pres, es); + auto changed = res._0; + changed = set_prestate_ann(fcx.ccx, id, pres) || changed; + /* if this is a failing call, it sets everything as initialized */ + alt (cf) { + case (noreturn) { + changed = + set_poststate_ann(fcx.ccx, id, + false_postcond(num_constraints(fcx.enclosing))) || + changed; + } + case (_) { + changed = set_poststate_ann(fcx.ccx, id, res._1) || changed; + } + } ret changed; } @@ -116,7 +196,7 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l, // FIXME: also want to set l as initialized, no? - changed = extend_prestate_ann(fcx.ccx, id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, id, 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) */ @@ -132,18 +212,22 @@ fn find_pre_post_state_loop(&fn_ctxt fcx, prestate pres, &@local l, auto res_p = intersect_postconds([expr_poststate(fcx.ccx, index), block_poststate(fcx.ccx, body)]); - changed = extend_poststate_ann(fcx.ccx, id, res_p) || changed; + changed = set_poststate_ann(fcx.ccx, id, res_p) || changed; ret changed; } -fn gen_if_local(&fn_ctxt fcx, node_id new_var, node_id id, &path p) -> bool { - alt (node_id_to_def(fcx.ccx, new_var)) { - case (some(def_local(?loc))) { - ret gen_poststate(fcx, id, - rec(id=loc._1, - c=ninit(path_to_ident(fcx.ccx.tcx, p)))); +fn gen_if_local(&fn_ctxt fcx, &poststate p, &@expr e) -> bool { + alt (e.node) { + case (expr_path(?pth)) { + alt (node_id_to_def(fcx.ccx, e.id)) { + case (some(def_local(?loc))) { + ret set_in_poststate_ident(fcx, loc._1, + path_to_ident(fcx.ccx.tcx, pth), p); + } + case (_) { ret false; } + } } - case (_) { ret false; } + case (_) { ret false; } } } @@ -152,7 +236,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, &prestate pres) -> bool { auto changed = false; - changed = extend_prestate_ann(fcx.ccx, id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, id, pres) || changed; changed = find_pre_post_state_expr(fcx, pres, antec) || changed; /* @@ -178,7 +262,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, conseq) || changed; changed = - extend_poststate_ann(fcx.ccx, id, + set_poststate_ann(fcx.ccx, id, expr_poststate(fcx.ccx, antec)) || changed; } @@ -218,7 +302,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, block_poststate(fcx.ccx, conseq))); */ changed = - extend_poststate_ann(fcx.ccx, id, poststate_res) || + set_poststate_ann(fcx.ccx, id, poststate_res) || changed; } } @@ -228,100 +312,44 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { auto changed = false; auto num_local_vars = num_constraints(fcx.enclosing); - /* - log_err("states:"); - log_expr_err(*e); - aux::log_bitv_err(fcx, expr_prestate(fcx.ccx, e)); - aux::log_bitv_err(fcx, expr_poststate(fcx.ccx, e)); - */ - /* FIXME could get rid of some of the copy/paste */ alt (e.node) { case (expr_vec(?elts, _, _)) { - ret find_pre_post_state_exprs(fcx, pres, e.id, elts); + ret find_pre_post_state_exprs(fcx, pres, e.id, elts, return); } case (expr_tup(?elts)) { - ret find_pre_post_state_exprs(fcx, pres, e.id, elt_exprs(elts)); + ret find_pre_post_state_exprs(fcx, pres, e.id, + elt_exprs(elts), return); } case (expr_call(?operator, ?operands)) { - /* do the prestate for the rator */ - - /* fcx.ccx.tcx.sess.span_note(operator.span, - "pres = " + aux::bitv_to_str(fcx, pres)); - */ - - changed = - find_pre_post_state_expr(fcx, pres, operator) || changed; - /* rands go left-to-right */ - - changed = - find_pre_post_state_exprs(fcx, - expr_poststate(fcx.ccx, operator), - e.id, operands) || changed; - /* if this is a failing call, it sets everything as initialized */ - - alt (controlflow_expr(fcx.ccx, operator)) { - case (noreturn) { - changed = - set_poststate_ann(fcx.ccx, e.id, - false_postcond(num_local_vars)) || - changed; - } - case (_) { } - } - - /* fcx.ccx.tcx.sess.span_note(operator.span, - "pres = " + aux::bitv_to_str(fcx, expr_poststate(fcx.ccx, e))); - */ + changed = find_pre_post_state_call(fcx, pres, operator, + e.id, operands, + controlflow_expr(fcx.ccx, operator)) + || changed; ret changed; } case (expr_spawn(_, _, ?operator, ?operands)) { - changed = find_pre_post_state_expr(fcx, pres, operator); - ret find_pre_post_state_exprs(fcx, - expr_poststate(fcx.ccx, operator), - e.id, operands) || changed; - } + ret find_pre_post_state_call(fcx, pres, operator, e.id, operands, + return); + } case (expr_bind(?operator, ?maybe_args)) { - changed = - find_pre_post_state_expr(fcx, pres, operator) || changed; - ret find_pre_post_state_exprs - (fcx, expr_poststate(fcx.ccx, operator), e.id, - cat_options[@expr](maybe_args)) || changed; + ret find_pre_post_state_call(fcx, pres, operator, e.id, + cat_options(maybe_args), return); } case (expr_path(_)) { ret pure_exp(fcx.ccx, e.id, pres); } case (expr_log(_, ?ex)) { - /* factor out the "one exp" pattern */ - - changed = find_pre_post_state_expr(fcx, pres, ex); - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, ex)) || changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, ex, e.id, none); } case (expr_chan(?ex)) { - changed = find_pre_post_state_expr(fcx, pres, ex); - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, ex)) || changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, ex, e.id, none); } case (expr_ext(_, _, _, ?expanded)) { - changed = find_pre_post_state_expr(fcx, pres, expanded); - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, expanded)) || changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, expanded, e.id, none); } case (expr_put(?maybe_e)) { alt (maybe_e) { case (some(?arg)) { - changed = find_pre_post_state_expr(fcx, pres, arg); - changed = extend_prestate_ann - (fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, arg)) || - changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, arg, e.id, none); } case (none) { ret pure_exp(fcx.ccx, e.id, pres); } } @@ -331,20 +359,20 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { case (expr_fn(?f)) { ret pure_exp(fcx.ccx, e.id, pres); } case (expr_block(?b)) { changed = find_pre_post_state_block(fcx, pres, b) || changed; - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_poststate_ann (fcx.ccx, e.id, block_poststate(fcx.ccx, b)) || changed; ret changed; } case (expr_rec(?fields, ?maybe_base)) { changed = find_pre_post_state_exprs - (fcx, pres, e.id, field_exprs(fields)) || changed; + (fcx, pres, e.id, field_exprs(fields), return) || changed; alt (maybe_base) { case (none) {/* do nothing */ } case (some(?base)) { changed = find_pre_post_state_expr(fcx, pres, base) || changed; - changed = extend_poststate_ann + changed = set_poststate_ann (fcx.ccx, e.id, expr_poststate(fcx.ccx, base)) || changed; } @@ -352,108 +380,34 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { ret changed; } case (expr_move(?lhs, ?rhs)) { - - extend_prestate_ann(fcx.ccx, e.id, pres); - alt (lhs.node) { - case (expr_path(?p)) { - // assignment to local var - - changed = pure_exp(fcx.ccx, lhs.id, pres) || changed; - changed = find_pre_post_state_expr - (fcx, pres, rhs) || changed; - // not extending e's poststate, - // because rhs is getting deinit'd anyway - changed = gen_if_local(fcx, lhs.id, e.id, p) || changed; - } - case (_) { - // assignment to something that must already have been - // init'd - - changed = find_pre_post_state_expr(fcx, pres, lhs) - || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, lhs), rhs) - || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) - || changed; - } - } - - changed = forget_in_poststate(fcx, rhs.span, e.id, rhs.id) - || changed; - ret changed; + ret find_pre_post_state_two(fcx, pres, lhs, rhs, + e.id, oper_move); } case (expr_assign(?lhs, ?rhs)) { - extend_prestate_ann(fcx.ccx, e.id, pres); - alt (lhs.node) { - case (expr_path(?p)) { - // assignment to local var - - changed = pure_exp(fcx.ccx, lhs.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, rhs) - || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) - || changed; - changed = gen_if_local(fcx, lhs.id, e.id, p) || changed; - } - case (_) { - // assignment to something that must already have been - // init'd - - changed = find_pre_post_state_expr(fcx, pres, lhs) - || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, lhs), rhs) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) - || changed; - } - } - ret changed; + ret find_pre_post_state_two(fcx, pres, lhs, rhs, + e.id, oper_assign); } case (expr_swap(?lhs, ?rhs)) { - /* quite similar to binary -- should abstract this */ - - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, lhs) || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, lhs), rhs) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) || changed; - ret changed; + ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, + oper_swap); + // Could be more precise and actually swap the role of + // lhs and rhs in constraints } case (expr_recv(?lhs, ?rhs)) { - extend_prestate_ann(fcx.ccx, e.id, pres); - alt (rhs.node) { - case (expr_path(?p)) { - // receive to local var - - changed = pure_exp(fcx.ccx, rhs.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, lhs) - || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, lhs)) - || changed; - changed = gen_if_local(fcx, rhs.id, e.id, p) || changed; - } - case (_) { - // receive to something that must already have been init'd - - changed = find_pre_post_state_expr - (fcx, pres, rhs) || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, rhs), lhs) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, lhs)) - || changed; - } - } + // Opposite order as most other binary operations, + // so not using find_pre_post_state_two + auto changed = set_prestate_ann(fcx.ccx, e.id, pres); + changed = find_pre_post_state_expr(fcx, pres, lhs) || changed; + changed = find_pre_post_state_expr(fcx, + expr_poststate(fcx.ccx, lhs), rhs) || changed; + auto post = tritv_clone(expr_poststate(fcx.ccx, rhs)); + forget_in_poststate_still_init(fcx, post, rhs.id); + gen_if_local(fcx, post, rhs); + changed = set_poststate_ann(fcx.ccx, e.id, post) || changed; ret changed; } case (expr_ret(?maybe_ret_val)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; /* normally, everything is true if execution continues after a ret expression (since execution never continues locally after a ret expression */ @@ -471,14 +425,14 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { alt (maybe_ret_val) { case (none) {/* do nothing */ } case (some(?ret_val)) { - changed = find_pre_post_state_expr - (fcx, pres, ret_val) || changed; + changed = find_pre_post_state_expr(fcx, pres, ret_val) + || changed; } } ret changed; } case (expr_be(?val)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; set_poststate_ann(fcx.ccx, e.id, false_postcond(num_local_vars)); changed = find_pre_post_state_expr(fcx, pres, val) || changed; ret changed; @@ -494,38 +448,17 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { } case (expr_binary(?bop, ?l, ?r)) { /* FIXME: what if bop is lazy? */ - - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, l) || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, l), r) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, r)) || changed; - ret changed; + ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure); } case (expr_send(?l, ?r)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, l) || changed; - changed = find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, l), r) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, r)) || changed; - ret changed; + ret find_pre_post_state_two(fcx, pres, l, r, e.id, oper_pure); } case (expr_assign_op(?op, ?lhs, ?rhs)) { - /* quite similar to binary -- should abstract this */ - - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, lhs) || changed; - changed = - find_pre_post_state_expr(fcx, expr_poststate(fcx.ccx, lhs), - rhs) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, rhs)) || changed; - ret changed; + ret find_pre_post_state_two(fcx, pres, lhs, rhs, e.id, + oper_assign); } case (expr_while(?test, ?body)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; /* to handle general predicates, we need to pass in pres `intersect` (poststate(a)) like: auto test_pres = intersect_postconds(pres, @@ -547,12 +480,12 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { auto e_post = expr_poststate(fcx.ccx, test); auto b_post = block_poststate(fcx.ccx, body); - ret extend_poststate_ann + ret set_poststate_ann (fcx.ccx, e.id, intersect_postconds([e_post, b_post])) || - changed + changed; } case (expr_do_while(?body, ?test)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; auto changed0 = changed; changed = find_pre_post_state_block(fcx, pres, body) || changed; /* conservative approximination: if the body of the loop @@ -579,7 +512,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { set_poststate_ann(fcx.ccx, e.id, pres); } else { - changed = extend_poststate_ann(fcx.ccx, e.id, + changed = set_poststate_ann(fcx.ccx, e.id, expr_poststate(fcx.ccx, test)) || changed; } @@ -592,18 +525,10 @@ 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, e.id); } case (expr_index(?val, ?sub)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, val) || changed; - changed = - find_pre_post_state_expr - (fcx, expr_poststate(fcx.ccx, val), sub) || changed; - changed = - extend_poststate_ann(fcx.ccx, e.id, - expr_poststate(fcx.ccx, sub)); - ret changed; + ret find_pre_post_state_two(fcx, pres, val, sub, e.id, oper_pure); } case (expr_alt(?val, ?alts)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; changed = find_pre_post_state_expr(fcx, pres, val) || changed; auto e_post = expr_poststate(fcx.ccx, val); auto a_post; @@ -624,32 +549,20 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { a_post = e_post; } - changed = extend_poststate_ann(fcx.ccx, e.id, a_post) || changed; + changed = set_poststate_ann(fcx.ccx, e.id, a_post) || changed; ret changed; } case (expr_field(?val, _)) { - changed = find_pre_post_state_expr(fcx, pres, val); - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, val)) || changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, val, e.id, none); } case (expr_unary(_, ?operand)) { - changed = find_pre_post_state_expr(fcx, pres, operand) || changed; - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - ret extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, operand)) - || changed; + ret find_pre_post_state_sub(fcx, pres, operand, e.id, none); } case (expr_cast(?operand, _)) { - changed = find_pre_post_state_expr(fcx, pres, operand) || changed; - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - ret extend_poststate_ann - (fcx.ccx, e.id, expr_poststate(fcx.ccx, operand)) - || changed; + ret find_pre_post_state_sub(fcx, pres, operand, e.id, none); } case (expr_fail(_)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; + changed = set_prestate_ann(fcx.ccx, e.id, pres) || changed; /* if execution continues after fail, then everything is true! woo! */ @@ -658,19 +571,14 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { ret changed; } case (expr_assert(?p)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, p) || changed; - changed = extend_poststate_ann(fcx.ccx, e.id, pres) || changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, p, e.id, none); } case (expr_check(?p)) { - changed = extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = find_pre_post_state_expr(fcx, pres, p) || changed; - changed = extend_poststate_ann(fcx.ccx, e.id, pres) || changed; /* predicate p holds after this expression executes */ let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); - changed = gen_poststate(fcx, e.id, c.node) || changed; + changed = find_pre_post_state_sub(fcx, pres, p, e.id, + some(c.node)) || changed; ret changed; } case (expr_if_check(?p, ?conseq, ?maybe_alt)) { @@ -686,14 +594,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { case (expr_anon_obj(?anon_obj, _, _)) { alt (anon_obj.with_obj) { case (some(?wt)) { - changed = find_pre_post_state_expr(fcx, pres, wt); - changed = - extend_prestate_ann(fcx.ccx, e.id, pres) || changed; - changed = - extend_poststate_ann(fcx.ccx, e.id, - expr_poststate(fcx.ccx, wt)) || - changed; - ret changed; + ret find_pre_post_state_sub(fcx, pres, wt, e.id, none); } case (none) { ret pure_exp(fcx.ccx, e.id, pres); } } @@ -705,15 +606,15 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { auto changed = false; auto stmt_ann = stmt_to_ann(fcx.ccx, *s); - /* + /* log_err "*At beginning: stmt = "; log_stmt_err(*s); log_err "*prestate = "; - log_err bitv::to_str(stmt_ann.states.prestate); + log_err tritv::to_str(stmt_ann.states.prestate); log_err "*poststate ="; - log_err bitv::to_str(stmt_ann.states.poststate); - log_err "*changed ="; - log_err changed; + log_err tritv::to_str(stmt_ann.states.poststate); + log_err "pres = "; + log_err tritv::to_str(pres); */ alt (s.node) { @@ -723,37 +624,32 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { alt (alocal.node.init) { case (some(?an_init)) { changed = - extend_prestate(stmt_ann.states.prestate, - pres) || changed; + set_prestate(stmt_ann, pres) || changed; + changed = find_pre_post_state_expr(fcx, pres, an_init.expr) || changed; - - /* FIXME less copypasta */ + auto post = tritv_clone(expr_poststate(fcx.ccx, + an_init.expr)); alt (an_init.op) { case (init_move) { - changed = forget_in_poststate(fcx, - an_init.expr.span, id, an_init.expr.id) - || changed; - /* Safe to forget rhs's poststate here 'cause it's a var. */ + clear_in_poststate_expr(fcx, an_init.expr, + post); } - case (_) { /* nothing gets deinitialized */ - changed = - extend_poststate( - stmt_ann.states.poststate, - expr_poststate(fcx.ccx, an_init.expr)) - || changed; - } + case (_) { /* nothing gets deinitialized */ } } - changed = - gen_poststate(fcx, id, - rec(id=alocal.node.id, - c=ninit(alocal.node.ident))) + set_in_poststate_ident(fcx, alocal.node.id, + alocal.node.ident, post); + + /* important to do this in one step to ensure + termination (don't want to set changed to true + for intermediate changes) */ + changed = set_poststate(stmt_ann, post) || changed; - + /* log_err "Summary: stmt = "; log_stmt_err(*s); @@ -769,22 +665,18 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { } case (none) { changed = - extend_prestate(stmt_ann.states.prestate, - pres) || changed; + set_prestate(stmt_ann, pres) || changed; changed = - extend_poststate(stmt_ann.states.poststate, - pres) || changed; + set_poststate(stmt_ann, pres) || changed; ret changed; } } } case (decl_item(?an_item)) { changed = - extend_prestate(stmt_ann.states.prestate, pres) || - changed; + set_prestate(stmt_ann, pres) || changed; changed = - extend_poststate(stmt_ann.states.poststate, pres) || - changed; + set_poststate(stmt_ann, pres) || changed; /* the outer "walk" will recurse into the item */ ret changed; @@ -794,14 +686,13 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool { case (stmt_expr(?ex, _)) { changed = find_pre_post_state_expr(fcx, pres, ex) || changed; changed = - extend_prestate(stmt_ann.states.prestate, - expr_prestate(fcx.ccx, ex)) || changed; + set_prestate(stmt_ann, expr_prestate(fcx.ccx, ex)) || changed; changed = - extend_poststate(stmt_ann.states.poststate, - expr_poststate(fcx.ccx, ex)) || changed; - + set_poststate(stmt_ann, expr_poststate(fcx.ccx, ex)) + || changed; + /* - log_err("Summary: stmt = "); + log_err "Finally:"; log_stmt_err(*s); log_err("prestate = "); // log_err(bitv::to_str(stmt_ann.states.prestate)); @@ -848,7 +739,7 @@ fn find_pre_post_state_block(&fn_ctxt fcx, &prestate pres0, &block b) -> set_prestate_ann(fcx.ccx, b.node.id, pres0); set_poststate_ann(fcx.ccx, b.node.id, post); - + /* log_err "For block:"; log_block_err(b); @@ -881,16 +772,7 @@ fn find_pre_post_state_fn(&fn_ctxt fcx, &_fn f) -> bool { if (!type_is_nil(fcx.ccx.tcx, tailty) && !type_is_bot(fcx.ccx.tcx, tailty)) { auto p = false_postcond(num_local_vars); - set_poststate_ann(fcx.ccx, tailexpr.id, p); - // be sure to set the block poststate to the same thing set_poststate_ann(fcx.ccx, f.body.node.id, p); - alt (fcx.enclosing.cf) { - case (noreturn) { - kill_poststate(fcx, tailexpr.id, - rec(id=fcx.id, c=ninit(fcx.name))); - } - case (_) { } - } } } case (none) {/* fallthrough */ } diff --git a/src/comp/middle/tstate/tritv.rs b/src/comp/middle/tstate/tritv.rs index 1531fde1092..aa7ee64b395 100644 --- a/src/comp/middle/tstate/tritv.rs +++ b/src/comp/middle/tstate/tritv.rs @@ -17,6 +17,7 @@ export tritv_intersect; export tritv_copy; export tritv_clear; export tritv_doesntcare; +export to_str; /* for a fixed index: 10 = "this constraint may or may not be true after execution" @@ -81,7 +82,6 @@ fn trit_or(trit a, trit b) -> trit { } } -// FIXME: not sure about this fn trit_and(trit a, trit b) -> trit { alt (a) { case (dont_care) { dont_care } @@ -89,13 +89,15 @@ fn trit_and(trit a, trit b) -> trit { alt (b) { case (dont_care) { dont_care } case (ttrue) { ttrue } - case (tfalse) { tfalse } // FIXME: ??? + case (tfalse) { dont_care } // ??? } } case (tfalse) { tfalse } } } +fn change(bool changed, trit old, trit new) -> bool { changed || new != old } + fn tritv_difference(&t p1, &t p2) -> bool { let uint i = 0u; assert (p1.nbits == p2.nbits); @@ -104,7 +106,7 @@ fn tritv_difference(&t p1, &t p2) -> bool { while (i < sz) { auto old = tritv_get(p1, i); auto new = trit_minus(old, tritv_get(p2, i)); - changed = changed || (old != new); + changed = change(changed, old, new); tritv_set(i, p1, new); i += 1u; } @@ -119,7 +121,7 @@ fn tritv_union(&t p1, &t p2) -> bool { while (i < sz) { auto old = tritv_get(p1, i); auto new = trit_or(old, tritv_get(p2, i)); - changed = changed || (old != new); + changed = change(changed, old, new); tritv_set(i, p1, new); i += 1u; } @@ -134,7 +136,7 @@ fn tritv_intersect(&t p1, &t p2) -> bool { while (i < sz) { auto old = tritv_get(p1, i); auto new = trit_and(old, tritv_get(p2, i)); - changed = changed || (old != new); + changed = change(changed, old, new); tritv_set(i, p1, new); i += 1u; } @@ -166,24 +168,26 @@ fn tritv_set(uint i, &t v, trit t) -> bool { bitv::set(v.val, i, false); } } - ret (old != t); + ret change(false, old, t); } fn tritv_copy(&t target, &t source) -> bool { let uint i = 0u; assert (target.nbits == source.nbits); auto changed = false; - auto old; - auto new; + auto oldunc; + auto newunc; + auto oldval; + auto newval; while (i < target.nbits) { - old = bitv::get(target.uncertain, i); - new = bitv::get(source.uncertain, i); - bitv::set(target.uncertain, i, new); - changed = changed || (old != new); - old = bitv::get(target.val, i); - new = bitv::get(source.val, i); - bitv::set(target.val, i, new); - changed = changed || (old != new); + oldunc = bitv::get(target.uncertain, i); + newunc = bitv::get(source.uncertain, i); + oldval = bitv::get(target.val, i); + newval = bitv::get(source.val, i); + bitv::set(target.uncertain, i, newunc); + changed = changed || (oldunc && !newunc); + bitv::set(target.val, i, newval); + changed = changed || (oldval && !newval); i += 1u; } ret changed; @@ -234,6 +238,20 @@ fn to_vec(&t v) -> vec[uint] { } ret rslt; } + +fn to_str(&t v) -> str { + let uint i = 0u; + let str res = ""; + while (i < v.nbits) { + res += alt (tritv_get(v, i)) { + case (dont_care) { "?" } + case (ttrue) { "1" } + case (tfalse) { "0" } }; + i += 1u; + } + ret res; +} + // // Local Variables: // mode: rust diff --git a/src/lib/vec.rs b/src/lib/vec.rs index 2d42abc8f7f..3be6c1ef9ad 100644 --- a/src/lib/vec.rs +++ b/src/lib/vec.rs @@ -116,7 +116,7 @@ fn buf_off[T](array[T] v, uint offset) -> vbuf { fn print_debug_info[T](array[T] v) { rustrt::vec_print_debug_info[T](v); } - +// FIXME: typestate precondition (list is non-empty) // Returns the last element of v. fn last[T](array[T] v) -> option::t[T] { auto l = len[T](v); diff --git a/src/test/compile-fail/pred-assign.rs b/src/test/compile-fail/pred-assign.rs new file mode 100644 index 00000000000..784164a589e --- /dev/null +++ b/src/test/compile-fail/pred-assign.rs @@ -0,0 +1,20 @@ +// xfail-stage0 +// -*- rust -*- + +// error-pattern: Unsatisfied precondition constraint (for example, lt(a, b) + +fn f(int a, int b) : lt(a,b) { +} + +pred lt(int a, int b) -> bool { + ret a < b; +} + +fn main() { + let int a = 10; + let int b = 23; + let int c = 77; + check lt(a,b); + a = 24; + f(a,b); +} diff --git a/src/test/compile-fail/pred-swap.rs b/src/test/compile-fail/pred-swap.rs new file mode 100644 index 00000000000..9d21ba75933 --- /dev/null +++ b/src/test/compile-fail/pred-swap.rs @@ -0,0 +1,20 @@ +// xfail-stage0 +// -*- rust -*- + +// error-pattern: Unsatisfied precondition constraint (for example, lt(a, b) + +fn f(int a, int b) : lt(a,b) { +} + +pred lt(int a, int b) -> bool { + ret a < b; +} + +fn main() { + let int a = 10; + let int b = 23; + let int c = 77; + check lt(a,b); + b <-> a; + f(a,b); +}