From 219924e669d98bfea2a6b48ac0b0638df1234432 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Thu, 16 Jun 2011 11:56:34 -0700 Subject: [PATCH] Bring back if-check Add "if check" (expr_if_check), a variation on check that executes an "else" clause rather than failing if the check doesn't hold. --- src/comp/front/ast.rs | 3 + src/comp/front/parser.rs | 19 ++- src/comp/middle/trans.rs | 7 +- src/comp/middle/tstate/collect_locals.rs | 3 + src/comp/middle/tstate/pre_post_conditions.rs | 104 ++++++++------- src/comp/middle/tstate/states.rs | 76 ++++++----- src/comp/middle/ty.rs | 1 + src/comp/middle/typeck.rs | 120 ++++++++++-------- src/comp/middle/visit.rs | 5 + src/comp/middle/walk.rs | 6 + src/test/run-fail/if-check-fail.rs | 26 ++++ src/test/run-pass/if-check.rs | 21 ++- 12 files changed, 258 insertions(+), 133 deletions(-) create mode 100644 src/test/run-fail/if-check-fail.rs diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index c05179ba550..b07d3d9fd80 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -269,6 +269,9 @@ fn unop_to_str(unop op) -> str { /* preds that typestate is aware of */ expr_check(@expr, ann); + /* FIXME Would be nice if expr_check desugared + to expr_if_check. */ + expr_if_check(@expr, block, option::t[@expr], ann); expr_port(ann); expr_chan(@expr, ann); expr_anon_obj(anon_obj, vec[ty_param], obj_def_ids, ann); diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs index be7e229b4e6..65f30195b14 100644 --- a/src/comp/front/parser.rs +++ b/src/comp/front/parser.rs @@ -1187,7 +1187,9 @@ fn parse_assign_expr(&parser p) -> @ast::expr { ret lhs; } -fn parse_if_expr(&parser p) -> @ast::expr { +fn parse_if_expr_1(&parser p) -> tup(@ast::expr, + ast::block, option::t[@ast::expr], + ast::ann, uint, uint) { auto lo = p.get_last_lo_pos(); expect(p, token::LPAREN); auto cond = parse_expr(p); @@ -1200,7 +1202,20 @@ fn parse_if_expr(&parser p) -> @ast::expr { els = some(elexpr); hi = elexpr.span.hi; } - ret @spanned(lo, hi, ast::expr_if(cond, thn, els, p.get_ann())); + ret tup(cond, thn, els, p.get_ann(), lo, hi); +} + +fn parse_if_expr(&parser p) -> @ast::expr { + auto lo = p.get_last_lo_pos(); + if (eat_word(p, "check")) { + auto q = parse_if_expr_1(p); + ret @spanned(q._4, q._5, + ast::expr_if_check(q._0, q._1, q._2, q._3)); + } + else { + auto q = parse_if_expr_1(p); + ret @spanned(q._4, q._5, ast::expr_if(q._0, q._1, q._2, q._3)); + } } fn parse_fn_expr(&parser p) -> @ast::expr { diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs index df8743214a7..6c79f12cffa 100644 --- a/src/comp/middle/trans.rs +++ b/src/comp/middle/trans.rs @@ -5516,6 +5516,10 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) -> ret with_out_method(bind trans_if(cx, cond, thn, els, ann, _), cx, ann, output); } + case (ast::expr_if_check(?cond, ?thn, ?els, ?ann)) { + ret with_out_method(bind trans_if(cx, cond, thn, els, ann, _), cx, + ann, output); + } case (ast::expr_for(?decl, ?seq, ?body, _)) { ret trans_for(cx, decl, seq, body); } @@ -5689,7 +5693,8 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) -> } case (_) { // The expression is an lvalue. Fall through. - + assert (ty::is_lval(e)); // make sure it really is and that we + // didn't forget to add a case for a new expr! } } // lval cases fall through to trans_lval and then diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index f669afa965d..587caf244b3 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -37,6 +37,9 @@ fn collect_pred(&ctxt cx, &@expr e) { case (expr_check(?e, _)) { vec::push(*cx.cs, expr_to_constr(cx.tcx, e)); } + case (expr_if_check(?e, _, _, _)) { + vec::push(*cx.cs, expr_to_constr(cx.tcx, e)); + } // If it's a call, generate appropriate instances of the // call's constraints. case (expr_call(?operator, ?operands, ?a)) { diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index cfa5aed2faf..5cc5679d2dd 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -172,6 +172,52 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body, set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond); } +// Generates a pre/post assuming that a is the +// annotation for an if-expression with consequent conseq +// and alternative maybe_alt +fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, + &option::t[@expr] maybe_alt, &ann a) { + auto num_local_vars = num_constraints(fcx.enclosing); + find_pre_post_block(fcx, conseq); + alt (maybe_alt) { + case (none) { + auto precond_res = + seq_preconds(fcx, + [expr_pp(fcx.ccx, antec), + block_pp(fcx.ccx, conseq)]); + set_pre_and_post(fcx.ccx, a, precond_res, + expr_poststate(fcx.ccx, antec)); + } + case (some(?altern)) { + find_pre_post_expr(fcx, altern); + auto precond_true_case = + seq_preconds(fcx, + [expr_pp(fcx.ccx, antec), + block_pp(fcx.ccx, conseq)]); + auto postcond_true_case = + union_postconds(num_local_vars, + [expr_postcond(fcx.ccx, antec), + block_postcond(fcx.ccx, conseq)]); + auto precond_false_case = + seq_preconds(fcx, + [expr_pp(fcx.ccx, antec), + expr_pp(fcx.ccx, altern)]); + auto postcond_false_case = + union_postconds(num_local_vars, + [expr_postcond(fcx.ccx, antec), + expr_postcond(fcx.ccx, altern)]); + auto precond_res = + union_postconds(num_local_vars, + [precond_true_case, + precond_false_case]); + auto postcond_res = + intersect_postconds([postcond_true_case, + postcond_false_case]); + set_pre_and_post(fcx.ccx, a, precond_res, postcond_res); + } + } +} + fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann, &ann new_var, &path pth) { alt (ann_to_def(fcx.ccx, new_var)) { @@ -345,47 +391,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { } case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { find_pre_post_expr(fcx, antec); - find_pre_post_block(fcx, conseq); - alt (maybe_alt) { - case (none) { - log "333"; - auto precond_res = - seq_preconds(fcx, - [expr_pp(fcx.ccx, antec), - block_pp(fcx.ccx, conseq)]); - set_pre_and_post(fcx.ccx, a, precond_res, - expr_poststate(fcx.ccx, antec)); - } - case (some(?altern)) { - find_pre_post_expr(fcx, altern); - log "444"; - auto precond_true_case = - seq_preconds(fcx, - [expr_pp(fcx.ccx, antec), - block_pp(fcx.ccx, conseq)]); - auto postcond_true_case = - union_postconds(num_local_vars, - [expr_postcond(fcx.ccx, antec), - block_postcond(fcx.ccx, conseq)]); - log "555"; - auto precond_false_case = - seq_preconds(fcx, - [expr_pp(fcx.ccx, antec), - expr_pp(fcx.ccx, altern)]); - auto postcond_false_case = - union_postconds(num_local_vars, - [expr_postcond(fcx.ccx, antec), - expr_postcond(fcx.ccx, altern)]); - auto precond_res = - union_postconds(num_local_vars, - [precond_true_case, - precond_false_case]); - auto postcond_res = - intersect_postconds([postcond_true_case, - postcond_false_case]); - set_pre_and_post(fcx.ccx, a, precond_res, postcond_res); - } - } + join_then_else(fcx, antec, conseq, maybe_alt, a); } case (expr_binary(?bop, ?l, ?r, ?a)) { /* *unless* bop is lazy (e.g. and, or)? @@ -484,9 +490,6 @@ fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp, copy_pre_post(fcx.ccx, a, p); } case (expr_check(?p, ?a)) { - /* FIXME: Can we bypass this by having a - node-id-to-constr_occ table? */ - find_pre_post_expr(fcx, p); copy_pre_post(fcx.ccx, a, p); /* predicate p holds after this expression executes */ @@ -494,6 +497,19 @@ fn combine_pp(pre_and_post antec, fn_ctxt fcx, &pre_and_post pp, let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); gen(fcx, a, c.node); } + case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) { + find_pre_post_expr(fcx, p); + copy_pre_post(fcx.ccx, a, p); + /* the typestate for the whole expression */ + join_then_else(fcx, p, conseq, maybe_alt, a); + + /* predicate p holds inside the "thn" expression */ + /* (so far, the negation of p does *not* hold inside + the "elsopt" expression) */ + let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); + gen(fcx, conseq.node.a, c.node); + } + case (expr_bind(?operator, ?maybe_args, ?a)) { auto args = vec::cat_options[@expr](maybe_args); vec::push[@expr](args, operator); /* ??? order of eval? */ diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index ebf6b7ca300..856b8c3f981 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -129,6 +129,38 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool { } } +fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq, + &option::t[@expr] maybe_alt, &ann a) -> bool { + auto changed = false; + + changed = + find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec), + conseq) || changed; + alt (maybe_alt) { + case (none) { + changed = + extend_poststate_ann(fcx.ccx, a, + expr_poststate(fcx.ccx, antec)) + || changed; + } + case (some(?altern)) { + changed = + find_pre_post_state_expr(fcx, + expr_poststate(fcx.ccx, + antec), + altern) || changed; + auto poststate_res = + intersect_postconds([block_poststate(fcx.ccx, conseq), + expr_poststate(fcx.ccx, + altern)]); + changed = + extend_poststate_ann(fcx.ccx, a, poststate_res) || + changed; + } + } + ret changed; +} + 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); @@ -407,37 +439,9 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) { changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; changed = find_pre_post_state_expr(fcx, pres, antec) || changed; - changed = - find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec), - conseq) || changed; - alt (maybe_alt) { - case (none) { - changed = - extend_poststate_ann(fcx.ccx, a, - expr_poststate(fcx.ccx, antec)) - || changed; - } - case (some(?altern)) { - changed = - find_pre_post_state_expr(fcx, - expr_poststate(fcx.ccx, - antec), - altern) || changed; - auto poststate_res = - intersect_postconds([block_poststate(fcx.ccx, conseq), - expr_poststate(fcx.ccx, - altern)]); - changed = - extend_poststate_ann(fcx.ccx, a, poststate_res) || - changed; - } - } - log "if:"; - log_expr(*e); - log "new prestate:"; - log_bitv(fcx, pres); - log "new poststate:"; - log_bitv(fcx, expr_poststate(fcx.ccx, e)); + changed = join_then_else(fcx, antec, conseq, maybe_alt, a) + || changed; + ret changed; } case (expr_binary(?bop, ?l, ?r, ?a)) { @@ -613,6 +617,16 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { changed = gen_poststate(fcx, a, c.node) || changed; ret changed; } + case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) { + changed = extend_prestate_ann(fcx.ccx, a, pres) || changed; + changed = find_pre_post_state_expr(fcx, pres, p) || changed; + let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); + changed = gen_poststate(fcx, expr_ann(p), c.node) || changed; + + changed = join_then_else(fcx, p, conseq, maybe_alt, a) + || changed; + ret changed; + } case (expr_break(?a)) { ret pure_exp(fcx.ccx, a, pres); } case (expr_cont(?a)) { ret pure_exp(fcx.ccx, a, pres); } case (expr_port(?a)) { ret pure_exp(fcx.ccx, a, pres); } diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs index e7f43e75bed..7a6d0f6b0b7 100644 --- a/src/comp/middle/ty.rs +++ b/src/comp/middle/ty.rs @@ -1519,6 +1519,7 @@ fn expr_ann(&@ast::expr e) -> ast::ann { case (ast::expr_lit(_, ?a)) { ret a; } case (ast::expr_cast(_, _, ?a)) { ret a; } case (ast::expr_if(_, _, _, ?a)) { ret a; } + case (ast::expr_if_check(_, _, _, ?a)) { ret a; } case (ast::expr_while(_, _, ?a)) { ret a; } case (ast::expr_for(_, _, _, ?a)) { ret a; } case (ast::expr_for_each(_, _, _, ?a)) { ret a; } diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 0b615740e3c..7ac053a9b16 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1453,6 +1453,68 @@ fn check_for_or_for_each(&@fn_ctxt fcx, &@ast::local local, auto typ = ty::mk_nil(fcx.ccx.tcx); write::ty_only_fixup(fcx, node_id, typ); } + + // A generic function for checking the pred in a check + // or if-check + fn check_pred_expr(&@fn_ctxt fcx, &@ast::expr e) { + check_expr(fcx, e); + demand::simple(fcx, e.span, ty::mk_bool(fcx.ccx.tcx), + expr_ty(fcx.ccx.tcx, e)); + + /* e must be a call expr where all arguments are either + literals or slots */ + alt (e.node) { + case (ast::expr_call(?operator, ?operands, _)) { + alt (operator.node) { + case (ast::expr_path(?oper_name, ?ann)) { + auto d_id; + alt (fcx.ccx.tcx.def_map.get(ann.id)) { + case (ast::def_fn(?_d_id)) { d_id = _d_id; } + } + for (@ast::expr operand in operands) { + if (!ast::is_constraint_arg(operand)) { + auto s = "Constraint args must be \ + slot variables or literals"; + fcx.ccx.tcx.sess.span_err(e.span, s); + } + } + require_pure_function(fcx.ccx, d_id, e.span); + } + case (_) { + auto s = "In a constraint, expected the \ + constraint name to be an explicit name"; + fcx.ccx.tcx.sess.span_err(e.span,s); + } + } + } + case (_) { + fcx.ccx.tcx.sess.span_err(e.span, + "check on non-predicate"); + } + } + } + + // A generic function for checking the then and else in an if + // or if-check + fn check_then_else(&@fn_ctxt fcx, &ast::block thn, + &option::t[@ast::expr] elsopt, &ann a, &span sp) { + check_block(fcx, thn); + auto if_t = + alt (elsopt) { + case (some(?els)) { + check_expr(fcx, els); + auto thn_t = block_ty(fcx.ccx.tcx, thn); + auto elsopt_t = expr_ty(fcx.ccx.tcx, els); + demand::simple(fcx, sp, thn_t, elsopt_t); + if (!ty::type_is_bot(fcx.ccx.tcx, elsopt_t)) { + elsopt_t + } else { thn_t } + } + case (none) { ty::mk_nil(fcx.ccx.tcx) } + }; + write::ty_only_fixup(fcx, a.id, if_t); + } + alt (expr.node) { case (ast::expr_lit(?lit, ?a)) { auto typ = check_lit(fcx.ccx, lit); @@ -1586,42 +1648,12 @@ fn check_for_or_for_each(&@fn_ctxt fcx, &@ast::local local, write::nil_ty(fcx.ccx.tcx, a.id); } case (ast::expr_check(?e, ?a)) { - check_expr(fcx, e); - demand::simple(fcx, expr.span, ty::mk_bool(fcx.ccx.tcx), - expr_ty(fcx.ccx.tcx, e)); - - /* e must be a call expr where all arguments are either - literals or slots */ - alt (e.node) { - case (ast::expr_call(?operator, ?operands, _)) { - alt (operator.node) { - case (ast::expr_path(?oper_name, ?ann)) { - auto d_id; - alt (fcx.ccx.tcx.def_map.get(ann.id)) { - case (ast::def_fn(?_d_id)) { d_id = _d_id; } - } - for (@ast::expr operand in operands) { - if (!ast::is_constraint_arg(operand)) { - auto s = "Constraint args must be \ - slot variables or literals"; - fcx.ccx.tcx.sess.span_err(expr.span, s); - } - } - require_pure_function(fcx.ccx, d_id, expr.span); - write::nil_ty(fcx.ccx.tcx, a.id); - } - case (_) { - auto s = "In a constraint, expected the \ - constraint name to be an explicit name"; - fcx.ccx.tcx.sess.span_err(expr.span,s); - } - } - } - case (_) { - fcx.ccx.tcx.sess.span_err(expr.span, - "check on non-predicate"); - } - } + check_pred_expr(fcx, e); + write::nil_ty(fcx.ccx.tcx, a.id); + } + case (ast::expr_if_check(?cond, ?thn, ?elsopt, ?a)) { + check_pred_expr(fcx, cond); + check_then_else(fcx, thn, elsopt, a, expr.span); } case (ast::expr_assert(?e, ?a)) { check_expr(fcx, e); @@ -1676,21 +1708,7 @@ fn check_for_or_for_each(&@fn_ctxt fcx, &@ast::local local, } case (ast::expr_if(?cond, ?thn, ?elsopt, ?a)) { check_expr(fcx, cond); - check_block(fcx, thn); - auto if_t = - alt (elsopt) { - case (some(?els)) { - check_expr(fcx, els); - auto thn_t = block_ty(fcx.ccx.tcx, thn); - auto elsopt_t = expr_ty(fcx.ccx.tcx, els); - demand::simple(fcx, expr.span, thn_t, elsopt_t); - if (!ty::type_is_bot(fcx.ccx.tcx, elsopt_t)) { - elsopt_t - } else { thn_t } - } - case (none) { ty::mk_nil(fcx.ccx.tcx) } - }; - write::ty_only_fixup(fcx, a.id, if_t); + check_then_else(fcx, thn, elsopt, a, expr.span); } case (ast::expr_for(?decl, ?seq, ?body, ?a)) { check_expr(fcx, seq); diff --git a/src/comp/middle/visit.rs b/src/comp/middle/visit.rs index 642d4d26e52..fe0a19be9fc 100644 --- a/src/comp/middle/visit.rs +++ b/src/comp/middle/visit.rs @@ -279,6 +279,11 @@ fn visit_expr[E](&@expr ex, &E e, &vt[E] v) { vt(v).visit_block(b, e, v); visit_expr_opt(eo, e, v); } + case (expr_if_check(?x, ?b, ?eo, _)) { + vt(v).visit_expr(x, e, v); + vt(v).visit_block(b, e, v); + visit_expr_opt(eo, e, v); + } case (expr_while(?x, ?b, _)) { vt(v).visit_expr(x, e, v); vt(v).visit_block(b, e, v); diff --git a/src/comp/middle/walk.rs b/src/comp/middle/walk.rs index 143069c3f58..c055adde49d 100644 --- a/src/comp/middle/walk.rs +++ b/src/comp/middle/walk.rs @@ -310,6 +310,12 @@ fn walk_expr(&ast_visitor v, @ast::expr e) { walk_block(v, b); walk_expr_opt(v, eo); } + case (ast::expr_if_check(?x, ?b, ?eo, _)) { + walk_expr(v, x); + walk_block(v, b); + walk_expr_opt(v, eo); + } + case (ast::expr_while(?x, ?b, _)) { walk_expr(v, x); walk_block(v, b); diff --git a/src/test/run-fail/if-check-fail.rs b/src/test/run-fail/if-check-fail.rs new file mode 100644 index 00000000000..1de7bd991bd --- /dev/null +++ b/src/test/run-fail/if-check-fail.rs @@ -0,0 +1,26 @@ +// xfail-stage0 +// error-pattern:Number is odd +pred even(uint x) -> bool { + if (x < 2) { + ret false; + } + else if (x == 2) { + ret true; + } + else { + ret even(x - 2); + } +} + +fn foo(uint x) -> () { + if check(even(x)) { + log x; + } + else { + fail "Number is odd"; + } +} + +fn main() { + foo(3u); +} diff --git a/src/test/run-pass/if-check.rs b/src/test/run-pass/if-check.rs index 9f9f8946554..32e4fed6656 100644 --- a/src/test/run-pass/if-check.rs +++ b/src/test/run-pass/if-check.rs @@ -1,6 +1,19 @@ // xfail-stage0 -fn foo(int x) -> () { - if check even(x) { + +pred even(uint x) -> bool { + if (x < 2) { + ret false; + } + else if (x == 2) { + ret true; + } + else { + ret even(x - 2); + } +} + +fn foo(uint x) -> () { + if check(even(x)) { log x; } else { @@ -9,5 +22,5 @@ fn foo(int x) -> () { } fn main() { - foo(2); -} \ No newline at end of file + foo(2u); +} -- GitLab