Skip to content

Commit 219924e

Browse files
catamorphismcatamorphism
committed
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.
1 parent 94ae459 commit 219924e

File tree

12 files changed

+258
-133
lines changed

12 files changed

+258
-133
lines changed

‎src/comp/front/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,6 +269,9 @@ tag expr_ {
269269
270270
/* preds that typestate is aware of */
271271
expr_check(@expr, ann);
272+
/* FIXME Would be nice if expr_check desugared
273+
to expr_if_check. */
274+
expr_if_check(@expr, block, option::t[@expr], ann);
272275
expr_port(ann);
273276
expr_chan(@expr, ann);
274277
expr_anon_obj(anon_obj, vec[ty_param], obj_def_ids, ann);

‎src/comp/front/parser.rs

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1187,7 +1187,9 @@ fn parse_assign_expr(&parser p) -> @ast::expr {
11871187
ret lhs;
11881188
}
11891189

1190-
fn parse_if_expr(&parser p) -> @ast::expr {
1190+
fn parse_if_expr_1(&parser p) -> tup(@ast::expr,
1191+
ast::block, option::t[@ast::expr],
1192+
ast::ann, uint, uint) {
11911193
auto lo = p.get_last_lo_pos();
11921194
expect(p, token::LPAREN);
11931195
auto cond = parse_expr(p);
@@ -1200,7 +1202,20 @@ fn parse_if_expr(&parser p) -> @ast::expr {
12001202
els = some(elexpr);
12011203
hi = elexpr.span.hi;
12021204
}
1203-
ret @spanned(lo, hi, ast::expr_if(cond, thn, els, p.get_ann()));
1205+
ret tup(cond, thn, els, p.get_ann(), lo, hi);
1206+
}
1207+
1208+
fn parse_if_expr(&parser p) -> @ast::expr {
1209+
auto lo = p.get_last_lo_pos();
1210+
if (eat_word(p, "check")) {
1211+
auto q = parse_if_expr_1(p);
1212+
ret @spanned(q._4, q._5,
1213+
ast::expr_if_check(q._0, q._1, q._2, q._3));
1214+
}
1215+
else {
1216+
auto q = parse_if_expr_1(p);
1217+
ret @spanned(q._4, q._5, ast::expr_if(q._0, q._1, q._2, q._3));
1218+
}
12041219
}
12051220

12061221
fn parse_fn_expr(&parser p) -> @ast::expr {

‎src/comp/middle/trans.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5516,6 +5516,10 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) ->
55165516
ret with_out_method(bind trans_if(cx, cond, thn, els, ann, _), cx,
55175517
ann, output);
55185518
}
5519+
case (ast::expr_if_check(?cond, ?thn, ?els, ?ann)) {
5520+
ret with_out_method(bind trans_if(cx, cond, thn, els, ann, _), cx,
5521+
ann, output);
5522+
}
55195523
case (ast::expr_for(?decl, ?seq, ?body, _)) {
55205524
ret trans_for(cx, decl, seq, body);
55215525
}
@@ -5689,7 +5693,8 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) ->
56895693
}
56905694
case (_) {
56915695
// The expression is an lvalue. Fall through.
5692-
5696+
assert (ty::is_lval(e)); // make sure it really is and that we
5697+
// didn't forget to add a case for a new expr!
56935698
}
56945699
}
56955700
// lval cases fall through to trans_lval and then

