Cleanup RMC Flags

scripts/cargo-rmc

@@ -6,6 +6,7 @@ import argparse
 import glob
 import sys
 import rmc
+import rmc_flags
 import os
 import pathlib
 
@@ -19,42 +20,31 @@ def main():
     if len(sys.argv) >= 2 and sys.argv[1] == "rmc":
         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("--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,
-                        default=[], help="Pass through directly to CBMC")
+    parser = argparse.ArgumentParser(prog="cargo rmc", description="Verify a Rust crate. For more information, see https://github.com/model-checking/rmc.")
+
+    crate_group = parser.add_argument_group("Crate", "You can pass in the rust crate positionally or with the --crate flag.")
+    crate_group.add_argument("crate", help="crate to verify", nargs="?")
+    crate_group.add_argument("--crate", help="crate to verify", dest="crate_flag", metavar="CRATE")
+
+    exclude_flags = [
+        # This should be able to be supported; https://github.com/model-checking/rmc/issues/359
+        "--gen-symbols",
+        # This should be able to be supported; https://github.com/model-checking/rmc/issues/360
+        "--allow-cbmc-verification-failure",
+    ]
+    rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
     args = parser.parse_args()
 
     if args.crate:
-        assert args.crate_flag is None, "Please provide a single crate to verify."
+        rmc.ensure(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."
+        rmc.ensure(args.crate_flag is not None, "Please provide a crate to verify.")
         args.crate = args.crate_flag
 
     if args.quiet:
         args.verbose = False
 
-    if not rmc.dependencies_in_path():
-        return 1
+    rmc.ensure_dependencies_in_path()
 
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
@@ -65,9 +55,8 @@ def main():
 
     pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
-    if len(jsons) != 1:
-        print("ERROR: unexpected number of json outputs")
-        return 1
+    rmc.ensure(len(jsons) == 1, "Unexpected number of json outputs.")
+
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):

scripts/rmc

@@ -6,6 +6,7 @@ import argparse
 import os
 import sys
 import rmc
+import rmc_flags
 import pathlib
 
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
@@ -15,57 +16,40 @@ 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", 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")
-    parser.add_argument("--keep-temps", action="store_true")
-    parser.add_argument("--gen-c", action="store_true")
-    parser.add_argument("--gen-symbols", action="store_true")
-    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,
-                        default=[], help="Pass through directly to CBMC")
+    parser = argparse.ArgumentParser(description="Verify a single Rust file. For more information, see https://github.com/model-checking/rmc.")
+
+    input_group = parser.add_argument_group("Input", "You can pass in the rust file positionally or with the --input flag.")
+    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)
     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."
