diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs index 48cf871b7201..eb3773991895 100644 --- a/kani-driver/src/args.rs +++ b/kani-driver/src/args.rs @@ -137,8 +137,8 @@ pub struct KaniArgs { pub harnesses: Vec, /// 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, /// 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(()) } diff --git a/tests/cargo-kani/simple-extern/Cargo.toml b/tests/cargo-kani/simple-extern/Cargo.toml index 00b85ac0973c..406c4b1870ae 100644 --- a/tests/cargo-kani/simple-extern/Cargo.toml +++ b/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 diff --git a/tests/kani/ForeignItems/fixme_main.rs b/tests/kani/ForeignItems/fixme_main.rs deleted file mode 100644 index a6aba093d3e3..000000000000 --- a/tests/kani/ForeignItems/fixme_main.rs +++ /dev/null @@ -1,76 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! To run this test, do -//! kani fixme_main.rs -- lib.c - -// kani-flags: --c-lib lib.c - -// TODO, we should also test packed and transparent representations -// https://doc.rust-lang.org/reference/type-layout.html -#[repr(C)] -pub struct Foo { - i: u32, - c: u8, -} - -// TODO: -//#[repr(packed)] -#[repr(C)] -pub struct Foo2 { - i: u32, - c: u8, - i2: u32, -} - -// https://doc.rust-lang.org/reference/items/external-blocks.html -// https://doc.rust-lang.org/nomicon/ffi.html -extern "C" { - // NOTE: this currently works even if I don't make S static, but is UB. - // We should have a check for that. - static mut S: u32; - - fn update_static(); - fn takes_int(i: u32) -> u32; - fn takes_ptr(p: &u32) -> u32; - // In rust, you say nullable pointer by using option of reference. - // Rust guarantees that this has the bitwise represntation - // 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; - fn mutates_ptr(p: &mut u32); - #[link_name = "name_in_c"] - fn name_in_rust(i: u32) -> u32; - fn takes_struct(f: Foo) -> u32; - fn takes_struct_ptr(f: &Foo) -> u32; - fn takes_struct2(f: Foo2) -> u32; - fn takes_struct_ptr2(f: &Foo2) -> u32; -} - -#[kani::proof] -fn main() { - unsafe { - assert!(S == 12); - update_static(); - assert!(S == 13); - - assert!(takes_int(1) == 3); - assert!(takes_ptr(&5) == 7); - //assert!(takes_ptr_option(Some(&5)) == 4); - //assert!(takes_ptr_option(None) == 0); - let mut p = 17; - mutates_ptr(&mut p); - assert!(p == 16); - - assert!(name_in_rust(2) == 4); - - let f = Foo { i: 12, c: 7 }; - assert!(takes_struct_ptr(&f) == 19); - assert!(takes_struct(f) == 19); - - let f2 = Foo2 { i: 12, c: 7, i2: 8 }; - assert!(takes_struct_ptr2(&f2) == 19); - assert!(takes_struct2(f2) == 19); - } -} diff --git a/tests/kani/ForeignItems/fixme_option_ref.rs b/tests/kani/ForeignItems/fixme_option_ref.rs new file mode 100644 index 000000000000..41b180c71e4d --- /dev/null +++ b/tests/kani/ForeignItems/fixme_option_ref.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 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 + // + 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); + } +} diff --git a/tests/kani/ForeignItems/main.rs b/tests/kani/ForeignItems/main.rs index 98debc0587b0..8c8152642815 100644 --- a/tests/kani/ForeignItems/main.rs +++ b/tests/kani/ForeignItems/main.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); } }