From 7a111dd234645b0a4aee56ec485940836f5379b9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 15:29:27 -0700 Subject: [PATCH 1/2] Change intrinsics tests to ensure the call is not removed by the compiler (#2552) The tests below started failing as part of the latest toolchain update because the value produced by intrinsics is not used, and the compiler just removes them. To avoid that to happen, we now wrap those calls with the black_box std function to avoid compiler optimizations. --- tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs | 3 ++- tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs | 3 ++- 9 files changed, 18 insertions(+), 9 deletions(-) diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs index 159f26842704..36708f9a5eca 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/add_fail.rs @@ -9,5 +9,6 @@ fn main() { let a: i32 = kani::any(); let b: i32 = kani::any(); - unsafe { std::intrinsics::unchecked_add(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_add(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs index ec5e2bd94279..973563bacce4 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/div_fail.rs @@ -10,5 +10,6 @@ fn main() { let a: i32 = i32::MIN; let b: i32 = -1; - unsafe { std::intrinsics::unchecked_div(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_div(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs index aac284a08e26..d1915505ed57 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/div_zero_fail.rs @@ -10,5 +10,6 @@ fn main() { let a: i32 = kani::any(); let b: i32 = 0; - unsafe { std::intrinsics::unchecked_div(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_div(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs index 3e703724fd67..7f6c60646510 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/mul_fail.rs @@ -9,5 +9,6 @@ fn main() { let a: i32 = kani::any(); let b: i32 = kani::any(); - unsafe { std::intrinsics::unchecked_mul(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_mul(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs index b2887a591174..5bed5ed6d346 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_fail.rs @@ -10,5 +10,6 @@ fn main() { let a: i32 = i32::MIN; let b: i32 = -1; - unsafe { std::intrinsics::unchecked_rem(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_rem(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs index eec7db57e123..0fbcb84865ae 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/rem_zero_fail.rs @@ -10,5 +10,6 @@ fn main() { let a: i32 = kani::any(); let b: i32 = 0; - unsafe { std::intrinsics::unchecked_rem(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_rem(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs index adc5e0a5dff4..a1f5b8dfaa56 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/shl_fail.rs @@ -9,5 +9,6 @@ fn main() { let a: u32 = kani::any(); let b: u32 = kani::any(); - unsafe { std::intrinsics::unchecked_shl(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_shl(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs index 77d1b44f91df..6bb68ff1f526 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/shr_fail.rs @@ -9,5 +9,6 @@ fn main() { let a: u32 = kani::any(); let b: u32 = kani::any(); - unsafe { std::intrinsics::unchecked_shr(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_shr(a, b) }); } diff --git a/tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs b/tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs index 695ae81f01e3..de5839b83ccf 100644 --- a/tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs +++ b/tests/kani/Intrinsics/Math/Arith/Unchecked/sub_fail.rs @@ -9,5 +9,6 @@ fn main() { let a: i32 = kani::any(); let b: i32 = kani::any(); - unsafe { std::intrinsics::unchecked_sub(a, b) }; + // Black box this so it doesn't get pruned by the compiler. + std::hint::black_box(unsafe { std::intrinsics::unchecked_sub(a, b) }); } From 43bc8904ba2c4f215fba261c11136e8d852bdb3d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 16:15:20 -0700 Subject: [PATCH 2/2] Fix flaky tests (#2553) This PR fixes a few flaky tests that started to fail in the ongoing toolchain update (#2551) - The object bits test itself doesn't create that many objects since an array is represented as the same allocated object. Use LinkedList instead. - Do not rely on property number. - Do not rely on the order that failed checks is printed. --- .../reserve_available_capacity_is_no_op.expected | 8 ++++---- tests/expected/object-bits/insufficient/main.rs | 12 ++++-------- .../should-panic-attribute/expected-panics/expected | 2 +- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected index 499ccc7008fc..1b18a4656c4f 100644 --- a/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected +++ b/tests/cargo-kani/vecdeque-cve/reserve_available_capacity_is_no_op.expected @@ -1,16 +1,16 @@ -fixed::VecDeque::::handle_capacity_increase.assertion.7\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.head < self.tail" -fixed::VecDeque::::handle_capacity_increase.assertion.8\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.head < self.cap()" -fixed::VecDeque::::handle_capacity_increase.assertion.9\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.tail < self.cap()" -fixed::VecDeque::::handle_capacity_increase.assertion.10\ +fixed::VecDeque::::handle_capacity_increase.assertion\ Status: UNREACHABLE\ Description: "assertion failed: self.cap().count_ones() == 1" diff --git a/tests/expected/object-bits/insufficient/main.rs b/tests/expected/object-bits/insufficient/main.rs index 310ef53667e5..4da74190cb21 100644 --- a/tests/expected/object-bits/insufficient/main.rs +++ b/tests/expected/object-bits/insufficient/main.rs @@ -1,15 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks for error message with an --object-bits value that is too small - // kani-flags: --default-unwind 30 --enable-unstable --cbmc-args --object-bits 5 +//! Checks for error message with an --object-bits value that is too small +//! Use linked list to ensure that each member represents a new object. #[kani::proof] fn main() { - let mut arr: [i32; 100] = kani::Arbitrary::any_array(); - for i in 0..30 { - arr[i] = kani::any(); - } - assert!(arr[0] > arr[0] - arr[99]); + let arr: [i32; 18] = kani::Arbitrary::any_array(); + std::hint::black_box(std::collections::LinkedList::from(arr)); } diff --git a/tests/ui/should-panic-attribute/expected-panics/expected b/tests/ui/should-panic-attribute/expected-panics/expected index c6a6fa5c6c48..855801a7c0df 100644 --- a/tests/ui/should-panic-attribute/expected-panics/expected +++ b/tests/ui/should-panic-attribute/expected-panics/expected @@ -1,4 +1,4 @@ - ** 2 of 2 failed\ + ** 2 of 2 failed Failed Checks: panicked on the `if` branch! Failed Checks: panicked on the `else` branch! VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)