Add support to --function to rmc script (#169) (#523)

This changes the compilation to use crate type lib instead of binary when
we are running rmc on a single .rs file. This allow us to use
any public function as a verification target.

We have also changed the tests to use pub main so it is exported and it
can be used as the entry point of the proof.

Fix cargo-rmc and the current testcase to support library build.

Author: celinval

rmc-docs/src/install-guide.md

@@ -82,7 +82,7 @@ Create a test file:
 
 ```rust
 // File: test.rs
-fn main() {
+pub fn main() {
     assert!(1 == 2);
 }
 ```

scripts/cargo-rmc

@@ -40,15 +40,20 @@ def main():
 
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
             return 1
-        
+
         rmc.gen_c_postprocess(c_runnable_filename, args.dry_run)
 
     rmc.cargo_build(args.crate, args.target_dir,
                     args.verbose, args.debug, args.mangler, args.dry_run, [])
 
     pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
-    rmc.ensure(len(jsons) == 1, f"Unexpected number of json outputs: {len(jsons)}")
+
+    if not args.dry_run:
+        rmc.ensure(len(jsons) == 1, f"Unexpected number of json outputs: {len(jsons)}")
+    else:
+        # Add a dummy value so dry-run works.
+        jsons = ["dry-run.json"]
 
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
@@ -101,15 +106,15 @@ def parse_args():
 
         exclude_flags = []
         rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
-        
+
         return parser
 
     # Determine what crate to analyze from flags
     def get_crate_from_args(args):
         validate(args)
         return args.crate or args.crate_flag or "."
 
-    # Combine the command line parameter to get a config file; 
+    # Combine the command line parameter to get a config file;
     # return None if no_config_toml is set
     def get_config_toml(no_config_toml, config_toml, args):
         crate = get_crate_from_args(args)
@@ -154,7 +159,7 @@ def parse_args():
 
     # Check for conflicting flags
     def validate(args):
-        rmc.ensure(not (args.crate and args.crate_flag), "Please provide a single crate to verify.")   
+        rmc.ensure(not (args.crate and args.crate_flag), "Please provide a single crate to verify.")
         rmc.ensure(not (args.no_config_toml and args.config_toml), "Incompatible flags: --config-toml, --no-config-toml")
 
     # Fix up args before returning
@@ -239,7 +244,7 @@ def extract_flags_from_toml(path):
             success = False
     for flag in flags:
         add_flag(flag, flags[flag])
-    
+
     rmc.ensure(success)
     return flag_list
 

scripts/rmc

@@ -38,7 +38,7 @@ def main():
 
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_runnable_filename, c_runnable_filename, args.verbose, args.dry_run):
             return 1
-        
+
         rmc.gen_c_postprocess(c_runnable_filename, args.dry_run)
 
     json_filename = base + ".json"
@@ -76,7 +76,7 @@ def main():
 
     if "--function" not in args.cbmc_args:
         args.cbmc_args.extend(["--function", args.function])
-    
+
     if args.visualize:
         # Use a separate set of flags for coverage checking (empty for now)
         cover_args = []
@@ -100,14 +100,8 @@ def parse_args():
         input_group.add_argument("input", help="Rust file to verify", nargs="?")
         input_group.add_argument("--input", help="Rust file to verify", dest="input_flag", metavar="INPUT")
 
-        exclude_flags = [
-            # In the future we hope to make this configurable in the command line.
-            # For now, however, changing this from "main" breaks rmc.
-            # Issue: https://github.com/model-checking/rmc/issues/169
-            "--function"
-        ]
-        rmc_flags.add_flags(parser, {"default-target": "."}, exclude_flags=exclude_flags)
-        
+        rmc_flags.add_flags(parser, {"default-target": "."})
+
         return parser
 
     # Check for conflicting flags
@@ -124,11 +118,6 @@ def parse_args():
         if args.quiet:
             args.verbose = False
 
-        # In the future we hope to make this configurable in the command line.
-        # For now, however, changing this from "main" breaks rmc.
-        # Issue: https://github.com/model-checking/rmc/issues/169
-        args.function = "main"
-
         # Add some CBMC flags by default unless `--no-default-checks` is being used
         if args.default_checks:
             rmc.add_selected_default_cbmc_flags(args)

scripts/rmc.py

@@ -48,7 +48,7 @@ def edit_output(self, text):
 def is_exe(name):
     from shutil import which
     return which(name) is not None
-    
+
 def ensure_dependencies_in_path():
     for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "cbmc-viewer", "goto-instrument", "goto-cc"]:
         ensure(is_exe(program), f"Could not find {program} in PATH")
@@ -116,11 +116,11 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve
         process = subprocess.run(
             cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
             env=env, cwd=cwd)
