Skip to content

Commit 9f1444c

Browse files
catamorphismcatamorphism
committed
Implement "claim"
Implement "claim" (issue #14), which is a version of "check" that doesn't really do the check at runtime. It's an unsafe feature. The new flag --check-claims turns claims into checks automatically -- but it's off by default, so by default, the assertion in a claim doesn't execute at runtime.
1 parent 866ee6e commit 9f1444c

15 files changed

+79
-15
lines changed

‎src/comp/driver/rustc.rs

+5-2
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,8 @@ options:
157157
--time-passes time the individual phases of the compiler
158158
--time-llvm-passes time the individual phases of the LLVM backend
159159
--sysroot <path> override the system root (default: rustc's directory)
160-
--no-typestate don't run the typestate pass (unsafe!)\n\n");
160+
--no-typestate don't run the typestate pass (unsafe!)
161+
--check-claims treat 'claim' and 'check' synonymously\n\n");
161162
}
162163

163164
fn get_os(str triple) -> session::os {
@@ -226,6 +227,7 @@ fn build_session_options(str binary, getopts::match match, str binary_dir) ->
226227
auto time_llvm_passes = opt_present(match, "time-llvm-passes");
227228
auto run_typestate = !opt_present(match, "no-typestate");
228229
auto sysroot_opt = getopts::opt_maybe_str(match, "sysroot");
230+
auto check_claims = opt_present(match, "check-claims");
229231
let uint opt_level =
230232
if (opt_present(match, "O")) {
231233
if (opt_present(match, "OptLevel")) {
@@ -261,6 +263,7 @@ fn build_session_options(str binary, getopts::match match, str binary_dir) ->
261263
stats=stats,
262264
time_passes=time_passes,
263265
time_llvm_passes=time_llvm_passes,
266+
check_claims=check_claims,
264267
output_type=output_type,
265268
library_search_paths=library_search_paths,
266269
sysroot=sysroot);
@@ -296,7 +299,7 @@ fn main(vec[str] args) {
296299
optflag("c"), optopt("o"), optflag("g"), optflag("save-temps"),
297300
optopt("sysroot"), optflag("stats"), optflag("time-passes"),
298301
optflag("time-llvm-passes"), optflag("no-typestate"),
299-
optflag("noverify")];
302+
optflag("check-claims"), optflag("noverify")];
300303
auto binary = vec::shift[str](args);
301304
auto binary_dir = fs::dirname(binary);
302305
auto match =

‎src/comp/driver/session.rs

+1
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ type options =
3232
bool stats,
3333
bool time_passes,
3434
bool time_llvm_passes,
35+
bool check_claims,
3536
back::link::output_type output_type,
3637
vec[str] library_search_paths,
3738
str sysroot);

‎src/comp/front/ast.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -231,6 +231,7 @@ type field = spanned[field_];
231231
232232
tag spawn_dom { dom_implicit; dom_thread; }
233233
234+
tag check_mode { checked; unchecked; }
234235
235236
// FIXME: temporary
236237
tag seq_kind { sk_unique; sk_rc; }
@@ -286,7 +287,7 @@ tag expr_ {
286287
expr_assert(@expr);
287288
288289
/* preds that typestate is aware of */
289-
expr_check(@expr);
290+
expr_check(check_mode, @expr);
290291
/* FIXME Would be nice if expr_check desugared
291292
to expr_if_check. */
292293
expr_if_check(@expr, block, option::t[@expr]);

‎src/comp/front/fold.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -404,7 +404,7 @@ fn noop_fold_expr(&expr_ e, ast_fold fld) -> expr_ {
404404
case (expr_be(?e)) { expr_be(fld.fold_expr(e)) }
405405
case (expr_log(?lv, ?e)) { expr_log(lv, fld.fold_expr(e)) }
406406
case (expr_assert(?e)) { expr_assert(fld.fold_expr(e)) }
407-
case (expr_check(?e)) { expr_check(fld.fold_expr(e)) }
407+
case (expr_check(?m, ?e)) { expr_check(m, fld.fold_expr(e)) }
408408
case (expr_port(?ot)) {
409409
expr_port(alt(ot) {
410410
case (option::some(?t)) { option::some(fld.fold_ty(t)) }

‎src/comp/front/parser.rs

+15-2
Original file line numberDiff line numberDiff line change
@@ -865,7 +865,20 @@ fn parse_bottom_expr(&parser p) -> @ast::expr {
865865

866866
auto e = parse_expr(p);
867867
auto hi = e.span.hi;
868-
ex = ast::expr_check(e);
868+
ex = ast::expr_check(ast::checked, e);
869+
} else if (eat_word(p, "claim")) {
870+
/* Same rules as check, except that if check-claims
871+
is enabled (a command-line flag), then the parser turns
872+
claims into check */
873+
874+
auto e = parse_expr(p);
875+
auto hi = e.span.hi;
876+
ex = if (p.get_session().get_opts().check_claims) {
877+
ast::expr_check(ast::checked, e)
878+
}
879+
else {
880+
ast::expr_check(ast::unchecked, e)
881+
};
869882
} else if (eat_word(p, "ret")) {
870883
alt (p.peek()) {
871884
case (token::SEMI) { ex = ast::expr_ret(none); }
@@ -1596,7 +1609,7 @@ fn stmt_ends_with_semi(&ast::stmt stmt) -> bool {
15961609
case (ast::expr_put(_)) { true }
15971610
case (ast::expr_be(_)) { true }
15981611
case (ast::expr_log(_, _)) { true }
1599-
case (ast::expr_check(_)) { true }
1612+
case (ast::expr_check(_, _)) { true }
16001613
case (ast::expr_if_check(_, _, _)) { false }
16011614
case (ast::expr_port(_)) { true }
16021615
case (ast::expr_chan(_)) { true }

‎src/comp/middle/trans.rs

+9-1
Original file line numberDiff line numberDiff line change
@@ -5988,9 +5988,17 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) ->
59885988
case (ast::expr_assert(?a)) {
59895989
ret trans_check_expr(cx, a, "Assertion");
59905990
}
5991-
case (ast::expr_check(?a)) {
5991+
case (ast::expr_check(ast::checked, ?a)) {
59925992
ret trans_check_expr(cx, a, "Predicate");
59935993
}
5994+
case (ast::expr_check(ast::unchecked, ?a)) {
5995+
if (cx.fcx.lcx.ccx.sess.get_opts().check_claims) {
5996+
ret trans_check_expr(cx, a, "Claim");
5997+
}
5998+
else {
5999+
ret rslt(cx, C_nil());
6000+
}
6001+
}
59946002
case (ast::expr_break) { ret trans_break(e.span, cx); }
59956003
case (ast::expr_cont) { ret trans_cont(e.span, cx); }
59966004
case (ast::expr_ret(?ex)) { ret trans_ret(cx, ex); }

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ fn collect_local(&ctxt cx, &@local loc) {
3636

3737
fn collect_pred(&ctxt cx, &@expr e) {
3838
alt (e.node) {
39-
case (expr_check(?ch)) {
39+
case (expr_check(_, ?ch)) {
4040
vec::push(*cx.cs, expr_to_constr(cx.tcx, ch));
4141
}
4242
case (expr_if_check(?ex, _, _)) {

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -536,7 +536,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
536536
find_pre_post_expr(fcx, p);
537537
copy_pre_post(fcx.ccx, e.id, p);
538538
}
539-
case (expr_check(?p)) {
539+
case (expr_check(_, ?p)) {
540540
find_pre_post_expr(fcx, p);
541541
copy_pre_post(fcx.ccx, e.id, p);
542542
/* predicate p holds after this expression executes */

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -554,7 +554,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
554554
case (expr_assert(?p)) {
555555
ret find_pre_post_state_sub(fcx, pres, p, e.id, none);
556556
}
557-
case (expr_check(?p)) {
557+
case (expr_check(_, ?p)) {
558558
/* predicate p holds after this expression executes */
559559
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
560560
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));

‎src/comp/middle/typeck.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1626,7 +1626,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) {
16261626
auto expr_t = check_expr(fcx, e);
16271627
write::nil_ty(fcx.ccx.tcx, id);
16281628
}
1629-
case (ast::expr_check(?e)) {
1629+
case (ast::expr_check(_, ?e)) {
16301630
check_pred_expr(fcx, e);
16311631
write::nil_ty(fcx.ccx.tcx, id);
16321632
}

‎src/comp/middle/visit.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -372,7 +372,7 @@ fn visit_expr[E](&@expr ex, &E e, &vt[E] v) {
372372
case (expr_put(?eo)) { visit_expr_opt(eo, e, v); }
373373
case (expr_be(?x)) { vt(v).visit_expr(x, e, v); }
374374
case (expr_log(_, ?x)) { vt(v).visit_expr(x, e, v); }
375-
case (expr_check(?x)) { vt(v).visit_expr(x, e, v); }
375+
case (expr_check(_, ?x)) { vt(v).visit_expr(x, e, v); }
376376
case (expr_assert(?x)) { vt(v).visit_expr(x, e, v); }
377377
case (expr_port(_)) { }
378378
case (expr_chan(?x)) { vt(v).visit_expr(x, e, v); }

‎src/comp/middle/walk.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,7 @@ fn walk_expr(&ast_visitor v, @ast::expr e) {
378378
case (ast::expr_put(?eo)) { walk_expr_opt(v, eo); }
379379
case (ast::expr_be(?x)) { walk_expr(v, x); }
380380
case (ast::expr_log(_, ?x)) { walk_expr(v, x); }
381-
case (ast::expr_check(?x)) { walk_expr(v, x); }
381+
case (ast::expr_check(_, ?x)) { walk_expr(v, x); }
382382
case (ast::expr_assert(?x)) { walk_expr(v, x); }
383383
case (ast::expr_port(_)) { }
384384
case (ast::expr_chan(?x)) { walk_expr(v, x); }

‎src/comp/pretty/pprust.rs

+9-2
Original file line numberDiff line numberDiff line change
@@ -859,8 +859,15 @@ fn print_expr(&ps s, &@ast::expr expr) {
859859
}
860860
print_expr(s, expr);
861861
}
862-
case (ast::expr_check(?expr)) {
863-
word_nbsp(s, "check");
862+
case (ast::expr_check(?m, ?expr)) {
863+
alt (m) {
864+
case (ast::unchecked) {
865+
word_nbsp(s, "claim");
866+
}
867+
case (ast::checked) {
868+
word_nbsp(s, "check");
869+
}
870+
}
864871
popen(s);
865872
print_expr(s, expr);
866873
pclose(s);

‎src/test/run-fail/fn-constraint-claim.rs

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// xfail-stage0
2+
// error-pattern:quux
3+
use std;
4+
import std::str::*;
5+
import std::uint::*;
6+
7+
fn nop(uint a, uint b) : le(a, b) {
8+
fail "quux";
9+
}
10+
11+
fn main() {
12+
let uint a = 5u;
13+
let uint b = 4u;
14+
claim le(a, b);
15+
nop(a, b);
16+
}

‎src/test/run-pass/claim-nonterm.rs

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// xfail-stage0
2+
// tests that the pred in a claim isn't actually eval'd
3+
use std;
4+
import std::str::*;
5+
import std::uint::*;
6+
7+
pred fails(uint a) -> bool {
8+
fail;
9+
}
10+
11+
fn main() {
12+
let uint a = 5u;
13+
let uint b = 4u;
14+
claim fails(b);
15+
}

0 commit comments

Comments
 (0)