Re-enable RMC to allow users to verify non-public main. (#656)

* Re-enable RMC to allow users to verify non-public main.

Users don't usually set their main function to be public and we should
enable them to verify their main function. For now, users will have to
manually set the create type when running RMC directly. For cargo rmc,
this should be automatically set up by cargo.

* Update src/tools/dashboard/src/books.rs

Co-authored-by: Adrian Palacios <[email protected]>

Co-authored-by: Adrian Palacios <[email protected]>

Author: celinval

scripts/rmc-rustc

@@ -53,8 +53,7 @@ then
     echo ${RMC_PATH}
 else
     set_rmc_lib_path
-    RMC_FLAGS="--crate-type=lib \
-            -Z codegen-backend=gotoc \
+    RMC_FLAGS="-Z codegen-backend=gotoc \
             -Z trim-diagnostic-paths=no \
             -Z human_readable_cgu_names \
             --cfg=rmc \

scripts/rmc.py

@@ -264,7 +264,7 @@ def get_config(option):
 
     rustflags = rustc_flags(mangler, symbol_table_passes) + get_config("--rmc-flags").split()
     rustc_path = get_config("--rmc-path").strip()
-    build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)]
+    build_cmd = ["cargo", "build", "--target-dir", str(target_dir)]
     if build_target:
         build_cmd += ["--target", str(build_target)]
     build_env = os.environ

src/test/cargo-rmc/simple-main/Cargo.toml

@@ -5,9 +5,6 @@ name = "empty-main"
 version = "0.1.0"
 edition = "2018"
 
-[lib]
-path="src/main.rs"
-
 [dependencies]
 
 [workspace]

src/test/cargo-rmc/simple-main/src/main.rs