+        rmc.ensure(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."
+        rmc.ensure(args.input_flag is not None, "Please provide a file to verify.")
         args.input = args.input_flag
 
     if args.quiet:
         args.verbose = False
 
-    if not rmc.dependencies_in_path():
-        return 1
+    rmc.ensure_dependencies_in_path()
 
     # Add some CBMC flags by default unless `--no-default-checks` is being used
     if not args.no_default_checks:
         rmc.add_selected_default_cbmc_flags(args)
 
     base, ext = os.path.splitext(args.input)
-    if ext != ".rs":
-        print("ERROR: Expecting .rs input file")
-        return 1
+    rmc.ensure(ext == ".rs", "Expecting .rs input file.")
+
     json_filename = base + ".json"
     goto_filename = base + ".goto"
     c_filename = base + ".c"

scripts/rmc.py

@@ -5,6 +5,7 @@
 import atexit
 import os
 import os.path
+import sys
 import re
 
 
@@ -43,16 +44,18 @@ def edit_output(self, text):
 def is_exe(name):
     from shutil import which
     return which(name) is not None
-
-
-def dependencies_in_path():
+
+def ensure_dependencies_in_path():
     for program in [RMC_RUSTC_EXE, "symtab2gb", "cbmc", "cbmc-viewer", "goto-instrument", "goto-cc"]:
-        if not is_exe(program):
-            print("ERROR: Could not find {} in PATH".format(program))
-            return False
-    return True
+        ensure(is_exe(program), f"Could not find {program} in PATH")
 
+# Assert a condition holds, or produce a user error message.
+def ensure(condition, message, retcode=1):
+    if not condition:
+        print(f"ERROR: {message}")
+        sys.exit(retcode)
 
+# Deletes a file; used by atexit.register to remove temporary files on exit
 def delete_file(filename):
     try:
         os.remove(filename)

scripts/rmc_flags.py

@@ -0,0 +1,134 @@
+#!/usr/bin/env python3
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+import argparse
+
+# Add flags related to debugging output.
+def add_loudness_flags(make_group, add_flag, config):
+    group = make_group(
+        "Loudness flags", "Determine how much textual output to produce.")
+    add_flag(group, "--debug", action="store_true",
+             help="Produce full debug information")
+    add_flag(group, "--quiet", "-q", action="store_true",
+             help="Produces no output, just an exit code and requested artifacts; overrides --verbose")
+    add_flag(group, "--verbose", "-v", action="store_true",
+             help="Output processing stages and commands, along with minor debug information")
+
+# Add flags which specify configurations for the proof.
+def add_linking_flags(make_group, add_flag, config):
+    group = make_group("Linking flags",
+                       "Provide information about how to link the prover for RMC.")
+    add_flag(group, "--c-lib", nargs="*", default=[], action="extend",
+             help="Link external C files referenced by Rust code")
+    add_flag(group, "--function", default="main",
+             help="Entry point for verification")
+
+# Add flags that produce extra artifacts.
+def add_artifact_flags(make_group, add_flag, config):
+    default_target = config["default-target"]
+    assert default_target is not None, \
+        f"Missing item in parser config: \"default-target\".\n" \
+        "This is a bug; please report this to https://github.com/model-checking/rmc/issues."
+
+    group = make_group(
+        "Artifact flags", "Produce artifacts in addition to a basic RMC report.")
+    add_flag(group, "--gen-c", action="store_true",
+             help="Generate C file equivalent to inputted program")
+    add_flag(group, "--gen-symbols", action="store_true",
+             help="Generate a goto symbol table")
+    add_flag(group, "--keep-temps", action="store_true",
+             help="Keep temporary files generated throughout RMC process")
+    add_flag(group, "--target-dir", default=default_target, metavar="DIR",
+             help=f"Directory for all generated artifacts; defaults to \"{default_target}\"")
+
+# Add flags to turn off default checks.
+def add_check_flags(make_group, add_flag, config):
+    group = make_group("Check flags", "Disable some or all default checks.")
+    add_flag(group, "--no-default-checks", action="store_true",
+             help="Disable all default checks")
+    add_flag(group, "--no-memory-safety-checks", action="store_true",
+             help="Disable default memory safety checks")
+    add_flag(group, "--no-overflow-checks", action="store_true",
+             help="Disable default overflow checks")
+    add_flag(group, "--no-unwinding-checks", action="store_true",
+             help="Disable default unwinding checks")
+
+# Add flags needed only for visualizer.
+def add_visualizer_flags(make_group, add_flag, config):
+    group = make_group(
+        "Visualizer flags", "Generate an HTML-based UI for the generated RMC report.\nSee https://github.com/awslabs/aws-viewer-for-cbmc.")
+    add_flag(group, "--srcdir", default=".",
+             help="The source directory: the root of the source tree")
+    add_flag(group, "--visualize", action="store_true",
+             help="Generate visualizer report to <target-dir>/report/html/index.html")
+    add_flag(group, "--wkdir", default=".",
+             help="""
+                  The working directory: used to determine source locations in output;
+                  this is generally the location from which rmc is currently being invoked
+                  """)
+
+# Add flags for ad-hoc features.
+def add_other_flags(make_group, add_flag, config):
+    group = make_group("Other flags")
+    add_flag(group, "--allow-cbmc-verification-failure", action="store_true",
+             help="Do not produce error return code on CBMC verification failure")
+    add_flag(group, "--dry-run", action="store_true",
+             help="Print commands instead of running them")
+
+# Add flags we don't expect end-users to use.
+def add_developer_flags(make_group, add_flag, config):
+    group = make_group(
+        "Developer flags", "These are generally meant for use by RMC developers, and are not stable.")
+    add_flag(group, "--cbmc-args", nargs=argparse.REMAINDER, default=[],
+             help="Pass through directly to CBMC; must be the last flag")
+    add_flag(group, "--mangler", default="v0", choices=["v0", "legacy"],
+             help="Change what mangler is used by the Rust compiler")
+
+# Adds the flags common to both rmc and cargo-rmc.
+# Allows you to specify flags/groups of flags to not add.
+# This does not return the parser, but mutates the one provided.
+def add_flags(parser, config, exclude_flags=[], exclude_groups=[]):
+    # Keep track of what excluded flags and groups we've seen
+    # so we can warn for possibly incorrect names passed in.
+    excluded_flags = set()
+    excluded_groups = set()
+
+    # Add a group to the parser with title/description, and get a handler for it.
+    def make_group(title=None, description=None):
+        if title in exclude_groups:
+            excluded_groups.add(group.title)
+            return None
+
+        return parser.add_argument_group(title, description)
+
+    # Add the flag to the group, 
+    def add_flag(group, flag, *args, **kwargs):
+        if group == None:
+            return
+
+        if flag in exclude_flags:
+            excluded_flags.add(flag)
+            return
+
+        group.add_argument(flag, *args, **kwargs)
+
+    add_groups = [
+        add_loudness_flags,
+        add_linking_flags,
+        add_artifact_flags,
+        add_check_flags,
+        add_visualizer_flags,
+        add_other_flags,
+        add_developer_flags
+    ]
+
+    for add_group in add_groups:
+        add_group(make_group, add_flag, config)
+
+    # Error if any excluded flags/groups don't exist.
+    extra_flags = set(exclude_flags) - excluded_flags
+    extra_groups = set(exclude_groups) - excluded_groups
+    assert len(extra_flags.union(extra_groups)) == 0, \
+        f"Attempt to exclude parser options which don't exist: {extra_groups.union(extra_flags)}\n" \
+        "This is a bug; please report this to https://github.com/model-checking/rmc/issues."