Skip to content

Commit 1744591

Browse files
authored
Disable debug_asserts inside std due to poor UX (rust-lang#1791)
This is a possible workaround for now to improve the UX around UB detection in intrinsics when using the MIR Linker. The issue is tracked here: model-checking/kani#1740 Basically, the rust toolchain uses a release build that removes all debug assertions from the standard library. When we switched to using our custom build of the `std` we decided to enable the debug assertions in order to catch more potential UBs. However, the UX is not always great. The assertions don't have any clear descriptions and they may fail in unexpected places. E.g.: The violation of an intrinsic safety condition triggers the following failures: ``` > Failed checks: Called `Option::unwrap()` on a `None` value ```
1 parent 4ae03e3 commit 1744591

File tree

7 files changed

+4
-23
lines changed

7 files changed

+4
-23
lines changed

tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,7 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
// kani-flags: --legacy-linker
43
//! Checks that `copy_nonoverlapping` triggers an overflow failure if the `count`
54
//! argument can overflow a `usize`
6-
//!
7-
//! When enabling "--mir-linker", the error we currently get is:
8-
//! > Failed checks: Called `Option::unwrap()` on a `None` value
9-
//! This happens because of std debug checks. The `is_nonoverlapping` check has a
10-
//! `checked_mul().unwrap()` that fails in the overflow scenario.
11-
//! See <https://github.com/model-checking/kani/issues/1740> for more details.
125
#[kani::proof]
136
fn test_copy_nonoverlapping_unaligned() {
147
let arr: [i32; 3] = [0, 1, 0];

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// kani-flags: --legacy-linker
5-
//! The MIR linker errors are not quite user friendly. For more details, see
6-
//! <https://github.com/model-checking/kani/issues/1740>
74
//! Checks that `copy_nonoverlapping` fails when `dst` is not aligned.
85
96
#[kani::proof]

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// kani-flags: --legacy-linker
5-
//! The MIR linker errors are not quite user friendly. For more details, see
6-
//! <https://github.com/model-checking/kani/issues/1740>
74
//! Checks that `copy_nonoverlapping` fails when `src` is not aligned.
85
#[kani::proof]
96
fn test_copy_nonoverlapping_unaligned() {

tests/expected/intrinsics/copy/copy-unaligned-dst/main.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// kani-flags: --legacy-linker
5-
//! The MIR linker errors are not quite user friendly. For more details, see
6-
//! <https://github.com/model-checking/kani/issues/1740>
74
//! Checks that `copy` fails when `dst` is not aligned.
85
#[kani::proof]
96
fn test_copy_unaligned() {

tests/expected/intrinsics/copy/copy-unaligned-src/main.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// kani-flags: --legacy-linker
5-
//! The MIR linker errors are not quite user friendly. For more details, see
6-
//! <https://github.com/model-checking/kani/issues/1740>
74
//! Checks that `copy` fails when `src` is not aligned.
85
#[kani::proof]
96
fn test_copy_unaligned() {

tests/expected/intrinsics/write_bytes/unaligned/main.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// kani-flags: --legacy-linker
5-
//! The MIR linker errors are not quite user friendly. For more details, see
6-
//! <https://github.com/model-checking/kani/issues/1740>
74
//! Checks that `write_bytes` fails when `dst` is not aligned.
85
//! This test is a modified version of the example in
96
//! https://doc.rust-lang.org/std/ptr/fn.write_bytes.html

tools/build-kani/src/sysroot.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,10 @@ pub fn build_lib() {
9393
"dev",
9494
"--config",
9595
"profile.dev.panic=\"abort\"",
96+
// Disable debug assertions for now as a mitigation for
97+
// https://github.com/model-checking/kani/issues/1740
98+
"--config",
99+
"profile.dev.debug-assertions=false",
96100
"--config",
97101
"host.rustflags=[\"--cfg=kani\"]",
98102
"--target",
@@ -126,7 +130,6 @@ pub fn build_lib() {
126130
cp_files(&kani_rlib_folder, &sysroot_lib, &is_rlib).unwrap();
127131

128132
// Copy `std` libraries and dependencies to sysroot folder following expected path format.
129-
// TODO: Create a macro for all these push.
130133
let src_path = path_buf!(target_folder, target, "debug", "deps");
131134

132135
let dst_path = path_buf!(sysroot_lib, "rustlib", target, "lib");

0 commit comments

Comments
 (0)