Add support for unit tests via $[test] attribute

src/lib/type_check.ml

@@ -4630,6 +4630,14 @@ let check_fundef_lazy env def_annot (FD_aux (FD_function (recopt, tannot_opt, fu
     | Some vs_l -> check_tannot_opt ~def_type:"function" vs_l env vtyp_ret tannot_opt
     | None -> ()
   end;
+  (* Check $[test] functions have type unit -> unit. *)
+  (* TODO: Does the annotation go on the type declaration or the function definition? *)
+  begin
+    if Option.is_some (get_def_attribute "test" def_annot) then
+      match (vtyp_args, vtyp_ret) with
+        | [arg], ret when is_unit_typ arg && is_unit_typ ret -> ()
+        | _ -> typ_error l "$[test] functions must have type: unit -> unit"
+  end;
   typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ)));
   let funcl_env =
     if Option.is_some have_val_spec then Env.add_typquant l quant env

src/sail_c_backend/c_backend.ml

@@ -2225,6 +2225,7 @@ let compile_ast env effect_info output_chan c_includes ast =
     let end_extern_cpp = separate hardline (List.map string [""; "#ifdef __cplusplus"; "}"; "#endif"]) in
     let hlhl = hardline ^^ hardline in
 
+    (* TODO: Formatting here isn't quite right. What are the arguments to jump? *)
     let unit_test_functions = string "unit (*const SAIL_TESTS[])(unit) = {" ^^ hardline ^^ jump 2 2 (
       IdSet.fold (fun id acc -> codegen_function_id id ^^ string "," ^^ hardline ^^ acc) ctx.unit_test_ids empty
       ^^ string "0" ^^ hardline
@@ -2235,6 +2236,25 @@ let compile_ast env effect_info output_chan c_includes ast =
       ^^ string "0" ^^ hardline
     ) ^^ string "};" in
 
+    (* A simple function to run the unit tests. It isn't called from anywhere
+       by default and you don't need to use it - you can use SAIL_TESTS directly
+       in your own custom test runner. *)
+    let model_test =
+      [
+        Printf.sprintf "%svoid model_test()" (static ());
+        "{";
+        "  for (size_t i = 0; SAIL_TESTS[i] != 0 && SAIL_TEST_NAMES[i] != 0; ++i) {";
+        "    model_init();";
+        "    printf(\"Testing %s\\n\", SAIL_TEST_NAMES[i]);";
+        "    SAIL_TESTS[i](UNIT);";
+        "    printf(\"Pass\\n\");";
+        "    model_fini();";
+        "  }";
+        "}";
+      ]
+      |> List.map string |> separate hardline
+    in
+
     Document.to_string
       (preamble ^^ hlhl ^^ docs ^^ hlhl
       ^^ ( if not !opt_no_rts then
@@ -2243,7 +2263,8 @@ let compile_ast env effect_info output_chan c_includes ast =
          )
       ^^ model_main ^^ hlhl
       ^^ unit_test_functions ^^ hlhl
-      ^^ unit_test_names ^^ hardline
+      ^^ unit_test_names ^^ hlhl
+      ^^ model_test ^^ hardline
       ^^ end_extern_cpp ^^ hardline
       )
     |> output_string output_chan

test/c/test_attribute.expect

@@ -0,0 +1 @@
+ok

test/c/test_attribute.sail

@@ -0,0 +1,24 @@
+default Order dec
+
+$[test]
+function test_0() -> unit = {
+  print_endline("test_0");
+}
+
+$[test]
+val test_1 : unit -> unit
+
+function test_1() = {
+  print_endline("test_1");
+}
+
+$[test]
+val test_2 : unit -> unit
+
+function test_2() -> unit = {
+  print_endline("test_2");
+}
+
+function main() -> unit = {
+  print_endline("ok");
+}

test/typecheck/fail/test_not_unit_0.expect

@@ -0,0 +1 @@
+test_bad must have type unit -> unit

test/typecheck/fail/test_not_unit_0.sail

@@ -0,0 +1,11 @@
+default Order dec
+
+$[test]
+function test_good() -> unit = {
+  print_endline("test_good");
+}
+
+$[test]
+function test_bad() -> int = 5
+
+function main() -> unit = ()

test/typecheck/fail/test_not_unit_1.expect

@@ -0,0 +1 @@
+test_bad must have type unit -> unit

test/typecheck/fail/test_not_unit_1.sail

@@ -0,0 +1,6 @@
+default Order dec
+
+$[test]
+function test_bad(x : int) -> unit = ()
+
+function main() -> unit = ()

test/typecheck/fail/test_not_unit_2.expect

@@ -0,0 +1 @@
+test_bad must have type unit -> unit

test/typecheck/fail/test_not_unit_2.sail

@@ -0,0 +1,6 @@
+default Order dec
+
+$[test]
+function test_bad(x : unit, y : unit) -> unit = ()
+
+function main() -> unit = ()

test/typecheck/fail/test_not_unit_3.expect

@@ -0,0 +1 @@
+test_bad must have type unit -> unit

test/typecheck/fail/test_not_unit_3.sail

@@ -0,0 +1,8 @@
+default Order dec
+
+$[test]
+val test_bad : unit -> int
+
+function test_bad() = 5
+
+function main() -> unit = ()

test/typecheck/fail/test_not_unit_4.expect

@@ -0,0 +1 @@
+test attribute must be on function declaration

test/typecheck/fail/test_not_unit_4.sail

@@ -0,0 +1,8 @@
+default Order dec
+
+val test_bad : unit -> unit
+
+$[test]
+function test_bad() = ()
+
+function main() -> unit = ()