C lib flag (rust-lang#260)

* Added --c-lib flag to rmc and cargo-rmc.

* Added rmc test for extern C files.

* Added cargo-rmc example for extern C files.

* PR fixes.

* Fixups after rebase.

* PR fixes.

Author: vecchiot-aws

.github/workflows/copyright.yml

@@ -15,7 +15,7 @@ jobs:
       - name: Get paths for files added
         id: git-diff
         run: |
-          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E '(expected|gitignore)$' | xargs)
+          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E '(expected|ignore|gitignore)$' | xargs)
           echo "::set-output name=paths::$files"
 
       - name: Execute copyright check

scripts/cargo-rmc

@@ -7,8 +7,10 @@ import glob
 import sys
 import rmc
 import os
+import pathlib
 
-
+MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
+RMC_C_LIB = MY_PATH / "library" / "rmc" / "rmc_lib.c"
 EXIT_CODE_SUCCESS = 0
 
 
@@ -18,28 +20,36 @@ def main():
         del sys.argv[1]
 
     parser = argparse.ArgumentParser(description="Verify a Rust crate")
+    parser.add_argument("crate", help="crate to verify", nargs="?")
+    parser.add_argument("--crate", help="crate to verify", dest="crate_flag")
     parser.add_argument("--verbose", "-v", action="store_true")
     parser.add_argument("--quiet", "-q", action="store_true")
     parser.add_argument("--debug", action="store_true")
     parser.add_argument("--keep-temps", action="store_true")
     parser.add_argument("--gen-c", action="store_true")
     parser.add_argument("--mangler", default="v0")
     parser.add_argument("--visualize", action="store_true")
+    parser.add_argument("--c-lib", nargs="*", default=[], action="extend")
     parser.add_argument("--srcdir", default=".")
     parser.add_argument("--target-dir", default="target",
                         help="Directory for all generated artifacts")
     parser.add_argument("--wkdir", default=".")
     parser.add_argument("--function", default="main")
-    parser.add_argument("crate", help="crate to verify")
     parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
     parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
     parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
     parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
     parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
-    parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
+    parser.add_argument("--cbmc-args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
 
+    if args.crate:
+        assert args.crate_flag is None, "Please provide a single crate to verify."
+    else:
+        assert args.crate_flag is not None, "Please provide a crate to verify."
+        args.crate = args.crate_flag
+
     if args.quiet:
         args.verbose = False
 
@@ -63,6 +73,11 @@ def main():
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):
         return 1
 
+    args.c_lib.append(str(RMC_C_LIB))
+
+    if EXIT_CODE_SUCCESS != rmc.link_c_lib(cbmc_filename, cbmc_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
+        return 1
+
     if args.gen_c:
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run):
             return 1
@@ -71,7 +86,9 @@ def main():
         args.cbmc_args.extend(["--function", args.function])
 
     if args.visualize:
-        return rmc.run_visualize(cbmc_filename, args.cbmc_args, \
+        # Use a separate set of flags for coverage checking (empty for now)
+        cover_args = []
+        return rmc.run_visualize(cbmc_filename, args.cbmc_args, cover_args, \
                                  args.verbose, args.quiet, args.keep_temps, \
                                  args.function, args.srcdir, args.wkdir, args.target_dir, args.dry_run)
     else:

scripts/rmc

@@ -7,6 +7,7 @@ import os
 import sys
 import rmc
 import pathlib
+
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
 RMC_C_LIB = MY_PATH / "library" / "rmc" / "rmc_lib.c"
 EXIT_CODE_SUCCESS = 0
@@ -15,7 +16,8 @@ CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
 def main():
     parser = argparse.ArgumentParser(description="Verify a single Rust file")
-    parser.add_argument("input", help="Rust file to verify")
+    parser.add_argument("input", help="Rust file to verify", nargs="?")
+    parser.add_argument("--input", help="Rust file to verify", dest="input_flag")
     parser.add_argument("--verbose", "-v", action="store_true")
     parser.add_argument("--quiet", "-q", action="store_true")
     parser.add_argument("--debug", action="store_true")
@@ -25,21 +27,30 @@ def main():
     parser.add_argument("--allow-cbmc-verification-failure", action="store_true")
     parser.add_argument("--mangler", default="v0")
     parser.add_argument("--visualize", action="store_true")
+    parser.add_argument("--c-lib", nargs="*", default=[], action="extend")
     parser.add_argument("--srcdir", default=".")
+    parser.add_argument("--target-dir", default=".",
+                        help="Directory for all generated artifacts")
     parser.add_argument("--wkdir", default=".")
     parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
     parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
     parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
     parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
     parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
-    parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
+    parser.add_argument("--cbmc-args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
 
     # 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"
+
+    if args.input:
+        assert args.input_flag is None, "Please provide a single file to verify."
+    else:
+        assert args.input_flag is not None, "Please provide a file to verify."
+        args.input = args.input_flag
 
     if args.quiet:
         args.verbose = False
@@ -66,6 +77,11 @@ def main():
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps, args.dry_run):
         return 1
 
+    args.c_lib.append(str(RMC_C_LIB))
+
+    if EXIT_CODE_SUCCESS != rmc.link_c_lib(goto_filename, goto_filename, args.c_lib, args.verbose, args.quiet, args.function, args.dry_run):
+        return 1
+
     if args.gen_c:
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose, args.dry_run):
             return 1
