From 0a6b1b40958ebd85ba087a80c7b6228dd29cbd7c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Nov 2021 16:14:30 -0800 Subject: [PATCH 1/2] 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. --- scripts/rmc-rustc | 3 +- scripts/rmc.py | 2 +- src/test/cargo-rmc/simple-main/Cargo.toml | 3 -- src/test/cargo-rmc/simple-main/src/main.rs | 2 +- src/test/expected/one-assert/test.rs | 6 ++- src/test/rmc/ArithOperators/main.rs | 2 +- src/tools/compiletest/src/runtest.rs | 59 +++++++++------------- src/tools/dashboard/src/books.rs | 25 ++++----- 8 files changed, 40 insertions(+), 62 deletions(-) diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index 710403daf9d7..0069fa033f5f 100755 --- a/scripts/rmc-rustc +++ b/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 \ diff --git a/scripts/rmc.py b/scripts/rmc.py index ff0972a18d23..4317dbad6b59 100644 --- a/scripts/rmc.py +++ b/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 diff --git a/src/test/cargo-rmc/simple-main/Cargo.toml b/src/test/cargo-rmc/simple-main/Cargo.toml index 92b6caccff3b..295edc0cb858 100644 --- a/src/test/cargo-rmc/simple-main/Cargo.toml +++ b/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] diff --git a/src/test/cargo-rmc/simple-main/src/main.rs b/src/test/cargo-rmc/simple-main/src/main.rs index 3f1fa2b4f1d1..37592b921f22 100644 --- a/src/test/cargo-rmc/simple-main/src/main.rs +++ b/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); } diff --git a/src/test/expected/one-assert/test.rs b/src/test/expected/one-assert/test.rs index c13a42074392..144392c29dbf 100644 --- a/src/test/expected/one-assert/test.rs +++ b/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); diff --git a/src/test/rmc/ArithOperators/main.rs b/src/test/rmc/ArithOperators/main.rs index 9625cc431a17..ba611f96b44b 100644 --- a/src/test/rmc/ArithOperators/main.rs +++ b/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); diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 40014f2edc6c..6a6f1ac8b0b6 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/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,12 +2371,20 @@ 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") @@ -2403,7 +2392,14 @@ impl<'test> TestCx<'test> { .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", diff --git a/src/tools/dashboard/src/books.rs b/src/tools/dashboard/src/books.rs index c75708a4a038..23a3b1e9536f 100644 --- a/src/tools/dashboard/src/books.rs +++ b/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) 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_or(Edition::Edition2018), + 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(); From b16357e953a8efa6ca6c85b2b30dfd1f0c33d638 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 19 Nov 2021 13:14:03 -0800 Subject: [PATCH 2/2] Update src/tools/dashboard/src/books.rs Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- src/tools/dashboard/src/books.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tools/dashboard/src/books.rs b/src/tools/dashboard/src/books.rs index 23a3b1e9536f..3260b0421d77 100644 --- a/src/tools/dashboard/src/books.rs +++ b/src/tools/dashboard/src/books.rs @@ -296,7 +296,7 @@ fn extract(par_from: &Path, par_to: &Path, config_paths: &mut HashSet) None, false, &Default::default(), - example.config.edition.unwrap_or(Edition::Edition2018), + example.config.edition.unwrap(), None, ) .0;