Added a goto-instrument --drop-unused-functions step to rmc and cargo-rmc (rust-lang#643)

* Added a goto-instrument --drop-unused-functions step to rmc and cargo-rmc

* Added a test that checks the number of asserts

* Marked test as verify-fail till rust-lang#648 is fixed

Author: zhassan-aws

scripts/cargo-rmc

@@ -83,17 +83,25 @@ def main():
         if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(cbmc_filename, symbols_filename, args.verbose, args.dry_run):
             return 1
 
-    # https://github.com/diffblue/cbmc/issues/6393
-    if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
-            cbmc_filename, cbmc_filename,
-            ['--add-library'],
-            args.verbose, dry_run=args.dry_run):
-        return 1
-    if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
-            cbmc_filename, cbmc_filename,
-            ['--generate-function-body-options', 'assert-false', '--generate-function-body', '.*'],
-            args.verbose, dry_run=args.dry_run):
-        return 1
+    if args.undefined_function_checks:
+        # https://github.com/diffblue/cbmc/issues/6393
+        if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
+                cbmc_filename, cbmc_filename,
+                ['--add-library'],
+                args.verbose, dry_run=args.dry_run):
+            return 1
+        if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
+                cbmc_filename, cbmc_filename,
+                ['--generate-function-body-options', 'assert-false', '--generate-function-body', '.*', '--drop-unused-functions'],
+                args.verbose, dry_run=args.dry_run):
+            return 1
+    else:
+        # Apply --drop-unused-functions if undefined-function-checks was turned off
+        if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
+                cbmc_filename, cbmc_filename,
+                ['--drop-unused-functions'],
+                args.verbose, dry_run=args.dry_run):
+            return 1
 
     if "--function" not in args.cbmc_args:
         args.cbmc_args.extend(["--function", args.function])

scripts/rmc

@@ -101,7 +101,14 @@ def main():
             return 1
         if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
                 goto_filename, goto_filename,
-                ['--generate-function-body-options', 'assert-false', '--generate-function-body', '.*'],
+                ['--generate-function-body-options', 'assert-false', '--generate-function-body', '.*', '--drop-unused-functions'],
+                args.verbose, dry_run=args.dry_run):
+            return 1
+    else:
+        # Apply --drop-unused-functions if undefined-function-checks was turned off
+        if EXIT_CODE_SUCCESS != rmc.run_goto_instrument(
+                goto_filename, goto_filename,
+                ['--drop-unused-functions'],
                 args.verbose, dry_run=args.dry_run):
             return 1
 

src/test/expected/one-assert/expected

@@ -0,0 +1 @@
+** 0 of 1 failed (1 iterations)

src/test/expected/one-assert/test.rs

@@ -0,0 +1,8 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub fn main() {
+    let x: u8 = rmc::nondet();
+    let y = x;
+    assert!(x == y);
+}

src/test/rmc/Never/never_return.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 #![feature(never_type)]