diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index f97db5d8ab6c..ce3c9fc1b7a2 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -159,8 +159,8 @@ fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) float_to_int_unchecked | No | | floorf32 | Yes | | floorf64 | Yes | | -fmaf32 | No | | -fmaf64 | No | | +fmaf32 | Partial | Results are overapproximated | +fmaf64 | Partial | Results are overapproximated | fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) | forget | Yes | | frem_fast | No | | @@ -211,8 +211,8 @@ sinf32 | Partial | Results are overapproximated; [this test](https://github.com/ sinf64 | Partial | Results are overapproximated; [this test](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs) explains how | size_of | Yes | | size_of_val | Yes | | -sqrtf32 | No | | -sqrtf64 | No | | +sqrtf32 | Partial | Results are overapproximated | +sqrtf64 | Partial | Results are overapproximated | sub_with_overflow | Yes | | transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) | truncf32 | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 91f7ea20c9b1..c4d5396f1fe8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -447,8 +447,8 @@ impl<'tcx> GotocCtx<'tcx> { } "floorf32" => codegen_simple_intrinsic!(Floorf), "floorf64" => codegen_simple_intrinsic!(Floor), - "fmaf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaf)), - "fmaf64" => unstable_codegen!(codegen_simple_intrinsic!(Fma)), + "fmaf32" => codegen_simple_intrinsic!(Fmaf), + "fmaf64" => codegen_simple_intrinsic!(Fma), "fmul_fast" => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(mul); @@ -570,8 +570,8 @@ impl<'tcx> GotocCtx<'tcx> { "simd_xor" => codegen_intrinsic_binop!(bitxor), "size_of" => unreachable!(), "size_of_val" => codegen_size_align!(size), - "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)), - "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)), + "sqrtf32" => codegen_simple_intrinsic!(Sqrtf), + "sqrtf64" => codegen_simple_intrinsic!(Sqrt), "sub_with_overflow" => self.codegen_op_with_overflow( BinaryOperator::OverflowResultMinus, fargs, diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 4e3a8d6f9f5b..6fe0979f08bc 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -103,16 +103,19 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// Allow users to auto generate `Arbitrary` implementations by using /// `#[derive(Arbitrary)]` macro. /// -/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint()]` -/// attribute can be added to its fields to indicate a type safety invariant -/// condition ``. Since `kani::any()` is always expected to produce -/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further -/// constrain the objects generated with `kani::any()`**. +/// ## Type safety specification with the `#[safety_constraint(...)]` attribute +/// +/// When using `#[derive(Arbitrary)]` on a struct, the +/// `#[safety_constraint()]` attribute can be added to either the struct +/// or its fields (but not both) to indicate a type safety invariant condition +/// ``. Since `kani::any()` is always expected to produce type-safe +/// values, **adding `#[safety_constraint(...)]` to the struct or any of its +/// fields will further constrain the objects generated with `kani::any()`**. /// /// For example, the `check_positive` harness in this code is expected to /// pass: /// -/// ```rs +/// ```rust /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -126,11 +129,11 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// } /// ``` /// -/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous +/// But using the `#[safety_constraint(...)]` attribute can lead to vacuous /// results when the values are over-constrained. For example, in this code /// the `check_positive` harness will pass too: /// -/// ```rs +/// ```rust /// #[derive(kani::Arbitrary)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)] @@ -158,6 +161,45 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { /// As usual, we recommend users to defend against these behaviors by using /// `kani::cover!(...)` checks and watching out for unreachable assertions in /// their project's code. +/// +/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields +/// +/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added +/// to either the struct or its fields, but not to both. Adding the +/// `#[safety_constraint(...)]` attribute to both the struct and its fields will +/// result in an error. +/// +/// In practice, only one type of specification is need. If the condition for +/// the type safety invariant involves a relation between two or more struct +/// fields, the struct-level attribute should be used. Otherwise, using the +/// `#[safety_constraint(...)]` on field(s) is recommended since it helps with readability. +/// +/// For example, if we were defining a custom vector `MyVector` and wanted to +/// specify that the inner vector's length is always less than or equal to its +/// capacity, we should do it as follows: +/// +/// ```rust +/// #[derive(Arbitrary)] +/// #[safety_constraint(vector.len() <= *capacity)] +/// struct MyVector { +/// vector: Vec, +/// capacity: usize, +/// } +/// ``` +/// +/// However, if we were defining a struct whose fields are not related in any +/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its +/// fields: +/// +/// ```rust +/// #[derive(Arbitrary)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` #[proc_macro_error] #[proc_macro_derive(Arbitrary, attributes(safety_constraint))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { @@ -167,15 +209,19 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// Allow users to auto generate `Invariant` implementations by using /// `#[derive(Invariant)]` macro. /// -/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint()]` -/// attribute can be added to its fields to indicate a type safety invariant -/// condition ``. This will ensure that the gets additionally checked when -/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro. +/// ## Type safety specification with the `#[safety_constraint(...)]` attribute +/// +/// When using `#[derive(Invariant)]` on a struct, the +/// `#[safety_constraint()]` attribute can be added to either the struct +/// or its fields (but not both) to indicate a type safety invariant condition +/// ``. This will ensure that the type-safety condition gets additionally +/// checked when using the `is_safe()` method automatically generated by the +/// `#[derive(Invariant)]` macro. /// /// For example, the `check_positive` harness in this code is expected to /// fail: /// -/// ```rs +/// ```rust /// #[derive(kani::Invariant)] /// struct AlwaysPositive { /// #[safety_constraint(*inner >= 0)] @@ -200,7 +246,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// For example, for the `AlwaysPositive` struct from above, we will generate /// the following implementation: /// -/// ```rs +/// ```rust /// impl kani::Invariant for AlwaysPositive { /// fn is_safe(&self) -> bool { /// let obj = self; @@ -212,6 +258,45 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// /// Note: the assignments to `obj` and `inner` are made so that we can treat the /// fields as if they were references. +/// +/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields +/// +/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added +/// to either the struct or its fields, but not to both. Adding the +/// `#[safety_constraint(...)]` attribute to both the struct and its fields will +/// result in an error. +/// +/// In practice, only one type of specification is need. If the condition for +/// the type safety invariant involves a relation between two or more struct +/// fields, the struct-level attribute should be used. Otherwise, using the +/// `#[safety_constraint(...)]` is recommended since it helps with readability. +/// +/// For example, if we were defining a custom vector `MyVector` and wanted to +/// specify that the inner vector's length is always less than or equal to its +/// capacity, we should do it as follows: +/// +/// ```rust +/// #[derive(Invariant)] +/// #[safety_constraint(vector.len() <= *capacity)] +/// struct MyVector { +/// vector: Vec, +/// capacity: usize, +/// } +/// ``` +/// +/// However, if we were defining a struct whose fields are not related in any +/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its +/// fields: +/// +/// ```rust +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` #[proc_macro_error] #[proc_macro_derive(Invariant, attributes(safety_constraint))] pub fn derive_invariant(item: TokenStream) -> TokenStream { diff --git a/tests/kani/Intrinsics/Math/Arith/fma.rs b/tests/kani/Intrinsics/Math/Arith/fma.rs new file mode 100644 index 000000000000..379d5aa81db5 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/fma.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_fma_32() { + let m = 10.0_f32; + let x = 4.0_f32; + let b = 60.0_f32; + + // 100.0 + let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs(); + + assert!(abs_difference <= f32::EPSILON); +} + +#[kani::proof] +fn verify_fma_64() { + let m = 10.0_f64; + let x = 4.0_f64; + let b = 60.0_f64; + + // 100.0 + let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs(); + + assert!(abs_difference < 1e-10); +} diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs new file mode 100644 index 000000000000..31afaba8a740 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_sqrt32() { + let positive = 4.0_f32; + let negative_zero = -0.0_f32; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= f32::EPSILON); + assert!(negative_zero.sqrt() == negative_zero); +} + +#[kani::proof] +fn verify_sqrt64() { + let positive = 4.0_f64; + let negative_zero = -0.0_f64; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= 1e-10); + assert!(negative_zero.sqrt() == negative_zero); +}