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