Merge remote-tracking branch 'origin/main' into merge-queue-fix

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 | |

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,

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(<cond>)]`
-/// attribute can be added to its fields to indicate a type safety invariant
-/// condition `<cond>`. 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(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. 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<T> {
+///     vector: Vec<T>,
+///     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(<cond>)]`
-/// attribute can be added to its fields to indicate a type safety invariant
-/// condition `<cond>`. 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(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. 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<T> {
+///     vector: Vec<T>,
+///     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 {

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);
+}

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);
+}