@@ -1,5 +1,5 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-pub fn main() {
+fn main() {
     assert!(1 == 2);
 }

src/test/expected/one-assert/test.rs

@@ -1,7 +1,9 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
-pub fn main() {
+// rmc-flags: --function check_assert
+// compile-flags: --crate-type lib
+#[no_mangle]
+pub fn check_assert() {
     let x: u8 = rmc::nondet();
     let y = x;
     assert!(x == y);

src/test/rmc/ArithOperators/main.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-pub fn main() {
+fn main() {
     let a: u32 = rmc::nondet();
     assert!(a / 2 <= a);
     assert!(a / 2 * 2 >= a / 2);

src/tools/compiletest/src/runtest.rs

@@ -2273,26 +2273,7 @@ impl<'test> TestCx<'test> {
     /// Runs RMC on the test file specified by `self.testpaths.file`. An error
     /// message is printed to stdout if the verification result is not expected.
     fn verify(&self) {
-        // Other modes call self.compile_test(...). However, we cannot call it here for two reasons:
-        // 1. It calls rustc instead of RMC
-        // 2. It may pass some options that do not make sense for RMC
-        // So we create our own command to execute RMC and pass it to self.compose_and_run_compiler(...) directly.
-        let mut rmc = Command::new("rmc");
-        // We cannot pass rustc flags directly to RMC. Instead, we add them
-        // to the current environment through the `RUSTFLAGS` environment
-        // variable. RMC recognizes the variable and adds those flags to its
-        // internal call to rustc.
-        if !self.props.compile_flags.is_empty() {
-            rmc.env("RUSTFLAGS", self.props.compile_flags.join(" "));
-        }
-        // Pass the test path along with RMC and CBMC flags parsed from comments at the top of the test file.
-        rmc.args(&self.props.rmc_flags)
-            .arg("--input")
-            .arg(&self.testpaths.file)
-            .arg("--cbmc-args")
-            .args(&self.props.cbmc_flags);
-        self.add_rmc_dir_to_path(&mut rmc);
-        let proc_res = self.compose_and_run_compiler(rmc, None);
+        let proc_res = self.run_rmc();
         // If the test file contains expected failures in some locations, ensure
         // that verification does indeed fail in those locations
         if proc_res.stdout.contains("EXPECTED FAIL") {
@@ -2390,20 +2371,35 @@ impl<'test> TestCx<'test> {
         self.verify_output(&proc_res, &expected);
     }
 
-    /// Runs RMC on the test file specified by `self.testpaths.file`. An error
-    /// message is printed to stdout if verification output does not contain
-    /// the expected output in `expected` file.
-    fn run_expected_test(&self) {
-        // We create our own command for the same reasons listed in `run_rmc_test` method.
+    /// Common method used to run RMC on a single file test.
+    fn run_rmc(&self) -> ProcRes {
+        // Other modes call self.compile_test(...). However, we cannot call it here for two reasons:
+        // 1. It calls rustc instead of RMC
+        // 2. It may pass some options that do not make sense for RMC
+        // So we create our own command to execute RMC and pass it to self.compose_and_run_compiler(...) directly.
         let mut rmc = Command::new("rmc");
+        // We cannot pass rustc flags directly to RMC. Instead, we add them
+        // to the current environment through the `RUSTFLAGS` environment
+        // variable. RMC recognizes the variable and adds those flags to its
+        // internal call to rustc.
+        if !self.props.compile_flags.is_empty() {
+            rmc.env("RUSTFLAGS", self.props.compile_flags.join(" "));
+        }
         // Pass the test path along with RMC and CBMC flags parsed from comments at the top of the test file.
         rmc.args(&self.props.rmc_flags)
             .arg("--input")
             .arg(&self.testpaths.file)
             .arg("--cbmc-args")
             .args(&self.props.cbmc_flags);
         self.add_rmc_dir_to_path(&mut rmc);
-        let proc_res = self.compose_and_run_compiler(rmc, None);
+        self.compose_and_run_compiler(rmc, None)
+    }
+
+    /// Runs RMC on the test file specified by `self.testpaths.file`. An error
+    /// message is printed to stdout if verification output does not contain
+    /// the expected output in `expected` file.
+    fn run_expected_test(&self) {
+        let proc_res = self.run_rmc();
         let expected =
             fs::read_to_string(self.testpaths.file.parent().unwrap().join("expected")).unwrap();
         self.verify_output(&proc_res, &expected);
@@ -2414,16 +2410,7 @@ impl<'test> TestCx<'test> {
     /// abstraction. At a later stage, it should be possible to add command-line
     /// arguments to test specific abstractions and modules.
     fn run_stub_test(&self) {
-        let mut rmc = Command::new("rmc");
-        // Arguments to choose specific abstraction are currently provided as
-        // as rmc-flags in the test file
-        rmc.args(&self.props.rmc_flags)
-            .arg("--input")
-            .arg(&self.testpaths.file)
-            .arg("--cbmc-args")
-            .args(&self.props.cbmc_flags);
-        self.add_rmc_dir_to_path(&mut rmc);
-        let proc_res = self.compose_and_run_compiler(rmc, None);
+        let proc_res = self.run_rmc();
         if !proc_res.status.success() {
             self.fatal_proc_rec(
                 "test failed: expected verification success, got failure",

src/tools/dashboard/src/books.rs

@@ -281,11 +281,6 @@ fn prepend_props(path: &Path, example: &mut Example, config_paths: &mut HashSet<
     example.code = format!("{}{}", props, example.code);
 }
 
-/// Make the main function of a test public so it can be verified by rmc.
-fn pub_main(code: String) -> String {
-    code.replace("fn main", "pub fn main")
-}
-
 /// Extracts examples from the markdown file specified by `par_from`,
 /// pre-processes those examples, and saves them in the directory specified by
 /// `par_to`.
@@ -296,17 +291,15 @@ fn extract(par_from: &Path, par_to: &Path, config_paths: &mut HashSet<PathBuf>)
     for mut example in examples.0 {
         apply_diff(par_to, &mut example, config_paths);
         example.config.edition = Some(example.config.edition.unwrap_or(Edition::Edition2021));
-        example.code = pub_main(
-            rustdoc::doctest::make_test(
-                &example.code,
-                None,
-                false,
-                &Default::default(),
-                example.config.edition.unwrap(),
-                None,
-            )
-            .0,
-        );
+        example.code = rustdoc::doctest::make_test(
+            &example.code,
+            None,
+            false,
+            &Default::default(),
+            example.config.edition.unwrap(),
+            None,
+        )
+        .0;
         prepend_props(par_to, &mut example, config_paths);
         let rs_path = par_to.join(format!("{}.rs", example.line));
         fs::create_dir_all(rs_path.parent().unwrap()).unwrap();