model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.09k stars 84 forks source link

Allow users to annotate functions without body with contracts #3325

Open celinval opened 1 month ago

celinval commented 1 month ago

Requested feature: Allow users to annotate external "C" functions and intrinsics with contracts. Use case: Adding safety contracts to std intrinsics and extern "C" functions. Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

    /// The size of the referenced value in bytes.
    ///
    /// The stabilized version of this intrinsic is [`crate::mem::size_of_val`].
    #[rustc_const_unstable(feature = "const_size_of_val", issue = "46571")]
    #[rustc_nounwind]
    #[requires(matches!(
        <T as Pointee>::Metadata::map_dyn(crate::ptr::metadata(_val)::metadata(), |dyn_meta| {
    ub_checks::can_dereference(dyn_meta)}), None | Some(true)))]
    pub fn size_of_val<T: ?Sized>(_val: *const T) -> usize;

Fails with the following compilation error:

error: expected curly braces
    --> /verify-std/library/core/src/intrinsics.rs:1070:59
     |
1070 |     pub fn size_of_val<T: ?Sized>(_val: *const T) -> usize;
celinval commented 1 month ago

In order to do this, I believe we will need to apply the same logic as stubbing external functions where we replace the method calls instead of replacing the function body.

pnkfelix commented 1 month ago

(this is probably obvious from context, but the test case in the description needs to be wrapped in extern "rust-intrinsic" { ... })