@@ -77,13 +93,12 @@ def main():
     if "--function" not in args.cbmc_args:
         args.cbmc_args.extend(["--function", args.function])
 
-    args.cbmc_args.append(str(RMC_C_LIB))
     if args.visualize:
         # Use a separate set of flags for coverage checking (empty for now)
         cover_args = []
         retcode = rmc.run_visualize(goto_filename, args.cbmc_args, cover_args, \
                                     args.verbose, args.quiet, args.keep_temps, \
-                                    args.function, args.srcdir, args.wkdir, args.dry_run)
+                                    args.function, args.srcdir, args.wkdir, args.target_dir, args.dry_run)
     else:
         retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run)
     if retcode == CBMC_VERIFICATION_FAILURE_EXIT_CODE and args.allow_cbmc_verification_failure:

scripts/rmc.py

@@ -79,9 +79,11 @@ def add_selected_default_cbmc_flags(args):
     if not args.no_unwinding_checks:
         add_set_cbmc_flags(args, UNWINDING_CHECKS)
 
+# Updates environment to use gotoc backend debugging
 def add_rmc_rustc_debug_to_env(env):
     env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_llvm::gotoc")
 
+# Prints info about the RMC process
 def print_rmc_step_status(step_name, completed_process, verbose=False):
     status = "PASS"
     if completed_process.returncode != EXIT_CODE_SUCCESS:
@@ -90,6 +92,7 @@ def print_rmc_step_status(step_name, completed_process, verbose=False):
         print(f"[RMC] stage: {step_name} ({status})")
         print(f"[RMC] cmd: {' '.join(completed_process.args)}")
 
+# Handler for running arbitrary command-line commands
 def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[], dry_run=False):
     # If this a dry run, we emulate running a successful process whose output is the command itself
     # We set `output_to` to `stdout` so that the output is not omitted below
@@ -123,6 +126,7 @@ def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, ve
 
     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):
     if not keep_temps:
         atexit.register(delete_file, output_filename)
@@ -134,7 +138,7 @@ 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):
     rustflags = ["-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", f"--cfg={RMC_CFG}"]
     rustflags = " ".join(rustflags)
@@ -150,17 +154,25 @@ def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler=
         add_rmc_rustc_debug_to_env(build_env)
     return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run)
 
+# Adds information about unwinding to the RMC output
 def append_unwind_tip(text):
     unwind_tip = ("[RMC] info: Verification output shows one or more unwinding failures.\n"
                   "[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n")
     return text + unwind_tip
 
+# Generates a goto program from a symbol table
 def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False, dry_run=False):
     if not keep_temps:
         atexit.register(delete_file, cbmc_filename)
     cmd = ["symtab2gb", json_filename, "--out", cbmc_filename]
     return run_cmd(cmd, label="to-gotoc", verbose=verbose, dry_run=dry_run)
 
+# Links in external C programs into a goto program
+def link_c_lib(src, dst, c_lib, verbose=False, quiet=False, function="main", dry_run=False):
+    cmd = ["goto-cc"] + ["--function", function] + [src] + c_lib + ["-o", dst]
+    return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run)
+
+# Runs CBMC on a goto program
 def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False):
     cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename]
     scanners = []
@@ -171,25 +183,22 @@ def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False
         scanners.append(unwind_asserts_scanner)
     return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners, dry_run=dry_run)
 
+# Generates a viewer report from a goto program
 def run_visualize(cbmc_filename, prop_args, cover_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir=".", dry_run=False):
     results_filename = os.path.join(outdir, "results.xml")
     coverage_filename = os.path.join(outdir, "coverage.xml")
     property_filename = os.path.join(outdir, "property.xml")
-    temp_goto_filename = os.path.join(outdir, "temp.goto")
     if not keep_temps:
-        for filename in [results_filename, coverage_filename, property_filename, temp_goto_filename]:
+        for filename in [results_filename, coverage_filename, property_filename]:
             atexit.register(delete_file, filename)
 
