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.

13 files changed, 48 insertions, 15 deletions

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 <path>   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);