From 6c50ae8fb5b79a01e5d18bc15fe6e94837336a0d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 3 May 2023 11:53:07 -0700 Subject: [PATCH 1/2] Move `--c-lib` to the new unstable format This will also give visibility to the compiler to whether this feature is enabled or not which is needed to avoid type mismatch issue (https://github.com/model-checking/kani/issues/1781). --- kani-driver/src/args.rs | 17 ++++- tests/cargo-kani/simple-extern/Cargo.toml | 4 +- tests/kani/ForeignItems/fixme_main.rs | 76 --------------------- tests/kani/ForeignItems/fixme_option_ref.rs | 26 +++++++ tests/kani/ForeignItems/main.rs | 4 +- 5 files changed, 47 insertions(+), 80 deletions(-) delete mode 100644 tests/kani/ForeignItems/fixme_main.rs create mode 100644 tests/kani/ForeignItems/fixme_option_ref.rs 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..37c9d6ef12b7 --- /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 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; +} + +#[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); } } From 826273841f02462b4f9903e60ba460def7006e9a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 3 May 2023 14:53:15 -0700 Subject: [PATCH 2/2] Update tests/kani/ForeignItems/fixme_option_ref.rs Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- tests/kani/ForeignItems/fixme_option_ref.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/kani/ForeignItems/fixme_option_ref.rs b/tests/kani/ForeignItems/fixme_option_ref.rs index 37c9d6ef12b7..41b180c71e4d 100644 --- a/tests/kani/ForeignItems/fixme_option_ref.rs +++ b/tests/kani/ForeignItems/fixme_option_ref.rs @@ -6,12 +6,12 @@ //! See for more details. extern "C" { - // In rust, you say nullable pointer by using option of reference. - // Rust guarantees that this has the bitwise represntation - // Some(&x) => &x; - // None => NULL; + // 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; }