From f8e9b992108c9c9214f69492b92b416be0f765ca Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 26 Apr 2022 14:03:04 -0700
Subject: [PATCH] Remove --object-bits option (#1109)

Delete --object-bits option from Kani. We still set the default to 16 if the user doesn't pick a value via --cbmc-args.
---
 kani-driver/src/args.rs                       | 24 +++++++++----------
 kani-driver/src/call_cbmc.rs                  |  6 +++--
 tests/expected/dry-run-flag-conflict/expected |  2 +-
 tests/expected/dry-run-flag-conflict/main.rs  | 11 +++++----
 .../virtio-balloon-compact/ignore-main.rs     |  2 +-
 5 files changed, 23 insertions(+), 22 deletions(-)

diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index babf6f265fb46..43c9e8fcbd267 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -7,6 +7,9 @@ use std::ffi::OsString;
 use std::path::PathBuf;
 use structopt::StructOpt;
 
+// By default we configure CBMC to use 16 bits to represent the object bits in pointers.
+const DEFAULT_OBJECT_BITS: u32 = 16;
+
 #[derive(Debug, StructOpt)]
 #[structopt(
     name = "kani",
@@ -98,9 +101,6 @@ pub struct KaniArgs {
     #[structopt(long, hidden_short_help(true))]
     pub only_codegen: bool,
 
-    /// Specify the number of bits used for representing object IDs in CBMC
-    #[structopt(long, default_value = "16")]
-    pub object_bits: u32,
     /// Specify the value used for loop unwinding in CBMC
     #[structopt(long)]
     pub default_unwind: Option<u32>,
@@ -163,6 +163,14 @@ impl KaniArgs {
         // Turn them off when visualizing an error trace.
         !self.no_assertion_reach_checks && !self.visualize
     }
+
+    pub fn cbmc_object_bits(&self) -> Option<u32> {
+        if self.cbmc_args.contains(&OsString::from("--object-bits")) {
+            None
+        } else {
+            Some(DEFAULT_OBJECT_BITS)
+        }
+    }
 }
 
 arg_enum! {
@@ -293,16 +301,6 @@ impl KaniArgs {
             .exit();
         }
 
-        let extra_object_bits = self.cbmc_args.contains(&OsString::from("--object-bits"));
-
-        if self.object_bits != 16 && extra_object_bits {
-            Error::with_description(
-                "Conflicting flags: `--object-bits` was specified twice.",
-                ErrorKind::ArgumentConflict,
-            )
-            .exit();
-        }
-
         if self.cbmc_args.contains(&OsString::from("--function")) {
             Error::with_description(
                 "Invalid flag: --function should be provided to Kani directly, not via --cbmc-args.",
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 6025dbc96c45f..73866bfdb8498 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -81,8 +81,10 @@ impl KaniSession {
     ) -> Result<Vec<OsString>> {
         let mut args = self.cbmc_check_flags();
 
-        args.push("--object-bits".into());
-        args.push(self.args.object_bits.to_string().into());
+        if let Some(object_bits) = self.args.cbmc_object_bits() {
+            args.push("--object-bits".into());
+            args.push(object_bits.to_string().into());
+        }
 
         if let Some(unwind_value) = resolve_unwind_value(&self.args, harness_metadata) {
             args.push("--unwind".into());
diff --git a/tests/expected/dry-run-flag-conflict/expected b/tests/expected/dry-run-flag-conflict/expected
index 2d200bbfd2550..9fe2c45e6f3ae 100644
--- a/tests/expected/dry-run-flag-conflict/expected
+++ b/tests/expected/dry-run-flag-conflict/expected
@@ -1 +1 @@
-Conflicting flags: `--object-bits` was specified twice.
+error: Invalid flag: --function should be provided to Kani directly, not via
diff --git a/tests/expected/dry-run-flag-conflict/main.rs b/tests/expected/dry-run-flag-conflict/main.rs
index 5cecdb183c75c..1208bd23a2b03 100644
--- a/tests/expected/dry-run-flag-conflict/main.rs
+++ b/tests/expected/dry-run-flag-conflict/main.rs
@@ -1,11 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --enable-unstable --dry-run --function main
+// cbmc-flags: --function main
 
-// kani-flags: --dry-run --object-bits 10 --enable-unstable --function main
-// cbmc-flags: --object-bits 8
+//! This testcase is to ensure that user cannot pass --function as cbmc-flags
+//! with our driver logic.
 
-// `--dry-run` causes Kani to print out commands instead of running them
-// In `expected` you will find substrings of these commands because the
-// concrete paths depend on your working directory.
+/// This shouldn't run.
 #[kani::proof]
 fn main() {}
diff --git a/tests/firecracker/virtio-balloon-compact/ignore-main.rs b/tests/firecracker/virtio-balloon-compact/ignore-main.rs
index 13dc5bcdb4b04..fab50e7edae2c 100644
--- a/tests/firecracker/virtio-balloon-compact/ignore-main.rs
+++ b/tests/firecracker/virtio-balloon-compact/ignore-main.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// Try with: kani ignore-main.rs -- --default-unwind 3 --unwinding-assertions --pointer-check --object-bits 11
+// Try with: kani ignore-main.rs --default-unwind 3 --enable-unstable --cbmc-args --object-bits 11
 // With kissat as the solver (--external-sat-solver /path/to/kissat) this takes ~5mins
 
 pub const MAX_PAGE_COMPACT_BUFFER: usize = 2048;