diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc index 5ac6d9de75d9..b1444a823fbd 100755 --- a/scripts/cargo-rmc +++ b/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): diff --git a/scripts/rmc b/scripts/rmc index dd9f9d83981f..6f0d14c840d8 100755 --- a/scripts/rmc +++ b/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" diff --git a/scripts/rmc.py b/scripts/rmc.py index 4bd3e8349d89..e2fdee7b2ca1 100644 --- a/scripts/rmc.py +++ b/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) diff --git a/scripts/rmc_flags.py b/scripts/rmc_flags.py new file mode 100644 index 000000000000..2a3ef783c23e --- /dev/null +++ b/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 /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."