Add support to verify test harness (#664) (#672)

This resolves #664. I added an argument to rmc and cargo rmc (--tests) to
allow users to target test harnesses as their verification function.

scripts/cargo-rmc

@@ -24,8 +24,7 @@ def main():
     rmc.ensure_dependencies_in_path()
 
     if args.gen_c_runnable:
-        rmc.cargo_build(args.crate, args.target_dir, args.build_target,
-                        args.verbose, args.debug, args.mangler, args.dry_run, ["gen-c"], args.restrict_vtable)
+        rmc.cargo_build(args.crate, args.target_dir, args, ["gen-c"])
 
         pattern = os.path.join(args.target_dir, "debug", "deps", "*.symtab.json")
         symbol_table_jsons = glob.glob(pattern)
@@ -51,8 +50,7 @@ def main():
 
         rmc.gen_c_postprocess(c_runnable_filename, args.dry_run)
 
-    rmc.cargo_build(args.crate, args.target_dir, args.build_target,
-                    args.verbose, args.debug, args.mangler, args.dry_run, [], args.restrict_vtable)
+    rmc.cargo_build(args.crate, args.target_dir, args)
 
     if args.build_target:
         pattern = os.path.join(args.target_dir, args.build_target, "debug", "deps", "*.symtab.json")

scripts/rmc

@@ -28,17 +28,7 @@ def main():
         json_runnable_filename = base + "_runnable.json"
         goto_runnable_filename = base + "_runnable.goto"
         c_runnable_filename = base + "_runnable.c"
-        if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(
-                args.input,
-                base,
-                json_runnable_filename,
-                args.verbose,
-                args.debug,
-                args.keep_temps,
-                args.mangler,
-                args.dry_run,
-                ["gen-c"],
-                args.restrict_vtable):
+        if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, base, json_runnable_filename, args, ["gen-c"]):
             return 1
 
         out_files = rmc.symbol_table_to_gotoc([json_runnable_filename], args.verbose, args.keep_temps, args.dry_run)
@@ -63,20 +53,7 @@ def main():
     symbols_filename = base + ".symbols"
 
     restrictions_filename = restrictions_filename if args.restrict_vtable else None
-
-    if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(
-            args.input,
-            base,
-            symbol_table_json_filename,
-            args.verbose,
-            args.debug,
-            args.keep_temps,
-            args.mangler,
-            args.dry_run,
-            args.use_abs,
-            args.abs_type,
-            [],
-            args.restrict_vtable):
+    if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, base, symbol_table_json_filename, args):
         return 1
 
     out_files = rmc.symbol_table_to_gotoc([symbol_table_json_filename], args.verbose, args.keep_temps, args.dry_run)

scripts/rmc.py

@@ -222,46 +222,44 @@ def compile_single_rust_file(
         input_filename,
         base,
         output_filename,
-        verbose=False,
-        debug=False,
-        keep_temps=False,
-        mangler="v0",
-        dry_run=False,
-        use_abs=False,
-        abs_type="std",
-        symbol_table_passes=[],
-        restrict_vtable=False):
-    if not keep_temps:
+
+        extra_args,
+        symbol_table_passes=[]):
+    if not extra_args.keep_temps:
         atexit.register(delete_file, output_filename)
         atexit.register(delete_file, base + ".type_map.json")
 
-    build_cmd = [RMC_RUSTC_EXE] + rustc_flags(mangler, symbol_table_passes, restrict_vtable)
+    build_cmd = [RMC_RUSTC_EXE] + rustc_flags(extra_args.mangler, symbol_table_passes,
+                                              extra_args.restrict_vtable)
 
-    if use_abs:
+    if extra_args.use_abs:
         build_cmd += ["-Z", "force-unstable-if-unmarked=yes",
                       "--cfg=use_abs",
-                      "--cfg", f'abs_type="{abs_type}"']
+                      "--cfg", f'abs_type="{extra_args.abs_type}"']
+
+    if extra_args.tests and "--test" not in build_cmd:
+        build_cmd += ["--test"]
 
     build_cmd += ["-o", base + ".o", input_filename]
 
     build_env = os.environ
