From deeb322e1da32b6adb69577c2feff2a0805d5468 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Mon, 3 Feb 2025 16:53:43 -0800 Subject: [PATCH 1/4] remove flag float-overflow-check Ref #3620 Removing default flag float overflow check, which reports overflow for arithmetic operations over floating-point numbers that result in +/-Inf. This doesn't panic in Rust and it shouldn't be consider a verification failure by default. Users can enable them using --cbmc-args as and when required. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/call_cbmc.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 4e10cb98c650..b6050d915666 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -233,7 +233,6 @@ impl KaniSession { args.push("--no-pointer-check".into()); } if self.args.checks.overflow_on() { - args.push("--float-overflow-check".into()); args.push("--nan-check".into()); // TODO: Implement conversion checks as an optional check. From 4aef8fc3af60bac19a8f4bd04fdd3eb7feb6b677 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Tue, 4 Feb 2025 15:11:06 -0800 Subject: [PATCH 2/4] added test to check float overflow. Handled NaN values and Div by zero err by adding bounds --- .../{expected => check_message.expected} | 0 .../float-overflow/check_message.rs | 1 + .../check_message_overflow.expected | 1 + .../float-overflow/check_message_overflow.rs | 23 +++++++++++++++++++ 4 files changed, 25 insertions(+) rename tests/ui/cbmc_checks/float-overflow/{expected => check_message.expected} (100%) create mode 100644 tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected create mode 100644 tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs diff --git a/tests/ui/cbmc_checks/float-overflow/expected b/tests/ui/cbmc_checks/float-overflow/check_message.expected similarity index 100% rename from tests/ui/cbmc_checks/float-overflow/expected rename to tests/ui/cbmc_checks/float-overflow/check_message.expected diff --git a/tests/ui/cbmc_checks/float-overflow/check_message.rs b/tests/ui/cbmc_checks/float-overflow/check_message.rs index 590a2be20230..229bc373a883 100644 --- a/tests/ui/cbmc_checks/float-overflow/check_message.rs +++ b/tests/ui/cbmc_checks/float-overflow/check_message.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // +// kani-flags: --enable-unstable --cbmc-args --float-overflow-check // Check we don't print temporary variables as part of CBMC messages. extern crate kani; diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs new file mode 100644 index 000000000000..b83c19616e83 --- /dev/null +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Check we don't print temporary variables as part of CBMC messages. +extern crate kani; + +use kani::any; + +// Use the result so rustc doesn't optimize them away. +fn dummy(result: f32) -> f32 { + result +} + +#[kani::proof] +fn main() { + let a = kani::any_where(|&x: &f32| x.is_finite() && x.abs() < 1e20); + let b = kani::any_where(|&x: &f32| x.is_finite() && x.abs() < 1e20); + + dummy(a + b); + dummy(a - b); + dummy(a * b); + dummy(-a); +} From 2a44655615762f0f45a101adffc6b07ccb494e96 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Tue, 4 Feb 2025 16:24:05 -0800 Subject: [PATCH 3/4] Update check_message_overflow.rs --- .../cbmc_checks/float-overflow/check_message_overflow.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs index b83c19616e83..44c4a5be0bc7 100644 --- a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs @@ -2,10 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // // Check we don't print temporary variables as part of CBMC messages. +// This test verifies that Kani does not report floating-point overflow by default +// for operations that result in +/-Infinity. extern crate kani; -use kani::any; - // Use the result so rustc doesn't optimize them away. fn dummy(result: f32) -> f32 { result @@ -13,8 +13,8 @@ fn dummy(result: f32) -> f32 { #[kani::proof] fn main() { - let a = kani::any_where(|&x: &f32| x.is_finite() && x.abs() < 1e20); - let b = kani::any_where(|&x: &f32| x.is_finite() && x.abs() < 1e20); + let a = kani::any_where(|&x: &f32| x.is_finite()); + let b = kani::any_where(|&x: &f32| x.is_finite()); dummy(a + b); dummy(a - b); From cd8e94ca88f3812a06c2ccba54af019b71114697 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal Date: Tue, 4 Feb 2025 21:59:52 -0800 Subject: [PATCH 4/4] remove comment --- tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs index 44c4a5be0bc7..5b57e4b4377d 100644 --- a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// Check we don't print temporary variables as part of CBMC messages. // This test verifies that Kani does not report floating-point overflow by default // for operations that result in +/-Infinity. extern crate kani;