-    
+
     # Print status
     if label != None:
         print_rmc_step_status(label, process, verbose)
-    
+
     stdout = process.stdout
     for scanner in scanners:
         if scanner.match(stdout):
@@ -129,24 +129,26 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve
     # Write to stdout if specified, or if failure, or verbose or debug
     if (output_to == "stdout" or process.returncode != EXIT_CODE_SUCCESS or verbose or debug) and not quiet:
         print(stdout)
-    
+
     # Write to file if given
     if output_to != None and output_to != "stdout":
         with open(output_to, "w") as f:
             f.write(stdout)
-    
+
     return process.returncode
 
 # Generates a symbol table from a rust file
 def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0", dry_run=False, use_abs=False, abs_type="std", symbol_table_passes=[]):
     if not keep_temps:
         atexit.register(delete_file, output_filename)
 
-    build_cmd = [RMC_RUSTC_EXE, 
-            "-Z", "codegen-backend=gotoc", 
+    build_cmd = [RMC_RUSTC_EXE,
+            "-Z", "codegen-backend=gotoc",
             "-Z", "trim-diagnostic-paths=no",
-            "-Z", f"symbol-mangling-version={mangler}", 
+            "-Z", f"symbol-mangling-version={mangler}",
             "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}",
+            "--crate-type=lib",
+            "-Z", "human_readable_cgu_names",
             f"--cfg={RMC_CFG}"]
 
     if use_abs:
@@ -165,20 +167,21 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb
     return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug, dry_run=dry_run)
 
 # Generates a symbol table (and some other artifacts) from a rust crate
-def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0", dry_run=False, symbol_table_passes=[]):
+def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry_run=False, symbol_table_passes=[]):
     ensure(os.path.isdir(crate), f"Invalid path to crate: {crate}")
 
     rustflags = [
         "-Z", "codegen-backend=gotoc",
         "-Z", "trim-diagnostic-paths=no",
         "-Z", f"symbol-mangling-version={mangler}",
-        "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}", 
+        "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}",
+        "-Z", "human_readable_cgu_names",
         f"--cfg={RMC_CFG}"]
     rustflags = " ".join(rustflags)
     if "RUSTFLAGS" in os.environ:
         rustflags = os.environ["RUSTFLAGS"] + " " + rustflags
 
-    build_cmd = ["cargo", "build", "--target-dir", target_dir]
+    build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)]
     build_env = {"RUSTFLAGS": rustflags,
                  "RUSTC": RMC_RUSTC_EXE,
                  "PATH": os.environ["PATH"],
@@ -229,7 +232,7 @@ def run_visualize(cbmc_filename, prop_args, cover_args, verbose=False, quiet=Fal
     # 2) cbmc --xml-ui --cover location ~/rmc/library/rmc/rmc_lib.c <cbmc_filename> > coverage.xml
     # 3) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c <cbmc_filename> > property.xml
     # 4) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto <cbmc_filename> --reportdir report
-    
+
     def run_cbmc_local(cbmc_args, output_to, dry_run=False):
         cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename]
         return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet, dry_run=dry_run)
@@ -266,7 +269,7 @@ def run_goto_instrument(input_filename, output_filename, args, verbose=False, dr
 # Generates a C program from a goto program
 def goto_to_c(goto_filename, c_filename, verbose=False, dry_run=False):
     return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose, dry_run=dry_run)
-    
+
 # Fix remaining issues with output of --gen-c-runnable
 def gen_c_postprocess(c_filename, dry_run=False):
     if not dry_run:

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

@@ -5,6 +5,9 @@ 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
-fn main() {
+pub fn main() {
     assert!(1 == 2);
 }

src/test/cbmc/ArithEqualOperators/main.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 include!("../../rmc-prelude.rs");
 
-fn main() {
+pub fn main() {
     let mut a: u32 = __nondet();
     a /= 2;
     let mut b: u32 = __nondet();

src/test/cbmc/ArithOperators/main.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 include!("../../rmc-prelude.rs");
 
-fn main() {
+pub fn main() {
     let a: u32 = __nondet();
     assert!(a / 2 <= a);
     assert!(a / 2 * 2 >= a / 2);

src/test/cbmc/Asm/main_fixme.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(asm)]
 
-fn main() {
+pub fn main() {
     unsafe {
         asm!("nop");
     }

src/test/cbmc/Assert/UninitValid/fixme_main.rs

@@ -4,7 +4,7 @@
 
 use std::mem::{self, MaybeUninit};
 
-fn main() {
+pub fn main() {
     // The compiler assumes that variables are properly initialized according to
     // the requirements of the variable's type (e.g., a variable of reference
     // type must be aligned and non-NULL). This is an invariant that must always