Handle common CBMC flags via RMC (rust-lang#639)

* Handle common CBMC flags via RMC

* Address some PR comments

* Format

* Improve help messages for CBMC common flags

* Remove `--default-values` and add `--auto-unwind`.

* Add feature to `cargo-rmc`

* Move default values to `rmc_flags`, add them to help message

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 2 people

scripts/cargo-rmc

@@ -219,7 +219,10 @@ def parse_args():
 
         # Add some CBMC flags by default unless `--no-default-checks` is being used
         if args.default_checks:
-            rmc.add_selected_default_cbmc_flags(args)
+            rmc.add_selected_default_cbmc_checks(args)
+
+        # Conditionally add common CBMC flags
+        rmc.process_common_cbmc_flags(args)
 
     # Remove "rmc" from arg if invoked `cargo rmc ...`
     if len(sys.argv) >= 2 and sys.argv[1] == "rmc":

scripts/rmc

@@ -153,7 +153,10 @@ def parse_args():
 
         # Add some CBMC flags by default unless `--no-default-checks` is being used
         if args.default_checks:
-            rmc.add_selected_default_cbmc_flags(args)
+            rmc.add_selected_default_cbmc_checks(args)
+
+        # Conditionally add common CBMC flags
+        rmc.process_common_cbmc_flags(args)
 
     parser = create_parser()
     args = parser.parse_args()

scripts/rmc.py

@@ -9,6 +9,7 @@
 import re
 import pathlib
 
+import rmc_flags
 
 RMC_CFG = "rmc"
 RMC_RUSTC_EXE = "rmc-rustc"
@@ -30,6 +31,7 @@
                    "--unsigned-overflow-check"]
 UNWINDING_CHECKS = ["--unwinding-assertions"]
 
+
 # A Scanner is intended to match a pattern with an output
 # and edit the output based on an edit function
 class Scanner:
@@ -78,15 +80,62 @@ def add_set_cbmc_flags(args, flags):
         else:
             args.cbmc_args.append(arg)
 
-# Add sets of selected default CBMC flags
-def add_selected_default_cbmc_flags(args):
+# Add sets of selected default CBMC checks
+def add_selected_default_cbmc_checks(args):
     if args.memory_safety_checks:
         add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS)
     if args.overflow_checks:
         add_set_cbmc_flags(args, OVERFLOW_CHECKS)
     if args.unwinding_checks:
         add_set_cbmc_flags(args, UNWINDING_CHECKS)
 
+# Add a common CBMC flag to `cbmc_args`
+def add_common_cbmc_flag(args, flag_info):
+    (cbmc_arg, rmc_arg, _) = flag_info
+    rmc_value = getattr(args, rmc_arg)
+    if rmc_value is not None:
+        args.cbmc_args.extend([cbmc_arg, rmc_value])
+
+# Set a common CBMC flag by examining both RMC & CBMC flags
+def set_common_cbmc_flag(args, flag_info):
+    (cbmc_arg, rmc_arg, default_value) = flag_info
+    if getattr(args, rmc_arg) is not None:
+        if cbmc_arg in args.cbmc_args:
+            # Case #1: The flag is specified twice - Result: Raise an exception
+            raise Exception(f"Conflicting flags: `{cbmc_arg}` was specified twice.")
+        # Case #2: Flag specified via `args.rmc_arg` only - Result: Use `args.rmc_arg`
+        return
+    if cbmc_arg in args.cbmc_args:
+        # Case #3: Flag specified via `cbmc_arg` only - Result: Use `cbmc_arg`
+        # Note: `args.rmc_arg` is `None` so nothing will be added later
+        return
+    # Case #4: The flag has not been specified - Result: Assign default value
+    setattr(args, rmc_arg, default_value)
+
+def process_object_bits_flag(args):
+    flag_info = ("--object-bits", "object_bits", rmc_flags.DEFAULT_OBJECT_BITS_VALUE)
+    set_common_cbmc_flag(args, flag_info)
+    add_common_cbmc_flag(args, flag_info)
+
+def process_unwind_flag(args):
+    # We raise an exception if `--auto-unwind` is being used in
+    # addition to other `--unwind` flags in RMC or CBMC
+    if args.auto_unwind:
+        if args.unwind is not None or "--unwind" in args.cbmc_args:
+            raise Exception("Conflicting flags: `--auto-unwind` is not"
+                            " compatible with other `--unwind` flags.")
+        return
+    flag_info = ("--unwind", "unwind", rmc_flags.DEFAULT_UNWIND_VALUE)
+    set_common_cbmc_flag(args, flag_info)
+    add_common_cbmc_flag(args, flag_info)
+
+# Process common CBMC flags
+def process_common_cbmc_flags(args):
+    # For each CBMC flag we set the RMC flag if needed, then
+    # we add the associated CBMC flag if RMC flag has been set
+    process_object_bits_flag(args)
+    process_unwind_flag(args)
+
 # Updates environment to use gotoc backend debugging
 def add_rmc_rustc_debug_to_env(env):
     env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_rmc")