‎src/comp/middle/tstate/collect_locals.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,9 @@ fn collect_pred(&ctxt cx, &@expr e) {
3737
case (expr_check(?e, _)) {
3838
vec::push(*cx.cs, expr_to_constr(cx.tcx, e));
3939
}
40+
case (expr_if_check(?e, _, _, _)) {
41+
vec::push(*cx.cs, expr_to_constr(cx.tcx, e));
42+
}
4043
// If it's a call, generate appropriate instances of the
4144
// call's constraints.
4245
case (expr_call(?operator, ?operands, ?a)) {

‎src/comp/middle/tstate/pre_post_conditions.rs

Lines changed: 60 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,52 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
172172
set_pre_and_post(fcx.ccx, a, loop_precond, loop_postcond);
173173
}
174174

175+
// Generates a pre/post assuming that a is the
176+
// annotation for an if-expression with consequent conseq
177+
// and alternative maybe_alt
178+
fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
179+
&option::t[@expr] maybe_alt, &ann a) {
180+
auto num_local_vars = num_constraints(fcx.enclosing);
181+
find_pre_post_block(fcx, conseq);
182+
alt (maybe_alt) {
183+
case (none) {
184+
auto precond_res =
185+
seq_preconds(fcx,
186+
[expr_pp(fcx.ccx, antec),
187+
block_pp(fcx.ccx, conseq)]);
188+
set_pre_and_post(fcx.ccx, a, precond_res,
189+
expr_poststate(fcx.ccx, antec));
190+
}
191+
case (some(?altern)) {
192+
find_pre_post_expr(fcx, altern);
193+
auto precond_true_case =
194+
seq_preconds(fcx,
195+
[expr_pp(fcx.ccx, antec),
196+
block_pp(fcx.ccx, conseq)]);
197+
auto postcond_true_case =
198+
union_postconds(num_local_vars,
199+
[expr_postcond(fcx.ccx, antec),
200+
block_postcond(fcx.ccx, conseq)]);
201+
auto precond_false_case =
202+
seq_preconds(fcx,
203+
[expr_pp(fcx.ccx, antec),
204+
expr_pp(fcx.ccx, altern)]);
205+
auto postcond_false_case =
206+
union_postconds(num_local_vars,
207+
[expr_postcond(fcx.ccx, antec),
208+
expr_postcond(fcx.ccx, altern)]);
209+
auto precond_res =
210+
union_postconds(num_local_vars,
211+
[precond_true_case,
212+
precond_false_case]);
213+
auto postcond_res =
214+
intersect_postconds([postcond_true_case,
215+
postcond_false_case]);
216+
set_pre_and_post(fcx.ccx, a, precond_res, postcond_res);
217+
}
218+
}
219+
}
220+
175221
fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, &ann larger_ann,
176222
&ann new_var, &path pth) {
177223
alt (ann_to_def(fcx.ccx, new_var)) {
@@ -345,47 +391,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
345391
}
346392
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
347393
find_pre_post_expr(fcx, antec);
348-
find_pre_post_block(fcx, conseq);
349-
alt (maybe_alt) {
350-
case (none) {
351-
log "333";
352-
auto precond_res =
353-
seq_preconds(fcx,
354-
[expr_pp(fcx.ccx, antec),
355-
block_pp(fcx.ccx, conseq)]);
356-
set_pre_and_post(fcx.ccx, a, precond_res,
357-
expr_poststate(fcx.ccx, antec));
358-
}
359-
case (some(?altern)) {
360-
find_pre_post_expr(fcx, altern);
361-
log "444";
362-
auto precond_true_case =
363-
seq_preconds(fcx,
364-
[expr_pp(fcx.ccx, antec),
365-
block_pp(fcx.ccx, conseq)]);
366-
auto postcond_true_case =
367-
union_postconds(num_local_vars,
368-
[expr_postcond(fcx.ccx, antec),
369-
block_postcond(fcx.ccx, conseq)]);
370-
log "555";
371-
auto precond_false_case =
372-
seq_preconds(fcx,
373-
[expr_pp(fcx.ccx, antec),
374-
expr_pp(fcx.ccx, altern)]);
375-
auto postcond_false_case =
376-
union_postconds(num_local_vars,
377-
[expr_postcond(fcx.ccx, antec),
378-
expr_postcond(fcx.ccx, altern)]);
379-
auto precond_res =
380-
union_postconds(num_local_vars,
381-
[precond_true_case,
382-
precond_false_case]);
383-
auto postcond_res =
384-
intersect_postconds([postcond_true_case,
385-
postcond_false_case]);
386-
set_pre_and_post(fcx.ccx, a, precond_res, postcond_res);
387-
}
388-
}
394+
join_then_else(fcx, antec, conseq, maybe_alt, a);
389395
}
390396
case (expr_binary(?bop, ?l, ?r, ?a)) {
391397
/* *unless* bop is lazy (e.g. and, or)?
@@ -484,16 +490,26 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
484490
copy_pre_post(fcx.ccx, a, p);
485491
}
486492
case (expr_check(?p, ?a)) {
487-
/* FIXME: Can we bypass this by having a
488-
node-id-to-constr_occ table? */
489-
490493
find_pre_post_expr(fcx, p);
491494
copy_pre_post(fcx.ccx, a, p);
492495
/* predicate p holds after this expression executes */
493496

494497
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
495498
gen(fcx, a, c.node);
496499
}
500+
case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) {
501+
find_pre_post_expr(fcx, p);
502+
copy_pre_post(fcx.ccx, a, p);
503+
/* the typestate for the whole expression */
504+
join_then_else(fcx, p, conseq, maybe_alt, a);
505+
506+
/* predicate p holds inside the "thn" expression */
507+
/* (so far, the negation of p does *not* hold inside
508+
the "elsopt" expression) */
509+
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
510+
gen(fcx, conseq.node.a, c.node);
511+
}
512+
497513
case (expr_bind(?operator, ?maybe_args, ?a)) {
498514
auto args = vec::cat_options[@expr](maybe_args);
499515
vec::push[@expr](args, operator); /* ??? order of eval? */

‎src/comp/middle/tstate/states.rs

Lines changed: 45 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,38 @@ fn gen_if_local(&fn_ctxt fcx, &ann a_new_var, &ann a, &path p) -> bool {
129129
}
130130
}
131131

