Remove --object-bits option (rust-lang#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

@@ -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.",

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());

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

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() {}

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;