scripts/rmc_flags.py

@@ -5,6 +5,15 @@
 import argparse
 import pathlib as pl
 
+# The default object bits value in CBMC is 8, which is not enough to handle most
+# medium-sized Rust programs. Increasing it to 16 should have no impact in
+# 64-bit architectures.
+DEFAULT_OBJECT_BITS_VALUE = "16"
+# CBMC performs automatic loop unwinding if no unwinding value is specified.
+# Even though this procedure is not guaranteed to terminate, passing a default
+# value for unwinding would prevent users from running automatic loop unwinding.
+DEFAULT_UNWIND_VALUE = None
+
 # Taken from https://github.com/python/cpython/blob/3.9/Lib/argparse.py#L858
 # Cannot use `BooleanOptionalAction` with Python 3.8
 class BooleanOptionalAction(argparse.Action):
@@ -139,6 +148,22 @@ def add_check_flags(make_group, add_flag, config):
     add_flag(group, "--unwinding-checks", default=True, action=BooleanOptionalAction,
              help="Turn on default unwinding checks")
 
+# Add flags for common CBMC flags
+def add_common_flags(make_group, add_flag, config):
+    # Note: The code for handling common CBMC flags is more complex than usual,
+    # since the flag may have been set via `--cbmc-args`. Here, we print the
+    # default values here but we set them later using `process_common_cbmc_flags`
+    default_unwind_value = DEFAULT_UNWIND_VALUE if DEFAULT_UNWIND_VALUE else "None"
+    group = make_group("Common flags", "Common CBMC flags handled by RMC.")
+    add_flag(group, "--object-bits", type=str,
+             help="Specify the number of bits used for representing object IDs in CBMC"
+                  " (default: " + DEFAULT_OBJECT_BITS_VALUE + ")")
+    add_flag(group, "--unwind", type=str,
+             help="Specify the value used for loop unwinding in CBMC"
+                  " (default: " + default_unwind_value + ")")
+    add_flag(group, "--auto-unwind", default=False, action=BooleanOptionalAction,
+             help="Turn on automatic loop unwinding")
+
 # Add flags needed only for visualizer.
 def add_visualizer_flags(make_group, add_flag, config):
     group = make_group(
@@ -207,6 +232,7 @@ def add_flag(group, flag, *args, **kwargs):
         add_linking_flags,
         add_artifact_flags,
         add_check_flags,
+        add_common_flags,
         add_visualizer_flags,
         add_other_flags,
         add_developer_flags

src/test/expected/dry-run-flag-conflict-auto-unwind/expected

@@ -0,0 +1 @@
+Conflicting flags: `--auto-unwind` is not compatible with other `--unwind` flags.

src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs

@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --dry-run --auto-unwind
+// cbmc-flags: --unwind 2
+
+// `--dry-run` causes RMC to print out commands instead of running them
+// In `expected` you will find substrings of these commands because the
+// concrete paths depend on your working directory.
+pub fn main() {}

src/test/expected/dry-run-flag-conflict/expected

@@ -0,0 +1 @@
+Exception: Conflicting flags: `--object-bits` was specified twice.

src/test/expected/dry-run-flag-conflict/main.rs

@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --dry-run --object-bits 10
+// cbmc-flags: --object-bits 8
+
+// `--dry-run` causes RMC to print out commands instead of running them
+// In `expected` you will find substrings of these commands because the
+// concrete paths depend on your working directory.
+pub fn main() {}

src/test/expected/dry-run/expected

@@ -1,4 +1,4 @@
 rmc-rustc -Z symbol-mangling-version=v0 -Z symbol_table_passes=
 symtab2gb
 goto-cc --function main
-cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main
+cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --object-bits 16 --function main

src/tools/compiletest/src/runtest.rs

@@ -2435,8 +2435,9 @@ impl<'test> TestCx<'test> {
     /// Print an error if the verification output does not contain the expected
     /// lines.
     fn verify_output(&self, proc_res: &ProcRes, expected: &str) {
-        if let Some(line) = TestCx::contains_lines(&proc_res.stdout, expected.split('\n').collect())
-        {
+        // Include the output from stderr here for cases where there are exceptions
+        let output = proc_res.stdout.to_string() + &proc_res.stderr;
+        if let Some(line) = TestCx::contains_lines(&output, expected.split('\n').collect()) {
             self.fatal_proc_rec(
                 &format!("test failed: expected output to contain the line: {}", line),
                 &proc_res,