132+
fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
133+
&option::t[@expr] maybe_alt, &ann a) -> bool {
134+
auto changed = false;
135+
136+
changed =
137+
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
138+
conseq) || changed;
139+
alt (maybe_alt) {
140+
case (none) {
141+
changed =
142+
extend_poststate_ann(fcx.ccx, a,
143+
expr_poststate(fcx.ccx, antec))
144+
|| changed;
145+
}
146+
case (some(?altern)) {
147+
changed =
148+
find_pre_post_state_expr(fcx,
149+
expr_poststate(fcx.ccx,
150+
antec),
151+
altern) || changed;
152+
auto poststate_res =
153+
intersect_postconds([block_poststate(fcx.ccx, conseq),
154+
expr_poststate(fcx.ccx,
155+
altern)]);
156+
changed =
157+
extend_poststate_ann(fcx.ccx, a, poststate_res) ||
158+
changed;
159+
}
160+
}
161+
ret changed;
162+
}
163+
132164
fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
133165
auto changed = false;
134166
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 {
407439
case (expr_if(?antec, ?conseq, ?maybe_alt, ?a)) {
408440
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
409441
changed = find_pre_post_state_expr(fcx, pres, antec) || changed;
410-
changed =
411-
find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, antec),
412-
conseq) || changed;
413-
alt (maybe_alt) {
414-
case (none) {
415-
changed =
416-
extend_poststate_ann(fcx.ccx, a,
417-
expr_poststate(fcx.ccx, antec))
418-
|| changed;
419-
}
420-
case (some(?altern)) {
421-
changed =
422-
find_pre_post_state_expr(fcx,
423-
expr_poststate(fcx.ccx,
424-
antec),
425-
altern) || changed;
426-
auto poststate_res =
427-
intersect_postconds([block_poststate(fcx.ccx, conseq),
428-
expr_poststate(fcx.ccx,
429-
altern)]);
430-
changed =
431-
extend_poststate_ann(fcx.ccx, a, poststate_res) ||
432-
changed;
433-
}
434-
}
435-
log "if:";
436-
log_expr(*e);
437-
log "new prestate:";
438-
log_bitv(fcx, pres);
439-
log "new poststate:";
440-
log_bitv(fcx, expr_poststate(fcx.ccx, e));
442+
changed = join_then_else(fcx, antec, conseq, maybe_alt, a)
443+
|| changed;
444+
441445
ret changed;
442446
}
443447
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 {
613617
changed = gen_poststate(fcx, a, c.node) || changed;
614618
ret changed;
615619
}
620+
case (expr_if_check(?p, ?conseq, ?maybe_alt, ?a)) {
621+
changed = extend_prestate_ann(fcx.ccx, a, pres) || changed;
622+
changed = find_pre_post_state_expr(fcx, pres, p) || changed;
623+
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
624+
changed = gen_poststate(fcx, expr_ann(p), c.node) || changed;
625+
626+
changed = join_then_else(fcx, p, conseq, maybe_alt, a)
627+
|| changed;
628+
ret changed;
629+
}
616630
case (expr_break(?a)) { ret pure_exp(fcx.ccx, a, pres); }
617631
case (expr_cont(?a)) { ret pure_exp(fcx.ccx, a, pres); }
618632
case (expr_port(?a)) { ret pure_exp(fcx.ccx, a, pres); }

‎src/comp/middle/ty.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1519,6 +1519,7 @@ fn expr_ann(&@ast::expr e) -> ast::ann {
15191519
case (ast::expr_lit(_, ?a)) { ret a; }
15201520
case (ast::expr_cast(_, _, ?a)) { ret a; }
15211521
case (ast::expr_if(_, _, _, ?a)) { ret a; }
1522+
case (ast::expr_if_check(_, _, _, ?a)) { ret a; }
15221523
case (ast::expr_while(_, _, ?a)) { ret a; }
15231524
case (ast::expr_for(_, _, _, ?a)) { ret a; }
15241525
case (ast::expr_for_each(_, _, _, ?a)) { ret a; }

0 commit comments

Comments
 (0)