-    # 1) goto-cc --function main <cbmc_filename> -o temp.goto
-    # 2) cbmc --xml-ui --trace ~/rmc/library/rmc/rmc_lib.c temp.goto > results.xml
-    # 3) cbmc --xml-ui --cover location ~/rmc/library/rmc/rmc_lib.c temp.goto > coverage.xml
-    # 4) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c temp.goto > property.xml
-    # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto --reportdir report
-
-    run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function, dry_run=dry_run)
+    # 1) cbmc --xml-ui --trace ~/rmc/library/rmc/rmc_lib.c <cbmc_filename> > results.xml
+    # 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 + [temp_goto_filename]
+        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)
 
     cbmc_prop_args = prop_args + ["--xml-ui"]
@@ -199,15 +208,12 @@ def run_cbmc_local(cbmc_args, output_to, dry_run=False):
     run_cbmc_local(cbmc_cover_args + ["--cover", "location"], coverage_filename, dry_run=dry_run)
     run_cbmc_local(cbmc_prop_args + ["--show-properties"], property_filename, dry_run=dry_run)
 
-    run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename,
+    run_cbmc_viewer(cbmc_filename, results_filename, coverage_filename,
                     property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"), dry_run=dry_run)
 
     return retcode
 
-def run_goto_cc(src, dst, verbose=False, quiet=False, function="main", dry_run=False):
-    cmd = ["goto-cc"] + ["--function", function] + [src] + ["-o", dst]
-    return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run)
-
+# Handler for calling cbmc-viewer
 def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report", dry_run=False):
     cmd = ["cbmc-viewer"] + \
           ["--result", results_filename] + \
@@ -219,15 +225,15 @@ def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property
           ["--reportdir", reportdir]
     return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet, dry_run=dry_run)
 
-
+# Handler for calling goto-instrument
 def run_goto_instrument(input_filename, output_filename, args, verbose=False, dry_run=False):
     cmd = ["goto-instrument"] + args + [input_filename]
     return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename, dry_run=dry_run)
 
-
+# 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)
 
-
+# Generates the CMBC symbol table from a goto program
 def goto_to_symbols(goto_filename, symbols_filename, verbose=False, dry_run=False):
     return run_goto_instrument(goto_filename, symbols_filename, ["--show-symbol-table"], verbose, dry_run=dry_run)

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

@@ -0,0 +1,10 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "simple-lib"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]

src/test/cargo-rmc/simple-extern/src/externs.rs

@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+extern "C" {
+    pub fn external_c_assertion(i: u32) -> u32;
+}
+
+#[no_mangle]
+pub extern "C" fn rust_add1(i: u32) -> u32 {
+    i + 1
+}

src/test/cargo-rmc/simple-extern/src/helper.c

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#include <stdint.h>
+#include <assert.h>
+#include <string.h>
+#include <stdio.h>
+#include <stdarg.h>
+
+uint32_t rust_add1(uint32_t i);
+
+uint32_t external_c_assertion(uint32_t x) {
+    assert(rust_add1(x) == x + 1);
+    return 0;
+}

src/test/cargo-rmc/simple-extern/src/lib.rs

@@ -0,0 +1,34 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub mod externs;
+pub use externs::external_c_assertion;
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn it_works() {
+        unsafe {
+            external_c_assertion(12);
+        }
+    }
+}
+
+#[cfg(rmc)]
+mod rmc_tests {
+    use super::*;
+
+    fn __nondet<T>() -> T {
+        unimplemented!()
+    }
+    #[allow(dead_code)]
+    #[no_mangle]
+    fn test_sum() {
+        let a: u32 = __nondet();
+
+        if a < 100 {
+            unsafe {
+                external_c_assertion(a);
+            }
+        }
+    }
+}

src/test/cargo-rmc/simple-extern/test_sum.ignore

@@ -0,0 +1 @@
+[call_into_rust.assertion.1] line 13 assertion takes_int(x) == x + 1: SUCCESS

src/test/cbmc/ForeignItems/fixme_main.rs

@@ -3,6 +3,8 @@
 //! To run this test, do
 //! rmc fixme_main.rs -- lib.c
 
+// rmc-flags: --c-lib lib.c
+
 // TODO, we should also test packed and transparent representations
 // https://doc.rust-lang.org/reference/type-layout.html
 #[repr(C)]

src/test/cbmc/ForeignItems/lib.c

@@ -84,7 +84,7 @@ uint32_t takes_struct_ptr(struct Foo* f) {
 
 uint32_t takes_struct2(struct Foo2 f) {
     assert(sizeof(unsigned int) == sizeof(uint32_t));
-    return f.i + f.c;
+    return f.i + f.i2;
 }
 
 uint32_t takes_struct_ptr2(struct Foo2* f) {