diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs index 7c035f84ae8..d4bda29a9b9 100644 --- a/src/comp/driver/rustc.rs +++ b/src/comp/driver/rustc.rs @@ -157,7 +157,8 @@ options: --time-passes time the individual phases of the compiler --time-llvm-passes time the individual phases of the LLVM backend --sysroot override the system root (default: rustc's directory) - --no-typestate don't run the typestate pass (unsafe!)\n\n"); + --no-typestate don't run the typestate pass (unsafe!) + --check-claims treat 'claim' and 'check' synonymously\n\n"); } fn get_os(str triple) -> session::os { @@ -226,6 +227,7 @@ fn build_session_options(str binary, getopts::match match, str binary_dir) -> auto time_llvm_passes = opt_present(match, "time-llvm-passes"); auto run_typestate = !opt_present(match, "no-typestate"); auto sysroot_opt = getopts::opt_maybe_str(match, "sysroot"); + auto check_claims = opt_present(match, "check-claims"); let uint opt_level = if (opt_present(match, "O")) { if (opt_present(match, "OptLevel")) { @@ -261,6 +263,7 @@ fn build_session_options(str binary, getopts::match match, str binary_dir) -> stats=stats, time_passes=time_passes, time_llvm_passes=time_llvm_passes, + check_claims=check_claims, output_type=output_type, library_search_paths=library_search_paths, sysroot=sysroot); @@ -296,7 +299,7 @@ fn main(vec[str] args) { optflag("c"), optopt("o"), optflag("g"), optflag("save-temps"), optopt("sysroot"), optflag("stats"), optflag("time-passes"), optflag("time-llvm-passes"), optflag("no-typestate"), - optflag("noverify")]; + optflag("check-claims"), optflag("noverify")]; auto binary = vec::shift[str](args); auto binary_dir = fs::dirname(binary); auto match = diff --git a/src/comp/driver/session.rs b/src/comp/driver/session.rs index da710fd3389..d416d9c57f4 100644 --- a/src/comp/driver/session.rs +++ b/src/comp/driver/session.rs @@ -32,6 +32,7 @@ type options = bool stats, bool time_passes, bool time_llvm_passes, + bool check_claims, back::link::output_type output_type, vec[str] library_search_paths, str sysroot); diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index f63a5636211..cae0794c945 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -231,6 +231,7 @@ type field = spanned[field_]; tag spawn_dom { dom_implicit; dom_thread; } +tag check_mode { checked; unchecked; } // FIXME: temporary tag seq_kind { sk_unique; sk_rc; } @@ -286,7 +287,7 @@ tag expr_ { expr_assert(@expr); /* preds that typestate is aware of */ - expr_check(@expr); + expr_check(check_mode, @expr); /* FIXME Would be nice if expr_check desugared to expr_if_check. */ expr_if_check(@expr, block, option::t[@expr]); diff --git a/src/comp/front/fold.rs b/src/comp/front/fold.rs index 9c9b08d9dac..5d3764c858e 100644 --- a/src/comp/front/fold.rs +++ b/src/comp/front/fold.rs @@ -404,7 +404,7 @@ fn noop_fold_expr(&expr_ e, ast_fold fld) -> expr_ { case (expr_be(?e)) { expr_be(fld.fold_expr(e)) } case (expr_log(?lv, ?e)) { expr_log(lv, fld.fold_expr(e)) } case (expr_assert(?e)) { expr_assert(fld.fold_expr(e)) } - case (expr_check(?e)) { expr_check(fld.fold_expr(e)) } + case (expr_check(?m, ?e)) { expr_check(m, fld.fold_expr(e)) } case (expr_port(?ot)) { expr_port(alt(ot) { case (option::some(?t)) { option::some(fld.fold_ty(t)) } diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs index 454e00ea77a..d1f47eb06c1 100644 --- a/src/comp/front/parser.rs +++ b/src/comp/front/parser.rs @@ -865,7 +865,20 @@ fn parse_bottom_expr(&parser p) -> @ast::expr { auto e = parse_expr(p); auto hi = e.span.hi; - ex = ast::expr_check(e); + ex = ast::expr_check(ast::checked, e); + } else if (eat_word(p, "claim")) { + /* Same rules as check, except that if check-claims + is enabled (a command-line flag), then the parser turns + claims into check */ + + auto e = parse_expr(p); + auto hi = e.span.hi; + ex = if (p.get_session().get_opts().check_claims) { + ast::expr_check(ast::checked, e) + } + else { + ast::expr_check(ast::unchecked, e) + }; } else if (eat_word(p, "ret")) { alt (p.peek()) { case (token::SEMI) { ex = ast::expr_ret(none); } @@ -1596,7 +1609,7 @@ fn stmt_ends_with_semi(&ast::stmt stmt) -> bool { case (ast::expr_put(_)) { true } case (ast::expr_be(_)) { true } case (ast::expr_log(_, _)) { true } - case (ast::expr_check(_)) { true } + case (ast::expr_check(_, _)) { true } case (ast::expr_if_check(_, _, _)) { false } case (ast::expr_port(_)) { true } case (ast::expr_chan(_)) { true } diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs index 95488f76a20..79fadcd8c9f 100644 --- a/src/comp/middle/trans.rs +++ b/src/comp/middle/trans.rs @@ -5988,9 +5988,17 @@ fn trans_expr_out(&@block_ctxt cx, &@ast::expr e, out_method output) -> case (ast::expr_assert(?a)) { ret trans_check_expr(cx, a, "Assertion"); } - case (ast::expr_check(?a)) { + case (ast::expr_check(ast::checked, ?a)) { ret trans_check_expr(cx, a, "Predicate"); } + case (ast::expr_check(ast::unchecked, ?a)) { + if (cx.fcx.lcx.ccx.sess.get_opts().check_claims) { + ret trans_check_expr(cx, a, "Claim"); + } + else { + ret rslt(cx, C_nil()); + } + } case (ast::expr_break) { ret trans_break(e.span, cx); } case (ast::expr_cont) { ret trans_cont(e.span, cx); } case (ast::expr_ret(?ex)) { ret trans_ret(cx, ex); } diff --git a/src/comp/middle/tstate/collect_locals.rs b/src/comp/middle/tstate/collect_locals.rs index 2a23dac596b..79375c4b40d 100644 --- a/src/comp/middle/tstate/collect_locals.rs +++ b/src/comp/middle/tstate/collect_locals.rs @@ -36,7 +36,7 @@ fn collect_local(&ctxt cx, &@local loc) { fn collect_pred(&ctxt cx, &@expr e) { alt (e.node) { - case (expr_check(?ch)) { + case (expr_check(_, ?ch)) { vec::push(*cx.cs, expr_to_constr(cx.tcx, ch)); } case (expr_if_check(?ex, _, _)) { diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs index 3e27e665054..ccff10fae5b 100644 --- a/src/comp/middle/tstate/pre_post_conditions.rs +++ b/src/comp/middle/tstate/pre_post_conditions.rs @@ -536,7 +536,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) { find_pre_post_expr(fcx, p); copy_pre_post(fcx.ccx, e.id, p); } - case (expr_check(?p)) { + case (expr_check(_, ?p)) { find_pre_post_expr(fcx, p); copy_pre_post(fcx.ccx, e.id, p); /* predicate p holds after this expression executes */ diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs index 82274937c8d..04b29f5ffa5 100644 --- a/src/comp/middle/tstate/states.rs +++ b/src/comp/middle/tstate/states.rs @@ -554,7 +554,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool { case (expr_assert(?p)) { ret find_pre_post_state_sub(fcx, pres, p, e.id, none); } - case (expr_check(?p)) { + case (expr_check(_, ?p)) { /* predicate p holds after this expression executes */ let aux::constr c = expr_to_constr(fcx.ccx.tcx, p); ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node)); diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index a47ef47ed80..95cd9d77b26 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1626,7 +1626,7 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) { auto expr_t = check_expr(fcx, e); write::nil_ty(fcx.ccx.tcx, id); } - case (ast::expr_check(?e)) { + case (ast::expr_check(_, ?e)) { check_pred_expr(fcx, e); write::nil_ty(fcx.ccx.tcx, id); } diff --git a/src/comp/middle/visit.rs b/src/comp/middle/visit.rs index 98db56e96c3..e2d0248ae20 100644 --- a/src/comp/middle/visit.rs +++ b/src/comp/middle/visit.rs @@ -372,7 +372,7 @@ fn visit_expr[E](&@expr ex, &E e, &vt[E] v) { case (expr_put(?eo)) { visit_expr_opt(eo, e, v); } case (expr_be(?x)) { vt(v).visit_expr(x, e, v); } case (expr_log(_, ?x)) { vt(v).visit_expr(x, e, v); } - case (expr_check(?x)) { vt(v).visit_expr(x, e, v); } + case (expr_check(_, ?x)) { vt(v).visit_expr(x, e, v); } case (expr_assert(?x)) { vt(v).visit_expr(x, e, v); } case (expr_port(_)) { } case (expr_chan(?x)) { vt(v).visit_expr(x, e, v); } diff --git a/src/comp/middle/walk.rs b/src/comp/middle/walk.rs index f4c954298fd..c6f60783571 100644 --- a/src/comp/middle/walk.rs +++ b/src/comp/middle/walk.rs @@ -378,7 +378,7 @@ fn walk_expr(&ast_visitor v, @ast::expr e) { case (ast::expr_put(?eo)) { walk_expr_opt(v, eo); } case (ast::expr_be(?x)) { walk_expr(v, x); } case (ast::expr_log(_, ?x)) { walk_expr(v, x); } - case (ast::expr_check(?x)) { walk_expr(v, x); } + case (ast::expr_check(_, ?x)) { walk_expr(v, x); } case (ast::expr_assert(?x)) { walk_expr(v, x); } case (ast::expr_port(_)) { } case (ast::expr_chan(?x)) { walk_expr(v, x); } diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs index 332d4dd3aca..433a7234dd4 100644 --- a/src/comp/pretty/pprust.rs +++ b/src/comp/pretty/pprust.rs @@ -859,8 +859,15 @@ fn print_expr(&ps s, &@ast::expr expr) { } print_expr(s, expr); } - case (ast::expr_check(?expr)) { - word_nbsp(s, "check"); + case (ast::expr_check(?m, ?expr)) { + alt (m) { + case (ast::unchecked) { + word_nbsp(s, "claim"); + } + case (ast::checked) { + word_nbsp(s, "check"); + } + } popen(s); print_expr(s, expr); pclose(s); diff --git a/src/test/run-fail/fn-constraint-claim.rs b/src/test/run-fail/fn-constraint-claim.rs new file mode 100644 index 00000000000..d70bef210f1 --- /dev/null +++ b/src/test/run-fail/fn-constraint-claim.rs @@ -0,0 +1,16 @@ +// xfail-stage0 +// error-pattern:quux +use std; +import std::str::*; +import std::uint::*; + +fn nop(uint a, uint b) : le(a, b) { + fail "quux"; +} + +fn main() { + let uint a = 5u; + let uint b = 4u; + claim le(a, b); + nop(a, b); +} \ No newline at end of file diff --git a/src/test/run-pass/claim-nonterm.rs b/src/test/run-pass/claim-nonterm.rs new file mode 100644 index 00000000000..d86154e9ea8 --- /dev/null +++ b/src/test/run-pass/claim-nonterm.rs @@ -0,0 +1,15 @@ +// xfail-stage0 +// tests that the pred in a claim isn't actually eval'd +use std; +import std::str::*; +import std::uint::*; + +pred fails(uint a) -> bool { + fail; +} + +fn main() { + let uint a = 5u; + let uint b = 4u; + claim fails(b); +} \ No newline at end of file