Enable CBMC's slicer

kani-driver/src/call_cbmc.rs

@@ -79,7 +79,10 @@ impl KaniSession {
         file: &Path,
         harness_metadata: &HarnessMetadata,
     ) -> Result<Vec<OsString>> {
-        let mut args = self.cbmc_check_flags();
+        let mut args = Vec::new();
+        if self.args.checks.unwinding_on() {
+            args.push("--unwinding-assertions".into());
+        }
 
         if let Some(object_bits) = self.args.cbmc_object_bits() {
             args.push("--object-bits".into());
@@ -124,10 +127,6 @@ impl KaniSession {
             // args.push("--conversion-check".into());
         }
 
-        if self.args.checks.unwinding_on() {
-            args.push("--unwinding-assertions".into());
-        }
-
         if self.args.extra_pointer_checks {
             // This was adding a lot of false positives with std dangling pointer. We should
             // still catch any invalid dereference with --pointer-check. Thus, only enable them

kani-driver/src/call_goto_instrument.rs

@@ -23,6 +23,11 @@ impl KaniSession {
             self.just_drop_unused_functions(output)?;
         }
 
+        self.add_checks(output)?;
+        // CBMC's slicer errors out if the program is empty:
+        // https://github.com/diffblue/cbmc/issues/6882
+        // so for now, ignore the exit status from the command
+        let _ = self.slice(output);
         self.rewrite_back_edges(output)?;
 
         if self.args.gen_c {
@@ -102,6 +107,26 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    /// Instrument automatic CBMC checks (e.g. bounds and pointer checks)
+    fn add_checks(&self, file: &Path) -> Result<()> {
+        let mut args = self.cbmc_check_flags();
+        args.push(file.to_owned().into_os_string()); // input
+        args.push(file.to_owned().into_os_string()); // output
+
+        self.call_goto_instrument(args)
+    }
+
+    /// Apply CBMC's slicer to prune code that doesn't impact any of the checks
+    fn slice(&self, file: &Path) -> Result<()> {
+        let args: Vec<OsString> = vec![
+            "--reachability-slice".into(),
+            file.to_owned().into_os_string(), // input
+            file.to_owned().into_os_string(), // output
+        ];
+
+        self.call_goto_instrument(args)
+    }
+
     fn rewrite_back_edges(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--ensure-one-backedge-per-target".into(),

tests/expected/dry-run/expected

@@ -3,4 +3,5 @@ symtab2gb
 goto-cc
 --function main
 goto-instrument
-cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16
+goto-instrument --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check
+cbmc --unwinding-assertions --object-bits 16

tests/expected/one-assert/expected

@@ -1 +1 @@
-** 0 of 2 failed
+** 0 of 1 failed

tests/ui/cbmc_checks/signed-overflow/expected

@@ -1,14 +1,8 @@
-Failed Checks: arithmetic overflow on signed addition
-Failed Checks: arithmetic overflow on signed subtraction
-Failed Checks: arithmetic overflow on signed multiplication
 Failed Checks: division by zero
-Failed Checks: arithmetic overflow on signed division
 Failed Checks: division by zero
 Failed Checks: result of signed mod is not representable
 Failed Checks: shift distance is negative
 Failed Checks: shift distance too large
 Failed Checks: shift operand is negative
-Failed Checks: arithmetic overflow on signed shl
 Failed Checks: shift distance is negative
 Failed Checks: shift distance too large
-Failed Checks: arithmetic overflow on signed unary minus