From f6af818250744089875f875e0f7b3a52c06bf986 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 13:50:03 +0000 Subject: [PATCH 01/14] Enable powf*, exp*, sqrt* intrinsics CBMC provides approximating implementations of these. Resolves: #2763, #2966 --- docs/src/rust-feature-support/intrinsics.md | 24 ++++++++--------- .../codegen/intrinsic.rs | 24 ++++++++--------- tests/kani/Intrinsics/Math/powf64.rs | 26 +++++++++++++++++++ 3 files changed, 50 insertions(+), 24 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/powf64.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 0705d3b00f1b..f83c519147e8 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -148,10 +148,10 @@ cttz_nonzero | Yes | | discriminant_value | Yes | | drop_in_place | No | | exact_div | Yes | | -exp2f32 | No | | -exp2f64 | No | | -expf32 | No | | -expf64 | No | | +exp2f32 | Partial | Results are overapproximated | +exp2f64 | Partial | Results are overapproximated | +expf32 | Partial | Results are overapproximated | +expf64 | Partial | Results are overapproximated | fabsf32 | Yes | | fabsf64 | Yes | | fadd_fast | Yes | | @@ -170,8 +170,8 @@ log10f32 | No | | log10f64 | No | | log2f32 | No | | log2f64 | No | | -logf32 | No | | -logf64 | No | | +logf32 | Partial | Results are overapproximated | +logf64 | Partial | Results are overapproximated | maxnumf32 | Yes | | maxnumf64 | Yes | | min_align_of | Yes | | @@ -185,10 +185,10 @@ nearbyintf64 | Yes | | needs_drop | Yes | | nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | -powf32 | No | | -powf64 | No | | -powif32 | No | | -powif64 | No | | +powf32 | Partial | Results are overapproximated | +powf64 | Partial | Results are overapproximated | +powif32 | Partial | Results are overapproximated | +powif64 | Partial | Results are overapproximated | pref_align_of | Yes | | prefetch_read_data | No | | prefetch_read_instruction | 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 3412cba290d2..edc76edc2f39 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -420,10 +420,10 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place_stable(place, e) } "exact_div" => self.codegen_exact_div(fargs, place, loc), - "exp2f32" => unstable_codegen!(codegen_simple_intrinsic!(Exp2f)), - "exp2f64" => unstable_codegen!(codegen_simple_intrinsic!(Exp2)), - "expf32" => unstable_codegen!(codegen_simple_intrinsic!(Expf)), - "expf64" => unstable_codegen!(codegen_simple_intrinsic!(Exp)), + "exp2f32" => codegen_simple_intrinsic!(Exp2f), + "exp2f64" => codegen_simple_intrinsic!(Exp2), + "expf32" => codegen_simple_intrinsic!(Expf), + "expf64" => codegen_simple_intrinsic!(Exp), "fabsf32" => codegen_simple_intrinsic!(Fabsf), "fabsf64" => codegen_simple_intrinsic!(Fabs), "fadd_fast" => { @@ -456,8 +456,8 @@ impl<'tcx> GotocCtx<'tcx> { "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)), "log2f32" => unstable_codegen!(codegen_simple_intrinsic!(Log2f)), "log2f64" => unstable_codegen!(codegen_simple_intrinsic!(Log2)), - "logf32" => unstable_codegen!(codegen_simple_intrinsic!(Logf)), - "logf64" => unstable_codegen!(codegen_simple_intrinsic!(Log)), + "logf32" => codegen_simple_intrinsic!(Logf), + "logf64" => codegen_simple_intrinsic!(Log), "maxnumf32" => codegen_simple_intrinsic!(Fmaxf), "maxnumf64" => codegen_simple_intrinsic!(Fmax), "min_align_of" => codegen_intrinsic_const!(), @@ -474,10 +474,10 @@ impl<'tcx> GotocCtx<'tcx> { "offset" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" ), - "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)), - "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)), - "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), - "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), + "powf32" => codegen_simple_intrinsic!(Powf), + "powf64" => codegen_simple_intrinsic!(Pow), + "powif32" => codegen_simple_intrinsic!(Powif), + "powif64" => codegen_simple_intrinsic!(Powi), "pref_align_of" => codegen_intrinsic_const!(), "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), @@ -555,8 +555,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/powf64.rs b/tests/kani/Intrinsics/Math/powf64.rs new file mode 100644 index 000000000000..82b8fde8e49c --- /dev/null +++ b/tests/kani/Intrinsics/Math/powf64.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub fn f(a: u64) -> u64 { + const C: f64 = 0.618; + (a as f64).powf(C) as u64 +} + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + fn verify_f() { + const LIMIT: u64 = 10; + let x: u64 = kani::any(); + let y: u64 = kani::any(); + // outside these limits our approximation may yield spurious results + kani::assume(x > LIMIT && x < LIMIT * 3); + kani::assume(y > LIMIT && y < LIMIT * 3); + kani::assume(x > y); + let x_ = f(x); + let y_ = f(y); + assert!(x_ >= y_); + } +} From 0f75d2d21ac1899c4bd0b09a4d47f9bdc33a7c29 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:17:32 +0000 Subject: [PATCH 02/14] Test for powf32 --- tests/kani/Intrinsics/Math/Arith/powf32.rs | 10 ++++++++++ tests/kani/Intrinsics/Math/{ => Arith}/powf64.rs | 0 2 files changed, 10 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/powf32.rs rename tests/kani/Intrinsics/Math/{ => Arith}/powf64.rs (100%) diff --git a/tests/kani/Intrinsics/Math/Arith/powf32.rs b/tests/kani/Intrinsics/Math/Arith/powf32.rs new file mode 100644 index 000000000000..4181b39db165 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powf32.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_pow() { + let x: f32 = kani::any(); + kani::assume(x.is_normal()); + let x2 = x.powf(2.0); + assert!(x2 >= 0); +} diff --git a/tests/kani/Intrinsics/Math/powf64.rs b/tests/kani/Intrinsics/Math/Arith/powf64.rs similarity index 100% rename from tests/kani/Intrinsics/Math/powf64.rs rename to tests/kani/Intrinsics/Math/Arith/powf64.rs From 890dca594b51fdae060b733c661b8c94731118a5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:34:47 +0000 Subject: [PATCH 03/14] Test exp --- tests/kani/Intrinsics/Math/Arith/exp.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/exp.rs diff --git a/tests/kani/Intrinsics/Math/Arith/exp.rs b/tests/kani/Intrinsics/Math/Arith/exp.rs new file mode 100644 index 000000000000..1c43d1d9ca83 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/exp.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_exp32() { + let two = 2.0_f32; + let two_sq = std::f32::consts::E * std::f32::consts::E; + let two_exp = two.exp(); + + assert!((two_sq - two_exp).abs() <= 1.0); +} + +#[kani::proof] +fn verify_exp64() { + let two = 2.0_f64; + let two_sq = std::f64::consts::E * std::f64::consts::E; + let two_exp = two.exp(); + + assert!((two_sq - two_exp).abs() <= 1.0); +} From fc560594484e42b8b99ebea040f74ecf0da3d7c3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:35:14 +0000 Subject: [PATCH 04/14] Test sqrt --- tests/kani/Intrinsics/Math/Arith/sqrt.rs | 28 ++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/sqrt.rs diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs new file mode 100644 index 000000000000..d9003ae8d066 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_sqrt32() { + let positive = 4.0_f32; + let negative = -4.0_f32; + let negative_zero = -0.0_f32; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= f32::EPSILON); + assert!(negative.sqrt().is_nan()); + assert!(negative_zero.sqrt() == negative_zero); +} + +#[kani::proof] +fn verify_sqrt64() { + let positive = 4.0_f64; + let negative = -4.0_f64; + let negative_zero = -0.0_f64; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= 1e-10); + assert!(negative.sqrt().is_nan()); + assert!(negative_zero.sqrt() == negative_zero); +} From 02de4326d8db5374236015fe7de4dcd1d2b073eb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:36:55 +0000 Subject: [PATCH 05/14] Test exp2 --- tests/kani/Intrinsics/Math/Arith/exp2.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/exp2.rs diff --git a/tests/kani/Intrinsics/Math/Arith/exp2.rs b/tests/kani/Intrinsics/Math/Arith/exp2.rs new file mode 100644 index 000000000000..ff1a4386b32e --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/exp2.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_exp2_32() { + let two = 2.0_f32; + let two_two = two.exp2(); + + assert!((two_two - 4.0).abs() <= 1.0); +} + +#[kani::proof] +fn verify_exp2_64() { + let two = 2.0_f64; + let two_two = two.exp2(); + + assert!((two_two - 4.0).abs() <= 1.0); +} From 2a286fc1c576c6d92926a0a5e331cc836e1f7201 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:39:21 +0000 Subject: [PATCH 06/14] Test powi --- tests/kani/Intrinsics/Math/Arith/powi.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/powi.rs diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs new file mode 100644 index 000000000000..adf53c4d5eb8 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_powi32() { + let x: f32 = kani::any(); + kani::assume(x.is_normal()); + let x2 = x.powi(2); + assert!(x2 >= 0); +} + +#[kani::proof] +fn verify_powi64() { + let x: f64 = kani::any(); + kani::assume(x.is_normal()); + let x2 = x.powi(2); + assert!(x2 >= 0); +} From a044577d2d017b358e126b7aa96cb43da5750da4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Feb 2024 21:42:04 +0000 Subject: [PATCH 07/14] Syntax fixes --- tests/kani/Intrinsics/Math/Arith/powf32.rs | 2 +- tests/kani/Intrinsics/Math/Arith/powi.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/kani/Intrinsics/Math/Arith/powf32.rs b/tests/kani/Intrinsics/Math/Arith/powf32.rs index 4181b39db165..d8c6ebea6a3e 100644 --- a/tests/kani/Intrinsics/Math/Arith/powf32.rs +++ b/tests/kani/Intrinsics/Math/Arith/powf32.rs @@ -6,5 +6,5 @@ fn verify_pow() { let x: f32 = kani::any(); kani::assume(x.is_normal()); let x2 = x.powf(2.0); - assert!(x2 >= 0); + assert!(x2 >= 0.0); } diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs index adf53c4d5eb8..70d9d8b0d46b 100644 --- a/tests/kani/Intrinsics/Math/Arith/powi.rs +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -6,7 +6,7 @@ fn verify_powi32() { let x: f32 = kani::any(); kani::assume(x.is_normal()); let x2 = x.powi(2); - assert!(x2 >= 0); + assert!(x2 >= 0.0); } #[kani::proof] @@ -14,5 +14,5 @@ fn verify_powi64() { let x: f64 = kani::any(); kani::assume(x.is_normal()); let x2 = x.powi(2); - assert!(x2 >= 0); + assert!(x2 >= 0.0); } From d5ae17ddc1f6af650cef336299a057b86487bc93 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 09:54:09 +0000 Subject: [PATCH 08/14] Don't do powi just yet --- tests/kani/Intrinsics/Math/Arith/powi.rs | 18 ------------------ 1 file changed, 18 deletions(-) delete mode 100644 tests/kani/Intrinsics/Math/Arith/powi.rs diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs deleted file mode 100644 index 70d9d8b0d46b..000000000000 --- a/tests/kani/Intrinsics/Math/Arith/powi.rs +++ /dev/null @@ -1,18 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[kani::proof] -fn verify_powi32() { - let x: f32 = kani::any(); - kani::assume(x.is_normal()); - let x2 = x.powi(2); - assert!(x2 >= 0.0); -} - -#[kani::proof] -fn verify_powi64() { - let x: f64 = kani::any(); - kani::assume(x.is_normal()); - let x2 = x.powi(2); - assert!(x2 >= 0.0); -} From b60abc63f8240cf21abdfef5eda480384734daab Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 09:57:05 +0000 Subject: [PATCH 09/14] Log test --- tests/kani/Intrinsics/Math/Arith/log.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/kani/Intrinsics/Math/Arith/log.rs diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs new file mode 100644 index 000000000000..a51b66967f90 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_logf32() { + let e = std::f32::consts::E; + let e_log = two.log(); + + assert!((e_log - 1.0).abs() <= 0.1); +} + +#[kani::proof] +fn verify_logf64() { + let e = std::f64::consts::E; + let e_log = two.log(); + + assert!((e_log - 1.0).abs() <= 0.1); +} From e0de5b583f1fa0c46734778d312f08a9e49a9650 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:01:37 +0000 Subject: [PATCH 10/14] Fixup --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 4 ++-- tests/kani/Intrinsics/Math/Arith/log.rs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index edc76edc2f39..dd6c37aef7f0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -476,8 +476,8 @@ impl<'tcx> GotocCtx<'tcx> { ), "powf32" => codegen_simple_intrinsic!(Powf), "powf64" => codegen_simple_intrinsic!(Pow), - "powif32" => codegen_simple_intrinsic!(Powif), - "powif64" => codegen_simple_intrinsic!(Powi), + "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), + "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), "pref_align_of" => codegen_intrinsic_const!(), "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs index a51b66967f90..deab02b6a713 100644 --- a/tests/kani/Intrinsics/Math/Arith/log.rs +++ b/tests/kani/Intrinsics/Math/Arith/log.rs @@ -4,7 +4,7 @@ #[kani::proof] fn verify_logf32() { let e = std::f32::consts::E; - let e_log = two.log(); + let e_log = e.ln(); assert!((e_log - 1.0).abs() <= 0.1); } @@ -12,7 +12,7 @@ fn verify_logf32() { #[kani::proof] fn verify_logf64() { let e = std::f64::consts::E; - let e_log = two.log(); + let e_log = e.ln(); assert!((e_log - 1.0).abs() <= 0.1); } From 9fed6e52ca181b5194806f5c1e7eecff79912f1c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:11:10 +0000 Subject: [PATCH 11/14] Fix powf32 --- tests/kani/Intrinsics/Math/Arith/powf32.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/kani/Intrinsics/Math/Arith/powf32.rs b/tests/kani/Intrinsics/Math/Arith/powf32.rs index d8c6ebea6a3e..d67c0025c033 100644 --- a/tests/kani/Intrinsics/Math/Arith/powf32.rs +++ b/tests/kani/Intrinsics/Math/Arith/powf32.rs @@ -5,6 +5,7 @@ fn verify_pow() { let x: f32 = kani::any(); kani::assume(x.is_normal()); + kani::assume(x > 1.0 && x < u16::MAX.into()); let x2 = x.powf(2.0); assert!(x2 >= 0.0); } From fa2ac24d5f32c00d30e01f20d439340d0e85c11d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:17:43 +0000 Subject: [PATCH 12/14] No sqrt just yet --- docs/src/rust-feature-support/intrinsics.md | 8 +++--- .../codegen/intrinsic.rs | 4 +-- tests/kani/Intrinsics/Math/Arith/sqrt.rs | 28 ------------------- 3 files changed, 6 insertions(+), 34 deletions(-) delete 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 f83c519147e8..7df1a093943f 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -187,8 +187,8 @@ nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | powf32 | Partial | Results are overapproximated | powf64 | Partial | Results are overapproximated | -powif32 | Partial | Results are overapproximated | -powif64 | Partial | Results are overapproximated | +powif32 | No | | +powif64 | No | | pref_align_of | Yes | | prefetch_read_data | No | | prefetch_read_instruction | 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 | Partial | Results are overapproximated | -sqrtf64 | Partial | Results are overapproximated | +sqrtf32 | No | | +sqrtf64 | No | | 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 dd6c37aef7f0..0709682afa65 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -555,8 +555,8 @@ impl<'tcx> GotocCtx<'tcx> { "simd_xor" => codegen_intrinsic_binop!(bitxor), "size_of" => unreachable!(), "size_of_val" => codegen_size_align!(size), - "sqrtf32" => codegen_simple_intrinsic!(Sqrtf), - "sqrtf64" => codegen_simple_intrinsic!(Sqrt), + "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)), + "sqrtf64" => unstable_codegen!(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 deleted file mode 100644 index d9003ae8d066..000000000000 --- a/tests/kani/Intrinsics/Math/Arith/sqrt.rs +++ /dev/null @@ -1,28 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -#[kani::proof] -fn verify_sqrt32() { - let positive = 4.0_f32; - let negative = -4.0_f32; - let negative_zero = -0.0_f32; - - let abs_difference = (positive.sqrt() - 2.0).abs(); - - assert!(abs_difference <= f32::EPSILON); - assert!(negative.sqrt().is_nan()); - assert!(negative_zero.sqrt() == negative_zero); -} - -#[kani::proof] -fn verify_sqrt64() { - let positive = 4.0_f64; - let negative = -4.0_f64; - let negative_zero = -0.0_f64; - - let abs_difference = (positive.sqrt() - 2.0).abs(); - - assert!(abs_difference <= 1e-10); - assert!(negative.sqrt().is_nan()); - assert!(negative_zero.sqrt() == negative_zero); -} From 22d33e3d2c0a9115e0f4227d68d8fcff8cc42615 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 18:14:56 +0000 Subject: [PATCH 13/14] Comments --- tests/kani/Intrinsics/Math/Arith/exp.rs | 4 ++++ tests/kani/Intrinsics/Math/Arith/exp2.rs | 4 ++++ tests/kani/Intrinsics/Math/Arith/log.rs | 4 ++++ tests/kani/Intrinsics/Math/Arith/powf32.rs | 4 ++++ tests/kani/Intrinsics/Math/Arith/powf64.rs | 4 ++++ 5 files changed, 20 insertions(+) diff --git a/tests/kani/Intrinsics/Math/Arith/exp.rs b/tests/kani/Intrinsics/Math/Arith/exp.rs index 1c43d1d9ca83..6f07f3b32dbe 100644 --- a/tests/kani/Intrinsics/Math/Arith/exp.rs +++ b/tests/kani/Intrinsics/Math/Arith/exp.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `expf32` and `expf64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. #[kani::proof] fn verify_exp32() { diff --git a/tests/kani/Intrinsics/Math/Arith/exp2.rs b/tests/kani/Intrinsics/Math/Arith/exp2.rs index ff1a4386b32e..b8e458171da7 100644 --- a/tests/kani/Intrinsics/Math/Arith/exp2.rs +++ b/tests/kani/Intrinsics/Math/Arith/exp2.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `exp2f32` and `exp2f64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. #[kani::proof] fn verify_exp2_32() { diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs index deab02b6a713..303676a608f9 100644 --- a/tests/kani/Intrinsics/Math/Arith/log.rs +++ b/tests/kani/Intrinsics/Math/Arith/log.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `logf32` and `logf64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. #[kani::proof] fn verify_logf32() { diff --git a/tests/kani/Intrinsics/Math/Arith/powf32.rs b/tests/kani/Intrinsics/Math/Arith/powf32.rs index d67c0025c033..f289171b64b8 100644 --- a/tests/kani/Intrinsics/Math/Arith/powf32.rs +++ b/tests/kani/Intrinsics/Math/Arith/powf32.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `powf32` intrinsic, which in turn invoke functions modelled in +// CBMC's math library. These models use approximations as documented in CBMC's source code: +// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. #[kani::proof] fn verify_pow() { diff --git a/tests/kani/Intrinsics/Math/Arith/powf64.rs b/tests/kani/Intrinsics/Math/Arith/powf64.rs index 82b8fde8e49c..e80ad777c09a 100644 --- a/tests/kani/Intrinsics/Math/Arith/powf64.rs +++ b/tests/kani/Intrinsics/Math/Arith/powf64.rs @@ -1,5 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `powf64` intrinsic, which in turn invoke functions modelled in +// CBMC's math library. These models use approximations as documented in CBMC's source code: +// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. pub fn f(a: u64) -> u64 { const C: f64 = 0.618; From bc5ef1f2e833f3abe0a2aa054dc5b9156d4737bb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 18:22:45 +0000 Subject: [PATCH 14/14] More precise bounds --- tests/kani/Intrinsics/Math/Arith/exp.rs | 4 ++-- tests/kani/Intrinsics/Math/Arith/exp2.rs | 4 ++-- tests/kani/Intrinsics/Math/Arith/log.rs | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/kani/Intrinsics/Math/Arith/exp.rs b/tests/kani/Intrinsics/Math/Arith/exp.rs index 6f07f3b32dbe..4f26fc5b5b96 100644 --- a/tests/kani/Intrinsics/Math/Arith/exp.rs +++ b/tests/kani/Intrinsics/Math/Arith/exp.rs @@ -11,7 +11,7 @@ fn verify_exp32() { let two_sq = std::f32::consts::E * std::f32::consts::E; let two_exp = two.exp(); - assert!((two_sq - two_exp).abs() <= 1.0); + assert!((two_sq - two_exp).abs() <= 0.192); } #[kani::proof] @@ -20,5 +20,5 @@ fn verify_exp64() { let two_sq = std::f64::consts::E * std::f64::consts::E; let two_exp = two.exp(); - assert!((two_sq - two_exp).abs() <= 1.0); + assert!((two_sq - two_exp).abs() <= 0.192); } diff --git a/tests/kani/Intrinsics/Math/Arith/exp2.rs b/tests/kani/Intrinsics/Math/Arith/exp2.rs index b8e458171da7..91244a383a0a 100644 --- a/tests/kani/Intrinsics/Math/Arith/exp2.rs +++ b/tests/kani/Intrinsics/Math/Arith/exp2.rs @@ -10,7 +10,7 @@ fn verify_exp2_32() { let two = 2.0_f32; let two_two = two.exp2(); - assert!((two_two - 4.0).abs() <= 1.0); + assert!((two_two - 4.0).abs() <= 0.345); } #[kani::proof] @@ -18,5 +18,5 @@ fn verify_exp2_64() { let two = 2.0_f64; let two_two = two.exp2(); - assert!((two_two - 4.0).abs() <= 1.0); + assert!((two_two - 4.0).abs() <= 0.345); } diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs index 303676a608f9..1185e8ae4d82 100644 --- a/tests/kani/Intrinsics/Math/Arith/log.rs +++ b/tests/kani/Intrinsics/Math/Arith/log.rs @@ -10,7 +10,7 @@ fn verify_logf32() { let e = std::f32::consts::E; let e_log = e.ln(); - assert!((e_log - 1.0).abs() <= 0.1); + assert!((e_log - 1.0).abs() <= 0.058); } #[kani::proof] @@ -18,5 +18,5 @@ fn verify_logf64() { let e = std::f64::consts::E; let e_log = e.ln(); - assert!((e_log - 1.0).abs() <= 0.1); + assert!((e_log - 1.0).abs() <= 0.058); }