The unstable --c-lib option now requires -Z c-ffi to enable C-FFI support (model-checking#2425)

This will also give visibility to the compiler to whether this feature is enabled or not which is needed to avoid type mismatch issue (model-checking#1781).

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

Author: celinval

kani-driver/src/args.rs

@@ -137,8 +137,8 @@ pub struct KaniArgs {
     pub harnesses: Vec<String>,
 
     /// Link external C files referenced by Rust code.
-    /// This is an experimental feature and requires `--enable-unstable` to be used
-    #[arg(long, hide = true, requires("enable_unstable"), num_args(1..))]
+    /// This is an experimental feature and requires `-Z c-ffi` to be used
+    #[arg(long, hide = true, num_args(1..))]
     pub c_lib: Vec<PathBuf>,
     /// Enable test function verification. Only use this option when the entry point is a test function
     #[arg(long)]
@@ -361,6 +361,8 @@ pub enum UnstableFeatures {
     Stubbing,
     /// Generate a C-like file equivalent to input program used for debugging purpose.
     GenC,
+    /// Allow Kani to link against C code.
+    CFfi,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, ValueEnum)]
@@ -593,6 +595,17 @@ impl KaniArgs {
             }
         }
 
+        if !self.c_lib.is_empty() && !self.unstable_features.contains(&UnstableFeatures::CFfi) {
+            if self.enable_unstable {
+                self.print_deprecated("`--enable-unstable`");
+            }
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `--c-lib` argument is unstable and requires `-Z c-ffi` to enable \
+                unstable C-FFI support.",
+            ));
+        }
+
         Ok(())
     }
 

tests/cargo-kani/simple-extern/Cargo.toml

@@ -10,5 +10,7 @@ edition = "2018"
 [workspace]
 
 [kani.flags]
-enable-unstable = true
 c-lib = ["src/helper.c"]
+
+[kani.unstable]
+c-ffi = true

tests/kani/ForeignItems/fixme_main.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z c-ffi --c-lib tests/kani/ForeignItems/lib.c
+//! Check how Kani handles declaration of Nullable reference (Option<&T>).
+//! See <https://github.com/model-checking/kani/issues/2152> for more details.
+
+extern "C" {
+    // In Rust, you say nullable pointer by using option of reference.
+    // Rust guarantees that this has the bitwise representation:
+    //  - Some(&x) => &x;
+    //  - None => NULL;
+    // FIXME: we need to notice when this happens and do a bitcast, or C is unhappy
+    // <https://github.com/model-checking/kani/issues/3>
+    fn takes_ptr_option(p: Option<&u32>) -> u32;
+}
+
+#[kani::proof]
+fn main() {
+    unsafe {
+        // if (ptr) { *ptr - 1 }
+        assert!(takes_ptr_option(Some(&5)) == 4);
+        // if (!ptr) { 0 }
+        assert!(takes_ptr_option(None) == 0);
+    }
+}

tests/kani/ForeignItems/fixme_option_ref.rs

@@ -3,7 +3,7 @@
 //! To run this test, do
 //! kani main.rs -- lib.c
 
-// kani-flags: --enable-unstable --c-lib tests/kani/ForeignItems/lib.c
+// kani-flags: -Z c-ffi --c-lib tests/kani/ForeignItems/lib.c
 
 #[repr(C)]
 pub struct Foo {
@@ -57,7 +57,9 @@ fn main() {
         assert!(takes_struct(f) == 19);
 
         let f2 = Foo2 { i: 12, c: 7, i2: 8 };
+        // f2.i + f2.c
         assert!(takes_struct_ptr2(&f2) == 19);
+        // f2.i + f2.i2
         assert!(takes_struct2(f2) == 20);
     }
 }