From beccc4c42111d14f369103bb0f9a6ccb15927968 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 20:42:31 +0200 Subject: [PATCH 1/3] Enable fma* intrinsics (#3002) Implemented in CBMC in https://github.com/diffblue/cbmc/pull/8195. --- docs/src/rust-feature-support/intrinsics.md | 4 +-- .../codegen/intrinsic.rs | 4 +-- tests/kani/Intrinsics/Math/Arith/fma.rs | 26 +++++++++++++++++++ 3 files changed, 30 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/fma.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index f97db5d8ab6c..77392cd37fc6 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 | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 91f7ea20c9b1..8f93a4c61553 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); 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); +} From 4a9255706dfcb336db59d30fbe327f9ed2680396 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 21:30:02 +0200 Subject: [PATCH 2/3] Enable sqrt* intrinsics (#3000) CBMC's sqrt* implementations were fixed in https://github.com/diffblue/cbmc/pull/8195. --- docs/src/rust-feature-support/intrinsics.md | 4 ++-- .../codegen/intrinsic.rs | 4 ++-- tests/kani/Intrinsics/Math/Arith/sqrt.rs | 24 +++++++++++++++++++ 3 files changed, 28 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/sqrt.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 77392cd37fc6..ce3c9fc1b7a2 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -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 8f93a4c61553..c4d5396f1fe8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -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/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); +} From b33708134a19a88f15fd3b6d84a20dc48accac22 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 2 Aug 2024 16:39:02 -0400 Subject: [PATCH 3/3] Update crates documentation with info. on `#[safety_constraint(...)]` attribute for structs (#3405) This PR updates the crates documentation we already had for the `#[safety_constraint(...)]` attribute to account for the changes in #3270. The proposal includes notes/guidelines on where to use the attribute (i.e., the struct or its fields) depending on the type safety condition to be specified. Also, it removes the `rs` annotations on the code blocks that appear in the documentation because they don't seem to have the intended effect (the blocks are not being highlighted at all). The current version of this documentation can be found [here](https://model-checking.github.io/kani/crates/doc/kani/derive.Arbitrary.html) and [here](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html). Related #3095 --- library/kani_macros/src/lib.rs | 113 +++++++++++++++++++++++++++++---- 1 file changed, 99 insertions(+), 14 deletions(-) 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 {