From 2de456151aaba9a04410a8bb5411fdb156627b82 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 24 Dec 2024 08:40:05 +0100 Subject: [PATCH] show an error on some invalid flag combinations: TB + permissive provenance; strict provenance + native calls --- src/tools/miri/README.md | 6 +++-- src/tools/miri/src/bin/miri.rs | 22 +++++++++++++------ src/tools/miri/tests/pass/ptr_int_casts.rs | 5 +---- .../miri/tests/pass/ptr_int_from_exposed.rs | 5 +---- 4 files changed, 21 insertions(+), 17 deletions(-) diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index d3912b4c658..b4be061f493 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -347,8 +347,8 @@ environment variable. We first document the most relevant and most commonly used can increase test coverage by running Miri multiple times with different seeds. * `-Zmiri-strict-provenance` enables [strict provenance](https://github.com/rust-lang/rust/issues/95228) checking in Miri. This means that - casting an integer to a pointer yields a result with 'invalid' provenance, i.e., with provenance - that cannot be used for any memory access. + casting an integer to a pointer will stop execution because the provenance of the pointer + cannot be determined. * `-Zmiri-symbolic-alignment-check` makes the alignment check more strict. By default, alignment is checked by casting the pointer to an integer, and making sure that is a multiple of the alignment. This can lead to cases where a program passes the alignment check by pure chance, because things @@ -437,6 +437,8 @@ to Miri failing to detect cases of undefined behavior in a program. of Rust will be stricter than Tree Borrows. In other words, if you use Tree Borrows, even if your code is accepted today, it might be declared UB in the future. This is much less likely with Stacked Borrows. + Using Tree Borrows currently implies `-Zmiri-strict-provenance` because integer-to-pointer + casts are not supported in this mode, but that may change in the future. * `-Zmiri-force-page-size=` overrides the default page size for an architecture, in multiples of 1k. `4` is default for most targets. This value should always be a power of 2 and nonzero. * `-Zmiri-unique-is-unique` performs additional aliasing checks for `core::ptr::Unique` to ensure diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs index 6b6fa31c673..617270c5599 100644 --- a/src/tools/miri/src/bin/miri.rs +++ b/src/tools/miri/src/bin/miri.rs @@ -539,6 +539,7 @@ fn main() { miri_config.borrow_tracker = None; } else if arg == "-Zmiri-tree-borrows" { miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows); + miri_config.provenance_mode = ProvenanceMode::Strict; } else if arg == "-Zmiri-unique-is-unique" { miri_config.unique_is_unique = true; } else if arg == "-Zmiri-disable-data-race-detector" { @@ -728,13 +729,20 @@ fn main() { "-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used" ); } - // Tree Borrows + permissive provenance does not work. - if miri_config.provenance_mode == ProvenanceMode::Permissive - && matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows)) - { - show_error!( - "Tree Borrows does not support integer-to-pointer casts, and is hence not compatible with permissive provenance" - ); + // Tree Borrows implies strict provenance, and is not compatible with native calls. + if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows)) { + if miri_config.provenance_mode != ProvenanceMode::Strict { + show_error!( + "Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance" + ); + } + if miri_config.native_lib.is_some() { + show_error!("Tree Borrows is not compatible with calling native functions"); + } + } + // Native calls and strict provenance are not compatible. + if miri_config.native_lib.is_some() && miri_config.provenance_mode == ProvenanceMode::Strict { + show_error!("strict provenance is not compatible with calling native functions"); } // You can set either one seed or many. if many_seeds.is_some() && miri_config.seed.is_some() { diff --git a/src/tools/miri/tests/pass/ptr_int_casts.rs b/src/tools/miri/tests/pass/ptr_int_casts.rs index 4e274f62981..94391eac3b2 100644 --- a/src/tools/miri/tests/pass/ptr_int_casts.rs +++ b/src/tools/miri/tests/pass/ptr_int_casts.rs @@ -1,7 +1,4 @@ -//@revisions: stack tree -// Tree Borrows doesn't support int2ptr casts, but let's make sure we don't immediately crash either. -//@[tree]compile-flags: -Zmiri-tree-borrows -//@[stack]compile-flags: -Zmiri-permissive-provenance +//@compile-flags: -Zmiri-permissive-provenance use std::{mem, ptr}; fn eq_ref(x: &T, y: &T) -> bool { diff --git a/src/tools/miri/tests/pass/ptr_int_from_exposed.rs b/src/tools/miri/tests/pass/ptr_int_from_exposed.rs index 9a76c8dd349..98f8f15608e 100644 --- a/src/tools/miri/tests/pass/ptr_int_from_exposed.rs +++ b/src/tools/miri/tests/pass/ptr_int_from_exposed.rs @@ -1,7 +1,4 @@ -//@revisions: stack tree -// Tree Borrows doesn't support int2ptr casts, but let's make sure we don't immediately crash either. -//@[tree]compile-flags: -Zmiri-tree-borrows -//@[stack]compile-flags: -Zmiri-permissive-provenance +//@compile-flags: -Zmiri-permissive-provenance use std::ptr;