Support cargo rmc flags (rust-lang#371)

* Support gen-symbols.

* Support allow-cbmc-verification-failure

scripts/cargo-rmc

@@ -13,6 +13,7 @@ import pathlib
 MY_PATH = pathlib.Path(__file__).parent.parent.absolute()
 RMC_C_LIB = MY_PATH / "library" / "rmc" / "rmc_lib.c"
 EXIT_CODE_SUCCESS = 0
+CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
 
 def main():
@@ -26,12 +27,7 @@ def main():
     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",
-    ]
+    exclude_flags = []
     rmc_flags.add_flags(parser, {"default-target": "target"}, exclude_flags=exclude_flags)
     args = parser.parse_args()
 
@@ -59,6 +55,7 @@ def main():
 
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
+    symbols_filename = os.path.join(args.target_dir, "cbmc.symbols")
     if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):
         return 1
 
@@ -71,17 +68,26 @@ def main():
         if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run):
             return 1
 
+    if args.gen_symbols:
+        if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(cbmc_filename, symbols_filename, args.verbose, args.dry_run):
+            return 1
+
     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 = []
-        return rmc.run_visualize(cbmc_filename, args.cbmc_args, cover_args, \
+        retcode = 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:
-        return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run)
+        retcode = rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run)
+
+    if retcode == CBMC_VERIFICATION_FAILURE_EXIT_CODE and args.allow_cbmc_verification_failure:
+        retcode = EXIT_CODE_SUCCESS
+
+    return retcode
 
 
 if __name__ == "__main__":

scripts/rmc

@@ -85,8 +85,10 @@ def main():
                                     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:
         retcode = EXIT_CODE_SUCCESS
+
     return retcode
 
 

scripts/rmc.py

@@ -12,6 +12,7 @@
 RMC_CFG = "rmc"
 RMC_RUSTC_EXE = "rmc-rustc"
 EXIT_CODE_SUCCESS = 0
+CBMC_VERIFICATION_FAILURE_EXIT_CODE = 10
 
 MEMORY_SAFETY_CHECKS = ["--bounds-check",
                         "--pointer-check",