-    if debug:
+    if extra_args.debug:
         add_rmc_rustc_debug_to_env(build_env)
 
-    return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug, dry_run=dry_run)
+    return run_cmd(
+        build_cmd,
+        env=build_env,
+        label="compile",
+        verbose=extra_args.verbose,
+        debug=extra_args.debug,
+        dry_run=extra_args.dry_run)
 
 # Generates a symbol table (and some other artifacts) from a rust crate
 def cargo_build(
         crate,
         target_dir,
-        build_target=None,
-        verbose=False,
-        debug=False,
-        mangler="v0",
-        dry_run=False,
-        symbol_table_passes=[],
-        restrict_vtable=False):
-
+        extra_args,
+        symbol_table_passes=[]):
     ensure(os.path.isdir(crate), f"Invalid path to crate: {crate}")
 
     def get_config(option):
@@ -277,23 +275,28 @@ def get_config(option):
                 process.stdout))
         return process.stdout
 
-    rustflags = rustc_flags(mangler, symbol_table_passes, restrict_vtable) + get_config("--rmc-flags").split()
+    rustflags = rustc_flags(extra_args.mangler, symbol_table_passes,
+                            extra_args.restrict_vtable) + get_config("--rmc-flags").split()
     rustc_path = get_config("--rmc-path").strip()
-    build_cmd = ["cargo", "build", "--target-dir", str(target_dir)]
-    if build_target:
-        build_cmd += ["--target", str(build_target)]
+    cargo_cmd = ["cargo", "build"] if not extra_args.tests else ["cargo", "test", "--no-run"]
+    build_cmd = cargo_cmd + ["--target-dir", str(target_dir)]
+    if extra_args.build_target:
+        build_cmd += ["--target", str(extra_args.build_target)]
     build_env = os.environ
     build_env.update({"RUSTFLAGS": " ".join(rustflags),
                       "RUSTC": rustc_path
                       })
-    if debug:
+    if extra_args.debug:
         add_rmc_rustc_debug_to_env(build_env)
-    if verbose:
+    if extra_args.verbose:
         build_cmd.append("-v")
-    if dry_run:
+    if extra_args.dry_run:
         print("{}".format(build_env))
 
-    return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run)
+    if run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=extra_args.verbose, debug=extra_args.debug,
+               dry_run=extra_args.dry_run) != EXIT_CODE_SUCCESS:
+        raise Exception("Failed to run command: {}".format(" ".join(build_cmd)))
+
 
 # Adds information about unwinding to the RMC output
 def append_unwind_tip(text):

scripts/rmc_flags.py

@@ -112,6 +112,8 @@ def add_linking_flags(make_group, add_flag, config):
              help="Link external C files referenced by Rust code")
     add_flag(group, "--function", default="main",
              help="Entry point for verification")
+    add_flag(group, "--tests", default=False, action=BooleanOptionalAction,
+             help="Enable test function verification. Only use this option when the entry point is a test function.")
 
 # Add flags that produce extra artifacts.
 def add_artifact_flags(make_group, add_flag, config):

src/test/rmc/ArithOperators/unsafe_mul_fail.rs

@@ -6,7 +6,7 @@
 // rmc-flags: --function check_mul
 // compile-flags: --crate-type lib
 
-pub fn check_add(a: u8, b: u8) {
+pub fn check_mul(a: u8, b: u8) {
     unsafe {
         a * b;
     }

src/test/rmc/Options/check_tests.rs

@@ -0,0 +1,27 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that we can verify test harnesses using the --tests argument.
+// Note: We need to provide the compile-flags because compile test runs rustc directly and via rmc.
+
+// compile-flags: --test
+// rmc-flags: --tests --function test_harness
+
+pub mod my_mod {
+    pub fn fn_under_verification(a: i32) {
+        assert!(a > 0);
+    }
+}
+
+#[cfg(test)]
+mod test {
+    use my_mod::fn_under_verification;
+
+    #[test]
+    #[no_mangle]
+    fn test_harness() {
+        let input: i32 = rmc::nondet();
+        rmc::assume(input > 1);
+        fn_under_verification(input);
+    }
+}